diff --git a/docs/continuations_design.md b/docs/continuations_design.md index 2fedef577..ce3ddddea 100644 --- a/docs/continuations_design.md +++ b/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). diff --git a/executor/programs/asm/test_keccak_64k.s b/executor/programs/asm/test_keccak_64k.s new file mode 100644 index 000000000..32fbed05c --- /dev/null +++ b/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 diff --git a/executor/tests/asm.rs b/executor/tests/asm.rs index a1c9baf2b..5e6439b2e 100644 --- a/executor/tests/asm.rs +++ b/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(); diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 7fa0ffd15..cf9c62411 100644 --- a/prover/src/auto_storage.rs +++ b/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 { let bitwise_rows = BITWISE_ROWS as u64; let register_rows = NUM_REGISTER_ADDRESSES.next_power_of_two() as u64; diff --git a/prover/src/constraints/templates.rs b/prover/src/constraints/templates.rs index d911cdf92..ae7457fb2 100644 --- a/prover/src/constraints/templates.rs +++ b/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] diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index ccee7f0f1..ef0689757 100644 --- a/prover/src/continuation.rs +++ b/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(); diff --git a/prover/src/debug_report.rs b/prover/src/debug_report.rs index 81e71441c..a317d8331 100644 --- a/prover/src/debug_report.rs +++ b/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()); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index c1b0cec51..184ae2392 100644 --- a/prover/src/lib.rs +++ b/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, pub hints: Vec, pub copy: VmAir, + pub is_whs: Vec, pub register: VmAir, pub pages: Vec, pub memw_registers: Vec, @@ -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, diff --git a/prover/src/statement.rs b/prover/src/statement.rs index fdc86a7b4..bb94817c2 100644 --- a/prover/src/statement.rs +++ b/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 diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index c73e1e341..8970daeaa 100644 --- a/prover/src/tables/bitwise.rs +++ b/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 diff --git a/prover/src/tables/copy.rs b/prover/src/tables/copy.rs index 98caeb1a8..6be9156fc 100644 --- a/prover/src/tables/copy.rs +++ b/prover/src/tables/copy.rs @@ -91,10 +91,10 @@ //! Three divergences in the columns from the spec's 34, all representational and all //! recorded in `shape_tests`: the spec types `timestamp` as a `Word` where this code uses a //! `DWordWL`; it types the three increments and `dst_res` as `DWordWHH` -//! (`Half, Half, Word`) where this code uses `DWordHL` (four `Half`s). `IS_WHH` -//! decomposes into an `IS_WH` chip this prover does not have; four `IS_HALF` -//! lookups prove the identical bound with the primitive it does have, at one extra -//! column each. `mu_com`/`mu_com_wide` are the COMMIT-bus gate the spec does not +//! (`Half, Half, Word`) where this code uses `DWordHL` (four `Half`s). Four `IS_HALF` +//! lookups prove the same bound `IS_WHH` would, at one extra column each; moving these +//! four to `IS_WHH` and the `IS_WH` table that KECCAK's `state_ptr` already uses would +//! drop those columns. `mu_com`/`mu_com_wide` are the COMMIT-bus gate the spec does not //! need because it writes the committed bytes through `MEMW` in domain `2·is_write`. //! //! A fourth divergence is not representational: constraints 37, 38 and 39 pin the @@ -1041,9 +1041,10 @@ mod shape_tests { /// `COPY_NEXT` propagates it), so it carries no information. /// - `src_incr`, `dst_incr`, `count_decr` and `dst_res` are `DWordWHH` /// (`Half, Half, Word`) in the spec and `DWordHL` (four `Half`s) here (+4). - /// The spec range-checks them with `IS_WHH`, which decomposes into the `IS_WH` - /// chip; this prover has no such chip, and four `IS_HALF` lookups prove exactly - /// the same bound with the primitive it does have. + /// The spec range-checks them with `IS_WHH`, which sends their top 48 bits to + /// the `IS_WH` table. This chip keeps four `IS_HALF` lookups instead, which prove + /// the same bound at one extra column each; moving them to `IS_WHH`, as KECCAK's + /// `state_ptr` already is, would drop those four columns. /// - `mu_com` and `mu_com_wide` (+2) gate the COMMIT bus. The spec has no such /// bus: it writes committed bytes through `MEMW` in domain `2 · is_write` and /// lets the verifier initialise and finalise that domain in the memory diff --git a/prover/src/tables/is_wh.rs b/prover/src/tables/is_wh.rs new file mode 100644 index 000000000..446590c28 --- /dev/null +++ b/prover/src/tables/is_wh.rs @@ -0,0 +1,215 @@ +//! IS_WH table — range check for the top 48 bits of a 64-bit value. +//! +//! Chips that read or write contiguous memory hold one address per access, and +//! those addresses usually differ only in their lowest limb. Instead of range +//! checking all 64 bits locally, a caller keeps the address as a `DWordWHH` +//! (`[half_lo, half_mid, word_hi]`), checks `half_lo` itself and sends the +//! `(word_hi, half_mid)` pair here on the `IsWh` bus (spec `is_wh.toml`). The +//! `IS_WHH` template (spec `is_whh.toml`) is that pair of sends, see [`is_whh`]. +//! +//! One row per distinct `(word, half)` pair, with `μ` counting its sends. +//! +//! ## Columns +//! - `value[0]`: Half — the `Half` of the pair (bits 16..32 of the address) +//! - `value[1]`, `value[2]`: Half — the `Word` of the pair as two halves +//! (bits 32..48 and 48..64) +//! - `μ`: B20 — number of sends of this pair +//! +//! ## Bus Interactions +//! - Sender: IS_B20[μ] (multiplicity 1, bounds μ) +//! - Sender: IS_HALFWORD (×3, one per `value` limb, multiplicity μ) +//! - Receiver: IS_WH[value[1] + 2^16·value[2], value[0]] (multiplicity μ) +//! +//! ## μ bound +//! `μ` lives in the field, so `μ = −1` would turn a row from receiver into +//! sender: it could cancel a forged `IS_WH` send while also receiving the row's +//! own `IS_HALFWORD` checks. The `IS_B20[μ]` send (multiplicity 1, so it is not +//! itself flipped by `μ`) pins `μ ∈ [0, 2^20)`. A pair sent more than +//! [`IS_WH_MU_MAX`] times is split over several rows (see [`dedup_is_wh_rows`]). +//! Padding rows send `IS_B20[0]`, which the BITWISE collector counts (see +//! [`collect_bitwise_from_is_wh`]). +//! +//! The table has no polynomial constraints. + +use std::collections::BTreeMap; + +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use super::bitwise::{BitwiseHistogram, BitwiseOperation, BitwiseOperationType}; +use super::types::{BusId, GoldilocksExtension, GoldilocksField, VmTable}; + +/// Column definitions for the IS_WH table. +pub mod cols { + /// value[0]: Half — the `Half` of the `(Word, Half)` pair. + pub const VALUE_0: usize = 0; + /// value[1]: Half — low half of the `Word`. + pub const VALUE_1: usize = 1; + /// value[2]: Half — high half of the `Word`. + pub const VALUE_2: usize = 2; + /// μ: B20 — number of `IS_WH` sends of this pair. + pub const MU: usize = 3; + + pub const NUM_COLUMNS: usize = 4; +} + +/// Largest multiplicity a single row may carry: `μ` is a `B20`. +pub const IS_WH_MU_MAX: u64 = (1 << 20) - 1; + +/// A `(Word, Half)` pair as it travels on the `IsWh` bus. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct IsWhKey { + /// Bits 32..64 of the checked value. + pub word: u32, + /// Bits 16..32 of the checked value. + pub half: u16, +} + +impl IsWhKey { + /// The pair a `DWordWHH` holding `value` sends to `IS_WH`. + pub fn of_dword(value: u64) -> Self { + Self { + word: (value >> 32) as u32, + half: ((value >> 16) & 0xFFFF) as u16, + } + } +} + +/// Deduplicates `IS_WH` sends into trace rows: `(key) -> μ`, splitting a key +/// over several rows when its count exceeds [`IS_WH_MU_MAX`]. Rows come out +/// sorted by key so the trace is deterministic. The trace builder calls it once +/// and hands the same rows to [`generate_is_wh_trace`] and +/// [`collect_bitwise_from_is_wh`]. +pub fn dedup_is_wh_rows(keys: impl IntoIterator) -> Vec<(IsWhKey, u64)> { + let mut counts: BTreeMap = BTreeMap::new(); + for key in keys { + *counts.entry(key).or_insert(0) += 1; + } + + let mut rows = Vec::with_capacity(counts.len()); + for (key, mut left) in counts { + while left > 0 { + let mu = left.min(IS_WH_MU_MAX); + left -= mu; + rows.push((key, mu)); + } + } + rows +} + +/// Number of trace rows (real + padding) for the given deduplicated row count. +fn padded_rows(real_rows: usize) -> usize { + real_rows.next_power_of_two().max(4) +} + +/// Generates the IS_WH trace from the rows of [`dedup_is_wh_rows`]. +/// +/// Padding rows are all zero (`value = 0`, `μ = 0`, spec `pad = 0`). +pub fn generate_is_wh_trace( + rows: &[(IsWhKey, u64)], +) -> TraceTable { + let num_rows = padded_rows(rows.len()); + let mut trace = TraceTable::new_main( + crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row_idx, (key, mu)) in rows.iter().enumerate() { + table.set_half(row_idx, cols::VALUE_0, key.half); + table.set_half(row_idx, cols::VALUE_1, (key.word & 0xFFFF) as u16); + table.set_half(row_idx, cols::VALUE_2, (key.word >> 16) as u16); + table.set_u64(row_idx, cols::MU, *mu); + } + + trace +} + +/// Counts the IS_WH table's BITWISE lookups: per row, `IS_HALFWORD` ×μ on each +/// `value` limb and `IS_B20[μ]` ×1 — padding rows included, which send +/// `IS_B20[0]`. +pub(crate) fn collect_bitwise_from_is_wh(rows: &[(IsWhKey, u64)], h: &mut BitwiseHistogram) { + if rows.is_empty() { + // No sends, no table (`generate_optional`), so nothing to count. + return; + } + let padding = padded_rows(rows.len()) - rows.len(); + + let half = |v: u16| { + BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (v & 0xFF) as u8, + (v >> 8) as u8, + ) + }; + let b20 = |v: u64| BitwiseOperation::b20(v as u8, (v >> 8) as u8, (v >> 16) as u8); + + for (key, mu) in rows { + h.bump_n(half(key.half), *mu); + h.bump_n(half((key.word & 0xFFFF) as u16), *mu); + h.bump_n(half((key.word >> 16) as u16), *mu); + h.bump(b20(*mu)); + } + h.bump_n(b20(0), padding as u64); +} + +/// Bus interactions of the IS_WH table. +pub fn bus_interactions() -> Vec { + let mu = || Multiplicity::Column(cols::MU); + let column = |c: usize| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }; + + vec![ + // IS_B20[μ] ×1: bounds μ (spec is_wh.toml, #1017). + BusInteraction::sender(BusId::IsB20, Multiplicity::One, vec![column(cols::MU)]), + // IS_HALF[value[i]] ×μ, i = 0..2 (is_wh:c:range_value). + BusInteraction::sender(BusId::IsHalfword, mu(), vec![column(cols::VALUE_0)]), + BusInteraction::sender(BusId::IsHalfword, mu(), vec![column(cols::VALUE_1)]), + BusInteraction::sender(BusId::IsHalfword, mu(), vec![column(cols::VALUE_2)]), + // IS_WH[value[1] + 2^16·value[2], value[0]] ×(−μ) (is_wh:c:is_wh). + BusInteraction::receiver( + BusId::IsWh, + mu(), + vec![ + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::VALUE_1, + }, + LinearTerm::Column { + coefficient: 1 << 16, + column: cols::VALUE_2, + }, + ]), + column(cols::VALUE_0), + ], + ), + ] +} + +/// The `IS_WHH` template (spec `is_whh.toml`, #1015): range-checks the +/// `DWordWHH` `[half_lo, half_mid, word_hi]` at `start_column` by sending +/// `IS_WH[word_hi, half_mid]` and `IS_HALF[half_lo]`, both with multiplicity +/// `cond`. +/// +/// `cond` must be constrained to a bit by the caller (spec `cond: Bit`). These +/// are bus sends, not constraints, so the template cannot enforce it: with +/// `cond = −1` the row would *receive* both checks, cancelling forged sends +/// elsewhere. +pub fn is_whh(start_column: usize, cond: Multiplicity) -> [BusInteraction; 2] { + let column = |c: usize| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }; + [ + BusInteraction::sender( + BusId::IsWh, + cond.clone(), + vec![column(start_column + 2), column(start_column + 1)], + ), + BusInteraction::sender(BusId::IsHalfword, cond, vec![column(start_column)]), + ] +} diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 8fa2c10ff..92a54f524 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -4,7 +4,7 @@ //! sends input state to the round chip via the Keccak bus, and receives the output //! state after 24 rounds. //! -//! ## Column layout (~511 columns) +//! ## Column layout (486 columns) //! //! | Group | Size | Description | //! |----------------|------|------------------------------------------------| @@ -12,7 +12,7 @@ //! | addr | 8 | State address as DWordBL (8 bytes) | //! | input_state | 200 | Input state bytes [5][5][8] | //! | output_state | 200 | Output state bytes [5][5][8] | -//! | state_ptr | 100 | Per-lane DWordHL addresses [25][4] | +//! | state_ptr | 75 | Per-lane DWordWHH addresses [25][3] | //! | mu | 1 | Multiplicity flag | use executor::vm::instruction::execution::KECCAK_SYSCALL_NUMBER; @@ -21,6 +21,7 @@ use stark::trace::TraceTable; use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use super::is_wh::{IsWhKey, is_whh}; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; use crate::constraints::templates::{AddOperand, INV_SHIFT_32}; @@ -41,12 +42,12 @@ pub mod cols { // output_state[5][5][8] = 200 bytes pub const OUTPUT_STATE: usize = INPUT_STATE + 200; // 210 - // state_ptr[25][4] = 100 halfwords (DWordHL per lane) + // state_ptr[25][3] = 75 columns (DWordWHH per lane: half_lo, half_mid, word_hi) pub const STATE_PTR: usize = OUTPUT_STATE + 200; // 410 - pub const MU: usize = STATE_PTR + 100; // 510 + pub const MU: usize = STATE_PTR + 75; // 485 - pub const NUM_COLUMNS: usize = MU + 1; // 511 + pub const NUM_COLUMNS: usize = MU + 1; // 486 // ------------------------------------------------------------------------- // Index helpers @@ -69,10 +70,10 @@ pub mod cols { OUTPUT_STATE + (x + 5 * y) * 8 + byte } - /// Index into state_ptr[lane_idx][halfword] (DWordHL = 4 halfwords) + /// Index into state_ptr[lane_idx][limb] (DWordWHH = [half_lo, half_mid, word_hi]) #[inline] - pub const fn state_ptr(lane_idx: usize, hw: usize) -> usize { - STATE_PTR + lane_idx * 4 + hw + pub const fn state_ptr(lane_idx: usize, limb: usize) -> usize { + STATE_PTR + lane_idx * 3 + limb } } @@ -88,6 +89,20 @@ pub struct KeccakOperation { pub output: [u64; 25], } +/// The `IS_WH` sends of the KECCAK table: one per lane of every call, the top +/// 48 bits of `state_ptr[lane] = state_addr + 8·lane` (`keccak:c:range_state_ptr`). +pub fn is_wh_keys(ops: &[KeccakOperation]) -> impl Iterator + '_ { + ops.iter().flat_map(|op| { + (0..25u64).map(move |lane_idx| { + let ptr = op + .state_addr + .checked_add(lane_idx * 8) + .expect("keccak state address range must be validated by the executor"); + IsWhKey::of_dword(ptr) + }) + }) +} + // ========================================================================= // Trace generation // ========================================================================= @@ -133,7 +148,7 @@ pub fn generate_keccak_trace( .state_addr .checked_add(lane_idx as u64 * 8) .expect("keccak state address range must be validated by the executor"); - table.set_dword_hl(row_idx, cols::state_ptr(lane_idx, 0), ptr); + table.set_dword_whh(row_idx, cols::state_ptr(lane_idx, 0), ptr); } // mu = 1 (real row) @@ -141,7 +156,7 @@ pub fn generate_keccak_trace( } // Padding rows: state_ptr[lane][0] = 8 * lane_idx (per spec keccak.toml pad). - // Halfwords 1..3 stay zero since 8*24 = 192 fits in the low halfword. + // half_mid and word_hi stay zero since 8*24 = 192 fits in half_lo. // mu = 0 gates all bus interactions and the ADD constraint, so these values // only need to satisfy the pad requirement, not reconstruct a real address. for row_idx in n..num_rows { @@ -160,7 +175,7 @@ pub fn generate_keccak_trace( pub fn bus_interactions() -> Vec { let syscall_lo = KECCAK_SYSCALL_NUMBER & 0xFFFF_FFFF; let syscall_hi = KECCAK_SYSCALL_NUMBER >> 32; - let mut interactions = Vec::with_capacity(160); + let mut interactions = Vec::with_capacity(84); // 1. ECALL receiver (shared bus, per spec keccak:c:output) // Payload: [ts_lo, ts_hi, syscall_lo32, syscall_hi32] in DWordWL [lo, hi] @@ -324,18 +339,14 @@ pub fn bus_interactions() -> Vec { )); } - // 4. IS_HALF range checks on state_ptr (100 interactions) + // 4. IS_WHH range checks on state_ptr (keccak:c:range_state_ptr): IS_WH on the + // top 48 bits and IS_HALF on half_lo, 50 interactions. μ is a bit (idx 51 below), + // as the template's `cond: Bit` requires. for lane_idx in 0..25 { - for hw in 0..4 { - interactions.push(BusInteraction::sender( - BusId::IsHalfword, - Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::state_ptr(lane_idx, hw), - packing: Packing::Direct, - }], - )); - } + interactions.extend(is_whh( + cols::state_ptr(lane_idx, 0), + Multiplicity::Column(cols::MU), + )); } // 5. Alignment: addr[0] & 7 = 0, which enforces addr % 8 == 0. @@ -385,7 +396,7 @@ pub fn bus_interactions() -> Vec { let x = lane_idx % 5; let y = lane_idx / 5; - // Address as DWordWL: lo32 = h0 + 2^16*h1, hi32 = h2 + 2^16*h3 + // Address as DWordWL: lo32 = half_lo + 2^16*half_mid, hi32 = word_hi let addr_lo = BusValue::linear(vec![ LinearTerm::Column { coefficient: 1, @@ -396,16 +407,10 @@ pub fn bus_interactions() -> Vec { column: cols::state_ptr(lane_idx, 1), }, ]); - let addr_hi = BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::state_ptr(lane_idx, 2), - }, - LinearTerm::Column { - coefficient: 65536, - column: cols::state_ptr(lane_idx, 3), - }, - ]); + let addr_hi = BusValue::Packed { + start_column: cols::state_ptr(lane_idx, 2), + packing: Packing::Direct, + }; let mut values = Vec::with_capacity(24); // old[0..8] = input_state bytes (the value being read) @@ -458,7 +463,7 @@ pub fn bus_interactions() -> Vec { /// The KECCAK core table's 52 transition constraints as a single [`ConstraintSet`]: /// - idx 0-49: for `lane_idx ∈ 0..25`, the `ADD` carry pair (gated on `μ`) /// enforcing `state_ptr[lane] = addr + 8·lane_idx` (`addr` DWordBL, -/// `state_ptr` DWordHL); +/// `state_ptr` DWordWHH); /// - idx 50: `μ · carry_1 = 0` (top-lane no-overflow), where `carry_1` is the /// high carry of `addr + 192 = state_ptr[24]`; /// - idx 51: `μ · (1 − μ) = 0` (MuIsBit). @@ -482,7 +487,7 @@ impl ConstraintSet for KeccakConstraints { &[cols::MU], &AddOperand::from_dword_bl(cols::ADDR), &AddOperand::constant(offset), - &AddOperand::from_dword_hl(cols::state_ptr(lane_idx, 0)), + &AddOperand::from_dword_whh(cols::state_ptr(lane_idx, 0)), ); } @@ -498,9 +503,8 @@ impl ConstraintSet for KeccakConstraints { + b.main(0, cols::addr(5)) * c256 + b.main(0, cols::addr(6)) * c65536.clone() + b.main(0, cols::addr(7)) * c16777216; - let ptr_lo = - b.main(0, cols::state_ptr(24, 0)) + b.main(0, cols::state_ptr(24, 1)) * c65536.clone(); - let ptr_hi = b.main(0, cols::state_ptr(24, 2)) + b.main(0, cols::state_ptr(24, 3)) * c65536; + let ptr_lo = b.main(0, cols::state_ptr(24, 0)) + b.main(0, cols::state_ptr(24, 1)) * c65536; + let ptr_hi = b.main(0, cols::state_ptr(24, 2)); let inv_2_32 = b.const_base(INV_SHIFT_32); let c192 = b.const_base(192); diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index bc46efcfb..620fa65d4 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -10,6 +10,7 @@ //! - **DECODE**: Instruction decode table //! - **BRANCH**: Branch target calculation table //! - **HALT**: Single-row halt table +//! - **IS_WH**: Range check for the top 48 bits of `DWordWHH` addresses (one row per distinct pair) //! //! ## Memory Tables //! @@ -35,6 +36,7 @@ pub mod eq; pub mod global_memory; pub mod halt; pub mod hint; +pub mod is_wh; pub mod keccak; pub mod keccak_rc; pub mod keccak_rnd; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 88531e0f8..d6cb6ebee 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -52,6 +52,7 @@ use super::ecsm; use super::eq; use super::halt; use super::hint; +use super::is_wh; use super::keccak::{self, KeccakOperation}; use super::keccak_rc; use super::keccak_rnd::{self, KeccakRoundOperation}; @@ -2755,19 +2756,18 @@ pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec )); } - // IS_HALF for state_ptr halfwords (100 per call) + // IS_HALF for state_ptr half_lo (25 per call). The top 48 bits go to + // IS_WH through `IS_WHH`; that table counts its own checks. for lane_idx in 0..25 { let ptr = state_addr .checked_add(lane_idx as u64 * 8) .expect("keccak state address range must be validated by the executor"); - for shift in [0, 16, 32, 48] { - let half = ((ptr >> shift) & 0xFFFF) as u16; - ops.push(BitwiseOperation::halfword( - BitwiseOperationType::IsHalf, - (half & 0xFF) as u8, - ((half >> 8) & 0xFF) as u8, - )); - } + let half = (ptr & 0xFFFF) as u16; + ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (half & 0xFF) as u8, + ((half >> 8) & 0xFF) as u8, + )); } // Replay keccak round computation to extract bitwise lookups @@ -3164,6 +3164,10 @@ pub struct Traces { /// makes no hint ecall. pub hints: Vec>, + /// IS_WH table (one row per distinct `(Word, Half)` address pair sent through + /// `IS_WHH`). Empty when no chip sends one. + pub is_whs: Vec>, + /// Unified COPY table: one streaming copy primitive for memcpy/memmove, /// memset and the commit byte loop, selected by decoded functionality columns. /// Always present: COPY receives the `write` ECALL, so any run that produces @@ -3597,6 +3601,11 @@ fn build_traces( // sources fold their transient `collect_*` Vec in and drop it. The histogram is a // commutative monoid, so per-worker histograms tree-reduce to multiplicities that are // independent of accumulation order. + // IS_WH rows from the `IS_WH` sends of every `IS_WHH` caller (today only KECCAK's + // state_ptr), deduplicated once and shared by the BITWISE collector below and the + // IS_WH trace in phase 5, so the two read the same rows by construction. + let is_wh_rows = is_wh::dedup_is_wh_rows(keccak::is_wh_keys(&keccak_ops)); + type Collector<'a> = Box; let lt_chunk = max_rows.lt; let branch_chunk = max_rows.branch; @@ -3648,6 +3657,7 @@ fn build_traces( Box::new(|h| h.add_ops(&collect_bitwise_from_ecsm(&ecsm_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_ecdas(&ecdas_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_hint(&hint_ops))), + Box::new(|h| is_wh::collect_bitwise_from_is_wh(&is_wh_rows, h)), Box::new(|h| add_padding_byte_checks(h, num_padding_rows)), ]; if let Some(image) = initial_image @@ -3968,6 +3978,15 @@ fn build_traces( storage_mode, ) }; + // IS_WH table. Absent entirely when no chip sends `IS_WH`. + let gen_is_whs = || { + generate_optional( + &is_wh_rows, + is_wh::generate_is_wh_trace, + #[cfg(feature = "disk-spill")] + storage_mode, + ) + }; // COPY is not optional: it receives the `write` ECALL directly. let gen_copy = || copy::generate_copy_trace(©_ops); @@ -3982,6 +4001,7 @@ fn build_traces( (None, None, None, None); let (mut ecsms_slot, mut ecdases_slot) = (None, None); let mut hints_slot = None; + let mut is_whs_slot = None; let mut copy_slot = None; #[cfg(feature = "disk-spill")] @@ -4024,6 +4044,7 @@ fn build_traces( spawn_into!(ecsms_slot, gen_ecsms); spawn_into!(ecdases_slot, gen_ecdases); spawn_into!(hints_slot, gen_hints); + spawn_into!(is_whs_slot, gen_is_whs); spawn_into!(copy_slot, gen_copy); }); } else { @@ -4052,6 +4073,7 @@ fn build_traces( ecsms_slot = Some(gen_ecsms()); ecdases_slot = Some(gen_ecdases()); hints_slot = Some(gen_hints()); + is_whs_slot = Some(gen_is_whs()); copy_slot = Some(gen_copy()); } @@ -4086,6 +4108,7 @@ fn build_traces( let ecsms = ecsms_slot.expect(PHASE5_RAN)?; let ecdases = ecdases_slot.expect(PHASE5_RAN)?; let hints = hints_slot.expect(PHASE5_RAN)?; + let is_whs = is_whs_slot.expect(PHASE5_RAN)?; #[allow(unused_mut)] let mut copy_trace = copy_slot.expect(PHASE5_RAN); @@ -4157,6 +4180,7 @@ fn build_traces( ecsms, ecdases, hints, + is_whs, copy: copy_trace, memw_registers, local_to_global, @@ -4573,6 +4597,7 @@ impl Traces { use super::eq::cols::NUM_COLUMNS as EQ_COLS; use super::halt::cols::NUM_COLUMNS as HALT_COLS; use super::hint::cols::NUM_COLUMNS as HINT_COLS; + use super::is_wh::cols::NUM_COLUMNS as IS_WH_COLS; use super::keccak::cols::NUM_COLUMNS as KECCAK_COLS; use super::keccak_rc::NUM_PRECOMPUTED_COLS as KECCAK_RC_PRECOMPUTED; use super::keccak_rc::cols::NUM_COLUMNS as KECCAK_RC_COLS; @@ -4611,6 +4636,7 @@ impl Traces { ecsms, ecdases, hints, + is_whs, copy, memw_registers, eqs, @@ -4689,6 +4715,9 @@ impl Traces { for t in hints { total += (t.num_rows() * HINT_COLS) as u64; } + for t in is_whs { + total += (t.num_rows() * IS_WH_COLS) as u64; + } total += (copy.num_rows() * super::copy::cols::NUM_COLUMNS) as u64; total } @@ -4732,6 +4761,7 @@ impl Traces { let n_ecdas = aux_cols(super::ecdas::bus_interactions().len()); let n_copy = aux_cols(super::copy::bus_interactions().len()); let n_hint = aux_cols(super::hint::bus_interactions().len()); + let n_is_wh = aux_cols(super::is_wh::bus_interactions().len()); let Traces { cpus, @@ -4754,6 +4784,7 @@ impl Traces { ecsms, ecdases, hints, + is_whs, copy, memw_registers, eqs, @@ -4832,6 +4863,9 @@ impl Traces { for t in hints { total += (t.num_rows() * n_hint) as u64; } + for t in is_whs { + total += (t.num_rows() * n_is_wh) as u64; + } total += (copy.num_rows() * n_copy) as u64; total } @@ -4858,6 +4892,7 @@ impl Traces { ecsm: self.ecsms.len(), ecdas: self.ecdases.len(), hint: self.hints.len(), + is_wh: self.is_whs.len(), } } diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index ebbad23d2..755bc23a6 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -356,7 +356,7 @@ pub enum BusId { // ========================================================================= // Copy accelerator // ========================================================================= - // IDs 29 and 32 are unused. The copy primitive chains over a single + // ID 29 is unused (32 is IS_WH, below). The copy primitive chains over a single // [`BusId::CopyNext`] and carries the functionality selectors inside the tuple, // rather than giving each of its three operations a bus of its own. @@ -367,6 +367,15 @@ pub enum BusId { /// boundary claims, matched across epochs by the final aggregation LogUp. GlobalMemory = 31, + // ========================================================================= + // Address range checks + // ========================================================================= + /// `IS_WH[Word, Half]`: range check that the top 48 bits of a `DWordWHH` + /// are a valid `(Word, Half)` pair. Callers send it through the `IS_WHH` + /// template; the IS_WH table receives it. ID 29 (the removed EC_SCALAR + /// `ServeK` bus) stays unused. + IsWh = 32, + // ========================================================================= // Unified copy primitive // ========================================================================= @@ -408,6 +417,7 @@ impl BusId { BusId::Ecdas => "Ecdas", BusId::Bit => "Bit", BusId::GlobalMemory => "GlobalMemory", + BusId::IsWh => "IsWh", } } } @@ -439,6 +449,7 @@ impl TryFrom for BusId { 28 => Ok(BusId::Ecdas), 30 => Ok(BusId::Bit), 31 => Ok(BusId::GlobalMemory), + 32 => Ok(BusId::IsWh), 33 => Ok(BusId::CopyNext), other => Err(other), } diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index c09022647..256e0fcc4 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -66,6 +66,7 @@ use crate::tables::halt::{bus_interactions as halt_bus_interactions, cols as hal use crate::tables::hint::{ HintConstraints, bus_interactions as hint_bus_interactions, cols as hint_cols, }; +use crate::tables::is_wh::{bus_interactions as is_wh_bus_interactions, cols as is_wh_cols}; use crate::tables::keccak::{ KeccakConstraints, bus_interactions as keccak_bus_interactions, cols as keccak_cols, }; @@ -918,6 +919,18 @@ pub fn create_hint_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { + build_air( + is_wh_cols::NUM_COLUMNS, + is_wh_bus_interactions(), + proof_options, + 1, + EmptyConstraints, + "IS_WH", + ) +} + /// Create the unified COPY AIR: one streaming copy primitive for memcpy/memmove, /// memset and the `write` syscall, selected by the decoded functionality columns. pub fn create_copy_air( diff --git a/prover/src/tests/constraint_emit_tests.rs b/prover/src/tests/constraint_emit_tests.rs index 64f03da51..095ea2af7 100644 --- a/prover/src/tests/constraint_emit_tests.rs +++ b/prover/src/tests/constraint_emit_tests.rs @@ -231,6 +231,22 @@ fn emit_add_pair_linear_unconditional() { check_add_pair_case("add_pair_linear_unconditional", &Body, false); } +#[test] +fn emit_add_pair_conditional_whh_sum() { + // DWordBL lhs + constant, DWordWHH sum: the KECCAK state_ptr shape. + emit_body!(Body, 2, |b| { + emit_add_pair( + b, + 0, + &[0], + &AddOperand::from_dword_bl(1), + &AddOperand::constant(192), + &AddOperand::from_dword_whh(9), + ) + }); + check_add_pair_case("add_pair_conditional_whh_sum", &Body, true); +} + #[test] fn emit_add_pair_multi_cond_bytes() { // Multi-column condition (flag sum), Word + Constant operands, and a diff --git a/prover/src/tests/constraint_program_device_tests.rs b/prover/src/tests/constraint_program_device_tests.rs index 040748daf..b1c51c90e 100644 --- a/prover/src/tests/constraint_program_device_tests.rs +++ b/prover/src/tests/constraint_program_device_tests.rs @@ -182,4 +182,5 @@ fn all_table_programs_lower_and_match_folders() { check_air_device(&create_ecsm_air(&opts), "ECSM"); check_air_device(&create_ecdas_air(&opts), "ECDAS"); check_air_device(&create_hint_air(&opts), "HINT"); + check_air_device(&create_is_wh_air(&opts), "IS_WH"); } diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs index c6ae628d9..51b520f1c 100644 --- a/prover/src/tests/constraint_program_tests.rs +++ b/prover/src/tests/constraint_program_tests.rs @@ -180,4 +180,5 @@ fn all_table_programs_match_folders() { check_air(&create_ecsm_air(&opts), "ECSM"); check_air(&create_ecdas_air(&opts), "ECDAS"); check_air(&create_hint_air(&opts), "HINT"); + check_air(&create_is_wh_air(&opts), "IS_WH"); } diff --git a/prover/src/tests/constraints_tests.rs b/prover/src/tests/constraints_tests.rs index 0caf71264..58af0b18a 100644 --- a/prover/src/tests/constraints_tests.rs +++ b/prover/src/tests/constraints_tests.rs @@ -259,6 +259,53 @@ fn test_add_operand_from_dword_hl() { } } +#[test] +fn test_add_operand_from_dword_whh() { + // Test DWordWHH → DWordWL (repack 2 halves → lo word, high word as is) + let op = AddOperand::from_dword_whh(4); + match op { + AddOperand::Linear { lo, hi } => { + assert_eq!(lo.len(), 2); + assert_eq!(hi.len(), 1); + + // lo = h[0] + 2^16 * h[1] + match &lo[0] { + AddLinearTerm::Column { + coefficient, + column, + } => { + assert_eq!(*coefficient, 1); + assert_eq!(*column, 4); + } + _ => panic!("Expected Column"), + } + match &lo[1] { + AddLinearTerm::Column { + coefficient, + column, + } => { + assert_eq!(*coefficient, 1 << 16); + assert_eq!(*column, 5); + } + _ => panic!("Expected Column"), + } + + // hi = w[2], unscaled: the word is the most significant limb + match &hi[0] { + AddLinearTerm::Column { + coefficient, + column, + } => { + assert_eq!(*coefficient, 1); + assert_eq!(*column, 6); + } + _ => panic!("Expected Column"), + } + } + _ => panic!("Expected Linear variant"), + } +} + #[test] fn test_add_operand_from_dword_bl() { // Test DWordBL → DWordWL (repack 8 bytes → 2 words) diff --git a/prover/src/tests/ir_stats_dump.rs b/prover/src/tests/ir_stats_dump.rs index 99767b3b8..3a4db42f4 100644 --- a/prover/src/tests/ir_stats_dump.rs +++ b/prover/src/tests/ir_stats_dump.rs @@ -129,4 +129,5 @@ fn dump_ir_stats() { stats(&create_keccak_rc_air(&opts), "KECCAK_RC"); stats(&create_ecsm_air(&opts), "ECSM"); stats(&create_ecdas_air(&opts), "ECDAS"); + stats(&create_is_wh_air(&opts), "IS_WH"); } diff --git a/prover/src/tests/is_wh_tests.rs b/prover/src/tests/is_wh_tests.rs new file mode 100644 index 000000000..e5989aac5 --- /dev/null +++ b/prover/src/tests/is_wh_tests.rs @@ -0,0 +1,698 @@ +//! Tests for the IS_WH table and the IS_WHH template (spec #1003, #1015, #1017), +//! and for the KECCAK `state_ptr` that is their first caller. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use stark::prover::{IsStarkProver, Prover}; + +use crate::statement::{StatementKind, absorb_statement}; +use crate::tables::bitwise::{ + BitwiseHistogram, BitwiseOperation, BitwiseOperationType, NUM_ROWS as BW_NUM_ROWS, + cols as bw_cols, row_index as bw_row_index, +}; +use crate::tables::is_wh::{ + self, IS_WH_MU_MAX, IsWhKey, collect_bitwise_from_is_wh, cols, dedup_is_wh_rows, + generate_is_wh_trace, +}; +use crate::tables::keccak::{ + self, KeccakConstraints, KeccakOperation, cols as keccak_cols, generate_keccak_trace, +}; +use crate::tables::trace_builder::Traces; +use crate::tables::types::{BusId, FE}; +use crate::test_utils::{E, asm_elf_bytes, busless_air, validate_busless}; +use crate::tests::prove_elfs_tests::{BusOutcome, weigh_the_bus_with}; +use crate::tests::skip_empty_tables_tests::assert_only_the_bus_rejected; +use crate::{MaxRowsConfig, VmAirs, VmProof}; + +use executor::elf::Elf; +use executor::vm::execution::Executor; + +const A: IsWhKey = IsWhKey { + word: 0x0000_0001, + half: 0x0002, +}; +const B: IsWhKey = IsWhKey { + word: 0xFFFF_FFFF, + half: 0xFFFF, +}; + +fn keccak_op(state_addr: u64) -> KeccakOperation { + KeccakOperation { + timestamp: 7, + state_addr, + input: [0x0102_0304_0506_0708; 25], + output: [0; 25], + } +} + +// ========================================================================= +// Keys and dedup +// ========================================================================= + +#[test] +fn test_is_wh_key_of_dword_takes_the_top_48_bits() { + let key = IsWhKey::of_dword(0x1234_5678_9ABC_DEF0); + assert_eq!(key.word, 0x1234_5678, "word = bits 32..64"); + assert_eq!(key.half, 0x9ABC, "half = bits 16..32"); + // The low half is not part of the key: it is IS_HALF-checked by the caller. + assert_eq!(IsWhKey::of_dword(0x1234_5678_9ABC_0000), key); +} + +#[test] +fn test_is_wh_dedup_collapses_repeated_keys() { + let rows = dedup_is_wh_rows([B, A, A, B, A]); + // Sorted by key, so the trace does not depend on hash order. + assert_eq!(rows, vec![(A, 3), (B, 2)]); +} + +#[test] +fn test_is_wh_dedup_of_no_sends_is_empty() { + assert!(dedup_is_wh_rows(std::iter::empty()).is_empty()); +} + +#[test] +fn test_is_wh_dedup_splits_mu_above_b20() { + let total_mu = |rows: &[(IsWhKey, u64)]| rows.iter().map(|(_, mu)| mu).sum::(); + + // Exactly IS_WH_MU_MAX fits one row. + let rows = dedup_is_wh_rows(vec![A; IS_WH_MU_MAX as usize]); + assert_eq!(rows, vec![(A, IS_WH_MU_MAX)]); + + // One more spills into a second row of the same key. + let rows = dedup_is_wh_rows(vec![A; IS_WH_MU_MAX as usize + 1]); + assert_eq!(rows, vec![(A, IS_WH_MU_MAX), (A, 1)]); + + // Two full rows and a remainder, next to an unrelated key. + let mut keys = vec![A; 2 * IS_WH_MU_MAX as usize + 3]; + keys.push(B); + let rows = dedup_is_wh_rows(keys.iter().copied()); + assert_eq!( + rows, + vec![(A, IS_WH_MU_MAX), (A, IS_WH_MU_MAX), (A, 3), (B, 1)] + ); + assert_eq!(total_mu(&rows), keys.len() as u64, "no send lost or added"); + assert!(rows.iter().all(|(_, mu)| *mu <= IS_WH_MU_MAX && *mu > 0)); +} + +/// The split point is the top of the `IS_B20` range: BITWISE row `i` receives +/// `IS_B20[i]`, so the last row takes `IS_WH_MU_MAX` and there is none past it. +/// A larger split point would build rows whose bound has no receiver. +#[test] +fn test_is_wh_mu_max_is_the_top_of_b20() { + let (x, y, z) = ( + IS_WH_MU_MAX as u8, + (IS_WH_MU_MAX >> 8) as u8, + (IS_WH_MU_MAX >> 16) as u8, + ); + assert_eq!(bw_row_index(x, y, z), BW_NUM_ROWS - 1); + assert_eq!(IS_WH_MU_MAX + 1, BW_NUM_ROWS as u64); +} + +// ========================================================================= +// Trace +// ========================================================================= + +#[test] +fn test_is_wh_trace_layout_and_padding() { + let trace = generate_is_wh_trace(&dedup_is_wh_rows([A, B, A])); + let t = &trace.main_table; + assert_eq!( + trace.num_rows(), + 4, + "two real rows padded to the minimum of 4" + ); + + // value[0] = half, value[1..2] = word as two halves (low first). + assert_eq!(*t.get(0, cols::VALUE_0), FE::from(A.half as u64)); + assert_eq!(*t.get(0, cols::VALUE_1), FE::from((A.word & 0xFFFF) as u64)); + assert_eq!(*t.get(0, cols::VALUE_2), FE::from((A.word >> 16) as u64)); + assert_eq!(*t.get(0, cols::MU), FE::from(2u64)); + assert_eq!(*t.get(1, cols::VALUE_0), FE::from(0xFFFFu64)); + assert_eq!(*t.get(1, cols::VALUE_1), FE::from(0xFFFFu64)); + assert_eq!(*t.get(1, cols::VALUE_2), FE::from(0xFFFFu64)); + assert_eq!(*t.get(1, cols::MU), FE::one()); + + // Padding is all zero (spec pad = 0). + for row in 2..4 { + for col in 0..cols::NUM_COLUMNS { + assert_eq!(*t.get(row, col), FE::zero(), "padding ({row}, {col})"); + } + } +} + +#[test] +fn test_is_wh_trace_exact_power_of_two_has_no_padding() { + let keys: Vec = (0..8).map(|i| IsWhKey { word: i, half: 0 }).collect(); + let trace = generate_is_wh_trace(&dedup_is_wh_rows(keys)); + assert_eq!(trace.num_rows(), 8); + for row in 0..8 { + assert_eq!(*trace.main_table.get(row, cols::MU), FE::one()); + } +} + +// ========================================================================= +// BITWISE collector +// ========================================================================= + +fn half_op(v: u16) -> BitwiseOperation { + BitwiseOperation::halfword(BitwiseOperationType::IsHalf, v as u8, (v >> 8) as u8) +} + +fn b20_op(v: u64) -> BitwiseOperation { + BitwiseOperation::b20(v as u8, (v >> 8) as u8, (v >> 16) as u8) +} + +/// Every lookup the collector counts, one op per unit of multiplicity. +fn expected_ops(rows: &[(IsWhKey, u64)], padding: usize) -> Vec { + let mut ops = Vec::new(); + for (key, mu) in rows { + for _ in 0..*mu { + ops.push(half_op(key.half)); + ops.push(half_op((key.word & 0xFFFF) as u16)); + ops.push(half_op((key.word >> 16) as u16)); + } + ops.push(b20_op(*mu)); + } + ops.extend(std::iter::repeat_n(b20_op(0), padding)); + ops +} + +#[test] +fn test_is_wh_collector_counts_mu_bound_and_padding() { + let keys = [A, B, A]; + let mut got = BitwiseHistogram::new(); + collect_bitwise_from_is_wh(&dedup_is_wh_rows(keys), &mut got); + + // Rows (A, 2), (B, 1), two padding rows each sending IS_B20[0]. + let mut want = BitwiseHistogram::new(); + want.add_ops(&expected_ops(&[(A, 2), (B, 1)], 2)); + assert!(got == want, "collector disagrees with the table's sends"); +} + +#[test] +fn test_is_wh_collector_counts_nothing_without_sends() { + // No sends: `generate_optional` emits no table, so no padding either. + let mut got = BitwiseHistogram::new(); + collect_bitwise_from_is_wh(&[], &mut got); + assert!(got == BitwiseHistogram::new()); +} + +// ========================================================================= +// KECCAK state_ptr as DWordWHH +// ========================================================================= + +/// `state_ptr[lane]` recomposed from its three limbs. +fn state_ptr_value(t: &stark::trace::TraceTable, lane: usize) -> u64 { + let limb = |l: usize| { + t.main_table + .get(0, keccak_cols::state_ptr(lane, l)) + .canonical_u64() + }; + limb(0) | (limb(1) << 16) | (limb(2) << 32) +} + +/// The ADD from `addr` to `state_ptr` has to carry across both limb boundaries +/// of a DWordWHH: into `half_mid` at 2^16 and into `word_hi` at 2^32. +#[test] +fn test_keccak_state_ptr_whh_across_limb_boundaries() { + let air = busless_air(keccak_cols::NUM_COLUMNS, KeccakConstraints); + for state_addr in [ + 0x1000, + 0x0000_0000_FFFF_FFA0, // lanes cross 2^32 (word_hi 0 → 1) + 0x0000_FFFF_FFFF_FFA0, // lanes cross 2^48 (word_hi low half wraps) + 0x0000_0000_0000_FFF8, // lane 1 crosses 2^16 (half_mid 0 → 1) + ] { + let op = keccak_op(state_addr); + let trace = generate_keccak_trace(std::slice::from_ref(&op)); + for lane in 0..25 { + assert_eq!( + state_ptr_value(&trace, lane), + state_addr + 8 * lane as u64, + "state_ptr[{lane}] for addr {state_addr:#x}" + ); + } + assert!( + validate_busless(&air, &trace), + "honest KECCAK trace must satisfy the ADD for addr {state_addr:#x}" + ); + + // The IS_WH keys are the top 48 bits of the same pointers. + let keys: Vec = keccak::is_wh_keys(std::slice::from_ref(&op)).collect(); + assert_eq!(keys.len(), 25); + for (lane, key) in keys.iter().enumerate() { + assert_eq!(*key, IsWhKey::of_dword(state_addr + 8 * lane as u64)); + } + } +} + +/// A `state_ptr` whose limbs describe a different address than `addr + 8·lane` +/// is rejected by the ADD, so the IS_WH keys cannot drift from the real pointers. +#[test] +fn test_keccak_state_ptr_whh_rejects_a_shifted_word() { + let air = busless_air(keccak_cols::NUM_COLUMNS, KeccakConstraints); + let mut trace = generate_keccak_trace(&[keccak_op(0x1000)]); + let col = keccak_cols::state_ptr(3, 2); + let old = *trace.main_table.get(0, col); + trace.main_table.set(0, col, old + FE::one()); + assert!(!validate_busless(&air, &trace)); +} + +// ========================================================================= +// End to end: the IS_B20 bound on μ +// ========================================================================= + +/// Moves `delta` onto the BITWISE `IS_B20` receiver row for `value`. +fn bump_b20(traces: &mut Traces, value: u64, delta: FE) { + let bw = &mut traces.bitwise.main_table; + let row = bw_row_index(value as u8, (value >> 8) as u8, (value >> 16) as u8); + let old = *bw.get(row, bw_cols::MU_IS_B20); + bw.set(row, bw_cols::MU_IS_B20, old + delta); +} + +/// Runs the asm program `name` and builds its traces with the full +/// preprocessed BITWISE table, the one a range-check forgery has to get past. +fn full_traces(name: &str) -> (Vec, Elf, Traces) { + let elf_bytes = asm_elf_bytes(name); + let program = Elf::load(&elf_bytes).expect("ELF load"); + let logs = Executor::new(&program, vec![]) + .expect("executor construction") + .run() + .expect("run") + .logs; + let traces = Traces::from_elf_and_logs( + &program, + &logs, + &MaxRowsConfig::default(), + &[], + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("trace build"); + (elf_bytes, program, traces) +} + +/// Proves `test_keccak` after letting `rewrite` reshape the IS_WH rows, and +/// returns whether the verifier accepts. The prover is the malicious one: it +/// skips no check of its own, it simply builds a proof over the rewritten trace. +fn prove_keccak_with(rewrite: impl FnOnce(&mut Traces)) -> bool { + prove_asm_with("test_keccak", rewrite) +} + +/// [`prove_keccak_with`] for any asm program. +fn prove_asm_with(name: &str, rewrite: impl FnOnce(&mut Traces)) -> bool { + let options = crate::GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 is valid"); + let (elf_bytes, program, mut traces) = full_traces(name); + + rewrite(&mut traces); + + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &program, + &options, + false, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + None, + ); + let runtime_page_ranges = traces.runtime_page_ranges(); + let num_private_input_pages = traces + .page_configs + .iter() + .filter(|c| c.is_private_input) + .count(); + let mut transcript = DefaultTranscript::::new(&[]); + absorb_statement( + &mut transcript, + StatementKind::Monolithic, + &elf_bytes, + &traces.public_output_bytes, + &table_counts, + num_private_input_pages, + &runtime_page_ranges, + options.fri_final_poly_log_degree, + ); + let proof = Prover::multi_prove( + airs.air_trace_pairs(&mut traces), + &mut transcript, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("prover must build the crafted proof; a prover refusal is not a verifier rejection"); + let proof = VmProof { + proof, + runtime_page_ranges, + table_counts, + public_output: traces.public_output_bytes.clone(), + num_private_input_pages, + }; + crate::verify_with_options(&proof, &elf_bytes, &options, None, None) + .expect("verify must not error") +} + +/// The same forgery on `test_keccak`, weighed instead of only verified: tells a +/// rejection by the bus balance apart from one anywhere else in the verifier +/// (see `assert_only_the_bus_rejected`). +fn weigh_keccak_with(rewrite: impl FnOnce(&mut Traces)) -> BusOutcome { + let (_, program, mut traces) = full_traces("test_keccak"); + rewrite(&mut traces); + weigh_the_bus_with(&program, &mut traces, true, false) +} + +/// Splits IS_WH row 0 (μ = m) into `m − moved` on row 0 and `moved` on the +/// first padding row, copying the key, and rebalances every BITWISE receiver +/// that has a row for the values involved. The IS_WH and IS_HALFWORD sums are +/// unchanged by construction (both rows carry the same key); only the IS_B20 +/// bound sees the split. +fn split_first_row(traces: &mut Traces, moved: FE) { + let t = &mut traces.is_whs[0].main_table; + let m = t.get(0, cols::MU).canonical_u64(); + assert!( + m >= 2, + "test_keccak's 25 lanes must share a key for this split" + ); + let pad = (0..t.height) + .find(|&r| *t.get(r, cols::MU) == FE::zero()) + .expect("a padding row"); + for col in [cols::VALUE_0, cols::VALUE_1, cols::VALUE_2] { + let v = *t.get(0, col); + t.set(pad, col, v); + } + let kept = FE::from(m) - moved; + t.set(0, cols::MU, kept); + t.set(pad, cols::MU, moved); + + // IS_B20 ×1 per row: row 0 moved from m to `kept`, the padding row from 0 + // to `moved`. A value outside [0, 2^20) has no BITWISE row to move onto. + // Read off the table's own sends, as the attacker would: with the bound + // removed there is nothing to rebalance and the forgery must go through, + // which is what keeps the negative test below falsifiable. + let b20: u64 = BusId::IsB20.into(); + if !is_wh::bus_interactions().iter().any(|bi| bi.bus_id == b20) { + return; + } + bump_b20(traces, m, -FE::one()); + bump_b20(traces, 0, -FE::one()); + for v in [kept, moved] { + let v = v.canonical_u64(); + if v <= IS_WH_MU_MAX { + bump_b20(traces, v, FE::one()); + } + } +} + +/// Control: a split into two positive multiplicities is an honest witness (the +/// same shape `dedup_is_wh_rows` produces past `IS_WH_MU_MAX`) and verifies. +/// This is what makes the rejection below attributable to the sign of μ alone. +#[test] +fn test_is_wh_positive_split_verifies() { + assert!(prove_keccak_with(|t| split_first_row(t, FE::one()))); +} + +/// The carrier #1017 closes: a μ = −1 row with an honest twin at μ = m + 1 +/// leaves the IS_WH and IS_HALFWORD sums untouched, so without the IS_B20 bound +/// the row would be free to receive range checks it never sends. The bound +/// sends `IS_B20[p − 1]`, which BITWISE has no row for. +#[test] +fn test_is_wh_negative_mu_is_rejected() { + assert!(!prove_keccak_with(|t| split_first_row(t, -FE::one()))); +} + +/// The honest proof of the fixture, so the two above are not both vacuous. +#[test] +fn test_is_wh_honest_keccak_verifies() { + assert!(prove_keccak_with(|t| { + assert_eq!(t.is_whs.len(), 1, "test_keccak must ship an IS_WH table"); + })); +} + +// ========================================================================= +// End to end: the IS_HALFWORD checks on the key +// ========================================================================= +// +// A key limb is only bound by IS_WH's own IS_HALFWORD sends: the `IS_WH` bus +// carries the Word packed (`value[1] + 2^16·value[2]`) and KECCAK's memory sends +// carry `half_lo + 2^16·half_mid`, so a non-canonical split of either sum keeps +// both buses and the ADD balanced. The forgeries below rebalance BITWISE from +// the IS_HALFWORD sends IS_WH declares, as the attacker would: with a send +// removed (and its count dropped from the collector) there is nothing to +// rebalance for that limb and the forgery must go through, which is what keeps +// the rejections falsifiable. + +/// IS_WH columns that IS_WH sends an `IS_HALFWORD` check on. +fn is_wh_half_checked_columns() -> Vec { + let half: u64 = BusId::IsHalfword.into(); + is_wh::bus_interactions() + .iter() + .filter(|bi| bi.bus_id == half && bi.is_sender) + .filter_map(|bi| match bi.values.as_slice() { + [stark::lookup::BusValue::Packed { start_column, .. }] => Some(*start_column), + _ => None, + }) + .collect() +} + +/// Moves `delta` onto the BITWISE `IS_HALFWORD` receiver row for `value`. A +/// value outside `[0, 2^16)` has no row to move onto, so it is left unbalanced. +fn bump_half(traces: &mut Traces, value: FE, delta: FE) { + let v = value.canonical_u64(); + if v >= 1 << 16 { + return; + } + let bw = &mut traces.bitwise.main_table; + let row = bw_row_index(v as u8, (v >> 8) as u8, 0); + let old = *bw.get(row, bw_cols::MU_IS_HALF); + bw.set(row, bw_cols::MU_IS_HALF, old + delta); +} + +/// `lo + 2^16·hi` split again with `lo` replaced by `new_lo`: `hi` absorbs the +/// difference, so the pair packs to the same field element. Unless +/// `new_lo == lo`, the new `hi` is far outside `[0, 2^16)`. +fn resplit_keeping_lo(lo: FE, hi: FE, new_lo: FE) -> (FE, FE) { + let inv_2_16 = FE::from(1u64 << 16).inv().expect("2^16 is invertible"); + (new_lo, hi + (lo - new_lo) * inv_2_16) +} + +/// Rewrites the Word of IS_WH row 0 into a non-canonical pair of halves with +/// the same packing, so it still receives the honest `IS_WH` sends. The limb at +/// `out_of_range` (`VALUE_1` or `VALUE_2`) leaves `[0, 2^16)`; the other limb +/// moves to a different in-range value. `None` rewrites the row to itself +/// through the same steps. +fn resplit_word(traces: &mut Traces, out_of_range: Option) { + let t = &mut traces.is_whs[0].main_table; + let m = *t.get(0, cols::MU); + let (v1, v2) = (*t.get(0, cols::VALUE_1), *t.get(0, cols::VALUE_2)); + let flip = |v: FE| FE::from(v.canonical_u64() ^ 1); + let (n1, n2) = match out_of_range { + None => (v1, v2), + Some(c) if c == cols::VALUE_2 => resplit_keeping_lo(v1, v2, flip(v1)), + Some(_) => { + // `v1 + 2^16·v2` with `v2` replaced: `v1` absorbs `2^16·(v2 − v2')`. + let n2 = flip(v2); + (v1 + (v2 - n2) * FE::from(1u64 << 16), n2) + } + }; + assert_eq!( + n1 + n2 * FE::from(1u64 << 16), + v1 + v2 * FE::from(1u64 << 16) + ); + t.set(0, cols::VALUE_1, n1); + t.set(0, cols::VALUE_2, n2); + + for col in is_wh_half_checked_columns() { + let (old, new) = match col { + c if c == cols::VALUE_1 => (v1, n1), + c if c == cols::VALUE_2 => (v2, n2), + _ => continue, + }; + bump_half(traces, old, -m); + bump_half(traces, new, m); + } +} + +/// Control: the rewrite path of the test below with the Word left canonical +/// verifies, so its BITWISE rebalancing is what an honest witness needs. +#[test] +fn test_is_wh_canonical_word_rewrite_verifies() { + assert!(prove_keccak_with(|t| resplit_word(t, None))); +} + +/// An IS_WH row whose Word is split into halves that pack to the honest Word +/// but are not both halfwords. It receives the honest `IS_WH` sends, so only its +/// own `IS_HALFWORD` check on the bad limb can reject it — once per Word limb. +#[test] +fn test_is_wh_noncanonical_word_is_rejected() { + for limb in [cols::VALUE_1, cols::VALUE_2] { + let what = format!("an IS_WH row with column {limb} out of range"); + assert!( + !prove_keccak_with(|t| resplit_word(t, Some(limb))), + "{what} must not verify" + ); + assert_only_the_bus_rejected(&weigh_keccak_with(|t| resplit_word(t, Some(limb))), &what); + } +} + +/// Moves lane 0 of the real KECCAK row onto its own IS_WH row: IS_WH row 0 +/// gives up one send (μ = m − 1) and the first padding row takes it (μ = 1). +/// With `noncanonical`, lane 0's `state_ptr` is also resplit as +/// `(half_lo ^ 1, half_mid')` with the same `half_lo + 2^16·half_mid`, so the +/// ADD and the memory address are untouched while `half_mid'` leaves +/// `[0, 2^16)`; the new IS_WH row carries that key. +fn move_lane_0_to_own_row(traces: &mut Traces, noncanonical: bool) { + let k = &mut traces.keccaks[0].main_table; + assert_eq!( + *k.get(0, keccak_cols::MU), + FE::one(), + "KECCAK row 0 is real" + ); + let (lo_col, mid_col) = (keccak_cols::state_ptr(0, 0), keccak_cols::state_ptr(0, 1)); + let (lo, mid) = (*k.get(0, lo_col), *k.get(0, mid_col)); + let (new_lo, new_mid) = if noncanonical { + resplit_keeping_lo(lo, mid, FE::from(lo.canonical_u64() ^ 1)) + } else { + (lo, mid) + }; + k.set(0, lo_col, new_lo); + k.set(0, mid_col, new_mid); + // KECCAK's own IS_HALFWORD[half_lo] (the IS_WHH template): both in range. + bump_half(traces, lo, -FE::one()); + bump_half(traces, new_lo, FE::one()); + + let t = &mut traces.is_whs[0].main_table; + assert_eq!( + *t.get(0, cols::VALUE_0), + mid, + "lane 0 sends IS_WH row 0's key" + ); + let m = t.get(0, cols::MU).canonical_u64(); + assert!(m >= 2, "test_keccak's 25 lanes must share a key"); + let pad = (0..t.height) + .find(|&r| *t.get(r, cols::MU) == FE::zero()) + .expect("a padding row"); + let row_0: Vec = (0..cols::MU).map(|c| *t.get(0, c)).collect(); + let mut new_row = row_0.clone(); + new_row[cols::VALUE_0] = new_mid; + for (c, v) in new_row.iter().enumerate() { + t.set(pad, c, *v); + } + t.set(0, cols::MU, FE::from(m - 1)); + t.set(pad, cols::MU, FE::one()); + + let b20: u64 = BusId::IsB20.into(); + if is_wh::bus_interactions().iter().any(|bi| bi.bus_id == b20) { + bump_b20(traces, m, -FE::one()); + bump_b20(traces, m - 1, FE::one()); + bump_b20(traces, 0, -FE::one()); + bump_b20(traces, 1, FE::one()); + } + for col in is_wh_half_checked_columns() { + bump_half(traces, row_0[col], -FE::one()); + bump_half(traces, new_row[col], FE::one()); + } +} + +/// Control: giving one lane its own row with the honest key is an honest +/// witness and verifies, so the rejection below is the resplit alone. +#[test] +fn test_keccak_lane_on_its_own_is_wh_row_verifies() { + assert!(prove_keccak_with(|t| move_lane_0_to_own_row(t, false))); +} + +/// A `state_ptr` resplit as `(half_lo ^ 1, half_mid')` that keeps +/// `half_lo + 2^16·half_mid`: the ADD, the memory sends and KECCAK's +/// `IS_HALFWORD[half_lo]` all still hold, and IS_WH has a row for the new key. +/// Only that row's `IS_HALFWORD[value[0]]` sees `half_mid'` out of range. +#[test] +fn test_keccak_noncanonical_state_ptr_is_rejected() { + let what = "a KECCAK state_ptr with half_mid out of range"; + assert!( + !prove_keccak_with(|t| move_lane_0_to_own_row(t, true)), + "{what} must not verify" + ); + assert_only_the_bus_rejected( + &weigh_keccak_with(|t| move_lane_0_to_own_row(t, true)), + what, + ); +} + +// ========================================================================= +// End to end: more than one key, continuations and recursion +// ========================================================================= + +/// `test_keccak_64k` puts the state right across a 64 KiB boundary, so its +/// lanes carry two keys: IS_WH ships two real rows, 12 lanes below the +/// boundary and 13 above, and the proof verifies. +#[test] +fn test_keccak_state_across_64k_boundary_verifies() { + assert!(prove_asm_with("test_keccak_64k", |t| { + assert_eq!(t.is_whs.len(), 1); + let is_wh = &t.is_whs[0].main_table; + let rows: Vec<(u64, u64)> = (0..is_wh.height) + .map(|r| { + ( + is_wh.get(r, cols::VALUE_0).canonical_u64(), + is_wh.get(r, cols::MU).canonical_u64(), + ) + }) + .filter(|&(_, mu)| mu > 0) + .collect(); + assert_eq!(rows.len(), 2, "two keys: {rows:?}"); + assert_eq!(rows[1].0, (rows[0].0 + 1) & 0xFFFF, "adjacent halves"); + assert_eq!((rows[0].1, rows[1].1), (12, 13)); + })); +} + +/// Continuations ship IS_WH per epoch: the epoch that runs the keccak ecall +/// has an IS_WH table and the others do not, and the bundle verifies. +#[test] +fn test_keccak_continuation_carries_is_wh_in_its_epoch() { + let elf_bytes = asm_elf_bytes("test_keccak_64k"); + let opts = crate::recursion::MIN_PROOF_OPTIONS; + let bundle = crate::continuation::prove_continuation(&elf_bytes, &[], 4, &opts) + .expect("continuation prove"); + let is_wh: Vec = bundle + .epoch_table_counts() + .iter() + .map(|c| c.is_wh) + .collect(); + assert!(is_wh.len() > 1, "16-cycle epochs must split the program"); + assert_eq!( + is_wh.iter().filter(|&&n| n == 1).count(), + 1, + "exactly the keccak epoch ships IS_WH: {is_wh:?}" + ); + assert!(is_wh.iter().all(|&n| n <= 1)); + crate::continuation::verify_continuation(&elf_bytes, &bundle, &opts) + .expect("verify_continuation errored") + .expect("a keccak bundle must verify"); +} + +/// The recursion guest's verify path (mirrored on the host) on an inner proof +/// that contains IS_WH: the blob carries `is_wh = 1` and still verifies and +/// attests. +#[test] +fn test_recursion_blob_with_is_wh_verifies_on_host() { + use crate::recursion::{self, MIN_PROOF_OPTIONS}; + + let elf_bytes = asm_elf_bytes("test_keccak_64k"); + let inner = crate::prove_with_options_and_inputs( + &elf_bytes, + &[], + &MIN_PROOF_OPTIONS, + &MaxRowsConfig::default(), + ) + .expect("inner prove"); + assert_eq!(inner.table_counts.is_wh, 1); + + let blob = + recursion::encode_guest_input(&inner, &elf_bytes, &MIN_PROOF_OPTIONS).expect("encode"); + let attestation = recursion::verify_and_attest_blob(&blob, &MIN_PROOF_OPTIONS) + .expect("verify_and_attest_blob errored") + .expect("an inner proof with IS_WH must verify on the guest path"); + let output = recursion::check_attestation(&attestation, &elf_bytes, &MIN_PROOF_OPTIONS) + .expect("check_attestation errored") + .expect("attestation must bind to the inner ELF"); + assert_eq!(output, inner.public_output); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 398949e67..7e4462b68 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -55,6 +55,8 @@ pub mod hint_tests; #[cfg(test)] pub mod ir_stats_dump; #[cfg(test)] +pub mod is_wh_tests; +#[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] pub mod keccak_tests; diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs index dd680f9e7..6901ca36d 100644 --- a/prover/src/tests/ood_window_ir_tests.rs +++ b/prover/src/tests/ood_window_ir_tests.rs @@ -115,4 +115,5 @@ fn all_table_windows_match_captured_ir() { assert_ood_window_matches_ir(&create_ecsm_air(&opts), true, "ECSM"); assert_ood_window_matches_ir(&create_ecdas_air(&opts), true, "ECDAS"); assert_ood_window_matches_ir(&create_hint_air(&opts), true, "HINT"); + assert_ood_window_matches_ir(&create_is_wh_air(&opts), true, "IS_WH"); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 42e63e831..755d835bd 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -101,6 +101,19 @@ pub(crate) fn weigh_the_bus( elf: &Elf, traces: &mut Traces, recheck_with_moved_target: bool, +) -> BusOutcome { + weigh_the_bus_with(elf, traces, recheck_with_moved_target, true) +} + +/// [`weigh_the_bus`] with the BITWISE table picked by `minimal_bitwise`: pass +/// `false` for traces from `Traces::from_elf_and_logs`, whose BITWISE is the +/// full preprocessed table. A forgery that leaves a range check out of range +/// needs that one: the minimal table's rows are the prover's to choose. +pub(crate) fn weigh_the_bus_with( + elf: &Elf, + traces: &mut Traces, + recheck_with_moved_target: bool, + minimal_bitwise: bool, ) -> BusOutcome { let _ = env_logger::builder().is_test(true).try_init(); let proof_options = ProofOptions::default_test_options(); @@ -110,7 +123,7 @@ pub(crate) fn weigh_the_bus( let airs = VmAirs::new( elf, &proof_options, - true, + minimal_bitwise, &traces.page_configs, &table_counts, None, @@ -3386,6 +3399,7 @@ fn test_verify_rejects_zero_table_counts() { ecsm: 0, ecdas: 0, hint: 0, + is_wh: 0, }, ..vm_proof }; @@ -3476,6 +3490,7 @@ fn test_crafted_zero_count_proof_must_not_verify() { ecsm: 0, ecdas: 0, hint: 0, + is_wh: 0, }; let airs = VmAirs::new( &elf, diff --git a/prover/src/tests/skip_empty_tables_tests.rs b/prover/src/tests/skip_empty_tables_tests.rs index fe69a0be3..b1d6401ef 100644 --- a/prover/src/tests/skip_empty_tables_tests.rs +++ b/prover/src/tests/skip_empty_tables_tests.rs @@ -36,7 +36,8 @@ fn run_rust_elf(name: &str) -> (Elf, ExecutionResult) { (elf, result) } -/// The claim every drop-forgery below makes, in one place. +/// The claim every drop-forgery below makes, in one place (the IS_WH range +/// forgeries in `is_wh_tests` make it too). /// /// `multi_verify_views` returns `false` from about ten places, so /// `assert!(!accepted)` on its own would pass just as happily if the forged @@ -44,11 +45,11 @@ fn run_rust_elf(name: &str) -> (Elf, ExecutionResult) { /// check — the opposite of what these tests say they demonstrate. Moving the /// target onto the sum the forgery actually produced is what separates them: if /// the same proof then verifies, the balance was the only objection. -fn assert_only_the_bus_rejected(outcome: &BusOutcome, what: &str) { - assert!(!outcome.accepted, "dropping {what} must not verify"); +pub(crate) fn assert_only_the_bus_rejected(outcome: &BusOutcome, what: &str) { + assert!(!outcome.accepted, "{what} must not verify"); assert_ne!( outcome.contribution_sum, outcome.target, - "dropping {what} left the bus balanced, so the rejection came from \ + "{what} left the bus balanced, so the rejection came from \ elsewhere and the bus did not notice the forgery at all" ); assert!( @@ -99,6 +100,7 @@ fn every_table_participates_in_the_bus() { ecsm: 1, ecdas: 1, hint: 1, + is_wh: 1, }; let airs = VmAirs::new( &elf, @@ -126,7 +128,7 @@ fn every_table_participates_in_the_bus() { } /// The tables a prover can declare away, under the names the AIRs carry. The -/// always-present ones (BITWISE, DECODE, KECCAK_RC, REGISTER, HALT, the PAGEs, +/// always-present ones (BITWISE, DECODE, KECCAK_RC, COPY, REGISTER, HALT, the PAGEs, /// L2G) have no `TableCounts` field, and they legitimately contribute zero when /// the run never reaches them — KECCAK_RC does exactly that in a program with no /// keccak, which is the padding this change is about and cannot be dropped. @@ -156,6 +158,7 @@ fn droppable_air_names(counts: &TableCounts) -> Vec<&'static str> { ecsm, ecdas, hint, + is_wh, } = counts; [ ("CPU", cpu), @@ -177,6 +180,7 @@ fn droppable_air_names(counts: &TableCounts) -> Vec<&'static str> { ("ECSM", ecsm), ("ECDAS", ecdas), ("HINT", hint), + ("IS_WH", is_wh), ] .into_iter() .map(|(name, _count)| name) @@ -371,12 +375,13 @@ fn dropping_a_used_table_through_the_real_verifier_is_rejected() { /// PAGE, REGISTER, GLOBAL_MEMORY — are exactly the mandatory ones, and nothing /// enforced that this stays true. /// -/// One exception, by bus: `ARE_BYTES` byte checks the spec gives no `cond` -/// (default 1) — the μ bounds of the dedup tables (spec #1017), SHIFT's -/// `shift[0..1]` bytes and KECCAK_RND's θ/ρ bytes. A padding row sends them as -/// `ARE_BYTES[0, 0]`, which is in range — the test checks this by requiring each -/// value to vanish on an all-zero row (columns only, no nonzero constant term) — -/// and their only counterparty is BITWISE, whose multiplicity columns are +/// One exception, by bus: `ARE_BYTES` and `IS_B20` range checks the spec gives +/// no `cond` (default 1) — the μ bounds of the dedup tables (spec #1017, an +/// `IS_B20[μ]` on IS_WH), SHIFT's `shift[0..1]` bytes and KECCAK_RND's θ/ρ +/// bytes. A padding row sends them as `ARE_BYTES[0, 0]` / `IS_B20[0]`, which is +/// in range — the test checks this by requiring each value to vanish on an +/// all-zero row (columns only, no nonzero constant term) — and their only +/// counterparty is BITWISE, whose multiplicity columns are /// free witnesses, so the contribution is absorbed whichever way an unused chip /// went; and an optional table with no ops is never shipped /// (`chunk_and_generate_optional`/`generate_optional` return no table), so the @@ -385,11 +390,11 @@ fn dropping_a_used_table_through_the_real_verifier_is_rejected() { #[test] fn no_optional_table_uses_a_constant_multiplicity() { use crate::tables::{ - branch, bytewise, cpu32, dvrm, ecdas, ecsm, eq, hint, keccak, keccak_rnd, load, lt, memw, - memw_aligned, mul, shift, store, + branch, bytewise, cpu32, dvrm, ecdas, ecsm, eq, hint, is_wh, keccak, keccak_rnd, load, lt, + memw, memw_aligned, mul, shift, store, }; use stark::lookup::{BusValue, LinearTerm}; - let optional: [(&str, Vec); 17] = [ + let optional: [(&str, Vec); 18] = [ ("LT", lt::bus_interactions()), ("MEMW", memw::bus_interactions()), ("MEMW_A", memw_aligned::bus_interactions()), @@ -407,6 +412,7 @@ fn no_optional_table_uses_a_constant_multiplicity() { ("ECSM", ecsm::bus_interactions()), ("ECDAS", ecdas::bus_interactions()), ("HINT", hint::bus_interactions()), + ("IS_WH", is_wh::bus_interactions()), ]; for (name, interactions) in optional { assert!( @@ -414,13 +420,15 @@ fn no_optional_table_uses_a_constant_multiplicity() { "{name} declares no bus interactions" ); for (i, interaction) in interactions.iter().enumerate() { + use crate::tables::types::BusId; let zero_on_padding = interaction.values.iter().all(|value| match value { BusValue::Packed { .. } => true, BusValue::Linear(terms) => terms .iter() .all(|term| !matches!(term, LinearTerm::Constant(c) if *c != 0)), }); - let byte_check = interaction.bus_id == u64::from(crate::tables::types::BusId::AreBytes) + let byte_check = (interaction.bus_id == u64::from(BusId::AreBytes) + || interaction.bus_id == u64::from(BusId::IsB20)) && interaction.is_sender && zero_on_padding; assert!( @@ -529,7 +537,7 @@ fn omitting_a_table_whose_ops_ran_fails_the_bus_balance() { "validate deliberately lets this through — the bus is what rejects it" ); - assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "MUL"); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "dropping MUL"); } /// What `validate` still refuses: a proof with no CPU describes no execution, @@ -557,8 +565,8 @@ fn validate_still_requires_cpu_and_the_register_file() { } /// The counts ride in the proof, so they are the prover's to choose, and the -/// sub-proof cross-check constrains only their *sum*. The five accelerators are -/// not chunked — `generate_optional` emits one table or none — so any count +/// sub-proof cross-check constrains only their *sum*. The five accelerators and +/// IS_WH are not chunked — `generate_optional` emits one table or none — so any count /// above 1 describes a table set no prover can build, and the sum alone does not /// catch it: lower another count by the same amount and the total still matches. /// This pins the per-field shape. @@ -583,12 +591,13 @@ fn an_accelerator_count_above_one_is_rejected() { // Named setters rather than a match with a catch-all: a wrong field would // otherwise pass the assertion below while testing the wrong count. type SetCount = fn(&mut TableCounts); - let inflate: [(&str, SetCount); 5] = [ + let inflate: [(&str, SetCount); 6] = [ ("keccak", |c| c.keccak = 2), ("keccak_rnd", |c| c.keccak_rnd = 2), ("ecsm", |c| c.ecsm = 2), ("ecdas", |c| c.ecdas = 2), ("hint", |c| c.hint = 2), + ("is_wh", |c| c.is_wh = 2), ]; for (name, set_to_two) in inflate { let mut counts = honest.clone(); @@ -599,8 +608,8 @@ fn an_accelerator_count_above_one_is_rejected() { ); } - // The chunked chips keep taking any count: this is a cap on the five, not a - // cap on chunking. + // The chunked chips keep taking any count: this is a cap on the five + // accelerators and IS_WH, not a cap on chunking. let mut many_mul = honest.clone(); many_mul.mul = 7; assert!(many_mul.validate().is_ok(), "chunked chips still chunk"); @@ -637,9 +646,9 @@ fn counts_that_wrap_have_no_total() { /// The accelerators are the ones a run most often never reaches, and each cost a /// four-row sub-proof regardless. A program with no keccak, no EC and no hint -/// ecall now carries none of the five. +/// ecall now carries none of the five, nor the IS_WH table KECCAK feeds. #[test] -fn a_run_without_accelerators_omits_all_five() { +fn a_run_without_accelerators_omits_all_five_and_is_wh() { let (elf, logs, _instructions) = run_asm_elf("xori"); let mut traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); @@ -651,6 +660,8 @@ fn a_run_without_accelerators_omits_all_five() { ("ecsm", counts.ecsm), ("ecdas", counts.ecdas), ("hint", counts.hint), + // Not an accelerator, but only KECCAK feeds it today. + ("is_wh", counts.is_wh), ] { assert_eq!( count, 0, @@ -685,7 +696,7 @@ fn omitting_a_used_accelerator_fails_the_bus_balance() { ); traces.hints.clear(); - assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "HINT"); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "dropping HINT"); } /// The dispatch above is CPU-to-chip. KECCAK_RND is reached from KECCAK, not @@ -708,7 +719,34 @@ fn omitting_a_chip_dispatched_by_another_chip_fails_the_bus_balance() { ); traces.keccak_rnds.clear(); - assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "KECCAK_RND"); + assert_only_the_bus_rejected( + &weigh_the_bus(&elf, &mut traces, true), + "dropping KECCAK_RND", + ); +} + +/// IS_WH is reached from a chip's range checks rather than from a dispatch: it +/// receives the `IS_WH` half of every `IS_WHH` send (today KECCAK's +/// `state_ptr`). Dropping it leaves those sends unmatched — and unlike the +/// BITWISE range checks, whose receiver multiplicities are free witnesses, no +/// other table receives `IS_WH`, so nothing can absorb them. +#[test] +fn omitting_the_is_wh_table_fails_the_bus_balance() { + let (elf, logs, _instructions) = run_asm_elf("test_keccak"); + let mut traces = + Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap(); + assert!( + !traces.is_whs.is_empty(), + "test_keccak must exercise IS_WH for this to be a forgery" + ); + + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "the honest proof must verify first, or the negative below proves nothing" + ); + + traces.is_whs.clear(); + assert_only_the_bus_rejected(&weigh_the_bus(&elf, &mut traces, true), "dropping IS_WH"); } /// The committed output is the one bus target that is not zero: the verifier @@ -741,5 +779,5 @@ fn dropping_the_committed_output_fails_the_bus_balance() { outcome.target, honest_target, "clearing the public output must move the target" ); - assert_only_the_bus_rejected(&outcome, "the committed output"); + assert_only_the_bus_rejected(&outcome, "dropping the committed output"); } diff --git a/prover/src/tests/statement_tests.rs b/prover/src/tests/statement_tests.rs index 68dc20023..830ecf7af 100644 --- a/prover/src/tests/statement_tests.rs +++ b/prover/src/tests/statement_tests.rs @@ -28,6 +28,7 @@ fn sample_counts() -> TableCounts { ecsm: 1, ecdas: 1, hint: 1, + is_wh: 1, } } @@ -96,6 +97,7 @@ fn each_count_mut(counts: &mut TableCounts) -> Vec<(&'static str, &mut usize)> { ecsm, ecdas, hint, + is_wh, } = counts; vec![ ("cpu", cpu), @@ -117,6 +119,7 @@ fn each_count_mut(counts: &mut TableCounts) -> Vec<(&'static str, &mut usize)> { ("ecsm", ecsm), ("ecdas", ecdas), ("hint", hint), + ("is_wh", is_wh), ] } @@ -133,7 +136,7 @@ fn state_depends_on_every_table_count() { .into_iter() .map(|(name, _)| name) .collect(); - assert_eq!(names.len(), 19, "every count must be probed"); + assert_eq!(names.len(), 20, "every count must be probed"); for name in names { let mut counts = sample_counts(); diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 7bc9026d4..dfd4b0277 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -630,8 +630,10 @@ mod keccak_tests { // θ/ρ halfword shifts are enforced by inline μ-gated identities on the // keccak_rnd chip, so no HWSL lookups are emitted (was 24 * 120). assert_eq!(hwsl, 0, "Hwsl count"); - assert_eq!(is_half, 100, "IsHalf count"); - assert_eq!(ops.len(), 105 + 24 * 1028, "Total bitwise ops"); + // IS_HALF only on each lane's state_ptr half_lo; the top 48 bits go to + // IS_WH (IS_WHH template), whose own checks the IS_WH collector counts. + assert_eq!(is_half, 25, "IsHalf count"); + assert_eq!(ops.len(), 30 + 24 * 1028, "Total bitwise ops"); } #[test] @@ -729,8 +731,8 @@ mod keccak_tests { fn test_keccak_bus_interaction_counts() { assert_eq!( keccak::bus_interactions().len(), - 134, - "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 BYTE_ALU alignment + 4 ARE_BYTES addr pairs + 1 Keccak send + 1 Keccak recv" + 84, + "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 25 IS_WHH (25 IS_WH + 25 IS_HALF) + 1 BYTE_ALU alignment + 4 ARE_BYTES addr pairs + 1 Keccak send + 1 Keccak recv" ); assert_eq!( keccak_rnd::bus_interactions().len(), @@ -749,7 +751,11 @@ mod keccak_tests { #[test] fn test_keccak_column_counts() { - assert_eq!(core_cols::NUM_COLUMNS, 511, "KECCAK core columns"); + assert_eq!( + core_cols::NUM_COLUMNS, + 486, + "KECCAK core columns (state_ptr DWordWHH)" + ); assert_eq!( rnd_cols::NUM_COLUMNS, 1480, diff --git a/prover/tests/gpu_constraint_interp_real.rs b/prover/tests/gpu_constraint_interp_real.rs index 7f60a6bc1..86a1abbbf 100644 --- a/prover/tests/gpu_constraint_interp_real.rs +++ b/prover/tests/gpu_constraint_interp_real.rs @@ -7,7 +7,7 @@ //! per-constraint eval matrix is bit-for-bit identical to the CPU reference //! oracle `eval_device_program`. The oracle is pinned bit-for-bit to the //! compiled prover folder by `tests::constraint_program_device_tests`, so -//! GPU == oracle closes the chain GPU == folder across all 26 tables. +//! GPU == oracle closes the chain GPU == folder across all 27 tables. //! //! Complements the synthetic all-ops coverage in //! `stark`'s `tests/gpu_constraint_interp.rs`: this exercises the kernel on the @@ -272,4 +272,5 @@ fn all_table_programs_gpu_match_cpu_oracle() { check_air(&create_ecdas_air(&opts), "ECDAS"); check_air(&create_copy_air(&opts), "copy"); check_air(&create_hint_air(&opts), "HINT"); + check_air(&create_is_wh_air(&opts), "IS_WH"); }