STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s - #1009
Draft
MauroToscano wants to merge 1106 commits into
Draft
MauroToscano wants to merge 1106 commits into
MauroToscano wants to merge 1106 commits into
Conversation
…ormula Part 1 charged each page a hand-written three-term form: one eq, two prefix indicators, one shared Sub, 103 rows. Two readers then checked that form and each found a term the other's lacked — three more per-column terms in stacked_verify_cost outside weight_at_rows, and an absorb of three coordinates per column into a THREADED sponge whose row cost depends on where the previous columns left the buffer. A number two careful readings disagree about is not a closed form, and the sponge term means no hand-written one can be exact. A folded correction would have been worse than the understatement it fixed: still missing that term, and now looking complete. So the marginal is GENESIS_PAGE_MARGINAL_ROWS, a literal beside PREPARED_LEG_ROWS, measured at MARGINAL_MEASURED_AT_VARS = 24, the height the block's thirty genesis pages give. The three-term derivation stays as its doc, explaining the magnitude and naming what it cannot account for. It is marked UNPINNED and a FLOOR: the pin that turns it into a measurement lives in lfm and belongs to the lane that owns the cost form, and nothing else may assert equality with it. One literal is also why the three parties agree — they read the same number rather than evaluating the same formula correctly, which is stronger than the set-independence the fixed height bought. Two ruled quantities move at 109 and the tests now derive rather than hard-code them. Tau is 6, not 5: it holds at 5 only for a marginal in [90, 107], and the only page reclassified carries five nonzero genesis bytes, which neither the block nor any fixture does. The lone-page pair (9,730 sparse, 9,731 dense) holds only for a marginal in [92, 109] and stands on ONE ROW at 109 — the page just over it clears the chain by a single row — so a pin above 109 moves the pair to (9,731, 9,732). The tests assert densest_sparse_entries() and one more, and a band sweep states each consequence's exact band: the block's three pages hold across [19, 2,100,474], the fixture's refusal everywhere, the two shared pages across [1, 2,484]. The emitter test is rescoped to a LOWER BOUND. weight_at_rows is a partial view of the cost form, so an equality against it would contradict the real pin the day it lands. It now reads the two terms that form does account for, 102 across one more page in one bracket, and requires the literal to be at least that plus the amortised Sub.
…es today The literal shipped at 109, built as the three-term reading plus the six per-column rows the cost form pays outside weight_at_rows. Two things were wrong with that. The 103 it was built on carried a shared Sub charged at one per page, and that term is per-POLYNOMIAL: differenced across one more page at one stack height it contributes ZERO, so the deterministic marginal is 102 + 6 = 108, not 109. And the threaded-sponge term is unmeasured, so 109 was 108 plus a guess at it — wrong in an unprincipled direction. 103 is what the rule actually charges today. The literal is then a faithful record of current behaviour, every consequence documented against it is true on the day it lands, and it is wrong in a direction the doc states: it understates the deterministic reading by five, which makes part 1 that much too eager until the pin lands. Consequences restored to their ruled values: tau is 5 again, the block's savings 10,248,261, the fixture's 1,931, two pages of 5,000 saving 89,915 apiece and 179,830 together. The lone-page pair is unchanged at (9,730, 9,731) — it holds for any marginal in [92, 109], so 103 sits with six rows of headroom rather than on the edge. The pin's expected reading is now pre-registered as an executed table rather than a claim: a measurement of 108 or 109 moves tau to 6 and leaves the pair alone; 110 or more moves the pair to (9,731, 9,732). The band sweep asserts both, so when the pin lands the consequence is already written down. The point the retired immateriality test made is kept as one point of that sweep. The weight-term test is renamed to say what it bounds and its doc now explains why the difference is 102 and not 103: the shared Sub differences to zero, so requiring the literal to be at least 102 + 1 is exactly the statement that it contains every term that form can see.
`cargo clippy -D warnings` refuses `prepared_claims`' return type as too complex, on the library target and on six of the nine lint steps. The type grew when a prepared opening stopped naming one table: it gathers a point per settled column and a value per settled column, and both are vectors of vectors. A type alias, which is clippy's own suggestion and not an allow. It carries no bound: a bound on a type alias is not enforced, and `FieldElement`'s own is checked at every use — the form `sumcheck::RoundGroup` and `batch::ResidentProof` already take in this workspace. A pure type alias is a name for a type that already existed, so no signature, no layout and no byte of any proof moves.
… maximum There is no single per-page marginal. The prepared leg's sponge is threaded: every column absorbs three coordinates into one buffer and a single squeeze follows, costing div_ceil(4) + div_ceil(8) + 1. A page is two columns, so six felts, which divides neither 4 nor 8. Differencing across one more page gives s = [2, 3, 1, 3] repeating with period 4, and the marginal is 109, 110 or 111 depending on which page is added. An equality against one number is unsatisfiable for a cost that has three. The literal becomes the MAXIMUM of that spread. Part 1 then asks a page to beat the dearest position it could occupy and part 2 understates its savings, so both parts are conservative, while all three parties still read one number which is what the single literal was for. An average would charge some pages less than they cost. Derived, not measured, by two independent readings that agree, and the doc says so along with the assumption it rests on. It also says what it does not bound: the indicator term grows two rows per prefix bit, so a stack one bracket taller costs up to 113 a page. Raising it there would move neither consequence, since both bands reach past it. Two derived quantities move and the tests name them rather than hiding them. The threshold in nonzero entries is 6, holding across a marginal of [108, 125]. The lone-page pair is (9,731, 9,732), holding across [110, 127]. The sparse-leg cap's bound moves with it, which the ruling's list did not mention and which would have reddened the gate. The band sweep now walks the whole spread and shows the threshold invariant across it, so the choice of maximum over midpoint costs exactly one entry on one quantity. Five clippy errors that the alias commit let clippy reach, fixed as its own suggestions and never an allow. The weight-term bound becomes a strict inequality. The threshold's floor assertion becomes a const block, so falling under the deterministic floor stops the tree compiling rather than failing a test nobody ran. A manual modulo becomes is_multiple_of. A test helper's five-tuple gets a named alias. `genesis_stack` becomes pub(crate) rather than its return type becoming public: that type's own field is a vector of another crate-private type, so widening would have published two types' fields, and every caller is in this crate.
… draft The alias commit let clippy reach the newer commits and the gate found five errors, each fixed as clippy's own suggestion and never an allow. The weight term's bound becomes a strict inequality. The marginal's floor assertion becomes a const block, so breaking it stops the tree compiling rather than failing a test nobody ran, and it now asserts the one bound that holds whatever that number becomes: it must exceed the 102 rows the weight closure alone bills. A manual modulo becomes is_multiple_of. A test helper's five-tuple gets a named alias. genesis_stack becomes pub(crate) rather than its return type becoming public. Widening the type cascades, because its own field is a vector of another crate-private type, so two types' fields would have become public API; every caller is in this crate, and widening later is trivial where un-publishing is not. The same gate failed two assertions, and both were about a draft rather than about the rule. A margin asserting the zero pages sit a factor of six under the threshold was true while the marginal was 109, false at 103, and true again at 111: a margin stated as a fixed multiple of a number that moves cannot survive that number moving. It is now the ratio it is, printed, floored at the weakest value any candidate gives. And the threshold band was tabled as five on one range and six above it, which is not a band; the sweep ran past the end of what had been written down and found seven. All three sub-bands are asserted now, with both edges. Where the literal falls is computed rather than named. Every earlier version of that test named the band it expected, so each time the number moved the test reddened on the naming instead of on the finding. It asserts only that the literal lies in the band for its own value, which holds at the current figure, at the form that is coming, and at the higher one a taller stack costs. The marginal's doc records why three shapes have been tried and why the arithmetic was never the problem: a formula wrong for omitted terms, a literal wrong because the quantity is not constant, and a formula again whose one irreducible term is a measured bound. The value stays where it is; the form and its measurement belong to the pin.
An `assert_eq!` message is a FORMAT STRING, so `{109, 110, 111}` in it is
read as a format argument and rustc refuses the file: "invalid format
string: python's numeric grouping ',' is not supported in rust format
strings". The test crate does not compile at 52c6cc1 or at 8a3f549
for that one line, and nothing else stands between this branch and its
merge.
`{{…}}` is rustc's own hint, and the rendered message is unchanged.
⚠ THE TRAP IS THAT THE LINE LOOKS LIKE PROSE. It sits inside a
backslash-continued string and carries no quote of its own, so a reader
scanning for string literals skips it and a search anchored on a quote
misses it. Two independent sweeps of this branch's six commits agree on
the count: over `60075209f..8a3f549`, the brace-on-a-digit class has
exactly ONE occurrence and this is it; the brace-enclosed-list class has
six raw hits, five of them inside doc comments where braces are inert,
plus this one. Both sweeps were calibrated against this known line
before being trusted, because a pattern that cannot match the one hit
you already have returns a confident zero.
The author of these commits has retired; this lands on their branch
under the lead's authorisation, and carries nothing else — the shape
change the marginal is getting belongs to the commit on the merged tip.
Brings W1j's gated tip 644b7de (eighteen commits over 60d7903) under the harness stage, the root, the main sync and V1j's constant-pool forms. With it the branch carries every half of the WHIR pipeline that exists: the base, the level-0 wraps, the cross-epoch stage, the shared interior and the root. NO CONFLICTS. The file intersection against this branch is TWO — `continuation.rs` and `tests/multilinear_bench_tests.rs`, both moved on this side by the main sync — and `git merge-tree --write-tree` wrote 7c4ef1c for the pair before the merge ran. Both instruments carry their own control: the intersection was taken with a two-sided positive control (the same search shown able to return a hit against each list), because a search reporting nothing to merge is not evidence until it has been shown capable of producing one. The semantic checks, over W1j's whole diff since the base: no statement tag and no fixed-part constant moved, and the single hit on the table-kind class is `Error::InvalidTableCounts` — a variant whose NAME contains the string, not a construction or a destructure. So the three facts the main sync rests on survive: the elision still does not reach the cross-epoch AIR set, the cross-epoch statement's tag and its 134-byte fixed part are unmoved, and nothing in this lineage builds or destructures a `TableCounts`. ⛔ WHAT THIS MERGE BRINGS THAT THE HARNESS CANNOT YET CONSUME. W1j's `prove_global` hands `multi_prove` a genesis opening, so a run with a genesis stack now produces a cross-epoch proof whose `preprocessed` is `Some` — and `whir_global_arena` still opens by asserting that it is `None`. Three sites answer it, in one commit and not this one: drop the assert, extend the arena with the opening's words, and teach the program to hint and verify that chain. ⚠ No fixture here reaches it. The laptop fixture's only page is the private-input one, which carries no genesis, so the arm stays green while the block — thirty of thirty-five pages on OFFSET+INIT — would fail at the global stage. The dense-genesis arm written for that commit is what closes the gap. The asm guest count goes 220 to 221, so the gate's ELF expectation is 266, and it is a recorded check rather than a printed number: a 265 after this merge is exactly the symptom of the new guest failing to build. Nothing is compiled here. This tip's first build is its gate.
…acket, and the cross-epoch program emits the prepared opening PART 1's term stops being a literal. `marginal_stacked_rows(num_vars, n_fixed)` is the rows one more carried page adds to the prepared leg, evaluated at the height THIS run's genesis page count puts the stack at: 101 at a lone page's bracket, 111 at the block's, 113 one bracket up. Three shapes were tried and the arithmetic was never the problem. A FORMULA, wrong because it omitted terms — two careful readings each found a term the other's lacked. A LITERAL, wrong because the quantity is not constant: it takes three values at one bracket and three more one bracket up, and a literal carries its bracket only in prose, where prose goes stale. A FORMULA again, whose one irreducible term is a proven BOUND. ⇒ when a cost splits into a deterministic part and a bounded nondeterministic one, write BOTH: a literal hides the split, and a form that omits the bound looks complete while being wrong. `MAX_SPONGE_MARGINAL = 3` is that bound, proven rather than measured: the wrapper absorbs three coordinates per column into one threaded buffer and squeezes once, a page is two columns, and six felts move `ceil(f/4)` by 1 or 2 and `ceil(f/8)` by 0 or 1. SET-INDEPENDENCE SURVIVES, which is what the single literal protected. `n_fixed` is `fixed_stack_vars` of the GENESIS PAGE COUNT — a quantity prover, verifier and emitter each derive from the ELF and the touched page list before any routing decision exists. It is never `n_dense`, which is the rule's own output. TWO DOCUMENTED CONSEQUENCES MOVE, and both are the form following the run. A lone page is charged at its own bracket, so its boundary is (9,730 sparse, 9,731 dense) with nine rows of margin over the chain, while a page inside the block's thirty faces (9,731, 9,732); both are asserted, each naming its bracket. And τ is not invariant across brackets — 5 while the marginal is under 108 and 6 from there, crossing at nine genesis pages — so the band sweep walks the brackets and asserts exactly one crossing. ⚠ Every such figure here is PREDICTED from the source, not measured: the box reads them at this tip. THE PIN, `whir_stacked_tests::the_marginal_the_routing_rule_charges_is_ the_one_the_stack_bills`, is where the form meets the cost form. It walks both single-polynomial brackets, guards each page count (one polynomial, the expected height), differences `stacked_verify_cost` across one more page, and asserts the form equals the DEAREST page the stack bills, the sponge term inside its bound at every position and the bound reached, and τ invariant across the spread. It also walks the same brackets under a different blowup, folding, security level and grind and asserts the marginals are identical — the claim that every chain term is per-polynomial, executed rather than argued. It needs no hash posture: it proves nothing and harvests nothing. THE CROSS-EPOCH PROGRAM NOW EMITS THE PREPARED OPENING, which is the half of the hybrid the emitter owes. The stack's roots are interned and absorbed in the roots block where `absorb_roots_and_challenge` puts them; the opening's chains are hinted after every group's; and the leg is `emit_stacked_verify` over one point per column, each page's own columns gathered at that page's own reduced point — the same gather `prepared_claims` performs, so the opening proves the pinned commitment takes exactly the values those tables settled on, with no separate equality anybody has to remember to write. ⛔ THE DENSE SET IS READ OFF THE OPENING, NEVER RE-DECIDED. Re-running the threshold in the emitter is the one way this leg goes silently unsound: a program could then skip a `check_preprocessed` the opening does not cover. `GlobalPlan::build` reads `GlobalPrepared.at` and refuses any shape it cannot mirror — a run that is not a genesis page's whole preprocessed prefix, a table visited twice or out of stack order, a settled table the route table calls a bookend or a private page. ⛔⛔ AND EVERY PREPROCESSED COLUMN IS COVERED EXACTLY ONCE — settled by the stack XOR checked by a closed form — asserted by a pass OUTSIDE the match that produces the routing. Written inside it, the check would restate its own expression and could not fail. The failure it exists for is a page that falls between the two routes: no value is wrong, the program is merely shorter, and every value gate stays green because there is simply no check. The F1 gains the prepared leg and its constants, and its body becomes a helper so the DENSE bundle gets the same comparison — without it the three forms the prepared path adds would be written and never read, which is the shape of defect that left seventeen tests green over a deleted preprocessed leg. Also here: W1h's dense-genesis arm, the only fixture that reaches the opening at all, with an anti-vacuity check on the state it exists to reach; the guest comment rewritten around the two-part rule, naming the tree it was read at; and the cross-epoch driver's module header, which said the proof carries no prepared opening and went stale because of this change. The sparse path is unmoved by construction: every new cost term is zero when the proof carries no opening, which is every fixture but `dense_data_page_touch`.
`a_candidate_the_chain_cannot_be_paid_for_stays_sparse` asserted the same quantity twice: once derived, `plan.savings == 2_034 - BLOCK_MARGINAL`, and once as the bare literal `1_931`. The form charges 111 where the retired literal charged 103, so the derived side moved to 1,923 and the bare one did not. Gate-2 read `left: 1923 / right: 1931`. ⛔ THE LITERAL NAMED NO SYMBOL, WHICH IS WHY IT SURVIVED. Re-pointing the rule at the form was done by sweeping for `GENESIS_PAGE_MARGINAL_ROWS` and `MARGINAL_MEASURED_AT_VARS`, and this line mentions neither: it is `2034 - 103` with the subtraction already done. A symbol sweep cannot see a number that has been folded, and that is the lesson worth keeping — after the sweep, sweep again BY VALUE, recomputing each candidate from the new form. That second sweep is now run and recorded: over `continuation.rs`, `whir_chain_tests.rs`, `tests/multilinear_continuation_tests.rs` and `lfm/preprocessed.rs`, every quantity the retired 103 could have produced was recomputed under the form and searched for in all three spellings (plain, Rust underscores, prose commas). The 112-entry savings is the ONLY stale one, in this assertion and in the doc sentence above it. The 5,000-entry savings, the block's savings, the 65,652 savings and the densest-sparse bound are clean — they were re-pointed with the rule. Every hit on 9,730 is the LONE page's pair, which the form leaves where it was. ⇒ THE FIX IS ONE DERIVATION WITH THE VALUE IN THE MESSAGE, not a corrected literal. A number a reader wants is a message; a second assertion of the same quantity is a thing that drifts, and drifts silently until the day the first one moves. The doc sentence above the test paired a 111-row marginal with a 1,931-row saving, which could not both be true; it reads 1,923 now.
`the_block_bundle_builds_its_cross_epoch_program` built the cross-epoch program at the block's shape and printed its size, but nothing in its output said WHICH ROUTE the genesis took — the reading the hybrid's ruling is actually quoted by. A box run could only infer it from the instruction count: sparse-only would be over 10 M in INIT alone and the emit-time cap would have refused the build outright, so a number inside the ruled band implied the stack had been taken. An inference from an absence is not a reading. The line now carries `prepared <rows> over <n> dense pages at n_stack <vars>`. Nonzero rows mean the opening was taken; zero means every genesis page went to the closed form, which is every fixture but `dense_data_page_touch`. ⚠ READ OFF THE DRIVER'S OWN RECORD, NEVER RE-DERIVED. The page count and the stack height come from `WhirRealGlobal::prepared`, which is what the VERIFICATION consumed. Evaluating the threshold a second time here would be a second opinion about a decision already made, and the two could disagree with nothing in the output to say which one was the run's. A println in an `#[ignore]`d box arm: no program text moves, no proof moves, and no fixture-scale gate can see it.
`two_pages_worth_less_than_the_chain_apiece_share_one` held `assert_eq!(plan.savings, 179_830)` one line under the derived `assert_eq!(plan.savings, 2 * alone)`. 179,830 is 2 × 89,915 — the retired constant's `alone` DOUBLED — so re-pointing `alone` to 89,907 left its double behind and the box read `left: 179814 / right: 179830`. ⛔ THE CLASS IS THE SAME AS THE REFUSED CANDIDATE'S AND THE SWEEP THAT CAUGHT THAT ONE COULD NOT SEE THIS ONE. That sweep recomputed every BASE quantity the retired 103 could produce and searched for its stale value. A MULTIPLE of a base quantity is a different number: 89,915 appears nowhere here, 179,830 does. ⇒ after a form moves, sweep its SUMS AND PRODUCTS too, not only its terms. The extended sweep is now run — every base quantity times one through four, and every pair-sum, in three spellings, over the four files that name the rule — and this is the ONLY further hit. Two families were checked rather than assumed: the lone page's boundary reads 9,730 in several places and is CORRECT, because at that bracket the form charges 101 and the pair genuinely is (9,730, 9,731); and 180,036 = 2 × 90,018 is two SPARSE LEGS with no marginal term in it, so it does not move at any value of the form and stays as the retired rule's contrast. The fix is the same shape as the first: the literal goes, and the sum rides in the surviving assertion's message beside the per-page figure it is twice.
…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.
Two checks for a device build, so a host fallback cannot pass as the device: - the head helper's device stamp says whether the device took the warm-up (`BASE HEAD: device warm-up` or `... declined`), since a decline is silent by design (the prove then builds the same state on demand); - `the_head_decode_root_is_committed_on_the_device` (cuda): the 4,097- instruction DECODE map, 8,192 rows at blowup 2 and so above the device's commit floor, moves the device group counter and still gives the host root. The counter is process-wide, so the test is run on its own.
The ZfFormat::DEFAULT doc quoted a block timing for whir_grind=query from an earlier measurement. A measured number in a comment goes stale, so the doc now says what the lever does and why it loses no proven bits. The same reasoning in whir_chain's module header, GrindBits::query_only and WhirGrind gave the out-of-domain grind's reason as "it follows the out-of-domain point". That is half of it: the grind sits right before the batching challenge and does guard it. Dropping it costs nothing because the batching challenge has far more bits than the target without any grind. Comments only.
the_inner_node_verifies_two_leaf_nodes needs FAN_IN^2 = 4 epochs and took FIXTURE_EPOCH_LOG2 - 1. Since 8f9aef1 moved the fixture to the 48-cycle continuation-fixture at FIXTURE_EPOCH_LOG2 = 5, that is 16-cycle epochs and three of them, so this box-tier test has stopped at its own epoch-count assert in setup, before proving anything, under either wrap attestation. A pre-existing fixture drift, found by the gates at e413989. Two below the shared constant is safe by an assertion the suite already holds: the_fixture_guest_commits_in_an_intermediate_epoch keeps the guest above one shared epoch and within two, so 8-cycle epochs give at least five (six today), where 16-cycle ones give three or four.
…le v2) Job 202's NICE arms lost 9.65 s at STARK level 0 while their mechanism moved the right way (level-0 held time -5.4 s). The cause was the one host-phase pool shared by the six level-0 workers: every whole host phase was an injected job there, and a rayon thread blocked in a join runs injected jobs before it returns to its own (rayon-core 1.13 wait_until_cold). A thread waiting inside one wrap's reconstruct ran other wraps' whole phases nested on its stack, so the reconstructs that started first finished last (2-3 s became up to 22 s) and the card sat with no holder for 17 s of the level. host_phase now installs into a pool of the CALLING thread's own, built at its first host phase and dropped with the thread. A worker runs one phase at a time, so its pool only ever holds that phase's jobs; a caller that is already a rayon worker runs the phase inline. Each pool prints one line naming its caller and how many of its threads took the nice value, counted after every thread has started. Knob unset: inline, as before. Tests: two callers' phases never share a thread (with the shared-pool design as the control, which puts both on the same threads); a caller reuses its own pool; a rayon worker runs a phase inline; unset runs on the caller; a new pool reports every thread.
A table outside the device-only envelope downloads its whole main and aux LDE inside its commit, on the driver that would otherwise submit its next table. At the 2^19 default the STARK block's base downloaded 39.74 GB that way (8.08 s of driver time), most of it KECCAK_RND and ECDAS tables of 1,480 and 521 columns whose device paths already run: they sat outside the envelope by row count alone. At 2^16, with the barycentric floor (trace >= 2^14 rows) below it, the base downloads 7.27 GB and the block proves 1.40 s faster (FAST job 206, ds850-861, two arms each: wall -1.40 s, base -1.10 s; program ids unchanged, the root verified). `LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD=524288` restores the 2^19 envelope. The default is process-wide, so the WHIR pipeline's recursion proofs (FRI STARKs through the same gate) take it too; that pipeline was not measured.
The head helpers (DECODE committed on the device, the first prove's domain, twiddle and staging state built beside epoch 0) become the default: `LAMBDA_VM_BASE_HEAD_AHEAD` unset, empty or `1` runs the head ahead, and `0` is the named opt-out that runs the serial head as before. FAST job 206 (ds850-861, two arms each against the serial head): the head 2.4 -> 1.0 s, the first prepass 0.37 -> 0.00 s, the base -2.00 s, the block -1.45 s; program ids unchanged, the root verified. The switch's test now pins the new reading (ahead unless exactly `0`); the equivalence test still proves both heads by parameter.
… by default The level-0 lead-in's prologues put parallel work on whatever pool they run in while the base still proves its last epochs, and the base's per-table drivers, plain OS threads, queue their own parallel iterators behind it in the global pool: the host-only OOD absorb summed 5.2-5.3 s over split 9's tables in all three G1 arms. In a pool of 16 threads of their own (FAST job 206, ds850-861, two arms each against the global pool) the base's worst split absorb fell to 0.04 s, the base by 2.35 s and the block by 2.20 s, level 0 +0.05 s; program ids unchanged. The pool now belongs to each `LeadIn`, sized by its caller: the STARK tree defaults to `STARK_TAIL_THREADS` (16); the WHIR tree keeps the global pool, its tail not having been measured in one. `LFM_TREE_TAIL_THREADS` overrides either (`0` is the global pool, the named opt-out; a count, a pool of that size), and the line naming the choice is printed where the lead-in starts. The rationale no longer says the prologues' verify fans out over the pool; what is established is that isolating them removed the stalls. Tests: the switch over each pipeline's default; a lead-in with a pool of 3 builds its prologues on that pool's threads and one without a pool does not (routing the prologue around the pool fails it).
…ries the_inner_node_verifies_two_leaf_nodes checked the composition property, that a node's published schema does not change with its level, as inner_layout.total() == leaf_layouts[0].total(). A node publishes its last child's output halves (emit_node_publishes), so that compare also required the FIRST leaf's carried output to be as long as the LAST leaf's: a fact about which epoch committed, not about the level. It held while neither leaf's last epoch committed. At the 8-cycle epochs the gate now runs at, the fixture commits in epoch 1, the first leaf's last, so that leaf publishes 146 words against the inner node's 144, under either STARK wrap attestation. Compare the words the two proofs published instead, the inner node against the last leaf, whose output halves it carries. The compare of two layouts built from the same count could not fail; the published counts can.
LFM_TREE_TAIL_THREADS now also takes `per-helper:<n>`: each lead-in helper builds its prologues in a rayon pool of n threads of its own. The default does not change (one shared pool of 16 for the STARK tree, the global pool for the WHIR tree), and `0` is still the global pool. Why: each helper installs a whole prologue, with joins inside, into its pool. A pool thread waiting in a join also takes injected jobs, so in a pool two helpers share it can run the other helper's whole prologue nested on its stack and finish its own only after that one; F-PREP measured that inversion on level 0. With one pool per helper, each pool has one caller and the inversion cannot happen. A per-helper pool of no threads is refused (rayon would read 0 as every core). A test checks that two helpers building at once run on two pools, each prologue on one pool of the per-helper width. Routing every helper to the first pool fails it.
Conflict in prover/src/zf_format.rs resolved by keeping both defaults: one_row=auto (the STARK pipeline's measured setting) and whir_grind=query (P2-W, which changes no STARK proof). The default banner is now cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 whir_grind=query.
…elper by default The STARK tree's default for LFM_TREE_TAIL_THREADS is now one pool of 8 threads per helper, the same 16 threads the shared pool had. LFM_TREE_TAIL_THREADS=16 is the named way back to one shared pool, and 0 is still the global pool. The WHIR tree keeps the global pool. A pool per helper has one caller, so a pool thread waiting inside one prologue can no longer run the other helper's whole prologue nested and finish its own late. FAST job 2115 (ds884-887, S P P S, two arms each) measured the per-helper pools against the shared pool: - wall +0.30 s, base -0.20 s, level 0 +0.70 s; - all inside the 0.8 s noise, and program ids unchanged. The only prologue it slows is the lead-in's last, which runs alone: 5.4-5.5 s on 8 threads against 3.9-4.1 s on the shared 16.
…by default STARK block ABBA: -4.15 s (EFFECTIVE). LAMBDA_VM_STARK_WRAP_FOLD=1 restores the in-guest fold and today's program ids byte for byte. Also repairs the box-tier inner-node test (a quarter-epoch fixture tree; the compare against the leaf it carries), whose failure was pre-existing at 8934b59.
…ad-in Head ahead (LAMBDA_VM_BASE_HEAD_AHEAD), the device-only envelope from LDE 2^16 (LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD) and the tree's lead-in prologues in their own pools, 8 threads per helper (LFM_TREE_TAIL_THREADS). STARK block ABBA: -5.05 s (confirmed); per-helper pools NO EFFECT against one shared pool.
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.
LAMBDA_VM_GAP_PREP_NICE now defaults to 10: the tree driver's reconstruct, emit and harvest and every LFM prove's execute and fill run on a pool of the calling thread's own, its threads at nice 10, so the proof holding the card keeps the CPU. LAMBDA_VM_GAP_PREP_NICE=0 is the opt-out and restores the schedule before the knob; 1..=19 picks another value. Measured at bbdac70 on FAST (F-PREP job 224, ABBA, one binary): the STARK tree took 1.55 s less (A 73.8 / 73.7 s, B 72.4 / 72.0 s). Level-0 card holds shrank 4.15 s; the card waits 2.49 s longer for the next wrap's host work. No wrap's reconstruct slowed past the stall guard (3.27 s against 6.26 s). Proofs are unchanged: a host phase moves where execute and fill run, not what they write (trace_identity_tests::execute_and_fill_on_the_host_phase_pool_are_byte_identical). The lead-in's prologues are untouched: they run in F-SIDLE's per-helper pools and never go through host_phase.
MauroToscano
changed the title
MauroToscano
changed the title
…GPU_COMPILED_CONSTRAINTS) The STARK quotient's constraint_composition_kernel is an interpreter. For every node of every row it: - loads the node; - decodes its operands; - reads them from, and writes the result to, a per-thread slot file in global memory. The slot file caps its grid at 65,536 threads, which is 0.30 waves on the 5090. G5's ncu of a base launch reads 77 % of L2, 30 % issue and 26 % occupancy: memory- and latency-bound on the interpreter's own traffic. The kernel takes 1.53 s of the STARK base's wall and 1.23 s of the recursion's (G1). This adds a straight-line twin of that kernel for every production program of at most ~4 k nodes: - the VM tables, the per-epoch local-to-global table and the LFM chips; - 36 kernels in all; - KECCAK_RND, ECDAS, ECSM and KECCAK stay interpreted. Each node becomes the call eval_program_row makes for its op, operand kinds and result class, over local variables, with no slot file and a grid that fills the card. The transition sum adds the roots in root order, and the boundary tail is the interpreter's own. Goldilocks values on the device are non-canonical u64s, so this exact mirroring is what makes H bit-identical. stark::constraint_ir::codegen emits the kernels, keyed by a structural hash of the lowered program. The prover crate's tests::compiled_constraints generates crypto/math-cuda/kernels/constraint_compiled.cu and its key table, and fails when the committed source is stale. math-cuda loads the module on first use. A program with no kernel, or a module that cannot load, runs the interpreter. LAMBDA_VM_GPU_COMPILED_CONSTRAINTS=1 turns it on. Unset or 0 keeps the interpreter, the default. Anything else stops the run. Evidence: - The host build of both CUDA sources (crypto/math-cuda/kernels/tools/ccomp_host_check.cpp) agrees limb for limb on all 36 programs, over random full-range inputs. - Three deliberate generator faults each fail every one of the 72 runs. - The freshness test fails on a one-character edit of the generated source. - Device tests compare the two kernels on the card and prove a program both ways, byte for byte.
…aces, with a mutation control `the_compiled_kernels_prove_the_same_bytes` proved add.elf three times through `prove_with_options`, and its control (two interpreter proofs) failed on the card: two builds of one program's traces differ. The LT, BRANCH, MUL, DVRM, EQ and BYTEWISE builders deduplicate through a std HashMap and lay rows out in its iteration order. On the laptop, two builds of add.elf's traces give different LT rows and different proof bytes. The test now builds the traces once and proves copies of them (`FixedTraces`, `prove_with_options`' prove step on a clone), at grinding 0: - the control: two interpreter proofs, byte-equal; - the compiled proof: byte-equal to them, verified, with compiled compositions counted; - the mutation control: BITWISE's kernel swapped for a mutant whose last root is off by one. The proof must change and fail to verify, or the prover must refuse it, and the mutant must have run. `one_set_of_traces_proves_the_same_bytes` runs the control alone on the path the build proves on (ignored: two proves at blowup 4). Supporting changes: - `Traces` derives Clone in this crate's tests only. - codegen: `mutant_composition_kernel` (the kernel plus one wrong statement) and `mutant_kernel_name`. - The generated source carries BITWISE's mutant last. It is not in the key table, so no program runs it. - gpu_interp: `substitute_compiled_kernel` and a call counter, compiled only under stark's `test-utils`, launch a named kernel in another's place. The 36 production kernels and the key table are unchanged.
LAMBDA_VM_GPU_COMPILED_CONSTRAINTS unset, empty or 1 now evaluates every composition that has a compiled kernel with it; 0 keeps the interpreter for every program. The banner names the setting either way. FAST job 260 (block 25368371, A B B A at 422c4b2): whole run 61.05 s with the interpreter, 60.25 s compiled (-0.80 s; base -0.70 s), identities equal in all four arms; the kernels run 2-3.8x faster than the interpreter per program at 2^20 rows. The proofs are byte-identical: the device parity test and the proof-bytes test with its mutation control passed on the card.
MauroToscano
changed the title
MauroToscano
added a commit
that referenced
this pull request
Sep 30, 2026
…st the epoch base A script for the counter-enabled RTX 5090 machine (run by its owner, text back only), forked from mauro-ncu.sh. One build at the recommit-span commit runs #1009's epoch base (its control test) and the no-epoch block proof with packing admission: an unprofiled reference of each; Nsight Systems with GPU metrics, per-stage tables from the prover's NVTX ranges (head, main commit, fused, the recommit), the kernels each range launched, CUDA API seconds per category, thread and stage, and a time series; Nsight Compute config and window passes on the RPX leaf and Merkle, NTT, compiled constraint, DEEP and FRI kernels for both workloads. The bundle is scrubbed, self-checked text with a SUMMARY.md. NP_DRY=1 validates everything but ncu on a box whose counters are closed.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
…st the epoch base A script for the counter-enabled RTX 5090 machine (run by its owner, text back only), forked from mauro-ncu.sh. One build at the recommit-span commit runs #1009's epoch base (its control test) and the no-epoch block proof with packing admission: an unprofiled reference of each; Nsight Systems with GPU metrics, per-stage tables from the prover's NVTX ranges (head, main commit, fused, the recommit), the kernels each range launched, CUDA API seconds per category, thread and stage, and a time series; Nsight Compute config and window passes on the RPX leaf and Merkle, NTT, compiled constraint, DEEP and FRI kernels for both workloads. The bundle is scrubbed, self-checked text with a SUMMARY.md. NP_DRY=1 validates everything but ncu on a box whose counters are closed.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
…st the epoch base A script for the counter-enabled RTX 5090 machine (run by its owner, text back only), forked from mauro-ncu.sh. One build at the recommit-span commit runs #1009's epoch base (its control test) and the no-epoch block proof with packing admission: an unprofiled reference of each; Nsight Systems with GPU metrics, per-stage tables from the prover's NVTX ranges (head, main commit, fused, the recommit), the kernels each range launched, CUDA API seconds per category, thread and stage, and a time series; Nsight Compute config and window passes on the RPX leaf and Merkle, NTT, compiled constraint, DEEP and FRI kernels for both workloads. The bundle is scrubbed, self-checked text with a SUMMARY.md. NP_DRY=1 validates everything but ncu on a box whose counters are closed.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
…t TABLE_PARALLELISM=8 The current noepoch/stark head (kept top levels rebuilt in parallel, still behind its knob) and i-noepoch's latest arm posture: nm-ab.sh's base env with TABLE_PARALLELISM=8 plus packing admission for the no-epoch arm; the epoch control stays at 4, #1009's record.
…s root check Ported from #1013 (1b4bb4a's stark half, and a4f1cb9's choice of the last column for the recommit fault hook), so #1009's cross-epoch global proof can run under it. Round 1 commits every table on the device and keeps only its root: the device LDE, tree and trace snapshot are freed inside the admitted region, so no table's buffers outlive its admission. At the top of each table's fused task the trace is committed on the device again, with Retain's function and device-only gate, and the prover refuses the proof with RecomputedCommitmentMismatch unless the new root (and the precomputed root) equals the absorbed one. From there the task is Retain's, so the proof is the same bytes. Tables the device declines in Round 1 keep their host tree and recompute on the host, as RecomputeLde does. Retain and RecomputeLde are unchanged; the PROVE SPLIT line gains recommit[Σ] only when a recommit ran. Tests: byte identity with Retain and the aux release on any build; on the card (ignored), every table recommitted and a moved trace refused for each table.
The global proof has one table per epoch and one per touched page. Under Retain every table's Round-1 LDE, tree and trace snapshot stay on the card until its fused task, outside the VRAM gate, and from 108 epochs Round 1 ran the card out (the BIG block ladder: a CUDA OOM in this proof's main commit at 108, 135, 142 and 143 epochs, with no host path). Under RecomputeLdeDevice Round 1 keeps only each root, and each fused task recommits its table on the device under the gate, its root checked equal to the absorbed one. The proof is the same bytes. LAMBDA_VM_GLOBAL_RESIDENCY=retain restores Retain (the A arm of the A/B, and the way back); unset, empty or `device` is the new default; anything else stops the run. The mode is named on stderr once per process. Tests: the setting's parse (host). On the GPU box, from one execution's boundaries at the block's options: two Retain global proofs equal (the control), the RecomputeLdeDevice proof equal to them, recommitted on the device and verifying, and the largest table's trace moved before its recommit refused with RecomputedCommitmentMismatch. A block-base arm for the A/B prints the global proof's sha256 and verifies the bundle.
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.
What made it fast, ranked
These are the optimizations that took block 25368371 from 104.2 minutes to 60.18 s on this pipeline (35.95 s on the
WHIR one, #1010), ranked by the speedup each measured when it landed. Each row is its own before/after at that
time, so the rows do not add up.
¹ The move also changed the hardware, from a CPU box to one RTX 5090 on a Ryzen 9950X host.
² On a Ryzen 9950X + RTX 5090 box. The base alone fell from 156.3 to 67.9 s.
107.45 s, STARK 157.45 → 121.65 s. On STARK the caps add no wall on top of the 2^d folds, though they remove
another 1.4 M permutations.
161.4 s, 18 Sep), and is 1.67× faster today (35.95 against 60.18 s). Rows 6, 9, 10 and 12, and most of 14, are
WHIR-only; rows 7 and 15 and the one-row openings are STARK-only.
14.7× and 8.8× on 28 Sep.
The number
Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21, fan-in 2. At this
head,
cc411aa2c, the compiled kernels' four arms in the last two A/Bs read 60.4, 60.1, 60.4 and 59.8 s (mean60.18 s). They were measured at
422c4b2acwithLAMBDA_VM_GPU_COMPILED_CONSTRAINTS=1, the code this head runs bydefault. The record launchers leave the device memory pool at the code's default, retained (open decision 4). Host
peak 20.6 GiB.
Each step below is its own ABBA on one binary: two arms per setting, alternated.
cap=auto fri=dp one_row=auto)946ca6045f2967e199(pool retained in both arms)f2967e199→ the MDS fix and NICE v2 (37d819add)¹¹ Two builds, alternated X Y Y X: the MDS fix has no knob.
² Two ABBAs on one binary at
422c4b2ac(jobs 260 and 261), pooled; the knob's setting is the only difference.In the gap-fix row's A arms, every fix of the next table is switched off by its opt-out. Their program ids and census equal
those before the batch (
a9defee79). The B arms' ids equal those of the arms that first measured the BITWISE drop andthe LFM_HASH split together. Census, arm 1 and root: 8,175,510,048 → 6,054,930,976 cells (−26 %).
Measured against the code before the batch, in one job, the batch is −24.45 s. That job alternated three arms:
946ca6045) with its opt-out set: 106.70 s;The previous head's A arms and that head's B arms, taken from the two ABBAs, give −25.35 s. The gap-fix row's −28.75 s
overstates the batch, because its A arms run that head's build, which is 3.25 s slower than the previous head's with
the same fixes off:
the measured wall includes, and the replay. Each is 15–25 % slower per item. The base, the global proof and the
interior proofs take the same time.
apart, and every arm of a build sits at the same one. This head's build is at the higher.
stay 1.20. Code placement is the likeliest mechanism [inferred].
A fifth arm, the defaults with only the level-0 lead-in off, read 81.7 s. So the lead-in is worth −2.90 s here, net of
the 3.4 s it adds to the base. The WHIR PR (#1010) measured the same batch at −39.65 s (99.85 → 60.20 s).
The gap fixes on this pipeline
Each fix was measured first in its own ABBA, on the base before the engine. Those rows do not add up to the cumulative
−28.75 s; the gap-fix row above is the measurement.
LAMBDA_VM_RPX_LIMB_PERMUTE=0LAMBDA_VM_STAGING_SHARED_SLAB=1program_idfold is a keccak permutation, which sends it lookupsLAMBDA_VM_LFM_KEEP_BITWISE=1LFM_TREE_PROLOGUES_AT_LEVEL0=1946ca6045LAMBDA_VM_LFM_HASH_SPLIT=0LAMBDA_VM_BASE_PREP_ON_PROVER=1LAMBDA_VM_RPX_WARP_MERKLE=0LAMBDA_VM_DEEP_INV_LEGACY=1LAMBDA_VM_RPX_GRIND_QUEUE=0EpochConstants::loadtakes the DECODE commitment the base already derivedLFM_TREE_REDERIVE_DECODE=1The rest of the batch is in the code but does not run on this pipeline:
The WHIR PR (#1010) describes them. The LFM_HASH split is the one per-pipeline default: it costs +2.80 s on the WHIR
pipeline, so #1010 keeps it off.
The wraps attest their program id host-side (R1b)
What changed. A STARK wrap used to fold its program id in-guest with keccak over the epoch's attested inputs. It
now takes the id computed when the program is emitted and asserts every input it consumes equal to a program constant.
by 1,051 M cells.
e413989e1): −4.15 s against a pre-registered −4.2 s.Soundness (
prover/src/lfm/SOUNDNESS.md§6.9). Every value the fold attested is now a program constant the wrapasserts. A forged ELF digest,
pc_startor DECODE constant has no wrap execution, and a tampered cell is refused(tests). The opt-out,
LAMBDA_VM_STARK_WRAP_FOLD=1, restores the in-guest fold and today's program ids byte for byte.Less idle card in the base and the lead-in (F-SIDLE)
What changed. Three scheduling changes. No proof byte moves.
there (the same root;
multi_proverefuses one that differs) and prewarms the twiddles and staging buffers.LAMBDA_VM_BASE_HEAD_AHEAD=0opts out.device paths never read.
LAMBDA_VM_GPU_DEVICE_ONLY_THRESHOLD=524288opts out.base's work, and one helper's prologue cannot run nested inside the other's wait.
LFM_TREE_TAIL_THREADS=0gives theglobal pool.
920c849e5). One pool perhelper against one shared pool read no effect (+0.30 s); it was kept because the shared pool can stall.
MDS fix and NICE v2
What changed.
core::array::from_fnclosure. They are the block path'slfm::rpo::Rpo256::mdsandcrypto::hash::rpx::mds.mds's ownunit. Otherwise every lane was an out-of-line call that recomputed
(j − i) mod 12with a 64-bit multiply per term:about +12 % instructions and +24 % multiplies per permutation.
production, wrap and node verify and on the replay, decided by unrelated edits.
the card keeps the CPU. Those phases are the reconstruct, emit and harvest, and every LFM prove's execute and fill.
LAMBDA_VM_GAP_PREP_SCOPEand_AHEAD.Measured on block 25368371 (FAST, one job per row):
37d819addagainstf2967e199(X Y Y X, ds940–943)37d819add: level 0 −4.35 s, interior −0.75 s, base −0.10 s. F-SIDLE's lead-in alreadytook most of the base window's verify work off the critical path.
0.60 s. A single-thread probe of the RPX permutation, run inside each binary, reads:
37d819add). Thelevel-0 holds shrink by more: the build holds go from 6.14 s to 4.15 s.
Soundness: nothing a proof commits to changes.
along with seven FB rounds = RPO256, the two implementations' agreement test, and a new test against the circulant's
definition. Transposing the matrix fails six of them.
(
trace_identity_tests::execute_and_fill_on_the_host_phase_pool_are_byte_identical).Opt-out.
LAMBDA_VM_GAP_PREP_NICE=0restores the schedule before the knob: host phases run where they are called.LAMBDA_VM_GAP_PREP_NICE=1..=19picks another nice value.Compiled constraint-composition kernels
What changed.
program's IR (
crypto/stark/src/constraint_ir/codegen.rs→crypto/math-cuda/kernels/constraint_compiled.cu, 36programs, keyed by a structural hash of the program).
per-thread slot file in global memory. That file caps its grid at 65,536 threads, 0.30 waves on the 5090, and binds
it on L2 (ncu: 77 % of L2, 30 % issue).
with a grid that fills the card.
every LFM chip except LFM_KECCAK and LFM_BLAKE3. Any program without a compiled kernel keeps the interpreter. The
largest compiled program is LFM_HASH (3,905 nodes).
LAMBDA_VM_GPU_COMPILED_CONSTRAINTS=0restores the interpreter for every program, and any valueother than
0or1stops the run. A banner names the setting, and each distinct program prints one line sayingwhether it ran compiled or on the interpreter.
Kernel speed (2^20 LDE rows, median of 5, interpreter ÷ compiled; FAST jobs 247 and 260):
Measured on block 25368371 (FAST, arms A B B A, one binary at
422c4b2ac; A = the interpreter, B = compiled):but composition is a small share of the card's time. Most of the gain lands in the base (−0.68 s).
Δ < 0 with every B arm below every A arm. Both hold.
reader now rounds to 0.01 s before testing the threshold. That boundary reading is why the replication was run.
Soundness: the proofs are byte-identical. A compiled kernel computes the interpreter's
Hbit for bit: the samefield operations, in the same order, on the same operands.
all equal limb for limb.
row, and no roots added.
Hequals the interpreter's on the 5090: 4,096 rows, framestep 4, two seeds, every program.
add.elfis proved from one set of traces at grinding 0.trace builders order some tables' rows by
HashMapiteration, so two separate trace builds never give equal proofs.fails verification.
compares one compiled kernel inside a proof. The gates rerun it with the floor lowered to 16 LDE rows: 8 compiled
kernels (CPU, DECODE, LT, MEMW_R, MEMW_A, BITWISE, REGISTER, KECCAK_RC) and one interpreted program give proofs
byte-equal to the interpreter's (see "Gate and CI"). The device parity test covers all 36 kernels.
and 63 on the interpreter.
constraint change without a regeneration cannot ship a stale kernel.
What is in the branch
and nodes, one root for the block.
main's Feat/skip empty tables #977 empty-leg elision andthe WHIR pipeline itself, which the STARK driver does not use.
ZfFormat(prover/src/zf_format.rs) parses sixLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT:banner. The default here iscap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27. Each lever alone, ABBA against legacy:are unchanged: −15.35 s.
−8.00 s and 7–8 GiB of host memory on their own. They cost +3.2 s on the WHIR pipeline, which keeps them off
(WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010).
whir_stackis the WHIR pipeline's lever; only the WHIR layouts read it, so no STARK proof depends on it.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), shared with the WHIR PR (WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010).as fit in 60 % of L2 at a time, 4 to 8 butterfly levels per launch, so a 2^22 transform is three passes. Its output
is column-major, so the commits lose their transpose.
rows) stay on the old path.
LAMBDA_VM_LDE_LEGACY=1sends every LDE back to the per-level pipeline.d1dc45514) is merged in, over three signed merges of its candidates: C2(
7d416688a), C3 (41549ebad) and C4 (d1dc45514).(
chunking::HASH_SPLIT_DEFAULT = true).zf_format.rs: this PR'sone_row=autodefault and the newwhir_stacklever, both kept. The other two merged clean.
f2967e199, all signed): WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010's P2-W (b4506b719, merged asebbba834d; one conflict inzf_format.rs, resolved by keeping this PR'sone_row=autoand addingwhir_grind=query), R1b (add21183c, mergedas
13d926774) and F-SIDLE (d1d443b65, merged asf2967e199).fix2/prep-ahead(bbdac70b2), merged asfaddcfe27, and37d819add(NICE v2 thedefault).
e2ab35935(the generator, the 36 kernels behindLAMBDA_VM_GPU_COMPILED_CONSTRAINTS, default off),422c4b2ac(the proof-bytes test from one set of traces, with amutation control) and
cc411aa2c(compiled by default;=0opts out): this head.main: perf(alloc): compile jemalloc's never-purge policy into the binary #996.Soundness
Query counts, grinding bits 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.
index is uniform over the whole domain. Preprocessed tables use one-row static roots at blowup 4; a missing root is a
proving error.
The gap fixes
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. The re-blessed registry rows hold under thisPR's
one_row=autodefault too.program_idand never read from a proof.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;
H, bit for bit — host parity on 36 programs × 2 seeds, deviceparity on the card, proofs byte-equal to the interpreter's with 8 kernels in one proof, and a one-node mutant that
the verifier rejects (see their section).
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);Security level
Under pil2-proofman's accounting (BCHKS25 Johnson-bound bounds, minimum over phases), every phase of every proof in the
block was ≥ 128 bits. The weakest was the batching phase of the fan-in-2 interior nodes, at 128.009 bits. That audit ran
before this batch and with one-row openings off. The BITWISE drop and the LFM_HASH split only remove or shrink tables
and change no query count, grinding or blowup; they were not re-audited. The later fixes, the compiled kernels
included, change no proof byte.
Fixed along the way
tables. It rejected honest one-row proofs that publish values.
Gate and CI
The compiled constraint kernels were gated at this head,
cc411aa2c, on the FAST2 box, in two jobs: every step greenbut one of job 171's, which job 172 settled:
switch's unit tests, stark's suite on the card build (408), freshness, coverage and device parity, the proof bytes at
the default floor, the whole
cuda_path_integrationsuite at the default (7 passed, the compiled banner, 56compiled-program lines), the opt-out (the interpreter banner, no compiled line), and the fallback, force-downgrade and
d=1 suites. Its one red step reran the bytes test at
LAMBDA_VM_GPU_LDE_THRESHOLD=128: the test passed, but only 4kernels ran compiled, below the ≥ 5 floor set before any count (add.elf has only those tables at ≥ 128 LDE rows);
rows (at 2 or 4, HALT's 1-row trace would reach the device NTT, which refuses log n = 0). It read the pre-registered
8 compiled kernels (CPU, DECODE, LT, MEMW_R, MEMW_A, BITWISE, REGISTER, KECCAK_RC), the compiled proof byte-equal to
the interpreter's and verified, and the mutant caught.
The MDS fix and NICE v2 were gated at
37d819add, on the FAST2 box: 10 steps, all green (the lib suite 1,627 / 0 / 90, crypto 164), with the NICE opt-out end to end, the cuda default and device paths, and the RPX suites.The landing merge before it was gated at
f2967e199, on the FAST2 box (the second RTX 5090): 26 steps, all green(the lib suite 1,607 / 0 / 90). Besides the standard steps, they ran R1b's lines (the shape and attestation tests, both
settings of the leaf node, the inner node and the block root over real children) and F-SIDLE's ten.
The batch was gated at
946ca6045, on the FAST box: 81 steps, every one at its exact pre-registered count,the same counts as #1010's gate. The standard steps:
The 75 targeted lines are #1010's, except that one of them reads this pipeline's LFM_HASH split default as on. For each
switch of the last two rounds, a gate line runs each setting and reads the banner its process printed. The cumulative
ABBA in the first table ran after the gate.
In CI at
37d819add, these pass: lint, the host known-answer tests, the prover test 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), as it does on the WHIR PR. The prover shards were still running when this waswritten.
Open decisions
b4506b719). WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010 has since added the argue'sGPU tables (A1, A2+A3), pure WHIR recursion, N1′, the permit after the prep, small blocks and fan-in 5, which reach
this PR at the next sync. Both PRs carry the MDS fix. The shared defaults differ in
one_row(auto here, off in WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010) and the LFM_HASH split (on here, off in WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010). A per-pipeline default would let one PR carry both.the proof. A few bits of proof-of-work before the DEEP batching challenge would add margin, at negligible cost
(parked).
code's default: −2.00 s on this pipeline. The WHIR pipeline measured −0.45 s, inside noise, and keeps the release.
measured twice: in the lead-in's own ABBA, and in this ABBA's fifth arm (base 30.9 → 34.3 s). They likely compete
with the prover's host work in the shared rayon pool [inferred]. A dedicated pool or a later start could recover up
to 3.4 s. Not built.
37d819add(see "MDS fix and NICE v2").iteration. Sorting their rows by key makes them reproducible (built and gated: two proves byte-equal, FAST2 173), but
its A/B read +0.50 s wall, outside its null band, and it was dropped (
fix2/1009-canonical-rows@9322032fc, keptas a reference).