Review fixes for prove-and-retire (#994) by MauroToscano · Pull Request #995 · yetanotherco/lambda_vm

MauroToscano · 2026-09-18T18:06:14Z

Fixes from an adversarial review of #994, onto its own branch so the review
trail stays separate from the feature work. Six commits, +370/−131, no
behaviour change to the proving path.

The one that matters

verify_batched's fold seed indexed both out-of-domain blocks at the
width/height the proof advertises, 92 lines before
ood_blocks_well_formed pinned those dimensions to the AIR. A proof whose
advertised dimensions disagree with its data length panicked in
Table::get_row's unchecked slice instead of being rejected. The guard's own
doc comment says it exists to close exactly that, and the ordinary verifier
keeps the ordering by running it inside the round-1 loop.

The three shape checks now run in the pre-pass that already validates each
table's domain. No transcript byte moves — the checks touch no transcript.
prover::batched_verifier::replay had the same pre-guard read via
Table::columns and gets the same treatment.

Direction is robustness, not soundness: nothing wrong was accepted, the
verifier aborted instead of returning false. It is unreachable from bytes
today because BatchedProof has no derives — which is also the cheapest moment
to pay for it, since serializing that format is the point of the format.

a_tampered_batched_proof_is_rejected gains five arms, including one that
lies about a block's width. That arm panics at crypto/stark/src/table.rs:362
without this change and is rejected with it — checked both ways.

The rest

CLI stopped changing the allocator for every command.
keep_large_buffers_warm() ran as the first statement of main(), so
verify, execute and --help all disabled dirty decay on the oversize
arena for the process lifetime and left a purge thread behind. It now runs
only on the prove-and-retire path, and its two silent returns log.
Separately, tikv-jemalloc-ctl had become non-optional with
features = ["stats"], which propagates to --enable-stats and put jemalloc
counters on the malloc fast path of every CLI build — including ones
measuring baselines. stats goes back behind jemalloc-stats.
--output with any stage but logup walked the whole execution, wrote
nothing and exited 0 (and with --through batched also forced a
verification, since --output is OR'd into verify). It now fails before
the walk.
Four assertions that could not fail: retire_lde_proof_is_byte_identical
compared a proof to itself under cuda (a live merge-queue config) and now
skips there and asserts the flag took effect; a > 100_000 tautology in
checkpoint_tests; and chunk_shape_matches_the_built_chunk covered the row
half for LT only, so a single generator's padding change would slip through —
it now populates MUL and SHIFT too, the latter above the 4-row padding floor.
Eight doc comments had been orphaned by an item inserted between them and
what they documented; three of the adopted sentences were wrong about their
new owner. replay_rounds_2_and_3 is renamed replay_rounds_2_to_4 because
its body still has a Round 4 section.
Residency claims corrected. pass.rs said the walk holds one table plus
the residents "no matter how long the run is", and the design doc listed LT
among the tables handed over as a chunk fills. LT, MUL, DVRM and SHIFT are
deliberately excluded from CHUNKED_KINDS — later derivations keep appending
to them — so their op lists are held whole and that term is O(cycles). It is
a small term and closing it would move LT's chunk boundaries and cost the
byte-identical-roots property, so no code changed: the documents now say
what the code does, and §10 records the gap.
Also in the design doc: a knob row quoting a sweep that does not match the one
in pass.rs; A1_INFLIGHT and LAMBDA_STREAM_LDE missing from a table that
claims to list every knob; a --features hash-metrics build command that
cannot work here (tooling(recursion): count keccak hashes to verify a proof (excl. grin… #987 is not on this branch, so the verify-hash column is not
reproducible); "the spec's Open optimization was not kept" describing code
that ships behind LAMBDA_STREAM_LDE; and §6's header missing the blowup and
knob settings.
Dead code: TableDeep::air_index (always usize::MAX, never read, with a
doc describing a mechanism that does not exist), Replay::iotas (documented
as the query indices, always empty), and a group_of loop that linearly
searched the list it was iterating for the element it already held, ending in
an unreachable expect on the prover path.
get_proof_by_pos_with_leaf_sibling read self.nodes directly where every
other read in that file goes through node_get's disk-spill indirection.
Unreachable today, but the prover's opening path expects the result.

Verification

make lint's four clippy arms (including --features lambda-vm-prover/cuda
with stub cubins) and cargo fmt --all --check all pass. Tests run in release:
all 8 batched_fri_tests, all 4 challenge_phase_tests,
chunk_shape_matches_the_built_chunk, both new merkle_tests,
prove_verify_roundtrip_tests and checkpoint_tests — green.

Not verified here: anything needing a GPU, and the ethrex block itself. The
numbers in the design doc are untouched and still rest on the author's runs.

Deliberately not addressed

The Feat/skip empty tables #977 merge. It is structural, not textual: Feat/skip empty tables #977 made six accelerator
AIRs optional and moved them after HALT, so the fixed prefix is no longer a
constant. Six sites break loudly; prover/src/streaming.rs's
NUM_FIXED_AIRS = 10, feeding AirOrder::first_chunked(), auto-merges clean
and is silently wrong on any program without ECSM and HINT rows — which is
every fixture here. That is a design decision plus a re-measurement, not a
review fix.
The four-way copy of the fixed-table order (challenge_phase.rs and three
sites in logup_phase.rs), where array position is the transcript-fork
index and only the length is compiler-checked. Worth collapsing to one shared
accessor — but the Feat/skip empty tables #977 resolution has to touch all four anyway, so doing it
here would only conflict.
Folding BITWISE's lookup list per segment, the cheap half of the residency
gap (a histogram is commutative, so no root moves). It is a perf change and
belongs with a measurement on the boxes.

`verify_batched`'s fold seed indexes both out-of-domain blocks at the `width`/`height` the proof advertises, but `ood_blocks_well_formed` — the guard that pins those dimensions to the AIR and calls `dimensions_consistent()` — did not run until 92 lines later. A proof whose advertised dimensions disagree with its data length therefore panicked in `Table::get_row`'s unchecked slice rather than being rejected. That is the exact gap the guard's own doc comment says it exists to close, and the ordinary verifier keeps the ordering by running it inside the round-1 loop. Hoist the three shape checks into the pre-pass that already validates each table's domain, before any of them is read. The division by `trace_length` is safe there: the same loop rejects zero first. No transcript byte moves — the checks touch no transcript. `prover::batched_verifier::replay` had the same pre-guard read through `Table::columns`; it is test-only, but a patch that fixed only the STARK half would leave a reader thinking the family was covered. Direction is robustness, not soundness: nothing wrong is accepted, the verifier aborts instead of returning false. It is unreachable from bytes today because `BatchedProof` has no derives — which is also why it is the cheapest moment to pay for it, since serializing that format is the point. Also drop `Replay::iotas`, documented as the per-group query indices and always empty, and say plainly that `replay` is a test oracle: it takes the prover's word on the precomputed root and never checks `fold_order` is a permutation, both of which `verify` does. `a_tampered_batched_proof_is_rejected` grows five arms: a group's FRI layer root (the one commitment batching relocated from per-table to per-group), a main root, a composition root, an out-of-domain value, and a block whose advertised width lies. The last one panics at `table.rs:362` without this change and is rejected with it.

Each of these inserted a new item between an existing doc comment and the item it documented, with no blank line, so rustdoc merged the two blocks and the original item lost its docs: prover.rs table_parallelism -> MainRoots prover.rs plain -> known_roots verifier.rs replay_rounds_* -> replay_rounds_2_and_3 decode.rs update_multiplicities -> add_multiplicities trace_builder.rs cpu32_chip_op -> WalkLeftover trace_builder.rs build_initial_image-> runtime_page_ranges trace_builder.rs touched_memory_cells -> op_count trace_builder.rs collect_epoch -> walk_and_emit_chunks Three of the adopted sentences were actively wrong about their new owner: `known_roots` was labelled "for a plain (non-preprocessed) table" when it takes `precomputed: Option<Commitment>` and serves both; `add_multiplicities` was described in terms of a `lookups` parameter it does not have; and `WalkLeftover`'s public rustdoc opened by describing an ALU dispatch helper. `replay_rounds_2_and_3` is renamed `replay_rounds_2_to_4`: its body still carries an explicit `Round 4` section sampling gamma and the DEEP coefficients, so the orphaned sentence ("rounds 2, 3 and 4") was the accurate one and the new name was not. `bitwise_histogram` carried two stacked doc blocks, the first saying LT, MUL, DVRM, SHIFT, the accelerators and PAGE "are not here yet" and the second, directly below, saying the histogram is complete. The first is left over from an earlier state; `finalize` folds all of them in.

Two claims about residency were wrong in the same way. `pass.rs`'s header said what the walk holds is one table plus the residents "no matter how long the run is", and the design doc listed LT among the tables handed over "as soon as a chunk fills". LT is not: it, MUL, DVRM and SHIFT are deliberately absent from `CHUNKED_KINDS` because later derivations keep appending to them, so their chunk boundaries are not knowable until the run ends — `walk_and_emit_chunks`'s own doc comment says so two paragraphs below the sentence that contradicted it. Their op lists, the `retired_*` rows a closing chunk converts its ops into, and the walk's BITWISE lookups are all held whole, so that term is O(cycles). It is a small term — compact routed intermediates against trace rows, a low single-digit percentage of the measured peak — and closing it would move LT's chunk boundaries and cost the byte-identical-roots property that makes the per-table variant a drop-in. So this changes no code: it makes the documents say what the code does, and lists the gap in §10 with the observation that BITWISE's half is the cheap one, since a histogram is commutative and could be folded per segment without moving any root. Also in the design doc: - the `A1_TABLE_PARALLELISM` row quoted a sweep ("flat between 12 and 24; 24 costs 6 GB") that does not match the one recorded on `pass::table_parallelism` (no k=12 or k=24 rows; the step is 16 -> 32 for 5.0 GB); - `A1_INFLIGHT` and `LAMBDA_STREAM_LDE` were missing from a table that claims to list every knob, and the second changes this approach's own memory profile; - `--features hash-metrics` is from #987, which is not on this branch, so the verify-hash column cannot be reproduced here — say so rather than give a build command that fails; - "the spec's Open optimization ... was not kept" described code that ships: what was dropped is holding whole Merkle trees between passes, while leaf-dropping is `drop_leaves`/`retire_leaves` behind `LAMBDA_STREAM_LDE`; - §6's header omitted the blowup and the knob settings the numbers were taken at. And five comments said the ethrex block has 227 tables where the doc says 245. Rather than guess which run is stale, they now say "once per table" and the like: none of them needed the number.

Three things, all outside the prove-and-retire path. `keep_large_buffers_warm()` ran as the first statement of `main()`, so every subcommand — `prove`, `verify`, `execute`, `--help` — allocated 16 MiB, disabled dirty decay on the oversize arena for the life of the process, and left a 10-second purge thread behind. Disabling decay retains RSS that `auto_storage::available_ram_bytes()` does not model, and it is the sort of change that quietly moves every memory number taken with this binary. Call it from the prove-and-retire path, which is the one that allocates and drops trace-sized buffers in a loop. Both of its mallctl failure paths returned silently, and `env_logger::init()` ran on the next line, so nothing could have been logged even if it had tried. A run where the knob did not land was indistinguishable from one where it did. They now warn. The doc comment also records why `opt.narenas` is the right index — jemalloc 5 reserves the slot after the automatic arenas for the oversize arena (`arena_init_huge`), whose threshold defaults to the same 8 MiB the comment names — since a count used as an index invites a second look. `tikv-jemalloc-ctl` had become a hard dependency carrying `features = ["stats"]`, and `jemalloc-stats` an empty feature. That propagates to `tikv-jemalloc-sys/stats` and so to `--enable-stats`, which puts counters on the malloc fast path of every CLI build, including ones measuring baselines. `keep_large_buffers_warm` needs only `raw`/`mallctl`, so the dependency stays and `stats` goes back behind `jemalloc-stats`, which is what the heap tracker is gated on anyway. Finally, `--output` with any stage but `logup` walked the whole execution, returned no proof, wrote no file and exited 0 — and with `--through batched` it also forced a verification the user had not asked for, because `--output` is OR'd into the `verify` argument. It now fails before the walk with a message naming the stage.

`retire_lde_proof_is_byte_identical` compared a proof against itself under `cuda`: there `retire_leaves` returns `None` unconditionally and `retire_main_lde` is compiled out, so both arms take the resident path. That configuration is not hypothetical — `make test-prover-cuda` runs this suite on the merge queue. It is now `#[cfg(not(feature = "cuda"))]`, and each arm asserts `streaming_retire_lde()` actually returned what it set, so the test fails rather than passes if the flag ever stops taking effect. Its `ENV_LOCK` was a function-local `static` that nothing else could name, and libtest calls each `#[test]` once, so it could never be contended — it guarded nothing, and the SAFETY comment above the `set_var` ("single-threaded section guarded by ENV_LOCK") was false on both clauses. Replaced with what is actually true: this is the only writer in the binary, every reader goes through `std::env`, which serialises readers against writers on its own lock, so the exposure is other tests observing the flag under a plain `cargo test` — their coverage, not memory safety. `cargo nextest`, which CI runs, forks per test. The note names the real fix (its own integration binary, as `prover/tests/gpu_force_downgrade.rs` already does) without doing it here. `checkpoint_tests`' `assert!(full.len() > 100_000)` followed an `assert_eq!(full.len(), N_ADDI + 1)` with `N_ADDI = 100_005` — a tautology. The property it was reaching for is already checked by the `logs.len() < full.len()` assertion further down. `chunk_shape_matches_the_built_chunk` gave ops to LT only, so for the other thirteen kinds both sides collapsed to the 4-row padding floor and only the column width was pinned. The row half was covered, but by one kind — so a divergence in a single generator's padding would be missed. It now also populates MUL (dedup, like LT) and SHIFT (plain, 20 ops over a limit of 8, so its chunks are 8/8/4 and sit above the floor), asserts each fixture exercises what it is there for, and counts populated chunks so the loop cannot silently go back to comparing constants. `prover/src/tests/mod.rs` declared `batched_fri_tests` and `challenge_phase_tests` without the `#[cfg(test)]` every other entry carries; the parent `mod tests` is ungated, so those two were the only ones compiled into a non-test build of the library.

`cargo fmt --all`, plus a `clone()` on a `Copy` field that the new out-of-domain tamper arm introduced.

`keep_large_buffers_warm`'s warnings are inside `#[cfg(target_os = "linux")]`, so a macOS build never compiles them and my local lint runs said nothing. CI, on Linux, did: `use of unresolved module or unlinked crate log`. `log` was reaching `bin/cli` only as a transitive dependency of `env_logger`, which is not a dependency you may name. Declared, with a note on the file that its only user is Linux-gated.

`make compile-recursion-elfs` compiles `lambda-vm-prover` for the RISC-V guest, where `parallel` is off and there is no rayon. The three new phase modules `use rayon::prelude::*` unconditionally and call `into_par_iter`/`par_iter`, so the recursion guest stopped building: 27 errors, 8 unresolved-`rayon` and 9 missing-method, plus three `E0505`s in `trace_builder`. This is on #994's branch as it stands, not introduced by this PR — the same `cargo check -p lambda-vm-prover --no-default-features` fails identically at `f800e4b0`. It went unnoticed because no CI run has ever touched that branch; this PR is the first, which is how it surfaced. The four `make lint` arms do not catch it either: the workspace-level `--no-default-features` arm still resolves `parallel` through another member's feature unification. Gated with the idiom already used in `trace_builder.rs` — a `#[cfg]` pair around the iterator source, serial arm `into_iter`/`iter`. Where the closure was long enough that duplicating it would be worse than the problem, it is hoisted to a named binding first and both arms map over that, so the body appears once. No behaviour change on any path that runs today: the serial arms exist to compile for the guest, which links the crate for its verifier and never executes these phases. The `E0505`s were the serial arm of the BITWISE collector loop iterating `&collectors` where the parallel arm moves it into `units`, so the closures' borrows of the op lists outlived the point where `CollectedOps` moves those lists. Consumed by value, matching the parallel arm. Verified: `make compile-recursion-elfs` succeeds, all four `make lint` arms and `cargo fmt --check` pass, and the prove-and-retire tests are unchanged at 13/13.

Brings in origin/perf/streaming-retire-lde (#995): the review corrections over the prove-and-retire work, not new functionality. The batched verifier now validates the declared block dimensions against the AIR before reading the out-of-domain blocks, so a proof with dishonest dimensions is rejected instead of panicking the verifier. tikv-jemalloc-ctl moves behind a feature so its stats counters stay out of the malloc fast path of every CLI binary, and the warm-buffer preallocation runs only in the subcommand that needs it; both were skewing the baselines we measure against. The CLI now errors on --output for stages other than logup instead of walking the whole run and exiting 0 without writing anything. Four tests that could not fail are fixed, including one that compared a proof against itself under cuda. Three resolutions. In prover/src/tests/mod.rs the incoming #[cfg(test)] gating wins: it keeps those test modules out of non-test builds of the library, which is the problem it was written for, while the parallel gate it replaces addressed something else and is now obsolete. In logup_phase.rs our move of BatchedProof to batched_proof.rs wins, since the type has to be reachable when the parallel feature is off; the definitions are otherwise identical field by field, and logup_phase re-exports it so existing paths keep working. In tables/trace_builder.rs git merged both sides cleanly and produced code that does not compile: both branches fixed the same borrow of the collector list, one by consuming it in the loop and one by dropping it afterwards, leaving a use of a moved value in builds without parallel. The drop is removed and the by-value loop stays.

MauroToscano added 8 commits September 18, 2026 14:41

Satisfy the lint gate

e05ca72

`cargo fmt --all`, plus a `clone()` on a `Copy` field that the new out-of-domain tamper arm introduced.

MauroToscano merged commit 0d5abe2 into perf/streaming-retire-lde Sep 18, 2026
20 checks passed

MauroToscano deleted the review/994-fixes branch September 18, 2026 23:13

Navigation Menu

Review fixes for prove-and-retire (#994) - #995

Review fixes for prove-and-retire (#994)#995
MauroToscano merged 8 commits into
perf/streaming-retire-ldefrom
review/994-fixes

MauroToscano commented Sep 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

MauroToscano commented Sep 18, 2026

The one that matters

The rest

Verification

Deliberately not addressed

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant