fix(tests): three more the main-sync port left, and a precompile test that proved the wrong guest

The full lib suite at 413b3a3 (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<RpxStarkHash>` and
`GrindingDigest<Blake3StarkHash>`. 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::<T>` and `is_valid_nonce::<T>`, 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.

Author: MauroToscano

prover/src/tests/hash_pin_enumeration.rs

@@ -79,6 +79,14 @@ const CONFIG_ALLOWED: &[&str] = &[
     "CommitmentHash",
     "StarkHash",
     "DeviceTreeBackend",
+    // ★ `GrindingDigest<H>` 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<RpxStarkHash>`.
+    "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<RpxStarkHash>`, then declares \
+         `GrindingDigest<Blake3StarkHash>` to prove a BLAKE3-ground nonce does \
+         NOT satisfy the RPX predicate. Delete that second type and the test \
+         becomes a tautology: `generate_nonce::<RpxGrind>` 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::<T>` \
+         and `is_valid_nonce::<T>`, 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`.

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/<name>.elf`,
+/// returning the argued tables by name.
+fn prove_and_verify_rust_guest(name: &str) -> Vec<String> {
     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."
     );
 }
 

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();