[llm] LOAD -noproof: admit the prefix's lemmas instead of proving them

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)

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 <uuid-or-name>` | Revert to a specific state (by uuid or checkpoint name) |
 | `GOALS` | Print the current goal (first subgoal only, with remaining count) |
@@ -102,6 +102,8 @@ These are protocol-level commands, not EasyCrypt syntax:
 | `CHECKPOINT <name>` | Save current uuid under a name for later `REVERT` |
 | `SEARCH <pattern>` | 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 |
 | `<BEGIN>` / `<DONE>` | Delimit multi-line EasyCrypt input |
 | `HELP` | Print this guide |
 | `QUIT` | Exit |
@@ -167,6 +169,72 @@ 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.
+
+**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:
 
@@ -307,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
@@ -318,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:
@@ -366,12 +476,12 @@ 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 |
 |------|-----------|-------------|
-| `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 |
@@ -381,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`, `-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
+mirror the REPL meta-commands — `-nosmt`, `-noproof`, `-trace`, dotted paths,
+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
 `<BEGIN>`/`<DONE>` (a `phrase` may simply contain newlines), `QUIET`
 has no purpose when the client decides what to display, `HELP` is this