Prove-and-retire prover (Approach 1), per-table and batched - #994
Draft
jotabulacios wants to merge 61 commits into
Draft
jotabulacios wants to merge 61 commits into
jotabulacios wants to merge 61 commits into
Conversation
Round 1's main commit is a phase-wide barrier: the shared LogUp challenges need every table's root absorbed first, so all N tables' main LDEs stay live at once, O(N x main_cols x lde_size) — the largest single term in the prover's peak heap. An instruments run on fib_iterative_1M puts it at 1854 MB of a 4284 MB peak. Under the opt-in LAMBDA_STREAM_LDE=1, drop each table's row-major main LDE right after its commit, keeping only the column count, and rebuild it inside the table's fused chain through the same production row-major coset LDE that built it. Values are identical by construction, so the proof is byte-identical; the trade is one extra LDE expansion per table for dropping the N-wide term to k. Off by default, and inert under cuda where the LDE is device-resident. Measured on fib_iterative_1M, 10 alternating runs per arm: peak heap 4276 -> 3490 MB (-18.4%), prove time 15.95 -> 17.67 s (+10.8%). It composes with what main gained since: continuations (4 epochs, -16.6% heap) and disk-spill (-27.4% heap for +1.3% time), both proving and verifying with the flag on. Port of milestone M1 from the closed PR #647, which implemented the spec's "Approach 1" prove-and-retire prover. That PR's own /bench never measured the mode: the workflow does not set the env var, so what it reported as a +14.1% regression was the flag-off path.
The retire-LDE mode only paid for itself when a human remembered to export an env var, which is not how a memory lever gets used. The spec that described this prover asked for the opposite: retire "once the memory pressure becomes too large". Add LAMBDA_STREAM_LDE=auto, resolved before proving from the same analytical peak-RAM estimate that already picks the storage mode: retire on exactly the inputs that pick Disk, so the two memory levers share one trigger and one safety margin, and a change to that threshold can never silently desynchronize them (a test pins the agreement on both sides of it). Unknown available RAM retires, matching the storage mode's conservative default. An explicit 0 or 1 still wins — that is the operator overriding the estimate. Unset stays off and costs nothing: only `auto` pays for the estimate's log pre-pass, and on a build without `disk-spill`, where the estimate does not exist, `auto` warns instead of proving with the mode off and reading as "auto decided no". Measured on fib_iterative_1M on a 16 GB box: the estimate (6.55 GB) clears the threshold, so auto turns on both levers and peak heap lands at 2084 MB against 4276 MB resident.
LT, MUL, DVRM, BRANCH, EQ and BYTEWISE deduplicate their rows through a HashMap and emitted `op_map.into_iter()` order, which std randomizes per map instance. Two builds of the same logs therefore produced the same rows in a different order. That is harmless while a trace is built once, and fatal for rebuilding a retired one: the rebuild has to hash to the root the first build committed. Derive Ord on each operation and sort the dedup'd ops by that key. NOTE: this changes the proof OUTPUT — row order is now sorted where it used to be HashMap order. Still a valid proof, now a reproducible one. `trace_build_is_deterministic_across_builds` compares two builds of the same logs across every chunked table; it fails if any of the sorts is removed.
Phase 5 built all 14 chunked tables from closures over local op lists, so a table could only ever be built at that one point in the function: the lists died with the call. Move the lists into a `RoutedOps` intermediate at the phase 4/5 seam, once all the cross-table coupling is folded in, and turn the per-table fills into `RoutedOps::build_table(TableKind)`. `build_traces` keeps its rayon-scope and sequential dispatch and its output is unchanged — the closures now call `build_table` instead of `chunk_and_generate` directly. The point is what this enables: after routing, each of these tables is a pure function of one op list, and the ops are far smaller than the trace they produce. Holding `RoutedOps` instead of the built traces is what lets a retired trace be rebuilt on demand.
Retiring the LDE left the traces resident, and they are the next term down: 675 MB of a 4284 MB peak on fib_iterative_1M, against the 1854 MB the LDE accounted for. Under the same LAMBDA_STREAM_LDE flag, build the chunked tables as empty placeholders and keep only the routed op lists they came from. `TraceProvider` hands the prover a trace at each of the two points that needs one — the Round 1 main commit, where it dies with the closure, and the table's fused chain, where it carries the aux columns and the LDE rebuild until the table is proved. The pre-pass and the memory estimates ask the provider for shapes instead of reading a trace that does not exist yet. Passing no provider is byte-for-byte the resident path. This rests on `build_chunk(kind, i)` equalling `build_table(kind)[i]`: Round 1 commits a trace built one way and the fused chain rebuilds it the other, so a divergence would hash to a root the verifier rejects. A test pins that equality across a multi-chunk table, and the sorted dedup from the previous commit is what makes both builds repeatable at all. A retired chunk's shape is derived, not built: every generator pads to `count.next_power_of_two().max(4)` over its op count — the number of DISTINCT ops for the six tables that deduplicate — and the width is a per-table constant. So the pre-pass and the memory estimates cost a counting pass rather than a trace generation each. `chunk_shape_matches_the_built_chunk` pins the derivation against real builds for all fourteen kinds, on a fixture where deduplication actually changes the answer. Measured on fib_iterative_1M: peak heap 4240 -> 3255 MB (-23.2%) for +14% prove time, against 3490 MB with the LDE alone. All 108 end-to-end ELF proofs pass with the flag on, and the proof verifies. Port of Approach 1 steps C.1/C.2b from the closed PR #647.
The retire modes were described by design, not measured: "one extra expansion per table", "two trace builds per retired chunk". Both happened to be true, and neither was checkable — which is how a third trace build per chunk sat in the shape lookup until it was reasoned about rather than read off a counter. Add three counters under the instruments feature — main LDE expansions, retired trace builds, and shapes answered without building one — and a RESIDENCY block in the prover report. They print on the resident path too, where the expansions are the per-table floor and the retired counters are zero; that zero is itself the thing worth seeing. On fib_iterative_1M: resident is 28 expansions / 0 / 0, retired is 56 / 32 / 16. The expansions double exactly, as one barrier predicts; the 32 builds over 16 retired chunks are the two the design claims, where deriving the shape instead of building it took them from three.
Approach 1 rests on being able to drop what the prover built and get exactly it back. Whatever is regenerated — a trace, a Merkle leaf, an op list — is a function of the execution, so regeneration ultimately means re-execution, and re-executing from cycle zero every time is not a mechanism, it is a threat. `Executor::snapshot` captures the mutable state (memory, registers, pc) and `from_snapshot` rebuilds an executor sitting exactly there, so the cost of regeneration is bounded by the distance to the previous checkpoint. The instruction cache is rebuilt from the ELF rather than carried; replay is deterministic because the private inputs are already in memory before the first cycle, so nothing nondeterministic enters after the snapshot. `snapshot_resume_produces_identical_logs` builds a program by hand — 100_005 ADDI then a JALR to 0 — runs it straight, then runs one chunk, snapshots, and resumes from the snapshot: the concatenated logs must equal the straight run's. The instruction count is over 100_000 on purpose so the cut lands mid-execution rather than where the chunking makes it easy. Advancing the restored pc by one instruction makes it fail. Nothing in the prover calls this yet: the phases that would (a LogUp pass and an opening pass over an execution proved under a single challenge) are not built. This is the capability they need, with its property pinned. Port of Approach 1 step B from the closed PR #647, which built it and left it unused.
The streaming provider maps an AIR index to the chunk that rebuilds it by walking the same order `VmAirs::air_trace_pairs` emits, and HALT sits between the fixed tables and the chunked groups. But `air_trace_pairs` only pushes it when `include_halt` holds, and the provider assumed it always did. That is true on the path wired today, which proves a single final epoch, and false for the intermediate epochs of a continuation. The failure it would cause is the bad kind: every slot shifts by one and each table is handed its neighbour's trace, which is not a crash but a wrong commitment. Take `include_halt` as an argument, from the caller's `VmAirs`, and pass the `true` this path genuinely has rather than leaving the assumption implicit for whoever wires the continuation path next.
The prover took every log of the run at once and built from the slice. Approach 1's Commit phase cannot start that way: it advances through the execution and retires what it has finished with, so it has to consume the run rather than receive it. `collect_epoch_streaming` drives the executor and folds one chunk of logs at a time into the same op lists, carrying `MemoryState` and `RegisterState` across chunks. It comes out identical because phases 1-3 are segment-local once that state is carried: the LT ops a memory access implies are built from the timestamps the access already holds, not from an ordering over the whole run. Identical except for one thing, which the test caught: a cycle's timestamp is `index * 4 + 4` over the slice it was collected in, so collecting in pieces restarted time at every chunk. `collect_cpu_ops` now takes the index of its first log within the execution, and `collect_streaming_matches_collect_epoch` compares the built traces of both paths table by table. Under the retire flag the prove path drops the run's logs before building, keeping only the public output it still needs to check, and the collector re-executes. Measured, that trade is currently a loss: peak heap 23773 -> 24779 MB at 16M cycles and 45026 -> 47005 MB at 32M, +4% on both, with +2.4% prove time. The logs were never the peak — they were already freed before the phase that peaks — and the executor now lives through the collection holding its memory image, which is the larger object. Kept anyway because it is the shape the Commit phase needs: a prover that advances through an execution can retire what it has finished with, and one handed a finished log cannot. If that phase does not land, this should go back. Also snapshots the heap once the fused chain is done, which is what showed that the ~33 GB between the commits and the reported peak at 32M cycles is transient: 11.2 GB is still held there against a 47.2 GB peak. Read with the fact that TABLE_PARALLELISM=1 barely moves that peak, it says the number is the allocator's high-water mark rather than simultaneous residency. The peak-heap line now also says when the mark was set. `stats.allocated` is live bytes, so the number was always real residency — what it could not say is where it happened, and a peak inside one table's work and a peak spread across the run call for opposite fixes. On the real ethrex block the mark lands at 26% of the run in both the continuation and the monolithic paths, which places it inside one table's work rather than in anything accumulating toward the end.
Approach 1's Commit phase turns on one question: can a table be closed and committed before the tables after it exist? Everything the phase claims — retiring as you go, memory that does not grow with the run — rests on the answer being yes, and on the commitment being the one the ordinary prover would have produced. `walk_and_emit_chunks` walks the execution and hands out each chunked table's chunk the moment it fills, dropping its ops right after, so its buffers never hold more than one chunk per table. `commit_table_root` commits a single table through the same row-major coset LDE and row-pair leaf layout Round 1 uses. Two tests carry the claim: the emitted chunks are byte-identical to the all-at-once build, and a chunk committed mid-walk carries the same root the resident chunk does. The tail is deliberately not emitted, and finding out why is the design result here. End-of-run finalization still appends to these op lists — the terminating ECALL's register writes land in MEMW — so a partial chunk is not final until the execution is over. A first version emitted tails too and the test caught it on MEMW_A. That is the spec's own split: full tables are committed and retired during the walk, and "at the end of the execution, the remaining tables are padded and committed". Only the tables whose ops leave `collect_ops_from_cpu` final are closed early. LT and MUL are not among them, since DVRM later appends range checks to one and a product to the other, and neither are the tables derived from the CPU ops afterwards. Those need their per-op derivations extracted before they can be closed mid-walk, which is the next step rather than a guess to make here.
The Commit phase could close seven of the chunked tables mid-run; the others were derived inside `collect_all_ops`, where the walk could not reach them without a second copy of each filter+map. Two copies of a derivation drift, and a table closed mid-walk has to be the table the finished run would produce. `derive_from_cpu` now produces BRANCH, EQ, BYTEWISE and STORE, and both the all-at-once path and the walk call it. That takes the phase from seven tables to eleven of the fourteen. DVRM, MUL and LT stay out, and the reason is ordering rather than effort. Each takes ops from more than one source — CPU32 appends to DVRM and MUL, DVRM appends to MUL and LT — and the finished run concatenates each source whole, while a walk would interleave them per segment. The op sets would match and the chunk boundaries would not, so the chunks would differ even though every table is internally sorted. Closing those early needs the concatenation order settled first, which is a change to what the prover commits, not a refactor. The tests now cover all eleven, and assert that the fixture actually splits at least three of them: a table with a single chunk compares an empty prefix and proves nothing about itself.
SHIFT was closed mid-walk on the strength of its ops leaving `collect_ops_from_cpu` final. They do not stay final: `cpu32_chip_op` appends a SHIFT op for every word instruction, after the segment that produced it has gone. On a program with `*W` ops the walk would have cut SHIFT's chunks somewhere the finished run does not, and committed tables the prover never builds. The existing test did not catch it because a fibonacci fixture has no word instructions, so the append never happened. Adding a fixture that does is not enough either — catching it by data needs word instructions AND enough SHIFT ops to split a chunk, and a fixture that quietly stops meeting that stops testing it. So the hazard is stated instead: `CPU32_APPENDS_TO` lists the tables `cpu32_chip_op` feeds, sits next to it, and `cpu32_appends_are_excluded_from_early_closing` asserts none of them is closed early. A future edit that feeds another table has one list to update and a test that fails if it does not. The walk covers ten tables rather than eleven. A second case runs it over a word-instruction program, which is worth having even though the invariant is what actually holds the line.
Both were still derived inside `collect_all_ops`, so the Commit-phase walk could not reach them without a second copy of each filter+map — the duplication the shared derivation exists to prevent. They move to `derive_from_cpu`, which now produces the six tables that are a pure per-op function of the CPU ops. This does not make MUL or DVRM closable mid-walk: CPU32 and DVRM both append to them after a segment ends, which is a separate obstacle from where the derivation lives. It makes the walk able to produce them at all, which is what a pass that no longer keeps the CPU ops to the end will need.
The Commit-phase walk buffered a `RoutedOps` while the finished run produced a `CollectedOps`, and the two were the same thing minus six fields: the walk's type had no accumulators, because the walk did not need them yet. It will — what it cannot close has to reach the caller so the run can be finished — and carrying two types that drift apart in six fields is how a table ends up built from the wrong list. `RoutedOps` goes; `CollectedOps` is the one intermediate, and the chunk machinery (`build_chunk`, `chunk_shape`, `num_chunks`, `build_table`) moves onto it. The value the trace build hands the provider leaves the accumulators empty, since rebuilding a chunked table never reads them, and says so where it is built. No behaviour change: same chunks, same traces, same proofs.
Approach 1's first pass, end to end. `commit_phase::run` walks the execution and commits each chunked table the moment it fills, dropping the trace right after, then hands back what it could not close — the partial tails and the tables that are still being fed. That leftover is what the spec's next step pads and commits. The obstacle worth naming is how a table gets committed before the number of chunks is known. Per-chunk AIRs differ only by the name used in reports; the commitment follows from the trace and the domain. So one AIR per kind serves every chunk of that kind, and the pass does not need the table counts it could not have yet. The test is the pass as a whole: every commitment it produced equals the one the ordinary prover gives that chunk, the cycles it walked match the straight run, and the chunks it closed plus the tail it kept are the chunks the resident build produced. That last part is exact for CPU — one op per executed cycle, nothing from finalization — and a bound elsewhere, since finalization appends after the last cycle and can spill a tail into another chunk. A kind listed in `CHUNKED_KINDS` without an AIR here fails the run rather than committing under the wrong one. The walk's end memory and register state is not carried yet. The Challenge phase that would use it does not exist, and a field nobody reads is a field that quietly goes wrong.
The spec's step after Commit is that "at the end of the execution, the remaining tables are padded and commited to". `commit_remaining` is that: the partial tail of every table the walk closed, and every chunk of the four it could not close at all, because CPU32 and DVRM keep feeding them after a segment ends. Finalization runs first, as it does in the ordinary build — HALT appends 33 register MEMW ops at `u64::MAX`, and the MEMW-derived LT ops are collected after them so those accesses get their timestamp checks. That is also what makes the phase possible without the CPU ops the walk already dropped: finalization is driven from the register state alone. Together the two phases now account for the whole chunked side of the proof. The test checks that against a real proof's AIRs, per chunk and in position, over CPU, BRANCH, MEMW and LT — LT among them on purpose, since it is one of the tables the walk never closes, so the tail path is what produces it. Nothing may be committed twice, and a chunk nobody committed fails the test. Still outside: the preprocessed and accumulator tables, built from the ELF and from counts gathered across the whole run rather than from an op list. The walk's end memory state, which the PAGE build needs, is not carried for the same reason the register state is — it is only worth holding once something reads it.
BITWISE counts lookups from tables the Commit phase closes and drops. Its multiplicities are accumulated across the whole run, so a chunk's contribution has to be taken while the chunk still exists — and the phase was dropping chunks without taking it. The table would have come out short and the bus would have stopped balancing at verification, a long way from the chunk that caused it. The walk now folds a chunk's lookups into a running histogram just before draining its ops, and carries the result. `build_bitwise` adds what the tables still held contribute and fills the multiplicity columns. Only three of the ten kinds the walk closes feed BITWISE — MEMW_A, MEMW_R and BRANCH — so that is what is folded; the others have no collector and owe nothing. The sources that are not retired (LT, MUL, DVRM, SHIFT, the accelerators, PAGE) still need adding. BITWISE comes back as a table rather than a commitment: it is preprocessed, so its commitment splits into two trees, and that path is its own step. The test compares the table the phase builds against the same three sources over a finished run, and fails if the fold before draining is removed.
COMMIT, KECCAK with its two round tables, and the three accelerator tables are functions of an op list accumulated across the entire execution. Nothing closes them mid-walk, so the Commit phase's job for them is the opposite of retiring: keep feeding them while it drops everything else. It was discarding those lists instead. The walk accumulates them now and `build_accumulated` writes the seven tables at the end, where KECCAK_RC's multiplicities come from the keccak op count and KECCAK_RND's rows are derived from the same ops. The risk here runs the other way from the chunked tables: a list quietly not accumulated does not fail loudly, it produces an empty table that still looks well-formed. So the test compares all seven against the ordinary build on a fixture that actually uses keccak, and asserts that fixture leaves KECCAK non-empty — otherwise it would pass on a program that exercises none of them. Dropping the keccak accumulation makes it fail.
DECODE takes one lookup per executed cycle at that cycle's pc, and the ordinary build gets them by listing every CPU op's pc. The Commit phase drops those ops as it goes, so it has to count the lookups while they still exist — and listing them would cost one entry per cycle, which is the thing the phase exists to avoid. The walk counts by pc instead: one entry per distinct program counter, bounded by the program rather than by how long it runs. `add_multiplicities` applies a count in one step where `update_multiplicities` applies a list. Padding rows look DECODE up too, at the padding pc, and each CPU chunk's share is known when the chunk closes, so the walk adds it there and `build_decode` only has to account for the tail's own. The test runs with a CPU limit that is deliberately not a power of two. With a power-of-two limit a full chunk pads by zero, the padding term is always correct by accident, and zeroing it leaves the test passing — which is exactly what happened before the limit was changed.
The three that depend on state rather than on an op list. HALT comes from the run's terminating ECALL, which the walk notes in passing since the CPU ops that carry it are dropped. REGISTER then finalizes the PC: the padding rows chain inline-PC tokens at a +4 cadence from HALT's emit, so the final token has to match the last padding write or the memory argument does not balance. PAGE reads the memory image at the last cycle, and owes BITWISE lookups of its own, so BITWISE is written only once those are in. Two ordering hazards came out of building it, and both are now structural rather than remembered. The CPU padding count is frozen by `finalize` while the tail is still whole. HALT's register token and DECODE's padding lookups are both derived from it, and both are built after the tails have been drained into chunks — reading it then counts a tail that no longer exists. It was a silent four-timestamp error in REGISTER before the freeze; now building either table before finalization is a panic with a message rather than a wrong number. An empty tail is not a chunk. `ops.chunks(n)` over a length that divides evenly yields no trailing empty one, so counting its padding invents four rows the run never had. BITWISE also gained the sources it was missing. BYTEWISE, EQ and STORE are retired by the walk, so their lookups are folded as their chunks close, like MEMW_A, MEMW_R and BRANCH; everything never retired — LT, MUL, DVRM, SHIFT, the accelerators, the padding byte checks — is folded at finalization. The test now compares the whole table against the ordinary build, and fails if the fold before draining is removed.
A preprocessed table commits as two trees: its precomputed columns, whose root is a constant of the AIR, and the multiplicities, which depend on the execution. The transcript absorbs both, precomputed first. commit_table_root committed the whole width as one tree, so for BITWISE, DECODE, KECCAK_RC, REGISTER and every PAGE it returned a root the proof never carries. Mirror commit_main_trace's branch instead, and return the pair as MainRoots rather than a bare Commitment so the absorption order travels with the value. The precomputed half is re-derived only to be checked against the AIR's constant, which is the same check the production path makes and the one that catches a table whose precomputed columns were built wrong.
The transcript binds the statement before any root is absorbed, so the Challenge phase cannot sample without the run's public output and its runtime page ranges. Neither was reachable from the walk: the output bytes were folded inline in the resident build, and the page ranges were a method on Traces, which is the one thing the Commit phase does not produce. Read the output off the COMMIT ops, which are an accumulator the walk never closes and so are all still there at the end, and make the page-range encoding a free function over the configs. Traces keeps its method, now delegating.
Committing the chunks and padding what is left were two calls, and the second needed the image, the decode artifacts and the register init that the first had built and dropped. Every caller had to rebuild all three to get from one to the other. Split the walk out of run so both entry points share it, and add run_to_end, which does the walk and the padding over one image and hands back a root per chunk of every chunked table. What it leaves resident is exactly the tables that are not built from an op list — the preprocessed ones and the accumulators — which is the state the Challenge phase starts from.
This is where Approach 1 parts from the continuations in main. There each epoch samples its own challenges, so tables from different epochs sit on different buses and need the local-to-global apparatus to be tied back together. Here every chunk of the run is absorbed into one transcript and answers to one (z, alpha), so there is nothing to tie. The phase commits the tables the walk could not — the preprocessed ones, the accumulators and PAGE — then assembles every root in air_trace_pairs order and absorbs it on top of the bound statement, a preprocessed table's precomputed root ahead of its own. The order is the protocol, so it is pinned against a real proof rather than against this module's idea of it: the test proves the same program the ordinary way and checks every root in position, then compares the challenge with the verifier's own replay, rebuilt from the proof's statement fields. Dropping a precomputed root or swapping two AIRs both fail it.
Peak heap is per process, so the two production paths cannot be compared inside one run. Add a trace-build subcommand that runs either the ordinary build or the Commit phase and reports chunks, time and peak, and give the ordinary build an entry point beside the Commit phase so both arms are driven identically — and so the storage-mode argument stays on the prover's side of the feature gate, which the CLI's does not track. On the ethrex mainnet block, 96 cores: resident 41077 MB in 8.95s against 7629 MB in 37.99s for the Commit phase, which also computes the LDE and the Merkle tree of all 173 chunks that the resident arm never touches. main's complete proof of the same block peaks at 110261 MB.
Approach 1 goes through the execution more than once: to commit the main traces, to build the auxiliary columns against the challenge that produced, and to open the Merkle trees. The three differ only in what they do with a finished table — the walk, the end-of-run finalization and the tables that cannot be retired are the same every time. Pull that out as a Visitor and give the Commit phase's own machinery back to it, so there is one walk rather than a copy per phase. The existing tests are what guards the move: they drove the Commit phase through this code and still do, including the one that checks the walk closes chunks mid-run instead of deferring them to the end. Also collects the AIRs a pass dispatches to. One AIR per kind serves every chunk of that kind — what a table commits to depends on its trace and its domain, not on the name in a report — which is what lets a chunk be dealt with before the number of chunks is known.
The spec's third step is a re-execution, and it has to be: the LogUp columns are a function of the challenge, and the challenge is not known until every main root has been absorbed — by which time the tables that produced them are gone. The ordinary prover avoids the second walk by keeping every trace resident across the Round 1 barrier, which is exactly the residency this approach refuses to pay. So the tables are rebuilt. The build is deterministic, so the trace a chunk gets here is byte-identical to the one the Commit phase committed, and the auxiliary columns are the ones that root answers for. Pinned against a real proof the way the Challenge phase is: every auxiliary root compared in position with the one the ordinary prover committed. Three things have to hold at once for that to land — the rebuild is identical, the challenge is the prover's, and the table is in the slot the proof expects — so all three fail the same assertion. Doubling the challenge fails it at table 0.
Peak heap is per process, so a pipeline that grows a pass at a time has to be runnable a pass at a time. --through picks how far down it to go. On the ethrex mainnet block, 96 cores: 7629 MB in 38.2s through Commit, 10534 MB in 45.6s through Challenge, 15323 MB in 142.1s through LogUp, against 110261 MB in 93.0s for main's complete proof. Seven times less memory for three of the five passes, at 1.53x the time. The peak has moved. Every stage peaks in its last seconds, and what runs there is the commit of the tables that cannot be retired — BITWISE at 2^20 rows, DECODE, REGISTER and the pages — whose auxiliary columns are extension-field and so three base elements wide. The chunks are no longer what costs; the resident set is.
The composition polynomial needs the main trace and the auxiliary one at the same time. The LogUp pass has both in hand at the moment it builds the auxiliary columns, so putting rounds 2 and 3 there saves a whole walk over the execution — and there is no cheaper place to put them, since any later pass would have to rebuild both traces to get back to this point. Each table runs against its own transcript fork: the shared state after the challenge, domain-separated by AIR index. The fork is reproducible without changing the protocol, so what comes out is what the ordinary prover produces, and can be pinned against it. Which is the point of doing this before the FRI changes shape: rounds 1-3 are now a checked foundation rather than something that has to be argued about afterwards. The fork is also left standing where round 4 would pick it up — the two out-of-domain blocks and then the composition parts, in the verifier's order — because batching the FRI means folding these states together. Knowing where a chunk sits in the AIR order is now a question a pass can ask, which it has to be: a walk produces chunks in the order they close, and the fork is separated by index. The first walk already counted the chunks, so the layout is known before the second one starts. The test grows to cover the composition root and both out-of-domain blocks for every table. It caught one thing worth recording: between the auxiliary root and round 2, the fork also takes bus_public_inputs.table_contribution. Leaving it out moves beta and everything below it, and the symptom — a composition root that differs while the main and auxiliary roots match — points nowhere near the transcript. Measured on the ethrex mainnet block: 21570 MB in 242.2s for rounds 1-3 of all 227 tables, against 110261 MB in 93.0s for main's complete proof. Rounds 2-3 cost 6.2 GB and 100s of that.
Rounds 2 and 3 read the trace LDE, never the commitment, and the LogUp pass opens nothing — so the main Merkle tree it built was constructed and dropped without ever being asked a question. Nothing is lost by not having it. The composition polynomial is computed from the very LDE that root would be taken over, so a rebuild that drifted moves the composition root instead; incrementing every element of the main LDE fails the test on exactly that assertion. Worth 8.5s of 242.2s on the ethrex mainnet block, and no memory: the tree was transient either way. I had predicted far more, reading main's "Main commit (Merkle) 104.99s" as wall time when it is summed over tables — a single table's Merkle build already uses every core, so a pass that does one table at a time gets it cheaply.
The pass creates no spans of its own — the prover's live in multi_prove, which it does not use — so asking where its time goes had no answer, and twice I guessed and was wrong: once predicting a redundant Merkle tree was worth ~100s when it was 8.5, once predicting that keeping Round 1 would recover 49s when it recovered 12.6 and cost 37.6 GB of peak. Both mistakes were the same one. main's report prints costs summed over tables, and a single table already uses every core, so a per-table cost that looks huge in the sum is cheap in wall time. Instrumenting the pass itself is the only way to stop making it. What it says, on the ethrex mainnet block (ratios, not absolutes — the instrumented build runs 1.6x slower): Round 1 is 58% of the per-table work, of which the main half is 27% and duplicated with the Commit phase, and the auxiliary half is 18% and cannot be — it depends on a challenge that does not exist yet when the Commit phase runs. Rounds 2 to 4 are the other 42%, and main pays those too. So the earlier budget experiment is explained rather than contradicted: it could only ever address that 27%, and 16-way concurrency already absorbs most of it.
The batched proof format does not need building: #951 has it, with one mixed-height MMCS per round and ONE FRI instance per epoch — which is what the spec asks for, rather than the group-by-exact-height fallback this branch was heading towards. It was deleted from another lane by #973 and #974 and is preserved at archive/batched-format-pre-deletion. So this brings the pieces over rather than reinventing them. What comes across is everything the format needs except the driver: crypto/crypto merkle_tree traits + the field-element backend they need crypto/stark fri/mmcs.rs the mixed-height tree fri/batched.rs height combination, batched commit phase, shared challenge derivation batched/round4.rs the round-4 transcript sequence par.rs par_for_each_mut_indexed, which #974 deleted 24 of their tests come with it and pass, including streaming_builder_serves_the_base_group_without_holding_it — the property this branch needs, since a builder that absorbs each table's LDE and frees it is what lets the batched rounds run without holding all of them. What is deliberately NOT brought is #951's own driver. It takes every table's trace at once, which is the residency this branch exists to remove: its floor is all 227 traces resident, measured at 41077 MB on the ethrex block, and this branch's whole proof fits in 21952 MB. The two remove different things — #951 the simultaneous LDEs, this the simultaneous traces — so the driver is the piece to write rather than to copy, and its header is the specification for it. round4's own five tests are not collected yet; they lean on parts of the format that are not across.
Brought in by 6917f6b and reverted unchanged: it is the next step, not this one. The spec's Approach 1 asks for a batched FRI — "accumulate FRI polys into one batch polynomial" — and that is deep_for_table plus batch_fri, which are already here and already checked against a real proof. Grouping their output by exact height gives 13 FRI instances where there are 227, which is the ~54% of proof size the histogram priced. The mixed-height MMCS is a different thing: it batches the COMMITMENTS, one tree per round instead of one per table, and takes 13 FRI instances down to 1. It is strictly more, and it costs a new proof format, a new verifier and the recursion ELFs behind them. Worth doing, after. Nothing is lost by taking it out: it is in this history, and in #951 and archive/batched-format-pre-deletion. Reverting the revert brings it back. And none of it bears on memory, which is what Approach 1 was for and which is already done — 21952 MB against main's 110261 MB, proof verified.
A batched fold is only binding if its coefficient depends on everything it folds; otherwise a table could be swapped after the coefficient was fixed and the fold would still check out. So alpha comes from the shared transcript as it stood before the per-table forks, plus every table's round-3 data in AIR order: the bus contribution when there is one, the composition root, the two out-of-domain blocks column by column, then the composition parts. That reads public data, not the forks, and the difference is the whole point. The first design absorbed each fork's state, which cannot work: the verifier has no forks, only a proof. Every field here is one the proof carries, so the verifier rebuilds the same seed from the same bytes. The byte order is #647's, which documented it as prover-and-verifier-must-match. The test moves one field of one table at a time — all five, in both tables — and requires alpha to move for each, then swaps the two tables and requires it to move again, since the order is part of what the verifier replays. Dropping any one absorption fails it by name.
The walk produces the chunked tables and the end-of-run step the rest; this takes all of them to their DEEP codeword, groups them by exact domain, and runs one FRI per group. On the ethrex mainnet block that is 227 instances collapsing into 13, and the per-table FRI data is 57.9% of the proof. The codewords are held, not the LDEs they came from — one extension element per row instead of every column, about 6.5 GB against tens — which is what lets the fold wait until every table is done without walking the execution a third time. Grouping is by exact domain and can only be: the fold squares the coset offset each layer, so a short codeword over offset*<w> never lines up with a tall fold over offset^2*<w>. Any AIR serves a group, since domain_and_twiddles keys on the proof options alone and every table in a prove shares them. Two things can go silently wrong here and the test pins both: a table can go missing, and a batch that skips one is not smaller but wrong, so the count is checked against a real proof's; and two domains can land in one group, which the fold cannot express, so every group is checked to be a single domain. It also pins something that looks like a bug and is not: a group commits FRI layers exactly when its codeword is longer than the terminal one, which is the blowup times the final polynomial's degree bound. The short tables — one row blown up to two, and the 256-long ones under a 2^7 bound at blowup 2 — are already terminal and fold zero times.
The Open pass cannot start without them: a member's openings are taken at its group's query indices, and those do not exist until that group's FRI is over and ground. So the batched FRI now carries through to them — layers, final polynomial, grinding nonce, the shared indices and their decommitments — instead of stopping at the layer roots. The sharing is the whole substance of batching on the opening side. One set of indices for a group of tables is what makes their openings a group's worth of work rather than a table's each. The batch-of-one test grows to cover it, and stops exactly where determinism does. Layers and final polynomial must equal the ordinary prover's, and do. The nonce must not be compared: grinding searches in parallel and returns whichever nonce it finds first, so two runs over the same transcript state produce different valid ones — and since the indices are sampled after the nonce is absorbed, they move with it. What can be checked there is that the group sampled as many indices as it decommitted, and as many as the proof carries.
The last of Approach 1's five passes is the one that opens, and it can only run once the batched FRI has fixed a group's query indices. open_for_table is the per-table half: the table is rebuilt — round 1 for the trace commitments, round 2 for the composition ones — its rows are taken at the group's indices, and it dies with the call, which is the trade this approach makes everywhere. For that to be possible a table has to know which group folded it, and after the codewords are sorted by domain they no longer sit in AIR order. So a codeword carries its AIR index, and the batch reports the group of each table. The test checks the mapping both ways: every table points at a group that exists, and the groups' own member counts agree with what the tables claim. A table pointing at the wrong group would open against a FRI that never folded it, which is the kind of thing that verifies fine right up until it does not. What is still missing is the walk that drives this over every table, and the proof shape that falls out of it.
Approach 1's fifth pass, and the last. The query indices do not exist until the batched FRI is over, so nothing here could have been folded into an earlier walk — which is exactly why the spec puts it last. Same shape as the three walks before it: a Visitor over the execution, batched k at a time, with the end-of-run tables served afterwards in AIR order. What is new is that each table is opened at ITS GROUP's indices, looked up through the mapping the batch reported. The test caught its own weakness, which is worth recording. Checking that a table opened as many rows as its group asked for proves less than it appears: the number of queries is a global option, so every group asks the same number and a table handed the wrong group's indices still opens the right count — pointing every table at group 0 does not fail it. What separates the groups is the indices themselves, addressed against different domains, so the test also requires every group's indices to be rows that group actually has. An index from a taller group is not a row a shorter one has.
The pieces existed and nothing joined them: roots and out-of-domain values from the batched pass, rows from the Open pass, one FRI per domain from the fold. BatchedProof is that join. It is additive. StarkProof and multi_verify are untouched and still produce byte-identical proofs; this is a second format beside them, for the path that folds one FRI per domain instead of one per table. Nothing has to be migrated for it to exist. The split is the claim: a table keeps what only it can answer for, and a group carries the FRI its tables share. So the test compares every table against a real per-table proof — main, auxiliary and precomputed roots, the composition root, the parts at z, the out-of-domain evaluations, the trace length — and requires them equal. What is absent per table is exactly the four things that became the group's: the layers, the final polynomial, the queries and the nonce. On the ethrex block those are 448 MB of 775.
The prize was priced before any of this was built — the per-table FRI data was 57.9% of the proof, and collapsing 227 instances into 13 was estimated at ~54% off. This measures it instead: 338 MB against 775, so 56.4% off, which is where the estimate said it would be. The split is 326 MB still per table — roots, out-of-domain values, openings — against 11 MB for all 13 groups. Those 11 MB are what used to be paid 227 times. It costs, against the per-table path, +95s and +8.5 GB: two extra walks to fold and to open, and the 227 DEEP codewords held until alpha is known. Against main it is still 3.6x less memory, at 2.57x the time, with a proof 56% smaller. The first run of this said 349.9s and 39.6 GB because the stage ran the per-table prove AND then the fold, which measures neither. The batched path replaces that pass rather than following it.
A perf profile of the batched path on the ethrex block puts keccak at 17.6%, the hottest thing in it by a wide margin — Merkle hashing, not arithmetic. That matches what the prover's own profile has always said and points at the same place: a tree built for nothing is the most expensive nothing available. The fold walk was building one. It rebuilt every table's main Merkle tree, but the Commit phase computed all 227 of those roots already and hands them over in AIR order, rounds 2 and 3 never read the commitment, and the fold does not open against the tree — the opening walk does. So the roots are passed in and the tree is not built: 103.24s to 96.79s for that walk, at no cost in memory. Correctness is not taken on trust. The assembled proof's main roots are compared against a real per-table proof's, table by table, which is the test that would fail first if a reused root were the wrong one. What the profile leaves on the table is bigger and not chased here: about 18% of the time is rayon and crossbeam plumbing, plus 2.2% of kernel spinlock. Sixteen concurrent tables each parallelising over 96 cores is oversubscription, and the k sweep measures the net effect without separating work from plumbing.
This is the one optimization the spec names for Approach 1's Open phase: "keeping the internal nodes of the merkle tree in memory, obviating the need to recompute it; while still dropping the biggest memory cost (the leaves)". It had been available since the first day of this branch — the leaf-dropping tree was ported with everything else — and nothing used it. The Open pass was rebuilding every table's main and auxiliary trees purely to have paths to open with. Now the fold walk hands its trees over. A perf profile of this path puts keccak at 17.6%, the hottest symbol in it, so hashing a tree once instead of twice is where the time was. It costs the earlier reuse of the Commit phase's roots: a table whose main commitment is roots-only cannot answer an opening, and handing one to the Open pass panics in get_proof_by_pos, which is how this was found. The fold walk builds real trees again, and the saving moves from that walk to the one after it, where both trees are saved rather than one. Also splits the batch seed out of the codeword. The seed is a function of public data alone, so a caller reasoning about it should not have to build a codeword or a tree to do so — SeedData carries exactly what the transcript absorbs.
Applied properly — inner nodes kept, leaves dropped, which is what the spec describes — it costs 9.1 GB and buys 3.8s. Applied the way it first went in, with the leaves still there, it cost 17.4 GB. Either way the peak passes the 41 GB that main needs merely to hold its traces, which is the advantage this branch exists for. Instrumenting the Open pass says why, and it is not what any of us guessed. Summed over the 227 tables: round 1 is 415s, rounds 2-3 are 172s, and the opening itself is 0.27s. The pass is essentially all reconstruction, and keeping trees removes only the Merkle part of round 1 — the LDE behind it is untouched and is the larger half. It also settles the idea of opening only the queried rows instead of rebuilding the LDE: there is nothing there to win. Opening already costs 0.27s of 90. What costs is rebuilding the inputs so that it can happen. So the reconstruction is the approach, not an inefficiency in it. Two experiments have now priced not paying for it — 37.6 GB for 12.6s, and 9.1 GB for 3.8s — and both are worse than paying. The sub-step spans stay. They are what closed this, and they name the next thing to look at: the auxiliary half of round 1 is 392s summed, the most expensive item in the pipeline, and nobody has looked at it yet.
The spec's sentence was read wrong all along. "All FRI polynomials generated during this phase can already be accumulated in a single batch polynomial, by sampling the batching coefficients after commiting to the polynomials they randomize" does not mean one coefficient drawn at the end. It means one per polynomial, drawn after that polynomial's data goes into the seed — which is what lets a codeword be folded and dropped the moment it exists. So the fold walk no longer holds 227 codewords waiting for a single alpha. It holds one accumulator per distinct domain, thirteen of them, and each table is absorbed, weighted, added and dropped. That makes the fold order part of the protocol: a table's coefficient depends on every table folded before it. The walk produces tables in the order they close, not in AIR order, so the proof carries the order it used — 227 indices against 338 MB of proof. Within a batch the order is fixed by AIR index so it is a function of the walk and not of which thread finished first. Measured on this branch only in that the five batched tests still pass, which covers correctness: the batch of one still reproduces the unbatched FRI, the coefficients still move when any table's data or position moves, and the assembled proof still matches a real one table by table. NOT measured for speed, and there is a signal against it: the test suite went from 58s to 190s locally. fold_one does an O(domain) accumulate while holding the lock, so a batch's sixteen tables accumulate in series with the walk stalled behind them. That needs the accumulate moved out of the critical section — the coefficients must be drawn in order, the additions need not be.
The first piece of the batched verifier, and the floor the rest stands on: the transcript replay. It reads a proof it has never seen a prover produce and derives every challenge from it — the statement, then the round 1 roots in AIR order for the shared LogUp challenge, then each table's fold coefficient in the order the proof says it was folded. That order is in the proof because it has to be. A table's coefficient depends on every table folded before it, and the walk produces tables as they close rather than in AIR order, so the sequence is part of what the verifier replays. Pinned against the prover's own values rather than against a second implementation of the same idea, which would only agree with itself. Dropping the precomputed root of a preprocessed table — one line, the kind of thing that looks like a detail — moves the shared challenge and fails it. What this is not: deriving the right challenges does not make a proof valid. It makes the questions right. Whether the answers are is what the pieces after this decide — the openings against the roots, the constraint identity at each z, the bus balance, and the fold against the terminal polynomial. It also changes nothing about proving time, which is worth saying plainly: the batched path costs 232.3s against the per-table path's 143.5s, and buys a proof of 338 MB against 775. This is the toll for collecting that, not a way to lower the other number.
The walk re-executes the program and is serial; proving a batch of tables is not. Batched processed each full batch inline, so the walk stood still while the batch was proved and the workers stood still while the walk built the next one. Measured at k=1, where summed spans equal wall time, the walk is ~22s of a 246s pass — time that was spent with one side idle either way. Now a full batch goes down a bounded channel to a worker thread and the walk keeps going. The bound on live tables moves from k to k per batch in flight, with A1_INFLIGHT choosing how many may wait; the default is a rendezvous, so at most one batch is being proved while one is being built. On the ethrex mainnet block, per-table path, k=16: 148.25s to 129.74s, with the peak unchanged at 21952 MB — not by a byte, because the peak is set by the resident tables at the end of the run and a batch of chunks is small beside them. Lowering k to 8 under the pipeline gives 135.12s, so k stays. That is 12.5% off, against a prediction of about 25%. The rest is not recoverable by slack: A1_INFLIGHT=1 gives 130.56s and costs 0.9 GB, with the peak moving to mid-run as the queued batch becomes it. The walk and the worker already overlap as far as they can, and the worker is the long pole; hiding the walk saves only what was not already hidden behind it. Rendezvous stays the default. The batched path, with its two extra walks, gains the same way: 232.3s to 202.4s, each of the fold and open walks from ~100s to 85s, peak unchanged at 30434 MB. A1_PIPELINE=0 keeps the inline behaviour so the two can be compared in one binary; both pass the same eight phase tests.
A pass is the walk plus what it does to each table, and until now the two could only be told apart by inference: summed spans at k=1 minus the wall time, which is where several wrong guesses this week came from. This adds a stage that runs the walk with a visitor that does nothing, so the floor every pass pays is a number rather than a residual. On the ethrex mainnet block it is 14.28s. That settles two things. Pass 1 is walk-bound: its own work, main LDE plus Merkle, is ~14s serial at k=1 and far less at k=16, so a fully overlapped pass 1 would cost the walk and no more — and it costs 22.68s, which puts ~8.4s of interference between the walk and the worker that the pipeline is not hiding. And the walk itself is 1.6x main's execute-plus-trace-build (8.9s): about 5s of rebuilding tables chunk by chunk, with the six deduplicating tables deduplicated per chunk where main does it once over the logs. Those are the two levers left in the time of this path, each with a ceiling measured rather than estimated — roughly 8s and 5s of 129.7. Neither closes the gap to main's 92.7s, and the spec's Approach 1 says outright that it costs "extra interpolations and Merkle tree evaluations" for its memory. The walk-only helper existed as a test fixture; it is now a public function.
jemalloc serves allocations of 8 MiB and up from a dedicated arena and purges each of them the moment it is freed, whatever the decay says, unless that arena's decay is disabled (extent_may_force_decay, extent.c:941). Every trace, LDE and composition buffer of the prover is that size, and the streaming prover allocates and drops one after another, so each chunk refaulted and re-zeroed the same pages. On the ethrex block the walk profile had the kernel's clear_page_erms as its top symbol at 12.9%. Disable the huge arena's decay at startup and purge it from a thread every 10 s instead. Hot buffers are reused across threads; cold ones still go back to the OS within the same window jemalloc would have used. Ethrex on 96 cores: per-table streaming 131.2 -> 117.4 s (-10.5%), batched 202.4 -> 181.5 s (-10.3%), RSS +2.8 GB (peak heap unchanged); main's prove gains ~2% since it barely churns. A long decay, a background thread, or oversize_threshold:0 do not reach this: the first two leave the eager purge active, the last scatters the buffers over 384 per-thread arenas. Linux only: elsewhere jemalloc is built without background threads and the decay mallctl for the huge arena traps. MALLOC_CONF in the environment still overrides the defaults.
The Challenge pass built every AIR to assemble the round-1 roots in AIR order, and the LogUp, fold and open passes each built them again from the same inputs. VmAirs::new is not free: it computes the preprocessed commitments, DECODE from the ELF and one per ELF data page among them, which is most of what the Challenge pass costs. Keep the AIRs in the Challenge and hand them to the later passes, as the ordinary prover builds them once.
The Challenge pass did two things after the walk that did not have to cost what they did. It computed the preprocessed commitments that depend on the ELF alone, DECODE and one per ELF data page; those now run on a thread started with the walk, which leaves most cores idle, and reach VmAirs::new through the parameters continuations already use for the same purpose. And it committed the resident tables one at a time, BITWISE, DECODE, the accumulators, REGISTER, HALT, then 43 PAGE tables, each too small to fill the machine on its own; they are committed in parallel now, in the same order. Ethrex on 96 cores: pass 2 7.3 -> 4.6 s, per-table streaming 116.4 -> 113.9 s, batched 179.8 -> 176.7 s. What is left of pass 2 is KECCAK_RND's commit (3.75 s), which needs the whole walk.
The streaming proof of the ethrex block did not verify: the LogUp bus did not balance, while every table passed its own rounds. Tables built at the end were missing rows the walk owed them from work it had already retired, and derivations the ordinary build does after its CPU pass. LT takes a row for every MEMW timestamp check, and finalize derived those from the tail alone; the MEMW and MEMW_A chunks retired during the walk never handed theirs over, so ethrex got 3 LT chunks where the ordinary build has 21. The walk now derives them as the chunk closes and finalize appends them in the ordinary build's order, general MEMW then aligned, so the tables come out byte for byte the same. BITWISE never counted the lookups CPU32 sends: the ordinary build sums collect_cpu32_bitwise over every word instruction outside the CPU collector, and the walk's fold had no arm for the kind. fib.asm has no word instructions, which is why the existing test could not see it; every Rust program has them in its runtime. MUL and DVRM were built empty: derive_from_cpu returns their ops with the branch, eq, bytewise and store ops, and the walk kept only those four. keccak showed it; programs without multiplies could not. And the ordinary build derives more after the CPU pass: CPU32 rows dispatch to SHIFT, MUL and DVRM (cpu32_chip_op), and every DVRM op owes LT a |r| < |d| row and MUL its d * q rows. The walk did none of it. Those run now for the retired CPU32 chunks as they close and for the tail in finalize, appended in the ordinary build's order so the tables match it byte for byte. HINT appends three LT range checks per call, selector and both address low limbs, after every other LT row; the walk stopped at the MEMW ones. On the ethrex block that was the last LT chunk, 261 rows short. Two tests cover the pattern from now on: a cell-by-cell diff of the walk's BITWISE table against the ordinary build's, and a full prove-and-verify with small chunks of every kind on a Rust program, which is what the block does at scale. trace-build gains --verify, which assembles the per-table proof and runs the ordinary verifier on it, and --output to keep the proof; cmp_proofs diffs two proofs table by table.
The Open pass rebuilt every table in full to serve its openings: round 1 for the trace commitments, round 2 for the composition commitment and round 3 for the out-of-domain values. The openings need the composition parts over the LDE domain and their tree, not the constraint evaluation that produces them, and round 3 not at all. With A1_KEEP_COMPOSITION set the fold pass keeps each table's composition parts, which it had already computed and was dropping, and the Open pass rebuilds round 1, commits the kept parts again and opens. Ethrex on 96 cores: pass 5 80.9 -> 57.0 s, the batched proof 194.9 -> 171.0 s, for 8.6 GB more of peak heap (30.4 -> 39.1 GB). Off by default: it is the memory-for-time trade the approach otherwise avoids, priced here at 2.8 s per GB.
Once the walk is over, the tables it could not retire — BITWISE, DECODE, the accumulators, REGISTER, HALT and one PAGE per page — were proved, folded and opened one at a time, each with only its own parallelism, most of them far too small to fill the machine. The three passes now build them as one parallel batch; the fold keeps its sequential order, which the proof records, and only the codewords are computed together.
The batched proof had a transcript replay and nothing behind it. This is the rest: every table's rounds after round 1, its openings at its group's query indices and its DEEP evaluations there, the fold of those evaluations with the replayed coefficients, and one FRI per height group verified from that first layer down to the final polynomial; on the VM side, the statement, the AIRs rebuilt from the layout the proof now carries, the preprocessed roots against the AIRs' constants and the LogUp bus balance against the public output. The per-table steps are the ordinary verifier's, run on a view of each table's data with the FRI left empty, so the replay of rounds 2 and 3 is split out of replay_rounds_after_round_1 and shared. The group FRI runs the ordinary query checks on a view carrying the group's layers, fed the accumulated DEEP values instead of a single table's. Two tests: the proof verifies, and each part the verifier reads — an out-of-domain value, an opening, the fold order, a final polynomial coefficient, a query index, the public output, the layout — is caught when changed on its own while the untouched proof still passes. trace-build --through batched --verify runs it on real workloads.
jotabulacios
changed the title
The design document for Approach 1, beside the continuations one: what each pass does and keeps, the per-table and batched variants and when each is the right one, every knob, how to run and verify both, the numbers on the ethrex block against the monolithic prover and continuations, where it departs from the spec, the code map, and the rule every change to the walk has to respect — what a retired chunk owes the shared tables is derived when it closes.
--streaming selected prove-and-retire, but "streaming" is the spec's name for both memory-bounding approaches, continuations included, and the comparison against continuations is the one this path is measured by. The flag is --prove-and-retire now, and the summary line says so.
MauroToscano
added a commit
that referenced
this pull request
Sep 18, 2026
`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.
* Reject a malformed out-of-domain block instead of panicking
`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.
* Reattach eight doc comments to the items they describe
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.
* Say what the walk actually holds, and drop a stale table count
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.
* Stop the CLI changing the allocator for every command
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.
* Make four test assertions able to fail
`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.
* Satisfy the lint gate
`cargo fmt --all`, plus a `clone()` on a `Copy` field that the new
out-of-domain tamper arm introduced.
* Declare the `log` dependency the CLI actually uses
`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.
* Build the prover without `parallel` again
`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.
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
2 participants
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.
Prove-and-retire prover (Approach 1), per-table and batched
Motivation
The monolithic prover holds every table of an execution in memory until the
LogUp challenge is sampled: 108 GB of peak heap for a mainnet ethrex block. The
spec's Approach 1 ("prove-and-retire",
spec/streaming.typat624998db)trades passes over the execution for retention: each pass proves what it can
and drops it, keeping only roots, challenges and an accumulated codeword. This
PR implements it end to end, both as a drop-in prover producing the existing
MultiProofand as a batched variant with one FRI per table height forrecursion.
Description
The design, the variants, every knob, what verifies with what and the code map
are in
docs/prove_and_retire_design.md;this section is the summary.
Passes (
prover/src/{pass,commit_phase,challenge_phase,logup_phase}.rs,crypto/stark/src/prover.rs): Commit (walk; per chunk trace → LDE → Merkle →root, dropped), Challenge (roots in AIR order, one
(z, α), AIRs built once,resident tables committed in parallel), LogUp (walk; per table aux, rounds 2-3,
composition, FRI, openings →
StarkProof). The batched variant stops the thirdpass at the DEEP codeword, folds every codeword into its height group with a
coefficient drawn from the shared transcript (Fold), runs one FRI per group, and
walks once more to open every table at its group's indices (Open;
A1_KEEP_COMPOSITION=1keeps the composition parts from the fold pass to skipthe constraint evaluation in the rebuild, memory for time).
Walk correctness: the retiring walk now feeds the shared tables everything
the retired chunks owe them — MEMW/MEMW_A timestamp checks to LT, CPU32
lookups to BITWISE, derived MUL/DVRM ops, CPU32 → SHIFT/MUL/DVRM and DVRM →
LT/MUL derivations, HINT range checks — so the per-table proof of the ethrex
block is byte for byte the monolithic prover's and verifies with the existing
verifier. Two tests pin the pattern (
bitwise_multiplicities_match_the_ordinary_build,a1_verifies_with_many_chunks).Batched verifier (
crypto/stark/src/batched_verifier.rs,prover/src/batched_verifier.rs): every table's rounds after round 1 runthrough the ordinary verifier's steps on a view with the FRI left empty
(
replay_rounds_after_round_1is split so the rounds 2-3 replay is shared);each group's FRI is verified from the fold of the tables' DEEP evaluations down
to the final polynomial; plus statement, AIRs from the declared layout,
preprocessed roots and bus balance. Tests: the proof verifies; seven
single-field tampers are each rejected while the untouched proof still passes.
Time: pipelined batches (the walk never waits for the batch), jemalloc's
eager purge of ≥ 8 MiB extents disabled for the arena that serves them
(
keep_large_buffers_warm, Linux only, −13%), AIRs built once, resident tablescommitted/proved/folded/opened in parallel after the walk (−10%).
CLI:
trace-build --prove-and-retire --through {walk|commit|challenge|logup|batched} [--verify] [--output];examples/cmp_proofs.rsdiffs two proofs table by table.Measured on
ethrex_mainnet_25368371(30.5 M cycles, 96 cores):Verify hashes are keccak finalizes on the verifier side (#987), grinding
excluded — the recursion cost proxy.
Against the spec (
spec/streaming.typ@624998db, Approach 1)The spec also has the Commit phase already accumulating "FRI polynomials"
into one batch polynomial; nothing FRI-able exists before the LogUp
challenge (the aux and the composition need
(z, α)), so batching startsin the re-execution pass instead.
challenges. One
(z, α)for the whole execution.One batch polynomial per table height (13 on ethrex), not one in total:
the fold squares the coset offset per layer, so codewords of different
lengths do not line up without a mixed-height commitment (Feat/multi merkle tree gpu resident #951's direction).
internal nodes, drop the leaves) was measured at +9 GB for −4 s and not
kept; keeping the composition parts instead (
A1_KEEP_COMPOSITION) buys−24 s for +8.6 GB.
is not in the spec; it is what makes the approach a drop-in.
the seam for it.
Merge notes
Main has moved by two commits since the branch base (
99d7567a): #987 (hashcounting; a CLI report for it is ready to apply afterwards) and #977 (skip
empty tables), which conflicts in
trace_builder.rsand changes the tablelayout the streaming walk and the batched verifier assume. To be resolved in
this PR.
Not in this PR: chunking KECCAK_RND (the remaining 4 s of pass 2, a protocol
change), serializing
BatchedProofto disk, and a soundness review of the foldcoefficient sampling and absorption order by someone who did not write it.
How to Test
Expected:
A1 proof verifies: 245 tablesandBatched proof verifies: 245 tables in 13 groups; peak heap ≈ 22 GB and ≈ 31 GB respectively (Peak heap:line).