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; 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/per_table_census_tests.rs b/prover/src/lfm/per_table_census_tests.rs index 15256b761..4c6f98102 100644 --- a/prover/src/lfm/per_table_census_tests.rs +++ b/prover/src/lfm/per_table_census_tests.rs @@ -608,23 +608,162 @@ 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 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: +/// +/// - *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: +/// +/// | 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. +/// +/// ✓ 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, +/// 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); - // ★ 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. + 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)" + ); + + // ★★ 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" + TENANTS + .iter() + .filter(|t| t.algebraic) + .map(|t| (t.label, t.hasher)) + .collect::>() ); - 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()); 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..dbecbcb8b 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,39 @@ 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 +804,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 ); 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 763b6a954..9b86539a9 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,38 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { ) .expect("the whole table set verifies"); - count + 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 @@ -371,39 +420,253 @@ fn prove_and_verify_all_tables(elf: Elf, logs: &[Log]) -> usize { /// 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 >= 20, "expected the full table set, argued {argued}"); + 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"); - assert!(prove_and_verify_all_tables(elf, &logs) >= 20); + 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(" ") + ); + 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. -#[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) +} - assert!(prove_and_verify_all_tables(elf, &logs) >= 20); +/// 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(" ") + ); + // 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!( + 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(" ") + ); + } +} + +/// 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." + ); } /// A proof is only a proof if it can leave the process. Round-trips a real 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();