Add LLM REPL improvements and built-in guide

New REPL features:
- LOAD -nosmt: skip SMT calls during prefix compilation (uses
  Proofs:weak pragma), restores strict mode for interactive tactics
- Error responses now include the current goal state, eliminating
  the need for a separate GOALS roundtrip after failures
- Multi-line input support via <BEGIN>/<DONE> delimiters
- HELP meta-command and -help flag: print the LLM agent guide
  (doc/llm/CLAUDE.md) from within the REPL or at startup

The guide is installed as part of the distribution (doc site) so it
stays version-matched with the binary. Agent frameworks can use
`easycrypt llm -help` to populate their system prompt automatically.

Documentation updates:
- REVERT-to-LOAD-uuid workflow (instant restart vs recompile)
- Pattern-based search syntax with examples
- SMT usage guidance (pure arithmetic/logic only)
- rewrite-in-H clarification

Author: strub

doc/llm/CLAUDE.md

@@ -17,7 +17,11 @@ easycrypt llm [OPTIONS]
 ```
 
 Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are
-available.
+available. Use `-help` to print this guide and exit:
+
+```
+easycrypt llm -help
+```
 
 ### Protocol
 
@@ -52,14 +56,16 @@ These are protocol-level commands, not EasyCrypt syntax:
 
 | Command | Description |
 |---------|-------------|
-| `LOAD "file.ec" [LINE[:COL]]` | Reset state, compile file up to the given line |
+| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) |
 | `UNDO` | Undo the last proof step |
 | `REVERT <uuid-or-name>` | Revert to a specific state (by uuid or checkpoint name) |
 | `GOALS` | Print the current goal (first subgoal only, with remaining count) |
 | `GOALS ALL` | Print all subgoals |
 | `CHECKPOINT <name>` | Save current uuid under a name for later `REVERT` |
 | `SEARCH <pattern>` | Search for lemmas matching a pattern |
 | `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics |
+| `<BEGIN>` / `<DONE>` | Delimit multi-line EasyCrypt input |
+| `HELP` | Print this guide |
 | `QUIT` | Exit |
 
 ### EasyCrypt commands
@@ -75,6 +81,16 @@ search (%/).
 print mulzK.
 ```
 
+For multi-line statements, wrap with `<BEGIN>` and `<DONE>`:
+
+```
+<BEGIN>
+lemma test :
+  0 <= n =>
+  0 < n + 1.
+<DONE>
+```
+
 ### Workflow
 
 **1. Load a file up to the proof point:**
@@ -94,19 +110,37 @@ Current goal
 <END>
 ```
 
-**2. Try tactics interactively:**
+For large files, use `-nosmt` to skip SMT calls during prefix
+compilation (safe when the prefix was already verified):
 
 ```
-smt().
+LOAD "myfile.ec" 436 -nosmt
 ```
 
-If it fails, the state is unchanged — try another tactic immediately:
+**2. Try tactics, using REVERT to restart:**
+
+The uuid returned by LOAD is a revertible state. Use `REVERT` to
+return to it after failed experiments — this is instant, unlike
+re-doing LOAD which recompiles the prefix.
 
 ```
-rewrite H1.
-smt(lemma1 lemma2).
+LOAD "myfile.ec" 42
+→ OK [uuid:15] [loaded:myfile.ec:42]
+
+smt().                  ← fails, state unchanged
+rewrite H1. smt().      ← succeeds (uuid:17)
+rewrite H2.             ← wrong direction
+REVERT 17               ← back to after the successful smt()
 ```
 
+To restart the proof from scratch, revert to the LOAD uuid:
+
+```
+REVERT 15               ← back to the state right after LOAD
+```
+
+Always note the LOAD uuid so you can return to it.
+
 **3. Use checkpoints for branching exploration:**
 
 ```
@@ -128,11 +162,23 @@ QUIET OFF
 GOALS
 ```
 
-**5. Search for lemmas:**
+**5. Search for lemmas using patterns:**
+
+EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as
+wildcard:
+
+```
+search (fdom _).                ← lemmas involving fdom
+search (_ %/ _).                ← integer division lemmas
+search (card (_ `|` _)).        ← card of union
+search (mu _ _) (_ <= _).       ← mu lemmas with inequalities
+```
+
+The SEARCH meta-command is a shorthand that adds `search`/`.`:
 
 ```
-SEARCH mulzK
-SEARCH dvdz
+SEARCH (fdom _)
+SEARCH (_ %/ _)
 ```
 
 ## EasyCrypt proof strategy
