[ScottMoore0]

Adds bend <file.bend> --profile: it checks the file as --check-only does, one order entry at a time, lists the 20 slowest entries with file and line, then gives --check-only's verdict and exit code. It adds 77 lines to main.ts (+958 tokens, 12,489 of the 16,000 cap) and doesn't touch bend.ts. It's independent of #1631: the two merge cleanly, and together leave main.ts at about 12,900.

$ bend proofs/crypto/aes/inverse.bend --profile
583 of 583 entries checked in 3901 ms; the slowest:
   3759.4 ms  96.4%  inverse_unit_bits (proof)  proofs/crypto/aes/inverse.bend:12
     13.8 ms   0.4%  inverse_zero (proof)  proofs/crypto/aes/inverse.bend:573
      6.6 ms   0.2%  U32.pow  Base:1624
...
ALL PROOFS CHECK
Use --verdict for mathematical validity.

How it works. book_valid(book, done) takes the first done entries as validated. cli_profile cuts the order after entry i and calls book_valid(book, i), so each call checks one entry against the entries before it, on the same book. Checked bodies and template instances stay in the book, so the times are the full check's, split by entry.

book_valid hides the bodies of the defs in the order it's given until their last entry. Because the order is cut at each step, cli_profile hides every body up front, as the full check does. Without that, a later def's body would be visible early and a forward reference would check. A law's statement entry keeps its body hidden, so its proof is timed once, at its fill, and rows are labelled (statement) or (proof). After the last entry it counts TODOs and calls cli_verdict, as --check-only does.

This is the loop from a standalone tool I published at https://github.com/ScottMoore0/bend-prof, offered here so it ships with bend.

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

• All 1,666 .bend files under tests/: --profile's output, with the table removed, is identical to --check-only's, and so is the exit code. This includes forward references, unfilled laws, TODOs and @unsafe dependants.
• --check-only output is unchanged by the patch (first 400 test files compared).
• Per-entry times add up to about a plain check: 3.9 s against 4.0 s on aes/inverse.bend (583 entries), and 1.2 s against 0.9 s on a dynamic_array proof (1,851 entries; each call has a small fixed cost).
• --profile with any other option fails with "--profile takes no other option".
• gates/repo.ts: PASS 54 / 54. tsc --noEmit reports the same errors as on main, none in main.ts.

Not run: gates/test.ts and gates/safe.ts on the minis. There's no test file for it, since its output is timings.

Happy to change the flag name, the row count or the output format, or to drop the verdict at the end.

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

[Lorenzobattistela]

Thanks for this, Scott, and for the careful testing (the full tests/ sweep against --check-only and the timing sanity checks especially).

We're going to close it, though. We're trying to keep the CLI small, and per-entry profiling is the kind of thing that works better outside the language: an agent can put together a one-off loop over book_valid quickly when someone needs it, and if we want a proper tool, a standalone Bend profiler (like your bend-prof) is a better home than a bend flag. Your repo already covers that well, so linking to it is probably the best way to get it to people.

Thanks again, and please keep the audit findings coming.