[ScottMoore0]

Closes #1234 if you want it in this form; otherwise it's a reference for your own version. It's an opt-in check cache for --check-only. It adds 34 lines to main.ts and changes 5 (+421 tokens, 11,952 of the 16,000 cap), and doesn't touch bend.ts.

Idea. book_valid(book, done) already takes the first done order entries as validated. A file's imports load before its own entries and can't name them, so the imports' entries check the same whatever the file adds. With BEND_CACHE=<dir> set, a successful --check-only records two keys:

• the prefix it checked before its own entries;
• its whole order (so a file that imports this one can skip all of it).

A later run that loads the same prefix starts book_valid after it.

What the key covers. A sha256 of VERSION, bend.ts, base.bend, the path and contents of every loaded file, and the exact list of entry names in the prefix. If any of these changes, it's a miss and a full check. The file's own entries are found by b, which marks Base's entries, so a file without import Base gets an empty prefix.

Scope. Only --check-only:

• --verdict needs every def's elaborated term, so it never uses the cache;
• a plain run and -o builds never use it either.

book_promises falls back to the def's body as written when a cached def has no elaborated term, so @unsafe and foreign-effect dependants are still reported.

Measured on the reproduction in #1234 (a library of 800 proofs, 10 small clients):

	stock	cached
client_0, first run	1.22 s	1.44 s (writes the cache)
client_0, again	1.22 s	0.13 s
clients 1–9, each for the first time	12.13 s	1.07 s

Tested on a copy of main at e5527d5 (this branch's main.ts is byte-identical to it):

• All 1,666 .bend files under tests/, --check-only text compared against stock: 0 differences cold, and 0 warm with one cache shared across all of them.
• Unsafe propagation through an imported body (lib has an @unsafe def, a client calls it): stock, cold, warm, and warm-from-another-client's-cache all report the same 3 dependent defs. --verdict still fails.
• A broken library proof is caught after the library changes, and so is a false law in a client.
• A failing file without import Base, checked right after a passing one with the same entry count, still fails.
• gates/repo.ts: PASS 54 / 54. tsc --noEmit reports the same errors as on main, all in bend.ts and safe.ts, none in main.ts.

Not run: gates/test.ts and gates/safe.ts on the minis.

Limits:

• The cache trusts its directory. Anyone who can write to it can mark a prefix as checked, so it's opt-in and should be a private directory.
• It caches whole prefixes, not single defs: an edit to a library re-checks everything after it in load order.

Happy to change the interface (a flag instead of an env var, a default directory) or the scope.

Found and tested with Claude Code, running Claude Opus 5.5, during an audit of --verdict.

[Lorenzobattistela]

Thanks for this, and for the careful write-up: the measurements and the cold/warm comparison over the whole test suite were really useful to read.

We're going to close it, though. We don't want a check cache inside the CLI itself. We're planning a separate tool for incremental checking that the LSP and other tools can build on, and caching will live there. That's no comment on the quality of the patch, and #1234 stays the reference for the problem.

A few things I noticed at a glance while reading the diff. I haven't run anything, so treat them as unverified, but they may help whoever picks this up in the new tool:

1. A skipped prefix can hide a TODO. book_valid counts a missing body as a TODO (and checks a body) only at a name's last place in the load order (fin). In PROOF.bend, a LAWS law that PROOF fills isn't counted in the prefix. If PROOF passes and saves its prefix key, another file that imports the same LAWS (same alias, same files) gets the same key, skips the count, and passes with an unproven law. Stock reports 1 TODO found. So the imports' entries don't always check the same whatever the root adds.

2. The whole-order key may never match. In an importer, an aliased import's names carry the alias (Lib:x), while the same file checked as the root has bare names (x), and the order of seen can differ too. All of the --check-only re-checks the whole import closure for every file (repro, see #1209) #1234 speedup seems to come from the prefix key.

3. Installed binary: in the compiled build, BEND_DIR is <exe>/../bend2. If bend.ts isn't shipped there, the key's readFileSync throws as soon as BEND_CACHE is set.

4. The book_promises fallback to term_lower(t.v) also applies outside the cache, to any def with a body but no elaborated term. The written body and the elaborated term can name different things: extra references could give false FAILs, and a reference only elaboration adds would be missed (a possible false PASS on an @unsafe dependency).

Thanks again for digging into this!