Feat/is whh

docs/continuations_design.md

@@ -577,8 +577,9 @@ becomes an **explicit verifier action**:
 - **Reconstruct the output** by concatenating the per-epoch commit slices (each
   commit-bus-bound, contiguous via the x254 chain).
 - The verifier also `validate()`s `table_counts` — which since per-epoch table skipping
-  means *only* that CPU and MEMW_R are present and that no accelerator claims more than
-  one table, not that every table is there — and never trusts a prover-supplied
+  means *only* that CPU and MEMW_R are present and that no accelerator, and no IS_WH,
+  claims more than one table (for IS_WH that cap is what bounds its multiplicity sum),
+  not that every table is there — and never trusts a prover-supplied
   page config (continuation epochs have none — PAGE is skipped under the L2G
   bookend, so `page_configs` is always empty).
 

executor/programs/asm/test_keccak_64k.s

@@ -0,0 +1,41 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+.Lfunc_end0:
+	.globl	main
+main:
+	# Place the 200-byte Keccak state (25 × u64) below sp so that it straddles
+	# a 64 KiB boundary: lanes 0..11 sit below it and lanes 12..24 above, so
+	# the 25 state pointers carry two different (Word, Half) keys.
+	li	t2, -65536
+	and	s0, sp, t2
+	addi	s0, s0, -96
+
+	# Zero out the state (200 bytes = 25 doublewords)
+	mv	t0, s0
+	li	t1, 25
+.Lzero_loop:
+	sd	zero, 0(t0)
+	addi	t0, t0, 8
+	addi	t1, t1, -1
+	bnez	t1, .Lzero_loop
+
+	# Call keccak-f[1600] permutation
+	# a0 = pointer to 200-byte state
+	# a7 = syscall number (0xFFFFFFFFFFFFFFFE = u64::MAX - 1)
+	mv	a0, s0
+	li	a7, -2
+	ecall
+
+	# Commit the post-permutation state so the test can verify the KAT.
+	# Commit syscall: a0=fd(1), a1=buf_addr, a2=count, a7=64
+	li	a0, 1
+	mv	a1, s0
+	li	a2, 200
+	li	a7, 64
+	ecall
+
+	# Halt
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

executor/tests/asm.rs

