[llm] LOAD -noproof: admit the prefix's lemmas instead of proving them - #1117
Open
bgregoir wants to merge 3 commits into
Open
[llm] LOAD -noproof: admit the prefix's lemmas instead of proving them#1117bgregoir wants to merge 3 commits into
bgregoir wants to merge 3 commits into
Conversation
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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014sRvA8imiFo9jSNLbPuX9W
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y2YZRRxpC8R1Ho2NGpD1fg
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y2YZRRxpC8R1Ho2NGpD1fg
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Replaying a long file to reach one proof spends nearly all its time re-proving lemmas that were already verified.
-nosmtonly silences the provers; the elaboration of every tactic in the prefix remains.LOAD "f.ec" LINE -noproofskips the prefix's proofs whole. The mechanism is the onerequirealready uses: a file is read with proof checking off, soAx.addstarts each lemma inPSNoCheck, its script is not even typed, andqedbinds 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.ecup 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
undomoves 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 afail tac.inside a skipped proof pins an error that can no longer happen, the tactic not being run, soprocess_actiongains~nofailto drop that verdict there -- without it-noprooffailed on files that compile,tests/bullets-errors.ecamong them.Plumbing:
EcScope.Prover.{get,set}_check_moderead and write the mode as it is, whichcheck_proofcannot (it is anOn/Offtoggle that ignoresForced), andEcCommands.{check,set_check}_modeapply it to the whole undo stack, so it behaves like a pragma rather than a scope the undo stack could take back.Claude-Session: https://claude.ai/code/session_014sRvA8imiFo9jSNLbPuX9W