From 8e4b829389fed9a62beb419955c8d0187f0f975b Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 2 Oct 2026 16:35:09 -0300 Subject: [PATCH 01/13] =?UTF-8?q?Bound=20MUL/DVRM=20multiplicities=20and?= =?UTF-8?q?=20bit-constrain=20SHIFT=20zbs=20and=20=CE=BC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- executor/programs/asm/poc_divu_commit.s | 22 + executor/programs/asm/poc_mul_commit.s | 22 + executor/programs/asm/poc_sll_commit.s | 22 + prover/src/tables/dvrm.rs | 76 ++- prover/src/tables/mul.rs | 77 ++- prover/src/tables/shift.rs | 21 +- prover/src/tables/trace_builder.rs | 158 +++--- prover/src/tests/dvrm_tests.rs | 128 ++++- prover/src/tests/mod.rs | 2 + prover/src/tests/mul_tests.rs | 143 +++++- prover/src/tests/multiplicity_forgery_poc.rs | 485 +++++++++++++++++++ prover/src/tests/shift_tests.rs | 173 ++++++- 12 files changed, 1227 insertions(+), 102 deletions(-) create mode 100644 executor/programs/asm/poc_divu_commit.s create mode 100644 executor/programs/asm/poc_mul_commit.s create mode 100644 executor/programs/asm/poc_sll_commit.s create mode 100644 prover/src/tests/multiplicity_forgery_poc.rs diff --git a/executor/programs/asm/poc_divu_commit.s b/executor/programs/asm/poc_divu_commit.s new file mode 100644 index 000000000..22cab3c7e --- /dev/null +++ b/executor/programs/asm/poc_divu_commit.s @@ -0,0 +1,22 @@ + .text + .attribute 5, "rv64i2p1_m2p0" + .globl main +main: + # Compute 7 / 2 with a real DIVU, spill the quotient to the stack and + # commit it. The committed public output is the DVRM chip's quotient, + # so a proof reporting anything but 3 certifies a false division. + addi a3, zero, 7 + addi a4, zero, 2 + divu t1, a3, a4 # t1 = 7 / 2 + addi sp, sp, -16 + sd t1, 0(sp) # spill to stack + li a0, 1 # fd = 1 + mv a1, sp # buf = sp + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + addi sp, sp, 16 + li a0, 0 + li a7, 93 # syscall = Halt + ecall diff --git a/executor/programs/asm/poc_mul_commit.s b/executor/programs/asm/poc_mul_commit.s new file mode 100644 index 000000000..6bc4000ef --- /dev/null +++ b/executor/programs/asm/poc_mul_commit.s @@ -0,0 +1,22 @@ + .text + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # Compute 3 * 5 with a real MUL, spill the product to the stack and + # commit it. The committed public output is the MUL chip's lo result, + # so a proof reporting anything but 15 certifies a false product. + addi a3, zero, 3 + addi a4, zero, 5 + mul t1, a3, a4 # t1 = 3 * 5 + addi sp, sp, -16 + sd t1, 0(sp) # spill to stack + li a0, 1 # fd = 1 + mv a1, sp # buf = sp + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + addi sp, sp, 16 + li a0, 0 + li a7, 93 # syscall = Halt + ecall diff --git a/executor/programs/asm/poc_sll_commit.s b/executor/programs/asm/poc_sll_commit.s new file mode 100644 index 000000000..9647f48ea --- /dev/null +++ b/executor/programs/asm/poc_sll_commit.s @@ -0,0 +1,22 @@ + .text + .attribute 5, "rv64i2p1" + .globl main +main: + # Compute 1 << 1 with a real SLL, spill the result to the stack and + # commit it. The committed public output is the SHIFT chip's result, + # so a proof reporting anything but 2 certifies a false shift. + addi a3, zero, 1 + addi a4, zero, 1 + sll t1, a3, a4 # t1 = 1 << 1 + addi sp, sp, -16 + sd t1, 0(sp) # spill to stack + li a0, 1 # fd = 1 + mv a1, sp # buf = sp + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + addi sp, sp, 16 + li a0, 0 + li a7, 93 # syscall = Halt + ecall diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index c499a72bf..b388e78cd 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -22,7 +22,7 @@ //! - `sign_n`, `sign_d`, `sign_q`, `sign_r`: Bit - sign bits //! //! ## Bus Interactions -//! - Sender: IS_HALF (×20: n, d, r, n_sub_r, q) +//! - Sender: IS_HALF (×20: n, d, r, n_sub_r, q; ×2: μ_q, μ_r bounds) //! - Sender: MSB16 (×3 for sign extraction: n, d, r) //! - Sender: ALU (×3, on the unified bus: ×1 LT-flavored for `|r| < |d|`, //! ×2 MUL-flavored for `n - r = d * q` lo/hi) @@ -273,19 +273,21 @@ impl DvrmOperation { // Trace generation // ========================================================================= -/// Generates the DVRM trace table from a list of operations. -/// -/// Operations are deduplicated by (n, d, signed). -/// Each unique operation tracks separate multiplicities for quotient and remainder lookups. -/// -/// # Arguments -/// * `operations` - List of (DvrmOperation, wants_remainder) pairs -pub fn generate_dvrm_trace( +/// Largest per-row multiplicity: `μ_q` and `μ_r` are each range-checked to a +/// halfword (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many +/// lookups of each kind. The bound is what makes `μ_q + μ_r = 0` imply +/// `μ_q = μ_r = 0`: without it a `μ_q = 1, μ_r = −1` row receives a quotient +/// lookup while sending none of its checks (forged `n = q·d + r`). +pub const MU_MAX: u64 = (1 << 16) - 1; + +/// Deduplicates DVRM operations into trace rows: `(n, d, signed) -> (μ_q, μ_r)`, +/// splitting an op over several rows when a count exceeds [`MU_MAX`]. Shared by +/// trace generation and the BITWISE collector so the per-row lookups they count +/// cannot drift apart. +pub fn dedup_dvrm_rows( operations: &[(DvrmOperation, bool)], -) -> TraceTable { - // Deduplicate: (n, d, signed) -> (mu_q, mu_r) +) -> Vec<(DvrmOperation, DvrmMultiplicities)> { let mut op_map: HashMap = HashMap::new(); - for (op, wants_remainder) in operations { let entry = op_map.entry(op.clone()).or_default(); if *wants_remainder { @@ -295,7 +297,32 @@ pub fn generate_dvrm_trace( } } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + let mut rows = Vec::with_capacity(op_map.len()); + for (op, mut left) in op_map { + while left.mu_q > 0 || left.mu_r > 0 { + let row = DvrmMultiplicities { + mu_q: left.mu_q.min(MU_MAX), + mu_r: left.mu_r.min(MU_MAX), + }; + left.mu_q -= row.mu_q; + left.mu_r -= row.mu_r; + rows.push((op.clone(), row)); + } + } + rows +} + +/// Generates the DVRM trace table from a list of operations. +/// +/// Operations are deduplicated by (n, d, signed) (see [`dedup_dvrm_rows`]). +/// Each unique operation tracks separate multiplicities for quotient and remainder lookups. +/// +/// # Arguments +/// * `operations` - List of (DvrmOperation, wants_remainder) pairs +pub fn generate_dvrm_trace( + operations: &[(DvrmOperation, bool)], +) -> TraceTable { + let unique_ops = dedup_dvrm_rows(operations); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), @@ -357,6 +384,7 @@ pub fn generate_dvrm_trace( /// /// The DVRM table: /// - **Sends** IS_HALF lookups for n, d, q, r, n_sub_r range checks (×20) +/// and for the μ_q/μ_r multiplicity bounds (×2) /// - **Sends** MSB16 lookups for sign extraction (×3: n, d, r) /// - **Sends** LT lookup for |r| < |d| (×1) /// - **Sends** MUL lookups for n_sub_r = d * q verification (×2: lo and hi) @@ -365,6 +393,28 @@ pub fn generate_dvrm_trace( pub fn bus_interactions() -> Vec { let mut interactions = Vec::new(); + // ------------------------------------------------------------------------- + // IS_HALF[μ_q] | μ_q, IS_HALF[μ_r] | μ_r. + // Every check below fires with μ_q + μ_r, so the multiplicities themselves + // must be bounded and non-negative. Otherwise μ_q = 1, μ_r = −1 receives a + // quotient lookup with all checks off (forged quotient), + // and an honest μ_r = 1 copy of the row cancels the stray −1. Each μ is sent + // with itself as multiplicity: `k` rows holding an out-of-range value `v` + // put weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // (μ = 0) contributes nothing, so an empty instance still matches an absent + // one. See `MU_MAX`. + // ------------------------------------------------------------------------- + for col in [cols::MU_Q, cols::MU_R] { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(col), + vec![BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }], + )); + } + // ------------------------------------------------------------------------- // DVRM-A1.i: IS_HALF[n[i]] (×4) and DVRM-A2.i: IS_HALF[d[i]] (×4), // multiplicity: μ_q + μ_r. diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index a615f74df..b9b2576f5 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -25,7 +25,8 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for sign extraction) -//! - Sender: IS_HALF (×16 for lhs/rhs input and lo/hi output range checks) +//! - Sender: IS_HALF (×16 for lhs/rhs input and lo/hi output range checks, +//! ×2 for the μ_lo/μ_hi multiplicity bounds) //! - Sender: IS_B20 (×4 for carry range checks) //! - Receiver: ALU (×2 for lo and hi results — every MUL lookup, CPU //! MUL/MULH dispatch and dvrm's internal `d*q` consistency) @@ -281,19 +282,21 @@ impl MulOperation { // Trace generation // ========================================================================= -/// Generates the MUL trace table from a list of operations. -/// -/// Operations are deduplicated by (lhs, lhs_signed, rhs, rhs_signed). -/// Each unique operation tracks separate multiplicities for lo and hi lookups. -/// -/// # Arguments -/// * `operations` - List of (MulOperation, wants_hi) pairs -pub fn generate_mul_trace( +/// Largest per-row multiplicity: `μ_lo` and `μ_hi` are each range-checked to a +/// halfword (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many +/// lookups of each kind. The bound is what makes `μ_lo + μ_hi = 0` imply +/// `μ_lo = μ_hi = 0`: without it a `μ_lo = 1, μ_hi = −1` row receives a lookup +/// while sending none of its range checks. +pub const MU_MAX: u64 = (1 << 16) - 1; + +/// Deduplicates MUL operations into trace rows: `(lhs, lhs_signed, rhs, +/// rhs_signed) -> (μ_lo, μ_hi)`, splitting an op over several rows when a count +/// exceeds [`MU_MAX`]. Shared by trace generation and the BITWISE collector so +/// the per-row lookups they count cannot drift apart. +pub fn dedup_mul_rows( operations: &[(MulOperation, bool)], -) -> TraceTable { - // Deduplicate: (lhs, lhs_signed, rhs, rhs_signed) -> (mu_lo, mu_hi) +) -> Vec<(MulOperation, MulMultiplicities)> { let mut op_map: HashMap = HashMap::new(); - for (op, wants_hi) in operations { let entry = op_map.entry(op.clone()).or_default(); if *wants_hi { @@ -303,7 +306,32 @@ pub fn generate_mul_trace( } } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + let mut rows = Vec::with_capacity(op_map.len()); + for (op, mut left) in op_map { + while left.mu_lo > 0 || left.mu_hi > 0 { + let row = MulMultiplicities { + mu_lo: left.mu_lo.min(MU_MAX), + mu_hi: left.mu_hi.min(MU_MAX), + }; + left.mu_lo -= row.mu_lo; + left.mu_hi -= row.mu_hi; + rows.push((op.clone(), row)); + } + } + rows +} + +/// Generates the MUL trace table from a list of operations. +/// +/// Operations are deduplicated by (lhs, lhs_signed, rhs, rhs_signed). +/// Each unique operation tracks separate multiplicities for lo and hi lookups. +/// +/// # Arguments +/// * `operations` - List of (MulOperation, wants_hi) pairs +pub fn generate_mul_trace( + operations: &[(MulOperation, bool)], +) -> TraceTable { + let unique_ops = dedup_mul_rows(operations); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), @@ -358,6 +386,7 @@ pub fn generate_mul_trace( /// The MUL table: /// - **Sends** MSB16 lookups for sign bit extraction (×2) /// - **Sends** IS_HALF lookups for lhs/rhs input and lo/hi output range checks (×16) +/// and for the μ_lo/μ_hi multiplicity bounds (×2) /// - **Sends** IS_B20 lookups for carry range checks (×4) /// - **Receives** MUL lookups from CPU table (×2: lo and hi) pub fn bus_interactions() -> Vec { @@ -398,6 +427,28 @@ pub fn bus_interactions() -> Vec { ], )); + // ------------------------------------------------------------------------- + // IS_HALF[μ_lo] | μ_lo, IS_HALF[μ_hi] | μ_hi. + // Every check below fires with μ_lo + μ_hi, so the multiplicities themselves + // must be bounded and non-negative. Otherwise μ_lo = 1, μ_hi = −1 receives a + // `lo` lookup with all range checks off (forged product), + // and an honest μ_hi = 1 copy of the row cancels the stray −1. Each μ is sent + // with itself as multiplicity: `k` rows holding an out-of-range value `v` + // put weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // (μ = 0) contributes nothing, so an empty instance still matches an absent + // one. See `MU_MAX`. + // ------------------------------------------------------------------------- + for col in [cols::MU_LO, cols::MU_HI] { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(col), + vec![BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }], + )); + } + // ------------------------------------------------------------------------- // IS_HALF lookups for lhs/rhs INPUT range checks (multiplicity: mu_lo + mu_hi). // The bus binds only the packed 32-bit words, so without these the input diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index 75d7605db..99cee2f8b 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -726,14 +726,14 @@ pub fn bus_interactions() -> Vec { } /// Total number of SHIFT transition constraints. -pub const NUM_SHIFT_CONSTRAINTS: usize = 19; +pub const NUM_SHIFT_CONSTRAINTS: usize = 21; // ========================================================================= // Single-body constraint set (ConstraintSet front-end) // ========================================================================= // // One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..19. +// folder, the verifier folder and IR capture. Constraint indices 0..21. use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; @@ -893,6 +893,23 @@ impl ConstraintSet for ShiftConstraints { let one = b.one(); b.emit_base(16 + off, flag.clone() * (one - flag)); } + + // idx 19: ZbsIsBit — zbs * (1 - zbs). The only other anchor on zbs is + // `ZERO[bit_shift] → zbs | μ`, which vanishes on a μ = 0 padding row; there + // a free zbs = 2 turns the five HWSL senders' `1 - zbs` into −1, so the row + // *provides* arbitrary HWSL tuples and cancels a real row's forged ones + // (`SLL 1, 1 = 0` verified). + let zbs = b.main(0, cols::ZBS); + let one = b.one(); + b.emit_base(19, zbs.clone() * (one - zbs)); + + // idx 20: MuIsBit — μ * (1 - μ). SHIFT never deduplicates (one row per op), + // and idx 0 only pins μ = 1 when direction = 1. For a left shift a free μ + // scales the output (`left = μ - direction`), and μ = −1 turns every + // μ-gated lookup into a provider. + let mu = b.main(0, cols::MU); + let one = b.one(); + b.emit_base(20, mu.clone() * (one - mu)); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index c3b695a80..e72ce502e 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1734,9 +1734,11 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { /// IS_HALF lookups for lhs/rhs input and lo/hi output range checks, /// and IS_B20 lookups for carry range checks. /// -/// IS_HALF and IS_B20 are emitted once per raw op. MSB16 is deduplicated -/// per `max_rows_mul` chunk, mirroring `chunk_and_generate_optional` — a unique -/// signed op that spans two instances is sent twice and must be tallied twice. +/// IS_HALF and IS_B20 are emitted once per raw op. The per-row lookups (MSB16 +/// and the IS_HALF[μ_lo]/IS_HALF[μ_hi] multiplicity bounds) are counted over the +/// rows of each `max_rows_mul` chunk, mirroring `chunk_and_generate_optional` — +/// a unique signed op that spans two instances is sent twice and must be tallied +/// twice. /// /// Returns: Vec of bitwise lookups pub(crate) fn collect_bitwise_from_mul( @@ -1793,28 +1795,38 @@ pub(crate) fn collect_bitwise_from_mul( } } - // MSB16: dedup per chunk — the MUL AIR sends Msb16 once per unique signed row - // per instance, so the collector must mirror the same chunk boundary. + // Per-row lookups, over exactly the rows `generate_mul_trace` builds for each + // `max_rows_mul` chunk (`chunk_and_generate_optional`): IS_HALF[μ_lo] and + // IS_HALF[μ_hi] are sent μ_lo / μ_hi times (so padding rows send nothing), and + // MSB16 fires once per row whose sign flag is set — a unique signed op spanning two + // instances, or split over two rows by `mul::MU_MAX`, is sent once per row. + let halfword = |v: u64| { + BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (v & 0xFF) as u8, + ((v >> 8) & 0xFF) as u8, + ) + }; for chunk in mul_ops.chunks(max_rows_mul) { - let mut msb16_seen = std::collections::HashSet::new(); - for (op, _wants_hi) in chunk { - if msb16_seen.insert((op.lhs, op.lhs_signed, op.rhs, op.rhs_signed)) { - if op.lhs_signed { - let lhs_3 = ((op.lhs >> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (lhs_3 & 0xFF) as u8, - (lhs_3 >> 8) as u8, - )); - } - if op.rhs_signed { - let rhs_3 = ((op.rhs >> 48) & 0xFFFF) as u16; - bitwise_ops.push(BitwiseOperation::halfword( - BitwiseOperationType::Msb16, - (rhs_3 & 0xFF) as u8, - (rhs_3 >> 8) as u8, - )); - } + for (op, mu) in &mul::dedup_mul_rows(chunk) { + for m in [mu.mu_lo, mu.mu_hi] { + bitwise_ops.extend(std::iter::repeat_n(halfword(m), m as usize)); + } + if op.lhs_signed { + let lhs_3 = ((op.lhs >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (lhs_3 & 0xFF) as u8, + (lhs_3 >> 8) as u8, + )); + } + if op.rhs_signed { + let rhs_3 = ((op.rhs >> 48) & 0xFFFF) as u16; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (rhs_3 & 0xFF) as u8, + (rhs_3 >> 8) as u8, + )); } } } @@ -1831,9 +1843,10 @@ pub(crate) fn collect_bitwise_from_mul( /// table itself (n/d IS_HALF senders in dvrm::bus_interactions), so their lookups /// are collected here alongside the constraint-level ones. /// -/// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16 and the -/// NEG-template ZERO lookups (C3/C5) are deduplicated per `max_rows_dvrm` -/// chunk, mirroring `chunk_and_generate_optional`. +/// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16, the +/// NEG-template ZERO lookups (C3/C5) and the IS_HALF[μ_q]/IS_HALF[μ_r] +/// multiplicity bounds are counted over the rows of each `max_rows_dvrm` chunk, +/// mirroring `chunk_and_generate_optional`. /// /// Returns: Vec of bitwise lookups pub(crate) fn collect_bitwise_from_dvrm( @@ -1920,11 +1933,26 @@ pub(crate) fn collect_bitwise_from_dvrm( bitwise_ops.push(BitwiseOperation::zero(d_sum)); } - // MSB16: same per-chunk dedup as MUL (Column(SIGNED) is a bit, not a count). + // Per-row lookups, over exactly the rows `generate_dvrm_trace` builds for each + // `max_rows_dvrm` chunk (`chunk_and_generate_optional`): IS_HALF[μ_q] and + // IS_HALF[μ_r] sent μ_q / μ_r times (padding rows send nothing); MSB16 (Column(SIGNED)) + // and the NEG-template ZERO lookups (Column(SIGN_R)/Column(SIGN_D)) once per + // row whose bit is set. An op split over two rows by `dvrm::MU_MAX` sends + // them once per row. + let halfword = |v: u64| { + BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (v & 0xFF) as u8, + ((v >> 8) & 0xFF) as u8, + ) + }; for chunk in dvrm_ops.chunks(max_rows_dvrm) { - let mut msb16_seen = std::collections::HashSet::new(); - for (op, _wants_remainder) in chunk { - if op.signed && msb16_seen.insert(op.clone()) { + for (op, mu) in &dvrm::dedup_dvrm_rows(chunk) { + for m in [mu.mu_q, mu.mu_r] { + bitwise_ops.extend(std::iter::repeat_n(halfword(m), m as usize)); + } + + if op.signed { let r = op.compute_remainder(); // MSB16[n[3]] @@ -1951,46 +1979,38 @@ pub(crate) fn collect_bitwise_from_dvrm( (d_3 >> 8) as u8, )); } - } - } - // ZERO (NEG template): same — SIGN_R/SIGN_D are bits, dedup per chunk. - for chunk in dvrm_ops.chunks(max_rows_dvrm) { - let mut zero_seen = std::collections::HashSet::new(); - for (op, _wants_remainder) in chunk { - if zero_seen.insert(op.clone()) { - // C3: NEG for r (when sign_r = 1) - if op.sign_r() { - let r = op.compute_remainder(); - let r_halves: [u32; 4] = [ - (r & 0xFFFF) as u32, - ((r >> 16) & 0xFFFF) as u32, - ((r >> 32) & 0xFFFF) as u32, - ((r >> 48) & 0xFFFF) as u32, - ]; - // C3a: ZERO[1-carry_r[0]; r[0]+r[1]] - bitwise_ops.push(BitwiseOperation::zero(r_halves[0] + r_halves[1])); - // C3b: ZERO[1-carry_r[1]; r[0]+r[1]+r[2]+r[3]] - bitwise_ops.push(BitwiseOperation::zero( - r_halves[0] + r_halves[1] + r_halves[2] + r_halves[3], - )); - } + // C3: NEG for r (when sign_r = 1) + if op.sign_r() { + let r = op.compute_remainder(); + let r_halves: [u32; 4] = [ + (r & 0xFFFF) as u32, + ((r >> 16) & 0xFFFF) as u32, + ((r >> 32) & 0xFFFF) as u32, + ((r >> 48) & 0xFFFF) as u32, + ]; + // C3a: ZERO[1-carry_r[0]; r[0]+r[1]] + bitwise_ops.push(BitwiseOperation::zero(r_halves[0] + r_halves[1])); + // C3b: ZERO[1-carry_r[1]; r[0]+r[1]+r[2]+r[3]] + bitwise_ops.push(BitwiseOperation::zero( + r_halves[0] + r_halves[1] + r_halves[2] + r_halves[3], + )); + } - // C5: NEG for d (when sign_d = 1) - if op.sign_d() { - let d_halves: [u32; 4] = [ - (op.d & 0xFFFF) as u32, - ((op.d >> 16) & 0xFFFF) as u32, - ((op.d >> 32) & 0xFFFF) as u32, - ((op.d >> 48) & 0xFFFF) as u32, - ]; - // C5a: ZERO[1-carry_d[0]; d[0]+d[1]] - bitwise_ops.push(BitwiseOperation::zero(d_halves[0] + d_halves[1])); - // C5b: ZERO[1-carry_d[1]; d[0]+d[1]+d[2]+d[3]] - bitwise_ops.push(BitwiseOperation::zero( - d_halves[0] + d_halves[1] + d_halves[2] + d_halves[3], - )); - } + // C5: NEG for d (when sign_d = 1) + if op.sign_d() { + let d_halves: [u32; 4] = [ + (op.d & 0xFFFF) as u32, + ((op.d >> 16) & 0xFFFF) as u32, + ((op.d >> 32) & 0xFFFF) as u32, + ((op.d >> 48) & 0xFFFF) as u32, + ]; + // C5a: ZERO[1-carry_d[0]; d[0]+d[1]] + bitwise_ops.push(BitwiseOperation::zero(d_halves[0] + d_halves[1])); + // C5b: ZERO[1-carry_d[1]; d[0]+d[1]+d[2]+d[3]] + bitwise_ops.push(BitwiseOperation::zero( + d_halves[0] + d_halves[1] + d_halves[2] + d_halves[3], + )); } } } diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index 8179a98ec..c129f45b6 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -311,8 +311,9 @@ fn test_bus_interactions_count() { // - 2x MUL senders (n_sub_r = d*q lo + hi) // - 6x ZERO senders (C3×2 NEG r, C5×2 NEG d, C8 overflow, C17 div_by_zero) // - 2x DVRM receivers (quotient, remainder) - // Total: 8 + 12 + 3 + 1 + 2 + 6 + 2 = 34 - assert_eq!(interactions.len(), 34, "Expected 34 bus interactions"); + // - 2x IS_HALF senders bounding the multiplicities (μ_q, μ_r) + // Total: 8 + 12 + 3 + 1 + 2 + 6 + 2 + 2 = 36 + assert_eq!(interactions.len(), 36, "Expected 36 bus interactions"); } #[test] @@ -555,3 +556,126 @@ fn neg_template_zero_lookups_dedup_per_chip_instance() { {two_instances} (2 instances) must exceed {one_instance} (1 instance)" ); } + +// Soundness regression: μ_q/μ_r are bounded, non-negative multiplicities. +// Every DVRM check fires with μ_q + μ_r, so a free μ_r = −1 next to μ_q = 1 +// switched them all off (`multiplicity_forgery_poc`). Each μ is now IS_HALF-checked +// weighted by itself, and trace generation splits a row whose count would +// exceed `MU_MAX`. + +/// Presence: each multiplicity is IS_HALF-checked weighted by itself, so an +/// out-of-range value `v` always lands on the bus with weight `v ≠ 0`. +#[test] +fn test_dvrm_bounds_its_multiplicities() { + use crate::tables::types::BusId; + use stark::lookup::{BusValue, Multiplicity, Packing}; + for col in [cols::MU_Q, cols::MU_R] { + assert!( + bus_interactions().iter().any(|i| i.is_sender + && i.bus_id == BusId::IsHalfword as u64 + && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) + && matches!(i.values.as_slice(), + [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col)), + "DVRM must IS_HALF-check multiplicity column {col} weighted by itself" + ); + } +} + +/// Splitting: a count above `MU_MAX` spreads over rows within the bound that +/// preserve both totals; exactly `MU_MAX` still fits one row. +#[test] +fn test_dedup_dvrm_rows_splits_counts_above_mu_max() { + use crate::tables::dvrm::{MU_MAX, dedup_dvrm_rows}; + let op = DvrmOperation::new(7, 2, UNSIGNED); + let ops: Vec<_> = std::iter::repeat_n((op.clone(), true), MU_MAX as usize + 5) + .chain(std::iter::repeat_n((op.clone(), false), 3)) + .collect(); + let mut rows: Vec<(u64, u64)> = dedup_dvrm_rows(&ops) + .iter() + .map(|(_, m)| (m.mu_q, m.mu_r)) + .collect(); + rows.sort(); + assert_eq!(rows, vec![(0, 5), (3, MU_MAX)]); + + let ops: Vec<_> = std::iter::repeat_n((op, false), MU_MAX as usize).collect(); + assert_eq!(dedup_dvrm_rows(&ops).len(), 1); + assert!(dedup_dvrm_rows(&[]).is_empty()); +} + +/// Consistency: the BITWISE collector tallies exactly the per-row lookups the +/// generated DVRM instances send — IS_HALF[μ_q], IS_HALF[μ_r] weighted by μ +/// (padding sends nothing), MSB16 ×3 per SIGNED row and the NEG-template ZERO ×2 per +/// SIGN_R / SIGN_D row — across small instances and for a row split by `MU_MAX`. +#[test] +fn test_dvrm_per_row_lookups_match_collector() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::dvrm::MU_MAX; + use crate::tables::trace_builder::collect_bitwise_from_dvrm; + use std::collections::HashMap; + + let half = |h: u64| ((h & 0xFF) as u8, ((h >> 8) & 0xFF) as u8); + let distinct = [ + DvrmOperation::new(7, 2, UNSIGNED), + DvrmOperation::new((-7i64) as u64, 2, SIGNED), + DvrmOperation::new(100, (-3i64) as u64, SIGNED), + ]; + let small: Vec<_> = distinct + .iter() + .cycle() + .take(11) + .enumerate() + .map(|(i, op)| (op.clone(), i % 2 == 0)) + .collect(); + let split: Vec<_> = std::iter::repeat_n((distinct[1].clone(), false), MU_MAX as usize + 2) + .chain(distinct.iter().map(|op| (op.clone(), true))) + .collect(); + + for (ops, chunk) in [(small, 4usize), (split, 1 << 19)] { + let collected = collect_bitwise_from_dvrm(&ops, chunk); + let count = |ty| collected.iter().filter(|b| b.lookup_type == ty).count(); + + let mut is_half: HashMap<(u8, u8), i64> = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::IsHalf) + { + *is_half.entry((b.x, b.y)).or_default() += 1; + } + for (op, _) in &ops { + let r = op.compute_remainder(); + for word in [op.n, op.d, r, op.n.wrapping_sub(r), op.compute_quotient()] { + for shift in [0, 16, 32, 48] { + *is_half.entry(half(word >> shift & 0xFFFF)).or_default() -= 1; + } + } + } + + let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + let (mut msb16, mut neg_zero) = (0usize, 0usize); + for c in ops.chunks(chunk) { + let t = generate_dvrm_trace(c); + for r in 0..t.num_rows() { + for col in [cols::MU_Q, cols::MU_R] { + let mu = t.get_main(r, col).to_raw(); + *expected.entry(half(mu)).or_default() += mu as i64; + } + msb16 += 3 * t.get_main(r, cols::SIGNED).to_raw() as usize; + neg_zero += 2 * t.get_main(r, cols::SIGN_R).to_raw() as usize; + neg_zero += 2 * t.get_main(r, cols::SIGN_D).to_raw() as usize; + } + } + is_half.retain(|_, n| *n != 0); + expected.retain(|_, n| *n != 0); + assert_eq!( + is_half, expected, + "IS_HALF[μ] tally must match the trace rows" + ); + assert_eq!(count(BitwiseOperationType::Msb16), msb16, "MSB16 tally"); + // ZERO = C8 + C20 per raw op, plus the per-row NEG-template sends. + assert_eq!( + count(BitwiseOperationType::Zero), + 2 * ops.len() + neg_zero, + "ZERO tally" + ); + } +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 73ff6ee45..4d8d08e23 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -69,6 +69,8 @@ pub mod memw_tests; #[cfg(test)] pub mod mul_tests; #[cfg(test)] +pub mod multiplicity_forgery_poc; +#[cfg(test)] pub mod ood_window_ir_tests; #[cfg(test)] pub mod page_layout_tests; diff --git a/prover/src/tests/mul_tests.rs b/prover/src/tests/mul_tests.rs index 0d2e22243..cce10d890 100644 --- a/prover/src/tests/mul_tests.rs +++ b/prover/src/tests/mul_tests.rs @@ -270,8 +270,9 @@ fn test_bus_interactions_count() { // - 8x IS_HALF senders for outputs (lo[0..4], hi[0..4]) // - 4x IS_B20 senders (carry[0..4] virtual range checks) // - 2x ALU receivers (lo, hi) - // Total: 2 + 8 + 8 + 4 + 2 = 24 - assert_eq!(interactions.len(), 24, "Expected 24 bus interactions"); + // - 2x IS_HALF senders bounding the multiplicities (μ_lo, μ_hi) + // Total: 2 + 8 + 8 + 4 + 2 + 2 = 26 + assert_eq!(interactions.len(), 26, "Expected 26 bus interactions"); } #[test] @@ -416,3 +417,141 @@ fn msb16_bitwise_multiplicity_matches_per_instance_sends() { sends ({sends}); a mismatch leaves the Msb16 bus unbalanced" ); } + +// Soundness regression: μ_lo/μ_hi are bounded, non-negative multiplicities. +// Every MUL range check fires with μ_lo + μ_hi, so a free μ_hi = −1 next to +// μ_lo = 1 switched them all off (`multiplicity_forgery_poc`). Each μ is now +// IS_HALF-range-checked weighted by itself, and trace generation splits a +// row whose count would exceed `MU_MAX`. + +/// Presence: each multiplicity is IS_HALF-checked weighted by itself, so an +/// out-of-range value `v` always lands on the bus with weight `v ≠ 0`. +#[test] +fn test_mul_bounds_its_multiplicities() { + use crate::tables::types::BusId; + use stark::lookup::{BusValue, Multiplicity, Packing}; + for col in [cols::MU_LO, cols::MU_HI] { + assert!( + bus_interactions().iter().any(|i| i.is_sender + && i.bus_id == BusId::IsHalfword as u64 + && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) + && matches!(i.values.as_slice(), + [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col)), + "MUL must IS_HALF-check multiplicity column {col} weighted by itself" + ); + } +} + +/// Splitting: a count above `MU_MAX` spreads over rows that each stay within the +/// bound and together preserve both totals; exactly `MU_MAX` still fits one row. +#[test] +fn test_dedup_mul_rows_splits_counts_above_mu_max() { + use crate::tables::mul::{MU_MAX, dedup_mul_rows}; + let op = MulOperation::new(3, false, 5, false); + let ops: Vec<_> = std::iter::repeat_n((op.clone(), false), MU_MAX as usize + 5) + .chain(std::iter::repeat_n((op.clone(), true), 3)) + .collect(); + let mut rows: Vec<(u64, u64)> = dedup_mul_rows(&ops) + .iter() + .map(|(_, m)| (m.mu_lo, m.mu_hi)) + .collect(); + rows.sort(); + assert_eq!(rows, vec![(5, 0), (MU_MAX, 3)]); + + let ops: Vec<_> = std::iter::repeat_n((op, true), MU_MAX as usize).collect(); + assert_eq!(dedup_mul_rows(&ops).len(), 1); + assert!(dedup_mul_rows(&[]).is_empty()); + + // The generated trace never holds a μ above the bound. + let ops: Vec<_> = std::iter::repeat_n( + (MulOperation::new(7, true, 9, true), false), + 2 * MU_MAX as usize + 1, + ) + .collect(); + let trace = generate_mul_trace(&ops); + let mut total = 0u64; + for r in 0..trace.num_rows() { + let mu = trace.get_main(r, cols::MU_LO).to_raw(); + assert!(mu <= MU_MAX); + total += mu; + } + assert_eq!(total, ops.len() as u64); +} + +/// Consistency: the BITWISE collector tallies exactly the per-row lookups the +/// generated MUL instances send — IS_HALF[μ_lo], IS_HALF[μ_hi] weighted by μ +/// (padding sends nothing) and MSB16 per row whose sign flag is set — both across +/// several small instances and for a row split by `MU_MAX`. +#[test] +fn test_mul_per_row_lookups_match_collector() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::mul::MU_MAX; + use crate::tables::trace_builder::collect_bitwise_from_mul; + use std::collections::HashMap; + + let half = |h: u64| ((h & 0xFF) as u8, ((h >> 8) & 0xFF) as u8); + let distinct = [ + MulOperation::new(3, false, 5, false), + MulOperation::new(0x1234_5678_9abc_def0, true, 0x8000_0000_0000_0001, true), + MulOperation::new(u64::MAX, true, 2, false), + ]; + let small: Vec<_> = distinct + .iter() + .cycle() + .take(11) + .enumerate() + .map(|(i, op)| (op.clone(), i % 2 == 0)) + .collect(); + let split: Vec<_> = std::iter::repeat_n((distinct[1].clone(), false), MU_MAX as usize + 2) + .chain(distinct.iter().map(|op| (op.clone(), true))) + .collect(); + + for (ops, chunk) in [(small, 4usize), (split, 1 << 20)] { + let collected = collect_bitwise_from_mul(&ops, chunk); + + // IS_HALF minus the per-raw-op range checks leaves the μ bounds. + let mut is_half: HashMap<(u8, u8), i64> = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::IsHalf) + { + *is_half.entry((b.x, b.y)).or_default() += 1; + } + for (op, _) in &ops { + let (lo, hi) = op.compute_product(); + for word in [op.lhs, op.rhs, lo, hi] { + for shift in [0, 16, 32, 48] { + *is_half.entry(half(word >> shift & 0xFFFF)).or_default() -= 1; + } + } + } + + let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + let mut msb16 = 0usize; + for c in ops.chunks(chunk) { + let t = generate_mul_trace(c); + for r in 0..t.num_rows() { + for col in [cols::MU_LO, cols::MU_HI] { + let mu = t.get_main(r, col).to_raw(); + *expected.entry(half(mu)).or_default() += mu as i64; + } + msb16 += t.get_main(r, cols::LHS_SIGNED).to_raw() as usize; + msb16 += t.get_main(r, cols::RHS_SIGNED).to_raw() as usize; + } + } + is_half.retain(|_, n| *n != 0); + expected.retain(|_, n| *n != 0); + assert_eq!( + is_half, expected, + "IS_HALF[μ] tally must match the trace rows" + ); + assert_eq!( + collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::Msb16) + .count(), + msb16, + "MSB16 tally must match the trace rows" + ); + } +} diff --git a/prover/src/tests/multiplicity_forgery_poc.rs b/prover/src/tests/multiplicity_forgery_poc.rs new file mode 100644 index 000000000..19eac4739 --- /dev/null +++ b/prover/src/tests/multiplicity_forgery_poc.rs @@ -0,0 +1,485 @@ +//! End-to-end regression tests for unconstrained multiplicities: MUL's +//! `μ_lo`/`μ_hi` and DVRM's `μ_q`/`μ_r` must be bounded and non-negative, and +//! SHIFT's `zbs` must be a bit. +//! +//! **MUL / DVRM.** Both chips send every range check (and DVRM its MUL/LT/ZERO checks) with +//! multiplicity `μ_a + μ_b`, the row's total lookup count. Before the fix neither +//! column was constrained, so a row with `μ_a = +1, μ_b = −1` sent no checks at +//! all while still receiving one `a` lookup: its result was free. The stray `−1` +//! on the `b` tuple was cancelled by an honest copy of the row with +//! `μ_a = 0, μ_b = +1`, whose checks fire once and pass. Both forgeries below +//! verified against `main` (ffc4ac19). The fix range-checks each μ to a halfword +//! (`IS_HALF[μ]`, weighted by μ), so `μ_b = −1` has no receiver. +//! +//! **SHIFT.** The five HWSL senders fire with `1 − zbs`, and on a μ = 0 padding +//! row nothing pinned `zbs`: `zbs = 2` made that −1, so the padding row provided +//! exactly the HWSL tuples a forged real row needed (`1 << 1 = 0` verified +//! against `main`). The fix bit-constrains `zbs` (and μ). +//! +//! Each guest computes a value with one real instruction and commits it; the +//! malicious prover claims a different value and reshapes the chip's rows. It +//! also rebalances every BITWISE receiver multiplicity it can (those are free +//! main-trace columns, as in `page_offset_forgery_poc`), so the only thing left +//! to reject the proof is the new constraint itself. +//! +//! Run under production proof options. + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::proof::options::ProofOptions; +use stark::prover::{IsStarkProver, Prover}; +use stark::trace::TraceTable; + +use crate::statement::{StatementKind, absorb_statement}; +use crate::tables::bitwise::{cols as bw_cols, row_index as bw_row_index}; +use crate::tables::trace_builder::Traces; +use crate::tables::types::{BusId, FE, GoldilocksExtension as Ext, GoldilocksField as Base}; +use crate::tables::{dvrm, mul}; +use crate::test_utils::{E, asm_elf_bytes}; +use crate::{MaxRowsConfig, VmAirs, VmProof}; + +use executor::elf::Elf; +use executor::vm::execution::Executor; + +fn opts() -> ProofOptions { + crate::GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 is valid") +} + +/// One forgery scenario: a guest whose single `lhs ∘ rhs` instruction yields +/// `honest`, and the chip rewrite that makes it yield `forged` instead. +struct Scenario { + guest: &'static str, + lhs: u64, + rhs: u64, + honest: u64, + forged: u64, + forge_rows: fn(&mut Traces, &Scenario), +} + +const MUL: Scenario = Scenario { + guest: "poc_mul_commit", + lhs: 3, + rhs: 5, + honest: 15, + forged: 99, + forge_rows: forge_mul_rows, +}; + +const DIVU: Scenario = Scenario { + guest: "poc_divu_commit", + lhs: 7, + rhs: 2, + honest: 3, + forged: 100, + forge_rows: forge_dvrm_rows, +}; + +const SLL: Scenario = Scenario { + guest: "poc_sll_commit", + lhs: 1, + rhs: 1, + honest: 2, + forged: 0, + forge_rows: forge_shift_rows, +}; + +/// Which deviations the malicious prover applies. +#[derive(Clone, Copy)] +struct Forge { + /// Rewrite the execution so the CPU claims `lhs ∘ rhs = forged`. + claim: bool, + /// Rewrite the chip's rows so they answer the forged claim. + rows: bool, +} + +fn craft_proof(s: &Scenario, forge: Forge) -> Result { + let elf_bytes = asm_elf_bytes(s.guest); + let options = opts(); + let program = Elf::load(&elf_bytes).expect("ELF load"); + let mut logs = Executor::new(&program, vec![]) + .expect("executor construction") + .run() + .expect("run") + .logs; + + if forge.claim { + let idx = logs + .iter() + .position(|l| l.src1_val == s.lhs && l.src2_val == s.rhs && l.dst_val == s.honest) + .expect("arithmetic log not found"); + logs[idx].dst_val = s.forged; + // The following `sd t1, 0(sp)` stores the result: keep it consistent. + logs[idx + 1..] + .iter_mut() + .find(|l| l.src2_val == s.honest) + .expect("SD of the result not found") + .src2_val = s.forged; + } + + let mut traces = Traces::from_elf_and_logs( + &program, + &logs, + &MaxRowsConfig::default(), + &[], + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ) + .expect("trace build"); + + if forge.rows { + (s.forge_rows)(&mut traces, s); + } + + 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, + )?; + + Ok(VmProof { + proof, + runtime_page_ranges, + table_counts, + public_output: traces.public_output_bytes.clone(), + num_private_input_pages, + }) +} + +/// Whether `interactions` range-check column `col`, weighted by itself. +fn bounds_column(interactions: &[BusInteraction], col: usize) -> bool { + interactions.iter().any(|i| { + i.is_sender + && i.bus_id == BusId::IsHalfword as u64 + && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) + && matches!( + i.values.as_slice(), + [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col + ) + }) +} + +/// Add `delta` to the BITWISE receiver multiplicity `mu_col` at halfword `half`. +fn bump_bitwise(traces: &mut Traces, mu_col: usize, half: u64, delta: FE) { + assert!(half < 1 << 16, "only halfwords have a BITWISE row"); + let bw = &mut traces.bitwise.main_table; + let row = bw_row_index((half & 0xFF) as u8, (half >> 8) as u8, 0); + let old = *bw.get(row, mu_col); + bw.set(row, mu_col, old + delta); +} + +/// The two-row rewrite shared by both chips, on one chip instance `t`: +/// +/// * row A (the honest row answering the claim, `μ_a = 1, μ_b = 0`) gets the +/// forged result written by `write_forged` and `μ_b = −1`; +/// * row B (an all-zero padding row) becomes an honest copy with +/// `μ_a = 0, μ_b = 1`. +/// +/// Returns the row-B copy's index so the caller can rebalance flag-gated sends. +/// If the chip range-checks its μ columns, also rebalances those IS_HALF sends +/// wherever a BITWISE row exists (`−1` has none — that is the fix). +fn forge_two_rows( + traces: &mut Traces, + table: fn(&mut Traces) -> &mut TraceTable, + find_a: impl Fn(&TraceTable, usize) -> bool, + (mu_a, mu_b, num_cols): (usize, usize, usize), + bounded: bool, + write_forged: impl Fn(&mut TraceTable, usize), +) -> usize { + let t = table(traces); + let rows = t.num_rows(); + let a = (0..rows) + .find(|&r| find_a(t, r)) + .expect("honest row not found"); + assert_eq!(*t.get_main(a, mu_a), FE::one()); + assert_eq!(*t.get_main(a, mu_b), FE::zero()); + let b = (0..rows) + .find(|&r| (0..num_cols).all(|c| *t.get_main(r, c) == FE::zero())) + .expect("an all-zero padding row is needed for the honest copy"); + + for c in 0..num_cols { + let v = *t.get_main(a, c); + t.set_main(b, c, v); + } + t.set_main(b, mu_a, FE::zero()); + t.set_main(b, mu_b, FE::one()); + write_forged(t, a); + t.set_main(a, mu_b, FE::zero() - FE::one()); + + if bounded { + // IS_HALF[μ] | μ sends: B's μ_b 0 -> 1 adds IS_HALF[1] once. A's μ_b + // 0 -> −1 adds IS_HALF[p−1] with weight −1, which has no BITWISE row. + bump_bitwise(traces, bw_cols::MU_IS_HALF, 1, FE::one()); + } + b +} + +/// MUL: `lo(3 * 5)` forged to 99 (`μ_lo = 1, μ_hi = −1`). +fn forge_mul_rows(traces: &mut Traces, s: &Scenario) { + use mul::cols; + let bounded = bounds_column(&mul::bus_interactions(), cols::MU_HI); + let forged = s.forged; + let b = forge_two_rows( + traces, + |t| &mut t.muls[0], + |t, r| { + *t.get_main(r, cols::LHS_0) == FE::from(s.lhs) + && *t.get_main(r, cols::RHS_0) == FE::from(s.rhs) + && *t.get_main(r, cols::MU_LO) == FE::one() + }, + (cols::MU_LO, cols::MU_HI, cols::NUM_COLUMNS), + bounded, + |t, a| t.set_main(a, cols::LO_0, FE::from(forged)), + ); + + // Row B's two MSB16 sign lookups are gated by the sign flags, not by μ, so + // the copy duplicates them. Rebalance the BITWISE MSB16 receiver. + for (half, flag) in [ + (cols::LHS_3, cols::LHS_SIGNED), + (cols::RHS_3, cols::RHS_SIGNED), + ] { + let t = &traces.muls[0]; + let (half, mult) = (t.get_main(b, half).to_raw(), *t.get_main(b, flag)); + bump_bitwise(traces, bw_cols::MU_MSB16, half, mult); + } +} + +/// DVRM: `7 / 2` (unsigned) forged to 100 (`μ_q = 1, μ_r = −1`). Unsigned, so +/// the copy duplicates no SIGNED/SIGN_R/SIGN_D-gated sends. +fn forge_dvrm_rows(traces: &mut Traces, s: &Scenario) { + use dvrm::cols; + let bounded = bounds_column(&dvrm::bus_interactions(), cols::MU_R); + let forged = s.forged; + let b = forge_two_rows( + traces, + |t| &mut t.dvrms[0], + |t, r| { + *t.get_main(r, cols::N_0) == FE::from(s.lhs) + && *t.get_main(r, cols::D_0) == FE::from(s.rhs) + && *t.get_main(r, cols::MU_Q) == FE::one() + }, + (cols::MU_Q, cols::MU_R, cols::NUM_COLUMNS), + bounded, + |t, a| t.set_main(a, cols::Q_0, FE::from(forged)), + ); + let t = &traces.dvrms[0]; + for flag in [cols::SIGNED, cols::SIGN_R, cols::SIGN_D] { + assert_eq!( + *t.get_main(b, flag), + FE::zero(), + "scenario must stay unsigned" + ); + } +} + +/// SHIFT: `1 << 1` forged to 0. Row A (the real op) gets `X[0] = 0`, so +/// `out = 0` and its five HWSL tuples are no longer honest; padding row B gets +/// `zbs = 2, in[0] = 1, bit_shift = 1`, so its five HWSL senders fire with +/// `1 − zbs = −1` on exactly A's tuples. With μ = 0 every other B lookup +/// vanishes. The HWSL bus then needs no BITWISE entry for A at all, so the +/// prover drops A's honest HWSL demand from the BITWISE multiplicities. +fn forge_shift_rows(traces: &mut Traces, s: &Scenario) { + use crate::tables::shift::cols; + let t = &mut traces.shifts[0]; + let rows = t.num_rows(); + let a = (0..rows) + .find(|&r| { + *t.get_main(r, cols::IN_0) == FE::from(s.lhs) + && *t.get_main(r, cols::SHIFT_AMOUNT) == FE::from(s.rhs) + && *t.get_main(r, cols::MU) == FE::one() + }) + .expect("honest SLL row not found"); + assert_eq!(*t.get_main(a, cols::X_0), FE::from(s.honest)); + let b = (0..rows) + .find(|&r| *t.get_main(r, cols::MU) == FE::zero() && r != a) + .expect("a padding row is needed"); + + // A's honest HWSL demand: [in[i], bit_shift] for i in 0..4 and the extension + // half `65535·is_negative`, each read at BITWISE row (half, bit_shift). + let bit_shift = t.get_main(a, cols::BIT_SHIFT).to_raw(); + let ext = 65535 * t.get_main(a, cols::IS_NEGATIVE).to_raw(); + let halves: Vec = cols::IN + .iter() + .map(|&c| t.get_main(a, c).to_raw()) + .chain([ext]) + .collect(); + + t.set_main(a, cols::X_0, FE::zero()); + t.set_main(a, cols::OUT_0, FE::from(s.forged)); + t.set_main(b, cols::ZBS, FE::from(2u64)); + t.set_main(b, cols::IN_0, FE::from(s.lhs)); + t.set_main(b, cols::BIT_SHIFT, FE::from(bit_shift)); + + let bw = &mut traces.bitwise.main_table; + for half in halves { + let row = bw_row_index((half & 0xFF) as u8, (half >> 8) as u8, bit_shift as u8); + let old = *bw.get(row, bw_cols::MU_HWSL); + bw.set(row, bw_cols::MU_HWSL, old - FE::one()); + } +} + +fn verifier_accepts(s: &Scenario, proof: &VmProof) -> bool { + crate::verify_with_options(proof, &asm_elf_bytes(s.guest), &opts(), None, None) + .expect("verify must not error") +} + +fn u64_output(proof: &VmProof) -> u64 { + u64::from_le_bytes(proof.public_output[..8].try_into().expect("8-byte output")) +} + +/// Honest proving of the scenario verifies and commits the honest result. +fn assert_honest_verifies(s: &Scenario) { + let proof = craft_proof( + s, + Forge { + claim: false, + rows: false, + }, + ) + .expect("honest proving"); + assert_eq!(u64_output(&proof), s.honest); + assert!(verifier_accepts(s, &proof), "honest proof must verify"); +} + +/// Did a crafted proof get accepted? A prover refusal also counts as rejected. +fn crafted_accepted(s: &Scenario, forge: Forge) -> bool { + match craft_proof(s, forge) { + Ok(proof) => { + assert_eq!( + u64_output(&proof), + s.forged, + "public output must be the forged value" + ); + verifier_accepts(s, &proof) + } + Err(_) => false, + } +} + +#[test] +fn mul_honest_control_verifies() { + assert_honest_verifies(&MUL); +} + +/// Negative control: the CPU claims 99 but the MUL rows are left honest. +#[test] +fn mul_unanswered_forged_claim_is_rejected() { + assert!(!crafted_accepted( + &MUL, + Forge { + claim: true, + rows: false + } + )); +} + +/// Regression: `3 * 5 = 99` via `μ_lo = 1, μ_hi = −1` (verified on ffc4ac19). +#[test] +fn mul_negative_mu_hi_forgery_is_rejected() { + assert!( + !crafted_accepted( + &MUL, + Forge { + claim: true, + rows: true + } + ), + "FORGERY: 3 * 5 = 99 was accepted — μ_lo/μ_hi are not bounded" + ); +} + +#[test] +fn dvrm_honest_control_verifies() { + assert_honest_verifies(&DIVU); +} + +/// Negative control: the CPU claims 7 / 2 = 100 but the DVRM rows are left honest. +#[test] +fn dvrm_unanswered_forged_claim_is_rejected() { + assert!(!crafted_accepted( + &DIVU, + Forge { + claim: true, + rows: false + } + )); +} + +/// Regression: `7 / 2 = 100` via `μ_q = 1, μ_r = −1` (verified on ffc4ac19). +#[test] +fn dvrm_negative_mu_r_forgery_is_rejected() { + assert!( + !crafted_accepted( + &DIVU, + Forge { + claim: true, + rows: true + } + ), + "FORGERY: 7 / 2 = 100 was accepted — μ_q/μ_r are not bounded" + ); +} + +#[test] +fn shift_honest_control_verifies() { + assert_honest_verifies(&SLL); +} + +/// Negative control: the CPU claims 1 << 1 = 0 but the SHIFT rows are left honest. +#[test] +fn shift_unanswered_forged_claim_is_rejected() { + assert!(!crafted_accepted( + &SLL, + Forge { + claim: true, + rows: false + } + )); +} + +/// Regression: `1 << 1 = 0` via a `zbs = 2` padding row (verified on ffc4ac19). +#[test] +fn shift_zbs_two_padding_row_forgery_is_rejected() { + assert!( + !crafted_accepted( + &SLL, + Forge { + claim: true, + rows: true + } + ), + "FORGERY: 1 << 1 = 0 was accepted — zbs is not bit-constrained" + ); +} diff --git a/prover/src/tests/shift_tests.rs b/prover/src/tests/shift_tests.rs index 33e3e4c65..1563c4030 100644 --- a/prover/src/tests/shift_tests.rs +++ b/prover/src/tests/shift_tests.rs @@ -37,5 +37,176 @@ fn test_shift_air_wires_in_chip_constraints() { bus_interactions(), ); assert_eq!(in_chip, NUM_SHIFT_CONSTRAINTS); - assert_eq!(NUM_SHIFT_CONSTRAINTS, 19); + // 19 + ZbsIsBit + MuIsBit. + assert_eq!(NUM_SHIFT_CONSTRAINTS, 21); +} + +// ========================================================================= +// Soundness regression: `zbs` and `μ` are bit-constrained. +// +// Before ZbsIsBit (idx 19) nothing pinned `zbs` on a μ = 0 padding row, so +// `zbs = 2` made the `1 - zbs` HWSL multiplicity −1 and the row provided the +// HWSL tuples a forged real row needed (`SLL 1, 1 = 0`, verified on ffc4ac19). +// Before MuIsBit (idx 20) a left shift's output scaled with a free μ. +// ========================================================================= + +mod zbs_mu_bit_regression { + use std::collections::HashMap; + + use math::field::element::FieldElement; + use stark::lookup::{LinearTerm, Multiplicity}; + use stark::trace::TraceTable; + + use crate::tables::shift::{ + ShiftConstraints, ShiftOperation, bus_interactions, cols, generate_shift_trace, + }; + use crate::tables::types::{BusId, GoldilocksExtension, GoldilocksField}; + use crate::test_utils::{busless_air, validate_busless}; + + type FE = FieldElement; + type Trace = TraceTable; + + fn mult(m: &Multiplicity, g: &dyn Fn(usize) -> FE) -> FE { + match m { + Multiplicity::One => FE::one(), + Multiplicity::Column(c) => g(*c), + Multiplicity::Sum(a, b) => g(*a) + g(*b), + Multiplicity::Negated(c) => FE::one() - g(*c), + Multiplicity::Diff(a, b) => g(*a) - g(*b), + Multiplicity::Sum3(a, b, c) => g(*a) + g(*b) + g(*c), + Multiplicity::Linear(ts) => ts.iter().fold(FE::zero(), |acc, t| match *t { + LinearTerm::Column { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::ColumnUnsigned { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::Constant(v) => acc + FE::from(v), + }), + } + } + + /// Net multiset contribution of the SHIFT table per (bus, tuple): sender +m, + /// receiver −m, zero entries dropped. This is exactly what LogUp checks. + fn bus_net(trace: &Trace) -> HashMap<(u64, Vec), FE> { + let t = &trace.main_table; + let mut net: HashMap<(u64, Vec), FE> = HashMap::new(); + for bi in bus_interactions() { + for r in 0..trace.num_rows() { + let g = |c: usize| *t.get(r, c); + let m = mult(&bi.multiplicity, &g); + if m == FE::zero() { + continue; + } + let tuple: Vec = bi + .values + .iter() + .flat_map(|v| v.combine_from(g)) + .map(|x: FE| x.canonical_u64()) + .collect(); + let e = net.entry((bi.bus_id, tuple)).or_insert(FE::zero()); + *e = if bi.is_sender { *e + m } else { *e - m }; + } + } + net.retain(|_, v| *v != FE::zero()); + net + } + + fn only(net: &HashMap<(u64, Vec), FE>, bus: BusId) -> HashMap, FE> { + let id: u64 = bus.into(); + net.iter() + .filter(|((b, _), _)| *b == id) + .map(|((_, t), m)| (t.clone(), *m)) + .collect() + } + + /// Forges `SLL 1, 1 = 0` (truth: 2) on the SHIFT chip. + /// + /// Row 0 (μ=1, real): honest except `X[0] = 0` → `out = 0`; its HWSL tuple + /// `[1, 1, 0, 0]` is not in the HWSL table. + /// Row 1 (padding, μ=0): `zbs = 2`, `in[0] = 1`, `bit_shift = 1`. With μ=0 + /// every other lookup and `left/right` vanish, so the zbs-override constraints + /// only force `X = Y = 0`; the five HWSL senders then fire with multiplicity + /// `1 - zbs = -1` and exactly cancel row 0's five HWSL tuples. + fn forged_sll() -> (ShiftOperation, Trace, Trace) { + let op = ShiftOperation::new(1, 1, false, false, false); + let honest = generate_shift_trace(std::slice::from_ref(&op)); + let mut forged = honest.clone(); + { + let t = &mut forged.main_table; + assert_eq!(*t.get(0, cols::X_0), FE::from(2u64)); + t.set(0, cols::X_0, FE::zero()); + t.set(0, cols::OUT_0, FE::zero()); + + t.set(1, cols::ZBS, FE::from(2u64)); + t.set(1, cols::IN_0, FE::one()); + t.set(1, cols::BIT_SHIFT, FE::one()); + } + (op, honest, forged) + } + + /// The forgery is complete on every bus: if the trace passed the in-chip + /// constraints, `1 << 1 = 0` would be accepted. This is what makes + /// `zbs_two_padding_row_is_rejected` load-bearing. + #[test] + fn forged_sll_would_balance_every_bus() { + let (op, honest, forged) = forged_sll(); + let (h, f) = (bus_net(&honest), bus_net(&forged)); + + // HWSL: the forged trace needs *no* HWSL table entries at all. + assert!(!only(&h, BusId::Hwsl).is_empty()); + assert!(only(&f, BusId::Hwsl).is_empty(), "HWSL fully self-cancels"); + + // Every other lookup bus is identical to the honest run (all real entries). + for bus in [ + BusId::ByteAlu, + BusId::Zero, + BusId::AreBytes, + BusId::IsHalfword, + BusId::Msb16, + ] { + assert_eq!(only(&h, bus), only(&f, bus), "{bus:?} demand unchanged"); + } + + // ALU: the chip would accept the CPU's claim `1 << 1 = 0`. + let alu = only(&f, BusId::Alu); + assert_eq!(alu.len(), 1); + let (tuple, m) = alu.iter().next().unwrap(); + assert_eq!(*m, -FE::one(), "received once"); + let out = tuple[tuple.len() - 2] | (tuple[tuple.len() - 1] << 32); + assert_eq!(op.compute_out(), 2); + assert_eq!(out, 0, "forged result"); + } + + #[test] + fn zbs_two_padding_row_is_rejected() { + let (_, honest, forged) = forged_sll(); + let air = busless_air(cols::NUM_COLUMNS, ShiftConstraints); + assert!(validate_busless(&air, &honest), "honest trace must pass"); + assert!( + !validate_busless(&air, &forged), + "zbs = 2 must be rejected by IS_BIT[zbs]" + ); + } + + /// A left shift with μ = 2 claims twice the result (`left = μ - direction` + /// scales `out`); it would answer two identical CPU lookups with `2·(x << s)`. + #[test] + fn mu_two_left_shift_row_is_rejected() { + let op = ShiftOperation::new(1, 1, false, false, false); + let mut trace = generate_shift_trace(std::slice::from_ref(&op)); + { + let t = &mut trace.main_table; + assert_eq!(*t.get(0, cols::OUT_0), FE::from(2u64)); + t.set(0, cols::MU, FE::from(2u64)); + t.set(0, cols::OUT_0, FE::from(4u64)); + } + let air = busless_air(cols::NUM_COLUMNS, ShiftConstraints); + assert!( + !validate_busless(&air, &trace), + "μ = 2 must be rejected by IS_BIT[μ]" + ); + } } From 7c7e62a43fd532239b7cd383f05d5aeb96f224b4 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 2 Oct 2026 17:05:17 -0300 Subject: [PATCH 02/13] =?UTF-8?q?Bit-constrain=20LOAD=20=CE=BC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- executor/programs/asm/poc_lb_commit.s | 23 +++ prover/src/tables/load.rs | 13 +- prover/src/tests/load_tests.rs | 73 +++++++++ prover/src/tests/multiplicity_forgery_poc.rs | 154 ++++++++++++++++++- 4 files changed, 256 insertions(+), 7 deletions(-) create mode 100644 executor/programs/asm/poc_lb_commit.s diff --git a/executor/programs/asm/poc_lb_commit.s b/executor/programs/asm/poc_lb_commit.s new file mode 100644 index 000000000..c657f4517 --- /dev/null +++ b/executor/programs/asm/poc_lb_commit.s @@ -0,0 +1,23 @@ + .text + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # Store the byte 0x05 (sign bit clear), read it back with a real + # sign-extending LB, spill the result and commit it. The committed public + # output is the LOAD chip's res, so a proof reporting anything but 5 + # certifies a false sign extension. + addi sp, sp, -16 + addi t0, zero, 5 + sb t0, 8(sp) + lb t1, 8(sp) # t1 = sext(0x05) = 5 + sd t1, 0(sp) # spill to stack + li a0, 1 # fd = 1 + mv a1, sp # buf = sp + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + addi sp, sp, 16 + li a0, 0 + li a7, 93 # syscall = Halt + ecall diff --git a/prover/src/tables/load.rs b/prover/src/tables/load.rs index a18ebddd9..d914fd394 100644 --- a/prover/src/tables/load.rs +++ b/prover/src/tables/load.rs @@ -476,10 +476,11 @@ pub fn bus_interactions() -> Vec { // ========================================================================= // // One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..13: +// folder, the verifier folder and IR capture. Constraint indices 0..14: // 0..4: FlagIsBit(SIGNED, READ2, READ4, READ8) 4: WidthSumIsBit // 5: ReadImpliesMu 6..10: ExtensionHigh(4..8) // 10..12: ExtensionMid(2..4) 12: ExtensionLow +// 13: MuIsBit use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; @@ -575,5 +576,15 @@ impl ConstraintSet for LoadConstraints { let expected = Self::extended(b); let one = b.one(); b.emit_base(12, (one - read2 - read4 - read8) * (res_1 - expected)); + + // idx 13: MuIsBit — μ * (1 - μ). LOAD never deduplicates (one row per + // op), and idx 5 only pins μ = 1 when a read2/4/8 flag is set. On a byte + // load a free μ = −1 turns every lookup into a provider: a −1/+1 pair of + // LBU rows with the same `res[0]` cancels on MEMORY/MEMW (neither carries + // `sign_bit`) but nets `MSB8[res[0]] → ¬sign_bit` minus `→ sign_bit`, + // which cancels a real LB row's forged sign bit (`lb 0x05 = 0xFF..05` + // verified). + let root = Self::flag_is_bit(b, cols::MU); + b.emit_base(13, root); } } diff --git a/prover/src/tests/load_tests.rs b/prover/src/tests/load_tests.rs index a85a7a920..c15a5710f 100644 --- a/prover/src/tests/load_tests.rs +++ b/prover/src/tests/load_tests.rs @@ -61,3 +61,76 @@ fn test_sign_bit_extraction() { let op4 = LoadOperation::new(0, 0, 4, true, [0, 0, 0, 0x80, 0, 0, 0, 0]); assert!(op4.compute_sign_bit()); } + +// ========================================================================= +// Soundness regression: μ is bit-constrained (MuIsBit, idx 13). +// +// Before MuIsBit, idx 5 pinned μ = 1 only when a read2/4/8 flag was set, so a +// byte-load row's μ was free. A μ = −1 / μ = 1 pair of LBU rows with the same +// `res[0]` cancels on MEMORY/MEMW but nets `MSB8[res[0]] → 0` minus `→ 1`, +// which cancels a real LB row's forged `sign_bit = 1`: `lb 0x05` answered +// `0xFFFF_FFFF_FFFF_FF05` and verified end to end +// (`multiplicity_forgery_poc::load_negative_mu_sign_extension_forgery_is_rejected`). +// ========================================================================= + +mod mu_bit_regression { + use crate::tables::load::{LoadConstraints, LoadOperation, cols, generate_load_trace}; + use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; + use crate::test_utils::{busless_air, validate_busless}; + + type Trace = stark::trace::TraceTable; + + /// Row 0: the real `lb` of 0x05 with the forged sign extension. Rows 1/2: + /// the cancelling `μ = −1 / μ = 1` byte-load pair. + fn forged_lb() -> (Trace, Trace) { + let op = LoadOperation::new(0x1000, 100, 1, true, [0x05, 0, 0, 0, 0, 0, 0, 0]); + let honest = generate_load_trace(std::slice::from_ref(&op)); + let mut forged = honest.clone(); + let t = &mut forged.main_table; + assert_eq!(*t.get(0, cols::SIGN_BIT), FE::zero()); + for &c in &cols::RES[1..] { + t.set(0, c, FE::from(0xFFu64)); + } + t.set(0, cols::SIGN_BIT, FE::one()); + for (row, mu, sign_bit) in [(1, -FE::one(), FE::one()), (2, FE::one(), FE::zero())] { + t.set(row, cols::RES[0], FE::from(0x05u64)); + t.set(row, cols::MU, mu); + t.set(row, cols::SIGN_BIT, sign_bit); + } + (honest, forged) + } + + #[test] + fn negative_mu_byte_load_pair_is_rejected() { + let (honest, forged) = forged_lb(); + let air = busless_air(cols::NUM_COLUMNS, LoadConstraints); + assert!(validate_busless(&air, &honest), "honest trace must pass"); + assert!( + !validate_busless(&air, &forged), + "μ = −1 must be rejected by IS_BIT[μ]" + ); + } + + /// Every other in-chip constraint holds on the forged rows: only MuIsBit + /// stands between the trace and a forged sign extension. + #[test] + fn forged_rows_differ_from_valid_only_in_mu() { + let (_, mut forged) = forged_lb(); + forged.main_table.set(1, cols::MU, FE::zero()); + forged.main_table.set(2, cols::MU, FE::zero()); + let air = busless_air(cols::NUM_COLUMNS, LoadConstraints); + assert!(validate_busless(&air, &forged)); + } + + #[test] + fn mu_two_byte_load_row_is_rejected() { + let op = LoadOperation::new(0x1000, 100, 1, false, [0x42, 0, 0, 0, 0, 0, 0, 0]); + let mut trace = generate_load_trace(std::slice::from_ref(&op)); + trace.main_table.set(0, cols::MU, FE::from(2u64)); + let air = busless_air(cols::NUM_COLUMNS, LoadConstraints); + assert!( + !validate_busless(&air, &trace), + "μ = 2 must be rejected by IS_BIT[μ]" + ); + } +} diff --git a/prover/src/tests/multiplicity_forgery_poc.rs b/prover/src/tests/multiplicity_forgery_poc.rs index 19eac4739..11d858c73 100644 --- a/prover/src/tests/multiplicity_forgery_poc.rs +++ b/prover/src/tests/multiplicity_forgery_poc.rs @@ -1,6 +1,6 @@ //! End-to-end regression tests for unconstrained multiplicities: MUL's //! `μ_lo`/`μ_hi` and DVRM's `μ_q`/`μ_r` must be bounded and non-negative, and -//! SHIFT's `zbs` must be a bit. +//! SHIFT's `zbs` and LOAD's `μ` must be bits. //! //! **MUL / DVRM.** Both chips send every range check (and DVRM its MUL/LT/ZERO checks) with //! multiplicity `μ_a + μ_b`, the row's total lookup count. Before the fix neither @@ -16,6 +16,13 @@ //! exactly the HWSL tuples a forged real row needed (`1 << 1 = 0` verified //! against `main`). The fix bit-constrains `zbs` (and μ). //! +//! **LOAD.** LOAD never deduplicates, but μ was pinned to 1 only when a +//! read2/4/8 flag was set, so a byte-load row's μ was free. A `μ = −1 / μ = 1` +//! pair of LBU rows with the same `res[0]` cancels on MEMORY/MEMW (neither +//! carries `sign_bit`) while netting `MSB8[res[0]] → 0` minus `→ 1`, which +//! cancels a real LB row's forged sign bit (`lb 0x05 = 0xFF..05` verified +//! against `main`). The fix bit-constrains μ. +//! //! Each guest computes a value with one real instruction and commits it; the //! malicious prover claims a different value and reshapes the chip's rows. It //! also rebalances every BITWISE receiver multiplicity it can (those are free @@ -40,28 +47,43 @@ use crate::{MaxRowsConfig, VmAirs, VmProof}; use executor::elf::Elf; use executor::vm::execution::Executor; +use executor::vm::logs::Log; fn opts() -> ProofOptions { crate::GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 is valid") } -/// One forgery scenario: a guest whose single `lhs ∘ rhs` instruction yields -/// `honest`, and the chip rewrite that makes it yield `forged` instead. +/// One forgery scenario: a guest whose target instruction (picked out of the +/// logs by `is_target`) yields `honest`, and the chip rewrite that makes it +/// yield `forged` instead. struct Scenario { guest: &'static str, lhs: u64, rhs: u64, honest: u64, forged: u64, + is_target: fn(&Log, &Scenario) -> bool, forge_rows: fn(&mut Traces, &Scenario), } +/// An `lhs ∘ rhs = honest` arithmetic instruction. +fn arith_log(l: &Log, s: &Scenario) -> bool { + l.src1_val == s.lhs && l.src2_val == s.rhs && l.dst_val == s.honest +} + +/// The `lb t1, 8(sp)` log: the only instruction with a non-zero base register +/// that writes the honest byte (`li t0, 5` reads `zero`, `sb`/`sd` write none). +fn lb_log(l: &Log, s: &Scenario) -> bool { + l.src1_val != 0 && l.dst_val == s.honest +} + const MUL: Scenario = Scenario { guest: "poc_mul_commit", lhs: 3, rhs: 5, honest: 15, forged: 99, + is_target: arith_log, forge_rows: forge_mul_rows, }; @@ -71,6 +93,7 @@ const DIVU: Scenario = Scenario { rhs: 2, honest: 3, forged: 100, + is_target: arith_log, forge_rows: forge_dvrm_rows, }; @@ -80,13 +103,24 @@ const SLL: Scenario = Scenario { rhs: 1, honest: 2, forged: 0, + is_target: arith_log, forge_rows: forge_shift_rows, }; +const LB: Scenario = Scenario { + guest: "poc_lb_commit", + lhs: 0, + rhs: 0, + honest: 5, + forged: 0xFFFF_FFFF_FFFF_FF05, + is_target: lb_log, + forge_rows: forge_load_rows, +}; + /// Which deviations the malicious prover applies. #[derive(Clone, Copy)] struct Forge { - /// Rewrite the execution so the CPU claims `lhs ∘ rhs = forged`. + /// Rewrite the execution so the CPU claims the target yields `forged`. claim: bool, /// Rewrite the chip's rows so they answer the forged claim. rows: bool, @@ -105,8 +139,8 @@ fn craft_proof(s: &Scenario, forge: Forge) -> Result = (0..rows) + .filter(|&r| (0..cols::NUM_COLUMNS).all(|c| *t.get_main(r, c) == FE::zero())) + .take(2) + .collect(); + let [b, c] = padding[..] else { + panic!("two all-zero padding rows are needed for the cancelling pair"); + }; + + for &col in &cols::RES[1..] { + t.set_main(a, col, FE::from(FF)); + } + t.set_main(a, cols::SIGN_BIT, FE::one()); + for (row, mu, sign_bit) in [ + (b, FE::zero() - FE::one(), FE::one()), + (c, FE::one(), FE::zero()), + ] { + t.set_main(row, cols::RES[0], FE::from(byte)); + t.set_main(row, cols::MU, mu); + t.set_main(row, cols::SIGN_BIT, sign_bit); + } + + let m = traces.memw_aligneds.iter_mut().find_map(|m| { + (0..m.num_rows()) + .find(|&r| { + *m.get_main(r, ma::IS_REGISTER) == FE::zero() + && *m.get_main(r, ma::MU_READ) == FE::one() + && *m.get_main(r, ma::TIMESTAMP_0) == ts[0] + && *m.get_main(r, ma::TIMESTAMP_1) == ts[1] + }) + .map(|r| (m, r)) + }); + let (m, r) = m.expect("the MEMW_A read answering the LB not found"); + assert_eq!(*m.get_main(r, ma::VALUE[0]), FE::from(byte)); + for i in 1..8 { + m.set_main(r, ma::OLD[i], FE::from(FF)); + m.set_main(r, ma::VALUE[i], FE::from(FF)); + } +} + fn verifier_accepts(s: &Scenario, proof: &VmProof) -> bool { crate::verify_with_options(proof, &asm_elf_bytes(s.guest), &opts(), None, None) .expect("verify must not error") @@ -483,3 +591,37 @@ fn shift_zbs_two_padding_row_forgery_is_rejected() { "FORGERY: 1 << 1 = 0 was accepted — zbs is not bit-constrained" ); } + +#[test] +fn load_honest_control_verifies() { + assert_honest_verifies(&LB); +} + +/// Negative control: the CPU claims `lb 0x05 = 0xFF..05` but the LOAD rows are +/// left honest. +#[test] +fn load_unanswered_forged_claim_is_rejected() { + assert!(!crafted_accepted( + &LB, + Forge { + claim: true, + rows: false + } + )); +} + +/// Regression: `lb` of 0x05 sign-extended to `0xFFFF_FFFF_FFFF_FF05` via a +/// `μ = −1 / μ = 1` byte-load pair that swaps A's MSB8 tuple. +#[test] +fn load_negative_mu_sign_extension_forgery_is_rejected() { + assert!( + !crafted_accepted( + &LB, + Forge { + claim: true, + rows: true + } + ), + "FORGERY: lb 0x05 = 0xFFFFFFFFFFFFFF05 was accepted — LOAD's μ is not bit-constrained" + ); +} From 8580f42555de9c4a6add5b957f58ce9aeae03691 Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 5 Oct 2026 10:53:34 -0300 Subject: [PATCH 03/13] Bound LT multiplicity --- executor/programs/asm/poc_slt_commit.s | 23 ++ prover/src/tables/lt.rs | 60 +++- prover/src/tables/trace_builder.rs | 25 +- prover/src/tests/lt_multiplicity_poc.rs | 306 +++++++++++++++++++ prover/src/tests/lt_tests.rs | 113 ++++++- prover/src/tests/mod.rs | 2 + prover/src/tests/multiplicity_forgery_poc.rs | 134 +++++++- 7 files changed, 648 insertions(+), 15 deletions(-) create mode 100644 executor/programs/asm/poc_slt_commit.s create mode 100644 prover/src/tests/lt_multiplicity_poc.rs diff --git a/executor/programs/asm/poc_slt_commit.s b/executor/programs/asm/poc_slt_commit.s new file mode 100644 index 000000000..1c8ee32b9 --- /dev/null +++ b/executor/programs/asm/poc_slt_commit.s @@ -0,0 +1,23 @@ + .text + .attribute 5, "rv64i2p1" + .globl main +main: + # Compare 5 < 3 with a real SLT, spill the result to the stack and commit + # it. The committed public output is the LT chip's result, so a proof + # reporting anything but 0 certifies a false comparison. The spill comes + # right after the SLT so it is the first instruction to read the result. + addi sp, sp, -16 + addi a3, zero, 5 + addi a4, zero, 3 + slt t1, a3, a4 # t1 = (5 < 3) = 0 + sd t1, 0(sp) # spill to stack + li a0, 1 # fd = 1 + mv a1, sp # buf = sp + li a2, 8 # count = 8 + li a7, 64 # syscall = Commit + ecall + + addi sp, sp, 16 + li a0, 0 + li a7, 93 # syscall = Halt + ecall diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index fb7d34267..0ea208ec2 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -22,7 +22,8 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for lhs_msb, rhs_msb) -//! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]) +//! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]; +//! ×1 for the μ multiplicity bound) //! - Receiver: ALU (all less-than lookups — CPU SLT/BLT/BGE dispatch and the //! internal `memw`/`memw_aligned`/`dvrm` timestamp / |r|<|d| checks) @@ -152,20 +153,43 @@ impl LtOperation { } } -/// Generates the LT trace table from a list of operations. -/// -/// Duplicate operations (same lhs, rhs, signed) are merged into a single row -/// with their multiplicities summed. The table is then padded to the next power of 2. -pub fn generate_lt_trace( - operations: &[LtOperation], -) -> TraceTable { - // Deduplicate operations: (lhs, rhs, signed) -> multiplicity +/// Largest per-row multiplicity: `μ` is range-checked to a halfword +/// (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many lookups. The +/// bound is what keeps μ non-negative: without it a `μ = −1` twin of an honest +/// row cancels it on the ALU bus while *receiving* its range lookups, which +/// absorbs another row's out-of-range limb (a forged `5 < 3 = 1` verified). +pub const MU_MAX: u64 = (1 << 16) - 1; + +/// Deduplicates LT operations into trace rows: `(lhs, rhs, signed, invert) -> μ`, +/// splitting an op over several rows when its count exceeds [`MU_MAX`]. Shared +/// by trace generation and the BITWISE collector so the per-row lookups they +/// count cannot drift apart. +pub fn dedup_lt_rows(operations: &[LtOperation]) -> Vec<(LtOperation, u64)> { let mut op_map: HashMap = HashMap::new(); for op in operations { *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + let mut rows = Vec::with_capacity(op_map.len()); + for (op, mut left) in op_map { + while left > 0 { + let mu = left.min(MU_MAX); + left -= mu; + rows.push((op.clone(), mu)); + } + } + rows +} + +/// Generates the LT trace table from a list of operations. +/// +/// Duplicate operations (same lhs, rhs, signed, invert) are merged into a single +/// row with their multiplicities summed (see [`dedup_lt_rows`]). The table is +/// then padded to the next power of 2. +pub fn generate_lt_trace( + operations: &[LtOperation], +) -> TraceTable { + let unique_ops = dedup_lt_rows(operations); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), @@ -306,6 +330,22 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), + // IS_HALF[μ] | μ. Every lookup here fires with μ, so μ itself must be + // bounded and non-negative. Otherwise a μ = −1 twin of an honest row + // cancels it on the ALU bus while *receiving* its range lookups, with + // `sub_0` free up to 2^32: it absorbs an out-of-range IS_HALFWORD sent + // by any row, another LT row included (forged `5 < 3 = 1`). Sent with + // itself as multiplicity: `k` rows holding an out-of-range `v` put + // weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // (μ = 0) contributes nothing. See `MU_MAX`. + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: cols::MU, + packing: Packing::Direct, + }], + ), // ALU[lhs, rhs, opsel(LT) + 32*signed + 64*invert] -> out (receiver). // Every LT lookup arrives here: the CPU dispatches SLT/BLT/BGE on the // unified ALU bus, and the internal memw/memw_aligned/dvrm comparisons diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index e72ce502e..fbccd74c3 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1679,8 +1679,15 @@ fn reg_ts_delta_in_range(timestamp: u64, old_ts: u64) -> bool { /// Collects bitwise lookups from LT operations (MSB16 and IS_HALFWORD). /// +/// MSB16 and the operand/difference IS_HALFWORD lookups are emitted once per raw +/// op. The IS_HALF[μ] multiplicity bound is counted over the rows of each +/// `max_rows_lt` chunk, mirroring `chunk_and_generate_optional`. +/// /// Returns: Vec of bitwise lookups -fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { +pub(crate) fn collect_bitwise_from_lt( + lt_ops: &[LtOperation], + max_rows_lt: usize, +) -> Vec { let mut bitwise_ops = Vec::with_capacity(lt_ops.len() * 8); for op in lt_ops { @@ -1725,6 +1732,19 @@ fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { )); } + // IS_HALF[μ] | μ: each row sends its own μ, μ times (padding sends nothing), + // over exactly the rows `generate_lt_trace` builds for each chunk. + for chunk in lt_ops.chunks(max_rows_lt) { + for (_, mu) in lt::dedup_lt_rows(chunk) { + let op = BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (mu & 0xFF) as u8, + ((mu >> 8) & 0xFF) as u8, + ); + bitwise_ops.extend(std::iter::repeat_n(op, mu as usize)); + } + } + bitwise_ops } @@ -3315,12 +3335,13 @@ fn build_traces( // commutative monoid, so per-worker histograms tree-reduce to multiplicities that are // independent of accumulation order. type Collector<'a> = Box; + let lt_chunk = max_rows.lt; let mul_chunk = max_rows.mul; let dvrm_chunk = max_rows.dvrm; // Every source except the two dominant ones (the in-walk lookups and MEMW_R, which are // split into row-ranges in the parallel path below) stays a single whole-source collector. let mut collectors: Vec = vec![ - Box::new(|h| h.add_ops(&collect_bitwise_from_lt(<_ops))), + Box::new(|h| h.add_ops(&collect_bitwise_from_lt(<_ops, lt_chunk))), Box::new(|h| h.add_ops(&collect_bitwise_from_mul(&mul_ops, mul_chunk))), Box::new(|h| h.add_ops(&collect_bitwise_from_dvrm(&dvrm_ops, dvrm_chunk))), Box::new(|h| h.add_ops(&collect_bitwise_from_branch(&branch_ops))), diff --git a/prover/src/tests/lt_multiplicity_poc.rs b/prover/src/tests/lt_multiplicity_poc.rs new file mode 100644 index 000000000..deecb0f4a --- /dev/null +++ b/prover/src/tests/lt_multiplicity_poc.rs @@ -0,0 +1,306 @@ +//! LT's `μ` must be a bounded, non-negative multiplicity (chip-level +//! regression; the end-to-end one is `multiplicity_forgery_poc::lt_*`). +//! +//! LT weights its ALU receive and all of its range lookups (2× MSB16, +//! 6× IS_HALFWORD) by the same `μ`. A row with `μ = −1` therefore acts as an ALU +//! *sender* and a range-check *receiver*. Paired with an honest `μ = +1` copy +//! carrying the same ALU tuple, the two cancel on the ALU bus, but their range +//! lookups do not have to match: the `−1` twin can hold `sub_0 = X` (any +//! `X < 2^32`) with `sub_1 = 0` and still satisfy the carry constraints, so one +//! IS_HALFWORD receive of X appears from nowhere. That absorbs an out-of-range +//! limb of *any* sender, another LT row included — which forges the LT result. +//! The fix range-checks μ (`IS_HALF[μ]`, weighted by μ), so a twin's `μ = −1` +//! itself has no receiver. +//! +//! Harness, with the real LT AIR (`lt::bus_interactions()` + `LtConstraints`): +//! - CPU: a mock ALU sender for the LT lookups the program "made". +//! - VICTIM: an optional mock IS_HALFWORD sender. +//! - RANGE / MSB16: stand-ins for the preprocessed BITWISE receivers, built +//! honestly (exactly the halfwords 0..2^16). Their multiplicities are the net +//! demand of every other table, *evaluated from the real interactions* — so a +//! lookup added by a fix is tallied automatically, and a value outside the +//! table can only balance if the other tables cancel it themselves. + +use std::collections::HashMap; + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use math::field::element::FieldElement; +use stark::constraints::builder::EmptyConstraints; +use stark::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, + NullBoundaryConstraintBuilder, Packing, +}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; +use stark::traits::AIR; +use stark::verifier::{IsStarkVerifier, Verifier}; + +use crate::tables::lt::{LtOperation, bus_interactions, cols, generate_lt_trace}; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField, alu_op}; +use crate::test_utils::{create_lt_air, multi_prove_ram}; + +type F = GoldilocksField; +type E = GoldilocksExtension; +type MockAir = AirWithBuses; +pub(crate) type Row = Vec; + +const HALF: u64 = 1 << 16; + +/// A mock table with one interaction: columns `0..n` are the tuple, column `n` +/// the multiplicity. +fn lookup_air(opts: &ProofOptions, bus: BusId, n: usize, sender: bool) -> MockAir { + let values = (0..n) + .map(|c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }) + .collect(); + let i = if sender { + BusInteraction::sender(bus, Multiplicity::Column(n), values) + } else { + BusInteraction::receiver(bus, Multiplicity::Column(n), values) + }; + AirWithBuses::new( + n + 1, + AuxiliaryTraceBuildData { + interactions: vec![i], + }, + opts, + 1, + EmptyConstraints, + ) +} + +/// Trace for `lookup_air`: one row per `(tuple, multiplicity)`, zero-padded. +fn lookup_trace(rows: &[(Vec, FE)], n: usize) -> TraceTable { + let len = rows.len().next_power_of_two().max(4); + let mut data = vec![FE::zero(); len * (n + 1)]; + for (r, (tuple, m)) in rows.iter().enumerate() { + for (c, v) in tuple.iter().enumerate() { + data[r * (n + 1) + c] = FE::from(*v); + } + data[r * (n + 1) + n] = *m; + } + TraceTable::new_main(data, n + 1, 1) +} + +fn eval_mult(m: &Multiplicity, g: &dyn Fn(usize) -> FE) -> FE { + match m { + Multiplicity::One => FE::one(), + Multiplicity::Column(c) => g(*c), + Multiplicity::Sum(a, b) => g(*a) + g(*b), + Multiplicity::Negated(c) => FE::one() - g(*c), + Multiplicity::Diff(a, b) => g(*a) - g(*b), + Multiplicity::Sum3(a, b, c) => g(*a) + g(*b) + g(*c), + Multiplicity::Linear(ts) => ts.iter().fold(FE::zero(), |acc, t| match *t { + LinearTerm::Column { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::ColumnUnsigned { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::Constant(v) => acc + FE::from(v), + }), + } +} + +/// Net sends per `(bus, tuple)` of LT's real interactions over `rows`. +pub(crate) fn lt_net(rows: &[Row]) -> HashMap<(u64, Vec), FE> { + let mut net: HashMap<(u64, Vec), FE> = HashMap::new(); + for bi in bus_interactions() { + for row in rows { + let g = |c: usize| row[c]; + let m = eval_mult(&bi.multiplicity, &g); + if m == FE::zero() { + continue; + } + let tuple = bi + .values + .iter() + .flat_map(|v| v.combine_from(g)) + .map(|x: FE| x.canonical_u64()) + .collect(); + let e = net.entry((bi.bus_id, tuple)).or_insert(FE::zero()); + *e = if bi.is_sender { *e + m } else { *e - m }; + } + } + net +} + +/// The ALU tuple an LT lookup carries: `[lhs_lo, lhs_hi, rhs_lo, rhs_hi, flags, out, 0]`. +fn alu_tuple(op: &LtOperation, out: u64) -> Vec { + let flags = alu_op::LT as u64 + 32 * op.signed as u64 + 64 * op.invert as u64; + vec![ + op.lhs & 0xFFFF_FFFF, + op.lhs >> 32, + op.rhs & 0xFFFF_FFFF, + op.rhs >> 32, + flags, + out, + 0, + ] +} + +/// The honest LT row for `op`. +pub(crate) fn honest_row(op: &LtOperation) -> Row { + let t = generate_lt_trace(std::slice::from_ref(op)); + let row = t.main_table.get_row(0).to_vec(); + assert_eq!(row[cols::MU], FE::one()); + row +} + +/// A `μ = −1` copy of `op`'s honest row whose `sub_0` is `x` (with `sub_1 = 0`, +/// so `sub_0 + 2^16·sub_1` and every carry are unchanged). Needs `lhs − rhs = x` +/// on the low word, `x < 2^32`. +pub(crate) fn twin_row(op: &LtOperation, x: u64) -> Row { + let mut row = honest_row(op); + assert_eq!(op.lhs.wrapping_sub(op.rhs) & 0xFFFF_FFFF, x); + row[cols::MU] = -FE::one(); + row[cols::LHS_SUB_RHS_0] = FE::from(x); + row[cols::LHS_SUB_RHS_1] = FE::zero(); + row +} + +/// Proves CPU + LT + VICTIM + RANGE + MSB16 and returns whether it verifies. +/// +/// `cpu`: the ALU lookups the CPU sends (once each). `victim`: IS_HALFWORD +/// values sent by another table. RANGE/MSB16 absorb the net demand for every +/// value they have a row for; anything else is left for the bus to reject. +fn prove_and_verify(lt_rows: &[Row], cpu: &[Vec], victim: &[u64]) -> bool { + let opts = ProofOptions::default_test_options(); + let half_id: u64 = BusId::IsHalfword.into(); + let msb_id: u64 = BusId::Msb16.into(); + + let mut net = lt_net(lt_rows); + for &v in victim { + *net.entry((half_id, vec![v])).or_insert(FE::zero()) += FE::one(); + } + let range: Vec<(Vec, FE)> = (0..HALF) + .map(|v| { + let m = net.get(&(half_id, vec![v])).copied().unwrap_or(FE::zero()); + (vec![v], m) + }) + .collect(); + let msb16: Vec<(Vec, FE)> = (0..HALF) + .map(|v| { + let t = vec![v, v >> 15]; + let m = net.get(&(msb_id, t.clone())).copied().unwrap_or(FE::zero()); + (t, m) + }) + .collect(); + let cpu_rows: Vec<(Vec, FE)> = cpu.iter().map(|t| (t.clone(), FE::one())).collect(); + let victim_rows: Vec<(Vec, FE)> = victim.iter().map(|&v| (vec![v], FE::one())).collect(); + + let lt_len = lt_rows.len().next_power_of_two().max(4); + let mut lt_data = vec![FE::zero(); lt_len * cols::NUM_COLUMNS]; + for (r, row) in lt_rows.iter().enumerate() { + lt_data[r * cols::NUM_COLUMNS..(r + 1) * cols::NUM_COLUMNS].copy_from_slice(row); + } + let mut lt_trace = TraceTable::new_main(lt_data, cols::NUM_COLUMNS, 1); + let mut cpu_trace = lookup_trace(&cpu_rows, 7); + let mut victim_trace = lookup_trace(&victim_rows, 1); + let mut range_trace = lookup_trace(&range, 1); + let mut msb16_trace = lookup_trace(&msb16, 2); + + let lt_air = create_lt_air(&opts); + let cpu_air = lookup_air(&opts, BusId::Alu, 7, true); + let victim_air = lookup_air(&opts, BusId::IsHalfword, 1, true); + let range_air = lookup_air(&opts, BusId::IsHalfword, 1, false); + let msb16_air = lookup_air(&opts, BusId::Msb16, 2, false); + + let pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&victim_air, &mut victim_trace, &()), + (<_air, &mut lt_trace, &()), + (&range_air, &mut range_trace, &()), + (&msb16_air, &mut msb16_trace, &()), + ]; + let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &victim_air, <_air, &range_air, &msb16_air]; + Verifier::multi_verify( + &airs, + &proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ) +} + +/// The honest LT row's out, as the CPU would receive it. +fn honest_out(op: &LtOperation) -> u64 { + honest_row(op)[cols::OUT].canonical_u64() +} + +/// Positive control: honest LT rows answering the CPU verify. Without this, a +/// "rejected" below would say nothing. +#[test] +fn control_honest_rows_verify() { + let ops = [ + LtOperation::new(5, 3, false), + LtOperation::new(HALF, 0, false), + ]; + let rows: Vec = ops.iter().map(honest_row).collect(); + let cpu: Vec<_> = ops.iter().map(|op| alu_tuple(op, honest_out(op))).collect(); + assert!(prove_and_verify(&rows, &cpu, &[])); +} + +/// Control: an out-of-range IS_HALFWORD send with no twin has no receiver. +#[test] +fn control_out_of_range_victim_is_rejected() { + let op = LtOperation::new(HALF, 0, false); + assert!(!prove_and_verify( + &[honest_row(&op)], + &[alu_tuple(&op, honest_out(&op))], + &[HALF] + )); +} + +/// Control: a twin whose carry no longer holds is rejected by `LtConstraints`. +#[test] +fn control_twin_with_broken_carry_is_rejected() { + let op = LtOperation::new(HALF, 0, false); + let mut twin = twin_row(&op, HALF); + twin[cols::LHS_SUB_RHS_1] = FE::one(); + assert!(!prove_and_verify(&[honest_row(&op), twin], &[], &[HALF])); +} + +/// Regression: a `μ = −1` twin absorbing another table's out-of-range +/// IS_HALFWORD[2^16] (accepted before LT's μ was bounded). +#[test] +fn regression_negative_mu_twin_cannot_absorb_victim() { + let op = LtOperation::new(HALF, 0, false); + assert!(!prove_and_verify( + &[honest_row(&op), twin_row(&op, HALF)], + &[], + &[HALF] + )); +} + +/// Regression: the victim can be LT itself — `5 < 3` claimed true (accepted +/// before LT's μ was bounded). +/// +/// Row A (μ = 1) answers the CPU's `LT(5, 3) = 1` with `carry_1 = 1`: its high +/// `lhs − rhs` word becomes `2^32`, split as `sub_2 = 0, sub_3 = 2^16` — every +/// LT constraint holds, but `sub_3` is not a halfword. Twin C (`μ = −1`, op +/// `2^16 − 0`) absorbs IS_HALFWORD[2^16]; D, the honest `2^16 − 0` row, cancels +/// C on the ALU bus. +#[test] +fn regression_negative_mu_twin_cannot_forge_5_lt_3() { + let op = LtOperation::new(5, 3, false); + assert_eq!(honest_out(&op), 0); + let mut a = honest_row(&op); + a[cols::LT] = FE::one(); + a[cols::OUT] = FE::one(); + a[cols::LHS_SUB_RHS_2] = FE::zero(); + a[cols::LHS_SUB_RHS_3] = FE::from(HALF); + + let carrier = LtOperation::new(HALF, 0, false); + let rows = [a, twin_row(&carrier, HALF), honest_row(&carrier)]; + assert!(!prove_and_verify(&rows, &[alu_tuple(&op, 1)], &[])); +} diff --git a/prover/src/tests/lt_tests.rs b/prover/src/tests/lt_tests.rs index d7f707a13..ea4f92e38 100644 --- a/prover/src/tests/lt_tests.rs +++ b/prover/src/tests/lt_tests.rs @@ -169,8 +169,8 @@ fn test_bus_interactions_count() { // MSB16 x2 + IS_HALFWORD x6 (lhs_sub_rhs x4 + lhs[1] + rhs[1]) // + ALU receiver x1 (every LT lookup goes through the unified ALU bus // — CPU SLT/BLT/BGE dispatch and the internal memw/dvrm - // timestamp / |r|<|d| checks) = 9. - assert_eq!(interactions.len(), 9); + // timestamp / |r|<|d| checks) + IS_HALFWORD x1 bounding μ = 10. + assert_eq!(interactions.len(), 10); } // Soundness regression: `lt` must equal `(lhs < rhs)`. The in-chip constraints were @@ -232,3 +232,112 @@ fn test_lt_rejects_forged_out() { "forged out=1 (lt=invert=0) must be rejected by OutXorInvert" ); } + +// Soundness regression: μ is a bounded, non-negative multiplicity. Every LT +// lookup fires with μ, so a free μ = −1 twin of an honest row received range +// lookups instead of sending them and absorbed another row's out-of-range limb +// (`lt_multiplicity_poc`, `multiplicity_forgery_poc`). μ is now IS_HALF-checked +// weighted by itself, and trace generation splits a row whose count would +// exceed `MU_MAX`. + +/// Presence: μ is IS_HALF-checked weighted by itself, so an out-of-range value +/// `v` always lands on the bus with weight `v ≠ 0`. +#[test] +fn test_lt_bounds_its_multiplicity() { + use crate::tables::types::BusId; + use stark::lookup::{BusValue, Multiplicity, Packing}; + assert!( + bus_interactions().iter().any(|i| i.is_sender + && i.bus_id == BusId::IsHalfword as u64 + && matches!(i.multiplicity, Multiplicity::Column(m) if m == cols::MU) + && matches!(i.values.as_slice(), + [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == cols::MU)), + "LT must IS_HALF-check μ weighted by itself" + ); +} + +/// Splitting: a count above `MU_MAX` spreads over rows within the bound that +/// preserve the total; exactly `MU_MAX` still fits one row. +#[test] +fn test_dedup_lt_rows_splits_counts_above_mu_max() { + use crate::tables::lt::{MU_MAX, dedup_lt_rows}; + let op = LtOperation::new(5, 3, SIGNED); + let ops: Vec<_> = std::iter::repeat_n(op.clone(), 2 * MU_MAX as usize + 7).collect(); + let mut rows: Vec = dedup_lt_rows(&ops).iter().map(|(_, mu)| *mu).collect(); + rows.sort(); + assert_eq!(rows, vec![7, MU_MAX, MU_MAX]); + + let ops: Vec<_> = std::iter::repeat_n(op, MU_MAX as usize).collect(); + assert_eq!(dedup_lt_rows(&ops).len(), 1); + assert!(dedup_lt_rows(&[]).is_empty()); + + // The generated trace never holds a μ above the bound. + let ops: Vec<_> = + std::iter::repeat_n(LtOperation::new(1, 2, UNSIGNED), MU_MAX as usize + 1).collect(); + let trace = generate_lt_trace(&ops); + let mut total = 0u64; + for r in 0..trace.num_rows() { + let mu = trace.get_main(r, cols::MU).to_raw(); + assert!(mu <= MU_MAX); + total += mu; + } + assert_eq!(total, ops.len() as u64); +} + +/// Consistency: the BITWISE collector tallies exactly the IS_HALF[μ] lookups the +/// generated LT instances send (each row's μ, weighted by μ; padding nothing), +/// across several small instances and for a row split by `MU_MAX`. +#[test] +fn test_lt_mu_bound_lookups_match_collector() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::lt::MU_MAX; + use crate::tables::trace_builder::collect_bitwise_from_lt; + use std::collections::HashMap; + + let half = |h: u64| ((h & 0xFF) as u8, ((h >> 8) & 0xFF) as u8); + let distinct = [ + LtOperation::new(5, 3, SIGNED), + LtOperation::new(u64::MAX, 1, UNSIGNED), + LtOperation::new(0x1234_5678_9abc_def0, 0x1234_5678_0000_0000, SIGNED), + ]; + let small: Vec<_> = distinct.iter().cycle().take(11).cloned().collect(); + let split: Vec<_> = std::iter::repeat_n(distinct[0].clone(), MU_MAX as usize + 2) + .chain(distinct.iter().cloned()) + .collect(); + + for (ops, chunk) in [(small, 4usize), (split, 1 << 20)] { + let collected = collect_bitwise_from_lt(&ops, chunk); + + // IS_HALF minus the per-raw-op range checks leaves the μ bound. + let mut is_half: HashMap<(u8, u8), i64> = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::IsHalf) + { + *is_half.entry((b.x, b.y)).or_default() += 1; + } + for op in &ops { + let sub = op.lhs.wrapping_sub(op.rhs); + for shift in [0, 16, 32, 48] { + *is_half.entry(half(sub >> shift & 0xFFFF)).or_default() -= 1; + } + *is_half.entry(half(op.lhs >> 32 & 0xFFFF)).or_default() -= 1; + *is_half.entry(half(op.rhs >> 32 & 0xFFFF)).or_default() -= 1; + } + + let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + for c in ops.chunks(chunk) { + let t = generate_lt_trace(c); + for r in 0..t.num_rows() { + let mu = t.get_main(r, cols::MU).to_raw(); + *expected.entry(half(mu)).or_default() += mu as i64; + } + } + is_half.retain(|_, n| *n != 0); + expected.retain(|_, n| *n != 0); + assert_eq!( + is_half, expected, + "IS_HALF[μ] tally must match the trace rows" + ); + } +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 4d8d08e23..11051e08e 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -59,6 +59,8 @@ pub mod local_to_global_bus_tests; #[cfg(test)] pub mod lt_bus_tests; #[cfg(test)] +pub mod lt_multiplicity_poc; +#[cfg(test)] pub mod lt_tests; #[cfg(test)] pub mod memw_aligned_tests; diff --git a/prover/src/tests/multiplicity_forgery_poc.rs b/prover/src/tests/multiplicity_forgery_poc.rs index 11d858c73..afb8677f9 100644 --- a/prover/src/tests/multiplicity_forgery_poc.rs +++ b/prover/src/tests/multiplicity_forgery_poc.rs @@ -1,6 +1,7 @@ //! End-to-end regression tests for unconstrained multiplicities: MUL's //! `μ_lo`/`μ_hi` and DVRM's `μ_q`/`μ_r` must be bounded and non-negative, and -//! SHIFT's `zbs` and LOAD's `μ` must be bits. +//! SHIFT's `zbs` and LOAD's `μ` must be bits, and LT's `μ` must be bounded and +//! non-negative. //! //! **MUL / DVRM.** Both chips send every range check (and DVRM its MUL/LT/ZERO checks) with //! multiplicity `μ_a + μ_b`, the row's total lookup count. Before the fix neither @@ -23,6 +24,13 @@ //! cancels a real LB row's forged sign bit (`lb 0x05 = 0xFF..05` verified //! against `main`). The fix bit-constrains μ. //! +//! **LT.** LT weights its ALU receive and all its range lookups by one free μ. A +//! `μ = −1` twin of an honest row cancels it on the ALU bus while *receiving* +//! its range lookups, with `sub_0` set to any `X < 2^32` — so it absorbs an +//! out-of-range IS_HALFWORD send. The victim can be another LT row: `5 < 3` +//! answered 1 with a `sub_3 = 2^16` limb verified against the branch before the +//! LT fix. See also `lt_multiplicity_poc` (chip level). +//! //! Each guest computes a value with one real instruction and commits it; the //! malicious prover claims a different value and reshapes the chip's rows. It //! also rebalances every BITWISE receiver multiplicity it can (those are free @@ -107,6 +115,16 @@ const SLL: Scenario = Scenario { forge_rows: forge_shift_rows, }; +const SLT: Scenario = Scenario { + guest: "poc_slt_commit", + lhs: 5, + rhs: 3, + honest: 0, + forged: 1, + is_target: arith_log, + forge_rows: forge_lt_rows, +}; + const LB: Scenario = Scenario { guest: "poc_lb_commit", lhs: 0, @@ -458,6 +476,87 @@ fn forge_load_rows(traces: &mut Traces, s: &Scenario) { } } +/// LT: `5 < 3` forged to 1. +/// +/// * Row A (the real SLT, `μ = 1`) gets `lt = out = 1` and `carry_1 = 1`: its +/// high `lhs − rhs` word becomes `2^32`, split as `sub_2 = 0, sub_3 = 2^16`. +/// Every LT constraint holds; only `IS_HALFWORD[2^16]` is out of range. +/// * Padding row C becomes a `μ = −1` twin of the op `2^16 − 0` with +/// `sub_0 = 2^16, sub_1 = 0`: it *receives* `IS_HALFWORD[2^16]`. +/// * Padding row D is the honest `2^16 − 0` row, cancelling C on the ALU bus. +/// +/// The BITWISE IS_HALF/MSB16 multiplicities are moved by the net change in LT's +/// own sends, evaluated from the real interactions (so a lookup added by the +/// fix is accounted for); a value with no BITWISE row is left for the bus. +fn forge_lt_rows(traces: &mut Traces, s: &Scenario) { + use super::lt_multiplicity_poc::{Row, honest_row, lt_net, twin_row}; + use crate::tables::lt::{LtOperation, cols}; + const HALF: u64 = 1 << 16; + + let t = &mut traces.lts[0]; + let rows = |t: &TraceTable| -> Vec { + (0..t.num_rows()) + .map(|r| (0..cols::NUM_COLUMNS).map(|c| *t.get_main(r, c)).collect()) + .collect() + }; + let before = rows(t); + + let a = (0..t.num_rows()) + .find(|&r| { + *t.get_main(r, cols::LHS_0) == FE::from(s.lhs) + && *t.get_main(r, cols::RHS_0) == FE::from(s.rhs) + && *t.get_main(r, cols::MU) == FE::one() + }) + .expect("honest SLT row not found"); + assert_eq!(*t.get_main(a, cols::OUT), FE::from(s.honest)); + // Equal high words and no low borrow: the honest high diff word is 0. + assert_eq!(*t.get_main(a, cols::LHS_SUB_RHS_2), FE::zero()); + assert_eq!(*t.get_main(a, cols::LHS_SUB_RHS_3), FE::zero()); + let padding: Vec = (0..t.num_rows()) + .filter(|&r| (0..cols::NUM_COLUMNS).all(|c| *t.get_main(r, c) == FE::zero())) + .take(2) + .collect(); + let [c, d] = padding[..] else { + panic!("two all-zero padding rows are needed for the twin and its honest copy"); + }; + + t.set_main(a, cols::LT, FE::one()); + t.set_main(a, cols::OUT, FE::from(s.forged)); + t.set_main(a, cols::LHS_SUB_RHS_3, FE::from(HALF)); + let carrier = LtOperation::new(HALF, 0, false); + for (r, row) in [(c, twin_row(&carrier, HALF)), (d, honest_row(&carrier))] { + for (col, v) in row.into_iter().enumerate() { + t.set_main(r, col, v); + } + } + let after = rows(t); + + let (old, new) = (lt_net(&before), lt_net(&after)); + let half_id: u64 = BusId::IsHalfword.into(); + let msb_id: u64 = BusId::Msb16.into(); + let keys: std::collections::HashSet<_> = old.keys().chain(new.keys()).cloned().collect(); + for (bus, tuple) in keys { + let delta = new + .get(&(bus, tuple.clone())) + .copied() + .unwrap_or(FE::zero()) + - old + .get(&(bus, tuple.clone())) + .copied() + .unwrap_or(FE::zero()); + let v = tuple[0]; + if delta == FE::zero() || v >= HALF { + continue; + } + if bus == half_id { + bump_bitwise(traces, bw_cols::MU_IS_HALF, v, delta); + } else if bus == msb_id { + assert_eq!(tuple[1], v >> 15, "MSB16 sends stay honest"); + bump_bitwise(traces, bw_cols::MU_MSB16, v, delta); + } + } +} + fn verifier_accepts(s: &Scenario, proof: &VmProof) -> bool { crate::verify_with_options(proof, &asm_elf_bytes(s.guest), &opts(), None, None) .expect("verify must not error") @@ -625,3 +724,36 @@ fn load_negative_mu_sign_extension_forgery_is_rejected() { "FORGERY: lb 0x05 = 0xFFFFFFFFFFFFFF05 was accepted — LOAD's μ is not bit-constrained" ); } + +#[test] +fn lt_honest_control_verifies() { + assert_honest_verifies(&SLT); +} + +/// Negative control: the CPU claims `5 < 3` but the LT rows are left honest. +#[test] +fn lt_unanswered_forged_claim_is_rejected() { + assert!(!crafted_accepted( + &SLT, + Forge { + claim: true, + rows: false + } + )); +} + +/// Regression: `5 < 3` answered 1 via a `μ = −1` twin absorbing the forged row's +/// out-of-range `sub_3 = 2^16` limb. +#[test] +fn lt_negative_mu_twin_forgery_is_rejected() { + assert!( + !crafted_accepted( + &SLT, + Forge { + claim: true, + rows: true + } + ), + "FORGERY: 5 < 3 = 1 was accepted — LT's μ is not bounded" + ); +} From 5fec4bf72a04def3cfcc686a1f808e7f35bead12 Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 5 Oct 2026 12:46:55 -0300 Subject: [PATCH 04/13] Bound BRANCH multiplicity --- prover/src/tables/branch.rs | 59 ++++- prover/src/tables/trace_builder.rs | 21 +- prover/src/tests/branch_bus_tests.rs | 112 ++++++++ prover/src/tests/branch_multiplicity_poc.rs | 246 ++++++++++++++++++ prover/src/tests/mod.rs | 4 + prover/src/tests/mul_mu_carrier_poc.rs | 270 ++++++++++++++++++++ 6 files changed, 700 insertions(+), 12 deletions(-) create mode 100644 prover/src/tests/branch_multiplicity_poc.rs create mode 100644 prover/src/tests/mul_mu_carrier_poc.rs diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 0d3c2e206..0847d6b8f 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -150,20 +150,43 @@ impl BranchOperation { } } -/// Generates the BRANCH trace table from a list of operations. -/// -/// Duplicate operations (same pc, offset, register, jalr) are merged into a single row -/// with their multiplicities summed. The table is then padded to the next power of 2. -pub fn generate_branch_trace( - operations: &[BranchOperation], -) -> TraceTable { - // Deduplicate operations: (pc, offset, register, jalr) -> multiplicity +/// Largest per-row multiplicity: `μ` is range-checked to a halfword +/// (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many lookups. The +/// bound keeps μ non-negative: without it a `μ = −1` twin of an honest row +/// cancels it on the BRANCH bus while *receiving* its range lookups, absorbing +/// another row's out-of-range limb (same bug as LT). +pub const MU_MAX: u64 = (1 << 16) - 1; + +/// Deduplicates BRANCH operations into trace rows: `(pc, offset, register, +/// jalr) -> μ`, splitting an op over several rows when its count exceeds +/// [`MU_MAX`]. Shared by trace generation and the BITWISE collector so the +/// per-row lookups they count cannot drift apart. +pub fn dedup_branch_rows(operations: &[BranchOperation]) -> Vec<(BranchOperation, u64)> { let mut op_map: HashMap = HashMap::new(); for op in operations { *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + let mut rows = Vec::with_capacity(op_map.len()); + for (op, mut left) in op_map { + while left > 0 { + let mu = left.min(MU_MAX); + left -= mu; + rows.push((op.clone(), mu)); + } + } + rows +} + +/// Generates the BRANCH trace table from a list of operations. +/// +/// Duplicate operations (same pc, offset, register, jalr) are merged into a +/// single row with their multiplicities summed (see [`dedup_branch_rows`]). The +/// table is then padded to the next power of 2. +pub fn generate_branch_trace( + operations: &[BranchOperation], +) -> TraceTable { + let unique_ops = dedup_branch_rows(operations); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), @@ -222,7 +245,8 @@ pub fn generate_branch_trace( /// - **Sends** ARE_BYTES lookup for next_pc_low[1] range check (Y=0) /// - **Sends** BYTE_ALU[AND] lookup for LSB masking /// (next_pc_low[0] = unmasked_low_byte & 254) -/// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks +/// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks and for +/// the μ multiplicity bound /// - **Receives** BRANCH lookups from CPU table pub fn bus_interactions() -> Vec { vec![ @@ -283,6 +307,21 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), + // IS_HALF[μ] | μ. Every lookup here fires with μ, so μ itself must be + // bounded and non-negative. Otherwise a μ = −1 twin of an honest row + // cancels it on the BRANCH bus while *receiving* its range lookups and + // absorbs an out-of-range IS_HALFWORD sent by any row (same as LT). Sent + // with itself as multiplicity: `k` rows holding an out-of-range `v` put + // weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // (μ = 0) contributes nothing. See `MU_MAX`. + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![BusValue::Packed { + start_column: cols::MU, + packing: Packing::Direct, + }], + ), // BRANCH[next_pc; pc, offset, register, JALR] (receiver) // Signature: [next_pc (DWordWL), pc (DWordWL), offset (DWordWL), register (DWordWL), JALR (Bit)] BusInteraction::receiver( diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index fbccd74c3..e56e68a0a 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2046,7 +2046,10 @@ pub(crate) fn collect_bitwise_from_dvrm( /// - IS_HALFWORD[next_pc_high[0..3]] - range checks for bits 16-63 /// /// Returns: Vec of bitwise lookups -fn collect_bitwise_from_branch(branch_ops: &[BranchOperation]) -> Vec { +pub(crate) fn collect_bitwise_from_branch( + branch_ops: &[BranchOperation], + max_rows_branch: usize, +) -> Vec { let mut bitwise_ops = Vec::with_capacity(branch_ops.len() * 5); for op in branch_ops { @@ -2097,6 +2100,19 @@ fn collect_bitwise_from_branch(branch_ops: &[BranchOperation]) -> Vec> 8) & 0xFF) as u8, + ); + bitwise_ops.extend(std::iter::repeat_n(op, mu as usize)); + } + } + bitwise_ops } @@ -3336,6 +3352,7 @@ fn build_traces( // independent of accumulation order. type Collector<'a> = Box; let lt_chunk = max_rows.lt; + let branch_chunk = max_rows.branch; let mul_chunk = max_rows.mul; let dvrm_chunk = max_rows.dvrm; // Every source except the two dominant ones (the in-walk lookups and MEMW_R, which are @@ -3344,7 +3361,7 @@ fn build_traces( Box::new(|h| h.add_ops(&collect_bitwise_from_lt(<_ops, lt_chunk))), Box::new(|h| h.add_ops(&collect_bitwise_from_mul(&mul_ops, mul_chunk))), Box::new(|h| h.add_ops(&collect_bitwise_from_dvrm(&dvrm_ops, dvrm_chunk))), - Box::new(|h| h.add_ops(&collect_bitwise_from_branch(&branch_ops))), + Box::new(|h| h.add_ops(&collect_bitwise_from_branch(&branch_ops, branch_chunk))), Box::new(|h| h.add_ops(&shift::collect_bitwise_from_shift(&shift_ops))), Box::new(|h| { for op in &bytewise_ops { diff --git a/prover/src/tests/branch_bus_tests.rs b/prover/src/tests/branch_bus_tests.rs index ee81ebb5a..710554155 100644 --- a/prover/src/tests/branch_bus_tests.rs +++ b/prover/src/tests/branch_bus_tests.rs @@ -690,3 +690,115 @@ fn test_soundness_wrong_offset() { assert!(!prove_and_verify_custom(&ops, &receiver_rows)); } + +// Soundness regression: μ is a bounded, non-negative multiplicity. Every BRANCH +// lookup fires with μ, so a free μ = −1 twin of an honest row received range +// lookups instead of sending them and absorbed another row's out-of-range limb +// (`branch_multiplicity_poc`). μ is now IS_HALF-checked weighted by itself, and +// trace generation splits a row whose count would exceed `MU_MAX`. +mod mu_bound { + use crate::tables::branch::BranchOperation; + use crate::tables::branch::{ + MU_MAX, bus_interactions, cols, dedup_branch_rows, generate_branch_trace, + }; + use crate::tables::types::{BusId, FE}; + + /// Presence: μ is IS_HALF-checked weighted by itself. + #[test] + fn branch_bounds_its_multiplicity() { + use stark::lookup::{BusValue, Multiplicity, Packing}; + assert!( + bus_interactions().iter().any(|i| i.is_sender + && i.bus_id == BusId::IsHalfword as u64 + && matches!(i.multiplicity, Multiplicity::Column(m) if m == cols::MU) + && matches!(i.values.as_slice(), + [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == cols::MU)), + "BRANCH must IS_HALF-check μ weighted by itself" + ); + } + + /// Splitting: a count above `MU_MAX` spreads over rows within the bound that + /// preserve the total; exactly `MU_MAX` still fits one row. + #[test] + fn dedup_branch_rows_splits_counts_above_mu_max() { + let op = BranchOperation::new(1 << 48, 0, 0, false); + let ops: Vec<_> = std::iter::repeat_n(op.clone(), 2 * MU_MAX as usize + 7).collect(); + let mut rows: Vec = dedup_branch_rows(&ops).iter().map(|(_, mu)| *mu).collect(); + rows.sort(); + assert_eq!(rows, vec![7, MU_MAX, MU_MAX]); + + let ops: Vec<_> = std::iter::repeat_n(op, MU_MAX as usize).collect(); + assert_eq!(dedup_branch_rows(&ops).len(), 1); + assert!(dedup_branch_rows(&[]).is_empty()); + + // The generated trace never holds a μ above the bound. + let ops: Vec<_> = std::iter::repeat_n( + BranchOperation::new(1 << 48, 0, 0, false), + MU_MAX as usize + 1, + ) + .collect(); + let trace = generate_branch_trace(&ops); + let mut total = 0u64; + for r in 0..trace.num_rows() { + let mu = trace.get_main(r, cols::MU).to_raw(); + assert!(mu <= MU_MAX); + total += mu; + } + assert_eq!(total, ops.len() as u64); + } + + /// Consistency: the BITWISE collector tallies exactly the IS_HALF[μ] lookups + /// the generated BRANCH instances send (each row's μ, weighted by μ; padding + /// nothing), across small instances and for a row split by `MU_MAX`. + #[test] + fn branch_mu_bound_lookups_match_collector() { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::trace_builder::collect_bitwise_from_branch; + use std::collections::HashMap; + + let half = |h: u64| ((h & 0xFF) as u8, ((h >> 8) & 0xFF) as u8); + let distinct = [ + BranchOperation::new(1 << 48, 0, 0, false), + BranchOperation::new(0x1234_5678, 0x100, 0, false), + BranchOperation::new(0, 0, 0x20, true), + ]; + let small: Vec<_> = distinct.iter().cycle().take(11).cloned().collect(); + let split: Vec<_> = std::iter::repeat_n(distinct[0].clone(), MU_MAX as usize + 2) + .chain(distinct.iter().cloned()) + .collect(); + + for (ops, chunk) in [(small, 4usize), (split, 1 << 20)] { + let collected = collect_bitwise_from_branch(&ops, chunk); + + // IS_HALF minus the per-raw-op next_pc_high range checks leaves the μ bound. + let mut is_half: HashMap<(u8, u8), i64> = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::IsHalf) + { + *is_half.entry((b.x, b.y)).or_default() += 1; + } + for op in &ops { + let next_pc = op.compute_next_pc(); + for shift in [16, 32, 48] { + *is_half.entry(half(next_pc >> shift & 0xFFFF)).or_default() -= 1; + } + } + + let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + for c in ops.chunks(chunk) { + let t = generate_branch_trace(c); + for r in 0..t.num_rows() { + let mu = t.get_main(r, cols::MU).to_raw(); + *expected.entry(half(mu)).or_default() += mu as i64; + } + } + is_half.retain(|_, n| *n != 0); + expected.retain(|_, n| *n != 0); + assert_eq!( + is_half, expected, + "IS_HALF[μ] tally must match the trace rows" + ); + } + } +} diff --git a/prover/src/tests/branch_multiplicity_poc.rs b/prover/src/tests/branch_multiplicity_poc.rs new file mode 100644 index 000000000..8357c80af --- /dev/null +++ b/prover/src/tests/branch_multiplicity_poc.rs @@ -0,0 +1,246 @@ +//! BRANCH's `μ` must be a bounded, non-negative multiplicity — same bug and fix +//! as LT (`lt_multiplicity_poc`). +//! +//! BRANCH weights its BRANCH receive and all range lookups (ARE_BYTES, +//! BYTE_ALU[AND], IS_HALFWORD ×3) by one free `μ`. A `μ = −1` twin of an honest +//! row cancels it on the BRANCH bus while *receiving* its range lookups; split +//! the high word non-canonically (`high_1 = 2^16, high_2 -= 1`, same packed +//! `next_pc`) and the twin absorbs an out-of-range `IS_HALFWORD[2^16]` sent by +//! another table. The fix range-checks `μ` (`IS_HALF[μ]`, weighted by μ), so the +//! twin's `μ = −1` itself lands at `p−1` with no receiver. +//! +//! Real BRANCH AIR + real bus balance; the surrounding tables are faithful mocks +//! built from BRANCH's own interactions (CPU sends what BRANCH receives; the +//! range buses receive what BRANCH sends, in-range only). A VICTIM mock sends an +//! out-of-range `IS_HALFWORD` value. + +use std::collections::HashMap; + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use math::field::element::FieldElement; +use stark::constraints::builder::EmptyConstraints; +use stark::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, + NullBoundaryConstraintBuilder, Packing, +}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; +use stark::traits::AIR; +use stark::verifier::{IsStarkVerifier, Verifier}; + +use crate::tables::branch::{BranchOperation, bus_interactions, cols, generate_branch_trace}; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; +use crate::test_utils::{create_branch_air, multi_prove_ram}; + +type F = GoldilocksField; +type E = GoldilocksExtension; +type MockAir = AirWithBuses; +type Row = Vec; + +const HALF: u64 = 1 << 16; + +fn eval_mult(m: &Multiplicity, g: &dyn Fn(usize) -> FE) -> FE { + match m { + Multiplicity::One => FE::one(), + Multiplicity::Column(c) => g(*c), + Multiplicity::Sum(a, b) => g(*a) + g(*b), + Multiplicity::Negated(c) => FE::one() - g(*c), + Multiplicity::Diff(a, b) => g(*a) - g(*b), + Multiplicity::Sum3(a, b, c) => g(*a) + g(*b) + g(*c), + Multiplicity::Linear(ts) => ts.iter().fold(FE::zero(), |acc, t| match *t { + LinearTerm::Column { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::ColumnUnsigned { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::Constant(v) => acc + FE::from(v), + }), + } +} + +/// Net sends per `(bus, tuple)` of BRANCH's real interactions over `rows`. +fn branch_net(rows: &[Row]) -> HashMap<(u64, Vec), FE> { + let mut net: HashMap<(u64, Vec), FE> = HashMap::new(); + for bi in bus_interactions() { + for row in rows { + let g = |c: usize| row[c]; + let m = eval_mult(&bi.multiplicity, &g); + if m == FE::zero() { + continue; + } + let tuple = bi + .values + .iter() + .flat_map(|v| v.combine_from(g)) + .map(|x: FE| x.canonical_u64()) + .collect(); + let e = net.entry((bi.bus_id, tuple)).or_insert(FE::zero()); + *e = if bi.is_sender { *e + m } else { *e - m }; + } + } + net +} + +fn mock(opts: &ProofOptions, bus: u64, n: usize, sender: bool) -> MockAir { + let values = (0..n) + .map(|c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }) + .collect(); + let i = if sender { + BusInteraction::sender(bus, Multiplicity::Column(n), values) + } else { + BusInteraction::receiver(bus, Multiplicity::Column(n), values) + }; + AirWithBuses::new( + n + 1, + AuxiliaryTraceBuildData { + interactions: vec![i], + }, + opts, + 1, + EmptyConstraints, + ) +} + +fn mock_trace(rows: &[(Vec, FE)], n: usize) -> TraceTable { + let len = rows.len().next_power_of_two().max(4); + let mut data = vec![FE::zero(); len * (n + 1)]; + for (r, (tuple, m)) in rows.iter().enumerate() { + for (c, v) in tuple.iter().enumerate() { + data[r * (n + 1) + c] = FE::from(*v); + } + data[r * (n + 1) + n] = *m; + } + TraceTable::new_main(data, n + 1, 1) +} + +/// An honest BRANCH row whose `next_pc = 2^48` (so `high_1 = 0, high_2 = 1`). +fn honest_row() -> Row { + let t = generate_branch_trace(&[BranchOperation::new(1 << 48, 0, 0, false)]); + let row = t.main_table.get_row(0).to_vec(); + assert_eq!(row[cols::MU], FE::one()); + assert_eq!(row[cols::NEXT_PC_HIGH_1], FE::zero()); + assert_eq!(row[cols::NEXT_PC_HIGH_2], FE::one()); + row +} + +/// A `μ = −1` copy of the honest row with the high word split non-canonically +/// (`high_1 = 2^16, high_2 = 0`): same packed `next_pc`, so BRANCH and its +/// constraints agree, but `high_1` is out of range. +fn twin_row() -> Row { + let mut row = honest_row(); + row[cols::MU] = -FE::one(); + row[cols::NEXT_PC_HIGH_1] = FE::from(HALF); + row[cols::NEXT_PC_HIGH_2] = FE::zero(); + row +} + +/// Proves CPU + BRANCH + range-bus mocks (+ VICTIM) and returns whether it +/// verifies. `victim` sends one out-of-range `IS_HALFWORD` value. +fn prove_and_verify(rows: &[Row], victim: Option) -> bool { + let opts = ProofOptions::default_test_options(); + let branch_id: u64 = BusId::Branch.into(); + let half_id: u64 = BusId::IsHalfword.into(); + let widths: HashMap = [ + (branch_id, 9usize), + (BusId::AreBytes.into(), 2), + (BusId::ByteAlu.into(), 4), + (half_id, 1), + ] + .into_iter() + .collect(); + + let mut net = branch_net(rows); + if let Some(v) = victim { + *net.entry((half_id, vec![v])).or_insert(FE::zero()) += FE::one(); + } + + // One mock per bus. BRANCH is received by the chip, so the CPU mock sends it; + // the range buses are sent by the chip, so their mocks receive. Out-of-range + // IS_HALFWORD values get no receiver row (only the victim/μ bound reach them). + let mut per_bus: HashMap, FE)>> = HashMap::new(); + for ((bus, tuple), m) in &net { + if *m == FE::zero() { + continue; + } + if *bus == half_id && tuple[0] >= HALF { + continue; + } + per_bus.entry(*bus).or_default().push((tuple.clone(), *m)); + } + + let mut airs: Vec = Vec::new(); + let mut traces: Vec> = Vec::new(); + let mut is_sender: Vec = Vec::new(); + for (&bus, rows) in &per_bus { + let n = widths[&bus]; + let sender = bus == branch_id; // CPU sends BRANCH lookups; others receive. + // BRANCH net is negative (chip receives); the sender supplies −net. + let rows: Vec<(Vec, FE)> = rows + .iter() + .map(|(t, m)| (t.clone(), if sender { -*m } else { *m })) + .collect(); + airs.push(mock(&opts, bus, n, sender)); + traces.push(mock_trace(&rows, n)); + is_sender.push(sender); + } + let _ = is_sender; + if let Some(v) = victim { + airs.push(mock(&opts, half_id, 1, true)); + traces.push(mock_trace(&[(vec![v], FE::one())], 1)); + } + + let branch_len = rows.len().next_power_of_two().max(4); + let mut branch_data = vec![FE::zero(); branch_len * cols::NUM_COLUMNS]; + for (r, row) in rows.iter().enumerate() { + branch_data[r * cols::NUM_COLUMNS..(r + 1) * cols::NUM_COLUMNS].copy_from_slice(row); + } + let mut branch_trace = TraceTable::new_main(branch_data, cols::NUM_COLUMNS, 1); + let branch_air = create_branch_air(&opts); + + let mut pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![(&branch_air, &mut branch_trace, &())]; + for (a, t) in airs.iter().zip(traces.iter_mut()) { + pairs.push((a, t, &())); + } + let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + + let mut air_refs: Vec<&dyn AIR> = + vec![&branch_air]; + for a in &airs { + air_refs.push(a); + } + Verifier::multi_verify( + &air_refs, + &proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ) +} + +/// Positive control: an honest BRANCH row answering the CPU verifies. +#[test] +fn control_honest_row_verifies() { + assert!(prove_and_verify(&[honest_row()], None)); +} + +/// Control: an out-of-range IS_HALFWORD send with no twin has no receiver. +#[test] +fn control_out_of_range_victim_is_rejected() { + assert!(!prove_and_verify(&[honest_row()], Some(HALF))); +} + +/// Regression: the `μ = −1` twin can no longer absorb the victim's +/// IS_HALFWORD[2^16] (accepted before BRANCH's μ was bounded). +#[test] +fn regression_negative_mu_twin_cannot_absorb_victim() { + assert!(!prove_and_verify(&[honest_row(), twin_row()], Some(HALF))); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 11051e08e..9df45c683 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -9,6 +9,8 @@ pub mod branch_bus_tests; #[cfg(test)] pub mod branch_constraints_tests; #[cfg(test)] +pub mod branch_multiplicity_poc; +#[cfg(test)] pub mod bytewise_tests; #[cfg(test)] pub mod commit_tests; @@ -69,6 +71,8 @@ pub mod memw_register_tests; #[cfg(test)] pub mod memw_tests; #[cfg(test)] +pub mod mul_mu_carrier_poc; +#[cfg(test)] pub mod mul_tests; #[cfg(test)] pub mod multiplicity_forgery_poc; diff --git a/prover/src/tests/mul_mu_carrier_poc.rs b/prover/src/tests/mul_mu_carrier_poc.rs new file mode 100644 index 000000000..e3e9ae42f --- /dev/null +++ b/prover/src/tests/mul_mu_carrier_poc.rs @@ -0,0 +1,270 @@ +//! Adversarial check of the MUL `μ` bound (`fix/multiplicity-soundness`). +//! +//! The fix bounds `μ_lo`/`μ_hi` with `IS_HALF[μ]` weighted *by μ itself* +//! (`Multiplicity::Column`), because the skip-empty-tables invariant (#977) +//! forbids a constant `Multiplicity::One` on an optional table. The open +//! question (raised reviewing BRANCH): does weighting by μ leave a hole that +//! `One` would not? A malicious `μ_hi = −1` row's bound send lands at value +//! `p−1` with weight `p−1 = −1`; the proof then balances iff *something else* +//! supplies `+1` at `p−1` on the IS_HALFWORD bus. +//! +//! This test pins down exactly that, with the real fixed MUL AIR and real bus +//! balance. Every surrounding table is a faithful mock built by evaluating +//! MUL's own interactions: the CPU sends what MUL receives on ALU; RANGE / +//! RANGE20 receive what MUL sends to IS_HALFWORD / IS_B20, but *only for values +//! a real range table has a row for* (`< 2^16` / `< 2^20`). A `CARRIER` mock +//! optionally sends `IS_HALFWORD[p−1]`, standing in for "some other table emits +//! an out-of-range halfword with +1". +//! +//! Result characterises the fix: +//! - no carrier → the `μ_hi = −1` forgery is REJECTED (the known attack is +//! blocked; same as `multiplicity_forgery_poc`); +//! - with carrier → whether it verifies says whether the bound is unconditional +//! or only holds while no table leaks an out-of-range halfword. + +use std::collections::HashMap; + +use crypto::fiat_shamir::default_transcript::DefaultTranscript; +use math::field::element::FieldElement; +use stark::constraints::builder::EmptyConstraints; +use stark::lookup::{ + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, Multiplicity, + NullBoundaryConstraintBuilder, Packing, +}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; +use stark::traits::AIR; +use stark::verifier::{IsStarkVerifier, Verifier}; + +use crate::tables::mul::{MulOperation, bus_interactions, cols, generate_mul_trace}; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; +use crate::test_utils::{create_mul_air, multi_prove_ram}; + +type F = GoldilocksField; +type E = GoldilocksExtension; +type MockAir = AirWithBuses; + +const HALF: u64 = 1 << 16; +const B20: u64 = 1 << 20; +/// `p − 1`, i.e. the field value of `−1` — where a `μ = −1` bound send lands. +fn minus_one() -> u64 { + (-FE::one()).canonical_u64() +} + +fn eval_mult(m: &Multiplicity, g: &dyn Fn(usize) -> FE) -> FE { + use stark::lookup::LinearTerm; + match m { + Multiplicity::One => FE::one(), + Multiplicity::Column(c) => g(*c), + Multiplicity::Sum(a, b) => g(*a) + g(*b), + Multiplicity::Negated(c) => FE::one() - g(*c), + Multiplicity::Diff(a, b) => g(*a) - g(*b), + Multiplicity::Sum3(a, b, c) => g(*a) + g(*b) + g(*c), + Multiplicity::Linear(ts) => ts.iter().fold(FE::zero(), |acc, t| match *t { + LinearTerm::Column { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::ColumnUnsigned { + coefficient, + column, + } => acc + g(column) * FE::from(coefficient), + LinearTerm::Constant(v) => acc + FE::from(v), + }), + } +} + +/// Net sends per `(bus, tuple)` of MUL's real interactions over `rows`. +fn mul_net(rows: &[Vec]) -> HashMap<(u64, Vec), FE> { + let mut net: HashMap<(u64, Vec), FE> = HashMap::new(); + for bi in bus_interactions() { + for row in rows { + let g = |c: usize| row[c]; + let m = eval_mult(&bi.multiplicity, &g); + if m == FE::zero() { + continue; + } + let tuple = bi + .values + .iter() + .flat_map(|v| v.combine_from(g)) + .map(|x: FE| x.canonical_u64()) + .collect(); + let e = net.entry((bi.bus_id, tuple)).or_insert(FE::zero()); + *e = if bi.is_sender { *e + m } else { *e - m }; + } + } + net +} + +fn mock(opts: &ProofOptions, bus: BusId, n: usize, sender: bool) -> MockAir { + let values = (0..n) + .map(|c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }) + .collect(); + let i = if sender { + BusInteraction::sender(bus, Multiplicity::Column(n), values) + } else { + BusInteraction::receiver(bus, Multiplicity::Column(n), values) + }; + AirWithBuses::new( + n + 1, + AuxiliaryTraceBuildData { + interactions: vec![i], + }, + opts, + 1, + EmptyConstraints, + ) +} + +fn mock_trace(rows: &[(Vec, FE)], n: usize) -> TraceTable { + let len = rows.len().next_power_of_two().max(4); + let mut data = vec![FE::zero(); len * (n + 1)]; + for (r, (tuple, m)) in rows.iter().enumerate() { + for (c, v) in tuple.iter().enumerate() { + data[r * (n + 1) + c] = FE::from(*v); + } + data[r * (n + 1) + n] = *m; + } + TraceTable::new_main(data, n + 1, 1) +} + +/// Forged MUL rows for `3 * 5 = 99`: row A (`μ_lo = 1, μ_hi = −1`, `lo` forged) +/// plus its honest `μ_lo = 0, μ_hi = 1` copy cancelling A on ALU-hi. +fn forged_mul_rows() -> Vec> { + let honest = generate_mul_trace(&[(MulOperation::new(3, false, 5, false), false)]); + let a = honest.main_table.get_row(0).to_vec(); + assert_eq!(a[cols::MU_LO], FE::one()); + assert_eq!(a[cols::MU_HI], FE::zero()); + assert_eq!(a[cols::LO_0], FE::from(15u64)); + + let mut forged = a.clone(); + forged[cols::LO_0] = FE::from(99u64); + forged[cols::MU_HI] = -FE::one(); + + let mut copy = a.clone(); + copy[cols::MU_LO] = FE::zero(); + copy[cols::MU_HI] = FE::one(); + vec![forged, copy] +} + +/// Proves CPU + MUL + RANGE(+RANGE20)(+CARRIER) and returns whether it verifies. +/// +/// RANGE/RANGE20 receive MUL's IS_HALFWORD/IS_B20 demand only for values a real +/// table has a row for; `extra_half` lets a carrier send one out-of-range value. +fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { + let opts = ProofOptions::default_test_options(); + let alu: u64 = BusId::Alu.into(); + let half: u64 = BusId::IsHalfword.into(); + let b20: u64 = BusId::IsB20.into(); + + let net = mul_net(rows); + let mut cpu = Vec::new(); + let mut range = Vec::new(); + let mut range20 = Vec::new(); + for ((bus, tuple), m) in &net { + if *m == FE::zero() { + continue; + } + if *bus == alu { + // MUL receives on ALU (net < 0); the CPU sends −net. + cpu.push((tuple.clone(), -*m)); + } else if *bus == half { + // MUL sends to IS_HALFWORD; RANGE receives it, if it is a halfword. + if tuple[0] < HALF { + range.push((tuple.clone(), *m)); + } + } else if *bus == b20 { + if tuple[0] < B20 { + range20.push((tuple.clone(), *m)); + } + } + } + let mut carrier = Vec::new(); + if let Some(v) = extra_half { + carrier.push((vec![v], FE::one())); + } + + let mul_len = rows.len().next_power_of_two().max(4); + let mut mul_data = vec![FE::zero(); mul_len * cols::NUM_COLUMNS]; + for (r, row) in rows.iter().enumerate() { + mul_data[r * cols::NUM_COLUMNS..(r + 1) * cols::NUM_COLUMNS].copy_from_slice(row); + } + let mut mul_trace = TraceTable::new_main(mul_data, cols::NUM_COLUMNS, 1); + let mut cpu_trace = mock_trace(&cpu, 7); + let mut range_trace = mock_trace(&range, 1); + let mut range20_trace = mock_trace(&range20, 1); + let mut carrier_trace = mock_trace(&carrier, 1); + + let mul_air = create_mul_air(&opts); + let cpu_air = mock(&opts, BusId::Alu, 7, true); + let range_air = mock(&opts, BusId::IsHalfword, 1, false); + let range20_air = mock(&opts, BusId::IsB20, 1, false); + let carrier_air = mock(&opts, BusId::IsHalfword, 1, true); + + let pairs: Vec<( + &dyn AIR, + _, + _, + )> = vec![ + (&cpu_air, &mut cpu_trace, &()), + (&mul_air, &mut mul_trace, &()), + (&range_air, &mut range_trace, &()), + (&range20_air, &mut range20_trace, &()), + (&carrier_air, &mut carrier_trace, &()), + ]; + let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + let airs: Vec<&dyn AIR> = + vec![&cpu_air, &mul_air, &range_air, &range20_air, &carrier_air]; + Verifier::multi_verify( + &airs, + &proof, + &mut DefaultTranscript::::new(&[]), + &FieldElement::zero(), + ) +} + +/// Positive control: honest `3 * 5 = 15` answering the CPU verifies. +#[test] +fn control_honest_mul_verifies() { + let honest = generate_mul_trace(&[(MulOperation::new(3, false, 5, false), false)]); + let row = honest.main_table.get_row(0).to_vec(); + assert!(prove_and_verify(&[row], None)); +} + +/// The forgery leaves exactly a `−1` at value `p−1` on IS_HALFWORD, and nowhere +/// else out of range — so a single carrier `+1` at `p−1` is all it would need. +#[test] +fn forgery_leaves_only_minus_one_at_p_minus_1() { + let half: u64 = BusId::IsHalfword.into(); + let net = mul_net(&forged_mul_rows()); + for ((bus, tuple), m) in &net { + if *bus == half && tuple[0] >= HALF && *m != FE::zero() { + assert_eq!(tuple[0], minus_one()); + assert_eq!(*m, -FE::one()); + } + } +} + +/// Known attack, no carrier: rejected (matches `multiplicity_forgery_poc`). +#[test] +fn forgery_without_carrier_is_rejected() { + assert!(!prove_and_verify(&forged_mul_rows(), None)); +} + +/// The decisive case: does a carrier that supplies `+1` at `p−1` let the +/// `μ_hi = −1` product forgery through the weighted-by-μ bound? +#[test] +fn forgery_with_carrier_at_p_minus_1() { + let verified = prove_and_verify(&forged_mul_rows(), Some(minus_one())); + // Asserting the observed behaviour so the harness is not vacuous; the point + // of the test is the printed verdict, interpreted in the module docs. + println!("MUL forgery with p-1 carrier verified = {verified}"); + assert!( + verified, + "if this fails the weighted-by-μ bound resisted the carrier" + ); +} From 4dd1ee5ebd6a665602774b26bb39c141b579ab8b Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 5 Oct 2026 15:29:10 -0300 Subject: [PATCH 05/13] Fix clippy lints in tests --- prover/src/tests/branch_bus_tests.rs | 2 +- prover/src/tests/mul_mu_carrier_poc.rs | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/prover/src/tests/branch_bus_tests.rs b/prover/src/tests/branch_bus_tests.rs index 710554155..2195009e0 100644 --- a/prover/src/tests/branch_bus_tests.rs +++ b/prover/src/tests/branch_bus_tests.rs @@ -701,7 +701,7 @@ mod mu_bound { use crate::tables::branch::{ MU_MAX, bus_interactions, cols, dedup_branch_rows, generate_branch_trace, }; - use crate::tables::types::{BusId, FE}; + use crate::tables::types::BusId; /// Presence: μ is IS_HALF-checked weighted by itself. #[test] diff --git a/prover/src/tests/mul_mu_carrier_poc.rs b/prover/src/tests/mul_mu_carrier_poc.rs index e3e9ae42f..409bb9f8f 100644 --- a/prover/src/tests/mul_mu_carrier_poc.rs +++ b/prover/src/tests/mul_mu_carrier_poc.rs @@ -177,10 +177,8 @@ fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { if tuple[0] < HALF { range.push((tuple.clone(), *m)); } - } else if *bus == b20 { - if tuple[0] < B20 { - range20.push((tuple.clone(), *m)); - } + } else if *bus == b20 && tuple[0] < B20 { + range20.push((tuple.clone(), *m)); } } let mut carrier = Vec::new(); From 6eea7c25b365e6ef83e852eaffd0ffe3386afde7 Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 6 Oct 2026 13:33:27 -0300 Subject: [PATCH 06/13] Bound table multiplicities with IS_BYTE instead of IS_HALFWORD --- prover/src/tables/branch.rs | 25 +++---- prover/src/tables/dvrm.rs | 26 ++++---- prover/src/tables/lt.rs | 26 ++++---- prover/src/tables/mul.rs | 27 ++++---- prover/src/tables/trace_builder.rs | 48 ++++---------- prover/src/tests/branch_bus_tests.rs | 40 ++++++++--- prover/src/tests/branch_multiplicity_poc.rs | 5 ++ prover/src/tests/dvrm_tests.rs | 34 +++++++--- prover/src/tests/lt_multiplicity_poc.rs | 73 ++++++++++++++++++++- prover/src/tests/lt_tests.rs | 34 +++++++--- prover/src/tests/mul_mu_carrier_poc.rs | 56 +++++++++++----- prover/src/tests/mul_tests.rs | 34 +++++++--- 12 files changed, 294 insertions(+), 134 deletions(-) diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 0847d6b8f..243f84925 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -150,12 +150,12 @@ impl BranchOperation { } } -/// Largest per-row multiplicity: `μ` is range-checked to a halfword -/// (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many lookups. The +/// Largest per-row multiplicity: `μ` is range-checked to a byte +/// (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many lookups. The /// bound keeps μ non-negative: without it a `μ = −1` twin of an honest row /// cancels it on the BRANCH bus while *receiving* its range lookups, absorbing /// another row's out-of-range limb (same bug as LT). -pub const MU_MAX: u64 = (1 << 16) - 1; +pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates BRANCH operations into trace rows: `(pc, offset, register, /// jalr) -> μ`, splitting an op over several rows when its count exceeds @@ -246,7 +246,7 @@ pub fn generate_branch_trace( /// - **Sends** BYTE_ALU[AND] lookup for LSB masking /// (next_pc_low[0] = unmasked_low_byte & 254) /// - **Sends** IS_HALFWORD lookups for next_pc_high[0..3] range checks and for -/// the μ multiplicity bound +/// (next_pc_high limbs); ARE_BYTES for the μ multiplicity bound /// - **Receives** BRANCH lookups from CPU table pub fn bus_interactions() -> Vec { vec![ @@ -307,20 +307,23 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // IS_HALF[μ] | μ. Every lookup here fires with μ, so μ itself must be + // ARE_BYTES[μ, 0] | μ. Every lookup here fires with μ, so μ itself must be // bounded and non-negative. Otherwise a μ = −1 twin of an honest row // cancels it on the BRANCH bus while *receiving* its range lookups and // absorbs an out-of-range IS_HALFWORD sent by any row (same as LT). Sent // with itself as multiplicity: `k` rows holding an out-of-range `v` put - // weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // weight `k·v ≠ 0` on a byte tuple ARE_BYTES has no row for, while padding // (μ = 0) contributes nothing. See `MU_MAX`. BusInteraction::sender( - BusId::IsHalfword, + BusId::AreBytes, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::MU, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::MU, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], ), // BRANCH[next_pc; pc, offset, register, JALR] (receiver) // Signature: [next_pc (DWordWL), pc (DWordWL), offset (DWordWL), register (DWordWL), JALR (Bit)] diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index b388e78cd..ee9c75451 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -22,7 +22,8 @@ //! - `sign_n`, `sign_d`, `sign_q`, `sign_r`: Bit - sign bits //! //! ## Bus Interactions -//! - Sender: IS_HALF (×20: n, d, r, n_sub_r, q; ×2: μ_q, μ_r bounds) +//! - Sender: IS_HALF (×20: n, d, r, n_sub_r, q) +//! - Sender: ARE_BYTES (×2: μ_q, μ_r bounds) //! - Sender: MSB16 (×3 for sign extraction: n, d, r) //! - Sender: ALU (×3, on the unified bus: ×1 LT-flavored for `|r| < |d|`, //! ×2 MUL-flavored for `n - r = d * q` lo/hi) @@ -274,11 +275,11 @@ impl DvrmOperation { // ========================================================================= /// Largest per-row multiplicity: `μ_q` and `μ_r` are each range-checked to a -/// halfword (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many +/// byte (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many /// lookups of each kind. The bound is what makes `μ_q + μ_r = 0` imply /// `μ_q = μ_r = 0`: without it a `μ_q = 1, μ_r = −1` row receives a quotient /// lookup while sending none of its checks (forged `n = q·d + r`). -pub const MU_MAX: u64 = (1 << 16) - 1; +pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates DVRM operations into trace rows: `(n, d, signed) -> (μ_q, μ_r)`, /// splitting an op over several rows when a count exceeds [`MU_MAX`]. Shared by @@ -384,7 +385,7 @@ pub fn generate_dvrm_trace( /// /// The DVRM table: /// - **Sends** IS_HALF lookups for n, d, q, r, n_sub_r range checks (×20) -/// and for the μ_q/μ_r multiplicity bounds (×2) +/// - **Sends** ARE_BYTES[μ_q, 0] and ARE_BYTES[μ_r, 0] to bound the multiplicities /// - **Sends** MSB16 lookups for sign extraction (×3: n, d, r) /// - **Sends** LT lookup for |r| < |d| (×1) /// - **Sends** MUL lookups for n_sub_r = d * q verification (×2: lo and hi) @@ -394,24 +395,27 @@ pub fn bus_interactions() -> Vec { let mut interactions = Vec::new(); // ------------------------------------------------------------------------- - // IS_HALF[μ_q] | μ_q, IS_HALF[μ_r] | μ_r. + // ARE_BYTES[μ_q, 0] | μ_q, ARE_BYTES[μ_r, 0] | μ_r. // Every check below fires with μ_q + μ_r, so the multiplicities themselves // must be bounded and non-negative. Otherwise μ_q = 1, μ_r = −1 receives a // quotient lookup with all checks off (forged quotient), // and an honest μ_r = 1 copy of the row cancels the stray −1. Each μ is sent // with itself as multiplicity: `k` rows holding an out-of-range value `v` - // put weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // put weight `k·v ≠ 0` on a byte tuple ARE_BYTES has no row for, while padding // (μ = 0) contributes nothing, so an empty instance still matches an absent // one. See `MU_MAX`. // ------------------------------------------------------------------------- for col in [cols::MU_Q, cols::MU_R] { interactions.push(BusInteraction::sender( - BusId::IsHalfword, + BusId::AreBytes, Multiplicity::Column(col), - vec![BusValue::Packed { - start_column: col, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], )); } diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index 0ea208ec2..b7f3d2710 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -23,7 +23,8 @@ //! ## Bus Interactions //! - Sender: MSB16 (×2 for lhs_msb, rhs_msb) //! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]; -//! ×1 for the μ multiplicity bound) +//! ) +//! - Sender: ARE_BYTES (×1 for the μ multiplicity bound) //! - Receiver: ALU (all less-than lookups — CPU SLT/BLT/BGE dispatch and the //! internal `memw`/`memw_aligned`/`dvrm` timestamp / |r|<|d| checks) @@ -153,12 +154,12 @@ impl LtOperation { } } -/// Largest per-row multiplicity: `μ` is range-checked to a halfword -/// (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many lookups. The +/// Largest per-row multiplicity: `μ` is range-checked to a byte +/// (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many lookups. The /// bound is what keeps μ non-negative: without it a `μ = −1` twin of an honest /// row cancels it on the ALU bus while *receiving* its range lookups, which /// absorbs another row's out-of-range limb (a forged `5 < 3 = 1` verified). -pub const MU_MAX: u64 = (1 << 16) - 1; +pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates LT operations into trace rows: `(lhs, rhs, signed, invert) -> μ`, /// splitting an op over several rows when its count exceeds [`MU_MAX`]. Shared @@ -330,21 +331,24 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // IS_HALF[μ] | μ. Every lookup here fires with μ, so μ itself must be + // ARE_BYTES[μ, 0] | μ. Every lookup here fires with μ, so μ itself must be // bounded and non-negative. Otherwise a μ = −1 twin of an honest row // cancels it on the ALU bus while *receiving* its range lookups, with // `sub_0` free up to 2^32: it absorbs an out-of-range IS_HALFWORD sent // by any row, another LT row included (forged `5 < 3 = 1`). Sent with // itself as multiplicity: `k` rows holding an out-of-range `v` put - // weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // weight `k·v ≠ 0` on a byte tuple ARE_BYTES has no row for, while padding // (μ = 0) contributes nothing. See `MU_MAX`. BusInteraction::sender( - BusId::IsHalfword, + BusId::AreBytes, Multiplicity::Column(cols::MU), - vec![BusValue::Packed { - start_column: cols::MU, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: cols::MU, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], ), // ALU[lhs, rhs, opsel(LT) + 32*signed + 64*invert] -> out (receiver). // Every LT lookup arrives here: the CPU dispatches SLT/BLT/BGE on the diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index b9b2576f5..08863abb5 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -25,8 +25,8 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for sign extraction) -//! - Sender: IS_HALF (×16 for lhs/rhs input and lo/hi output range checks, -//! ×2 for the μ_lo/μ_hi multiplicity bounds) +//! - Sender: IS_HALF (×16 for lhs/rhs input and lo/hi output range checks) +//! - Sender: ARE_BYTES (×2 for the μ_lo/μ_hi multiplicity bounds) //! - Sender: IS_B20 (×4 for carry range checks) //! - Receiver: ALU (×2 for lo and hi results — every MUL lookup, CPU //! MUL/MULH dispatch and dvrm's internal `d*q` consistency) @@ -283,11 +283,11 @@ impl MulOperation { // ========================================================================= /// Largest per-row multiplicity: `μ_lo` and `μ_hi` are each range-checked to a -/// halfword (`IS_HALF[μ]`, weighted by μ), so a row holds at most this many +/// byte (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many /// lookups of each kind. The bound is what makes `μ_lo + μ_hi = 0` imply /// `μ_lo = μ_hi = 0`: without it a `μ_lo = 1, μ_hi = −1` row receives a lookup /// while sending none of its range checks. -pub const MU_MAX: u64 = (1 << 16) - 1; +pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates MUL operations into trace rows: `(lhs, lhs_signed, rhs, /// rhs_signed) -> (μ_lo, μ_hi)`, splitting an op over several rows when a count @@ -386,7 +386,7 @@ pub fn generate_mul_trace( /// The MUL table: /// - **Sends** MSB16 lookups for sign bit extraction (×2) /// - **Sends** IS_HALF lookups for lhs/rhs input and lo/hi output range checks (×16) -/// and for the μ_lo/μ_hi multiplicity bounds (×2) +/// - **Sends** ARE_BYTES[μ_lo, 0] and ARE_BYTES[μ_hi, 0] to bound the multiplicities /// - **Sends** IS_B20 lookups for carry range checks (×4) /// - **Receives** MUL lookups from CPU table (×2: lo and hi) pub fn bus_interactions() -> Vec { @@ -428,24 +428,27 @@ pub fn bus_interactions() -> Vec { )); // ------------------------------------------------------------------------- - // IS_HALF[μ_lo] | μ_lo, IS_HALF[μ_hi] | μ_hi. + // ARE_BYTES[μ_lo, 0] | μ_lo, ARE_BYTES[μ_hi, 0] | μ_hi. // Every check below fires with μ_lo + μ_hi, so the multiplicities themselves // must be bounded and non-negative. Otherwise μ_lo = 1, μ_hi = −1 receives a // `lo` lookup with all range checks off (forged product), // and an honest μ_hi = 1 copy of the row cancels the stray −1. Each μ is sent // with itself as multiplicity: `k` rows holding an out-of-range value `v` - // put weight `k·v ≠ 0` on a tuple IS_HALF has no row for, while padding + // put weight `k·v ≠ 0` on a byte tuple ARE_BYTES has no row for, while padding // (μ = 0) contributes nothing, so an empty instance still matches an absent // one. See `MU_MAX`. // ------------------------------------------------------------------------- for col in [cols::MU_LO, cols::MU_HI] { interactions.push(BusInteraction::sender( - BusId::IsHalfword, + BusId::AreBytes, Multiplicity::Column(col), - vec![BusValue::Packed { - start_column: col, - packing: Packing::Direct, - }], + vec![ + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], )); } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index e56e68a0a..5ecbf57ef 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1732,15 +1732,11 @@ pub(crate) fn collect_bitwise_from_lt( )); } - // IS_HALF[μ] | μ: each row sends its own μ, μ times (padding sends nothing), + // IS_BYTE[μ] | μ: each row sends its own μ, μ times (padding sends nothing), // over exactly the rows `generate_lt_trace` builds for each chunk. for chunk in lt_ops.chunks(max_rows_lt) { for (_, mu) in lt::dedup_lt_rows(chunk) { - let op = BitwiseOperation::halfword( - BitwiseOperationType::IsHalf, - (mu & 0xFF) as u8, - ((mu >> 8) & 0xFF) as u8, - ); + let op = BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, mu as u8); bitwise_ops.extend(std::iter::repeat_n(op, mu as usize)); } } @@ -1755,7 +1751,7 @@ pub(crate) fn collect_bitwise_from_lt( /// and IS_B20 lookups for carry range checks. /// /// IS_HALF and IS_B20 are emitted once per raw op. The per-row lookups (MSB16 -/// and the IS_HALF[μ_lo]/IS_HALF[μ_hi] multiplicity bounds) are counted over the +/// and the IS_BYTE[μ_lo]/IS_BYTE[μ_hi] multiplicity bounds) are counted over the /// rows of each `max_rows_mul` chunk, mirroring `chunk_and_generate_optional` — /// a unique signed op that spans two instances is sent twice and must be tallied /// twice. @@ -1816,21 +1812,15 @@ pub(crate) fn collect_bitwise_from_mul( } // Per-row lookups, over exactly the rows `generate_mul_trace` builds for each - // `max_rows_mul` chunk (`chunk_and_generate_optional`): IS_HALF[μ_lo] and - // IS_HALF[μ_hi] are sent μ_lo / μ_hi times (so padding rows send nothing), and + // `max_rows_mul` chunk (`chunk_and_generate_optional`): IS_BYTE[μ_lo] and + // IS_BYTE[μ_hi] are sent μ_lo / μ_hi times (so padding rows send nothing), and // MSB16 fires once per row whose sign flag is set — a unique signed op spanning two // instances, or split over two rows by `mul::MU_MAX`, is sent once per row. - let halfword = |v: u64| { - BitwiseOperation::halfword( - BitwiseOperationType::IsHalf, - (v & 0xFF) as u8, - ((v >> 8) & 0xFF) as u8, - ) - }; + let mu_byte = |v: u64| BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, v as u8); for chunk in mul_ops.chunks(max_rows_mul) { for (op, mu) in &mul::dedup_mul_rows(chunk) { for m in [mu.mu_lo, mu.mu_hi] { - bitwise_ops.extend(std::iter::repeat_n(halfword(m), m as usize)); + bitwise_ops.extend(std::iter::repeat_n(mu_byte(m), m as usize)); } if op.lhs_signed { let lhs_3 = ((op.lhs >> 48) & 0xFFFF) as u16; @@ -1864,7 +1854,7 @@ pub(crate) fn collect_bitwise_from_mul( /// are collected here alongside the constraint-level ones. /// /// IS_HALF and ZERO (C8/C20) are emitted once per raw op. MSB16, the -/// NEG-template ZERO lookups (C3/C5) and the IS_HALF[μ_q]/IS_HALF[μ_r] +/// NEG-template ZERO lookups (C3/C5) and the IS_BYTE[μ_q]/IS_BYTE[μ_r] /// multiplicity bounds are counted over the rows of each `max_rows_dvrm` chunk, /// mirroring `chunk_and_generate_optional`. /// @@ -1954,22 +1944,16 @@ pub(crate) fn collect_bitwise_from_dvrm( } // Per-row lookups, over exactly the rows `generate_dvrm_trace` builds for each - // `max_rows_dvrm` chunk (`chunk_and_generate_optional`): IS_HALF[μ_q] and - // IS_HALF[μ_r] sent μ_q / μ_r times (padding rows send nothing); MSB16 (Column(SIGNED)) + // `max_rows_dvrm` chunk (`chunk_and_generate_optional`): IS_BYTE[μ_q] and + // IS_BYTE[μ_r] sent μ_q / μ_r times (padding rows send nothing); MSB16 (Column(SIGNED)) // and the NEG-template ZERO lookups (Column(SIGN_R)/Column(SIGN_D)) once per // row whose bit is set. An op split over two rows by `dvrm::MU_MAX` sends // them once per row. - let halfword = |v: u64| { - BitwiseOperation::halfword( - BitwiseOperationType::IsHalf, - (v & 0xFF) as u8, - ((v >> 8) & 0xFF) as u8, - ) - }; + let mu_byte = |v: u64| BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, v as u8); for chunk in dvrm_ops.chunks(max_rows_dvrm) { for (op, mu) in &dvrm::dedup_dvrm_rows(chunk) { for m in [mu.mu_q, mu.mu_r] { - bitwise_ops.extend(std::iter::repeat_n(halfword(m), m as usize)); + bitwise_ops.extend(std::iter::repeat_n(mu_byte(m), m as usize)); } if op.signed { @@ -2100,15 +2084,11 @@ pub(crate) fn collect_bitwise_from_branch( )); } - // IS_HALF[μ] | μ: each row sends its own μ, μ times (padding sends nothing), + // IS_BYTE[μ] | μ: each row sends its own μ, μ times (padding sends nothing), // over exactly the rows `generate_branch_trace` builds for each chunk. for chunk in branch_ops.chunks(max_rows_branch) { for (_, mu) in branch::dedup_branch_rows(chunk) { - let op = BitwiseOperation::halfword( - BitwiseOperationType::IsHalf, - (mu & 0xFF) as u8, - ((mu >> 8) & 0xFF) as u8, - ); + let op = BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, mu as u8); bitwise_ops.extend(std::iter::repeat_n(op, mu as usize)); } } diff --git a/prover/src/tests/branch_bus_tests.rs b/prover/src/tests/branch_bus_tests.rs index 2195009e0..e9d83741d 100644 --- a/prover/src/tests/branch_bus_tests.rs +++ b/prover/src/tests/branch_bus_tests.rs @@ -709,11 +709,11 @@ mod mu_bound { use stark::lookup::{BusValue, Multiplicity, Packing}; assert!( bus_interactions().iter().any(|i| i.is_sender - && i.bus_id == BusId::IsHalfword as u64 + && i.bus_id == BusId::AreBytes as u64 && matches!(i.multiplicity, Multiplicity::Column(m) if m == cols::MU) - && matches!(i.values.as_slice(), - [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == cols::MU)), - "BRANCH must IS_HALF-check μ weighted by itself" + && matches!(i.values.first(), + Some(BusValue::Packed { start_column, packing: Packing::Direct }) if *start_column == cols::MU)), + "BRANCH must IS_BYTE-check μ weighted by itself" ); } @@ -785,19 +785,41 @@ mod mu_bound { } } - let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + // The μ bound moved to ARE_BYTES, so IS_HALF must now be exactly the + // next_pc_high limbs. + is_half.retain(|_, n| *n != 0); + assert!( + is_half.is_empty(), + "IS_HALF must match exactly the next_pc_high range checks" + ); + + // ARE_BYTES carries both the real next_pc_low[1] byte check and the + // μ bound; subtract the former to isolate the latter. + let mut arebytes: HashMap = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::AreBytes) + { + assert_eq!(b.y, 0, "BRANCH ARE_BYTES sends are single bytes"); + *arebytes.entry(b.x).or_default() += 1; + } + for op in &ops { + let next_pc = op.compute_next_pc(); + *arebytes.entry(((next_pc >> 8) & 0xFF) as u8).or_default() -= 1; + } + let mut expected: HashMap = HashMap::new(); for c in ops.chunks(chunk) { let t = generate_branch_trace(c); for r in 0..t.num_rows() { let mu = t.get_main(r, cols::MU).to_raw(); - *expected.entry(half(mu)).or_default() += mu as i64; + *expected.entry(mu as u8).or_default() += mu as i64; } } - is_half.retain(|_, n| *n != 0); + arebytes.retain(|_, n| *n != 0); expected.retain(|_, n| *n != 0); assert_eq!( - is_half, expected, - "IS_HALF[μ] tally must match the trace rows" + arebytes, expected, + "ARE_BYTES[μ] tally must match the trace rows" ); } } diff --git a/prover/src/tests/branch_multiplicity_poc.rs b/prover/src/tests/branch_multiplicity_poc.rs index 8357c80af..ab486219f 100644 --- a/prover/src/tests/branch_multiplicity_poc.rs +++ b/prover/src/tests/branch_multiplicity_poc.rs @@ -168,6 +168,11 @@ fn prove_and_verify(rows: &[Row], victim: Option) -> bool { if *m == FE::zero() { continue; } + // A real byte table has rows only for [0, 256); the μ bound sends + // ARE_BYTES[μ, 0], so an out-of-range μ (p−1) has no receiver. + if *bus == BusId::AreBytes as u64 && tuple[0] >= 256 { + continue; + } if *bus == half_id && tuple[0] >= HALF { continue; } diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index c129f45b6..588b77c55 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -572,11 +572,11 @@ fn test_dvrm_bounds_its_multiplicities() { for col in [cols::MU_Q, cols::MU_R] { assert!( bus_interactions().iter().any(|i| i.is_sender - && i.bus_id == BusId::IsHalfword as u64 + && i.bus_id == BusId::AreBytes as u64 && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) - && matches!(i.values.as_slice(), - [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col)), - "DVRM must IS_HALF-check multiplicity column {col} weighted by itself" + && matches!(i.values.first(), + Some(BusValue::Packed { start_column, packing: Packing::Direct }) if *start_column == col)), + "DVRM must IS_BYTE-check multiplicity column {col} weighted by itself" ); } } @@ -650,25 +650,41 @@ fn test_dvrm_per_row_lookups_match_collector() { } } - let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + // The μ bounds moved to ARE_BYTES, so IS_HALF must now be exactly the limbs. + is_half.retain(|_, n| *n != 0); + assert!( + is_half.is_empty(), + "IS_HALF must match exactly the limb range checks" + ); + + // μ bounds: ARE_BYTES[μ_q, 0] and ARE_BYTES[μ_r, 0], weighted by μ. + let mut arebytes: HashMap = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::AreBytes) + { + assert_eq!(b.y, 0, "μ bounds send ARE_BYTES[μ, 0]"); + *arebytes.entry(b.x).or_default() += 1; + } + let mut expected: HashMap = HashMap::new(); let (mut msb16, mut neg_zero) = (0usize, 0usize); for c in ops.chunks(chunk) { let t = generate_dvrm_trace(c); for r in 0..t.num_rows() { for col in [cols::MU_Q, cols::MU_R] { let mu = t.get_main(r, col).to_raw(); - *expected.entry(half(mu)).or_default() += mu as i64; + *expected.entry(mu as u8).or_default() += mu as i64; } msb16 += 3 * t.get_main(r, cols::SIGNED).to_raw() as usize; neg_zero += 2 * t.get_main(r, cols::SIGN_R).to_raw() as usize; neg_zero += 2 * t.get_main(r, cols::SIGN_D).to_raw() as usize; } } - is_half.retain(|_, n| *n != 0); + arebytes.retain(|_, n| *n != 0); expected.retain(|_, n| *n != 0); assert_eq!( - is_half, expected, - "IS_HALF[μ] tally must match the trace rows" + arebytes, expected, + "ARE_BYTES[μ] tally must match the trace rows" ); assert_eq!(count(BitwiseOperationType::Msb16), msb16, "MSB16 tally"); // ZERO = C8 + C20 per raw op, plus the per-row NEG-template sends. diff --git a/prover/src/tests/lt_multiplicity_poc.rs b/prover/src/tests/lt_multiplicity_poc.rs index deecb0f4a..af53429bf 100644 --- a/prover/src/tests/lt_multiplicity_poc.rs +++ b/prover/src/tests/lt_multiplicity_poc.rs @@ -172,6 +172,7 @@ fn prove_and_verify(lt_rows: &[Row], cpu: &[Vec], victim: &[u64]) -> bool { let opts = ProofOptions::default_test_options(); let half_id: u64 = BusId::IsHalfword.into(); let msb_id: u64 = BusId::Msb16.into(); + let byte_id: u64 = BusId::AreBytes.into(); let mut net = lt_net(lt_rows); for &v in victim { @@ -190,6 +191,13 @@ fn prove_and_verify(lt_rows: &[Row], cpu: &[Vec], victim: &[u64]) -> bool { (t, m) }) .collect(); + // ARE_BYTES receiver (the μ bound sends ARE_BYTES[μ, 0]); a real byte table + // has rows only for [0, 256), so an out-of-range value has no receiver. + let arebytes: Vec<(Vec, FE)> = net + .iter() + .filter(|((bus, t), m)| *bus == byte_id && t[0] < 256 && **m != FE::zero()) + .map(|((_, t), m)| (t.clone(), *m)) + .collect(); let cpu_rows: Vec<(Vec, FE)> = cpu.iter().map(|t| (t.clone(), FE::one())).collect(); let victim_rows: Vec<(Vec, FE)> = victim.iter().map(|&v| (vec![v], FE::one())).collect(); @@ -203,12 +211,14 @@ fn prove_and_verify(lt_rows: &[Row], cpu: &[Vec], victim: &[u64]) -> bool { let mut victim_trace = lookup_trace(&victim_rows, 1); let mut range_trace = lookup_trace(&range, 1); let mut msb16_trace = lookup_trace(&msb16, 2); + let mut arebytes_trace = lookup_trace(&arebytes, 2); let lt_air = create_lt_air(&opts); let cpu_air = lookup_air(&opts, BusId::Alu, 7, true); let victim_air = lookup_air(&opts, BusId::IsHalfword, 1, true); let range_air = lookup_air(&opts, BusId::IsHalfword, 1, false); let msb16_air = lookup_air(&opts, BusId::Msb16, 2, false); + let arebytes_air = lookup_air(&opts, BusId::AreBytes, 2, false); let pairs: Vec<( &dyn AIR, @@ -220,10 +230,17 @@ fn prove_and_verify(lt_rows: &[Row], cpu: &[Vec], victim: &[u64]) -> bool { (<_air, &mut lt_trace, &()), (&range_air, &mut range_trace, &()), (&msb16_air, &mut msb16_trace, &()), + (&arebytes_air, &mut arebytes_trace, &()), ]; let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); - let airs: Vec<&dyn AIR> = - vec![&cpu_air, &victim_air, <_air, &range_air, &msb16_air]; + let airs: Vec<&dyn AIR> = vec![ + &cpu_air, + &victim_air, + <_air, + &range_air, + &msb16_air, + &arebytes_air, + ]; Verifier::multi_verify( &airs, &proof, @@ -237,6 +254,21 @@ fn honest_out(op: &LtOperation) -> u64 { honest_row(op)[cols::OUT].canonical_u64() } +/// A *real, constraint-satisfying* LT row whose `sub_0 = p−1` — the non-canonical +/// split `(p−1, 1)` of `sub_lo = 0xFFFF`. `carry_0` reads only `sub_0 + 2^16·sub_1` +/// (lt.rs:410), so every LtConstraint holds, yet its IS_HALFWORD send carries the +/// out-of-range value `p−1` with multiplicity +1. This is the carrier that cancels +/// a twin's `IS_HALF[μ=p−1]` bound send — no mock, no other table needed. +fn p_minus_1_carrier() -> (LtOperation, Row) { + let op = LtOperation::new(0xFFFF, 0, false); + let mut row = honest_row(&op); + assert_eq!(row[cols::LHS_SUB_RHS_0], FE::from(0xFFFFu64)); + assert_eq!(row[cols::LHS_SUB_RHS_1], FE::zero()); + row[cols::LHS_SUB_RHS_0] = -FE::one(); // p−1 + row[cols::LHS_SUB_RHS_1] = FE::one(); // (p−1) + 2^16 = 0xFFFF, carry unchanged + (op, row) +} + /// Positive control: honest LT rows answering the CPU verify. Without this, a /// "rejected" below would say nothing. #[test] @@ -304,3 +336,40 @@ fn regression_negative_mu_twin_cannot_forge_5_lt_3() { let rows = [a, twin_row(&carrier, HALF), honest_row(&carrier)]; assert!(!prove_and_verify(&rows, &[alu_tuple(&op, 1)], &[])); } + +/// Regression: the in-table carrier that defeated the OLD `IS_HALF[μ]` bound no +/// longer works now that the μ bound is on ARE_BYTES. +/// +/// The four-row forgery of `5 < 3 = 1`: +/// - A: the attacked `5<3` row forced to `lt=1` (high diff word 2^32, `sub_3=2^16`). +/// - T: a `μ=−1` twin of `2^16 < 0` with `sub_0=2^16`, absorbing A's `IS_HALF[2^16]`. +/// - D: the honest `2^16 < 0` row, cancelling T on the ALU bus. +/// - C: a carrier (`sub_0=p−1`) that used to cancel T's bound send on IS_HALF. +/// +/// With the bound on ARE_BYTES, T's `μ=p−1` send lands on `ARE_BYTES[p−1]` (out +/// of byte range, no receiver) and C's `IS_HALF[p−1]` is now itself uncancelled: +/// both buses reject. A limb (IS_HALF) carrier can no longer reach the bound. +#[test] +fn are_bytes_bound_resists_in_table_carrier() { + let op_a = LtOperation::new(5, 3, false); + let mut a = honest_row(&op_a); + a[cols::LT] = FE::one(); + a[cols::OUT] = FE::one(); + a[cols::LHS_SUB_RHS_2] = FE::zero(); + a[cols::LHS_SUB_RHS_3] = FE::from(1u64 << 16); + + let carrier = LtOperation::new(1 << 16, 0, false); + let t = twin_row(&carrier, 1 << 16); + let d = honest_row(&carrier); + + let (op_c, c) = p_minus_1_carrier(); + + let rows = [a, t, d, c]; + let cpu = [alu_tuple(&op_a, 1), alu_tuple(&op_c, honest_out(&op_c))]; + let verified = prove_and_verify(&rows, &cpu, &[]); + println!("LT 5<3=1 with in-table p-1 carrier verified = {verified}"); + assert!( + !verified, + "carrier no longer defeats the ARE_BYTES-bus bound" + ); +} diff --git a/prover/src/tests/lt_tests.rs b/prover/src/tests/lt_tests.rs index ea4f92e38..d11493544 100644 --- a/prover/src/tests/lt_tests.rs +++ b/prover/src/tests/lt_tests.rs @@ -248,11 +248,11 @@ fn test_lt_bounds_its_multiplicity() { use stark::lookup::{BusValue, Multiplicity, Packing}; assert!( bus_interactions().iter().any(|i| i.is_sender - && i.bus_id == BusId::IsHalfword as u64 + && i.bus_id == BusId::AreBytes as u64 && matches!(i.multiplicity, Multiplicity::Column(m) if m == cols::MU) - && matches!(i.values.as_slice(), - [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == cols::MU)), - "LT must IS_HALF-check μ weighted by itself" + && matches!(i.values.first(), + Some(BusValue::Packed { start_column, packing: Packing::Direct }) if *start_column == cols::MU)), + "LT must IS_BYTE-check μ weighted by itself" ); } @@ -325,19 +325,35 @@ fn test_lt_mu_bound_lookups_match_collector() { *is_half.entry(half(op.rhs >> 32 & 0xFFFF)).or_default() -= 1; } - let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + // The μ bound moved to ARE_BYTES, so IS_HALF must now be exactly the limbs. + is_half.retain(|_, n| *n != 0); + assert!( + is_half.is_empty(), + "IS_HALF must match exactly the limb range checks" + ); + + // μ bound: ARE_BYTES[μ, 0] weighted by μ. + let mut arebytes: HashMap = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::AreBytes) + { + assert_eq!(b.y, 0, "μ bound sends ARE_BYTES[μ, 0]"); + *arebytes.entry(b.x).or_default() += 1; + } + let mut expected: HashMap = HashMap::new(); for c in ops.chunks(chunk) { let t = generate_lt_trace(c); for r in 0..t.num_rows() { let mu = t.get_main(r, cols::MU).to_raw(); - *expected.entry(half(mu)).or_default() += mu as i64; + *expected.entry(mu as u8).or_default() += mu as i64; } } - is_half.retain(|_, n| *n != 0); + arebytes.retain(|_, n| *n != 0); expected.retain(|_, n| *n != 0); assert_eq!( - is_half, expected, - "IS_HALF[μ] tally must match the trace rows" + arebytes, expected, + "ARE_BYTES[μ] tally must match the trace rows" ); } } diff --git a/prover/src/tests/mul_mu_carrier_poc.rs b/prover/src/tests/mul_mu_carrier_poc.rs index 409bb9f8f..813639b9e 100644 --- a/prover/src/tests/mul_mu_carrier_poc.rs +++ b/prover/src/tests/mul_mu_carrier_poc.rs @@ -160,11 +160,13 @@ fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { let alu: u64 = BusId::Alu.into(); let half: u64 = BusId::IsHalfword.into(); let b20: u64 = BusId::IsB20.into(); + let byte: u64 = BusId::AreBytes.into(); let net = mul_net(rows); let mut cpu = Vec::new(); let mut range = Vec::new(); let mut range20 = Vec::new(); + let mut arebytes = Vec::new(); for ((bus, tuple), m) in &net { if *m == FE::zero() { continue; @@ -179,6 +181,9 @@ fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { } } else if *bus == b20 && tuple[0] < B20 { range20.push((tuple.clone(), *m)); + } else if *bus == byte && tuple[0] < 256 { + // μ bound: ARE_BYTES[μ, 0]; a real byte table has rows only for [0,256). + arebytes.push((tuple.clone(), *m)); } } let mut carrier = Vec::new(); @@ -195,12 +200,14 @@ fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { let mut cpu_trace = mock_trace(&cpu, 7); let mut range_trace = mock_trace(&range, 1); let mut range20_trace = mock_trace(&range20, 1); + let mut arebytes_trace = mock_trace(&arebytes, 2); let mut carrier_trace = mock_trace(&carrier, 1); let mul_air = create_mul_air(&opts); let cpu_air = mock(&opts, BusId::Alu, 7, true); let range_air = mock(&opts, BusId::IsHalfword, 1, false); let range20_air = mock(&opts, BusId::IsB20, 1, false); + let arebytes_air = mock(&opts, BusId::AreBytes, 2, false); let carrier_air = mock(&opts, BusId::IsHalfword, 1, true); let pairs: Vec<( @@ -212,11 +219,18 @@ fn prove_and_verify(rows: &[Vec], extra_half: Option) -> bool { (&mul_air, &mut mul_trace, &()), (&range_air, &mut range_trace, &()), (&range20_air, &mut range20_trace, &()), + (&arebytes_air, &mut arebytes_trace, &()), (&carrier_air, &mut carrier_trace, &()), ]; let proof = multi_prove_ram(pairs, &mut DefaultTranscript::::new(&[])).unwrap(); - let airs: Vec<&dyn AIR> = - vec![&cpu_air, &mul_air, &range_air, &range20_air, &carrier_air]; + let airs: Vec<&dyn AIR> = vec![ + &cpu_air, + &mul_air, + &range_air, + &range20_air, + &arebytes_air, + &carrier_air, + ]; Verifier::multi_verify( &airs, &proof, @@ -233,16 +247,25 @@ fn control_honest_mul_verifies() { assert!(prove_and_verify(&[row], None)); } -/// The forgery leaves exactly a `−1` at value `p−1` on IS_HALFWORD, and nowhere -/// else out of range — so a single carrier `+1` at `p−1` is all it would need. +/// The twin's `μ_hi = −1` bound now lands on ARE_BYTES, not IS_HALFWORD: it +/// leaves a `−1` at `ARE_BYTES[p−1]` (out of byte range, no receiver), which is +/// why an IS_HALFWORD carrier cannot cancel it. The IS_HALFWORD bus carries no +/// out-of-range residue from the bound. #[test] -fn forgery_leaves_only_minus_one_at_p_minus_1() { +fn forgery_bound_residue_is_on_are_bytes() { let half: u64 = BusId::IsHalfword.into(); + let byte: u64 = BusId::AreBytes.into(); let net = mul_net(&forged_mul_rows()); + + // The μ bound's out-of-range residue is on ARE_BYTES[p−1] with weight −1. + assert_eq!( + net.get(&(byte, vec![minus_one(), 0])).copied(), + Some(-FE::one()) + ); + // No out-of-range IS_HALFWORD send comes from the μ bound any more. for ((bus, tuple), m) in &net { - if *bus == half && tuple[0] >= HALF && *m != FE::zero() { - assert_eq!(tuple[0], minus_one()); - assert_eq!(*m, -FE::one()); + if *bus == half && tuple[0] == minus_one() { + assert_eq!(*m, FE::zero(), "no μ-bound residue on IS_HALFWORD"); } } } @@ -253,16 +276,15 @@ fn forgery_without_carrier_is_rejected() { assert!(!prove_and_verify(&forged_mul_rows(), None)); } -/// The decisive case: does a carrier that supplies `+1` at `p−1` let the -/// `μ_hi = −1` product forgery through the weighted-by-μ bound? +/// Regression: the μ bound now lives on ARE_BYTES, a bus the `lo`/`hi` limb +/// range checks (IS_HALFWORD) never touch. So an IS_HALFWORD carrier at `p−1` +/// can no longer cancel the twin's `μ_hi = −1` bound send (it lands on +/// ARE_BYTES[p−1], out of byte range, with no receiver). The forgery is +/// rejected even WITH the carrier. #[test] -fn forgery_with_carrier_at_p_minus_1() { - let verified = prove_and_verify(&forged_mul_rows(), Some(minus_one())); - // Asserting the observed behaviour so the harness is not vacuous; the point - // of the test is the printed verdict, interpreted in the module docs. - println!("MUL forgery with p-1 carrier verified = {verified}"); +fn is_halfword_carrier_no_longer_defeats_byte_bound() { assert!( - verified, - "if this fails the weighted-by-μ bound resisted the carrier" + !prove_and_verify(&forged_mul_rows(), Some(minus_one())), + "ARE_BYTES bound must resist an IS_HALFWORD carrier" ); } diff --git a/prover/src/tests/mul_tests.rs b/prover/src/tests/mul_tests.rs index cce10d890..1c72dfab8 100644 --- a/prover/src/tests/mul_tests.rs +++ b/prover/src/tests/mul_tests.rs @@ -433,11 +433,11 @@ fn test_mul_bounds_its_multiplicities() { for col in [cols::MU_LO, cols::MU_HI] { assert!( bus_interactions().iter().any(|i| i.is_sender - && i.bus_id == BusId::IsHalfword as u64 + && i.bus_id == BusId::AreBytes as u64 && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) - && matches!(i.values.as_slice(), - [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col)), - "MUL must IS_HALF-check multiplicity column {col} weighted by itself" + && matches!(i.values.first(), + Some(BusValue::Packed { start_column, packing: Packing::Direct }) if *start_column == col)), + "MUL must IS_BYTE-check multiplicity column {col} weighted by itself" ); } } @@ -526,24 +526,40 @@ fn test_mul_per_row_lookups_match_collector() { } } - let mut expected: HashMap<(u8, u8), i64> = HashMap::new(); + // The μ bound moved to ARE_BYTES, so IS_HALF must now be exactly the limbs. + is_half.retain(|_, n| *n != 0); + assert!( + is_half.is_empty(), + "IS_HALF must match exactly the limb range checks" + ); + + // μ bounds: ARE_BYTES[μ_lo, 0] and ARE_BYTES[μ_hi, 0], weighted by μ. + let mut arebytes: HashMap = HashMap::new(); + for b in collected + .iter() + .filter(|b| b.lookup_type == BitwiseOperationType::AreBytes) + { + assert_eq!(b.y, 0, "μ bounds send ARE_BYTES[μ, 0]"); + *arebytes.entry(b.x).or_default() += 1; + } + let mut expected: HashMap = HashMap::new(); let mut msb16 = 0usize; for c in ops.chunks(chunk) { let t = generate_mul_trace(c); for r in 0..t.num_rows() { for col in [cols::MU_LO, cols::MU_HI] { let mu = t.get_main(r, col).to_raw(); - *expected.entry(half(mu)).or_default() += mu as i64; + *expected.entry(mu as u8).or_default() += mu as i64; } msb16 += t.get_main(r, cols::LHS_SIGNED).to_raw() as usize; msb16 += t.get_main(r, cols::RHS_SIGNED).to_raw() as usize; } } - is_half.retain(|_, n| *n != 0); + arebytes.retain(|_, n| *n != 0); expected.retain(|_, n| *n != 0); assert_eq!( - is_half, expected, - "IS_HALF[μ] tally must match the trace rows" + arebytes, expected, + "ARE_BYTES[μ] tally must match the trace rows" ); assert_eq!( collected From 3a5a3f46cc15825444b606a2b686c306026c9308 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 7 Oct 2026 09:23:02 -0300 Subject: [PATCH 07/13] Force is_negative to 0 on unsigned shift rows --- prover/src/tables/shift.rs | 16 ++++++++-- prover/src/tests/shift_tests.rs | 56 +++++++++++++++++++++++++++++++-- 2 files changed, 68 insertions(+), 4 deletions(-) diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index 99cee2f8b..ea0fce6e8 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -726,14 +726,14 @@ pub fn bus_interactions() -> Vec { } /// Total number of SHIFT transition constraints. -pub const NUM_SHIFT_CONSTRAINTS: usize = 21; +pub const NUM_SHIFT_CONSTRAINTS: usize = 22; // ========================================================================= // Single-body constraint set (ConstraintSet front-end) // ========================================================================= // // One body against the generic `ConstraintBuilder` serves the compiled prover -// folder, the verifier folder and IR capture. Constraint indices 0..21. +// folder, the verifier folder and IR capture. Constraint indices 0..22. use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; @@ -910,6 +910,18 @@ impl ConstraintSet for ShiftConstraints { let mu = b.main(0, cols::MU); let one = b.one(); b.emit_base(20, mu.clone() * (one - mu)); + + // idx 21: UnsignedIsNotNegative — (1 - signed) * is_negative. On a signed + // row `is_negative` is pinned to the real MSB via the MSB16 bus (multiplicity + // `signed`); on an unsigned row nothing constrains it, yet `shifted_half` + // fills with `extension = 65535 * is_negative` without gating on `signed`. + // So an unsigned right shift (SRL) could set `is_negative = 1` and forge a + // sign-filled result (e.g. `srl 0, 16 = 0xFFFF_0000_0000_0000`). This pins + // it to 0 when `signed = 0`. + let signed = b.main(0, cols::SIGNED); + let is_negative = b.main(0, cols::IS_NEGATIVE); + let one = b.one(); + b.emit_base(21, (one - signed) * is_negative); } } diff --git a/prover/src/tests/shift_tests.rs b/prover/src/tests/shift_tests.rs index 1563c4030..88b5bc465 100644 --- a/prover/src/tests/shift_tests.rs +++ b/prover/src/tests/shift_tests.rs @@ -37,8 +37,8 @@ fn test_shift_air_wires_in_chip_constraints() { bus_interactions(), ); assert_eq!(in_chip, NUM_SHIFT_CONSTRAINTS); - // 19 + ZbsIsBit + MuIsBit. - assert_eq!(NUM_SHIFT_CONSTRAINTS, 21); + // 19 + ZbsIsBit + MuIsBit + UnsignedIsNotNegative. + assert_eq!(NUM_SHIFT_CONSTRAINTS, 22); } // ========================================================================= @@ -210,3 +210,55 @@ mod zbs_mu_bit_regression { ); } } + +// Separate preexisting bug (NOT a multiplicity bug, not fixed by this PR): +// Soundness regression: `is_negative` must be 0 on unsigned rows. It is pinned +// to the real MSB via the MSB16 bus only when `signed = 1` (multiplicity +// `signed`), but `shifted_half` fills with `extension = 65535·is_negative` +// without gating on `signed`, so an unsigned right shift (SRL) could set +// `is_negative = 1` and sign-fill the result. Closed by idx 21 +// `(1 − signed)·is_negative = 0`. +mod is_negative_unsigned_poc { + use crate::tables::shift::{ShiftConstraints, ShiftOperation, cols, generate_shift_trace}; + use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField}; + use crate::test_utils::{busless_air, validate_busless}; + + type Trace = stark::trace::TraceTable; + + /// `srl 0, 16` (unsigned right shift, direction = right, signed = false). + /// Honest result is 0; forged `is_negative = 1` sign-fills the top limb. + fn srl_0_by_16() -> Trace { + // new(value, shift_amount, direction=right, signed, word_instr) + let op = ShiftOperation::new(0, 16, true, false, false); + generate_shift_trace(std::slice::from_ref(&op)) + } + + #[test] + fn honest_srl_is_zero_and_valid() { + let t = srl_0_by_16(); + let air = busless_air(cols::NUM_COLUMNS, ShiftConstraints); + assert!(validate_busless(&air, &t), "honest SRL must validate"); + assert_eq!(*t.main_table.get(0, cols::IS_NEGATIVE), FE::zero()); + assert_eq!(*t.main_table.get(0, cols::OUT_0), FE::zero()); + assert_eq!(*t.main_table.get(0, cols::OUT_1), FE::zero()); + } + + /// Regression: the same unsigned row with `is_negative = 1` and the + /// sign-filled output (`srl 0, 16 = 0xFFFF_0000_0000_0000`) is now rejected + /// by `(1 − signed)·is_negative = 0`. + #[test] + fn unsigned_srl_forged_sign_extension_is_rejected() { + let mut t = srl_0_by_16(); + assert_eq!(*t.main_table.get(0, cols::SIGNED), FE::zero()); + // Flip the aux bit and set the sign-filled output it implies + // (top 16-bit limb = extension = 0xFFFF): out = 0xFFFF_0000_0000_0000. + t.main_table.set(0, cols::IS_NEGATIVE, FE::one()); + t.main_table.set(0, cols::OUT_1, FE::from(0xFFFF_0000u64)); + + let air = busless_air(cols::NUM_COLUMNS, ShiftConstraints); + assert!( + !validate_busless(&air, &t), + "unsigned SRL with is_negative=1 must be rejected by UnsignedIsNotNegative" + ); + } +} From de098d6692307c485435b30e9e67eae2a178d351 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 7 Oct 2026 09:32:31 -0300 Subject: [PATCH 08/13] Document why the multiplicity bound rides the ARE_BYTES bus --- prover/src/tables/branch.rs | 7 +++++++ prover/src/tables/dvrm.rs | 7 +++++++ prover/src/tables/lt.rs | 7 +++++++ prover/src/tables/mul.rs | 7 +++++++ 4 files changed, 28 insertions(+) diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index 243f84925..2dccf8e4a 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -155,6 +155,13 @@ impl BranchOperation { /// bound keeps μ non-negative: without it a `μ = −1` twin of an honest row /// cancels it on the BRANCH bus while *receiving* its range lookups, absorbing /// another row's out-of-range limb (same bug as LT). +/// +/// The bound rides the ARE_BYTES bus, which the limb range checks +/// (IS_HALFWORD) never use. That is what closes it: an IS_HALFWORD-bus +/// bound could be cancelled by a non-canonical limb `(p−1, b+1)` (same +/// packed value, passes every constraint) sending `IS_HALFWORD[p−1]`; +/// on ARE_BYTES no limb can reach the `p−1` tuple, so a `μ = −1` row's +/// bound send has no receiver and the whole proof is rejected. pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates BRANCH operations into trace rows: `(pc, offset, register, diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index ee9c75451..21ab9da06 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -279,6 +279,13 @@ impl DvrmOperation { /// lookups of each kind. The bound is what makes `μ_q + μ_r = 0` imply /// `μ_q = μ_r = 0`: without it a `μ_q = 1, μ_r = −1` row receives a quotient /// lookup while sending none of its checks (forged `n = q·d + r`). +/// +/// The bound rides the ARE_BYTES bus, which the limb range checks +/// (IS_HALFWORD) never use. That is what closes it: an IS_HALFWORD-bus +/// bound could be cancelled by a non-canonical limb `(p−1, b+1)` (same +/// packed value, passes every constraint) sending `IS_HALFWORD[p−1]`; +/// on ARE_BYTES no limb can reach the `p−1` tuple, so a `μ = −1` row's +/// bound send has no receiver and the whole proof is rejected. pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates DVRM operations into trace rows: `(n, d, signed) -> (μ_q, μ_r)`, diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index b7f3d2710..fa5e0ac52 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -159,6 +159,13 @@ impl LtOperation { /// bound is what keeps μ non-negative: without it a `μ = −1` twin of an honest /// row cancels it on the ALU bus while *receiving* its range lookups, which /// absorbs another row's out-of-range limb (a forged `5 < 3 = 1` verified). +/// +/// The bound rides the ARE_BYTES bus, which the limb range checks +/// (IS_HALFWORD) never use. That is what closes it: an IS_HALFWORD-bus +/// bound could be cancelled by a non-canonical limb `(p−1, b+1)` (same +/// packed value, passes every constraint) sending `IS_HALFWORD[p−1]`; +/// on ARE_BYTES no limb can reach the `p−1` tuple, so a `μ = −1` row's +/// bound send has no receiver and the whole proof is rejected. pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates LT operations into trace rows: `(lhs, rhs, signed, invert) -> μ`, diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index 08863abb5..2869c9160 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -287,6 +287,13 @@ impl MulOperation { /// lookups of each kind. The bound is what makes `μ_lo + μ_hi = 0` imply /// `μ_lo = μ_hi = 0`: without it a `μ_lo = 1, μ_hi = −1` row receives a lookup /// while sending none of its range checks. +/// +/// The bound rides the ARE_BYTES bus, which the limb range checks +/// (IS_HALFWORD) never use. That is what closes it: an IS_HALFWORD-bus +/// bound could be cancelled by a non-canonical limb `(p−1, b+1)` (same +/// packed value, passes every constraint) sending `IS_HALFWORD[p−1]`; +/// on ARE_BYTES no limb can reach the `p−1` tuple, so a `μ = −1` row's +/// bound send has no receiver and the whole proof is rejected. pub const MU_MAX: u64 = (1 << 8) - 1; /// Deduplicates MUL operations into trace rows: `(lhs, lhs_signed, rhs, From af6f14de8f4474db673af355f6b19a297e2d65cd Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 7 Oct 2026 10:00:05 -0300 Subject: [PATCH 09/13] Bit-constrain KECCAK and KECCAK_RND multiplicities --- prover/src/tables/keccak.rs | 9 ++ prover/src/tables/keccak_rnd.rs | 10 +++ prover/src/tests/keccak_rnd_tests.rs | 110 ++++++++++++++++++++++++ prover/src/tests/keccak_tests.rs | 38 ++++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/trace_builder_tests.rs | 8 +- 6 files changed, 173 insertions(+), 4 deletions(-) create mode 100644 prover/src/tests/keccak_tests.rs diff --git a/prover/src/tables/keccak.rs b/prover/src/tables/keccak.rs index 7b84cbd48..8c4c879b1 100644 --- a/prover/src/tables/keccak.rs +++ b/prover/src/tables/keccak.rs @@ -507,5 +507,14 @@ impl ConstraintSet for KeccakConstraints { let carry_1 = (addr_hi + carry_0 - ptr_hi) * inv_2_32; let mu = b.main(0, cols::MU); b.emit_base(50, mu * carry_1); + + // idx 51: MuIsBit — μ·(1−μ). Every other constraint and bus send is + // weighted by μ, so μ ≠ 0 is indistinguishable from μ = 1 at the + // constraint level, while on the bus a μ = −1 row inverts a range check + // (carrier). KECCAK does not deduplicate (one row per hash, μ ∈ {0,1}), + // so the bit constraint is honest and forbids μ = −1. + let mu = b.main(0, cols::MU); + let one = b.one(); + b.emit_base(51, mu.clone() * (one - mu)); } } diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 51b7759f3..f6ebd7031 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -918,5 +918,15 @@ impl ConstraintSet for KeccakRndConstraint } } } + + // MuIsBit — μ·(1−μ). Every other constraint and bus send is weighted by + // μ, so μ = 2, 7 or −1 is indistinguishable from μ = 1 at the constraint + // level, while on the bus a μ = −1 row inverts a range check and can hold + // a non-canonical (out-of-range) shift byte — the carrier mechanism. + // KECCAK_RND does not deduplicate (one row per round, μ ∈ {0,1}), so the + // bit constraint is honest and forbids μ = −1, closing the carrier. + let mu = b.main(0, cols::MU); + let one = b.one(); + b.emit_base(idx, mu.clone() * (one - mu)); } } diff --git a/prover/src/tests/keccak_rnd_tests.rs b/prover/src/tests/keccak_rnd_tests.rs index 230ef6065..1b643d4e5 100644 --- a/prover/src/tests/keccak_rnd_tests.rs +++ b/prover/src/tests/keccak_rnd_tests.rs @@ -55,3 +55,113 @@ fn test_pi_virtual_matches_rotate() { } } } + +// Soundness gap (unfixed): KECCAK_RND's `μ` is not bit-constrained. Every +// Soundness regression: μ must be a bit. Every other constraint is `μ · identity` +// (or `μ · x·(1−x)`), so μ = 2, 7 or −1 used to be indistinguishable from μ = 1 at +// the constraint level, while on the bus μ weights (and with −1 inverts) every +// send — so a μ = −1 row could invert a range check and act as a carrier (the +// bytes are not pinned, see `are_bytes_carrier_poc`). The chip does not +// deduplicate, so `MuIsBit` (μ·(1−μ)=0) is the right fix (like SHIFT/LOAD): it +// forbids μ = −1 and closes the carrier. +mod mu_unconstrained_poc { + use crate::tables::keccak_rnd::{ + KeccakRndConstraints, KeccakRoundOperation, cols, generate_keccak_rnd_trace, + }; + use crate::tables::types::FE; + use crate::test_utils::{busless_air, validate_busless}; + use executor::vm::instruction::execution::keccak_f1600; + + #[test] + fn mu_is_bit_constrained() { + let input = [0x0102030405060708u64; 25]; + let mut output = input; + keccak_f1600(&mut output); + let honest = generate_keccak_rnd_trace(&[KeccakRoundOperation { + timestamp: 42, + input, + output, + }]); + let air = busless_air(cols::NUM_COLUMNS, KeccakRndConstraints); + + assert!( + validate_busless(&air, &honest), + "honest trace must validate" + ); + assert_eq!(*honest.main_table.get(0, cols::MU), FE::one()); + + // μ = 2, 7, −1 are now all rejected by MuIsBit. + for bad in [FE::from(2u64), FE::from(7u64), -FE::one()] { + let mut t = honest.clone(); + t.main_table.set(0, cols::MU, bad); + assert!( + !validate_busless(&air, &t), + "μ ∉ {{0,1}} must be rejected by MuIsBit" + ); + } + } +} + +// Why MuIsBit is necessary: the θ shift identity reads `cxz_left` as a HALFWORD +// (`byte_lo + 256·byte_hi`), while ARE_BYTES range-checks the two bytes. So the +// bytes are NOT pinned by the constraints — a non-canonical split keeps the +// halfword (and the identity) unchanged while sending an out-of-range byte to +// ARE_BYTES. A μ = −1 row would invert that send (carrier). With `MuIsBit` +// forbidding μ = −1 the carrier is closed, but this test shows the underlying +// gap — the constraints still do not range-constrain the bytes; a μ=−1 row could +// hold an out-of-range byte and absorb another table's out-of-range ARE_BYTES. +mod are_bytes_carrier_poc { + use crate::tables::keccak_rnd::{ + KeccakRndConstraints, KeccakRoundOperation, cols, generate_keccak_rnd_trace, + }; + use crate::tables::types::FE; + use crate::test_utils::{busless_air, validate_busless}; + use executor::vm::instruction::execution::keccak_f1600; + + #[test] + fn non_canonical_cxz_byte_passes_constraints() { + let input = [0x0102030405060708u64; 25]; + let mut output = input; + keccak_f1600(&mut output); + let honest = generate_keccak_rnd_trace(&[KeccakRoundOperation { + timestamp: 42, + input, + output, + }]); + let air = busless_air(cols::NUM_COLUMNS, KeccakRndConstraints); + assert!( + validate_busless(&air, &honest), + "honest trace must validate" + ); + + // Row 0 is a real round row (μ = 1). Take the first θ halfword of x = 0. + let lo_col = cols::cxz_left(0, 0); + let hi_col = cols::cxz_left(0, 1); + let lo = honest.main_table.get(0, lo_col).to_raw(); + let hi = honest.main_table.get(0, hi_col).to_raw(); + let value = lo + 256 * hi; // the halfword the identity reads + + // Non-canonical split: byte_lo = p−1 (= −1), byte_hi = (value + 1)/256. + // Then byte_lo + 256·byte_hi = value (mod p), so the identity is unchanged, + // but byte_lo is out of range for ARE_BYTES. + let inv_256 = FE::from(256u64).inv().expect("256 invertible"); + let new_hi = (FE::from(value) + FE::one()) * inv_256; + let mut forged = honest.clone(); + forged.main_table.set(0, lo_col, -FE::one()); + forged.main_table.set(0, hi_col, new_hi); + + // Sanity: the halfword is preserved. + let lo2 = *forged.main_table.get(0, lo_col); + let hi2 = *forged.main_table.get(0, hi_col); + assert_eq!(lo2 + FE::from(256u64) * hi2, FE::from(value)); + // And the forged low byte is out of the byte range [0, 256). + assert!((-FE::one()).to_raw() >= 256); + + // The AIR accepts the non-canonical bytes: the constraints read only the + // halfword, so they never range-constrain the bytes. + assert!( + validate_busless(&air, &forged), + "out-of-range cxz_left byte must still satisfy KECCAK_RND's constraints" + ); + } +} diff --git a/prover/src/tests/keccak_tests.rs b/prover/src/tests/keccak_tests.rs new file mode 100644 index 000000000..98e71fe70 --- /dev/null +++ b/prover/src/tests/keccak_tests.rs @@ -0,0 +1,38 @@ +//! Tests for the KECCAK (core) table. + +// Soundness regression: μ must be a bit. Every KECCAK constraint and bus send is +// weighted by μ, so μ = 2 or −1 was indistinguishable from μ = 1 at the +// constraint level while on the bus a μ = −1 row inverts a range check (carrier). +// KECCAK does not deduplicate (one row per hash, μ ∈ {0,1}), so `MuIsBit` +// (μ·(1−μ)=0) is the right fix and forbids μ = −1. + +use crate::tables::keccak::{KeccakConstraints, KeccakOperation, cols, generate_keccak_trace}; +use crate::tables::types::FE; +use crate::test_utils::{busless_air, validate_busless}; + +#[test] +fn mu_is_bit_constrained() { + let op = KeccakOperation { + timestamp: 7, + state_addr: 0x1000, + input: [0x0102030405060708u64; 25], + output: [0u64; 25], + }; + let honest = generate_keccak_trace(std::slice::from_ref(&op)); + let air = busless_air(cols::NUM_COLUMNS, KeccakConstraints); + + assert!( + validate_busless(&air, &honest), + "honest trace must validate" + ); + assert_eq!(*honest.main_table.get(0, cols::MU), FE::one()); + + for bad in [FE::from(2u64), -FE::one()] { + let mut t = honest.clone(); + t.main_table.set(0, cols::MU, bad); + assert!( + !validate_busless(&air, &t), + "μ ∉ {{0,1}} must be rejected by MuIsBit" + ); + } +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 9df45c683..b3147f0e4 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -55,6 +55,8 @@ pub mod ir_stats_dump; #[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] +pub mod keccak_tests; +#[cfg(test)] pub mod load_tests; #[cfg(test)] pub mod local_to_global_bus_tests; diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 428fd4700..ca5426dce 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -763,13 +763,13 @@ mod keccak_tests { use stark::constraints::builder::ConstraintSet; assert_eq!( keccak::KeccakConstraints.meta().len(), - 51, - "KECCAK core: 25 ADD pairs + no-overflow" + 52, + "KECCAK core: 25 ADD pairs + no-overflow + MuIsBit" ); assert_eq!( keccak_rnd::KeccakRndConstraints.meta().len(), - 140, - "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) + 20 θ + 100 ρ inline shift identities" + 141, + "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) + 20 θ + 100 ρ inline shift identities + MuIsBit" ); } } From 01f8f5e37dfd69fc3a36b92a46c5149a77c3d275 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 7 Oct 2026 13:29:49 -0300 Subject: [PATCH 10/13] Fix stale test docs and rebalance forgery residue on ARE_BYTES --- prover/src/tables/lt.rs | 3 +-- prover/src/test_utils.rs | 8 +++++- prover/src/tests/dvrm_tests.rs | 6 ++--- prover/src/tests/keccak_rnd_tests.rs | 7 +++-- prover/src/tests/keccak_tests.rs | 3 +++ prover/src/tests/lt_tests.rs | 10 +++---- prover/src/tests/mul_tests.rs | 4 +-- prover/src/tests/multiplicity_forgery_poc.rs | 28 +++++++++++++------- 8 files changed, 44 insertions(+), 25 deletions(-) diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index fa5e0ac52..2c618fa9d 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -22,8 +22,7 @@ //! //! ## Bus Interactions //! - Sender: MSB16 (×2 for lhs_msb, rhs_msb) -//! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]; -//! ) +//! - Sender: IS_HALFWORD (×6: ×4 for lhs_sub_rhs, ×1 for lhs[1], ×1 for rhs[1]) //! - Sender: ARE_BYTES (×1 for the μ multiplicity bound) //! - Receiver: ALU (all less-than lookups — CPU SLT/BLT/BGE dispatch and the //! internal `memw`/`memw_aligned`/`dvrm` timestamp / |r|<|d| checks) diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 5b4206356..b0d1d3977 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -237,7 +237,13 @@ pub fn asm_elf_bytes(name: &str) -> Vec { .join("asm") .join(format!("{}.elf", name)); - std::fs::read(&path).unwrap_or_else(|_| panic!("Failed to read ELF: {}", path.display())) + std::fs::read(&path).unwrap_or_else(|_| { + panic!( + "Failed to read ELF: {} — the .elf artifacts are gitignored; run \ + `make compile-programs-asm` first", + path.display() + ) + }) } /// Helper to run an ELF from the program_artifacts directory. diff --git a/prover/src/tests/dvrm_tests.rs b/prover/src/tests/dvrm_tests.rs index 588b77c55..ba4f95296 100644 --- a/prover/src/tests/dvrm_tests.rs +++ b/prover/src/tests/dvrm_tests.rs @@ -311,7 +311,7 @@ fn test_bus_interactions_count() { // - 2x MUL senders (n_sub_r = d*q lo + hi) // - 6x ZERO senders (C3×2 NEG r, C5×2 NEG d, C8 overflow, C17 div_by_zero) // - 2x DVRM receivers (quotient, remainder) - // - 2x IS_HALF senders bounding the multiplicities (μ_q, μ_r) + // - 2x ARE_BYTES senders bounding the multiplicities (μ_q, μ_r) // Total: 8 + 12 + 3 + 1 + 2 + 6 + 2 + 2 = 36 assert_eq!(interactions.len(), 36, "Expected 36 bus interactions"); } @@ -559,11 +559,11 @@ fn neg_template_zero_lookups_dedup_per_chip_instance() { // Soundness regression: μ_q/μ_r are bounded, non-negative multiplicities. // Every DVRM check fires with μ_q + μ_r, so a free μ_r = −1 next to μ_q = 1 -// switched them all off (`multiplicity_forgery_poc`). Each μ is now IS_HALF-checked +// switched them all off (`multiplicity_forgery_poc`). Each μ is now ARE_BYTES-checked // weighted by itself, and trace generation splits a row whose count would // exceed `MU_MAX`. -/// Presence: each multiplicity is IS_HALF-checked weighted by itself, so an +/// Presence: each multiplicity is ARE_BYTES-checked weighted by itself, so an /// out-of-range value `v` always lands on the bus with weight `v ≠ 0`. #[test] fn test_dvrm_bounds_its_multiplicities() { diff --git a/prover/src/tests/keccak_rnd_tests.rs b/prover/src/tests/keccak_rnd_tests.rs index 1b643d4e5..8b42f10eb 100644 --- a/prover/src/tests/keccak_rnd_tests.rs +++ b/prover/src/tests/keccak_rnd_tests.rs @@ -56,7 +56,6 @@ fn test_pi_virtual_matches_rotate() { } } -// Soundness gap (unfixed): KECCAK_RND's `μ` is not bit-constrained. Every // Soundness regression: μ must be a bit. Every other constraint is `μ · identity` // (or `μ · x·(1−x)`), so μ = 2, 7 or −1 used to be indistinguishable from μ = 1 at // the constraint level, while on the bus μ weights (and with −1 inverts) every @@ -64,7 +63,11 @@ fn test_pi_virtual_matches_rotate() { // bytes are not pinned, see `are_bytes_carrier_poc`). The chip does not // deduplicate, so `MuIsBit` (μ·(1−μ)=0) is the right fix (like SHIFT/LOAD): it // forbids μ = −1 and closes the carrier. -mod mu_unconstrained_poc { +// +// DEFENSIVE: this is a constraint-presence regression (μ ∉ {0,1} is rejected), not +// an end-to-end forgery; the carrier was confirmed structurally (bytes not pinned, +// see `are_bytes_carrier_poc`), not demonstrated. +mod mu_bit_regression { use crate::tables::keccak_rnd::{ KeccakRndConstraints, KeccakRoundOperation, cols, generate_keccak_rnd_trace, }; diff --git a/prover/src/tests/keccak_tests.rs b/prover/src/tests/keccak_tests.rs index 98e71fe70..59eccdfbd 100644 --- a/prover/src/tests/keccak_tests.rs +++ b/prover/src/tests/keccak_tests.rs @@ -5,6 +5,9 @@ // constraint level while on the bus a μ = −1 row inverts a range check (carrier). // KECCAK does not deduplicate (one row per hash, μ ∈ {0,1}), so `MuIsBit` // (μ·(1−μ)=0) is the right fix and forbids μ = −1. +// +// DEFENSIVE: this is a constraint-presence regression (μ ∉ {0,1} is rejected), not +// an end-to-end forgery. The carrier was confirmed structurally, not demonstrated. use crate::tables::keccak::{KeccakConstraints, KeccakOperation, cols, generate_keccak_trace}; use crate::tables::types::FE; diff --git a/prover/src/tests/lt_tests.rs b/prover/src/tests/lt_tests.rs index d11493544..b32faf6a5 100644 --- a/prover/src/tests/lt_tests.rs +++ b/prover/src/tests/lt_tests.rs @@ -169,7 +169,7 @@ fn test_bus_interactions_count() { // MSB16 x2 + IS_HALFWORD x6 (lhs_sub_rhs x4 + lhs[1] + rhs[1]) // + ALU receiver x1 (every LT lookup goes through the unified ALU bus // — CPU SLT/BLT/BGE dispatch and the internal memw/dvrm - // timestamp / |r|<|d| checks) + IS_HALFWORD x1 bounding μ = 10. + // timestamp / |r|<|d| checks) + ARE_BYTES x1 bounding μ = 10. assert_eq!(interactions.len(), 10); } @@ -236,11 +236,11 @@ fn test_lt_rejects_forged_out() { // Soundness regression: μ is a bounded, non-negative multiplicity. Every LT // lookup fires with μ, so a free μ = −1 twin of an honest row received range // lookups instead of sending them and absorbed another row's out-of-range limb -// (`lt_multiplicity_poc`, `multiplicity_forgery_poc`). μ is now IS_HALF-checked -// weighted by itself, and trace generation splits a row whose count would -// exceed `MU_MAX`. +// (`lt_multiplicity_poc`, `multiplicity_forgery_poc`). μ is now range-checked on +// ARE_BYTES (`ARE_BYTES[μ, 0]`, weighted by μ), and trace generation splits a row +// whose count would exceed `MU_MAX`. -/// Presence: μ is IS_HALF-checked weighted by itself, so an out-of-range value +/// Presence: μ is ARE_BYTES-checked weighted by itself, so an out-of-range value /// `v` always lands on the bus with weight `v ≠ 0`. #[test] fn test_lt_bounds_its_multiplicity() { diff --git a/prover/src/tests/mul_tests.rs b/prover/src/tests/mul_tests.rs index 1c72dfab8..1429ba424 100644 --- a/prover/src/tests/mul_tests.rs +++ b/prover/src/tests/mul_tests.rs @@ -270,7 +270,7 @@ fn test_bus_interactions_count() { // - 8x IS_HALF senders for outputs (lo[0..4], hi[0..4]) // - 4x IS_B20 senders (carry[0..4] virtual range checks) // - 2x ALU receivers (lo, hi) - // - 2x IS_HALF senders bounding the multiplicities (μ_lo, μ_hi) + // - 2x ARE_BYTES senders bounding the multiplicities (μ_lo, μ_hi) // Total: 2 + 8 + 8 + 4 + 2 + 2 = 26 assert_eq!(interactions.len(), 26, "Expected 26 bus interactions"); } @@ -424,7 +424,7 @@ fn msb16_bitwise_multiplicity_matches_per_instance_sends() { // IS_HALF-range-checked weighted by itself, and trace generation splits a // row whose count would exceed `MU_MAX`. -/// Presence: each multiplicity is IS_HALF-checked weighted by itself, so an +/// Presence: each multiplicity is ARE_BYTES-checked weighted by itself, so an /// out-of-range value `v` always lands on the bus with weight `v ≠ 0`. #[test] fn test_mul_bounds_its_multiplicities() { diff --git a/prover/src/tests/multiplicity_forgery_poc.rs b/prover/src/tests/multiplicity_forgery_poc.rs index afb8677f9..cc0b86f97 100644 --- a/prover/src/tests/multiplicity_forgery_poc.rs +++ b/prover/src/tests/multiplicity_forgery_poc.rs @@ -9,8 +9,10 @@ //! all while still receiving one `a` lookup: its result was free. The stray `−1` //! on the `b` tuple was cancelled by an honest copy of the row with //! `μ_a = 0, μ_b = +1`, whose checks fire once and pass. Both forgeries below -//! verified against `main` (ffc4ac19). The fix range-checks each μ to a halfword -//! (`IS_HALF[μ]`, weighted by μ), so `μ_b = −1` has no receiver. +//! verified against `main` (ffc4ac19). The fix range-checks each μ to a byte on +//! the ARE_BYTES bus (`ARE_BYTES[μ, 0]`, weighted by μ) — a bus the limb checks +//! (IS_HALFWORD) never use — so `μ_b = −1` lands at `ARE_BYTES[p−1, 0]` with no +//! receiver. //! //! **SHIFT.** The five HWSL senders fire with `1 − zbs`, and on a μ = 0 padding //! row nothing pinned `zbs`: `zbs = 2` made that −1, so the padding row provided @@ -234,11 +236,11 @@ fn craft_proof(s: &Scenario, forge: Forge) -> Result bool { interactions.iter().any(|i| { i.is_sender - && i.bus_id == BusId::IsHalfword as u64 + && i.bus_id == BusId::AreBytes as u64 && matches!(i.multiplicity, Multiplicity::Column(m) if m == col) && matches!( - i.values.as_slice(), - [BusValue::Packed { start_column, packing: Packing::Direct }] if *start_column == col + i.values.first(), + Some(BusValue::Packed { start_column, packing: Packing::Direct }) if *start_column == col ) }) } @@ -260,8 +262,8 @@ fn bump_bitwise(traces: &mut Traces, mu_col: usize, half: u64, delta: FE) { /// `μ_a = 0, μ_b = 1`. /// /// Returns the row-B copy's index so the caller can rebalance flag-gated sends. -/// If the chip range-checks its μ columns, also rebalances those IS_HALF sends -/// wherever a BITWISE row exists (`−1` has none — that is the fix). +/// If the chip range-checks its μ columns (ARE_BYTES[μ, 0]), also rebalances +/// those sends wherever a BITWISE row exists (`p−1` has none — that is the fix). fn forge_two_rows( traces: &mut Traces, table: fn(&mut Traces) -> &mut TraceTable, @@ -291,9 +293,10 @@ fn forge_two_rows( t.set_main(a, mu_b, FE::zero() - FE::one()); if bounded { - // IS_HALF[μ] | μ sends: B's μ_b 0 -> 1 adds IS_HALF[1] once. A's μ_b - // 0 -> −1 adds IS_HALF[p−1] with weight −1, which has no BITWISE row. - bump_bitwise(traces, bw_cols::MU_IS_HALF, 1, FE::one()); + // ARE_BYTES[μ, 0] | μ sends: B's μ_b 0 -> 1 adds ARE_BYTES[1, 0] once; A's + // μ_b 0 -> −1 adds ARE_BYTES[p−1, 0] with weight −1, which has no BITWISE + // row (that out-of-range send is what rejects the forgery). + bump_bitwise(traces, bw_cols::MU_ARE_BYTES, 1, FE::one()); } b } @@ -534,6 +537,7 @@ fn forge_lt_rows(traces: &mut Traces, s: &Scenario) { let (old, new) = (lt_net(&before), lt_net(&after)); let half_id: u64 = BusId::IsHalfword.into(); let msb_id: u64 = BusId::Msb16.into(); + let byte_id: u64 = BusId::AreBytes.into(); let keys: std::collections::HashSet<_> = old.keys().chain(new.keys()).cloned().collect(); for (bus, tuple) in keys { let delta = new @@ -553,6 +557,10 @@ fn forge_lt_rows(traces: &mut Traces, s: &Scenario) { } else if bus == msb_id { assert_eq!(tuple[1], v >> 15, "MSB16 sends stay honest"); bump_bitwise(traces, bw_cols::MU_MSB16, v, delta); + } else if bus == byte_id { + // LT's only ARE_BYTES send is the μ bound (`ARE_BYTES[μ, 0]`). + assert_eq!(tuple[1], 0, "the μ bound sends ARE_BYTES[μ, 0]"); + bump_bitwise(traces, bw_cols::MU_ARE_BYTES, v, delta); } } } From 2c1335db5293fca5f727d58a69a4b3835b04c591 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 7 Oct 2026 14:25:36 -0300 Subject: [PATCH 11/13] Bound BYTEWISE multiplicity with IS_BYTE and keep EQ multiplicity a bit --- prover/src/tables/bytewise.rs | 50 ++++++++++++++++++++++++++---- prover/src/tables/eq.rs | 27 ++++++++-------- prover/src/tables/trace_builder.rs | 11 +++++++ prover/src/tests/bytewise_tests.rs | 4 +-- prover/src/tests/eq_tests.rs | 13 ++++---- 5 files changed, 77 insertions(+), 28 deletions(-) diff --git a/prover/src/tables/bytewise.rs b/prover/src/tables/bytewise.rs index 2808365c6..f05886c2c 100644 --- a/prover/src/tables/bytewise.rs +++ b/prover/src/tables/bytewise.rs @@ -92,11 +92,16 @@ impl BytewiseOperation { /// Generates the BYTEWISE trace from a list of operations. /// -/// Duplicate operations are merged with summed multiplicities, then padded to -/// the next power of two (minimum 4). -pub fn generate_bytewise_trace( - operations: &[BytewiseOperation], -) -> TraceTable { +/// Largest per-row multiplicity: `μ` is range-checked to a byte on the ARE_BYTES +/// bus (`IS_BYTE[μ]`, weighted by μ), so a row holds at most this many lookups. +/// The bound keeps μ non-negative: without it a `μ = −1` row inverts its byte +/// range checks and can hold an out-of-range byte (carrier). See [`dedup_bytewise_rows`]. +pub const MU_MAX: u64 = (1 << 8) - 1; + +/// Deduplicates BYTEWISE operations into trace rows: `op -> μ`, splitting an op +/// over several rows when its count exceeds [`MU_MAX`]. Shared by trace +/// generation and the BITWISE collector so the per-row lookups cannot drift. +pub fn dedup_bytewise_rows(operations: &[BytewiseOperation]) -> Vec<(BytewiseOperation, u64)> { use std::collections::HashMap; let mut op_map: HashMap = HashMap::new(); @@ -104,7 +109,23 @@ pub fn generate_bytewise_trace( *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + let mut rows = Vec::with_capacity(op_map.len()); + for (op, mut left) in op_map { + while left > 0 { + let mu = left.min(MU_MAX); + left -= mu; + rows.push((op.clone(), mu)); + } + } + rows +} + +/// Duplicate operations are merged with summed multiplicities (split at +/// [`MU_MAX`]), then padded to the next power of two (minimum 4). +pub fn generate_bytewise_trace( + operations: &[BytewiseOperation], +) -> TraceTable { + let unique_ops = dedup_bytewise_rows(operations); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), @@ -132,6 +153,7 @@ pub fn generate_bytewise_trace( /// All bus interactions for the BYTEWISE table: /// - **Sends** `BYTE_ALU[op, a[i], b[i]] -> res[i]` for each of the 8 bytes. +/// - **Sends** `ARE_BYTES[μ, 0]` to bound the multiplicity. /// - **Receives** `ALU[a, b, op] -> res` (operands packed DWordBL -> 2 words). pub fn bus_interactions() -> Vec { let mut interactions = Vec::with_capacity(9); @@ -161,6 +183,22 @@ pub fn bus_interactions() -> Vec { )); } + // ARE_BYTES[μ, 0] | μ. Bounds μ to a byte and keeps it non-negative: the eight + // BYTE_ALU sends above are weighted by μ, so a free μ = −1 would invert them + // and let the row hold an out-of-range byte. The bound rides ARE_BYTES with + // value = weight = μ, so a μ = −1 row lands at `(p−1, 0)` with no receiver. + interactions.push(BusInteraction::sender( + BusId::AreBytes, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: cols::MU, + packing: Packing::Direct, + }, + BusValue::constant(0), + ], + )); + // ALU[a, b, op] -> res (receiver). a/b/res are DWordBL (8 bytes) packed // into 2 words each, matching the CPU's DWordWL operands. interactions.push(BusInteraction::receiver( diff --git a/prover/src/tables/eq.rs b/prover/src/tables/eq.rs index f967becf4..b3287f6d8 100644 --- a/prover/src/tables/eq.rs +++ b/prover/src/tables/eq.rs @@ -113,20 +113,14 @@ impl EqOperation { /// Generates the EQ trace from a list of operations. /// -/// Duplicate operations are merged into a single row with summed multiplicities, -/// then padded to the next power of two (minimum 4). +/// One row per operation (no deduplication), each with `μ = 1`, then padded to +/// the next power of two (minimum 4). Keeping `μ` a bit lets `MuIsBit` +/// (`μ·(1−μ) = 0`) pin it: a free `μ = −1` would invert every bus send (a +/// carrier), and a `μ = 2` would over-answer the ALU lookup. pub fn generate_eq_trace( operations: &[EqOperation], ) -> TraceTable { - use std::collections::HashMap; - - let mut op_map: HashMap = HashMap::new(); - for op in operations { - *op_map.entry(op.clone()).or_insert(0) += 1; - } - - let unique_ops: Vec<_> = op_map.into_iter().collect(); - let num_rows = unique_ops.len().next_power_of_two().max(4); + let num_rows = operations.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), cols::NUM_COLUMNS, @@ -134,7 +128,7 @@ pub fn generate_eq_trace( ); let table = &mut trace.main_table; - for (row_idx, (op, multiplicity)) in unique_ops.iter().enumerate() { + for (row_idx, op) in operations.iter().enumerate() { // a, b as DWordWL (2 words each) table.set_dword_wl(row_idx, cols::A_0, op.a); table.set_dword_wl(row_idx, cols::B_0, op.b); @@ -147,7 +141,7 @@ pub fn generate_eq_trace( table.set_dword_hl(row_idx, cols::DIFF_0, diff); table.set_bool(row_idx, cols::EQ, op.compute_eq()); - table.set_u64(row_idx, cols::MU, *multiplicity); + table.set_u64(row_idx, cols::MU, 1); } trace @@ -249,7 +243,8 @@ pub fn bus_interactions() -> Vec { /// The EQ table's transition constraints as a single [`ConstraintSet`]: /// - idx 0,1: `ADD` pair `b + diff = a` (unconditional); /// - idx 2: `IS_BIT(invert)` (unconditional); -/// - idx 3: `res = eq XOR invert`. +/// - idx 3: `res = eq XOR invert`; +/// - idx 4: `IS_BIT(μ)` — μ is a bit (no dedup), so it cannot invert the bus. #[derive(Clone, Copy)] pub struct EqConstraints; @@ -272,5 +267,9 @@ impl ConstraintSet for EqConstraints { let invert = b.main(0, cols::INVERT); let two = b.const_base(2); b.emit_base(3, res - (eq.clone() + invert.clone() - two * eq * invert)); + // IS_BIT(μ): the table does not deduplicate, so μ ∈ {0, 1}. Without this a + // μ = −1 row would invert every bus send (carrier) and μ = 2 would + // over-answer the ALU lookup. + emit_is_bit(b, 4, cols::MU, None); } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5ecbf57ef..2ce3891eb 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -3335,6 +3335,7 @@ fn build_traces( let branch_chunk = max_rows.branch; let mul_chunk = max_rows.mul; let dvrm_chunk = max_rows.dvrm; + let bytewise_chunk = max_rows.bytewise; // Every source except the two dominant ones (the in-walk lookups and MEMW_R, which are // split into row-ranges in the parallel path below) stays a single whole-source collector. let mut collectors: Vec = vec![ @@ -3347,6 +3348,16 @@ fn build_traces( for op in &bytewise_ops { h.add_ops(&op.collect_bitwise_ops()); } + // IS_BYTE[μ] | μ: each dedup row sends its own μ, μ times (padding + // sends nothing), over exactly the rows `generate_bytewise_trace` + // builds for each chunk. Mirrors the LT/MUL/DVRM/BRANCH bound. + for chunk in bytewise_ops.chunks(bytewise_chunk) { + for (_, mu) in bytewise::dedup_bytewise_rows(chunk) { + let op = + BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, mu as u8); + h.add_ops(&std::iter::repeat_n(op, mu as usize).collect::>()); + } + } }), Box::new(|h| { for op in &eq_ops { diff --git a/prover/src/tests/bytewise_tests.rs b/prover/src/tests/bytewise_tests.rs index ac534cdc2..619679ba2 100644 --- a/prover/src/tests/bytewise_tests.rs +++ b/prover/src/tests/bytewise_tests.rs @@ -70,8 +70,8 @@ fn test_multiplicity_aggregation() { #[test] fn test_bus_interactions_shape() { let interactions = bus_interactions(); - // 8 BYTE_ALU senders + 1 ALU receiver. - assert_eq!(interactions.len(), 9); + // 8 BYTE_ALU senders + 1 ARE_BYTES[μ] sender + 1 ALU receiver. + assert_eq!(interactions.len(), 10); let byte_alu_senders = interactions .iter() diff --git a/prover/src/tests/eq_tests.rs b/prover/src/tests/eq_tests.rs index df0c76fdb..d1495dfb7 100644 --- a/prover/src/tests/eq_tests.rs +++ b/prover/src/tests/eq_tests.rs @@ -73,8 +73,9 @@ fn test_trace_dword_split() { } #[test] -fn test_multiplicity_aggregation() { - // Same op three times + one distinct → 2 unique rows, padded to 4. +fn test_no_dedup_one_row_per_op() { + // No deduplication: each op gets its own row with μ = 1 (μ is kept a bit so + // MuIsBit can pin it). Three identical ops + one distinct → 4 rows. let ops = vec![ EqOperation::new(5, 5, false), EqOperation::new(9, 8, false), @@ -84,15 +85,15 @@ fn test_multiplicity_aggregation() { let trace = generate_eq_trace(&ops); assert_eq!(trace.main_table.height, 4); - let mut found = false; + let mut fives = 0; for row_idx in 0..4 { let row = trace.main_table.get_row(row_idx); + assert_eq!(row[cols::MU], FE::from(1u64), "every real row has μ = 1"); if row[cols::A_0] == FE::from(5u64) && row[cols::B_0] == FE::from(5u64) { - assert_eq!(row[cols::MU], FE::from(3u64)); - found = true; + fives += 1; } } - assert!(found, "expected the (5,5) row with multiplicity 3"); + assert_eq!(fives, 3, "the three (5,5) ops each get their own row"); } #[test] From a4b80837cd05a78e215de5b34ba87752ee9518aa Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 8 Oct 2026 15:30:44 -0300 Subject: [PATCH 12/13] Guard the BYTEWISE multiplicity collector against a zero row cap --- prover/src/tables/trace_builder.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 2ce3891eb..cfe055ef2 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -3351,7 +3351,9 @@ fn build_traces( // IS_BYTE[μ] | μ: each dedup row sends its own μ, μ times (padding // sends nothing), over exactly the rows `generate_bytewise_trace` // builds for each chunk. Mirrors the LT/MUL/DVRM/BRANCH bound. - for chunk in bytewise_ops.chunks(bytewise_chunk) { + // `.max(1)`: `chunks(0)` panics, and `bytewise_chunk` is an + // externally supplied row cap that could be 0. + for chunk in bytewise_ops.chunks(bytewise_chunk.max(1)) { for (_, mu) in bytewise::dedup_bytewise_rows(chunk) { let op = BitwiseOperation::single_byte(BitwiseOperationType::AreBytes, mu as u8); From cb19d79fa53d2be6493ddd43848385d03275a194 Mon Sep 17 00:00:00 2001 From: Nicole Date: Thu, 8 Oct 2026 15:31:36 -0300 Subject: [PATCH 13/13] Treat a prover refusal as inconclusive instead of a rejection in the forgery harness --- prover/src/tests/multiplicity_forgery_poc.rs | 25 ++++++++++---------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/prover/src/tests/multiplicity_forgery_poc.rs b/prover/src/tests/multiplicity_forgery_poc.rs index cc0b86f97..b8bb71689 100644 --- a/prover/src/tests/multiplicity_forgery_poc.rs +++ b/prover/src/tests/multiplicity_forgery_poc.rs @@ -588,19 +588,20 @@ fn assert_honest_verifies(s: &Scenario) { assert!(verifier_accepts(s, &proof), "honest proof must verify"); } -/// Did a crafted proof get accepted? A prover refusal also counts as rejected. +/// Did a crafted proof get accepted by the verifier? The prover must succeed: a +/// prover refusal is not a verifier rejection (a malicious prover skips the +/// honest prover's checks), so an `Err` here means the test cannot conclude the +/// forgery is blocked and must fail loudly rather than pass silently. fn crafted_accepted(s: &Scenario, forge: Forge) -> bool { - match craft_proof(s, forge) { - Ok(proof) => { - assert_eq!( - u64_output(&proof), - s.forged, - "public output must be the forged value" - ); - verifier_accepts(s, &proof) - } - Err(_) => false, - } + let proof = craft_proof(s, forge).expect( + "prover must build the crafted proof; a prover refusal is not a verifier rejection", + ); + assert_eq!( + u64_output(&proof), + s.forged, + "public output must be the forged value" + ); + verifier_accepts(s, &proof) } #[test]