Per-table GPU recursion, end to end: one root for block 25368371 - #985
Draft
MauroToscano wants to merge 569 commits into
Draft
Per-table GPU recursion, end to end: one root for block 25368371#985MauroToscano wants to merge 569 commits into
MauroToscano wants to merge 569 commits into
Conversation
…lt gadget is gone felt_be_halves rendered every opened field element for the hash as one BitDec row plus 64 base-ALU recomposition rows. At the real epoch that gadget was 99.9% of all BALU rows, 99.99% of BITDEC reads, and 77% of the whole wrap program's main cells (1.18B of 1.53B, measured 2026-08-21) — the wrap was a byte-marshalling program with a verifier attached. The two big-endian u32 halves are fixed LINEAR FORMS over the 64 bit columns the BitDec row already carries and constrains, so the chip now SENDS them on the memory bus — the keccak REV_ADDR pattern: two interactions, four preprocessed columns (HALF*_ADDR/MULT, prep width 130 → 134), no value columns, no new constraint. Booleanity and the canonicity witnesses already pin the bits; the receiver already forces them to recompose the input; the sends are functions of constrained columns. Identical bytes reach the hash: same digests, same transcript, same wire format. bit_dec_be_halves emits one BitDec with two half outputs and NO bit cells (the bits stay as witness columns); felt_be_halves delegates, so every consumer — both wrap formats, keccak and blake3 leaves, the statement absorb — collapses at once. Executor computes byteswapped halves; compiler assigns their mults and fills the new preprocessed columns; validator checks the outputs like any other. Expected at the real epoch: LFM_BALU 2^27 → ~2^17 rows (−536M main cells, −35% of the wrap), instructions 113M → ~6M. To be measured on the box, one change at a time, per the ladder. The LFM machine AIR changed, so the registry is deliberately re-blessed (compute_lfm_registry): exactly one group root per entry moved — slot 4, BITDEC's preprocessed group — everything else byte-identical, which is the drift tests' own proof the change is surgical. The three pinned-cost tests are re-pinned to the new contract, with the zero direction asserted so a reintroduced per-felt ALU cost fails loudly.
…e whole LDE Round 3 reads the trace LDE only at stride blowup — the size-n coset evaluation. Under RecomputeLde the batched phase 4 was paying a full 4n expansion (iFFT n → scale → FFT 4n) per table to then subsample a quarter of it. The recompute arm now materializes the n-sized evaluation directly (iFFT n → scale → FFT n, via a lazily-built size-n forward twiddle set): bit-identical values — both compute the same DFT in exact arithmetic, and the residency-equality tests are the proof — at ~37% of the work and a quarter of the transient bytes. Retention still serves phase 4 from the full LDE it already holds. get_trace_evaluations_from_lde takes its read stride from the TABLE's own blowup instead of the domain's — coincident for every existing caller, and what lets a blowup-1 table mean 'the subsample, already taken'. The parts stride stays the domain's (retained parts are full-LDE-sized). The recompute budget moves from 5+5 to 4+4 full expansions per table plus one cheap coset evaluation per side, counted in new stats fields so the full-expansion number stays honest; the budget pin asserts both.
# Conflicts: # crypto/math-cuda/build.rs # crypto/stark/src/prover.rs # crypto/stark/src/trace.rs
…e proofs alone (P1) verify_epoch's AIR reconstruction moves into reconstruct_epoch_airs and the wrap flow's new RealEpoch-from-proof constructor calls the same function, so the verifier and the wrap emitter cannot diverge on what an epoch IS. The replay harvest is extracted from real_epoch_from and shared; a wrap can now be emitted for ANY epoch of a continuation bundle — the final epoch (HALT on board) included — with no live proving session and no prove_continuation changes. Gates: session-vs-from-proof wrap programs byte-identical through the registry artifacts; the final epoch wraps end to end from proofs alone; bundle tamper rejected at its two layers (reg_fini by the constructor's production-verify, l2g_root by verify_continuation). The block driver the_real_block_proves_and_wraps_end_to_end runs prove_continuation, full bundle verification, and all per-epoch wraps in one process and reports block-level numbers. The gates prove their fixtures at blowup-4 diagnostic options: the per-table replay indexes each table's own LDE pairs (index_bits = log2(h*blowup) - 1), which a height-1 fixture table makes impossible at MIN's blowup 2.
…cuda Under cuda builds with a live device, build_auxiliary_trace's resident-aux arm builds the LogUp columns on device and skips the host writes; the batched prover expands the aux LDE from the host trace, so every table above the GPU-logup eligibility height committed an aux round built from unwritten columns — aux and composition-parts roots diverged from the non-cuda build and the verifier's OOD composition check rejected the proof (main root identical; a_batched_vm_epoch_host_verifies_end_to_end red under cuda, green with LAMBDA_VM_NO_GPU_LOGUP=1). The batched prover now throws the same switch the per-table prover uses under disk-spill and RecomputeLde: resident aux disabled per table before the aux round. Device consumption of the aux LDE belongs to the RoundCommit device path. Covered by a tall (2^13/2^12-row) tiling of the CPU/ADD/MUL fixture: host-path completeness unconditionally, and the same epoch under cuda — eligible for the GPU arm — must host-verify. The VM-epoch harness itself is a plain #[test], so the merge-group GPU CI prover suite runs it as soon as this branch line merges.
…the batched format The L2G carve-out's stark layer (D1). A batched epoch can commit ONE table's main matrix as its own row-pair tree instead of a matrix of the shared main round: the tree is built by the same committer the per-table prover uses over the same expansion, so its root is byte-identical to the per-table table's — which is what lets the cross-epoch root-equality binding read the same root from either format. The root is PROOF-CARRIED and absorbed after the preprocessed roots, before main_root, ahead of every challenge draw. Which table (if any) is carved is verifier-owned configuration, never read from the proof; the carved opening authenticates per query at the reduced index and feeds the DEEP/FRI join in place of the table's main-round row. Gates: end-to-end round trip at mixed heights (the carved table shorter than h_max, so the reduction is real); per-table byte-identity differential; tamper on the root and on an opened row; carve-state configuration mismatch both directions; the absorb-slot order pin on the transcript itself; the index-reduction convention pinned against literally-computed row pairs.
…d-MMCS proof with the L2G main matrix carved standalone (D1) prove_continuation_batched proves every epoch of a continuation in the batched format: one proof per epoch, the L2G table (last air, as always) carved into its own standalone tree whose root is byte-identical to the per-table L2G tree's. The claimed l2g_root is the proof-carried carved root, so verify_l2g_commitment_binding_view reads the same commitment out of either format and the binding code does not fork. The global memory proof is per-table in both arms. EpochProof's body is now an enum (per-table | batched, rkyv on both); verify_epoch dispatches on it — the batched arm mirrors the per-table one exactly: challenges replayed on a fork of the statement seed, the expected COMMIT-bus balance from the replayed shared pair, the complete carved batched verification, then the claimed-vs-committed L2G root equality. The batched proof types join the rkyv wire format. Gates: the D1 differential — the same execution proven per-table AND batched yields byte-equal L2G roots for every epoch, across at least two distinct L2G heights, and the batched bundle passes the complete host verification (epochs, global proof, binding view) through the rkyv round trip; tamper arms — a flipped claimed l2g_root and a flipped reg_fini are both rejected on the batched arm.
…d root absorb, standalone walk, census (D1 emitted side) The M-8 batched-verifier emitter learns the carve: the emitted program absorbs the proof-carried carved root in its pinned slot (after the preprocessed roots, before main_root — arena declaration order is absorb order), authenticates the carved table's row pair per query against those very cells at the reduced shared index (the preprocessed walk pattern with the root's provenance moved to the proof), and the DEEP crossing consumes the carved walk's cells in place of a main-round matrix row. The census closed form, the opening serializer and the schema words all carry the carved term; an uncarved epoch's program is byte-identical to before — every existing batched gate passes unchanged. The harness gains the carved sibling (real_batched_epoch_carved_from — the L2G bookend carved, the continuation batched format), with host verification threaded through the carve configuration one code path both ways. Gate (one test, five arms): the assembled carved verifier RUNS on an honest proof; census and schema match the carved closed forms; a tampered carved root, opening value and path sibling are each unprovable; and the wrong-reduction control fires on the carved walk — verdict condition 4's emitted side.
…aggregator-facing word schema (P2 wrap side) Three pieces, one landing: 1. real_batched_epoch_from_continuation — the batched sibling of the P1 constructor: any epoch of a batched continuation reconstructs from the bundle (chain position + reconstruct_epoch_airs, the same reconstruction verify_epoch runs) into a RealBatchedEpoch whose harvest — replay, COMMIT target, provenances, statement shape, and production's complete carved verify as the acceptance gate — is one function shared with the session harness, so the two paths cannot diverge. 2. The published-word schema (verdict condition 2), on CARVED programs only: after the bus total, the wrap publishes the register boundary vectors (init then fini), the epoch label, the epoch's output bytes, and the carved L2G root — the words P3's aggregator byte-compares across wraps and against the global proof. Every published cell is existing program state: zero new arena words, zero wrap-hash permutations (both asserted by the census and schema gates), ~135 publish instructions on a ~200k program, no height boundary crossed. Uncarved programs are untouched. 3. The P2 block driver (the_real_block_proves_and_wraps_end_to_end_batched, box-tier) and its suite-gated fixture twin: prove_continuation_batched → complete host verify → every epoch wrapped from proofs alone through the carved program — with the wrap's published L2G root byte-compared against the bundle's claim, exactly the aggregator's check. Gates: genesis AND final epochs of a batched fixture continuation reconstruct, emit, and RUN; a tampered reg_fini is rejected inside the constructor; the fixture driver flow proves + verifies the final epoch's carved wrap and its published root matches the claim. Suite 997/1-standing; make lint/fmt green.
…he aggregation wrap preset (blowup4/110q, terminal 2^8) The aggregation layer consumes batched-format wraps as serialized bytes; BatchedLfmProof now carries the rkyv wire derives, gated by a round trip through the complete verifier. aggregation_wrap_options() pins the decided A-point for the wrap layer — blowup 4 (110 queries at the Johnson-bound target) with the FRI terminal at degree 2^8 — chosen for the wrap's VERIFIER: the aggregator pays per query per wrap, and the terminal trade swaps one committed layer's 110 openings for 128 absorbed coefficients. Inner epochs are untouched: the wrap program is a function of the inner proof's options, so no program identity moves.
…ed wraps verified in ONE emitted program (P3 core) The batched-LFM verify leg is the first emitted verifier whose target is an LFM-machine proof: the spine replays absorb_lfm_statement byte for byte with the wrap's program id as an emit-time constant, preprocessed roots absorb from the AIR set as constants, and the LogUp closure's target is the LFM_PUBLIC balance recomputed in-machine from the wrap's claimed words (canonicity-guarded halves). Every soundness-critical emission is the wrap program's own machinery — the leg adds no new cryptographic arithmetic. aggregator_program assembles N legs (arena declaration order = absorb order, leg by leg) and the chain bindings: one shared attestation id, register fini→init across every seam, each epoch label pinned to its chain position as a program constant. The aggregate publishes the id, the block's register boundary vectors, the final output bytes, and every wrap's carved L2G root. Gates: the leg runs and reproduces production's replay challenge for challenge on a real wrap; a tampered opening and a moved public word are each unprovable. The assembled aggregate verifies EVERY epoch of a batched-carved fixture chain wrapped at the aggregation preset in one execution; a broken register chain and a swapped wrap order are each unprovable. A page-census probe (execution only, no proving) reports the global proof's real shape for the aggregation census.
…obe, drop redundant casts The previous commit pushed with make lint red (a shell-flow slip: the compound command continued past the lint failure); this restores the lint-before-push invariant. No behavior change: unused-import removal, same-type-cast removal, and cfg(test) on the page-census probe, which has no production caller by design.
…, the L2G binding in-VM, the attestation joined and folded (P3 assembly) The global-verifier program is the per-table machinery pointed at the cross-epoch global proof: one constant-run statement, Phase A over the L2G re-commits and the per-page GLOBAL_MEMORY tables (genesis roots as AIR-set constants), full verification legs per table, the GlobalMemory bus closed at zero — publishing each epoch's L2G re-commit root. Proven as a sixth batched wrap, it makes the aggregator six uniform batched-LFM legs. The aggregation program adds, over the legs and the chain bindings: the in-VM L2G root-equality (each epoch wrap's published carved root byte-compared against the global wrap's published re-commit root), the attestation join (one hinted (elf, pc, decode) triple whose num_pages = 0 fold must equal EVERY wrap's published id) and the final attestation (ProgramIdShape num_pages > 0 — its first caller — folding the genesis page commitments), and the block artifact's published words: the final id, the register boundary vectors, the output bytes, the five L2G roots, the folded page bases, and the touched-page list with the private-input count as program constants (the consumer contract's data availability). Gates: the global leg runs on a real fixture bundle's global proof and rejects a flipped re-commit root; the six-leg aggregate runs on the fixture chain with its published id equal to the CONSUMER'S OWN recompute (program_id_from_digest over continuation_precomputed_commitments — the contract's compare as the gate's oracle); a broken register chain, a forged attestation input and a moved global root are each unprovable; and the leg census gate pins the walks to the in-code closed form (batched_query_permutations_for), delta-measured, hash-aware. The box driver (the_real_block_aggregates_end_to_end) runs the whole pipeline to ONE PROOF in one process, consumer ritual included and timed. SOUNDNESS.md carries the applied η re-tune note (base ≈114-117; the class-split floor tracks it 1:1 — the ε_C lift carries no η — settling the review's unresolved point) and the query-sweep boundaries. Suite 1008/1-standing; lint/fmt green.
…n residency posture The first real-scale aggregation attempt was OOM-killed at the 483 GiB cgroup under Retain, after ~62 minutes of base and wrap proving that the retry would have re-paid. The driver now persists the bundle and all six wrap proofs over the rkyv wire when P3_ARTIFACT_DIR is set and loads them on relaunch — programs and artifacts re-emit deterministically in minutes; only the proves are cached. P3_AGG_RESIDENCY selects the aggregation prove's own residency (recompute trades ~2x prove time for the LDE peak) without touching the wrap proves' measured Retain posture.
…a pipe-swallowed exit code pushed red The same failure class this campaign has now hit three times (exit codes laundered through pipes); the previous commit's lint run went through tail and its Error 101 never stopped the chain. Verified green with the exit code read directly this time.
…G_TERMINAL_BLOWUP) Three straight OOM kills at 483 GiB (P3-OOM-REPORT.md): the blowup-4 LDE terms of the 2^21x3056 aggregation trace do not fit the box under either residency posture. The terminal layer's options are separable from the wrap layer's — the wraps and the aggregation program keep Design A's blowup4/110q and the cached wrap proofs stay valid — so the driver now lets the aggregation prove itself take a smaller blowup. P3_AGG_TERMINAL_BLOWUP=2 halves every LDE term; the query count re-derives from the same 128-bit Johnson target by construction (with_blowup: 2 -> 219 q), and the FRI terminal stays at the preset's fp8. Unset, nothing changes.
…nsumer precompute Run 4 proved the block (terminal blowup2/219q, 34.7 min, 336.8 GiB peak) and saved nothing but a byte count — the proof died with the process. The driver now writes block_proof.rkyv into P3_ARTIFACT_DIR next to the inputs it loads. The consumer ritual's expensive half (continuation_precomputed_commitments, a native FFT+Merkle pass) and build_artifacts each get their own timing line — run 4 hid them inside a ~401 s unaccounted gap, and design-review condition 1 asks for the ritual's price by name.
The chip is one row per compression at 3,056 value columns, so its matrix is WIDE rather than tall: the aggregation program's ~1.39M compressions land in a 2^21 x 3,056 table whose blowup-2 LDE is a single ~102 GB allocation, and that allocation is the aggregation prove's measured spike. Blake3Chunking splits the rows over several instances, exactly as KeccakChunking already splits KECCAK_RND and for the same reason its header gives: the chip has no row-to-row constraint at all (every b.main() reads offset 0), every bus interaction is a within-row token gated by MU or a per-word multiplicity, and a compression's inputs and outputs travel on LfmMem by address matching over PREPROCESSED addresses. LogUp cannot tell which instance a row lived in. BITWISE stays one shared receiver fed the whole record list, as it must. One thing differs from KECCAK_RND, and it runs through the whole change: this chip HAS a preprocessed instruction group, so a chunk is its own committed matrix with its own Merkle root and its own height. Chunk 0's root is the roots array's slot-11 entry — which is what makes a single-chunk program bit-identical to an unchunked one — and chunks 1.. ride LfmArtifacts, are absorbed by the batched preprocessed round in slot order, and are folded into program_id as a tagged, length-prefixed TAIL. An unsplit program absorbs no tail, so all six blessed LFM_REGISTRY digests are the byte-identical values they were blessed at. The policy defaults to a single unbounded table, so nothing moves until a caller asks. LfmRegistryEntry gains no column: every registered program is a fixture at the default, LfmRegistryEntry::artifacts derives the shape, and every_registry_entry_is_a_single_blake3_table pins that premise so blessing a chunked program fails loudly rather than resolving the wrong shape. verify_against keeps its signature as the single-LFM_BLAKE3 door; chunked callers go through verify_against_artifacts / verify_against_chunked, and a chunked proof handed to the old door rejects on the AIR count.
…3_MAX_CHUNK_ROWS_LOG2) Read at PROGRAM EMISSION time and applied to the AGGREGATION program alone, in the P3_AGG_TERMINAL_BLOWUP / P3_AGG_RESIDENCY pattern: the six wraps are cached artifacts at the census point, and re-chunking them would invalidate the cache for no gain — the ~1.39M compressions that make the spike are the aggregation program's own. Unset is one table, i.e. today's shape. When set, the driver prints the chunk geometry beside the terminal options it already prints. The chunk shape is bound into program_id, so a chunked aggregation is a new emit-time identity. That is fine here and nowhere else in the block run: the layer builds fresh artifacts and the consumer contract pins the identity. The aggregate leg's query census gets its chunk-invariance stated as a control rather than assumed. Chunking redistributes rows over AIR instances after compilation, so the instruction stream the closed form counts is the same program; a chunking that reached back into emission would move the census silently, and the aggregation program is exactly where chunking is switched on.
…er permutation
Rescue-Prime Optimized behind the frozen LFM_HASH tuple contract, as the
socket's first production-candidate tenant. Poseidon is off the table
(2026/306, 2026/1692) and RPO is the algebraic candidate the break class does
not structurally reach: no partial rounds, and no cheap algebraic direction in
either composition order.
Parameter provenance is two independent sources checked against each other.
The spec's own SHAKE256 generator ("RPO(p,12,4,128)", nine-byte little-endian
chunks) was re-run outside this repository and reproduces miden-crypto's 168
ARK1/ARK2 constants exactly; the MDS row is the spec's get_mds(12) and miden's
first row, identically. The oracle is miden's own hash_elements table — all
nineteen vectors replay through this permutation.
The lane convention turned out to be a gift rather than a choice. miden's
RPO256 puts the rate at lanes 0..8, the capacity at 8..12 and the digest at
0..4, which IS the socket's own layout, so no lane permutation is needed
anywhere and a Compress row with the zero capacity is literally Rpo256::merge —
checkable against miden by someone who has never seen this codebase.
Layout W, one row per permutation: 28 shared prefix + 7x48 ladder columns +
6x12 inter-round state = 436 value columns, 429 constraints, max degree 3. The
inverse S-box is verified as the FORWARD power, (y3)^2*y = v — the spec's own
4.3 folding trick — so a ~2^63 exponent costs one ladder rather than a degree
explosion. Padding by zero survives in both S-box directions, so blowup 2 is
untouched.
Domain separation lands here rather than later because it costs zero cells and
the S8 copy constraint is the hook: the capacity copy is now PER MODE, carrying
miden's merge_in_domain construction (tag in capacity lane 9, padding flag
reserved in lane 8, security argument in the RPX spec's Appendix C). A
transcript step and a Merkle parent over the same two cells are different
functions, and the AIR rejects a row carrying another mode's capacity.
That change found a live bug in the trait rather than only in RPO: transcript_out
and leaf_out routed through compress_out, which hardcodes compress_iv(), so a
hasher separating its domains through the CAPACITY would have had its overrides
silently dropped on the host while the chip constrained the separated version.
The defaults now route through one permute_two_cells(a, b, iv) helper and each
mode passes its own IV. Test, Poseidon and Blake3 are unchanged.
No existing root moves: the preprocessed group is hasher-independent, so RPO is
a new program identity through the hasher tag and nothing needs re-blessing.
Measured against the scoping doc: 436 columns as predicted, 445 cells per
permutation against a predicted ~448, and 429 constraints against a predicted
433 — the doc assumed eight unread-IN pins where there are four, the leaf RATE
having emptied input slot 1's set. 11.1x cheaper per compression than slot-11
BLAKE3, 1.40x cheaper than the Poseidon reference.
…and the chain is not the reason
The scoping doc's second-riskiest unknown was host RPO commit throughput,
estimated at "20-60x slower than BLAKE3 per byte scalar". Measured on an
M-series laptop, single thread, release:
RPO256 permutation 17,180 ns (58.2k perms/s)
of which the inverse S-box 14,887 ns = 87%
Goldilocks FieldElement mul 2.64 ns
BLAKE3 64-byte parent 61 ns
RPO / BLAKE3 per compression 280x
Both hashes absorb 64 bytes per invocation, so 280x per compression is 280x
per byte. The estimate was 5-14x optimistic.
The attribution is the point, and it exonerates the implementation: 72
multiplies at 2.64 ns predicts 190 ns for one inverse S-box against 177 ns
measured, and ~8.4k multiplies predicts ~22 us for the permutation against
17 us measured. The chain is running at the field multiply's speed limit and
there is nothing in it to tune. The headroom is SIMD across the twelve lanes,
which is exactly what miden-crypto ships hand-vectorized kernels for (ARM SVE,
AVX2, AVX512, scalar as fallback) — RPO's S-box layers are embarrassingly
parallel across lanes.
Consequence for the projection, at aggregation scale on 11 cores: RPO does
4.4x FEWER compressions than BLAKE3 (2.8B cells against 12.2B) and still pays
~36 minutes of commitment hashing against BLAKE3's ~34 seconds. The doc's
~8 min prove was extrapolated cells-linearly from a BLAKE3 prove in which
commitment hashing was a rounding error, and that assumption does not survive
the swap. The cell and memory halves stand — 445 cells/perm is measured, so
~2.8B cells and the 128 GiB envelope claim are unaffected, since throughput
costs time and not residency.
So the honest headline is that RPO buys memory at a price in time, and the SIMD
kernels move from nice-to-have to required for Stage 1 rather than Stage 2.
Kept as an #[ignore]d test rather than a criterion bench: it prints the numbers
and asserts only a floor loose enough that no honest machine trips it.
… and a single-reduction MDS Two changes, both gated by the same miden known-answer table the module has always been pinned to, so correctness is not the question and speed is the whole point. 17,180 ns per permutation to 4,712 ns; RPO against a BLAKE3 64-byte parent falls from 280x to 74x, which is back inside the scoping doc's original 20-60x estimate. The inverse S-box moves from per-element to WHOLE-STATE. Its addition chain is 72 multiplications each depending on the last, so a single lane is latency-bound: ~2.6 ns of multiply latency times 72 is the entire cost and the multiplier pipeline idles between them. The twelve lanes are independent, so running them in lockstep interleaves twelve chains and fills the pipeline. That is 5.3x the serial rate, measured, and it is the same shape miden's scalar fallback has and the shape its SVE/AVX2/AVX512 kernels vectorize from. Per lane: 177 ns to 35 ns. The MDS becomes one u128 accumulation and one reduction per lane instead of twelve field multiplications. Every constant is at most 26, so a term fits 70 bits and the twelve-term row sum fits 73 — comfortably inside a u128 — and the row reduces once at the end via 2^64 = EPSILON (mod p), with the carry small enough that its correction needs no reduction of its own. Both facts are asserted rather than trusted to the comment. 180 ns to 94 ns. The remaining breakdown, which is the useful handoff for whoever ports the SIMD kernels: inverse S-box 63%, MDS 28%, forward S-box 5%. At aggregation scale on 11 cores this takes the host commitment phase from ~36 minutes to ~10, i.e. the prove roughly doubles rather than quintuples.
…mn needs no closed form of its own The census decomposition is "absorption is rate-sensitive, compression is not". RPO's rate is 8 felts and a BLAKE3 block is 8 felts, and both share the no-spurious-final-block rule — an exact multiple of the rate emits no extra invocation, unlike keccak's pad10*1. A digest is four felts on both sides, so a Merkle parent is one invocation under both. The consequence is worth stating as a test rather than a comment: blocks_for and query_permutations_for need NO RPO arm, because the aggregator's already measured BLAKE3 compression count IS its RPO permutation count. Only the cells-per-invocation moves, from 4,946 to the measured 445. That is what lets the RPO column of the comparison table be computed on the same instrument that measured the BLAKE3 one, instead of on a second closed form nobody has validated. Keccak is included as the control: its padding DOES spend a trailing block on an exact multiple, so the invariance is a property of these two hashes and not of the closed form. The test also records what it assumes — the rate-8 overwrite duplex of spec 2.6, not the socket's as-built rate-4 leaf chain. Under the chain the absorb terms double and the invariance fails, which is the open leaf-convention fork. This pins the arithmetic of the good branch, not that the branch was taken.
… twelve lanes The commitment workload has a billion INDEPENDENT permutations, so the obvious follow-on to the whole-state rewrite was to interleave two or four of them and widen the same trick that already won 5.3x — a portable speedup needing no SIMD, no unsafe, and no architecture-specific code. It does not work. Cost per lane rises monotonically with the independent-chain width, measured on an M-series laptop: 12 lanes 46.2 ns, 24 lanes 51.1, 48 lanes 54.2, 96 lanes 53.7. Twelve chains already saturate the multiplier pipeline, and past that the working set — a width-24 state is 24 u64 plus seven addition-chain temporaries — exceeds the general-purpose register file and spills. This is the load-bearing NEGATIVE result behind the lane's SIMD verdict: there is no portable instruction-level parallelism left to extract, so any further speedup has to come from real vector instructions. Kept as a test rather than deleted, and asserting its conclusion rather than only printing it, so that if wider batching ever does start winning, the verdict gets revisited instead of silently standing on a measurement nobody re-ran. Worth one run on Zen2 before anyone writes a batching layer there: the conclusion rests on a register-file argument and that box has a different file.
…, and the program text is hash-generic already A host FRI commitment-opening proof whose every hash — Merkle leaves, tree nodes, and the Fiat-Shamir transcript — goes through RPO, verified by the machine: sponge replay, Merkle-authenticated openings, alpha-combination, two unnormalized folds, terminal check. Plus the tamper gates that make it mean something (a tampered opened row must break its Merkle path, a tampered commitment must break the transcript replay) and the cross-hasher rejection (an RPO-committed proof must not be provable under Poseidon or Test). The finding is what did NOT have to change. `programs::fri_toy_program` is emitted once and unchanged, and nothing in it is RPO-specific: it speaks only the frozen LFM_HASH socket ops, and which permutation those rows prove is HasherKind, chosen at AIR-build time. The same program text is a Test-verifier, a Poseidon-verifier and an RPO-verifier. That matters for the three-way comparison the campaign wants. The socket-native world — edsl::merkle_walk, SpongeVar, compress/leaf/transcript_step, with the host mirror in fixture.rs already parameterised by HasherKind — is a complete, tested, field-native emitter and commitment pair. It is not something this lane has to build. A third algebraic candidate joins it by supplying a permutation and a chip arm, with zero emitter work. What remains genuinely unbuilt is the PRODUCTION path: crypto/stark commits under byte-oriented keccak/blake3 with 32-byte two-cell digests, and taking a real epoch or wrap proof to RPO is where WrapDigest has to become hash-dependent. That piece is unchanged in scope; this one turned out already done.
…ation and 2.37x RPO's host speed Rescue-Prime eXtended (XHash12, eprint 2023/1045) is a round-function swap on RPO's geometry, not a redesign: same state width 12, same rate 8 and capacity 4, same four-felt digest, same MDS, and literally the same ARK1/ARK2 tables, which this module imports from rpo rather than re-deriving so the two cannot drift. The schedule is what changes — FB E FB E FB E M, where the three FB rounds are RPO's round verbatim, the three E rounds raise four lane-triples to the seventh power in the degree-3 extension field with no linear layer at all, and the final round is MDS plus constants and nothing else. That attacks precisely the term this lane measured as dominant. The inverse S-box is 60% of an RPO permutation on the box; RPX runs three inverse layers where RPO runs seven. Measured on one machine in one run (hash_ladder_throughput, which times all three candidates and BLAKE3 together so the RATIOS are machine-independent even where the absolutes are not): RPX 2503 ns against RPO 5922, a 2.37x speedup, and 41x a BLAKE3 parent against RPO's 96x. It is also narrower in the AIR: 316 value columns and 309 constraints against RPO's 436 and 429, because an E round commits two extension intermediates per triple where an FB round commits two ladders per lane, and the M round commits nothing. Measured cells per permutation, on the same census instrument as every other column: RPX 325, RPO 445, Poseidon 621. Degree stays exactly 3 in all three round kinds. The extension seventh power lowers the same way the base-field one does — commit t2 = x*x and t3 = t2*x, then write the output as (t3)^2 * x — with each extension operation stating three base-field coefficients, which is why an E round costs 36 columns rather than 12. Padding by zero survives all three kinds, so blowup 2 is untouched. The per-mode capacity prefix is now emitted once and shared by both tenants rather than restated per arm: RPO and RPX have identical socket geometry, so that prefix was the one place their AIRs could silently disagree about domain separation. PROVENANCE IS WEAKER THAN RPO'S AND THE MODULE SAYS SO. miden publishes no RPX known-answer table — its tests are structural only. So the anchors are (a) the shared constants, MDS and FB round, externally anchored through RPO's nineteen vectors, and (b) the new extension arithmetic, pinned against naive polynomial multiplication mod x^3 - x - 1 and against generic exponentiation — different algorithms for the same functions, not a second transcription. A deployment decision should treat "no published KAT" as a real cost. NOT XHash8: its extra speed comes from a partial S-box layer, and a partial layer is one of the three structural footholds this project's own break analysis identified in the 2026 Poseidon collapse. Flagged in the module header rather than adopted quietly.
…the variance was the story The ladder reported RPO at 5,922 ns where this lane's own rpo::throughput reported 4,712 for the same code on the same machine. Two numbers for one quantity is exactly the confusion the campaign's per-number labelling rule exists to prevent, so it was worth finding out which was right. Neither, quite. Monomorphising the timing helper over the concrete hasher instead of dispatching through HasherKind moved it only 5,922 to 5,647 — so the enum was not the cause. The cause is run-to-run variance: rpo::throughput itself produced 4,712, 5,685 and 6,576 across earlier runs, roughly plus or minus 20%, which is larger than the gap between two candidates would need to be to matter. Quoting 4,712 as though it were precise was reading a lucky sample. So the ladder now takes the best of five runs at 50,000 permutations each. The minimum is the standard robust estimator for a throughput microbenchmark — noise only ever adds time — and it reproduces: two consecutive runs gave an RPX/RPO ratio of 0.56 and 0.55, and Poseidon's absolute agreed to 0.04%. The correction that matters is which output is load-bearing. Absolutes on this laptop are not; RATIOS measured within one run are, because the candidates share conditions. That is why the ladder times all of them together, and it is what the box column should be scaled by rather than by a laptop absolute. It also moves the Poseidon reading: best-of-five puts it around 1.4x SLOWER than RPO, where a single sample had shown the two roughly equal.
… a hash swap as it stands Every RPO/RPX/Poseidon figure this lane has produced is a proxy: measured chip cells and measured host ns, extrapolated cells-linearly off BLAKE3's single measured full-scale prove. The obvious cheap de-risk is the fixture, which already commits end to end under any tenant — so the question is whether it can produce one genuinely measured algebraic data point. As it stands, no. The FRI fixture verifier's LFM_HASH chip is 0.4% of its 15.9M cells (RPO 56,192; RPX 40,832; Poseidon 78,720), because the program is dominated by FIXED-height lookup tables that do not scale with its workload. Swapping RPO for RPX therefore moves the total by about 0.1%, far under this laptop's own run-to-run variance of roughly 20%. That is the opposite mix from the aggregator, whose hash table is ~85% of 12.2B cells and whose fixed floor is a rounding error, and it is the number that decides how much work a fixture-based de-risk actually is. The sizing it feeds is in HASH-SWAP-DESIGN.md section F. Asserting the finding rather than only printing it, so that if the fixture is ever scaled to where a swap IS measurable, this fails and the sizing gets revisited instead of standing on a measurement nobody re-ran.
…gainst-machine (A2) The one open correctness question in the algebraic swap. A wrap program verifies a proof the host produced, so the in-VM transcript replay must re-derive exactly the challenges the host derived. Get the encoding wrong and Fiat-Shamir does not fail loudly: the walk reconstructs nothing, a difference that should have been non-zero is inverted, and the executor reports DivByZero at an address that names neither the hash nor the site. Three facts made it tractable, each checked rather than assumed. The transcript is a caller-supplied parameter — prove and verify take `&mut impl IsStarkTranscript` — so this is a new type and nothing the byte path uses is edited. IsTranscript is already felt-native where it matters: append_field_element and sample_field_element speak FieldElement, and only append_bytes and state() are byte-typed. And append_bytes has a tiny regular call surface: across the whole STARK core it takes exactly two things, 32-byte Merkle roots and 8-byte integers, and a 32-byte root under an algebraic hash IS four felts, which is exactly one SpongeVar cell. The convention: state is one cell, zero-initialised, every step one transcript- domain LFM_HASH step, identical to SpongeVar because matching it is the point. append_bytes absorbs a length cell then the payload in 32-byte cells, as DIGESTS. append_field_element absorbs the three Fp3 coefficients as one DATA cell through the leaf encoding — a different hash domain, so a program that absorbs a root cannot claim it absorbed a field element. state() serialises the four state felts canonically for grinding. sample_u64 masks rather than rejection-samples, so it consumes exactly one cell per draw: every STARK call site passes a power of two, where the incumbent's rejection threshold is zero and its loop never rejects, and a straight-line machine cannot emit a loop whose trip count depends on a sampled value. The length prefix is the injectivity argument, not decoration: without it a 32-byte root whose tail is zero and an 8-byte integer holding the same leading bytes absorb identically. There is a test for exactly that collision, with the control showing the payload cells really are the same and the prefix is the only thing separating them. The rule is uniform rather than special-cased on 32 and 8, because a conditional encoding is how a third call shape introduces a collision later. The gate is a differential: a program drives SpongeVar through the same sequence written from the CONVENTION rather than from this implementation, is proved, and its published challenges are compared against the host's — under Test, Poseidon, RPO and RPX. If the two sides ever disagree about the encoding they disagree about the challenges, and that is a failing test rather than a DivByZero. The type is parameterised by HasherKind, so all four tenants share one implementation and a fifth costs nothing here.
…ng it An `#[ignore]`d measurement that prints the artifact build's wall at this host's rayon width, so the branch is not pushed with an unmeasured claim: run it twice, once with `LFM_ARTIFACT_PARALLEL=0`, and the two walls bracket the change. ⚠ AND IT CARRIES ITS OWN WARNING, because this lane was misled by it. The fixtures available to a laptop concentrate almost all their committed felts in ONE NARROW group, and a `par_iter` over columns can only spread across the columns that exist — so they are close to the WORST case for exactly the change they are measuring. A 27 MiB scaled sponge read serial 1.547 s against parallel 1.447 s and I reported that as "a wash, the parallel build is not the lever". The box then measured **−31% on `build_artifacts`, −21% on the wraps, −20% on level 1**. The conclusion was a statement about the fixture; the measurement was fine. ⇒ The harness now prints the WIDEST GROUP'S COLUMN COUNT beside each wall, and says in the same breath that lane P measures `emit_lde` at 445% CPU on a real node — 4.5 of 30.7 cores — which is where the headroom is. A number that cannot be read wrong is better than a number with a caveat somewhere else.
…st reproduce Lane K phase 3, derived before any code so it is not re-derived: the host grinding predicate over AlgebraicDigest<RpxCommit> is the LEAF sponge over felts_from_bytes of inner_hash || nonce.to_be_bytes() — five big-endian u64 felts (FE::from reduces a raw value >= p once; the inner felts are already canonical, the nonce may not be), one permutation of [f0..f3, nonce, 0, 0, 0 | 5, LFML, 0, 0], and the head is the canonical lane 0 read back big-endian, so on device valid <=> s[0] < limit. The kernel shape (twin of keccak.cu grind_search, one __noinline__ permute per candidate), the launcher policy, the pin-decided dispatch key and the PTX, register and timing predictions are stated with it.
The device grind has been keccak-only, so under the RPX pin every table's ~2^20-trial nonce search ran on the host: one RPX permutation per trial, 2,368 ns each on the 9950X, ~41.9M permutations per base epoch. `rpx_grind_search` is the twin of keccak.cu's `grind_search` — grid-stride over `[base, base+count)`, one hash per candidate, `atomicMin` of the first hit so the launch returns the globally smallest valid nonce in its block. What differs is the hash, and the mapping it has to reproduce is lane K's derivation, kept with the kernel: the outer 40 bytes are exactly five big-endian felts, `f0..f3` the inner hash and `f4` the nonce, sponged as ONE leaf permutation with capacity `[5, LFML, 0, 0]`, and the host's `from_be_bytes(digest[..8])` IS canonical lane 0 — so the predicate on device is `digest[0] < limit`. The five absorbs go through `rpx::Sponge` rather than writing the twelve lanes out, so the capacity rule keeps one statement on device and a change to it cannot leave the grind behind. The nonce lane is `goldilocks::canonical`, which is `FE::from` exactly; it is a no-op for every reachable nonce, and absorbing it makes that true by inspection instead of by an argument about reachability. The launcher's range walk is now written once and shared by both arms: same min-factor gate, same block sizing, same sentinel loop. The RPX arm launches at 128 threads, what every other RPX kernel uses for a twelve-lane state. The host shim grows `gridDim` and `atomicMin` because `rpx_host_kat.cpp` includes this file, plus a single-thread driver for grid-stride kernels — `CUDA_HOST_FOR_EACH_THREAD` leaves a zero stride, which is an unterminated loop.
…tion's hash The dispatch keyed the device search on `TypeId == PlatformKeccak256` and sent everything else to the host. The RPX arm cannot be keyed that way: its digest is `prover::lfm::algebraic_commit::AlgebraicDigest<RpxCommit>`, and `prover` depends on this crate rather than the reverse, so there is no type here to name. The key is `H::COMMITMENT_HASH`, read at the call site. ★ `H`'s constant, NOT the global `config::COMMITMENT_HASH`. The global names the aliases' hash and stays BLAKE3 under the RPX pin — `hash_pin` pins `BlockStarkHash` separately, on purpose, so the two can differ on a branch. A dispatch keyed on the global would read BLAKE3 while the block proved under RPX and the arm would be dead code that still compiled. `config.rs` says as much about which of the two constants a call site may read; this is that rule applied. What the key does not settle — that a configuration naming `Rpx256` also transcripts with RPX — is left to the unconditional host validation that was already there: a mismatch costs one device search per table and falls back loudly, and can never append an unverifiable nonce to the transcript. The keccak arm keeps its `TypeId` check on top of the key, so its behaviour is unchanged. `inner_hash_felts` is the big-endian reading of the inner hash, next to the little-endian `inner_hash_lanes` keccak needs and named separately rather than flagged: the two read the same bytes in opposite orders, and crossing them compiles, runs, and silently searches for a nonce under a message the host never hashes. Bycatch: the grinding factor is read into a local called `grinding_factor`. It was `security_bits`, which it is not.
… with no GPU The grind kernel is the one RPX kernel whose correctness is a claim about a HOST predicate rather than about the permutation: it must find the nonces `stark::grinding::is_valid_nonce` accepts over `AlgebraicDigest<RpxCommit>`. The two reach the sponge by different routes — the host through a byte buffer and `felts_from_bytes`, the kernel by building the five felts directly — so the agreement is the thing to pin, and per-PR CI has no GPU to pin it on. Table 5 of the oracle is that agreement. The generator takes the smallest valid nonce through the production predicate and asserts, over the whole scanned range, that an explicit five-felt block answers identically; a row that passed only one of the two routes would not print. Layer 8 of the host-compiled harness then replays `rpx_grind_search` single-threaded over those rows: the nonce, its minimality (nothing in `[0, nonce)`, which also exercises the not-found path the launcher's range walk depends on), that `base` participates, and the endianness control — the little-endian reading of the same inner hash, the one keccak uses, finds NOTHING where the correct reading finds the nonce. Not vacuous: four mutations of the kernel were each rejected — padding flag 5 → 4 (7 failures), the first two absorbs swapped (6), the head read from lane 1 (7), and the loop bound off by one (3). Tables 2-4 regenerate byte-identical.
… reaching it The kernel's arithmetic is pinned without a GPU by the host harness. What needs one, and is here: that a real parallel launch reduces to the same answer, and that the production dispatch actually reaches the device. The first two tests assert validity under `is_valid_nonce` — never a proof byte, and never a comparison with the CPU search, whose `find_any` does not agree with itself between runs. At factor 14 the returned nonce must also be the smallest, which is the probe of search completeness plain validity cannot make: a stride or bounds defect still returns a *valid* nonce, just not the first one. It is deterministic despite the parallel grid because `atomicMin` is order-independent — the property the single-threaded host harness cannot exercise and this test exists for. The third is the one that can fail for the reason this feature can fail. Both dispatch arms return a valid nonce whatever happens, because the CPU fallback is correct, so validity alone would pass with the device never touched. `gpu_grind_calls` counts only device searches whose nonce passed the host check, so the deltas are the claim: +1 under `Rpx256`, and unchanged under `Blake3`, the control that makes the first delta mean something. Run on the box with cargo test -p lambda-vm-prover --release --features cuda --test rpx_device_parity -- --nocapture
…ating a felt Vec Every `AlgebraicDigest` finalize built a `Vec<FE>` through `felts_from_bytes` and handed it to `sponge_leaf`, which consumes the felts one rate block at a time and never looks back. The felt count the capacity needs is `ceil(len/8)`, known from the length alone, so the Vec bought nothing. Under the algebraic pin it was one of the two heap allocations every proof-of-work grinding trial paid, and grinding is ~2^20 trials per table. MEASURED, paired ABBA over 2.4M calls on the 40-byte grinding message, three runs: 691 / 322 / 269 ns per trial, 8.6% / 5.5% / 4.3% of the trial's hash. The laptop is under contention from other lanes, which is why the pairing is not optional — unpaired runs moved the untouched `permute` by 45% between them. ⚠ The OTHER allocation is deliberately left: `AlgebraicDigest`'s own `buf` Vec. Removing it means reusing one digest instance across the rayon search, and the same paired A/B puts the prize at −60 to −75 ns, i.e. indistinguishable from zero and on the wrong side of it. It is not worth restructuring `find_any` for. `sponge_leaf_bytes` is equivalent to the two-step form BY TEST, not by construction: the test walks every length across two rate blocks, for all three tenants, and the trailing group's zero-extension side is exactly the thing that is easy to get backwards — extending on the high side instead of the low fails it at one byte. The host search gets its own gate too. It is the arm every non-GPU build, device error and `LAMBDA_VM_NO_GPU_GRIND` falls back to, and it now runs on the changed code path. A break that moved the search and the verifier's check TOGETHER would leave a self-consistent prover, so the cross-hash control — BLAKE3 work must not satisfy the RPX predicate — is what makes it more than a tautology.
…nd-trip test Inserting two tests above it displaced them onto the first of the new ones, which left `a_digest_round_trips_through_its_commitment_bytes` without a `#[test]` — silently not run — and gave a neighbour two. `make lint` catches the duplicate; nothing catches the orphan, so the test count is checked against the base: 14 before, 16 after, and the only new functions are the three this branch adds.
…evice `gpu_lde` already does, for the main trace, exactly what the LFM artifact build does on the host for every program's instruction column groups: coset LDE, leaf hash and Merkle tree. Lane P measured the host version at 12.6 s per epoch wrap and 22.0 s per interior node — the largest phase of the recursion pipeline — with the card at 1 MiB and 0% throughout. The only thing standing between the two was that every entry point in the module is `pub(crate)` and the caller is in another crate. `try_commit_row_major` is that entry point. A named `pub` wrapper rather than a visibility change on the dispatch layer, so the caller sees one function with one contract instead of the module's internals. It returns the ROOT and nothing else, because that is all the artifact build wants: the root goes into `lfm_program_id` and into the AIR's declared commitment, and the nodes have no host reader. The tree stays resident on the device in the handle, which is dropped here, and `retain_host_lde = false` skips the row-major device-to-host copy entirely. ⚠ It deliberately does NOT feed the process-wide precomputed-tree cache. `precomputed_tree_cache_put` takes a FULL host tree because `multi_prove` opens against it, and a root-only tree in that cache would be one that cannot answer a query — a silent failure, not a loud one. Nothing is lost: `multi_prove` already builds and caches its own precomputed tree on the device (`try_expand_split_trees_row_major_keep` with `build_precomputed`). ⛔ THE WEIGHTS ARE NOW ONE DERIVATION, and that is the load-bearing part of this commit. `coset_weights` — `[n_inv, n_inv·g, n_inv·g², …]`, the iFFT normalization folded with the coset generator's powers — was written inline inside `LdeTwiddles::new`. It now has two readers: a table's weights for the prove, and a preprocessed group's weights for a commit taken outside any prove. Left inline in both, a change to the normalization would move one path's roots and not the other's — and the two are REQUIRED to agree bit for bit, because a proof declares the root the artifact build produced. ★ That agreement is not a hope; it is already a production invariant. `multi_prove` rebuilds the precomputed tree on the device from the row-major main trace and REFUSES the proof when its root differs from the one the AIR declares (`ProvingError::PrecomputedCommitmentMismatch`); for an LFM proof the declared root is exactly what the host artifact build produced, and every GPU recursion proof passes that check today. So the device leaf convention and `commit_bit_reversed_with(.., ROWS_PER_LEAF)` already agree on this class of matrix. ⚠ NOT MEASURED HERE, and it cannot be on this machine: there is no local CUDA, so this is verified by reading plus a `--features cuda` compile plus the non-cuda build. The roots gate is the six `registry_drift_*` tests, which must be run on the box against a cuda build before any number is claimed.
`build_artifacts_with_hasher` ran the whole preprocessed commit pass on the host — interpolate, coset-expand, Merkle — even on a cuda build, because `commit_lde_columns` has no device path. Lane P measured the result: 12.6 s per epoch wrap and 22.0 s per interior node, the largest phase of the recursion pipeline, with the card at 1 MiB and 0% throughout. The identical operation on the main trace has run on the GPU inside `r1_main_commit` all along. `commit_group_device_or_host` sends each group to `stark::gpu_lde`'s fused call and falls back to the host pass when there is no device, when the field is not one the kernels take, or when admission declines the shape. ★ THE GROUP IS ALREADY IN THE RIGHT LAYOUT, which is what makes this small. `ColumnGroup.data` is row-major `padded_rows × width` — exactly what the fused commit takes — so the device path skips `group_columns` entirely. That transpose is a strided gather over the whole group and exists only to feed the host's column-major pipeline. ⚠ WHAT THIS DOES NOT DO. It does not put anything in the process-wide precomputed-tree cache. That cache holds FULL host trees because `multi_prove` opens against them, and the fused call deliberately returns a root-only host tree with the nodes resident on the card. Nothing is lost: `multi_prove` already builds and caches its own precomputed tree on the device. The tree cache-put is therefore NOT folded in here, and was sized at 1.3–1.6% separately. THE DEVICE SET IS REPORTED, NOT GUESSED. `device_artifact_peak_bytes` carries the largest working set any artifact commit asked for, taken from `stark::device_set`'s own term-by-term accounting — one LDE buffer, the trace-domain snapshot, one full Merkle node buffer, the scratch — which is the number admission decides on. ⓘ It over-states this caller by the snapshot term: the fused call sizes with `snapshot = true` because the main commit needs the pre-NTT column-major copy for the LogUp fingerprint kernel, and an artifact commit has no such reader. That is `padded_rows · width · 8` of head-room, not a leak, and narrowing it means a `snapshot` parameter on the shared entry point. `LFM_DEVICE_ARTIFACTS=0` forces the host pass and is the A/B control. ⛔ NOT MEASURED, AND NOT MEASURABLE HERE. This machine has no CUDA, so the device path has never executed: what is verified is a `--features cuda` compile of `stark` and `prover` (lib and tests), a non-cuda compile, and the host-path gates — 9/9 including the six `registry_drift_*` pins, which still exercise the HOST branch because that is the branch this build takes. ⇒ The roots gate has to run on the box, against a cuda build, BEFORE any timing is claimed: `registry_drift_*` rebuilds every registered program's artifacts and compares roots, heights and `program_id` against blessed constants, so a device leaf convention that differed fails there immediately. If it passes, the pre-registered band is per-node `build_artifacts` 15.2 → 5–9 s and per wrap 9.8 → 3–5 s, with under 30% off `build_artifacts` counting as the hypothesis failing.
`make lint` caught what `cargo check -p stark --features cuda --lib` could not: the `what` parameter added one commit ago has a second caller in the cuda-gated admission box test, and it takes the function past clippy's seven-argument bound. ⚠ The lesson is the check, not the fix. `--lib` does not build test targets, and the cuda test module only exists under that feature, so the two arms I ran — non-cuda lib+tests and cuda lib — between them never compiled the one file that broke. `cargo clippy -p stark --features cuda --all-targets` is what would have, and it is what `make lint` runs. The test gets a `what` of its own rather than inheriting the main commit's, so an abort from the admission box says where it came from. The `allow` matches the split-trees call beside it, which carries the same one for the same reason.
…sked for
O1 sends the preprocessed commits to the card, and "what did that cost the
device" should not be a question anyone has to go and ask. The per-level line
already exists and is where a box run is read, so the number goes there:
level 0: 19 proofs, 19 distinct programs, artifacts 4.5s · device set 2.31 GiB (N/N …)
⛔ It is what the build ASKED FOR, not a sampler reading, and the distinction is
the whole value of it. The figure is `stark::device_set`'s own term-by-term
accounting — one LDE buffer, the trace-domain snapshot, one full Merkle node
buffer, the scratch — which is the number `admit_commit` decides on. So a run
that was DECLINED and fell back to the host is explained by this line, where a
sampler would only show the card idle. What the process actually held is the
sampler's answer, and the two are worth reading together.
A process maximum rather than the level's own: the commits are sequential and
the card is released between them, so the largest single set is what the build
ever needed.
Zero on a host build — every non-cuda build, and any cuda build where admission
declined every group — and the line then omits it entirely rather than printing
"0.00 GiB", so a host run reads exactly as it did before.
…the gate that does Asked whether the green `registry_drift` run under `--features cuda` exercised the device branch at all, or compared a host root with a host root. The answer is neither, exactly, and the measurement is now in the tree. THE DECISION, as written: `gpu_lde` admits on `lde_size = padded_rows · blowup >= 2^14` — a ROW count, not bytes and not columns (`DEFAULT_GPU_LDE_THRESHOLD`, and the note beside it explains that a cells floor would degenerate at FRI's width-1 re-derivation). Below it the commit falls back to the host. ✓ MEASURED over the registered fixtures, at both blowup 2 (what the drift tests use) and blowup 4, printed by `the_fixture_groups_against_the_device_floor`: EXACTLY ONE group per fixture clears the floor, and it is the same group in all six — slot 10, `LFM_RANGE`, 65,536 rows × 1 column, which is program-INDEPENDENT. Every program-dependent group is far below it; the largest is `statement_replay`'s slot 1 at 4,096 rows (lde 8,192 at blowup 2). Most are at the 4-row pad floor. ⇒ So the gate DID run the device path and its root DID match a blessed constant — but it is ONE device observation repeated six times, at the narrowest shape the machine has, on a group no program can change. It is evidence, and it is nowhere near coverage: no program-dependent group, no realistic width, has been committed on a device and checked. THE GATE THAT DOES REACH IT: `the_device_commit_matches_the_host_commit_above_the_floor` commits a group ABOVE the floor both ways and compares roots, at the production width extremes — 1 (`LFM_RANGE`), 20 (`LFM_BLAKE3`), 134 (`LFM_BITDEC`, the widest prep group there is). It asserts its own premise first, so a shape that silently fell below the floor fails loudly instead of passing as a host-host tautology. ⛔ It is `#[cfg(feature = "cuda")]`. Without that feature both sides ARE the host pass and the test cannot fail — and a check that cannot fail is worse than no check, because it reads like coverage. It exists only where it bites. Values are position-dependent (a multiply-xor of the flat index) so a transposed or mis-strided read cannot land on the same root by symmetry.
O1's first box number was a wrap saving of 9.7 s against a pre-change artifact
build of 9.8 s — the whole phase, not the 3-5 s residual that was pre-registered.
A saving that large is only explicable if almost every committed group left the
host, and nothing in the run said how many did.
`gpu_lde` admits on `padded_rows · blowup >= 2^14`, so a program's SHORT groups
stay on the host whatever the card is doing. Without the split, "the artifact
build got faster" cannot distinguish "the big groups moved and the small ones
stayed" from "everything moved", and the two imply different residual host time
— which is exactly the quantity in question.
The level line now carries it:
level 0: 19 proofs, 19 distinct programs, artifacts 0.1s · device set 2.31 GiB · groups 7/11 on device
⇒ A reader can now check the saving against the shapes instead of inferring it.
Process totals, like the peak, because the floor is a process constant and the
groups repeat per proof.
A gate that commits on the host and compares a host root with a host root is green and evidence of nothing. That is not hypothetical — it is what the six `registry_drift_*` pins nearly are: ✓ MEASURED, exactly ONE of their eleven groups clears `gpu_lde`'s `padded_rows · blowup >= 2^14` floor, and it is `LFM_RANGE` at 65,536 × 1, program-INDEPENDENT and identical in all six. `the_block_root_proves_over_real_children` is the opposite case: its groups are program-dependent and tall. ✓ VERIFIED that the mapping from a chip's trace height to its group height is the identity — `chip_trace` opens `rows = group.padded_rows` and copies the group into the first `group.width` columns of each row (`prover/src/lfm/trace.rs:100,183`), which is also why the AIR's declared precomputed root IS the artifact root. ⇒ So under cuda this gate CAN assert what it exercises, and now does. The message names the two things that would make it fire — a fixture that shrank below the floor, or `LFM_DEVICE_ARTIFACTS=0` left set — because a bare "0 device groups" would send the reader hunting. `#[cfg(feature = "cuda")]`: on a host build the count is legitimately zero and the assert would be a false alarm. ⚠ This pins the device path in the tree, but it is a 44-minute box run. `the_device_commit_matches_the_host_commit_above_the_floor` pins the same claim at production widths in seconds, and is the gate to run first.
…he closure's output half has a subject `epoch_tests::the_closure_rejects_a_moved_index_or_output` has been failing on its own anti-vacuity guard — "the fixture epoch must actually commit output, or this proves nothing" — since `c150dbc8` re-measured the fixture's epoch size on 2026-08-15. The guard was right and the test was never the problem, so this moves the FIXTURE and leaves every assertion alone. The shape it was stuck in is structural, not a mis-tuned constant. `EpochFront::build` asserts `!is_final`: it harvests an INTERMEDIATE epoch on purpose. `bench_vs/lambda/fibonacci` commits once, immediately before `halt()`. Those two together put the public output in an epoch that harness cannot reach, at EVERY epoch size — the run is 15 cycles with the commit at 11, so 8-cycle epochs leave the commit in epoch 1 (final) and 16-cycle ones swallow the whole run into a single final epoch. The test passed originally only because the then-current ELF ran a little over 16 cycles and the commit fell one cycle inside epoch 0. A private input does not rescue it either: the commit stays at the end, wherever the end is. So the guest has to commit and then keep going, and `fibonacci` cannot be that guest. `bench_vs/run.sh` builds it as the Lambda VM arm of a cross-prover benchmark against `bench_vs/sp1/fibonacci`; a tail loop that one arm runs and the other does not stops the two measuring the same program. `continuation-fixture` is its sibling plus a bounded tail, added to `RECURSION_GUESTS` and named by `FIXTURE_INNER_ELF`. Measured by counting logs under `Executor::resume_with_limit`: the commit lands at cycle 13 and the run is 48 cycles, one tail step costing two (10 steps gave 36, 16 gave 48). `FIXTURE_EPOCH_LOG2` moves 3 -> 5, putting the boundary at 32 with three margins — 19 cycles commit-to-boundary, 16 boundary-to-halt, 16 halt-to-64 — so epoch 0 carries the output, epoch 0 is intermediate, and there are exactly two epochs. Ten steps would also "work", with four cycles to spare; that is the state this change exists to get out of, since the old constant was a four-cycle question and the answer moved under it when the toolchain rebuilt the ELF shorter. ★ And the epoch COUNT did not move when that happened, which is why `continuation_fixture_generates_two_epochs` never rang. The count is necessary and was never sufficient — a run can split in two with its commit on either side of the boundary. `proof_fixture::tests::the_fixture_guest_commits_in_an_intermediate_epoch` asserts all three margins in the currency the guest's `TAIL_STEPS` is denominated in, so the property is checked rather than recorded in a comment. ⚠ The tail's arithmetic is more fibonacci rather than anything with a constant in it, and that is not a style choice — it cost a red test to learn. `recursion::precomputed_commitments` lists every ELF page whose `init_values.is_some()`, a pure function of the BINARY and not of the run, and `program_id_matches_production_on_the_real_fixture` asserts the fixture carries none. A 64-bit LCG multiplier is not materialisable inline on rv64, so LLVM spills it to a constant pool and the guest grows a `.rodata` section `fibonacci` does not have. Wrapping adds of values already in registers keep the section table identical to `fibonacci`'s: `.text` and nothing else, verified with `llvm-readelf`. The volatile store stays, because the sink is never read back and anything weaker is dead code the optimiser may delete — deleting it would silently restore the shape this guest exists to avoid. It targets a stack local, which is not an ELF page and so not in that accounting. ⚠ For the next reader: the blob cache keys on the ELF NAME and the epoch size, not on the ELF's contents, so editing the guest source and rebuilding leaves the stale blob in place and the page assert keeps failing against it. Delete `$TMPDIR/lfm-r1f-continuation-fixture-*` when the guest changes. Blob size at the new shape: 596,828 bytes, against 947,340 recorded for the old one. Epoch 0 now proves in ~25s rather than ~20s, four times the cycles.
…y is ABOUT `machine_tests::transcript_replay_cell_counts` reads 0 compressions against a pinned 8. Same family as `558faa5d` and the same mover — `603c1e15` took `WrapHash::production()` to `Algebraic` — but it lands on the opposite side of the carve-out, and the difference is the whole fix. The REGISTER derivation had to follow the pin, because the root it builds has to equal one production committed under it. This program must not. It is the R1d instrument, and `WrapHash::production`'s own doc names it: the R1b/R1c/R1d instruments spell their hash directly and must keep doing so. Its script is a BYTE sponge — the table over `transcript_replay_program_source` is denominated in 32- and 136-byte segments and in which rate block each of five squeezes lands in, with one segment deliberately spanning two. None of that is a claim an algebraic sponge can be right or wrong about; there is no re-derived count for that arm, only an absence. So the program keeps its hash and the MEASUREMENT stops following the pin. `TRANSCRIPT_REPLAY_WRAP_HASH` names it once, in `programs.rs`, and the builder and the count both read it — a single source, so the two cannot drift the way they just did. `wrap_hash_rows_at` is `wrap_hash_rows` against a named hash; `wrap_hash_rows` is now that function applied to the pin, so nothing else moves. The pinned 8 is unchanged and needed no re-derivation: it was already the BLAKE3 number, re-derived when that arm arrived because a 136-byte keccak rate does not divide this script the way a 64-byte block does. What the pin had lost was only the ability to say which hash it was counting.
…ounts twelve Two reporting defects the box found, neither affecting a root. 1. THE COUNTERS WERE PROCESS-CUMULATIVE AND THE LINE READ AS PER-LEVEL. Level 0 printed `152/228`, level 1 printed `256/384` — totals, so a reader wanting level 1's own had to subtract two lines by hand. The window now snapshots the counters when it opens and reports the DELTA. The process totals stay in `commit`, where a running count against a process-constant floor is the useful thing to keep. ⚠ And the peak does NOT become per-level, because it cannot: it is an atomic maximum and a window cannot un-see one. So the line now says which scope each figure has — `groups D/T on device` is this level's, `device set <= X GiB (process max)` is not. Two scopes on one line is fine; two scopes that both look per-level is not. 2. THE FLOOR DIAGNOSTIC WALKED ELEVEN GROUPS AND THE BUILD COMMITS TWELVE. `build_artifacts_with_hasher` commits `program_groups` (10) plus `LFM_RANGE`, and THEN one group per `LFM_BLAKE3` chunk in a second loop. Slot 11 is committed whether or not the family is used — the digest binds it either way, and the registry says so at the chunk-roots comment. A walk that stopped at `range` undercounted by the chunk count, which is exactly how this lane predicted "8 of 11" for a production wrap when the box read 8 of 12. ✓ The on-device 8 was right; the miscount was the denominator, and it was mine to catch before the box did. The diagnostic now prints slot 11 with the rest: 4 rows × 20 columns for every fixture that never compresses, far under the floor. ⇒ The 12th group is `LFM_BLAKE3` chunk 0, and it is a host group in a production wrap for a reason that is verifiable rather than incidental: lane P's per-table panel lists FOURTEEN tables for a wrap and `LFM_BLAKE3` is not among them, so the chip mask dropped it; `ChipSet::for_program` sets `blake3` from `groups.blake3.real_rows > 0`, so masked means the group is empty, which pads to 4 rows and cannot clear a 2^14 lde floor at any blowup. ⓘ `blake3_chunk_group`'s doc still says "the aggregation program's group is ~1.39M rows x 20 columns". That was true when `LFM_HASH` was BLAKE3; under the RPX pin an aggregation program compresses nothing. Left alone here — it is a one-line doc fix in a file this commit has no other business in — but it is stale, and it is the sentence that would talk the next reader out of the paragraph above.
… their phases Four timers, no behaviour change and no feature gate. Together they close the block with no gap wide enough to hide a lever in. (a) `lfm_prove_with_residency` records `execute · fill · multi_prove`. The driver's TIMING line prints this function as ONE number, and the three statements inside it are three different machines — a single-threaded interpreter, a parallel trace fill, and the only one that reaches the card. Recorded in a per-thread cell rather than printed, for three reasons: this file is a production path and the module's one existing diagnostic is a `log::info!`, not a `println!`; a stage LOADED from cache did not prove, so the driver stays silent instead of reprinting the previous stage's numbers; and a per-thread cell stays attributable when sibling proofs run concurrently, which a bare print in a shared function does not. (b) The level-0 loop prints a per-wrap TIMING line. Level 0 is 49% of the block and printed ONE number for nineteen wraps, so every per-phase figure ever published for a wrap was derived by subtracting an assumed term from a level wall. It now prints the same five fields the interior node has printed all along, plus the wrap wall, so the account is closed and the residual is visible. (c) `harvest_real_epoch` separates its two halves: the complete host STARK verify of the base epoch's sub-proofs, whose only use is to refuse, from the Phase A replay and per-table forks a driver genuinely needs. Reported as one `reconstruct` figure they are indistinguishable, which is why the block's production-equivalent time has only ever been quotable as a band. (d) `real_child`'s opening assert is timed, so `harvest` reads `(verify + replay)`. Same reason: one owner is the harness, the other is the pipeline, and the sum prices a phase no real pipeline has. ⛔ Both asserts are TIMED, never skipped, and no knob skips them. An epoch nothing verified is not a faster epoch, it is a different experiment. Gated by a unit test that fails without the recording, verified by removing the recording and watching it fail: the split must be present after a prove, must cover the prove rather than a corner of it, and must be consumed exactly once.
…ever builds Step 2's prerequisite, on its own so the scheduling commit that follows changes no counting. The level window is process-global behind a `Mutex`, and membership in it was ambient: any thread calling `build_artifacts_counted` while a window was open was counted as part of that level. That already shipped a defect — at `--test-threads=2` the counting test read 5 proofs where it had made 3, and the first run that happened to serialize them passed. The fix available then was to serialize the builders. It is not available to a level that proves its siblings concurrently, because concurrent builders are the point. ⇒ Membership is now EXPLICIT. `begin_level` enrols the calling thread; a worker takes an `Enrolment` for as long as it is part of the level; `record` ignores a build from any thread that holds neither. A stray builder cannot inflate a level no matter what it builds or when — unreachable rather than unlikely, and the same guarantee covers the serial path, which is where it actually bit. `Enrolment::drop` does not use the panicking lock. It runs during unwinding when a worker panics, and a panic inside a `Drop` that is already unwinding aborts the process. A counter is not worth that. Second, `artifacts Xs` stops being a wall the moment a level runs concurrently: two overlapping 9 s builds sum to 18 s inside a 9 s window. Serial they are the same number, which is why this needs saying BEFORE anything runs concurrently — a figure that has been a wall for the whole campaign would quietly become something else and read as a regression. The window now keeps its own elapsed time and the level line names the sum as a sum when the two disagree. While serial the line is byte-identical to every one already in the campaign's logs, and there is a test for that too. Three gates, each verified to fail without the code it gates: an un-enrolled thread's build must not be counted; an enrolled worker's build must be; and the line must acquire the clause only when the sum exceeds its window.
…ady does The level-0 loop now calls `census_and_panel`, so each wrap prints its cells, its instruction count, the empty-machine floor and the chip panel — the lines every node has printed since the census went in. Why it is worth two lines. With only a clock, a wrap can be priced but not explained: nothing says whether it is dear because of its instruction count or because of its cells, and those point at different levers — the executor in the first case, the prover in the second. The arm at `94540566` measured a wrap's prove at 4.75 s and an arity-2 level-1 node's at 6.05 s, and the node's census is the only reason the second number can be turned into a coefficient. Level 0 is 49% of the block and was the half without one. `fan_in` is 1: a wrap consumes ONE epoch, so the panel's step line reads as "at twice this epoch size", which is the posture question actually asked of a wrap. Placed OUTSIDE the five timed fields, exactly as the node's census sits outside its TIMING line, so every field stays comparable to the arm that measured them. The cost lands in `wall`, and the residual comment now names it.
…proof Step 2's gate, on its own and inert. Nothing arms it yet, so no run changes. A proof reaches the card TWICE and neither entry can see the other. `commit_group_device_or_host` dispatches to `gpu_lde` from inside `build_artifacts`, outside `multi_prove` and so outside every `VramGate`, and its only check is `device_set::admit_bytes` — a `const fn` comparing ONE dispatch's bytes against the WHOLE card budget, with no running total. And each `multi_prove` builds a fresh `VramGate` with the full budget, keeping a total over the tables of its own prove and nothing else. Two proofs in flight can therefore ask the card for twice its budget from two directions, which is the two-VramGates condition that caused the production base aborts, one level up. So the permit is MUTUAL EXCLUSION and cannot be a byte budget: a byte-budget permit would admit a second holder because its bytes fit, against a budget the first is already spending. ⛔ TAKEN TWICE, NOT HELD ACROSS BOTH PHASES. A node runs host, build_artifacts, host, multi_prove, host — the two device phases are not adjacent. On the measured arity-2 level-1 node the executor and fill between them are 2.53 s of 7.66 s, so holding across both covers 6.33 s and floors a level at 83% of its serial wall, while releasing between them covers 3.80 s and floors it at half. Overlapping the executor IS the lever. Mutual exclusion is unaffected: at every instant at most one proof is inside a device phase. Releasing there is safe because the artifact commit keeps nothing: `try_commit_row_major` binds `(tree, _handle, _lde)` and returns the root, and `_handle` — the GpuLdeBase holding the device tree and buffers — drops at function exit. Two hazards are named rather than suffered. A second hold on a thread that already holds one PANICS instead of parking, because a silent park is how the census memo cost twelve minutes of a test binary at 0% CPU. And the acquire asserts that it is the only holder, so "two holders at once" fails at the instant it happens rather than being inferred afterwards from a VRAM abort. The level line reports occupancy, not just safety: acquisitions, max holders, and the held time against the level's wall — which is what says whether a level was bound by the card or by the host. ⚠ THE FIRST VERSION OF THE FALSIFIER TEST COULD NOT FAIL. It spun two workers through twenty fast acquisitions and asserted the peak was one; with the exclusion removed it still passed, because a nanosecond critical section never overlapped. The overlap is now forced: the first worker keeps the card, the second is released only once the first is inside and then times its own acquire. Verified against the same control, it now fails.
…at a time The lever. `LFM_TREE_SIBLINGS` proofs of one interior level run at once, each taking the shared card permit across each of its two device phases and releasing it between them, so one proof's LFM executor and trace fill overlap another's time on the card. Sized from the arm at `94540566`, not from a model. An arity-2 level-1 node is device 3.80 s against host 3.86 s, so a level is device-bound at two siblings and the floor is the device sum: level 1 is 36.3 s of its 75.5 s serial wall. A wrap is device 2.85 s against host 7.90 s, one to 2.8 — a different machine, which is why this is armed for the INTERIOR only and whoever extends it to level 0 has to re-derive the count rather than inherit it. ⛔ UNSET OR 1 IS THE CONTROL AND RUNS THE ORIGINAL PATH: no threads, no permit, no sampler change. An A/B whose control is the parallel code with one worker measures the scheduler against itself and hides a constant cost in both arms. The permit is likewise armed immediately before the interior levels and disarmed immediately after, so the base and the epoch wraps are untouched and a level-0 number from this binary is comparable to one from any earlier tip. ⚠ NOT `TABLE_PARALLELISM`, which is how many TABLES one prove puts on the card and is governed by that prove's own VramGate. This is how many PROOFS are in flight. The two multiply: at TABLE_PARALLELISM=4 and SIBLINGS=2 the card still sees one proof's four tables, because the permit admits one proof at a time. Scheduling is invisible to the bytes, and `in_index_order` is where that is enforced. A level's children, layouts and label runs are three parallel vectors and the level above takes contiguous subslices of each — which is what makes contiguity across sibling subtrees a consequence of the label pins rather than a check of its own. Drain them in completion order and the pins still verify, one subtree at a time, while the tree they describe is not the tree that was built. So results land in per-index slots and are drained by index. The test forces the completion order to the reverse of the index order, and a completion-order drain fails it. Three things the levels now print. Their own host peak, because the per-node figures become process-wide readings inside overlapping windows the moment siblings run together, and that peak is what the 52 GiB stop is about — the per-node line says so on itself rather than in a note. The permit's max holders, which must read 1 and is the falsifier's own evidence rather than an inference from a VRAM abort. And the permit's held time against the level wall, which is what says whether the card or the host was the wall, and therefore whether a higher sibling count would buy anything. A worker panic is re-raised on the caller's thread with its payload intact. `std::thread::scope` otherwise propagates the fixed string "a scoped thread panicked" and libtest's global hook drops a spawned thread's own message, which cost the prover eleven anonymous failures in one suite run.
…either name Two things the A/B needs that did not exist. ★ THE IDENTITY LINE. Nothing printed a node's program identity, its group heights, or its published word count — grep the driver for `program_id` or `log_heights` and there are no prints at all. So "the bytes did not move" could only be argued from walls and census shapes, neither of which binds a committed root. Each node now prints its `program_id` prefix, its per-chip log heights, its LFM_BLAKE3 chunk heights and its published word count, so a serial arm and a concurrent one are compared by diffing their IDENTITY lines and an EMPTY DIFF IS THE PROOF. `program_id` is the right fingerprint because it is what a PARENT absorbs: a digest over every group root, the chunk-root tail, the heights, the chip set and the hasher. Move any committed felt and it moves. The heights are printed beside it because when the digest does move, they say WHICH shape did, and a bare digest mismatch prices no debugging. ★ EITHER SPELLING OF THE KNOB. `LFM_TREE_K` and `LFM_TREE_SIBLINGS` name the same thing, and set to different values the run refuses. This is not indecision: a launch line naming a knob the driver does not read fails SILENTLY — the run goes serial, reports no speed-up, and the lever is filed as refuted by an arm that never armed it. Four lines removes that whole class of result. And the driver PRINTS the resolved count before it arms anything, so the log says what the run did rather than what the launcher meant. A knob that never reached the process is otherwise indistinguishable from a lever that did not work, and the second reading is the one that gets written down. The resolution is a pure function of two `Option<&str>`, so the contradiction, the empty-is-unset spelling, a non-integer and a zero count are all tested without mutating process state.
…e worker and two The level-2 A/B exposed it: the same node's `prove` field read 4.8 and 4.1 serially and 5.0 and 7.1 at two siblings. None of that is work. A queued worker's wait for the card lands inside whatever phase was running when it asked, so `prove` absorbed it and the two arms stopped being comparable — which is the one thing a scheduling A/B needs them to be. `multi_prove` is now reported NET of the wait, and the wait is its own field on both lines. The node's TIMING line says explicitly that the wait is CONTAINED in `build_artifacts` and `prove` rather than additional to them, and splits it between the two, because those are wall times and a reader cannot otherwise tell which phase queued. That also closes the level's accounting. At K workers a level spends K × wall worker-seconds, of which the permit's `held` is the card, the per-node waits are the queue, and the remainder is host work. Level 2 measured `held 13.3s of 19.5s` with no way to price the other 25.7 worker-seconds; now there is one. The counter is MONOTONE and per-thread, read-only, never cleared. A take-and-clear counter couples every reader to every other one: whoever samples first silently steals the wait from whoever samples next. Callers bracket the span they care about and subtract, which composes — the driver does it around the artifact build and `lfm_prove_with_residency` does it around `multi_prove`. Both new clauses are ABSENT when the wait is zero, so a serial line stays byte-identical to every one already in the campaign's logs and the arms diff on their numbers rather than on their shape. Gated on the waiting thread itself: the blocked worker's self-reported wait must be at least half the hold and must agree with the wait observed from outside to within 50 ms. And the prove-split coverage floor now counts the wait, without which it would start failing in the one regime it most needs to hold in.
… order The level-2 ABBA caught it: the second lever arm printed L2N1 before L2N0, because a worker prints when it FINISHES. A raw diff of those lines therefore files a scheduling order as a byte difference, which is a false red on the one gate that exists to rule byte differences in or out. Sorting both sides is a correct remedy and remains sound — each line begins with its own node label, so a permuted tree still sorts differently and the check keeps its teeth. But it is a step a reader has to remember, and the reader who forgets reports a failure that did not happen. The join already holds every child in index order and `RealChild` carries its own artifacts, so printing there costs nothing and needs no procedure. The line also now carries cells and instructions, so it subsumes the census for this purpose and ONE grep is the whole gate rather than two that must be sorted and compared separately. ⚠ For logs already produced at `7a8f3e96`, sort both sides before diffing — that commit prints on the worker.
…nstrumented ⛔ NOT PUSHED until the e2e pair reports. Written so the numbers can be read against a design rather than the other way round. Nineteen epoch wraps now prove `LFM_TREE_SIBLINGS_L0` at a time, through the same card permit and the same index-ordered join as the interior. A SECOND KNOB, defaulting to 1 rather than to the interior's value. The falsifiers are different: the interior's binding constraint is the card, level 0's is the HOST PEAK, and one knob would let a safe interior setting arm the risky level — discovered by exhausting 57.53 GiB two hundred seconds in. They are also different machines: measured, a level-1 node is device 3.80 s against host 3.86, one to one, while a wrap is 2.85 against 7.90, one to 2.8. The count that saturates one starves the other. And unset, level 0 runs exactly as it did, so every existing e2e number stays comparable. Deliberately not a list on the existing knob: that spelling makes the common case need punctuation and lets a typo arm level 0 silently, which is the one thing this must never do. THREE LINES THAT DID NOT EXIST, and the first is why this commit is more than a scheduler. Per-wrap host peak. The count is chosen on what a second live wrap transient costs, and nothing measured it. The interior prints a per-node peak and that is how its retention per node was read; level 0 printed none, so the figure could only be scaled from a node, which is a different machine. The serial arm now measures it directly. The level's own host peak, which is the figure the 52 GiB stop is about — the per-wrap peaks become process-wide readings inside overlapping windows the moment wraps run together, and the line says so on itself. A per-wrap IDENTITY line at the join, the same shape the interior carries, so one grep covers the whole tree and the wraps get the same byte gate the nodes have. The permit's own line prints for level 0 too, so `max holders 1` is asserted there and `held` against the level wall says whether the card or the host was the wall — which is the evidence for whether a higher count would buy anything.
…te flag out of the memory cell Two allocation changes inside `execute`. Neither changes what is executed, recorded or proved: the bytes are identical. RECORDS ARE SIZED, NOT GROWN. Ten record vectors were built by `push` doubling while the compiler already held every one of their final lengths. `ColumnGroup::real_rows` is not an upper bound on a record count — it IS the count: pass 2 opens exactly one column-group row per instruction and this executor pushes exactly one record per instruction of the same chip. The trace fill already depends on that identity, filling rows `0..real_rows` by indexing the record vector, so a short vector is a panic there today. Sizing from it is therefore a use of an invariant the code already relies on, not a new assumption. Doubling instead re-allocated and copied every vector ~log2(rows) times per proof — a few hundred MB of memcpy and ~20 large reallocations, on each concurrent worker at once. THE OCCUPANCY FLAG LEAVES THE CELL. `LfmWord` is `[F; 4]` = 32 bytes and a Goldilocks felt has no niche, so `Option<LfmWord>` is 40: the flag cost 8 bytes per address AND pushed the stride off the cache line, so a cell spanned two lines at half of all addresses. It becomes one bit per address in a separate array — `num_addrs / 8` bytes, which stays cache-resident where the value array cannot — and the value array keeps a 32-byte stride and shrinks 20%. THE WRITE-ONCE CHECKS ARE UNCHANGED, AND NOW EACH HAS A TEST. A second write is still `DoubleWrite`, a read of an unwritten address is still `ReadBeforeWrite`, and an address past the end still reports differently in the two directions. `DoubleWrite` already had a test; `ReadBeforeWrite` had none from the executor — only from the validator — and that gap matters more after this change than before it. The value array is zero-filled, so the bit is now the ONLY thing separating "never written" from "written zero", where `Option` carried that distinction inside the cell: dropping the check would hand out zeros instead of failing. Both halves are asserted — a written zero reads back as a value, an unwritten address does not — together with both out-of-range directions. Two more pins, because both of these are claims about layout that a later edit could quietly cost. `the_memory_cell_divides_the_cache_line` fixes the 32-byte stride the argument above rests on. `the_records_are_sized_from_the_census` asserts `capacity == real_rows` per chip on a fixture whose row counts are deliberately not powers of two, so push doubling overshoots and says so; the same identity is asserted for every program under `debug_assert` at the end of `execute`, where the emitter and the executor arm are written.
…hase `lfm_prove_with_residency` held the whole `LfmExecution` — the final write-once memory and all ten record vectors — to the end of its scope, so both stayed live across the fill AND the whole `multi_prove` card phase. On a wrap that is a few hundred MB of memory plus a few hundred MB of records kept for nothing, on every concurrent sibling at once. `memory` has no consumer on the proving path at all: it is a diagnostic surface the tests read. `records` are consumed by the fill and dead the moment it returns — the traces it produced are the live set from there on. So `execute`'s result is destructured, `memory` dropped straight after it, and `records` dropped straight after the fill. TIME-NEUTRAL BY CONSTRUCTION. Both drops sit AFTER the `elapsed()` read of the phase they follow, so `execute` and `fill` keep measuring exactly what they measured before and stay comparable across this change; only the wall absorbs the free, which is a handful of `munmap`s. The value is not the clock. It is the host PEAK, which is the quantity that fenced a third concurrent interior sibling: interior 3 measured 54.36 GiB on the 120 GiB host, past the 52 GiB stop on the 57.5 GiB one. This is a straight subtraction from every live proof's footprint through the phase where the peak is taken.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft: the per-table GPU recursion, end to end — block 25368371 compressed into one root proof, and three optimization passes.
What this is
The full per-table pipeline on the GPU: the epoch base proofs, the epoch wraps, the interior aggregation tree, the block-wide memory argument (as slices and a parent), and the block-artifact root. Every stage is proved on the card; the root is proved and verified. This branch is for sharing the work — not for merging yet.
Block 25368371, 19 epochs at 2^21 rows, fan-in 2 → 19 wraps, 21 interior nodes in 5 levels, 2 global slices, their parent, one root.
Times
Ryzen 9 9950X + RTX 5090,
TABLE_PARALLELISM=4, one arm per process, nodes within a level proved serially. "Before" is the first end-to-end of the pipeline; "pass 1" (8a59fa1d) and "pass 2" (4fcb3341) are the tips of the first two optimization passes; "pass 3" is this branch's tip — each measured end to end on the same box from a fresh cache, every stage proved.The record was reproduced within 0.1% on a second fresh-cache run (252.5 s), and the executor housekeeping at this branch's tip reads 251.6 s with the level-1 host peak at 46.6 GiB.
On a Ryzen 7950X + RTX 5090 (16 cores, 120 GiB host) the same commit runs in 9.3 min serial, 6.3 min at two wrap and two interior siblings, and 5.4 min at four wrap and three interior siblings — the third interior sibling peaks at 54.4 GiB of host memory, above the 9950X box's 52 GiB stop, so it is a 120 GiB configuration. Device peaks and host peaks are the same on both hosts to within 1%, wall times are not — memory bands transfer across hosts, time bands never do. Recursion overhead — everything after the base proofs — is now ≈ 2.7× the base time (was 11× after pass 1, 5.2× after pass 2). The harness re-verifies every child and every proof it makes as a test precondition; measured in the serial run that is ≈ 66 s of host work (2.6 s per wrap, 0.7 s per node), and under concurrency it overlaps other work, so no production-equivalent subtraction is made for pass 3.
Where the time went, measured phase by phase before anything was changed (the profile is in the campaign's state file): the recursion was host-CPU-bound — the GPU read 0% in 91% of samples through the wraps — and the largest single phase was the preprocessed-column commit (
build_artifacts, an LDE + Merkle pass on the host, 43% of the block), followed by LFM program execution + trace fill (15%), the per-epoch reconstruction in the harvest (9%), and the STARK prover itself at 13% running at a healthy 57% device utilization.What changed in pass 1
prover/src/lfm/trace.rs): the per-chip row loop walkspar_chunks_muton rayon's global pool; every fill closure was read and is row-local; a cell-for-cell identity test against the serial reference covers all chips under RPX and BLAKE3 dispatch. 6.5× on the hash chip on an 11-thread laptop; on the box the per-node prove component fell 13.6 → 9.7 s with the artifact phase unchanged.prover/src/lfm/commit.rs):lde_columnsruns an explicitpar_iterover columns with interpolate→expand fused (one fewer copy of each group's coefficients); the group loop is windowed (LFM_ARTIFACT_GROUPS_IN_FLIGHT, default 4) with the memory reasoning kept. Roots are pinned byte-identical to the serial build by theregistry_drift_*tests. Per node:build_artifacts21.9 → 15.2 s.603c1e15) made byte-hash counts structurally zero; the register-derivation instrument now follows the block pin in all three places; the FRI-leg byteswap counts carry a hash width.crypto/math-cuda/kernels/rpx.cu,crypto/stark/src/grinding.rs): the 2^20-trial search ran on the host per table because the device arm accepted only Keccak — about two-thirds of each base epoch's CPU time (RPX costs 2,368 ns per permutation on the host) and ~1.4 s of every recursion proof. An RPX kernel loops the existing device permutation over a nonce range and returns the smallest valid nonce (atomicMin, deterministic), dispatched by the configuration's commitment hash; pinned by a no-GPU known-answer layer replaying the kernel againststark::grinding::is_valid_nonce(four kernel mutations each red) and three device gates, one of which asserts the dispatch actually reached the device. Same factor, same predicate — no security change. Base 156 → 68 s. This cost is specific to the RPX pin;maingrinds a Keccak-class digest and is unaffected.What changed in pass 2
prover/src/lfm/commit.rs,crypto/stark): the per-proof artifact build — coset LDE, leaf hashing and Merkle tree for every preprocessed column group of an LFM program — ran on the host, and after the RPX pin its Merkle half was RPX permutations on ~26 cores (56% of the phase). A named public entry point instark(try_commit_row_major) exposes the device's fused LDE + leaf-hash + Merkle for one row-major group, which is the layoutColumnGroupalready holds, so the host's strided transpose is skipped too; the host pass remains the fallback below the device floor (padded_rows × blowup ≥ 2^14, a row count) and underLFM_DEVICE_ARTIFACTS=0. Per proof the phase went 14.4 → 0.4 s on interior nodes and 9.8 → 0.3 s on wraps, withproveandharvestunchanged (5.9 s and 0.7 s per node before and after). Device peaks did not move: the artifact commit runs while the card is otherwise empty, and the device tree is freed beforemulti_provebuilds its own.registry_drift_*root pins (which reach the device exactly once per fixture, on the one program-independent group above the floor — evidence, not coverage), adevice_paritytest that commits a group above the floor both ways and compares roots at the production width extremes (1, 20 and 134 columns) after asserting its own premise, and the fixture-scale root test, which undercudanow refuses to pass if every group fell back to the host. The census line reports how many groups took the device path per level (groups D/T on device; a production wrap prints 8 of 12, a level-1 node 8 of 12) and the device set the build asked the card for. On every production proofmulti_proverebuilds the precomputed tree on the device and refuses on a root mismatch — the strongest witness, and it stayed silent on all 44 proofs of the record run.LFM_DEVICE_ARTIFACTS=0as the control): wraps 388.9 s host vs 206.2 s device; level 1 215.7 s host vs 75.5 s device.prover/src/lfm/proof_fixture.rs,bench_vs/lambda/continuation-fixture): the closure test's fixture guest committed at the very end of its run, so the "output half" of the check had no subject — a sibling fixture guest commits in an intermediate epoch and then does bounded work, and the fixture asserts its commit-to-boundary, boundary-to-halt and halt-to-end margins in the guest's own step currency (the epoch count never moved when this broke, so the two-epoch canary never rang). The R1d transcript-replay instrument is a byte sponge that names its hash directly, per the hash-pin carve-out; its count now reads the same named constant as its builder.What changed in pass 3
prover/src/lfm/per_table_aggregator_tests.rsdriver,prover/src/lfm/commit.rs,prover/src/lfm/proof.rs): after pass 2 the top of the block was four sequential host walks per proof (LFM program execution, epoch reconstruction, program emission, harvest — none of them parallel) with the device prover in between; the driver proved siblings one at a time. It now proves K siblings of a level at once, with a single mutual-exclusion permit taken around each proof's two device phases (the artifact commit andmulti_prove) and released between them, so one proof's host walks overlap the other's card time while the card never holds two proofs (the two-VramGates trap, closed at the callers by Fix A, is not reopened one level up: neither admission path keeps a cross-proof total, so the permit is exclusion, not a byte budget). K is a per-level knob (LFM_TREE_SIBLINGSfor the interior,LFM_TREE_SIBLINGS_L0for the wraps, both default 1 = the serial control); the census window enrols workers explicitly so a stray builder cannot inflate a level; the level line reports acquisitions, max holders, and the card's held share; each node prints its program identity (the digest a parent absorbs), heights and published words on one line, so byte identity between schedules is adiff.K_min = ceil(1 + host/device)— and it reproduces the measured card share at both interior levels (75% and 68% at K=2); a wrap wants four workers on time grounds and the host peak decides how many it gets.prover/src/lfm/executor.rs,proof.rs): the executor's record vectors are sized from the census the compiler already holds (one record per instruction per chip, exact), the write-once memory cell drops from 40 to 32 bytes with a bit-per-address written map (a read-before-write test now exists on the executor, not only the validator), and the executor's memory and records are freed before the card phase. Byte-identical (the identity lines diff clean); the executor is 3% faster per wrap and the level-1 host peak, the number that bounds a third interior sibling, falls from 48.2 to 46.6 GiB. The executor itself is 83% software RPX permutations (one full permutation per hash instruction, 644,250 per wrap at 2,356 ns each on the 9950X), so it is not a lever for layout work; the levers left are running those permutations on the parallel side or making one permutation faster, both being priced before any code.execute · fill · multi_prove(recorded in a per-thread cell, printed by the driver), every wrap prints its own TIMING line and census (level 0 printed one number for nineteen wraps), the harness-only verification is timed rather than banded, and the permit wait is its own field. On an arity-2 level-1 node: executor 2.25 s, fill 0.27 s, device prover 3.4 s.The root
LFM_HASHheightroot_schema_words(67, 40, AssertOnly)A is the default: 7% more root cells than B, but it retires the top node (one proof fewer, one level less latency). The option is an input (
LFM_TREE_ROOT_OPTION=A|B, refused when unset), not a ruling.Gates
At the arm's commit, in a box
--librun: 27 unit gates (the parent's 12 — z/α agreement, L2G-root agreement and republish, partials summing to zero, partition tiling, gap / overlap / stop-short, slice count both ways — and the root's 15, including the five pre-registered tamper arms), the honest control (two real slices and their parent, summed to zero), and the fixture-scale root proved over real children under both options. Mutation-tested: each tamper arm fires on exactly the check it names. The trace-fill identity test and the sixregistry_drift_*root pins gate pass 1's changes; pass 2 adds thedevice_paritygate and the fixture root test's device assertion (bothcuda-only, because without a card both sides are the host pass and the check could not fail).Caveats, by design
recursion::check_attestationbinds the proof to the block host-side, against an ELF the consumer trusts; the guest uses the supplied roots verbatim. "One proof for this block" terminates there.Running it
LFM_TREE_LEVELSproves or loads the interior levels; the global stage and the parent have their ownprove|loadmodes; Prove refuses to overwrite a cached entry. Knobs:LFM_TREE_SIBLINGS=KandLFM_TREE_SIBLINGS_L0=Kprove K siblings at once in the interior / at level 0 (default 1, the serial control; pass 3's record runs both at 2);LFM_DEVICE_ARTIFACTS=0forces the host artifact build (pass 2's control);LFM_ARTIFACT_PARALLEL=0reproduces the pre-pass-1 host build exactly;LFM_ARTIFACT_GROUPS_IN_FLIGHT=Nbounds host residency.Not in this branch
The VRAM admission/scheduler decoupling and the barrier levers (
pt/barrier-levers) are separate; 2^22 needs the epoch wrap sliced the same way and is not attempted here. Next levers, sized at this tip: a third sibling where the host peak allows it (level 1 is the binding level at 47.9 GiB with two), the sequential LFM executor (≈20% of the block, single-threaded), and running the two boxes as one tree. Mixed fan-in is worth ≈ −30 s, not the −130 s once estimated: emission, commit and prove are linear in legs; only the flat per-proof harvest is saved on a removed node.