EasyCrypt · strub · May 26, 2026 · May 27, 2026
diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md
@@ -6,59 +6,267 @@ computations, program logics (Hoare logic, probabilistic Hoare logic,
 probabilistic relational Hoare logic), and ambient mathematical
 reasoning.
 
-## Using the `llm` command
+## Using the `llm` interactive mode
 
-The `llm` subcommand is designed for non-interactive, LLM-friendly
-batch compilation. It produces no progress bar and no `.eco` cache
-files.
+The `llm` subcommand provides an interactive REPL with a
+machine-friendly protocol designed for LLM agents. The LLM sends
+commands over stdin and receives structured responses on stdout.
 
 ```
-easycrypt llm [OPTIONS] FILE.ec
+easycrypt llm [OPTIONS]
 ```
 
-### Options
+Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are
+available. Use `-help` to print this guide and exit:
 
-- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not
-  including) the given location, then print the current goal state to
-  stdout and exit with code 0. Use this to inspect the proof state at
-  a specific point in a file.
+```
+easycrypt llm -help
+```
 
-- `-lastgoals` — On failure, print the goal state (as it was just
-  before the failing command) to stdout, then print the error to
-  stderr, and exit with code 1. Use this to understand what the
-  failing tactic was supposed to prove.
+### Protocol
 
-Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are
-also available.
+**Startup.** EasyCrypt prints a `READY` message and waits for input:
+
+```
+READY [uuid:0]
+<END>
+```
+
+**Responses.** Every response has a typed envelope and an `<END>`
+sentinel:
+
+```
+OK [uuid:N]
+<body>
+<END>
+```
+
+```
+ERROR [uuid:N]
+<error message>
+<END>
+```
+
+The `uuid` is a monotonically increasing integer identifying the proof
+engine state. It increments with each successful command.
+
+### Meta-commands
+
+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) |
+| `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
+
+Any line that is not a meta-command is parsed as EasyCrypt input.
+This covers tactics, declarations, `search`, `print`, `require`,
+etc. The line must be a complete EasyCrypt statement ending with `.`
+
+```
+smt().
+rewrite H1 H2.
+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:**
+
+```
+LOAD "myfile.ec" 42
+```
+
+This compiles the file through line 42 (processing any command whose
+end is on or before that line). The response includes where it
+stopped:
+
+```
+OK [uuid:15] [loaded:myfile.ec:42]
+Current goal
+...
+<END>
+```
+
+For large files, use `-nosmt` to skip SMT calls during prefix
+compilation (safe when the prefix was already verified):
+
+```
+LOAD "myfile.ec" 436 -nosmt
+```
+
+Add `-trace` to a LOAD to inspect the proof state around the last
+loaded sentence. The reply body contains four delimited blocks:
+
+```
+LOAD "myfile.ec" 42 -trace
+
+=== BEFORE: line 42 (col 0) ===
+<focused goal before the sentence>
+=== TACTIC (lines 42:0 - 42:10) ===
+<exact source text of the sentence>
+=== AFTER: line 42 (col 0) ===
+<new focused goal, plus any new sibling goals>
+=== SUMMARY ===
+open goals: N1 -> N2
+```
+
+The position comes from the existing `LINE[:COL]` argument; omit it to
+trace the file's last sentence. On tactic failure the reply uses the
+`ERROR` envelope and still includes the BEFORE/TACTIC blocks plus an
+`<sentence failed>` marker in the AFTER block.
+
+**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.
+
+```
+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()
+```
 
-### Output conventions
+To restart the proof from scratch, revert to the LOAD uuid:
 
-- **Goals** are printed to **stdout**.
-- **Errors** are printed to **stderr**.
-- **Exit code 0** means success (or `-upto` reached its target).
-- **Exit code 1** means a command failed.
-- If there is no active proof at the point where goals are requested,
-  stdout will contain: `No active proof.`
+```
+REVERT 15               ← back to the state right after LOAD
+```
 
-### Workflow for writing and debugging proofs
+Always note the LOAD uuid so you can return to it.
 
