Repository navigation
WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1014
Draft
MauroToscano wants to merge 1389 commits into
Draft
MauroToscano wants to merge 1389 commits into
MauroToscano wants to merge 1389 commits into
Conversation
…no byte Against a codeword opened with the switch off: the same root, paths, and paths with their cap, with no build; then a covered eviction takes the tree, the next opening builds the same tree and keeps it whole again.
…tention line Appended after the futile misses: whole trees on|off (N openings served).
Flips LFM_WHIR_WHOLE_TREES to on: the tree a commit builds stays on the card whole, inside the codeword's promise and behind the same evictor as a leaf layer, and an opening with a matching kept tree reads its paths and builds nothing. LFM_WHIR_WHOLE_TREES=0 keeps leaf layers as before. Measured on the block (A B B A): the whole run -1.00 s, the base -0.90 s, the openings' tree rebuilds -0.82 s; 952 openings served a kept tree. The argue's peaks in epochs 3-5 reach 25,633 / 25,306 / 25,681 of the 25,688 MiB budget. That is safe because everything kept is evictable: a request the kept bytes can cover evicts them and succeeds, one they cannot cover fails either way, so fallbacks cannot rise and the worst case is the old rebuild. A unit test pins the default and the kept-tree size. The comments that said a tree is never held past its build (whir.rs, stacked_eval.rs, whir_commit.rs, gpu.rs) now state the invariant that replaced it: nothing of a tree is held outside a promise.
…s guard Every card test whose counts or byte figures depend on what a commit keeps now forces LFM_WHIR_WHOLE_TREES both ways instead of running at whatever the default is: the per-codeword counts, the reservation test, the blocking-key test, the process-wide counter identities, and in whir_cap.rs the served, rehashed and evicted cap regimes. H4's group guard used to forbid a tree held past its build. It now asserts the invariant that replaced that rule: four unopened commits keep exactly the object the mode names, the ledger grew by exactly four codewords and those objects, the driver holds less than one tree and one codeword beyond the promise (four trees kept outside it would read four trees there), and what is kept is really held (more than the next smaller retention). Under leaf layers the old two-sided bound is kept as it was.
…its slot An opening served a kept whole tree reads it through its own Arc after the slot's lock is let go. The promise used to be given back by the slot's drop, so an eviction during that read (or the codeword dropping) returned the tree's bytes to the ledger while the buffer was still held: for as long as the read lasted the ledger counted less than the card held. With whole trees that read happens on every served opening. The buffer now carries its own promise (KeptNodes): grown into the room when it is admitted, given back by its own Drop, after the free is enqueued, on the last handle. It holds its room strongly, so a room can no longer drop, giving back every byte it counts, while a buffer it counts is still held; that only happens during the evictor's walk, which can hold a slot past its codeword, and it keeps the rest of the room counted for that long. The evictor passes over a tree an opening is reading, and does not count it as reclaimable: dropping the slot's handle would give nothing back and lose the tree. A request only that tree could cover now fails, counted, instead of being handed bytes the card still holds. Passes are counted (retention_read_passes) and noted on the eviction lines. The card test holds a reader (hold_kept_tree, test-only) across an eviction and across its codeword's drop, and asserts the ledger counts the tree until the reader lets go, then gives back every byte.
…and a capture hook
multilinear::fused computes a table's zerocheck batch the stage-1 way
and sends today's messages: the bus's two rules as one column L (S1-2),
the eq weights pulled out of the rounds with A_j(1) from the claim
(S1-4, Gruen), and rounds 0 and 1 from one base-field pass over the
4-row groups on the {0..d}^2 grid (S1-5), with a corner skip for traces
that satisfy their AIR and a corner check that refuses the first row
that does not. Today's rounds and S1-2 alone run through a counted copy
of today's round loop. Every variant counts its work by phase, and
fused::model states the same counts in closed form for any height.
Host only: nothing in the prover calls it. The only production change is
multilinear_table::argue_capture, a test hook that records a table's
argue inputs while a test has armed its width; disarmed it is one
atomic load and records nothing.
Tests: every variant against batch::prove over today's batch (rounds,
point, transcript, next challenge, factor values) on a synthetic table
at every height to 2^7 and on all 26 VM tables and 10 W-LFM chips over
random columns; model == counters throughout; the base-field
precondition on all 36; negative controls (a wrong L coefficient, the
corner skip on a broken trace, a flipped cell). The real-trace half
proves a program to capture one and is ignored, for the box.
D-ARGUE stage 1's device twin of multilinear::fused, behind
LAMBDA_VM_ARGUE_FUSED=1 (every table, or the committed widths
LAMBDA_VM_ARGUE_FUSED_WIDTHS lists): rounds 0 and 1 from one base-field
pass over the 4-row groups on the {0..d}^2 grid (zc_grid01, zc_bus_u),
both folds at once into a quarter-size ext3 copy (zc_fold2), the bus as
one column L there (zc_bus_column), and the later rounds walking the
constraint part alone at the integer nodes {0, 2..d} under split eq
weights (zc_round_gruen, zc_halve), down to today's host crossover. The
messages come out of the sums through the reference's own assembly
(fused::message), so every message is today's.
The constraint program is the base DAG with an ACC step after each root
(gpu_fused::lower_fused), so roots are summed as they are made. The
lifted factors are only read, so LAMBDA_VM_ARGUE_FUSED_XCHECK=1 can run
today's device rounds after the fused ones with the same challenges,
compare every message and the factors at the crossover, time both
(one ARGUE FUSED line per table, with R = fused / today) and check the
grid's corners per row.
S1-1 on today's kernel: LAMBDA_VM_ARGUE_INT_NODES=1 takes a round kernel
that interpolates with the componentwise base multiply when every node
is (k, 0, 0).
Both knobs default off, and off is today's path unchanged: the table
prove builds nothing for the fused rounds, batch::prove_resident is
prove_resident_with(.., None, ..).
Tests: the lowered blob against today's zerocheck rule on all 36 tables
(host); on the card (box): the fused rounds against today's host rounds
on every table at 2^8 and the three at 2^10 and 2^12 with the
cross-check confirming each, the integer-node rounds, and two negative
controls - a wrong bus coefficient refused by the cross-check, a broken
trace refused by the corner check - each with a mutation switch that
makes its check inert.
They flip process-global switches (the fused rounds, the cross-check, the faults), which would reach any proving test running beside them in a suite run. Ignored, so a gate runs them with --ignored --test-threads=1.
A committed table carries no name, so each ARGUE FUSED line gives its signature - roots, bus terms, walk slots - beside its factor count, and a declined table prints a line of its own under the cross-check or LAMBDA_VM_ARGUE_FUSED_LOG. LAMBDA_VM_ARGUE_INT_NODES=1 prints one banner when it is first read, so an arm's log shows it took effect.
The upload declines a table under 4096 cells (gpu::worth_the_device), and the prover then argues it on the host, so a run at 2^8 of EQ's 12 factors never reached the card: FAST job 271's one red. Each table now runs at 2^8 or the first height above it with 4096 cells.
A table without roots has a zero constraint part and d_C = 0, so its
grid {0,1}^2 is all corners; with the corners skipped - the production
setting, no cross-check - no grid point is left, and the launch sizing
divided by that empty row count. FAST job 273's B arm panicked there
("attempt to divide by zero", argue_fused.rs:101) at the first such
table; its X arm, whose cross-check computes the corners, proved and
verified with all 390 fused tables confirmed.
An empty point list now launches nothing (T is zero) and sizes no slot
file; U is still computed. A host test pins the sizing (it reproduced
the panic at the same line before this change). Two card tests close
the gap that let it through, both with the production switches: every
table without roots against today's host rounds, the corners skipped;
and test_keccak proved under the B arm's switches, with and without the
cross-check, and verified.
The FAST A/B at 9e27289 read EFFECTIVE twice (jobs 274 and 270, pooled over 4 A and 4 B arms): base -2.80 s, the argue -2.94 s, the whole run -2.75 s, every B arm's base below every A arm's, identities equal on all eight arms, no fallback; the cross-check arm confirmed every one of 390 fused tables' messages against today's rounds. LAMBDA_VM_ARGUE_FUSED and LAMBDA_VM_ARGUE_INT_NODES are now on unless set to 0, and 0 is today's rounds exactly. Each prints a banner when first read, and a unit test pins each default. A fused session counts as a device sumcheck (gpu::sumcheck_calls, sumcheck_rounds), and the split's ARGUE ZEROCHECK line ends with the fused sessions, the declined ones and their device time, so an arm's log shows which rounds it ran.
…is refused With the fused zerocheck on by default, the tall-table knob tests pin it off: every other argue knob acts on today's rounds. Two tests on top: the tall tables proved with the fused rounds (alone, and with the device columns, tables and gathered reads) give today's canonical bytes table by table and whole, the same transcript and next challenge, and verify - on a device the fused arm shows its sessions; and with the fused rounds' bus coefficient off by one the proof parts from today's at CPU and does not verify. The fused faults are per thread now: the fused rounds run by default, so a fault armed for one test must not reach a proof another test runs beside it, and a table's argument runs on the calling thread.
…AMBDA_VM_ARGUE_GKR_GRUEN
D-ARGUE S1-3 (D-BATCH M1-1). A device GKR layer's round sends
s(t) = E·eq1(u_j, t)·H(t), with H(t) the layer's h summed under
eq(u_{>j}, ·). The card now sums H(1) and H(2) only - every node by
additions, no eq factor and no program walk - and folds the previous
challenge on the way in; the host puts E·eq1 back, takes H(0) from the
claim (the card sums it where 1 - u_j has no inverse) and extrapolates
H(3). The weight is two small tables a layer (the tail's variables and
one level per card round), not a layer-sized eq table folded each round.
The rounds stop at a cube of LAMBDA_VM_ARGUE_GKR_GRUEN_TAIL (default 64)
and hand the host today's five factors there.
Every message is today's field element, so the transcript and the
canonical bytes do not move. Off by default: off is today's rounds.
- math-cuda: kernels gkr_eq_levels_ext3, gkr_round_gruen,
gkr_gruen_finish; GruenLayer (tree layers and the rebuilt input
layer); SumcheckSession::fold_first for the cross-check's shadow.
- multilinear: gkr_gruen (knobs, the host's half of a round, counters,
a per-thread fault, a host reference of the device algorithm);
DeviceTree::prove_layer_gruen; LAMBDA_VM_ARGUE_GKR_GRUEN_XCHECK walks
today's program over the same folded halves each round and compares
rounds and factors; the ARGUE GKR line ends with the Gruen counts.
- tests: the host reference equals today's rounds, challenges and
factors at m 1..9 over every tail split, with H(0) direct or derived,
and with coordinates of one; a wrong claim changes it. Device tests
(tests/argue_gkr_gruen.rs) and stark's tall-table byte identity and
fault test run on a card.
…H B-2)
A new proof format behind ChainFormat.argue (default PerTable, today's):
ArgueFormat::Batched { bin_log_cells } runs one lockstep LogUp-GKR ladder
per bin of tables (multilinear::gkr_lockstep), one front-loaded constraint
sumcheck over every table with virtual padding by the product of the
missing variables (multilinear::front_loaded), and no claim reduction for a
table whose committed factors are all unshifted: its factor values are its
column claims. A shifted table keeps today's reduction at its prefix point.
The batched proof is its own type (stark::multilinear_table::batched::
BatchedMultiProof), so MultiProof and today's bytes do not move; the
openings are shared code, factored out of multi_prove/multi_verify
unchanged. Each side refuses the other format's config
(Error::ArgueFormatMismatch). argue_plan is the one function that bins the
tables (first-fit-decreasing by input cells under the cap).
Tests: round trips across heights and bins, one-row and rootless tables, a
shifted table; every D-BATCH negative (bus output, ladder halves at a mid
step, GKR and constraint rounds, factor values, swapped tables, padding by
scaling, suffix of xi, cross-table weight, table claim, bin partition,
reduction shape, violated constraint, bus multiplicity, preprocessed column,
cross-format); a mutation test per new verifier check. Box tests for every
VM table and the W-LFM chips are #[ignore]d.
…he epoch bookend The first box run argued 22 of the census's VM labels. The round trip now also proves test_ecsm (ECSM, ECDAS), the load/store programs (LOAD, MEMW), hint_min (HINT) and every epoch of two continuations (the L2G bookend, DECODE's prepared opening, two commitment groups), and asserts that every label of lean_program_census::vm_airs was argued batched and verified.
…GRUEN=0 the opt-out FAST job 330 (4 + 4 arms on #1010 + Q1b): base -1.77 s, the argue -2.08 s, the whole run -1.57 s, the GKR 4.24 -> 2.13 s, the same program ids; its cross-check arm compared 3,381 real layers with the old rounds and found every one equal. A unit test pins the default.
Continuation AIRs carry no name (they print as `unknown`), so FAST2 206 argued and verified the L2G bookend of every epoch yet reported the census label L2G missing. The bookend is pushed last, and is now recorded by its label.
A committed stack can now be retired: each codeword is dropped and only the root and the top of its tree (every level but the bottom few, never into the Merkle cap) stay on the host. Reviving it re-encodes the same codewords from the columns, on the card with no tree built (math_cuda::whir::encode_codeword_*), and the first round's paths are read from the kept top plus the dropped levels re-hashed from the queried cosets. The re-hashed subtree root is checked against the kept node before any path leaves, so a codeword that is not the committed one is refused (RecomputedCodewordMismatch) instead of opened. This is what the block prover holds between committing a group and opening it. Nothing on an existing path moves: commit_from is split into encode + tree with the same calls, and a commitment that kept its tree reads its paths exactly as before. Tests: a retired and revived stack opens to the same bytes as one that kept everything (drop 0, 1, 3, more than the depth; and under a cap); revived over other columns it refuses to open (the kept-node check is load-bearing: disabling it fails that test).
…by group multilinear_block: the tables split into groups a card holds (contiguous runs, at most N stacked polynomials each, a function of the shapes and the format that both sides compute). Phase A commits each group and retires its codewords; every root goes into the transcript and (z, alpha, beta) are drawn once; phase B re-uploads each group's columns, argues its tables and opens its stack on the fork S_post || g. The verifier mirrors the forks, refuses roots no layout claims, and checks the bus balance once over every table of the block. Per-group stamps (upload, commit, retire; upload, argue, encode, open) are returned for the W1 readout. No existing proof path is touched.
A separate entry point beside #1010's epoch pipeline, which it does not touch: execute the block, build its traces at 2^21 rows a table, split KECCAK_RND into 2^16-row tables (today's tallest), and prove every table in one multilinear_block proof under a statement tag of its own (MULTILINEAR_BLOCK_TAG; the monolithic statement otherwise). Memory is the monolithic PAGE argument. The groups (3 polynomials of 2^27 at most, today's heaviest epoch) and the stack are verifier-side constants (BlockFormat); the KECCAK_RND height and the tree levels kept are the prover's. A block statement may declare several KECCAK_RND tables, up to a bound checked before any AIR is built. Tests: round trips at one group and over many; KECCAK_RND in chunks; proofs that verify at every kept tree depth, byte-identical from the same traces under a deterministic grind; refusals for a group proved on another fork, a block missing a real KECCAK_RND chunk (on the bus; the balance check is load-bearing), a tampered column claim, bus output, public output, table height, an extra root and an inflated count. An ignored test proves and verifies a real block with the phase stamps.
…ock's fallbacks block_whir_epoch_reference_on_a_real_block proves the block through #1010's epoch pipeline (prove_continuation at 2^21) with the base split on and prints the summed argue, openings and commit of every epoch and the cross-epoch proof: the same-binary control the block's phase B is read against. The block test now prints the device's host fallbacks, so a readout that ran on the host says so.
|
Benchmark Results for modified programs 🚀
|
…3, first cut) multi_prove_batched now runs where today's argue runs: each bin's trees are built from the factors on the card (else here), the ladder steps every active tree's layer on the card through a steppable LayerSession (DeviceTree::layer_session, the session prove_layer opens) with the batched step's per-tree program eq*(w_p*num + w_q*den), hands the cube to the host at today's crossover, and sums the trees' rounds on the host before the one shared challenge. The constraint sumcheck drives each table's fused zerocheck (FusedStepper, prove_fused's rounds made steppable; prove_fused is now a loop over it) in lockstep through front_loaded's RoundStepper, a table's message read at D_max nodes by interpolation past its own degree. A table the card declines runs on the host. The host reference (Where::Host) is what the negative tests prove; the card must produce its bytes. Not yet: one sync per round across trees (each session reads its own round back), the crossover on the bin's summed half-cube, and the VRAM plan (every table's lifted factors stay resident from its tree to the end of the constraint phase), which waits on M1-2.
…up during the argue Phase A no longer waits for every table: a producer lays each group's tables out (transposition, preprocessed check, layout; the group's tables in parallel) and hands the group over while the card commits the group before it (BlockCommitted::commit_streamed, one group of slack). In phase B the next group's columns go up on a helper thread during the current group's argument, so only the part the argument did not cover is paid. For the readout: the trace build's phase ends and each phase-5 generator's finish (trace_builder::build_stamps, off unless the block prover turns it on), phase A's per-group wait for its tables, and the first-round path counters (open_many calls served from kept tree tops, leaves re-hashed): a revived commitment builds no tree, so nothing re-commits.
…H S0) Under LAMBDA_VM_BASE_SPLIT only, and byte-identical: the argue's "rest" - what is neither a device GKR layer nor a zerocheck round, 3.19 s a block known only by subtraction - is timed per region of a table's prove: interactions, tree, output, gkr (its host prefix apart), setup, batch, factor values, claim reduce, column evaluation, release. One `ARGUE REST #k` line an epoch sums them against the argue's wall, and one `ARGUE AIR #k t NAME` line a table gives the shape D-BATCH's plan is sized from (n, columns, factors and how many read a shifted row, interactions, k, degree, roots, widest bus message) with its tree, gkr and core times.
…lves prove_argue and verify_argue run phases G, C and Rd from the shared challenges to every table's column claims; the roots block, the bus balance, the preprocessed checks and the openings stay in prove_batched_on and verify_batched_with. No transcript moves. The halves exist for the in-guest leg's gate, which argues a few tables with no commitment, as the per-table leg's gate calls prove. The real-table card-vs-host byte test compares the roots and the argue: the openings grind under the production config, and the parallel nonce search makes any two honest proofs part there (FAST 340: test_keccak's card and host proofs both verified and differed).
… B-4a)
emit_batched_argue is verify_argue emitted: per bin its outputs and one
lockstep ladder (a shared mu, each step's relation asserted), one
front-loaded constraint sumcheck (xi, lambda, the tables' rules weighted
lambda^{3t}, each padded by the suffix product of the challenges it
lacks, asserted), the factor values absorbed, a shifted table's reduction
and an unshifted one's direct column claims. It derives every challenge
from the transcript it drives; the plan is argue_plan's.
batched_argue_cost predicts its rows, constants (by value) and sponge.
Gated against real batched argues of three tables (two shifted), in one
bin and in three: the verdict equals the host's verify_argue, the form
equals the emitted census exactly (1517 and 2026 rows), and six forgeries
the host rejects cannot execute. On that fixture the leg is 1517 rows and
109 permutations against the per-table legs' 2322 and 182.
Table::columns_blocked: row blocks in parallel, a band of 64 columns at a time, so each row's cache lines are read once instead of once per column. Same columns in the same order (pinned against Table::columns over one-column, sub-band, band-plus-remainder and KECCAK_RND-wide shapes, partial last blocks). Used by block_whir's layout only: FAST 361 showed the per-column strided read's memory traffic tripling phase A's upload when the two overlap. Laptop timing (38 x 2^21): 1.02 s -> 0.54 s.
Under LAMBDA_VM_BASE_SPLIT, an ARGUE TREE line an epoch splits the tree region S0 measured at 1.80 s a block: the factors lifted, the input layer's programs lowered and written, the levels folded, the output read. The card runs the first three asynchronously, so LAMBDA_VM_ARGUE_TREE_SYNC=1 (a diagnostic, never a wall measurement) makes each part wait for its own kernels and charges it its card time. Byte-identical.
…byte-identical) Every long list the windowed builder grows over the run (the routing's segments: BRANCH, EQ, BYTEWISE, STORE, the MUL / DVRM / SHIFT / BITWISE / LT parts; the kept rest: ECDAS, CPU32, KECCAK, COMMIT, BLAKE3, ECSM, HINT, the in-walk lookups; the compact LT stream) was a Vec grown by extend once a window. A full Vec doubles: an allocation as large as the list and a copy of it on the accumulator thread. At p90 after S1 the largest is BRANCH, 2.44 GiB in one Vec (its next doubling 4.9 GiB); the builder term stepped up to +1.36 GiB between two memlog ticks of the walk (+3.21 before S1, BIG 670); the 195 Mgas scout died on such a step (+24.2 GiB, RYZEN 015). BlockVec stores a list in blocks of a fixed length: the first grows as a Vec does up to that length, every later one is allocated whole, and a full block never moves. A block is a table's chunk (2^21 ops at the production rows for ops of 32 bytes or less) or at most 64 MiB; ECDAS's are the block proof's 2^17-row cut (about 245 MiB). The compact LT stream goes in 64 MiB blocks, an op's two varints never straddling two, its sparse index addressing (block, offset). The finish reads every such list as the concatenation of its blocks (S1's Segmented): a chunk the block length divides is a block, borrowed; a chunk that straddles two blocks or segments is copied as it is generated. The lists the routing makes from several segments (MUL, DVRM, SHIFT, BITWISE, LT) are their segments' blocks in the routing's order, so assembling them no longer copies them either; a whole-run build's lists are one block each. Phase 4 counts block by block, MUL and DVRM instance by instance of the concatenation. STORE's streamed chunks are its front blocks, moved out. BLOCK MEM prints each builder list's largest single allocation at windows walked (builder largest). Tests: a block list is the Vec it was appended, pushed or a window at a time, at block lengths 1 to 64 and every list length around them (empty, one, exactly full, one past), every range and every chunk size, a chunk of the block length borrowed; chained and taken from the front in order; the block length fits 64 MiB and the chunk. The compact LT list expands to what was pushed with its stream cut into blocks of a few ops. ECDAS's block is the block's ECDAS cut. The windowed drop test builds the whole-run tables at every window and chunk size. Mutations each fail one: a block overfilled by one, the front taken one element late, a chain's length dropped, the compact decoder crossing a block one byte late, MUL's segments out of order. Every table's digest over 13 asm programs, whole-run and windowed in six configurations, is S1's (351 digests, fixed trace hash; a probe, not kept).
…s, packed (byte-identical)
The finish built each of the three whole and wide (they stayed wide under
pack_finished), and the block then copied each apart with split_rows: at p90
ten tables, 5.09 GiB at eight bytes a cell, the rest's only wide tables. Their
layout then transposes them into one 1 MiB column at a time on the layout
thread, which lands on fresh pages while the finish's freed extents sit
unused: VmRSS +4.7 GiB with live flat from `finish done` to `rest laid out`
in every p90 run (BIG 660, 668, 669).
A row of each reads its own op alone (one permutation call, one scalar
multiplication, one double/add step) and their padding rows are constants,
so rows [k*R, (k+1)*R) of the whole padded table are the ops in that range
and the padding to R rows. generate_{keccak,ecsm,ecdas}_rows_as build a
table of R rows from such a slice (the whole-table generators are that at
the padded height), and cut_tables builds the cuts the split makes, the
first alone until G-pack knows the family's widths and then the rest in
parallel, each packed as it is built and read from the list's blocks (a
cut that is a block is borrowed: ECDAS's blocks are its cut).
StreamSkip::{keccak,ecsm,ecdas}_rows and WindowedTraceBuilder::cuts_at_finish
carry the block's cut sizes;
BlockOptions::finish_cuts turns it on (production, unless
LAMBDA_VM_BLOCK_FINISH_PLAN=0, the A arm: whole, wide, then split), and the
block no longer splits tables the finish cut (a packed table has no rows for
split_rows to copy).
Tests: for each family, every op count around the cut sizes and every cut
from one row to past the whole table, built wide, packed after the build and
written packed, the cuts are split_rows of the whole wide table word for
word, with the same heights, packed exactly when asked, the ops in one
block or in blocks of three that the cuts straddle; no ops give no
table; a cut that is not a power of two is refused. The windowed build with
the cuts at the finish is the whole-run build with the three split, table
for table, on the keccak and ECSM fixtures at cuts of 1 to 64 rows.
…dentical) build_traces is now FinishPlan::new, which runs what needs the whole run before any table (LT's segments, the BITWISE histogram, HALT and the REGISTER final state, the public output, the PAGE layout) and counts every table it will build without generating one (RestHeader: the table counts, the page configs, the public output and the BLAKE3 count, what a statement is read from), and FinishPlan::emit_all, phase 5 as it was. emit_all refuses tables the header did not count (Error::Prover). One path still serves the block's windowed finish, the epochs and the whole-run build. This is the enabler for streaming the finish: a statement's shape is known before the tables are, and the tables can then be made and handed on in AIR order. Nothing is streamed yet and nothing moves in time. generate_page_tables is split into page_configs_of (the layout) and page_trace (one page's table), the same loop; Traces::runtime_page_ranges is runtime_page_ranges_of over the configs. Tests: the table phase as it was (build_traces at 6cbf1c4) is frozen test-only as the oracle (finish_oracle, switched on per thread, counting its runs so a test knows its oracle side ran). The plan builds the oracle's tables word for word on whole-run builds (13 asm programs, small, 4-row and production chunks), on non-final and final epochs with and without the L2G bookend, and on windowed builds in six configurations (streamed ops kept or dropped, the derived LT ops raw and concatenated, KECCAK_RND chunked at the finish or streamed, the KECCAK / ECSM / ECDAS cuts, packed and written packed, the MEMW-derived LT streamed) at two chunk sizes and two windows. The header is the oracle's counts, runtime pages, page count, public output and BLAKE3 count before any table is built, and every family miscounted by one either way is refused.
…3c-ECDAS; byte-identical) The windowed builder keeps every ECDAS row to the finish, and a row (EcdasStep and its timestamp) is about 1.87 KB, 1.5 KB of which are its three carry arrays, [i64; 64] each: at p90 the kept ECDAS list is 1.78 GiB, the builder's largest after BRANCH, and transfer-heavy blocks grow it fastest (7-16 GiB projected at 200 Mgas, D-FINISH 2.6). The trace range-checks every carry as its offset 16-bit value. A CompactEcdasOp keeps the row's other fields as they are and its carries as those offset u16 values, about 0.72 KB a row. A row with any carry outside 0..2^16 once offset keeps all three arrays as they are (boxed), so every row widens back to exactly the op it was made from whatever the input; the release build has no range assert to rely on. The builder holds ECDAS as compact rows (in its 2^17-row blocks, now about 91 MiB each), and so does every collected run. Each reader widens a row as it reads it, never a list or a cut: the generator fills a table from rows in any form (generate_ecdas_rows_of), and phase 4 counts a row's lookups from its widened op. The tables are the same. Tests: every row widens to the op it was made from, carries at both ends of their offset range held compact, and a row with one carry outside it (by one either side, at i64's ends, far out) held as it is; a compact row is under 40% of the op. A table built from compact rows is the table of the ops, wide and packed (with the fallback rows where the debug checks are off). Phase 4 counts compact rows' lookups as the ops'. Mutation: rows held compact whatever their carries (the fallback dropped) fails both. Every table's digest over 13 asm programs, whole-run and windowed in eight configurations (the cuts at the finish included), is the build's without this (455 digests, fixed trace hash; a probe, not kept).
`kept rest ecsm` and a walked window's lists counted ECSM ops at their inline size, so the double/add steps every witness holds (one Vec of ECDAS steps a call, ~768 KiB at 200 Mgas, ~10 GiB in all there) showed up only as unnamed memory. They now count each op's steps buffer too, and the largest single allocation of the list takes it into account. Logging only; the tables are unchanged.
… byte-identical) collect_ecsm_ops cloned each witness's steps into the ECDAS ops and kept the whole witness, steps included, in the ECSM op for the rest of the run. Nothing reads an ECSM op's steps: its table and its BITWISE lookups read the witness's other fields. The steps are now taken out of the witness and moved into the ECDAS ops, so each call's steps are held once. Tables are unchanged: a test builds a call's ops for six scalars and checks the ECDAS rows against a fresh witness's steps, the ECSM row against the fresh witness, and that the ECSM op keeps no steps.
…yte-identical) The finish built every table of the rest in one parallel scope, so all of p5's allocations landed together (T200-R: +40.3 GiB in one step at gen_decode), and the layout took the rest only once the whole of it existed. The finish now plans the rest as units in AIR order (a job a table, or a streamed chunk's slot; each family's ops held by its jobs alone and freed with the last) and streams them: waves of at most half the gate's budget are built in parallel and handed on in order from the builder thread. A byte gate (BLOCK_REST_LAYOUT_BYTES) holds each table's bytes from before it is built until the packer places it; the lowest table not yet placed always passes, so a budget under one table cannot deadlock, and a job's error or a stopped packer stops every waiter. The layout thread builds the run's AIRs from the header the finish sends first, takes each table as it comes (checked to be the next AIR in order, of that AIR's width, every AIR reached) and lays it out narrow; the packer places the rest as it comes, after the streamed chunks, as before. The tables, their order and the groups are the same. LAMBDA_VM_BLOCK_FINISH_STREAM=0 keeps the monolithic finish (the A arm); the epochs, the continuations and the inline path keep it always. Tests: the stream is the monolithic finish table for table, in AIR order with every streamed slot, in every windowed configuration the block uses, at budgets of one byte, 2 GiB and none; the streamed tables are the header's AIRs' widths; a one-byte budget completes; a job's error and a stopped packer stop the stream and every waiter within a timeout; a miscounted header is refused before a table is handed on; the layout refuses a table out of order, of the wrong width, past the AIRs or missing. Mutations caught: the lowest-pending rule removed, two units swapped, a chunk range off by one, the width check removed, the gate not stopped on an error.
…entical) The BRANCH segment is the builder's largest list (2.44 GiB at p90, 5.70 at 200 Mgas, 32 bytes an op) and lives until its tables are built. It is now kept as a stream: a flags byte and three zigzag LEB128 varints an op (the pc from the previous op's, the offset, the register the cheapest of as-is / from the previous op's register / from the op's own pc), in 64 MiB blocks never reallocated, with a sparse index every 4096 ops so any range expands on its own (as CompactLt). Every op takes at most 31 bytes whatever its values, so it is lossless with no raw form. The finish reads it as a compact segment: p4 counts its lookups range by range, the tables expand each chunk as it is built. Tests: any range, across the index and across small blocks, expands to the ops pushed, fields at both ends of u64 / i64 included; the worst op round trips at 31 bytes and a common one takes a few; the BRANCH table of the expanded ops is the table of the ops. The finish's oracle and stream tests pass on it. The digest probe is identical against b0f8c68 (455 and 351 table-set digests). Mutations caught: the register codings swapped on decode (the round trip fails, 35 of 455 probe digests differ); an index mark's pc wrong (the round trip fails).
…c (byte-identical) S3c-BRANCH's stream (varint blocks, a sparse index, any range expanded on its own) moves to `delta::DeltaStream<C>`, generic over a `Codec` that writes each op from the ops before it and keeps that part of them as a state the index records. BRANCH becomes its first codec, with the same coding, so EQ and BYTEWISE can follow with codecs of their own. The index's spacing is a field (4096); a test can make every stream on its thread mark every few ops, so chunks and p4 slices start past index marks. A finish test builds windowed runs with marks every three ops and checks they make the same tables as the default spacing, and a codec test reads chunks of every size around the spacing.
The EQ segment (0.75 GiB at p90, 24 bytes an op) is now a delta stream: a flags byte (invert, and how each operand is coded) and two zigzag varints, `a` as it is or from the previous op's, `b` as it is, from the op's own `a` (equal operands cost a byte) or from the previous op's, each the cheapest. Every op takes at most 21 bytes, so any op is kept losslessly. The finish reads it as a compact segment; p4 counts its lookups range by range. Tests: any range, across the index and small blocks, and chunks of every size around the index's spacing (and at marks every three ops) expand to the ops pushed, operands at both ends of u64 / i64 included; the worst op round trips at 21 bytes and a common one takes three; the EQ table of the expanded ops is the table of the ops.
…e-identical) The BYTEWISE segment (1.03 GiB at p90, 24 bytes an op) is now a delta stream: a flags byte (how each operand is coded, and the opcode when it is under 8; a larger one follows in a byte of its own) and two zigzag varints, `a` as it is or from the previous op's, `b` as it is (a mask), from the op's own `a` or from the previous op's, each the cheapest. Every op takes at most 22 bytes, so any op is kept losslessly. The finish reads it as a compact segment; p4 counts its lookups range by range. Tests: any range, across the index and small blocks, and chunks of every size around the index's spacing (and at marks every three ops) expand to the ops pushed, operands at both ends of u64 / i64 and an opcode past the flags byte included; the worst op round trips at 22 bytes and a byte mask on a small value takes three; the BYTEWISE table of the expanded ops is the table of the ops.
prover/src/lfm/program_budget.rs and prover/src/alloc_purge.rs are #1013's at 82e777c, byte for byte: LAMBDA_VM_TREE_PROGRAM_BUDGET (auto, off or a size; AHEAD = 4) with its ordered streaming emitter, and LAMBDA_VM_TREE_LEVEL_PURGE. block_whir's spill target becomes crate-visible, as the budget's host target. Nothing calls them yet.
Every leaf and node program of the W3 tree is admitted under LAMBDA_VM_TREE_PROGRAM_BUDGET (auto by default, against the spill target) before it is emitted, in prove order. The leaves the budget admits at the statement are emitted beside phase B as before; the rest by four streaming threads in the tree, as it admits them. Each node is admitted on one of the builder's plain emitter threads (an admission never waits on a rayon worker) and emitted on the builder's pool. A prover claims a program as it takes it and lets it go once done with it (a leaf after its proof, a node after its fill), which frees the program and gives its bytes back. The leaves' artifacts are published all at once after the last while every leaf's program is there (today's order: published one by one, ULTRA 101 cost the 1x tree 0.24 s), and each as it is built from the first leaf whose program is not, so the publisher never waits for a program while it holds what the provers need. W3_LEAF_ARTIFACTS_EACH=1 forces per-leaf publication. After a tree level's last proof, LAMBDA_VM_TREE_LEVEL_PURGE may purge the allocator where the host is short. On a host with room every program is admitted by room and the schedule is today's. Programs are functions of the plan and their children's artifacts alone, so no proof byte moves.
…estamp The CPU holds its clock in one column and sends a zero high word on the Memw bus; MEMW_R receives the timestamp as two 32-bit words. Below 2^32 the messages are one; past it only the two timestamp slots differ. The block's clock is 4·cycle + 4 over the whole execution, so a block past 2^30 cycles cannot balance the Memw bus (T200-R, 1.83 G cycles, refused with BusImbalance).
…imestamp) A cycle's timestamp is 4·cycle + 4 over the whole run, and the CPU sends it with a zero high word while the tables it talks to take two 32-bit words. At 2^32 the two encodings part, the buses cannot balance and the proof cannot verify (T200-R, 1.83 G cycles: BusImbalance). The walk now refuses, with Error::ClockPastLimit, the window whose last cycle would reach 2^32 (cycle 2^30 − 1), and the finish refuses a final PC token the last chunk's padding rows would put there. Below the bound nothing changes. LAMBDA_VM_BLOCK_UNVERIFIABLE_CLOCK=1 proves past the bound anyway, for memory and timing measurements, with a warning that the proof will not verify.
…the knob is release-only The REGISTER table's final PC token, halt_timestamp + 4·padding_rows + 1, is the largest timestamp a run's trace holds: the last CPU padding row's PC write. The finish now takes it from clock::final_pc_timestamp, and a test builds a run just under 2^30 cycles whose padding rows cross 2^32: every window fits, the CPU trace's last padded row writes the PC at the final PC token, and that token is refused. LAMBDA_VM_BLOCK_UNVERIFIABLE_CLOCK=1 proves past the bound only in a release build: HALT and HINT debug-assert 32-bit timestamps, so a build with debug assertions refuses instead of proving into them.
…n, ported) A block table dropped after its group's commit leaves a RegenSlot: the shape and the spill store's digest of its packed columns. A regenerator deposits the columns again in phase B; the deposit is checked against the slot, paced by rank from the window's frontier, and every exit of the regenerator settles what it did not deposit. #1013's stark::regen over NarrowColumns, the form a block holds, instead of a trace's NarrowMain. Nothing uses it yet; the proof is unchanged.
…med chunks The walk's one body is generic over whether it lists the ops only the finish reads; without them it is the regeneration walk (#1013's R1), which advances the same state and emits only the streamed tables' lists. RegenBuilder walks a run again from its logs with it and cuts each streamed table's list as the hand-out does, STORE's from the CPU ops as the routing filters it, in the hand-out's order within a window. Fed phase A's windows it rebuilds phase A's chunks in phase A's order. Accumulator::absorb_counted reports the ops a window added to each streamed list, for a recorder. Nothing in the prove calls them yet.
…off by default LAMBDA_VM_BLOCK_REGEN=shadow: phase A records a recipe per streamed chunk (its chunk, the windows it spans, its place in the hand-out, the spill store's digest of its packed columns taken on the layout thread that generated them), and phase B runs #1013's sequential regenerator beside the prove on threads of its own: a fresh execution, the regeneration walk, the slicer and generators writing packed, each chunk checked against its recipe and dropped. Nothing it builds reaches the proof. It reports mismatches, failures and its CPU, and plans the chunks against phase B's groups as they ran: in group order, and with the groups that hold no streamed chunk first (each group's phase-B span is now stamped). Any other value of the knob is an error; a mismatch is a report entry, never a panic. The shadow records nothing where phase A streams chunks the regenerator does not cut (KECCAK_RND, the MEMW-derived LT ops) or generates them 64-bit.
…entical) block_prove_in_order proves the groups in a given permutation: each group proves on its own fork S_post ‖ g and nothing one group proves enters another's transcript, so each group's share is the same in any order; the shares are assembled in group order, the next group in the order is restored and uploaded beside this one's argue, and spilled tables are read back in phase B's order. block_prove_on_forks_observed is the group order; rebuilt_last orders the groups whose columns phase B rebuilds last. A test proves reversed and interleaved orders (spilled too) to the group order's bytes; an order that is not a permutation is refused.
…, off by default LAMBDA_VM_BLOCK_REGEN=auto|always: phase A drops a streamed chunk after its group's commit instead of keeping or spilling it — its packed columns leave after the spill store's digest, on a drop thread, and a RegenSlot stands in the parked table — and phase B's regenerator (#1013's run_live: a fresh execution, the regeneration walk, generators writing packed) deposits each into its slot, paced by rank from the window's frontier. A table's group waits on its slot before its upload; a deposit that is not the dropped columns refuses the table there, and the kept tree top's check stands behind the digest. Phase B takes the rebuilt groups last, in rank order, so the regenerator has the rest's phase B as a head start; any other order of them is refused. auto arms on the policy's first wish to move a table off the host, or at the walk's hand-off: every parked droppable chunk is dropped back and every later one dropped; always drops every one (the identity test mode). With the spill off, auto still decides with no store: no disk, what cannot be rebuilt stays on the host. A block that never arms drops nothing and starts no regenerator. Every exit of the regenerator settles its slots, and the prove's end closes its window. The proof is unchanged.
Phase B proves the rest's groups first, and the regenerator, held to a 4 GiB window ahead of the frontier, idled through that head and then ran at parity with phase B: at T200-R its takers waited 2.97 s (RYZEN 049). With 16 or 32 GiB they waited 0.0 s (RYZEN 052) while the run's peak, set in phase A, did not move. The window is now adaptive when LAMBDA_VM_BLOCK_REGEN_AHEAD_GIB is unset: a pacer beside the regenerator reads VmHWM and VmRSS every 250 ms and sets it to VmHWM - (VmRSS - parked) - 4 GiB, clamped to [4, 16] GiB. Above the floor it holds only memory the run has already reached, so it cannot raise the peak. RegenWindow::set_ahead resizes a window under its lock: a larger one admits the depositors it held, a smaller one holds the next deposits. The knob still fixes the window. Regeneration stays off by default.
An oscillating adaptive window is a finding even when phase B never waits: the BLOCK REGEN window pacer line now says how many times the pacer grew and shrank the window.
…own churn At p90 with no disk the adaptive window shrank 109 times and grew 28 in 455 readings (RYZEN 057). Its reading, VmHWM - (VmRSS - parked) - 4 GiB, churns with every chunk deposited or taken, whose pages the allocator keeps, and drifts as phase B's resident set grows. The pacer now takes the reading rounded down to whole GiB, and only once the reading is a GiB or more away from the window either way. The window stays under a step above the reading, so the run's peak less 3 GiB is still never passed, and churn inside a step moves nothing.
…lock alloc_purge.rs is #1013's at 07931f4, byte for byte: LAMBDA_VM_ALLOC_WATERMARK (auto by default) runs one monitor thread for the block. Every 0.5 s it reads VmRSS, and once the block's memory is short, VmRSS has reached 90 % of the host target and the allocator holds at least 4 GiB of freed pages, it purges every arena, at most once per 5 s. Under off it only samples, for the ALLOC PEAK lines. prove_whir_block_tree starts it against the block's spill target and prints its end line after W3 RECURSION. A host with room never fires it (#1013: RYZEN 053, 0 fires at 1x, the median and p90 on 128 GiB).
…he's live bytes The W3 driver prints one ALLOC PEAK line for the base and for each tree level at its last proof: the watermark monitor's highest-VmRSS reading of the window, with jemalloc's allocated and resident bytes at it, and the precomputed-tree cache's live node bytes (a new reading in the stark crate: inserts add, the cap's evictions remove), as #1013's block tree does (507e098). Measurement only.
…host target program_budget.rs is #1013's at 07931f4, byte for byte: auto admits a tree program by room only while VmRSS plus the programs not yet emitted stays under a share of the target (ROOM_SHARE 0.75; knob LAMBDA_VM_TREE_PROGRAM_BUDGET_SHARE, 1.0 is the line at the target, the budget before). Above the line, programs come in by the AHEAD rule alone, so what the allocator's watermark (at 0.9 of the target) returns is not spent again on programs held ahead (#1013: RYZEN 050 against 053). The W3 driver passes the share with its spill target; a nonsense share is an error.
… block) LFM_PRECOMPUTED_TREE_CACHE_CAP, when the environment leaves it unset, is set by the CLI's posture from the host target (block_whir's spill target): 64 entries (about 6.2 GiB once full) from a 64 GiB target up, 16 below it, as #1013's CLI does (49c4bb5). A miss only rebuilds a tree whose root is the key, so nothing moves in a proof. The BLOCK POSTURE line compares the knob against the same rule, and a note says when the posture set 16.
…second after a fire that returned little The trigger read jemalloc's resident − allocated, which also counts the free space inside active pages that a purge cannot return. At the median on a 32 GiB emulated host a fire read that gap at 4 GiB or more and returned nothing (VmRSS 25.52 → 25.50 GiB), and its 5 s spacing then held the next fire past level 1's peak (29.16 GiB, RYZEN 058b). The trigger now reads resident − active (dirty pages and metadata). A fire that returned at least 1 GiB starts the 5 s spacing; one that returned less lets the next come no sooner than 1 s later, so purges that find little cannot spin (each takes every arena's lock). The fire line and the ALLOC PEAK lines print jemalloc's active bytes and what was purgeable.
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.