Make the WHIR path's hash a parameter, and add an RPX256 instantiation - #992
Draft
MauroToscano wants to merge 28 commits into
Draft
MauroToscano wants to merge 28 commits into
MauroToscano wants to merge 28 commits into
Conversation
`Traces::from_elf_and_logs` takes a fifth argument under the `disk-spill` feature (`prover/src/tables/trace_builder.rs:4535-4541`, `#[cfg(feature = "disk-spill")] storage_mode: StorageMode`). Four call sites in `multilinear_bench_tests.rs` pass four arguments unconditionally, so `make lint`'s third pass — `cargo clippy --workspace --all-targets --features lambda-vm-prover/disk-spill` — fails with four `E0061`s and the feature's tests cannot build. VERIFIED PRE-EXISTING, by a controlled run rather than by inspection: the identical four errors appear at lines 113, 500, 690 and 883 on a pristine checkout of this commit's own parent. Nothing above this commit introduced them. The repair is the idiom the crate already uses at `prover/src/multilinear_prove.rs:190-197` — the argument inline under its own `cfg`, so the default build is unchanged and there is no second call shape to keep in step.
…the default The WHIR path hard-codes keccak-256 in three places — the Merkle backend (`whir_commit.rs:25`), the Fiat-Shamir sponge (`DefaultTranscript`'s `hasher` field) and the proof-of-work grind — and a recursion arm needs it to be RPX: a keccak-f costs ~73,700 LFM cells against RPX's 325, which is the difference between a WHIR wrap that is 2x today's and one that is a third of it. This is the seam, with nothing behind it yet. WHAT THE SEAM IS. One trait, `multilinear::whir_hash::WhirHash`, naming the Merkle backend AND the Fiat-Shamir configuration the grind follows. One trait rather than three parameters, because separate ones make the HALF-FLIP spellable — one hash's trees under another hash's sponge, which is self-consistent between prover and verifier and therefore silent. Here there is one name to write, so there is nothing to assert against. WHAT DOES NOT MOVE. `Commitment` stays `[u8; 32]` for every hash: a keccak digest is 32 bytes and a four-felt Goldilocks digest is 32 canonical bytes. So `MultiProof`, `TableProof`, `StackedProof`, `ChainProof`, `CosetOpening` and `Proof<Commitment>` keep their layout, their rkyv derives and their serialized length. A hash swap is not a proof-format change. The parameter threads through six modules — whir_commit, whir_round, whir_chain, stacked_eval, stark::multilinear_table, prover::multilinear_* — and three types gain it (`CodewordCommitment`, `StackedCommitment`, `CommittedTables`), each defaulting to `KeccakWhir` so existing call sites read unchanged. Grinding becomes generic over its digest with NO default: a defaulted proof-of-work hash would silently keep grinding on keccak for a configuration that had moved everything else. THE BYTE GATE, AND THE CORRECTION IT FORCED. The gate was designed as "hash the proof with every grinding nonce zeroed", on the reasoning that the nonce is the only nondeterministic field. `whir_identity_tests` found that wrong: the nonce is ABSORBED into the transcript (`whir_chain.rs:119`), so every challenge after the first grind depends on which valid nonce the search returned, and the divergence is not in the nonce fields. Two further findings came out of the same test — a proof of the same program is not byte-reproducible across processes for a second, unrelated reason (six trace generators lay their rows out in `HashMap` iteration order, `eq.rs:128` and five siblings), and the committed trace's root precedes the first grind and so cannot depend on it. So `crypto::grinding` gains `generate_nonce_smallest` — the smallest valid nonce, a function of the seed alone — reached in production through `LAMBDA_VM_DETERMINISTIC_GRIND`, off by default and changing nothing about validity. `prover::whir_identity` is the instrument; its six tests pin what it can and cannot see, including the correction, so the next reader is told by a test rather than by a comment. `make lint`: passes 1-3 exit 0 (pass 3 needs the `disk-spill` repair in the commit below this one). Pass 4, `--features lambda-vm-prover/cuda`, is RED AT THE AUTHOR'S HEAD `307d7c00` with six errors, all in `crypto/multilinear/src/gpu.rs` — a file this commit does not touch. Verified by a controlled run on a pristine base, not inferred; the repairs land separately so they can be taken or dropped on their own. Tests: crypto 59 passed (4 new), multilinear 286 passed, stark 256 passed, prover multilinear 30 passed / 8 ignored, prover whir_identity 6 passed.
The hash the recursion arm needs. A keccak-f[1600] costs ~73,700 trace
cells in a field-native verifier against RPX's 325, so a WHIR proof
verified inside another proof pays ~227x less for its hashing under this
configuration. Nothing here is an improvement for a host prover and the
module says so: RPX is slower than keccak in software, and the only reason
to pay for it is the verifier that is not a host.
PORTED, NOT INVENTED. The permutation, the leaf construction, the parent
and all 168 round constants come from `prover::lfm::{rpo, rpx,
algebraic_commit}` on `per-table-gpu` (`9f6e964b`, `5ceeef29`, `73ee2a64`,
`5482c067`, `ab8f5b0f`, `80d74632`), byte for byte, because the CUDA kernel
`50c633e1` and its known-answer tables are pinned to exactly those. A
cherry-pick was not available: none of those commits is an ancestor of this
branch's base, and they are written against `StarkHash` / `CommitmentHash`
/ `IsStreamingLeafBackend` / the LFM's own types, none of which exist here.
The LFM machine itself is NOT carried over — no chip, no AIR, no eDSL, no
witness recorder.
TWO ANCHORS, OF DIFFERENT STRENGTH, AND THE MODULE SAYS WHICH IS WHICH.
* RPO's half is EXTERNAL. RPX is a round-schedule swap on RPO's geometry
with literally the same constants, so seven `fb_round`s composed ARE
RPO256 — and `seven_fb_rounds_are_rpo256` replays miden-crypto's
nineteen published `hash_elements` vectors through them. Those
seventy-six numbers were produced by nothing in this repository, and
they pin ARK1, ARK2, the MDS row AND its orientation, both S-box chains
and the lane convention at once.
* RPX's own half is NOT externally anchored. miden publishes no RPX
known-answer table (verified: its `rpx/tests.rs` has only structural
tests). The RPX vectors here are transcribed from
`math-cuda/tests/host_kat/rpx_kat_vectors.h` on the per-table branch —
the per-table host speaking, not an external publication. That is still
worth having for a reason beyond agreement: the CUDA kernel is pinned
to those same tables, so a port reproducing them is byte-compatible
with both that branch's host and its device, which is what H2's device
half will need.
* The E round and the schedule have no oracle at all, so they rest on
independent algorithms: the cubic product against naive polynomial
arithmetic mod phi^3 - phi - 1, `power7` against square-and-multiply,
the inverse S-box against `pow(INV_ALPHA)`.
Also extended, rather than caveated: `hash_metrics` was keyed on
`TypeId::of::<PlatformKeccak256>()`, so under RPX every Merkle counter
would have read ZERO — a check that cannot fail, reporting "no hashing"
for the arm whose purpose is to change the hashing. The algebraic backend
bumps `count_merkle_direct` / `count_merkle_node_direct`, which also bump
`total` because no digest `finalize` will. Five tests gate it; mutation-
tested by removing the backend's counter calls, which fails exactly the
three that assert the counting and leaves the keccak case passing.
Byte gate (canonically-ordered EQ fixture, grinding off): identity line
7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880
bytes — identical at 307d7c0, at bcdd3dd and here.
Tests: crypto 87 (92 with `hash-metrics`), multilinear 286, prover whir 14.
`make lint` passes 1-3 exit 0, plus `-p crypto --features hash-metrics`.
Pass 4 (`cuda`) remains red at 307d7c0 in `multilinear/src/gpu.rs`, which
this commit does not touch.
`hash-metrics` is host-only and off by default, so not one of `make lint`'s
four clippy passes compiled it and `make test` never ran its tests. That is
how its Merkle counters came to be keyed on `TypeId::of::<PlatformKeccak256>()`
and stayed that way after a second hash arrived on the multilinear path:
under RPX every one of them read ZERO, reporting "no hashing" for the arm
whose entire purpose is to change the hashing, and nothing in the build
could notice.
Two lines, in the two targets that mean different things:
* `lint` gains `cargo clippy -p crypto --all-targets --features
hash-metrics`, so the feature keeps COMPILING and linting;
* `test` gains `cargo test -p crypto --features hash-metrics`, so its
tests actually RUN.
Deliberately not one line doing both: lint compiles and lints, test runs
tests, and a lint target that executed tests would make the fast gate slow
for everyone.
`make lint` is now five passes. Four are clean; the `cuda` pass was already
red at 307d7c0 in `crypto/multilinear/src/gpu.rs`, which no commit on this
branch touches.
The instrument the hash work is measured against: keccak-256 over the rkyv bytes of a fixed, unground EQ-table proof, printed rather than asserted so two revisions can be compared. WHY THE SORT. The obvious version of this — hash the proof of `generate_eq_trace`'s output — is NOT reproducible across processes, and quoting it across two revisions produces a number that looks like evidence and is not. The generator deduplicates through a `HashMap` and lays its rows out in iteration order (`prover/src/tables/eq.rs:128`); five siblings do the same. Four consecutive runs of the unsorted form, on one unchanged tree and one unchanged binary, gave four different digests — recorded in the module header, because two of them agreeing by chance across two revisions is roughly a one-in-ten event and it happened to me. So the rows are sorted HERE, in the measurement, after the generator returns. Row order is free to the argument — the bus is a multiset — so the sorted trace still proves and verifies; it is simply reproducible. None of the six builders is touched. THE EXPECTED VALUE, and the gate: 307d7c0 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880 bcdd3dd 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880 29fbb45 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880 A commit that moves this line has changed the proof PR #988 produces and owes an explanation. `#[ignore]`d with a reason string, because comparing two runs is something a harness cannot do for you. Grinding is off, so this covers no proof-of-work path; `whir_identity_tests` records why a ground proof cannot be gated this way at all.
The host half of H2 gave the WHIR path an RPX configuration; under `cuda` that configuration was still a label on a tree keccak's kernels built. This is the other half. WHY A KEY AND NOT A TYPE. On the host a Merkle backend both NAMES a hash and computes it, so a tree cannot wear a name its own code did not produce. On the device the backend only names it — the kernels hash — so nothing but a key travelling with the request stops a tree labelled RPX from being built by keccak. `math_cuda::DeviceHash` is that key; every launch site matches on it exhaustively, so a hash added later is a compile error at each site rather than a silent fallthrough to whichever arm came first. `WhirHash::DEVICE` carries it from the configuration, as its own `DeviceHashKey` rather than `math_cuda::DeviceHash` directly, because `math-cuda` is optional and the trait must exist without it; the bridge between them is total both ways and asserted at compile time, as is the rule that a configuration and its device key answer to the same name. TWO KERNELS THAT EXISTED NOWHERE. `per-table-gpu` has seven RPX leaf kernels and all seven hash a ROW GROUP. WHIR's leaf is a fold COSET — leaf `j` holds the positions strided by `num_leaves` — so `rpx_leaves_base_coset` and `rpx_leaves_ext3_coset` are new here, twins of `keccak.cu`'s pair, argument for argument. `rpx_merkle_level`, `rpx_merkle_tail` and `rpx_grind_search` come over unchanged. GATED ON A LAPTOP, WITHOUT A CARD. `rpx.cu` compiles as ordinary host C++ through `cuda_host_shim.h`, so `make test-rpx-host-kat` pins its arithmetic, its schedule, its sponge, its parent and every leaf kernel's read pattern in seconds. The two new kernels get their own case, built from the definition (`codeword[j + t * num_leaves]`) rather than from a second call, plus a control asserting the strided read differs from the contiguous one — otherwise the whole case would pass on a kernel that dropped the stride whenever `num_leaves == 1`. Mutation-checked: replacing the stride with `tid * block + t` fails it. ⚠ Necessary, never sufficient. The shim cannot tell you whether nvcc accepts the file, nor anything about execution rather than arithmetic — grid indexing, register pressure, local-memory spills. Those need the box. THE PARITY TESTS ASSERT THE DEVICE PATH WAS TAKEN. `commit_codeword_to_host` has no host fallback: it runs the kernels or errors. That matters because the commit path proper falls back silently (below a size threshold, with no card, under `LAMBDA_VM_NO_GPU_WHIR_COMMIT`), and a parity test that allowed it would compare the host against itself and pass — the shape recon B found in `whir_fold.rs`. Both hashes run every shape, and a third test requires the two keys to produce DIFFERENT device trees, which is what a dispatch ignoring its key would fail. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880 bytes, as at 307d7c0. Tests: host KAT all pass (now including the coset kernels), crypto 87, multilinear 286, prover whir 14. `make lint` passes 1-3 and the hash-metrics pass exit 0; the cuda pass is still red at 307d7c0 in `gpu.rs`, repaired by the commit after this one.
…t pass runs `make lint`'s fifth pass — `cargo clippy --workspace --all-targets --features lambda-vm-prover/cuda` — has been failing with six errors from four findings, all in `crypto/multilinear/src/gpu.rs`. VERIFIED PRE-EXISTING by a controlled run on a pristine checkout of 307d7c0, this branch's base: the identical six appear there, and no commit on this branch touches the code they name. A whole lint pass nobody can run is worse than the findings in it: it is the pass that covers the cuda-gated modules, which is most of the device work this branch is about to add. Each is repaired on its own terms, not silenced: * `items after a test module` — `mod tests` sat in the middle of the file with ~1,290 lines of production code after it. Moved to the end, where a reader expects it. No code changed. * `type parameter F goes unused` — `columns_at<'a, F>` never mentioned `F`. Dropped, along with the turbofish at its two call sites. A type parameter a function does not use is a claim about it that is not true. * `very complex type used` — the device sumcheck's return tuple, written out inside a `Result`, where it reads as punctuation. Named `ClosedRounds`, beside the existing `ResidentRounds` it is a two-member variant of; the doc says which path each belongs to. * `field 0 is never read` on `DeviceRoom` — and here the lint is wrong. The field IS the behaviour: an RAII guard whose `Drop` returns the device reservation, so holding it is the whole point and deleting it would delete the promise. `#[allow(dead_code)]` on the field, with the reason written where someone tempted to delete it will read it. `make lint` is now five passes, all five green, for the first time on this stack. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880 bytes. Tests: multilinear 286, crypto 87, prover whir 14.
`ChainConfig::with_security` computed `num_queries` with `f64` sqrt, log2 and ceil. That is fine on a host and a problem everywhere this protocol is headed: a field-native verifier has no floating point, and a prover and verifier that disagree by one query do not fail gracefully — the transcript diverges and every challenge after it is different. The formula is unchanged, including what it is not: the conservative mirror of the parameters the univariate prover ships, and not a soundness analysis of this protocol. Moving it to integers changes who can evaluate it, not what it claims. Fixed point at Q62 in a `u128` — more precise than the `f64`'s 53-bit mantissa, so the only way the two could still differ is a ratio landing within a rounding step of an integer, where `ceil` goes either way. That is not argued, it is ENUMERATED: `the_integer_derivation_agrees_with_the_f64_reference` walks all 4,259,840 points of the realistic grid — blowup 2^1..2^4, rounds 1..64, security 0..255, grind 0..64 — and fails on any disagreement. It passes in 3s, and a sibling test asserts the grid is not one answer everywhere, because a grid that agreed trivially would prove nothing. Q62 rather than Q64 for one concrete reason: the log2 loop squares its running mantissa, and a Q64 value in [1,2) squares to 130 bits, which a `u128` does not hold. The primitives are checked against independent algorithms, not against themselves: `isqrt` against `r^2 <= n < (r+1)^2`, `log2_fixed` against `f64::log2` and exactly against the powers of two, where any drift in the squaring loop would show as a fraction. The shipped posture's outputs are pinned where they already were and again here: 110 at one round, 112 at 4..7 rounds, 113 at 8..15. SCOPE, as ruled. Only the multilinear derivation moves. The univariate one at `crypto/stark/src/proof/options.rs:121-125` stays `f64` and stays where it is; `the_query_count_matches_the_univariate_provers` remains green by construction, because it compares OUTPUTS rather than formulas. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880 bytes. Tests: multilinear 295 (+9), stark 256, prover multilinear 30.
The control the A/B runs on. `LAMBDA_VM_WHIR_HASH=keccak|rpx`, read once per process and cached, so a run cannot change hash halfway through and produce a proof no single configuration describes. Unset is keccak, which is the same monomorphisation PR #988 compiles today. Three decisions worth stating, because each has a quieter alternative: * AN UNKNOWN VALUE ABORTS. `LAMBDA_VM_WHIR_HASH=rpx-256` — a plausible typo, since `rpx256` is what the configuration calls itself — would otherwise fall through to keccak and produce a perfectly valid proof under the hash the operator was trying to move away from. A measurement taken that way is worse than no measurement: it looks like the RPX arm and is not. `a_near_miss_is_not_silently_accepted` pins the list. * THE BANNER PRINTS ON EVERY SETTING, including the default. A banner that only appeared for RPX could not be told apart from a banner that did not appear because this code was never reached — exactly what a byte gate comparing two arms has to rule out. Its absence from a log is now a fact about the run, not an ambiguity. * BOTH ARMS ARE ALWAYS COMPILED. A feature gate would make the RPX arm unreachable in a default build, and the knob would then be a control that does nothing on the binary most people run. The price is doubled monomorphisations below each of the seven dispatch sites. The dispatch is a macro because the seam is a TYPE parameter and a function cannot return a type: one `match` per site, each arm monomorphising its body at its own configuration. Seven sites — the monolithic prove and verify, the L2G commitment, the two grouped commits, and the two epoch verifies — all reading one process-wide `OnceLock`, so a proof cannot be half one hash and half the other. Verified end to end on a real program (`multilinear_prove_tests:: a_program_proves_and_verifies`): banner `★ WHIR HASH: keccak256` unset and `★ WHIR HASH: rpx256` when set, and the proof verifies on both. ⚠ One host-only number from that run, recorded because it will be quoted at me otherwise and it is NOT the pre-registered band: 10.3s keccak against 31.5s RPX, on a small ELF, CPU only, no card, no grinding of consequence. The band is device prove time on block 25368371 and nothing here measures it. Byte gate unmoved with the knob unset: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880. Tests: prover whir 18 (+4), and the 30 multilinear tests unchanged.
…ke `phases` refuse Adding `LAMBDA_VM_WHIR_HASH` gave the two shape benches a way to lie: both pin `KeccakWhir` at their commit sites, so under `LAMBDA_VM_WHIR_HASH=rpx` they would print `★ WHIR HASH: rpx256` from the knob's banner and then report keccak's seconds underneath it. A measurement labelled with the arm it is not is worse than no measurement, and this one was created by the commit that added the knob. `commit_phases` NOW FOLLOWS THE KNOB, and it is the right bench to do it in: its four passes clock `stack`, `lift`, `encode` and `merkle` apart, and `merkle` is the leaf-and-tree hashing ALONE. That is the hash term itself — precisely the number a hash comparison wants, and the one the `continuations` bench cannot separate because it times a whole `prove_continuation`. The commitment is dropped inside the dispatch arm, which is also why this bench can take the knob at all: nothing whose type names the hash escapes the block. `phases` CANNOT, and now says so rather than mislabelling. Its committed tables escape into the rest of the function, so the two arms would have to return the same type and they do not. It asserts the knob is keccak and refuses otherwise, naming `commit_phases` as the bench for the hash arms. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880. fmt 0; clippy default, disk-spill and cuda passes exit 0.
`rpx_grind_search` has been in the cubin, pinned by the host KAT and loaded as a handle, since the device commit landed — and dispatched by nothing. `generate_nonce_maybe_gpu`'s guard read "is `D` the platform keccak digest", so every RPX grind fell to the host rayon search: ~2^20 RPX permutations each, thousands of grinds per block proof. A measured WHIR block arm came in at 571.04 s against keccak's 39.27 s with the card at 7.4% utilisation and 31 host threads at ~90%; ~510 s of that was this one line. Nothing failed. The proofs were valid. Only the clock said so. THE GUARD is now keyed on WHICH KERNEL `D` HAS, not on `D` being keccak — the host twin of the `DeviceHash` key the commit path already carries. `has_device_kernel` is the one place the supported set is written down, so a hash added to `math_cuda::grinding` without a line there keeps grinding on the host, which is the failure this commit exists to remove. THE MAPPING, and why the two entry points are named rather than flagged. The arms read the SAME 32 bytes in OPPOSITE orders: keccak takes four LITTLE-endian lanes, RPX four BIG-endian felts, because `felts_from_bytes` reads consecutive eight-byte groups big-endian and those four `u64`s ARE the felts the host sponge absorbs. Crossing them compiles, runs, and searches under a message the host never hashes — every nonce rejected, the fallback taken forever, one warning line. So there is `inner_hash_lanes` and `inner_hash_felts`, each with its own doc, and the preimage is stated where the kernel is called: `inner ‖ nonce` is 40 bytes, five felts, padding flag `5 mod 8 = 5` with the LEAF domain — ONE rate-8 block, hence the kernel's `init(5)`. TWO COUNTERS, NOT ONE. A single "device grinds" counter is satisfied by the keccak kernel firing under an RPX configuration, which is exactly the failure the dispatch prevents; it must not also be the failure the test cannot see. So the RPX arm must show `rpx > 0 && keccak == 0`, and keccak the reverse. TESTS. Card-free, in `crypto`: `inner_hash_felts` reproduces the three rows of `RPX_GRIND_VECTORS` from the CUDA KAT header — the per-table branch's host implementation, which this repository did not produce — their nonces pass the host predicate and are exhaustively the smallest, the two readings are byte-reversals that disagree (the endianness control, without which `inner_hash_felts` could be `inner_hash_lanes` renamed and every other assertion would still pass), and the preimage is one block by two independent routes. On a card, `prover/tests/rpx_grind_device.rs`: the counter assertions above, plus the device returning the ORACLE's nonce for all three rows — which is what makes the counters more than launch counts. ⚠ Mutation-checked, and the result is the point: deleting the RPX arm COMPILES and passes every card-free gate, because a grind still succeeds — on the host. Only the counter test discriminates, and only on the box. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880. Lint 5/5, fmt 0, host KAT all pass, crypto 93 (+6), prover whir 18.
…ntinuation arm The `continuations` bench printed prove, verify, proof size and epochs — every one of which is consistent with "the hash is just expensive" when what actually happened is that a dispatch never reached the device. That is not hypothetical. A measured WHIR arm came in at 571 s against keccak's 39 s with a correct, KAT-pinned `rpx_grind_search` sitting unused in the cubin, and nothing in this output named the cause. It took a 100 ms GPU-utilisation histogram from outside the process to see it. One line now says it from inside: commits, keccak grinds, rpx grinds, each counter zeroed per arm so the numbers belong to this prove. A grind count of ZERO beside a commit count in the thousands names an unwired dispatch immediately, and it distinguishes that from the other candidate — a commit that fell back to the host, which reads as commits 0 instead. ★ Read 0 for every future WHIR arm. The `★ WHIR HASH:` banner says which hash was SELECTED; these say which kernels RAN, and the two are not the same claim — a whole diagnosis rested on that distinction.
⛔ The instrument meant to catch "a measurement wearing the wrong arm's
label" was wearing one. Run on the box under `LAMBDA_VM_WHIR_HASH=rpx` with
the deterministic grind, `the_whir_identity_line_over_a_canonically_sorted_eq_trace`
printed **keccak's line and no banner at all** — because it pinned
`KeccakWhir` at its prove site and so never reached a dispatch. It was the
third instance of that class on this branch and the first inside the gate
itself; the two shape benches were fixed at `43a1cb76` and this one was
missed.
The prove now goes through `with_whir_hash!`. It can, for the reason the
whole seam rests on: `MultiProof` does not mention the hash in its type —
32-byte digests either way — so the proof leaves the dispatch arm and both
arms unify. Reaching a dispatch is also what makes the `★ WHIR HASH:`
banner print.
AND IT NOW ASSERTS, because printing is not a gate:
* the serialized length is 6880 under BOTH arms — the strict one, since a
hash swap is not a proof-format change;
* the keccak arm equals `7b8afea2…6dd3`, so a commit that changes the
proof PR #988 produces fails here and owes an explanation;
* the rpx arm must DIFFER from it. An arm that cannot produce a different
answer is not an arm.
Measured locally, both settings, banner on each:
keccak 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880
rpx 5226e4cfffac7eb2ba629470a0c5ebf879421078b389e3a8065ae63768031adb 6880
⚠ Mutation-checked by restoring the pin: the test then reproduces the box's
failure exactly — keccak's line under the rpx label — and fails with
"the rpx arm produced KECCAK's line". Note the banner DOES print in that
mutated build, because the new assertion calls `selected()` itself. So the
banner is no longer the signal here; the assertion is. On the box at
`f2d93e1a` there was no banner because nothing in this test called the knob
at all, which is what made the absence diagnostic that once.
Lint 5/5, fmt 0, host KAT all pass, prover whir 18, crypto 93,
multilinear 295.
Draft
…hash once `commit()` built the Merkle tree, took the root and dropped the buffer; `paths()` then rebuilt the whole thing — leaves included — to read a kilobyte per query out of it. Every commitment on this path is opened, so every commitment paid for TWO leaf-hash passes over its codeword. Measured on block 25368371 at 2^21: RPX device hashing is ~25 s of the 38.3 s the hash swap costs, and by construction about half of that is the second pass. The keccak arm pays the same structure at ~3.8 s, so this is a keccak-side win too. WHAT IT KEEPS, AND WHERE. `commit` now caches the node buffer on the `DeviceCodeword` and `paths` reads it. Behind an `Arc<Mutex<..>>` because `DeviceCodeword` is `Clone` and the clones are the same codeword — a cache that cloned would be rebuilt per clone, which is the cost being removed. A fold gets its own slot: it is committed and opened in its own right, and sharing the parent's would make each evict the other every round. THE SHAPES. `commit_calls = 1050` over 15 epochs is 70 device commits per epoch, and a chain commits once per round, so 70/7 = 10 chains per epoch — which independently confirms the ~11 inferred from proof bytes. rounds = 7 with MAX_STACK_VARS = 25 pins n_stack = 25, so round 0's codeword is 2^27 elements and its tree is 2^23 leaves: 2*L-1 nodes of 32 bytes = 536,870,880 B. ★ That is exactly the "half a gigabyte per commitment" the old comment cited, now derived rather than quoted. Two commitments are live at once (a round opens `current` and `next`), worst pair round 0 + round 1, so the peak held is 512 + 32 = 544 MiB against a measured VRAM p99 of ~24.1 GiB on a 32 GiB card. ⚠ THE RESERVATION, which is the condition this turns on. Device memory held outside the accounting is an under-count nothing reports until a second prover shares the card — the two-accountings shape this codebase has paid for before. So `DeviceReservation` becomes atomic and GROWABLE: the cached tree grows the chain's existing reservation by exactly its bytes, through the `Arc` the folds already share, and eviction shrinks it back. ONE number still answers "what does this chain hold". If the budget will not take the bytes, the tree is served for that call and NOT cached — the old behaviour, never a silent over-commit. THE CACHE KEY is `(log_folding, hash)`, and a miss REBUILDS rather than refusing: both are legitimate parameters of the call and a rebuild is always correct, whereas refusing would turn an unusual-but-valid call into an error. What the key rules out is the dangerous outcome — serving a tree that answers a different question, whose paths would be internally consistent and wrong. ★ HOST UNAFFECTED, and it was already right: `from_codeword_on_host` keeps its tree and host `paths` is a walk with no hashing (`whir_commit.rs:372-379`). The double hash was purely the device's. TESTS (`crypto/math-cuda/tests/whir_tree_cache.rs`, GPU): the leaf-hash pass is COUNTED and must read 1 after commit-then-open and still 1 on a second open; the cached paths must equal a freshly built tree's and the openings must verify against the commitment through the production types; the reservation must cover the tree as a NUMBER and give every byte back on drop; a `paths` at a different blocking must rebuild, checked by the count AND by the resulting paths being two levels deeper. Both hashes throughout. `LAMBDA_VM_NO_WHIR_TREE_CACHE=1` restores the rebuild, so the mutation is an env var rather than an edit and anyone can re-run it. Byte gate unmoved: 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880. Lint 5/5, fmt 0. multilinear 295, crypto 93, prover whir 18.
…odeword
The H4 gate found two things and both were real. Neither was caught here,
because every assertion in that file needs a card.
⛔ **`paths` never used the cache.** `commit` built the tree and kept it, and
`paths` still called `build_tree` directly — the doc comment said it read
the cached tree and the code did not. So H4 as committed at `3e38c9d9`
delivered NOTHING: every commitment still hashed its leaves twice, and the
one test written to catch exactly that could not see it, because the count
it read was process-wide and its neighbours were committing too.
⚠ **The counter was global and the tests run in parallel.** Six tests share
one binary, cargo runs them concurrently, and `leaf_hash_calls()` counts the
whole process — so a test expecting 1 read 5. An assertion on a global
counter is an assertion about every test in the binary, and it flakes with
the scheduler.
Both fixed at the source rather than by serialising around the problem:
* `paths` goes through `with_tree`, like `commit` and `nodes_to_host`.
* `DeviceCodeword` counts ITS OWN leaf-hash passes (`tree_builds()`), and
every counting assertion uses that. It is immune to the scheduler, and
it localises a failure to the codeword that caused it rather than to
whoever happened to run alongside. A fold gets its own count, as it
already gets its own cache slot.
The process-wide counter stays — it is what the `continuations` bench
prints — and now has one test of its own, which takes a lock across its
window precisely because it cannot tell whose work it is counting.
⚠ Note for whoever reads the first gate log: the two reported failures were
at `:78` and `:224` of the previous file, and the line numbers moved under
`cargo fmt` between the commit and the run. The failures are explained by
the two defects above; the per-codeword counter makes the next run
unambiguous either way, since a count of 2 after a commit can then only
mean the commit built twice.
Lint 5/5, fmt 0. Byte gate unmoved:
7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3, 6880.
multilinear 295, crypto 93. The H4 tests still need a card and are still
unrun here.
Test-only; no production code moves.
`the_cached_tree_is_inside_the_reservation` asserted that
`Backend::reserved_bytes()` returns to its baseline after a codeword is
dropped — a statement about a PROCESS-WIDE total, made while sibling tests
held live reservations on the same card. On the gate it read 786,400 B of
someone else's tree and failed. Same class as the leaf-counter flake fixed
in `e14f63c3`: an assertion about shared state is an assertion about every
test in the binary.
The counting half of that lesson was fixed by removing the shared state —
per-codeword `tree_builds()`. This one cannot be: "dropping a codeword
gives its promised bytes BACK" is irreducibly global, and there is no
per-codeword handle left to ask once the codeword is gone. So the file
takes turns instead.
* One `DEVICE_GLOBALS` lock, taken by all seven tests, because all seven
commit and a commit moves both process-wide quantities. They share one
card and serialise on it anyway, so the cost is nil; what the lock buys
over `--test-threads=1` is that the property holds however the suite is
invoked rather than only when someone remembers the flag.
* The three propositions are now separated and each says what it is
about: (a) this codeword's OWN promise covers its tree — no global, so
it would hold without the lock at all; (b) the global grew by a DELTA
equal to that promise, read against a baseline rather than an assumed
zero; (c) dropping it returns the accounting to that baseline, which is
the half the lock exists for.
The baseline in (b) is the part that matters for the next reader: the first
version assumed the global started where this test left it, and a sibling's
live reservation is exactly what that assumption forbids.
Lint 5/5, fmt 0. Still unrunnable here — every assertion needs a card.
…is O(chains) by construction H4 kept the tree a commit built so the openings that follow would not hash its leaves a second time. Measured on the card it returned exactly the hashing it promised and cost more than it returned: prove +15.6 s keccak and +2.4 s RPX against bands of -1.5/-2.5 and -10/-13, VRAM max at 96% of the card, host peak +19.7 GiB. The retention is not one tree. `StackedCommitment::commit` builds EVERY chain's commitment before it returns, because all the roots enter the transcript before any query index is drawn, and the openings follow one chain at a time. So the last chain's tree lives from its commit to the end of `multi_prove` — the commitments are held by `StackedCommitment`, which is held by `CommittedTables`, which `multi_prove` borrows for the whole prove. Ten chains at half a gigabyte is 5,120 MiB; the measured VRAM delta was 5,664 MiB, eleven trees exactly, ten round-0 and one fold pair. No placement of an eviction call bounds that peak, because all N trees exist before the first opening. Past the ceiling the cost stops being memory. A device allocation that fails becomes `None` at `gpu.rs`'s `commit_codeword_resident(..).ok()?`, `commit_stacked` then takes its host arm, and `from_codeword` retains both a 1 GiB host codeword and a 512 MiB host node array for the rest of the proof — which is the host growth, the utilisation fall from 46% to 33%, and the seconds. Two comments already said so. `multilinear::whir_commit`'s `paths` priced it before any of this was built — "keeping it would cost half a gigabyte of device memory per commitment for the whole proof" — and the reservation in `StackedCommitment::commit` promises "nine codewords of room instead of sixteen", a retained codeword per commitment and no tree. The design note said "one chain at a time" because it reasoned about `prove_with_factors`'s locals and never asked who owned them. So the cache goes: `CachedTree`, the slot, the reservation growth and the `LAMBDA_VM_NO_WHIR_TREE_CACHE` escape hatch. `with_tree` stays as the one place that builds and frees, and carries the finding so the next reader does not re-derive it. What the measurement earned is kept: - `LEAF_HASH_CALLS` and per-codeword `tree_builds()`, retargeted to the two passes they now count — a commit's, and one per round that opens it. - `Backend::free_vram_bytes()`, the driver's own accounting. This is the instrument the shipped unit test lacked: `reserved_bytes()` counts what callers promised, so it reads baseline while the card fills. - `device::drain_and_trim` made public, so a memory test can empty the pool before it samples and measure the caller rather than the allocator. - `a_group_holds_only_its_codewords_before_any_open` — four live, unopened commitments at log_domain 22 / log_folding 4 take under 160 MiB. Four codewords are 128 MiB; four codewords and their kept trees are 192 MiB. The unit test that shipped dropped ONE bare codeword and passed on the leaking prover, because an O(chains) peak is not a state one codeword can be in. This one fails wherever the holding is written.
A commit that asks the device and gets nothing encodes on the host instead, and nothing said so. `commit_calls()` simply does not rise, and a count merely lower than expected says nothing when the expected count is itself derived from the table census. That silence hid H4's regression for a whole six-arm run. Keeping a Merkle tree per commitment put VRAM at 96% of the card; every commit after the ceiling took the fallback arm; and the visible symptoms were host memory and a utilisation figure that read like a scheduling problem. The arm was taken and no line of output named it. It is not a slower route to the same place. `from_codeword` retains the host codeword and its node array for the rest of the proof, so a card that fills partway through an epoch converts into gigabytes of host memory that never comes back — which is the +19.7 GiB the arm reported. So `commit_stacked`'s `None` arm counts, and `host fallbacks` prints on the per-arm WHIR line and in both shape tables, beside `gpu commits`. The test is card-free and pins the invariant rather than the machine: three commits, three accounted for, on the device or on the host. A test asserting `host_fallbacks() == 3` would be true on a GPU-less host and false on the box, which pins nothing; the sum holds on both and reads short exactly when an arm forgets to count. Mutation run — the increment removed reads `left: 0, right: 3` and fails.
The guard as written put 32 MiB between passing and failing: at `log_folding = 4` a tree is half a codeword, so four codewords read 128 MiB and four codewords with their kept trees read 192 MiB, against a bound of 160 MiB. That margin is arithmetic, not measurement. `free_vram_bytes` reports what the PROCESS has taken from the driver, so it also carries whatever one-time workspace and twiddle caches the first commit of a given size sets up — counted identically in both cases, and easily a codeword on its own. A single such allocation inside a 32 MiB margin is a false failure, and no bound at that blocking has room for one. So the blocking is `log_folding = 2`, where a tree is TWO codewords: four codewords are 128 MiB, four with their trees are 384 MiB, and the bound at 256 MiB has 128 MiB of slack on each side. A warm-up commit of the same shape pays the one-time costs before the sample, and the margin absorbs what the warm-up misses. Caught by asking what would make the assertion fire when nothing was being kept, before the test had run anywhere — it has still never run on a card, and the gate that decides it is the box's.
…changed
`DefaultTranscript::sample` reversed all 32 bytes of every squeeze before
handing them out and chaining them back in. Under an algebraic sponge that
is pure loss: the squeeze is already four canonical big-endian felts
(`digest_to_commitment(sponge_leaf_bytes(..))`), and reversing them gives
the sampler the LAST felt's bytes backwards — a number with no canonicality
property, which a field-native verifier then pays to undo. V1 sizes it at
+9.7 M instructions and +456 M cells per epoch verify on the LFM side.
`TranscriptHash::REVERSES_SQUEEZE` decides it per configuration: `true` for
keccak, `false` for RPX. It is an associated constant, so each
configuration monomorphises to straight-line code and the keccak arm keeps
the instruction sequence it had before this was a choice. The returned
bytes and the chained bytes stay the same value under either setting — a
replaying verifier reproducing the chain should have one byte convention to
carry, not two.
`CANDIDATES_PER_COORDINATE` comes with it, and the two are one change
rather than two: `None` for keccak, `Some(1)` for RPX. An earlier revision
of `transcript_hash.rs` argued at length that `Some(1)` could not be
claimed here, naming the reversal as the reason and calling it "a constant
whose stated justification is false". That argument was correct and its
conclusion is now inverted; both paragraphs are rewritten rather than
deleted, because the reasoning is why the constant is safe.
⚠ THE REVERSAL WAS BIASING THE RPX SAMPLER. This is the strongest reason to
remove it and it is not a cost argument.
A candidate under the old code was `byteswap(canonical(felt))`, which is
>= p exactly when the felt's low four bytes are all 0xFF — reversing puts
them in the top four, and p's top four bytes are 0xFFFFFFFF. Witness:
v = 0x00000001ffffffff is canonical, byteswap(v) = 0xffffffff01000000 >= p,
rejected. The rejection sampler therefore drew uniformly from a SUBSET of
[0, p) missing about 2^32 elements: statistical distance ~2^-32 per
coordinate, and over an epoch verify's ~3e4 coordinate draws a loose hybrid
bound of ~2^-17 of added soundness error.
Not a demonstrated attack — the excluded set is fixed and public and no
prover steers into it — and never exercised in production, because the RPX
transcript was not wired to any prover (below). It was inherited, not
chosen: harmless under keccak, whose 8-byte groups are uniform on 64 bits
and whose sampler is therefore exactly uniform. It exists only in the
RPX-under-`DefaultTranscript` combination. But it is the kind of unquoted
term an audit names, so it is stated here and exhibited in
`the_reversal_would_have_biased_the_rpx_sampler`, which carries the witness,
generates the whole excluded set rather than sampling it, and checks over a
million felts of the complement to show the bias is exactly that one and no
larger. Found by V1.
SOUNDNESS. Challenges become the canonical coordinates of an RPX digest —
the standard algebraic-sponge transcript, and how miden's RPO transcript
samples. The reversal had no security role to lose: reversing 32 bytes is a
bijection, so the distribution a sampler draws from is the digest's before
and after, and every squeeze remains a function of everything absorbed. What
changes is which bijection sits between the digest and the sampler.
Removing it makes the coordinates canonical felts rather than felts read
backwards, which is what lets one candidate per coordinate be exact rather
than typical. Keccak's configuration is untouched in value and in code
path; its proofs are byte-identical, asserted by the gate.
The derivation is sound without it. With the RPX permutation ideal the four
output lanes are uniform and independent on F; each 8-byte big-endian group
IS `canonical(felt)` and `FieldElement::from` maps it back, so the round
trip is the identity on F — a bijection onto [0, p) — and each coordinate is
exactly uniform, the cubic element exactly uniform on E, with no rejection
step left to bias anything. `canonical` picks the reduced representative and
discards no entropy. The reversal was a fixed public bijection: composing a
random oracle with one leaves a random oracle, and the chaining re-absorb
likewise, so nothing is lost by dropping it. The absorb order, the domain
separation, the padding rule, the grind preimage, the Merkle construction
and every keccak byte are unchanged. `CANDIDATES_PER_COORDINATE = Some(1)`
for RPX is then a theorem rather than a measurement — every candidate is
canonical, so the loop cannot iterate — and K5 pins it.
TWO FACTS, TWO REASONS, kept apart because a verifier that needs both must
not take one as evidence of the other:
- A field coordinate is one candidate under RPX BECAUSE the squeeze is
canonical felts. That is this commit.
- A query index is one draw BECAUSE every WHIR query bound is
`num_leaves = 1 << (log_domain_size - log_folding)`, a power of two, so
`sample_u64`'s rejection region `2^64 mod bound` is empty. That is true
today and hash-independent, and it has its own test with a constructed
non-power-of-two counter-example — without which the test would assert
that zero equals zero for 64 values and pass on anything.
Ten tests in `crypto/crypto/src/tests/rpx_transcript_tests.rs`. Three
mutations, each firing on exactly one:
REVERSES_SQUEEZE = true -> an_rpx_squeeze_is_the_unreversed_digest… FAILED
sample() always reverses -> an_rpx_squeeze_is_the_unreversed_digest… FAILED
threshold hard-coded to 0 -> …_and_a_ragged_one_does FAILED
"bound 3 is not a power of two yet
shows no rejection region"
⚠ Two of the ten still PASS with the reversal restored — the canonicality
sweep and the three-draw count — and the file says so. A canonical felt's
bytes read backwards are almost always still below p, so 2048 reversed
groups look exactly like 2048 canonical ones. Those two guard
`digest_to_commitment`'s canonicalisation, not the byte order. Exactly one
test guards the byte order.
The same 2^-32 rules out the obvious control: "keccak needing more than one
candidate" takes on the order of a billion squeezes to observe, and a test
that appeared to show it would be measuring noise. The difference between
the configurations is structural, not statistical, so the controls are
constructed — a candidate built to be >= p drives the rejection branch and
reads 4 draws where 3 would otherwise pass.
⚠ THIS COMMIT MOVES NO PROOF BYTES, on either arm, and that is not a
disappointment but this A/B's control. No WHIR call site constructs a
transcript over `RpxTranscriptHash`: all eight write `DefaultTranscript::<E>`
and take its keccak default, because the transcript is built and absorbed
into before the `with_whir_hash!` block opens and `H` does not exist yet
where the type would be named. So today's RPX configuration is RPX Merkle
backend, RPX grind, keccak Fiat-Shamir. Wiring it is W1-A2, and this commit
is what makes the wiring worth doing.
Measured locally on the byte gate, both arms, at this head:
keccak 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880
rpx 5226e4cfffac7eb2ba629470a0c5ebf879421078b389e3a8065ae63768031adb 6880
Both unchanged. The gate not moving under a change that had to move it is
how the missing wiring was found.
MauroToscano
force-pushed
the
whir/rpx
branch
from
September 16, 2026 17:08
faadcc8 to
3e8c6fa
Compare
`hash_metrics`'s own header fixed this trap for Merkle and named it
exactly: a counter that compares `TypeId` against keccak and does nothing
otherwise "became a check that cannot fail the moment a second hash
arrived — under RPX every Merkle counter would have read ZERO, reporting
*no hashing* for precisely the arm whose purpose is to change the hashing".
The transcript and the absorb counters never got that treatment:
- `count_absorb` had ONE call site, the keccak wrapper's `update`, so
`absorb_calls` and `absorb_bytes` read zero for every RPX proof measured.
- `Rpx256Digest::update` was a bare `Vec::extend_from_slice` with no
metrics call at all, and its finalizes never reached `total` — whose own
documentation says it counts "every finalize … transcript squeeze".
- Nothing anywhere counted transcript work as transcript work.
So an RPX arm read zero, and zero is also what a correctly instrumented
keccak-free run reads. The measurement could not distinguish "the other
hash ran" from "nobody instrumented it" — which is not hypothetical here:
for four measured A/Bs the RPX arm ran a KECCAK transcript and no
instrument disagreed.
WHAT IS COUNTED, AND WHERE
`transcript_absorbs{,_keccak,_rpx}` and `transcript_squeezes{,_keccak,_rpx}`,
bumped from `DefaultTranscript`'s own append and sample methods — the
transcript, not a hash. Two reasons, the second being the one that matters:
1. Hash-agnostic by construction. A counter inside keccak cannot see an
algebraic sponge, which is the whole defect.
2. TRANSCRIPT absorbs only. `count_absorb` is bumped from a digest's
`update`, so it mixes Merkle leaf bytes with Fiat-Shamir bytes and
cannot answer "how much did the transcript absorb" for either hash.
Both arms are instrumented and both are asserted, because one side is not
evidence: "rpx > 0, keccak 0" is equally true when the keccak transcript
ran and nobody counted it. `Counts::transcript_unattributed()` reports what
neither bucket claimed, so a third configuration arriving without a counter
shows up rather than looking like silence.
`Rpx256Digest` now bumps `count_absorb` and `count_total` too, so the
pre-existing generic counters stop being keccak-only.
THE PER-ARM LINE
`transcript absorbs K/R · squeezes K/R (keccak/rpx) · unattributed K/R`,
printed next to `gpu commits` under `--features hash-metrics`, with the
counters reset per arm. The line above it says which KERNELS ran; this one
says which sponge the transcript used, and they are not the same claim.
TESTS — `crypto/crypto/tests/transcript_counters.rs`, six of them.
Its own integration binary AND a lock, because neither alone is enough.
The binary because `crypto`'s lib-test binary runs neighbours that hash: an
early version of this read 215 squeezes of which 200 were keccak, purely
from parallel siblings. The lock because an integration binary also runs
its own tests in parallel — moving them out left four of five failing, one
reading `left: 2, right: 0` where a sibling's `reset` landed inside this
test's measurement window.
Non-vacuity is tied to a counter that predates these:
absorb_calls == transcript_absorbs + transcript_squeezes
on a keccak-only run — they differ by exactly the chaining re-absorb, one
per squeeze, which is part of squeezing rather than an absorb anyone asked
for. It fails if either counter is moved, double-counted or misattached.
Mutations run, both firing on the right test:
drop `count_absorb` from Rpx256Digest::update
-> the_rpx_digest_bumps_the_generic_counters FAILED
"absorbing into an RPX digest moved `absorb_calls` to 0 — it read 0
before this was instrumented, for every RPX proof ever measured"
tag RPX as keccak in `sponge<D>()`
-> an_rpx_transcript_counts_as_rpx_and_nothing_else FAILED (left 0, right 4)
a_field_element_absorb_costs_the_same_on_both_arms FAILED
⚠ A test of mine failed correctly and took a wrong comment with it. It
asserted that a cubic element absorbs in "several chunks"; it does not.
`stream_bytes` for the degree-3 extension writes one 24-byte buffer and
calls the sink ONCE (`extensions_goldilocks.rs:567-571`). The claim, and a
comment in `default_transcript.rs` repeating it, are corrected — the
counter follows the sponge's `update` calls because that is the unit
`absorb_calls` has always used, not because an element streams in pieces.
`make test` gains the integration binary and `make lint` gains
`-p lambda-vm-prover --features hash-metrics`, without which the per-arm
line compiles in no pass — which is how an instrument rots.
The closed-form assertion on the squeeze count (V1's part-(4) order) lands
when V1 hands the number; the identity above holds meanwhile.
…ed by the compiler
The RPX configuration ran an RPX Merkle backend, an RPX grind and a
KECCAK Fiat-Shamir sponge. Through four measured A/Bs, with no instrument
disagreeing: the proofs were valid, the two arms genuinely differed from
each other, the banner printed the right name and the counters showed RPX
kernels running. The arm was one third narrower than its label.
The cause is structural rather than a line anyone could spot.
`DefaultTranscript`'s hash parameter has a default, so `DefaultTranscript::<E>`
IS a keccak transcript while looking like it names no hash — and the
transcript is built and absorbed into BEFORE the `with_whir_hash!` block
opens (constructed at `multilinear_prove.rs:226`, dispatch at `:265`), so
`H` does not exist where the type would have to be named. All eight WHIR
call sites wrote the default.
HOW IT WAS FOUND. W1-A alters how every RPX squeeze is handed out, so the
byte gate's RPX line was required to move. It printed `5226e4cf…031adb`,
exactly as before. A pinned constant's REFUSAL to move carried the
information; the `assert_ne!` against keccak's line that this arm had
instead would have passed and said nothing.
THE FIX IS A BOUND, NOT A CONVENTION. `HasTranscriptHash` names the hash a
concrete transcript runs on, and `multi_prove`/`multi_verify` now require
T: HasTranscriptHash<Hash = <H as WhirHash>::Transcript>
so a mismatched transcript does not compile. Requiring each site to NAME a
hash would not have caught this — a site can name the wrong one as easily
as it can take a default. An equality the compiler checks makes the
half-configured arm unspellable, and it costs the several hundred STARK
call sites nothing, because they are not generic over `H`.
The compiler then found the defect itself: six type-mismatch errors, one
per production site, before any test ran.
The seven transcript constructions move inside their dispatch blocks, and
with them two `owed` computations that FORK the transcript to draw `z` and
`alpha` — those challenges are a function of the configuration's sponge, so
computing them against another hash is the same defect one level down and
just as quiet. `absorb`, `absorb_epoch`, `absorb_global` and `owed` become
generic over the transcript's hash; they had `&mut DefaultTranscript<E>` in
their signatures, the same default baked in one level further out.
THE BYTE GATE. The RPX line moves, which is the proof the wiring reached
the prove path — nothing else in this commit changes proof bytes:
keccak 7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3 6880
rpx dcc0e8d52a80a6c9ee4ed9911d54b41e7df132d209fbf91e43018b0ac01c4985 6880
Both measured locally at this head. Keccak's is unchanged, as it must be.
The RPX arm is now PINNED to a constant rather than merely required to
differ from keccak's, with the old value kept in the header and the reason:
an arm that can only report a category cannot report a surprise.
TESTS
`prover/tests/whir_transcript_configuration.rs`, three of them: a real
prove through the production entry point, counters read afterwards. Each
arm asserts both that its own counters moved AND that the other's are zero,
because a single number cannot tell "the other hash ran" from "nothing
ran" — and under this defect the RPX arm squeezed thousands of times, all
keccak. Its own binary plus a lock: the counters are process-global and the
prover's lib-test binary runs 600+ parallel tests, which is how an early
version read 215 squeezes of which 200 were a neighbour's.
The mutation cannot be expressed. Putting `DefaultTranscript::<Ext>` back
in the fixture gives:
error[E0271]: type mismatch resolving
`<DefaultTranscript<...> as HasTranscriptHash>::Hash == <... as WhirHash>::Transcript`
expected associated type, found `KeccakTranscriptHash`
A test that cannot be broken by the defect it guards is usually a bad sign;
here it is because the defect stopped being writable.
⚠ `the_transcript_follows_the_configuration` is renamed to
`the_two_transcript_types_draw_different_challenges`, which is what its body
asserts. It constructs both transcript types itself and never mentions the
prover, so it was true throughout the period in which no call site built an
RPX transcript at all, and would have stayed true if none ever did. The
claim its old name made is now checked twice: by the bound above, and by
the system test.
…ides of the proof Two defects in A2a's instrument, both found by lane V1's closed form rather than by a test of mine. STATE READS WERE INVISIBLE. `count_transcript_squeeze` is called from `sample`, which is `finalize_reset`. `state()` finalizes a CLONE — no reset, no re-absorb, the chain does not advance — so it was counted nowhere. On a block proof that is 2,996 finalizes missed, one per grind check, against 182,734 squeezes (V1's closed form, pinned to a measured verify with difference 0 on two programs). They are now separate counters, not a sum. A sum of 185,730 could be checked against neither number, and the split makes the state column a free control: there is exactly one state read per grind check, so it must equal the grind count the same run already prints. Two independent instruments on one quantity, and a disagreement names which is wrong. THE LINE MEASURED THE WRONG SIDE. The per-arm print sat before `verify_continuation`, so it reported the PROVER's transcript — and the number that matters for recursion is the VERIFIER's, because that is what an LFM replays. The two are different work: on the block the prove side reads 583,924 absorbs / 183,226 squeezes while V1's verify-side closed form is 765,437 / 182,734. Those are not a discrepancy of 492 to be explained; they are two quantities, and differencing them is the same category error as comparing a prove stopwatch to a verify one. So the line prints twice, each with its own reset and labelled by window: `WHIR prove` and `WHIR verify`. `print_transcript_counts` carries the warning that the window is part of the number. WHAT THIS DOES NOT CHANGE, and it is worth stating because V1's note reads as if it might. The keccak floor V1 identifies — 11,490 eager REGISTER absorbs plus 16 `elf_digest` — cannot reach the transcript counters, so the RPX arm's `transcript_absorbs_keccak == 0` assertion stands. `elf_digest` is a bare `Keccak256` over the ELF (`statement.rs:25-29`) and `compute_precomputed_commitment_with_fini` builds a Merkle commitment (`register.rs:334`); neither goes through a `DefaultTranscript`. The floor is in the GENERIC `absorb_calls`, which mixes Merkle bytes with Fiat-Shamir bytes — the reason these counters were put in the transcript rather than in a digest in the first place. Two tests, both directions each, because either conflation is live: a state must not appear as a squeeze AND a squeeze must not appear as a state. The first also asserts that `state()` really did not advance the chain, which is why it is a different number rather than another name for the same one.
… the ELF
The rows came out of `instructions.iter()`, so their order was hashbrown's:
a function of the hasher, the capacity the map happened to grow to, and the
insertion sequence. Nothing has ever failed on it and nothing could — the
prover and the verifier both reach `generate_decode_trace` through
`instructions_from_elf` (`trace_builder.rs:2762`, `decode.rs:337`), so they
construct the map identically and agree. What they agree on is a
CONSTRUCTION PROCEDURE, not the ELF.
That distinction is about to start mattering. DECODE's five preprocessed
columns are ELF-derived and their Merkle root is on its way to being a
program constant pinned in a recursion guest (W1-B). A pinned root has to
be a function of the ELF alone. Sorted by pc it is, and a hashbrown version
bump, a capacity change or a `reserve` added upstream cannot move it.
Unsorted it is not, and the failure mode is the bad kind: a toolchain
update silently invalidates the pin with no ELF change, no code change and
no failing test, until a verifier rejects a valid proof.
pc is the map's key, so it is unique and the order is not merely
deterministic but canonical.
THE TEST IS THE PROPERTY, NOT THE MECHANISM.
`the_decode_trace_does_not_depend_on_the_map_that_carried_it` builds the
same instruction set through two independently-constructed maps — ascending
with no reserve, descending with `reserve(1024)` — and asserts the traces
agree row for row and the `pc_to_row` indices agree. That is what a pinned
root needs: two parties holding the same ELF and nothing else in common
produce the same rows. A test asserting "the rows are sorted" would pass on
any total order and would never say why the order matters.
⚠ It asserts its own premise first. If hashbrown ever made iteration order
insertion- and capacity-independent, the body would still pass while
testing nothing, so the two maps are required to iterate differently before
anything else is checked.
`decode_rows_are_in_ascending_pc_order` pins the mechanism separately, so a
future change that keeps determinism but moves the rows has to come here
and re-baseline rather than slide past.
Mutation — the sort removed, both fail, and on the right assertion:
the_decode_trace_does_not_depend_on_the_map_that_carried_it FAILED
"row 1 differs between two maps holding the same instructions"
decode_rows_are_in_ascending_pc_order FAILED
"the instruction rows are not in ascending pc order"
THE PIN THAT MOVES. `SUB_DECODE_COMMITMENT_BLOWUP_2` is re-baselined from
`e97168d6…5f` to `0a710a9c…1b`, regenerated with the
`print_decode_commitment_for_sub` helper the constant's own doc names for
this. The cause is in the comment beside it, because "a constant changed"
is not a reason: the old value was the root of a trace whose row order
hashbrown chose. This is the last time it can move for a reason nobody
picked — a future drift means the AIR or the FFT pipeline changed, which is
what the constant was always for.
Nothing else moves. The WHIR byte-gate lines are computed over an EQ air
with no DECODE table and were re-measured unchanged at
`7b8afea2…6dd3` / 6880 bytes.
This commit is independent of the WHIR seam and cherry-picks to main on its
own, where it also closes one of the six trace generators whose row order
comes from `HashMap` iteration.
The verify-side transcript counts are what a recursive verifier replays, so
they are the number the WHIR recursion is sized against. They are now a
constant, measured on FAST under `cuda,hash-metrics` and independently
predicted by lane V1's shape-derived closed form — two derivations, one
number, on all three columns.
prove 583,924 absorbs / 183,226 squeezes / 2,996 states
verify 584,061 / 183,256 / 2,996
owed 137 / 30 / 0
BOTH SIDES, because the pair makes their difference checkable and that
difference is derived rather than measured: the verifier runs `owed` and
the prover does not, so it is `Sum roots.len()` absorbs and `2 x epochs`
squeezes. The 2 squeezes per call are not "two samples, two squeezes" — a
cubic element is three 8-byte draws from a 32-byte buffer, so the first
sample squeezes and leaves a group over and the second spends it and
squeezes again. Three not dividing four is the reason it is two.
THE GUARD IS THE ELF'S SHA256, NOT ITS NAME. Two builds of the same guest,
same sources, two worktrees, share a name and differ in bytes. Not
hypothetical: a 0.23% difference in these very counts was read as a model
error before it was traced to a different build of "the same" guest, whose
ELF touches genesis pages (0x280000, 0x680000) another build does not,
which moves the GLOBAL_MEMORY set and with it the chain shapes the counts
are made of.
A rebuild therefore SKIPS the assert rather than failing it, and says so,
printing BOTH shas — the one found and the one pinned — so a skipped run
names which rebuild happened rather than only that one did. A silent pass
and an absent assert are the same thing. The counts are a function of the
ELF, the input and the epoch size, so all three are in the guard.
An exact pin beat the tolerance first proposed (+/- 0.3%): that band was
wide enough to swallow a 0.23% event, and that event was a different guest.
A tolerance tuned to survive a rebuild cannot report one. The sha guard
gives the same protection against spurious failure while keeping failure at
any magnitude, and leaves the closed form the better job — predicting the
number rather than bounding it.
THE ASSERTIONS ARE SPLIT FROM THE GUARD so they can be reached without the
pinned guest. That split is the point, not tidiness: together, they ran on
the box and NOWHERE ELSE, so a mistyped constant or a swapped pair would
have been found by a GPU run rather than by `cargo test`.
WHAT WRITING THE TESTS FOUND. The runtime `owed` assertion could never
fire. With both lines asserted against their pins, their difference is
forced — `OWED` is `VERIFY - PROVE` by construction. The constructed
counter-example never reached it; the VERIFY assertion rejected it two
lines earlier. So the delta moved to where it can fail: a test on the
CONSTANTS, which is the claim that survives a re-baseline. If someone
measures a new run and updates both lines together, it fires unless `owed`
is still `owed`, forcing them to look at why the difference moved instead
of carrying a changed protocol into two numbers that agree with each other.
An earlier draft of that test also asserted `oa % 1 == 0`, which is true of
every integer. Removed, with a note saying why the absorb count gets no
predicate of its own: it is data from the table shapes, so anything this
test could write about it is circular or vacuous.
Five tests, none `#[ignore]`d, because the skip path runs on every other
invocation of this bench and is the half that would fail silently. The skip
test passes deliberately absurd counts (1, 2, 3): reaching the assertions
with them would panic, so returning at all proves the guard returned first.
It checks wrong-bytes-wrong-length, and then RIGHT length with wrong bytes,
which is what says the guard is the sha rather than the size.
Mutations, each isolating:
PROVE +1 unit -> 4 fail, incl. the delta and both off-by-one guards
VERIFY +1 unit -> the measurement and the delta fail; the guards pass
OWED +1 alone -> ONLY the delta test fails
guard on length -> ONLY the skip test fails
"the PROVE-side transcript counts moved"
`sha2` joins the prover's dev-dependencies for this, test-only.
…e shows both in full The transcript pin skipped on the guest it was pinned to. The box ran it against the recognised fixture, both arms, and both printed a SKIPPED line while the counters read the constants exactly. fixture 8f826601776d4085cbb6fbf0302fe8d8d5d1be7940ac1aaca24899c6244ec80a pinned 8f826601776d4085a9c1f1b4f30ab4e1de2f8e9e1e2c9bb0bb0e1d39e64e94f7 The first 16 hex agree. The remaining 48 were never a measurement: every message that carried this sha carried a 16-character prefix, and the tail was written to look measured. The constant was a guess in the costume of a value. AND THE DIAGNOSTIC MADE IT UNFALSIFIABLE BY READING. The skip line printed `[..16]` of both sides — precisely the width at which the real sha and the invented one agree. So the line that existed to report a mismatch showed two identical-looking values and called them different. That is the structural half of the defect, and the worse one: a diagnostic truncated to a window where the compared values can agree reports the comparison it is not making. Two fixes, because either alone leaves the other's failure live: 1. `ELF_SHA256` is the full `sha256sum` of the box fixture, and its doc says where it came from rather than only what it is. 2. `pin_skip_line` prints the FULL 64 hex of both sides. The decision (`pin_applies`) and the diagnostic (`pin_skip_line`) are now separate pure functions, so a near-miss sha can be tested without forging an ELF. Two tests: - `a_sha_agreeing_only_on_the_prefix_is_refused_and_says_so` — a sha sharing the first 16 hex is refused, AND the printed line carries both values in full and shows them differing. A refusal that works beside a truncated diagnostic would still hide the next wrong constant; a full-width diagnostic beside a prefix comparison would still accept the wrong guest. - `the_pinned_sha_is_full_width` — 64 lowercase hex, so a constant that is a display cannot be pinned. Mutations, each reproducing one half of what actually happened: diagnostic truncated to [..16] -> the prefix test FAILED comparison looks at a prefix -> the prefix test FAILED constant cut to the measured 16 -> both tests FAILED The rule, for the note: anything shortened for a message is a display; the constant is the measurement. A value that arrives truncated must be measured at its source before it is pinned, and a diagnostic must show enough of both sides that any difference is visible in its own output.
The transcript hashes bytes, and the algebraic configuration's sponge re-slices everything absorbed since its last squeeze into field elements every eight (`rpx::sponge_leaf_bytes`). A value absorbed at an offset that is not a multiple of eight straddles two of them, which the field machine replaying this transcript can only reproduce by decomposing bits. Every window after the first is aligned already: a squeeze leaves the sponge holding its own 32-byte output, and roots, extension elements, grind nonces and final values are all multiples of eight. The first window is the exception, as it opens with the statement and the roots land wherever the statement ended. The pad is COMPUTED, not a constant, because the roots do not follow the fixed prefix: two variable-length fields sit in between. The epoch statement's fixed prefix is 237 bytes, and rounding that to 240 leaves the roots at 2 mod 8 at the shape this system runs, so it would move every pinned constant and align nothing. Each statement function now accumulates its own length beside its `append_bytes` calls, with `absorb_table_counts` reporting its own width, and pads from that length. The padding absorb is made even when the pad is empty, so "one padding absorb per statement" is shape-independent and the pinned pair moves by exactly one per statement rather than by a number that needs the shapes to predict. Padded: the continuation epoch, the cross-epoch and the monolithic multilinear statements. Not padded: the univariate statement, whose sponge is keccak (it never re-slices a byte stream into field elements) and whose bytes the block identity lines pin. The WHIR byte gate cannot see this and must not be cited as if it could: its fixture builds its own transcript and calls `multi_prove`, which begins at the roots, so it absorbs no statement at all. Both arms were run and both print their pinned lines unchanged; that fact is now recorded beside the constants. What sees it: the transcript pair pin's absorb counts (+1 per statement) and `tests::statement_alignment_tests`, which records the window offset of every absorb. Three tests sweep the statements against a recording transcript, asserting the alignment first and then two corroborating derivations — a closed form written from the field list, and an absorb-call count. The fourth writes out the arithmetic that killed the constant-pad design. The fifth drives a real `multi_prove` through the recorder under both hashes and requires the whole proof to be aligned; the recorder is validated rather than trusted, by requiring its prove to serialise to the same bytes as the production transcript's.
… term Every epoch statement binds one u64 per per-table count, so a continuation proof's absorb total carries `epochs * kinds`. That kind count is not a constant of the protocol: the per-table campaign adds `TableCounts::blake3`, so this lineage absorbs fourteen per epoch statement and the merged one fifteen. The box found that as a pin FAILURE at the merged base, +15 on both sides, and the term was legitimate — the BLAKE3 table is conditional and its count is the one entry a verifier cannot derive, which is why per-table bumped both domain tags for it. A pin carrying the total was therefore a constant describing one branch while claiming to describe the protocol. It now stores branch-independent bases and derives the totals, with the kind count read from `statement::NUM_TABLE_KINDS` rather than written down. That constant is guarded by two compile errors that need each other: the exhaustive destructure of `TableCounts` fails when a field is added, and the array's return type fails when the field is pushed in without bumping the constant. The epoch count joins the pinned shape beside the ELF and the epoch size, and `owed`'s squeeze assertion reads it instead of repeating 15. The provenance says which half is a measurement and which a prediction: the bases come from the box's measured 583,924 / 584,061 at c73568f plus this branch's computed statement padding, and that +16 has not been measured yet. These constants are what will say so if it is wrong.
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
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
PR #988's WHIR path hard-codes keccak-256 in three places — the Merkle backend, the Fiat-Shamir sponge and
the proof-of-work grind. This makes the hash a parameter with keccak as the default and byte-identical,
and adds RPX256 (XHash12) as the second instantiation, host and device.
⚠ All three are reached as of
a783f2de. They were not for most of this branch's life: the Fiat-Shamirsponge stayed keccak-256 under both arms through four measured A/Bs — see Four things a reviewer should know
went wrong below. Every timing number on this page predates the wiring, so each is a number for
RPX-Merkle + RPX-grind + keccak-transcript. They stand as measurements; this is their description.
It is not a performance change and does not claim to be. RPX is slower than keccak everywhere a host or
a GPU is doing the hashing, and the numbers below say by how much. The reason to carry it is a proof that
will be verified inside another proof: a keccak-f[1600] costs ≈73,700 trace cells in a field-native
verifier against RPX's 325, so a WHIR epoch proof verified recursively pays ≈227× less for its hashing. On
the recursion side that is the difference between ≈1.59 G cells per chain and ≈10.6 M — between a wrap about
twice today's cost and one about a third of it.
Nothing here is a soundness analysis, and one assumption is explicitly unproven: that swapping the hash
leaves the protocol sound. The security accounting is unchanged and remains what
with_security's own doccalls it — a conservative mirror of the univariate parameters, not an analysis of this protocol.
The measurement
Block 25368371, epoch 2^21,
--features cuda, one backend per process, ABBA (keccak, rpx, rpx, keccak), allfour arms at
0cbc9623, same ELF and fixture, 10 Hz VRAM histograms.Paired Δ = +38.3 / +39.4 s, mean +38.8 s (+98%). Controls reproduce to 0.38 s, RPX arms to 0.70 s.
The one VRAM figure that looks like an outlier is not one: rr3's 26,062 MiB is a single 100 ms sample,
and the four arms' distributions agree through p90 (13,038–13,262 MiB median, 17,326–18,286 MiB p90, in the
sampler's own units as in the VRAM row above, with the keccak arms marginally higher). Every arm spends
the same 8–9 samples above 24,000 MiB, at the same 19–23% point of its run. See
handoffs/W1.mdfor thefull reading; the short version is that a sampled maximum is not a level, and the RPX arms take twice as
many samples, so they catch the top of the same transient more often.
All of the cost is on the device, and it decomposes exactly:
The host term is negative: the RPX arm no longer grinds on the CPU while the keccak arm still does. Split
of the device term — every term measured, none derived, each from a subtraction of two integrals:
A fifth arm — keccak with
LAMBDA_VM_NO_GPU_GRIND=1, which moves that grind to the host — pins the lastunknown:
K_g = 1.5 – 2.7 sof device keccak grinding, the spread being the two keccak arms' own 1.2 s.R_g = 17.4 sfrom both pairs independently. So ≈25 s hashing and ≈15 s grinding.The device grind's per-permutation ratio is ≈6–12× (RPX : keccak) — quoted as a range on purpose:
K_gis 1.5–2.7 s and its own noise floor dominates the quotient, so a point estimate here would beprecision the measurement does not have.
★ A finding for the keccak path, not the RPX one. That fifth arm also prices the existing device grind:
keccak WHIR prove is 82.32 s with the grind on the host against 39.5–39.9 s with it on the device, so
the device grind is worth 52% of the keccak WHIR prove on this block. Against it, run 1's host RPX grind
(≈510 s) puts the host grind ratio near 12× — a different code path from the
merklepass's 5.4× perpermutation (platform keccak with its assembly backend, against scalar RPX), so the two numbers are not in
tension and neither supersedes the other.
Why hashing costs what it does, measured independently (
commit_phases,ethrex_10_transfers, tworounds per arm): the
merklepass — leaf and tree hashing, isolated from stack, lift and encode, which areidentical between arms to two decimals — is 3.61 s keccak against 29.43 s RPX, a ratio of 8.15×. A tree
of
Lleaves doesLleaf hashes andL−1parents, so the permutation-count ratio is 1.5×; theper-permutation cost is therefore ≈5.4×.
Proof size and host memory do not move. A 32-byte digest either way and no proof struct gains a field,
so the serialized length is equal to the byte across all four arms — a hash swap here is not a
proof-format change.
What is in it
The seam. One trait,
multilinear::whir_hash::WhirHash, naming the Merkle backend, the Fiat-Shamirconfiguration, the device kernel family and a name. One trait rather than four parameters, because separate
ones make the half-flip spellable — one hash's trees under another hash's sponge. That configuration is
self-consistent between prover and verifier, so it verifies, so nothing fails; it is silent by construction,
and the only thing wrong with it is that no single name describes the proof. With one name to write there is
nothing to assert against.
Commitmentstays[u8; 32], soMultiProof,TableProof,StackedProof,ChainProof,CosetOpeningand
Proof<Commitment>keep their layout, their rkyv derives and their serialized length. The parameterflows through six modules and three types, each defaulting to
KeccakWhirso existing call sites readunchanged. Grinding became generic over its digest with no default — a defaulted proof-of-work hash
would silently keep grinding on keccak for a configuration that had moved everything else.
RPX256, ported not invented. The permutation, the leaf construction, the parent and all 168 round
constants come from
prover::lfm::{rpo, rpx, algebraic_commit}on the per-table branch, byte for byte,because the CUDA kernel and its known-answer tables are pinned to exactly those. A cherry-pick was not
available — none of the source commits is an ancestor of this base, and they are written against APIs it
does not have — so it is a port whose commit body names every source. The LFM machine is not carried
over: no chip, no AIR, no eDSL.
Two anchors of different strength, and the module says which is which:
fb_rounds composed are RPO256, and the tests replay miden-crypto's nineteen publishedhash_elementsvectors through them — seventy-six numbers this repository did not produce, pinning ARK1, ARK2, the MDS row
and its orientation, both S-box chains and the lane convention at once.
rpx/tests.rshasonly structural tests). The RPX vectors here are the per-table branch's host implementation, transcribed
from the CUDA KAT header — worth having because the kernel is pinned to those same tables, so a port
reproducing them is byte-compatible with that branch's host and its device. It reproduced all of them on
the first run: 11 permutation states including the canonicalisation witness, 7 leaf lengths, 2 parents.
The device. On the host a Merkle backend both names a hash and computes it; on the device it only names
it, so a key must travel with the request or a tree labelled RPX can be built by keccak's kernels with
nothing to notice.
math_cuda::DeviceHashis that key, matched exhaustively at every launch site.rpx_leaves_base_cosetandrpx_leaves_ext3_cosetare new — the per-table branch's seven RPX leafkernels all hash a row group, and WHIR's leaf is a fold coset.
Gated without a card.
make test-rpx-host-katcompilesrpx.cuas host C++ through a shim and pins itsarithmetic, its schedule, its sponge, its parent and every leaf kernel's read pattern in seconds. The two
new kernels have their own case, built from the definition rather than from a second kernel call, with a
control asserting the strided read differs from the contiguous one. ⚠ Necessary, never sufficient: it cannot
say whether nvcc accepts the file or anything about execution rather than arithmetic. Both were then
confirmed on a real 5090 under nvcc 13.1.
LAMBDA_VM_WHIR_HASH={keccak|rpx}, read once per process. An unknown value aborts rather thandefaulting —
rpx-256silently proving keccak is a measurement worse than none. The banner prints on everysetting including the default, because a banner only for RPX cannot be told from a banner absent because the
code never ran.
The
f64leaves the multilinear query-count derivation (query_count.rs), replaced by Q62 fixed pointand enumerated against the
f64reference over all 4,259,840 points of the realistic parameter grid.The shipped posture's 110 / 112 / 113 are unchanged, and the univariate derivation is untouched.
Also in the diff, and why
Three repairs the branch needed to be gateable at all, each its own commit so they can be taken or dropped
separately:
f57a71a5— fourdisk-spillcall sites passed the wrong arity, somake lint's third pass couldnot build. Verified red at this PR's own head before this branch touched anything.
140e2694— four clippy findings incrypto/multilinear/src/gpu.rs, likewise red at that head, in afile this branch's feature commits do not touch.
make lintis now five passes and all five are green,the
cudapass for the first time on this stack.c9c452c6—hash-metricswas in no lint pass and no test target, which is how its Merkle countersstayed keccak-only after a second hash arrived and would have reported ZERO for the RPX arm.
Four things a reviewer should know went wrong
The first measured RPX arm was 571 s, not 78. A guard added in this branch's own first commit dispatched
the grind to the device only for keccak, so every RPX grind fell to the host — ~2^20 RPX permutations each,
2,996 per block proof — while a correct, KAT-pinned grind kernel sat in the cubin, loaded and called by
nothing. Nothing failed and every proof was valid; only the clock said so. It was diagnosed from a GPU
utilisation histogram plus the host-only verify ratio, and the bench now prints device commit and grind
counts after every arm so the next one is named from inside the run rather than from outside the process.
The RPX arm was never running an RPX transcript, and four measured A/Bs did not notice. The transcript
is built and absorbed into before the
with_whir_hash!block opens, soHdoes not exist yet where itstype would be named — and
DefaultTranscript's second parameter defaults to keccak. All eight WHIR callsites take that default. Nothing failed: every proof was valid, both arms differed from each other (the
Merkle backend and the grind are genuinely RPX), the banner printed the right name, and the counters showed
RPX kernels running. The arm was simply one third narrower than its label.
It was found by a change that had to move the bytes and did not.
faadcc8falters how every RPX squeeze ishanded out; the byte gate's RPX line was therefore required to move, and it printed
5226e4cf…031adb— the same value as before. A passing test would have said nothing here; it was thepinned line's refusal to move that carried the information, which is the argument for pinning it rather
than asserting
!=against the other arm.Also recorded because it is the same lesson twice: a test named
the_transcript_follows_the_configurationhas existed on this branch since the seam landed. It constructs both transcript types itself and shows they
draw different challenges — true, and it never mentions the prover. It is renamed to what its body asserts,
and the system test it claimed to be arrives with the wiring.
A performance change was designed against a doc comment nobody read. H4 kept each commitment's Merkle
tree to remove a second leaf-hash pass; the retention is O(chains) rather than O(1), it filled the card, and
the function being changed already said so. Measured, reverted, and written up under What this does not do
below — including the counter that makes the failure mode self-reporting next time.
Two instruments printed the wrong arm's label. Both shape benches and then the byte gate itself pinned
keccak at their prove sites, so under
LAMBDA_VM_WHIR_HASH=rpxthey reported keccak's numbers. All threenow go through the dispatch,
phasesrefuses to run under a hash it cannot honour, and the byte gateasserts rather than prints: same length under both arms, the keccak line equal to its constant, the RPX line
required to differ.
The squeeze reversal, and a soundness term it was carrying (
3e8c6fac)DefaultTranscript::samplereversed all 32 bytes of every squeeze before handing them out. Under keccak thatis a harmless byte convention. Under RPX the squeeze is already four canonical big-endian felts, so reversing
them hands the sampler the last felt's bytes backwards — and a field-native verifier then spends rows undoing
it: V1 sizes the replay cost at +9.7 M instructions and +456 M cells per epoch verify.
TranscriptHash::REVERSES_SQUEEZEmakes it a per-configuration constant —truekeccak,falseRPX — andCANDIDATES_PER_COORDINATEarrives with it (None,Some(1)). The two are one change: the schedule is aconsequence of the byte order, which is why an earlier revision of that file argued at length that
Some(1)could not be claimed here. The argument was right; its conclusion is now inverted, and both paragraphs are
rewritten rather than deleted.
⚠ The reversal was also biasing the RPX sampler, which is a better reason to remove it than the cost. A
candidate was
byteswap(canonical(felt)), which is>= pexactly when the felt's low four bytes are all0xFF— witness0x00000001ffffffff, canonical, whose byteswap is0xffffffff01000000and is rejected. Therejection sampler therefore drew uniformly from a subset of
[0, p)missing ~2^32elements: ~2^-32statistical distance per coordinate, ~
2^-17of added soundness error over an epoch verify's ~3e4 draws on aloose hybrid bound. Not a demonstrated attack — the excluded set is fixed and public — and never exercised
in production, because the RPX transcript was never wired to a prover. It was inherited from the keccak
transcript, where it is harmless because keccak's 8-byte groups are uniform on 64 bits. Found by V1;
exhibited in
the_reversal_would_have_biased_the_rpx_sampler, which carries the witness, generates the wholeexcluded set rather than sampling it, and checks a million felts of the complement to show the bias is
exactly that one and no larger.
Soundness of the result: with the permutation ideal, each 8-byte group IS
canonical(felt)andFieldElement::frommaps it back, so the round trip is the identity onFand each coordinate is exactlyuniform, with no rejection step left to bias anything. The reversal was a fixed public bijection, and
composing a random oracle with one leaves a random oracle. Absorb order, domain separation, padding, the
grind preimage, the Merkle construction and every keccak byte are unchanged.
This commit moves no proof bytes on either arm — both gate lines read exactly as before, which is this
change's control and, as above, how the missing wiring was found.
The transcript reaches the configuration (
3f75574b,a783f2de)DefaultTranscript's hash parameter has a default, soDefaultTranscript::<E>is a keccak transcriptwhile looking like it names no hash — and the transcript is built and absorbed into before the
with_whir_hash!block opens, soHdoes not exist where the type would have to be named. All eight WHIRcall sites wrote the default. The RPX configuration therefore ran an RPX Merkle backend, an RPX grind and a
keccak sponge, and no instrument disagreed: valid proofs, genuinely different arms, the right banner, RPX
kernels in the counters.
The fix is an equality the compiler checks, not a convention.
HasTranscriptHashnames the hash atranscript runs on, and
multi_prove/multi_verifyrequireT: HasTranscriptHash<Hash = <H as WhirHash>::Transcript>. Requiring each site to name a hash would not havecaught this — a site can name the wrong one as easily as take a default. The compiler then found the defect
itself: six type-mismatch errors, one per production site, before any test ran. And the guard test's mutation
can no longer be written — restoring the old spelling gives
error[E0271] … expected associated type, found KeccakTranscriptHash.⚠ The default hash parameter is NOT removed, deliberately. Doing so would touch 344 turbofish sites
across ~60 files, all STARK code, for which keccak is not an unchosen default but the answer. The bound
already makes the WHIR bad state unspellable, which is the part that matters; the rest is verbosity. Parked
as a possible mechanical follow-up, not scheduled.
Moved inside the dispatch with the transcript: two
owedcomputations that fork it to drawzandalpha. Those challenges are a function of the configuration's sponge, so computing them against anotherhash is the same defect one level down, and just as quiet.
The counters that would have named it (
3f75574b):transcript_absorbs{,_keccak,_rpx}andtranscript_squeezes{,_keccak,_rpx}, bumped fromDefaultTranscript's own append and sample methods ratherthan from a hash — a counter living inside keccak cannot see an algebraic sponge, and a counter in a digest's
updatemixes Merkle leaf bytes with Fiat-Shamir bytes and answers neither question.Rpx256Digestalsobumps the pre-existing
count_absorb/count_total, which had exactly one call site (the keccak wrapper) andso read zero for every RPX proof ever measured, while
total's own documentation claimed to counttranscript squeezes.
Both arms are instrumented and both are asserted, because one side is not evidence: "rpx > 0, keccak 0" is
equally true when the keccak transcript ran and nobody counted it.
transcript_unattributed()reports whatneither bucket claimed, so a third configuration arriving without a counter shows up instead of looking like
silence. The per-arm bench line prints
absorbs K/R · squeezes K/R · unattributed K/Rbesidegpu commits.The RPX gate line moved, which is the proof the wiring reached the prove path — nothing else in these
commits changes proof bytes:
7b8afea2618350600e99bb67200bb4447d962f753b6e858ee0982336436e6dd3dcc0e8d52a80a6c9ee4ed9911d54b41e7df132d209fbf91e43018b0ac01c49855226e4cf…031adb)Both arms are now pinned to constants. The RPX arm previously only had to differ from keccak's, and that is
precisely why the defect survived: an arm that can only report a category cannot report a surprise.
The statement is padded to a field element boundary (
8c933bd6)⚠ THE THIRD PROTOCOL-TOUCHING CHANGE ON THIS BRANCH, after the squeeze reversal drop and the DECODE
preprocessed commitment, and like them it is on the list Mauro holds the veto over. It moves the bytes of
every WHIR statement, so every continuation proof this branch produces differs from one produced before it.
The transcript hashes BYTES. The algebraic configuration's sponge re-slices everything absorbed since its
last squeeze into field elements every eight bytes (
rpx::sponge_leaf_bytes), so a value absorbed at anoffset that is not a multiple of eight straddles two of them — and the field machine that replays this
transcript can only reproduce such an absorb by decomposing bits.
Every window after the first is aligned already: a squeeze leaves the sponge holding its own 32-byte output,
and roots (32), extension elements (24), grind nonces (8) and final values (24) are all multiples of eight.
The first window is the exception, because it opens with the statement and the roots land wherever the
statement ended.
The pad is COMPUTED, and that is the whole point. The roots do not follow the statement's fixed prefix;
two variable-length fields sit in between. The epoch statement's fixed prefix is 237 bytes, and padding that
to 240 leaves the roots at
(|public_output| + |table_num_vars|) mod 8= 2 mod 8 at the shape this systemruns — it would move every pinned constant and align nothing. So each statement function accumulates its own
length beside its
append_bytescalls, withabsorb_table_countsreporting its own width, andpad = (8 - len % 8) % 8. No literal, and no constant a caller has to keep in step.The padding absorb is made even when the pad is empty, so "one padding absorb per statement" holds for
every shape and an absorb count stays a function of the statement's fields rather than of its lengths.
Padded: the continuation epoch, the cross-epoch and the monolithic multilinear statements. Not padded: the
univariate statement, whose sponge is keccak (it never re-slices a byte stream into field elements) and whose
bytes the block identity lines pin.
What moves, and what does not
owedabsorb_bytes0..=7each7b8afea2…6dd3·dcc0e8d5…4985· 6880⛔ The byte gate is not a witness here. Its fixture builds its own transcript from
b"whir-identity"andcalls
multi_provedirectly, so it absorbs no statement at all —multi_provebegins at the roots. "The gateis unmoved" is the assertion this change owes, not evidence that it did nothing; both arms were run and both
printed their pinned lines. The same fact means the gate's own first window (13 seed bytes, then roots) is not
aligned, and it must never be quoted as a witness that a real proof's is. That is now written beside the
constants.
The tests, and what each of them can fail on
tests::statement_alignment_tests, five tests, card-free:Each asserts the property first (the statement ends on a multiple of eight), then two corroborating
derivations: the total equals a closed form written from the field list — a second derivation from the
production accumulator, and the only place the two can disagree — and the absorb-call count equals its own
closed form, which is what a padding absorb skipped at
pad == 0fails. The epoch sweep also asserts itsshapes do not all share one residue, so it cannot be satisfied by a constant pad.
padding_only_the_fixed_prefix_would_not_align_the_rootswrites the arithmetic that killed the constant-paddesign as an assertion, so it cannot be forgotten: fixed prefix 237, rounded 240, roots at 2 mod 8.
every_absorb_of_a_real_prove_is_field_element_aligneddrives a realmulti_provethrough therecorder, under both
KeccakWhirandRpxWhir, and requires every absorb after the statement to bealigned — 119 absorbs, 0 misaligned, at a pad of 2 and a pad of 0. The recorder is not trusted: it
mirrors
DefaultTranscript's duplex output buffer (the only part that says where a window ends) and thetest first requires the recorded prove to serialise to the same bytes as the same fixture proved through the
production transcript. A mirror that drifted would draw different challenges and fail there.
Mutations, each run and each failing on the assertion named:
The pair pin is now a base plus a per-branch term (
d4f983f8)The absorb columns carry
EPOCHS * NUM_TABLE_KINDS— oneu64per per-table count, per epoch statement —and that kind count is not a constant of the protocol: this lineage binds fourteen and the merged one
fifteen, because per-table adds
TableCounts::blake3(legitimately: the BLAKE3 table is conditional and itscount is the one entry a verifier cannot derive, which is why per-table bumped both domain tags for it). The
box found that as a pin FAILURE at the merged base, +15 on both sides.
So the pin now stores branch-independent bases and derives the totals, with the kind count read from the
struct rather than written down.
NUM_TABLE_KINDSis guarded by two compile errors that need each other: theexhaustive destructure fails when a field is added to
TableCounts, and the array's return type fails whenthe field is pushed in without bumping the constant. A new test checks the split is the protocol's, and a
mutation confirms both halves (a bumped constant without the field does not compile; a base off by one fails
the_pinned_pair_is_the_measurementandthe_pinned_constants_differ_by_owed).⚠ Half the provenance is a PREDICTION and the comment says so: the bases come from the box's measured
583,924 / 584,061atc73568f4plus this branch's+16, which has not been measured yet. These constantsare what will say so if it is wrong.
What this does not do, and what is next
crypto/multilinear/srcstill do not run in CI (-p multilinearis absent frompr_main.yaml), which is orthogonal to this PR but worth knowing while reviewing it.The largest remaining term is not the hash — and the attempt to remove it was measured and reverted.
The WHIR device path hashes each commitment's leaf layer twice:
commitbuilds the tree, takes the rootand drops it, and
pathsrebuilds the whole thing per opening. Every commitment here is opened, so every onepays twice — by construction about half of the ≈25 s of RPX device hashing above, and the keccak arm pays the
same structure at its own ≈3.8 s.
3e38c9d9kept the tree so the second pass would go away. It was measured on the card and it lost:Not a cache miss: it returned the hashing it promised, and the ~+15 s penalty is the same in both arms.
The retention is one tree per commitment in the group, not one tree.
StackedCommitment::commitbuildsevery chain's commitment before it returns — all the roots enter the transcript before any query index is
drawn — and the openings follow one chain at a time, so the last chain's tree lives from its commit to the
end of
multi_prove. Ten chains at 512 MiB is 5,120 MiB; the measured VRAM delta is 5,664 MiB, eleven treesexactly (ten round-0, one fold pair). No placement of an eviction call bounds that peak, because all N trees
exist before the first opening.
Past the ceiling the cost stops being memory: a failed device allocation becomes
None,commit_stackedtakes its host arm, and
from_codewordthen retains a 1 GiB host codeword and a 512 MiB host node arrayfor the rest of the proof — the +19.7 GiB, the utilisation fall, and the seconds.
⚠ This PR's own code said so before any of it was built.
whir_commit.rs'spathscarries, unchangedfrom
aa38739d: "keeping it would cost half a gigabyte of device memory per commitment for the wholeproof". An earlier draft of this paragraph quoted that sentence, called the figure "derived rather than
quoted", re-derived the 512 MiB correctly — and read the window as two live commitments, 544 MiB, because it
reasoned about the local variables in
prove_with_factorsand never asked who owned them. The reservation inStackedCommitment::commitsays it a second way: "nine codewords of room instead of sixteen" budgets aretained codeword per commitment and no tree.
So
2997b97aremoves the cache andwith_treeis the one place that builds and frees, carrying the finding.What the run earned is kept: the per-codeword and process-wide leaf-pass counters,
Backend::free_vram_bytes(the driver's own accounting —
reserved_bytes()counts what callers promised, which is how the retentionstayed invisible to a unit test that passed), and a group-scale guard,
a_group_holds_only_its_codewords_before_any_open: four live, unopened commitments must take under256 MiB from the driver, where four codewords are 128 MiB and four codewords with their trees are
384 MiB — the blocking is chosen so a tree is two codewords, which is what makes the margin survive the
allocator rather than only the arithmetic. The shipped unit test dropped one bare codeword and
passed on the leaking prover, because an O(chains) peak is not a state one codeword can be in.
107bde98adds the counter that would have named it from inside the run:host fallbacksprints besidegpu commits, so a device commit that silently degrades to the host is never invisible again.Removing the second pass still looks worth having, and one shape remains: bring the tree home over pinned
memory instead of keeping it on the card — host RAM has the room the card does not. The same comment prices
that too ("a pageable copy of half a gigabyte is the slowest thing in the commit"), and the pinned bandwidth
that would decide it has not been measured. Flagged, not built.