Repository navigation
WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1014
Draft
MauroToscano wants to merge 1860 commits into
Draft
MauroToscano wants to merge 1860 commits into
MauroToscano wants to merge 1860 commits into
Conversation
|
Benchmark Results for modified programs 🚀
|
|
Benchmark Results for unmodified programs 🚀
|
MauroToscano
force-pushed
the
noepoch/whir
branch
from
October 1, 2026 14:57
e9107c6 to
97ba486
Compare
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
… leaves The builder kept every walked window until finish, so at the run's end all of its op lists were resident, about 300 B per cycle (0.28 GiB per M cycles: 8.6 GiB on block 25368371 and about 100 GiB on a median mainnet block). WindowedTraceBuilder::drop_streamed_ops keeps only the ops not yet in a handed-out chunk for each of the 8 streamed tables (Tail: the windows' lists moved in whole and freed once used up). As a chunk leaves, the builder takes what the table phase would have read from its ops. It counts BITWISE's lookups from LT, SHIFT, STORE, MEMW_A and MEMW_R, plus DECODE's lookups and the last ECALL from CPU. It derives and keeps the phase-3 LT ops of MEMW and MEMW_A, unless stream_memw_lt already put them in the windows' LT lists. The other walk lists are appended window by window instead of being concatenated at finish. The in-walk BITWISE lookups are counted and dropped. finish runs the table phase over the tails (StreamSkip::tails), padding the dropped CPU chunks and placing the kept LT ops where phase 3 would have derived them. The tables are the same. The new tests compare every table with the whole-run build, and with stream_memw_lt every table with the builder that keeps its windows, plus LT's multiplicities. Both go through push and the split, at window lengths 1 to the whole run, and with chunks small enough that all 8 tables drop. The same comparison runs with KECCAK_RND streamed. Another test checks that after each window each table holds less than a chunk of ops. Removing any one accounting step (LT, MEMW_R or DECODE counts, the CPU padding, either LT prefix) fails the first test. Off by default. Cherry-picked from mem/m1 74e1df1 onto #1014, with the streamed finish's build marks kept.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…es are laid out #1014 now lays the streamed chunks out on three workers (0498480), and phase A waits on the groups the rest closes, which close only once the whole rest is laid out. With b1's waves the AIR order's prefix is laid out first, so pack_rest_as_laid_out (the rest's sink, groups identical by test) is now on in production: each wave's tables go to the packer as the wave ends, and a group closes once its own tables are laid out. Laid out all at once, the first table in AIR order was ready only with the last, which is why packing as laid out read +0.21 s before (FAST 422). The real-block tests' BLOCK_WHIR_PACK_REST=0|1 now overrides the production choice instead of replacing it with off. Readouts for the finish's place in phase A: each group's commit start (from@, beside done@), and every rest table's layout end and group in AIR order (BLOCK REST TABLES).
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…s its tables, the block memory log) into nw2/r2ii No conflicts. multilinear_block.rs: the memory log's phase-B marks and the group observer sit side by side at the end of each group (the observer first, then the group's columns are released and the mark taken). block_whir.rs and the W3 harness: the new BlockOptions fields and the memory log's plumbing next to the group observer's.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
… proof to an observer; the block tree's first leaf executes during phase B) into m4b/b2 No conflict. R2-ii's two full BlockOptions literals in lfm/whir_block_tests.rs already carry b2's pack_finished: true, so its hand-over tests run with the finish's tables packed, as production does.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…14fea1 crypto/stark/src/narrow.rs and crypto/stark/src/spill.rs are #1013's files, byte-identical to mem/stark-f1 @ e5214fea1 (i-mem3's F1: the page-backed Bytes, the streaming Digester, the fused writer, over the S1/S2 store). #1013 is their one source of truth: #1014 never edits them, re-imports any change from there, and they merge as one when both PRs reach main. Wiring only: the two modules in lib.rs (dead code allowed there, since some parts serve #1013's prover alone), math's page-bytes feature, and libc unconditional as the store needs it (it was behind disk-spill). #1013's prover glue (TraceTable::spill_main) and its spill tests are not imported; #1014's adapter and tests follow.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
… reserve LAMBDA_VM_BLOCK_SPILL now reads as #1013's (prover/src/block.rs SpillPolicy … spill_decision @ edddc68): auto (and unset) | off | always | <GiB> resident budget. auto spills a committed table once the host's bytes (the larger of VmHWM and the cgroup's memory.current), the reserve and the table would pass the target (LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, else the cgroup's memory.max less 10 GiB, else MemTotal less 10 GiB). Phase A decides per table and never past the writers' queue; groups 0 and 1 count but never spill. The reserve is #1014's own, inferred from the median block (BIG 565): the finish's p5 transient (25.5 GiB) and the tree's leaf programs alive through phase B (16.3 GiB), about 1.25 GiB per total G cells or 1.65 per G cells committed so far, plus 6 GiB for phase B's bump and the read-back window. BlockSpill carries the policy's choice (SpillWanted) and the kept bytes and committed cells it reads. A block that fits spills nothing; the store opens for every policy but off. Tests: the knob and the decision (unit), a budget the block fits in spills nothing and one of zero spills (block).
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…@ 278e6a8 The rule #1014 copies from #1013 read only cgroup v2's memory.max and memory.current. On a v1 host (FAST) the target fell through to MemTotal less 10 GiB, and the host's charge was not read at all. #1013 fixed both in 278e6a8; this re-copies spill_target_bytes, spill_target_from, cgroup_memory and host_bytes_now from that sha, with its two tests (the cgroup files from fake trees, and the target rule), cited as before. The only changes from #1013's text are the citations and the tests' temporary directory, which gets a name of its own so the two copies of the test never share one if they ever run in one process.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…cf253d2) The host measure #1014 copies from #1013 took max(VmHWM, the cgroup's charge), and the charge counts page cache. FAST charged 40.58 GB at 17:28Z with 15.18 GB of it inactive file pages, which would have made auto spill the last groups of a 1x block that fits. This re-copies #1013's measure from its landed head 035aef5 (commit cf253d2): HostReading reads VmHWM, the charge and memory.stat's inactive file pages (v2 inactive_file, v1 total_inactive_file, by their exact key), and the host's bytes are max(VmHWM, charge - inactive_file). CgroupValue lets cgroup_memory read a whole-file number or one memory.stat key. The BLOCK SPILL line ends with the largest reading auto decided on, as #1013's does. With #1013's two tests; the text differs only in citations and the test's temporary directory. The rest of #1013's train (lazy queue budgets, the allocator purge) is not copied: #1014 has no queue budgets.
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
The spill code (stark, multilinear, block_whir) and the streamed top (executor, proof, the W3 tree) touch disjoint code; the one shared file, whir_block_tests.rs, merges without conflict (the spill side adds BlockSpillPolicy::Off to two test fixtures).
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
…114; min proven bits unchanged at 130.393) The default flip of LAMBDA_VM_ZF_WHIR_GRIND_BITS: the port of #1010's 5364aa2 and its pin follow-up 2687e48. PRODUCTION_WHIR_GRIND_BITS is 18; LEGACY_WHIR_GRIND_BITS = 20 keeps the legacy format and is the opt-out (LAMBDA_VM_ZF_WHIR_GRIND_BITS=20). It reaches #1014's WHIR proofs: the block's group chains and prepared openings, verify_block_whir, and the W3 leaves' in-guest verifier. The W3 tree's own STARK LFM proofs do not read it. The binding WHIR phase is unchanged (the unground fold at 27 variables, 130.393 bits); the query phases move 130.926 -> 130.907. Measured behind the knob on c55dec4: ULTRA 019 1x phase B -0.344 s (t -12.9), whole -0.270 s, recursion -0.010 s; BIG 628 median whole -3.42 s, both arms verified. The opt-out reproduces the previous 1x proof byte for byte (top digest 0da6fea9 under fixed hash keys and deterministic grind); the new default's is b9b4826d. The W-leg sizing pins follow the process's grind bits, as 2687e48 did on #1010.
MauroToscano
added a commit
that referenced
this pull request
Oct 6, 2026
…all, commit pairs off the pool) ULTRA 096 (median 25475471, #1014 + cap 256, one binary, 3 + 3 runs plus 2 + 2 single-lever arms) read LEVER EFFECTIVE on every pre-registered row: phase-A end -6.66 s with every run of the pair below every run without it, whole block -6.86 s (154.67 -> 147.81 s), finish 15.8 -> 9.3 s at most, KECCAK_RND's span 12.0 -> 5.4 s at most, the largest phase-A commit 2.93 -> 0.68 s, the card's wait for the rest 6.65 -> 1.77 s, max RSS -0.97 GiB. The wave alone gave -5.92 s whole, the commit pairs alone -0.47 s. At 1x (ULTRA 095) the pair is neutral (whole -0.016 s, t -0.4) and the top digest is unchanged. Both become the defaults; the knobs stay as opt-outs: LAMBDA_VM_KR_PACKED_WAVE=4 builds the chunks four at a time again, and LAMBDA_VM_BLOCK_COMMIT_OFF_POOL=0 puts the commit pairs back on the global pool. The proof bytes are the same either way.
MauroToscano
added a commit
that referenced
this pull request
Oct 6, 2026
…W_WINDOW=1) A #1014 block leaf's LFM_BALU is 70,692 rows a full group, so a 4-group leaf holds 282,768 rows and pads to 2^19. 34,200 of a group's rows are the lean fold's point x0^-1 = prod g^(-2^i b_i): one Select and one Mul a bit through edsl::pow_bits. pow_bits_windowed drops the identity multiply (the first factor read is the accumulator) and reads each of the first two bit pairs through a 4-way Select mux over the constants {1, f0, f1, f0 f1}. A fold then pays three fewer Muls and two more Selects at four or more index bits, two and one below. A full group goes -6,498 LFM_BALU and +4,104 LFM_SELECT, so a 4-group leaf's LFM_BALU drops to 256,776 (under 2^18) while its LFM_SELECT stays under 2^19 at 480,168. The value is the same and so is the Select semantics. The knob is read at program emission like LAMBDA_VM_WHIR_FOLD_CLASSIC and defaults off, so today's programs and ids are unchanged. pow_bits itself is untouched, so the STARK paths keep their programs. The lean fold's row and constant closed forms follow the setting.
MauroToscano
added a commit
that referenced
this pull request
Oct 10, 2026
…E_DOWNLOAD (default off) The port to #1014 of #1013's 6d25865: the same changed lines in device.rs, lde.rs, stark's gpu_lde.rs and the new device test, applied to functions that were identical on both PRs. On a precomputed-tree cache miss the preprocessed commit downloads the full node buffer into a zeroed pageable Vec<u8> and stark copies it once more into Vec<[u8; 32]>. #1014's median recursion pulls about 14.7 GB this way at 2.75 GB/s (I-PROF4 B.5.1). LAMBDA_VM_TREE_DOWNLOAD=staged sends it through a staging pair straight into the node vector and queues the multiplicity tree behind the last chunk; the device peak stays one tree and the nodes are the same bytes.
MauroToscano
added a commit
that referenced
this pull request
Oct 10, 2026
The port to #1014 of #1013's 814a4b6. LAMBDA_VM_TREE_DOWNLOAD unset (or any unknown value) now selects the staged download; `legacy` or `pageable` keeps the old pageable copy as an opt-out. The nodes are the same bytes on both paths. A unit test pins the default. On #1013, legacy vs staged on the median 25475471, one binary per job: recursion -2.94 s (t -15.9, ULTRA 094) and -6.26 s (t -27.6, RYZEN 002), with the base digest and the top program id unchanged (ULTRA 093, 100). #1014's own gate is I-COPIES §10.
a_block_with_keccak256_calls_across_keccak_tables_proves_and_verifies proves a block whose KECCAK tables are cut to a few rows, as keccak_and_ecsm_split_into_chunks_prove_and_verify does in 324 s on a GitHub runner, past the list's 42 s line (21 s on a 9950X box). It still runs in the full reproduction on the GPU machines and locally.
Each leaf emits the constraint leg of the AIRs it verifies, so KECCAK's sponge mode and its round-chip tokens on the mode bits move the first and last leaf programs under both query checks (the leaf count, 5, does not move). The test now measures and prints every pinned value before comparing any, so one run shows all of them when the leaves move.
…y test The box test proves and verifies each load-bearing forgery with its check left out, but the check was left out only on the threads of a rayon pool the test built, and the prover proves each table on plain scoped threads: the prover kept the check while the verifier dropped it, so every forgery read as refused either way. The test now leaves the checks out process-wide through a test-only switch (a guard puts every check back when it drops, also on a panic), and refuses to run unless its runner says it is alone in the process (LAMBDA_VM_KECCAK256_BOX_ALONE=1, --exact --test-threads=1), since it loosens any other KECCAK proof made meanwhile. Outside the tests nothing is ever left out.
The longest bus message of any block AIR is now KECCAK's link between two rows of one Keccak-256 call: the call's timestamp, the block index, the bytes left, the next block's address (two words), the digest address (two words) and the 200-byte state, 207 values and the bus id, 208 against the round chip's 204. The census reads (1475, 208); the block-wide LogUp bound at the group maximum moves 136.79 -> 136.77 bits at 1024 groups and 140.79 -> 140.77 at 64 (log2(209/205) = 0.03 bits).
test_utils keeps one prototype of each AIR a process builds, keyed by name and proof options, and serves clones of it afterwards. In the box test the first KECCAK AIR was built before any check was left out, so the three checks that live in a bus interaction (the digest address on the link, lane 0's memory read, the round-chip tokens on the mode bits) stayed in the AIR the prover and verifier used, while the walk left them out: the KeccakSponge, Memw and Keccak buses then refused those forgeries, not the Memory bus. With every check left out in the traces, every bus, Memory and Commit included, balances on the laptop for all three. Each prove now takes a query count no earlier prove in the process used, so its AIRs are built under the checks it leaves out, and the test asserts that the KECCAK AIRs it proves with carry exactly the interactions those checks make.
ECALL -12 (u64::MAX - 11) recovers the secp256k1 key of a signature in one call: x10 = output (Q.x, Q.y big-endian, then a status doubleword), x11 = r || s (big-endian), x12 = the message hash (big-endian), x13 = the parity of R's y. Status 0 carries the key u1*G + u2*R with u1 = -z/r and u2 = s/r mod N. Status 1 means the call bailed: the key bytes are zero and the caller recovers the key itself. The executor bails exactly when the chips cannot represent the answer: r or s outside [1, N), r not the x of a curve point, u1 = 0, or x(u1*G) = x(u2*R). It errors on a parity above 1, on overlapping signature and hash regions, and on an address range past its low limb. crypto/ecsm gains the reference (k256), the witness the chip will prove (the three products mod N, R's curve relations and parity, both chains and the final addition row), and builders for a chain on a full point and for one addition row. The ECSM witness now builds from a point either root of y, which the second chain needs. Tests: k256-signed signatures recover their key on both parities, every bail class bails in the reference and the witness, a hash at or above N is reduced as the recovery reduces it, the chains have one row per step; the executor's errors.
One row per call (1,543 columns, 981 constraints, degree 3). Under OK (the row computed the key; MU - OK is the bail status it writes) it proves 0 < r, s < N; w = 1/r, u1 = -z*w and u2 = s*w by byte convolutions mod N, u1 and u2 as bits below N and nonzero; R = (r, yR) on the curve with yR < p and yR[0] = 2*H + PAR, PAR the x13 value; the chains A = u1*G and B = u2*R through ECDAS, keyed at TS and TS + 1; the final addition Q = A + B as one ECDAS addition row keyed at TS + 2, with xA, xB < p and xA != xB (an inverse witness over the eight word differences); Q < p. A bail writes a zero key. ECDAS is unchanged. Every ECALL timestamp is a multiple of 4, so the three keys never meet another call's; the second chain's key is what keeps the two chains' Bit messages apart. The table is a counted chip like HINT: TableCounts gains `ecrec` (last field), so the statement tags move to V7, the recursion input to version 7 and the LFM statement replay to 23 counts. The walk, both finishes, the lean pass, VmAirs and the AIR registry carry it. Tests: constraints hold on computed, bailed and padding rows; the other root of R, a wrong inverse or scalar bit, r = N, coordinates at p, xA = xB and a nonzero key on a bail are each refused at the constraint level; the counted BITWISE lookups are the table's sends; the collector keys the ECDAS rows at T, T+1, T+2; prove tests on the new test_ecrec program (two keys and a bail), a forged key and a forged bail refused; block tests where a chain row borrows a neighbouring call's or chain's key, and where the two chains run with swapped scalars (every constraint holds, only the TS + 1 key refuses it). The spec gains an ECREC chapter.
The recovery calls ECREC with the signature and hash in place (big-endian, as the call takes them) and the recovery id's low bit, and returns the key when the status is 0. On a bail it runs the recovery as before (hinted decompression, the ECSM path, k256), which decides valid and invalid exactly as it did: a bail can only cost cycles. Median block: 330 calls, none bailed; ECSM and hint calls 1,320 and 990 -> 0; 130,579,100 -> 126,834,376 instructions; public outputs equal on all 25 blocks.
The Keccak-256 and ECREC changes each added their assembly program to the finish, lean-pass and parallel-walk suites and bumped the list lengths by one from the same base; together each list holds one more.
…CPU stride The bounds s < N, u1 < N, u2 < N, xA < p and xB < p had no test of their own: removing the first three left every ECREC row test green. Each new test builds a row that is consistent except for one out-of-range value (the relation's quotient and carries recomputed for it) and requires that bound's closing carry, and nothing else, to refuse it. Without u1 < N or u2 < N a chain could end in G + G through ECDAS's chord branch, where lambda is free; without s < N a signature Ethereum refuses would recover a key. The second chain and the final addition are keyed at TS + 1 and TS + 2, which is sound only while both offsets stay below the CPU timestamp stride; a compile-time check now ties them to it. A prove test shows the two calls' final additions cannot swap results (refused by the bus alone).
The executor stops the run (no proof) when the signature and hash overlap or an operand crosses a 2^32 address-word boundary, and the guest wrapper passed the caller's pointers unchecked. ecrecover_fits now checks the executor's own conditions first, and the wrapper recovers the key in software when they fail, so the call can never make a block unprovable. The status doubleword starts nonzero, so a call that wrote nothing would read as a bail rather than as the key (0, 0). A stale comment said recid 2 or 3 made decompression fail; the code reads only the low bit, so they behave as 0 and 1.
The argument that ECREC's keys T, T + 1, T + 2 never meet another call's rests on every ECALL timestamp being a multiple of 4: the preprocessed column gives 4(i + 1), and each CPU table's base 4 S_k gives the rest. The spec named only the first half.
ecrec_chains_are_keyed_apart_on_the_bus and ecrec_chains_swapped_between_keys_are_refused prove test_ecrec as blocks whose ECDAS tables are cut to a few rows, as the 324 s keccak_and_ecsm_split_into_chunks_prove_and_verify does (about 100 s for the two and two others on a 9950X box). They still run in the full reproduction on the GPU machines and locally.
The ECREC table's count joined the continuation-epoch statement the StatementReplayV0 program replays (statement V7, 8 bytes more), so its roots[0], roots[7] and program_id moved. The entry is compute_lfm_registry's output at the ECREC cut, pasted unchanged; the program's heights, chunk count, hasher and chip set, and the other five registered programs, came back identical.
The ECREC table joins the AIRs a leaf verifies and the epoch statement gains its count, so the first and last leaf programs move again under both query checks (the leaf count, 5, does not move).
The ECREC table's count joined the continuation-epoch statement (23 counts), eight bytes more, so the statement before the public output is 280 bytes, not 272; 280 is a multiple of four too, so no shift moves.
The census of the longest message and the most fractions a row is meant to cover every AIR a block may carry; it left ECREC out. With it the census is unchanged, (1475, 208): ECREC's messages are shorter than KECCAK's sponge link and it carries fewer interactions than BLAKE3.
The notes under thoughts/shared/, thoughts/blake3/ and others/, and the RESUME.md, RESUME-MMCS.md and HASH-PINNING.md files at the root, are design history, hand-off notes, and the one-off scripts and oracles that produced constants now committed as code. No build, CI job, test or script uses them; they stay reachable in the history of this branch. The one part of thoughts/blake3/ that CI runs is moved, not dropped: the round-parameterised upstream BLAKE3 C (reference-impl/) and the three oracle files it checks against (blake3_ref.py and the two vector files) now live in tooling/blake3-second-source/. The `test-blake3-second-source` target, the formal-verification reference test and the comments that cite these files point at the new location; the CI step calls the make target, so the workflow is unchanged.
bench_vs/lambda/blake3-absorb-bench/ is a hand-run in-guest cycle harness and scripts/gen_blake3_bench.sh generates a BLAKE3-saturated guest for a one-off bench. No make target, CI job, test or script uses either.
Removes tests that measure, time or print rather than guard the prover. No CI list, named test list or benchmark or gate script names any of them; most are #[ignore]d and only ever ran by hand. - Eleven whole probe and bench files: the tenant-width census (per_table_census_tests), the Poseidon1 width-16 chain census (p1w16_census_tests), the Poseidon1 tree-node census (p1_node_census_tests), the round-1 LDE-rebuild probe (c5_probe), the trace-digest printer, the WHIR identity-line printer (whir_byte_gate), the RPX grind bench, counted grind and occupancy sweep, and the math-cuda LDE-engine and upload benches. The few non-ignored tests among them check the censuses' own premises and arithmetic; the emitters they read are pinned by their own tests. - Ignored timers, censuses and production-scale measurement runs in the per-table aggregator, WHIR chain, WHIR global, WHIR one-chain, wrap, multilinear bench, transcript count, argue stage-1, lean program census, BLAKE3 probe, RPO/RPX throughput, RPX chip, program census, Poseidon1 width-16 host/chip/socket/device, decode, decode residency, statement alignment, shape profile, one-LDE-buffer, sumcheck, table transpose, WHIR encode and RPX device-path tests. - Three non-ignored tests that assert nothing and only print a cost (deep_leg_cost, the batched-leg comparison, the bus-leg shape). - The helpers, constants, imports and emptied test modules only those tests used; one import that only hash-metrics code still needs is now gated on that feature. 76 tests in all. Kept on purpose: two probes in files the VM-call change edits (machine_tests, whir_p1_census_tests); the WHIR production tree, the node-emission timing split and the real block's page census, whose removal would force edits to a live test harness or to test-only code in library files; and every probe a current benchmark or gate script still runs.
…over No CLI mode reaches either: prove-block runs the no-epoch block prover and its STARK-proved LFM tree. Removed: - the multilinear continuation (the epoch WHIR base and the cross-epoch global proof) and its recursion programs: whir_global, whir_real_epoch, whir_real_global, block_root, global_parent, global_split, whir_statement, and the epoch-program items of whir_epoch; - the LFM prover over stacked WHIR: whir_proof, whir_leg, whir_wide and lfm_prover_knob (LAMBDA_VM_LFM_PROVER, _LFM_ROOT_PROVER, _LFM_WIDE), the batched-argue measurement knob only the epoch base read, and a device-entry counter only its card test read; - their tests, the continuation transcript-pin bench, and the epoch-tree drivers in per_table_aggregator_tests. The child harvest and the node tests the block tree's tests share stay. whir_epoch keeps the table and group walks the block leaves emit. decode_table_index moves into block_whir with its test. The statement alignment tests run on the monolithic statement now, and the argue stage-1 and batched-argue tests keep the VM's tables. Twenty lines leave .config/ci-slow-tests.txt with their tests.
Nothing selects either: the block recursion proves under Poseidon1 at width 16, the legacy LFM proofs under RPX, and the BLAKE3 arm stays for the BLAKE3 experiments. Removed: - HasherKind::Poseidon and HasherKind::Rpo, their chip layouts, constraint bodies and trace fillers, the Poseidon-original permutation, and the RPO chip's round witness; - the RPO and Poseidon commitment configurations (RpoStarkHash, PoseidonStarkHash and their transcripts) and the matching CommitmentHash and DeviceHash variants with their device arms, all of which aborted or refused; - rpo_chip_tests and poseidon_chip_tests. The surviving HasherKind discriminants and program-identity tags keep their values; the retired ones (1 and 3, tags 2 and 4) are never reused, so no program id moves. The RPO permutation, its constants and its known-answer vectors stay: RPX runs on its rounds and constants, and those vectors are their external anchor. Tests that used RPO or Poseidon as "another hasher" use RPX or BLAKE3 now; two lines leave .config/ci-slow-tests.txt.
LFM_WHIR_PREFETCH=1 built the next table's fraction tree during the current table's per-table argue. It never became the default, and off was the serial path: every table's tree is built at its own turn, which is what the per-table prove now does unconditionally. The deferred tree it used stays, for the batched argue.
…, opt-in The round-0 encode runs the Möbius transform as five passes over the stack, after a memset and a device copy that assemble the stack from its parts; every pass is bound by memory bandwidth. LAMBDA_VM_WHIR_MOBIUS_WIDE=1 takes the first 11 levels over contiguous tiles of 2^11 and the rest in strided tiles of up to 8 levels: three passes. For a stack the card already holds (a resident store or a buffer's slices) the first pass gathers it from its parts, so the copy and the memset are not run. Every element gets the same operations in the same level order, so the coefficients, the codeword and its tree are the same words; by default nothing changes. The card test compares the codeword under both transforms for host, resident and sliced sources at 2^11 to 2^22 (mixed parts at unaligned offsets, gaps, edge words) and for a committed whole stack and its root; an ignored bench times the encode at the production 2^27 shape after checking its codeword.
…stack At a 2^11 stack the ragged part (1,000 words at 2^10 + 2^8 + 17) ran past the end, so today's host encode panicked inside its copy before any codeword was compared. The ragged part now shrinks with the stack, the layout asserts it fits with a named message, the encodes fail by name, and every comparison prints its parity line before it asserts so the box read-out counts the compares that ran. The timed bench now asserts the wide arm took the gather and today's did not.
The round-0 encode's forward transform runs in the column engine's ceil(log_n / 8) passes, four at the production 2^28 codeword, and every pass is bound by memory bandwidth. LAMBDA_VM_WHIR_NTT_WIDE=1 plans the encoding in ceil(log_n / 10) passes instead ([10, 9, 9] at 2^28). The pass kernel now takes up to 12 levels: three register rounds with two shared-memory exchanges, a radix table of 2^(k-1) roots built from the windowed table, and a tile skewed every 16 rows so that a wide pass's first-round half-warps do not share banks. Kernels of 9 and 10 levels are instantiated, forward only. Passes of up to 8 levels keep today's table, tile and operations, the trace LDEs keep today's plan, and by default nothing changes. The codeword's values are today's; only a value's non-canonical representative may differ, which the hashes and the serialisation canonicalise. The host KAT replays every pass of 4..12 levels against the textbook levels, and the wide plan against the naive DFT and against today's plan with edge words planted. The card test compares canonicalised codewords at every size where the plans differ from 2^9 to 2^29, against today's plan and the legacy encoding, and a committed stack's root; an ignored bench times the encode at the production shape under four arms: today, the wide Möbius transform, the wide NTT, both.
…NTT, opt-in A first-pass block of the encoding's spread NTT stages 2^12 positions, which at spacing 2^lb are 2^(12 - lb) consecutive coefficients: exactly the low Möbius levels the wide transform's contiguous pass runs. The Möbius levels act on distinct index bits and commute, so under LAMBDA_VM_WHIR_MOBIUS_FUSED=1 the strided levels run first (the first of them gathering a resident stack from its parts) and the low levels run on the staged coefficients inside the NTT's first pass (F_MOBIUS, one level a phase). That removes one read and one write of the whole stack. Where it does not apply (the legacy encoding, a stack the first pass holds whole) the encoding is the wide transform's or today's, and by default nothing changes. The field values are today's; the subtractions run in another order, so a word's representative may differ, which the hashes and the serialisation canonicalise. The host KAT checks the fused first pass against the whole transform on the host followed by today's spread transform, in both NTT plans and at spacings 1 to 16. The card test compares canonicalised codewords from host, resident and sliced sources under both NTT plans, and a committed stack's root; an ignored bench times the encode at the production shape under five arms.
…cube of 4 Today every fused table hands its last five rounds (a cube of 32) to the host, which walks the rule through the program interpreter once for every index pair and node. For KECCAK_RND that host tail is about 7 ms a table, the card idle meanwhile: one 30 ms stretch a KECCAK_RND group at the median block. A card round costs about one walk whatever the cube. `LAMBDA_VM_ZC_DEVICE_TAIL=1` (default off) keeps the rounds of a program of at least 1000 lowered steps (KECCAK, KECCAK_RND, ECSM, ECDAS, ECREC) on the card down to a cube of 4, so the host runs two rounds instead of five. The messages are the same field values, so the proof is the same bytes. The cross-check keeps today's crossover, since it replays today's rounds. Under the split each batched argue prints its fused tables' card and host rounds by program length (BATCHED ARGUE ZC TAIL), and a test proves the host reference's bytes with the tail forced to a cube of 4 and of 2.
…M_FIRST_PROVE, off) The tree's first prove pays three first-use costs on the tree's critical path: its per-domain prove constants (LDE-size boundary-zerofier inversions and their card copies) in its host preparation after the leaves' artifacts are published, the DEEP's whole LDE coset uploaded from pageable memory inside its card window, and the staging pairs' pinned allocations inside the first build's and first prove's windows. With LFM_WARM_FIRST_PROVE=1 the early leaf's thread makes the staging pairs when it starts and, after its fill, warms the constants and the DEEP cosets for its own tables from an AIR set built from shape-only artifacts (every height, chunk and merge of the real ones, roots zero). Every prove also warms its DEEP cosets before it takes the card. Each warmed value is the one the prove caches for itself, keyed by domain, so no proof byte moves. Off by default; every prove's host preparation is printed in both arms.
…EEP_HOISTED, off) deep_composition_ext3_fused_m* forms gamma*(value - ood) and multiplies by the pole's inverse for every column and pole: two ext3 products a term, and at the recursion's shapes it runs 2.4-4.5x a copy of the bytes it reads. Summing per pole first, sum_j g_jk (t_j - o_jk) = sum_j g_jk t_j - C_k with C_k = sum_j g_jk o_jk (and C_h for the composition parts) computed once on the host, leaves one ext3-by-base product per main column and pole and one multiply by each inverse a row. A micro-bench at the doubled leaf's XALU (2^22 rows at blowup 4) read it 3.06x faster, at the copy's speed. With the knob on, deep_composition_ext3_fused_keep launches deep_composition_ext3_hoisted_m* (row stride 1, the R4 callers'; any other stride keeps the fused kernel). The codeword is the same field element, written canonical; the fused kernel's words are canonical but for a ~2^-32 chance a word, and nothing downstream reads a word's representation (the commitment hashes canonicalise, as the fused kernel's own parity tests rely on). Both arms print the setting and its launches (W3 DEEP HOISTED). Off by default; off, nothing new runs.
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
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.
One WHIR (multilinear) proof per block, with no epochs (the prove-and-retire / VADCOP shape). This is a second prover next to #1010's epoch-based one. #1010 stays the reference and this branch does not touch it. The branch starts from #1010's head
f3d359998; compare againstf3d359998to see only this work.What it is
prover::block_whir::prove_block_whir/verify_block_whir. The whole block is oneMultiProof:(z, α, β)are drawn once.S_post ‖ g: upload again, argue (LogUp-GKR), re-encode with the NTT alone, open. The dropped tree levels are rebuilt from the queried cosets and checked against the kept nodes.WindowedTraceBuilder(noepoch/windowed-builder, also used by STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013). Every full chunk of CPU, MEMW_R, MEMW_A, MEMW, LOAD, LT, SHIFT and STORE is laid out and committed as soon as it exists.⚠ Format changes (all approved by Mauro, 10-02 (§7 on 10-05), but §6, the port of #1013's S0a; for the cryptography team's end review; ledger rows W-0…W-6, W-8, W-9 in CRYPTO-REVIEW.md)
The block is one WHIR proof (
BlockWhirProof, oneMultiProof) over all of the block's tables.z, α, β.S_post ‖ g).Every parameter below is a verifier-side constant. None is read from the proof.
BLOCK_GROUP_POLYSBLOCK_MAX_GROUPSBLOCK_MAX_TABLE_VARSBLOCK_MAX_KECCAK_RNDBLOCK_KECCAK_RND_MAX_VARSBLOCK_MAX_ECDASBLOCK_ECDAS_MAX_VARSBLOCK_MAX_KECCAKBLOCK_KECCAK_MAX_VARSBLOCK_MAX_ECSMBLOCK_ECSM_MAX_VARSArgueFormat::BATCHEDPRODUCTION_WHIR_GRIND_BITSLEAF_PERMS_CAP,BLOCK_FAN_IN1. The group partition is in the statement
What. The streamed prover packs tables into groups in the order their chunks complete. It writes the partition (per group, its tables' indices) into the statement. The transcript absorbs it before any root.
Verifier. The verifier checks:
It then rebuilds every group's stack layout itself.
Security. Proven bits are unchanged.
BLOCK_MAX_TABLE_VARS(change 3), so no partition can make a chain taller than 2^27.Proof bytes vary from run to run. Arrival order depends on thread timing, and the hash-ordered tables' row order (LT, EQ, BYTEWISE, BRANCH, MUL, DVRM) follows a hash state that is random per process. Mauro, 10-02: "the proof not having the same bytes it's fine, they never had the same bytes anyways".
LAMBDA_VM_FIXED_TRACE_HASH=1(fixed hash keys) andLAMBDA_VM_DETERMINISTIC_GRIND=1. Under both, two processes prove the same bytes (FAST 423).2. Prepared openings, one stack per group (approved by Mauro, 10-02: "it's a standard technique, go ahead")
In short. This is #1010's existing prepared DECODE opening, carried into the block format. It is extended to the dense genesis pages and stacked per group.
What. The recursion guest cannot evaluate DECODE's five 2^20 preprocessed columns, nor the dense genesis pages (millions of rows), on its own. So each group's prepared tables (DECODE and the dense genesis pages chosen by
genesis_stack_plan) have their leading preprocessed columns stacked into one commitment.verify_block_whir, andverify_block_tree's plan. The prover's own roots only shortcut the prover's side.z.Negatives, on a guest with two dense genesis pages. Each is refused by the host verifier and by the recursion leaf, and admitted when the openings are skipped (the mutation):
Wrongly committed stacks are refused at the roots block: two pages swapped, a page holding another page's columns, another program's DECODE.
Cost. One stack per group costs +0.14 s of base (FAST 419; one commitment per table cost +0.49 s) and saves 0.57 s of recursion, by taking 90 k permutations out of the leaves.
BlockFormat::prepared = falseturns the openings off, for measurement only.3. ECDAS split; table heights capped
What.
split_ecdas).(round, op).Why. At a median block, one ECDAS table (2^19) argues on a 12 GiB tree. At p90 (2^20) it stacks into five polynomials on a 24 GiB tree.
Gates. FAST 534 and 535: the negatives, 3 mutations caught.
4. Recursion leaf: the leaf cap (G3) and the inverse share (W1)
LEAF_PERMS_CAP. With no fixed leaf count, it adds leaves while the heaviest leaf is over the cap. The block's own partition is unchanged.p · ediv(1, q), which has no satisfying assignment for q = 0 whatever p is. The formerediv(p, q)left the share free at p = q = 0 (≈ 2^-160 under GKR soundness).LFM_WHIR_SHARE_INVERSE=0keeps the former form.5. Batched argue, on by default since d9d0ac5 (
BlockFormat::argue = ArgueFormat::BATCHED; Mauro, 10-02: "batch the constraints")What. Each group's tables are argued together on the group's fork:
Verifier side. The verifier derives the bins from the statement's shapes and its own cap; the variant is never read from the proof. The proof carries one
BatchedArgueper group inBlockWhirProof.argues, andproof.tablesis empty under this format. The recursion leaves verify the same format (lane i-batch2, N-4).Security at the block's measured inputs (D-BATCH §3.2's formulas; re-checked at FAST 424's inputs: |T| ≤ 60 tables a group, ≤ 51 trees a bin, ≤ 2^28.87 input cells, bus messages ≤ 204 elements, N_C ≤ 413, D_max 4, n ≤ 21; L = 300):
Every term is above the WHIR phase, so the proof minimum is unchanged: 128.946 under the campaign accounting (130.393 for the WHIR fold under the calculator of record).
Measured.
The knob.
ArgueFormat::PerTable(one argument per table, the format before) stays measurable, withBLOCK_WHIR_ARGUE=per-tablein the real-block tests. At the per-table format, the MultiProof, the prepared openings and the partition are digest-equal to the head before the batched merge (BIG 393).6. KECCAK and ECSM split; their heights capped (the port of #1013's S0a; landed at 3cfffe2; approved by the lead under Mauro's any-block target, Mauro to confirm)
What.
split_keccak,split_ecsm), as ECDAS is at 2^17.Why. A keccak-heavy block at the gas limit makes about 2^21 permutation calls. One KECCAK table that tall stacks into eight polynomials of 2^27, against a group budget of three. At its cap each table fits one polynomial.
Bytes. Every block measured so far has KECCAK ≤ 2^17 rows and ECSM ≤ 2^11, so it builds the same tables and the same proof (FAST 830: digest 07d1bd43… unchanged on block 25368371).
Gates. FAST 830: KECCAK and ECSM forced into 4 tables each on block 25368371 prove and verify, base and tree; the count and height negatives; mutation C caught.
7. WHIR grinding 20 → 18 bits, queries 112 → 114 (landed at cbfa7d7; approved by Mauro, 10-05)
What.
Each WHIR chain grinds 18 bits instead of 20 before each round's queries, and opens 114 queries instead of 112 to buy the two bits back. At every block height (15 to 27 variables) Q =
num_queries(2, rounds, 128, 18).One site,
multilinear_prove::chain_config_under. Every side of the block reaches it throughBlockFormat::chain_config:verify_block_whir;The statement absorbs Q and the grind bits.
Scope: the block's WHIR proofs only. The recursion tree's own leaf, node and top proofs are STARK proofs (FRI) and keep their own grind.
It ports WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010's grind 18 (landed there at 2687e48). Opt-out:
LAMBDA_VM_ZF_WHIR_GRIND_BITS=20, which reproduces the previous proofs byte for byte.Security. The calculator of record: Johnson bound, η = 1/300, the fold proof of work unground.
Measured behind the knob, on c55dec4, one binary per box:
Bytes. The proof bytes change. Under the fixed trace hash and deterministic grind, the 1× top proof's digest is b9b4826d… at the default and 0da6fea9… under
=20. Both trees are accepted (ULTRA 015, at this head).Known limit. The leaf cap (279,000 permutations) sits above 2^18 LFM_HASH rows, and 18 bits moves every leaf about 1.7 % closer to that doubling.
Gates.
zf_format::; the chain refusals and the legacy-bytes KAT; the pins the flip moved; the host block refusal.One-binary A/B: the block tree vs #1010's epoch tree (FAST 416, noepoch/whir @ 454dad6)
Eight arms E B B E E B B E on the same binary (md5 checked after every arm):
Base, block 25368371 on FAST (each run against #1010's epoch base on the same binary)
Recursion (W3): proved and verified on block 25368371 (FAST 413)
lfm::whir_block::WhirBlockPlan) runs the host verifier's own statement checks, derives every shape from the AIR and every prepared root from the program, and never reads a proof. It prices each group in permutations and partitions the groups over the leaves (heaviest first, onto the least-loaded leaf).block_node, shared byte for byte with STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013). They check the id, the state and the output equal across children, add the shares, and the top asserts zero.verify_block_tree(elf, statement, top)derives the top program and checks the top proof against it. Every preset is pinned inside: the base's options, the block format, the tree's options, the leaf rule and the fan-in.Every proof was verified by the harness off the clock. The base is unchanged by the emission running beside phase B (20.98 s vs 21.18 s in the arms without the change).
Next:
Base levers after the A/B (FAST 417–422, each S/P on one binary)
Memory (D-MEMORY, with i-mem / i-mem2)
drop_streamed_ops)layout_ahead, D-EXEC)Narrow trace storage (M4, lane i-m4)
Prover-only; the proof bytes are the same. The proof digest equals the head's before M4 (07d1bd43…) under the fixed trace hash + deterministic grind (FAST 820).
BlockOptions::narrow, productionNarrowing::CARD).Max RSS, wide → narrow (BIG 560; the traces themselves shrink about 4×, e.g. 24.89 → 6.20 GiB at 1×):
Before M4, #1014 ran out of memory at 3.03× (i-m4); the narrow line puts the 120.7 GiB edge near 5.5–6×.
Phase A uploads the next group beside the commit (3′, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 832; the commits, their order and their bytes are unchanged).
BlockOptions::upload_ahead, on by default;BLOCK_WHIR_UPLOAD_AHEAD=0is the control).Streamed chunks laid out on three threads (E3 on by default, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 838 and 835; the groups, their order and the packing are unchanged).
layout_workers0 → 3 inBlockOptions::production(59e9890). The streamed chunks are laid out on three threads, with at most K + 1 = 3 of them unpacked at a time (layout_ahead, E3), instead of on the builder's one layout thread.BLOCK_WHIR_LAYOUT_WORKERS=0(the inline layout, 01da99f's) is the control.Phase B's kept-top paths re-hashed in parallel (lever 1, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 840 at 733557a — 82f9046 adds only the knob; the paths, their order and the refusal are unchanged).
BLOCK_WHIR_REHASH_SERIAL=1restores the serial re-hash (a measurement knob).BLOCK OPEN SPLIT(withLAMBDA_VM_BASE_SPLIT=1), phase B's openings by host stage and the kept-top gather and re-hash seconds.The tree's leaves execute while their artifacts are built (R2-i, lane i-noepoch-w2)
Prover-only; the proofs are the same (the top proof's digest equal with and without it, 0da6fea9…, under the fixed trace hash + deterministic grind, FAST 841).
prove_tree_pipelined, the way a prover would run it; there is no production tree driver yet). Its level 0 built all three leaves' artifacts first (three serial card holds, 0.24 s at 1×) and only then let the leaves execute and fill their traces (0.46 s until the first was ready) while the card sat idle (nsys timeline, FAST 839). Execution and fill do not read the artifacts; only the prove does.lfm_proveis now cut into its host half (lfm_execute_and_fill) and its card half (LfmFilled::prove, which asserts the artifacts' hasher is the one the traces were filled for), in the same order; the harness builds the artifacts on a thread of their own and each leaf executes and fills beside them, waiting for its artifacts only to prove.W3_EXEC_BESIDE_ARTIFACTS=0is the control (the order before).A second whole-block field. The W3 readout prints, on the clock between the base and the tree, the block report, a second block frame for the LT heights and the group tables: 0.13–0.14 s at 1× that a prover would not spend. "Whole block" keeps its meaning (every number above includes them); from d169edd on,
W3 RECURSIONalso prints "whole excl. harness readouts" beside it (at d169edd, FAST 841 + 842 pooled: whole 18.54 s, whole excl. harness readouts 18.40 s).The rest laid out in waves; KECCAK_RND built as its tables (W, lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43… under the fixed trace hash + deterministic grind: FAST 854 at 0bcc1fc, and FAST 855's W arm on this head's code).
BlockOptions::rest_layout_bytes). The tables, their order and the groups are the same (test).split_keccak_rndthen copied into its 2^16-row tables. At 4.13× that copy was a second peak of the same height. The finish now builds the 2^16-row tables directly (BlockOptions::finish_keccak_rnd_chunks), the same tables as the split's (test), and hands none out during the windows, which would change the groups.BLOCK_WHIR_REST_LAYOUT=allandBLOCK_WHIR_KR_FINISH_CHUNKS=0restore the old behaviour.pack_rest_as_laid_out) was re-measured with the waves: no gain (+0.01 s), so it stays off.LAMBDA_VM_BLOCK_MEMLOG=1(off by default). It prints the host memory term by term every half second and at each phase mark, with the line at jemalloc's active peak and each arena's bytes (those two in the lib tests, which install jemalloc).BLOCK REST TABLES(each rest table's layout end and group) and each group's commit start (from@).The tree's first finished leaf executes during phase B (R2-ii, lane i-noepoch-w2)
Prover-only; the proofs are the same (base digest 07d1bd43… and the top proof's digest equal with and without it, 0da6fea9… — FAST 841's — under the fixed trace hash + deterministic grind: FAST 845, and FAST 847 again on fac261f, the merge with W).
block_prove_on_forks_observed; the old entry point passes a no-op, and the proof is the same with any observer). A leaf's arena is built from its groups' words alone (group_arena_words+leaf_arena;block_leaf_arenais built from them). The W3 harness turns the groups into words as they arrive; the first leaf whose groups are all opened while another group is still to come (leaf 0 = groups 1, 5, 6 at 1×, done after group 6) executes and fills its traces on a thread of its own, about 1.5 s before the base ends, and the tree picks it up. Off the clock its arena is checked against the finished proof's.W3_LEAF_DURING_PHASE_B=0is the control.The finish's tables packed as they are built (b2, lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43… under the fixed trace hash + deterministic grind at both arms: FAST 855 at 0cebe16, and FAST 857 again on 365e3ab, the merge with R2-ii).
BlockOptions::pack_finished). KECCAK_RND is packed in waves of four 2^16-row tables. Phase A takes those tables as narrow columns and uploads them as they are, so the card packs only the groups' other tables. Nothing packed is transposed.BLOCK REST PACKEDcounts the rest: 187 of 191 tables at 4.13×).BLOCK_WHIR_PACK_FINISHED=0restores W.Measurement posture: the card's pool now retains freed memory (baseline shift)
Not a prover change; the proofs are the same (the top proof's digest 0da6fea9… under both postures, fixed trace hash + deterministic grind, FAST 848; 351a773 adds only a test readout).
LAMBDA_VM_MEMPOOL_RELEASE_MB=0. The card's stream-ordered memory pool then hands its freed blocks back to the driver at each synchronize, so a VRAM sampler's total − free reads the live working set. The code default is to retain every freed block (DEFAULT_MEMPOOL_RELEASE_THRESHOLD_BYTES = u64::MAXin math-cuda), and that is what a prover runs.cuStreamSynchronizeandcuMemAllocAsyncwhile the card was idle was ≈ 0.25 s in phase A, 0.42 s in phase B (0.26 s of it in the encode: one 18–33 ms gap per group) and 0.34 s in the tree.W3 DEVICEline).The prover refuses a partition over the group maximum (lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43…, FAST 858). The prover now refuses a block over
BlockFormat::max_groupsas its groups close, with the verifier's ownInvalidTableCountserror, instead of proving a block the verifier refuses. The median block (90 groups against the cap of 64) spent its whole ≈ 190 s base on such a proof (BIG 564). A test covers both prover paths, with a mutation for each check.The tree's nodes built beside it, each level proving as its nodes arrive (A, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same (the top proof's digest 0da6fea9… — FAST 841's — with and without it, under the fixed trace hash + deterministic grind: FAST 889, and FAST 891 again after the permit fix below).
prove_tree_pipelined) built every node program and its artifacts on one thread, level after level, and level 0 joined that thread before any node proved, so level 1 waited for the whole tree's builds. At the median block, 32 s of serial node builds after the leaves' artifacts held level 0 open 10.7 s past its last leaf proof, and the card sat idle 11.4 s before level 1 (BIG 565 / 568's card trace). At 2.66× the wait was 1.5–2.1 s (FAST 888).W3_EMIT_THREADSthreads (default 4, the builder's own: on the global pool a prover's join can steal an emission and leave the card idle, STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013's FAST 454), and the builder's thread builds each one's artifacts as it arrives. Each node proves once its children are proved and its slot is filled. A builder that stops fails every empty slot.W3_NODE_PIPE=0is the control.Published<T>serves as the slot; there is no per-group early emission (W3 builds every leaf's artifacts up front, so a level's programs are emitted together); and there is no host-only thread marking (WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014 has none).build_levels, an emit on the pool and a finish on the builder's thread). A toy tree at the median's shape puts the serial builder's programs in their slots whatever order a pool finishes them in, and finishes every node off the rayon workers (test; finishing on a worker, or publishing in arrival order, fails it). A failed build fails every slot above it without a hang (test).WhirBlockPlan::programsbuilds as rayon jobs.W3_NODE_TIMES=1(off by default). It prints, per program, when it was built, taken and proved; its prove's split (execute, fill, the prove net of the card wait, the wait); and each node level's start against the level below. The stamps are taken either way and cost a handful ofInstantreads.prove_tree_pipelinedis its de-facto driver. With the slots it now has a driver's shape: leaves from phase B, nodes from slots, levels as their nodes and children arrive. Moving it out of the test harness is a landing item for STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013 and WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014 both.Each node proved as soon as its own children are (C, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same (the 1× top proof's digest with and without it, under the fixed trace hash + deterministic grind, both trees accepted: 0da6fea9…, BIG 614 — the digest FAST 841 / 889 / 891 printed).
siblingsworkers proves every program of the tree, leaves and nodes, taking them in topological order (the leaves, then each node level) and publishing each proof into a slot of its own. A node waits only for its own children's slots, so it executes, fills and proves while the rest of the level below still proves.W3_DATAFLOW=0is the control: each node waits for its whole level below (tested never to start early).W3 LEVELwall now runs from the level below's last proof to its own.The held tables spill to disk, by default only when memory is short (lane i-m4b)
Prover-only; the proof bytes are the same: one shape and one proof digest (07d1bd43…) across the base and all four policies, under the fixed trace hash + deterministic grind (BIG 616). The 1× top proof's digest (0da6fea9…) and the tree verify at the landed merge (ULTRA 006).
crypto/stark/src/spill.rs) is imported byte-identical; it digests each slot and writes it with O_DIRECT on a writer thread, off the committer's path. A table moves only when the writer's queue has room at that moment, so the committer never waits.SpillFailed). After a group's opening its packed columns are let go.LAMBDA_VM_BLOCK_SPILL=auto(the default) |off|always|<GiB>(a resident budget).autospills a table when the host's bytes plus a reserve plus the table would pass the target.LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, else min(the cgroup's limit, v2 or v1;MemTotal) − 10 GiB.BLOCK SPILLprints the policy, the slots and bytes, the writer's split, the read-back, and the largest host readingautodecided on.always(BIG 566, single runs): 22.74 GiB spilled, max RSS 52.53 → 40.12 GiB, whole block +1.15 s, drivers waited 0 s.auto(BIG 567): by default nothing spills (target 110.7 GiB). Under a 35 GiB target it spills 21.21 GiB, max RSS 41.04 GiB, +2.91 s.autospilled 26.98 GiB from group 44 of 90, and the tree verified.auto, O =off, S =always, T =autoat a 47.5 GiB target):autorun spilled 0 in both jobs, at 110.7 GiB and under the 47.5 GiB target (FAST's limit, kept as a real test on BIG's 128 GiB; the host read 25.3–26.8 GiB across those runs);alwaysandautoat 0 spilled within noise.autospilled 0 (host at most 27.65 GiB).Phase 4 counts the BITWISE lookups in slices (#1013's c369843, lane i-m4b)
Prover-only; the bytes are the same:
What changes:
LAMBDA_VM_P4_SLICED=0keeps the whole-source collectors. The knob is WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014's only, for the A/B.Measured: the median, BIG 619. One binary on the cap-128 exploration head, N P P N,
autospill on. N runs the whole-source path, P the slices.auto)autospills only once memory is short.The top executes each child's share as that child is proved, while a child is still unproved (B and B′, lane i-noepoch-w2)
Prover-only (the W3 harness and the LFM executor); the proofs are the same. The 1× top digest is 0da6fea9… with the streamed top on and off, under the fixed trace hash + deterministic grind, and both trees are accepted (BIG 617; ULTRA 008 and 009; ULTRA 011 at c55dec4 itself).
executor::StreamedExecutionruns an execution as its arena groups land: each instruction runs in the wave in which the last group it reads lands (each instruction's group set comes from one forward pass), in the level schedule's order, into the slot the schedule gives it. So the witness isexecute's, word for word.finishchecks that every instruction ran once. Dropping the group propagation (ReadBeforeWrite) or re-running instructions across waves (DoubleWrite) fails them.W3_STREAM_TOP, on by default), so only the last child's share and the fill remain after the last child.W3 TOP EXECUTEprints which. A test covers a program ready before the last child (streamed), after it (whole), and a failed child (whole, which then reports the failure). Inverting the predicate fails the test.A node executes from its program; only its prove waits for its artifacts (b′, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same: the 1× top digest is 0da6fea9… with
W3_EXEC_EARLYon and off, under the fixed trace hash + deterministic grind, and both trees are accepted (ULTRA 012; ULTRA 013 at 806c211 itself).node_flow). The traces are filled under the block hasher, which the node artifacts are built for. The top's streaming choice (B′) is taken when the top can execute.W3_EXEC_EARLY=0is the control.LfmProveError::HasherMismatch, naming both) instead of failing a release assert, and the streamed execution's finish returns an error instead of asserting its public words' capacity. Each has a test and a mutation.