@@ -176,6 +222,18 @@ SEARCH dvdz
 - For induction on naturals: `elim/natind: n` gives base (`n ≤ 0`)
   and step (`0 ≤ n → P n → P (n+1)`).
 
+### SMT usage
+
+`smt()` and `/#` are equivalent — both call external SMT solvers.
+
+- Use `smt()` **only** on goals that are pure arithmetic or pure
+  propositional logic. If the goal contains abstract operators,
+  FMap terms, or `if-then-else`, reduce it first with `rewrite`,
+  `case`, or `have` before calling `smt()`.
+- If `smt()` takes more than 1 second, the goal is too complex.
+  Simplify with interactive tactics instead of increasing the
+  timeout.
+
 ### Common pitfalls
 
 - `rewrite (factS n) //` generates a side goal `0 <= n`. Use
@@ -185,6 +243,9 @@ SEARCH dvdz
   one.
 - When a tactic generates multiple subgoals, each subgoal must be
   closed in order. Use `GOALS ALL` to see them all.
+- `rewrite lemma in H` modifies hypothesis `H` in place (it does
+  not consume it). If you need to preserve the original, copy it
+  first: `have H' := H; rewrite lemma in H'`.
 
 ## EasyCrypt language overview
 

dune

@@ -1,12 +1,14 @@
-(dirs 3rdparty src etc theories examples assets scripts)
+(dirs 3rdparty src etc theories examples assets scripts doc)
 
 (install
   (section (site (easycrypt commands)))
   (files (scripts/testing/runtest as runtest)))
 
 (install
   (section (site (easycrypt doc)))
-  (files (assets/styles/styles.css as styles.css)))
+  (files
+    (assets/styles/styles.css as styles.css)
+    (doc/llm/CLAUDE.md as llm-guide.md)))
 
 (install
   (section (bin))

src/ec.ml

@@ -408,7 +408,34 @@ let main () =
   (* LLM interactive mode                                                  *)
   (* -------------------------------------------------------------------- *)
 
-  let run_llm_repl (prvopts : prv_options) =
+  let llm_guide_path () =
+    let (module Sites) = EcRelocate.sites in
+    match EcRelocate.sourceroot with
+    | Some root ->
+      Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md"
+    | None ->
+      Filename.concat Sites.doc "llm-guide.md"
+  in
+
+  let print_llm_guide () =
+    let path = llm_guide_path () in
+    try
+      let ic = open_in path in
+      begin try while true do
+        print_char (input_char ic)
+      done with End_of_file -> () end;
+      close_in ic
+    with Sys_error e ->
+      Printf.eprintf "cannot read LLM guide: %s\n%!" e
+  in
+
+  let run_llm_repl (llmopts : llm_option) =
+    if llmopts.llmo_help then begin
+      print_llm_guide ();
+      exit 0
+    end;
+
+    let prvopts = llmopts.llmo_provers in
     (* Initialize PRNG *)
     Random.self_init ();
 
@@ -510,8 +537,15 @@ let main () =
     in
 
     let reply_error msg =
-      Printf.printf "ERROR [uuid:%d]\n%s\n<END>\n%!"
-        (EcCommands.uuid ()) msg;
+      let goals = goals_to_string () in
+      Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg;
+      if goals <> "" then begin
+        print_string goals;
+        let len = String.length goals in
+        if len > 0 && goals.[len - 1] <> '\n' then
+          print_char '\n'
+      end;
+      Printf.printf "<END>\n%!";
       Buffer.clear notices
     in
 
@@ -592,16 +626,27 @@ let main () =
             | f :: rest -> (f, String.concat " " rest)
         in
 
-        (* Parse optional LINE[:COL] *)
-        let upto =
-          if rest = "" then None
+        (* Parse optional LINE[:COL] and flags (-nosmt) *)
+        let upto, nosmt =
+          if rest = "" then (None, false)
           else
-            match String.split_on_char ':' rest with
-            | [line] ->
-              Some (int_of_string line, None)
-            | [line; col] ->
-              Some (int_of_string line, Some (int_of_string col))
-            | _ -> failwith "LOAD: invalid LINE[:COL] format"
+            let words = String.split_on_char ' ' rest in
+            let words = List.filter (fun s -> s <> "") words in
+            let nosmt = List.mem "-nosmt" words in
+            let words = List.filter (fun s -> s <> "-nosmt") words in
+            let upto = match words with
+              | [] -> None
+              | [w] ->
+                begin match String.split_on_char ':' w with
+                | [line] ->
+                  Some (int_of_string line, None)
+                | [line; col] ->
+                  Some (int_of_string line, Some (int_of_string col))
+                | _ -> failwith "LOAD: invalid LINE[:COL] format"
+                end
+              | _ -> failwith "LOAD: unexpected arguments"
+            in
+            (upto, nosmt)
         in
 
         (* Validate file extension *)
@@ -632,6 +677,9 @@ let main () =
 
         let last_loc = ref None in
 
+        (* In -nosmt mode, admit all SMT calls during prefix loading *)
+        if nosmt then EcCommands.pragma_check `WeakCheck;
+
         begin try while true do
           let (src, prog) = EcIo.xparse reader in
           let src = String.strip src in
@@ -653,10 +701,17 @@ let main () =
             EcCommands.doc_comment doc
         done with
         | Exit | End_of_file -> ()
-        | e -> EcIo.finalize reader; raise e
+        | e ->
+          EcIo.finalize reader;
+          if nosmt then EcCommands.pragma_check `Check;
+          raise e
         end;
 
         EcIo.finalize reader;
+
+        (* Restore full SMT checking for interactive tactics *)
+        if nosmt then EcCommands.pragma_check `Check;
+
         let tag =
           match !last_loc with
           | None -> ""
@@ -685,14 +740,49 @@ let main () =
       (EcCommands.uuid ());
 
     (* Main REPL loop *)
+    let multi_buf = Buffer.create 256 in
+    let in_multi = ref false in
+
     begin try while true do
       let line = input_line stdin in
       let line = String.strip line in
 
-      if line = "" then
+      (* Multi-line input: <BEGIN> starts, <DONE> flushes *)
+      if line = "<BEGIN>" then begin
+        Buffer.clear multi_buf;
+        in_multi := true
+      end
+      else if line = "<DONE>" && !in_multi then begin
+        let input = Buffer.contents multi_buf in
+        Buffer.clear multi_buf;
+        in_multi := false;
+        if input <> "" then process_ec_input input
+      end
+      else if !in_multi then begin
+        if Buffer.length multi_buf > 0 then
+          Buffer.add_char multi_buf ' ';
+        Buffer.add_string multi_buf line
+      end
+
+      else if line = "" then
         ()
       else if line = "QUIT" then
         exit 0
+      else if line = "HELP" then begin
+        Buffer.clear notices;
+        let buf = Buffer.create 4096 in
+        let path = llm_guide_path () in
+        begin try
+          let ic = open_in path in
+          begin try while true do
+            Buffer.add_char buf (input_char ic)
+          done with End_of_file -> () end;
+          close_in ic;
+          reply_ok (Buffer.contents buf)
+        with Sys_error e ->
+          reply_error (Printf.sprintf "cannot read guide: %s" e)
+        end
+      end
       else if line = "UNDO" then begin
         Buffer.clear notices;
         let uuid = EcCommands.uuid () in
@@ -910,7 +1000,8 @@ let main () =
 
     | `Llm llmopts ->
         run_llm_repl
-          {llmopts.llmo_provers with prvo_iterate = true}
+          {llmopts with llmo_provers =
+            {llmopts.llmo_provers with prvo_iterate = true}}
 
     | `Runtest _ ->
         (* Eagerly executed *)

src/ecOptions.ml

@@ -50,6 +50,7 @@ and doc_option = {
 
 and llm_option = {
   llmo_provers   : prv_options;
+  llmo_help      : bool;
 }
 
 and prv_options = {
@@ -358,7 +359,8 @@ let specs = {
 
     ("llm", "LLM-friendly interactive mode", [
       `Group "loader";
-      `Group "provers"]);
+      `Group "provers";
+      `Spec  ("help", `Flag, "Print the LLM agent guide and exit")]);
 
     ("cli", "Run EasyCrypt top-level", [
       `Group "loader";
@@ -543,7 +545,8 @@ let doc_options_of_values values input =
     doco_outdirp   = get_string "outdir" values; }
 
 let llm_options_of_values ini values =
-  { llmo_provers   = prv_options_of_values ini values; }
+  { llmo_provers   = prv_options_of_values ini values;
+    llmo_help      = get_flag "help" values; }
 
 (* -------------------------------------------------------------------- *)
 let parse getini argv =

src/ecOptions.mli

@@ -46,6 +46,7 @@ and doc_option = {
 
 and llm_option = {
   llmo_provers   : prv_options;
+  llmo_help      : bool;
 }
 
 and prv_options = {