From 8cedf2e2593bd83818e12aeb104d902465dc1bc5 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 14:40:48 -0300 Subject: [PATCH 1/8] fix(lfm,tests): the pins the main-sync port left behind, each against its mover MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The lineage's first PR CI (run 35533170457, PR #999) turned up four red prover tests. All four are pre-existing at the base c00342c1f, all four have ONE mover, and hypothesis B — a posture or env dependence, the campaign's LAMBDA_VM_MAX_ROWS_LOG2=21 or LAMBDA_VM_WHIR_HASH=rpx — is ruled out for every one of them: the registry path reads no env (REGISTRY_HASHER is a const and `build_artifacts` passes it explicitly), and the one knob that IS read, `max_rows_log2_override`, points the other way, since CI's bare env uses the LARGER production caps. THE MOVER is `FIXED_TABLE_COUNT` 11 -> 5, which arrived with 892c7d1bc (main's c2ac5d546, #977). COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT stopped being always-on and became `TableCounts` fields — a run that never reaches one carries no sub-proof for it. That has two arms, and every red pin sits on one: (i) THE TABLE SET SHRANK. `air_trace_pairs` pushes only BITWISE, DECODE, KECCAK_RC and REGISTER unconditionally; everything else comes from a `Vec` that is empty when the count is zero. (ii) THE STATEMENT ENCODING GREW 49 BYTES. The six counts joined the absorbed epoch statement and #977 bound `is_final` into it as the last byte: `NUM_TABLE_COUNTS` 15 -> 21 and a trailing `+ 1` on `EpochStatementShape::byte_len`. Recomputed from the code rather than from the prose, with a 30-byte CONTINUATION_EPOCH_TAG: 30+32+8+8*15+8+1+8+8 = 215, and 30+32+8+8*21+8+1+8+8+1 = 264. Each re-blessed assertion names 892c7d1bc and its arm, so the next reader can trace it without the thread this came from. None of these is a regression. Each pin caught a deliberate production change that was ported without re-running it, which is the pin working. The port DID update everything that fails to COMPILE — algebraic_transcript's `[u64; NUM_TABLE_COUNTS]` literal, logup_tests' `[...; FIXED_TABLE_COUNT - 1]` census, whir_statement_tests, statement_replay's own derivation and module doc — and missed every pin that fails only at runtime. These test files exist on no other branch and the lineage had no PR CI until #999, so nothing ever ran them against #977. Confirmed independently: the four names appear in none of the box gate logs either, and every earlier box `cargo test -p lambda-vm-prover` run was a filtered `--exact` run of a single unrelated test. LFM_REGISTRY, regenerated. StatementReplayV0 is the one registered program that replays the epoch statement, so arm (ii) moved its script by one Blake3Chain compression and seven of its fifteen roots with `program_id`. Regenerated with `compute_lfm_registry`; `compute_static_commitments` was not re-run and did not need to be, this being no hash-pin change. EXACTLY ONE ENTRY MOVED, checked rather than assumed: the other five programs build no epoch statement, and every root, log-height, `keccak_rnd_chunks`, `hasher` and `chip_set` of each came back byte-identical — slots 13 and 14, the statics, included. `log_heights[11]` did not move even for StatementReplayV0, 9 and 10 compressions both padding to the 16-row group. And the regenerated `roots[11]` equals the value the pin computes from the program (`7a 3b 86 1b ...`), which is what says the paste closes the gap the pin found instead of moving the pin to meet the paste. The runtime pins: - blake3_chip_tests, arm (ii): STATEMENT_REPLAY_BLAKE3_ROWS 9 -> 10. 49 bytes is under one 64-byte Blake3Chain block, so it is worth exactly one more compression. TRANSCRIPT_REPLAY_BLAKE3_ROWS stays 8 — TranscriptReplayV0 replays no statement, and that is what keeps the two an oracle rather than two literals: a change that moved BOTH would not be this one. - epoch_verify_tests, arm (i): SUB_PROOFS 25 -> 16, CHALLENGES_AT_MIN_PRESET 115 -> 79. Six of the nine that left are the accelerators; the pre-#977 25 was 14 split families + 10 intermediate fixed + 1 L2G_MEMORY, and the fixed term is now 4, which lands at 19. The remaining three are split families this fixture leaves empty and are NOT named, because the measurement does not name them. 79 falls out twice: from the stated model, 111 + 4*(16-24); and from the loop's own counter, 2 + 16*4 + 13, the 13 zetas being 115 - 2 - 25*4. The `checked` assertion is the real oracle and fails if the four-challenge model stops describing the move. The accounting identity had to be respelled, not just re-blessed. SUB_PROOFS is now BELOW the 24 it is measured against, and `SUB_PROOFS - 24` on a usize is an underflow rather than a failed assertion. Both sides are positive now, so it still fails in either direction. - machine_tests, arm (ii): `epoch_statement_cursor_is_three_plus_output_len` was never red on CI because nextest cancelled its shard first, and it is red — 215 + L + 16R against an actual 264 + L + 16R, 261 versus 310 at the acceptance shape. Renamed to `..._is_the_output_len_alone`: the constant term's own shift is gone, so Phase A inherits `L mod 4` where it inherited `(3 + L) mod 4`. The rider asking for a one-byte pad at the end of the statement encoding got it from #977 without anyone aiming there, tag bump included, and is marked resolved. - constraint_artifact_tests, arm (i): `continuation_epoch_constraint_leg` asserted `fixed_final.len() == FIXED_TABLE_COUNT`, i.e. 11 == 5. Also never reached by CI. The list splits into `always_on` (five, the census target) and `accelerators` (six), which stay in the COST sum because that sum is the figure a recursion budget has to clear. So (25, 26) survives, as a CEILING rather than as the composition — 19/20 is the accelerator-free floor. Swept by VALUE and not only by test name — 215/264, 261/310, 207/223, 11/5, 15/21, 24/25/26, 79/111/115/119, the moved root and program_id prefixes, and the spelled-out counts — across prover/ and crypto/, tests and non-tests. Two hits beyond the six were pins in substance: - SOUNDNESS.md's `T = 24`. Two corrections, and the bound survives both. `T` is now smaller (16 on the fibonacci fixture), and since `E = 4 + sum_t (3 + L_t)` is increasing in `T` and `P <= 3E * 2^-32` in `E`, a smaller `T` only lowers `P`: the quoted `P ~ 2.5e-7` stays a valid, now conservative, upper bound, and the `T ~ 60` figure that matters for a real block is untouched. The second correction is sharper: the test the paragraph cites as the measurement, `arena_filler_reads_real_committed_roots`, asserts `tables > 0` and that no root is all-zero — never a count. "Measured, not assumed" was true of the run somebody did and false of the suite, so nothing would have failed when `T` moved, and nothing did. `T` for that two-epoch continuation fixture is unmeasured since #977 and is now read against the 25/26 ceiling. - logup_tests' "all 25 sub-proofs declare interactions". Corrected without spelling a count: the loop walks `census`, so a literal there would be a second, driftable copy of a length the loop already holds. Judged NOT pins, and left alone: `FE::new(215)` (fri_tests, a polynomial coefficient); 215 squeezes (crypto's transcript_counters, a different quantity); 16,777,215 (math-cuda, 2^24-1); 261 (ecdas column index); 1,261 and 1,397 (blake3 interaction counts); 223,380 and 229,290 (continuation page census); BLOCK_MARGINAL = 111 (continuation page cost); `rejects >= 20` (machine_tests, a rejection count); `i >= 26` (blake3_socket_tests); the blake3 KAT "all ten vectors"; and every `FIXED_TABLE_COUNT`/`NUM_TABLE_KINDS` use that names the constant instead of a literal, since those adapt. Left for a measurement rather than an edit: wrap_tests' measured record table (25 sub-proofs, 210,782 instructions, 82,059,828 cells, 45,953,352 proof bytes) and epoch_verify_tests' `[pinned: see the run output]` figures. Re-blessing a measured record without a measurement is the thing the rules forbid. STILL OPEN: multilinear_table_tests' three `>= 20` table-set assertions, which want the argued set BY NAME rather than a count, and therefore one run first. --- others/lfm-migration-riders.md | 18 ++++- prover/src/lfm/SOUNDNESS.md | 26 ++++++- prover/src/lfm/blake3_chip_tests.rs | 23 +++++- prover/src/lfm/constraint_tests.rs | 35 ++++++--- prover/src/lfm/epoch_tests.rs | 3 +- prover/src/lfm/epoch_verify_tests.rs | 64 +++++++++++---- prover/src/lfm/logup_tests.rs | 19 +++-- prover/src/lfm/machine_tests.rs | 48 ++++++++---- prover/src/lfm/registry.rs | 70 +++++++++++------ prover/src/tests/constraint_artifact_tests.rs | 78 +++++++++++-------- 10 files changed, 275 insertions(+), 109 deletions(-) diff --git a/others/lfm-migration-riders.md b/others/lfm-migration-riders.md index dfb0438af..e983a2de5 100644 --- a/others/lfm-migration-riders.md +++ b/others/lfm-migration-riders.md @@ -19,11 +19,23 @@ draw counts. Acceptable — hence a rider, not a fix. ## 2. One-byte pad at the end of the statement encoding +**★ RESOLVED — the pad arrived, and nobody aimed it here.** #977 took the six +accelerator chips out of `FIXED_TABLE_COUNT` (11 → 5) and made them counted, so +the statement absorbs six more `u64` counts (`NUM_TABLE_COUNTS` 15 → 21, `+48`, +which moves no shift), and the same PR appended `is_final` as the statement's +last byte (`+1`). `215 + 49 = 264 ≡ 0 (mod 4)`. The constant term's own shift is +gone; the cursor Phase A inherits is now `L mod 4` alone, so the splice is free +whenever `L ≡ 0 (mod 4)` instead of `L ≡ 1`. The domain tag went to +`LAMBDAVM_CONTINUATION_EPOCH_V5` along the way, so the tag bump the note at the +bottom asks for was paid too. Everything below is the analysis as it stood, kept +for the arithmetic; the numbers in it are the pre-#977 encoding. + **What:** pad the continuation-epoch statement so its length is `≡ 0 (mod 4)`. -**Why:** the encoding is `207 + L + 16R` bytes (not 223 — an arithmetic slip in -the first report, now machine-checked by -`epoch_statement_cursor_is_three_plus_output_len`). Every subsequent absorb +**Why:** the encoding is `264 + L + 16R` bytes (207 when this was written, then +215 with `TableCounts::blake3`; not 223 — an arithmetic slip in the first +report, now machine-checked by +`epoch_statement_cursor_is_the_output_len_alone`). Every subsequent absorb inherits the resulting cursor — including all of Phase A, whose roots are individually 32-byte-aligned but land misaligned because they inherit the statement's cursor. (Alignment is a property of the CURSOR, not of the field: diff --git a/prover/src/lfm/SOUNDNESS.md b/prover/src/lfm/SOUNDNESS.md index 7c4b49fbf..fa314a4eb 100644 --- a/prover/src/lfm/SOUNDNESS.md +++ b/prover/src/lfm/SOUNDNESS.md @@ -193,10 +193,28 @@ is what keeps `E` small. At `T = 24` with tables at their row cap (`L_t = 12`), `3E = 1,092` base candidates and `P ≈ 2.5·10^−7`. At a larger `T ≈ 60`, `E = 904` and `P ≈ 6.3·10^−7`. -`T = 24` is **measured, not assumed**: reading a real two-epoch continuation proof -(`machine_tests::arena_filler_reads_real_committed_roots`) gives 24 sub-proofs for an -intermediate epoch and 25 for the final one, the extra being HALT. It was an honest hedge when -this section was written; it no longer needs to be. +`T = 24` was the epoch shape when this section was written: a real two-epoch continuation proof +gave 24 sub-proofs for an intermediate epoch and 25 for the final one, the extra being HALT. + +⚠ TWO CORRECTIONS, and the bound survives both. + +**`T` is now SMALLER, and the bound is monotone in `T`.** #977 (`892c7d1bc` on this lineage) took +`FIXED_TABLE_COUNT` 11 → 5 and made COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT counted, so +an epoch that never reaches one carries no sub-proof for it — `epoch_verify_tests`' +`SUB_PROOFS` measures 16 on the fibonacci fixture, down from 25. `E = 4 + Σ_t (3 + L_t)` is +increasing in `T`, and `P ≤ 3E · 2^−32` is increasing in `E`, so a smaller `T` only lowers `P`: +the `P ≈ 2.5·10^−7` quoted at `T = 24` remains a valid upper bound, now a conservative one. The +`T ≈ 60` figure is the side that matters for a real block and is untouched. + +**The cited test does not pin the number.** `machine_tests::arena_filler_reads_real_committed_roots` +asserts `tables > 0`, one main root per sub-proof, and that no root is all-zero — never a count. +So "measured, not assumed" was true of the run that was done and false of the suite: nothing +would have failed when `T` moved, and nothing did. The count that IS asserted is +`epoch_verify_tests`' `SUB_PROOFS`, on a different fixture (`epoch_tests::real_epoch`) than the +two-epoch continuation this paragraph describes. `T` for THAT fixture is unmeasured since #977; +it is bounded above by the 25/26 ceiling in +`tests::constraint_artifact_tests::continuation_epoch_constraint_leg`, which is what the bound +above should be read against until someone runs it. **State it as `< 10^−6` per proof at production shapes**, growing by `≈ 1.05·10^−8` per additional table — each table contributes `3 + L_t ≈ 15` extension draws, so the per-table increment is 15× diff --git a/prover/src/lfm/blake3_chip_tests.rs b/prover/src/lfm/blake3_chip_tests.rs index c263f5249..76e7007e7 100644 --- a/prover/src/lfm/blake3_chip_tests.rs +++ b/prover/src/lfm/blake3_chip_tests.rs @@ -1215,8 +1215,29 @@ fn the_flip_inventory_of_registered_programs_is_pinned() { /// takes a 64-byte block where the keccak sponge takes a 136-byte rate, so /// the same message divides into more compressions — which is the in-machine /// half of the cost the campaign priced, visible here as a row count. + /// + /// ★ StatementReplayV0 moved 9 → 10 on the main-sync port, and the mover is + /// NAMED rather than absorbed. + /// + /// MOVER: `892c7d1bc` (main's `c2ac5d546`, #977) — arm (ii), the STATEMENT + /// ENCODING. That merge's two arms are (i) the table set shrank, empty + /// tables now being elided rather than padded, and (ii) the absorbed epoch + /// statement grew. This pin is on (ii); `epoch_verify_tests`' SUB_PROOFS is + /// on (i). + /// + /// #977 took the six accelerator chips out of + /// `FIXED_TABLE_COUNT` (11 → 5) and made them counted, so the epoch + /// statement absorbs six more `u64` counts, and the same PR appended + /// `is_final` as the statement's last byte. `NUM_TABLE_COUNTS` went 15 → 21 + /// and `EpochStatementShape::byte_len` gained a trailing `+ 1`: the + /// statement is **+49 bytes**, which is under one 64-byte `Blake3Chain` + /// block and therefore worth exactly one more compression. + /// + /// TranscriptReplayV0 stays at 8, and that is what keeps this a pair rather + /// than two literals: it replays no statement, so a change that moved BOTH + /// counts would not be this one and would have to name itself. const TRANSCRIPT_REPLAY_BLAKE3_ROWS: usize = 8; - const STATEMENT_REPLAY_BLAKE3_ROWS: usize = 9; + const STATEMENT_REPLAY_BLAKE3_ROWS: usize = 10; use super::instr::Instr; use super::programs::{ diff --git a/prover/src/lfm/constraint_tests.rs b/prover/src/lfm/constraint_tests.rs index c283cea24..c19f43349 100644 --- a/prover/src/lfm/constraint_tests.rs +++ b/prover/src/lfm/constraint_tests.rs @@ -1477,10 +1477,19 @@ fn quotient_rows(artifact: &ConstraintArtifact, log2_trace_length: u32) -> usize /// /// The composition is `others/lfm-constraint-lowering-design.md` §8.2.2's, which /// `tests::constraint_artifact_tests::continuation_epoch_constraint_leg` derives -/// from the real epoch shape and pins against a measured 24/25 sub-proof count: -/// 14 split-table families at one chunk each, plus the nine fixed tables an -/// intermediate epoch carries (all ten on the final one), plus one L2G_MEMORY. -/// PAGE does not appear — epochs pass `page_configs = &[]`. +/// from the real epoch shape and pins against a measured 25/26 sub-proof +/// CEILING: 14 split-table families at one chunk each, plus the nine +/// always-on-or-accelerator tables an intermediate epoch can carry (all ten on +/// the final one), plus one L2G_MEMORY. PAGE does not appear — epochs pass +/// `page_configs = &[]`. +/// +/// ⚠ THE FIXED TERM IS A CEILING SINCE #977, not a floor. That PR took +/// `FIXED_TABLE_COUNT` 11 → 5, moving COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS +/// and HINT into `TableCounts` — a run that never reaches one carries no +/// sub-proof for it. So the sums below are what a workload that calls every +/// accelerator pays, which is the right figure for a budget and the wrong one +/// for a specific epoch: `epoch_verify_tests` measures 16 on the fibonacci +/// fixture, which reaches none of the six. /// /// ### What this instrument cannot see /// @@ -1499,8 +1508,16 @@ fn continuation_epoch_constraint_leg_cost() { "CPU", "LT", "SHIFT", "EQ", "BYTEWISE", "STORE", "CPU32", "MEMW", "MEMW_A", "MEMW_R", "LOAD", "MUL", "DVRM", "BRANCH", ]; - /// `FIXED_TABLE_COUNT`'s ten, which contribute exactly one sub-proof each - /// regardless of `TableCounts`. HALT is last: an intermediate epoch drops it. + /// The ten an epoch can carry outside the split families: `FIXED_TABLE_COUNT`'s + /// five (BITWISE, DECODE, KECCAK_RC, REGISTER, HALT), which contribute one + /// sub-proof each regardless of `TableCounts`, plus five of the six + /// accelerators #977 moved into `TableCounts`. HALT is last: an intermediate + /// epoch drops it. + /// + /// ⚠ HINT is the sixth accelerator and is absent from this list, which is + /// why the enumeration is ten where the pre-#977 constant said eleven. The + /// omission is inherited, not deliberate, and it makes these sums a LOWER + /// bound on the accelerator-inclusive ceiling. const FIXED: &[&str] = &[ "BITWISE", "DECODE", @@ -1554,16 +1571,16 @@ fn continuation_epoch_constraint_leg_cost() { let design_intermediate = families_unfused + fixed_unfused + l2g_unfused; println!( - "\ncontinuation epoch, constraint leg (minimum shape, 25 sub-proofs)\n\ + "\ncontinuation epoch, constraint leg (minimum shape, 25-sub-proof ceiling)\n\ \x20 14 split families {families:>7} (unfused {families_unfused})\n\ \x20 9 fixed, no HALT {fixed_no_halt:>7} (unfused {fixed_unfused})\n\ \x20 1 L2G_MEMORY {l2g:>7} (unfused {l2g_unfused})\n\ \x20 INTERMEDIATE leg {intermediate:>7} vs the design's {design_intermediate}\n\ \x20 + recombination @ log2(N) = {LOG2_TRACE_LENGTH} {recombination:>7} \ (zerofier, beta-fold, one division, claimed-parts Horner, assert)\n\ - \x20 INTERMEDIATE total {:>7} over 25 sub-proofs\n\ + \x20 INTERMEDIATE total {:>7} over <=25 sub-proofs\n\ \x20 FINAL epoch (+HALT) {final_leg:>7} leg, {final_total} total, \ - over 25 sub-proofs", + over <=26 sub-proofs", intermediate + recombination ); diff --git a/prover/src/lfm/epoch_tests.rs b/prover/src/lfm/epoch_tests.rs index fcf63bb5e..18e0fca6e 100644 --- a/prover/src/lfm/epoch_tests.rs +++ b/prover/src/lfm/epoch_tests.rs @@ -23,7 +23,8 @@ //! //! It stops at the challenges. That the legs then CONSUME these cells is //! [`the_legs_consume_the_replayed_challenges`]'s job, and the whole-epoch -//! composition (25 sub-proofs behind one statement) is not built here. +//! composition (16 sub-proofs behind one statement on this fixture, 25 at the +//! post-#977 ceiling) is not built here. use stark::config::Commitment; use stark::proof::stark::MultiProof; diff --git a/prover/src/lfm/epoch_verify_tests.rs b/prover/src/lfm/epoch_verify_tests.rs index cb3a424b2..dd014e77b 100644 --- a/prover/src/lfm/epoch_verify_tests.rs +++ b/prover/src/lfm/epoch_verify_tests.rs @@ -1,8 +1,8 @@ //! ★ The assembled epoch verifier — spine plus legs — run on a real //! continuation epoch proof. //! -//! [`super::epoch_tests`] built the Fiat-Shamir spine and checked all 115 of a -//! real 25-sub-proof epoch's challenges against production's own replay. Every +//! [`super::epoch_tests`] built the Fiat-Shamir spine and checked all 79 of a +//! real 16-sub-proof epoch's challenges against production's own replay. Every //! verification leg, meanwhile, was driven by its own isolation program with //! HINTED challenges. This module hangs the legs off the spine: per sub-proof the //! OOD grid is rebuilt from the two pruned blocks the transcript absorbed, the @@ -19,7 +19,7 @@ //! `assert_word_eq_lanes` against a root the transcript absorbed, and the FRI //! chain ends in `assert_eq_ext` against the terminal polynomial. A program that //! executes at all has passed them. So the differential that remains is the -//! spine's — the 115 challenges, still checked — plus the fact of execution, and +//! spine's — the 79 challenges, still checked — plus the fact of execution, and //! the falsification tests below are what turn "it executed" into evidence, by //! showing what does NOT execute. //! @@ -27,7 +27,7 @@ //! //! The preset. The fixture epoch is proved at the MIN preset (blowup 2, one //! query per table, grinding factor 1), because that is what -//! `proof_fixture::fixture_options` gives and what keeps a 25-sub-proof epoch +//! `proof_fixture::fixture_options` gives and what keeps a 16-sub-proof epoch //! provable in a unit test. Every per-query cost here is therefore ONE query's, //! and the blowup-8 predictions the phase pinned (73 queries, 14,454 FRI //! permutations per sub-proof) are reached by scaling, not by measurement — the @@ -341,12 +341,12 @@ impl TableLegs { /// continuation epoch proof that production accepts. /// /// What executing proves, stated precisely. Every check is an assert inside the -/// program, so reaching the end means: all 25 quotient identities held at the -/// spine's own `z` and `β`; every one of the 25 sub-proofs' opened row pairs +/// program, so reaching the end means: all 16 quotient identities held at the +/// spine's own `z` and `β`; every one of the 16 sub-proofs' opened row pairs /// hashed to a leaf that walked to the root the transcript absorbed, at the index /// the transcript sampled; every DEEP reconstruction fed a FRI chain that folded /// to the terminal polynomial the transcript absorbed; and the LogUp closure -/// reached production's COMMIT-bus target. The 115 published challenges are +/// reached production's COMMIT-bus target. The 79 published challenges are /// checked against production's replay on top, so the Fiat-Shamir the whole thing /// hangs from is still differentialled. #[test] @@ -425,11 +425,44 @@ fn the_assembled_epoch_verifier_runs() { // bisect priced — a near-empty always-on table is four challenges here and // +31.2% of the wrap's cells at the secure preset. // + // ★ And then FURTHER the same way, for the same reason at six times the + // size. + // + // MOVER: `892c7d1bc` (main's `c2ac5d546`, #977) — arm (i), the TABLE SET. + // That merge's two arms are (i) the table set shrank, empty tables now + // being elided rather than padded, and (ii) the absorbed epoch statement + // grew 49 bytes. This pin is on (i); `blake3_chip_tests`' + // STATEMENT_REPLAY_BLAKE3_ROWS and `machine_tests`' statement byte length + // are on (ii). + // + // #977 did to the six accelerator + // chips what #903's revert did to BLAKE3: `FIXED_TABLE_COUNT` 11 → 5, with + // `commit`, `keccak`, `keccak_rnd`, `ecsm`, `ecdas` and `hint` becoming + // `TableCounts` fields that a run which never reaches them reports as zero. + // This fixture epoch reaches none of the six, so 25 → 16 and 115 → 79. + // Six of the nine are those accelerators: the pre-#977 25 was 14 split + // families + 10 intermediate fixed (11 less HALT) + 1 L2G_MEMORY, and the + // fixed term is now 4, which lands at 19. The remaining three are split + // families this fixture leaves empty, and they are NOT named here because + // the measurement does not name them — only `e.tables.len()` is read. + // + // The accounting below is what says the whole move is empty tables at four + // challenges each: every one of them opens nothing, so it contributes a + // (β, z, γ) triple and one query index and no DEEP zeta, exactly as an + // always-on table did. If that model is wrong for any of the nine, the + // `checked` assertion two below fails and says so. + // + // The identity is spelled with both sides positive because `SUB_PROOFS` is + // now BELOW the 24 it used to be measured against, and `SUB_PROOFS - 24` on + // a `usize` is an underflow rather than a failed assertion. Moved this way + // it still fails — in either direction — if the four-challenge model stops + // describing the move. + // // `LFM_BLAKE3` (P-a Stage 5) does NOT appear in either number: it is a chip // of the LFM machine, counted by `NUM_LFM_CHIPS`, and this is the RV64 // epoch the LFM machine verifies. - const SUB_PROOFS: usize = 25; - const CHALLENGES_AT_MIN_PRESET: usize = 115; + const SUB_PROOFS: usize = 16; + const CHALLENGES_AT_MIN_PRESET: usize = 79; const CHALLENGES_PER_ALWAYS_ON_TABLE: usize = 4; assert_eq!( e.tables.len(), @@ -438,9 +471,10 @@ fn the_assembled_epoch_verifier_runs() { function of" ); assert_eq!( - CHALLENGES_AT_MIN_PRESET, - 111 + CHALLENGES_PER_ALWAYS_ON_TABLE * (SUB_PROOFS - 24), - "the always-on tables account for the whole move from the original 111" + CHALLENGES_AT_MIN_PRESET + CHALLENGES_PER_ALWAYS_ON_TABLE * 24, + 111 + CHALLENGES_PER_ALWAYS_ON_TABLE * SUB_PROOFS, + "the tables that left the proof account for the whole move from the \ + original 111" ); assert_eq!( checked, CHALLENGES_AT_MIN_PRESET, @@ -581,7 +615,7 @@ fn the_assembled_epoch_verifier_runs() { println!( "\x20 constraint leg inside the assembled verifier: {constraint_alu} ALU \ rows lowering ({constraint_unfused} unfused) + {recombination} \ - recombination = {} over 25 sub-proofs [pinned: see the run output]\ + recombination = {} over 16 sub-proofs [pinned: see the run output]\ \n\x20 that is {:.1}% of the legs' {} instructions", constraint_alu + recombination, 100.0 * (constraint_alu + recombination) as f64 @@ -665,7 +699,7 @@ fn the_assembled_epoch_verifier_runs() { // The pinned 213,744 came from `join_tests::join_leg_cost`, whose stated // assumptions are: all 28 PRODUCTION AIRs, every trace at a UNIFORM // 2^20, blowup 8, 73 queries, and NO FRI (the joined leg has none). The - // measurement above is: this epoch's 25 sub-proofs, at their REAL trace + // measurement above is: this epoch's 16 sub-proofs, at their REAL trace // lengths, blowup 2, one query, FRI included. Three parameters differ, so // the two numbers cannot be compared directly — they are projected onto each // other one parameter at a time instead, which is also what says which @@ -801,7 +835,7 @@ fn the_assembled_epoch_verifier_runs() { "\n RECONCILIATION against the pinned blowup-8 predictions (projections \ from shapes — this run is at the min preset and measures none of them):\n\ \x20 openings only, 73 queries, UNIFORM 2^20 (deep-join's own \ - assumption, over this epoch's 25 sub-proofs): {} [pinned: see the run output \ + assumption, over this epoch's 16 sub-proofs): {} [pinned: see the run output \ over all 28 production AIRs]\n\ \x20 openings only, 73 queries, this epoch's REAL trace lengths: {}\n\ \x20 openings + FRI, 73 queries, real lengths: {}\n\ diff --git a/prover/src/lfm/logup_tests.rs b/prover/src/lfm/logup_tests.rs index cd954aa2b..58e672ee9 100644 --- a/prover/src/lfm/logup_tests.rs +++ b/prover/src/lfm/logup_tests.rs @@ -949,8 +949,9 @@ enum RowWitness { /// /// ## Why this had to be measured /// -/// `FIXED_TABLE_COUNT` forces a sub-proof for all ten fixed tables whatever the -/// workload, so a real epoch always carries tables with no real rows. The +/// `FIXED_TABLE_COUNT` forces a sub-proof for its five tables whatever the +/// workload — ten before #977 moved the six accelerators into `TableCounts` — +/// so a real epoch always carries tables with no real rows. The /// closure's [`LogUpShape::num_contributing_tables`] is a program CONSTANT, so /// if such a table reported `None` the count would be workload-dependent and the /// constant wrong. The LogUp leg closed with this labelled INFERENCE: production @@ -978,8 +979,11 @@ enum RowWitness { /// "No rows" is read off the TRACE, not inferred from the workload, and not read /// back off the contribution being measured — see [`RowWitness`] for the two /// forms it takes and why one would not do. `FIXED_TABLE_COUNT` keeps the -/// sub-proof either way: `generate_keccak_trace` pads a zero-operation table to -/// four rows rather than dropping it. +/// sub-proof either way, and KECCAK_RC is the example since #977: it is one of +/// the five always-on tables, and its trace is padded with `MU` gated off +/// rather than dropped. KECCAK itself is no longer such a table — it is +/// `TableCounts::keccak`, and an epoch that calls no keccak carries no KECCAK +/// sub-proof to measure. /// /// ## Which sub-proof is which table /// @@ -1350,8 +1354,11 @@ fn a_zero_row_fixed_table_carries_some_zero_not_none() { // None would make every real epoch unverifiable. That is now a run: strip // the bus public inputs off a zero-row sub-proof and watch this very proof // stop verifying. Only the `is_some` direction can be tested on an epoch — - // all 25 sub-proofs declare interactions, so :1244's converse has no - // subject here. + // every sub-proof this epoch carries declares interactions, so :1244's + // converse has no subject here. It reads "all 16" since #977 (`892c7d1bc`) + // rather than all 25, and the count is deliberately not spelled: the loop + // walks `census`, so a literal here would be a second, driftable copy of a + // length the loop already has. for (i, (name, _, no_rows)) in census.iter().enumerate() { if !no_rows { continue; diff --git a/prover/src/lfm/machine_tests.rs b/prover/src/lfm/machine_tests.rs index cb26e662c..7a9830eec 100644 --- a/prover/src/lfm/machine_tests.rs +++ b/prover/src/lfm/machine_tests.rs @@ -2309,26 +2309,46 @@ fn assert_challenges_match(public: &[(u32, LfmWord)], f: &StatementFixture, what /// Phase A is spliced and at what shift. /// /// CORRECTION to an earlier claim of mine: the statement is NOT unconditionally -/// 3 bytes past a boundary. Its length is `215 + L + 16R`, so the shift Phase A -/// inherits is `(3 + L) mod 4` — it is 3 only when the public output happens to -/// be a multiple of four, and it is ZERO (Phase A entirely unspliced) whenever -/// `L ≡ 1 (mod 4)`. Since `L` is one byte per COMMIT op and therefore workload- -/// determined, the Phase-A splice cost is workload-dependent and free for about -/// one workload in four. +/// 3 bytes past a boundary. Its length is `264 + L + 16R`, so the shift Phase A +/// inherits is `L mod 4` — since `L` is one byte per COMMIT op and therefore +/// workload-determined, the Phase-A splice cost is workload-dependent, and free +/// (Phase A entirely unspliced) for about one workload in four. +/// +/// ★ THE CONSTANT TERM'S OWN SHIFT IS GONE, and this test is where that is +/// pinned. It was `215 + L + 16R`, giving `(3 + L) mod 4` — free only at +/// `L ≡ 1` — and `statement_replay`'s module doc said a single pad byte at the +/// end of the encoding would make all of Phase A free. The main-sync port +/// supplied it without aiming at it. +/// +/// MOVER: `892c7d1bc` (main's `c2ac5d546`, #977) — arm (ii), the STATEMENT +/// ENCODING. That merge's two arms are (i) the table set shrank, empty tables +/// now being elided rather than padded, and (ii) this one. `epoch_verify_tests`' +/// SUB_PROOFS is the pin on (i). +/// +/// #977 took the six accelerator chips out of +/// `FIXED_TABLE_COUNT` (11 → 5) and made them counted, so `NUM_TABLE_COUNTS` +/// went 15 → 21 (`+48 ≡ 0 mod 4`, which moves no shift), and the same PR +/// appended `is_final` as the statement's last byte (`+1`). `215 + 49 = 264`, +/// and `264 ≡ 0 (mod 4)`. +/// +/// The acceptance shape is still spliced, which is what keeps the splice path +/// under test: `L = 14 ≢ 0 (mod 4)`, so the cursor lands at shift 2 where it +/// used to land at 3. #[test] -fn epoch_statement_cursor_is_three_plus_output_len() { +fn epoch_statement_cursor_is_the_output_len_alone() { let shape = epoch_statement_shape(); let r = shape.page_ranges.len(); - // 215, not the 207 of the fourteen-count era: `TableCounts::blake3` added - // one absorbed u64. Eight bytes is a whole number of halves, so the shift - // Phase A inherits is unchanged. - assert_eq!(shape.byte_len(), 215 + STMT_PUBLIC_OUTPUT_LEN + 16 * r); + // 264, not the 215 of the fifteen-count era and not the 207 of the + // fourteen-count one: six accelerator counts (+48) and the trailing + // `is_final` byte (+1). Both terms are named in the doc above, because 264 + // is the sum of a change that moves NO shift and one that moves it by one. + assert_eq!(shape.byte_len(), 264 + STMT_PUBLIC_OUTPUT_LEN + 16 * r); for l in 0..8usize { - let total = 215 + l + 16 * r; + let total = 264 + l + 16 * r; assert_eq!( total % keccak_host::BYTES_PER_HALF, - (3 + l) % keccak_host::BYTES_PER_HALF, - "Phase A inherits shift (3 + L) mod 4" + l % keccak_host::BYTES_PER_HALF, + "Phase A inherits shift L mod 4" ); } // The acceptance shape is chosen to exercise BOTH new paths at once: an diff --git a/prover/src/lfm/registry.rs b/prover/src/lfm/registry.rs index 7bda2402b..8130d0c5c 100644 --- a/prover/src/lfm/registry.rs +++ b/prover/src/lfm/registry.rs @@ -570,6 +570,28 @@ pub fn resolve( // cargo run --bin compute_lfm_registry --release // and paste the output below. Drift tests recompute and compare on every PR. // +// ★ LAST REGENERATION, and what forced it: the main-sync merge `892c7d1bc` +// (main's `c2ac5d546`, #977) grew the absorbed continuation-epoch statement by +// 49 bytes — six accelerator counts joined it when `FIXED_TABLE_COUNT` went +// 11 -> 5 (`NUM_TABLE_COUNTS` 15 -> 21, +48) and `is_final` was appended as its +// last byte (+1). StatementReplayV0 is the one registered program that replays +// that statement, so its script gained one `Blake3Chain` compression and seven +// of its fifteen roots moved with `program_id`. +// +// ⚠ EXACTLY ONE ENTRY MOVED, and that was checked rather than assumed: the +// other five programs build no epoch statement, and all fifteen roots, the +// log-heights, `keccak_rnd_chunks`, `hasher` and `chip_set` of each came back +// byte-identical. `log_heights[11]` did NOT move even for StatementReplayV0 — +// 9 and 10 compressions both pad to the 16-row group. The regenerated +// `roots[11]` also equals the value `machine_tests:: +// every_registry_entry_is_a_single_blake3_table` computes from the program +// (`7a 3b 86 1b ...`), which is what says the paste closes the gap the pin +// found rather than moving the pin to meet the paste. +// +// `compute_static_commitments` was NOT re-run and did not need to be: this is +// not a hash-pin change, so slots 13 and 14 (KECCAK_RC's and BITWISE's static +// preprocessed commitments) are untouched — and they came back identical. +// // ★ WHICH CONFIGURATION THIS TABLE ASSUMES, and what would move it. // // Three axes are BOUND into every digest below, and the fourth stopped being @@ -1083,14 +1105,14 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ blowup_factor: 2, roots: [ [ - 0x8e, 0x12, 0x29, 0x48, 0x9e, 0xac, 0x16, 0x2c, 0x45, 0x9a, 0x99, 0xbf, 0xde, 0x4a, - 0x9a, 0xd5, 0x57, 0x3c, 0xff, 0x61, 0xee, 0x7a, 0xd5, 0x20, 0xa0, 0x1d, 0x7a, 0x27, - 0x4c, 0x93, 0xef, 0xb4, + 0xc0, 0x80, 0x4f, 0xab, 0xb9, 0xa1, 0x41, 0xe8, 0xcf, 0xda, 0x76, 0xea, 0xca, 0x45, + 0x0d, 0xdc, 0x21, 0xf1, 0xb3, 0x32, 0xe0, 0x91, 0xc8, 0xce, 0xa5, 0x96, 0x96, 0xa3, + 0x30, 0x36, 0x09, 0x97, ], [ - 0x79, 0x6f, 0x6d, 0xe6, 0xb0, 0x27, 0x4a, 0x4f, 0x35, 0x50, 0x4f, 0x02, 0x76, 0x26, - 0x3c, 0x73, 0x2b, 0xbe, 0xa6, 0xdd, 0xab, 0xb3, 0x9e, 0xf7, 0x4a, 0xce, 0x51, 0xc1, - 0x12, 0xa2, 0x80, 0x40, + 0xfb, 0xca, 0xf1, 0x74, 0xa1, 0xad, 0xf6, 0x3d, 0x24, 0x92, 0x44, 0x80, 0xc8, 0x64, + 0x4d, 0xb2, 0xdc, 0x8a, 0x33, 0xc0, 0x98, 0x7a, 0x9f, 0xba, 0xbd, 0xe4, 0x8e, 0xa6, + 0xa9, 0x43, 0x5c, 0x5a, ], [ 0x07, 0xdb, 0x70, 0x37, 0x6d, 0xff, 0x1c, 0x50, 0x7f, 0x82, 0xf7, 0x83, 0x73, 0x7c, @@ -1098,14 +1120,14 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ 0xae, 0x17, 0x71, 0x37, ], [ - 0x06, 0xfe, 0x81, 0xac, 0x1e, 0xd6, 0x2e, 0x90, 0xec, 0xd5, 0x9a, 0x03, 0x33, 0xe2, - 0xdf, 0xeb, 0xa5, 0xa5, 0x42, 0xe4, 0x7a, 0xec, 0x27, 0x4c, 0xda, 0x74, 0x87, 0x31, - 0xe1, 0x40, 0xe0, 0x58, + 0x36, 0xb7, 0x63, 0x4d, 0x83, 0x5b, 0xfc, 0x7e, 0x23, 0x62, 0xfe, 0x2c, 0xf1, 0xc4, + 0xf6, 0x2f, 0x2f, 0x8d, 0x45, 0x5c, 0x21, 0xaf, 0x24, 0xd8, 0x01, 0xfe, 0x3a, 0x68, + 0x64, 0x9e, 0xdd, 0x38, ], [ - 0x60, 0xdf, 0x05, 0x40, 0x1e, 0x94, 0x4d, 0x5a, 0x43, 0xd7, 0x0b, 0xe9, 0x8e, 0x38, - 0x1e, 0x3d, 0x22, 0xa5, 0x91, 0xeb, 0xa4, 0x1f, 0xf8, 0xff, 0x1f, 0x96, 0x8b, 0x53, - 0xb6, 0x48, 0x97, 0xd7, + 0x5c, 0x51, 0x64, 0x8c, 0xad, 0x71, 0x1f, 0x07, 0x17, 0x09, 0x71, 0x74, 0x03, 0x60, + 0x90, 0x87, 0x6e, 0x7b, 0x9d, 0xe6, 0xd0, 0x59, 0x6e, 0xf4, 0x2c, 0x1b, 0xb5, 0x83, + 0x58, 0xf2, 0x98, 0x1f, ], [ 0x7d, 0x25, 0xc1, 0xee, 0x40, 0x2b, 0x03, 0x6b, 0xf9, 0x14, 0x9a, 0xa3, 0x50, 0x04, @@ -1118,9 +1140,9 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ 0xff, 0x31, 0xec, 0xb2, ], [ - 0x92, 0x13, 0x7a, 0xa0, 0xb8, 0xe0, 0xe3, 0xb7, 0xb0, 0x4e, 0x49, 0x3d, 0x2b, 0x8f, - 0x7d, 0x1a, 0xef, 0x0b, 0x47, 0x68, 0x28, 0xd7, 0x23, 0x8c, 0xa4, 0x4c, 0x10, 0x2c, - 0x2e, 0x1c, 0x6d, 0x0c, + 0x8f, 0xad, 0x35, 0x4f, 0xa7, 0x06, 0x90, 0xd9, 0x49, 0x80, 0x19, 0xcc, 0x81, 0xfd, + 0xaf, 0xdd, 0x5f, 0x32, 0x13, 0xc8, 0xfc, 0xf9, 0xae, 0xcc, 0x0f, 0xfa, 0x67, 0x16, + 0xd8, 0x6e, 0x06, 0x20, ], [ 0x8a, 0xc9, 0x0a, 0xc6, 0x8d, 0x5c, 0x71, 0xf7, 0x0d, 0x60, 0x13, 0x14, 0x21, 0xcc, @@ -1128,9 +1150,9 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ 0xc5, 0xb2, 0x5e, 0x21, ], [ - 0xe5, 0x6d, 0x6f, 0x2a, 0x3b, 0x38, 0x2f, 0xd0, 0xcf, 0x6f, 0xcb, 0x53, 0xb3, 0xfa, - 0x03, 0x1b, 0x4e, 0x99, 0xda, 0x4a, 0xa2, 0xf7, 0x82, 0x23, 0x9f, 0x03, 0x59, 0x06, - 0x51, 0xec, 0x4d, 0x4f, + 0x99, 0x86, 0x5e, 0xbf, 0x36, 0xe0, 0xaa, 0xf0, 0x3a, 0xed, 0x45, 0x21, 0xb9, 0xca, + 0x8c, 0x4f, 0x9e, 0x5a, 0x16, 0x37, 0x1d, 0xea, 0xd9, 0x84, 0xae, 0x56, 0x93, 0xf8, + 0x7f, 0xcb, 0x4a, 0x18, ], [ 0xa3, 0xd2, 0x1d, 0x58, 0xbf, 0x0c, 0x09, 0xb2, 0x14, 0xce, 0xe6, 0x4f, 0x94, 0xf8, @@ -1138,9 +1160,9 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ 0xe8, 0xc4, 0x17, 0x99, ], [ - 0x6a, 0xc2, 0xa2, 0x99, 0xe6, 0x48, 0x90, 0x8b, 0xe6, 0xa1, 0xca, 0xbf, 0x87, 0x9c, - 0x70, 0x73, 0xe2, 0x70, 0x50, 0x82, 0xf9, 0xeb, 0xdf, 0xeb, 0x61, 0x21, 0x06, 0x7f, - 0x37, 0x78, 0x2a, 0x1d, + 0x7a, 0x3b, 0x86, 0x1b, 0xc0, 0x56, 0x74, 0x90, 0x30, 0x0f, 0x37, 0x0b, 0x20, 0x41, + 0x27, 0x22, 0x29, 0x0d, 0xa4, 0x4d, 0xa1, 0xeb, 0x68, 0xed, 0x82, 0x13, 0x1e, 0xa6, + 0xfd, 0x6f, 0x02, 0x41, ], [ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, @@ -1166,9 +1188,9 @@ pub static LFM_REGISTRY: &[LfmRegistryEntry] = &[ blake3: true, }, program_id: [ - 0xd9, 0x80, 0x4c, 0xab, 0xc9, 0xa2, 0xbb, 0x15, 0xb2, 0x36, 0xe3, 0x4b, 0x50, 0x05, - 0x97, 0x07, 0x99, 0xf6, 0x54, 0xa3, 0x87, 0x07, 0x34, 0xa5, 0x14, 0x8a, 0xd5, 0x63, - 0x21, 0xd6, 0xa6, 0x4d, + 0x5f, 0x89, 0x18, 0xf9, 0x16, 0xd3, 0xc5, 0xb8, 0x38, 0xfe, 0x73, 0x6e, 0x5f, 0xc0, + 0x30, 0x62, 0xf6, 0x4a, 0x72, 0xa4, 0xd6, 0x12, 0x27, 0x98, 0x8b, 0x2c, 0x24, 0xa4, + 0xcf, 0x6e, 0x28, 0x21, ], }, ]; diff --git a/prover/src/tests/constraint_artifact_tests.rs b/prover/src/tests/constraint_artifact_tests.rs index 2f8f41921..cd7e40c63 100644 --- a/prover/src/tests/constraint_artifact_tests.rs +++ b/prover/src/tests/constraint_artifact_tests.rs @@ -716,17 +716,27 @@ fn epoch_chunk_multiplier() { /// /// ```text /// 14 split-table families (>= 1 chunk each) -/// + FIXED_TABLE_COUNT (10 final, 9 intermediate — HALT only on the last) +/// + FIXED_TABLE_COUNT (5 final, 4 intermediate — HALT only on the last) +/// + up to 6 accelerators (COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS, HINT — +/// one each, and only when the workload reaches it) /// + 1 L2G_MEMORY /// ``` /// -/// which gives **24 sub-proofs intermediate, 25 final** — independently measured -/// on the LFM fibonacci epoch fixture. This test asserts that arithmetic so the -/// composition is pinned rather than inferred: if the epoch shape changes, the -/// count here stops matching the measured one and this fails. +/// which gives **25 sub-proofs intermediate and 26 final AT MOST**, and 19 / 20 +/// for a workload that calls no accelerator. This test asserts that arithmetic +/// so the composition is pinned rather than inferred: if the epoch shape +/// changes, the count here stops matching and this fails. /// -/// The instruction total is then a minimum, since it assumes one chunk per -/// family — a larger epoch adds chunks of the CHEAP AIRs (see +/// ★ The ceiling is what moved. MOVER: `892c7d1bc` (main's `c2ac5d546`, #977) +/// — arm (i), the TABLE SET; arm (ii) is the +49-byte epoch statement, pinned +/// in `machine_tests` and `blake3_chip_tests`. #977 took the six accelerators out of +/// `FIXED_TABLE_COUNT` (11 → 5), so the 25/26 that used to be THE composition +/// is now its upper bound — the same count, reached only by a workload that +/// touches every accelerator. `epoch_verify_tests` measures the other end on +/// the fibonacci fixture, which reaches none of the six and carries 16. +/// +/// The instruction total is a minimum in the other axis, since it assumes one +/// chunk per family — a larger epoch adds chunks of the CHEAP AIRs (see /// `epoch_chunk_multiplier`). #[test] fn continuation_epoch_constraint_leg() { @@ -746,33 +756,35 @@ fn continuation_epoch_constraint_leg() { // sub-proof each REGARDLESS of TableCounts, because a zero-row table still // needs its proof or its constraints drop out of verification. HALT is the // one an intermediate epoch omits. + let always_on = ["BITWISE", "DECODE", "HALT", "KECCAK_RC", "REGISTER"]; + // ★ THE SIX THAT LEFT, and they left the way BLAKE3 did. #977 — on this + // lineage, the merge `892c7d1bc` — took + // `FIXED_TABLE_COUNT` 11 → 5 and made these six `TableCounts` fields, so a + // run that never reaches one carries no sub-proof for it — the same EC + // campaign argument (PR #871) that moved BLAKE3 out first, applied to the + // rest of the accelerator group. // - // ⚠ BLAKE3 is deliberately NOT here. It left this list when it became - // `TableCounts::blake3`, a 0-or-1 count — a workload that never executes a - // BLAKE3 syscall carries no BLAKE3 sub-proof at all, so the counts below are - // the blake3-free shape and a blake3-using epoch is one higher. HINT was - // missing from this list outright, which is why it read 10 while the - // constant said 11. - let fixed_final = [ - "BITWISE", - "DECODE", - "HALT", - "COMMIT", - "KECCAK", - "KECCAK_RND", - "KECCAK_RC", - "REGISTER", - "ECSM", - "ECDAS", - "HINT", - ]; + // They stay in the COST sum below because the sum is a ceiling: a workload + // that calls every accelerator pays all eleven legs, and that is the figure + // the recursion budget has to clear. What changed is that the figure is now + // a MAXIMUM rather than a floor — a workload reaching none of the six pays + // `always_on` plus the families alone. + // + // ⚠ BLAKE3 is deliberately in NEITHER list. It is `TableCounts::blake3`, a + // 0-or-1 count, and it is not in `TableCounts::total`'s accelerator group + // either, so the counts below are the blake3-free shape and a blake3-using + // epoch is one higher. + let accelerators = ["COMMIT", "KECCAK", "KECCAK_RND", "ECSM", "ECDAS", "HINT"]; // The list is a census OF the constant, so it must not be able to drift from - // it silently — the failure this pin previously had. + // it silently — the failure this pin previously had. It is `always_on` and + // not the eleven that the constant counts, which is exactly the assertion + // that went red on the main-sync port and named its own cause. assert_eq!( - fixed_final.len(), + always_on.len(), crate::FIXED_TABLE_COUNT, "the always-on list must name every FIXED_TABLE_COUNT table" ); + let fixed_final: Vec<&str> = always_on.iter().chain(accelerators.iter()).copied().collect(); let families_instr: usize = families.iter().map(|l| get(l)).sum(); let fixed_final_instr: usize = fixed_final.iter().map(|l| get(l)).sum(); @@ -788,17 +800,19 @@ fn continuation_epoch_constraint_leg() { (n_intermediate, n_final), (25, 26), "epoch sub-proof composition no longer reproduces the measured 25 intermediate / \ - 26 final (blake3-free; a BLAKE3-using epoch is one higher)" + 26 final CEILING (every accelerator reached; blake3-free, and a BLAKE3-using \ + epoch is one higher)" ); println!( - "\ncontinuation epoch constraint leg (minimum: one chunk per family)\n \ + "\ncontinuation epoch constraint leg (every accelerator reached, one chunk per family)\n \ 14 split families {families_instr}\n \ - 10 fixed (no HALT) {fixed_intermediate_instr}\n \ + 4 fixed + 6 accel {fixed_intermediate_instr} (no HALT)\n \ 1 L2G_MEMORY {l2g}\n \ INTERMEDIATE epoch {intermediate} instr over {n_intermediate} sub-proofs\n \ FINAL epoch (+HALT) {final_epoch} instr over {n_final} sub-proofs\n \ - fixed share {:.0}% — the leg is workload-INDEPENDENT\n", + fixed+accel share {:.0}% — the 4 fixed legs are workload-INDEPENDENT, \ + the 6 accelerator legs are not\n", 100.0 * fixed_intermediate_instr as f64 / intermediate as f64 ); From 788f36a192156eee95db11a0cd677d4f4b4e7dc6 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 15:01:58 -0300 Subject: [PATCH 2/8] test(prover): the multilinear table-set gates name the tables they argued MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `prove_and_verify_all_tables` returned a count, and its three callers asserted `>= 20` against it. Two of the three are red on the lineage since 892c7d1bc (#977) elided empty tables, and between them they produced one usable diagnostic and one that said nothing at all: every_live_table_is_proved_and_verified "expected the full table set, argued 10" the_whole_instruction_set_..._verified "assertion failed: ... >= 20" The second is a bare `assert!`, so neither CI nor the box could say what it argued — which is why a red gate on the lineage base needed a second run to diagnose at all. The helper now returns the argued tables BY NAME, in `air_trace_pairs` order, and each of the three assertions prints the whole list. Captured from `pairs` rather than from the AIR set, so it is the proof's own sub-proof order, and pinned against `tables.len()` so a census that described a different proof cannot pass. This is a diagnostic step, taken separately on purpose: the `>= 20` bound itself is what wants replacing, and it wants the measured sets first. Since #977 the set is workload-dependent — an empty table is elided rather than padded — so "how many" stopped being the question and "which ones" became it. A count cannot tell a table that vanished from one that gained a chunk while another vanished, which is exactly the class of move #977 made. The bound is left at `>= 20` here and is expected to stay red for two of the three; the named-set pins land once the three lists are in hand. --- prover/src/tests/multilinear_table_tests.rs | 45 ++++++++++++++++++--- 1 file changed, 40 insertions(+), 5 deletions(-) diff --git a/prover/src/tests/multilinear_table_tests.rs b/prover/src/tests/multilinear_table_tests.rs index 763b6a954..3cb27a977 100644 --- a/prover/src/tests/multilinear_table_tests.rs +++ b/prover/src/tests/multilinear_table_tests.rs @@ -260,7 +260,13 @@ fn layout_dyn<'a>( /// counterparty is not another table but the statement, so the tables only sum /// to zero for a program that outputs nothing. `compute_commit_bus_offset` is /// the same quantity the univariate verifier demands. -fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { +/// +/// ★ Returns the argued tables BY NAME, in `air_trace_pairs` order, because a +/// count cannot say which. Since #977 the set is workload-dependent — an empty +/// table is elided rather than padded — so "how many" stopped being the +/// question and "which ones" became it: a count cannot tell a table that +/// vanished from one that gained a chunk while another vanished. +fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> Vec { let mut traces = Traces::from_elf_and_logs_minimal(&elf, logs, &Default::default(), &[]).unwrap(); let public_output = traces.public_output_bytes.clone(); @@ -298,6 +304,13 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { }) .collect(); + // Captured before `tables` is moved into the commitment, and from `pairs` + // rather than from the AIR set, so it is the proof's own sub-proof order. + let names: Vec = pairs + .iter() + .map(|(air, _, _)| air.name().to_string()) + .collect(); + let mut tables = Vec::with_capacity(pairs.len()); for ((air, trace, _), &(width, num_vars)) in pairs.iter().zip(&shapes) { let columns = trace.columns_main(); @@ -309,6 +322,11 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { ); } let count = tables.len(); + assert_eq!( + names.len(), + count, + "one name per argued table, or the census below describes another proof" + ); // Every table's columns in one commitment: 55 of them still open once. let committed = CommittedTables::<_, _, KeccakWhir>::commit(tables, &config()).expect("commit every table"); @@ -362,7 +380,7 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { ) .expect("the whole table set verifies"); - count + names } /// **The whole VM through the multilinear path**: every live table of a real @@ -375,7 +393,12 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { fn every_live_table_is_proved_and_verified() { let (elf, logs, _) = run_asm_elf("sub"); let argued = prove_and_verify_all_tables(elf, &logs); - assert!(argued >= 20, "expected the full table set, argued {argued}"); + assert!( + argued.len() >= 20, + "expected the full table set, argued {}: {}", + argued.len(), + argued.join(" ") + ); } /// The same over the whole 64-bit instruction set, which lights up the tables a @@ -383,7 +406,13 @@ fn every_live_table_is_proved_and_verified() { #[test] fn the_whole_instruction_set_is_proved_and_verified() { let (elf, logs, _) = run_asm_elf("all_instructions_64"); - assert!(prove_and_verify_all_tables(elf, &logs) >= 20); + let argued = prove_and_verify_all_tables(elf, &logs); + assert!( + argued.len() >= 20, + "expected the full table set, argued {}: {}", + argued.len(), + argued.join(" ") + ); } /// And over a Rust program that calls the keccak precompile — which brings @@ -403,7 +432,13 @@ fn a_program_using_a_precompile_is_proved_and_verified() { .expect("run") .logs; - assert!(prove_and_verify_all_tables(elf, &logs) >= 20); + let argued = prove_and_verify_all_tables(elf, &logs); + assert!( + argued.len() >= 20, + "expected the full table set, argued {}: {}", + argued.len(), + argued.join(" ") + ); } /// A proof is only a proof if it can leave the process. Round-trips a real From 865c689b0b2516457d605fb231cac2519bf1d920 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 15:11:22 -0300 Subject: [PATCH 3/8] style(tests): rustfmt the accelerator-list chain MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `make fmt` from the repo root. One line, in the `fixed_final` construction the re-bless added: the `always_on.iter().chain(accelerators.iter())` chain sat at 93 columns, which rustfmt breaks onto one method per line. Nothing else moved, which is the useful part. The registry regeneration in 8cedf2e25 hand-reproduced rustfmt's 14/14/4 wrapping for eight `[u8; 32]` literals rather than running the formatter over them, and rustfmt touched none of the eight — so the reconstruction was exact. Had any been wrong, `cargo fmt --check --all` would have failed as `make lint`'s first step instead of passing. --- prover/src/tests/constraint_artifact_tests.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prover/src/tests/constraint_artifact_tests.rs b/prover/src/tests/constraint_artifact_tests.rs index cd7e40c63..dbecbcb8b 100644 --- a/prover/src/tests/constraint_artifact_tests.rs +++ b/prover/src/tests/constraint_artifact_tests.rs @@ -784,7 +784,11 @@ fn continuation_epoch_constraint_leg() { crate::FIXED_TABLE_COUNT, "the always-on list must name every FIXED_TABLE_COUNT table" ); - let fixed_final: Vec<&str> = always_on.iter().chain(accelerators.iter()).copied().collect(); + let fixed_final: Vec<&str> = always_on + .iter() + .chain(accelerators.iter()) + .copied() + .collect(); let families_instr: usize = families.iter().map(|l| get(l)).sum(); let fixed_final_instr: usize = fixed_final.iter().map(|l| get(l)).sum(); From 413b3a3b77a2108a9c040440d38ab446a27e739f Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 15:16:50 -0300 Subject: [PATCH 4/8] test(prover): the table-set gates pin the SET, and one of them pins a gap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The three multilinear table-set cases asserted `>= 20` argued tables. Two went red when the main-sync merge `892c7d1bc` (main's `c2ac5d546`, #977) took `FIXED_TABLE_COUNT` 11 -> 5 and made COMMIT, KECCAK, KECCAK_RND, ECSM, ECDAS and HINT counted: an empty table is ELIDED from the proof now rather than padded into it, so the argued set is workload-dependent and "the full table set" stopped being something a bound could describe. A count is the wrong instrument for that move, twice over. It cannot tell a table that VANISHED from one that gained a chunk while another vanished, and it says nothing about ORDER — which `air_trace_pairs` calls the proof's sub-proof layout in as many words, since `air_refs` has to reproduce it. So the bound is replaced by the ordered census, MEASURED on the box at 788f36a19, CPU-only, no campaign env: sub 10 BITWISE DECODE KECCAK_RC REGISTER HALT CPU[0] LT[0] MEMW_A[0] PAGE:0x0 MEMW_R[0] all_instructions_64 15 ... + SHIFT[0] MUL[0] DVRM[0] BYTEWISE[0] CPU32[0] The first five of each are exactly `FIXED_TABLE_COUNT`'s five, in `air_trace_pairs` order, which is a third independent confirmation of the 11->5 move — after the epoch's 25 -> 16 sub-proofs and the statement's +49 bytes. `ALWAYS_ON_TABLES` holds them once and `the_always_on_prefix_is_the_constants_own` pins its length against the constant, so the shared half of both censuses cannot drift from the machine the way `constraint_artifact_tests`' sibling list did (it named eleven while the constant said five). ⚠ `all_instructions_64` IS NOT THE FULL TABLE SET, and the old bound is what hid that. Fifteen argued, and six counted families absent: MEMW (the unaligned one — only MEMW_A and MEMW_R appear), LOAD, STORE, BRANCH, EQ and COMMIT, plus every accelerator. Since #977 an absent table is a table with NO ROWS, so the fixture executes no branch, no load, no store and no `eq` — a narrower program than its name suggests. Not fixed here: widening it edits `executor/programs/asm`, and this census is the thing that would notice. Pinned, with a non-vacuity check that the five tables it does add over `sub` are actually present, so the two censuses cannot decay into one test written twice. The precompile case keeps its bound and is the only one without an ordered census, deliberately: it PASSED the measuring run, so its assertion never fired and never printed its set, and pinning a list nobody has read would be a literal invented to fit a bound. It gains instead the checks its doc has always claimed and never made — that KECCAK_RND and COMMIT are argued at all, which is the whole reason it sits beside the two asm cases. Since #977 those are counted tables, so a workload that stopped reaching the precompile would drop them silently and still clear any bound. Matched as "equal, or followed by `[`" so a bare prefix cannot let KECCAK_RC answer for the family. Every assertion prints the full set, so the run that fails one is the run that supplies the census. --- prover/src/tests/multilinear_table_tests.rs | 171 ++++++++++++++++++-- 1 file changed, 160 insertions(+), 11 deletions(-) diff --git a/prover/src/tests/multilinear_table_tests.rs b/prover/src/tests/multilinear_table_tests.rs index 3cb27a977..c483e18e2 100644 --- a/prover/src/tests/multilinear_table_tests.rs +++ b/prover/src/tests/multilinear_table_tests.rs @@ -383,41 +383,164 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> Vec { names } +/// The `FIXED_TABLE_COUNT` always-on tables, in `air_trace_pairs` order — the +/// prefix EVERY argued set opens with, whatever the workload runs. +/// +/// One copy, shared by the cases below, because it is the half of each census +/// that is machine shape rather than program shape: a workload cannot add to it +/// or take from it. The counted tables that follow are the program's own. +const ALWAYS_ON_TABLES: [&str; 5] = ["BITWISE", "DECODE", "KECCAK_RC", "REGISTER", "HALT"]; + +/// The shared prefix of `argued`, as `&str` so it compares against the literal +/// censuses below. +fn always_on_prefix(argued: &[String]) -> Vec<&str> { + argued + .iter() + .take(ALWAYS_ON_TABLES.len()) + .map(String::as_str) + .collect() +} + +/// [`ALWAYS_ON_TABLES`] is a census OF `FIXED_TABLE_COUNT`, so it must not be +/// able to drift from it silently — the failure the sibling list in +/// `constraint_artifact_tests` actually had, where it named eleven while the +/// constant said five. +#[test] +fn the_always_on_prefix_is_the_constants_own() { + assert_eq!( + ALWAYS_ON_TABLES.len(), + crate::FIXED_TABLE_COUNT, + "the always-on prefix must name every FIXED_TABLE_COUNT table" + ); +} + /// **The whole VM through the multilinear path**: every live table of a real /// run proved in one multi-table proof and verified, buses included. /// /// The traces come from the executor, not from hand-written operations, so the /// widths, the interaction counts, the packings and the multiplicity patterns /// are whatever the VM actually produces. +/// +/// ★ THE SET BY NAME, NOT A COUNT, and the reason is #977. This asserted +/// `>= 20` until the main-sync merge `892c7d1bc` (main's `c2ac5d546`, #977) +/// took `FIXED_TABLE_COUNT` 11 -> 5 and made COMMIT, KECCAK, KECCAK_RND, ECSM, +/// ECDAS and HINT counted: an empty table is now ELIDED from the proof rather +/// than padded into it, so the argued set is workload-dependent and "the full +/// table set" stopped being a thing a bound could describe. It read 10 here. +/// +/// A count is the wrong instrument for that move twice over. It cannot tell a +/// table that VANISHED from one that gained a chunk while another vanished, and +/// it says nothing about ORDER — which `air_trace_pairs` calls the proof's +/// sub-proof layout in as many words, since `air_refs` must reproduce it. The +/// ordered census fails on any of the three and names which. +/// +/// MEASURED at `788f36a19`, box, CPU-only, no campaign env. `[0]` is a chunk +/// index and `PAGE:0x0` a page base, both as `AIR::name` renders them. #[test] fn every_live_table_is_proved_and_verified() { let (elf, logs, _) = run_asm_elf("sub"); let argued = prove_and_verify_all_tables(elf, &logs); - assert!( - argued.len() >= 20, - "expected the full table set, argued {}: {}", - argued.len(), + assert_eq!( + always_on_prefix(&argued), + ALWAYS_ON_TABLES, + "every argued set opens with the always-on tables; argued: {}", argued.join(" ") ); + assert_eq!( + argued, + [ + "BITWISE", + "DECODE", + "KECCAK_RC", + "REGISTER", + "HALT", + "CPU[0]", + "LT[0]", + "MEMW_A[0]", + "PAGE:0x0", + "MEMW_R[0]", + ], + "the argued table set moved — a table appeared, vanished, or the \ + sub-proof order changed" + ); } -/// The same over the whole 64-bit instruction set, which lights up the tables a -/// two-instruction program never reaches. +/// The same over the whole 64-bit instruction set, which lights up tables a +/// two-instruction program never reaches: SHIFT, MUL, DVRM, BYTEWISE and CPU32, +/// five more than `sub`'s ten. +/// +/// ⚠ AND IT IS NOT THE FULL TABLE SET, which is what the old `>= 20` bound and +/// its "expected the full table set" message both claimed. Fifteen tables are +/// argued, and six counted families are absent: MEMW (the unaligned one; only +/// MEMW_A and MEMW_R appear), LOAD, STORE, BRANCH, EQ and COMMIT — plus every +/// accelerator. Since #977 an absent table means a table with NO ROWS, so this +/// says the `all_instructions_64` fixture executes no branch, no load, no store +/// and no `eq`, which is a narrower program than its name suggests. +/// +/// That gap is PINNED rather than fixed here: widening the fixture is a change +/// to `executor/programs/asm`, and this census is what would notice it. A +/// family arriving fails this test saying which, which is the outcome to want. +/// +/// MEASURED at `788f36a19`, box, CPU-only, no campaign env. #[test] fn the_whole_instruction_set_is_proved_and_verified() { let (elf, logs, _) = run_asm_elf("all_instructions_64"); let argued = prove_and_verify_all_tables(elf, &logs); - assert!( - argued.len() >= 20, - "expected the full table set, argued {}: {}", - argued.len(), + assert_eq!( + always_on_prefix(&argued), + ALWAYS_ON_TABLES, + "every argued set opens with the always-on tables; argued: {}", argued.join(" ") ); + assert_eq!( + argued, + [ + "BITWISE", + "DECODE", + "KECCAK_RC", + "REGISTER", + "HALT", + "CPU[0]", + "LT[0]", + "SHIFT[0]", + "MEMW_A[0]", + "MUL[0]", + "DVRM[0]", + "PAGE:0x0", + "MEMW_R[0]", + "BYTEWISE[0]", + "CPU32[0]", + ], + "the argued table set moved — a table appeared, vanished, or the \ + sub-proof order changed" + ); + // NON-VACUITY against the case above: this fixture must actually reach + // further than `sub` did, or the two censuses are one test written twice. + for wider in ["SHIFT[0]", "MUL[0]", "DVRM[0]", "BYTEWISE[0]", "CPU32[0]"] { + assert!( + argued.iter().any(|n| n == wider), + "{wider} is what this case adds over `sub`; argued: {}", + argued.join(" ") + ); + } } /// And over a Rust program that calls the keccak precompile — which brings /// KECCAK, KECCAK_RND and KECCAK_RC in, **and** writes public output, so the /// statement's share of the bus is load-bearing here and nowhere else. +/// +/// ⚠ THE ONLY CASE WITHOUT AN ORDERED CENSUS, and deliberately so. The two +/// above are pinned to sets MEASURED at `788f36a19`; this one PASSED that run, +/// so its assertion never fired and never printed its set, and pinning a list +/// nobody has read would be a literal invented to match a bound. It keeps the +/// bound and gains the checks its own doc has always claimed instead. +/// +/// The presence checks are the point: `>= 20` never once asserted that the +/// keccak family or COMMIT is argued here, which is the entire reason this case +/// exists next to the two asm ones. Since #977 those tables are counted, so a +/// workload that stopped reaching the precompile would silently drop them and +/// still clear any bound this case could carry. Both assertions print the whole +/// set, so the run that fails one is also the run that supplies the census. #[test] fn a_program_using_a_precompile_is_proved_and_verified() { let root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) @@ -433,9 +556,35 @@ fn a_program_using_a_precompile_is_proved_and_verified() { .logs; let argued = prove_and_verify_all_tables(elf, &logs); + assert_eq!( + always_on_prefix(&argued), + ALWAYS_ON_TABLES, + "every argued set opens with the always-on tables; argued: {}", + argued.join(" ") + ); + // The tables this case is ABOUT, by presence rather than by a full census. + // KECCAK_RC is excluded from the prefix match on purpose — it is always-on + // and asserted above, so matching it here would let a run that reaches no + // precompile at all satisfy a check named for one. + for family in ["KECCAK_RND", "COMMIT"] { + // The name is either the bare family or the family plus a chunk index, + // so the match is "equal, or followed by `[`" — never a bare prefix, + // which would let `KECCAK_RC` answer for `KECCAK`. + assert!( + argued.iter().any(|n| { + let s = n.as_str(); + s == family || (s.starts_with(family) && s[family.len()..].starts_with('[')) + }), + "{family} must be argued — it is what this case exists for, and \ + since #977 it is a counted table that an unreached workload drops \ + silently; argued: {}", + argued.join(" ") + ); + } assert!( argued.len() >= 20, - "expected the full table set, argued {}: {}", + "argued {}, fewer than the 20 this workload reached when the bound was \ + written: {}", argued.len(), argued.join(" ") ); From 3218346c76b87fbdfbe65795f8708294a62fa73d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 19:27:24 -0300 Subject: [PATCH 5/8] fix(tests): three more the main-sync port left, and a precompile test that proved the wrong guest MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The full lib suite at 413b3a3b7 (plain libtest, every test regardless of failures) found four red. One was mine to expect; three were pre-existing at the lineage base and invisible to nextest's fail-fast. Three are fixed here. The fourth is a MEASUREMENT and is left red on purpose — see the end. ⛔ THE PRECOMPILE TEST HAS BEEN PROVING THE WRONG GUEST. `a_program_using_a_precompile_is_proved_and_verified` loaded `keccak.elf`, which is `executor/programs/rust/keccak`: a guest whose Cargo.toml depends on `tiny-keccak` and whose `main` hashes in SOFTWARE, issuing no syscall but `commit`. It has never touched a precompile. The accelerator guest is `keccak_precompile`, whose `main` calls `lambda_vm_syscalls::keccak::keccak256` — the `keccak_permute` ecall — over five padding edge cases. ★ And the doc's claim was false BEFORE #977 too; it was merely unfalsifiable. KECCAK and KECCAK_RND were always-on then, so they sat in the table set of every workload whether reached or not, and "which brings KECCAK, KECCAK_RND and KECCAK_RC in" described MACHINE shape while reading as program behaviour. `892c7d1bc` (main's `c2ac5d546`, #977) made them counted and turned a latent falsehood into a visible one — the same shape as SOUNDNESS.md's `T = 24`: a claim no assertion defended. The census that finally said so carries COMMIT[0] and no keccak table at all. Worse, `keccak_precompile.elf` is built by the Makefile's `RUST_PROGRAM_DIRS` wildcard and the prover proved it NOWHERE — its only reference in the tree is `executor/tests/rust.rs`, which runs it in the executor. So the suite had no precompile coverage on the multilinear path at all. Both halves land rather than one: - the precompile case now loads `keccak_precompile.elf` and asserts KECCAK, KECCAK_RND and COMMIT are argued. By PRESENCE, not an ordered census: this guest has never been proved on this path, so there is no measured set, and inventing one would repeat the mistake above. Its prove cost is likewise unmeasured. KECCAK_RC is deliberately not in that list — it is always-on and covered by the prefix, so matching it would let a run reaching no precompile satisfy a check named for one, which is exactly how the software guest passed for as long as it did. - `a_software_hash_guest_argues_the_widest_table_set` keeps the software guest and pins its MEASURED 21-table census, because it is the widest set in the suite: it reaches MEMW, LOAD, STORE, BRANCH and EQ, the five families `the_whole_instruction_set_is_proved_and_verified` does not despite its name, plus public output and two PAGE tables including the stack page. A Rust guest doing ordinary work exercises more of the VM than the asm fixture named for the instruction set. `state_depends_on_every_table_count` read 21 against a literal 20. ✓ VERIFIED cause: #977 moved COMMIT into `TableCounts` — `pub commit: usize` is absent at `892c7d1bc^1` and present now — so `each_count_mut` grew a field and the literal did not. The fix is not 21. It is `statement::NUM_TABLE_KINDS`, the same length `table_count_values` returns as `[u64; NUM_TABLE_KINDS]` and the guest absorbs as `statement_replay::NUM_TABLE_COUNTS`; a bare literal there says nothing about WHICH count is missing and is a second copy of a number the crate already holds. `no_call_site_outside_the_pin_reaches_a_default_alias` flagged `lfm/algebraic_commit.rs`, and it is a FALSE POSITIVE — but not blessed away as one. Both matches are in `#[test] the_host_search_finds_a_valid_nonce_under_rpx` (added by `80d746321`): `GrindingDigest` and `GrindingDigest`. Neither reaches a DEFAULT; both name their hash, which is what §6.7 asks for. The second is a cross-hash CONTROL — BLAKE3 work must not satisfy the RPX predicate — and deleting it makes the test a tautology. The two halves are treated differently on purpose, because the allowlist's own doc says it holds hash-AGNOSTIC items: - `GrindingDigest` joins CONFIG_ALLOWED. Generic over the tag, selects nothing. - `Blake3StarkHash` does NOT. The file joins BLESSED instead, so the concrete tag keeps flagging everywhere else — a site naming it on the block path under an RPX pin is precisely what this gate is for. The BLESSED entry answers the reachability question the list demands rather than stopping at "test-only", which that doc calls one scope too wide: the consumers are `stark::grinding::generate_nonce::` and `is_valid_nonce::`, generic over the tag passed at the call site, so no global is read; and the value never leaves the test body, so the paired-default failure the list exists to catch has no subject here. ⚠ LEFT RED, DELIBERATELY: `the_blake3_tenant_socket_matches_the_record`. `BLAKE3_TENANT_SOCKET` is `Test` and `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08), while the census it is a ratio against is `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days older. The instrument is working: it says the module measures a shape nothing proves. Moving the constant to `Rpx` is not a fix, because `RECORDED = (28, 3)` is the *Test* socket's width pair, and that number's own doc says it moves the headline ratio by a third in the FLATTERING direction if wrong. It needs a re-recorded CHIP CENSUS under the current pin, which is a run, not an edit. --- prover/src/tests/hash_pin_enumeration.rs | 29 ++++ prover/src/tests/multilinear_table_tests.rs | 157 +++++++++++++++----- prover/src/tests/statement_tests.rs | 21 ++- 3 files changed, 167 insertions(+), 40 deletions(-) diff --git a/prover/src/tests/hash_pin_enumeration.rs b/prover/src/tests/hash_pin_enumeration.rs index d0dd85b6a..ea6dcf97b 100644 --- a/prover/src/tests/hash_pin_enumeration.rs +++ b/prover/src/tests/hash_pin_enumeration.rs @@ -79,6 +79,14 @@ const CONFIG_ALLOWED: &[&str] = &[ "CommitmentHash", "StarkHash", "DeviceTreeBackend", + // ★ `GrindingDigest` is generic over the hash tag and selects nothing on + // its own — the same class as `StarkHash` above, and it joined this list + // rather than `BLESSED` for that reason: blessing the FILE would have + // excused every future mention in it, where allowing the hash-agnostic + // GENERIC keeps the gate on the concrete tags a caller pairs it with. + // Added when `80d746321` gave `lfm/algebraic_commit.rs` a host grinding + // test spelling `GrindingDigest`. + "GrindingDigest", ]; /// Every item named from `stark::config` on this line, `use` lists included. @@ -197,6 +205,27 @@ const BLESSED: &[(&str, &str)] = &[ "Host-side BYTE-transcript differentials: the oracle for the machine's \ byte `TranscriptReplay` arm is deliberately the byte transcript.", ), + ( + "lfm/algebraic_commit.rs", + "One mention, and it is a CROSS-HASH CONTROL that names its hash rather \ + than defaulting to it — the opposite of what this gate is for. \ + `the_host_search_finds_a_valid_nonce_under_rpx` (added by `80d746321`) \ + grinds under `GrindingDigest`, then declares \ + `GrindingDigest` to prove a BLAKE3-ground nonce does \ + NOT satisfy the RPX predicate. Delete that second type and the test \ + becomes a tautology: `generate_nonce::` could hash anything \ + and every other assertion would still hold. \ + ✓ REACHABILITY, named as this list demands rather than left at \ + 'test-only': the CONSUMERS are `stark::grinding::generate_nonce::` \ + and `is_valid_nonce::`, both generic over the tag passed at the \ + call site, so no global is read and nothing is handed a defaulted \ + hash. The value never leaves the `#[test]` body — no artifact, no \ + commitment, no trace is built from it — so the paired-default failure \ + this list exists to catch (a default handed to a consumer that follows \ + the pin) has no subject here. `GrindingDigest` itself is hash-agnostic \ + and lives in CONFIG_ALLOWED; this entry covers only the concrete \ + `Blake3StarkHash`, which must keep flagging everywhere else.", + ), ]; /// Every `.rs` under `dir`, relative to `root`. diff --git a/prover/src/tests/multilinear_table_tests.rs b/prover/src/tests/multilinear_table_tests.rs index c483e18e2..9b86539a9 100644 --- a/prover/src/tests/multilinear_table_tests.rs +++ b/prover/src/tests/multilinear_table_tests.rs @@ -525,68 +525,147 @@ fn the_whole_instruction_set_is_proved_and_verified() { } } -/// And over a Rust program that calls the keccak precompile — which brings -/// KECCAK, KECCAK_RND and KECCAK_RC in, **and** writes public output, so the -/// statement's share of the bus is load-bearing here and nowhere else. -/// -/// ⚠ THE ONLY CASE WITHOUT AN ORDERED CENSUS, and deliberately so. The two -/// above are pinned to sets MEASURED at `788f36a19`; this one PASSED that run, -/// so its assertion never fired and never printed its set, and pinning a list -/// nobody has read would be a literal invented to match a bound. It keeps the -/// bound and gains the checks its own doc has always claimed instead. -/// -/// The presence checks are the point: `>= 20` never once asserted that the -/// keccak family or COMMIT is argued here, which is the entire reason this case -/// exists next to the two asm ones. Since #977 those tables are counted, so a -/// workload that stopped reaching the precompile would silently drop them and -/// still clear any bound this case could carry. Both assertions print the whole -/// set, so the run that fails one is also the run that supplies the census. -#[test] -fn a_program_using_a_precompile_is_proved_and_verified() { +/// Proves and verifies the guest at `executor/program_artifacts/rust/.elf`, +/// returning the argued tables by name. +fn prove_and_verify_rust_guest(name: &str) -> Vec { let root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) .parent() .expect("workspace root") - .join("executor/program_artifacts/rust/keccak.elf"); + .join("executor/program_artifacts/rust") + .join(format!("{name}.elf")); let bytes = std::fs::read(&root).unwrap_or_else(|_| panic!("read {}", root.display())); - let elf = Elf::load(&bytes).expect("load keccak.elf"); + let elf = Elf::load(&bytes).unwrap_or_else(|e| panic!("load {name}.elf: {e:?}")); let logs = Executor::new(&elf, vec![]) .expect("executor") .run() .expect("run") .logs; + prove_and_verify_all_tables(elf, &logs) +} - let argued = prove_and_verify_all_tables(elf, &logs); +/// Is `family`, or `family` plus a chunk index, among the argued tables? +/// +/// "Equal, or followed by `[`" — never a bare prefix, which would let +/// `KECCAK_RC` answer for `KECCAK`. +fn argues(argued: &[String], family: &str) -> bool { + argued.iter().any(|n| { + let s = n.as_str(); + s == family || (s.starts_with(family) && s[family.len()..].starts_with('[')) + }) +} + +/// And over a Rust program that calls the keccak PRECOMPILE — the +/// `keccak_permute` ecall — so KECCAK and KECCAK_RND are argued, **and** which +/// writes public output, so the statement's share of the bus is load-bearing. +/// +/// ⛔ THIS CASE PROVED THE WRONG GUEST UNTIL NOW, and the bound is what hid it. +/// It loaded `keccak.elf`, which is `executor/programs/rust/keccak` — a guest +/// whose `Cargo.toml` depends on `tiny-keccak` and whose `main` hashes in +/// SOFTWARE, issuing no syscall but `commit`. It has never touched a precompile. +/// The measured census at `413b3a3b7` carries COMMIT[0] and no keccak table at +/// all, which is what finally said so. +/// +/// ★ And the claim was false BEFORE #977 too — it was merely unfalsifiable. +/// KECCAK and KECCAK_RND were always-on then, so they appeared in the table set +/// of every workload, reached or not, and a doc sentence about which tables the +/// program "brings in" described MACHINE shape while reading like program +/// behaviour. `892c7d1bc` (main's `c2ac5d546`, #977) made them counted, which +/// turned a latent falsehood into a visible one. Another instance of the +/// pattern in `SOUNDNESS.md`: a claim no assertion defended. +/// +/// The accelerator guest it should have used is `keccak_precompile`, whose +/// `main` calls `lambda_vm_syscalls::keccak::keccak256` over five padding edge +/// cases. It is built by the Makefile's `RUST_PROGRAM_DIRS` wildcard like every +/// other guest, and before this commit **nothing in the prover proved it** — its +/// only reference in the tree is `executor/tests/rust.rs`, which runs it in the +/// executor and never proves it. So the suite had no precompile coverage on the +/// multilinear path at all. +/// +/// ⚠ The census here is by PRESENCE, not an ordered list: this guest has never +/// been proved on this path, so there is no measured set to pin, and inventing +/// one would repeat the mistake above. Its cost is likewise unmeasured — five +/// `keccak256` calls including a multi-block input. +/// +/// ✓ The ELF resolves on a CI prover shard exactly as `keccak.elf` does, and +/// this is written down so the next reader does not re-ask: the lineage's +/// prover-tests job runs `make compile-programs-asm`, `make compile-programs-rust` +/// and `make compile-recursion-elfs` before `cargo nextest run`, and +/// `compile-programs-rust` builds every directory under +/// `executor/programs/rust/` through the `RUST_PROGRAM_DIRS` wildcard — this +/// guest included, with no per-program list to extend. +#[test] +fn a_program_using_a_precompile_is_proved_and_verified() { + let argued = prove_and_verify_rust_guest("keccak_precompile"); assert_eq!( always_on_prefix(&argued), ALWAYS_ON_TABLES, "every argued set opens with the always-on tables; argued: {}", argued.join(" ") ); - // The tables this case is ABOUT, by presence rather than by a full census. - // KECCAK_RC is excluded from the prefix match on purpose — it is always-on - // and asserted above, so matching it here would let a run that reaches no - // precompile at all satisfy a check named for one. - for family in ["KECCAK_RND", "COMMIT"] { - // The name is either the bare family or the family plus a chunk index, - // so the match is "equal, or followed by `[`" — never a bare prefix, - // which would let `KECCAK_RC` answer for `KECCAK`. + // KECCAK_RC is deliberately NOT in this list: it is always-on and asserted + // in the prefix above, so matching it here would let a run that reaches no + // precompile satisfy a check named for one — which is exactly how the + // software guest passed as a precompile test for as long as it did. + for family in ["KECCAK", "KECCAK_RND", "COMMIT"] { assert!( - argued.iter().any(|n| { - let s = n.as_str(); - s == family || (s.starts_with(family) && s[family.len()..].starts_with('[')) - }), + argues(&argued, family), "{family} must be argued — it is what this case exists for, and \ since #977 it is a counted table that an unreached workload drops \ silently; argued: {}", argued.join(" ") ); } - assert!( - argued.len() >= 20, - "argued {}, fewer than the 20 this workload reached when the bound was \ - written: {}", - argued.len(), - argued.join(" ") +} + +/// The SOFTWARE-hash guest, kept because it is the widest live table set in the +/// suite — and it is the one the precompile case above used to prove. +/// +/// `executor/programs/rust/keccak` hashes with `tiny-keccak` in guest code, so +/// it reaches no accelerator and argues the RV64 core broadly instead: 21 +/// tables, including MEMW, LOAD, STORE, BRANCH and EQ — the five families +/// `the_whole_instruction_set_is_proved_and_verified` does NOT reach despite its +/// name. A Rust guest doing ordinary work exercises more of the VM than the asm +/// fixture named for the instruction set, which is worth keeping a case for. +/// +/// It also carries public output (COMMIT[0]) and two PAGE tables, one of them +/// the stack page — the only case here that does either. +/// +/// MEASURED at `413b3a3b7`, box, CPU-only, no campaign env. +#[test] +fn a_software_hash_guest_argues_the_widest_table_set() { + let argued = prove_and_verify_rust_guest("keccak"); + assert_eq!( + argued, + [ + "BITWISE", + "DECODE", + "KECCAK_RC", + "REGISTER", + "HALT", + "COMMIT[0]", + "CPU[0]", + "LT[0]", + "SHIFT[0]", + "MEMW[0]", + "MEMW_A[0]", + "LOAD[0]", + "MUL[0]", + "BRANCH[0]", + "PAGE:0x0", + "PAGE:0xfffffffffffc0000", + "MEMW_R[0]", + "EQ[0]", + "BYTEWISE[0]", + "STORE[0]", + "CPU32[0]", + ], + "the argued table set moved — a table appeared, vanished, or the \ + sub-proof order changed. NOTE what is absent and must stay absent: \ + KECCAK, KECCAK_RND, ECSM, ECDAS and HINT. This guest hashes in \ + software, and an accelerator appearing here means it is proving \ + something else — which is precisely the confusion the precompile case \ + above lived in. A separate `!argues(..)` loop would restate the list \ + and could only fire after this assertion already had." ); } diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index 1ae96d2ea..31068ebff 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -131,6 +131,21 @@ fn each_count_mut(counts: &mut TableCounts) -> Vec<(&'static str, &mut usize)> { /// destructured in `absorb_statement` and then left out of the array it /// absorbs compiles clean and changes nothing about the state, which is a /// prover-chosen number the verifier would no longer be bound to. +/// +/// ★ THE PROBE COUNT IS THE CONSTANT'S, NOT A LITERAL. It was `20` and read +/// 21, because the main-sync merge `892c7d1bc` (main's `c2ac5d546`, #977) took +/// `FIXED_TABLE_COUNT` 11 -> 5 and moved COMMIT into `TableCounts` alongside +/// the five accelerators already there — ✓ VERIFIED, `pub commit: usize` is +/// absent at `892c7d1bc^1` and present now. `each_count_mut` grew the field and +/// the literal did not. +/// +/// A bare literal here is the wrong shape twice over: it says nothing about +/// WHICH count is missing, and it is a second copy of a length +/// `statement::NUM_TABLE_KINDS` already holds — the same number +/// `table_count_values` returns as `[u64; NUM_TABLE_KINDS]` and the guest +/// absorbs as `statement_replay::NUM_TABLE_COUNTS`. Pinned against the +/// constant, a field added to `TableCounts` without a probe fails here, and one +/// added to the encoding without a field fails to compile. #[test] fn state_depends_on_every_table_count() { let baseline = state_after_absorb(b"elf", b"out", &sample_counts(), 1, &sample_ranges(), 7); @@ -139,7 +154,11 @@ fn state_depends_on_every_table_count() { .into_iter() .map(|(name, _)| name) .collect(); - assert_eq!(names.len(), 20, "every count must be probed"); + assert_eq!( + names.len(), + crate::statement::NUM_TABLE_KINDS, + "every count the statement encodes must be probed; probing {names:?}" + ); for name in names { let mut counts = sample_counts(); From c8c7c036e95e19253642f486a512bcd129cabda1 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 19:35:49 -0300 Subject: [PATCH 6/8] test(lfm): the tenant socket census measures before it asserts, and names its hasher MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `the_blake3_tenant_socket_matches_the_record` is red and is right to be: `BLAKE3_TENANT_SOCKET` is `Test`, `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08), and the record this whole census is a ratio against is `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days older than the pin. The instrument is doing its job: it says the module may be measuring a shape nothing proves. It could not SAY what the shape is, though. The socket assertion fires before any tenant is built, so a red run yielded no number at all — and the obvious cheap run does not yield one either. `wrap_tests::the_wrap_census` reaches `lfm_chip_census`, which is `lfm_chip_census_with_hasher(program, HasherKind::default())`, and `HasherKind::default()` is `Test` (`hash.rs:251`, `#[default] Test = 0`). It reports this very pair under ANY pin: a confirmation that cannot fail, on the one number whose error is flattering. That symbol is itself one of the three `IMPLIED_HASH_SYMBOLS` the §6.7 gate hunts for, which is what a census defaulting its hasher looks like from the other side. So the test now prints every tenant's MEASURED `LFM_HASH` width before it asserts anything, one line per tenant, each naming its `HasherKind` and flagging the one that IS `BLOCK_HASHER`. A width without the tag that produced it is the mistake this finding is about, so no line omits it. All eight tenants are walked; both halves already go through `tenant.airs` + `tenant_tables` in the algebraic and non-algebraic loops elsewhere in the module, so this adds no new construction. Nothing is re-blessed. `RECORDED` keeps its value and the assertions keep their polarity, because the replacement pair has not been measured yet — that is one cheap CPU run away, and this commit is what makes that run informative. ⛔ AND THE 2^24 REAL-BLOCK RUN IS NOT NEEDED, which the doc comment now says so nobody schedules it later. The quantities split, and only the first is in question: socket WIDTH (main, aux) depends on the HasherKind alone static per tag idle socket HEIGHT (4 rows) the group floor static non-hash heights, 670,468,916 the workload socket-independent the 0.774x lever-0 ratio arithmetic over the above recompute `tenant_log_heights` overrides `h[HASH_SLOT]` only for ALGEBRAIC tenants and every non-hash height is socket-independent, so `RECORDED_WRAP_LOG_HEIGHTS` survives the pin move intact. What is stale is one width pair, the socket identity, and the ratio that is arithmetic over them. The stakes are in the doc too, because the direction matters: `wrap_tests` already puts the socket at 436 columns for RPO against the 28 of an idle `Test`, and this module's own note says mistaking the idle chip for a live one moves lever 0 from 0.774x to 0.632x — bigger, i.e. the flattering way. --- prover/src/lfm/per_table_census_tests.rs | 79 +++++++++++++++++++++++- 1 file changed, 77 insertions(+), 2 deletions(-) diff --git a/prover/src/lfm/per_table_census_tests.rs b/prover/src/lfm/per_table_census_tests.rs index 15256b761..a8ca31e58 100644 --- a/prover/src/lfm/per_table_census_tests.rs +++ b/prover/src/lfm/per_table_census_tests.rs @@ -608,12 +608,86 @@ fn the_block_rule_is_hash_invariant_on_every_tenant_group() { /// This is the one number in the census that, if wrong, moves the headline /// ratio by a third and in the flattering direction, so it is asserted against /// the recorded run rather than left to the tenant table's spelling. +/// +/// ⚠⚠ **THIS TEST IS RED, AND IT IS RIGHT TO BE.** `BLAKE3_TENANT_SOCKET` is +/// `Test`; `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08). The +/// record this census is a ratio against is +/// `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days +/// older than the pin. The assertion is not a stale literal to re-bless; it is +/// the instrument saying the module may be measuring a shape nothing proves. +/// Moving the constant to `Rpx` is NOT the fix: `RECORDED` is the *`Test`* +/// socket's width pair, and `wrap_tests.rs`'s own note puts the socket at 436 +/// columns for RPO against 28 idle — so the chip this census calls absent could +/// be present, in the direction the paragraph above calls flattering. +/// +/// ★ **WHAT IT NEEDS, AND WHAT IT DOES NOT.** The panel below prints every +/// tenant's measured `LFM_HASH` width beside the record, flagging the one whose +/// hasher IS the pin, so one cheap CPU run settles the pair. It prints BEFORE +/// the assertions so a red run still yields the measurement. +/// +/// ⛔ **DO NOT schedule the 2^24 real-block run for this.** The quantities +/// split, and only the first is in question: +/// +/// | quantity | depends on | needs a re-record? | +/// |---|---|---| +/// | socket WIDTH (main, aux) | the `HasherKind` alone | no — static per tag | +/// | idle socket HEIGHT (4 rows, 0 used) | the group floor | no — static | +/// | non-hash heights, the 670,468,916 non-hash cells | the workload | no — socket-independent | +/// | the 0.774× lever-0 ratio | arithmetic over the above | no — recompute | +/// +/// `tenant_log_heights` overrides `h[HASH_SLOT]` only for ALGEBRAIC tenants, and +/// every non-hash height is socket-independent, so `RECORDED_WRAP_LOG_HEIGHTS` +/// survives the pin move intact. What is stale is one width pair, the socket +/// identity, and the ratio that is arithmetic over them. +/// +/// ⚠ And the obvious cheap run does NOT answer it: `wrap_tests::the_wrap_census` +/// reaches `lfm_chip_census`, which is `lfm_chip_census_with_hasher(program, +/// HasherKind::default())` and `HasherKind::default()` is `Test` — so it reports +/// this very pair under ANY pin. That is why the panel below names its hasher on +/// every line: a census that does not is not evidence about `BLOCK_HASHER`. #[test] fn the_blake3_tenant_socket_matches_the_record() { /// `LFM_HASH` as `tip-wrappt-24.stdout`'s CHIP CENSUS reports it: 28 main /// value columns over the 13-column preprocessed prefix, 3 ext aux. const RECORDED: (usize, usize) = (28, 3); + let opts = wrap_options(); + + // ★ MEASURED FIRST, ASSERTED SECOND — the ordering is the point. The socket + // assertion below fires before any tenant is built, so while it is red this + // panel is the only way the measurement reaches a log. Every line names its + // hasher, because a width without the tag that produced it is the mistake + // this whole finding is about. + println!( + "\n★ LFM_HASH SOCKET WIDTH BY TENANT — BLOCK_HASHER is {:?}", + crate::hash_pin::BLOCK_HASHER + ); + for tenant in TENANTS.iter() { + let airs = tenant.airs(&opts); + let tables = tenant_tables(tenant, &airs, &tenant.present_log_heights()); + let hash = tables + .iter() + .find(|t| t.name == "LFM_HASH") + .expect("every tenant carries LFM_HASH"); + println!( + " {:>8} hasher {:<9?} algebraic {:<5} LFM_HASH {:>5} main + {} ext aux{}", + tenant.label, + tenant.hasher, + tenant.algebraic, + hash.main_cols, + hash.aux_cols, + if tenant.hasher == crate::hash_pin::BLOCK_HASHER { + " <== THE PIN" + } else { + "" + } + ); + } + println!( + " RECORDED {RECORDED:?} — tip-wrappt-24.stdout, 2026-08-21, taken \ + BEFORE the RPX pin of 603c1e155 (2026-09-08)" + ); + // ★ The tenant's socket IS the pin's, not a value chosen here. A branch that // re-pins `BLOCK_HASHER` moves what a BLAKE3-tenant wrap proof actually // carries, and this census would then be measuring a shape nothing proves. @@ -621,10 +695,11 @@ fn the_blake3_tenant_socket_matches_the_record() { BLAKE3_TENANT_SOCKET, crate::hash_pin::BLOCK_HASHER, "the BLAKE3 tenant's LFM_HASH socket must be the build's own pin — the \ - recorded census this census is a ratio against was produced under it" + recorded census this census is a ratio against was produced under it. \ + The panel above has the measured width for every tenant; read the line \ + marked THE PIN" ); - let opts = wrap_options(); for tenant in TENANTS.iter().filter(|t| !t.algebraic) { let airs = tenant.airs(&opts); let tables = tenant_tables(tenant, &airs, &tenant.present_log_heights()); From 05f0500a213bb58660da2e1fbd0fad1e4c46d54f Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 21 Sep 2026 20:27:20 -0300 Subject: [PATCH 7/8] fix(lfm): the tenant socket assertion tied a counterfactual to the live pin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MEASURED at c8c7c036e on the box, CPU-only, env clean — `LFM_HASH` main columns by socket: Test 28, Rpx 316, Rpo 436, Poseidon 612, 3 ext aux throughout. Two things fall out that nobody had: the pinned socket is 316, not the 436 the RPO figure in `wrap_tests.rs` would have implied, and it is 11x the idle 28 rather than the 106x a BLAKE3 socket would have been. ⛔ AND NOTHING NEEDS RE-BLESSING. `the_blake3_tenant_socket_matches_the_record` was red because its assertion was wrong, not because its numbers were stale. Both obvious repairs would have been mistakes: - Re-bless the pair. No: `RECORDED = (28, 3)` is a faithful record of the BLAKE3 tenant, and that tenant did not change when the block path's pin did. - Point `BLAKE3_TENANT_SOCKET` at `BLOCK_HASHER`. No, and this is the one worth writing down. A tenant's socket width is a property of the build that PRODUCED the wrap proof, not of the build reading it. A byte-arm program emits no `Instr::Hash` and never consults the socket, so a BLAKE3-committing build has no reason to instantiate an algebraic one — `Test` is that build's own pin. Giving this tenant a 316-column socket would price a build nobody would ship, a socket paid for and never used, and would move the lever-0 baseline on the way past. The 0.774x stands, unrecomputed, because its inputs did not move. So the constant and the pair both keep their values and the assertion is replaced. It required assert_eq!(BLAKE3_TENANT_SOCKET, hash_pin::BLOCK_HASHER) which ties a COUNTERFACTUAL tenant to the CURRENT build — a category error a pin move was always going to expose, and `603c1e155` (2026-09-08) exposed it. What it was reaching for is checkable, and is now two assertions that can each fail. ✓ VERIFIED by reading: `hash_pin::BlockStarkHash = RpxStarkHash`, so `BLOCK_COMMITMENT_HASH` is `Rpx256`, and `WrapHash::production()` maps Rpo256/Rpx256/Poseidon to `Algebraic` — the production wrap EMITS `Instr::Hash` and USES the socket, so it is the RPX tenant and the BLAKE3 tenant is the comparison arm lever 0 is a ratio against. - `WrapHash::production() == WrapHash::Algebraic`. A commitment pin moved to a byte hash makes production a BYTE tenant: baseline and subject swap places and every ratio in this module needs re-reading before it is quoted. - some tenant is algebraic AND at `BLOCK_HASHER`. If the TENANTS table stops covering the pin, the census prices only builds nobody ships. The message prints the pin and the algebraic tenants so the failure names its own cause. The panel from c8c7c036e stays and keeps printing before any assertion, so a future red run yields numbers rather than a bare mismatch. Its measured widths are now in the doc comment, as is the reason the obvious cheap census cannot answer this question: `lfm_chip_census` is `lfm_chip_census_with_hasher(program, HasherKind::default())` and that default is `Test`, so it reports 28 under ANY pin. ⚠ The fork is recorded rather than hidden, because it is a modelling judgement with a campaign number attached: taking the other reading is two lines, `BLAKE3_TENANT_SOCKET = BLOCK_HASHER` and `RECORDED = (316, 3)`, and would put lever 0 near 0.757x — ? INFERRED, from a linear fit of the doc's own two points (28 cols -> 16 blocks/query, 2,980 -> 1,201) and then the algebra of its two stated ratios, never measured. The module's own gate recomputes that number from the tenant bills and prints it, so quote the gate and not this estimate. Either way it clears the gate's thresholds (> 0.4255, within 0.30..0.95). --- prover/src/lfm/per_table_census_tests.rs | 112 ++++++++++++++++++----- 1 file changed, 88 insertions(+), 24 deletions(-) diff --git a/prover/src/lfm/per_table_census_tests.rs b/prover/src/lfm/per_table_census_tests.rs index a8ca31e58..4c6f98102 100644 --- a/prover/src/lfm/per_table_census_tests.rs +++ b/prover/src/lfm/per_table_census_tests.rs @@ -609,21 +609,35 @@ fn the_block_rule_is_hash_invariant_on_every_tenant_group() { /// ratio by a third and in the flattering direction, so it is asserted against /// the recorded run rather than left to the tenant table's spelling. /// -/// ⚠⚠ **THIS TEST IS RED, AND IT IS RIGHT TO BE.** `BLAKE3_TENANT_SOCKET` is -/// `Test`; `BLOCK_HASHER` has been `Rpx` since `603c1e155` (2026-09-08). The -/// record this census is a ratio against is -/// `bench_cache/optladder_2026-08-21/TIP/tip-wrappt-24.stdout` — eighteen days -/// older than the pin. The assertion is not a stale literal to re-bless; it is -/// the instrument saying the module may be measuring a shape nothing proves. -/// Moving the constant to `Rpx` is NOT the fix: `RECORDED` is the *`Test`* -/// socket's width pair, and `wrap_tests.rs`'s own note puts the socket at 436 -/// columns for RPO against 28 idle — so the chip this census calls absent could -/// be present, in the direction the paragraph above calls flattering. +/// ⚠⚠ **THIS TEST WAS RED, AND THE DEFECT WAS THE ASSERTION, NOT THE NUMBER.** +/// It required `BLAKE3_TENANT_SOCKET == hash_pin::BLOCK_HASHER`, which has been +/// false since `603c1e155` (2026-09-08) re-pinned the block path to RPX. The +/// obvious readings were both wrong: /// -/// ★ **WHAT IT NEEDS, AND WHAT IT DOES NOT.** The panel below prints every -/// tenant's measured `LFM_HASH` width beside the record, flagging the one whose -/// hasher IS the pin, so one cheap CPU run settles the pair. It prints BEFORE -/// the assertions so a red run still yields the measurement. +/// - *Re-bless the pair.* No. `RECORDED` is a faithful record of the BLAKE3 +/// tenant, and that tenant did not change when the block path's pin did. +/// - *Point the constant at `Rpx`.* No, and this is the interesting one. A +/// tenant's socket width is a property of the build that PRODUCED the wrap +/// proof, not of the build reading it. A byte-arm program emits no +/// `Instr::Hash` and never consults the socket, so a BLAKE3-committing build +/// has no reason to instantiate an algebraic one. Giving this tenant a +/// 316-column socket would price a build nobody would ship and would move the +/// lever-0 baseline while doing it. +/// +/// So the constant and the pair both STAND, and the 0.774× stands with them. +/// What is replaced is the assertion, which tied a COUNTERFACTUAL tenant to the +/// CURRENT build's pin — a category error that a pin move was always going to +/// expose. The check it was reaching for is the one now in the body: production +/// must be the ALGEBRAIC tenant. +/// +/// ★ **THE MEASURED PANEL**, printed BEFORE any assertion so a red run still +/// yields numbers. ✓ MEASURED at `c8c7c036e` on the box, CPU-only, env clean — +/// `LFM_HASH` main columns by socket: **Test 28, Rpx 316, Rpo 436, Poseidon +/// 612**, 3 ext aux throughout. Two things fall out. The pinned socket is 316, +/// not the 436 the RPO figure in `wrap_tests.rs` would have suggested. And it +/// is 11× the idle 28 rather than the 106× a BLAKE3 socket would have been, so +/// the failure mode this test's first paragraph warns about is real but far +/// smaller than the 2,980-column case that motivated it. /// /// ⛔ **DO NOT schedule the 2^24 real-block run for this.** The quantities /// split, and only the first is in question: @@ -637,8 +651,16 @@ fn the_block_rule_is_hash_invariant_on_every_tenant_group() { /// /// `tenant_log_heights` overrides `h[HASH_SLOT]` only for ALGEBRAIC tenants, and /// every non-hash height is socket-independent, so `RECORDED_WRAP_LOG_HEIGHTS` -/// survives the pin move intact. What is stale is one width pair, the socket -/// identity, and the ratio that is arithmetic over them. +/// survives the pin move intact. +/// +/// ✓ And in the end NOTHING in that table needed re-recording — the panel +/// settled it. The question the split was framed against, "which of these does +/// the pin move invalidate?", turns out to have the answer "none", because the +/// BLAKE3 tenant is modelled at its OWN build's pin and not at this build's. +/// The table stays because it is the reasoning that would be needed again if +/// the COMMITMENT pin moved, which is the move that would actually reach these +/// numbers — and because it is what says the expensive run is never the answer +/// to a socket-width question. /// /// ⚠ And the obvious cheap run does NOT answer it: `wrap_tests::the_wrap_census` /// reaches `lfm_chip_census`, which is `lfm_chip_census_with_hasher(program, @@ -688,16 +710,58 @@ fn the_blake3_tenant_socket_matches_the_record() { BEFORE the RPX pin of 603c1e155 (2026-09-08)" ); - // ★ The tenant's socket IS the pin's, not a value chosen here. A branch that - // re-pins `BLOCK_HASHER` moves what a BLAKE3-tenant wrap proof actually - // carries, and this census would then be measuring a shape nothing proves. + // ★★ WHAT THE OLD ASSERTION GOT WRONG, and it is a modelling error rather + // than a stale number. It read + // + // assert_eq!(BLAKE3_TENANT_SOCKET, hash_pin::BLOCK_HASHER) + // + // — "the BLAKE3 tenant's socket must be the build's own pin". That ties a + // COUNTERFACTUAL tenant to the CURRENT build. The BLAKE3 tenant models a + // wrap proof produced by a BLAKE3-COMMITTING build, and a tenant's socket + // width is a property of the build that PRODUCED the proof, not of the one + // reading it. A byte-arm program emits no `Instr::Hash` and never consults + // the socket, so a BLAKE3-committing build has no reason to instantiate an + // algebraic one: `Test` is that build's own pin, and 28 columns is a + // faithful record of it. Re-pointing the constant at `Rpx` would price a + // build nobody would ship — a 316-column socket paid for and never used — + // and would move the lever-0 baseline in the process. + // + // So NOTHING here is re-blessed: `BLAKE3_TENANT_SOCKET` stays `Test`, + // `RECORDED` stays `(28, 3)`, and the 0.774× the module reports stands. The + // panel above is what settles that, and the measured widths are + // Test 28 / Rpx 316 / Rpo 436 / Poseidon 612 main, 3 ext aux throughout. + // + // ★ WHAT THE ASSERTION WAS REACHING FOR is below, and it is checkable: + // production must be the ALGEBRAIC tenant, and one tenant must model it. + // ✓ VERIFIED at `c8c7c036e`: `hash_pin::BlockStarkHash = RpxStarkHash`, so + // `BLOCK_COMMITMENT_HASH` is `Rpx256`, and `WrapHash::production()` maps + // Rpo256/Rpx256/Poseidon to `Algebraic`. The production wrap therefore + // EMITS `Instr::Hash` and USES the socket — it is the RPX tenant, not the + // BLAKE3 one. Both halves can fail: a pin moved to a byte commitment hash + // fails the first, and a TENANTS table that stopped covering the pin fails + // the second. assert_eq!( - BLAKE3_TENANT_SOCKET, + WrapHash::production(), + WrapHash::Algebraic, + "the production wrap is the tenant this census prices as `algebraic`. \ + If `BLOCK_COMMITMENT_HASH` has moved to a byte hash, production is a \ + BYTE tenant, the baseline and the subject of the lever-0 ratio swap \ + places, and every ratio in this module needs re-reading before it is \ + quoted" + ); + assert!( + TENANTS + .iter() + .any(|t| t.algebraic && t.hasher == crate::hash_pin::BLOCK_HASHER), + "no tenant models the production wrap: the pin is {:?} and the \ + algebraic tenants are {:?}. The census would then be pricing only \ + builds nobody ships", crate::hash_pin::BLOCK_HASHER, - "the BLAKE3 tenant's LFM_HASH socket must be the build's own pin — the \ - recorded census this census is a ratio against was produced under it. \ - The panel above has the measured width for every tenant; read the line \ - marked THE PIN" + TENANTS + .iter() + .filter(|t| t.algebraic) + .map(|t| (t.label, t.hasher)) + .collect::>() ); for tenant in TENANTS.iter().filter(|t| !t.algebraic) { From b420ee950f07496215d9766025fc0b018fe492cf Mon Sep 17 00:00:00 2001 From: MauroFab Date: Sun, 20 Sep 2026 13:54:04 -0300 Subject: [PATCH 8/8] fix(test): the host KAT punned its result type, and LP64 made it matter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `run_grind` declared its result `uint64_t` and handed the address to the kernel as `volatile unsigned long long *`. Those are the same type on Darwin/arm64 and different types of the same width on LP64 glibc, so on Linux the cast type-punned; with `#include "rpx.cu"` putting the whole kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to assume a write through `unsigned long long *` could not touch an `unsigned long`, and to keep `result` in a register across the inlined call. It did. `run_grind` returned UINT64_MAX for every input, so layer 8's two checks per vector that expect the SENTINEL passed VACUOUSLY while the two that expect a found nonce failed. Six rows, at every sha back to the gated base c00342c1f, on a target that passes on a clang/arm64 laptop where the two types coincide. Measured on the box at this sha: -O2 6 FAILURE(S) -O2 -fno-strict-aliasing ALL HOST KAT CHECKS PASS -O0 ALL HOST KAT CHECKS PASS None of it was ever a statement about the device grind. This file is a HOST replay of the kernel source through `cuda_host_shim.h` — no nvcc, no cubin, no device — so the defect was in the harness holding the result, not in the kernel it tests. The production path re-validates every device nonce with the host predicate, and the block pins read `host fallbacks 0` throughout. `crypto/math-cuda/tests/host_kat/` holds exactly one instance of the pattern and this is it: the shim's `atomicMin` takes `unsigned long long *` as a parameter, and the kernels' casts there only drop `volatile` from an already-matching type. Test-only; no production code and no proof bytes move. It also unblocks this lineage's CI `host-kat` job, which has been failing since the device grind landed. (cherry picked from commit 90a38eccdca0c23ca195189b4dc55db9b10d39c8) --- .../math-cuda/tests/host_kat/rpx_host_kat.cpp | 26 ++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp b/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp index 7cdf8cbd5..5f69ae403 100644 --- a/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp +++ b/crypto/math-cuda/tests/host_kat/rpx_host_kat.cpp @@ -1097,7 +1097,31 @@ void permute_probe_matches_the_oracle_table() { // --------------------------------------------------------------------------- uint64_t run_grind(const uint64_t inner[4], uint8_t factor, uint64_t base, uint64_t count) { const uint64_t limit = (uint64_t)1 << (64 - factor); - uint64_t result = UINT64_MAX; + // ⛔⛔ `unsigned long long`, NOT `uint64_t`, AND THAT DIFFERENCE WAS THE BUG. + // The kernel takes `volatile unsigned long long *` because that is the type + // CUDA's `atomicMin` overload wants, so this object's address is handed out + // under it. `uint64_t` is `unsigned long long` on Darwin/arm64 and + // `unsigned long` on LP64 glibc — a DIFFERENT type of the same width — so on + // Linux the cast type-punned, and with `#include "rpx.cu"` putting the whole + // kernel in this translation unit, GCC 13.3 at -O2 was free under TBAA to + // assume a write through `unsigned long long *` could not touch an + // `unsigned long`, and to keep `result` in a register across the inlined call. + // + // It did. `run_grind` returned `UINT64_MAX` for every input on the box, so + // every check below that expects the SENTINEL passed vacuously while every + // check that expects a FOUND nonce failed — six rows, at every sha back to + // the gated base `c00342c1f`, while the same source passed on a clang/arm64 + // laptop where the two types coincide. Measured on the box 2026-09-20: + // `-O2` → 6 failures; `-O2 -fno-strict-aliasing` → all pass; `-O0` → all pass. + // + // ⚠ NONE OF THAT WAS EVER A STATEMENT ABOUT THE DEVICE GRIND. This file is a + // HOST replay of the kernel source through `cuda_host_shim.h`; the defect + // was in the harness holding the result, not in the kernel it was testing. + // ⛔ Do not "tidy" this back to `uint64_t`: matching the pointer type the + // kernel is given is what makes the access well-defined, and the box gate + // carries a mutation that restores `uint64_t` and requires those six rows + // back — so the tidy-up would be caught, loudly, by a red nobody wants again. + unsigned long long result = UINT64_MAX; CUDA_HOST_SINGLE_THREAD(); rpx_grind_search(inner, limit, base, count, (volatile unsigned long long *)&result); return result;