WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 107.5 s - #1004
Draft
MauroToscano wants to merge 1005 commits into
Draft
MauroToscano wants to merge 1005 commits into
MauroToscano wants to merge 1005 commits into
Conversation
…ng's chain Run a2v's pin went red on the box on both hashes, and the pre-registration was the wrong half. W1-B's landing gate priced the out-of-band DECODE commitment at "+1 absorb per epoch" — the derived root's absorb. But opening a committed polynomial in WHIR IS a chain, and the epoch opens that commitment at DECODE's reduced point once per epoch: six rounds over a 2^23 stacked polynomial, its grinds, its sumcheck evaluations and its query draws. The terms are derived here from the round structure rather than taken from the box. `stacked_eval::verify` absorbs one field element per column of the group and draws one batching challenge, then runs one chain per stacked polynomial; each chain grinds `3R - 1` times, absorbs two sumcheck evaluations per folded variable, absorbs a successor root and an out-of-domain value per non-final round plus the final value, and draws `K` sumcheck challenges, two challenges per non-final round and `ceil(Q / 4)` query positions a round. The columns, the polynomial count and the schedule come from `global_layout` and `decode_prepared_config` — the same two functions `decode_prepared_for` uses — so nothing here describes a group the prover does not build. At the pinned guest that is 79 absorbs, 202 squeezes and 17 states an epoch, and the pair becomes prove (585_140, 186_256, 3_251) and verify (585_292, 186_286, 3_251) — the box's a2v reading, reached from the code. `owed` is unchanged at (152, 30, 0): the prover runs the opening too and the replay covers only the roots block, so the new term moves both lines equally. `PROVE` and `VERIFY` become functions of the shape because `schedule()` allocates. The shape itself, `DECODE_PREPARED_SHAPE`, is not assumed: `check_transcript_pins` derives it from the ELF through `preprocessed_columns_from_elf` and asserts it before comparing any count, so a guest whose instruction table changed size fails by name instead of moving every number by an amount that would read as a protocol change. It costs the instruction map, no commitment, and runs after both measurement windows close. `the_prepared_opening_is_the_schedule_the_shape_implies` pins what the shape implies — stacked width 23, one polynomial, five placements, the schedule [4,4,4,4,4,3] and 112 queries — on a laptop, so a change to the stacking rule, the fold width or the shipped query count fails there rather than on the box. `the_pinned_pair_is_the_measurement` keeps its rule of re-spelling instead of calling: it writes the opening's arithmetic out at those four numbers while the pin derives it from `schedule()`, and the two must agree. The device counters are pinned the same way, under `cuda`. The grind line is an IDENTITY, not a second number: the only production readers of `transcript.state()` on this path are `whir_chain`'s `grind` and `check_grind`, one read each, so device grinds must equal the prove side's state column, and a host fallback or a new state reader says which instrument moved. The commit line cannot be an identity — its base is a measured total over every table of every epoch — so it is `COMMITS_BASE` plus the opening's own device work, `R - 1` successor codewords an epoch plus the one-time commitment, from the same layout. The pins now run BELOW the backend/prove/verify/proof/epochs table. a2v's red run printed no prove time, no verify time and no proof size, because the assert panicked before the table: a gate that destroys its own subject costs a box slot every time it fires. Also: `decode_prepared` is deleted. It had zero callers — production goes through `decode_prepared_for` at four sites — while carrying an `#[allow(dead_code)]` whose comment promised a wiring commit that had already landed, so the marker was structurally permanent while reading as temporary. Its four doc references are repointed, and `decode_prepared_tests`' module header no longer says the feature is unwired; it says where it is wired, and says that it said the opposite for one commit too long.
`check_transcript_pins` asserts the derived DECODE shape against `DECODE_PREPARED_SHAPE`, and that assertion sits behind the sha guard, so it runs on the box and nowhere else — the blindness the pin's own guard/assertion split was written to remove. The way the comparison goes wrong without the pinned guest is the tuple: two `usize`s, with nothing in the type saying which is the width. `the_shape_deriver_reads_columns_then_log2_rows` runs the deriver on `sub` and compares both elements against the columns `preprocessed_columns_from_elf` builds, so a swapped pair fails here rather than on the box.
…rgo test cannot see `make lint` runs clippy over test code under `-D warnings` and `cargo test` does not run clippy at all, so a suite that is 100 % green says nothing about the lint. Four findings, none of which changes what any program computes or costs: - `emit_claim_statements` took eight positional arguments (`too_many_arguments`, 7 allowed). Grouped into `BusInputs`, which is the better API anyway: item 2e's per-table assembly builds it once, and a wide positional list is exactly where a caller swaps two factor slots without the compiler noticing. - two `clone`s on a `Copy` field element and three `x = x + y` in test code (`clone_on_copy`, `assign_op_pattern`). - rustfmt's layout on the two files it had not seen. Verdicts at this tip: `make fmt` exit 0 with `git status --short` identical before and after; `make lint` exit 0, `Checking lambda-vm-prover` 6, zero `^error`, six `^warning` and all six the known `math-cuda: nvcc not found` build note; `-p stark --lib multilinear_logup` 10 of 10; `-p lambda-vm-prover --lib whir_` 88 passed of 95 listed, 7 ignored.
…est is a knob Run rs1 died in 0.93 s on `the_decode_commitment_is_held_across_the_epochs`' secondary VRAM assertion, and the two RESIDENCY count lines — the actual discriminator between "DECODE's commitment is held across the epochs" and "rebuilt every epoch" — never printed. A secondary check that runs before the primary one can spend a box slot answering nothing. The VRAM READING stays where it must be, straight after `prove_epochs` and a drain, because anything allocated later would spoil it. Only the printing and the verdict move: derivations, commits and the shape-derived prediction print and assert first, then the retention prints. And it only prints. `drain_and_trim` synchronises the context and trims the device's default memory pool to zero, so what it cannot return is memory a live `CudaSlice` owns, allocations outside that pool, and the driver's own per-process reservations. `Backend` holds device buffers for the life of the process — the forward and inverse twiddle caches are `Arc<CudaSlice<u64>>` per `log_n`, filled lazily and never dropped — and the cubin modules with their per-SM local-memory backing store are the driver's, paid at the first launch. rs1 read 544 MiB and none of those can be sized from the source at this fixture's shapes. ★ What separates them is already in the test and was being thrown away: it runs TWO arms in ONE process and every candidate above is paid once, so the SECOND arm's retention is the number that decides it. Both arms' readings are now printed with their arm number, and the doc pre-registers what each outcome means: arm 2 far below arm 1 is one-time process cost, arm 2 level with arm 1 is the run's own buffers outliving the call, which is a real regression. No assertion rides on that yet, deliberately — the threshold would be a number nobody has measured, and a second red box slot spent on a guessed bound is what this reordering exists to prevent. `the_one_commit_cost` ran on `test_private_input_xpage`, whose DECODE table is 5 x 16. That times the SHAPE working; it is not the 2^23 commit the WHIR prove's delta has to be attributed to, and the two print the same sentence while differing by five orders of magnitude in cells. The guest is now `LAMBDA_VM_ONE_COMMIT_ELF` with NO fallback: unset, it panics naming why. It resolves through `multilinear_bench_tests::elf_bytes`, made `pub(crate)` so there is one answer to "which ELF is `ethrex`" rather than two, and the printed line carries the guest's full sha256 and byte length beside the columns, rows, cells and time — a name in the output is a display, and this campaign has already spent a day on a difference that was two builds of "the same" guest.
…ables A root that cannot apply on the last row carries a `Selector`, and that selector's value at the reduced point is a PUBLIC FACTOR the verifier recomputes. `public_values` evaluates them and hands back the answers, which is right for a verifier that has the point; a caller that is EMITTING that evaluation as code needs the selectors themselves. `public_tables` is not a substitute: it builds a `2^num_vars` table per selector, which is exactly the pass the closed form exists to avoid. Read-only, no behaviour change.
The first leg of the per-table verify that no earlier one covers:
`Selector::evaluate`, which is a public factor's value.
s(x) = 1 - geq(x, cutoff), cutoff = 2^n - end_exemptions
`geq` is the multilinear indicator of `index(x) >= cutoff`: either x matches
cutoff bit for bit, or the two first differ where cutoff has a zero and x a one.
`prefix` is the running "everything above this bit matched", and variable 0 is
the most significant bit.
`prefix` starts at ONE and `geq` at ZERO, so each is carried as an `Option`
whose `None` IS that literal and a row is spent only once the value is a wire.
This is not an optimisation bolted onto the host's expression; it is the host's
expression with the identity steps left out, and the cost form counts the same
cases. On a VM table's `except_last(1)` at twenty variables the cutoff is all
ones, so the whole selector is nineteen multiplies and one subtract.
Gated against `Selector::evaluate` at EVERY exemption count from zero to `2^n`
for n = 1..5 at three points each, because both the value and the cost turn on
the bit pattern of `cutoff` and a gate that sampled counts would be sampling bit
patterns. The two branches that return before the loop — applies everywhere,
applies nowhere — are named in their own test, and each is compared against the
host's answer rather than only against the literal expected.
F1 is INCREMENTAL: each selector's own marginal rows against its form, because
the interned `1` is shared across the whole set and a total would let one
selector's over-count cancel another's. A second test pins the sharing itself —
seventeen selectors at four variables cost 125 rows pooled against 141 counted
separately, the difference being the sixteen `1`s that are not paid again.
`Cost`'s accumulator methods are made public for this: the whole table shares
one constant pool, so a later term has to be added into one of these rather than
summed as a number.
`--lib whir_table_tests` 4 of 4.
…inside one The alignment counter read 25 on the EQ fixture and a zero had been pre-registered for a real proof. That zero was a wish: a STATEMENT is variable-length by nature — a tag, one byte per table count, a three-byte grind trailer — so absorbs inside it start off field element boundaries constantly, and the padding never promised otherwise. What it promises is that whatever FOLLOWS a statement starts aligned, and the transcript could not tell where a statement ended. It is told now. `IsTranscript` gains `mark_statement_end`, a default no-op that `DefaultTranscript` overrides and `absorb_statement_padding` calls after the pad; the counter counts from there. `Counts::transcript_misaligned_absorbs` becomes `transcript_misaligned_absorbs_after_statement`, which is a compile error at any exhaustive destructure — the intended catch. That does put a metrics concern into a production trait, and the trait's doc says so: only the transcript knows the window, and only the statement path knows where a statement ends. ⛔ THE MARK DOES NOT RESET THE WINDOW, and that is the whole design. Zeroing the offset would make the first absorb after any statement aligned BY CONSTRUCTION — including when the pad is broken, which is the one case the counter exists for: a check that cannot fail, wearing the name of the one the pad owes. It sets a per-transcript flag and leaves the offset alone. `a_statement_that_ends_off_a_boundary_is_still_counted` is what holds that line: three bytes, a mark, a 32-byte absorb, exactly one counted. A per-transcript flag rather than a global reset of the counting origin, for two reasons. The counters are process-global, so a reset would clobber a concurrent transcript. And a continuation has sixteen statements on sixteen transcripts, where "since the last mark" would report only the last of them while a flag reports every one. The flag rides through `clone`, so the `owed` fork is past its statement exactly as its parent is. ★ AND ONE HOLE THE RENAME OPENED, closed in the same commit. Deleting the call from `absorb_statement_padding` passes every other test in these files: the counter reads zero because it never started, the recorder reads zero because the pad is correct, and the two agree on a number that means nothing. `the_statement_padding_tells_the_transcript_the_statement_ended` asserts the CALL instead of a count — the production `absorb_epoch` against a recorder that notes whether the mark arrived — and needs neither `hash-metrics` nor a global counter, so it runs in the ordinary suite. The three counter tests are kept with their exact numbers, each gaining one `mark_statement_end()` line: the 13-byte-seed fixture still requires 2, because the mark does not move the window and both roots are still misaligned; the aligned stream still requires 0; the squeeze test still requires 1. The cross-check gets sharper rather than weaker. It compared the counter against the recorder's total; it now compares the two after-the-statement counts, and they reach that boundary by different roads — the counter is told by the padding, the recorder is handed the statement's call count from `epoch_expected`'s independent field-by-field derivation — so a wrong mark and a wrong expectation cannot agree by construction. Its AGREE line still prints the total, taken from the recorder since the counter no longer reports it, and W1c's measured 25 / 24 with 22 / 21 felt-sized are kept in the field's documentation as the reason the boundary is in its name.
Level 0's driver cannot refuse a bundle by reading a label. A WHIR proof's bytes are hash-agnostic by design — both arms serialise to the same length, which is the byte gate's own invariant — and `whir_hash_knob` is a cached process setting that says what THIS process proves under, not what a bundle was proven under. So the refusal the design settles on is the verification itself: hand the epoch to a verifier configured with a hash, and a bundle proven under another one fails because the transcript's sponge is part of the configuration and every challenge diverges. That was a design claim. `an_epoch_proven_under_one_hash_is_refused_under_the_other` runs it: epoch 0 of `sub` proven with `prove_epoch::<KeccakWhir>`, verified under `KeccakWhir` (which must be ACCEPTED — a verifier that refused everything would pass the refusing half alone) and under `RpxWhir` (which must refuse). `verify_epoch_bookend` collapses every failure to `Ok(None)`, so the control is what makes the refusal mean anything. This is NOT the level-0 seam: there is no driver and no bundle here. It is what the seam rests on, measured now so it arrives with its premise checked rather than assumed. `verify_epoch_bookend` becomes `pub(crate)`, because it is the only verify entry point that takes its hash as a parameter — `verify_epoch` chooses `H` from the cached process knob, so from outside this module one process verifies under exactly one hash. W1c's handoff recorded that the seam's test needs prove and verify generic over `H` "which `whir/decode-group` has"; the prove half is public and generic, the verify half was module-private, so the test could not have been written on the merged lineage either.
…, and the device model is printed Run rs2 read `arm 1 ... derivations 1 commits 9 predicted 3` and the commit assert fired before arm 2 ran. The PRIMARY instrument passed; the prediction modelled the wrong counter and took the second arm's verdict with it. ⛔ THE TWO COUNTERS COUNT DIFFERENT SETS. `note_host_fallback` has exactly one call site in the tree — the INITIAL commitment of a chain's stacked polynomial. Fold commits have no host-fallback counterpart: `CodewordCommitment::commit` and `commit_tree_ext3` bump `COMMIT_CALLS` and nothing else. So without a card `host_fallbacks` is the count of initial commitments and nothing more, while with one `commit_calls` counts the initial commitments AND every fold. The test summed the two against a single model. Each counter now has its own model, named for what it counts. The host-path model is one stacked polynomial per group per epoch plus one for DECODE, and it is asserted where it applies — 3 at one epoch and 7 at three, card-free. The device model is read off the proofs: a group's opening is a `StackedProof`, each polynomial a `ChainProof`, and `rounds.len()` is one initial commitment plus `R - 1` successors, so the epoch's chains contribute `rounds.len()` each and DECODE's prepared chain contributes `rounds.len() - 1` per epoch with its held commitment counted once. No layout is reconstructed and no AIR rebuilt. ★★ AND THAT DEVICE MODEL IS PRINTED, NOT ASSERTED, because a measurement says it is wrong at this fixture's shapes. Computed card-free from the same proofs: arm 1 has 3 chains, 9 group rounds and 1 prepared fold, so the model reads 11 — and the box read 9, which is exactly the group rounds with both DECODE terms absent. The mechanism is an admission boundary: a polynomial too small for the device is committed on the host, where a fold commit is counted nowhere. This fixture's DECODE group is 5 x 16, sitting at that boundary; the pinned guest's is 5 x 2^20, far above it, which is why the pinned run's commit total does contain DECODE's folds and its held commitment. One arithmetic cannot describe both without the admission rule, and asserting the wrong one is how a box slot was already spent. So the box prints the decomposition instead — `device N host M model K = groups G + prepared folds P + 1 held` — and two arms of it identify the model outright: `device == groups` means the prepared chain went to the host entirely, `device == groups + prepared` means only the held commitment did, and `device == model` means all three counted. The assert lands afterwards, on a measurement. Structurally: both arms' derivation lines print and assert inside the loop, before any commit model or memory reading is compared, and the readings are collected into an `Arm` per arm so the secondary comparisons run after every primary verdict. rs1 lost the verdict to a VRAM assert and rs2 lost it to a commit assert; neither can pre-empt it now.
…erived re-pin) into whir/lfm W1-B's out-of-band DECODE commitment (steps 1-4, the hoist, the per-epoch opening, the replay fix), the REGISTER INIT/FINI binding on the multilinear path, the transcript re-pin derived from the opening's chain structure, the residency counts and the hash-agreement premise test, onto the per-table LFM base. Three resolutions, all forced by the two lineages meeting: * `multilinear_bench_tests.rs` - the only textual conflict, `elf_bytes`' visibility. decode-group widened it to `pub(crate)` so `decode_residency_tests`' guest knob resolves an ELF name through the same function this bench does; the LFM base had widened it to `pub(super)` for `whir_epoch_shapes`. `pub(crate)` serves both, so it wins with its reason. Everything else in that file auto-merged and both sides survive: the pin's W1-B terms (the derived-root absorbs, the prepared opening's per-epoch chain, the commits and grind identities) and the LFM base's fifteenth table count. The pin reads `NUM_TABLE_KINDS` off the struct, so the merged tree's pair is derived rather than edited: prove (585_155, 186_256, 3_251) and verify (585_307, 186_286, 3_251), which is a2w's measured pair at fourteen kinds plus `EPOCHS` on each absorb line, with OWED (152, 30, 0) unchanged. * `lfm/epoch_tests.rs` and `lfm/logup_tests.rs` - two `VmAirs::new` call sites that exist only on the LFM lineage, so the register fix never reached them. Both passed `(commitment, num_cols)`; both now pass `RegisterPreprocessed` with the same commitment plus the two vectors it commits, which is what makes INIT and FINI binding on the multilinear path. Test-only, and the commitment value is unchanged, so no proof either file builds moves. Gated on the merged tree: `cargo fmt --check --all` clean, `make lint` exit 0 over all eight clippy arms with six `Checking lambda-vm-prover` lines and no diagnostic.
…statement) into whir/lfm The Fiat-Shamir alignment counter and the statement-end mark: one additive `Counts` field, the counting window defined inside `DefaultTranscript` under `hash-metrics`, and `absorb_statement_padding` telling the transcript where a statement ended, after the pad rather than before it. One conflict, and it was a false one. Both lineages append tests to the end of `crypto/crypto/tests/transcript_counters.rs`, so the two blocks are disjoint but share the `);` and `}` that close their last assertion, which git factored out as context. Keeping both therefore needed that closer restored between them: W1-B's `the_derived_root_is_absorbed_after_the_carried_ones` keeps its own, and the counter's four window tests keep the shared one. Thirteen test functions on the merged tree, no content overlap between the sides. Nothing else conflicted. The new `Counts` field meets no exhaustive destructure on this lineage: the only constructions are the snapshot in `hash_metrics.rs`, which arrives with the field, and a `..Default::default()` literal in the pin's skip test. The mark lands in the shared padding helper, so it covers the fifteen-count statements the per-table lineage produces as well as the seam's. Gated on the merged tree: `cargo fmt --check --all` clean with zero files, `make lint` exit 0 over all eight clippy arms with six `Checking lambda-vm-prover` lines and no clippy diagnostic.
…han supplied Item 2e of the WHIR in-guest verifier: `multilinear_table::verify` assembled — the bus output absorbed, the GKR ladder, the row challenges, the bus statements and the zerocheck rule batched into one sumcheck, and `claim_reduce` leaving every column claimed at one point. The leg drives its own `WhirTranscript`, because `claim_reduce` already takes one and a table cannot hand over what it does not have. So every challenge is DERIVED, and executing an honest proof is the challenge-stream comparison: a wrong challenge anywhere leaves one of three refusals with no satisfying assignment — the GKR layer relation, the batch's residual, and the shifted read. One reordering, stated rather than hidden: the host interleaves the ladder's transcript operations with its arithmetic and this draws a layer's challenges first. The order of TRANSCRIPT operations is unchanged, which is the only order that is a property of the protocol — `gkr::verify` absorbs nothing it computed. `weights` becomes `weight_slots` and public: a verifier written outside the crate has to index the same two factor slots, and a second spelling of a convention both sides must agree on is drift nothing would catch. Gated on a REAL per-table proof. `multilinear_table::prove` reads no commitment root, so a table at three and four variables proves and verifies on the laptop with no guest ELF. The AIR is three constraint roots over a SATISFIABLE trace, one of them carrying `except_last(1)` — that selector is what puts a public factor in the woven vector, so the assembly's gate reaches the selector leg too. The machine's verdict is compared against the host's: the bus output, the reduced point, and every column value. ★ THE ROW FORM FOUND A CONSTANT NO PER-HASH FORM CAN SEE. `algebraic_leaf_hash` interns `leaf_capacity(felts)` for the leaf it is about to hash, so a program pays one `LFM_CONST` per DISTINCT leaf LENGTH it ever hashes — six of them on this table. `SpongeHash::rows()` is right to leave it out, because a hash does not know what other lengths the program will use; the pool is per PROGRAM. The form adds them off the finished schedule, and `Cost` now keys its pool on the canonical WORD rather than on an extension element, since a leaf capacity is a four-lane digest sharing that same pool. The other half of that finding: `combine_rows` folds the DAG's own constants in as rows, so the assembly subtracts them and puts the VALUES in the one pool instead — a DAG constant that is also the `1` every `eq` seeds costs one row and not two. F1 is exact at both heights: 570 rows at three variables (413 operations, 13 constants, 144 sponge rows, 43 permutations) and 777 at four (566, 13, 198, 59). The test also asserts that the form NAMES every constant the program interns, which is how the leaf capacities were found rather than absorbed. ⛔ `check_preprocessed` is not emitted, and the seam is named at the seam: the host's MLE pass is replaced by BITWISE's closed form and DECODE's own pinned group. The gate's table has no preprocessed columns, said so rather than left to read as coverage. `--lib whir_table_tests` 6 of 6.
Every site runs all three halves (instance 49): the untouched proof executes on
both sides, the HOST rejects the forgery, and the machine refuses it. The middle
half is what tells a soundness success apart from a completeness bug — a machine
that refused something the host accepts would score as the former.
The three sites land on three different host refusals, which is the statement
that the arm reaches three independent checks rather than one:
a GKR layer's q_lo LayerRelationMismatch { layer: 0 }
a main sumcheck evaluation BatchMismatch
a claimed column value ShiftedReadMismatch
each met by a machine `DivByZero` at a different address. Every one of them is
reached only if the machine drew the same challenges the host did, which the arm
witnesses as a side effect of refusing.
…st cannot see `make lint` runs clippy over test code under `-D warnings`; `cargo test` runs no clippy at all, so a 95-of-95 suite says nothing about the lint. Six findings, none of which changes what any program computes or costs: - four unused imports left behind while the assembly's fixture was being cut down; - `very_complex_type` on the tamper arm's site list, factored into a `TamperSite` alias — which then exposed that a boxed closure in a `'static` alias cannot borrow a local, so the `bump` helper became an item; - rustfmt's layout on the module declarations and the two new files. Verdicts at this tip: `make fmt` exit 0 with `git status --short` identical before and after; `make lint` exit 0, `Checking lambda-vm-prover` 6, zero `^error`, six `^warning` and all six the known `math-cuda: nvcc not found` build note; `-p stark --lib multilinear_logup` 10 of 10; `-p lambda-vm-prover --lib whir_` 95 passed of 102 listed, 7 ignored.
…e rs3's two open readings
Four things, all consequences of measurements the box returned.
THE PIN'S COMMIT TOTAL HAS NO BASE LITERAL. `COMMITS_BASE = 1_050` was a number
read off a run; it is not a constant, it is a sum the proof states. A group's
opening is a `StackedProof`, each of its polynomials a `ChainProof`, and
`rounds.len()` is one initial commitment plus `R - 1` successor codewords — one
commit per round. Summed over every epoch's groups and the cross-epoch proof's,
that IS the 1,050 `whir_epoch_shapes` prints as "chains 154 rounds 1050", and
DECODE's prepared opening adds `rounds.len() - 1` folds per epoch with its
polynomial committed once and held. `transcript_pin::commits` now takes the
bundle's proofs and computes it, and the harness builds that model in the same
block that reads the counter, so the two cannot describe different runs.
⚠ It is `cuda`-only and it carries an assumption the doc states: the counter
counts DEVICE commits, and a polynomial too small for the device is committed on
the host, where a fold commit is counted nowhere. The derivation therefore
assumes every chain reached the device, which holds for the pinned guest and not
in general — and the ELF sha guard is what lets the function assume it. The
shape half stays laptop-checked by
`the_prepared_opening_is_the_schedule_the_shape_implies`.
THE RESIDENCY COMMIT ASSERT IS A BOUND, NOT AN EQUALITY, because rs3's two arms
do not identify the model:
arm 1 device 7 host 2 seen 9 model 11 = groups 9 + prepared folds 1 + 1 held
arm 2 device 21 host 4 seen 25 model 30 = groups 26 + prepared folds 3 + 1 held
On arm 1 the shortfall of 2 is exactly the prepared group's held commitment and
its one fold, both invisible for the reason above. On arm 2 the same reasoning
accounts for 4 of the 5 and ONE COMMIT IS UNEXPLAINED, so `device == groups`,
`device == groups + prepared` and `device == model` are all refuted by the two
arms together. What is established is the direction that matters: every commit
the counters see is one the chains predict, and DECODE rebuilt per epoch adds
commits BEYOND the model. So `device + host <= model` is asserted and the
shortfall prints beside the term that should explain it, leaving the open number
visible in the box line.
THE ARM-2 VRAM BOUND IS BACK, on a measurement. rs3 read 570,425,344 B retained
after arm 1 and ZERO after arm 2, so the 544 MiB is one-time process cost — the
first arm's twiddle caches and module load, neither of which a pool trim can
return — and not a leak. Arm 1 stays a printed measurement; arm 2 carries
`retained < one DECODE codeword`, where the one-time costs are already paid and
the run's own buffers are the only thing left that could show.
AND THE REDUNDANT ABSORB IS ARGUED AGAINST WHERE SOMEONE WOULD ADD IT.
`register::preprocessed_columns_with_fini` gains a section saying why the epoch
statement does not absorb `init` or `fini` and must not: the roots fix the FINI
column before any challenge is drawn, and `check_preprocessed` binds the
verifier's own pair to that committed column at the reduced point, so a prover
cannot choose the claim after the fact. Absorbing them would bind nothing
further and would move every pinned constant. `absorb_epoch` carries the matching
warning, because that is the function someone would edit.
… the level-0 driver The level-0 WHIR driver was written on `whir/lfm` @ 7fc64a2 and stopped at two seams it could not reach from that base. This merge brings the base it needs. What arrives, and why the driver wanted it: - The REGISTER fix (5e3df0c). `build_epoch_airs` now hands `VmAirs::new` a `RegisterPreprocessed { commitment, init, fini }` and the branch supplies the columns closure as well as the root, so the multilinear verifier's `check_preprocessed` walks three columns for REGISTER where it walked none. The driver's own `an_epoch_that_does_not_verify_is_refused` documented the consequence — that a restated register carry was NOT a usable tamper — and that sentence stops being true here. - W1-B (491d2ef..4e3701f): DECODE's commitment derived from the ELF, held across the epochs and opened per epoch, with `MultiProof` carrying the prepared opening. The driver's `decode_commitment` argument is the host side of that. - The H-generic entry points and the seam-1 premise (214d7ad). `prove_epoch` is pub and generic; `verify_epoch_bookend::<H>` is `pub(crate)` with its `DecodePrepared<H>`. Seam 1 — the cryptographic hash refusal — becomes writable on this lineage for the first time, which is the next commit's work. - The alignment counter's statement mark (a96a287). THE MERGE IS DISJOINT AND THAT IS PRECISELY WHY IT PROVES NOTHING. The merge base is 7fc64a2, this side's only parent; this side touches `prover/src/lfm/mod.rs` and `prover/src/lfm/whir_epoch_tests.rs` and the other side touches neither, so git reports no conflict. But the driver's body is almost entirely calls into files the other side rewrote, so the question a conflict-free merge cannot answer is whether it still compiles and still verifies the same epochs. The four signatures it calls were read on the incoming tip before merging: `build_epoch_airs` keeps its eight-argument shape and builds the new struct internally; `verify_epoch` keeps its seven-argument shape; `prove_epoch::<H>` and `verify_epoch_bookend::<H>` are the seam's handles. The gate is the build and the suite, not this paragraph.
…han kept `the_register_carry_is_not_bound_on_the_multilinear_path` was an `#[ignore]`d, panicking test that FILED A FINDING: flipping one bit of `epochs[0].reg_fini` and harvesting epoch 1 — whose `register_init` IS that vector — was accepted. It was written that way deliberately, because asserting the observed behaviour would have recorded a suspected defect as intended behaviour. The finding is established and FIXED on the base this branch just merged, so the test now files a closed question as open — which is worse than not having it. A reader greps the name, finds a panicking test, and concludes the gap is live. The record that replaces it, on this tree rather than in a handoff: - 5e3df0c established it wider than a carry. Three epochs of `test_private_input_xpage` at 2^2, both index 1 and `X254_INDEX` (the commit index), accepted per epoch by `verify_epoch` AND through `verify_epochs`. - The mechanism is fixed at its source: `register::preprocessed_columns_with_fini` and `compute_precomputed_commitment_with_fini` are ONE derivation, and `VmAirs::new` takes `RegisterPreprocessed { commitment, init, fini }`, so the root the univariate verifier compares and the columns the multilinear one checks cannot describe different tables. - `a_restated_register_carry_is_refused_by_the_epoch_it_lands_in` and `a_restated_register_fini_is_refused_by_the_epoch_that_states_it` cover the vector from both ends, each beside the control that the honest epoch is ACCEPTED — so a verifier that refused everything would not pass them. - 5e3df0c also repaired two tests that could not have failed: `a_broken_register_carry_is_rejected` ran at an epoch size yielding ONE epoch and returned before its assertion, and `the_epochs_chain_through_their_registers` compared `1 >= 1`. ⚠ AND THE DELETION HAS BYCATCH, which is fixed here rather than left dangling. `an_epoch_that_does_not_verify_is_refused` pointed at the deleted test BY NAME for the reason its own tamper is the public output and not the register carry. That sentence was not merely a reference to a removed item: its claim ("the carry does not work as a tamper") is FALSE on this base. It now says what was wrong, that 5e3df0c fixed it, which tests cover it, and why the public output is still the right tamper for a driver test — it is the field `absorb_epoch` binds before any challenge, so it exercises the acceptance check through the statement the guest's replay reads. `the_hash_agreement_is_owed` stays: seam 1 is still owed. It is written next, now that the H-generic entry points are on this lineage.
… half `whir_bus_shapes` was written when only the bus statements existed and printed what they cost. The per-table verify is assembled now, so one card-free run can return the whole per-table half of epoch 0 instead of a term of it — which is the number item 5's recount against arm B's 12,301,266 actually needs, and the box's latency is the campaign's scarcest resource. Per epoch-0 table it now prints, beside the bus terms, the GKR ladder's length, the batched sumcheck's degree, and `table_verify_cost`'s rows and permutations; then the epoch totals. The sponge is THREADED across the tables the way an assembled epoch threads it rather than restarted at each one, so a table enters on whatever the one before it left. The output names what the total is NOT, rather than estimating those terms into it: the chain half, the DECODE group's own chain per epoch, `stacked_eval`'s wrapper, the epoch statement, and the preprocessed seam. ⚠ It also carries the warning that these rows INCLUDE their constants where `chain_rows` does not — `the_chain_emits_its_closed_form` subtracts `const_rows` before comparing, so 185,509 and the 1,484,072 chain half are const-free figures. Measured on the chain's own gated shapes, a chain interns 15 to 23 constants at five to nine variables, so the correction is small; the point is that the two halves must not be added without saying which convention the sum is in. The instrument has produced no log yet, so this supersedes the earlier invocation rather than invalidating a filed record. The command is unchanged; run it at this tip.
…constants
The number the campaign quotes — 185,509 rows and 22,828 permutations a chain —
was derived by EVALUATING the closed form at S = 25, k = 4, Q = 112, not by
emitting the program; the gated shapes run at five to nine variables. This emits
it, and the form is exact:
185,509 rows = 184,673 shape + 836 schedule
22,828 permutations = 22,512 openings + 40 grind + 276 schedule
both against the same numbers predicted, and every arena word hinted once. A
program costs nothing to build but its own construction — `chain_program` takes
the SHAPE alone, so no proof, no commitment and no guest ELF are involved, and
the whole thing is 221,288 instructions of which 35,615 are the hinted arena.
★ AND THE NUMBER THE CENSUS NEEDS: a production chain interns 39 CONSTANTS.
`the_chain_emits_its_closed_form` subtracts `const_rows` before comparing, so
`chain_rows` — and therefore 185,509 and the 1,484,072 chain half — is a
CONST-FREE figure, while V1e's per-table form includes its constants. The gap is
now measured rather than extrapolated: 39 rows a chain, 312 across epoch 0's
eight chains, 0.02 % of the chain half. Small, but the two halves must not be
added without saying which convention the sum is in, and now there is a number
to add rather than a caveat.
`#[ignore]`d: a few hundred thousand instructions is a second or two and a few
hundred megabytes, which is fine on a laptop and not something every
`cargo test` should pay.
…her than labelled The driver could not refuse a bundle proven under the wrong hash, and it could not be asked to: `ContinuationProof` carries no hash tag and cannot, because a WHIR proof's bytes are hash-agnostic by design — the byte gate asserts exactly that, both arms at 6904 bytes — and `whir_hash_knob::selected()` is a cached process setting that says what THIS PROCESS proves under, never what the bundle in front of it was proven under. So the agreement is the verification. `real_epoch_from_whir_continuation_under::<H>` verifies each harvested epoch under the hash it was HANDED, through `verify_epoch_bookend::<H>` and a `decode_prepared_for::<H>` built for the same `H`; a bundle proven under another hash fails there because the transcript's sponge is part of the configuration and every challenge diverges at the first squeeze. `real_epoch_from_whir_continuation` keeps its signature and dispatches through `with_whir_hash!`. The split mirrors `verify_epoch` and `verify_epoch_bookend::<H>` in the module it drives, so production keeps one entry point and the agreement gets one that can be argued about. ⚠ THE REFUSAL'S REASON NOW NAMES `H`, AND IT USED TO NAME THE KNOB. The message filled its slot from `whir_hash_knob::selected().name()`, which is wrong in exactly the case worth diagnosing: a keccak process harvesting under RPX would have reported "keccak256" while the verifier ran RPX. `verify_epoch_bookend` collapses every failure to `Ok(None)`, so this string is the only reason anyone gets, and it pointed away from the defect. `an_epoch_proven_under_keccak_is_refused_when_harvested_under_rpx` measures it. ★★ THE BUNDLE IS KECCAK BY CONSTRUCTION, NOT BY THE PROCESS DEFAULT. The cheap form of this test proves with `prove_continuation` and harvests at `RpxWhir`; `prove_continuation` dispatches on the cached knob, which is keccak only because `LAMBDA_VM_WHIR_HASH` is usually unset. Under `LAMBDA_VM_WHIR_HASH=rpx` that bundle is RPX, the two arms SILENTLY INVERT, and the failure reads as a broken hash agreement when it is a configuration mismatch. `a_keccak_bundle` re-proves the epochs with a literal `prove_epoch::<KeccakWhir>` through `for_each_epoch` and substitutes them into a real bundle, which keeps a real cross-epoch proof and a real touched page set. It costs one extra prove of the same run and makes the test mean the same thing in every process. ⚠ BOTH ARMS, ON THE SAME BUNDLE. The refusal is a bare `None` with no reason of its own, so a driver that refused everything would pass the refusing half alone. The accept arm — the same bundle, the same epoch, at `KeccakWhir` — is what makes the refusal mean anything. The process posture is REPORTED and decides nothing. `whir_process_posture_note` names a non-RPX setting because level 0's wraps commit under the RPX block hasher, and refuses nothing: a keccak bundle harvested under keccak is a correctly verified epoch, merely not the production posture, and a driver that refused it would break every keccak arm the campaign runs. ⚠ Its test asserts a RELATION and not a value. `selected()` is a cached process-global, so `assert!(note.is_some())` would be an assertion about how the whole test binary was invoked — green by default, red under `LAMBDA_VM_WHIR_HASH=rpx`, for a reason no reader would guess. What holds in every process is that the note fires exactly when the setting is not RPX. The "decides nothing" half is a check too: a bundle under the process's own hash still harvests. `a_restated_register_carry_is_refused_by_the_driver` replaces the red flag deleted in the previous commit, at the entry point level 0 actually calls. Both indices are flipped — index 1 and `X254_INDEX`, the commit index riding in the same vector — with the untouched bundle harvested first as the control. `the_hash_agreement_is_owed` is deleted: it is owed no longer. The module header stops saying the refusal is untestable on this base and records what the test measures instead.
Layout only. Verdicts at this tip: `make fmt` exit 0 with `git status --short` identical before and after; `make lint` exit 0, `Checking lambda-vm-prover` 6, zero `^error`, six `^warning` and all six the known `math-cuda: nvcc not found` build note; `-p stark --lib multilinear_logup` 10 of 10; `-p lambda-vm-prover --lib whir_` 95 passed of 103 listed, 8 ignored.
…fails both ways Two comment-only additions to the seam-1 tests, both recording measurements that were taken but lived only in a handback. THE RATIO, stated plainly rather than counted as two. Seam 1 has ONE program mutation — the verdict computed and discarded in `real_epoch_from_whir_continuation_under`, which makes the driver build a `WhirRealEpoch` from a proof that failed verification — and it turns the three refusal tests red on their own named assertions while the six others stay green. Running the refusal arm at `KeccakWhir` as well is NOT a second program mutation and is no longer written as if it were: it changes the TEST, being the accept arm read the other way, so what it shows is this test's discriminating power — that the arm measures `H` and not something incidental about the bundle. Calling both "mutations" would have claimed twice the evidence that exists. THE POSTURE NOTE'S TWO ASSERTS CATCH DIFFERENT DEFECTS, and now say so. The relation (`note.is_some()` iff the setting is not RPX) is the only thing true in every process, since `selected()` is a cached process-global. But a relation alone would pass a note that fired at the right time and named the wrong hash, so the setting is read into a local ONCE and the note's text must contain THAT name. Measured rather than asserted: making the note report the opposite setting leaves the relation holding and turns the test red on the naming assert.
…rived commit total) into whir/lfm The two test-only commits left behind when `whir/decode-group` @ 214d7ad was merged as c1e2b1c: - f1f0328 — the residency verdict completes before any commit model runs, and the device decomposition is PRINTED rather than asserted. rs2 had reddened on a commit prediction before arm 2 ever ran, so the primary instrument (one derivation per production run) never reported. The two counters count different sets: `note_host_fallback` has one call site, a chain's INITIAL commitment, while a card's `commit_calls` counts initial and fold commits both, and the test had summed them against one model. - 8ac8144 — the pinned commit total is derived from the bundle's own chains instead of the measured literal `COMMITS_BASE = 1_050`, which is why that constant disappears here, plus rs3's two asserts and the `reg_fini` doc lines. THE MERGE BASE IS 214d7ad, which is already an ancestor of this side through c1e2b1c, so this brings exactly those two commits and nothing else: four files, +306/−76. ★ THE ONE FILE BOTH SIDES MOVED IS `multilinear_bench_tests.rs`, AND THAT IS WHERE A 3-WAY MERGE COULD HAVE DONE REAL DAMAGE QUIETLY. This side re-derived the transcript pin when the 14-kind branch met the 15-kind one — prove 585,155 / verify 585,307, OWED 152, against the incoming branch's 585,140 / 585,292 — so a hunk resolved the wrong way would have restored the wrong numbers with no conflict to show for it. Two readings taken BEFORE merging said it would not: the incoming diff contains no line matching `585`, `OWED` or `owed`, and the pin on this side carries no `585` literal at all — it is computed, `OWED` being `OWED_CARRIED_ABSORBS + prove_derived_root_absorbs()`. The gate is that the pinned pair still prints the merged base's numbers, not this paragraph. A merge that reports no conflict has not been shown to build. The verdict is `make lint` and the suites at this tree.
…rough its chains Item 3 of the WHIR emitter: the wrapper `stacked_eval::verify` (`stacked_eval.rs:409-459`) puts around the weight leg — every column value absorbed, one batching draw, and one `whir_chain::verify_weighted` per stacked polynomial with `emit_weight_at` as its `W` and the batched column claims as its claim. `emit_stacked_verify` returns the batching challenge so a gate can compare it against the element the host verifier sampled; the host's verify returns only a verdict, and the position of that draw relative to the column absorbs would otherwise show up only as an absence of execution. THE THREADING. `chain_hash_schedule` built a `SpongeSchedule` internally and threw its successor away, so a wrapper could not say what its second chain enters holding. The round structure moves to `chain_sponge(shape, &mut SpongeSchedule)` and `chain_hash_schedule` becomes a thin wrapper over it. The alternative — replaying the structure beside it — would be a second copy that the chain's own schedule gate (`the_schedule_is_the_host_transcripts`, which compares that walk against a real verifier's calls) says nothing about; sharing the walk puts the wrapper inside that gate instead. THE FORM, `stacked_verify_cost` -> `StackedCost`, every term by its shape: C absorb `Unpack`s and the draw's `Pack`; `challenge_powers_rows(C)`; per polynomial its root's `Unpack`, `|columns|` rows for the claimed fold, its `weight_at_rows` and its `chain_shape_rows`; and one threaded schedule. The row count is CONST-FREE, the convention `chain_rows` is in and NOT the per-table form's — `own_constants` names the two kinds this leg owns by value instead: the `1` that the chains, `emit_challenge_powers` and `emit_weight_at` share, and one `leaf_capacity` per hash of the threaded schedule (`edsl.rs:676-692`). GATES, all on this laptop and needing no guest ELF: - the wrapper executes on a real `stacked_eval::prove` proof under RpxWhir that `stacked_eval::verify` accepts, and draws the gamma the host drew; - its threaded schedule is the host's own hash events, reconstructed by `HostDuplex` from a real verify and compared event for event; - rows and permutations against the emitted program, pinned apart; - the constant POOL as a SET: exactly the chain's arithmetic constants (from a one-chain program at the same shape, its own sponge's leaf capacities removed) plus the two kinds the form names. It measures that the pool does NOT grow with the number of chains — 20 constants over one chain and over two — which is what a census needs before it multiplies a per-chain constant count; - the production cross-check, shape-only: the DECODE group (five columns, one polynomial, n_stack 23, the posture `multilinear_prove.rs:93` sizes) threads to 202 squeezes and 17 state reads, reproducing the box's per-epoch hash-metrics counters. Test-side, in `whir_chain_tests`: `Recording`, `HostDuplex`, `CurrentBlock`, `chain_program` and the four instruction counters become `pub(super)`, and one chain's round wires and arena words are factored into `RoundStorage` and `push_round_words` so a program holding several chains builds them from the same walk rather than a second copy. `chain_program` and `chain_arena` are rewritten on top of them; the chain suite is the control that the factoring moved nothing.
…into the V1 emitter branch Item 4's prerequisite: the epoch statement is emitted against the base that computes its padding, so the branch takes the LFM base's tip rather than the 7fc64a2 it carried. What comes in: W1-B's computed statement padding and per-branch pin, the REGISTER preprocessed-columns fix (`build_epoch_airs` passing a closure so INIT/FINI are bound on the multilinear path), the pin derived from the bundle's own chains, and the transcript alignment counter with its statement mark. Git auto-merged the two files both sides had touched — `multilinear_table.rs` (this branch made `weights` public as `weight_slots` for the emitter; the incoming side rewrote the preprocessed seam) and `multilinear_bench_tests.rs`. That is a statement about text: the verdict is the build and the suites, taken at the tip and reported with this merge rather than inferred from the absence of a conflict.
…inear_table::verify The merge built RED, which is the half git's "no conflict" cannot report: `stark::multilinear_table::verify` gained a seventh argument on the incoming side and the per-table leg's two host-comparison call sites still passed six. `settled_out_of_band` is how many of a table's LEADING preprocessed columns a prepared opening has already settled at the reduced point, so `check_preprocessed` skips their MLE evaluations. This fixture has no preprocessed columns at all, so both sites pass zero — the value that also keeps the check maximally strict, said at the call rather than left as a bare literal. ★ The argument is the seam `emit_table_verify` already names. Its doc said the DECODE replacement was something the caller supplies; the host now takes the count itself, and the two sides have to agree on it. The doc is rewritten to say that, and to say what stays owed: every preprocessed column PAST that prefix is still an MLE pass the host makes and this leg does not.
…mit total) into the level-0 driver Brings the same two test-only commits this branch's base just took — f1f0328's residency verdict-first reorder with the printed device decomposition, and 8ac8144's commit total derived from the bundle's own chains instead of the measured `COMMITS_BASE` literal. Seam 2's harness will read the residency split's lines, which is why the driver branch takes it now rather than at the harness. Disjoint again, and again that proves nothing on its own: the incoming side touches four files, none of them this branch's two. The verdict is `make lint` and the driver's nine tests at this tree.
…ead of deriving one per epoch `real_epoch_from_whir_continuation_under::<H>` gains `prepared: Option<&DecodePrepared<H>>`. A caller walking every epoch of a bundle derives DECODE's prepared commitment ONCE and hands the same value to all of them; `None` derives it here exactly as before. On the block that is fifteen derivations rather than one. The STARK driver's `decode_commitment` argument is the precedent, and lane P measured that driver rebuilding its commitment 38 times over 19 epochs before it existed. ⚠ `decode_commitment` AND `prepared` ARE DIFFERENT OBJECTS AND BOTH STAY. Collapsing them would read as a simplification while quietly changing which root the AIR carries. `decode_commitment` is the UNIVARIATE preprocessed root from `commitment_from_elf` and feeds `build_epoch_airs`; `prepared` is the MULTILINEAR prepared columns, their derived roots and the stacked commitment, and feeds `verify_epoch_bookend`. The knob-dispatching `real_epoch_from_whir_continuation` passes `None` and keeps its five arguments. That is a constraint, not a choice: it has no `H` to name, so `&DecodePrepared<H>` cannot appear in its signature at all. The reuse is therefore available exactly where a level-0 walk will call it — the generic entry point, which knows its hash — and nowhere it would be a lie. Every existing test calls the knob form and needed no edit. ★ THE TEST IS THE REFUSAL, BECAUSE THE ACCEPT PATH CANNOT SEE THE DIFFERENCE. A driver that took the argument and derived its own anyway would harvest the good case exactly as one that used it. So `the_prepared_commitment_handed_in_is_the_one_used` hands in a prepared built from a DIFFERENT program and requires the refusal, beside the accept control that the bundle's own prepared commitment harvests. Ignored, the argument would leave the epoch verifying as it does today and the test fails. Measured rather than predicted — the refusal's printed reason is `epoch 1 of this bundle does not verify under keccak256`, which is the verification's own branch. So it fired on the CRYPTOGRAPHIC path, not on a shape guard: `DecodePrepared::agrees_with` compares only `log_blowup` and `log_folding`, which two programs at the same options share, so the wrong program's prepared sails past it and is caught by the derived roots block the transcript absorbs — the same mechanism as the hash agreement one commit back. ⚠ AND THE WRONG-HASH HALF IS UNREACHABLE RATHER THAN UNTESTED. A prepared built for the wrong hash cannot be handed to this function: `DecodePrepared<H>` carries the hash in its type and the driver is `::<H>`, so the mismatch is a compile error. Recorded in the doc as made unreachable, because a test for a state the type system forbids is a check that cannot fail.
… a lever rs4 on FAST at the 8f826601 fixture reads `ONE-COMMIT 0.083 s` for DECODE's prepared derivation (columns 5, rows 1,048,576, one GPU commit, no host fallback); rs2 read 0.068 s earlier, and both are single untimed reads. So fifteen harvests spend about 1.2 s deriving and handing `prepared` in once saves about 1.1 s of it. Written down beside the parameter precisely so it is not quoted as a lever: on a 220-second block that is a tidy-up. What makes the parameter worth having is that a walk over every epoch should not repeat a pure function of (ELF, options) fifteen times.
Item 4: `absorb_epoch` (`multilinear_continuation.rs:397`) and `absorb_global` (`:560`) written into a `WhirTranscript`, with the pad that closes them. ★ THE LEG EMITS NO OPERATION ROW, and that is a property rather than a shortcut. Every field of a continuation statement is a property of the epoch the program is compiled FOR, so the whole statement is a run of program-constant bytes; `absorb_const_bytes` packs such a run into felts at emit time by `sponge_leaf_bytes`' own rule, at any length. The cost is the DISTINCT felt values it interns and nothing else. A program that read these from an arena would be claiming to verify a shape it was not compiled for, and — the fields sit at offsets that are not multiples of eight — could not absorb them without the byte shift the transcript refuses by design. `EpochStatement` takes the `TableCounts` STRUCT, not an array of its values, and goes through the host's own `table_count_values`, so a field added to that struct moves the emitter and the host together. THE PADS, evaluated from the byte stream and asserted against the block's measured `WHIR-PAD` lines: the epoch's fixed part is 245 bytes counted field by field (tag 42, digest 32, label 8, the output's length 8, counts 15x8, the num-vars length 8, config 24, trailer 3), so `pad = (3 - |po| - |tnv|) mod 8` and the three block shapes give 1, 2 and 3 — the measured values. The global's fixed part is 134, so `pad = (2 - |table_num_vars|) mod 8`, which is 0 at the block's shape. ⚠ The campaign's `global pad = (2 - epochs - pages) mod 8` is the SAME formula and I briefly recorded it as refuted. `table_num_vars` is one byte per table and the cross-epoch proof's tables are every epoch's bookend plus the global-memory tables (`:556`), so `|table_num_vars| = epochs + pages`. The test now asserts that identity and the equality of the two forms, so the agreement is a measurement and not a coincidence, and it fails if the global's table set ever changes shape. The error was reading the two numbers a WHIR-PAD line prints (`page_bases`, `table_num_vars`) as the recorded formula's variables. GATES, all laptop-side and against the host functions themselves, which are `pub(crate)` and callable from here: - the machine draws the challenge the host draws, on all three block shapes and on the global — a transcript's state is not observable but its next draw is, so each arm runs the real absorb, the 32-byte root a verifier absorbs next (`multilinear_table.rs:659`) and one sample, on both sides; - the pads above, and the felt count they produce; - the row form: no operation, and the constant pool equal to the statement's distinct groups unioned with the two the squeeze interns — its `leaf_capacity` and the zero it pads a partial word with. The zero is free when the statement already has a zero group and costs a row when it does not, which is why the form is a union by value and not a `+ 2`; - the refusal, BOTH ways: at all 64 residues of the two variable lengths, a padded statement lets the root absorb and an unpadded one refuses it, at exactly the 56 residue pairs where the pad is nonzero.
S2 commits every trace tree with one bit-reversed row per leaf. The row-pair
row-major kernels read rows brev(2i), brev(2i+1) and cannot be reused at
another width (I-FRI-D note 1), so each hash gets its own one-row kernel
({keccak256,blake3,rpx}_leaves_base_row_major_row_range: row brev(i), a
column range).
- lde.rs: launch_row_major_leaves dispatches by rows_per_leaf (2 launches
exactly the kernels it did before); coset_lde_row_major_inner and the split
trees take rows_per_leaf; *_rpl public variants, the old names stay as the
row-pair wrappers. row_major_leaves is a host-matrix parity harness.
- merkle.rs / blake3.rs / rpx.rs: composition trees take rows_per_leaf; one
row uses the existing per-row ext3 kernels (same arguments).
- host KATs: the blake3 and rpx one-row kernels replayed thread by thread
against the CPU one-row leaf spec, every column range, plus a control that a
one-row leaf is not the row-pair leaf.
The default (rows_per_leaf = 2) launches the same kernels with the same
arguments.
…input tree Lifts I-S2-H's CPU-only gating for one-row tables: every device arm now follows the table's leaf layout (table_leaf_layout, per table under auto, so one proof may mix device row-pair and device one-row tables). - gpu_lde: the fused main commit, the preprocessed split, the aux commits (host input and resident) and both composition-tree entries take rows_per_leaf; LFM artifact commit via try_commit_row_major_with. Counters gpu_one_row_trees / gpu_one_row_tree_peak_bytes / gpu_one_row_fri_calls (tests assert on them so a host fallback fails). - FRI: the group drive commits layer 0 (the input tree) from the codeword with zero folds and NO challenge before it under one row (the CPU loop's pending = 0); the one_row declines in fri_commit_gpu_drive, fri/mod.rs and the DEEP->FRI arm are gone, so the tree is built off the resident DEEP codeword. - prover: device openings at row r (device_query_rows / device_rows by layout, the host cross-checks by layout); one-row tables may be device-only and keep the resident aux build. - device_set: tree_bytes_for(lde, rows_per_leaf) — a one-row tree is (2*lde-1)*32 bytes; commit/table sets and the VRAM gate estimates take the layout; FRI admission uses the one-row bound under one row. - lfm/commit.rs: REVIEW-FRI F8.1 lifted (device one-row artifact roots) with a cuda parity test against the host one-row root. Default format: rows_per_leaf = 2 everywhere, the same kernels and the same admission numbers (device_set test pins table_device_set_rpl(_, 2) == table_device_set).
…ee, (e) vectors, VM bytes - stark::s2_device_parity (cuda, test/test-utils): one-row and row-pair device trees against the host over the same evaluations — fused main, preprocessed split, aux (host input and resident), composition (host parts and resident slabs); roots, leaf counts, paths gathered off the resident trees, and the device row gathers at the query rows; the (e) leaf-digest KAT; 13 cases per hash, one S2DEV line each. - fri::device_parity: fri_parity runs one-row layouts (layer 0 = input tree, queries over the whole LDE); one_row_cases (40) and one_row_resident_cases (5), pinned by count. - tests::zf_s2_device_tests (Keccak, Blake3) and zf_rpx_device_tests (RPX): trees, FRI and resident FRI parity, and the (e) vector proofs proved on the device equal the checked-in CPU bytes (one one-row device FRI commit per proof, >= 3 one-row device trees per proof). - zf_vm_one_row_tests::one_row_vm_proof_bytes_for_the_device_comparison (ignored, box): writes the one-row VM proof bytes (grinding 0) from a CPU build and a cuda build for a byte compare; the cuda run asserts the device one-row paths fired and prints the ZF S2 DEVMEM line.
…(RULINGS 22) The fri=dp schedule DP now prices every row the in-guest verifier emits for one query's opening of a committed FRI layer, not only the slot mux, the group fold and the twiddle chain: the x_g derivation (d selects + d BALU), fold-level scaling (max(0, d-2) XALU + [d>=2] BALU), the slot assert (2 XALU), the root compare (8 BALU + 1 unpack), the group's 2^d value hints and unpacks, the leaf's ceil(3*2^d/4) Pack rows, and the path's sibling hints (depth - c: a cap now also saves c hints per query). fri_group_layer_rows and fri_pair_layer_rows are the row model; lfm::fri_group_tests pins them against the emitter kind by kind and in total, for d = 1..6 and today's pair layer, at caps 0, 1 and 2. The legacy pair-layer body moves into emit_pair_layer (the same instructions in the same order) so it can be measured. The S2 auto rule gains the in-guest DEEP term: row pairs evaluate DEEP at two points, one row at one, each num_surviving + 4E + P + 3 XALU rows (deep_point_xalu_rows, pinned against emit_deep_point); TableWidths carries it from the AIR's OOD layout. The FRI chain is priced by FriFormat::chain_cost_q, with today's pair encoding priced as pair layers when the format is legacy. Format changes (default proofs unchanged; goldens green): - U1: cap auto unchanged; cap off T=9 B=16 S2 and B=17 S3 [4,3] -> [3,2,2], T=10 B=14 S2 and B=15 S3 [4] -> [2,2]. - a_schedules.json regenerated (12 of 456 schedules move, every cost moves, weights_ns gains xalu/balu). No proof vector (d, e) moved. - auto pins: the MEMW-like and the narrow short preprocessed cases now go one row. - the device parity shape list drops [4] from the DP's own set; [4] is kept as an extra shape so the sweep still covers it (29 cases).
The box wrapper names a fresh directory per run; creating it in the test keeps the extras line self-contained.
…RI row priced, the S2 DEEP term)
… folds, FRI host S3) and the gate fixes 737415e = zf/candidate-b f985944 (merges of e6ea359 I-CAP-S wave B, d281c3b I-CAP-W, ac73346 I-WHIR-F, 6092c77 I-FRI-H) + I-FIX-B's five commits: the AIR prototype cache in prover/src/test_utils.rs now keys the whole ProofOptions (format included); the WHIR eviction test evicts before every cap height; the cuda-size tests prove the bus_permutation AirWithBuses example; merkle_cap_vm asserts the cap engaged. Gates on FAST at 737415e (default format): zf-gates GATES GREEN in 19 steps; prover lib 1494 passed / 0 failed / 86 ignored; math-cuda 214 / 0 / 10 (the lane pre-registered 197: a count error, zero failures); the 13 knob-on extras at their counts; CAPDEV 9 and CAPVM 112 device cap reads; capped tables 14 of 14 (CPU and cuda). Measured (block A/B/B/A on FAST): W2 first6 -9.30 s, W1 -0.95 s, W1+first6 -9.10 s on the WHIR block.
…LINGS 26) ZfFormat::DEFAULT, what every production site stamps when no knob is set, becomes the configuration the block runs measured net positive: cap=auto, whir_cap=auto, fri=dp, whir_folds=first6 (one_row stays 0 here; it flips in its own commit). ZfFormat::LEGACY is every lever off, and every knob keeps its off spelling (cap=off, whir_cap=off, fri=pair, one_row=0, whir_folds=uniform4), so all five at off reproduce the pre-campaign format for rollback and A/B. Security parameters (queries, grinding, blowup) do not move. The crypto crates' own defaults (stark ProofFormat::DEFAULT, multilinear ChainFormat::DEFAULT) stay the legacy format: ProofFormat gains LEGACY and is_legacy(), ProofOptions gains has_legacy_format(). ProofOptions' format is still skipped by serde and rkyv, so no serialized byte moves (RULINGS 10). The RV64 recursion guest stays on the legacy format explicitly: every Preset and MIN_PROOF_OPTIONS name ProofFormat::LEGACY, and both guest entries refuse anything but the legacy format, the production default included (the_recursion_guest_stays_on_the_legacy_format). Pins: - RPX goldens: the legacy set is kept (legacy_format_rpx_goldens_are_byte_identical, bytes unmoved) and a production-default set is added. - WHIR production chain at the default (first6 under the auto cap, S=25, Q=112, grind 20): 16,443 permutations, 203,426 rows, emitted == closed form; the legacy chain pins (22,828 / 185,509) are unchanged. - whir_epoch_program_tests::the_production_epoch_recount is a record of sh1, measured at the legacy format: its config is now named LEGACY, and the default's 6 rounds at 25 are asserted beside it. - The hash-metrics transcript pins were measured at the legacy WHIR format: their closed-form tests use the legacy config, the runtime pins skip (and say so) at any other WHIR format, and the DECODE opening's schedule assert follows the process format ([6,4,4,4,4,1] at the default; same counts). - transcript_counts drives ChainConfig::schedule instead of a uniform fold width, so its closed form prices first6 as proved.
… format It asserted that the PROCESS format is not legacy, so the legacy A/B arm (every ZF knob at off) turned it red. It now checks ZfFormat::DEFAULT for that, and refuses block_base_options() only when the process format is not legacy (always, with no knob set).
…ULINGS 26) ZfFormat::DEFAULT gains S2 one_row=auto: per table, one-row openings where the shared cost function prices them cheaper, row pairs elsewhere. It is PROVISIONAL (pre-registered net positive on STARK, neutral on WHIR) and is its own commit so it reverts cleanly if the ds30-35 / wt72-77 arms disagree. LAMBDA_VM_ZF_ONE_ROW=0 keeps selecting row pairs. No pinned byte moves: the production RPX goldens' AIRs all resolve to row pairs under auto (now asserted), one-row bytes stay pinned by the (e) vectors and the VM device comparison, the static one-row twins exist at blowup 4 (the production blowup), and the LFM registry policy is read off the options each caller passes (a one-row format builds the roots at run time), not off the process format. Banner: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6.
…ding the process format It built the production chain through chain_config, so the legacy A/B arm (every ZF knob off) read uniform4's seven rounds where the assert expects the default's six. It now builds ZfFormat::DEFAULT's config explicitly.
… leaf layout Under one-row openings (S2) the STARK prover absorbs a preprocessed table's root of that table's leaf layout (`precomputed_commitment_for(layout)`) before sampling the shared LogUp challenges z and alpha, and the STARK verifier does the same. `replay_transcript_phase_a_view`, which the LFM verify path and the VM/continuation commit-bus balance use to recover z and alpha, still absorbed the row-pair root (`precomputed_commitment()`) for every table. For a one-row preprocessed table the replay diverged, the expected public balance was computed at the wrong z and alpha, and `multi_verify_views` rejected an honest proof whenever that balance depended on them: every LFM proof (the published words) and every VM proof with public output. This is why the block tree's level-0 wraps failed `verify_against_artifacts` at one_row=auto (wt73, ds31) while the base epochs, which publish nothing, verified. The replay now resolves the layout exactly as the prover and verifier do (`table_leaf_layout(air, proof.trace_length())`) and absorbs that layout's root; a table with no root for its layout returns None and the caller rejects (RULINGS 14), so the replay returns Option<(z, alpha)>. Verifier-side only: no proof byte moves. At the default format every layout is row pairs and the absorbed root is byte-identical to before.
… auto, VM with public output) Two round trips that fail before the replay fix and pass after: - an LFM proof (TrivialV0) at the wrap's options (blowup 4, terminal 2^8, 128-bit queries) under one_row=auto: layouts mix within the proof and 8 preprocessed chips go one-row (asserted, so the test keeps exercising the bug); verified through verify_against_artifacts, the call the tree harness makes, and through lfm_verify; a moved public word still rejects. - a VM proof with public output (test_commit_4) at one_row=1; a moved output byte still rejects.
The CUDA composition arm evaluates `AIR::constraint_program()` once main and aux are device-resident. `LogReadOnlyRAP`, the AIR of the checked-in S3 (d) and S2 (e) proof vectors, had none, so the four device full-proof byte tests (`proved_vectors_equal_the_cpu_bytes`, `proved_one_row_vectors_equal_the_cpu_bytes` and their RPX twins) panicked in the trait default before comparing a byte. The program is captured once (OnceLock) from the same `LogReadOnlyRAPConstraints` body the CPU folders run, so the device composes the same polynomials and no vector byte can move; the CPU prover never reads the program. New CPU tests pin folder == interpreted program == lowered device program (host model of the kernel) on random frames. The four device tests now also assert that every proof composed on the device (`gpu_composition_calls` moves once per proof), next to their existing FRI and one-row tree counters, so a host composition fallback fails them.
…ed twice per process
`one_row_vm_proof_bytes_for_the_device_comparison` compared a CPU-build and a
cuda-build RV64 VM proof of `test_mul_8`, on the premise that at grinding 0
the proof is a function of the ELF and the format. It is not: six base-table
builders dedup through a std HashMap (RandomState) and lay rows out in
iteration order, so the main roots and the whole transcript change per
process; the lead's control showed the same build differing from itself in
~80% of the bytes. The test is deleted (pinning the VM row order would move
every proof and is not this lane's call).
The replacement, `zf_lfm_bytes_tests::lfm_proof_bytes_for_the_device_comparison`
(ignored, box), proves the `TrivialV0` LFM machine program (public output,
so the balance depends on z, alpha) at blowup 4, 128-bit queries, grinding 0,
under `legacy`, `one_row_1` and `production` (cap auto, fri dp, one_row auto),
proves each TWICE in the same process and asserts the two byte strings equal,
writes `$ZF_S2_PROOF_DIR/{cpu,cuda}_<fmt>.rkyv`, then verifies. Under cuda the
`one_row_1` arm must build one-row trees and take the one-row FRI commit on
the device; the legacy arm must do neither.
…ry arm Under cuda each format must commit FRI on the device for its two large chips (2^16 and 2^20 rows, above the default device floor), so a host proof cannot pass as a device proof in the cross-build cmp; the counter is printed on the `ZF LFM DEVICE` line. Also make fmt.
… the layout root) Lane I-FIX-S2, second parent 91764db: 6a4a244 replay_transcript_phase_a_view absorbs precomputed_commitment_for(table_leaf_layout) and returns Option (a missing root rejects, RULINGS 14); 91764db adds two one-row regression tests (LFM at the wrap options under auto, VM with public output). Conflicts: none.
…OnlyRAP program, LFM bytes oracle) Lane I-FIX-D2, second parent 39dea55: LogReadOnlyRAP gets a constraint program captured from its CPU constraint body (+ tests), the four device byte tests assert one device composition per proof, the LFM bytes oracle lands in prover/src/tests/zf_lfm_bytes_tests.rs, and the invalid VM-bytes test one_row_vm_proof_bytes_for_the_device_comparison is deleted. Conflict: prover/src/tests/zf_vm_one_row_tests.rs (one file). Resolution: kept I-FIX-S2's two regression tests (an_lfm_proof_at_the_wrap_options_round_trips_ at_one_row_auto, a_vm_proof_with_public_output_round_trips_at_one_row) and its module-doc bullet; kept I-FIX-D2's deletion of the VM-bytes test and its doc comment; dropped the module-doc bullet that described the deleted test.
…nally (RULINGS 26)" This reverts commit 0dd6341 (I-FLIP commit B). The DROP-B variant of candidate-f, prepared for the lead's decision on the provisional one_row=auto default (RULINGS 26): the default format keeps commit A (cap=auto whir_cap=auto fri=dp whir_folds=first6) with one_row=0. LAMBDA_VM_ZF_ONE_ROW=auto still selects S2. Commits cfbff6a and 5ed2f15 belong with A and stay.
…levers as separate arms The `production` arm proved cap auto + fri dp + one_row auto, which is no longer the prover's default format (one_row stays off by default). The oracle now has four arms: - legacy: every lever off (bytes unchanged); - one_row_1: legacy + one row on every chip (bytes unchanged); - production: the STARK part of ZfFormat::DEFAULT (cap auto, fri dp, one_row off), asserted equal to what the default stamps so the arm cannot drift; - all_levers: cap auto + fri dp + one_row auto, the former `production` arm, with the same bytes. Every existing assertion is kept: twice-equal bytes per process, verify, and the cuda counters (one-row device work only where one_row is on).
Comments only. Every comment line added since the proof-format work began now states its reason in place instead of pointing to material outside the repository (design notes, review findings, rulings, run tags, work-lane names). Soundness reasons are written out where they apply: a one-row layout with no preprocessed root is a hard miss, never a recompute; exact path lengths keep a leaf hash from being compared with an internal node; the RV64 recursion guest verifies the legacy format only. The ZfFormat::DEFAULT doc now says why one_row stays off: in ABBA block runs it costs +3.2 s on the WHIR pipeline and saves 8.0 s and 8 GiB of host memory on the STARK pipeline, so it is a knob (LAMBDA_VM_ZF_ONE_ROW=auto) recommended for the STARK pipeline. Unchanged because they are code, not comments: the test name the_production_shape_reproduces_the_campaigns_permutation_count (and its two doc links) and one assertion message in whir_chain_tests.rs.
Merkle caps on every STARK and WHIR tree, FRI folds by 2^d with a verifier-side DP schedule, and a six-variable first WHIR fold are the new default format (cap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6). One-row openings with a committed FRI input are built and selectable (LAMBDA_VM_ZF_ONE_ROW=auto); they stay off by default. Also: the Phase-A replay absorbs each preprocessed root at its leaf layout, and the device byte-parity tests run on a card.
…eline's best configuration
MauroToscano
changed the title
|
Benchmark Results for unmodified 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. ABBA on one binary: the new default against the legacy format, two arms each, alternated.
That is −20.55 s (−16.1 %). A no-knob run on the final code read 107.0 s, with a permutation census and program ids identical to the arms above. For reference, the STARK pipeline measured 159.35 s before these levers and 129.55 s with them, in the same kind of ABBA.
What is in the branch
ZfFormat(prover/src/zf_format.rs) parses fiveLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT:banner. The default iscap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6:LAMBDA_VM_ZF_ONE_ROW=auto) are built on host, GPU and in-guest, but off here: they cost +3.2 s on this pipeline. They are on in the STARK pipeline's PR (Per-table GPU recursion, end to end: one root for block 25368371 #985), where they save 8 s.ZfFormat::LEGACYstays pinned by a golden test. The RV64 recursion guest verifies only the legacy format.main: perf(alloc): compile jemalloc's never-purge policy into the binary #996 (jemalloc never-purge compiled into the CLI).Soundness of the format levers
Query counts, grinding bits and blowup are unchanged.
Fixed along the way
Gate and CI
The final gate ran at
d8ffc0702, whose prover library is identical to this branch's;main's merge adds only CLI and test files. It ran on the FAST box:--test-threads=3.In CI, one prover shard's hosted runner receives a shutdown signal and SIGKILLs
epoch_chunk_multiplier; this branch failed the same way before the format levers. That test passes on the box.Open decisions
one_rowdefault. A per-pipeline default would let one PR carry both.