-1. Try to write a pen-and-paper proof first.
+**3. Use checkpoints for branching exploration:**
 
-2. Write the `.ec` file with your proof attempt. For a large proof,
-   write down skeleton and `admit` subgoals first, and then detail
-   the proof.
+```
+CHECKPOINT before_split
+split.
+smt().          ← fails
+REVERT before_split
+apply H.        ← try a different approach
+```
 
-3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file.
-   - If it succeeds (exit 0), you are done.
-   - If it fails (exit 1), read the error from stderr and the goal
-     state from stdout to understand what went wrong.
+**4. Use QUIET mode to save tokens during bulk tactic application:**
 
-4. Use `-upto LINE` to inspect the proof state at a specific point
-   without running the rest of the file. This is useful for
-   incremental proof development.
+```
+QUIET ON
+rewrite H1.
+rewrite H2.
+rewrite H3.
+QUIET OFF
+GOALS
+```
+
+**5. Search for lemmas using patterns:**
 
-5. Fix the proof and repeat from step 2. The ultimate proof should
-   not contain `admit` or `admitted`.
+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 (fdom _)
+SEARCH (_ %/ _)
+```
+
+## EasyCrypt proof strategy
+
+### General approach
+
+- Start with a pen-and-paper proof plan before writing tactics.
+- Use `smt()` aggressively. Try it first — if it fails, add hints:
+  `smt(lemma1 lemma2)`.
+- Build proofs with `have` assertions. Establish intermediate facts
+  as named hypotheses, then combine with `smt()`. Avoid long rewrite
+  chains.
+- Case split early: `case (n = 0) => [->|hn0].` Base cases often
+  close by computation.
+- Provide specific instances of lemmas to smt:
+  `have h := lemma arg1 arg2.` SMT works much better with ground
+  instances than with universally quantified axioms.
+
+### Integer division (`%/`)
+
+- `divzK`: `d %| m => m %/ d * d = m` — recovering from exact
+  division
+- `mulzK`: `d <> 0 => m * d %/ d = m` — canceling a known factor
+- `divzMpl`: `0 < p => p * m %/ (p * d) = m %/ d` — simplifying
+  common factors
+- To prove `a %/ d = x`, establish `a = x * d` (with `d %| a`),
+  then use `mulzK`.
+- Don't try to rewrite inside `%/` expressions directly. Instead,
+  prove the equality as a `have` and use it.
+
+### What works, what doesn't
+
+- `ring` solves polynomial equalities over integers but treats
+  abstract ops (like `fact`) as opaque. It **cannot** simplify
+  `fact(n-1+1)` to `fact(n)`.
+- `smt()` can do linear arithmetic and combine hypotheses, but
+  struggles with nonlinear integer division. Pre-compute key facts
+  with `have` and `divzK`/`mulzK`, then let smt combine them.
+- `rewrite {k}h` rewrites the k-th occurrence only. Essential when a
+  term appears on both sides of an equation.
+- 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
+  `first smt()` or provide the precondition explicitly.
+- `by` closes **all** remaining subgoals. If it fails, the error
+  refers to the first unclosed goal, which may not be the intended
+  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
 
@@ -91,8 +299,6 @@ proof. by ring. qed.
 
 ### Common tactics
 
-<!-- TODO: expand this section with descriptions and examples -->
-
 - `trivial` — solve trivial goals
 - `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints
 - `auto` — automatic reasoning
@@ -141,9 +347,10 @@ proof. by ring. qed.
 
 ### Guidelines
 
-* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals).
+* Use SMT solver only in direct mode (smt() or /#) on simple goals
+  (arithmetic goals, pure logical goals).
 
 * Refrain from unfolding operator definitions unless necessary.
-  If you need more properties on an operator, state this property in a dedicated lemma,
-  but avoid unfolding definitions in higher level proofs.
-
+  If you need more properties on an operator, state this property
+  in a dedicated lemma, but avoid unfolding definitions in higher
+  level proofs.
diff --git a/dune b/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))