From a77f2a7884d65677df4adf277b065d5574319ede Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 7 Sep 2026 08:22:58 +0200 Subject: [PATCH 1/3] [llm] LOAD -noproof: admit the prefix's lemmas instead of proving them Replaying a long file to reach one proof spends nearly all its time re-proving lemmas that were already verified. `-nosmt` only silences the provers; the elaboration of every tactic in the prefix remains. `LOAD "f.ec" LINE -noproof` skips the prefix's proofs whole. The mechanism is the one `require` already uses: a file is read with proof checking off, so `Ax.add` starts each lemma in `PSNoCheck`, its script is not even typed, and `qed` binds the statement as it stands. The one proof that must still be checked is the one LINE points inside -- seeing its goal state is the reason for stopping there. Which proof that is cannot be known when its opening sentence is read, so it is settled beforehand by a parse-only pass over the prefix (`target_proof`): EasyCrypt's grammar does not depend on the environment, and parsing is nothing next to proving. Checking goes back on at that sentence, so the goals LOAD reports are the true ones. On `theories/datatypes/List.ec` up to line 1487: 8.1s plain, 1.3s under `-nosmt`, 0.5s under `-noproof`, for byte-identical goals. Compared against a plain LOAD at the midpoint of all 77 stdlib theories, the goal state matches everywhere. The prefix is admitted, not proved, so replies carry a `[noproof]` tag: a successful load is no evidence that the file compiles. Skipping ends with the LOAD -- the mode is restored on every exit path, failures included -- so phrases typed afterwards are checked as usual. Two things the flag is careful about. A prefix holding an `undo` moves the engine in a way the parse-only pass cannot follow, so it is loaded with checking on throughout: slower, never wrong, and the missing tag says so. And a `fail tac.` inside a skipped proof pins an error that can no longer happen, the tactic not being run, so `process_action` gains `~nofail` to drop that verdict there -- without it `-noproof` failed on files that compile, `tests/bullets-errors.ec` among them. Plumbing: `EcScope.Prover.{get,set}_check_mode` read and write the mode as it is, which `check_proof` cannot (it is an `On`/`Off` toggle that ignores `Forced`), and `EcCommands.{check,set_check}_mode` apply it to the whole undo stack, so it behaves like a pragma rather than a scope the undo stack could take back. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014sRvA8imiFo9jSNLbPuX9W --- doc/llm/CLAUDE.md | 40 +++- src/ecCommands.ml | 21 ++ src/ecCommands.mli | 9 + src/ecLlm.ml | 38 ++-- src/ecLlmCore.ml | 202 ++++++++++++++++-- src/ecLlmCore.mli | 11 +- src/ecMcp.ml | 11 +- src/ecScope.ml | 21 ++ src/ecScope.mli | 13 ++ tests/llm/expected/load-noproof-checked.out | 19 ++ tests/llm/expected/load-noproof-undo.out | 8 + tests/llm/expected/load-noproof.out | 30 +++ tests/llm/fixtures/noproof.ec | 36 ++++ tests/llm/scripts/load-noproof-checked.script | 16 ++ tests/llm/scripts/load-noproof-undo.script | 11 + tests/llm/scripts/load-noproof.script | 11 + tests/mcp/expected/load-options.out | 3 +- tests/mcp/expected/tools-list.out | 2 +- tests/mcp/scripts/load-options.script | 12 +- 19 files changed, 469 insertions(+), 45 deletions(-) create mode 100644 tests/llm/expected/load-noproof-checked.out create mode 100644 tests/llm/expected/load-noproof-undo.out create mode 100644 tests/llm/expected/load-noproof.out create mode 100644 tests/llm/fixtures/noproof.ec create mode 100644 tests/llm/scripts/load-noproof-checked.script create mode 100644 tests/llm/scripts/load-noproof-undo.script create mode 100644 tests/llm/scripts/load-noproof.script diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index d5681c31b..05478a94e 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -89,7 +89,7 @@ These are protocol-level commands, not EasyCrypt syntax: | Command | Description | |---------|-------------| -| `LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]` | Reset state, compile file (optionally skip SMT or trace last sentence) | +| `LOAD "file.ec" [LINE[:COL]] [-nosmt] [-noproof] [-trace]` | Reset state, compile file (optionally weaken SMT, skip the prefix's proofs, or trace the last sentence) | | `UNDO` | Undo the last proof step | | `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | | `GOALS` | Print the current goal (first subgoal only, with remaining count) | @@ -167,6 +167,40 @@ compilation (safe when the prefix was already verified): LOAD "myfile.ec" 436 -nosmt ``` +`-noproof` goes further and skips the prefix's **proofs** altogether: + +``` +LOAD "myfile.ec" 436 -noproof +``` + +Every lemma before the target is admitted on its statement alone — its +script is not run, not even typed — exactly as a `require`d file's +lemmas are. The one exception is the proof line 436 falls inside: that +one is replayed for real, so the goal state you land on is the true +one. Positions outside any proof skip the whole file. + +This is the fastest way into a proof in a long file, and it is a large +margin: replaying `theories/datatypes/List.ec` up to line 1487 takes +around 8s plainly, 1.3s under `-nosmt` and 0.5s under `-noproof`, for +byte-identical goals. `-nosmt` only silences the provers; `-noproof` +also skips the elaboration of every tactic in the prefix, which is +where the rest of the time goes. + +What you give up is any assurance about the prefix: a `-noproof` load +succeeds on a file whose earlier proofs are broken, so it is no +evidence that the file compiles. Replies say so — the tag carries +`[noproof]`: + +``` +OK [uuid:1295] [loaded:myfile.ec:436] [noproof] [focus: 1/2] +``` + +Skipping ends with the LOAD. Whatever you type next is checked +normally, and so is anything you `COMMIT` and put back in the file. A +prefix holding an `undo` is loaded with checking on throughout — the +flag is then silently a no-op, which the missing `[noproof]` tag +reports. + Add `-trace` to a LOAD to inspect the proof state around the last loaded sentence. The reply body contains four delimited blocks: @@ -371,7 +405,7 @@ noted. | Tool | Arguments | Description | |------|-----------|-------------| -| `ec_load` | `file` (req), `line`, `col`, `nosmt` (false), `trace` (false) | Reset the session and compile `file` from the top, stopping after the last sentence that ends on or before `line` | +| `ec_load` | `file` (req), `line`, `col`, `nosmt` (false), `noproof` (false), `trace` (false) | Reset the session and compile `file` from the top, stopping after the last sentence that ends on or before `line` | | `ec_step` | `phrase` (req) | Run EasyCrypt sentences — tactics, declarations, `require`, `print`, ... — against the current session | | `ec_try` | `phrase` (req) | Like `ec_step`, but roll the engine back to its pre-call state whenever a sentence fails | | `ec_goals` | `all` (false) | Print the focused subgoal, or, with `all`, every open subgoal | @@ -385,7 +419,7 @@ noted. `tools/list` carries a fuller, agent-facing `description` and a JSON Schema for every tool; those are the authoritative texts. The tools -mirror the REPL meta-commands — `-nosmt`, `-trace`, dotted paths, +mirror the REPL meta-commands — `-nosmt`, `-noproof`, `-trace`, dotted paths, checkpoints, bullets and search patterns all behave exactly as described above, and `NEXT` folds into `ec_focus` with path `"next"` — plus `ec_try`, which has no REPL equivalent. The meta-commands that are diff --git a/src/ecCommands.ml b/src/ecCommands.ml index ea78d5048..54af3b7bf 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1135,6 +1135,27 @@ let apply_pragma_option (x : string) = else if n > 1 && x.[0] = '-' then setflag (String.sub x 1 (n - 1)) false else apply_pragma x +(* -------------------------------------------------------------------- *) +(* Proof checking on/off, on the *current* scope. Reading and writing it + is how LOAD skips the proofs it was asked to skip: [`Off] is the mode + a [require]d file is already read in, so the lemmas it declares are + admitted as they stand. Both the current scope and the root are + updated, so the setting survives the undo stack the way a pragma + does -- an [undo] back into the skipped region must not resurrect a + checking mode the caller has since turned off. *) +let check_mode () : EcScope.Prover.check_mode = + EcScope.Prover.get_check_mode (oget !context).ct_current + +let set_check_mode (mode : EcScope.Prover.check_mode) = + let ct = oget !context in + context := Some { ct with + ct_current = EcScope.Prover.set_check_mode ct.ct_current mode; + ct_root = EcScope.Prover.set_check_mode ct.ct_root mode; + ct_stack = + Option.map + (List.map (fun sc -> EcScope.Prover.set_check_mode sc mode)) + ct.ct_stack; } + (* -------------------------------------------------------------------- *) let uuid () : int = (oget !context).ct_level diff --git a/src/ecCommands.mli b/src/ecCommands.mli index d4daa6ff9..9ec71478e 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -83,6 +83,15 @@ val undo_restore : undo_mark -> unit val uuid : unit -> int val mode : unit -> string +(* Whether the proofs of the lemmas the engine reads from here on are + checked. [`Off] admits every lemma as an axiom -- its proof script is + skipped whole, not even typed -- which is the mode a [require]d file + is already read in; see [EcScope.Prover.check_mode]. The setting is + applied to the whole undo stack, so it behaves like a pragma rather + than like a scope the undo stack could take back. *) +val check_mode : unit -> EcScope.Prover.check_mode +val set_check_mode : EcScope.Prover.check_mode -> unit + val check_eco : string -> bool val doc_comment : [`Global | `Item] * string -> unit diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 60d2302d5..69078f63c 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -85,10 +85,11 @@ module Parse = struct | Blank and load = { - ld_file : string; - ld_upto : (int * int option) option; - ld_nosmt : bool; - ld_trace : bool; + ld_file : string; + ld_upto : (int * int option) option; + ld_nosmt : bool; + ld_noproof : bool; + ld_trace : bool; } exception Parse_error of string @@ -135,10 +136,11 @@ module Parse = struct in Search query - (* LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]. Argument errors are - signalled with [failwith] and turned into [Parse_error] below, so - they reach the wire exactly as any other line-parse error does - (including the bare "int_of_string" of a malformed LINE:COL). *) + (* LOAD "file.ec" [LINE[:COL]] [-nosmt] [-noproof] [-trace]. + Argument errors are signalled with [failwith] and turned into + [Parse_error] below, so they reach the wire exactly as any other + line-parse error does (including the bare "int_of_string" of a + malformed LINE:COL). *) let parse_load args = try let args = String.strip args in @@ -171,17 +173,20 @@ module Parse = struct | Ok () -> () | Error msg -> failwith msg); - (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) - let upto, nosmt, trace = + (* Parse optional LINE[:COL] and flags (-nosmt, -noproof, + -trace). *) + let upto, nosmt, noproof, trace = let words = String.split_on_char ' ' rest |> List.filter (fun s -> s <> "") in - let nosmt = List.mem "-nosmt" words in - let trace = List.mem "-trace" words in + let nosmt = List.mem "-nosmt" words in + let noproof = List.mem "-noproof" words in + let trace = List.mem "-trace" words in let words = List.filter - (fun s -> s <> "-nosmt" && s <> "-trace") + (fun s -> + s <> "-nosmt" && s <> "-noproof" && s <> "-trace") words in let upto = match words with @@ -196,10 +201,10 @@ module Parse = struct end | _ -> failwith "LOAD: unexpected arguments" in - (upto, nosmt, trace) + (upto, nosmt, noproof, trace) in - Load { ld_file = filename; ld_upto = upto; - ld_nosmt = nosmt; ld_trace = trace; } + Load { ld_file = filename; ld_upto = upto; ld_nosmt = nosmt; + ld_noproof = noproof; ld_trace = trace; } with Failure msg -> raise (Parse_error msg) let of_line ~multi_active (raw : string) : command = @@ -386,6 +391,7 @@ let run ~relocdir ~boot ~projini (llmopts : EcOptions.llm_option) = ~file:args.Parse.ld_file ~upto:args.Parse.ld_upto ~nosmt:args.Parse.ld_nosmt + ~noproof:args.Parse.ld_noproof ~trace:args.Parse.ld_trace) | Ec input -> Wire.answer (EcLlmCore.step st input) | Begin_multi -> do_begin_multi () diff --git a/src/ecLlmCore.ml b/src/ecLlmCore.ml index 0a65abf01..9ededcaf7 100644 --- a/src/ecLlmCore.ml +++ b/src/ecLlmCore.ml @@ -421,8 +421,15 @@ let reset_session (st : state) : unit = (* Process a single EasyCrypt command, respecting [gl_fail]. When [~record:true], append a transcript entry on success: the parent handle (focused goal before the phrase) and the open-handle list, - which together let [Commit] reconstruct bullet structure. *) -let process_action (st : state) ?(record=false) ~src (p : EP.global) = + which together let [Commit] reconstruct bullet structure. + + [~nofail:true] drops the [gl_fail] verdict -- the sentence is still + run, and a failure is still swallowed, but succeeding is no longer + an error. LOAD -noproof sets it inside a proof it is skipping: there + the tactic is not run at all, so it cannot fail, and a `fail tac.' + the file wrote to pin an error would otherwise fail the load. *) +let process_action (st : state) ?(record=false) ?(nofail=false) ~src + (p : EP.global) = let transcript = st.transcript in let loc = p.EP.gl_action.EcLocation.pl_loc in let pre_uuid = EcCommands.uuid () in @@ -454,7 +461,7 @@ let process_action (st : state) ?(record=false) ~src (p : EP.global) = spend a uuid, or REVERT targets and the MCP [readOnlyHint] would both be lying. A no-op when the query failed (nothing was pushed). *) if is_query then EcCommands.undo pre_uuid; - if !succeeded && p.EP.gl_fail then + if !succeeded && p.EP.gl_fail && not nofail then raise (EcScope.toperror_of_exn ~gloc:loc (EcScope.HiScopeError (None, "this command is expected to fail"))); @@ -871,11 +878,98 @@ let try_step (st : state) input = reverted = true; changed = uuid <> pre; }) +(* -------------------------------------------------------------------- *) +(* Is [loc] beyond the position LOAD was asked to stop at? [None] as + [upto] means "no bound": load the whole file. A sentence counts as + in-prefix when it *ends* on or before the bound, so LOAD always stops + on a sentence boundary. *) +let past_upto ~upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.EcLocation.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + +(* -------------------------------------------------------------------- *) +(* LOAD -noproof: which proof, if any, is the one the caller is aiming + at. + + Skipping the proofs of a prefix is what [require] already does: it + reads a file with proof checking off, so every lemma is admitted as + it stands (see [EcScope.Prover.check_mode]). The one proof that must + still be checked is the one [upto] points *inside* -- seeing its goal + state is the whole reason for stopping there. + + Which proof that is cannot be known when its opening sentence is + read, so it is settled beforehand, by a parse-only pass over the + prefix: EasyCrypt's grammar does not depend on the environment, and + parsing is nothing next to proving. The pass returns the location of + the sentence that opened the proof still open at [upto]. + + Only two forms leave a proof open across sentences: a [lemma] with no + inline proof, and a [realize] with none. [lemma ... by tac], [clone + ... with proof] and [instance] each open and close within their own + sentence, and a [clone] leaving proof obligations behind opens no + goal until the [realize] that discharges one. [Gsave] -- [qed], + [admitted], [abort] -- closes. + + [`Unsupported] is the safe answer: the caller then loads with + checking on throughout, which is slower and never wrong. It is + returned for a prefix holding an [undo], whose effect on the sentence + stream this pass cannot replay without executing it, and for a prefix + that does not parse -- the real load reports that error, in its own + words and at its own point. *) +let target_proof (filename : string) ~upto + : [`None | `At of EcLocation.t | `Unsupported] += + let reader = EcIo.from_file filename in + let opened = ref `None in + let exception Stop in + + let visit (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto ~upto loc then raise Stop; + match EcLocation.unloc p.EP.gl_action with + | EP.Gaxiom { EP.pa_kind = EP.PLemma None; _ } -> + opened := `At loc + | EP.Grealize { EcLocation.pl_desc = { EP.pr_proof = None; _ }; _ } -> + opened := `At loc + | EP.Gsave _ -> + opened := `None + | _ -> () + in + + let result = + try + while true do + let (_, prog) = EcIo.xparse reader in + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter visit commands; + if locterm then raise Stop + | EP.P_Undo _ -> + if past_upto ~upto (EcLocation.loc prog) then raise Stop; + opened := `Unsupported; raise Stop + | EP.P_Exit -> + raise Stop + | EP.P_DocComment _ -> () + done; + `None + with + | Stop | End_of_file -> !opened + | _ -> `Unsupported + in + + EcIo.finalize reader; result + (* -------------------------------------------------------------------- *) (* LOAD: run [file] up to [upto], optionally with SMT calls weakened - ([nosmt]) or with the last sentence of the prefix traced. The - argument string is parsed by the front-end. *) -let load (st : state) ~file ~upto ~nosmt ~trace = + ([nosmt]), the proofs of the prefix skipped altogether ([noproof]) + or the last sentence of the prefix traced. The argument string is + parsed by the front-end. *) +let load (st : state) ~file ~upto ~nosmt ~noproof ~trace = let notices = st.notices in let cur_prvopts = st.cur_prvopts in let pre = EcCommands.uuid () in @@ -884,6 +978,10 @@ let load (st : state) ~file ~upto ~nosmt ~trace = let last_src = ref "" in let trace_prefix = ref "" in let exception Trace_failed of exn in + (* Set once -noproof has turned proof checking off, so the handlers + below -- which are outside the scope of that state -- can put it + back however the load ends. *) + let cleanup = ref (fun () -> ()) in try begin try @@ -920,16 +1018,74 @@ let load (st : state) ~file ~upto ~nosmt ~trace = EcCommands.addidir (Filename.dirname filename); EcCommands.set_current_path (Filename.dirname filename); + (* -noproof: read the prefix the way a [require] is read, with + proof checking off, so every lemma it declares is admitted as it + stands. The proof [upto] falls inside -- if it falls inside one + -- is the exception: checking goes back on at the sentence that + opens it, and its script is replayed for real, which is what + makes the goal state at [upto] the true one. + + The mode is read *after* [reset_session]: that call rebuilds the + engine's scope from scratch, so a mode sampled before it would + describe a scope that no longer exists. It is put back on every + way out, failures included: the session goes on after LOAD, and + phrases typed into it are checked. *) + let saved_check = EcCommands.check_mode () in + let skipping = ref false in + let check_back_at = ref None in + (* Idempotent, and called on every exit path: leaving the engine in + [`Off] would silently admit whatever the session is fed next. *) + let restore_check () = + if !skipping then begin + skipping := false; + check_back_at := None; + EcCommands.set_check_mode saved_check + end + in + + if noproof then begin + let skip loc = + skipping := true; + check_back_at := loc; + EcCommands.set_check_mode `Off + in + cleanup := restore_check; + match target_proof filename ~upto with + | `Unsupported -> () + | `None -> skip None + | `At loc -> skip (Some loc) + end; + let reader = EcIo.from_file filename in - let past_upto (loc : EcLocation.t) = - match upto with - | None -> false - | Some (line, col) -> - let (el, ec) = loc.loc_end in - el > line || (el = line && match col with - | None -> false - | Some c -> ec > c) + let past_upto (loc : EcLocation.t) = past_upto ~upto loc in + + (* Every sentence of the prefix goes through here, so that the + switch back to checked proofs happens when the target sentence is + *run*, not when it is read: under -trace the last sentence of the + prefix is deferred, and the two moments are not the same one. The + test is [>=] rather than an equality on locations so that a + target somehow stepped over still turns checking back on. *) + let run_action ~src (p : EP.global) = + begin match !check_back_at with + | Some (tloc : EcLocation.t) + when p.EP.gl_action.EcLocation.pl_loc.EcLocation.loc_bchar + >= tloc.EcLocation.loc_bchar -> + EcCommands.set_check_mode saved_check; + check_back_at := None + | _ -> () + end; + (* A [fail tac.] inside a proof whose script is being skipped + pins an error that cannot happen any more, the tactic not + being run: honour it and the load fails on a file that + compiles. Outside a proof the sentence is executed for real, + so its verdict still holds. *) + let nofail = + p.EP.gl_fail + && EcCommands.check_mode () = `Off + && EcCommands.in_proof () + in + process_action st ~nofail ~src p in (* [upto] stops the prefix at the requested position whatever kind @@ -969,7 +1125,7 @@ let load (st : state) ~file ~upto ~nosmt ~trace = | None -> () | Some (src, p) -> last_src := src; - process_action st ~src p; + run_action ~src p; last_loc := Some p.EP.gl_action.EcLocation.pl_loc; pending := None in @@ -981,7 +1137,7 @@ let load (st : state) ~file ~upto ~nosmt ~trace = pending := Some (src, p) end else begin last_src := src; - process_action st ~src p; + run_action ~src p; last_loc := Some loc end in @@ -1010,12 +1166,16 @@ let load (st : state) ~file ~upto ~nosmt ~trace = | e -> EcIo.finalize reader; if nosmt then EcCommands.pragma_check `Check; + restore_check (); raise e end; EcIo.finalize reader; if nosmt then EcCommands.pragma_check `Check; + (* Kept for the tag below: [restore_check] clears [skipping]. *) + let did_skip = !skipping in + restore_check (); (* If -trace is set, the last in-prefix sentence is still pending. Run it under goal capture and build the @@ -1060,7 +1220,7 @@ let load (st : state) ~file ~upto ~nosmt ~trace = last_src := src; begin try - process_action st ~src p; + run_action ~src p; last_loc := Some loc; pending := None; let after_goals = EcCommands.pp_all_goals () in @@ -1115,7 +1275,10 @@ let load (st : state) ~file ~upto ~nosmt ~trace = let (el, _) = loc.EcLocation.loc_end in Printf.sprintf " [loaded:%s:%d]" filename el in - loaded ^ Goals.focus_tag () + (* The prefix is admitted, not proved: say so, so that a + successful LOAD is not read as a verification of the file. *) + let skipped = if did_skip then " [noproof]" else "" in + loaded ^ skipped ^ Goals.focus_tag () in Ok (mk_reply st ~pre ~tag (Text body)) @@ -1124,11 +1287,14 @@ let load (st : state) ~file ~upto ~nosmt ~trace = reset_session st; Ok (mk_reply st ~pre (Text "Session restarted")) | Trace_failed e -> + !cleanup (); let msg = Goals.format_error ~src:!last_src e in Error (mk_failure st ~pre (!trace_prefix ^ msg)) | Failure s -> + !cleanup (); Error (mk_failure st ~pre s) | e -> + !cleanup (); Error (mk_failure st ~pre (Goals.format_error ~src:!last_src e)) (* -------------------------------------------------------------------- *) diff --git a/src/ecLlmCore.mli b/src/ecLlmCore.mli index 4a9a92e2f..5df8e88c0 100644 --- a/src/ecLlmCore.mli +++ b/src/ecLlmCore.mli @@ -73,12 +73,21 @@ val create : (* -------------------------------------------------------------------- *) (* Operations. *) -(* LOAD, on already-parsed arguments. *) +(* LOAD, on already-parsed arguments. + + [noproof] reads the prefix the way a [require]d file is read: proof + checking off, so every lemma is admitted on its statement and its + script is skipped whole -- not even typed. The proof [upto] points + inside, if any, is the exception; checking goes back on for it, so + the goal state LOAD reports is the real one. The reply is tagged + [[noproof]] whenever proofs were skipped, a successful load of an + unverified prefix being no evidence about the file. *) val load : state -> file:string -> upto:(int * int option) option -> nosmt:bool + -> noproof:bool -> trace:bool -> (reply, failure) result diff --git a/src/ecMcp.ml b/src/ecMcp.ml index c1fc0f2d8..d799a6eff 100644 --- a/src/ecMcp.ml +++ b/src/ecMcp.ml @@ -228,6 +228,10 @@ let tools : J.t list = loaded file, and tactics need the position to land inside a \ proof. Set nosmt to weaken SMT calls while replaying a prefix \ that was already verified, which is much faster on large files. \ + Set noproof to go further and skip the prefix's proofs \ + altogether, admitting every lemma before the target on its \ + statement alone -- only the proof the position lands inside is \ + replayed, which is the fastest way into a proof in a long file. \ Set trace to have the reply describe the last loaded sentence as \ BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports \ where compilation stopped and the resulting goal state; note the \ @@ -245,6 +249,10 @@ let tools : J.t list = ("nosmt", Schema.bool ~description:"weaken SMT calls while compiling the \ prefix" ~default:false ()); + ("noproof", Schema.bool + ~description:"skip the prefix's proofs entirely, \ + admitting the lemmas before the \ + target as axioms" ~default:false ()); ("trace", Schema.bool ~description:"report the proof state around the last \ loaded sentence" ~default:false ()); @@ -649,6 +657,7 @@ let run ~relocdir ~boot ~projini (mcpopts : EcOptions.mcp_option) = let line = Args.int_opt name args "line" in let col = Args.int_opt name args "col" in let nosmt = Args.bool_opt name args "nosmt" ~default:false in + let noprf = Args.bool_opt name args "noproof" ~default:false in let trace = Args.bool_opt name args "trace" ~default:false in if line = None && col <> None then raise (Invalid_params "ec_load: `col' requires `line'"); @@ -656,7 +665,7 @@ let run ~relocdir ~boot ~projini (mcpopts : EcOptions.mcp_option) = | Ok () -> () | Error msg -> raise (Tool_error msg)); let upto = Option.map (fun line -> (line, col)) line in - outcome (EcLlmCore.load st ~file ~upto ~nosmt ~trace) + outcome (EcLlmCore.load st ~file ~upto ~nosmt ~noproof:noprf ~trace) | "ec_step" -> answer (EcLlmCore.step st (Args.string_req name args "phrase")) diff --git a/src/ecScope.ml b/src/ecScope.ml index 0e99b1aae..672772913 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -216,6 +216,18 @@ module Check_mode = struct let set_fullcheck options = GenOptions.set options oid (Check `Forced) + + (* Unconditional read/write of the mode, for a caller that wants to + turn checking off and later put back exactly what was there. + [set_checkproof] cannot do it: it is a toggle between [`On] and + [`Off] and silently ignores [`Forced]. *) + let get options = + match GenOptions.get options oid with + | Check mode -> mode + | _ -> `On + + let set options (mode : mode) = + GenOptions.set options oid (Check mode) end (* -------------------------------------------------------------------- *) @@ -786,6 +798,15 @@ module Prover = struct (* -------------------------------------------------------------------- *) let check_proof scope b = { scope with sc_options = Check_mode.set_checkproof scope.sc_options b } + + (* -------------------------------------------------------------------- *) + type check_mode = Check_mode.mode + + let get_check_mode scope = + Check_mode.get scope.sc_options + + let set_check_mode scope (mode : check_mode) = + { scope with sc_options = Check_mode.set scope.sc_options mode } end (* -------------------------------------------------------------------- *) diff --git a/src/ecScope.mli b/src/ecScope.mli index 5aeae3e3b..08c5a020c 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -269,6 +269,19 @@ module Prover : sig val full_check : scope -> scope val check_proof : scope -> bool -> scope + (* Whether lemma proofs are checked in this scope. [`Off] makes every + lemma an axiom: [Ax.add] starts it in [PSNoCheck], its proof script + is not even typed, and [qed] binds the statement as it stands. This + is the mode a [require]d file is read in ([`Forced] is the [-check- + all] override that survives that switch). Unlike [check_proof], + which is a toggle that ignores [`Forced], these two read and write + the mode as it is, so a caller can turn checking off for a while + and then restore exactly what was in force. *) + type check_mode = [`Off | `On | `Forced] + + val get_check_mode : scope -> check_mode + val set_check_mode : scope -> check_mode -> scope + val pprover_infos_to_prover_infos : EcEnv.env -> EcProvers.prover_infos diff --git a/tests/llm/expected/load-noproof-checked.out b/tests/llm/expected/load-noproof-checked.out new file mode 100644 index 000000000..1cfd33fcf --- /dev/null +++ b/tests/llm/expected/load-noproof-checked.out @@ -0,0 +1,19 @@ +READY [uuid:0] + +OK [uuid:27] [loaded:fixtures/noproof.ec:36] [noproof] +added lemma: `first_and' +added lemma: `second_and' +added lemma: `third_and' +added lemma: `target_and' +No active proof. + +ERROR [uuid:30] +: line 1 (40-44): cannot save an incomplete proof +source: qed. +Current goal + +Type variables: + +------------------------------------------------------------------------ +false + diff --git a/tests/llm/expected/load-noproof-undo.out b/tests/llm/expected/load-noproof-undo.out new file mode 100644 index 000000000..4337ddb08 --- /dev/null +++ b/tests/llm/expected/load-noproof-undo.out @@ -0,0 +1,8 @@ +READY [uuid:0] + +OK [uuid:4] [loaded:fixtures/undoafter.ec:10] +No more goals + +OK [uuid:4] +No more goals + diff --git a/tests/llm/expected/load-noproof.out b/tests/llm/expected/load-noproof.out new file mode 100644 index 000000000..3a05aa911 --- /dev/null +++ b/tests/llm/expected/load-noproof.out @@ -0,0 +1,30 @@ +READY [uuid:0] + +OK [uuid:23] [loaded:fixtures/noproof.ec:32] [noproof] [focus: 1/3] +added lemma: `first_and' +added lemma: `second_and' +added lemma: `third_and' +Current goal (remaining: 3) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:23] [focus: 1/3] + [1.1] 1 = 1 <- focused + [1.2] 2 = 2 +[2] 3 = 3 + +OK [uuid:23] [focus: 1/3] +* In [lemmas or axioms]: + +lemma first_and: 1 = 1 /\ 2 = 2. + +Current goal (remaining: 3) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + diff --git a/tests/llm/fixtures/noproof.ec b/tests/llm/fixtures/noproof.ec new file mode 100644 index 000000000..8d01255ae --- /dev/null +++ b/tests/llm/fixtures/noproof.ec @@ -0,0 +1,36 @@ +(* Three lemmas whose proofs `LOAD -noproof' skips -- each is admitted + on its statement alone -- and a fourth one the LOAD position lands + inside, whose script is replayed for real. `first_and' is the one + the scripts `print' afterwards, to show a skipped lemma is bound and + usable all the same. *) +require import AllCore. + +lemma first_and : 1 = 1 /\ 2 = 2. +proof. +split. +trivial. +trivial. +qed. + +lemma second_and : 3 = 3 /\ 4 = 4. +proof. +split. +trivial. +trivial. +qed. + +lemma third_and : 5 = 5 /\ 6 = 6. +proof. +split. +trivial. +trivial. +qed. + +lemma target_and : (1 = 1 /\ 2 = 2) /\ 3 = 3. +proof. +split. +split. +trivial. +trivial. +trivial. +qed. diff --git a/tests/llm/scripts/load-noproof-checked.script b/tests/llm/scripts/load-noproof-checked.script new file mode 100644 index 000000000..f8806b103 --- /dev/null +++ b/tests/llm/scripts/load-noproof-checked.script @@ -0,0 +1,16 @@ +# exit: 1 +# Two properties of -noproof past the prefix it skipped. +# +# First, a position outside any proof (the whole file here) skips every +# proof in it: the reply is tagged [noproof] and leaves no active proof. +# +# Second, skipping ends with the LOAD. Proof checking is restored on +# the way out, so the phrase typed next is checked for real and its +# `qed.' is refused -- which is what makes the exit status 1. +LOAD "fixtures/noproof.ec" -noproof + +lemma unproved : false. +proof. +trivial. +qed. + diff --git a/tests/llm/scripts/load-noproof-undo.script b/tests/llm/scripts/load-noproof-undo.script new file mode 100644 index 000000000..202072f0a --- /dev/null +++ b/tests/llm/scripts/load-noproof-undo.script @@ -0,0 +1,11 @@ +# exit: 0 +# -noproof gives up rather than guess. Deciding which proof to replay +# is a parse-only pass over the prefix, and an `undo' in it moves the +# engine in a way that pass cannot follow without running the file. So +# a prefix holding one is loaded with checking on throughout: slower, +# never wrong. The tell is the reply tag, which carries no [noproof] +# here -- `fixtures/undoafter.ec' has an `undo 3.' on line 9, and +# stopping at line 10 puts it inside the prefix. `load-upto-undo' pins +# the same file stopping short of the `undo'. +LOAD "fixtures/undoafter.ec" 10 -noproof +GOALS diff --git a/tests/llm/scripts/load-noproof.script b/tests/llm/scripts/load-noproof.script new file mode 100644 index 000000000..9cb6b0d2b --- /dev/null +++ b/tests/llm/scripts/load-noproof.script @@ -0,0 +1,11 @@ +# exit: 0 +# -noproof admits every lemma before the target on its statement alone +# and replays only the proof the position lands inside. Line 32 is the +# second `split.' of `target_and', so the goals here are exactly the +# ones `load-goals'-style plain LOAD reports at that line -- run the +# same LOAD without the flag to see it. The reply tag carries +# [noproof], and `print first_and' shows a skipped lemma is bound and +# usable like any other. +LOAD "fixtures/noproof.ec" 32 -noproof +TREE +print first_and. diff --git a/tests/mcp/expected/load-options.out b/tests/mcp/expected/load-options.out index 4e14c5854..52b680e81 100644 --- a/tests/mcp/expected/load-options.out +++ b/tests/mcp/expected/load-options.out @@ -1,3 +1,4 @@ {"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} {"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} -{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"=== BEFORE: line 8 (col 0) ===\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n\n=== TACTIC (lines 8:0 - 8:6) ===\nsplit.\n\n=== AFTER: line 8 (col 0) ===\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n\n\n=== SUMMARY ===\nopen goals: 1 -> 2\n"}],"structuredContent":{"text":"=== BEFORE: line 8 (col 0) ===\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n\n=== TACTIC (lines 8:0 - 8:6) ===\nsplit.\n\n=== AFTER: line 8 (col 0) ===\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n\n\n=== SUMMARY ===\nopen goals: 1 -> 2\n","uuid":4,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"added lemma: `first_and'\nadded lemma: `second_and'\nadded lemma: `third_and'\nCurrent goal (remaining: 3)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"added lemma: `first_and'\nadded lemma: `second_and'\nadded lemma: `third_and'\nCurrent goal (remaining: 3)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":23,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":"=== BEFORE: line 8 (col 0) ===\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n\n=== TACTIC (lines 8:0 - 8:6) ===\nsplit.\n\n=== AFTER: line 8 (col 0) ===\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n\n\n=== SUMMARY ===\nopen goals: 1 -> 2\n"}],"structuredContent":{"text":"=== BEFORE: line 8 (col 0) ===\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n\n=== TACTIC (lines 8:0 - 8:6) ===\nsplit.\n\n=== AFTER: line 8 (col 0) ===\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n\n\n=== SUMMARY ===\nopen goals: 1 -> 2\n","uuid":4,"changed":true},"isError":false}} diff --git a/tests/mcp/expected/tools-list.out b/tests/mcp/expected/tools-list.out index 7e4b76bd3..0c20d43a4 100644 --- a/tests/mcp/expected/tools-list.out +++ b/tests/mcp/expected/tools-list.out @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"tools":[{"name":"ec_load","description":"Reset the session and compile FILE from the top, stopping after the last sentence that ends on or before LINE (and column COL when given). This is the entry point: every other tool needs a loaded file, and tactics need the position to land inside a proof. Set nosmt to weaken SMT calls while replaying a prefix that was already verified, which is much faster on large files. Set trace to have the reply describe the last loaded sentence as BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports where compilation stopped and the resulting goal state; note the uuid it returns, reverting to it is the instant way back to the start of the proof.","inputSchema":{"type":"object","properties":{"file":{"type":"string","description":"path to the .ec/.eca file"},"line":{"type":"integer","description":"stop after the last sentence ending on or before this line; omit to compile the whole file"},"col":{"type":"integer","description":"column bound within `line'; requires `line'"},"nosmt":{"type":"boolean","description":"weaken SMT calls while compiling the prefix","default":false},"trace":{"type":"boolean","description":"report the proof state around the last loaded sentence","default":false}},"required":["file"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_step","description":"Run EasyCrypt sentences -- tactics, declarations, require, print, ... -- against the current session. Every complete sentence in the argument is executed, in order, exactly as if the text had been appended to the source file, and a single reply describes the state they leave behind; sentences may span several lines. Requires a file loaded with ec_load, and, for tactics, an open proof. On success the reply carries the new goal state; on failure the prover's error text comes back with isError set, the sentences before the failing one stay applied and the engine is left wherever that sentence left it -- use ec_try when you want a guaranteed rollback. Successful non-query phrases are recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one or more complete EasyCrypt sentences, each ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false,"idempotentHint":false}},{"name":"ec_try","description":"Like ec_step, but the engine is rolled back to the state it had before the call whenever a sentence fails, including input that failed only after having already advanced the proof. The failure reply sets structuredContent.reverted to true, and its uuid and goal text describe the restored state, not the point of failure. Use this to probe a tactic without having to ec_revert afterwards; use ec_step when you mean to keep whatever progress the phrase makes. A successful phrase behaves exactly as under ec_step and is recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one complete EasyCrypt sentence, ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"},"reverted":{"type":"boolean","description":"set when the phrase failed and the engine was rolled back to its pre-call state"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_goals","description":"Print the current proof state: the focused subgoal alone, or, with all set, every open subgoal. Requires an open proof, and does not advance the engine.","inputSchema":{"type":"object","properties":{"all":{"type":"boolean","description":"print every open subgoal instead of the focused one","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_tree","description":"List the open subgoals as a tree of dotted-path labels -- [1], [1.2], [2.1.1] -- showing how the splits nest, and marking the focused one. Those labels are exactly what ec_focus accepts. Set full for whole goal bodies rather than one-line conclusions. The labels are not stable across focus changes: the tree always shows the focused goal first, so re-read it after every ec_focus. Does not advance the engine.","inputSchema":{"type":"object","properties":{"full":{"type":"boolean","description":"print full goal bodies instead of one-line conclusions","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_focus","description":"Rotate the focus onto the subgoal at dotted path PATH, as printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"). The path walks the tree, one component per level, so a single integer selects the k-th TOP-LEVEL node -- not the k-th open goal: with four goals nested under two top-level nodes, \"3\" is out of range. Selecting a node that is an internal frame rather than a leaf goal is an error. The special value \"next\" is a different operation, not a synonym for \"2\": it moves to the next open subgoal in ec_goals-with-all order, whatever the nesting, and the two coincide only when the tree is flat. Subsequent tactics act on the focused goal.","inputSchema":{"type":"object","properties":{"path":{"type":"string","description":"\"N\", a dotted path \"N1.N2...\", or \"next\""}},"required":["path"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_undo","description":"Undo the last engine step, returning to the immediately preceding state. The ec_commit transcript is trimmed to match. Fails when there is nothing left to undo.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_revert","description":"Return the session to an earlier state, named either by a uuid reported in some previous structuredContent or by a name given to ec_checkpoint. Reverting is instant, unlike re-running ec_load, so going back to the uuid ec_load returned is the cheap way to restart a proof from scratch after a failed experiment. The ec_commit transcript is trimmed to match.","inputSchema":{"type":"object","properties":{"target":{"type":"string","description":"a uuid (as a decimal string) or a checkpoint name"}},"required":["target"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_checkpoint","description":"Record the current uuid under NAME, so that ec_revert can address it by name later. Worth doing before a branching experiment, when carrying the bare uuid around is awkward. Does not change the proof state.","inputSchema":{"type":"object","properties":{"name":{"type":"string","description":"checkpoint name"}},"required":["name"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_commit","description":"Emit the phrases recorded since the last ec_load as a proof body, with bullets inserted at every multi-child split: the result compiles under `pragma +strict_bullets' and can be pasted straight into the source file. Queries (search, print, locate, ec_search) are never recorded, so looking things up mid-proof does not pollute the body, and ec_undo / ec_revert trim the transcript. Still works after `qed.'. Does not change the proof state.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_search","description":"Search the environment for lemmas matching an EasyCrypt search pattern. This is pattern syntax, not keyword search: use _ as the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ <= _)\". Requires a loaded file. The query neither advances the proof nor enters the ec_commit transcript.","inputSchema":{"type":"object","properties":{"pattern":{"type":"string","description":"an EasyCrypt search pattern"}},"required":["pattern"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}}]}} +{"jsonrpc":"2.0","id":1,"result":{"tools":[{"name":"ec_load","description":"Reset the session and compile FILE from the top, stopping after the last sentence that ends on or before LINE (and column COL when given). This is the entry point: every other tool needs a loaded file, and tactics need the position to land inside a proof. Set nosmt to weaken SMT calls while replaying a prefix that was already verified, which is much faster on large files. Set noproof to go further and skip the prefix's proofs altogether, admitting every lemma before the target on its statement alone -- only the proof the position lands inside is replayed, which is the fastest way into a proof in a long file. Set trace to have the reply describe the last loaded sentence as BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports where compilation stopped and the resulting goal state; note the uuid it returns, reverting to it is the instant way back to the start of the proof.","inputSchema":{"type":"object","properties":{"file":{"type":"string","description":"path to the .ec/.eca file"},"line":{"type":"integer","description":"stop after the last sentence ending on or before this line; omit to compile the whole file"},"col":{"type":"integer","description":"column bound within `line'; requires `line'"},"nosmt":{"type":"boolean","description":"weaken SMT calls while compiling the prefix","default":false},"noproof":{"type":"boolean","description":"skip the prefix's proofs entirely, admitting the lemmas before the target as axioms","default":false},"trace":{"type":"boolean","description":"report the proof state around the last loaded sentence","default":false}},"required":["file"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_step","description":"Run EasyCrypt sentences -- tactics, declarations, require, print, ... -- against the current session. Every complete sentence in the argument is executed, in order, exactly as if the text had been appended to the source file, and a single reply describes the state they leave behind; sentences may span several lines. Requires a file loaded with ec_load, and, for tactics, an open proof. On success the reply carries the new goal state; on failure the prover's error text comes back with isError set, the sentences before the failing one stay applied and the engine is left wherever that sentence left it -- use ec_try when you want a guaranteed rollback. Successful non-query phrases are recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one or more complete EasyCrypt sentences, each ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false,"idempotentHint":false}},{"name":"ec_try","description":"Like ec_step, but the engine is rolled back to the state it had before the call whenever a sentence fails, including input that failed only after having already advanced the proof. The failure reply sets structuredContent.reverted to true, and its uuid and goal text describe the restored state, not the point of failure. Use this to probe a tactic without having to ec_revert afterwards; use ec_step when you mean to keep whatever progress the phrase makes. A successful phrase behaves exactly as under ec_step and is recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one complete EasyCrypt sentence, ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"},"reverted":{"type":"boolean","description":"set when the phrase failed and the engine was rolled back to its pre-call state"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_goals","description":"Print the current proof state: the focused subgoal alone, or, with all set, every open subgoal. Requires an open proof, and does not advance the engine.","inputSchema":{"type":"object","properties":{"all":{"type":"boolean","description":"print every open subgoal instead of the focused one","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_tree","description":"List the open subgoals as a tree of dotted-path labels -- [1], [1.2], [2.1.1] -- showing how the splits nest, and marking the focused one. Those labels are exactly what ec_focus accepts. Set full for whole goal bodies rather than one-line conclusions. The labels are not stable across focus changes: the tree always shows the focused goal first, so re-read it after every ec_focus. Does not advance the engine.","inputSchema":{"type":"object","properties":{"full":{"type":"boolean","description":"print full goal bodies instead of one-line conclusions","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_focus","description":"Rotate the focus onto the subgoal at dotted path PATH, as printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"). The path walks the tree, one component per level, so a single integer selects the k-th TOP-LEVEL node -- not the k-th open goal: with four goals nested under two top-level nodes, \"3\" is out of range. Selecting a node that is an internal frame rather than a leaf goal is an error. The special value \"next\" is a different operation, not a synonym for \"2\": it moves to the next open subgoal in ec_goals-with-all order, whatever the nesting, and the two coincide only when the tree is flat. Subsequent tactics act on the focused goal.","inputSchema":{"type":"object","properties":{"path":{"type":"string","description":"\"N\", a dotted path \"N1.N2...\", or \"next\""}},"required":["path"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_undo","description":"Undo the last engine step, returning to the immediately preceding state. The ec_commit transcript is trimmed to match. Fails when there is nothing left to undo.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_revert","description":"Return the session to an earlier state, named either by a uuid reported in some previous structuredContent or by a name given to ec_checkpoint. Reverting is instant, unlike re-running ec_load, so going back to the uuid ec_load returned is the cheap way to restart a proof from scratch after a failed experiment. The ec_commit transcript is trimmed to match.","inputSchema":{"type":"object","properties":{"target":{"type":"string","description":"a uuid (as a decimal string) or a checkpoint name"}},"required":["target"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_checkpoint","description":"Record the current uuid under NAME, so that ec_revert can address it by name later. Worth doing before a branching experiment, when carrying the bare uuid around is awkward. Does not change the proof state.","inputSchema":{"type":"object","properties":{"name":{"type":"string","description":"checkpoint name"}},"required":["name"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_commit","description":"Emit the phrases recorded since the last ec_load as a proof body, with bullets inserted at every multi-child split: the result compiles under `pragma +strict_bullets' and can be pasted straight into the source file. Queries (search, print, locate, ec_search) are never recorded, so looking things up mid-proof does not pollute the body, and ec_undo / ec_revert trim the transcript. Still works after `qed.'. Does not change the proof state.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_search","description":"Search the environment for lemmas matching an EasyCrypt search pattern. This is pattern syntax, not keyword search: use _ as the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ <= _)\". Requires a loaded file. The query neither advances the proof nor enters the ec_commit transcript.","inputSchema":{"type":"object","properties":{"pattern":{"type":"string","description":"an EasyCrypt search pattern"}},"required":["pattern"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}}]}} diff --git a/tests/mcp/scripts/load-options.script b/tests/mcp/scripts/load-options.script index 7c47ca671..e4c7ce178 100644 --- a/tests/mcp/scripts/load-options.script +++ b/tests/mcp/scripts/load-options.script @@ -1,10 +1,14 @@ # exit: 0 -# The two ec_load options that change what the engine does, which the +# The three ec_load options that change what the engine does, which the # other scenarios never set. `nosmt' weakens SMT calls while replaying -# the prefix; `trace' has the reply describe the last loaded sentence +# the prefix; `noproof' skips the prefix's proofs whole, admitting the +# lemmas before the target and replaying only the proof the position +# lands inside; `trace' has the reply describe the last loaded sentence # as BEFORE/TACTIC/AFTER/SUMMARY instead of just showing the goals. -# The REPL side of both is tests/llm's load-nosmt and load-trace. +# The REPL side of the three is tests/llm's load-nosmt, load-noproof +# and load-trace. {"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} {"jsonrpc":"2.0","method":"notifications/initialized"} {"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6,"nosmt":true}}} -{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/midproof.ec","trace":true}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/noproof.ec","line":32,"noproof":true}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/midproof.ec","trace":true}}} From f017b9c0e4eb5a476cce90cf380adcc225779738 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 7 Sep 2026 11:20:30 +0200 Subject: [PATCH 2/3] [llm] keep elaborated theories across a LOAD, so reloading is cheap What a LOAD costs is almost never the file. On mediummem.ec, a 470-line development over the Jasmin libraries, loading into the last proof takes 33s of which 30s is `require': `require import Goldbach.' alone is 49s, `Sieve' 33s, and the file's own body is milliseconds. None of it is proofs -- a required file is already read with checking off -- so neither -nosmt nor -noproof can touch it, and .eco is no help either, being a record of digests rather than a compiled theory. EcScope declines to read a theory twice: `Theory.require' consults the scope's `sc_loaded' before it runs a loader. But that table is part of the scope, and LOAD rebuilds the scope from nothing on every call, so every reload started from an empty one. The theories are now kept outside the scope as well, in `EcCommands.ThCache', and a rebuilt scope is seeded from it. Four alternating LOADs of memory_pool.ec and mediummem.ec go from 83.7s to 37.4s; a second LOAD of mediummem.ec at line 470 goes from 33s to 2s under -noproof -nosmt, and that 2s is the target proof being replayed, nothing else. A kept theory must never outlive its source. An entry is served only while the file it was read from digests to what it did then and every theory it required is served too, so an edit five requires down invalidates everything above it -- checking the closure, not the file, is the point. The include path is the other half of the key, since under a different one a name may name another file; a rebuild that starts from a different one drops the table whole rather than reason about which names moved. That is narrower than it sounds: `addidir' ignores a directory already searched, so loading file after file of one project keeps everything, which is what a session does. LOAD therefore adds the loaded file's own directory to the include path *before* it rebuilds the session rather than after: added after, it sat outside the key, and two files of the same name in two directories were served each other's theories. The `shadowed' scenario below caught exactly that. The cache is off unless a front-end asks for it, and only the LLM REPL and the MCP server do. The batch compiler reads each file once per process, so it has nothing to gain and no reason to carry the risk. `Theory.require' also bumps the prelude snapshot on the path that takes a theory from `sc_loaded', as the loading path always has: nothing reached that path during the prelude before, and a seeded table does -- without it `for_loading' rewound to a prelude that had never been recorded. Checked three ways. Every one of the 128 stdlib theories, loaded to its midpoint and then reloaded in the same session, gives byte- identical replies. `tests/llm/scripts/warm-reload.script' freezes both halves of such a pair, so a cache that ever showed on the wire would diff. And `scripts/testing/llm-warm-reload' drives the REPL over stdin -- which a -eval script cannot do, the edit having to land between two LOADs of one session -- to check that a warm session answers what a cold process answers after an edit to a required file, an edit to a file reached only through another, and an include path that changes so a name resolves elsewhere. Both new tests pass against the binary from before this commit too: they pin the contract the cache had to meet, not its presence. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Y2YZRRxpC8R1Ho2NGpD1fg --- Makefile | 3 + doc/llm/CLAUDE.md | 32 ++++ scripts/testing/llm-warm-reload | 216 +++++++++++++++++++++++++++ src/ecCommands.ml | 123 +++++++++++++++ src/ecCommands.mli | 11 ++ src/ecLlmCore.ml | 17 ++- src/ecScope.ml | 32 +++- src/ecScope.mli | 21 +++ tests/llm/README.md | 30 +++- tests/llm/expected/warm-reload.out | 44 ++++++ tests/llm/fixtures/sub/reload.ec | 10 ++ tests/llm/scripts/warm-reload.script | 13 ++ 12 files changed, 549 insertions(+), 3 deletions(-) create mode 100755 scripts/testing/llm-warm-reload create mode 100644 tests/llm/expected/warm-reload.out create mode 100644 tests/llm/fixtures/sub/reload.ec create mode 100644 tests/llm/scripts/warm-reload.script diff --git a/Makefile b/Makefile index a6b5b0ed1..64a8467d8 100644 --- a/Makefile +++ b/Makefile @@ -13,6 +13,8 @@ CHECK += $(foreach arg,$(ECARGS),--bin-args="$(arg)") CHECK += $(ECEXTRA) config/tests.config LLMCHECK := scripts/testing/llm-golden LLMCHECK += --bin=./ec.native +LLMWARM := scripts/testing/llm-warm-reload +LLMWARM += --bin=./ec.native MCPCHECK := scripts/testing/mcp-golden MCPCHECK += --bin=./ec.native MCPPARITY := scripts/testing/mcp-parity @@ -58,6 +60,7 @@ examples: build test-llm: build $(LLMCHECK) + $(LLMWARM) test-mcp: build $(MCPCHECK) diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 05478a94e..69022c938 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -201,6 +201,38 @@ prefix holding an `undo` is loaded with checking on throughout — the flag is then silently a no-op, which the missing `[noproof]` tag reports. +**Reloading is much cheaper than loading.** What a LOAD costs is +almost never the file: it is the theories the file `require`s, read +from source because nothing used to keep them from one LOAD to the +next. A session keeps them now, so the second LOAD and every one after +it skip that work. On a 470-line development over the Jasmin +libraries, a LOAD into the last proof went from 33s every time to 33s +once and then 2s — and that 2s is the target proof being replayed, +nothing else. + +So stay in one session and reload freely. Editing the file and +LOADing it again is a normal move now, not the expensive one; after an +edit it is often simpler than reverting to a checkpoint, and it is the +only way to see the edit at all, a session holding the file as it was +read. + +Edits are noticed. A theory is kept only while the file it came from, +and every file below it, is byte-for-byte what it was when it was +read; change any of them and it is read again. A LOAD after an edit +therefore shows the edit, whether you edited the file being loaded, a +theory it requires, or a theory five requires down. Changing the +include path starts over likewise, so nothing is ever served across +two developments that happen to name a theory the same way. That is +narrower than it sounds: a directory the session has already searched +is not a change, so loading file after file of one project — which is +what a session does — keeps everything. + +What none of this makes cheap is `require`ing a file that does not +compile: a file that fails produces no theory to keep, so a session +whose dependency is mid-edit pays for it on every LOAD. Worth knowing +when a reload that should be instant is not — the file below is +probably failing. + Add `-trace` to a LOAD to inspect the proof state around the last loaded sentence. The reply body contains four delimited blocks: diff --git a/scripts/testing/llm-warm-reload b/scripts/testing/llm-warm-reload new file mode 100755 index 000000000..33eb5c64d --- /dev/null +++ b/scripts/testing/llm-warm-reload @@ -0,0 +1,216 @@ +#! /usr/bin/env python3 + +# -------------------------------------------------------------------- +# The theory cache the interactive front-ends run with (EcCommands' +# ThCache) keeps elaborated theories across the scope rebuild a LOAD +# does, so that reloading a file does not re-read everything it +# requires. What it must never do is serve a theory the sources no +# longer describe, and that cannot be checked from a `-eval' script: +# the file has to change *between* two LOADs of one session. So this +# harness drives the REPL over stdin instead. +# +# llm-warm-reload [--bin PATH] [-v] +# +# Four scenarios, on a fixture tree written into a temporary +# directory. Each asserts the same invariant, which is the whole +# contract of the cache: a warm session answers exactly what a cold +# process answers on the same sources, byte for byte. +# +# quiet no edit at all -- the reload the cache exists for +# direct a required file is edited +# deep a file required only through another one is edited +# shadowed the include path changes so a name resolves elsewhere +# +# The edited scenarios also assert the answer *moved*: an invariant +# that only says "warm equals cold" is satisfied by a session that +# reports the same stale thing a cold process would, and a fixture +# whose edit is invisible would pass while testing nothing. +# -------------------------------------------------------------------- + +import argparse +import os +import shutil +import subprocess +import sys +import tempfile + +# -------------------------------------------------------------------- +BASE = """require import AllCore. +op k : int = %s. +""" + +MID = """require import AllCore Base. +op m : int = k + 1. +""" + +TOP = """require import AllCore Mid. + +lemma target : m = k + 1. +proof. +rewrite /m. +trivial. +qed. +""" + +# `Mid' as the shadowing directory writes it: same theory, other body. +MID_SHADOW = """require import AllCore Base. +op m : int = k + 99. +""" + + +# -------------------------------------------------------------------- +class Session: + """A `llm' REPL driven over stdin, one command at a time.""" + + def __init__(self, binary, cwd): + self.p = subprocess.Popen( + [binary, 'llm'], cwd=cwd, text=True, bufsize=1, + stdin=subprocess.PIPE, stdout=subprocess.PIPE, + stderr=subprocess.DEVNULL) + self.reply() # the READY frame + + def reply(self): + out = [] + while True: + line = self.p.stdout.readline() + if line == '': + raise SystemExit('llm-warm-reload: the engine died') + if line.rstrip('\n') == '': + return ''.join(out) + out.append(line) + + def send(self, command): + self.p.stdin.write(command + '\n') + self.p.stdin.flush() + return self.reply() + + def quit(self): + self.p.stdin.write('QUIT\n') + self.p.stdin.flush() + self.p.wait() + + +# What a session is asked, in every scenario: reload the file, then +# look at the two theories under it -- one required directly, one only +# through the other. +def probe(session, entry='Top.ec'): + return (session.send('LOAD "%s" 5' % entry) + + session.send('print Base.k.') + + session.send('print Mid.m.')) + + +def cold(binary, cwd, entry='Top.ec'): + session = Session(binary, cwd) + answer = probe(session, entry) + session.quit() + return answer + + +# -------------------------------------------------------------------- +def scenario(binary, root, name, verbose): + cwd = os.path.join(root, name) + os.makedirs(cwd) + for (path, text) in [('Base.ec', BASE % '1'), ('Mid.ec', MID), + ('Top.ec', TOP)]: + with open(os.path.join(cwd, path), 'w') as stream: + stream.write(text) + + entry = 'Top.ec' + session = Session(binary, cwd) + before = probe(session) + + if name == 'quiet': + pass + + elif name == 'direct': + # Mid.ec is required by Top.ec itself. + with open(os.path.join(cwd, 'Mid.ec'), 'w') as stream: + stream.write(MID.replace('k + 1', 'k + 5')) + + elif name == 'deep': + # Base.ec is not named by Top.ec at all: it is reached through + # Mid.ec, so serving it from the cache means having decided + # that Mid.ec's own dependencies still hold. + with open(os.path.join(cwd, 'Base.ec'), 'w') as stream: + stream.write(BASE % '42') + + elif name == 'shadowed': + # No file changes: the *include path* does, and under the new + # one `Mid' is another file. Nothing digests differently, so + # only dropping the table on a load-path change gets this + # right. + other = os.path.join(cwd, 'other') + os.makedirs(other) + for (path, text) in [('Base.ec', BASE % '1'), + ('Mid.ec', MID_SHADOW), ('Top.ec', TOP)]: + with open(os.path.join(other, path), 'w') as stream: + stream.write(text) + entry = os.path.join('other', 'Top.ec') + + after = probe(session, entry) + session.quit() + + reference = cold(binary, cwd, entry) + + ok = True + if after != reference: + ok = False + print('FAIL %s (warm session and cold process disagree)' % name) + for line in _diff(reference, after): + print(' ' + line) + if name != 'quiet' and after == before: + ok = False + print('FAIL %s (the change is invisible: the fixture tests ' + 'nothing)' % name) + if name == 'quiet' and after != before: + ok = False + print('FAIL %s (an untouched reload moved)' % name) + for line in _diff(before, after): + print(' ' + line) + + if ok: + print('PASS %s' % name) + if verbose: + for line in after.split('\n'): + print(' ' + line) + return ok + + +def _diff(want, got): + import difflib + return list(difflib.unified_diff( + want.split('\n'), got.split('\n'), + fromfile='cold', tofile='warm', lineterm='')) + + +# -------------------------------------------------------------------- +def main(): + here = os.path.dirname(os.path.abspath(__file__)) + root = os.path.dirname(os.path.dirname(here)) + parser = argparse.ArgumentParser() + parser.add_argument( + '--bin', default=os.path.join(root, '_build/default/src/ec.exe')) + parser.add_argument('-v', '--verbose', action='store_true') + args = parser.parse_args() + + binary = os.path.abspath(args.bin) + if not os.access(binary, os.X_OK): + print('llm-warm-reload: no such executable: %s' % binary, + file=sys.stderr) + return 2 + + tmp = tempfile.mkdtemp(prefix='llm-warm-reload.') + try: + results = [scenario(binary, tmp, name, args.verbose) + for name in ['quiet', 'direct', 'deep', 'shadowed']] + finally: + shutil.rmtree(tmp, ignore_errors=True) + + print('----') + print('%d passed, %d failed' + % (results.count(True), results.count(False))) + return 0 if all(results) else 1 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 54af3b7bf..c2125f7b5 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -232,6 +232,122 @@ end (* -------------------------------------------------------------------- *) type loader = Loader.loader +(* -------------------------------------------------------------------- *) +(* Elaborated theories, kept across the scope rebuilds a reload does. + + [EcScope] already declines to read a theory twice: [Theory.require] + consults the scope's [sc_loaded] before it runs a loader. But that + table is part of the scope, and a front-end that reloads a file by + rebuilding the scope from nothing -- the LLM REPL's LOAD, [pragma + restart.] -- starts from an empty one and re-reads every theory the + file requires. On a development of any size that *is* the reload: on + the goldbach sources, [require import Goldbach.] alone is 49s where + the file's own 470 lines are milliseconds, and none of it is proofs + ([require] already reads with checking off, which is the same + mechanism LOAD -noproof borrows). + + So the theories are kept here as well, outside the scope, and a + rebuilt scope is seeded with the ones the sources still describe. + Still describe is decided by digest, transitively: a theory is + served from here only if the file it was read from digests to what + it did then, and if every theory it required is served too -- an + edit to a file five requires down invalidates everything above it, + which is the whole point of checking the closure rather than the + file. The load path is the other half of the key, since under a + different one the same name may name a different file; rather than + work out which names moved, a reload that starts from a different + load path drops the table whole. + + Off unless a front-end asks for it. The batch compiler reads each + file once, in a process of its own, so it has nothing to gain here + and no reason to carry the risk of an entry that outlives its + source. *) +module ThCache : sig + val enable : unit -> unit + + (* Take the theory [ri] names out of [scope], which must be the scope + [Theory.require] returned for it, and file it under [file]. *) + val record : file:string -> EcScope.required_info -> EcScope.scope -> unit + + (* Seed a freshly built scope with the entries that are still good + under [loadpath]. Both stamps are taken at the same point of a + reload, so they compare. *) + val seed : + loadpath:((Loader.namespace option * string) * Loader.idx_t) list + -> EcScope.scope -> EcScope.scope +end = struct + type entry = { + ce_file : string; (* the file the theory was read from *) + ce_digest : Digest.t; (* ... and its digest, as read *) + ce_deps : EcScope.required; (* the theories reading it required *) + ce_th : EcScope.thloaded; + } + + let enabled : bool ref = ref false + + let table : (EcSymbols.symbol, entry) Hashtbl.t = Hashtbl.create 97 + + let stamp : + (((Loader.namespace option * string) * Loader.idx_t) list) option ref = + ref None + + let enable () = enabled := true + + let record ~(file : string) (ri : EcScope.required_info) scope = + if !enabled then + EcScope.Theory.loaded scope ri.EcScope.rqd_name + |> oiter (fun (th, deps) -> + Hashtbl.replace table ri.EcScope.rqd_name + { ce_file = file; + ce_digest = ri.EcScope.rqd_digest; + ce_deps = deps; + ce_th = th; }) + + (* Drop the entries the sources have moved out from under, and return + the names of those left. The recursion is memoized, and answers + [false] for a name it is still deciding: requires are acyclic + ([process_th_require1] refuses a cycle), and a cycle that got in + all the same must not be served. *) + let prune () = + let verdict : (EcSymbols.symbol, bool) Hashtbl.t = Hashtbl.create 97 in + + let rec live (name : EcSymbols.symbol) = + match Hashtbl.find_opt verdict name with + | Some b -> b + | None -> + Hashtbl.replace verdict name false; + let b = + match Hashtbl.find_opt table name with + | None -> false + | Some e -> + (try Digest.file e.ce_file = e.ce_digest + with Sys_error _ -> false) + && List.for_all + (fun (d : EcScope.required_info) -> live d.EcScope.rqd_name) + e.ce_deps + in Hashtbl.replace verdict name b; b + in + + let names = Hashtbl.fold (fun name _ acc -> name :: acc) table [] in + let (keep, drop) = List.partition live names in + List.iter (Hashtbl.remove table) drop; + keep + + let seed ~loadpath scope = + if not !enabled then scope else begin + if !stamp <> Some loadpath then Hashtbl.reset table; + stamp := Some loadpath; + EcScope.Theory.seed_loaded scope + (List.map + (fun name -> + let e = Hashtbl.find table name in + (name, (e.ce_th, e.ce_deps))) + (prune ())) + end +end + +let enable_theory_cache = ThCache.enable + (* -------------------------------------------------------------------- *) let process_search scope qs = EcScope.Search.search scope qs @@ -658,6 +774,7 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) = in let scope = EcScope.Theory.require scope (name, kind) loader in + ThCache.record ~file:filename name scope; match io with | None -> scope | Some `Export -> EcScope.Theory.export scope ([], name.EcScope.rqd_name) @@ -976,12 +1093,18 @@ let initial ~checkmode ~boot ~checkproof = EcScope.Prover.po_quorum = checkmode.cm_quorum; } in + (* Taken before [loader] is shadowed by its system-only view below: + the stamp the cache is keyed on is the whole include path, which + is what a reload of a file from another project changes. *) + let lpstamp = Loader.aslist loader in + let perv = (None, (mk_loc _dummy EcCoreLib.i_Pervasive, None), Some `Export) in let tactics = (None, (mk_loc _dummy "Tactics", None), Some `Export) in let prelude = (None, (mk_loc _dummy "Logic", None), Some `Export) in let loader = Loader.forsys loader in let gstate = EcGState.from_flags [("profile", profile)] in let scope = EcScope.empty gstate in + let scope = ThCache.seed ~loadpath:lpstamp scope in let scope = process_th_require1 loader scope perv in let scope = if boot then scope else List.fold_left (process_th_require1 loader) diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 9ec71478e..d0248408e 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -22,6 +22,17 @@ type loadpath_mark val loadpath_mark : unit -> loadpath_mark val loadpath_reset : loadpath_mark -> unit +(* Keep the theories a [require] elaborates across the scope rebuilds + [initialize ~restart:true] does, so that reloading a file does not + re-read everything it requires -- which, on a development of any + size, is what a reload costs. An entry is reused only while the file + it came from, and every file below it, digests to what it did when + it was read; a rebuild that starts from a different include path + drops the lot. Off until this is called, and there is no way back: + the batch compiler reads each file once per process and has nothing + to gain, the interactive front-ends reload all day. *) +val enable_theory_cache : unit -> unit + (* -------------------------------------------------------------------- *) type notifier = EcGState.loglevel -> string Lazy.t -> unit diff --git a/src/ecLlmCore.ml b/src/ecLlmCore.ml index 9ededcaf7..65a32d07e 100644 --- a/src/ecLlmCore.ml +++ b/src/ecLlmCore.ml @@ -175,6 +175,12 @@ let create ~relocdir ~boot ~projini ~prvopts = messages, [search] and [locate] included, already arrive. *) EcCommands.set_print_formatter (Format.formatter_of_buffer st.notices); + (* A session reloads: LOAD rebuilds the scope on every call, and so + does [pragma restart.]. Without this each one re-reads every + theory the file requires, which is nearly all of what a LOAD + costs. *) + EcCommands.enable_theory_cache (); + do_initialize st; st (* -------------------------------------------------------------------- *) @@ -1014,10 +1020,19 @@ let load (st : state) ~file ~upto ~nosmt ~noproof ~trace = ~recursive:isrec dir) (EcOptions.ini_loadpath ini); - reset_session st; + (* The file's own directory joins the include path *before* the + session is rebuilt, not after. The theory cache is keyed on the + include path as it stands at the rebuild -- change it and a name + may resolve to another file, so the cache is dropped -- and the + directory being loaded from is exactly the part of it that a + LOAD of a file elsewhere changes. Added afterwards, it would sit + outside the key, and two files of the same name in two + directories would be served each other's theories. *) EcCommands.addidir (Filename.dirname filename); EcCommands.set_current_path (Filename.dirname filename); + reset_session st; + (* -noproof: read the prefix the way a [require] is read, with proof checking off, so every lemma it declares is admitted as it stands. The proof [upto] falls inside -- if it falls inside one diff --git a/src/ecScope.ml b/src/ecScope.ml index 672772913..b195821d5 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2061,6 +2061,31 @@ module Theory = struct Msym.add ri.rqd_name (oget cth, rqs) new_.sc_loaded; } in bump_prelude (require_loaded ri scope) + (* The elaborated theories this scope holds, and the seeding of a + fresh scope with theories elaborated in an earlier one. + + [sc_loaded] is what spares a session the cost of reading a theory + twice: [require] consults it before it runs a loader. It is per + scope, so it dies with the scope -- and a front-end that rebuilds + the scope to reload a file (the LLM REPL's LOAD does) pays every + [require] again, which on a development of any size is the whole + cost of the reload. These two let a caller carry the table across + that rebuild. Whether the theories are still the ones the files on + disk describe is the caller's to answer: nothing here re-reads a + file, and [seed] believes what it is given. *) + let loaded (scope : scope) (name : symbol) : (thloaded * required) option = + Msym.find_opt name scope.sc_loaded + + let seed_loaded (scope : scope) + (entries : (symbol * (thloaded * required)) list) : scope + = + assert (scope.sc_pr_uc = None); + let sc_loaded = + List.fold_left + (fun loaded (name, entry) -> Msym.add name entry loaded) + scope.sc_loaded entries + in { scope with sc_loaded } + let require (scope : scope) ((name, mode) : required_info * thmode) loader = assert (scope.sc_pr_uc = None); @@ -2070,7 +2095,12 @@ module Theory = struct else scope end else match Msym.find_opt name.rqd_name scope.sc_loaded with - | Some _ -> require_loaded name scope + (* [bump_prelude], as on the loading path below: while the scope + is still the prelude's, every require it takes has to move the + snapshot [for_loading] later rewinds to. The loading path has + always done it, this one never had to -- nothing reached it + during the prelude -- and a seeded [sc_loaded] does. *) + | Some _ -> bump_prelude (require_loaded name scope) | None -> try let imported = require_start scope name.rqd_name mode in diff --git a/src/ecScope.mli b/src/ecScope.mli index 08c5a020c..673c2f01c 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -27,6 +27,11 @@ type required_info = { type required = required_info list +(* An elaborated theory, as [Theory.loaded] hands it back and + [Theory.seed_loaded] takes it: opaque here, and only ever moved from + one scope to another. *) +type thloaded + type scope type proof_uc = { @@ -198,6 +203,22 @@ module Theory : sig * theory. *) val require : scope -> (required_info * thmode) -> (scope -> scope) -> scope + (* [loaded scope name] is the elaborated theory [name] this scope has + already read, with the theories reading it required, or [None]. + [seed_loaded scope entries] puts such entries into a scope, so that + a [require] naming one of them takes the loaded path and never runs + its loader. + + They exist for a front-end that rebuilds the scope in order to + reload a file: the table [require] consults is part of the scope, + so without them every reload re-reads every required theory, which + is the bulk of what a reload costs. Nothing here looks at the file + system: a caller that seeds a theory the sources no longer describe + gets a session built on the stale one, so validating the entries + against disk before seeding them is the caller's job. *) + val loaded : scope -> symbol -> (thloaded * required) option + val seed_loaded : scope -> (symbol * (thloaded * required)) list -> scope + (* start/finish adding a new top-level required theory, not using loader * * [require_start] enters the theory, with the given name and theory mode, diff --git a/tests/llm/README.md b/tests/llm/README.md index 92d6f8a09..cea18c795 100644 --- a/tests/llm/README.md +++ b/tests/llm/README.md @@ -10,10 +10,11 @@ compared against recorded goldens. | Path | Contents | |------|----------| | `fixtures/*` | tiny EasyCrypt files the scripts `LOAD` (plus one non-`.ec` file, for the unknown-extension error, and one deliberately Latin-1 file used by `../mcp`) | -| `fixtures/sub/*` | a second directory, so a scenario can check that one `LOAD`'s include path does not survive into the next | +| `fixtures/sub/*` | a second directory, so a scenario can check that one `LOAD`'s include path does not survive into the next, and that a theory in it is elaborated once however often the file is reloaded | | `scripts/*.script` | the newline-separated commands passed to `-eval` | | `expected/*.out` | recorded stdout, one file per script | | `../../scripts/testing/llm-golden` | the runner | +| `../../scripts/testing/llm-warm-reload` | a second runner, for what a `-eval` script cannot reach | ## Running @@ -108,6 +109,33 @@ sentence's source verbatim; that sentence hides a bare `` and a bare `OK [uuid:99]` in a comment. The MCP front-end needs no such rule: its frame is a JSON string. +## The reload the goldens cannot reach + +The interactive front-ends keep the theories a `require` elaborates +across the scope rebuild a LOAD does, so that reloading a file does not +re-read everything under it. Two halves of that have to be tested, and +only one of them fits here. + +`warm-reload` covers the half that does: it LOADs one fixture twice and +freezes both frames, which must match line for line — the cache is not +supposed to be visible on the wire, and a golden that shows the two +halves side by side is the plainest way to say so. + +The other half is what happens when a file *changes*, and it cannot be +a `-eval` script: the change has to land between two LOADs of one +session, and `-eval` hands the whole script over at once. +`scripts/testing/llm-warm-reload` drives the REPL over stdin instead, +on a fixture tree it writes into a temporary directory, and checks four +scenarios — an untouched reload, an edit to a required file, an edit to +a file reached only through another one, and an include path that +changes so a name resolves elsewhere. Each asserts that the warm +session answers exactly what a cold process answers on the same +sources, and the edited ones also assert the answer moved, so that a +fixture whose edit turns out to be invisible fails instead of passing +without testing anything. + +`make test-llm` runs both. + ## Adding a scenario 1. Add `scripts/NAME.script` starting with `# exit: N`. diff --git a/tests/llm/expected/warm-reload.out b/tests/llm/expected/warm-reload.out new file mode 100644 index 000000000..54f824cc9 --- /dev/null +++ b/tests/llm/expected/warm-reload.out @@ -0,0 +1,44 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/sub/reload.ec:7] +Current goal + +Type variables: + +------------------------------------------------------------------------ +neighbour = 3 + +OK [uuid:3] +* In [operators, predicates or exceptions]: + +(* Neighbour.neighbour (shorten name: neighbour) *) +op neighbour : int = 3. + +Current goal + +Type variables: + +------------------------------------------------------------------------ +neighbour = 3 + +OK [uuid:3] [loaded:fixtures/sub/reload.ec:7] +Current goal + +Type variables: + +------------------------------------------------------------------------ +neighbour = 3 + +OK [uuid:3] +* In [operators, predicates or exceptions]: + +(* Neighbour.neighbour (shorten name: neighbour) *) +op neighbour : int = 3. + +Current goal + +Type variables: + +------------------------------------------------------------------------ +neighbour = 3 + diff --git a/tests/llm/fixtures/sub/reload.ec b/tests/llm/fixtures/sub/reload.ec new file mode 100644 index 000000000..606d96fcd --- /dev/null +++ b/tests/llm/fixtures/sub/reload.ec @@ -0,0 +1,10 @@ +(* LOADed twice in one session, to pin what a reload costs nothing: + `Neighbour' is elaborated once and served from the theory cache the + second time, and the two replies have to be indistinguishable. *) +require import AllCore Neighbour. + +lemma warm : neighbour = 3. +proof. +rewrite /neighbour. +trivial. +qed. diff --git a/tests/llm/scripts/warm-reload.script b/tests/llm/scripts/warm-reload.script new file mode 100644 index 000000000..6958ce75e --- /dev/null +++ b/tests/llm/scripts/warm-reload.script @@ -0,0 +1,13 @@ +# exit: 0 +# The interactive front-ends keep the theories a `require' elaborates +# across the scope rebuild a LOAD does, so that reloading a file does +# not re-read everything under it. Whether that happened is not +# visible on the wire, and must not be: the contract is that a reload +# answers exactly what the first load answered. The two LOAD frames +# below are that contract -- same uuid, same tag, same goal -- and so +# are the two `print' frames, which read the served theory rather than +# the reloaded file. +LOAD "fixtures/sub/reload.ec" 7 +print neighbour. +LOAD "fixtures/sub/reload.ec" 7 +print neighbour. From c9751bd32508e76efdc5a9297101b72fedf2cf5c Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 7 Sep 2026 11:31:10 +0200 Subject: [PATCH 3/3] [llm] STRICT: stop the session at a failure instead of drifting past it A session behaves as a source file does: a failing phrase is reported and whatever comes next runs against wherever it left the engine. For a client that sends one phrase per call and acts on each reply, that is a trap. `split.' opens two goals, the tactic after it fails, and the phrase after *that* lands on the first subgoal rather than on the state it was written for. Nothing says so. The proof stops making sense several phrases later, and the way back is a checkpoint. `STRICT ON' (`ec_strict' over MCP) stops the session there instead. Any failure of an operation that could have advanced arms the stop -- whether or not that particular failure advanced anything, since the drift is in the client's picture of where the session is and not in the engine -- and everything that could move the engine further is refused until the session is put somewhere the client chose: UNDO, REVERT and LOAD by arriving somewhere definite, RESUME (`ec_resume') by saying so. Being stopped is not being locked out: GOALS, TREE, SEARCH, CHECKPOINT and COMMIT all answer, the point being to look at the failure. The gate is in EcLlmCore, not in either front-end, so the REPL and the MCP server cannot come to differ on what a stopped session refuses. `try_step' is the one advancing operation whose failures do not arm it: they restore the state the call started from and report having done so, so the client's picture stays exact. It is still refused *while* stopped, since succeeding would advance from a point the client has not acknowledged, and a refusal restores the stop it was refused by, so being refused changes nothing either. RESUME fails on a session that is not stopped, and on one where the mode is off. That is not pedantry: a client resuming a session that was never stopped has lost track of it, which is the one thing this mode is here to say. Off by default, so nothing changes for anyone who has not asked -- the 36 existing REPL goldens and 17 MCP goldens are untouched, and only the tool table moved. Three scenarios and a parity leg. `strict-stop' plays the trap: a phrase fails after `split.' has moved the engine, the next one is refused, GOALS still answers, RESUME releases it, and the COMMIT at the end shows the emitted body carries no trace of either the failed phrase or the refused one. `strict-resume-unstopped' pins RESUME's two refusals. The MCP `strict-stop' covers what a -eval script cannot show, ec_try being refused while stopped although its own failure never stopped anything. And mcp-parity gains five steps, so the two wires are checked to say the same thing at the stop, at the refusal and at the release. `Schema.bool' takes `default' as optional now: `ec_strict.on' is required, and a schema that declares a default and demands the property anyway says two things at once. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Y2YZRRxpC8R1Ho2NGpD1fg --- doc/llm/CLAUDE.md | 58 ++++++++- scripts/testing/mcp-parity | 15 +++ src/ecLlm.ml | 7 ++ src/ecLlmCore.ml | 119 +++++++++++++++++- src/ecLlmCore.mli | 25 ++++ src/ecMcp.ml | 64 +++++++++- tests/llm/README.md | 18 +++ .../llm/expected/strict-resume-unstopped.out | 29 +++++ tests/llm/expected/strict-stop.out | 74 +++++++++++ .../scripts/strict-resume-unstopped.script | 10 ++ tests/llm/scripts/strict-stop.script | 23 ++++ tests/mcp/README.md | 7 +- tests/mcp/expected/strict-stop.out | 11 ++ tests/mcp/expected/tools-list.out | 2 +- tests/mcp/scripts/strict-stop.script | 21 ++++ 15 files changed, 469 insertions(+), 14 deletions(-) create mode 100644 tests/llm/expected/strict-resume-unstopped.out create mode 100644 tests/llm/expected/strict-stop.out create mode 100644 tests/llm/scripts/strict-resume-unstopped.script create mode 100644 tests/llm/scripts/strict-stop.script create mode 100644 tests/mcp/expected/strict-stop.out create mode 100644 tests/mcp/scripts/strict-stop.script diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 69022c938..9755712f0 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -102,6 +102,8 @@ These are protocol-level commands, not EasyCrypt syntax: | `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | | `SEARCH ` | Search for lemmas matching a pattern (read-only: the uuid does not move) | | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | +| `STRICT ON` / `STRICT OFF` | Stop the session at a failure, instead of carrying on from wherever it left the engine | +| `RESUME` | Release a `STRICT` stop without moving the engine | | `` / `` | Delimit multi-line EasyCrypt input | | `HELP` | Print this guide | | `QUIT` | Exit | @@ -373,7 +375,49 @@ is read from a snapshot taken while the proof was open. `UNDO` / `REVERT` trim the COMMIT transcript automatically. -**6. Use QUIET mode to save tokens during bulk tactic application:** +**6. Use `STRICT ON` if you send one phrase at a time:** + +A session behaves as a source file does: a failing phrase is reported, +and whatever you send next runs against wherever that failure left the +engine. Sending phrases one at a time and acting on each reply, that +is a trap. `split.` opens two goals, the tactic after it fails, and +the phrase after *that* lands on the first subgoal rather than where +you wrote it for. Nothing says so; the proof simply stops making +sense several phrases later. + +`STRICT ON` stops the session at the failure instead: + +``` +STRICT ON +split. +apply etrivial. ← fails, having left two goals open +trivial. +→ ERROR [uuid:42] + strict: the session stopped at a failed phrase and has not been + resynchronized + stopped at: apply etrivial. + UNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and + COMMIT answer meanwhile +``` + +Being stopped is not being locked out: `GOALS`, `TREE`, `SEARCH`, +`CHECKPOINT` and `COMMIT` all answer, which is the point — you are +meant to look at the failure. What is refused is anything that would +move the engine further. To carry on, either go somewhere definite +(`UNDO`, `REVERT`, `LOAD`) or say you meant to stay (`RESUME`). + +`RESUME` fails if the session was not stopped, and so does `STRICT +OFF` release any stop: a session that does not stop at failures cannot +be sitting at one. + +Over MCP the mode is `ec_strict` and the release is `ec_resume`, and +there `ec_try` earns its keep: a failing `ec_try` never stops the +session, its contract being that a failure leaves the engine exactly +where it was, so there is no drift to prevent. It is still refused +*while* stopped, since succeeding would advance from a point you have +not acknowledged. + +**7. Use QUIET mode to save tokens during bulk tactic application:** ``` QUIET ON @@ -384,7 +428,7 @@ QUIET OFF GOALS ``` -**7. Search for lemmas using patterns:** +**8. Search for lemmas using patterns:** EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as wildcard: @@ -432,7 +476,7 @@ resources, no prompts, no sampling. ### Tools -Eleven tools. Required arguments are marked; the others default as +Thirteen tools. Required arguments are marked; the others default as noted. | Tool | Arguments | Description | @@ -447,14 +491,16 @@ noted. | `ec_revert` | `target` (req) | Return the session to an earlier state, named by a uuid or by a checkpoint name | | `ec_checkpoint` | `name` (req) | Record the current uuid under `name`, for a later `ec_revert` | | `ec_commit` | — | Emit the phrases recorded since the last `ec_load` as a bulleted proof body | +| `ec_strict` | `on` (req) | Stop the session at a failure, instead of carrying on from wherever it left the engine | +| `ec_resume` | — | Release a strict-mode stop without moving the engine | | `ec_search` | `pattern` (req) | Search the environment for lemmas matching an EasyCrypt search pattern | `tools/list` carries a fuller, agent-facing `description` and a JSON Schema for every tool; those are the authoritative texts. The tools mirror the REPL meta-commands — `-nosmt`, `-noproof`, `-trace`, dotted paths, -checkpoints, bullets and search patterns all behave exactly as -described above, and `NEXT` folds into `ec_focus` with path `"next"` — -plus `ec_try`, which has no REPL equivalent. The meta-commands that are +checkpoints, bullets, strict mode and search patterns all behave +exactly as described above, and `NEXT` folds into `ec_focus` with path +`"next"` — plus `ec_try`, which has no REPL equivalent. The meta-commands that are pure console affordances have no tool: multi-line input needs no ``/`` (a `phrase` may simply contain newlines), `QUIET` has no purpose when the client decides what to display, `HELP` is this diff --git a/scripts/testing/mcp-parity b/scripts/testing/mcp-parity index 52756123d..4ccf015e8 100755 --- a/scripts/testing/mcp-parity +++ b/scripts/testing/mcp-parity @@ -60,6 +60,21 @@ STEPS = [ "ec_commit", {}), ("failure", 'apply nosuchlemma.', "ec_step", {"phrase": "apply nosuchlemma."}), + # Strict mode, which is a session setting rather than an operation + # on the proof: turning it on and failing again stops the session, + # the phrase after that is refused, and both wires have to say the + # same thing at each of those four points. `STRICT OFF' puts the + # session back before the loads below, which reset it anyway. + ("strict/on", 'STRICT ON', + "ec_strict", {"on": True}), + ("strict/stop", 'apply nosuchlemma.', + "ec_step", {"phrase": "apply nosuchlemma."}), + ("strict/refused", 'trivial.', + "ec_step", {"phrase": "trivial."}), + ("resume", 'RESUME', + "ec_resume", {}), + ("strict/off", 'STRICT OFF', + "ec_strict", {"on": False}), # The two load options that change what the engine does. Both # reset the session, so they come last. `trace' is the one whose # reply body the core builds itself, rather than handing back the diff --git a/src/ecLlm.ml b/src/ecLlm.ml index 69078f63c..3620d3751 100644 --- a/src/ecLlm.ml +++ b/src/ecLlm.ml @@ -76,6 +76,8 @@ module Parse = struct | Checkpoint of string | Revert of string (* uuid-or-name; the core resolves *) | Quiet of bool + | Strict of bool + | Resume | Search of string (* trailing "." already stripped *) | Load of load (* parsed LOAD arguments *) | Ec of string (* fall-through: raw EasyCrypt input *) @@ -227,6 +229,9 @@ module Parse = struct | "NEXT" -> Next | "QUIET ON" -> Quiet true | "QUIET OFF" -> Quiet false + | "STRICT ON" -> Strict true + | "STRICT OFF"-> Strict false + | "RESUME" -> Resume | _ -> match keyword_arg "FOCUS" line with Some a -> parse_focus a | None -> match keyword_arg "CHECKPOINT" line with Some a -> parse_checkpoint a | None -> @@ -385,6 +390,8 @@ let run ~relocdir ~boot ~projini (llmopts : EcOptions.llm_option) = | Checkpoint n -> Wire.reply (EcLlmCore.checkpoint st ~name:n) | Revert s -> Wire.reply (EcLlmCore.revert st s) | Quiet on -> do_quiet on + | Strict on -> Wire.reply (EcLlmCore.strict st ~on) + | Resume -> Wire.reply (EcLlmCore.resume st) | Search q -> Wire.reply (EcLlmCore.search st ~pattern:q) | Load args -> Wire.reply (EcLlmCore.load st diff --git a/src/ecLlmCore.ml b/src/ecLlmCore.ml index 65a32d07e..e393fb384 100644 --- a/src/ecLlmCore.ml +++ b/src/ecLlmCore.ml @@ -105,6 +105,19 @@ type state = { that don't collide with frames opened by the LOAD prefix. Cleared with the transcript on LOAD/Restart. *) prior_bullets : EcBullets.stack option ref; + + (* Strict mode: is a failure allowed to be followed by more input? + Off, a session behaves as a file does -- the failure is reported + and whatever comes next is run against wherever it left the + engine. On, the session stops there instead. *) + strict_mode : bool ref; + + (* Set, while strict, to the phrase a failure stopped the session + at. Every operation that could move the engine refuses until the + session is resynchronized ([undo], [revert], [load], [resume]), + so a client that sends its phrases one at a time cannot walk past + the failure and carry on against a state it did not mean. *) + stopped_at : string option ref; } (* -------------------------------------------------------------------- *) @@ -166,6 +179,8 @@ let create ~relocdir ~boot ~projini ~prvopts = checkpoints = Hashtbl.create 16; transcript = ref []; prior_bullets = ref None; + strict_mode = ref false; + stopped_at = ref None; } in (* [print] renders on the process's stdout by default, which in the @@ -399,6 +414,62 @@ let mk_failure (st : state) ~(pre : int) (message : string) = { uuid; message; goals = Goals.goals_to_string (); notices; reverted = false; changed = uuid <> pre; } +(* -------------------------------------------------------------------- *) +(* Strict mode. + + A session is a file that is still being written: a failure is + reported and whatever is sent next runs against wherever it left the + engine, exactly as the sentences after a failure in a file would. + That is the right default, and it is also the trap a client that + sends its phrases one at a time falls into -- it keeps sending, + each phrase lands on a state one phrase further from the one it was + written against, and the drift is only noticed later. + + Under strict mode the session stops instead. Any failure of an + operation that could have advanced arms [stopped_at] -- whether or + not that particular failure did advance, since the drift is in the + client's picture of where the session is, not in the engine: the + phrase after a failed one was written for the state the failed one + was to produce, and runs against the state before it either way. + Every operation that could move the engine further is then refused + until the session is put somewhere the client chose: [undo], + [revert] and [load] do that by arriving somewhere definite, and + [resume] by saying so. Reading is never refused -- the point is to + look at the failure, not to be locked out of it -- so goals, trees, + searches, checkpoints and COMMIT answer while stopped. + + [try_step] is the one advancing operation whose failures do not arm + it: they restore the state the call started from and say so + ([reverted]), so the client's picture stays exact and there is no + drift to prevent. It is still refused *while* stopped, since + succeeding would advance from a point the client has not + acknowledged. *) +module Strict = struct + let stopped (st : state) = + !(st.strict_mode) && !(st.stopped_at) <> None + + (* Arm the stop. [at] is how the reply will name the phrase that + stopped the session. Only the first failure arms it: what the + client needs is where it stopped being in control, not where the + last refusal happened. *) + let arm (st : state) (at : string) = + if !(st.strict_mode) && !(st.stopped_at) = None then + st.stopped_at := Some (if at = "" then "" else at) + + let clear (st : state) = + st.stopped_at := None + + (* The refusal. It carries the phrase that stopped the session and + the ways out, because a client that hits this has by definition + lost track of where the session is. *) + let refuse (st : state) ~(pre : int) = + let at = odfl "" !(st.stopped_at) in + mk_failure st ~pre (Printf.sprintf + "strict: the session stopped at a failed phrase and has not been \ + resynchronized\nstopped at: %s\nUNDO, REVERT, LOAD or RESUME to \ + continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile" at) +end + (* -------------------------------------------------------------------- *) (* Transcript manipulation. *) module Transcript = struct @@ -421,7 +492,9 @@ end let reset_session (st : state) : unit = do_initialize st; Hashtbl.clear st.checkpoints; - Transcript.clear st + Transcript.clear st; + (* A strict stop names a phrase of a session that no longer exists. *) + st.stopped_at := None (* -------------------------------------------------------------------- *) (* Process a single EasyCrypt command, respecting [gl_fail]. When @@ -790,6 +863,7 @@ let step (st : state) input = let prior_bullets = st.prior_bullets in let pre = EcCommands.uuid () in Buffer.clear notices; + if Strict.stopped st then Done (Error (Strict.refuse st ~pre)) else begin (* On the first REPL phrase of each proof, capture the bullet stack the LOAD prefix left so COMMIT can avoid token collisions with it. Subsequent calls return [None] and don't clobber the snapshot. *) @@ -838,11 +912,13 @@ let step (st : state) input = reset_session st; Done (Ok (mk_reply st ~pre (Text "Session restarted"))) | e -> + Strict.arm st !last_src; Done (Error (mk_failure st ~pre (Goals.format_error ~src:!last_src e))) end in EcIo.finalize reader; answer + end (* -------------------------------------------------------------------- *) (* [step] with an automatic rollback on failure. A phrase can fail @@ -870,6 +946,7 @@ let try_step (st : state) input = let mark = EcCommands.undo_mark () in let transcript = !(st.transcript) in let bullets = !(st.prior_bullets) in + let stopped_at = !(st.stopped_at) in match step st input with | Quit -> Quit | Done (Ok _) as answer -> answer @@ -877,6 +954,11 @@ let try_step (st : state) input = EcCommands.undo_restore mark; st.transcript := transcript; st.prior_bullets := bullets; + (* Restored like the rest of the bookkeeping: strict mode stops a + session because a failure may have moved the engine, and this + one provably did not. A refusal restores the stop that produced + it, so being refused does not itself change anything. *) + st.stopped_at := stopped_at; let uuid = EcCommands.uuid () in Done (Error { failure with uuid; @@ -1340,6 +1422,8 @@ let undo (st : state) = if uuid > 0 then begin EcCommands.undo (uuid - 1); Transcript.trim st (uuid - 1); + (* Somewhere definite: the stop has been answered. *) + Strict.clear st; Ok (mk_reply_goals st ~pre) end else Error (mk_failure st ~pre "nothing to undo") @@ -1351,6 +1435,7 @@ let focus (st : state) request = and focus the matching leaf. *) let pre = EcCommands.uuid () in Buffer.clear st.notices; + if Strict.stopped st then Error (Strict.refuse st ~pre) else let resolved = match request with | `Next -> @@ -1372,6 +1457,37 @@ let checkpoint (st : state) ~name = Ok (mk_reply st ~pre (Text (Printf.sprintf "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())))) +(* Strict mode on and off. Turning it off releases a stop: a session + that does not stop at failures cannot be sitting at one. *) +let strict (st : state) ~(on : bool) = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + st.strict_mode := on; + if not on then Strict.clear st; + Ok (mk_reply st ~pre (Text ( + if on then + "strict: on -- a failure stops the session until UNDO, REVERT, \ + LOAD or RESUME" + else + "strict: off"))) + +(* Release a stop without going anywhere: the client has read the + failure and means to carry on from where it left the engine. The + two refusals are not pedantry -- a client that resumes a session + that was never stopped has lost track of it, which is the one thing + this mode exists to tell it. *) +let resume (st : state) = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + if not !(st.strict_mode) then + Error (mk_failure st ~pre "RESUME: strict mode is off") + else if !(st.stopped_at) = None then + Error (mk_failure st ~pre "RESUME: the session is not stopped") + else begin + Strict.clear st; + Ok (mk_reply_goals st ~pre) + end + let revert (st : state) spec = let pre = EcCommands.uuid () in Buffer.clear st.notices; @@ -1391,6 +1507,7 @@ let revert (st : state) spec = else begin EcCommands.undo target; Transcript.trim st target; + Strict.clear st; Ok (mk_reply_goals st ~pre) end diff --git a/src/ecLlmCore.mli b/src/ecLlmCore.mli index 5df8e88c0..11d7fbc04 100644 --- a/src/ecLlmCore.mli +++ b/src/ecLlmCore.mli @@ -110,6 +110,31 @@ val step : state -> string -> answer advanced. *) val try_step : state -> string -> answer +(* Strict mode. Off, a session behaves as a file does: a failure is + reported and the next input runs against wherever it left the + engine. On, the session stops at any failure of an operation that + could have advanced, and every operation that could advance it + further is refused until the session is resynchronized -- by + [undo], [revert] or [load], which arrive somewhere definite, or by + [resume], which says so. Reads are never refused: [goals], [tree], [search], [checkpoint] + and [commit] answer while stopped, the point being to look at the + failure rather than be locked out of it. + + It is the client sending one phrase per call that this is for. Such + a client keeps sending after a failure, and each phrase runs against + a state it was not written for -- the one the failed phrase was + meant to leave, and never reached. The drift is silent and is + noticed much later. [try_step]'s failures do not arm the stop, since + they restore the state the call started from and report having done + so, but it is refused while stopped like anything else that would + advance. + + [resume] fails if the session is not stopped, or if strict mode is + off: a client resuming a session that was never stopped has lost + track of it, which is what this mode is here to say. *) +val strict : state -> on:bool -> (reply, failure) result +val resume : state -> (reply, failure) result + val goals : state -> all:bool -> (reply, failure) result val tree : state -> all:bool -> (reply, failure) result val focus : state -> [`Next | `Path of int list] -> (reply, failure) result diff --git a/src/ecMcp.ml b/src/ecMcp.ml index d799a6eff..f930fccd9 100644 --- a/src/ecMcp.ml +++ b/src/ecMcp.ml @@ -156,10 +156,15 @@ module Schema = struct `Assoc [("type", `String "integer"); ("description", `String description)] - let bool ~description ~default () = - `Assoc [("type", `String "boolean"); - ("description", `String description); - ("default", `Bool default)] + (* [default] is omitted for a required property: a schema that + declares one and demands the property anyway says two things at + once, and a client is entitled to believe either. *) + let bool ~description ?default () = + `Assoc ([("type", `String "boolean"); + ("description", `String description)] + @ (match default with + | None -> [] + | Some d -> [("default", `Bool d)])) let obj ?(required = []) props = `Assoc ([("type", `String "object"); @@ -423,6 +428,43 @@ let tools : J.t list = ~output:(Schema.output ()) (); + tool + ~name:"ec_strict" + ~description: + "Turn strict mode on or off. Off (the default) a session \ + behaves as a source file does: a failing phrase is reported \ + and the next call runs against wherever it left the engine. \ + On, the session stops at a failure that may have moved the \ + engine, and ec_step, ec_try and ec_focus are refused until it \ + is resynchronized -- by ec_undo, ec_revert or ec_load, which \ + arrive somewhere definite, or by ec_resume, which says so. \ + Turn it on if you send one phrase per call and act on each \ + result: without it a failure is followed by calls landing on \ + a state you did not mean, and the drift is silent. Reads \ + (ec_goals, ec_tree, ec_search, ec_checkpoint, ec_commit) \ + always answer, stopped or not." + ~input:(Schema.obj ~required:["on"] [ + ("on", Schema.bool + ~description:"true to stop the session at a failure" ()); + ]) + ~annotations:[("destructiveHint", `Bool false)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_resume" + ~description: + "Release a strict-mode stop without moving the engine: you have \ + read the failure and mean to carry on from where it left the \ + session. Use ec_undo or ec_revert instead when you would \ + rather go back. Fails when the session is not stopped, or when \ + strict mode is off -- either way you are not where you think \ + you are, which is what strict mode is for." + ~input:(Schema.obj []) + ~annotations:[("destructiveHint", `Bool false)] + ~output:(Schema.output ()) + (); + tool ~name:"ec_search" ~description: @@ -475,6 +517,14 @@ module Args = struct | Some (`Bool b) -> b | Some _ -> bad tool name "a boolean" + let bool_req tool args name = + match List.assoc_opt name args with + | Some (`Bool b) -> b + | Some _ -> bad tool name "a boolean" + | None -> + raise (Invalid_params + (Printf.sprintf "%s: missing required argument `%s'" tool name)) + let int_opt tool args name = match List.assoc_opt name args with | None | Some `Null -> None @@ -701,6 +751,12 @@ let run ~relocdir ~boot ~projini (mcpopts : EcOptions.mcp_option) = | "ec_commit" -> outcome (EcLlmCore.commit st) + | "ec_strict" -> + outcome (EcLlmCore.strict st ~on:(Args.bool_req name args "on")) + + | "ec_resume" -> + outcome (EcLlmCore.resume st) + | "ec_search" -> outcome (EcLlmCore.search st ~pattern:(Args.string_req name args "pattern")) diff --git a/tests/llm/README.md b/tests/llm/README.md index cea18c795..3a0ac3bb8 100644 --- a/tests/llm/README.md +++ b/tests/llm/README.md @@ -109,6 +109,24 @@ sentence's source verbatim; that sentence hides a bare `` and a bare `OK [uuid:99]` in a comment. The MCP front-end needs no such rule: its frame is a JSON string. +## Strict mode + +`strict-stop` plays the scenario the mode exists for: a phrase fails +after having moved the engine, the phrase after it is refused rather +than run against a state nobody meant, `GOALS` answers all the same, +and `RESUME` releases it. The `COMMIT` at the end is part of the +point — the body it emits carries no trace of either the failed phrase +or the refused one. + +`strict-resume-unstopped` pins the two ways `RESUME` refuses, which +are one mistake seen twice: a client resuming a session that was never +stopped does not know where it is. + +The MCP side has its own `strict-stop`, for the one case a REPL script +cannot show: `ec_try` is refused while stopped like anything else that +would advance, although a failing `ec_try` never stops the session in +the first place. + ## The reload the goldens cannot reach The interactive front-ends keep the theories a `require` elaborates diff --git a/tests/llm/expected/strict-resume-unstopped.out b/tests/llm/expected/strict-resume-unstopped.out new file mode 100644 index 000000000..5495062dd --- /dev/null +++ b/tests/llm/expected/strict-resume-unstopped.out @@ -0,0 +1,29 @@ +READY [uuid:0] + +ERROR [uuid:0] +RESUME: strict mode is off +No active proof. + +OK [uuid:0] +strict: on -- a failure stops the session until UNDO, REVERT, LOAD or RESUME + +OK [uuid:2] [loaded:fixtures/simple.ec:5] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:2] +RESUME: the session is not stopped +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:2] +strict: off + diff --git a/tests/llm/expected/strict-stop.out b/tests/llm/expected/strict-stop.out new file mode 100644 index 000000000..4503070f2 --- /dev/null +++ b/tests/llm/expected/strict-stop.out @@ -0,0 +1,74 @@ +READY [uuid:0] + +OK [uuid:0] +strict: on -- a failure stops the session until UNDO, REVERT, LOAD or RESUME + +OK [uuid:2] [loaded:fixtures/simple.ec:5] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +ERROR [uuid:3] +: line 1 (0-15): unknown lemma `etrivial' +source: apply etrivial. +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +ERROR [uuid:3] +strict: the session stopped at a failed phrase and has not been resynchronized +stopped at: apply etrivial. +UNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:3] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:3] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] +Current goal + +Type variables: + +------------------------------------------------------------------------ +2 = 2 + +OK [uuid:5] +No more goals + +OK [uuid:5] +split. +- trivial. +- trivial. + diff --git a/tests/llm/scripts/strict-resume-unstopped.script b/tests/llm/scripts/strict-resume-unstopped.script new file mode 100644 index 000000000..73ad86679 --- /dev/null +++ b/tests/llm/scripts/strict-resume-unstopped.script @@ -0,0 +1,10 @@ +# exit: 1 +# The two ways RESUME refuses, which are the same mistake seen twice: +# a client resuming a session that was never stopped does not know +# where it is, and strict mode exists to say so. First with the mode +# off, then with it on but nothing having failed. +RESUME +STRICT ON +LOAD "fixtures/simple.ec" 5 +RESUME +STRICT OFF diff --git a/tests/llm/scripts/strict-stop.script b/tests/llm/scripts/strict-stop.script new file mode 100644 index 000000000..961fc9357 --- /dev/null +++ b/tests/llm/scripts/strict-stop.script @@ -0,0 +1,23 @@ +# exit: 1 +# Strict mode. Off, a session is a file still being written: a failure +# is reported and the next phrase runs against wherever it left the +# engine. That is the trap a client sending one phrase per call falls +# into, so STRICT ON stops the session at the failure instead. +# +# `apply etrivial.' fails after `split.' has opened two goals, so the +# session is left somewhere the caller did not intend. The `trivial.' +# that follows is refused, and the refusal names the phrase that +# stopped it. GOALS answers all the same -- being stopped is not being +# locked out -- and RESUME releases it. The COMMIT at the end shows the +# body carries no trace of any of it: a failed phrase was never +# recorded, and a refused one never ran. +STRICT ON +LOAD "fixtures/simple.ec" 5 +split. +apply etrivial. +trivial. +GOALS +RESUME +trivial. +trivial. +COMMIT diff --git a/tests/mcp/README.md b/tests/mcp/README.md index 31a8ab1a0..51391de06 100644 --- a/tests/mcp/README.md +++ b/tests/mcp/README.md @@ -64,6 +64,7 @@ gate for changes to the protocol layer. | `non-utf8` | engine output that is not UTF-8 comes back as U+FFFD, not as invalid JSON | | `try-revert` | `ec_try` rolling back a phrase that had already advanced the proof | | `try-undo` | `ec_try` rolling *forward* again after a phrase whose `undo` lowered the uuid | +| `strict-stop` | `ec_strict` stopping the session at a failure: what is refused, what still answers, and that a failing `ec_try` never stops it | | `protocol-errors` | `-32700`, `-32600`, `-32601` and the `-32602` family | | `revert` | `ec_revert` by uuid and by checkpoint name | | `load-missing` | a missing file and an unknown extension: `isError`, *not* `-32602` | @@ -125,8 +126,10 @@ same answer on both. It plays one representative operation per tool family — load, step, goals, tree, focus, undo, checkpoint, step again, revert, search, -commit, a failing phrase, and finally a `nosmt` load and a `trace` load -(both reset the session, hence last) — in that order, against two +commit, a failing phrase, then strict mode (on, a failure that stops +the session, a refused phrase, resume, off), and finally a `nosmt` +load and a `trace` load (both reset the session, hence last) — in that +order, against two sessions started from the same directory (`tests/llm`, so both name the fixture identically and no path difference can leak into a reply): a REPL session driven with `llm -eval`, and an MCP session driven with a diff --git a/tests/mcp/expected/strict-stop.out b/tests/mcp/expected/strict-stop.out new file mode 100644 index 000000000..47b319a4d --- /dev/null +++ b/tests/mcp/expected/strict-stop.out @@ -0,0 +1,11 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"strict: on -- a failure stops the session until UNDO, REVERT, LOAD or RESUME"}],"structuredContent":{"text":"strict: on -- a failure stops the session until UNDO, REVERT, LOAD or RESUME","uuid":0,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":": line 1 (0-18): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":": line 1 (0-18): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false,"reverted":true},"isError":true}} +{"jsonrpc":"2.0","id":5,"result":{"content":[{"type":"text","text":": line 1 (7-25): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":": line 1 (7-25): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":true},"isError":true}} +{"jsonrpc":"2.0","id":6,"result":{"content":[{"type":"text","text":"strict: the session stopped at a failed phrase and has not been resynchronized\nstopped at: apply nosuchlemma.\nUNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"strict: the session stopped at a failed phrase and has not been resynchronized\nstopped at: apply nosuchlemma.\nUNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":false},"isError":true}} +{"jsonrpc":"2.0","id":7,"result":{"content":[{"type":"text","text":"strict: the session stopped at a failed phrase and has not been resynchronized\nstopped at: apply nosuchlemma.\nUNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"strict: the session stopped at a failed phrase and has not been resynchronized\nstopped at: apply nosuchlemma.\nUNDO, REVERT, LOAD or RESUME to continue; GOALS, TREE, SEARCH and COMMIT answer meanwhile\nCurrent goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":false,"reverted":true},"isError":true}} +{"jsonrpc":"2.0","id":8,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":9,"result":{"content":[{"type":"text","text":"split.\n"}],"structuredContent":{"text":"split.\n","uuid":4,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":10,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":11,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n","uuid":5,"changed":true},"isError":false}} diff --git a/tests/mcp/expected/tools-list.out b/tests/mcp/expected/tools-list.out index 0c20d43a4..6464e5836 100644 --- a/tests/mcp/expected/tools-list.out +++ b/tests/mcp/expected/tools-list.out @@ -1 +1 @@ -{"jsonrpc":"2.0","id":1,"result":{"tools":[{"name":"ec_load","description":"Reset the session and compile FILE from the top, stopping after the last sentence that ends on or before LINE (and column COL when given). This is the entry point: every other tool needs a loaded file, and tactics need the position to land inside a proof. Set nosmt to weaken SMT calls while replaying a prefix that was already verified, which is much faster on large files. Set noproof to go further and skip the prefix's proofs altogether, admitting every lemma before the target on its statement alone -- only the proof the position lands inside is replayed, which is the fastest way into a proof in a long file. Set trace to have the reply describe the last loaded sentence as BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports where compilation stopped and the resulting goal state; note the uuid it returns, reverting to it is the instant way back to the start of the proof.","inputSchema":{"type":"object","properties":{"file":{"type":"string","description":"path to the .ec/.eca file"},"line":{"type":"integer","description":"stop after the last sentence ending on or before this line; omit to compile the whole file"},"col":{"type":"integer","description":"column bound within `line'; requires `line'"},"nosmt":{"type":"boolean","description":"weaken SMT calls while compiling the prefix","default":false},"noproof":{"type":"boolean","description":"skip the prefix's proofs entirely, admitting the lemmas before the target as axioms","default":false},"trace":{"type":"boolean","description":"report the proof state around the last loaded sentence","default":false}},"required":["file"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_step","description":"Run EasyCrypt sentences -- tactics, declarations, require, print, ... -- against the current session. Every complete sentence in the argument is executed, in order, exactly as if the text had been appended to the source file, and a single reply describes the state they leave behind; sentences may span several lines. Requires a file loaded with ec_load, and, for tactics, an open proof. On success the reply carries the new goal state; on failure the prover's error text comes back with isError set, the sentences before the failing one stay applied and the engine is left wherever that sentence left it -- use ec_try when you want a guaranteed rollback. Successful non-query phrases are recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one or more complete EasyCrypt sentences, each ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false,"idempotentHint":false}},{"name":"ec_try","description":"Like ec_step, but the engine is rolled back to the state it had before the call whenever a sentence fails, including input that failed only after having already advanced the proof. The failure reply sets structuredContent.reverted to true, and its uuid and goal text describe the restored state, not the point of failure. Use this to probe a tactic without having to ec_revert afterwards; use ec_step when you mean to keep whatever progress the phrase makes. A successful phrase behaves exactly as under ec_step and is recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one complete EasyCrypt sentence, ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"},"reverted":{"type":"boolean","description":"set when the phrase failed and the engine was rolled back to its pre-call state"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_goals","description":"Print the current proof state: the focused subgoal alone, or, with all set, every open subgoal. Requires an open proof, and does not advance the engine.","inputSchema":{"type":"object","properties":{"all":{"type":"boolean","description":"print every open subgoal instead of the focused one","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_tree","description":"List the open subgoals as a tree of dotted-path labels -- [1], [1.2], [2.1.1] -- showing how the splits nest, and marking the focused one. Those labels are exactly what ec_focus accepts. Set full for whole goal bodies rather than one-line conclusions. The labels are not stable across focus changes: the tree always shows the focused goal first, so re-read it after every ec_focus. Does not advance the engine.","inputSchema":{"type":"object","properties":{"full":{"type":"boolean","description":"print full goal bodies instead of one-line conclusions","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_focus","description":"Rotate the focus onto the subgoal at dotted path PATH, as printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"). The path walks the tree, one component per level, so a single integer selects the k-th TOP-LEVEL node -- not the k-th open goal: with four goals nested under two top-level nodes, \"3\" is out of range. Selecting a node that is an internal frame rather than a leaf goal is an error. The special value \"next\" is a different operation, not a synonym for \"2\": it moves to the next open subgoal in ec_goals-with-all order, whatever the nesting, and the two coincide only when the tree is flat. Subsequent tactics act on the focused goal.","inputSchema":{"type":"object","properties":{"path":{"type":"string","description":"\"N\", a dotted path \"N1.N2...\", or \"next\""}},"required":["path"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_undo","description":"Undo the last engine step, returning to the immediately preceding state. The ec_commit transcript is trimmed to match. Fails when there is nothing left to undo.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_revert","description":"Return the session to an earlier state, named either by a uuid reported in some previous structuredContent or by a name given to ec_checkpoint. Reverting is instant, unlike re-running ec_load, so going back to the uuid ec_load returned is the cheap way to restart a proof from scratch after a failed experiment. The ec_commit transcript is trimmed to match.","inputSchema":{"type":"object","properties":{"target":{"type":"string","description":"a uuid (as a decimal string) or a checkpoint name"}},"required":["target"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_checkpoint","description":"Record the current uuid under NAME, so that ec_revert can address it by name later. Worth doing before a branching experiment, when carrying the bare uuid around is awkward. Does not change the proof state.","inputSchema":{"type":"object","properties":{"name":{"type":"string","description":"checkpoint name"}},"required":["name"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_commit","description":"Emit the phrases recorded since the last ec_load as a proof body, with bullets inserted at every multi-child split: the result compiles under `pragma +strict_bullets' and can be pasted straight into the source file. Queries (search, print, locate, ec_search) are never recorded, so looking things up mid-proof does not pollute the body, and ec_undo / ec_revert trim the transcript. Still works after `qed.'. Does not change the proof state.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_search","description":"Search the environment for lemmas matching an EasyCrypt search pattern. This is pattern syntax, not keyword search: use _ as the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ <= _)\". Requires a loaded file. The query neither advances the proof nor enters the ec_commit transcript.","inputSchema":{"type":"object","properties":{"pattern":{"type":"string","description":"an EasyCrypt search pattern"}},"required":["pattern"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}}]}} +{"jsonrpc":"2.0","id":1,"result":{"tools":[{"name":"ec_load","description":"Reset the session and compile FILE from the top, stopping after the last sentence that ends on or before LINE (and column COL when given). This is the entry point: every other tool needs a loaded file, and tactics need the position to land inside a proof. Set nosmt to weaken SMT calls while replaying a prefix that was already verified, which is much faster on large files. Set noproof to go further and skip the prefix's proofs altogether, admitting every lemma before the target on its statement alone -- only the proof the position lands inside is replayed, which is the fastest way into a proof in a long file. Set trace to have the reply describe the last loaded sentence as BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports where compilation stopped and the resulting goal state; note the uuid it returns, reverting to it is the instant way back to the start of the proof.","inputSchema":{"type":"object","properties":{"file":{"type":"string","description":"path to the .ec/.eca file"},"line":{"type":"integer","description":"stop after the last sentence ending on or before this line; omit to compile the whole file"},"col":{"type":"integer","description":"column bound within `line'; requires `line'"},"nosmt":{"type":"boolean","description":"weaken SMT calls while compiling the prefix","default":false},"noproof":{"type":"boolean","description":"skip the prefix's proofs entirely, admitting the lemmas before the target as axioms","default":false},"trace":{"type":"boolean","description":"report the proof state around the last loaded sentence","default":false}},"required":["file"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_step","description":"Run EasyCrypt sentences -- tactics, declarations, require, print, ... -- against the current session. Every complete sentence in the argument is executed, in order, exactly as if the text had been appended to the source file, and a single reply describes the state they leave behind; sentences may span several lines. Requires a file loaded with ec_load, and, for tactics, an open proof. On success the reply carries the new goal state; on failure the prover's error text comes back with isError set, the sentences before the failing one stay applied and the engine is left wherever that sentence left it -- use ec_try when you want a guaranteed rollback. Successful non-query phrases are recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one or more complete EasyCrypt sentences, each ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false,"idempotentHint":false}},{"name":"ec_try","description":"Like ec_step, but the engine is rolled back to the state it had before the call whenever a sentence fails, including input that failed only after having already advanced the proof. The failure reply sets structuredContent.reverted to true, and its uuid and goal text describe the restored state, not the point of failure. Use this to probe a tactic without having to ec_revert afterwards; use ec_step when you mean to keep whatever progress the phrase makes. A successful phrase behaves exactly as under ec_step and is recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one complete EasyCrypt sentence, ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"},"reverted":{"type":"boolean","description":"set when the phrase failed and the engine was rolled back to its pre-call state"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_goals","description":"Print the current proof state: the focused subgoal alone, or, with all set, every open subgoal. Requires an open proof, and does not advance the engine.","inputSchema":{"type":"object","properties":{"all":{"type":"boolean","description":"print every open subgoal instead of the focused one","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_tree","description":"List the open subgoals as a tree of dotted-path labels -- [1], [1.2], [2.1.1] -- showing how the splits nest, and marking the focused one. Those labels are exactly what ec_focus accepts. Set full for whole goal bodies rather than one-line conclusions. The labels are not stable across focus changes: the tree always shows the focused goal first, so re-read it after every ec_focus. Does not advance the engine.","inputSchema":{"type":"object","properties":{"full":{"type":"boolean","description":"print full goal bodies instead of one-line conclusions","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_focus","description":"Rotate the focus onto the subgoal at dotted path PATH, as printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"). The path walks the tree, one component per level, so a single integer selects the k-th TOP-LEVEL node -- not the k-th open goal: with four goals nested under two top-level nodes, \"3\" is out of range. Selecting a node that is an internal frame rather than a leaf goal is an error. The special value \"next\" is a different operation, not a synonym for \"2\": it moves to the next open subgoal in ec_goals-with-all order, whatever the nesting, and the two coincide only when the tree is flat. Subsequent tactics act on the focused goal.","inputSchema":{"type":"object","properties":{"path":{"type":"string","description":"\"N\", a dotted path \"N1.N2...\", or \"next\""}},"required":["path"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_undo","description":"Undo the last engine step, returning to the immediately preceding state. The ec_commit transcript is trimmed to match. Fails when there is nothing left to undo.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_revert","description":"Return the session to an earlier state, named either by a uuid reported in some previous structuredContent or by a name given to ec_checkpoint. Reverting is instant, unlike re-running ec_load, so going back to the uuid ec_load returned is the cheap way to restart a proof from scratch after a failed experiment. The ec_commit transcript is trimmed to match.","inputSchema":{"type":"object","properties":{"target":{"type":"string","description":"a uuid (as a decimal string) or a checkpoint name"}},"required":["target"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_checkpoint","description":"Record the current uuid under NAME, so that ec_revert can address it by name later. Worth doing before a branching experiment, when carrying the bare uuid around is awkward. Does not change the proof state.","inputSchema":{"type":"object","properties":{"name":{"type":"string","description":"checkpoint name"}},"required":["name"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_commit","description":"Emit the phrases recorded since the last ec_load as a proof body, with bullets inserted at every multi-child split: the result compiles under `pragma +strict_bullets' and can be pasted straight into the source file. Queries (search, print, locate, ec_search) are never recorded, so looking things up mid-proof does not pollute the body, and ec_undo / ec_revert trim the transcript. Still works after `qed.'. Does not change the proof state.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_strict","description":"Turn strict mode on or off. Off (the default) a session behaves as a source file does: a failing phrase is reported and the next call runs against wherever it left the engine. On, the session stops at a failure that may have moved the engine, and ec_step, ec_try and ec_focus are refused until it is resynchronized -- by ec_undo, ec_revert or ec_load, which arrive somewhere definite, or by ec_resume, which says so. Turn it on if you send one phrase per call and act on each result: without it a failure is followed by calls landing on a state you did not mean, and the drift is silent. Reads (ec_goals, ec_tree, ec_search, ec_checkpoint, ec_commit) always answer, stopped or not.","inputSchema":{"type":"object","properties":{"on":{"type":"boolean","description":"true to stop the session at a failure"}},"required":["on"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_resume","description":"Release a strict-mode stop without moving the engine: you have read the failure and mean to carry on from where it left the session. Use ec_undo or ec_revert instead when you would rather go back. Fails when the session is not stopped, or when strict mode is off -- either way you are not where you think you are, which is what strict mode is for.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_search","description":"Search the environment for lemmas matching an EasyCrypt search pattern. This is pattern syntax, not keyword search: use _ as the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ <= _)\". Requires a loaded file. The query neither advances the proof nor enters the ec_commit transcript.","inputSchema":{"type":"object","properties":{"pattern":{"type":"string","description":"an EasyCrypt search pattern"}},"required":["pattern"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}}]}} diff --git a/tests/mcp/scripts/strict-stop.script b/tests/mcp/scripts/strict-stop.script new file mode 100644 index 000000000..69bf6fa45 --- /dev/null +++ b/tests/mcp/scripts/strict-stop.script @@ -0,0 +1,21 @@ +# exit: 0 +# Strict mode over MCP, and the one case the REPL cannot show: ec_try +# is refused while stopped like anything else that would advance, +# although a failing ec_try never arms the stop in the first place -- +# its contract is that a failure moves nothing, so there is no drift +# to prevent. +# +# `apply nosuchlemma.' fails after `split.' has moved the engine, so +# the session stops. ec_step and ec_try are then refused with isError; +# ec_goals and ec_commit answer; ec_resume releases it. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_strict","arguments":{"on":true}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_try","arguments":{"phrase":"apply nosuchlemma."}}} +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"split. apply nosuchlemma."}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"trivial."}}} +{"jsonrpc":"2.0","id":7,"method":"tools/call","params":{"name":"ec_try","arguments":{"phrase":"trivial."}}} +{"jsonrpc":"2.0","id":8,"method":"tools/call","params":{"name":"ec_goals","arguments":{}}} +{"jsonrpc":"2.0","id":9,"method":"tools/call","params":{"name":"ec_commit","arguments":{}}} +{"jsonrpc":"2.0","id":10,"method":"tools/call","params":{"name":"ec_resume","arguments":{}}} +{"jsonrpc":"2.0","id":11,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"trivial."}}}