From 8bb18bb53e6ce943ae04b8e90caadff286dbdd53 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 6 Apr 2026 10:11:01 -0300 Subject: [PATCH 01/16] save work --- prover/src/lib.rs | 22 +- prover/src/tables/memw_register.rs | 470 ++++++++++++++++++++++++ prover/src/tables/mod.rs | 6 + prover/src/tables/trace_builder.rs | 85 ++++- prover/src/test_utils.rs | 22 ++ prover/src/tests/prove_elfs_tests.rs | 29 ++ prover/src/tests/trace_builder_tests.rs | 85 ++--- 7 files changed, 662 insertions(+), 57 deletions(-) create mode 100644 prover/src/tables/memw_register.rs diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 2a9d2c912..7cb947f6f 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -41,8 +41,8 @@ use crate::tables::types::BusId; use crate::test_utils::{ E, F, VmAir, create_bitwise_air, create_branch_air, create_commit_air, create_cpu_air, create_decode_air, create_dvrm_air, create_halt_air, create_load_air, create_lt_air, - create_memw_air, create_memw_aligned_air, create_mul_air, create_page_air, create_register_air, - create_shift_air, + create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air, + create_page_air, create_register_air, create_shift_air, }; use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions}; @@ -73,6 +73,7 @@ pub struct TableCounts { pub dvrm: usize, pub shift: usize, pub branch: usize, + pub memw_register: usize, } impl TableCounts { @@ -91,6 +92,7 @@ impl TableCounts { + self.dvrm + self.shift + self.branch + + self.memw_register } /// Validate that all required tables have at least one chunk. @@ -108,6 +110,7 @@ impl TableCounts { ("dvrm", self.dvrm), ("shift", self.shift), ("branch", self.branch), + ("memw_register", self.memw_register), ]; for (name, count) in checks { if count == 0 { @@ -195,6 +198,7 @@ pub(crate) struct VmAirs { pub commit: VmAir, pub register: VmAir, pub pages: Vec, + pub memw_registers: Vec, } impl VmAirs { @@ -242,6 +246,13 @@ impl VmAirs { for (air, trace) in self.pages.iter().zip(traces.pages.iter_mut()) { pairs.push((air, trace, &())); } + for (air, trace) in self + .memw_registers + .iter() + .zip(traces.memw_registers.iter_mut()) + { + pairs.push((air, trace, &())); + } pairs } @@ -286,6 +297,9 @@ impl VmAirs { for air in &self.pages { refs.push(air); } + for air in &self.memw_registers { + refs.push(air); + } refs } @@ -358,6 +372,9 @@ impl VmAirs { ) }) .collect(); + let memw_registers: Vec<_> = (0..table_counts.memw_register) + .map(|i| create_memw_register_air(proof_options).with_name(&format!("MEMW_R[{}]", i))) + .collect(); #[cfg(feature = "debug-checks")] debug_report::print_bus_legend(); @@ -378,6 +395,7 @@ impl VmAirs { commit, register, pages, + memw_registers, } } } diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs new file mode 100644 index 000000000..6810e2400 --- /dev/null +++ b/prover/src/tables/memw_register.rs @@ -0,0 +1,470 @@ +//! MEMW_R (Memory Write/Read -- Register) table. +//! +//! Ultra-slim fast path for register accesses. Registers are always 2 words +//! (DWordWL), always aligned, and `is_register=1`, so this table strips out +//! all memory-specific columns (address decomposition, alignment mask, width +//! flags, per-byte old_timestamps). +//! +//! ## Column layout (10 columns) +//! +//! - `ADDRESS`: Byte (register index 0-31) +//! - `TIMESTAMP_0`: Word (low 32 bits) +//! - `TIMESTAMP_1`: Word (high 32 bits) +//! - `VAL_0`: Word (low 32 bits of register value) +//! - `VAL_1`: Word (high 32 bits of register value) +//! - `OLD_0`: Word (low 32 bits of previous value) +//! - `OLD_1`: Word (high 32 bits of previous value) +//! - `OLD_TIMESTAMP_LO`: Word (low 32 bits of old timestamp; upper limb = TIMESTAMP_1) +//! - `MU_READ`: Bit +//! - `MU_WRITE`: Bit +//! +//! ## Virtual +//! +//! - `old_timestamp = [OLD_TIMESTAMP_LO, TIMESTAMP_1]` (shares upper limb!) +//! - `mu_sum = MU_READ + MU_WRITE` +//! +//! ## Bus Interactions (7) +//! - 1 IS_HALFWORD[timestamp_0 - old_timestamp_lo - 1] +//! - 4 Memory bus tokens (read-old + write-new, per word) +//! - 2 MEMW output interactions (read + write, from CPU) + +use math::field::element::FieldElement; +use math::field::traits::{IsField, IsSubFieldOf}; +use stark::constraints::transition::TransitionConstraint; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::table::TableView; +use stark::trace::TraceTable; +use stark::traits::TransitionEvaluationContext; + +use super::memw::MemwOperation; +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; + +// ========================================================================= +// Column indices (10 columns) +// ========================================================================= + +pub mod cols { + /// Register index (0-31). CPU sends base_address = 2*reg_index. + pub const ADDRESS: usize = 0; + + /// Timestamp low 32 bits + pub const TIMESTAMP_0: usize = 1; + /// Timestamp high 32 bits + pub const TIMESTAMP_1: usize = 2; + + /// Register value low 32 bits + pub const VAL_0: usize = 3; + /// Register value high 32 bits + pub const VAL_1: usize = 4; + + /// Previous value low 32 bits + pub const OLD_0: usize = 5; + /// Previous value high 32 bits + pub const OLD_1: usize = 6; + + /// Old timestamp low 32 bits (upper limb shared with TIMESTAMP_1) + pub const OLD_TIMESTAMP_LO: usize = 7; + + /// Read multiplicity + pub const MU_READ: usize = 8; + /// Write multiplicity + pub const MU_WRITE: usize = 9; + + pub const NUM_COLUMNS: usize = 10; +} + +// ========================================================================= +// Trace generation +// ========================================================================= + +/// Generates the MEMW_R trace table from register operations. +/// +/// Reuses `MemwOperation` -- the trace generator divides `base_address` by 2 +/// to recover the register index (CPU sends `2 * register_index`). +pub fn generate_memw_register_trace( + operations: &[MemwOperation], +) -> TraceTable { + let num_rows = operations.len().next_power_of_two().max(4); + let mut data = vec![FE::zero(); num_rows * cols::NUM_COLUMNS]; + + for (row_idx, op) in operations.iter().enumerate() { + let base = row_idx * cols::NUM_COLUMNS; + + debug_assert_eq!( + op.base_address % 2, + 0, + "register base_address must be even (got {})", + op.base_address + ); + debug_assert_eq!( + op.old_timestamp[0], op.old_timestamp[1], + "register words must share old_timestamp ({} != {})", + op.old_timestamp[0], op.old_timestamp[1] + ); + + // ADDRESS = base_address / 2 (CPU sends 2 * register_index) + data[base + cols::ADDRESS] = FE::from(op.base_address / 2); + + // Timestamp split into lo/hi 32-bit words + data[base + cols::TIMESTAMP_0] = FE::from(op.timestamp & 0xFFFF_FFFF); + data[base + cols::TIMESTAMP_1] = FE::from(op.timestamp >> 32); + + // Value: registers are DWordWL = 2 words + data[base + cols::VAL_0] = FE::from(op.value[0]); + data[base + cols::VAL_1] = FE::from(op.value[1]); + + // Old value + data[base + cols::OLD_0] = FE::from(op.old[0]); + data[base + cols::OLD_1] = FE::from(op.old[1]); + + // Old timestamp low (upper limb shared with TIMESTAMP_1) + data[base + cols::OLD_TIMESTAMP_LO] = FE::from(op.old_timestamp[0] & 0xFFFF_FFFF); + + // Multiplicity + data[base + cols::MU_READ] = FE::from(op.is_read as u64); + data[base + cols::MU_WRITE] = FE::from(!op.is_read as u64); + } + + TraceTable::new_main(data, cols::NUM_COLUMNS, 1) +} + +// ========================================================================= +// Bus interactions (7 total) +// ========================================================================= + +pub fn bus_interactions() -> Vec { + let mut interactions = Vec::with_capacity(7); + + let mu_sum = Multiplicity::Sum(cols::MU_READ, cols::MU_WRITE); + + // ------------------------------------------------------------------------- + // IS_HALFWORD[timestamp_0 - old_timestamp_lo - 1] with mu_sum + // ------------------------------------------------------------------------- + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + mu_sum.clone(), + vec![BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::TIMESTAMP_0, + }, + LinearTerm::Column { + coefficient: -1, + column: cols::OLD_TIMESTAMP_LO, + }, + LinearTerm::Constant(-1), + ])], + )); + + // ------------------------------------------------------------------------- + // Memory bus read-old (sender, for i=0,1) + // memory[is_register=1, addr_lo=2*ADDRESS+i, addr_hi=0, + // OLD_TIMESTAMP_LO, TIMESTAMP_1, OLD[i]] + // ------------------------------------------------------------------------- + for i in 0..2 { + let addr_lo = BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 2, + column: cols::ADDRESS, + }, + LinearTerm::Constant(i as i64), + ]); + + interactions.push(BusInteraction::sender( + BusId::Memory, + mu_sum.clone(), + vec![ + BusValue::constant(1), + addr_lo, + BusValue::constant(0), + BusValue::Packed { + start_column: cols::OLD_TIMESTAMP_LO, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: if i == 0 { cols::OLD_0 } else { cols::OLD_1 }, + packing: Packing::Direct, + }, + ], + )); + } + + // ------------------------------------------------------------------------- + // Memory bus write-new (receiver, for i=0,1) + // memory[is_register=1, addr_lo=2*ADDRESS+i, addr_hi=0, + // TIMESTAMP_0, TIMESTAMP_1, VAL[i]] + // ------------------------------------------------------------------------- + for i in 0..2 { + let addr_lo = BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 2, + column: cols::ADDRESS, + }, + LinearTerm::Constant(i as i64), + ]); + + interactions.push(BusInteraction::receiver( + BusId::Memory, + mu_sum.clone(), + vec![ + BusValue::constant(1), + addr_lo, + BusValue::constant(0), + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: if i == 0 { cols::VAL_0 } else { cols::VAL_1 }, + packing: Packing::Direct, + }, + ], + )); + } + + // ------------------------------------------------------------------------- + // CO24: MEMW read receiver (from CPU M1/M3 sender) + // ------------------------------------------------------------------------- + let addr_lo_linear = BusValue::linear(vec![LinearTerm::Column { + coefficient: 2, + column: cols::ADDRESS, + }]); + + interactions.push(BusInteraction::receiver( + BusId::Memw, + Multiplicity::Column(cols::MU_READ), + vec![ + // old[0..8] + BusValue::Packed { + start_column: cols::OLD_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::OLD_1, + packing: Packing::Direct, + }, + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + // is_register = 1 + BusValue::constant(1), + // base_address = [2*ADDRESS, 0] + addr_lo_linear.clone(), + BusValue::constant(0), + // value[0..8] + BusValue::Packed { + start_column: cols::VAL_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::VAL_1, + packing: Packing::Direct, + }, + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + // timestamp + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + // write flags: write2=1, write4=0, write8=0 (registers are always 2 words) + BusValue::constant(1), + BusValue::constant(0), + BusValue::constant(0), + ], + )); + + // ------------------------------------------------------------------------- + // CO25: MEMW write receiver (from CPU M5/STORE sender) + // ------------------------------------------------------------------------- + interactions.push(BusInteraction::receiver( + BusId::Memw, + Multiplicity::Column(cols::MU_WRITE), + vec![ + // is_register = 1 + BusValue::constant(1), + // base_address = [2*ADDRESS, 0] + addr_lo_linear, + BusValue::constant(0), + // value[0..8] + BusValue::Packed { + start_column: cols::VAL_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::VAL_1, + packing: Packing::Direct, + }, + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + // timestamp + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + // write flags: write2=1, write4=0, write8=0 + BusValue::constant(1), + BusValue::constant(0), + BusValue::constant(0), + ], + )); + + interactions +} + +// ========================================================================= +// Constraints (3 algebraic) +// ========================================================================= + +/// MEMW_R constraint: IS_BIT(mu_sum) = (mu_read + mu_write) * (1 - mu_read - mu_write) = 0 +pub struct MemwRegisterMuSumIsBit { + constraint_idx: usize, +} + +impl MemwRegisterMuSumIsBit { + pub fn new(constraint_idx: usize) -> Self { + Self { constraint_idx } + } + + fn compute(&self, step: &TableView) -> FieldElement + where + F: IsSubFieldOf, + E: IsField, + { + let one = FieldElement::::one(); + let mu_read = step.get_main_evaluation_element(0, cols::MU_READ).clone(); + let mu_write = step.get_main_evaluation_element(0, cols::MU_WRITE).clone(); + let mu_sum = &mu_read + &mu_write; + &mu_sum * (&one - &mu_sum) + } +} + +impl TransitionConstraint for MemwRegisterMuSumIsBit { + fn degree(&self) -> usize { + 2 + } + + fn constraint_idx(&self) -> usize { + self.constraint_idx + } + + fn end_exemptions(&self) -> usize { + 0 + } + + fn evaluate( + &self, + evaluation_context: &TransitionEvaluationContext, + transition_evaluations: &mut [FieldElement], + ) { + match evaluation_context { + TransitionEvaluationContext::Prover { + frame, + periodic_values: _, + rap_challenges: _, + .. + } => { + let v = self.compute(frame.get_evaluation_step(0)); + transition_evaluations[self.constraint_idx] = v.to_extension(); + } + TransitionEvaluationContext::Verifier { + frame, + periodic_values: _, + rap_challenges: _, + .. + } => { + let v = self.compute(frame.get_evaluation_step(0)); + transition_evaluations[self.constraint_idx] = v; + } + } + } +} + +/// Creates all constraints for the MEMW_R table (3 total). +/// +/// - IS_BIT(MU_READ) -- unconditional +/// - IS_BIT(MU_WRITE) -- unconditional +/// - IS_BIT(mu_sum) = (mu_read + mu_write) * (1 - mu_read - mu_write) = 0 +pub fn constraints() -> Vec>> { + use crate::constraints::templates::IsBitConstraint; + + vec![ + Box::new(IsBitConstraint::unconditional(cols::MU_READ, 0)), + Box::new(IsBitConstraint::unconditional(cols::MU_WRITE, 1)), + Box::new(MemwRegisterMuSumIsBit::new(2)), + ] +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_memw_register_trace_generation() { + // Create a simple register op (reg x1 = address 1, so base_address = 2) + let ops = vec![ + MemwOperation::new( + true, // is_register + 2, // base_address = 2 * register_index (reg x1) + [42, 7, 0, 0, 0, 0, 0, 0], + 100, + 2, // width = 2 words (registers are DWordWL) + true, + ) + .with_old([10, 3, 0, 0, 0, 0, 0, 0], [50, 50, 0, 0, 0, 0, 0, 0]), + ]; + + let trace = generate_memw_register_trace(&ops); + assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); + assert!(trace.num_rows() >= 4); // minimum 4 rows + + // ADDRESS = base_address / 2 = 2 / 2 = 1 + assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(1u64)); + + // TIMESTAMP split + assert_eq!(*trace.get_main(0, cols::TIMESTAMP_0), FE::from(100u64)); + assert_eq!(*trace.get_main(0, cols::TIMESTAMP_1), FE::from(0u64)); + + // Values + assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(42u64)); + assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(7u64)); + + // Old values + assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(10u64)); + assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(3u64)); + + // Old timestamp lo + assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(50u64)); + + // Multiplicity: is_read = true => MU_READ=1, MU_WRITE=0 + assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(1u64)); + assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(0u64)); + } +} diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 268d75dee..d9ed155ae 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -32,6 +32,7 @@ pub mod load; pub mod lt; pub mod memw; pub mod memw_aligned; +pub mod memw_register; pub mod mul; pub mod page; pub mod register; @@ -59,6 +60,7 @@ pub use types::BusId; /// | SHIFT | 27 | 15 | 72 | 2^20 | /// | LOAD | 18 | 5 | 33 | 2^21 | /// | BRANCH | 14 | 6 | 32 | 2^21 | +/// | MEMW_R | 10 | 7 | 31 | 2^21 | pub mod max_rows { pub const CPU: usize = 1 << 19; // 524,288 — eff. width 194 pub const MEMW: usize = 1 << 19; // 524,288 — eff. width 127 (baseline) @@ -69,6 +71,7 @@ pub mod max_rows { pub const SHIFT: usize = 1 << 20; // 1,048,576 — eff. width 72 pub const LOAD: usize = 1 << 21; // 2,097,152 — eff. width 33 pub const BRANCH: usize = 1 << 21; // 2,097,152 — eff. width 32 + pub const MEMW_R: usize = 1 << 21; // 2,097,152 — eff. width 31 } /// Per-table maximum row limits, configurable for different environments. @@ -86,6 +89,7 @@ pub struct MaxRowsConfig { pub shift: usize, pub load: usize, pub branch: usize, + pub memw_register: usize, } impl Default for MaxRowsConfig { @@ -100,6 +104,7 @@ impl Default for MaxRowsConfig { shift: max_rows::SHIFT, load: max_rows::LOAD, branch: max_rows::BRANCH, + memw_register: max_rows::MEMW_R, } } } @@ -118,6 +123,7 @@ impl MaxRowsConfig { shift: 1 << 5, load: 1 << 5, branch: 1 << 5, + memw_register: 1 << 5, } } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 6ed876682..03c540d6a 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -10,9 +10,9 @@ //! ```text //! PHASE 0: ELF → DECODE, MEMORY_INIT (preprocessed tables) //! PHASE 1: Logs → CPU ops -//! PHASE 2: CPU ops → MEMW, MEMW_A, LOAD, LT, Bitwise (with state tracking for MEMW/LOAD) -//! PHASE 3: MEMW/MEMW_A → LT ops (timestamp ordering) -//! PHASE 4: LT, MEMW_A → Bitwise lookups +//! PHASE 2: CPU ops → MEMW, MEMW_A, MEMW_R, LOAD, LT, Bitwise (with state tracking for MEMW/LOAD) +//! PHASE 3: MEMW/MEMW_A → LT ops (timestamp ordering); MEMW_R uses IS_HALFWORD instead +//! PHASE 4: LT, MEMW_A, MEMW_R → Bitwise lookups //! PHASE 5: Generate all traces //! ``` //! @@ -44,6 +44,7 @@ use super::load::{self, LoadOperation}; use super::lt::{self, LtOperation}; use super::memw::{self, MemwOperation}; use super::memw_aligned; +use super::memw_register; use super::mul::{self, MulOperation}; use super::page::{self, FinalByteState, FinalStateMap, PageConfig}; use super::register::{self, FinalRegisterStateMap, FinalRegisterWordState}; @@ -895,6 +896,55 @@ fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec old_timestamp[0] (lower limb ordering) +/// 5. timestamp[0] - old_timestamp[0] <= 0xFFFF (delta fits in halfword) +/// +/// Width-1 register ops (e.g. COMMIT x254) stay in MEMW, which has +/// dynamic write flags. MEMW_R hardcodes write2=1. +fn is_register_op(op: &MemwOperation) -> bool { + if !op.is_register || op.width != 2 { + return false; + } + // Both words must share old_timestamp (atomic register write assumption) + if op.old_timestamp[0] != op.old_timestamp[1] { + return false; + } + let ts = op.timestamp; + let old_ts = op.old_timestamp[0]; + let ts_lo = ts & 0xFFFF_FFFF; + let old_ts_lo = old_ts & 0xFFFF_FFFF; + let ts_hi = ts >> 32; + let old_ts_hi = old_ts >> 32; + ts_hi == old_ts_hi && ts_lo > old_ts_lo && (ts_lo - old_ts_lo) <= 0xFFFF +} + +/// Collects IS_HALFWORD bitwise lookups for MEMW_R operations. +/// +/// For each register op: checks that `timestamp[0] - old_timestamp_lo - 1` fits +/// in a halfword (proving the timestamp delta is in range [1, 0xFFFF]). +fn collect_bitwise_from_memw_register(ops: &[MemwOperation]) -> Vec { + ops.iter() + .map(|op| { + let ts_lo = op.timestamp & 0xFFFF_FFFF; + let old_ts_lo = op.old_timestamp[0] & 0xFFFF_FFFF; + let diff_minus_1 = (ts_lo - old_ts_lo - 1) as u16; + BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (diff_minus_1 & 0xFF) as u8, + (diff_minus_1 >> 8) as u8, + ) + }) + .collect() +} + // ============================================================================= // Phase 4: All → Bitwise lookups // ============================================================================= @@ -1562,6 +1612,9 @@ pub struct Traces { /// COMMIT table for write syscall (byte-by-byte commit with recursive bus) pub commit: TraceTable, + + /// MEMW_R register-only fast-path traces (split into chunks of max_rows::MEMW_R) + pub memw_registers: Vec>, } /// Chunk raw ops and generate one trace table per chunk. @@ -1590,6 +1643,7 @@ impl Traces { dvrm: self.dvrms.len(), shift: self.shifts.len(), branch: self.branches.len(), + memw_register: self.memw_registers.len(), } } @@ -1746,7 +1800,10 @@ impl Traces { let halt_memw_ops = collect_halt_ops(&mut register_state); memw_ops.extend(halt_memw_ops); - // Route MEMW operations: aligned ops → MEMW_A, rest → MEMW + // Route MEMW_R (register fast-path) first, then MEMW_A (aligned), rest → MEMW. + // Order matters: register ops would also pass is_aligned_op, so check first. + let (memw_register_ops, memw_ops): (Vec<_>, Vec<_>) = + memw_ops.into_iter().partition(is_register_op); let (memw_aligned_ops, memw_ops): (Vec<_>, Vec<_>) = memw_ops.into_iter().partition(is_aligned_op); @@ -1827,6 +1884,8 @@ impl Traces { bitwise_ops.extend(collect_bitwise_from_branch(&branch_ops)); bitwise_ops.extend(shift::collect_bitwise_from_shift(&shift_ops)); bitwise_ops.extend(collect_bitwise_from_memw_aligned(&memw_aligned_ops)); + // MEMW_R sends IS_HALFWORD[timestamp_0 - old_timestamp_lo - 1] + bitwise_ops.extend(collect_bitwise_from_memw_register(&memw_register_ops)); // PAGE tables do IS_BYTE lookups for init and fini values (C1, C2) bitwise_ops.extend(collect_bitwise_from_page(elf, &memory_state)); @@ -1865,6 +1924,11 @@ impl Traces { max_rows.memw_aligned, memw_aligned::generate_memw_aligned_trace, ); + let memw_registers = chunk_and_generate( + &memw_register_ops, + max_rows.memw_register, + memw_register::generate_memw_register_trace, + ); let loads = chunk_and_generate(&load_ops, max_rows.load, load::generate_load_trace); let lts = chunk_and_generate(<_ops, max_rows.lt, lt::generate_lt_trace); let shifts = chunk_and_generate(&shift_ops, max_rows.shift, shift::generate_shift_trace); @@ -1947,6 +2011,7 @@ impl Traces { branches, halt: halt_trace, commit: commit_trace, + memw_registers, }) } @@ -1982,7 +2047,9 @@ impl Traces { let halt_memw_ops = collect_halt_ops(&mut register_state); memw_ops.extend(halt_memw_ops); - // Route MEMW operations: aligned ops → MEMW_A, rest → MEMW + // Route MEMW_R (register fast-path) first, then MEMW_A (aligned), rest → MEMW. + let (memw_register_ops, memw_ops): (Vec<_>, Vec<_>) = + memw_ops.into_iter().partition(is_register_op); let (memw_aligned_ops, memw_ops): (Vec<_>, Vec<_>) = memw_ops.into_iter().partition(is_aligned_op); @@ -2063,6 +2130,8 @@ impl Traces { bitwise_ops.extend(collect_bitwise_from_branch(&branch_ops)); bitwise_ops.extend(shift::collect_bitwise_from_shift(&shift_ops)); bitwise_ops.extend(collect_bitwise_from_memw_aligned(&memw_aligned_ops)); + // MEMW_R sends IS_HALFWORD[timestamp_0 - old_timestamp_lo - 1] + bitwise_ops.extend(collect_bitwise_from_memw_register(&memw_register_ops)); let public_output_bytes: Vec = commit_ops .iter() @@ -2098,6 +2167,11 @@ impl Traces { max_rows.memw_aligned, memw_aligned::generate_memw_aligned_trace, ); + let memw_registers = chunk_and_generate( + &memw_register_ops, + max_rows.memw_register, + memw_register::generate_memw_register_trace, + ); let loads = chunk_and_generate(&load_ops, max_rows.load, load::generate_load_trace); let lts = chunk_and_generate(<_ops, max_rows.lt, lt::generate_lt_trace); let shifts = chunk_and_generate(&shift_ops, max_rows.shift, shift::generate_shift_trace); @@ -2166,6 +2240,7 @@ impl Traces { branches, halt: halt_trace, commit: commit_trace, + memw_registers, }) } diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 93d6d2971..155af86cb 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -54,6 +54,10 @@ use crate::tables::memw_aligned::{ bus_interactions as memw_aligned_bus_interactions, cols as memw_aligned_cols, constraints as memw_aligned_constraints, }; +use crate::tables::memw_register::{ + bus_interactions as memw_register_bus_interactions, cols as memw_register_cols, + constraints as memw_register_constraints, +}; use crate::tables::mul::{bus_interactions as mul_bus_interactions, cols as mul_cols}; use crate::tables::page::{bus_interactions as page_bus_interactions, cols as page_cols}; use crate::tables::register::{ @@ -576,6 +580,24 @@ pub fn create_memw_aligned_air(proof_options: &ProofOptions) -> VmAir { .with_name("MEMW_A") } +/// Create MEMW_R (register) AIR with constraints and bus interactions. +pub fn create_memw_register_air(proof_options: &ProofOptions) -> VmAir { + let transition_constraints = memw_register_constraints(); + + let auxiliary_trace_build_data = AuxiliaryTraceBuildData { + interactions: memw_register_bus_interactions(), + }; + + AirWithBuses::new( + memw_register_cols::NUM_COLUMNS, + auxiliary_trace_build_data, + proof_options, + 1, + transition_constraints, + ) + .with_name("MEMW_R") +} + /// Create LOAD AIR with constraints and bus interactions. pub fn create_load_air(proof_options: &ProofOptions) -> VmAir { let transition_constraints = load_constraints(); diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index dcc54d935..d847ef536 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1666,6 +1666,33 @@ fn test_heap_alloc_runtime_pages_roundtrip() { ); } +/// Verify that register ops route to MEMW_R and a full prove/verify roundtrip +/// succeeds. Uses `test_add_8` which exercises register reads and writes. +#[test] +fn test_prove_verify_with_memw_register() { + let (elf, logs, instructions) = run_asm_elf("test_add_8"); + let mut traces = + Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); + + // Register ops must go to MEMW_R, not to MEMW_A. + assert!( + !traces.memw_registers.is_empty(), + "register ops should route to MEMW_R: memw_registers must be non-empty" + ); + + // MEMW_A should still have non-register aligned ops (e.g. stack stores). + assert!( + !traces.memw_aligneds.is_empty(), + "MEMW_A should still have aligned non-register ops" + ); + + // Full prove + verify roundtrip. + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "prove/verify should succeed when MEMW_R handles register ops" + ); +} + /// Verify rejects table_counts with all zeros. #[test] fn test_verify_rejects_zero_table_counts() { @@ -1692,6 +1719,7 @@ fn test_verify_rejects_zero_table_counts() { dvrm: 0, shift: 0, branch: 0, + memw_register: 0, }, ..vm_proof }; @@ -1759,6 +1787,7 @@ fn test_crafted_zero_count_proof_must_not_verify() { dvrm: 0, shift: 0, branch: 0, + memw_register: 0, }; let airs = VmAirs::new(&elf, &proof_options, true, &[], &zero_counts); diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index ba2de9c3b..4dd903954 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -3,7 +3,7 @@ use crate::tables::bitwise; use crate::tables::cpu::cols; use crate::tables::lt; -use crate::tables::memw_aligned; +use crate::tables::memw_register; use crate::tables::trace_builder::Traces; use crate::tables::types::FE; use executor::vm::instruction::decoding::{ArithOp, Comparison, Instruction}; @@ -393,43 +393,39 @@ fn test_memw_generated_from_register_ops() { let traces = Traces::from_logs(&logs, instructions, &Default::default()).unwrap(); - // MEMW_A table should have register operations (register ops are always aligned) - // First instruction generates: M1 (read x2), M3 (read x3), M5 (write x1) + // Register ops should route to MEMW_R (memw_registers), not MEMW_A. + // First instruction generates: M1 (read x2), M3 (read x3), M5 (write x1). assert!( - !traces.memw_aligneds.is_empty(), - "MEMW_A should have at least one chunk for register ops" + !traces.memw_registers.is_empty(), + "MEMW_R should have at least one chunk for register ops" ); assert!( - traces.memw_aligneds[0].main_table.height >= 3, - "MEMW_A should have at least 3 rows for register ops" + traces.memw_registers[0].main_table.height >= 3, + "MEMW_R should have at least 3 rows for register ops (reads x2, x3 + write x1)" ); - // Find the register write to x1 in MEMW_A - // Register address for x1 = 2*1 = 2, decomposed: high=0, mid=0, low=[2,0] + // Find the register write to x1 in MEMW_R. + // MEMW_R columns: ADDRESS = register_index (x1 → index 1), + // MU_WRITE = 1 for writes, VAL_0 = value low 32 bits. let mut found_write = false; - for chunk in &traces.memw_aligneds { - for row_idx in 0..chunk.main_table.height { - let row = chunk.main_table.get_row(row_idx); - // Check for register write: is_register=1, base_address_low[0]=2, mu_write=1 - if row[memw_aligned::cols::IS_REGISTER] == FE::one() - && row[memw_aligned::cols::BASE_ADDRESS_LOW[0]] == FE::from(2u64) - && row[memw_aligned::cols::BASE_ADDRESS_MID] == FE::zero() - && row[memw_aligned::cols::BASE_ADDRESS_HIGH] == FE::zero() - && row[memw_aligned::cols::MU_WRITE] == FE::one() - { - // Check value is 300 (lo32 word for register DWordWL packing) - assert_eq!(row[memw_aligned::cols::VALUE[0]], FE::from(300u64)); - found_write = true; - break; - } - } - if found_write { + for row_idx in 0..traces.memw_registers[0].main_table.height { + let row = traces.memw_registers[0].main_table.get_row(row_idx); + // ADDRESS = 1 (x1), MU_WRITE = 1, VAL_0 = 300 + if row[memw_register::cols::ADDRESS] == FE::from(1u64) + && row[memw_register::cols::MU_WRITE] == FE::one() + { + assert_eq!( + row[memw_register::cols::VAL_0], + FE::from(300u64), + "Write value for x1 should be 300" + ); + found_write = true; break; } } assert!( found_write, - "Register write to x1 not found in MEMW_A table" + "Register write to x1 (ADDRESS=1, MU_WRITE=1, VAL_0=300) not found in MEMW_R" ); } @@ -478,31 +474,20 @@ fn test_memw_generates_lt_for_timestamp_ordering() { let traces = Traces::from_logs(&logs, instructions, &Default::default()).unwrap(); - // LT table should have ops from MEMW timestamp ordering - // First instruction: 3 register ops (M1, M3, M5) → at least 3 LT ops for C7 - // Each LT op checks old_timestamp < timestamp - // For first access, old_timestamp=0, timestamp=4, so LT(0, 4) should exist + // Register ops route to MEMW_R (IS_HALFWORD, not LT). + assert!( + !traces.memw_registers.is_empty(), + "Register ops should route to MEMW_R" + ); - // Find LT op with lhs=0, rhs=4 (first register read's timestamp check) - let mut found_timestamp_lt = false; - for row_idx in 0..traces.lts[0].main_table.height { - let row = traces.lts[0].main_table.get_row(row_idx); - // Check for LT(0, 4): lhs=0, rhs=4, signed=0 - if row[lt::cols::LHS_0] == FE::zero() - && row[lt::cols::LHS_1] == FE::zero() - && row[lt::cols::LHS_2] == FE::zero() - && row[lt::cols::RHS_0] == FE::from(4u64) - && row[lt::cols::RHS_1] == FE::zero() - && row[lt::cols::RHS_2] == FE::zero() - && row[lt::cols::SIGNED] == FE::zero() - { - found_timestamp_lt = true; - break; - } - } + // The LT table should still have ops from non-register MEMW accesses + // (e.g. PC next-pc write is a non-register memory op that needs LT). + // Just verify the LT table is non-empty — the exact contents depend on + // which non-register MEMW ops exist in this trace. + let total_lt_rows: usize = traces.lts.iter().map(|t| t.main_table.height).sum(); assert!( - found_timestamp_lt, - "LT op for timestamp ordering (0 < 4) not found" + total_lt_rows > 0, + "LT table should have ops from non-register MEMW timestamp ordering" ); } From c47953db92f3e34463fa6b291af57b23093f1d3f Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 6 Apr 2026 12:01:29 -0300 Subject: [PATCH 02/16] Fix MEMW_R routing predicate to allow timestamp delta = 2^16 --- prover/src/tables/trace_builder.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 03c540d6a..b2f151b9c 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -905,7 +905,7 @@ fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec old_timestamp[0] (lower limb ordering) -/// 5. timestamp[0] - old_timestamp[0] <= 0xFFFF (delta fits in halfword) +/// 5. timestamp[0] - old_timestamp[0] <= 0x10000 (delta fits in IS_HALF range [1, 2^16]) /// /// Width-1 register ops (e.g. COMMIT x254) stay in MEMW, which has /// dynamic write flags. MEMW_R hardcodes write2=1. @@ -923,13 +923,13 @@ fn is_register_op(op: &MemwOperation) -> bool { let old_ts_lo = old_ts & 0xFFFF_FFFF; let ts_hi = ts >> 32; let old_ts_hi = old_ts >> 32; - ts_hi == old_ts_hi && ts_lo > old_ts_lo && (ts_lo - old_ts_lo) <= 0xFFFF + ts_hi == old_ts_hi && ts_lo > old_ts_lo && (ts_lo - old_ts_lo) <= 0x10000 } /// Collects IS_HALFWORD bitwise lookups for MEMW_R operations. /// /// For each register op: checks that `timestamp[0] - old_timestamp_lo - 1` fits -/// in a halfword (proving the timestamp delta is in range [1, 0xFFFF]). +/// in a halfword (proving the timestamp delta is in range [1, 2^16]). fn collect_bitwise_from_memw_register(ops: &[MemwOperation]) -> Vec { ops.iter() .map(|op| { From 07eec950499699b2af11167c0b9b9524ff2455a3 Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 6 Apr 2026 13:04:25 -0300 Subject: [PATCH 03/16] promote old_timestamp assert, add IS_HALF vs LT doc, and expand test coverage --- prover/src/tables/memw_register.rs | 52 ++++++++++++++++++++++++- prover/src/tables/trace_builder.rs | 51 ++++++++++++++++++++++++ prover/src/tests/trace_builder_tests.rs | 12 +++++- 3 files changed, 112 insertions(+), 3 deletions(-) diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 6810e2400..1860656ab 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -5,6 +5,16 @@ //! all memory-specific columns (address decomposition, alignment mask, width //! flags, per-byte old_timestamps). //! +//! ## Timestamp ordering: IS_HALF instead of LT +//! +//! The general MEMW table proves `old_timestamp < timestamp` by routing through +//! the LT table, which requires extra LT trace rows and bus interactions. +//! MEMW_R instead checks `IS_HALF[timestamp[0] - old_timestamp[0] - 1]`, +//! which proves the delta is in `[1, 2^16]` in a single lookup. This is safe +//! because registers are accessed very frequently — their timestamp deltas are +//! almost always small — and the routing predicate (`is_register_op`) enforces +//! the delta fits before admitting an op into this table. +//! //! ## Column layout (10 columns) //! //! - `ADDRESS`: Byte (register index 0-31) @@ -96,7 +106,11 @@ pub fn generate_memw_register_trace( "register base_address must be even (got {})", op.base_address ); - debug_assert_eq!( + // Both register words must have been last accessed at the same timestamp. + // MEMW_R stores a single old_timestamp_lo and shares TIMESTAMP_1 as the + // upper limb, so if the two words differ, the wrong token would be sent + // to the memory bus. The routing predicate enforces this before dispatch. + assert_eq!( op.old_timestamp[0], op.old_timestamp[1], "register words must share old_timestamp ({} != {})", op.old_timestamp[0], op.old_timestamp[1] @@ -467,4 +481,40 @@ mod tests { assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(1u64)); assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(0u64)); } + + #[test] + fn test_memw_register_trace_generation_write_op() { + // Write op: is_read = false => MU_WRITE=1, MU_READ=0 + let ops = vec![ + MemwOperation::new( + true, // is_register + 4, // base_address = 2 * register_index (reg x2) + [99, 55, 0, 0, 0, 0, 0, 0], + 200, + 2, // width = 2 words + false, // is_read = false (write) + ) + .with_old([11, 22, 0, 0, 0, 0, 0, 0], [180, 180, 0, 0, 0, 0, 0, 0]), + ]; + + let trace = generate_memw_register_trace(&ops); + + // ADDRESS = base_address / 2 = 4 / 2 = 2 + assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(2u64)); + + // Values + assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(99u64)); + assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(55u64)); + + // Old values + assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(11u64)); + assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(22u64)); + + // Old timestamp lo + assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(180u64)); + + // Multiplicity: is_read = false => MU_WRITE=1, MU_READ=0 + assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(0u64)); + assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(1u64)); + } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index b2f151b9c..0215aa716 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2292,3 +2292,54 @@ impl Traces { Self::from_logs_trimmed(logs, instructions, max_rows) } } + +#[cfg(test)] +mod routing_tests { + use super::*; + + fn make_register_op(timestamp: u64, old_timestamp: u64) -> MemwOperation { + MemwOperation::new(true, 2, [1, 0, 0, 0, 0, 0, 0, 0], timestamp, 2, false) + .with_old([0; 8], [old_timestamp, old_timestamp, 0, 0, 0, 0, 0, 0]) + } + + #[test] + fn test_is_register_op_delta_at_boundary_routes_in() { + // delta = 0x10000 = 2^16: spec allows this (IS_HALF[0xFFFF] is valid) + let op = make_register_op(0x10000, 0); + assert!(is_register_op(&op), "delta = 2^16 should route to MEMW_R"); + } + + #[test] + fn test_is_register_op_delta_above_boundary_falls_back() { + // delta = 0x10001: one above the IS_HALF range, must fall back to MEMW_A + let op = make_register_op(0x10001, 0); + assert!( + !is_register_op(&op), + "delta = 2^16 + 1 should fall back to MEMW_A" + ); + } + + #[test] + fn test_is_register_op_delta_one_routes_in() { + // delta = 1: minimum allowed value + let op = make_register_op(1, 0); + assert!(is_register_op(&op), "delta = 1 should route to MEMW_R"); + } + + #[test] + fn test_is_register_op_delta_zero_falls_back() { + // delta = 0: ts[0] not strictly greater than old_ts[0] + let op = make_register_op(5, 5); + assert!(!is_register_op(&op), "delta = 0 should not route to MEMW_R"); + } + + #[test] + fn test_is_register_op_upper_limb_mismatch_falls_back() { + // ts_hi != old_ts_hi: shared upper limb assumption violated + let op = make_register_op(0x1_0000_0001, 0x0_0000_0000); + assert!( + !is_register_op(&op), + "different upper limbs should fall back to MEMW_A" + ); + } +} diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 4dd903954..a21f2c273 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -480,10 +480,18 @@ fn test_memw_generates_lt_for_timestamp_ordering() { "Register ops should route to MEMW_R" ); + // Register ops use IS_HALF for timestamp ordering instead of LT. + // Verify the bitwise table has at least one IS_HALF entry with non-zero + // multiplicity, proving that MEMW_R's IS_HALF lookups were emitted. + let has_is_half_entry = (0..traces.bitwise.main_table.height) + .any(|i| traces.bitwise.main_table.get_row(i)[bitwise::cols::MU_IS_HALF] != FE::zero()); + assert!( + has_is_half_entry, + "MEMW_R register ops should produce IS_HALF bitwise entries" + ); + // The LT table should still have ops from non-register MEMW accesses // (e.g. PC next-pc write is a non-register memory op that needs LT). - // Just verify the LT table is non-empty — the exact contents depend on - // which non-register MEMW ops exist in this trace. let total_lt_rows: usize = traces.lts.iter().map(|t| t.main_table.height).sum(); assert!( total_lt_rows > 0, From a5c911c88c69cd1f76d20a8861114b0cd62c1ef0 Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 6 Apr 2026 16:01:51 -0300 Subject: [PATCH 04/16] fix comment --- prover/src/tables/memw_register.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 1860656ab..22565d46d 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -308,7 +308,7 @@ pub fn bus_interactions() -> Vec { )); // ------------------------------------------------------------------------- - // CO25: MEMW write receiver (from CPU M5/STORE sender) + // CO25: MEMW write receiver (from CPU M5 sender — register write to rd) // ------------------------------------------------------------------------- interactions.push(BusInteraction::receiver( BusId::Memw, From 02b1bab75c590698c751f4ce7dea5d5f39d92c91 Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 7 Apr 2026 10:02:52 -0300 Subject: [PATCH 05/16] Add underflow guard and change assert to debug_assert --- prover/src/tables/memw_register.rs | 2 +- prover/src/tables/trace_builder.rs | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 22565d46d..206a9c746 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -110,7 +110,7 @@ pub fn generate_memw_register_trace( // MEMW_R stores a single old_timestamp_lo and shares TIMESTAMP_1 as the // upper limb, so if the two words differ, the wrong token would be sent // to the memory bus. The routing predicate enforces this before dispatch. - assert_eq!( + debug_assert_eq!( op.old_timestamp[0], op.old_timestamp[1], "register words must share old_timestamp ({} != {})", op.old_timestamp[0], op.old_timestamp[1] diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 0215aa716..cbebf4267 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -935,6 +935,10 @@ fn collect_bitwise_from_memw_register(ops: &[MemwOperation]) -> Vec old_ts_lo, + "ts_lo must exceed old_ts_lo (enforced by is_register_op)" + ); let diff_minus_1 = (ts_lo - old_ts_lo - 1) as u16; BitwiseOperation::halfword( BitwiseOperationType::IsHalf, From ef6775b10cf5912e31178dcba6e02d5759626893 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 14:51:11 -0300 Subject: [PATCH 06/16] =?UTF-8?q?docs:=20add=20spec=20and=20plan=20for=20m?= =?UTF-8?q?erged=20bitwise=20bus=20(AND/OR/XOR=20=E2=86=92=20BitwiseByte)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Merges 3 separate byte-level bitwise buses into 1 with op_type discriminant. Reduces CPU interactions from 24 to 8, saving ~8 aux columns. Affects CPU, bitwise, shift, and potentially memw_aligned tables. --- .../plans/2026-04-08-merged-bitwise-bus.md | 288 ++++++++++++++++++ .../2026-04-08-merged-bitwise-bus-design.md | 168 ++++++++++ 2 files changed, 456 insertions(+) create mode 100644 docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md create mode 100644 docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md diff --git a/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md b/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md new file mode 100644 index 000000000..4bd26da7b --- /dev/null +++ b/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md @@ -0,0 +1,288 @@ +# Merged Bitwise Bus Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Merge AndByte/OrByte/XorByte buses into a single BitwiseByte bus with op_type discriminant, reducing CPU interactions from 24 to 8. + +**Architecture:** Replace 3 separate bus IDs with 1. Add a 4th fingerprint field (op_type: 0=AND, 1=OR, 2=XOR). CPU uses `Multiplicity::Sum3(AND, OR, XOR)` and a virtual op_type column. SHIFT and MEMW_A add op_type=0 constant. Bitwise table receivers get op_type constants. + +**Tech Stack:** Rust, lambdaworks STARK framework + +**Spec:** `docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md` + +--- + +### Task 1: Replace BusId variants in types.rs + +**Files:** +- Modify: `prover/src/tables/types.rs` + +- [ ] **Step 1: Find the BusId enum and replace variants** + +Replace `AndByte`, `OrByte`, `XorByte` with `BitwiseByte`. Keep the same +numeric discriminant for `BitwiseByte` (use `AndByte`'s old value = 3). +Renumber any subsequent variants if needed. + +```rust +// Before: +// AndByte = 3, +// OrByte = 4, +// XorByte = 5, + +// After: +BitwiseByte = 3, // Merged AND/OR/XOR byte bus (replaces AndByte, OrByte, XorByte) +``` + +Adjust subsequent discriminant values to fill the gap (or leave gaps — they're +just identifiers). + +- [ ] **Step 2: Fix all compilation errors from removed variants** + +Run `cargo check -p lambda-vm-prover 2>&1 | head -40` to find all references +to the old variant names. Don't fix the logic yet — just note which files +need changes. They should be: `cpu.rs`, `bitwise.rs`, `shift.rs`, and +possibly `memw_aligned.rs`. + +- [ ] **Step 3: Commit** + +```bash +git add prover/src/tables/types.rs +git commit -m "refactor: replace AndByte/OrByte/XorByte BusIds with BitwiseByte" +``` + +(This commit intentionally breaks compilation — subsequent tasks fix it.) + +--- + +### Task 2: Update bitwise table receivers + +**Files:** +- Modify: `prover/src/tables/bitwise.rs` + +- [ ] **Step 1: Update the 3 receiver interactions in `bus_interactions()`** + +Find the 3 `BusInteraction::receiver` calls for `BusId::AndByte`, +`BusId::OrByte`, `BusId::XorByte` (around line 547-605). Replace each with +`BusId::BitwiseByte` and add a 4th bus value for op_type: + +```rust +// AND: [X, Y, AND_result, op_type=0] +BusInteraction::receiver( + BusId::BitwiseByte, + Multiplicity::Column(cols::MU_AND), + vec![ + BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::AND, packing: Packing::Direct }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), + ], +), +// OR: [X, Y, OR_result, op_type=1] +BusInteraction::receiver( + BusId::BitwiseByte, + Multiplicity::Column(cols::MU_OR), + vec![ + BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::OR, packing: Packing::Direct }, + BusValue::Linear(vec![LinearTerm::Constant(1)]), + ], +), +// XOR: [X, Y, XOR_result, op_type=2] +BusInteraction::receiver( + BusId::BitwiseByte, + Multiplicity::Column(cols::MU_XOR), + vec![ + BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, + BusValue::Packed { start_column: cols::XOR, packing: Packing::Direct }, + BusValue::Linear(vec![LinearTerm::Constant(2)]), + ], +), +``` + +- [ ] **Step 2: Commit** + +```bash +git add prover/src/tables/bitwise.rs +git commit -m "feat(bitwise): update receivers to merged BitwiseByte bus with op_type" +``` + +--- + +### Task 3: Update CPU table senders (the main optimization) + +**Files:** +- Modify: `prover/src/tables/cpu.rs` + +- [ ] **Step 1: Replace the three bitwise loops with one merged loop** + +Find the three `for i in 0..8` loops for AND_BYTE, OR_BYTE, XOR_BYTE +interactions (around lines 1026-1096). Replace all three with: + +```rust + // ------------------------------------------------------------------------- + // BITWISE_BYTE interactions (×8, merged AND/OR/XOR) + // ------------------------------------------------------------------------- + // AND, OR, XOR are mutually exclusive per CPU cycle (enforced by DECODE). + // Merged into a single bus with op_type discriminant: + // op_type = 0*AND + 1*OR + 2*XOR + // multiplicity = AND + OR + XOR (at most 1) + for i in 0..8 { + interactions.push(BusInteraction::sender( + BusId::BitwiseByte, + Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), + vec![ + BusValue::Packed { + start_column: cols::ARG1[i], + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::ARG2[i], + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::RES[i], + packing: Packing::Direct, + }, + // op_type: 0=AND, 1=OR, 2=XOR + BusValue::Linear(vec![ + LinearTerm::Column { coefficient: 1, column: cols::OR }, + LinearTerm::Column { coefficient: 2, column: cols::XOR }, + ]), + ], + )); + } +``` + +- [ ] **Step 2: Update interaction count in any doc comments** + +Search for comments mentioning the old count of AND/OR/XOR interactions and +update them. + +- [ ] **Step 3: Commit** + +```bash +git add prover/src/tables/cpu.rs +git commit -m "feat(cpu): merge AND/OR/XOR into 8 BitwiseByte interactions (was 24)" +``` + +--- + +### Task 4: Update SHIFT table senders + +**Files:** +- Modify: `prover/src/tables/shift.rs` + +- [ ] **Step 1: Find all AndByte references in shift.rs** + +There are 3 `BusId::AndByte` sender interactions (around lines 396, 417, 521). +For each, change `BusId::AndByte` → `BusId::BitwiseByte` and add the 4th +bus value: + +```rust +BusValue::Linear(vec![LinearTerm::Constant(0)]), // op_type=0 (AND) +``` + +- [ ] **Step 2: Update trace builder if needed** + +Check `shift.rs` for any `BitwiseOperationType::AndByte` references in trace +generation. These should still work unchanged since the operation type enum +is separate from the BusId. + +- [ ] **Step 3: Commit** + +```bash +git add prover/src/tables/shift.rs +git commit -m "feat(shift): migrate AndByte senders to BitwiseByte with op_type=0" +``` + +--- + +### Task 5: Update MEMW_A table if needed + +**Files:** +- Modify: `prover/src/tables/memw_aligned.rs` (if it still uses AndByte) + +- [ ] **Step 1: Check if MEMW_A still uses AndByte on this branch** + +```bash +grep -n "AndByte" prover/src/tables/memw_aligned.rs +``` + +If yes: change `BusId::AndByte` → `BusId::BitwiseByte` and add op_type=0. +If no (already migrated to IsHalfword): skip this task. + +- [ ] **Step 2: Commit (if changes made)** + +```bash +git add prover/src/tables/memw_aligned.rs +git commit -m "feat(memw_a): migrate AndByte sender to BitwiseByte with op_type=0" +``` + +--- + +### Task 6: Remove old BusId variants and verify compilation + +**Files:** +- Modify: `prover/src/tables/types.rs` (already done in Task 1) + +- [ ] **Step 1: Verify no remaining references to old variants** + +```bash +cargo check -p lambda-vm-prover 2>&1 +``` + +Expected: compiles with no errors. If there are remaining references, +fix them. + +- [ ] **Step 2: Regenerate precomputed bitwise commitment** + +The bitwise table's precomputed commitment is a hardcoded hash. Since the +fingerprints changed (4 fields instead of 3), the commitment must be +regenerated. Find where the commitment is hardcoded and run the commitment +generation tool/test. + +Search for the hardcoded commitment: +```bash +grep -rn "precomputed_commitment\|PRECOMPUTED_COMMITMENT" prover/src/tables/bitwise.rs +``` + +Run the commitment generation (likely a test or script that prints the new +hash). + +- [ ] **Step 3: Commit** + +```bash +git add -A +git commit -m "fix(bitwise): regenerate precomputed commitment for merged bus fingerprints" +``` + +--- + +### Task 7: Verify correctness + +**Files:** No changes — verification only. + +- [ ] **Step 1: Run stark crate tests** + +```bash +cargo test -p stark -- --test-threads=1 +``` + +Expected: all tests pass + +- [ ] **Step 2: Run prover tests (if any are working)** + +```bash +cargo test -p lambda-vm-prover -- --test-threads=1 +``` + +Note: some tests may have pre-existing failures (UnknownSyscall). Focus on +tests that were passing before this change. + +- [ ] **Step 3: Verify CPU aux column count decreased** + +Check the CPU's `num_auxiliary_rap_columns()` or count the bus interactions. +With the merged bus, the CPU should have 16 fewer interactions. After batching +(pairs of 2), this saves ~8 aux columns. diff --git a/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md b/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md new file mode 100644 index 000000000..9aa4f6acd --- /dev/null +++ b/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md @@ -0,0 +1,168 @@ +# Merged Bitwise Bus: AND/OR/XOR Interaction Consolidation + +## Problem + +The CPU table sends 24 bus interactions for bitwise operations: 8 per byte for +each of AND, OR, XOR on separate buses (AndByte, OrByte, XorByte). Since these +operations are mutually exclusive per CPU cycle (enforced via DECODE), 16 of +these 24 interactions always have zero multiplicity. Each interaction adds a +LogUp term column to the CPU's auxiliary trace, inflating the aux width by ~8 +columns (after batching). + +## Goals + +- Merge 3 bitwise buses (AndByte, OrByte, XorByte) into 1 (BitwiseByte) +- Reduce CPU interactions from 24 to 8 for these operations +- Save ~8 CPU aux columns (from ~42 to ~34) +- Keep CPU main columns unchanged (AND/OR/XOR selectors stay) +- Keep bitwise table row count unchanged (2^20) + +## Non-Goals + +- Eliminating AND/OR/XOR selector columns from the CPU (used by DECODE) +- Restructuring the bitwise table layout +- Merging other bitwise bus types (IsHalfword, IsByte, MSB8, etc.) + +## Design + +### Replace Three Buses with One: BitwiseByte + +Replace `BusId::AndByte`, `BusId::OrByte`, and `BusId::XorByte` with a single +`BusId::BitwiseByte`. The message adds an `op_type` discriminant: + +``` +BitwiseByte[X, Y, result, op_type] +``` + +Where `op_type` = 0 (AND), 1 (OR), 2 (XOR). + +**Important:** `AndByte`, `OrByte`, and `XorByte` are used by multiple tables, +not just the CPU: + +| Bus | Senders | +|-----|---------| +| AndByte | CPU (×8), SHIFT (×3), MEMW_A (×1) | +| OrByte | CPU (×8) | +| XorByte | CPU (×8) | + +All senders must migrate to `BitwiseByte` with the appropriate `op_type`. +OrByte and XorByte are CPU-only, so only the CPU changes for those. AndByte +requires updating SHIFT and MEMW_A as well — they add `op_type=0` to their +existing `[X, Y, result]` messages. This is a straightforward addition of one +constant field per interaction. + +### CPU Table Changes + +Replace the three `for i in 0..8` loops (24 interactions) with one loop (8): + +```rust +for i in 0..8 { + interactions.push(BusInteraction::sender( + BusId::BitwiseByte, + Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), + vec![ + BusValue::Packed { start_column: cols::ARG1[i], packing: Packing::Direct }, + BusValue::Packed { start_column: cols::ARG2[i], packing: Packing::Direct }, + BusValue::Packed { start_column: cols::RES[i], packing: Packing::Direct }, + BusValue::linear(vec![ + LinearTerm::Column { coefficient: 1, column: cols::OR }, + LinearTerm::Column { coefficient: 2, column: cols::XOR }, + ]), + ], + )); +} +``` + +- `Multiplicity::Sum3(AND, OR, XOR)` is 0 or 1 per row (mutual exclusivity) +- `op_type` = `0*AND + 1*OR + 2*XOR` (virtual linear column) + +### SHIFT Table Changes + +Replace `BusId::AndByte` with `BusId::BitwiseByte` in all 3 SHIFT interactions. +Add `BusValue::Linear(vec![LinearTerm::Constant(0)])` as the 4th field +(op_type=0 for AND). Multiplicity and other fields stay the same. + +### MEMW_A Table Changes + +Replace `BusId::AndByte` with `BusId::BitwiseByte` in the 1 MEMW_A interaction. +Add `BusValue::Linear(vec![LinearTerm::Constant(0)])` as the 4th field. + +Note: on `feat/memw_r`, MEMW_A may have already replaced AndByte with +IsHalfword (per PR #472). If so, this table needs no changes. Verify at +implementation time. + +### Bitwise Table Changes + +Replace 3 receivers (one per old bus) with 3 receivers on `BitwiseByte`, +distinguished by the constant `op_type` field: + +```rust +// AND: [X, Y, AND_result, op_type=0] +BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_AND), + vec![X, Y, AND, BusValue::Linear(vec![LinearTerm::Constant(0)])]), + +// OR: [X, Y, OR_result, op_type=1] +BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_OR), + vec![X, Y, OR, BusValue::Linear(vec![LinearTerm::Constant(1)])]), + +// XOR: [X, Y, XOR_result, op_type=2] +BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_XOR), + vec![X, Y, XOR, BusValue::Linear(vec![LinearTerm::Constant(2)])]), +``` + +Each receiver keeps its own multiplicity column (MU_AND, MU_OR, MU_XOR). +The `op_type` constant in the fingerprint ensures AND lookups only match +AND receivers. + +### Trace Builder Changes + +The trace builder emits `BitwiseOperation` entries tagged with +`BitwiseOperationType::{AndByte, OrByte, XorByte}`. These types still +map to the same multiplicity columns (MU_AND, MU_OR, MU_XOR) in the bitwise +table. No changes needed to the operation types or multiplicity routing — +only the `BusId` on the constraint side changes. + +### Remove Old BusIds + +After migrating all senders and receivers, remove `AndByte`, `OrByte`, and +`XorByte` from the `BusId` enum. + +## Files Changed + +| File | Change | +|------|--------| +| `prover/src/tables/types.rs` | Add `BitwiseByte`, remove `AndByte`/`OrByte`/`XorByte` | +| `prover/src/tables/cpu.rs` | Replace 24 interactions with 8 | +| `prover/src/tables/bitwise.rs` | Replace 3 receivers with 3 on merged bus + op_type | +| `prover/src/tables/shift.rs` | Update 3 AndByte senders → BitwiseByte + op_type=0 | +| `prover/src/tables/memw_aligned.rs` | Update 1 AndByte sender if still present | + +## Soundness Argument + +1. The `op_type` discriminant (0/1/2) in the fingerprint makes AND/OR/XOR + lookups cryptographically distinct. A send with op_type=0 cannot match a + receiver with op_type=1. + +2. `Multiplicity::Sum3(AND, OR, XOR)` produces 0 or 1 because the flags are + mutually exclusive (enforced by DECODE). + +3. SHIFT and MEMW_A always use op_type=0 (AND) with their existing multiplicity + columns — no soundness change for those tables. + +4. The bitwise table receivers still validate `result = X op Y` for each + op_type. The fingerprint binding ensures no cross-operation forgery. + +## Expected Impact + +- CPU bus interactions: 24 → 8 (saves 16) +- CPU aux columns: ~42 → ~34 (saves ~8 after LogUp batching) +- CPU effective width: ~114 → ~106 +- SHIFT: +1 field per interaction (3 interactions, minor fingerprint cost) +- Bitwise table: same columns, same row count, same 3 receiver count +- Precomputed bitwise commitment: must be regenerated (fingerprints change) + +## Testing + +- All existing prove/verify tests cover correctness +- Verify bus balance with merged interactions +- Verify precomputed bitwise commitment is updated From c4262cc7a92a20d606bc91c95c0d7ce7fe37e79b Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:16:04 -0300 Subject: [PATCH 07/16] refactor(types): merge AndByte/OrByte/XorByte BusId into BitwiseByte Replace three separate BusId variants (AndByte=3, OrByte=4, XorByte=5) with a single BitwiseByte=3 variant using an op_type discriminant field (0=AND, 1=OR, 2=XOR). Renumber subsequent variants accordingly. --- prover/src/tables/types.rs | 49 ++++++++++++++++---------------------- 1 file changed, 21 insertions(+), 28 deletions(-) diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index 8e89490ae..5096fa324 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -53,12 +53,9 @@ pub enum BusId { // ========================================================================= // Bitwise operations (BITWISE table provides) // ========================================================================= - /// Bitwise AND of two bytes: AND_BYTE[X, Y] -> X & Y - AndByte, - /// Bitwise OR of two bytes: OR_BYTE[X, Y] -> X | Y - OrByte, - /// Bitwise XOR of two bytes: XOR_BYTE[X, Y] -> X ^ Y - XorByte, + /// Merged bitwise bus: BITWISE_BYTE[X, Y, result, op_type] where + /// op_type = 0 (AND), 1 (OR), 2 (XOR) + BitwiseByte, /// Most significant bit of a byte: MSB8[X] -> (X >> 7) & 1 Msb8, /// Most significant bit of a halfword: MSB16[X] -> (X >> 15) & 1 @@ -118,9 +115,7 @@ impl BusId { BusId::IsByte => "IsByte", BusId::IsHalfword => "IsHalfword", BusId::IsB20 => "IsB20", - BusId::AndByte => "AndByte", - BusId::OrByte => "OrByte", - BusId::XorByte => "XorByte", + BusId::BitwiseByte => "BitwiseByte", BusId::Msb8 => "Msb8", BusId::Msb16 => "Msb16", BusId::Zero => "Zero", @@ -149,25 +144,23 @@ impl TryFrom for BusId { 0 => Ok(BusId::IsByte), 1 => Ok(BusId::IsHalfword), 2 => Ok(BusId::IsB20), - 3 => Ok(BusId::AndByte), - 4 => Ok(BusId::OrByte), - 5 => Ok(BusId::XorByte), - 6 => Ok(BusId::Msb8), - 7 => Ok(BusId::Msb16), - 8 => Ok(BusId::Zero), - 9 => Ok(BusId::Hwsl), - 10 => Ok(BusId::Lt), - 11 => Ok(BusId::Mul), - 12 => Ok(BusId::Dvrm), - 13 => Ok(BusId::Shift), - 14 => Ok(BusId::Memw), - 15 => Ok(BusId::Load), - 16 => Ok(BusId::Memory), - 17 => Ok(BusId::Branch), - 18 => Ok(BusId::Decode), - 19 => Ok(BusId::Ecall), - 20 => Ok(BusId::CommitNextByte), - 21 => Ok(BusId::Commit), + 3 => Ok(BusId::BitwiseByte), + 4 => Ok(BusId::Msb8), + 5 => Ok(BusId::Msb16), + 6 => Ok(BusId::Zero), + 7 => Ok(BusId::Hwsl), + 8 => Ok(BusId::Lt), + 9 => Ok(BusId::Mul), + 10 => Ok(BusId::Dvrm), + 11 => Ok(BusId::Shift), + 12 => Ok(BusId::Memw), + 13 => Ok(BusId::Load), + 14 => Ok(BusId::Memory), + 15 => Ok(BusId::Branch), + 16 => Ok(BusId::Decode), + 17 => Ok(BusId::Ecall), + 18 => Ok(BusId::CommitNextByte), + 19 => Ok(BusId::Commit), other => Err(other), } } From 3013396ba89f03be6d2140b759c9c18e29885fa0 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:16:53 -0300 Subject: [PATCH 08/16] refactor(bitwise): update receivers to use merged BitwiseByte bus Replace three separate BusId::AndByte/OrByte/XorByte receivers with three BitwiseByte receivers distinguished by a constant op_type field: AND receiver: op_type=0, OR receiver: op_type=1, XOR receiver: op_type=2 MU_AND, MU_OR, MU_XOR multiplicity columns remain separate and unchanged. Adds LinearTerm to import. --- prover/src/tables/bitwise.rs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/prover/src/tables/bitwise.rs b/prover/src/tables/bitwise.rs index 4b1e99d09..6466e09bc 100644 --- a/prover/src/tables/bitwise.rs +++ b/prover/src/tables/bitwise.rs @@ -31,7 +31,7 @@ use std::sync::OnceLock; use math::fft::cpu::bit_reversing::in_place_bit_reverse_permute; use math::polynomial::Polynomial; use stark::config::{BatchedMerkleTree, Commitment}; -use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::proof::options::ProofOptions; use stark::prover::evaluate_polynomial_on_lde_domain; use stark::trace::{TraceTable, columns2rows}; @@ -546,9 +546,9 @@ impl BitwiseOperation { /// in the spec corresponds to receiving lookups from other tables). pub fn bus_interactions() -> Vec { vec![ - // AND_BYTE[X, Y] -> AND + // BITWISE_BYTE[X, Y, AND, op_type=0] -> AND (merged bus, op_type discriminant) BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_AND), vec![ BusValue::Packed { @@ -563,11 +563,12 @@ pub fn bus_interactions() -> Vec { start_column: cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], ), - // OR_BYTE[X, Y] -> OR + // BITWISE_BYTE[X, Y, OR, op_type=1] BusInteraction::receiver( - BusId::OrByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_OR), vec![ BusValue::Packed { @@ -582,11 +583,12 @@ pub fn bus_interactions() -> Vec { start_column: cols::OR, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(1)]), ], ), - // XOR_BYTE[X, Y] -> XOR + // BITWISE_BYTE[X, Y, XOR, op_type=2] BusInteraction::receiver( - BusId::XorByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU_XOR), vec![ BusValue::Packed { @@ -601,6 +603,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::XOR, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(2)]), ], ), // MSB8[X] -> MSB8 From b4634f40bd7801d1ac1aa12f0a25e353a4a93995 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:17:43 -0300 Subject: [PATCH 09/16] refactor(cpu): merge 24 AND/OR/XOR bus interactions into 8 BITWISE_BYTE Replace three separate 8-iteration loops (AND_BYTE, OR_BYTE, XOR_BYTE) with a single merged loop over BitwiseByte using: - Multiplicity::Sum3(AND, OR, XOR) (at most 1 active per cycle) - op_type field: 1*OR + 2*XOR (so AND=0, OR=1, XOR=2) This reduces CPU bus interactions from 24 to 8. AND/OR/XOR are mutually exclusive per cycle (enforced by DECODE), so Sum3 acts as a single active multiplicity. --- prover/src/tables/cpu.rs | 66 ++++++++-------------------------------- 1 file changed, 13 insertions(+), 53 deletions(-) diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index e29ae1d57..ebee264eb 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -42,7 +42,7 @@ //! - STORE ADD: for STORE (res = arg1 + imm, separate from main ADD) //! - SUB: for SUB, BEQ operations //! - LT: for SLT, BLT operations -//! - AND_BYTE, OR_BYTE, XOR_BYTE: for bitwise operations (×8 each) +//! - BITWISE_BYTE: for bitwise operations (×8, merged AND/OR/XOR with op_type discriminant) //! - SHIFT: for shift operations //! - MUL: for multiplication //! - DIVREM: for division/remainder @@ -941,7 +941,7 @@ fn linear_term(bit: u32, column: usize) -> LinearTerm { /// /// The CPU table sends to: /// - DECODE: instruction fetch (every row) -/// - AND_BYTE, OR_BYTE, XOR_BYTE: for bitwise operations (×8 each) +/// - BITWISE_BYTE: for bitwise operations (×8, merged AND/OR/XOR with op_type discriminant) /// /// Note: LT interaction is TODO - needs proper DWordHHW packing to match LT table receiver. pub fn bus_interactions() -> Vec { @@ -1024,60 +1024,16 @@ pub fn bus_interactions() -> Vec { // )); // ------------------------------------------------------------------------- - // AND_BYTE interactions (×8 for each byte) + // BITWISE_BYTE interactions (×8, merged AND/OR/XOR) // ------------------------------------------------------------------------- + // AND, OR, XOR are mutually exclusive per CPU cycle (enforced by DECODE). + // Merged into a single bus with op_type discriminant: + // op_type = 0*AND + 1*OR + 2*XOR + // multiplicity = AND + OR + XOR (at most 1) for i in 0..8 { interactions.push(BusInteraction::sender( - BusId::AndByte, - Multiplicity::Column(cols::AND), - vec![ - BusValue::Packed { - start_column: cols::ARG1[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::ARG2[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES[i], - packing: Packing::Direct, - }, - ], - )); - } - - // ------------------------------------------------------------------------- - // OR_BYTE interactions (×8) - // ------------------------------------------------------------------------- - for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::OrByte, - Multiplicity::Column(cols::OR), - vec![ - BusValue::Packed { - start_column: cols::ARG1[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::ARG2[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES[i], - packing: Packing::Direct, - }, - ], - )); - } - - // ------------------------------------------------------------------------- - // XOR_BYTE interactions (×8) - // ------------------------------------------------------------------------- - for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::XorByte, - Multiplicity::Column(cols::XOR), + BusId::BitwiseByte, + Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), vec![ BusValue::Packed { start_column: cols::ARG1[i], @@ -1091,6 +1047,10 @@ pub fn bus_interactions() -> Vec { start_column: cols::RES[i], packing: Packing::Direct, }, + BusValue::Linear(vec![ + LinearTerm::Column { coefficient: 1, column: cols::OR }, + LinearTerm::Column { coefficient: 2, column: cols::XOR }, + ]), ], )); } From 8feeebd43faf5443cfe3745b8516717615124e3d Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:18:11 -0300 Subject: [PATCH 10/16] refactor(shift): update AndByte senders to BitwiseByte with op_type=0 Update SHIFT-C1, SHIFT-C2, and SHIFT-C11 interactions from BusId::AndByte to BusId::BitwiseByte, adding a constant op_type=0 (AND) as the 4th bus field to match the merged bus protocol. --- prover/src/tables/shift.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/prover/src/tables/shift.rs b/prover/src/tables/shift.rs index bb535c537..f6f4df354 100644 --- a/prover/src/tables/shift.rs +++ b/prover/src/tables/shift.rs @@ -391,9 +391,9 @@ pub fn bus_interactions() -> Vec { ], )); - // SHIFT-C1: AND_BYTE[shift, 15] → bit_shift | left (= μ - direction) + // SHIFT-C1: BITWISE_BYTE[shift, 15, bit_shift, op_type=0(AND)] → bit_shift | left (= μ - direction) interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Diff(cols::MU, cols::DIRECTION), vec![ BusValue::Packed { @@ -405,16 +405,17 @@ pub fn bus_interactions() -> Vec { start_column: cols::BIT_SHIFT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); - // SHIFT-C2: AND_BYTE[256 - zbs * 16 - shift, 15] → bit_shift | right (= direction) + // SHIFT-C2: BITWISE_BYTE[256 - zbs * 16 - shift, 15, bit_shift, op_type=0(AND)] → bit_shift | right (= direction) // 256 - shift would overflow a byte when shift = 0. Subtracting zbs * 16 keeps it in // [0,255]. // When zbs = 1, shift is a multiple of 16 (i.e. shift ∈ [0, 240]), so // 256 - 16 - shift ∈ [0,255]. interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::DIRECTION), vec![ BusValue::linear(vec![ @@ -433,6 +434,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::BIT_SHIFT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); @@ -514,11 +516,11 @@ pub fn bus_interactions() -> Vec { ], )); - // SHIFT-C11: AND_BYTE[encoded_limb; shift, mask] | μ + // SHIFT-C11: BITWISE_BYTE[encoded_limb; shift, mask, op_type=0(AND)] | μ // encoded = (1 - ls[0]) + 15*ls[1] + 31*ls[2] + 47*ls[3] // mask = 48 - 32 * word_instr interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU), vec![ // first input: shift @@ -553,6 +555,8 @@ pub fn bus_interactions() -> Vec { column: cols::LIMB_SHIFT_RAW_2, }, ]), + // op_type = 0 (AND) + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); From 908c68ceca09cccbeb37f7a07d0a3c8c9f2c0463 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:18:18 -0300 Subject: [PATCH 11/16] refactor(memw_aligned): update AndByte sender to BitwiseByte with op_type=0 Update the alignment-check bus interaction from BusId::AndByte to BusId::BitwiseByte, adding a constant op_type=0 (AND) as the 4th field. --- prover/src/tables/memw_aligned.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/memw_aligned.rs b/prover/src/tables/memw_aligned.rs index 916491dde..f01d81fc7 100644 --- a/prover/src/tables/memw_aligned.rs +++ b/prover/src/tables/memw_aligned.rs @@ -145,12 +145,12 @@ pub fn bus_interactions() -> Vec { let mu_sum = Multiplicity::Sum(cols::MU_READ, cols::MU_WRITE); // ------------------------------------------------------------------------- - // AND_BYTE[base_address_low[0], mask] → 0 with μ_sum + // BITWISE_BYTE[base_address_low[0], mask, 0, op_type=0(AND)] with μ_sum // mask = write2*1 + write4*3 + write8*7 // This implicitly range-checks low[0] to [0, 256) AND checks alignment. // ------------------------------------------------------------------------- interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, mu_sum.clone(), vec![ // x = base_address_low[0] @@ -175,6 +175,8 @@ pub fn bus_interactions() -> Vec { ]), // result = 0 (alignment constraint: low bits must be 0) BusValue::constant(0), + // op_type = 0 (AND) + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )); From 495ea6c4c71eebdf81eafc9bc21f7a214ab11722 Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:18:25 -0300 Subject: [PATCH 12/16] refactor(branch): update AndByte sender to BitwiseByte with op_type=0 Update the PC alignment AND_BYTE interaction to BusId::BitwiseByte with a constant op_type=0 (AND) as the 4th bus field. --- prover/src/tables/branch.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index d4ae06cff..127b711df 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -245,10 +245,10 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }], ), - // AND_BYTE[next_pc_low[0]; unmasked_low_byte, 254] + // BITWISE_BYTE[unmasked_low_byte, 254, next_pc_low[0], op_type=0(AND)] // Verifies: next_pc_low[0] = unmasked_low_byte & 0xFE BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(cols::MU), vec![ BusValue::Packed { @@ -260,6 +260,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::NEXT_PC_LOW_0, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], ), // IS_HALFWORD[next_pc_high[0]] From d6ce76dbd126c940bdf62d46b6bc23cb6e8a876e Mon Sep 17 00:00:00 2001 From: diegokingston Date: Wed, 8 Apr 2026 15:18:47 -0300 Subject: [PATCH 13/16] test: update bitwise bus tests to use BitwiseByte with op_type=0 Update standalone bus interaction tests in bitwise_bus_tests.rs and bitwise_tests.rs to use BusId::BitwiseByte with a constant op_type=0 on both sender and receiver sides (both test AND operations). Add LinearTerm to imports where missing. --- prover/src/tests/bitwise_bus_tests.rs | 8 +++++--- prover/src/tests/bitwise_tests.rs | 8 +++++--- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/prover/src/tests/bitwise_bus_tests.rs b/prover/src/tests/bitwise_bus_tests.rs index 6b1e2e98d..71b816b7a 100644 --- a/prover/src/tests/bitwise_bus_tests.rs +++ b/prover/src/tests/bitwise_bus_tests.rs @@ -11,7 +11,7 @@ use math::field::element::FieldElement; use stark::constraints::transition::TransitionConstraint; use stark::lookup::{ - AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, Multiplicity, + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, NullBoundaryConstraintBuilder, Packing, }; use stark::proof::options::ProofOptions; @@ -59,7 +59,7 @@ fn new_sender_air( let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(sender_cols::AND), vec![ BusValue::Packed { @@ -74,6 +74,7 @@ fn new_sender_air( start_column: sender_cols::AND_RESULT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; @@ -94,7 +95,7 @@ fn new_receiver_air( let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(receiver_cols::MU_AND), vec![ BusValue::Packed { @@ -109,6 +110,7 @@ fn new_receiver_air( start_column: receiver_cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; diff --git a/prover/src/tests/bitwise_tests.rs b/prover/src/tests/bitwise_tests.rs index f92f4e946..6430897c8 100644 --- a/prover/src/tests/bitwise_tests.rs +++ b/prover/src/tests/bitwise_tests.rs @@ -381,7 +381,7 @@ mod soundness_tests { use crypto::fiat_shamir::default_transcript::DefaultTranscript; use stark::constraints::transition::TransitionConstraint; use stark::lookup::{ - AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, Multiplicity, + AirWithBuses, AuxiliaryTraceBuildData, BusInteraction, BusValue, LinearTerm, Multiplicity, NullBoundaryConstraintBuilder, Packing, }; use stark::proof::options::ProofOptions; @@ -421,7 +421,7 @@ mod soundness_tests { let transition_constraints: Vec>> = vec![]; let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::sender( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(sender_cols::FLAG), vec![ BusValue::Packed { @@ -436,6 +436,7 @@ mod soundness_tests { start_column: sender_cols::AND_RESULT, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; @@ -472,7 +473,7 @@ mod soundness_tests { let transition_constraints: Vec>> = vec![]; let auxiliary_trace_build_data = AuxiliaryTraceBuildData { interactions: vec![BusInteraction::receiver( - BusId::AndByte, + BusId::BitwiseByte, Multiplicity::Column(receiver_cols::MU_AND), vec![ BusValue::Packed { @@ -487,6 +488,7 @@ mod soundness_tests { start_column: receiver_cols::AND, packing: Packing::Direct, }, + BusValue::Linear(vec![LinearTerm::Constant(0)]), ], )], }; From fe2fe55d9a91d54de501ed0748eb62c65c511835 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 9 Apr 2026 14:36:57 -0300 Subject: [PATCH 14/16] lint --- prover/src/tables/cpu.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index ebee264eb..e0d1bf199 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -1048,8 +1048,14 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }, BusValue::Linear(vec![ - LinearTerm::Column { coefficient: 1, column: cols::OR }, - LinearTerm::Column { coefficient: 2, column: cols::XOR }, + LinearTerm::Column { + coefficient: 1, + column: cols::OR, + }, + LinearTerm::Column { + coefficient: 2, + column: cols::XOR, + }, ]), ], )); From 3a4b92c7901ab8b26da949ac7c08113ca13d220d Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 14 Apr 2026 16:53:04 -0300 Subject: [PATCH 15/16] rm files --- .../plans/2026-04-08-merged-bitwise-bus.md | 288 ------------------ .../2026-04-08-merged-bitwise-bus-design.md | 168 ---------- 2 files changed, 456 deletions(-) delete mode 100644 docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md delete mode 100644 docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md diff --git a/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md b/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md deleted file mode 100644 index 4bd26da7b..000000000 --- a/docs/superpowers/plans/2026-04-08-merged-bitwise-bus.md +++ /dev/null @@ -1,288 +0,0 @@ -# Merged Bitwise Bus Implementation Plan - -> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. - -**Goal:** Merge AndByte/OrByte/XorByte buses into a single BitwiseByte bus with op_type discriminant, reducing CPU interactions from 24 to 8. - -**Architecture:** Replace 3 separate bus IDs with 1. Add a 4th fingerprint field (op_type: 0=AND, 1=OR, 2=XOR). CPU uses `Multiplicity::Sum3(AND, OR, XOR)` and a virtual op_type column. SHIFT and MEMW_A add op_type=0 constant. Bitwise table receivers get op_type constants. - -**Tech Stack:** Rust, lambdaworks STARK framework - -**Spec:** `docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md` - ---- - -### Task 1: Replace BusId variants in types.rs - -**Files:** -- Modify: `prover/src/tables/types.rs` - -- [ ] **Step 1: Find the BusId enum and replace variants** - -Replace `AndByte`, `OrByte`, `XorByte` with `BitwiseByte`. Keep the same -numeric discriminant for `BitwiseByte` (use `AndByte`'s old value = 3). -Renumber any subsequent variants if needed. - -```rust -// Before: -// AndByte = 3, -// OrByte = 4, -// XorByte = 5, - -// After: -BitwiseByte = 3, // Merged AND/OR/XOR byte bus (replaces AndByte, OrByte, XorByte) -``` - -Adjust subsequent discriminant values to fill the gap (or leave gaps — they're -just identifiers). - -- [ ] **Step 2: Fix all compilation errors from removed variants** - -Run `cargo check -p lambda-vm-prover 2>&1 | head -40` to find all references -to the old variant names. Don't fix the logic yet — just note which files -need changes. They should be: `cpu.rs`, `bitwise.rs`, `shift.rs`, and -possibly `memw_aligned.rs`. - -- [ ] **Step 3: Commit** - -```bash -git add prover/src/tables/types.rs -git commit -m "refactor: replace AndByte/OrByte/XorByte BusIds with BitwiseByte" -``` - -(This commit intentionally breaks compilation — subsequent tasks fix it.) - ---- - -### Task 2: Update bitwise table receivers - -**Files:** -- Modify: `prover/src/tables/bitwise.rs` - -- [ ] **Step 1: Update the 3 receiver interactions in `bus_interactions()`** - -Find the 3 `BusInteraction::receiver` calls for `BusId::AndByte`, -`BusId::OrByte`, `BusId::XorByte` (around line 547-605). Replace each with -`BusId::BitwiseByte` and add a 4th bus value for op_type: - -```rust -// AND: [X, Y, AND_result, op_type=0] -BusInteraction::receiver( - BusId::BitwiseByte, - Multiplicity::Column(cols::MU_AND), - vec![ - BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::AND, packing: Packing::Direct }, - BusValue::Linear(vec![LinearTerm::Constant(0)]), - ], -), -// OR: [X, Y, OR_result, op_type=1] -BusInteraction::receiver( - BusId::BitwiseByte, - Multiplicity::Column(cols::MU_OR), - vec![ - BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::OR, packing: Packing::Direct }, - BusValue::Linear(vec![LinearTerm::Constant(1)]), - ], -), -// XOR: [X, Y, XOR_result, op_type=2] -BusInteraction::receiver( - BusId::BitwiseByte, - Multiplicity::Column(cols::MU_XOR), - vec![ - BusValue::Packed { start_column: cols::X, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::Y, packing: Packing::Direct }, - BusValue::Packed { start_column: cols::XOR, packing: Packing::Direct }, - BusValue::Linear(vec![LinearTerm::Constant(2)]), - ], -), -``` - -- [ ] **Step 2: Commit** - -```bash -git add prover/src/tables/bitwise.rs -git commit -m "feat(bitwise): update receivers to merged BitwiseByte bus with op_type" -``` - ---- - -### Task 3: Update CPU table senders (the main optimization) - -**Files:** -- Modify: `prover/src/tables/cpu.rs` - -- [ ] **Step 1: Replace the three bitwise loops with one merged loop** - -Find the three `for i in 0..8` loops for AND_BYTE, OR_BYTE, XOR_BYTE -interactions (around lines 1026-1096). Replace all three with: - -```rust - // ------------------------------------------------------------------------- - // BITWISE_BYTE interactions (×8, merged AND/OR/XOR) - // ------------------------------------------------------------------------- - // AND, OR, XOR are mutually exclusive per CPU cycle (enforced by DECODE). - // Merged into a single bus with op_type discriminant: - // op_type = 0*AND + 1*OR + 2*XOR - // multiplicity = AND + OR + XOR (at most 1) - for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::BitwiseByte, - Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), - vec![ - BusValue::Packed { - start_column: cols::ARG1[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::ARG2[i], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES[i], - packing: Packing::Direct, - }, - // op_type: 0=AND, 1=OR, 2=XOR - BusValue::Linear(vec![ - LinearTerm::Column { coefficient: 1, column: cols::OR }, - LinearTerm::Column { coefficient: 2, column: cols::XOR }, - ]), - ], - )); - } -``` - -- [ ] **Step 2: Update interaction count in any doc comments** - -Search for comments mentioning the old count of AND/OR/XOR interactions and -update them. - -- [ ] **Step 3: Commit** - -```bash -git add prover/src/tables/cpu.rs -git commit -m "feat(cpu): merge AND/OR/XOR into 8 BitwiseByte interactions (was 24)" -``` - ---- - -### Task 4: Update SHIFT table senders - -**Files:** -- Modify: `prover/src/tables/shift.rs` - -- [ ] **Step 1: Find all AndByte references in shift.rs** - -There are 3 `BusId::AndByte` sender interactions (around lines 396, 417, 521). -For each, change `BusId::AndByte` → `BusId::BitwiseByte` and add the 4th -bus value: - -```rust -BusValue::Linear(vec![LinearTerm::Constant(0)]), // op_type=0 (AND) -``` - -- [ ] **Step 2: Update trace builder if needed** - -Check `shift.rs` for any `BitwiseOperationType::AndByte` references in trace -generation. These should still work unchanged since the operation type enum -is separate from the BusId. - -- [ ] **Step 3: Commit** - -```bash -git add prover/src/tables/shift.rs -git commit -m "feat(shift): migrate AndByte senders to BitwiseByte with op_type=0" -``` - ---- - -### Task 5: Update MEMW_A table if needed - -**Files:** -- Modify: `prover/src/tables/memw_aligned.rs` (if it still uses AndByte) - -- [ ] **Step 1: Check if MEMW_A still uses AndByte on this branch** - -```bash -grep -n "AndByte" prover/src/tables/memw_aligned.rs -``` - -If yes: change `BusId::AndByte` → `BusId::BitwiseByte` and add op_type=0. -If no (already migrated to IsHalfword): skip this task. - -- [ ] **Step 2: Commit (if changes made)** - -```bash -git add prover/src/tables/memw_aligned.rs -git commit -m "feat(memw_a): migrate AndByte sender to BitwiseByte with op_type=0" -``` - ---- - -### Task 6: Remove old BusId variants and verify compilation - -**Files:** -- Modify: `prover/src/tables/types.rs` (already done in Task 1) - -- [ ] **Step 1: Verify no remaining references to old variants** - -```bash -cargo check -p lambda-vm-prover 2>&1 -``` - -Expected: compiles with no errors. If there are remaining references, -fix them. - -- [ ] **Step 2: Regenerate precomputed bitwise commitment** - -The bitwise table's precomputed commitment is a hardcoded hash. Since the -fingerprints changed (4 fields instead of 3), the commitment must be -regenerated. Find where the commitment is hardcoded and run the commitment -generation tool/test. - -Search for the hardcoded commitment: -```bash -grep -rn "precomputed_commitment\|PRECOMPUTED_COMMITMENT" prover/src/tables/bitwise.rs -``` - -Run the commitment generation (likely a test or script that prints the new -hash). - -- [ ] **Step 3: Commit** - -```bash -git add -A -git commit -m "fix(bitwise): regenerate precomputed commitment for merged bus fingerprints" -``` - ---- - -### Task 7: Verify correctness - -**Files:** No changes — verification only. - -- [ ] **Step 1: Run stark crate tests** - -```bash -cargo test -p stark -- --test-threads=1 -``` - -Expected: all tests pass - -- [ ] **Step 2: Run prover tests (if any are working)** - -```bash -cargo test -p lambda-vm-prover -- --test-threads=1 -``` - -Note: some tests may have pre-existing failures (UnknownSyscall). Focus on -tests that were passing before this change. - -- [ ] **Step 3: Verify CPU aux column count decreased** - -Check the CPU's `num_auxiliary_rap_columns()` or count the bus interactions. -With the merged bus, the CPU should have 16 fewer interactions. After batching -(pairs of 2), this saves ~8 aux columns. diff --git a/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md b/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md deleted file mode 100644 index 9aa4f6acd..000000000 --- a/docs/superpowers/specs/2026-04-08-merged-bitwise-bus-design.md +++ /dev/null @@ -1,168 +0,0 @@ -# Merged Bitwise Bus: AND/OR/XOR Interaction Consolidation - -## Problem - -The CPU table sends 24 bus interactions for bitwise operations: 8 per byte for -each of AND, OR, XOR on separate buses (AndByte, OrByte, XorByte). Since these -operations are mutually exclusive per CPU cycle (enforced via DECODE), 16 of -these 24 interactions always have zero multiplicity. Each interaction adds a -LogUp term column to the CPU's auxiliary trace, inflating the aux width by ~8 -columns (after batching). - -## Goals - -- Merge 3 bitwise buses (AndByte, OrByte, XorByte) into 1 (BitwiseByte) -- Reduce CPU interactions from 24 to 8 for these operations -- Save ~8 CPU aux columns (from ~42 to ~34) -- Keep CPU main columns unchanged (AND/OR/XOR selectors stay) -- Keep bitwise table row count unchanged (2^20) - -## Non-Goals - -- Eliminating AND/OR/XOR selector columns from the CPU (used by DECODE) -- Restructuring the bitwise table layout -- Merging other bitwise bus types (IsHalfword, IsByte, MSB8, etc.) - -## Design - -### Replace Three Buses with One: BitwiseByte - -Replace `BusId::AndByte`, `BusId::OrByte`, and `BusId::XorByte` with a single -`BusId::BitwiseByte`. The message adds an `op_type` discriminant: - -``` -BitwiseByte[X, Y, result, op_type] -``` - -Where `op_type` = 0 (AND), 1 (OR), 2 (XOR). - -**Important:** `AndByte`, `OrByte`, and `XorByte` are used by multiple tables, -not just the CPU: - -| Bus | Senders | -|-----|---------| -| AndByte | CPU (×8), SHIFT (×3), MEMW_A (×1) | -| OrByte | CPU (×8) | -| XorByte | CPU (×8) | - -All senders must migrate to `BitwiseByte` with the appropriate `op_type`. -OrByte and XorByte are CPU-only, so only the CPU changes for those. AndByte -requires updating SHIFT and MEMW_A as well — they add `op_type=0` to their -existing `[X, Y, result]` messages. This is a straightforward addition of one -constant field per interaction. - -### CPU Table Changes - -Replace the three `for i in 0..8` loops (24 interactions) with one loop (8): - -```rust -for i in 0..8 { - interactions.push(BusInteraction::sender( - BusId::BitwiseByte, - Multiplicity::Sum3(cols::AND, cols::OR, cols::XOR), - vec![ - BusValue::Packed { start_column: cols::ARG1[i], packing: Packing::Direct }, - BusValue::Packed { start_column: cols::ARG2[i], packing: Packing::Direct }, - BusValue::Packed { start_column: cols::RES[i], packing: Packing::Direct }, - BusValue::linear(vec![ - LinearTerm::Column { coefficient: 1, column: cols::OR }, - LinearTerm::Column { coefficient: 2, column: cols::XOR }, - ]), - ], - )); -} -``` - -- `Multiplicity::Sum3(AND, OR, XOR)` is 0 or 1 per row (mutual exclusivity) -- `op_type` = `0*AND + 1*OR + 2*XOR` (virtual linear column) - -### SHIFT Table Changes - -Replace `BusId::AndByte` with `BusId::BitwiseByte` in all 3 SHIFT interactions. -Add `BusValue::Linear(vec![LinearTerm::Constant(0)])` as the 4th field -(op_type=0 for AND). Multiplicity and other fields stay the same. - -### MEMW_A Table Changes - -Replace `BusId::AndByte` with `BusId::BitwiseByte` in the 1 MEMW_A interaction. -Add `BusValue::Linear(vec![LinearTerm::Constant(0)])` as the 4th field. - -Note: on `feat/memw_r`, MEMW_A may have already replaced AndByte with -IsHalfword (per PR #472). If so, this table needs no changes. Verify at -implementation time. - -### Bitwise Table Changes - -Replace 3 receivers (one per old bus) with 3 receivers on `BitwiseByte`, -distinguished by the constant `op_type` field: - -```rust -// AND: [X, Y, AND_result, op_type=0] -BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_AND), - vec![X, Y, AND, BusValue::Linear(vec![LinearTerm::Constant(0)])]), - -// OR: [X, Y, OR_result, op_type=1] -BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_OR), - vec![X, Y, OR, BusValue::Linear(vec![LinearTerm::Constant(1)])]), - -// XOR: [X, Y, XOR_result, op_type=2] -BusInteraction::receiver(BusId::BitwiseByte, Multiplicity::Column(cols::MU_XOR), - vec![X, Y, XOR, BusValue::Linear(vec![LinearTerm::Constant(2)])]), -``` - -Each receiver keeps its own multiplicity column (MU_AND, MU_OR, MU_XOR). -The `op_type` constant in the fingerprint ensures AND lookups only match -AND receivers. - -### Trace Builder Changes - -The trace builder emits `BitwiseOperation` entries tagged with -`BitwiseOperationType::{AndByte, OrByte, XorByte}`. These types still -map to the same multiplicity columns (MU_AND, MU_OR, MU_XOR) in the bitwise -table. No changes needed to the operation types or multiplicity routing — -only the `BusId` on the constraint side changes. - -### Remove Old BusIds - -After migrating all senders and receivers, remove `AndByte`, `OrByte`, and -`XorByte` from the `BusId` enum. - -## Files Changed - -| File | Change | -|------|--------| -| `prover/src/tables/types.rs` | Add `BitwiseByte`, remove `AndByte`/`OrByte`/`XorByte` | -| `prover/src/tables/cpu.rs` | Replace 24 interactions with 8 | -| `prover/src/tables/bitwise.rs` | Replace 3 receivers with 3 on merged bus + op_type | -| `prover/src/tables/shift.rs` | Update 3 AndByte senders → BitwiseByte + op_type=0 | -| `prover/src/tables/memw_aligned.rs` | Update 1 AndByte sender if still present | - -## Soundness Argument - -1. The `op_type` discriminant (0/1/2) in the fingerprint makes AND/OR/XOR - lookups cryptographically distinct. A send with op_type=0 cannot match a - receiver with op_type=1. - -2. `Multiplicity::Sum3(AND, OR, XOR)` produces 0 or 1 because the flags are - mutually exclusive (enforced by DECODE). - -3. SHIFT and MEMW_A always use op_type=0 (AND) with their existing multiplicity - columns — no soundness change for those tables. - -4. The bitwise table receivers still validate `result = X op Y` for each - op_type. The fingerprint binding ensures no cross-operation forgery. - -## Expected Impact - -- CPU bus interactions: 24 → 8 (saves 16) -- CPU aux columns: ~42 → ~34 (saves ~8 after LogUp batching) -- CPU effective width: ~114 → ~106 -- SHIFT: +1 field per interaction (3 interactions, minor fingerprint cost) -- Bitwise table: same columns, same row count, same 3 receiver count -- Precomputed bitwise commitment: must be regenerated (fingerprints change) - -## Testing - -- All existing prove/verify tests cover correctness -- Verify bus balance with merged interactions -- Verify precomputed bitwise commitment is updated From a2f4bef98bfd425f29aadf762de62b8e41282355 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 14 Apr 2026 18:03:37 -0300 Subject: [PATCH 16/16] Fix hardcoded BusId for Memory --- prover/src/tests/prove_elfs_tests.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 9a1b8a6d0..43f1db821 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1004,7 +1004,7 @@ fn test_debug_memory_bus_tokens() { let z: i128 = 1000; let alpha: i128 = 2; - let bus_id: i128 = 17; // BusId::Memory + let bus_id: i128 = 14; // BusId::Memory // Compute fingerprint for a token let fingerprint =