WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1014
Draft
MauroToscano wants to merge 1348 commits into
Draft
MauroToscano wants to merge 1348 commits into
MauroToscano wants to merge 1348 commits into
Conversation
The fix was made on fix2/gpu-tables-a23, from A2+A3's 8c925a4, so that A2+A3's re-run measures A2+A3 alone. Here the test takes A4's Knobs helper; its assertions are the same. # Conflicts: # crypto/stark/src/multilinear_table.rs
L1N{j} (arity k) in place of "whir wide j", on its census panel, IDENTITY,
TIMING and host-peak lines and in its prove and harvest labels, so a tree
log's readers file the proof as level 1's node j (zf_summary.py's
L{level}N{j} rule). Labels reach prints and error messages only: no program
or proof byte moves, and a wrap's lines are unchanged.
Under LAMBDA_VM_LFM_WIDE=on the level-0 stage yields one node per fan_in epochs, not one wrap per epoch, and the interior's report covers levels 2..=child_level: the two counts the fixture asserted assumed wraps (job 215's FW arm stopped on the first). The wrap path's asserts are unchanged.
The level-0 lead-in's slots gain a span: slot k waits for epochs 0..(k+1)*span and its builder is handed that prefix; span 1 is today's wrap lead-in, call for call. Under LAMBDA_VM_LFM_WIDE=on the production tree starts the wide lead-in (start_whir_wide_lead_in, span = fan-in) where it started none: helpers harvest each group's epochs as the base proves them and emit the wide node with wide_prologue_emit, the emission the pool shares, so the pool takes a prologue instead of building it. Job 215 measured level 1 opening with 2.7 s of host prologue and the card idle; this moves that work into the base's tail. The wide level prints its start on the prove-split clock so the gap to the first card hold is read from the log. Card-free unit test for the spanning slots.
…A_VM_ARGUE_LEAN_TAIL) A5. On FAST (job 213) the host's work between two device GKR layers is 264 us a layer, and 52 % of it is the tail's arithmetic: the nine rounds the host finishes over a cube of 512 after the device hands the layer back. The generic round extends every factor to t = 2, 3 by multiplication and sums the whole relation at three points. Under the knob (default off) a device layer's tail runs lean. Its weight is eq(point, .) folded on the device's challenges, so at each round it factors as l(t) * w(x), with l(t) = eq(rho_k, t) and w the sum of its two halves. The round polynomial is l(t) * h(t) with h of degree two: - the tail sums h(1) and h(2), extending the factors to t = 2 by addition; - h(0) comes from the claim the round carries, carried through the device's rounds exactly as the verifier does; - h(3) comes from the zero third difference; - w is carried by additions and one scalar; - only the four halves are folded, with the generic fold. That is about 14 extension multiplications a pair where the generic round makes 30. Every sent value, challenge and bound factor is the generic round's field element, so the transcript and the canonical bytes are unchanged. Raw limbs of the round values may differ, and only a device layer takes this path, so no host-only byte gate reaches it. The tail declines, before absorbing anything, when the point does not match or some 1 - rho_k has no inverse. Tests: - host: the lean tail against the generic rounds (values, challenges, transcript state, bound factors) at 2^1..2^11, 0..3 device rounds in, over Goldilocks and its cubic extension. Five mutations (the h(3) difference, the claim chain, w's halves, the scalar, l(1)) each fail it; - host: LAMBDA_VM_ARGUE_XCHECK sums every round the generic way too and refuses a faulted tail; - device (cuda-only): argue_lean_tail proves a 2^15 tree to the same proof with every card layer lean, keeps host trees generic, and shows a wrong lean round refused by GKR's layer check and by the cross-check; - device: the stark tall tables prove the same bytes with the tail lean (alone and with every argue knob), and the faulted tail is refused. Under the base split an `ARGUE TAIL` line counts lean tails per record.
Brings fix2/gpu-tables-a23 up to 34c1760, the sha job 216 measured on FAST: WHIR ABBA EFFECTIVE, whole run B - A -5.20 s (band [-5.5, -3.3] HIT), base 41.65 -> 36.65 s, sum of ARGUE 19.7 -> 14.7 s, 1,364 tables built on the card per B arm, every arm proved, verified and on the record's identities, and the untimed cross-check arm clean. Device checks 7/7, the corrected negative control's mutation step included. The only conflict is gpu.rs's knob helpers: the A1 landing added env_not_off and not_off where A2+A3 added its knob block, and both stay, unchanged. LAMBDA_VM_ARGUE_DEVICE_TABLES is still off by default here; the next commit turns it on. # Conflicts: # crypto/multilinear/src/gpu.rs
LAMBDA_VM_ARGUE_DEVICE_TABLES is now on unless set to 0, which is the opt-out and the old path exactly. Its WHIR A/B on the block (FAST, job 216, at 34c1760) read EFFECTIVE: - the whole run 5.20 s faster (band [-5.5, -3.3]); - base 41.65 -> 36.65 s and the argue 19.7 -> 14.7 s; - 1,364 tables built on the card a run; - every arm proved and verified on the record's identities, and the untimed cross-check arm, which compares every card table with the host's, clean. The proof does not change. The card builds the zerocheck's eq weights and the reduce's shift tables and batched columns as the same field elements the host built, and the sumchecks run over them as before, so the canonical bytes, the transcript and every challenge are the same. The fixture identity test, the cross-check arm and the verified arms showed it. No pin moves. Without a device a weight given as its point is made into the table eq_mle made before, in the same batch order, and the reduce keeps its host path, so a host-only proof is the same to the raw limb. The WHIR byte gate builds without cuda. No STARK path reaches the argue. A unit test pins that the knob reads its variable the default-on way (unset on, 0 off). A mutation restoring the old reading fails it.
…ed A/B Brings fix2/gpu-tables up to 8d2cb35 on top of land/gfs-a23: - A4, a session's end read back in one copy (LAMBDA_VM_ARGUE_LEAN_READS); - the GKR layer timers under LAMBDA_VM_BASE_SPLIT; - A5, a device GKR layer's host tail finished lean (LAMBDA_VM_ARGUE_LEAN_TAIL). Both knobs stay off by default here. The combined A/B measures them together on top of what is landed (A1 and A2+A3 on), and they land together if it is EFFECTIVE. No conflicts.
…vel 1) The recursion's LFM proofs proved by the stacked-WHIR prover: W-LFM proofs and their in-guest W-legs, the preprocessed-count binding, policy B, the wide level-1 node with its base-tail lead-in, and the knobs LAMBDA_VM_LFM_PROVER / LAMBDA_VM_LFM_WHIR_PREP / LAMBDA_VM_LFM_WIDE, still default-off here. W4's ABBA at 4150afa: 56.65 s against 60.70 s. The one conflict, crypto/stark/src/multilinear_table.rs's test module, is the union of both sides' blocks: A1 and A2+A3's tests on the card, then the count-trap and policy-B tests, inserted at the same base line.
On #1010's line a WHIR chain grinds before its queries only, with one spent nonce a round (P2), and a W-LFM proof takes its chain config from the same chain_config. The production-config anchor now asserts GrindBits::query_only(20), and the W-leg's sizing pins drop each round's folding and OOD grinds and their two nonce words (wrap 0, policy B: 38,440 -> 38,374 perms, 384,825 -> 383,715 ops, 73,961 -> 73,937 hints); the previous values are kept in the comments. The F1 exactness tests pass unchanged, and every pin stays within the design's 0.5 % band.
LAMBDA_VM_LFM_PROVER defaults to whir, LAMBDA_VM_LFM_WHIR_PREP to prepared (policy B), and LAMBDA_VM_LFM_WIDE, unset, follows the tree's prover: on under whir, off under stark, whose tree has wraps. The opt-outs are LAMBDA_VM_LFM_PROVER=stark (the per-table STARK recursion as it was), LAMBDA_VM_LFM_WHIR_PREP=both and LAMBDA_VM_LFM_WIDE=off. D-WHIR W4, the ABBA at 4150afa: 56.65 s against 60.70 s for the block's whole run. The §2.4 count-trap tests build under policy A explicitly: only there is a proof without its prepared opening well-formed, and under the new default the prover refuses to leave out a prefix nothing settles.
…ts (S0) A device round's per-thread slot file is the lowered program's live set, and the slot budget divides by it: the widest batch, KECCAK_RND's, holds 2,763 values and caps its early rounds at 8,096 threads. That is exactly the head trace's 253x32 shape, 1.31 s in 14 launches. The census (an ignored printing test) builds each VM table's zerocheck program and the batch its session runs (the constraint rule beside the bus's two), lowers them, and reports steps, slots and the thread ceiling three ways: - today; - with roots, and the bus's interaction terms, folded into their sums as soon as they are computed; - with every factor and constant read emitted again at each use instead of held. At a random point it asserts that every variant is the same polynomial. On the three batches that bind, folding early barely moves the live set (KECCAK_RND 2,763 -> 2,344). Reloading the reads cuts it 6-13x (KECCAK_RND 211, ECSM 269, ECDAS 161) at 50-60 % more steps: the held values are shared column reads and constants, not roots. IrShape::program_lean (the zerocheck folded early) and its host parity test are included; nothing calls it outside the census yet.
…ult off) A big batch holds so many values a thread that its first device rounds run a few thousand threads: KECCAK_RND's 2,763 left 8,096 at the 512 MiB slot budget, 94 ms a launch on the head's trace. The values are the order the batch was written in: every shared read held from its first use to its last, every root and every interaction's side held until the sum at the end. `Program::on_demand` re-emits the same steps in Sethi-Ullman demand order and emits every read again at each use. Each step is the same operation on the same operands, so every value is the same; a sum's terms are added in as they are made. On the four big VM batches the live set drops 2,763 -> 207 (KECCAK_RND), 1,782 -> 48 (ECSM), 1,291 -> 159 (ECDAS), 859 -> 14 (KECCAK), at about 60 % more steps. Under LAMBDA_VM_ARGUE_LEAN_PROGRAM (off by default; off is today's path) a zerocheck whose lowered program holds more than 341 values a thread (under 64 k threads a round) runs the program on demand, with the session's slot file sized for every interpolation node from the first round (`session_spread`). Small batches, the byte gate's EQ fixture among them, keep today's program. Under LAMBDA_VM_ARGUE_XCHECK a shadow session walks today's program over the same factors each round and the prove is refused at the first disagreement: the block's identity gate, since block proof bytes are not reproducible. The base split gains an ARGUE ZEROCHECK line: big sessions, lean and checked counts, and the big batches' early (half >= 2^13) and late device rounds, the other batches' rounds and the host tail, timed. Tests: host parity on every VM batch and the gate's four big batches; device parity round by round on the four (box); the stark identity knob off and on, alone and with every argue knob; a fault that the verifier (BatchMismatch) and the cross-check (DeviceFailed) both refuse.
…the pure-WHIR landing Merges fix2/lean-program @ 965e13d into land/pure-whir @ 6a6e266. S1a read EFFECTIVE on FAST (job 223): the whole run 1.35 s faster, the big batches' early device rounds 1,527 -> 442 ms, the argue 1.43 s faster, every arm proved and verified with equal identities. The merge brings S1a's ancestry from gfs/a45 with it, every knob default off: A4 (LAMBDA_VM_ARGUE_LEAN_READS), A5 (LAMBDA_VM_ARGUE_LEAN_TAIL), the device GKR layer timers under LAMBDA_VM_BASE_SPLIT, and the S0 census test. One conflict, in stark's multilinear_table tests: both sides added tests at the same place (the preprocessed-prefix tests here, the argue-knob tests there). Both are kept.
LAMBDA_VM_ARGUE_LEAN_PROGRAM is now on unless set to 0, which is the opt-out and the old path exactly. Its WHIR A/B on the block (FAST, job 223, at 965e13d) read EFFECTIVE: - the whole run 1.35 s faster (band [-1.6, -0.5]); - the big batches' early device rounds 1,527 -> 442 ms, the argue 1.43 s faster, the other batches' rounds +8 ms, and the late rounds held (no S1b); - every arm proved and verified on the record's identities and census, and the untimed cross-check arm, which walks today's program beside every big session round by round, clean. The proof does not change. The program on demand is the same steps on the same operands in another order, so every round's values are the same field elements, and so are the transcript and every challenge. The stark identity test, the device parity test on the four big VM batches and the cross-check arm showed it. The round sums of a big batch are added over another launch shape, so their raw representatives, and a device proof's rkyv bytes, may differ, as between any two launch shapes. No pin moves. Only a batch whose lowered program holds more than 341 values a thread takes the path, and only on a device: the WHIR byte gate builds without cuda, and its EQ fixture holds 26. The W-LFM pins count the W-leg's permutations, operations and hints, which no argue path changes. No STARK path reaches the argue. A unit test pins that the knob reads its variable the default-on way (unset on, 0 off). A mutation restoring the old reading fails it.
Under pure WHIR the recursion proves its LFM programs with the base's argue, so the lean program's gate reaches their zerocheck batches too. A census of the W-LFM chips (the WHIR recursion chip set at the recursion's hasher, as whir_lfm_airs builds it) finds one big batch: LFM_HASH holds 365 values a thread today, a 61,286-thread ceiling, and 34 on demand, 657,930, at 41 % more steps. LFM_BITDEC holds 233 and stays under the gate. - every_w_lfm_batch_on_demand_is_the_same_program: host parity on every W-LFM batch, and LFM_HASH as the only big one. - the device parity test now finds its batches by the gate, over the VM's and the W-LFM's AIRs, and pins the five. - the_w_lfm_zerocheck_programs_and_their_live_sets: the printing census, ignored.
Both RPX implementations (prover lfm::rpo::Rpo256::mds, used by the block path's RpxStarkHash, and crypto::hash::rpx::mds) built each output lane with a core::array::from_fn closure. The closure's generic from_fn wrapper is placed in a codegen unit of rustc's choosing and is inlined into mds only when that unit happens to be mds's own. When it is not, every lane is an out-of-line call that recomputes (j - i) mod 12 with a 64-bit multiply per term: about a fifth more instructions per permutation. That is the two-speed host verify on the STARK tree. A Linux x86-64 cross build of the prover test crate at 8934b59, ef6d4be and 3fd644e shows mds inlined (2499 B, no calls) only at ef6d4be, the one FAST build, and twelve closure calls at the other two, the SLOW builds. Crypto's mds makes the twelve calls in its current partitioning too. Loops over a precomputed circulant compile the same way in every build. The permutation's values are unchanged: the RPO and RPX known-answer vectors, the two-implementation agreement test and a new test against the circulant definition all pass.
Under `parallel` the grind is `find_any`. It returns any valid nonce, 0 included, and the nonce it returns is absorbed, so every later state varies from run to run. Two tests assumed otherwise and were flaky there: - a_ground_proof_verifies asserted every spent nonce was non-zero, but nonce 0 passes an 8-bit PoW with probability 2^-8. - a_query_only_chain_checks_its_query_nonce_in_every_round accepted only Ok or GrindingRejected for a flipped query nonce. A flip that still passes the PoW is absorbed, moves the transcript and fails elsewhere. The tests now read the verifier's grind checks through a logging transcript that records each check's state and nonce: - A ground proof's checks are exactly its spent slots, in order, and each nonce passes the PoW at its own state. - A forged nonce is the first value above the honest one that fails the PoW at that state, so the check itself must refuse it with GrindingRejected. The three a_forged_*_nonce_is_rejected tests forged nonce + 1 and carried the same latent flake; they now take the same forgery. Tests only.
Two P2-W tests read a nonce that grinding picks with find_any under the parallel feature: one asserted it non-zero, the other expected a flipped query nonce that still passes the proof of work to verify. Both now assert what the proof of work guarantees. Tests only.
Every device entry point calls device::backend() before it touches the card. A process-wide, monotone count of those calls (backend_entries()) lets a test bracket a phase and show it never reached the device. The first user is the W-LFM prove's host prep, which LFM_CARD_AFTER_PREP=1 moves outside the card permit. This is one relaxed atomic add per backend() call, with no other change.
…REP, default off) prove_traces_whir_opening takes the card permit as its first statement, so the card is held idle, and closed to every other proof, while the prove builds its tables on the host. At job 222 that prep was 2.05 s of the pure-WHIR recursion's 9.89 s of W-LFM holds, 1.68 s of it at level 1. The prep moves unchanged into prep_whir_tables: the plan's layouts, each table's main columns moved into its layout, and the prefix check. It takes no device handle. LFM_CARD_AFTER_PREP=1 takes the permit after that function instead of before. Unset, empty or 0 keeps today's order; any other value panics. The setting is read once and named once on stdout. The split line's wall stays prep + the held part in both settings, so the wait for the card is in neither. Tests: - Laptop: the knob parse and the test override. - Box, #[ignore]: the fixture's wraps and a wide node, proved with the setting off and on, serially and three at a time with the permit armed, under the deterministic grind. Every proof must equal the default's bytes. - Box, cuda: device::backend_entries() must not move across prep_whir_tables for any job. The paired control requires that it moves across the prove that follows.
The W-LFM prove now takes the card permit after prep_whir_tables, so its host prep runs while another proof holds the card instead of holding the card idle. LFM_CARD_AFTER_PREP=0 restores the permit before the prep. Only the lock moves: card_after_prep_tests proves the same programs under both settings, serially and three at a time, to the same bytes. Measured on block 25368371 (FAST, A B B A): -0.65 s at fan-in 3 (job 234) and -0.90 s together with fan-in 4 (job 236).
An unset LFM_CENSUS_FAN_IN now selects WHIR_WIDE_FAN_IN (4) when level 1 is wide, which it is by default under the W-LFM prover. Fifteen epochs then make four wide level-1 nodes (4/4/4/3), and the block-artifact root takes them directly beside the global wrap, so the interior level is gone. The WHIR trees without a wide level 1 (LAMBDA_VM_LFM_PROVER=stark and LAMBDA_VM_LFM_WIDE=off) keep WHIR_FAN_IN (3), and the STARK tree keeps FAN_IN (2), so their shapes and program ids do not move. LFM_CENSUS_FAN_IN=3 restores the previous pure-WHIR tree. Measured on block 25368371 (FAST, A B B A): -0.70 s alone (job 235) and -0.90 s with the card permit after the host prep (job 236). The tree-shape and root tests gain fan-in-4 rows. The production root (15 epochs at fan-in 4) joins the honest control, the fixed-size schema and both L2G tamper tests.
On a wide tree, level 1 verifies epochs rather than proofs. With two to fan-in epochs there is one wide node and no proofs below it, so root option A, which takes level top-1's output, would hand the root that one node against a fold shape expecting one digest per epoch; the drivers' child-count assert then refuses the block. RootOption::for_tree maps A to B there, so the root sits above the single node. One epoch needs no mapping: its one node folds a single root to itself. Tests: for 1..=40 epochs at fan-in 2..=4 the children a wide tree hands the root equal what the option's fold shape refolds to, and A as named fails exactly at 2..=fan-in epochs; the root over every small wide tree (1..=6 epochs at fan-in 4) executes at the artifact's fixed width; the moved-L2G tamper test covers one epoch and one node of three.
Both WHIR tree drivers now run the root option through RootOption::for_tree, so a block of at most fan-in epochs composes under the default wide tree. Such blocks failed the root's child-count assert: up to 3 epochs at fan-in 3, up to 4 at fan-in 4. The 15-epoch block's tree is unchanged. The fixture tree becomes a body over a block (guest, private input, epoch size, arity and the epoch count the run must reach); the three-epoch fixture runs as before. the_whir_fixture_tree_proves_every_ small_block (box tier) proves 1..=6 epochs of a new guest, test_private_input_spin, whose private input sets its spin count and so its cycle count, each to a verified root at the default arity. the_spin_guest_lands_every_small_epoch_count executes the guest on the host and checks each input reaches its epoch count.
The WHIR production driver's arity bound becomes 2..=5 so that fan-in 5 can be measured: LFM_CENSUS_FAN_IN=5 puts 15 epochs into three wide level-1 nodes of five, and the root takes them beside the global wrap. The default stays 4. The two STARK drivers keep 2..=4: nothing above four has been costed on them, and their arity-3 node did not fit the card. The tree-shape test gains the fan-in-5 row (15 epochs: 2 levels, 4 nodes); the root's fold-shape tests run at fan-in 5 as well, and the fan-in-5 root (15 epochs, 3 nodes) joins the root gates' shapes.
WHIR_WIDE_FAN_IN becomes 5: fifteen epochs make three wide level-1 nodes of five, and the root takes them beside the global wrap. LFM_CENSUS_FAN_IN=4 or 3 opts out; the stark opt-out and LAMBDA_VM_LFM_WIDE=off keep fan-in 3, and the STARK tree keeps 2. Measured on block 25368371 (FAST, A B B A, job 238) against fan-in 4: -1.55 s (level 1 -0.76, root -0.70). Level 1's census falls from 1,052.8 M to 852.6 M cells and the root's from 270.9 M to 149.6 M (its hash table stays under 2^18). The W-LFM argue's reservation peaked at 24.3 GiB of the 25.7 GiB budget: 1.4 GiB of margin, so a block with heavier epochs should be measured before relying on five. The small-block fixture test runs at the new default: one epoch, one node of two to five epochs, and two nodes at six. The root tests gain the fan-in-5 root in the tamper arms and the small-tree execution test.
The WHIR_WIDE_FAN_IN doc comment, and b682091's commit message, read the RESERVED HW figures, which the tree log prints in MiB, as GiB by dividing by 1000. The W-LFM argue's reservation peaked at 24,342 MiB (23.8 GiB) of a 25,688 MiB (25.1 GiB) budget at fan-in 5: 1,346 MiB of margin, not 1.4 GiB. Fan-in 4 peaked at 21,754 MiB. The ratio, and so the claim, stands. Comment only.
When the card refuses a GKR fraction tree's carry and handing it back saves enough to be worth it, input_layer_tree_impl asks for one promise for the whole tree. If the budget refuses that too on the consume path, logup::resident_tree gets None and the per-table argue builds the table's factors and whole tree on the host: slower, never wrong, and until now uncounted. The refusal is now counted where it happens, in multilinear::gpu::gkr_tree_refusals and in math-cuda's argue-surface device_fallbacks, and logged as it happens. A prefetch refused the same way is not counted: it only means no prefetch, and the consume site asks again. The WHIR production tree prints "gkr tree refusals N" beside "device fallbacks N", which now includes it. DEVICE_FALLBACKS' doc names its six sites by function instead of line numbers that had moved, and says why the other argue-side reservations in multilinear::gpu are not fallbacks: the carry is speculative, a prefetch is optional, and reserve_room's two callers keep the work on the card. A test-only hand-back threshold (set_hand_back_threshold_for_tests) lets a table smaller than the widest precompiles reach the whole-tree promise. multilinear's call-site census pins the one counted site; math-cuda's keeps its five.
A box test (cuda, ignored, run alone) on an ADD table of 2^12 rows, whose factors go to the card. At the normal budget the card builds the tree and nothing is counted. With every carry handed back and the rest of the budget held by the test, a prefetch is declined uncounted, and the consume path's refusal reads one GKR tree refusal and one argue-side device fallback. The host's tree, the path the refusal hands the table to, has the card's output fraction.
…re proved (W3_DATAFLOW) The tree proved level by level: a node whose children were all proved waited for the whole level below, and then for its own execute + fill with the card idle. At the median after the node pipeline the card still sat idle 1.4-1.6 s before level 1 and 0.9-1.1 s before each later level (BIG 611). Now one pool of `siblings` workers proves every program of the tree, taking them in topological order (the leaves, then each node level), each publishing its proof into a slot; 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. Workers that take programs in this order reach a node only after every program before it has been taken, so the earliest unfinished program never waits on an untaken one: no deadlock at any number of workers (tested; taking the nodes first deadlocks the test). The siblings bound, and so the memory in flight, is unchanged. A failed or panicking prove fails every program above it without a hang (tested). W3_DATAFLOW=0 is the control: each node waits for its whole level below (tested to never start early). A level's W3 LEVEL wall is now from the level below's last proof to its own.
…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.
…group lands StreamedExecution runs an LFM program as its arenas arrive in groups: one forward pass gives every instruction the set of groups it reads through any chain of memory (a Hint reads its arena's group; every operand address is below its destination), and each instruction runs in the wave in which the last of its groups lands, in the level schedule's order restricted to that wave, writing the record slot the schedule gives it. What reads no arena runs before any group lands. finish() refuses unless every group landed and every instruction ran exactly once, then publishes the slots as execute() does. The witness is execute()'s, word for word: the identity gate now also runs a node-shaped program (three independent sponges and a step over all three) in all six landing orders, and every identity case in two, against the serial reference; on the node-shaped case at least two thirds of the program runs before the last group lands. A wrong group set fails stop rather than miscomputes: dropping the propagation through memory is ReadBeforeWrite, and re-running an instruction in a later wave is DoubleWrite (both tested as mutations). Malformed landings (twice, wrong arena count or length, finishing early) are refused. The machine now holds its arenas as slices (an unlanded one is empty, so reading it is ArenaOutOfBounds), and the fill half of lfm_execute_and_fill is lfm_fill_executed, for an execution run elsewhere.
… child is proved (W3_STREAM_TOP) After the node pipeline and dataflow, the card still sits idle ≈ 1.05 s at the top node's start at the median (BIG 611 / 612): the top executes and fills only after its last child is proved. The top now streams its execution (StreamedExecution): its children are its arena groups, in order and the same number of arenas each; it lands each child's arenas as that child's proof is published (in arrival order, each once; a failed child fails the top with its error), so only the last child's share, the fill and the prove remain after the last child. The prove is the unstreamed one's over the same witness. The execute the split reports is the part after the last child landed. prove_dataflow now hands a program its children's slots unwaited, so a node waits for them as it needs them; the others still wait for all of their children first. W3_STREAM_TOP=0 is the control.
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).
Phase 4 round-robins its collectors into at most eight 80 MiB histograms, but LT, KECCAK and the other per-op sources were one collector each: at the median block LT (2.6 G cells of its ops kept to the finish) and KECCAK were single long poles, and each built one list of every lookup it sends (LT 8 lookups per op, KECCAK about 5,000 per permutation) before counting it. Every source that is a sum over its ops is now cut into slices of whole ops (LT, SHIFT, BRANCH, BYTEWISE, EQ, STORE 2^20; MEMW_A 2^22; KECCAK 2^11; ECDAS 2^16), and MUL and DVRM, which deduplicate per instance, into one slice per instance. The histogram is a commutative sum, so BITWISE does not move: the 187 whole-run trace digests (four programs at small and default caps) are equal before and after. (cherry picked from commit c369843)
…lectors (the A/B's control) The cherry-picked c369843 cuts phase 4's per-op BITWISE sources into slices. #1014 measures it as a memory lever: at the median, phase 4's whole-source lists were the peak's largest term that does not spill (unnamed 7.5 -> 31.8 GiB inside p4, BIG 568). So the path before stays behind LAMBDA_VM_P4_SLICED=0 for a one-binary A/B; unset, the slices run. The slice lengths now come from one function, p4_slice_len (MUL and DVRM: one instance, since they deduplicate per instance; the per-op sums: a bound on a slice's list of lookups). A test counts MUL, DVRM and LT whole and slice by slice at those lengths and needs them equal; its MUL and DVRM ops repeat inside instances, so a cut one row off does change the counts (checked in the test), and a p4_slice_len that misaligns them fails it.
At 1x and 2.66x the top node's program and artifacts arrive after its last child is proved (its artifacts are a short card hold that queues behind the children's proves), so a streamed top had nothing to stream behind and ran its forward pass and one wave per child after the last child: +0.19 s from its slot to its prove at 1x, and 1x recursion +0.22 s (BIG 617 / 618). At the median the slot fills 6-8 s before the first child and streaming paid (-0.47 s, BIG 613). Now the top streams only if a child is still unproved when its program and artifacts arrive, and executes whole otherwise (the control's path, so the proof is the same either way). W3 TOP EXECUTE prints which it did. A test covers a program ready before the last child (streamed), after it (whole), and a failed child (whole, which reports the failure).
…for its artifacts (W3_EXEC_EARLY) A node's slot held its program and its artifacts together, and the artifacts are a card hold that queues behind the proves below: at 1x and 2.66x the top's slot came 0.12-0.15 s after its last child although its program was emitted 0.03-2.1 s before it, and at 2.66x a level-1 node's artifacts waited 2.0 s for the card while its children were already proved (BIG 614 / 615 / 617 / 618's CARD HOLD lines). The node's execute and fill need only its program. Now the builder publishes each node's program as it is emitted, before its finish builds the artifacts, and the node executes and fills from it as soon as its children are proved; only the prove waits for the artifacts, in the node's own slot (node_flow). The traces are filled under the block hasher, which the node artifacts are built for; the prove asserts it. The top's streaming choice is taken when it can execute. W3_EXEC_EARLY=0 is the control (the execute also waits for the artifacts). The proof is the same: the execution, the fill and the artifacts do not change, only when each runs. A toy at the median's shape over build_levels, prove_dataflow and node_flow shows, at 1 to 6 workers and without a hang, that every node proves only with its own artifacts and after they are built, and that nodes execute before them. The toy builder checks each program is published before its finish starts.
…ts emission ends The builder's thread published a node's program only when it took the emission off the channel, between finishes, and a finish holds the card for the node's artifacts: a program emitted while a sibling's artifacts waited for the card was published only after them. At 2.66x a level-1 node emitted at 4.04 s got its program at 6.30 s, behind its sibling's artifacts that waited 2.1 s for the card, so it executed after level 0 and the card sat idle 1.08 s (BIG 622, run 9). Now each emission publishes its program on the pool thread that emitted it, before it is sent to the builder's thread to finish. The toy now emits a level in reverse and holds the card 120 ms in the first finish, and checks every node gets its program within 40 ms of its emission or its take.
…s is refused, not asserted LfmFilled::prove checked that the artifacts were built for the hasher the traces were filled with by a release assert_eq. Since the W3 tree fills its leaves and nodes before their artifacts exist, the pair comes from two places, and a mismatch would panic the prover. It is now LfmProveError::HasherMismatch, naming both hashers, returned before anything reaches the card. The streamed execution's finish likewise returns an internal error instead of asserting the public words' capacity before its set_len. The proofs are unchanged.
…as a knob Port of #1010's knob (fc0ff59) to the no-epoch WHIR block. The WHIR chains ground 20 bits, a constant. The knob makes the bits a format parameter read at the one config site, chain_config_under, which every side of the block reaches through BlockFormat::chain_config: the prover's group chains and prepared openings, verify_block_whir, and the plan the block leaves are emitted from. All of them take the bits from the process format, never from a proof, and the block statement absorbs Q and the grind bits. The query count already subtracts the query grind, so 18 bits raises Q from 112 to 114 at every production height (15..=27 variables); every proven phase keeps its minimum (binding WHIR phase: the unground fold at 27 variables, 130.393; query phases 130.926 -> 130.907). The block tree's own leaf, node and top proofs are STARK proofs under aggregation_wrap_options and do not read this knob. Unset is 20: today's configs and proofs, byte for byte. The banner gains whir_grind_bits=. A chain ground at fewer bits is refused by a stricter verifier on both the host and the machine, and a proof opened at a Q the verifier does not expect is refused. (cherry picked from commit fc0ff59)
…nd 18 grind bits Prints the emitted chain verifier's real rows per chip, production format, n 21..=27, under LAMBDA_VM_ZF_WHIR_GRIND_BITS 20 (Q 112) and 18 (Q 114): the per-chain deltas that size the recursion's table heights under the 18-bit arm. Asserts nothing; ignored. (cherry picked from commit 9d51421)
… host and in its leaves - a_block_ground_at_18_bits_is_refused_by_a_verifier_at_20: a block proved at 18 bits (Q 114) verifies under 18 and is refused by verify_block_whir at 20; a block proved at 20 is refused at 18. - a_block_leaf_at_20_bits_refuses_a_block_ground_at_18 (box tier): over a block ground at 18, the plan at 18 emits a leaf that executes and the plan at 20 emits one that refuses it. - grind_bits_group_cost_census (ignored instrument): the plan's charge for a group's stacked opening per stack height and polynomial count at 20 and 18 bits, which predicts the W3 plan's costs and leaf count under the arm. - The real-block tree driver prints each leaf's chips, real / padded rows (W3 LEAF CENSUS), so a run shows which leaf table, if any, doubled.
…used, not asserted Two release asserts on the prover's path become typed errors: lfm_prove_with_hasher's assert_eq between the artifacts' hasher and the one asked for is now LfmProveError::HasherMismatch, returned before anything runs; and the unstreamed execute's capacity assert before its public words' set_len is now LfmExecError::Internal, through public_rows_fit, which the streamed execution's finish uses too. Each has a test. The proofs are unchanged.
…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.
…e tests HostTable / host_table_forked, TableLegs / build_table_legs / fri_layer_openings and the child harvest (RealChild, now HarvestedChild, with its arenas) are what the W3 tree's driver needs to fill each node's arenas from its children. They lived in epoch_tests, epoch_verify_tests and per_table_aggregator_tests; they now live in lfm::harvest (the same module as #1013's), and a proof that disagrees with its AIR is an Err instead of an assert. The suites keep every name and its panicking form through re-exports and shims. Same logic, same order.
the_whir_block_tree_on_a_real_block's body, with prove_tree_pipelined and its machinery (the publish slots, build_levels / build_nodes, the dataflow, node_flow, the streamed top), was the only way to prove a whole WHIR block as a tree. It is now lfm::whir_block_tree::prove_whir_block_tree, with every knob read once by WhirTreeConfig::from_env (same names, same defaults: W3_*, BLOCK_WHIR_*), every line sent through a WhirTreeSink (the harness prints to stdout as before, byte for byte, plus a first BLOCK POSTURE line), and every panic on the run's path an Err. The harness test is a wrapper that keeps its off-clock checks (the early leaf's arena, the device line, the top digest, every tree proof and the base verified, the block verifier). in_index_order moves to lfm::tree_run; the BLOCK_WHIR_* env readers in block_whir are no longer test-only. The toy and dataflow tests stay in whir_block_tests and import what moved.
…verifier WhirBlockTreeProof is what a consumer of a whole W3 block receives: the block's statement and the top node's proof, behind the magic, the layout version and a pipeline tag shared with #1013's STARK block file (so the two trees' files are never read as each other's). verify_whir_block_tree_proof is whir_block::verify_block_tree over the claimed statement, unchanged: the plan and the top program are still derived from the trusted ELF under the block presets, and no format parameter is read from the file.
The shipped binary could not prove a whole WHIR block as a tree, and it had no CUDA build. prove-block runs lfm::whir_block_tree::prove_whir_block_tree (the driver the W3 harness runs) and writes a WhirBlockTreeProof; verify-block checks it with verify_whir_block_tree_proof. For the two block commands the binary sets the production posture (table parallelism, the row cap, retention, the RPX WHIR hash, the tree cache cap, the executor schedule, the grind search) for every knob the environment leaves unset, before any thread exists; the WHIR hash is a format knob, so verify-block sets it too. W3_LEAVES, W3_FAN_IN and BLOCK_WHIR_ARGUE make a tree the block verifier does not derive and are refused. No purge: #1014's harness has none. New tests: the arguments, the posture plan, and the never-purge conf this binary compiles in.
…tamps dataflow_proves_the_level_by_level_programs_in_any_completion_order asked whether any node started before its level below ended by comparing millisecond stamps, and at a laptop load of 11 a 2-worker run once found no such node (i-cli, 1 of 5 runs). Now the last leaf, once taken, holds its worker until some node starts or 1 s passes, and the test reads whether that signal came: with two or more workers and dataflow a node takes the free worker and starts while the leaf still proves; under the barrier, or with one worker, none can. The proved texts are checked as before. Making the barrier inert, or always on, fails it.
The same writer as #1013's G-pack: a generator writes its trace straight into packed columns at guessed widths, the writer keeps the OR of every word per column, narrows the columns given more bytes than they needed in place, and names the widths the trace needs when a word did not fit. Its bytes are NarrowMain::pack's for the same words. Here a trace holds its packed columns as multilinear's NarrowColumns (the same layout), so NarrowMain::into_parts is public and TraceTable::try_from_narrow_main takes the columns, giving them back where a trace cannot be held packed.
…ctly Each generator's fill runs through generate_main! (tables::gpack), as on #1013: TraceForm::Wide is today's 64-bit table; TraceForm::Narrow writes the packed columns directly at the widths the table's earlier traces needed, narrows or rewrites on a miss, and builds a kind's first trace wide then packs it to learn them. The bytes are NarrowColumns::pack_row_major's of the same words whatever the hint. On the block (BlockOptions::gpack, LAMBDA_VM_BLOCK_GPACK=0 the old path): - each streamed chunk is written packed by its job and laid out narrow from its packed columns (table_of_narrow), with no 64-bit table and no transposition, when the groups are held narrow; - with pack_finished, the finish writes each table it packs packed (WindowedTraceBuilder::generate_packed), KECCAK_RND's chunks included; - BLOCK GPACK reports how each trace was built. Tests: every path of the writer gives the wide table packed; every table of a windowed build in the block's configuration, on four programs, has the packed bytes and words of the same build without G-pack; one column a width too wide or shifted fails that comparison; the block proves with the same partition and tables (the same bytes under the deterministic grind) with G-pack on or off; a box-only test compares every table of a real block.
stark gained a libc dependency (ee252c1, the packed-trace store imported from #1013) without the recursion guest workspace's lockfile, so every make compile-recursion-elfs rewrote bench_vs/lambda/recursion/Cargo.lock and left a tracked file modified. This is the lockfile cargo writes; no dependency version moves.
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
1 participant
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.