@@ -880,11 +880,10 @@ fn test_sub_underflow() {
 
 // ==================== Keccak Precompile ====================
 
-#[test]
-fn test_keccak() {
-    // Runs keccak-f[1600] on a zeroed state and commits the 200-byte result.
-    // Expected output is the FIPS-202 zero-input KAT.
-    let elf_data = std::fs::read("./program_artifacts/asm/test_keccak.elf").unwrap();
+/// Runs `name`, which applies keccak-f[1600] to a zeroed state and commits the
+/// 200-byte result, and checks the output against the FIPS-202 zero-input KAT.
+fn assert_keccak_zero_state_kat(name: &str) {
+    let elf_data = std::fs::read(format!("./program_artifacts/asm/{name}.elf")).unwrap();
     let program = Elf::load(&elf_data).unwrap();
     let executor = Executor::new(&program, vec![]).expect("Failed to create executor");
     let result = executor.run().expect("Failed to run program");
@@ -924,6 +923,17 @@ fn test_keccak() {
     assert_eq!(result.return_values.register_values.0, 0);
 }
 
+#[test]
+fn test_keccak() {
+    assert_keccak_zero_state_kat("test_keccak");
+}
+
+/// Same KAT with the state straddling a 64 KiB boundary.
+#[test]
+fn test_keccak_64k() {
+    assert_keccak_zero_state_kat("test_keccak_64k");
+}
+
 #[test]
 fn test_run_epochs_splits_execution_into_n_cycle_epochs() {
     let elf_data = std::fs::read("./program_artifacts/asm/basic_program.elf").unwrap();

prover/src/auto_storage.rs

@@ -108,8 +108,8 @@ fn aux_cols(bus_count: usize) -> u64 {
 /// consumer sums or sorts — and it does not track `air_trace_pairs`.
 ///
 /// Note this list models only the tables `TableLengths` carries: there is no
-/// entry for eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas or
-/// hint, so a run dominated by one of those is under-estimated.
+/// entry for eq, bytewise, store, cpu32, keccak, keccak_rnd, ecsm, ecdas, hint
+/// or is_wh, so a run dominated by one of those is under-estimated.
 fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
     let bitwise_rows = BITWISE_ROWS as u64;
     let register_rows = NUM_REGISTER_ADDRESSES.next_power_of_two() as u64;

prover/src/constraints/templates.rs

@@ -109,6 +109,7 @@ impl core::ops::Deref for AddTerms {
 /// - Constants: `AddOperand::constant(42)` → lo=42, hi=0
 /// - Word → DWordWL: `AddOperand::from_word(col)` → lo=col, hi=0
 /// - DWordHL → DWordWL: `AddOperand::from_dword_hl(col)` → repack 4 halves
+/// - DWordWHH → DWordWL: `AddOperand::from_dword_whh(col)` → repack 2 halves + word
 /// - DWordBL → DWordWL: `AddOperand::from_dword_bl(col)` → repack 8 bytes
 /// - Expressions: `AddOperand::linear(...)` → arbitrary linear combinations
 #[derive(Debug, Clone, Copy)]
@@ -185,6 +186,29 @@ impl AddOperand {
         }
     }
 
+    /// DWordWHH → DWordWL: repack the two low halves into a word; the high
+    /// word is already a single column.
+    /// lo = h[0] + 2^16 * h[1]
+    /// hi = w[2]
+    pub fn from_dword_whh(start_column: usize) -> Self {
+        AddOperand::Linear {
+            lo: AddTerms::of(&[
+                AddLinearTerm::Column {
+                    coefficient: 1,
+                    column: start_column,
+                },
+                AddLinearTerm::Column {
+                    coefficient: 1 << 16,
+                    column: start_column + 1,
+                },
+            ]),
+            hi: AddTerms::of(&[AddLinearTerm::Column {
+                coefficient: 1,
+                column: start_column + 2,
+            }]),
+        }
+    }
+
     /// DWordBL → DWordWL: repack 8 bytes into 2 words.
     /// lo = b[0] + 2^8*b[1] + 2^16*b[2] + 2^24*b[3]
     /// hi = b[4] + 2^8*b[5] + 2^16*b[6] + 2^24*b[7]

prover/src/continuation.rs

@@ -2085,6 +2085,7 @@ mod tests {
                     ("ecsm", c.ecsm),
                     ("ecdas", c.ecdas),
                     ("hint", c.hint),
+                    ("is_wh", c.is_wh),
                 ]
             })
             .collect();

prover/src/debug_report.rs

@@ -9,7 +9,7 @@ use crate::tables::types::BusId;
 /// Print a legend mapping numeric bus IDs to their names.
 pub fn print_bus_legend() {
     eprintln!("=== BUS ID LEGEND ===");
-    for id in 0u64..=21 {
+    for id in 0u64..=u64::from(u8::MAX) {
         if let Ok(bus) = BusId::try_from(id) {
             eprintln!("  Bus {:2} = {}", id, bus.name());
         }

prover/src/lib.rs

@@ -53,10 +53,10 @@ use crate::tables::types::BusId;
 use crate::test_utils::{
     E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_copy_air,
     create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ecdas_air,
-    create_ecsm_air, create_eq_air, create_halt_air, create_hint_air, create_keccak_air,
-    create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air,
-    create_memw_aligned_air, create_memw_register_air, create_mul_air, create_page_air,
-    create_register_air, create_shift_air, create_store_air,
+    create_ecsm_air, create_eq_air, create_halt_air, create_hint_air, create_is_wh_air,
+    create_keccak_air, create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air,
+    create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air,
+    create_page_air, create_register_air, create_shift_air, create_store_air,
 };
 
 // Re-exported for downstream hosts and verifier guests (e.g. the in-VM
@@ -93,8 +93,8 @@ pub struct RuntimePageRange {
 pub const FIXED_TABLE_COUNT: usize = 6;
 
 /// How many sub-proofs each counted table contributes. Chunked chips report
-/// their chunk count; the five accelerators are not chunked and report 0 or 1
-/// (see `validate`). The verifier needs this to reconstruct matching AIRs.
+/// their chunk count; the five accelerators and IS_WH are not chunked and report
+/// 0 or 1 (see `validate`). The verifier needs this to reconstruct matching AIRs.
 #[derive(Debug, Clone, rkyv::Archive, rkyv::Serialize, rkyv::Deserialize)]
 pub struct TableCounts {
     pub cpu: usize,
@@ -120,6 +120,9 @@ pub struct TableCounts {
     pub ecsm: usize,
     pub ecdas: usize,
     pub hint: usize,
+    // Range-check chip for the top 48 bits of `DWordWHH` addresses. One table
+    // when a chip sends `IS_WH` (today only KECCAK), none otherwise.
+    pub is_wh: usize,
 }
 
 impl TableCounts {
@@ -151,6 +154,7 @@ impl TableCounts {
             self.ecsm,
             self.ecdas,
             self.hint,
+            self.is_wh,
         ]
         .into_iter()
         .try_fold(0usize, usize::checked_add)
@@ -196,25 +200,32 @@ impl TableCounts {
                 )));
             }
         }
-        // The accelerators are not chunked: `generate_optional` emits one table
-        // or none, so a count above 1 is a shape no prover can produce. The
-        // sub-proof cross-check constrains only the *total*, so on its own it
-        // lets an inflated accelerator count through whenever another count is
+        // The accelerators and IS_WH are not chunked: `generate_optional` emits
+        // one table or none, so a count above 1 is a shape no prover can produce.
+        // The sub-proof cross-check constrains only the *total*, so on its own it
+        // lets an inflated count through whenever another count is
         // lowered to match; this pins the per-field shape instead. It is not
         // load-bearing for memory safety — both verifiers run the cross-check
-        // before any count sizes an AIR set — and if one of them ever becomes
-        // chunked, this list is what changes.
+        // before any count sizes an AIR set. For the accelerators it is only
+        // shape, and if one of them ever becomes chunked, this list is what
+        // changes. IS_WH is the exception, see its entry.
         let at_most_one = [
             ("keccak", self.keccak),
             ("keccak_rnd", self.keccak_rnd),
             ("ecsm", self.ecsm),
             ("ecdas", self.ecdas),
             ("hint", self.hint),
+            // Load-bearing for soundness: this is what bounds the IS_WH
+            // multiplicity sum per proof. One table of at most 2^k rows, each
+            // μ < 2^20, stays far below p, so no stack of repeated rows reaches
+            // μ = −1 (spec verifier.typ TODO). Chunking IS_WH needs a bound on
+            // its total row count in place of this one.
+            ("is_wh", self.is_wh),
         ];
         for (name, count) in at_most_one {
             if count > 1 {
                 return Err(Error::InvalidTableCounts(format!(
-                    "{name} count is {count} — accelerator tables are not chunked"
+                    "{name} count is {count} — this table is not chunked"
                 )));
             }
         }
@@ -274,14 +285,14 @@ pub struct GuestInput {
 /// 4-byte magic identifying a lambda-vm recursion input blob ("LVMR").
 pub const RECURSION_INPUT_MAGIC: [u8; 4] = *b"LVMR";
 
-/// Wire-format version of the recursion input blob. v4: `TableCounts` lost its
-/// `commit` field when COPY absorbed the COMMIT table, which shortens the
-/// archive. v3: `TableCounts` gained the six accelerator fields, which moves
-/// every field after it in the archive. v2: rkyv pointer_width_64 (64-bit
-/// rel-ptrs) — v1 archives use 32-bit offsets.
+/// Wire-format version of the recursion input blob. v5: `TableCounts` gained
+/// `is_wh`. v4: `TableCounts` lost its `commit` field when COPY absorbed the
+/// COMMIT table, which shortens the archive. v3: `TableCounts` gained the six
+/// accelerator fields, which moves every field after it in the archive. v2:
+/// rkyv pointer_width_64 (64-bit rel-ptrs) — v1 archives use 32-bit offsets.
 /// Any change to a type reachable from `GuestInput` belongs here: the guest
 /// reads the archive in place, so a stale blob is misread rather than rejected.
-pub const RECURSION_INPUT_VERSION: u32 = 4;
+pub const RECURSION_INPUT_VERSION: u32 = 5;
 
 /// Required alignment (bytes) of the archive's first byte in guest memory.
 pub const RECURSION_INPUT_ALIGN: usize = 16;
@@ -593,6 +604,7 @@ pub(crate) struct VmAirs {
     pub ecdases: Vec<VmAir>,
     pub hints: Vec<VmAir>,
     pub copy: VmAir,
+    pub is_whs: Vec<VmAir>,
     pub register: VmAir,
     pub pages: Vec<VmAir>,
     pub memw_registers: Vec<VmAir>,
@@ -629,6 +641,7 @@ impl VmAirs {
                 self.ecsms.len(),
                 self.ecdases.len(),
                 self.hints.len(),
+                self.is_whs.len(),
                 self.pages.len(),
                 self.memw_registers.len(),
                 self.eqs.len(),
@@ -651,6 +664,7 @@ impl VmAirs {
                 traces.ecsms.len(),
                 traces.ecdases.len(),
                 traces.hints.len(),
+                traces.is_whs.len(),
                 traces.pages.len(),
                 traces.memw_registers.len(),
                 traces.eqs.len(),
@@ -685,6 +699,9 @@ impl VmAirs {
         for (air, trace) in self.hints.iter().zip(traces.hints.iter_mut()) {
             pairs.push((air.as_ref(), trace, &()));
         }
+        for (air, trace) in self.is_whs.iter().zip(traces.is_whs.iter_mut()) {
+            pairs.push((air.as_ref(), trace, &()));
+        }
 
         for (air, trace) in self.cpus.iter().zip(traces.cpus.iter_mut()) {
             pairs.push((air.as_ref(), trace, &()));
@@ -770,6 +787,9 @@ impl VmAirs {
         for air in &self.hints {
             refs.push(air.as_ref());
         }
+        for air in &self.is_whs {
+            refs.push(air.as_ref());
+        }
 
         for air in &self.cpus {
             refs.push(air.as_ref());
@@ -960,6 +980,11 @@ impl VmAirs {
             })
             .collect();
         let copy: VmAir = Box::new(create_copy_air(proof_options));
+        let is_whs: Vec<_> = (0..table_counts.is_wh)
+            .map(|i| {
+                Box::new(create_is_wh_air(proof_options).with_name(&format!("IS_WH[{i}]"))) as VmAir
+            })
+            .collect();
         let register: VmAir =
             if let Some((commitment, num_preprocessed_cols)) = register_preprocessed {
                 Box::new(
@@ -1081,6 +1106,7 @@ impl VmAirs {
             ecdases,
             hints,
             copy,
+            is_whs,
             register,
             pages,
             memw_registers,

prover/src/statement.rs

@@ -17,7 +17,7 @@ use crate::test_utils::E;
 use crate::{RuntimePageRange, TableCounts};
 
 /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change.
-const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V4";
+const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V5";
 
 /// Canonical full-ELF identity digest — exactly what [`absorb_statement`] binds
 /// into the transcript. The recursion attestation folds the same digest into
@@ -117,6 +117,7 @@ pub(crate) fn absorb_statement_with_digest(
         ecsm,
         ecdas,
         hint,
+        is_wh,
     } = table_counts;
     for count in [
         cpu,
@@ -138,6 +139,7 @@ pub(crate) fn absorb_statement_with_digest(
         ecsm,
         ecdas,
         hint,
+        is_wh,
     ] {
         t.append_bytes(&(count as u64).to_le_bytes());
     }
@@ -187,7 +189,7 @@ pub(crate) fn absorb_statement_with_digest(
 
 /// Continuation domain tags. Distinct from the monolithic `DOMAIN_TAG` so a
 /// monolithic proof and a continuation proof can never share a transcript prefix.
-const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V4";
+const CONTINUATION_EPOCH_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_EPOCH_V5";
 const CONTINUATION_GLOBAL_TAG: &[u8] = b"LAMBDAVM_CONTINUATION_GLOBAL_V2";
 
 /// Statement bound into the cross-epoch **global** proof's transcript before

prover/src/tables/bitwise.rs

@@ -527,6 +527,15 @@ pub(crate) struct BitwiseHistogram {
     counters: Box<[u64]>,
 }
 
+/// Cell-by-cell equality, so a test can compare a collector against the
+/// lookups it should have counted.
+#[cfg(test)]
+impl PartialEq for BitwiseHistogram {
+    fn eq(&self, other: &Self) -> bool {
+        self.counters == other.counters
+    }
+}
+
 impl BitwiseHistogram {
     /// Allocate a zeroed histogram (80 MiB).
     // No `Default` impl on purpose: `new()` allocates 80 MiB, so a stray