WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 43.85 s - #1010
Draft
MauroToscano wants to merge 1117 commits into
Draft
MauroToscano wants to merge 1117 commits into
MauroToscano wants to merge 1117 commits into
Conversation
…ready named it The WHIR base prints one number for fifteen epochs - 57% of the block's wall with nothing under it - and there is not a timer, span or print between `multilinear_continuation::prove_continuation` and the bottom of the chain. Every optimisation round so far has moved that number without anyone being able to say which part of it moved. The knob is not new. The LFM tree launcher has exported `LAMBDA_VM_BASE_SPLIT=1` on the WHIR arm since that arm existed, 'byte identical to the D-S exports', and it reached nothing: the WHIR base does not go through `continuation::prove_continuation`, where the STARK instrument lives. An inert knob printed as if it mattered is worse than a missing one, because the export is the evidence a reader uses to believe the breakdown was taken. The same name now means the same thing on both pipelines, in the same line format. The stages partition their own thread's wall: execute/collect/build/ handoff on the producer, prep/absorb/commit/prove on the prover, and challenge/argue/open_groups/open_prepared inside the argument. The two threads run concurrently, so their sums must never be added - what the pair says is which of them set the wall, and `handoff` is the one stage that can answer it, being a blocking send on an unbuffered channel. `check_closure` is a pure function over the records, so the arms can be fed manufactured omissions rather than only whatever a real run produces: a missing prover stage reddens arm A naming the epoch, a missing inner slot reddens arm B (the four stages still close without it), a missing producer stage reddens arm C, and a zeroed tolerance reddens a run carrying real timer cost. It deliberately does not assert that the two sums equal the base wall; that identity is false on a correct instrument and a check that reddens honestly gets widened until it cannot fail. Cost when off: `mark` returns None and no clock is read. Two defects the wiring itself surfaced. `prove_epoch` receives `label`, not the epoch index, and `epoch_label(i) = i + 1` - keying the prover records on it would have joined the producer's epoch 0 to the prover's epoch 1 across the whole table. And a committed table carries no name, so the argument can only see an index; the names are sent down from the layer that holds the AIRs.
…ly the production one The read-back landed in the production WHIR tree arm's base window, which is the arm that needs a block ELF, a census and a card. The gate that is supposed to prove the instrument closes cannot afford that arm, and ran the production one by name: it refused in 0.00s with its own guard - 'LFM_CENSUS_ELF must name a file: this composes the PRODUCTION WHIR tree, and a silent fixture fallback would report a fixture number under a production name' - which is the harness being right and the gate being wrong. An instrument checked only in the arm nothing can afford is an instrument nothing gates. The fixture arm keeps its own base window, so this is the same call in the second place rather than a shared helper growing a caller. The base wall is taken where the base ends, not recomputed lower down: `t_all` runs for the whole tree, so a second `elapsed()` would hand the split a denominator including level 0 and the interior, and every stage's share would read far too small.
…n it `open_groups` is 43.8% of the WHIR base and 24.9% of the block's whole wall, and wt12 printed it as one number. These six resolve the round loop: the three 20-bit grinds, the opening sumcheck, the fold, the fresh successor commit, the out-of-domain block, and the query openings that rebuild the tree on device per batch. Six and not the four the round obviously has: `factors.rounds` and the out-of-domain block are neither grind nor fold nor commit nor query, and leaving them out would have made the closure arm redden on a correct instrument - which is how a tolerance gets widened until it cannot fail. Arm E asserts the six close `open_groups` per record, and it caught two real defects in this instrument before either reached a block run. The first: the slots are process-global, and reading them at the window's close alone attributes to this group loop whatever ran the chain earlier in the process. They are now cleared at the window's OPEN, so 'the group openings only' is a property of the window and not an assumption about callers. The second: the out-of-domain window spanned its own grind, and the grind was separately added to GRIND - so that time was counted twice and the six summed to MORE than the wall containing them. Slots that partition must not nest; the two out-of-domain windows now abut the grind instead. The fix is visible in the slot that moved: ood 3.83s -> 0.04s. A negative remainder is therefore not drift. It means the parts are not parts, and it has two causes - a window that is too wide, and windows that overlap. The message says so rather than reporting a percentage. The prepared opening keeps its wall and no breakdown: it is 2.5% of the base, and six more fields would not move a ranking. The success line names arms A-E, because a line that under-names what it checked reads exactly like a check that never ran.
…e posture in the pin's identity Runs lb17 and lb18 measured the transcript pins at two tips of this lineage and read the same four deltas at both: +77 absorbs, +200 squeezes and +17 states on BOTH sides, and one device commit the model did not account for. The pins had not actually been measured on this lineage since V3's tip -- the "unmoved" readings from W1h's v4/v5 gate were greps matching the tuples the two should_panic tests print, which appear on any machine and touch no guest -- so the move is the lineage's, not any one commit's. An A/B across the two tips read identical counters, which is what says so. Two causes, both now derived rather than re-measured. THE POSTURE. The constants were taken with LAMBDA_VM_MAX_ROWS_LOG2 unset, where MaxRowsConfig::default returns the production per-table caps and an epoch carries 34 tables; every run of record is at the uniform 2^21, where the same block's epoch carries 27. pin_applies took the sha, the length and the epoch size, so a run at a posture nobody pinned was the pinned configuration by the pin's own identity. The cap is now part of that identity, read through max_rows_log2_override -- extracted out of MaxRowsConfig::default so the posture the pin checks is by construction the posture the epochs were chunked at -- and the bases are the record posture's, measured at 892c7d1. A run at any other cap skips and names both caps; another posture is not a defect, it is a different measurement. This held on the ladder branch only; this commit is what makes it true on this lineage. THE STACK. The stacked INIT polynomial of the dense genesis pages entered the cross-epoch statement after the pin's constants were taken. Its cost is now a function of the plan the run used -- read through the verifier's own global_airs_for(..).genesis_stack(), so no threshold is re-decided here -- and of the chain config that proof argues at: absorbs one root per stacked polynomial in the cross-epoch roots block, one claimed value per stacked column, then the chain squeezes the batching challenge, then the chain's own draws states 3R - 1: three grinds a round, with no out-of-domain one on the last At the block's six columns of 2^18 -- one stacked polynomial at n_stack 21, six rounds at fold width four -- that is 1 + 6 + 70 = 77, 1 + 199 = 200 and 17, which are the measured deltas exactly. A run with no dense page adds nothing, and the unit pin evaluates the same form at n_stack 19 as well so a wrong term cannot be flat across both shapes. The stack costs the run once and not once per epoch, and it moves both sides equally: it lives in the cross-epoch proof, which has no `owed` replay, so unlike DECODE's derived root it is absorbed once on each side and owed is unmoved. The measurement confirms that at 160 = 145 + 15 absorbs and 30 = 2 x 15 squeezes. THE DEVICE COMMIT. commits() walked a flat list of proofs, so the stack's five fold commits were picked up the moment it landed while its held commitment was not: the held term was a find_map, which stops at the first proof carrying a prepared opening, and the epoch proofs come first in the list the bench builds. The two held commitments have different scopes -- DECODE's is a function of the ELF and is held across every epoch, the stack's is built once per prove_global call and belongs to that one proof -- so they are now two arguments and two terms, and neither can be inferred from slice order. 1106 + 80 + 2 = 1188, which is the counter's reading. The carried bases compose with the derived terms onto the lb17/lb18 measurement on all six numbers with no residue, which is what makes carrying them a verified move rather than a new literal; the arithmetic is written out in the doc comment. owed's carried half is no longer only a constant either: it is checked against the run's own proofs -- the sum of roots.len() over the bundle's fifteen epochs, one root per chain -- so a posture that moves the chain count reddens by name instead of arriving as "the counts moved". Also: make lint gains a TENTH step. Everything under cfg(all(cuda, hash-metrics)) -- check_device_pins and transcript_pin::commits, which is the whole device-commit model -- was compiled by no pass in the matrix: the cuda pass carries no hash-metrics and both hash-metrics passes carry no cuda, so a box run was that code's first compiler. From this sha the lineage's lint is ten steps run separately, not nine, and the tenth needs no GPU.
… lint step needs the parity allow
Two fixes to the commit before this one, both found by running the gate rather
than by reading it.
then_some. `global_stack` built its Option with `.then(|| StackShape { .. })` on
a struct literal with no side effects, which `clippy::unnecessary_lazy_evaluations`
rejects under -D warnings. Lint step 9 caught it; the commit before this one had
been made with that step red, because the gate script committed unconditionally
between the test run and the mutations. The script now refuses to commit while
any step above it is red -- a script that commits on a red is the same class of
defect as a gate whose verdict is not read.
The tenth lint step. It was added without `-A clippy::op_ref`, which every one
of the other nine carries; without it the step reports 156 op_ref errors from
code the workspace writes that way by design, so it was a step that could not go
green on any sha. The line is now
cargo clippy -p lambda-vm-prover --all-targets --features cuda,hash-metrics -- -D warnings -A clippy::op_ref
and with it the step reads exit 0 with zero error lines, which is what makes the
device pin's cfg(all(cuda, hash-metrics)) code covered rather than merely
mentioned. From this sha the lineage's lint is ten steps run separately.
One finding recorded and NOT fixed here, because it is outside this lane: a
clippy pass with --all-features -- a posture the Makefile's matrix never runs --
fails on crypto/stark/src/prover.rs:1544, `too_many_arguments` (8/7) on
`commit_main_trace`. Nothing in this branch touches that file.
The six chain slots closed to +1.4% on the laptop and +5.1% on the box's card-free fixture. Widening the tolerance to admit 5% would have made the arm unable to fail, and it would have been wrong about the cause. The cause is not the round loop's bookkeeping. `Factors::from_shares` runs in `prove_shared`, and `stacked_eval::prove` builds the weights and the stacked polys, all inside `open_groups` and outside the round loop entirely; `config.schedule` and `domain.clone()` sit before the first round. That is a setup phase - the same class of miss as the out-of-domain grind - and it is roughly fixed per epoch, so its share grows as the window shrinks on a faster machine. So the loop's own wall is measured, and what was one unattributed gap becomes two NAMED terms: `round_other` is the loop's bookkeeping between windows, `setup_tail` is everything outside the loop. The reading says which owns the gap rather than a comment asserting it. On the fixture it is unambiguous: round_other 0.00 on every record, setup_tail 0.20 / 0.17 / 0.16 / 0.01. Arm E had to change with it. `Sigma(six) + round_other + setup_tail = open_groups` is an IDENTITY once the wall is measured - the remainders are defined as the differences - so asserting it would be a check that cannot fail. It now asserts what can: both remainders NON-NEGATIVE. A negative one is not drift; it means the parts are not parts, and the two bounds separate the two causes - the six overlapping or escaping the loop, and the loop escaping the opening. Those are the shapes the two real defects took. A slot merely reading small is therefore a READING, not an error: its time lands in a named remainder. One unit case exists to assert the arm does NOT redden there, so it cannot drift back into asserting an identity.
The seventh slot fixed a false red and removed the check's power to see a missing timer. Asserting only that the two remainders are non-negative meant an omitted slot shrank Sigma(six), so round_other = round_wall - Sigma(six) GREW - positive, allowed, invisible. The gate proved it: the mutation arm E caught before the round wall existed sailed straight through after it. The identity was never the thing to remove; ASSERTING the identity was. round_other is the loop's own bookkeeping and reads 0.00 on every record of a correct instrument, so an upper bound at 3% of the loop's wall is enormous headroom honestly and trips on any omitted slot above it. setup_tail keeps >= 0 only: it is legitimately un-slotted work outside the loop, and bounding it would assert a size nobody measured. Two more defects surfaced while fixing it, both from the unit run rather than from reasoning. The honest() fixture carried a 5.9% remainder and tripped the very bound it was written to test. A fixture that is not itself a correct instrument makes every arm built on it meaningless, so the wall now models what real records show: Sigma(six) plus a hair. And the checks ran in the wrong order. A loop wall that escapes its opening also leaves a large positive round_other, so with the accounting check first it was reported as 'a slot is not being added' - the wrong defect, named confidently. Containment is checked before arithmetic. The new unit case has a twin that must NOT redden: a slot genuinely small, where the wall shrinks with it. Without it, queries reading 0.00 on any card-free fixture would become a permanent red and the next lane would widen the bound to silence it.
…ck, the cap in the pin's identity, the tenth lint step
…t it is not `LAMBDA_VM_GRIND_SCAN_FACTOR` (default 8 — the record posture, unmoved) replaces the literal 8 at the one site that sizes a device grind's launch block. Read once per process through a `OnceLock`, refused outside 1..=64 with the offending value named, and printed as `★ GRIND SCAN FACTOR: n` on the first device grind, so a log that quotes the factor can be shown to have read it rather than assumed it. ⛔ The knob is NOT the lever it was ruled to be, and the doc comment now says why. Both grind kernels carry `if (nonce >= *result) break;` against a `volatile` result the `atomicMin` writes through L2, and the stride walk gives every nonce in `[base, base+count)` exactly one owner — so the scan stops at the first hit. The permutations executed are `h + stride` whatever the block size, and the launches before the hitting one cover exactly the part of `[0, h)` below it. The factor buys only the probability that one launch suffices, `1 - e^-k`. Lowering it removes no permutations (they were never executed) and adds `1/(1 - e^-k)` expected round trips. The same reading says the returned nonce is the globally smallest valid one at any factor — which `tests/grinding.rs::gpu_grind_returns_smallest_valid_nonce` already pins — so sweeping the knob moves no proof byte. `prover/tests/rpx_grind_bench.rs` is the arm that settles this on the card in seconds rather than in four tree runs: ms/grind and the full nonce list at one scan factor per process. Flat means the block is a ceiling; halving means the scan dominates; an identical nonce list across the arms is the byte control.
…ead off the driver
`LAMBDA_VM_GRIND_GRID` joins `LAMBDA_VM_GRIND_SCAN_FACTOR` in one module, both
read once, both defaulting to today's exact values (8 and 1024) so the record
posture is byte-unchanged. ONE line prints both AND the stride each arm gets —
`★ GRIND KNOBS: scan 8 · grid 1024 · stride rpx 131072 / keccak 262144` — because
the stride is the mechanism and a reader should not have to multiply it back
out. The two block dims stay constants: they are tuned per kernel against
register pressure, which belongs to the kernel body, and moving them would
change what an occupancy reading means.
Why the GRID is the candidate lever now that the scan factor is not. The
kernels stop at the first hit, so a search executes `h + stride` permutations
and `stride = grid × block_dim` is the term left behind — the overshoot is
`stride/h`, 12.5% at the default. That gives the knob two opposite edges: while
the card is not filled a wider grid raises throughput faster than overshoot,
and once it is filled the surplus blocks only queue and the wider stride is
pure added work. The sweep therefore has to run BOTH ways.
`device_fill()` answers which edge the default sits on by READING the driver —
SM count, max threads per SM, the kernel's registers per thread, and the
occupancy the driver will actually grant — instead of estimating residency from
a block dim. A grid above the resident-block ceiling buys no parallelism.
`search` now takes its knobs as a parameter, so `generate_nonce_{gpu,rpx_gpu}_at`
can sweep them inside ONE process. That is not a convenience: the knobs cache in
a `OnceLock`, so comparing settings through the environment would need a process
per arm, and four processes are four device contexts, four cubin loads and four
clock domains compared across an exponential spread of hit distances. Paired
arms on identical seeds make the ratios exact instead.
`prover/tests/rpx_grind_bench.rs` runs the nine arms that way — scan 8/4/2/1 at
grid 1024 and grid 256/512/1024/2048/4096 at scan 8, the 8/1024 arm shared — over
256 seeds at the production factor, reporting mean, median and `ns/perm`. The
nonce IS the hit distance, so the permutations a launch executed are known
exactly and `ns/perm` is the seed-independent throughput the grid question turns
on. Three controls travel with it: the environment path is exercised and
asserted to agree with the explicit one, every arm's nonce list must be
identical, and the measured ms/grind is projected over the base's 3,428 grinds
against the window wt14 read (15.73-18.03 s) and reported in or out.
`crypto/math-cuda/tests/grinding.rs` gains the card-side twin: the nonce is the
same, and still the smallest, at every scan factor and every grid.
…anism The first run read a monotone fall down the scan column — ratios of 1.000, 0.953, 0.872 and 0.800 at scan factors 8, 4, 2 and 1 — which the kernels say cannot exist. Both stop at the first hit, so the executed permutations are `h + stride` whatever the block size, and for the median seed, whose hit falls inside even the narrowest block here, the two launches are the same kernel doing the same rounds. There is nothing for the knob to change. The arms ran in one fixed order in one process, so that fall is confounded with drift. Pairing on seeds cancels the seed spread; it does not cancel a boosting clock. Four changes to the procedure, none to the measurement: Every seed now runs every arm in a rotating order, so each arm sits in every position of the rotation equally often and drift pairs out too. The control is repeated as a final arm with identical knobs: its ratio is the noise floor, measured rather than assumed, and no arm may claim less than it. Statistics are per-seed and paired — the median of the per-seed ratios and the count of seeds the arm actually beat, because a real twenty percent shows on most of 256 seeds while drift shows as a trend a rotation destroys. And the combined arms run, in case the two effects are real and additive. ★ The split that can falsify a mechanism. The returned nonce IS the hit distance, so every seed can be labelled by whether its hit fell inside the arm's block. Seeds inside take one launch and run the identical kernel at every arm, so no knob can touch them; seeds outside are the only ones that miss and relaunch. An arm whose gain is the same on both groups is not the knob, it is the procedure. A gain living only in the outside group is a real miss-path effect and owes a mechanism from the kernel before it is priced.
… survives a zero QUERIES is the largest slot in the WHIR chain and, like `open_groups` before it, one number. Four slots partition it — `QUERY_SAMPLE`, `TREE_REBUILD`, `COSET_GATHER`, `OPEN_ASSEMBLE` — counted on EVERY `open_many` call, which is twice per non-final round because `whir_round::prove` opens the current commitment and its successor, and once in the final round. ⛔ The boundary is `open_many`, not `paths()`. On the device arm `paths()` is a range check, ONE device call and a `map` into `Proof`, so splitting inside it would weigh the rebuild against host bookkeeping over a hundred kilobyte-sized paths and read ~100% every time. What competes with the rebuild is the coset gather, which sits beside `paths()` rather than inside it and would otherwise stay in QUERIES as an unnamed remainder — the same shape as the setup gap the seventh slot was added to name. `queries_other` is bounded above as well as below, and the bound carries an ABSOLUTE allowance beside the relative one. Card-free the fixture's query openings read 0.00 s, and three percent of two milliseconds is below the glue between the windows and below the clock itself, so a purely relative bound would fire on the honest path at the shape the gate actually runs. ★ Arm F is the arm that survives that shape: `rebuild_calls` must equal `2·round_count − chain_count`, every term counted by the run rather than read off the source. The durations vanish card-free; the calls do not. ⛔ And the term is CHAINS, not groups. `stacked_eval::prove` runs one chain per COMMITMENT in the stacked commitment, so a group can open several, and an identity written over groups would have been red on the honest path the first time one did. Its guard is "any of the three counters is nonzero" rather than "the rounds are", because guarding on the rounds alone makes a dropped ROUND counter invisible — the same blind spot the seventh slot opened in arm E. The harness sums the four over the epoch records and prints `tree_rebuild`'s SHARE of the query openings, which is round 3's kill condition: retention removes the rebuilds and nothing else, so if they are not the bulk of QUERIES the lever is dead before any lifetime code is written. The closure line now names arms A-F, because a line that under-names what it checked reads exactly like a check that never ran. ★ The new arm found a defect in the existing fixture on its first run: the "must NOT redden" twin zeroed the QUERIES slot while leaving the four inside it at their honest values, which models four parts summing to more than their whole. The fixture was wrong, not the bound.
…es the mean ⛔ The launcher read the repeated control's ratio by COLUMN POSITION, and that arm's label is two words, so it read the throughput column instead. It reported the procedure as 327% unstable on a run whose ratio column read 1.000 — a check that could not pass, in a script that reads every other verdict by name. The fix is not a better column index. The bench now prints the floor on its own named line, so nothing downstream has to count spaces to find the truth. And two readings the means still owe. The per-seed median ratios are flat while the means fall, which is a statement about a distribution, so the distribution is now printed: the deciles of the per-seed ratio per arm, and the twenty seeds that move the mean most against the control. Each of those twenty carries its hit distance and its launch count at both arms. The launch count is DERIVED rather than instrumented — the search advances its base by one block per miss and returns on the block containing the hit, so the count is the hit distance over the block plus one, exactly. It is the only quantity that differs between two arms for one seed, which makes it the discriminator: if the twenty are the largest-hit-distance seeds and their launch counts exceed one, the effect lives in the miss-and-relaunch path or in what a long sustained launch costs under the board power limiter, and the card drew its full power on that run. If they are ordinary seeds, neither survives.
…nd is the only thing left v4's top-20 killed three of the four candidates for the tail effect. The seeds that move the mean are SMALL-h (258k-512k, inside 2^20), take ONE launch at both arms, and it is the CONTROL that is slow by 5-11 ms while scan 1 costs what `h + stride` predicts. That rules out the power limiter (these are not the long sustained launches), the miss-and-relaunch path (one launch either way) and the volatile load's per-iteration cost (the same iterations either way). What is left is readable from the code. For a one-launch seed `search` does nothing that scales with `count` — one 8-byte sentinel, a launch at a grid the knob fixes, 8 bytes back, a synchronize — and inside the kernel `count` reaches exactly one thing, the loop bound `i < count`. Work is `h + stride` ONLY IF the early exit stops every thread; a thread that never observes the atomicMin runs to `count` and wastes in proportion to it. So sweep the knob UP instead of down. Scan 16, 32 and 64 join the arms, and the new COUNT SLOPE section prints each arm's excess over the tightest cap in the sweep, normalised to the control, BESIDE its prediction (k-1)/7. Count-bound reads 2.14 / 4.43 / 9.00 at k = 16 / 32 / 64; saturated reads ~1.00 from k = 8 up. The two branches are a factor of eight apart at k = 64, which no clock ramp, thermal drift, ordering or seed spread produces. The grid pair is run at BOTH caps (grid 4096 at scan 8 and at scan 1) so the same defect can be tested from the block-count side: if wide grids make stragglers worse by contending the atomicMin's line, a tight `count` should mask it. Equal damage at both caps refuses that unification. The verdict is printed on a named line and the section is read by its name, not by column position or section order: `scan 64` also begins a row in THE ARMS and in the DECILE tables, so the launcher anchors the read to the COUNT SLOPE section itself. That is v3's lesson, which cost this file a noise floor that could not pass. No default moves. Scan 16/32/64 exist to make waste visible by exaggerating it and are candidates for nothing; the record posture stays scan 8 / grid 1024. This measures wasted work, never a wrong answer: the nonce control asserts all twelve arms return identical nonce lists before any timing is read.
Stage A swept the scan factor upward and killed the last timing-only hypothesis: threads do not run to the loop bound. The excess saturates above count = 2^23 instead of growing with it, reading 1.05 at scan 16, 32 and 64 against a prediction of 2.14, 4.43 and 9.00. It does not saturate immediately either. In iterations per thread the excess fits T·(1 - e^(-(N-8)/tau)) with T = 1.06 ms and tau = 19 on three independent points, which is the shape of a thread scanning for a bounded TIME after the answer is known rather than to a bound. One iteration at grid 1024 is 131,072 permutations, about 0.56 ms, so 19 iterations is about 10.6 ms -- where the earlier top movers sat. That is a fit, not a reading, and this commit replaces it with a reading. `rpx_grind_search_counted` is the shipped search with three device counters: the permutations its threads ran, the deepest thread's iteration count, and how many threads left by the loop bound rather than by the early exit. So executed - (h + stride) becomes a number per search. The counters reduce inside the warp and hit memory four times a warp rather than once a thread -- 131,072 serialised updates of one L2 line would be the same order as the effect under measurement, and an instrument that manufactures its own signal answers a different question. The twin is device-only. The host KAT compiles this file through a shim that supplies gridDim, blockDim and atomicMin but not the shuffle, and a KAT has no answer to check for a kernel that produces no digest. Its agreement with the shipped kernel is asserted instead where it can be: on the device, seed by seed, on the nonce. Nothing on a proving path launches it, no default moves, and the shipped kernel is not touched. The bench pairs every counted search with a shipped one on the same seed and refuses to draw a conclusion from any arm where the two disagree on milliseconds beyond the noise floor -- a counted kernel with different register pressure has different occupancy and measures a different kernel. Both branches are written into the file before the run: a stale poll means real extra permutations, bounded by time and therefore the same at scan 8 and scan 64, with ran_to_end near zero at scan 64 and nonzero at scan 1; no overrun means the slow launches run the same permutations more slowly and the cost is outside this loop. The cross-arm verdict is computed and named in the test, not left for the log's reader. Sized before the first cubin, by this file's own rule: one more call site for `permute`, not one more inlined copy, so the entry is of order 150-250 PTX lines against a file of 6,241. The shuffles take `unsigned long long` rather than `uint64_t` because the intrinsics have no overload for `unsigned long`.
H4 kept the whole Merkle node array so an opening would not re-hash the leaves, measured it on the card, and lost about 15 s: the retention is one object per commitment IN THE GROUP, because every chain's commitment is built before any query index is drawn, and ten of those put the device at 96% -- after which allocations fail, commits fall back to the host, and the host grows about 1.5 GiB per fallen-back chain. That finding stands and is not edited away. What changes is which object. A tree is 2*num_leaves - 1 nodes; its leaf layer is num_leaves of them, half the bytes -- C * 2^(5-k) at fold width k, a quarter of a base codeword at the production k = 4 where H4 held half of one. And the leaf pass is the expensive part: a leaf absorbs a whole 2^k coset, two permutations on a base codeword and six on an extension one, against one per inner node. So the layer carries two thirds of a base tree's work and six sevenths of an extension tree's, and rebuilding the inner levels from it is the cheap third. Half the memory for most of the saving is a different trade from the one H4 measured. It can also decline, which H4 could not. The capture asks DeviceReservation::grow -- which already existed, unused, with a doc comment describing exactly this case -- and a refusal costs one leaf pass and nothing else, the behaviour of this file before the change. Allocate, then promise, then give the promise back if the allocation failed, so neither direction leaks. The commit cannot fail because of the cache, so commit_stacked's device attempt cannot start returning None, so the fallback cliff is unreachable rather than unmeasured. The key is part of the object. A leaf is the 2^log_folding coset that folds onto one position, so a layer is valid only for the width it was built at and the hash that built it; paths() takes the width as a parameter and the cache test opens one codeword at two widths on purpose. Served across widths this would hand back authentication paths that are internally consistent and wrong. The predicate is a free function so it takes unit cases on a machine with no device -- it is the one part of this whose failure is not slowness. Counters diverge where they used to agree: tree_builds counts trees assembled, leaf_hash_calls counts passes actually paid, and the two together assert the retention in both directions. The group-scale memory test is now two-sided against the form -- the layers must be held, and a whole tree must still never be -- where the old one-sided bound sat on its own edge. The base split prints admitted against refused retentions on every run, including the runs that retain nothing, because a refusal path that is silent is indistinguishable from a lever that never fired. No proof byte moves: the same leaves give the same tree, the same root and the same paths.
…issed `executed - ideal` came back NEGATIVE on the two arms where searches miss -- scan 1 read -4.17 strides -- and an overrun is not a quantity that can be negative. The cause is the model, not the counters. `ideal` added `(launches - 1) * block` on the reasoning that a missed block costs its whole `count`. It does, but `nonce` is ABSOLUTE: those nonces are already inside it, so the term counted them twice. The model is `nonce + stride`, full stop -- every nonce below the hit, plus one stride round for the threads that were mid-permutation when it landed. Scan 8 and scan 64 are untouched, because at those block sizes every seed in this bench hits on its first launch and the extra term was zero. Those are the two arms the verdict is written over, so the stage-B reading stands: the overrun is the same at both, and `ran_to_end` is 0 at scan 64.
`the_process_wide_counter_tracks_the_same_passes` asserted that a tree and a leaf pass are the same event -- `tree_builds() == leaf_hash_calls()`, and that an opening moves the global counter by one. With the leaf layer retained they are no longer the same event by design, so this test would have reddened on the box for the one reason the gate was not looking for: an invariant that expired when the code under it changed, in a file whose other tests were rewritten and this one was not. It now asserts the relationship that replaced it, in deltas because the three counters are process-wide and diverge on purpose: a commit assembles one tree and pays one pass; an opening assembles a tree and pays NOTHING, recording one saving instead; and over any window, trees == passes + savings. That identity fails in both directions -- a tree that skipped its pass without recording a saving breaks it, and so does a saving recorded for a tree never assembled -- where the old equality could only fail in one.
`run_grind` declared its result `uint64_t` and handed the address to the kernel as `volatile unsigned long long *`. Those are the same type on Darwin/arm64 and different types of the same width on LP64 glibc, so on Linux the cast type-punned; with `#include "rpx.cu"` putting the whole kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to assume a write through `unsigned long long *` could not touch an `unsigned long`, and to keep `result` in a register across the inlined call. It did. `run_grind` returned UINT64_MAX for every input, so layer 8's two checks per vector that expect the SENTINEL passed VACUOUSLY while the two that expect a found nonce failed. Six rows, at every sha back to the gated base c00342c, on a target that passes on a clang/arm64 laptop where the two types coincide. Measured on the box at this sha: -O2 6 FAILURE(S) -O2 -fno-strict-aliasing ALL HOST KAT CHECKS PASS -O0 ALL HOST KAT CHECKS PASS None of it was ever a statement about the device grind. This file is a HOST replay of the kernel source through `cuda_host_shim.h` — no nvcc, no cubin, no device — so the defect was in the harness holding the result, not in the kernel it tests. The production path re-validates every device nonce with the host predicate, and the block pins read `host fallbacks 0` throughout. `crypto/math-cuda/tests/host_kat/` holds exactly one instance of the pattern and this is it: the shim's `atomicMin` takes `unsigned long long *` as a parameter, and the kernels' casts there only drop `volatile` from an already-matching type. Test-only; no production code and no proof bytes move. It also unblocks this lineage's CI `host-kat` job, which has been failing since the device grind landed.
`a_group_holds_only_its_codewords_before_any_open` took `free_before` AFTER a `drain_and_trim()` and `free_after` without one. `free_vram_bytes()` is the driver's count and the device pool is configured to retain all freed blocks, so that difference measured the code PLUS every transient the four commits made. A delta between two samples is about the code only if both are taken at the same pool state, and the test's own comment says exactly that about the first drain. It read 301,989,888 B — nine codewords on a bound of nine, where the model says eight are held. The old one-sided bound was `8 x codeword` against four codewords held, so it carried 128 MiB of margin the pool had been living in unnoticed; the leaf-layer retention did not add pool retention, it consumed that margin. The slack was never sized against the transients either: `build_tree` allocates `(2L-1)*32` = 64 MiB, twice the bound's 32. The mutation arm settles which it is. Holding a whole node array instead of a layer moved the measurement to 480 MiB where the code then holds 384 - an excess of 96 against the honest run's 32, tripling while the holding grew by half. No "the code holds one more object" form fits both: 4*(cw+tree)+tree = 448, +cw = 416, and 5*(cw+tree) = 480 fits that run exactly but dies on the honest one, where 5*(cw+leaf) = 320 != 288. Every peak-demand model misses on BOTH sides (320 and 448 predicted). That is driver suballocation, not an accounting this tree keeps. So the driver's count is sampled at the same pool state on both sides, and the assertion messages now carry the CODE's own number beside it: the delta of `Backend::reserved_bytes()` across the window, the pool's share as the difference, and each held codeword's `reserved_bytes()`/`retained_leaf_bytes()`. A future failure says which of the two it is instead of posing the question. Pre-registered for the next card run: the honest case falls 288 -> ~256 and the whole-tree mutation 480 -> ~384. If the honest case still reads 288, the ninth block is the CODE and this reasoning is wrong. The assertion is not weakened: drained on both sides, four kept layers read ~256 below the 288 bound and four kept TREES still read ~384 above it, so the 128 MiB of separation the bound was designed around is restored rather than spent. Test-only.
The ledger the previous commit added is built inside the two assertion messages, so it appears only when the test FAILS. On the passing path its numbers were inferred rather than read, and what a pass alone establishes is `driver < bound` — pool share under one codeword — and nothing narrower. That is not enough for this guard. The mutation run that keeps a whole node array reads `driver 448 MiB · promised 383 MiB · pool share 64 MiB` even after the symmetric drain: a fragmentation floor of one largest transient, because a best-effort pool trim cannot release a chunk still backing a live allocation. If the honest path sits anywhere near that floor, this test has a margin of a few MiB and will flake, and a green run would never say so. 0 MiB and 31 MiB are the same observation today. So the line is printed unconditionally, under --nocapture, which is how the box gate runs this suite. Once its honest value is known a ceiling can be asserted against it, which is a gate change rather than a test change and is not made here. `promised` is worth having in the log for its own sake: at the mutation it read 383 MiB against a model of 4 x 96.00, exact to the MiB, which is what settled that the excess is the pool rather than a ninth object the code holds. Test-only; no assertion changes, no production code.
…olumns) The only fallback number the WHIR campaign read was `multilinear::gpu::host_fallbacks()`, which has exactly one caller — the COMMIT path in `whir_chain.rs` — so every `host fallbacks 0` certified that no commitment fell back and said nothing about the per-table argument. wt16 read as a slot-level win for exactly that blind spot: the leaf-layer retention grew `be.reserved`, argue's `reserve` then refused, and its work moved to the host uncounted while `tree_rebuild` alone showed the saving. Add a process-wide counter in `device.rs` beside `reserve` (`device_fallbacks` / `reset_device_fallbacks` / `note_device_fallback`), always compiled and reading zero on a non-cuda build, bumped at the five argue-side `reserve`->`None` sites in math-cuda: `sumcheck.rs` (x3), `gkr.rs` (x1), `columns.rs` (x1). The doc states this scope precisely and records the multilinear residual (`gpu.rs:177`/`:1572`) as a follow-up that needs each caller traced, and why `gpu.rs:1551` — a speculative reserve whose `None` selects a lazy on-device path — must never be counted. Tests: a card test drives the cheapest site (`DeviceColumns::upload`) with the budget fully reserved (an atomic bump, no device memory) and asserts the counter reads one; a card-free unit test covers the counter API; a card-free source-count test asserts the call appears at exactly the five sites, so the four undriven sites fail without four card fixtures.
…e-run block The WHIR tree harness printed no fallback line at all, so the launcher had nothing to gate on and (v9) voided every run by reading a `host fallbacks` line that only the lb-class grind harness prints. Print BOTH fallback surfaces, whole-run scope, at the WHOLE-RUN block of the production-tree test: `commit fallbacks` (`multilinear::gpu::host_fallbacks`, the commit path) and `device fallbacks` (`math_cuda::device::device_fallbacks`, the argue surface added in the previous commit). The launcher (A-tree-whir.v10) refuses a block number unless both read zero and refuses loudly if either line is absent — closing the blind spot wt16 read as a slot-level win, where argue's per-table work fell to the host uncounted.
…er instruments The evictable retention (round 2's fix) and any honest reading of the leaf-layer lever need two numbers the code lacked. RETAIN_BYTES_LIVE: the SIMULTANEOUS retained device footprint — fetch_add on admit, fetch_sub in a new Drop on RetainedLeaves — plus its per-run peak. Unlike the cumulative RETAIN_BYTES_ADMITTED (39,057 MiB in wt16), this rises and falls with the live layers, so it is the ~2 GiB that actually contends with argue for the budget. The peak is printed on the retention line; the instantaneous count is ~0 by the time the base readback prints (the codewords have dropped). reserved_high_water: the peak be.reserved, updated by note_reserved on every rise in Backend::reserve and DeviceReservation::grow. This is the reservation quantity argue's reserve is checked against, which the raw device trace cannot report — never-purge inflates the raw peak above the budget. Printed at the whole-run block. Tests: a card test asserts the live footprint rises with a held layer, the peak and high-water bound it, and — the balance the eviction relies on — the footprint returns to baseline when the codeword drops. Card-free unit tests cover the high-water's monotone max.
…e bytes instead of falling to host wt16 read the leaf-layer retention net-negative at the block: it grew be.reserved during commit and the openings, argue's per-table reserve then refused and fell to the host uncounted (+11.3 s argue vs the -9.45 s tree_rebuild saved). The cause was a single byte budget raced between the retention and argue. Make the retention SUBORDINATE to argue by eviction, so it holds only genuinely spare bytes and gives them back the instant a real caller needs them: - Backend::reserve, on a budget miss, consults an evictor ONCE before returning None and retries after it frees. grow (the retention's own capture) never evicts, so the retention can only ever yield to argue, never displace it. - whir installs the evictor (a fn pointer, via OnceLock) and keeps a registry of Weak handles to each codeword's (leaves mutex, reservation), registered once at first capture and pruned when the codeword drops. Eviction takes a layer out under its own mutex (a concurrent serve sees None and rebuilds -> no UAF; the evicted nodes' free is stream-ordered on the codeword's own stream, cited to cudarc core.rs:776-795 in the code), drops it, and shrinks the reservation -- freeing the BUDGET while never-purge keeps the raw bytes pooled. The evictor never calls reserve/grow (no reentrancy); lock order is registry -> one layer at a time, be.reserved lock-free -- acyclic. LFM_WHIR_RETENTION=0 disables capture entirely, so the ABBA control arm runs off the same binary as the retention arm. RETAIN_EVICTED / RETAIN_BYTES_EVICTED and the live-footprint peak are on the retention print. Tests: a card test fills the budget below a held layer's size and asserts the next reserve SUCCEEDS by evicting it (the layer reads None after) -- the arm that fails when the evictor is disabled.
…counted twin Round 3's poll fix is blocked on one bench reading: does the grind's stale-poll overrun FALL, RISE, or stay FLAT as the poll rate is lowered? That sign — not a magnitude — decides whether the "poll less" family of kernel fixes lives. O2 falsified the scan-factor lever; O4 read the SASS and closed the cache-qualifier lever (the poll is already LDG.E.64.STRONG.SYS). The one surviving hypothesis is CONTENTION on the single *result address. rpx_grind_search_counted (the diagnostic twin, on no proving path) gains a poll_period launch parameter: it polls *result for the early exit only every poll_period-th iteration, STAGGERED by thread via (n + tid) & (poll_period-1) so at any one iteration only 1/poll_period of the resident threads issue the system-scope load — average AND peak request rate both fall by poll_period. poll_period == 1 (mask 0) reproduces the shipped every-iteration poll exactly; the production rpx_grind_search is untouched. n is the thread's own loop counter (not i/stride, whose identity holds only while tid < stride). search_counted threads poll_period through to the launch (arg LAST) behind a zero/not-power-of-two guard, and echoes it back in GrindCounts so a report quotes the knob as read on the path. The rewritten rpx_grind_counted test sweeps k = 1/4/16/64 at scan 8 / grid 1024 over O3's 256 seeds, paired and rotated, and reads the overrun vs k. Controls: k=1 admissibility against the shipped kernel; the winning nonce identical across every k — the soundness control, since atomicMin only ever lowers *result, so a staler poll can only delay an exit, never change the nonce a launch returns. The verdict prints a granularity-adjusted (overrun - (k-1)/2) column to isolate the contention component from the poll-coarseness term.
…gister sweep of the RPX permutation The poll k-sweep falsified contention (POLL FAMILY DEAD), so round 3's lever must speed the RPX permutation itself: grind + two hashing passes all share it, and the file's cost model shows it is compute-heavy (inverse S-box = 95% of the field mults). The open question that picks the lever: is the permutation latency-bound (raising occupancy speeds it) or compute/issue-bound (it does not)? The card runs RPX at ~2/3 occupancy, register-limited. This adds the discriminator, card-free authored, as a whole-cubin register cap rather than __launch_bounds__: the SHIPPED grind kernel — which the sweep must move — is off-limits for a per-kernel annotation, and launch-bounds variants would need new kernels loaded in the off-limits device.rs. A -maxrregcount cap moves the untouched production kernels at build time. - build.rs: opt-in LAMBDA_VM_RPX_MAXRREGCOUNT ⇒ nvcc -maxrregcount, mirroring the existing -lineinfo knob; empty/unset ⇒ no cap ⇒ production cubins byte-stable. - math-cuda::rpx::permute_probe_sweep: times the pure permutation probe (htod once, so the cross-build delta is kernel time) and reports the ACHIEVED regs / blocks-per-SM read back from the loaded function. - math-cuda::grinding::grind_occupancy: the shipped grind kernel's achieved regs / blocks-per-SM. - prover/tests/rpx_occupancy_sweep.rs: one point per build — probe ns/permutation and grind mean ms at the achieved occupancy, one OCCSWEEP line to collect across the caps. The sign is read ACROSS builds (unset/85/51/42 ⇒ ~8/6/10/12 blocks/SM): time FALLS as occupancy rises ⇒ latency-bound ⇒ build the register-pressure lever; RISES/FLAT ⇒ compute-bound ⇒ occupancy and LDL.64 are dead, only a KAT-preserving arithmetic lever remains or round 3 lands at the arithmetic floor. A register cap cannot change a kernel result, so there is no soundness question; permutation parity stays pinned by rpx_device_parity. No default and no shipped kernel change.
…ytes probe (STEP 2, ncu-free)
The occupancy sweep put the RPX permutation at its arithmetic floor, so round
3's only remaining stage is argue (the WHIR field-argument: sumcheck + gkr +
columns, ~16.6s). STEP 1 (the O5 device-fallback counter, read from the round-2
logs) established argue does NOT host-fall-back at the tip — it is device-side
and stable. This is STEP 2's instrument: does argue's device work hit the HBM
roofline (memory-bound ⇒ an MLE layout/reuse lever exists) or run far below it
(compute-bound ⇒ near a floor, like the permutation)?
ncu is unavailable on the box (ERR_NVGPUCTRPERM), so the roofline is read by
ARITHMETIC: a new `math_cuda::argue_probe` records, per surface, the DEVICE-path
bytes reserved and the op count, at the same five reserve sites the fallback
counter already guards (sumcheck.rs x3, gkr.rs, columns.rs). Divided by the
`argue` wall time the harness already prints, the total bytes give an achieved
HBM bandwidth. Reserved bytes ≈ the HBM working set (a resident buffer re-read
within an op is L2/L1, not HBM), and it is additive — unlike a wall-timer at
these sites, which would double-count when gkr's layer sumcheck nests inside a
reserve; a per-surface time / device-host split is STEP 2b, only if the byte
roofline is borderline.
- crypto/math-cuda/src/argue_probe.rs: per-surface {bytes, calls} atomics +
note_device / surface_totals / reset (mirrors the DEVICE_FALLBACKS pattern).
- the five reserve-SUCCESS sites call note_device beside the else's
note_device_fallback.
- per_table_aggregator_tests.rs prints `argue probe: sumcheck B/ops · gkr · columns
· total` beside the existing `device fallbacks` line.
Diagnostic only, on no production decision path; a reservation is unchanged, so
this cannot move a proof. No default and no shipped kernel change.
… argue discriminator
The argue census put the WHIR argument at ~2% of the HBM roofline and single-digit-%
of compute on LARGE kernels — GPU-under-utilized, not floored. ncu is driver-locked
on our box (ERR_NVGPUCTRPERM), but Mauro has a profiler-capable server. This gives
him one representative launch to profile.
`ncu_sumcheck_round_block_scale` (an #[ignore] test in tests/sumcheck.rs) builds a
block-scale sumcheck — num_vars=21 (KECCAK_RND scale, the census byte-leader), a
Builder-lowered program at the tested (width 4, degree 5) shape — and runs a handful
of round + fold launches so Nsight Compute can profile sumcheck_round_ext3 (and
sum_partials_ext3 / sumcheck_fold_ext3) at realistic dims. It reuses the file's
existing factor()/program() helpers, so the program is a valid lowering, not a
hand-fabricated node stream. No host cross-check (a 2^21 host round is far too slow)
and no correctness claim — parity is device_rounds_match_the_host_sumcheck's job;
this exists only to hand the profiler a launch. On no production path.
⚠ ncu -c 1 profiles ONE kernel = that kernel's own occupancy/SoL, NOT the inter-round
host-sync idle (round() synchronizes every round to cross the transcript answer to
the host — sumcheck.rs's own note: "more time than the rounds themselves"), which is
a timeline property for nsys. So it answers "is the round kernel itself
under-occupied?" — the complement to the host-sync finding.
Build + profile (WHIR branch only — the argue stack is not on main):
cargo test -p math-cuda --release --test sumcheck --no-run
ncu --set full --section SpeedOfLight --section WarpStateStats --section Occupancy \
--section MemoryWorkloadAnalysis -k regex:'sumcheck_round_ext3' -c 1 \
<target/release/deps/sumcheck-*> ncu_sumcheck_round_block_scale --exact --ignored
…n discriminator) Round 3's concurrency lever is soundness-dead: the whole argue is one sequential Fiat-Shamir chain (run_rounds is a per-round chain; multilinear_table.rs:444 argues all tables in one transcript), so no sumcheck round can overlap another — the challenge order is the proof. Argue's ~2% GPU utilization is therefore mostly INHERENT per-round host-sync latency, not a recoverable inefficiency. This sizes it, on our own box (ncu is driver-locked): a gated, opt-in device-busy probe measures how many seconds the sumcheck round kernels are actually executing, so idle = argue wall − device-busy is the total gap. It is not a recoverable ceiling by itself — the recoverable-without-a-rewrite part is only what transcript-independent prefetch can fill. - argue_probe: DEVICE_BUSY_NS + add_device_busy_ns/device_busy_ns, and busy_probe_enabled() (reads LAMBDA_VM_ARGUE_BUSY_PROBE once, cached). - sumcheck.rs round(): when enabled, a reusable TIMING-enabled CUDA event pair (thread-local, created ONCE — a mid-prove cuEventCreate convoys the driver lock) brackets the round kernels; the elapsed is read after the EXISTING per-round synchronize(), so no extra sync and no perf change. Off by default: production round() only reads a cached bool and skips it. - per_table_aggregator_tests.rs: prints `argue device-busy (round kernels): X s` beside the argue probe line. Round kernels only (fold + setup excluded), so idle = wall − this slightly OVER-estimates. Diagnostic; no default and no shipped-kernel behavior change when the env is unset.
The head's trace leaves 0.79 s of card idle between one GKR layer's read-back and the next layer's first kernel (3,489 transitions, 227 us each) and cannot say whose it is. Stage A5 is to be built only once that is known. Under the base split only, each device layer is now timed region by region: lambda, the program, its lowering, the session set-up (the input layer's rebuild apart), the rounds, the read-back, the factors, the host tail (its transcript share through a timing wrapper) and the close. Every prove record prints them as one `ARGUE GKR` line with the host work between layers and its mean a layer. The wrapper makes the same calls on the transcript it wraps; a test pins that it draws the same challenges and leaves the same state, and fails if a call is dropped. With the split off nothing reads a clock.
…card Brings fix2/gpu-tables up to 93a2b56, the sha job 208 measured on FAST: WHIR ABBA EFFECTIVE, whole run B - A -1.05 s (band [-1.5, -0.7] HIT), host-walked columns 24,195 -> 3,478, every arm proved, verified and on the record's identities. The knob, LAMBDA_VM_ARGUE_DEVICE_COLUMNS, is still off by default here; the next commit turns it on.
LAMBDA_VM_ARGUE_DEVICE_COLUMNS 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 208, at 93a2b56) read EFFECTIVE: the whole run 1.05 s faster (band [-1.5, -0.7]), the columns the host walked 24,195 -> 3,478, every arm proved and verified on the record's identities. The proof does not change: each card value is the column's multilinear extension at the point in exact arithmetic, the host's value, so the canonical bytes, the transcript and every challenge are the same; the fixture identity test and the cross-check arm showed it. No pin moves: the WHIR byte gate builds without cuda, where the knob has no card to use, and no STARK path reaches the claim reduce. Without a device the knob only spreads the host walk over the pool, value for value. A unit test pins the reading: unset, empty or any value is on, and only 0 is off.
whir_epoch_program's steps 1-6 move verbatim into emit_epoch_leg, which declares the epoch's one arena, emits its verifier on its own transcript and returns the four wires the published set needs (EpochLegWires). The wrap is that leg plus emit_epoch_publishes over EpochLegWires::publishes: the same builder calls in the same order, so every wrap program is byte-identical. A wide level-1 node reuses the leg per epoch.
… L1) emit_wide_node emits each epoch's verifier leg (emit_epoch_leg: its own arena and transcript), then runs the node's own emit_chain_bindings and emit_node_publishes over what each wrap would have published (epoch_would_publish). It binds what an L1 node binds between its wraps, in the same order, and publishes the node schema; the labels it pins are the tree positions the caller passes, not the epochs' own. Box-tier tests at the continuation fixture's scale: the honest node publishes the first INIT, the last FINI, the position range, the last output and the fold of the epochs' bookend roots; a broken register chain, swapped positions and a disagreeing attestation id are each refused, each paired with a control without the bindings that executes.
Read once, bannered on every setting, an unknown value aborts; unset is off (today's wraps). on takes k = the tree's fan-in epochs per node and is refused under LAMBDA_VM_LFM_PROVER=stark.
Job 212's device checks stopped at the argue's negative control. Under the Eq fault the corrupted proof was refused, but as ShiftedReadMismatch, where the test expected BatchMismatch. The Eq fault writes the first cell of two tables per table argued: the zerocheck's eq(r) weight and the reduce's offset-0 eq(alpha) table. Each table is verified GKR, then batch::verify (BatchMismatch), then claim_reduce::verify (ShiftedReadMismatch). CPU, the first table, has no constraints of its own (EmptyConstraints), so its zerocheck rule is eq(r) times an empty sum, which Builder::sum makes the constant zero. A wrong eq(r) therefore moves no zerocheck round, and the first check that can see the fault is the reduce's final one. Nothing is wrong with the protocol or the kernels: the zerocheck weight fault is refused as BatchMismatch under a table with constraints, which multilinear's argue_device_tables matrix already pins and which passed on the box. The test now expects ShiftedReadMismatch for both faults and pins the mechanism: CPU's GKR, zerocheck and factor values equal today's, and its reduce does not. It also proves the same arm without a fault first, as a control that must equal today's proof and verify, so the faulted arms fail for the fault alone.
…IDE=on whir_level_zero takes wide: one pool task per fan_in consecutive epochs, each harvesting its epochs, emitting the wide node over the tree's positions, proving it under the tree's prover and checking the node schema's ends (the first epoch's INIT, the last epoch's FINI, the label range). The interior gains start_level, 2 under a wide level 1, so it proves only the levels above it; the root, its fold shape and the global stage are untouched. Off, every call and every printed line is today's. The lead-in builds wrap prologues, so a wide run starts none.
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.
MauroToscano
changed the title
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.
MauroToscano
changed the title
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.
MauroToscano
changed the title
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.
The number
Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21. At this head,
5f15641b9, the two default arms of the last ABBA read 43.8 s and 43.9 s (mean 43.85 s). Host peak 16.2 GiB,device peak 27.0 GiB (27,634 MiB).
Each step below is its own ABBA on one binary: two arms per setting, alternated.
d1dc45514¹ Measured on its stage branch (
34c17603b), before P2-W and A1.² Two builds, alternated X XF X XF, at
6a6e26611: the MDS fix has no knob.In the third row's A arms, every fix in the next table is switched off by its opt-out. Their program ids and census equal
those before the batch (
668a89a4c). The one change with no opt-out of its own, the WHIR encoding through the engine,is in both arms. A fifth arm, the defaults with only the level-0 lead-in off, read 61.4 s, so the lead-in is worth
−1.20 s here. The STARK PR (#1009) measured the same batch at −28.75 s (107.55 → 78.80 s).
The gap fixes
Each fix was measured first in its own ABBA, mostly on the base before the engine. Those rows do not add up to the
cumulative −39.65 s; the last row above is the measurement.
LAMBDA_VM_ZF_WHIR_STACK=25LAMBDA_VM_RPX_LIMB_PERMUTE=0LAMBDA_VM_RPX_GRIND_QUEUE=0LAMBDA_VM_BASE_PREP_ON_PROVER=1LAMBDA_VM_LFM_KEEP_BITWISE=1LAMBDA_VM_RPX_WARP_MERKLE=0LFM_TREE_PROLOGUES_AT_LEVEL0=1d1dc45514LAMBDA_VM_WHIR_FOLD_CLASSIC=1LAMBDA_VM_STAGING_SHARED_SLAB=1LAMBDA_VM_NO_WHIR_FUSED_FOLD=1,LAMBDA_VM_WHIR_LEAN_ROUNDS=0LFM_TREE_REDERIVE_DECODE=1LAMBDA_VM_LDE_LEGACY=1, which also reverts every other LDELAMBDA_VM_DEEP_INV_LEGACY=1LAMBDA_VM_NO_WHIR_ROOM_PARK=1,LAMBDA_VM_NO_WHIR_ROOM_RESIZE=1LAMBDA_VM_LFM_HASH_SPLIT=1turns it onAlso in the batch, with no knob:
Grinding only before the queries (P2-W)
What changed. Each round of a WHIR base chain used to grind 20 bits before three challenges: the first folding
challenge, the out-of-domain batching challenge γ and the query positions. It now grinds before the query positions
only.
1,472.
whir_grind, defaultquery; the banner reads… whir_stack=27 whir_grind=query.The proof carries only the nonces it spends (
NonceLayout::Spent).1,036 fewer a block.
nonzero value in a field the format does not carry.
Measured on block 25368371 (FAST, one binary, arms A B B A, wt820–823):
LAMBDA_VM_ZF_WHIR_GRIND=allpredicted from the grind count.
Soundness: no proven bits are lost. Of a round's three grinds, only the query grind raises the proven minimum as
placed:
challenge by varying that message, without grinding again, so this grind earned no credit.
with no grind at all.
Every phase keeps its bits:
security/zisk_calc.py).[0,0,20]against[20,20,20]), so a proofground one way does not verify the other.
red.
Opt-out.
LAMBDA_VM_ZF_WHIR_GRIND=allrestores the grinds before all three challenges and the three-nonce format:the previous proofs, program ids and census, byte for byte. Golden tests on the chain programs, arenas and host proof
bytes pin it, and so does the A arms' match above.
The argue's short, wide tables on the GPU (A1)
What changed. In the WHIR base's argue, a table whose columns are already resident on the card is now valued there
once it holds 2^16 cells (width × rows). Before, each column needed 2^16 rows. The few columns left on the host are
walked across the thread pool.
fall from 24,195 to 3,478 a block.
Measured on block 25368371 (FAST, one binary, arms A B B A):
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=093a2b5643, wt831–834)8930490e5, wt850–853)The whole saving is in the base (41.90 → 40.95 s in the stage's ABBA); level 0 and the interior stay within noise.
Soundness: the proof does not change. The card computes each column's multilinear value exactly, the same field
element the host computes, so the transcript, every challenge and the serialized proof are identical, and so are the
program ids and census.
LAMBDA_VM_ARGUE_XCHECK=1) re-evaluated every card value on the host: 30,086 of 30,086 matched.on the card; a wrong card value is refused.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=0restores the height rule and the one-at-a-time host walk, line for line.The argue's challenge tables on the GPU (A2+A3)
What changed. The WHIR base's argue built its challenge-dependent tables on the host and uploaded them: the
zerocheck's
eq(r)andeq(row)weights, and the claim reduce's shift tables and batched columns. It now builds themon the card from the columns already resident there.
eq(α)table; each batched column is one kernel over theresident columns.
pageable uploads a block (1.16 s of copies).
Measured on its stage branch (
34c17603b, before P2-W and A1; wt836–839): A 59.65 s (59.5, 59.8) → B 54.45 s(54.4, 54.5), −5.20 s. The base fell 41.65 → 36.65 s and the argue 19.7 → 14.7 s; the card built 1,364 tables an
arm.
Soundness: the proof does not change. The card builds the same field elements the host built, so the transcript,
every challenge and the serialized proof are identical.
LAMBDA_VM_ARGUE_XCHECK=1) compared every card table with the host's before its first round.the fault inert fails that test.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_TABLES=0builds the tables on the host and uploads them, as before.Pure WHIR recursion
What changed. The recursion's LFM proofs (the global wrap, the nodes and the block-artifact root) are proved by the
base's own stacked-WHIR prover instead of one STARK per table. Each parent verifies a child with the WHIR verifier the
wraps already run, over the child's LFM statement.
three times, then the node's own bindings and publishes. The 15 wraps and their proofs are gone. With three epochs a
node, the tree's fan-in, the node schema, the root's L2G fold and every level above are unchanged.
own point. The main stack holds the value columns only.
harvests and the emission.
global wrap's program is the same one.
Measured on block 25368371 (FAST, one binary per row, arms A B B A):
4150afab6, wt860–863)6a6e26611, wt880–883; A =LAMBDA_VM_LFM_PROVER=stark)against the wraps' 7.4 s, the interior 1.8 s against 9.0 s, the root 1.0 s against 1.4 s.
≥ 4. The base is 9 s faster than when that row was set, which leaves the two helpers a 4.7 s tail. The property the
count stood for held: the GPU's first hold came 0.17 s after level 1 started.
Soundness: every phase keeps ≥ 128 proven bits, and the recursion's minimum rises.
stacks of 2^24–2^27. Their minimum is 130.393 bits, the n = 27 first fold, unground, the same as the base's. It
replaces the STARK recursion's 128.946 bits, which came from its LFM query phase. Measured by the calculator on each
run's own chain lines.
statement built from the AIR's column list would count zero and bind nothing: a forged program would verify.
statement. The sponge receives each as a base token, so a non-canonical upper lane is unprovable.
next one's INIT, each epoch at its tree position. It reads these from what the wraps would have published. Its L2G
item is the fold of the epochs' bookend roots, the fold a node over those wraps takes.
AIR's count. A forged instruction column is refused by the prepared opening. A deleted opening, a restated table
height, a tampered or reordered public word and a prepared root absorbed after
zare each refused.that nothing settles are each refused.
disagreeing attestation id are each refused, each beside a control without the bindings that executes.
verifies with the count at zero and is refused with the AIR's count.
Opt-outs.
LAMBDA_VM_LFM_PROVER=starkrestores the per-table STARK recursion. The A arms above print8930490e5's 24 programids byte for byte.
LAMBDA_VM_LFM_WHIR_PREP=bothalso keeps each table's instruction columns in the main stack.LAMBDA_VM_LFM_WIDE=offkeeps the wraps under the WHIR recursion.Narrow sumcheck rounds on demand (N1′)
What changed. In the WHIR argue's zerocheck, a big batch's device rounds now walk its program on demand.
Each step is emitted where the step that uses it first needs it, in Sethi–Ullman order: of two operands, the one
needing more values goes first.
Every read, a column's value or a constant, is emitted again at each use instead of once and held.
The steps are the same operations on the same operands. What changes is how many values a thread holds at once,
which sizes the round kernel's per-thread slot file and so how many threads a round can run.
The slot file is also sized for every interpolation node from the first round.
A batch is big when its program holds more than 341 values a thread, which leaves a round under 64 k threads at the
512 MiB slot budget. Five batches are big:
Every other batch keeps its program as it was, the byte gate's EQ fixture (26 values) included.
Measured on block 25368371 (FAST, one binary):
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0965e13de2, wt890–894)a28ad36af, wt910–914)Where the gain lands: the base.
fell 1.28 s.
2 of 5 programs are ready, and the card waits in the gaps between them, so the saving does not reach the wall.
column values instead of 331, over up to ≈ 4 GB of columns.
Soundness: 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 the census: equal in every arm of both runs.
LAMBDA_VM_ARGUE_XCHECK=1) walked the old program in a shadow session over the same card-residentvalues. It compared every big session's rounds, round by round, in the base and in every W-LFM proof, and every one
matched.
BatchMismatch), and by the cross-checkbefore a proof exists (
DeviceFailed);Opt-out.
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0keeps every batch's program as before and sizes the slot file for onethread an index, line for line.
The RPX MDS compiled the same way in every build
What changed. Both RPX implementations compute the MDS over a compile-time circulant with plain loops, instead of a
core::array::from_fnclosure. The closure's wrapper was inlined only when rustc's codegen-unit partitioning placed itin
mds's own unit; otherwise each output lane was an out-of-line call. That made the host's hashing about 20 % slowerin some builds than in others, decided by unrelated edits.
Measured at
6a6e26611(two builds, X XF X XF): −0.50 s (45.65 → 45.15 s). The executor's hashing runs at0.81 of its old time per permutation; most of the gain is in the base (−0.30 s). The STARK PR (#1009), where host
hashing sits on more of the critical path, measured −5.95 s.
Soundness. The same values: the RPO and RPX known-answer vectors, the two implementations' agreement test and a new
test against the circulant's definition pin it, and transposing the matrix fails six of them. No knob.
What is in the branch
for the block.
(−8.3 s).
inside level 0's pool, saved −11.9 s. Together they took the block to 128.3 s.
ZfFormat(prover/src/zf_format.rs) parses sevenLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT:banner. The default iscap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6 whir_stack=27 whir_grind=query.end of each tree's first path, so the proof structs are unchanged.
chain.
8–11 of 2^25.
whir_grind, defaultquery: one grind and one nonce a round inthe WHIR chains; see "Grinding only before the queries" above.
LAMBDA_VM_ZF_ONE_ROW=auto) are built on host, on the GPU andin-guest, but are off here: they cost +3.2 s on this pipeline. They are on in the STARK pipeline's PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009).
ZfFormat::LEGACYstays pinned by a golden test. The RV64 recursion guestverifies only the legacy format.
crypto/math-cuda/src/lde_cm.rs,kernels/ntt_cm.cu).zero fill, and a transpose before a row-major commit.
launch in registers and shared memory, so a 2^22 transform is three passes. The coset spread is fused into the
first pass, and the output is column-major, so the commits lose their transpose.
commit's encoding. LDEs that keep a host copy (below 2^19 rows) stay on the old path.
LAMBDA_VM_LDE_LEGACY=1sends every LDE back to the per-level pipeline.gap-fix/ntt(da2da9d93),gap-fix/wbatch-int(7e3eac501),gap-fix/harness(f81f0a80f),gap-fix/rec-int(c679a771b),gap-fix/stack-int(8c2450ff6) andgap-fix/idle-a-int(d3c76d2ed), eacha signed merge;
gap-fix/idle-b-int(bdb2d37b6) andgap-fix/hash-int(e041e9fb0), each a signed merge;gap-fix/kern-int, one commit (d1dc45514).the stack.
9cea599a3(the nonce layout, default off),ce292de3e(the default)and
b4506b719(comments).93a2b5643(behind its knob), merged asc7228f310, and8930490e5(the default).34c17603b, merged as7364d1292, andb9698b05d(thedefault).
whir/full-recursion(4150afab6), merged as3722e7376;70cdb3719(its pins under P2-W)and
6a6e26611(the default).1177d5a13(the census) and965e13de2(behind its knob), merged as06d2d48e8;26adbf501(the default) anda28ad36af(the W-LFM parity tests). The merge also carries two argue knobswhose A/Bs read MECHANISM-ONLY,
LAMBDA_VM_ARGUE_LEAN_READSandLAMBDA_VM_ARGUE_LEAN_TAIL, both off.d61a3c729) and deterministic whir_chain grind tests (d6648e653, merged as5f15641b9):this head.
main: perf(alloc): compile jemalloc's never-purge policy into the binary #996 (jemalloc never-purge compiled into the CLI).Soundness
Query counts and blowup are unchanged.
The format levers
cap node the query index selects. Path lengths are checked exactly, including at c = 0.
changes, in a term that stays more than 50 bits below the dominant one.
layout Plonky3 uses. The query index is uniform over the whole domain.
fewer rounds, and queries stay 112 per round.
The gap fixes
all take the layout from
global_layout(shapes, cap), never from a proof.table. It stays 112 at every production shape.
security/zisk_calc.py): the WHIRchain minimum is 130.393 bits at 27, against 130.926 at 25. With the per-table STARK recursion
(
LAMBDA_VM_LFM_PROVER=stark) the pipeline minimum is 128.946 bits, set by the query phase of every LFM proof; withthe default pure WHIR recursion it is 130.393 bits (see "Pure WHIR recursion").
message, so a cheating prover can re-draw α₁ by varying h₁ without grinding again. The bits above are the unground
ones. P2-W drops the folding and out-of-domain grinds (see "Grinding only before the queries"); K4 changes only how
the card searches for the nonce.
sender, its honest multiplicities are all zero and the table constrains nothing.
instantiated chip's interactions, stored in the artifacts and folded into
program_id, and the verifier re-checksit against the mask it was handed. No proof supplies it.
LAMBDA_VM_LFM_KEEP_BITWISE=1reproduces the legacy registry digests.emissions compute the same field value on accepted and on tampered chains (tests). The WHIR wrap program ids move.
program_idand never read from aproof. Tests refuse a forged tail root, the single-table door and a wrong chunk root.
parity through either staging, on the card;
reference, and the fault suite under both settings.
the 64-bit multiply. Its bytes were shown equal three ways:
with a failing control). It also replays the cooperative kernels lane by lane (the half-warp Merkle kernels and
the queue grind) against the shipped ones. CI runs it on every PR;
path and, where cheap, against the host oracle (
rpx_device_paths);Fixed along the way
tables, which rejected honest proofs that publish values.
failed, the error was dropped, and every such commit fell back to the host; the base took 647 s. The grid now splits
into z, and device commit and tree errors are logged and counted.
source codeword dropped.
GPU.
Gate and CI
N1′, the MDS fix and the grind tests were gated at this head,
5f15641b9, on the FAST2 box: 21 steps, all green (thelib suite 1,625 / 0 / 94): the standard six, N1′'s 13 (card parity on the five big batches, the whole argument's
identity and its negative control, the slot-budget pin, multilinear's lib at the default and under the opt-out, and the
byte gate for both hashes and under the opt-out) and the MDS fix's 2 (the RPX suites).
Pure WHIR was gated at
6a6e26611, on the FAST2 box: 14 steps, all green (the lib suite 1,622 / 0 / 92). These are the standard steps,plus the WHIR recursion's prover, verifier, leg, wide-node, switch and lead-in suites on the card with their negative
tests, the fixture tree at the default and under the opt-out, and the opt-out's byte gate: the production tree under
LAMBDA_VM_LFM_PROVER=starkprints8930490e5's 24 program ids.A2+A3 was gated at
b9698b05don FAST2: 17 steps, all green.A1 was gated at
8930490e5, on the FAST2 box (the second RTX 5090): 14 steps, all green. These are thestandard steps, plus A1's device tests, the whole argument's identity and its negative control, the multilinear suite at
the new default and under the opt-out, and the WHIR byte gate on both hashes and under the opt-out.
P2-W was gated at
b4506b719on the FAST box: 11 steps, all green. These are the standard steps, plus themultilinear suite, the WHIR chain gates with their production-shape emissions, the WHIR byte gate on both hashes, and
the WHIR epoch verifier programs under the opt-out.
The batch was gated at
d1dc45514on the FAST box: 81 steps, every one at its exact pre-registered count.The standard steps:
The 75 targeted lines cover:
the room on the card;
tests;
For each switch of the last two rounds, a gate line runs each setting and reads the banner its process printed. The
previous candidate without K6 (
41549ebad) passed its own 70-step gate. The cumulative ABBA in the first table ranafter the gate.
In CI at
d1dc45514, these pass: lint, the host known-answer tests (including the RPX lane-by-lane replay), the provertest build, the stark cuda-feature tests, and the CLI and executor tests. The spec structure check fails on a key the
spec tooling does not know (
spec/src/blake3.toml:constants). The prover shards were still running when this waswritten.
Open decisions
STARK in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009),
one_row(off here, auto in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009) and the LFM_HASH split (off here, on in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009). A per-pipeline default would let one PR carry both.LAMBDA_VM_MEMPOOL_RELEASE_MB=0, which releases thedevice memory pool; the code's default retains it. Retaining measured −4.50 s on this pipeline before the engine, but
only −0.45 s at the current head (inside noise), so this PR keeps reporting with the release. The STARK PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.95 s #1009)
measured −2.00 s and reports with the retain.
budget at 27. A block that adds one polynomial to such an epoch moves that argument's reservation to the host:
counted, proof unchanged, slower. The device peak at this head is 27,634 MiB (the highest of the last ABBA's four
arms) of the card's 32,607 MiB. Worth a run on a heavier block before relying on 27 there.
keeps 128 bits.
iteration.