STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 78.80 s - #1009
Draft
MauroToscano wants to merge 1075 commits into
Draft
MauroToscano wants to merge 1075 commits into
MauroToscano wants to merge 1075 commits into
Conversation
…r/lfm-l0 Thirteen of seventeen overlapping files conflicted. Every resolution below is semantic; none is "take one side" except where stated, and the reasons are here rather than in a note because the next reader of this history is the one who needs them. ## The encoding: two branches that both reached the same version number DOMAIN_TAG was V4 on this lineage (it appended TableCounts::blake3) and V4 on main (it appended the six accelerator counts). Two different encodings, one suffix — exactly what the tag exists to prevent. Every tag, with what it was on each side and what it is now: LAMBDAVM_STARK_STATEMENT lineage V4 | main V4 -> V5 LAMBDAVM_CONTINUATION_EPOCH lineage V3 | main V4 -> V5 LAMBDAVM_MULTILINEAR_STATEMENT V1 -> V2 LAMBDAVM_MULTILINEAR_CONTINUATION_EPOCH_V1 unmoved LAMBDAVM_CONTINUATION_GLOBAL_V2 unmoved LAMBDAVM_MULTILINEAR_CONTINUATION_GLOBAL_V1 unmoved The three that moved are the three whose statement absorbs the shared per-table count list, which grew by six. The two GLOBAL tags bind no per-table counts, so nothing in their encoding moved. Every suffix is the same byte length as the one it replaces, so no length-derived constant moves with them. ⚠ MULTILINEAR_CONTINUATION_EPOCH is the one to read twice: its statement DOES absorb the count list, through the same shared helper. It is left unmoved deliberately — the WHIR epoch encoding is not this port's to version, and the one thing that would force it (binding is_final there, as the STARK statement now does) is explicitly out of scope and recorded as an owed parity question. Whoever takes that question up bumps this tag with it. RECURSION_INPUT_VERSION had the same collision and it is the dangerous one. The prefix version IS checked — recursion_archive_bytes refuses a number it does not recognise before the guest's in-place read — so an OLD blob fails legibly. What that check cannot catch is two DIFFERENT layouts sharing one number, which is what we had: the lineage's v3 is the one-epoch-proof format, main's v3 is the six accelerator fields, neither archive can read the other, and both claimed 3. Keeping either suffix would have been a silent misread at the wrong offsets. The merged format carries both changes and is v4, so every recursion guest ELF must be rebuilt; one built before the bump refuses a v4 blob rather than misreading it. ## The count list The merged count list is TWENTY-ONE, and that number was read rather than assumed: the two sides' additions are disjoint. Main's TableCounts has no blake3 field, the lineage's has no accelerator fields, and the fourteen split families are shared — 14 + 6 + 1 = 21. Each of the twenty-one reads a distinct source in Traces::table_counts (twenty Vec lengths and num_blake3_ops), so no table is counted twice. Getting this wrong in the other direction would not have failed a test: both sides of the transcript pin derive the term from NUM_TABLE_KINDS, so a double-absorbed blake3 would have moved the pin and still passed it. statement.rs keeps this lineage's shared helper (absorb_table_counts / table_count_values) rather than main's inlined loop, and the six accelerator counts are added to it. That is the whole reason the WHIR statements pick the change up for free: multilinear_continuation::absorb_epoch and multilinear_prove both call the same helper. NUM_TABLE_KINDS 15 -> 21, and the exhaustive destructure that makes a new TableCounts field a compile error moves with it. lfm/statement_replay.rs carries a second, independent copy of that number (NUM_TABLE_COUNTS) for the guest-side replay: 15 -> 21, plus the trailing is_final byte the host now appends. Nothing in the type system ties the two constants together; what catches a drift is the host-versus-machine challenge equality in lfm/algebraic_transcript.rs and its hand-written array literal, which fails to compile if one moves without the other. ## AIR sets and table counts FIXED_TABLE_COUNT 11 -> 5. The lineage's eleven minus main's six accelerators is exactly main's five (BITWISE, DECODE, HALT, KECCAK_RC, REGISTER), so the two lists agree with no residue. BLAKE3 stays a counted chip and joins main's accelerators in TableCounts::validate's at-most-one list, where its own upper bound used to sit alone. VmAirs takes main's counted vectors for the six accelerators and keeps this lineage's conditional BLAKE3. Git line-merged both models into a body that pushed the singular AIRs and then looped over the vectors; that could not have compiled, and it is why this file was read rather than merged. BLAKE3 now closes the accelerator group instead of keeping its old slot between KECCAK_RC and ECSM, because that slot no longer exists — air_trace_pairs and air_refs make the identical choice, which is the only obligation, since those two orders are the proof's sub-proof layout. ## Two of main's hunks were NOT taken, and one of its fixes was Not taken: main builds keccak_rc and register with with_preprocessed (the commitment alone) where this lineage builds both with with_preprocessed_columns (commitment plus the column generator). Taking main's would have reintroduced the defect 5e3df0c fixed — the multilinear verifier checks the precomputed columns' claimed openings, and an empty column list is checked in zero iterations, which left REGISTER's INIT and FINI prover-chosen on the WHIR path. Git reported this as an ordinary content conflict with nothing to say that one side was a soundness fix. ANY FUTURE MERGE OF MAIN MUST MAKE THE SAME CHOICE. On the production VM path every preprocessed AIR takes the columns form — bitwise, keccak_rc, register, the page AIRs, and continuation.rs's. A main-side hunk that reverts one of them to the commitment alone is a soundness regression wearing the clothes of a whitespace conflict. Not taken: prove_elfs_tests' bus harness keeps hash_pin's pinned transcript and BlockVerifier, where main's hunk used a plain DefaultTranscript and Verifier. Main's improvement to that harness IS taken — a prover failure now panics instead of returning false, so a negative test cannot pass because proving fell over. Main's target-moved recheck is rewired to the same pinned transcript as the accepting arm; on a plain one the two arms would have differed by hash as well as by target, and a rejection would no longer have been evidence about the target. Taken: main's missing count_merkle call in the field_element Merkle backend. merkle_nodes was NOT a subset of merkle on this lineage's byte path — the algebraic path's count_merkle_node_direct bumps both counters, the byte path's hash_new_parent bumped only the node one. The printed merkle figure therefore moves by exactly merkle_nodes on keccak runs. No pin reads it. ## hash_metrics: the same module, written twice An add/add conflict. Both branches independently wrote crypto's hash_metrics with the same feature name, the same Counts type and the same closing doc paragraph. Resolved as a union: this lineage's transcript counters (which is where the WHIR transcript pin is read from) plus main's perms counter and count_finalize(nbytes). Both count_finalize and count_total survive on purpose — only the byte sponges can report a byte count, so the algebraic backend keeps count_total and leaves perms alone, which is right, because perms counts keccak-f permutations. crypto/stark/src/grinding.rs takes this lineage's re-export shim. Main's two count_grinding calls are not lost: the implementation moved to crypto's own grinding.rs, where both calls already sit in the same two functions main instruments. Both Cargo.toml conflicts were the same hash-metrics feature declared identically on both sides. ## Consequences this merge is expected to have The STARK wraps' programs move, and in both directions. Empty legs are elided, and separately the LFM statement's fixed part goes from 215 to 264 bytes, so its trailing residue moves from 3 to 0 mod 4 and the Phase-A shift-3 splice statement_replay's own doc complained about should disappear. The WHIR transcript absorb totals move by six per epoch statement; the pin derives that term from NUM_TABLE_KINDS rather than carrying it as a literal, so the expected value tracks. recursion_smoke_test's keccak_permute census numbers predate this merge and are a print rather than a gate; they are flagged in place.
…s, not during E0506: `airs()` borrows the whole driver and the lie this arm tells is a field of it, so the precondition read and the restatement could not both hold the same value. The precondition now reads in its own scope and the AIR set is re-taken after the field moves. Nothing about what the arm proves changes. It still restates an INPUT — a bundle whose page is a private-input page saying the run had none — against an AIR set that is untouched, so the route expects OFFSET and INIT from a table presenting OFFSET alone.
THE REFUSAL WAS A CONFIGURATION MISMATCH, not a defect in the emitter, and the gate log said so on a line above the failures: the process ran under LAMBDA_VM_WHIR_HASH=keccak256. The machine's transcript is the ALGEBRAIC sponge — `whir_transcript.rs`' own header says the mirror is `DefaultTranscript<E, RpxTranscriptHash>` — while the cross-epoch prover and verifier both dispatch on that process-wide knob. So the bundle carried a keccak challenge stream, the machine replayed an RPX one, every challenge diverged from the first squeeze and the honest proof refused at its first table. The level-0 suite documents this exact failure at `driver_bundle` and solves it by re-proving its epochs under a literal RpxWhir; that door is shut here, because `prove_global` and `verify_global` take no hash parameter and re-implementing either in a test would be a second derivation of the cross-epoch prover. So the three executing arms are `#[ignore]`d with the knob named in the reason AND refuse when run in the wrong posture. Both halves: the ignore keeps a default run from going red over a configuration it never set, and the refusal stops a deliberate run in the wrong posture from producing a DivByZero nobody can place. A silent skip would have been neither — green in every default run, and unable to fail. A refusal now names its site. `locate_addr` maps the reported address to the instruction that wrote the cell and its neighbours, because a DivByZero is always a failing equality and the address always names the difference. THE POOL is asserted as what is provable and pinned as what is not. Two emitters intern words no cost form reports — `emit_newton_step`'s interpolation weights, and the chains' own constants, which `own_constants` says in its doc it does not name. So the words the form NAMES must all be interned, which is exact and is what a deleted leg breaks, and the unnamed remainder is pinned at the measured 24 with its source named. The total assert is gone: `ops` is defined as the total minus the other three, so given their asserts it had two sides that could not differ. Also: clone_on_copy on two Copy field elements, and rustfmt.
W1g's reading — that the INIT leg cannot be gated on `test_private_input_xpage` at all — is right, and the answer is the second fixture rather than a comment claiming coverage. So the route table now names, per arm, the run that reaches it and what that run cannot show. The part worth writing down is the third row: NEITHER fixture shows the MIX. A block carries both kinds of page at once under a sixteen-group split, while at fixture scale the page group is a singleton and shape-identical to a bookend's. So the route table's behaviour on a mixed set rests on the block instrument, and saying that is the difference between a stated gap and a false guard.
THE ARM COULD NOT HAVE FAILED, AND ITS MUTATION COULD NOT HAVE FIRED. It ran on the `data_page_touch` bundle, which reaches ONE epoch — the box read its published set as `publics 6`, which is `2 + 1 x 4`. With one epoch the pairwise-distinctness guard iterates zero times, and reversing a one-element published order is the identity, so the transposition mutation the arm exists for was a no-op against a check that was vacuous. Two of this campaign's catalogued failures from one fixture choice. `test_private_input_xpage` reaches three epochs, so both become real, and the arm now refuses a bundle of fewer than two rather than leaving the next reader to notice.
Its closing assert compared `census.len()` against the touched page count, and the comment above it called that "a count that can disagree". It cannot: the census maps one entry per config and `global_memory_configs` maps one config per base, so the identity holds by construction and no input reaching this arm could make it false. A check that cannot fail, with a comment asserting the opposite. It now checks relations between fields the census reads SEPARATELY, which is where a wrong column would actually show: a page that loads no genesis bytes must have no nonzero entries, a page cannot hold more nonzero genesis than it loads, and a private-input page — whose genesis the verifier never recomputes — must be charged none. The structural identity is stated as an argument instead of dressed as a check.
W1g's `whir/lfm-global-airs` @ 1f7a0cd into the cross-epoch program's branch: the verifier generic over the hash with the dispatch moved to its callers, `real_global_from_whir_continuation_under::<H>` beside the knob-dispatching form, the driver's fields and accessors `pub`, and the identity test guarded on the nonces its assertion can see. Clean over six files, none of them this branch's, because the route decision was moved onto `GlobalPlan` precisely so `whir_real_global.rs` would stay byte-identical while W1g worked on it. ⛔ IT DOES NOT RETIRE THE EXECUTION ARMS' `#[ignore]`. The new `_under::<H>` names a hash for the VERIFY; `prove_global` still takes no hash parameter and dispatches on the process knob inside itself, so in a default process the bundle is still PROVED under keccak and the machine's algebraic transcript still cannot replay it. The posture guard stays until the prover moves too.
THE FORM EXISTED AND COULD NOT BE USED. `sumcheck_round_consts` has always counted the pairs `(1/(j+1), -j/(j+1))` a degree-d round interns, and a count is exactly what a program-level pool cannot consume: the builder interns on the canonical word, so a degree-13 round and a degree-3 round SHARE their first two steps, and adding their counts charges four words twice. There is no scalar that composes. That is why the cross-epoch pool carried an unnamed remainder, and why `StackedCost::own_constants` could only disclaim the chains' constants rather than name them — they are these, reached through the chains' own sumcheck rounds. THE LAW that makes one call enough: the pairs NEST in the degree, so the union over every round of every leg is the set for the LARGEST degree among them. `sumcheck_round_constants(D)` is therefore a whole program's Newton pool, with D read off the shapes — the GKR ladder's 3, the reduce's 2, the chain's 2, and the tables' own `sumcheck_degree()` — and never off a proof. It returns a deduplicated SET, not a count, because these are field elements and nothing forbids two pairs colliding in Goldilocks; a collision would make the true pool smaller, and the identity against the count form is asserted over a range so that such a collision is discovered as a finding rather than as an unexplained gap. The emitter and the form now share one derivation, so the pool a program pays and the pool a form predicts are the same expression. The gate against the EMITTER therefore computes its oracle a second way, in the extension field throughout, because a test whose oracle shares the function under test agrees with itself. The cross-epoch F1 asserts its pool BY VALUE in both directions and the pinned remainder is deleted.
The harness stage below builds against `real_global_from_whir_continuation_under::<H>` and `WhirRealGlobal`'s published fields, neither of which exists at this branch's base. This is the merge that brings them.
The cross-epoch F1 found the interpolation weights interned by every sumcheck leg and named by no form. The epoch program has the identical gap and has never had it measured — no F1 there compares a pool at all, only staged row deltas — so this reads the number off the assembled program and prints it for the ladder note to aim at. It asserts what is exact and prints the rest: the Newton set through the degree the program reaches must be interned, which can fail, and the remaining constants are reported rather than pinned, because naming them is other forms' work. `interned_newton_degree` reads that degree out of a pool, which gives the cross-epoch F1 a SECOND SOURCE for a number it otherwise derives from the shapes alone. The two must agree, and a disagreement is a real finding: a leg running at a degree no shape predicts, or a form naming one no leg reaches.
…ree harness Level 0 is followed by the WHIR GLOBAL stage and the interior by the ROOT over `fan_in + 1` children, so the WHIR driver composes a block artifact rather than stopping at a closed interior and printing that it is not one. `prove_whir_global_child` is a SIBLING of `prove_global_child`, not a generalisation, and the reason is a type: that one takes the STARK `continuation::ContinuationProof` and returns `Option<(RealGlobal, RealChild)>`, while the WHIR bundle is `multilinear_continuation::ContinuationProof` and its harvest is `WhirRealGlobal`. What it produces is a plain `RealChild` — that type holds the harvest of an LFM PROOF and knows nothing about what the proof verified, which is why one child type serves both families. Four differences from the STARK stage, each with its reason in the code: - it returns `Result<_, String>` and never an `Option` the caller turns into a `return`. There is no sizing arm here and nothing to stop for, so a stage that cannot build REFUSES WITH THE REASON and the caller panics with it. Inheriting the STARK shape would end the run green having composed nothing; - no slicing, no cache and no parent: at k = 1 the published layout IS `GlobalLayout`, which is the field the driver already carries, so `GlobalPublishes` and `SlicePartition` do not appear on this path; - ONE host verify. The STARK stage verifies explicitly and then `real_child` verifies again; its three reasons are all inapplicable here, and the third is answered by taking the verify through `real_child_timed` so the stage PRINTS its seconds instead of hiding it inside a harvest; - the `WhirRealGlobal` is dropped before the interior runs. It owns a clone of the cross-epoch proof and the whole cross-epoch AIR set; what survives into the root is the child and two `usize`s. The root is NAMED, not inferred: `LFM_TREE_PROVE_ROOT=1` with `LFM_TREE_ROOT_OPTION=A|B`, which carries no default. Unlike the STARK arm it needs no cache directory — this driver caches nothing, so it proves base, level 0, the global child, the interior and the root in one run. The interior stops at `RootOption::child_level(top)`, the same named rule the STARK driver reads, and the child count is checked in the driver where the levels are still in view rather than inside `emit_l2g_compare`'s refold guard a root emission later. The knob refusals now carry one reason each. A blanket message would have survived this change and gone on saying "the cross-epoch WHIR program is not written" about knobs whose real objection is that the wrap is unsliced or that nothing here caches. The fixture arm is renamed for what it now proves: it runs the global stage, the interior at option A's child level and the root, and its "interior closes to one proof" assert becomes the option's own count guard plus the artifact's width. Two limits are stated in its doc: at `test_private_input_xpage` the cross-epoch shape is three bookends and one PRIVATE page, so the OFFSET+INIT route 30 of the block's 35 pages take has no table and no gate here; and only option A is emitted at fixture scale.
… closes THE SAME DEFECT, TWICE. `fold_coset_consts` has always counted what `emit_fold_coset` interns — `two_inv`, the `pow_bits` factors `g^(2^i)`, and each level's stride — and a count is exactly what a program-level pool cannot take, because counts ADD where values MERGE. That is why 24 words survived the cross-epoch F1's `unnamed` assert while this very fold suite was green on their number. ⚠ AND THEY DO NOT NEST, which is the difference from the sumcheck round's Newton pairs. Those nest in the degree, so one call at a program's maximum is its whole pool. These are `g^e`: round r folds over the base domain squared once per scheduled variable, so the same exponent set under a different generator gives different field elements. A program's fold pool is a genuine UNION over its distinct domains, and a form taking a maximum here would be wrong in a way the other is not. The values form also retires an assumption the count had to make. The count's own doc calls its last term 'assumed distinct from every g^e … an assumption about a discrete log, not a proof'. Deduplicating by value does not need it. The exponent set is extracted so the count and the values share ONE derivation, the chain-level union advances the domain by k squarings a round exactly as the emitter advances it, and the fold suite's existing count gate gains a VALUES arm in both directions — a word named but not interned would make a pool over-count, and a word interned but unnamed is the same gap one level down. Why the values looked like powers of two: in Goldilocks 2^48 is -1, so the small-order roots of unity are clean powers of two and 2^48, p-2^24, 2^39, p-2^60 are generator powers, not weights.
…column that is not the first The cross-epoch INIT hybrid needs a prepared commitment over the dense genesis pages' INIT columns. Those columns live one per GLOBAL_MEMORY page table, each claimed at that table's own reduced point, and INIT is preprocessed column 1 of `[OFFSET, INIT]` — so neither "which table" nor "which column" survives the `(table index, leading count)` shape `Prepared` and `PreparedCheck` had. Both now carry `at: &[PreparedColumn]`, one entry per stacked column, naming a table and one of its preprocessed columns. DECODE is the single-table prefix case and reaches it through `leading_columns`, so nothing about what DECODE means moves. No change below `crypto/stark`: `Claimed::PerColumn` has always resolved the point per column — it is what every group opening in `multi_prove` uses — so the generality was in `stacked_eval` all along. A single-table commitment produces the same weight shares under `PerColumn` as under the `Shared` it replaces, because `Claimed::point` hands back that one point for every column and `Claimed` reaches nothing but the weight; the epoch byte gate is the assertion of that rather than this paragraph. `check_preprocessed` takes the set of settled indices instead of a leading count, and `multi_verify` asserts the set is distinct — the distinctness a count got for free, and without which one stacked column could stand in for two skipped checks. The claim a prepared column is settled against is resolved through `preprocessed_source`, the same `slot_of` -> `kinds` -> `source.column` chain `check_preprocessed` walks, rather than by assuming preprocessed column `c` is value `c`. The identity does hold today — `LeafLayout::build_live_over` registers main columns first and in index order — but the opening and the skipped check must agree about which claim they mean, and one derivation is how they cannot disagree. Tests: a two-table stack over EQ's column 1 and LT's column 1, settled at the two points those arguments reduced to; the honest round trip first, then the two columns swapped at the verifier, then one column named twice. The two stacked columns are asserted to differ before anything is proven, so the swap arm cannot be a no-op.
…lter that must precede it Which cross-epoch genesis pages a prepared opening carries, as one closed form that the prover, the verifier and the in-guest emitter each evaluate from their own inputs. They must reach the same set: the stack's root is absorbed in the roots block, so two sides that disagree about it diverge at `z` and the proof dies with nothing in it that names why. A page joins when its sparse leg alone would cost more than the ENTIRE prepared leg could. That is conservative on purpose — every page that joins pays for the whole stack by itself — and it is a pure function of that page's own nonzero count, so the answer never depends on which other pages joined or in what order they were considered. The marginal-plus-fixed alternative is cheaper by a few tens of thousands of rows and buys an order-dependent set; on the block the choice is moot, because the three dense pages are 12x to 24x over the budget and the 27 zero pages are four orders of magnitude under it. `PREPARED_LEG_ROWS` is a constant and not a call because this module sits below `crate::lfm`, where the chain cost forms live. A routing rule the protocol depends on must not move with the machine's row accounting. Its provenance is V1i's measured 175,066 chain rows at 24 variables — larger than the block's 20-variable stack, so the budget errs toward leaving pages sparse — and is to be asserted where it can be computed rather than restated here. The private-input pages are filtered out FIRST, and not as an optimisation. The prover builds their configs with the private bytes and the verifier with an empty vec, so a threshold that read those bytes would select different sets on the two sides. The filter is on `is_private_input`, which both derive from `page_base` and `num_private_input_pages` — values the cross-epoch statement already binds — and the reason is that a private page presents no INIT preprocessed column to settle at all. Tests reproduce the box census of block 25368371 to the row: the three dense pages' legs plus 27 interned zeros is 10,249,056, the figure `cens2` read. The selection is pre-registered as exactly `0x0`, `0x40000` and `0x280000`, with the existing fixture's 112-entry page asserted sparse — the fixture gap, stated rather than hidden. A private page holding 20,000 nonzero bytes is asserted not stacked, and the prover's and verifier's views of that page are asserted to plan identically.
… prover can be asked which one `verify_global_bookends` stopped reading `whir_hash_knob::selected()` for itself at 1f7a0cd; `prove_global` still did, and that is what kept the cross-epoch execution arms `#[ignore]`d behind a posture guard. A function that reads the process knob can only be asked what THIS PROCESS proves under, never what hash a bundle in front of it was argued with, so a test that wanted a bundle under a named hash had to re-implement the prover. It is now `prove_global<H>` with the dispatch at its two callers, which is the arrangement `prove_epoch` and `verify_global_bookends` already have. The second reason is coming: the genesis stack is a `StackedCommitment<F, H>`, whose type names the hash, so it cannot be built outside a dispatch and handed in — the same argument that made `prove_epoch` generic so DECODE's commitment could outlive one call. In `prove_continuation` the epochs and the cross-epoch proof now share one dispatch. They read the same knob before, in two places that happened to agree; a bundle whose two halves were argued under different sponges is no longer spellable. The test this makes possible asserts the agreement in BOTH directions and without the knob: each proof is built under a named hash and checked under both, so the diagonal accepts and the off-diagonal refuses. W1g's sibling could only say that exactly one of the two accepts, and its own doc records why — under a default keccak suite a verifier dispatch pinned to keccak is indistinguishable from a correct one. The diagonal is asserted first, as the control a refusal needs, and the two proofs are asserted to differ so the four readings are not about one object. The boundaries come from `for_each_epoch` with a closure that proves nothing, which is the same walk `prove_continuation` uses and costs the execution alone. Re-deriving them would have been a second spelling of the epoch split. This retires the reason for V1j's three `#[ignore]`s on the executing cross-epoch arms. Those tests are V1j's and are untouched here.
… dense genesis pages The protocol half of the INIT hybrid. `prove_global` commits the dense pages' INIT columns as one stacked polynomial and hands it to `multi_prove`, whose roots block absorbs its root before `z`; `verify_global_bookends` recomputes the same commitment from the page configs its AIR set was built from and settles the opening through a `PreparedCheck`. Each column is settled at its own page table's reduced point, which is what the multi-table `Prepared` exists for. `WhirGlobalAirs` now carries the configs its page AIRs were built from. The verifier needs them to decide the stack's membership, and calling `global_memory_configs` a second time to get them is precisely what that struct's own doc forbids — two call sites that agree today is the shape that let REGISTER's preprocessed columns and its root describe different tables. The plan comes from `WhirGlobalAirs::genesis_stack`, so the table index a stacked column names is derived from that set's own bookend count rather than restated by a caller. ★ NOTHING IN FLIGHT MOVES. `genesis_prepared_for` returns `None` when no page is dense enough, and every existing fixture is entirely sparse — the worst is `data_page_touch`'s 112 nonzero entries against a threshold of 9,725. Those proofs absorb no extra root and are byte for byte the ones they were. Only a bundle with a dense genesis page changes, and none exists yet outside the block. So a fixture was written rather than an assertion added: `dense_data_page_touch.s` is `data_page_touch` with its touched cell surrounded by 32 KiB of non-zero bytes on each side. The fill is on BOTH sides because where `.data` starts inside its page is the linker's business — with `n` bytes either side the counter's own page holds at least `n` of them at any offset, while a single trailing fill would leave a counter near the end of a page with almost none. The floor is 32,768 nonzero entries, 3.4x the threshold, so the fixture is not sized to just barely qualify. ⚠ There is deliberately no `agrees_with` on the genesis stack. DECODE asserts its commitment's blowup and folding against each epoch's config because it is built once per ELF at a config of its own shape; this one is built per proof from the very config the same call hands `multi_prove`, so a comparison between them could not fail. The note says what a per-ELF cache would have to bring back with it, and states the cost this pays instead: one commitment over `n_dense * 2^18` elements per prove and per verify, against 10,249,056 rows of in-guest sparse evaluation. Tests: the dense fixture's plan is printed page by page and asserted to put exactly one page over the threshold BEFORE anything is proven — without that precondition the test would take the `None` path and pass while checking nothing — then the proof is asserted to carry an opening and to verify. The sparse control asserts the opposite for `test_private_input_xpage`: no opening, because a route that fired everywhere would make the "nothing moves" claim false.
…ld budget asserted where it can be computed TWO THINGS THE ROUTE OWED. ★ The provenance of the fourth per-ELF pin. The in-guest verifier cannot recompute the genesis stack's commitment, so it interns the root as program text exactly as it interns DECODE's, and the statement owed out of band is "this root is the commitment to the ELF's genesis bytes at the dense page bases, under this blowup and folding". Nothing inside the program checks it; this is the evidence for it. The test rebuilds the stacked columns from the ELF's PT_LOAD segments byte by byte and compares the roots. ⚠ The second derivation is the whole value: built through `build_initial_image_paged` or `page::preprocessed_columns` — the functions the production path uses — it would compare a value with itself and pass for any pair of agreeing bugs. It also asserts each rebuilt column carries more nonzero entries than the threshold that put its page in the stack, because two all-zero stacks match and say nothing. The comment says in as many words that these are NOT the 35 univariate roots `recursion::precomputed_commitments` builds. Those are Merkle roots over each page's LDE codeword and are what `program_id` folds; no multilinear verifier compares one, and a stacked WHIR commitment has no per-page subtree to match against them. ★ `PREPARED_LEG_ROWS` is asserted in `lfm`, where the cost form lives. The constant sits in `genesis_stack` below `lfm`, because a routing rule the prover, the verifier and the emitter must agree on cannot depend on the emitter's row accounting — but a constant nothing checks is a number that drifts. The assertion is a BAND: the budget must be at least the 20-variable stack the block uses and at most the 24-variable one it was read from, which is the conservatism the threshold's own doc claims. An equality would redden on any schedule change, which is a different finding from a drifted routing rule. ⚠ PRE-REGISTERED AS A READING THAT MAY GO EITHER WAY. V1i measured 175,066 at 24 variables "at the harness's own posture", and this asserts at `config(112, 20)` — blowup 2, fold 4, the production figures' shape. If the two postures disagree, this goes red and the finding is that the constant's provenance is at a posture the production path does not use, which is worth knowing and is the reason to assert rather than assume. A second test makes the insensitivity argument against the cost form rather than the constant: across every stack width from 18 to 25 variables the chain figure stays between the block's dearest sparse page (18 rows) and its cheapest dense one (2,100,474), so the same three pages are selected at any of them.
…pied from a log `genesis_stack`'s unit tests encode the block's census as numbers transcribed from a box log. That checks the closed form's arithmetic and nothing else: a routing rule whose pre-registration rests on a transcription is a rule nobody has run against the program it routes. This arm executes the block guest once — no proving, no card, the same shape as the census arm it sits beside — rebuilds the page configs from the ELF, evaluates the plan on them, and asserts the dense set is EXACTLY `0x0`, `0x40000`, `0x280000`. ⚠ The assertion is the SET AND ITS ORDER, not a count: three pages of the wrong three would satisfy a count, and the stack's column order IS page-base order, so the order is part of what the opening means. A second assertion requires the pages left sparse to cost under a hundredth of the pages stacked, because the hybrid's whole claim is that the genesis bytes are concentrated. It REFUSES rather than skips when the two shas are unstated, and SKIPS with its own line when the ELF is simply absent. Two outcomes with two meanings: a routing quoted as a fact about one program and one input must not be producible from an unnamed pair, while a missing build product is not a failure of the check.
…fix contract stays put
The lead ruled against generalising `check_preprocessed` from a leading count to
a set of column indices, on V1j's recommendation and for the smaller review
surface. This puts that contract back and shapes the prepared commitment to fit
it instead.
What generalised is the TABLE LIST — the cross-epoch genesis stack covers one
GLOBAL_MEMORY table per dense page, each settled at its own reduced point, which
is the part DECODE's single-table `Prepared` could not describe. What did not
generalise is which columns of a table an opening may settle: still its leading
`n`, still a count, and `verify`/`check_preprocessed` are byte-identical to what
they were.
So a cross-epoch page's stack carries BOTH its preprocessed columns rather than
INIT alone. The page loses its OFFSET ramp, which on the block is 51 rows lost
against 282 gained by three more stack columns — about 230 rows on a hybrid
costing order 10^5, in exchange for a contract in `crypto/stark` not moving.
`prefix_at` is where the two meet, and it refuses rather than reinterprets. A
`PreparedColumn` list CAN describe `{1}` or `{1, 0}` or two tables interleaved,
none of which a count can express — so a commitment shaped that way is an error,
not a silent reinterpretation that would have the host skip columns the opening
never settled while every value gate stayed green.
`prepared_runs` is the one walk that enforces it and also pins the stack's COLUMN
ORDER: `at` visits each table once, in the order the stack's columns were
committed, so run `k` settles table `k`'s claims. A reordering would settle one
table's columns against another's commitment — the failure the AIR set's
single-derivation rule exists to prevent, one level down.
The shared `slot_of` resolver goes with the set change, per the same ruling. The
gather survives because a stack spanning several tables still needs one, but each
run is contiguous and is that table's own leading columns, which is exactly the
old single-table behaviour extended.
Tests rewritten to the new shape: the honest two-table round trip first, then the
two tables swapped at the verifier, then a non-prefix, then two tables
interleaved. The two tables' stacked columns are asserted to differ before
anything is proven, so the swap arm cannot be a no-op.
…e emitter gets what the verification consumed
Three rulings, applied together because they touch the same objects.
THE SPLIT LIVES IN `continuation.rs`, not in a module of its own above it. Three
parties evaluate it — the cross-epoch prover, its verifier, and the in-guest
emitter — and they must reach the same answer or the stack's root differs and
the transcript dies at `z` with nothing naming the cause. `crate::lfm` depends
on `continuation` and not the reverse, so a rule the prover and verifier
evaluate cannot live there or call anything that does. Its tariff constants sit
beside it, and `lfm::whir_chain_tests` pins them against the cost form.
A DENSE PAGE STACKS BOTH ITS PREPROCESSED COLUMNS. `check_preprocessed` skips a
prefix, and INIT alone is not one, so `{0, 1}` it is: the page loses its OFFSET
ramp and the stack gains a column. About 230 rows on the block against a hybrid
costing order 10^5, in exchange for the prefix contract not moving. A side
effect worth having: two columns means one prefix bit even at a single dense
page, so a P=1 fixture already exercises the stacked layout's prefix indicator
rather than degenerating to a flat stack.
THE EMITTER GETS THE OBJECTS THE VERIFICATION CONSUMED. `verify_global_bookends`
now answers a `GlobalVerdict` carrying both the bookend roots and the genesis
stack, and `WhirRealGlobal.prepared_roots` becomes `prepared: Option<GlobalPrepared>`
holding the roots, the destinations, and the `StackedLayout` and `Domain` CLONED
off the commitment. Handing over only roots would have the emitter rebuild those
two from the column heights and the config — a second derivation of the object
the host actually committed, which is the defect the single-derivation rule
exists to prevent, one level down.
`GlobalPrepared`'s doc keeps two obligations in two sentences on purpose: its
roots are the fourth owed per-ELF pin for the DENSE pages, while the pages left
sparse owe something else entirely — their nonzero genesis entries interned as
program constants, bound by the program id. Written as one sentence, whichever
is actually unchecked would look covered by the other.
The stack's COLUMN ORDER is asserted where the columns and their destinations
meet, not left to the fact that two walks of the same list agree today. Column
`k` is settled at `at[k]`, so a length mismatch or a reorder would settle one
page's values against another page's commitment with every individual value gate
still green.
`agrees_with` returns, on both the committed and the published form, with its
condition stated: it cannot fire while the commitment is built from the very
config the same call hands `multi_prove`, and it fires the day this becomes the
per-ELF cache it obviously should be. That is the difference between a check
that cannot fail and a check whose caller has not arrived yet.
…order is the caller's Two findings handed over by the gate lane, both in this module. ⛔ `stacks[..num_epochs]` PANICKED where the contract is to reject. Under a mutation it produced "range end index 3 out of range for slice of length 2" — a prover-side panic on a path whose whole job is to answer `Ok(None)` or an error, which is the no-prod-panic policy's exact shape. It is now an `InvalidTableCounts` naming both numbers. It is not attacker-reachable as written: `global_groups` builds `sizes` from the same `num_epochs` two lines above, so the length is right by construction. That is the reason it survived, and it is not a reason to leave it — a panic that is unreachable today and one that is unreachable by construction are different things, and only the second survives someone rewriting the construction. ⚠ AND THE "canonical page-base order `global_memory_configs` hands back" was an unsupported attribution. ✓ That function is a one-to-one `map` over the page bases it is given, with no sort, dedup or filter, so it PRESERVES an order rather than imposing one. Canonicality comes from `touched_page_bases`, which collects through a `BTreeSet` — and on the VERIFIER side the list arrives in the bundle, where it is a claim rather than a fact, bound by `absorb_global` and by the GlobalMemory bus. The doc now says that, because the old wording would have left a reader believing a duplicate base was impossible on the path where it is merely caught.
Two independent rules decide a genesis page's fate. `continuation::is_dense` decides whether the prepared opening carries it; `MAX_SPARSE_INIT_ENTRIES` decides whether the sparse leg is willing to emit it, and refuses above the cap because a column that dense has no cheap closed form. A page the threshold leaves sparse and the cap then refuses would have NO ROUTE AT ALL: too dense to emit, not dense enough to stack, and the refusal would fire on a program nobody could fix by moving either constant alone. So the two must overlap with the threshold strictly tighter, and this asserts it — 9,724 entries at the densest page left sparse, against a 60,000-entry cap, 6.2x of margin. ★ That is the state the block was actually in. V1j's block bundle arm refused at that cap — 116,692 nonzero entries on page `0x0` against a cap of 60,000 — because the prepared route did not exist and every genesis page went to the sparse leg. ⛔ Once the threshold routes the dense pages to the opening, the cap should never fire again, and a refusal from it after this lands is not a page needing a bigger cap: it is these two constants having drifted apart. The test says so where a reader meets the cap.
…global lineage Brings P1's resolved main sync (892c7d1 = origin/main c2ac5d5 merged into bad7cac) under V1j's cross-epoch builder, W1g's driver and the harness stage, so the tree that composes a block artifact runs at a tip the block arms are scored against. NO CONFLICTS: P1 resolved all thirteen main-vs-lineage ones inside 892c7d1, and the WHIR global work sits in files main never touched. A clean textual merge is the risk here rather than the reassurance, so the semantic surface was computed instead of assumed. Intersecting the 28 files the merge touches with the 14 the lineage touched since bad7cac leaves exactly ONE: `whir_statement_tests.rs`. It resolved correctly — the EPOCH fixed part is now derived from `NUM_TABLE_KINDS` (293 at 21 kinds) rather than the 245 literal, and both of the lineage's `fixed part is 134 bytes` assertions for the CROSS- EPOCH statement survive unmoved. Four facts the merge rests on, each read rather than inferred: - ★ #977's elision does NOT reach the cross-epoch AIR set. `global_airs_for` builds bookends through `l2g_global_air` and pages through `global_memory_air`, and neither goes through `build_epoch_airs` or `VmAirs::new` — the function #977 rewrote and the path by which the elision reaches the WHIR epochs. So the cross-epoch table count stays `num_epochs + touched_pages` whatever VM tables an epoch carries, the sixteen group split is unmoved, and the one-polynomial-per-bookend assertion is not put at risk. - The cross-epoch STATEMENT is unmoved. Its tag stays `LAMBDAVM_MULTILINEAR_CONTINUATION_GLOBAL_V1` and its fixed part stays 134 bytes; only the STARK, MULTILINEAR and CONTINUATION_EPOCH tags moved. - Nothing in the lineage constructs or destructures a `TableCounts`. All four references across fourteen files are pass-through — a field, a `&TableCounts` parameter, `absorb_table_counts`, `traces.table_counts()` — so the missing- initializer and missing-destructure errors that main's own tripwire raised four times during the sync cannot reach here. - The three global AIR constructors' signatures are byte-identical in the merged tree, so the driver's call sites still type-check. What moves: every WHIR level-0 wrap program, twice over — the epoch statement grows by 48 bytes and the elision changes each epoch's table set, heights and chain shape — so the wrap identity lines differ from every pre-merge WHIR run by construction. What does not move is any PUBLISHED count, which comes from the schemas and not from statement bytes: the cross-epoch wrap still publishes `2 + epochs x lanes` and the root still publishes `root_schema_words`. Nothing is compiled here. The merged tip's first build is its gate.
THREE ROUNDS OF THIS GAP WERE CLOSED BY READING EMITTERS AND MATCHING VALUE SHAPES, and each round cost a box run. A constant's VALUE says nothing about who interned it: the sumcheck round's Newton pairs were identified from a degree, the coset fold's from Goldilocks' small-order roots being powers of two, and both identifications were guesses that happened to be right. `locate_addr` is the tool this codebase already has for exactly that question — it reports the instruction that wrote a cell and its neighbours, and its own doc explains that this is how a DivByZero's address is turned into the assert that failed. The same question is being asked of a constant, so the same answer applies: the F1 now carries each interned constant's ADDRESS beside its value and prints the neighbourhood of every word no form names. The leg is READ, not inferred. It costs nothing on the success path: the block only runs when a word is already unaccounted for. RULED OUT BY READING for the three words still open, so the next reader does not redo it: they are not squeeze markers — `edsl::squeeze_cell` interns `[SQUEEZE_MARK, index, 0, 0]` and SQUEEZE_MARK is 811225427, not 6 — and they are not Newton pairs, coset powers, constraint-DAG `Fixed` values or statement byte groups, each of which now has a values form that the pool unions.
Round one of the attribution narrowed the three survivors to ONE `algebraic_leaf_hash` call and then stalled, and the stall is the instrument's fault rather than the reader's: `locate_addr`'s window is plus or minus four instructions, which shows a leg's SHAPE and not the loop that called it. WHAT THE FIRST WINDOW DID ESTABLISH, recorded so the next round starts there: - the three constants are contiguous, all `mult: 19`, and bracket ONE permute — they belong to a single leaf hash, not to three legs; - the leaf is SIX felts: a constant, all FOUR lanes of a digest unpacked immediately before it, and a second constant; - the third constant IS `leaf_capacity(6)` — `leaf_capacity` sets `cap[0] = num_felts % RATE_FELTS`, and the observed lane 0 is 6, which the six-felt payload independently confirms. Its remaining lanes are `domain_iv(DOMAIN_LEAF)`; - ⛔ it is NOT `whir_open::emit_block_leaf`'s extension arm, which was the leading candidate because that file's own header names a six-felt leaf for the last round's two-wide tail block. That arm takes `FELTS_PER_EXT` = 3 lanes per value and DROPS the fourth; this leaf uses all four lanes of one digest. Eliminated by reading, not by preference. So the two payload constants are framing felts of a leaf whose builder is outside the old window. The window is now plus or minus twenty-four, which reaches the loop. I am not naming them on a resemblance. Three rounds of this gap were closed by matching value shapes and each was a guess that happened to be right; the fourth would be one guess too many, and the instrument costs one gate run against a wrong answer costing the same and being believed.
…y table The second derivation in `the_interned_genesis_root_is_the_elfs_own_bytes_at_the_dense_pages` mapped every entry of `plan.at` to a column of the ELF's genesis bytes and never read `entry.column`. It was written before the both-columns ruling, when a dense page stacked INIT alone; once the stack began carrying `[OFFSET, INIT]` the test committed `[INIT, INIT]` against it and reported a mismatch it had manufactured itself. The two identical `PROVENANCE table 1 rebuilt nonzero 65652` lines in the gate log are the witness: a rebuilt OFFSET ramp reads 262,143. Rebuild by `entry.column` — the ramp from its own closed form, INIT from the ELF's segments, an unknown column a panic naming itself rather than a silent third INIT. The anti-vacuity floor is scoped to INIT, where density means something, and OFFSET gets the exact count only a ramp can have. The comparison is now executed both ways: the honest control first, then one INIT byte moved and the roots required to differ. With that, the fourth owed per-ELF pin can be stated, and the test prints it: the root, the guest by sha256, the column count and height, and the hash.
THE THREE SURVIVORS ARE THE ALGEBRAIC GRIND'S, and the form that should
have named them says so in its own doc while returning a number:
`grind_check_const_felts` is `2`, described as "the PREFIX felt and the
factor felt" beyond "leaf_capacity(6) for the 41-byte inner preimage
and leaf_capacity(5) for the 40-byte outer one". All three unnamed
words are in that sentence.
A = GRINDING_PREFIX, which is literally 0x0123456789abcded
B = the FACTOR felt, carrying the grind width in its top big-endian
byte: 0x14 = 20 bits
C = leaf_capacity(6), the inner preimage's capacity
★ THE FOURTH FACE OF ONE DEFECT. `sumcheck_round_consts`,
`fold_coset_consts`, `whir_program::steps_rows` and now
`grind_check_const_felts` all compute or know their constants and
return a COUNT. Counts ADD where values MERGE, so none can feed a pool.
This one survived three rounds of attribution precisely because a count
tells nobody WHICH words.
⚠ AND IT IS THE ONE WHERE A COUNT IS NOT MERELY USELESS BUT WRONG: the
factor felt is keyed on the BIT COUNT, so nineteen grinds at one width
intern four words between them while two widths intern five, not eight.
No scalar expresses that. The values form unions over the DISTINCT
widths a chain grinds at — folding, ood, query — and the count keeps its
one honest use with a warning naming the values form.
The derivation reuses `felts_from_bytes` and `single_block_leaf_cells`,
the same two helpers the emitter builds its cells from, so the words a
program pays and the words a form names come off one pair of functions.
…needed it to be `global_memory_configs` does NOT canonicalise. ✓ It hands its argument straight to `global_memory_configs_from_init_page_data`, which is a one-to-one map over the list — no sort, no dedup. So the AIR order IS the list's own order and there is no second list to confuse this one with. Four comments here claimed the opposite and reasoned from it, including one that warned a reader against a mix-up that cannot occur. ⚠ The word still belongs somewhere, so it is moved rather than deleted: canonicality comes from the PROVER, whose `touched_page_bases` builds the list through a BTreeSet. On the VERIFIER's side it is a CLAIM and does not need to be a guarantee, because it is bound twice — `absorb_global` absorbs the list before any challenge, and a restated set leaves the GlobalMemory bus unbalanced or the AIR count mismatched. That is the reason the emitter can take the list as given, which is what the old comments were groping for and got backwards. No code moves: the emitter already indexed pages positionally and absorbed the list as it travels, which is correct under a one-to-one map. Only the reasoning was wrong.
The canonicality correction replaced a clause and left the rest of its sentence dangling — "and the AIRs are / built from, which is a different job done in a different place" — which was both broken prose and, worse, still asserting the separation the same commit had just disproved. There is no different job: one list is absorbed and indexes the AIRs, which is why the emitter can take it as it travels.
…age budget The retired rule charged every page the whole prepared chain, so two pages worth 89,915 rows apiece were each refused and 180,036 rows were spent keeping them sparse — more than the chain that was declined. A fixed cost charged per page cannot be right; the fix is to charge each term to the thing that causes it. PART 1, per page and set-independent: a genesis page is a CANDIDATE when its sparse leg exceeds what carrying it would ADD to the prepared leg. The marginal is one eq with its group join, one prefix indicator per stacked column, and one shared Sub, evaluated at a FIXED height `num_vars + ceil(log2(2 * P_touched))` rather than at the stack's own — the real height depends on the answer, and all three parties must reach the same set from data they hold before deciding. On the block that is 103 rows, so tau = 5. PART 2, once on the whole set: the candidates' total savings must exceed PREPARED_LEG_ROWS, which now prices the chain and nothing else. If it refuses, every candidate stays sparse; a subset still pays the whole chain. The block still selects 0x0, 0x40000 and 0x280000 in that order, and the consequences are asserted with their numbers on real plans: the 27 zero pages fail part 1 at 18 rows against 103; a lone page is carried at 9,731 entries and left sparse at 9,730; two pages of 5,000 now share one chain; and a fixture's 112-entry page passes part 1 and is refused by part 2, which is why PageRoute records candidacy separately from the answer. The sparse-leg cap's overlap test is re-derived in the same commit. Its bound was 9,724 under the retired rule and is 9,730 under this one; both are under the 60,000-entry cap, so a test left at the old number stays green while measuring a rule that no longer exists. The quantity now lives with the rule as `densest_sparse_entries`, and the cap's own refusal message cites it instead of asking for a protocol change that has since landed. Two readings pay for the form rather than restating it: the marginal is differenced out of the emitter's own `weight_at_rows` across 29 and 30 pages in one bracket, and the terms the form omits (two absorbs and two challenge powers per page) are shown to move no boundary the rule is quoted for.
… drop BITWISE, the WHIR coset fold is emitted lean, the LFM_HASH split is a named policy R1: a recursion program carries BITWISE only when one of its chips sends it a lookup (opt-out LAMBDA_VM_LFM_KEEP_BITWISE=1, which reproduces today's programs; TrivialV0 and FriToyV0 re-blessed). R4: the WHIR coset fold is emitted in about three rows a value (opt-out LAMBDA_VM_WHIR_FOLD_CLASSIC=1). R2: the LFM_HASH split is LAMBDA_VM_LFM_HASH_SPLIT, off by default on this pipeline (it costs the WHIR block +2.80 s); the STARK pipeline turns it on with a separate one-line commit. Each setting names itself on stderr in one write. Measured on WHIR (jobs 52, 53): R1 -4.70 s, R4 -2.85 s, in separate ABBAs. rec-int carries the harness commit f81f0a8, merged above.
… default 25 The WHIR stack cap, how wide one stacked polynomial may get, was the constant MAX_STACK_VARS = 25 in the stark crate. It is now a field of the chain format, `ChainFormat::stack` (`StackVars`, 1..=27), carried in the `ChainConfig` both sides already build from: `commit_grouped` and the prepared commitments on the prover's side, `stacks()` in the host verifier and in the LFM's WHIR emitters. Nothing reads it from a proof. The ZF format parses it from LAMBDA_VM_ZF_WHIR_STACK (25 | 26 | 27, the stacks proved, verified and measured to fit on the 32 GiB card) and prints it in the banner (`whir_stack=…`) and on the WHIR schedule line. The default stays 25: every production proof is unchanged. The default moves to 27 in its own commit once the stack's ABBA is read. A prepared commitment (DECODE, the genesis stack) records the cap its layout was built under, and `agrees_with` refuses a reuse under another. The query count is now charged the tallest stacked polynomial as well as the widest table: a group of narrow tables can stack taller than any one of them, and `stack_height` over all of a proof's shapes bounds every group's. At every production shape the charged height does not change (the widest table already stands at or above the cap) and Q stays 112. It can move only for a proof whose stack crosses a round edge that no single table reaches, which only small test programs do. A proof stacked under one cap is refused, as an error, by a verifier at another, in both directions (caps 5 and 7 on three small tables, with the honest controls).
… cap The stack cap now decides the layout a prepared commitment (DECODE, the genesis stack) is handed, and `agrees_with` compares it. This is the negative test for that comparison: a DECODE commitment built under 27 is refused by an epoch at 25 and the reverse, each as an error naming the stack. DECODE fits one polynomial under either cap here, so the roots are equal and only the config check can refuse. With the stack left out of the comparison, the test fails.
…ACK=25 rolls back Measured on block 25368371 in an ABBA (job 152, one RTX 5090, one binary for every arm, arms A B B A): stack 27 against 25 is −13.80 s WHOLE RUN (99.20 → 85.40; A spread 0.60 s, B spread 0.40 s). - By stage: base −6.75 s, level 0 −7.10 s, interior +0.05 s. - By mechanism: the openings the wider stack removes are −9.38 s (50 base chains and 331 rounds instead of 145 and 866), against +1.98 s of commits. - Both B arms proved and verified with the identities, the census and the per-phase ledger peaks registered from E2c. No fallback, no host argument, no refused room turn. - The argument's reserved peak is 24,218 of a 25,688 MiB budget; the device peak 30,576 and 30,736 MiB. This needs the NTT grid split and the WHIR room park and resize, both in the base. What moves, and why. Every WHIR base proof whose groups hold more than 2^25 cells (every real epoch) now stacks into 2–3 polynomials of 2^27 instead of 8–11 of 2^25. With it, every WHIR recursion program id moves (the wraps, the nodes, the global wrap and the root): the wrap programs are emitted from the inner layout. No STARK proof moves, because only the WHIR layouts read the stack. Q stays 112. Re-derived for that cause: - the production-default chain config pins stack 27; - the prepared leg's one-chain pricing limit moves from 64 to 256 genesis pages, because 2 · pages · 2^18 cells must fit 2^27 (the test is renamed for the new limit); - the marginal walk now covers every single-chain bracket up to the production stack, 24 to 27, and the form holds exactly at the two new ones (115 at 26, 117 at 27); - the banner reads `whir_stack=27`, and the schedule line runs to n=27; - `StackVars::WIDEST` quotes the largest device peak of the three runs at 27.
The transcript pins were measured at the legacy WHIR format and skip at any other, printing how to reach it. With the stack at 27 by default, reaching the legacy format also needs LAMBDA_VM_ZF_WHIR_STACK=25, so the line says so.
…ap is 27 by default The WHIR stack cap becomes a ZF format lever, LAMBDA_VM_ZF_WHIR_STACK (25 | 26 | 27), 27 by default; LAMBDA_VM_ZF_WHIR_STACK=25 rolls back to today's bytes. Only the WHIR layouts read it; STARK proofs do not move. The cap travels in the chain config both sides build from, and a prepared commitment built under one cap is refused under another. Measured on WHIR (ABBA27, job 152, with the kernels and the room): -13.80 s whole run, 145 -> 50 base chains.
…d of the prover thread Both bases did each epoch's host preparation on the prover thread, just before its prove: the bitwise multiplicities, the AIR set, the epoch-local L2G trace, and on WHIR also materializing every table's main columns and checking the preprocessed ones. The global proof's preparation ran after the last epoch, in front of its prove. None of it touches the card, and the prover thread is the critical path. By default that work now runs ahead of the prover thread. STARK: a trace builder prepares each epoch after building it (`prep_epoch`), and the producer prepares the global proof once it has handed over the last epoch (`prep_global`); the prover only proves (`prove_prepped_epoch`, `prove_prepped_global`). The pipeline scope still spawns exactly the producer, the builders and the prover, and the global PROVE still runs after the scope has joined, so it never overlaps an epoch prove. WHIR: the producer prepares each epoch before the hand-off (`for_each_epoch_overlapped_prepped`, `prep_epoch_ahead`) and the global proof after the last one (`prep_global_ahead`). The proofs are the same either way; only which thread does the host work, and when, changes. `LAMBDA_VM_BASE_PREP_ON_PROVER=1` keeps the preparation on the prover thread; the setting is read once and named on stderr (`BASE PREP: ...`). `prove_continuation_scheduled` takes the schedule as a parameter, and a test per pipeline proves one run under both and compares every root that does not follow HashMap order, the statement values and the verified output. Also: `prove_continuation_keeping_decode` (both pipelines) returns the DECODE derivations the base made alongside the bundle, for a caller that reconstructs every epoch afterwards; `prove_continuation` is a wrapper that drops them. Measured on block 25368371 (FAST, RTX 5090, ABBA palindromes at 109b705, the preparation behind a temporary knob): WHIR 106.95 -> 101.55 s (-5.40), the prover thread's preparation 6.73 -> 0.00 s; STARK 121.45 -> 119.70 s (-1.75), the global prove starting 0.07 s after the last epoch prove instead of 0.98 s. Program identities and the census unchanged.
…iving them again Both production tree drivers proved the base, dropped the DECODE derivations it had made from the ELF, and derived the same values again in level 0's lead-in before the first wrap could start, with nothing on the card: the univariate DECODE commitment (STARK `EpochConstants::load`, WHIR's root) and, on WHIR, the prepared opening. The drivers now prove the base with `prove_continuation_keeping_decode` and hand its derivations to level 0 (STARK `EpochConstants::load(.., Some(c))`, WHIR `whir_level_zero(.., Some(&BaseDecode))`); the WHIR fixture tree does the same. They are the same function of the same ELF and options, so no program identity moves. A base loaded from a cache has none to hand over, and the lead-in derives them as before. `LFM_TREE_REDERIVE_DECODE=1` restores the second derivation; the setting is read once and named on stderr (`L0 DECODE: ...`), and the lead-in's own lines say which ran. Measured on block 25368371 (FAST, RTX 5090, ABBA palindromes at 109b705, behind a temporary knob): WHIR 106.95 -> 105.45 s (-1.50), the lead-in 3.13 -> 1.81 s, DECODE derivations 1.31 -> 0.00 s; STARK 121.45 -> 121.00 s (-0.45, inside the A pair's 0.50 s spread), `EpochConstants::load` 1.24 -> 0.00 s, the lead-in 5.57 -> 3.93 s. Program identities unchanged.
… of the prover thread, level 0 reuses the base's DECODE I4: each base epoch and the global proof are prepared ahead of the prover thread (the STARK trace builders or the WHIR producer); opt-out LAMBDA_VM_BASE_PREP_ON_PROVER=1, named once on stderr (BASE PREP: ...). I2: level 0 takes the base's DECODE derivations instead of deriving them again, in both production tree drivers; opt-out LFM_TREE_REDERIVE_DECODE=1 (L0 DECODE: ...). No proof byte moves. Measured on the pre-K1 base (job 151): WHIR I4 -5.40 s, I2 -1.50 s; STARK I4 -1.75 s, I2 -0.45 s. I1, I3 and I5 are not carried.
…n C2S C2 = C1 (0b5e3f1) + gap-fix/stack-int (8c2450f, the WHIR stack cap 27) + gap-fix/idle-a-int (d3c76d2, base prep ahead of the prover thread and level 0 reusing the base's DECODE), each a signed merge. One conflict, in prover/src/zf_format.rs: per-table-gpu made one_row=auto the default and C2 adds the whir_stack lever. Both are kept: the default format is cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27; the module and DEFAULT docs carry both levers' sentences and the default-banner test expects the combined string. The stack reaches no STARK proof (only the WHIR layouts read it). The LFM_HASH split joins this pipeline's default in the next commit.
chunking::HASH_SPLIT_DEFAULT = true: every program this build compiles splits LFM_HASH into two power-of-two instances where the rule removes at least 2^15 padded rows. This commit belongs on the STARK pipeline's branch (per-table-gpu) only, the way one_row=auto's default did; the WHIR pipeline's branch keeps the split off, its measured best. Measured on block 25368371 (one RTX 5090, ABBA at d379cef, on top of the BITWISE drop): STARK arm 1 115.95 -> 114.05 s (-1.90 s; level 0 -1.80 s), census -1,095 M cells on arm 1. Thirteen of the fifteen wraps and three of the four L2 nodes split (-931.8 M and -253.6 M); the L3 and L4 nodes and the global parent grow by 90 M, re-verifying split children. The same setting costs the WHIR block +2.80 s, which is why it is not the WHIR default. LAMBDA_VM_LFM_HASH_SPLIT=0 restores one table here. Registry programs carry at most three hash rows and never split, so no pinned digest moves; the program ids of the split block programs move, and no test pins one. (cherry picked from commit 989395a)
…d pair of its own The per-table scheduler's driver threads are not rayon workers, so every one of them staged through the shared slot-0 pinned slab. Uploads went one single-buffered chunk at a time, and a driver copying a retained LDE out held the slab's mutex through the whole host copy while the others queued with the card idle. The slab also grew to the largest retained LDE's next power of two and stayed pinned for the rest of the process. By default the row-major commit's trace upload and its retained-LDE download go through a pair of 32 MiB pinned buffers lent to that one transfer. That covers both upload sites, the row-major expansion and the column-major engine's. - htod_staged: the host fills one buffer while the previous chunk's DMA drains the other. It returns once the last chunk is queued; each buffer's event guards it for the next borrower. - dtoh_staged_into: two chunks in flight, each landed chunk copied straight into the Vec's spare capacity with no zero fill, and the in-place transpose queued right behind the last chunk's read. - At most 8 pairs (512 MiB pinned, 16 allocations), made on demand and never grown or freed; a transfer beyond that waits for a pair. LAMBDA_VM_STAGING_SHARED_SLAB=1 keeps the shared slab. The setting is read once and named on stderr (`[gpu] transfer staging: ...`). Both tree drivers print the staging counters after the base and at the end: bytes and host seconds per path, pairs, waits, and the shared slabs' pinned footprint. Measured on block 25368371 (FAST, RTX 5090), ABBA palindromes at 5cbdf06, on the pre-engine base 169b668 behind a temporary knob. STARK: 121.30 -> 115.50 s (-5.80, A spread 1.20); the base 48.3 -> 44.0 s; under nsys the base's card idle 9.89 -> 5.32 s; host peak -4.41 GiB, which is the slab: 4.01 GiB after the base against 0.13. WHIR: 107.60 -> 105.50 s (-2.10); level 0 -1.3 s. Program identities unchanged. On this base the column-major engine's upload takes the same pairs; that site is new here and not in the measurement above. Tests. Device: exact round trips across chunk boundaries, the closure contract, the buffer-reuse hazard, 12 threads over 8 pairs, and root / host LDE / handle parity of the base, ext3, split-tree and column-major engine commits through either staging, with the staged path's bytes counted. Card-free: the slab footprint and the staging line's shape.
Level 0 opened with host work alone: every first-round wrap's prologue at once (reconstruct, emit, arenas, and on WHIR the epoch harvest), with nothing on the card. None of it needs the card or the global proof, only the ELF and the epoch proofs the base finished long before. By default the tree drivers now start a lead-in before the base. Its helpers (two by default) wait until the base reports its epoch count, then build the prologues of wraps 0..want (want = level 0's first pool round) from copies of the leading epoch proofs, with the same functions the pool calls, so the programs are the pool's own. Level 0 takes each prologue instead of building it. A prologue no helper started is built by the pool as before, and a panicking one is handed back. Nothing in the lead-in takes the card permit or holds device memory of its own. It uses the base's DECODE derivations as the base shares them: the STARK commitment, and on WHIR the root and the prepared opening, whose derivation is a device commit. The base reports through an EpochObserver installed for the calling thread (with_epoch_observer): the epoch count from the producer as soon as the final epoch is executed, each proved epoch, and the DECODE work. That holds on both preparation schedules and both pipelines; with no observer installed, the pipeline is unchanged. Level 0 still takes its own DECODE derivations from the base, and LFM_TREE_REDERIVE_DECODE=1 still re-derives them there; the lead-in's copies are only for its prologues. BaseDecode now holds the Arc the base shares. An I4 schedule test reads epoch positions through the slice-based epoch_chain_position. LFM_TREE_PROLOGUES_AT_LEVEL0=1 builds the prologues at level 0's start instead; LFM_TREE_TAIL_PROLOGUES and LFM_TREE_TAIL_HELPERS size the lead-in. The driver prints `L0 PROLOGUES: ...` either way, and at level 0's start how many prologues were ready. Measured on block 25368371 (FAST, RTX 5090), ABBA palindromes at 5cbdf06, on 169b668 behind a temporary knob, before the base-prep and DECODE-handoff changes. WHIR: 107.60 -> 104.40 s (-3.20, A spread 1.20); the lead-in 3.19 -> 0.07 s; level 0 -3.1 s; base unchanged; device peak +592 MiB, from the harvest's MLE evaluations running unreserved beside the base's tail. STARK: 121.30 -> 118.65 s (-2.65); the lead-in 5.54 -> 0.22 s and level 0 -6.1 s, but the base +3.4 s, because the two helpers slow the base's epoch proofs. Program identities unchanged. On this base the DECODE handoff already removes part of the lead-in, so the gain here is smaller than above. Tests. Card-free: the hand-off (order, the count gate, handing back an unstarted, failed or context-failed prologue, waiting on one in progress, close). Fixture scale, on both bases: the observer sees the count once and every epoch byte for byte, and a prologue built from the leading epochs emits the pool's own program and arenas.
…te does Every staged_transfers test forces its path with the thread override, and only the block-scale tree drivers read the lead-in's setting, so no card-free test read either setting from the environment. One test each now does, and prints the line that names it: - staged_transfers: staging_pairs_enabled() is !LAMBDA_VM_STAGING_SHARED_SLAB, with its `[gpu] transfer staging: ...` line; - the tree tests: lead_in_enabled() is !LFM_TREE_PROLOGUES_AT_LEVEL0, with an `L0 PROLOGUES setting: ...` line. The gate runs each with --nocapture under the default and under the opt-out and counts the named lines.
…nned staging, level 0's first wrap prologues built in the base's tail I6: each row-major commit transfer is staged through a pinned pair of its own instead of the worker's shared slab; opt-out LAMBDA_VM_STAGING_SHARED_SLAB=1, named once on stderr ([gpu] transfer staging: ...). I7: level 0's first wrap prologues are built by helpers in the base's tail; opt-out LFM_TREE_PROLOGUES_AT_LEVEL0=1, sized by LFM_TREE_TAIL_PROLOGUES / LFM_TREE_TAIL_HELPERS (L0 PROLOGUES: ...). No proof byte moves. Measured on the lane's base (IDLE-B box2): I6 STARK -5.80 s, WHIR -2.10 s; I7 WHIR -3.20 s, STARK -2.65 s net.
…xes K3/K4/K5 Brings the HASH lane's six commits onto candidate C2 (7d41668): the half-warp Merkle tops (K3), the work-queue grind (K4), the limb-multiply permutation variants (K5), each still behind its LAMBDA_VM_GAP_* knob, their parity tests and host KATs, the serialised grind-counter tests and the queue grid's context fix. No conflict; the next commits make the three fixes the defaults.
…imb permutation by default The three RPX device fixes measured EFFECTIVE on the WHIR block (job 160, wt300-307: K3 -3.90 s, K4 -6.45 s, K5 variant 5 -10.05 s against 107.15 s, identities identical in every arm) are now the defaults. Each keeps an opt-out, and its default lives in one constant in `rpx_paths`, so a pipeline that needs one off flips one line: - LAMBDA_VM_RPX_WARP_MERKLE (WARP_MERKLE_DEFAULT): narrow levels and the tail on rpx_merkle_level_warp / rpx_merkle_tail_warp; =0 walks a thread per parent (rpx_merkle_level, rpx_merkle_tail). - LAMBDA_VM_RPX_GRIND_QUEUE (GRIND_QUEUE_DEFAULT): rpx_grind_search_queue on a card-filling grid; =0 is rpx_grind_search on LAMBDA_VM_GRIND_GRID. - LAMBDA_VM_RPX_LIMB_PERMUTE (LIMB_PERMUTE_DEFAULT): every RPX kernel from rpx_v5.cubin (32-bit limb multiply, square_n unrolled by four); =0 loads rpx_v0.cubin, the 64-bit multiply. Each variable takes 0 or 1 (anything else aborts) and each switch prints one line on first use, "[gpu] RPX Merkle: ...", "[gpu] RPX grind: ...", "[gpu] RPX permutation: ...", naming the path and whether it came from the pipeline default or the variable. The queue's grid line becomes "[gpu] RPX grind queue: grid ...". build.rs now builds rpx.cu twice (variants 0 and 5) instead of five times. The LAMBDA_VM_GAP_* knobs and the gap_hash module are gone. The parity tests move to prover/tests/rpx_device_paths.rs, named for what they compare (the per-parent walk, the stride grind), and the temporary wording leaves the kernels, the host KATs and the docs.
The PROVE SPLIT line's "r4_grind (n/airs on device)" took its delta of gpu_lde::gpu_grind_calls(), the keccak arm's counter. An RPX grind that runs on the device counts in gpu_grind_calls_rpx(), so under RPX every line read 0/airs while every table ground on the card: on the WHIR block (job 160) the root proof printed 0/11 beside the harness's own count of 11 RPX device grinds for it. device_grinds_now() sums both arms and report() takes its delta of that. rpx_grind_device gains a test that reads it around one RPX device grind (the keccak-only count reads 0 there and fails).
The result lines still carried the campaign's fix ids (K3, K4, K5) and called the old paths "shipped", which stopped meaning anything once the new paths became the defaults. They now say what is compared: the warp walk against the per-parent walk, the queue grind against the stride grind, the limb primitives and the permutation variants. Output only; every check is unchanged and both binaries still pass.
…er half-warp, a queue grind, the limb permutation K3: a Merkle level and the tail compress one permutation per half-warp (opt-out LAMBDA_VM_RPX_WARP_MERKLE=0). K4: the device grind claims nonces from a work queue (LAMBDA_VM_RPX_GRIND_QUEUE=0). K5: the whole RPX module runs the limb-multiply permutation variant (LAMBDA_VM_RPX_LIMB_PERMUTE=0). Each opt-out accepts 0 or 1 and names itself once on first use. Every digest, root and grind nonce search is byte-identical to the previous kernels (host known-answer tests and device parity). The prove split now counts RPX device grinds. Measured on the pre-K1 base: WHIR K3 -3.90 s, K4 -6.45 s, K5 -10.05 s; STARK K3 -1.00 s, K4 -0.50 s, K5 -7.95 s.
…n C3S C3 = C2 (7d41668) + gap-fix/idle-b-int (bdb2d37, per-transfer pinned staging and level 0's first wrap prologues built in the base's tail) + gap-fix/hash-int (e041e9f, RPX Merkle tops per half-warp, a queue grind and the limb permutation), each a signed merge. per-table-gpu's head b773514 is C2S (a9defee + C2 + the LFM_HASH split flip), so the merge base is C2 and only C3's two lanes come in. No conflict: the flip and the one_row=auto default stay as they are.
The DEEP and out-of-domain denominators were inverted by a global
Montgomery scan: compute_denoms plus five scan kernels, each a full pass
over the domain with prefix and suffix scratch, although every row needs
only its own few inverses. By default now:
- compute_and_invert_denoms_ext3_dev runs one kernel,
invert_denoms_rowwise_ext3_k{1..8}: each thread builds its row's
denominators and inverts them in registers with one base-field
inversion (adjugate over norm, the norms batched by Montgomery's
trick, kernels/ext3_inv.cuh). More than 8 per row keep the scan.
- the fully resident R4 DEEP inverts its own row's 1 + K denominators
(deep_composition_ext3_fused_m{1..4}) and needs no inverse buffer; it
falls back to the buffered kernel above 3 points or on any
precondition miss.
- the single-point OOD sums (the R3 composition parts: 1-2 columns, so
1-2 blocks on the card) run on the row-chunked multi kernel, and the
multi kernels' chunk count loses its 64 cap.
The values are the same field elements; raw limbs may differ by p, which
nothing downstream observes. Measured on block 25368371 on one RTX 5090,
ABBA behind a switch on 169b668: STARK (one_row=auto) -0.70 s whole
run against a 0.50 s A spread and -2.35 GiB device peak; WHIR kernels
-49.8 % with the wall inside the noise.
LAMBDA_VM_DEEP_INV_LEGACY=1 restores all three (the scan, the buffered
DEEP, one block per OOD column), read once per process with a banner,
as LAMBDA_VM_LDE_LEGACY does for the LDE. The legacy paths stay public
for tests/deep_inv_parity.rs, whose tests name both paths per call;
tests/deep_inv_setting.rs checks that the process setting is followed.
gpu_fused_deep_calls() counts the fused dispatch, and
cuda_path_integration asserts it follows the setting: a table that
silently fell back to the buffered kernel would still verify.
C4 = C3 (41549eb) + gap-fix/kern-int (d1dc455): the DEEP and OOD denominators inverted row-wise, the R4 DEEP kernel inverting its own denominators, and the single-point OOD sums row-chunked, all by default (opt-out LAMBDA_VM_DEEP_INV_LEGACY=1). Every field element is the legacy path's, so roots and proofs do not move. C3S (4d8a096) is per-table-gpu's head: the merge base is C3, and only the one K6 commit comes in. No conflict: the flip and the one_row=auto default stay as they are.
recompute_lde_produces_byte_identical_proofs compares the bytes of two proves of one instance, one per residency mode, at the test options' grinding factor of 1. Under `parallel` the CPU nonce search is rayon's find_any (crypto::grinding::generate_nonce), so the two proves can return different valid nonces; the nonce is absorbed before the queries are drawn, and every opening after it moves. The test fails whenever the two searches disagree, whichever residency mode runs: on a laptop it failed 11/20 at d1dc455 and 15/20 at 7d41668, and 20/20 passed with LAMBDA_VM_DETERMINISTIC_GRIND=1 (the smallest nonce) or without `parallel` (a sequential find). The residency tests now prove at grinding factor 0, as zf_golden_tests already does for the same reason. The residency mode acts on the main LDE, which the grind never reads, so the comparison loses nothing it could catch.
The residency-mode tests compared two proves byte for byte while grinding with rayon's find_any, so any two nonce searches could disagree. They now prove at grinding factor 0, as the golden tests do.
This was referenced Sep 28, 2026
|
Benchmark Results for modified programs 🚀
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The number
Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21, fan-in 2. At this
head,
946ca6045, the two default arms of the last ABBA read 78.7 s and 78.9 s (mean 78.80 s). Host peak 26.3 GiB,device peak 27.5 GiB (28,146 MiB).
Each step below is its own ABBA on one binary: two arms per setting, alternated.
cap=auto fri=dp one_row=auto)In the last 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:
The previous head's A arms and this head's B arms, taken from the two ABBAs, give −25.35 s. The last row's −28.75 s
overstates the batch, because its A arms run this 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 last 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=1LAMBDA_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.
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 57.80 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 57.80 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.
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.
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 change no proof byte.
Fixed along the way
tables. It rejected honest one-row proofs that publish values.
Gate and CI
The batch was gated at this head,
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 this head, 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
one_row(auto here,off in WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 57.80 s #1010) and the LFM_HASH split (on here, off in WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 57.80 s #1010). A per-pipeline default would let one PR carry both.
constants, instead of folding the id in-guest with keccak. That also lets the wraps drop BITWISE.
the proof. A few bits of proof-of-work before the DEEP batching challenge would add margin, at negligible cost
(parked).
LAMBDA_VM_MEMPOOL_RELEASE_MB=0, which releases thedevice memory pool; the code's default retains it. Retaining measured −0.90 s on this pipeline (before the engine).
No code changes; the decision is which configuration to report.
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.
and replay 15–25 % slower per item than the previous head's build, with the same source on that path.
is the build, not contention.
but lose only about half a second there [estimate].
not tried yet.
iteration.