diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index c8568b3d6..97419fa22 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -11,12 +11,12 @@ //! - `timestamp`: DWordWL (64-bit timestamp, 2 cols) //! - `write2/4/8`: Bit (access width flags) //! - `old[8]`: BaseField[8] (previous values at address) -//! - `add_limb_overflow[7]`: Bit[7] (carry flags for base_address + i) +//! - `carry[7]`: Bit[7] (carry flags for base_address + i) //! - `old_timestamp[8]`: DWordWL[8] (previous timestamps, 16 cols) //! - `mu_read`, `mu_write`: multiplicity columns //! //! ## Virtual (computed inline) -//! - `address_add[i]` = (base_address_0 + i+1 - 2^32 * overflow[i], base_address_1 + overflow[i]) +//! - `address_add[i]` = (base_address_0 + i+1 - 2^32 * carry[i], base_address_1 + carry[i]) //! - `w2`: write2 + write4 + write8 (writing at least 2 bytes) //! - `w4`: write4 + write8 (writing at least 4 bytes) //! - `μ_sum`: μ_read + μ_write @@ -25,6 +25,8 @@ //! - 8 LT timestamp checks (old_timestamp[i] < timestamp) //! - 16 Memory bus tokens (read old + write new, per byte) //! - 2 MEMW output interactions (read + write, from CPU) +//! +//! ## Constraints (11 total: 2 custom + 2 IS_BIT for multiplicities + 7 IS_BIT for carry) use math::field::element::FieldElement; use math::field::traits::{IsField, IsSubFieldOf}; @@ -72,8 +74,8 @@ pub mod cols { pub const OLD: [usize; 8] = [16, 17, 18, 19, 20, 21, 22, 23]; // Auxiliary columns - /// add_limb_overflow[7]: Bit columns indicating carry when adding i+1 to base_address_0 - pub const ADD_LIMB_OVERFLOW: [usize; 7] = [24, 25, 26, 27, 28, 29, 30]; + /// carry[7]: Bit columns indicating carry when adding i+1 to base_address_0 + pub const CARRY: [usize; 7] = [24, 25, 26, 27, 28, 29, 30]; /// old_timestamp[8]: each is DWordWL (2 words = 2 columns) /// Total: 8 * 2 = 16 columns @@ -206,11 +208,11 @@ pub fn generate_memw_trace( data[base + cols::OLD[i]] = FE::from(op.old[i]); } - // Auxiliary: add_limb_overflow[7] - // overflow[i] = 1 if (base_address_lo + i+1) >= 2^32 + // Auxiliary: carry[7] + // carry[i] = 1 if (base_address_lo + i+1) >= 2^32 for i in 0..7 { let overflows = base_addr_lo + (i as u64 + 1) >= (1u64 << 32); - data[base + cols::ADD_LIMB_OVERFLOW[i]] = FE::from(overflows as u64); + data[base + cols::CARRY[i]] = FE::from(overflows as u64); } // Auxiliary: old_timestamp[8] - each as DWordWL (2 words) @@ -245,18 +247,17 @@ pub fn bus_interactions() -> Vec { // Memory bus interactions (16 total) // ------------------------------------------------------------------------- // address_add[i] is VIRTUAL: - // lo = base_address_0 + (i+1) - 2^32 * add_limb_overflow[i] - // hi = base_address_1 + add_limb_overflow[i] + // lo = base_address_0 + (i+1) - 2^32 * carry[i] + // hi = base_address_1 + carry[i] // // Safety: `hi` is at most `base_address_1 + 1`. This never reaches 2^32 // because the CPU table splits addresses into (lo, hi) with both halves // in [0, 2^32), and the Memw bus ties MEMW's base_address to the CPU's // value. MEMW only receives accesses where base_address_1 <= 0xFFFF_FFFE // (addresses near u64::MAX are rejected by the executor before proving). - // Consequently, `add_limb_overflow[i]` is implicitly correct: a wrong - // carry bit produces a memory token at a wrong address that has no - // matching PAGE/REGISTER token, causing multiset imbalance and an - // invalid proof. + // Consequently, `carry[i]` is implicitly correct: a wrong carry bit + // produces a memory token at a wrong address that has no matching + // PAGE/REGISTER token, causing multiset imbalance and an invalid proof. // CM8: memory[is_register, base_address, old_timestamp[0], old[0]] with +μ_sum interactions.push(BusInteraction::sender( @@ -323,8 +324,8 @@ pub fn bus_interactions() -> Vec { )); // CM10/11: byte 1, multiplicity w2 = write2 + write4 + write8 - // address_add[0] is virtual: lo = base_address_0 + 1 - 2^32 * overflow[0] - // hi = base_address_1 + overflow[0] + // address_add[0] is virtual: lo = base_address_0 + 1 - 2^32 * carry[0] + // hi = base_address_1 + carry[0] let addr_add_0_lo = BusValue::linear(vec![ LinearTerm::Column { coefficient: 1, @@ -333,7 +334,7 @@ pub fn bus_interactions() -> Vec { LinearTerm::Constant(1), LinearTerm::Column { coefficient: -(1i64 << 32), - column: cols::ADD_LIMB_OVERFLOW[0], + column: cols::CARRY[0], }, ]); let addr_add_0_hi = BusValue::linear(vec![ @@ -343,7 +344,7 @@ pub fn bus_interactions() -> Vec { }, LinearTerm::Column { coefficient: 1, - column: cols::ADD_LIMB_OVERFLOW[0], + column: cols::CARRY[0], }, ]); @@ -401,7 +402,7 @@ pub fn bus_interactions() -> Vec { // CM12/13: bytes 2-3 with multiplicity w4 = write4 + write8 for i in 2..=3 { - let overflow_col = cols::ADD_LIMB_OVERFLOW[i - 1]; + let overflow_col = cols::CARRY[i - 1]; let addr_add_lo = BusValue::linear(vec![ LinearTerm::Column { coefficient: 1, @@ -479,7 +480,7 @@ pub fn bus_interactions() -> Vec { // CM14/15: bytes 4-7 with multiplicity write8 for i in 4..=7 { - let overflow_col = cols::ADD_LIMB_OVERFLOW[i - 1]; + let overflow_col = cols::CARRY[i - 1]; let addr_add_lo = BusValue::linear(vec![ LinearTerm::Column { coefficient: 1, @@ -857,7 +858,7 @@ where } // ========================================================================= -// Constraints (9 total: 2 custom + 7 IS_BIT) +// Constraints (11 total: 2 custom + 2 IS_BIT for multiplicities + 7 IS_BIT for carry) // ========================================================================= /// MEMW table constraint kinds. @@ -946,10 +947,12 @@ impl TransitionConstraint for MemwConstrai /// Creates all constraints for the MEMW table. /// -/// 9 constraints total: +/// 11 constraints total: /// - IS_BIT<μ_sum> (1) /// - w2 => μ_sum (1) -/// - IS_BIT for add_limb_overflow[0..6] (7) +/// - IS_BIT<μ_read> (1) +/// - IS_BIT<μ_write> (1) +/// - IS_BIT for carry[0..6] (7) pub fn constraints() -> Vec>> { let mut constraints: Vec>> = Vec::new(); @@ -970,8 +973,19 @@ pub fn constraints() -> Vec + constraints.push(Box::new(IsBitConstraint::unconditional(cols::MU_READ, idx))); + idx += 1; + + // IS_BIT<μ_write> + constraints.push(Box::new(IsBitConstraint::unconditional( + cols::MU_WRITE, + idx, + ))); + idx += 1; + + // IS_BIT for carry[0..6] + for &col in &cols::CARRY { constraints.push(Box::new(IsBitConstraint::unconditional(col, idx))); idx += 1; } @@ -1013,45 +1027,45 @@ mod tests { } #[test] - fn test_add_limb_overflow() { - // Address 0xFFFF_FFFF should overflow when adding 1 + fn test_carry_flags() { + // Address 0xFFFF_FFFF should carry when adding 1 let op = MemwOperation::new(false, 0xFFFF_FFFF, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); let trace = generate_memw_trace(&[op]); - // All 7 overflow flags should be 1 since 0xFFFF_FFFF + i >= 2^32 for i >= 1 + // All 7 carry flags should be 1 since 0xFFFF_FFFF + i >= 2^32 for i >= 1 for i in 0..7 { - let val = trace.get_main(0, cols::ADD_LIMB_OVERFLOW[i]); - assert_eq!(*val, FE::one(), "overflow[{i}] should be 1"); + let val = trace.get_main(0, cols::CARRY[i]); + assert_eq!(*val, FE::one(), "carry[{i}] should be 1"); } - // Address 0x0000_0000 should not overflow + // Address 0x0000_0000 should not carry let op2 = MemwOperation::new(false, 0x0000_0000, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); let trace2 = generate_memw_trace(&[op2]); for i in 0..7 { - let val = trace2.get_main(0, cols::ADD_LIMB_OVERFLOW[i]); - assert_eq!(*val, FE::zero(), "overflow[{i}] should be 0"); + let val = trace2.get_main(0, cols::CARRY[i]); + assert_eq!(*val, FE::zero(), "carry[{i}] should be 0"); } // Address 0xFFFF_FFFE with width=8 exercises mixed per-byte carry bits: - // overflow[0]=0 (0xFFFF_FFFE+1 = 0xFFFF_FFFF < 2^32) - // overflow[1..6]=1 (0xFFFF_FFFE+2..8 >= 2^32) + // carry[0]=0 (0xFFFF_FFFE+1 = 0xFFFF_FFFF < 2^32) + // carry[1..6]=1 (0xFFFF_FFFE+2..8 >= 2^32) let op3 = MemwOperation::new(false, 0xFFFF_FFFE, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); let trace3 = generate_memw_trace(&[op3]); - let val0 = trace3.get_main(0, cols::ADD_LIMB_OVERFLOW[0]); + let val0 = trace3.get_main(0, cols::CARRY[0]); assert_eq!( *val0, FE::zero(), - "overflow[0] should be 0 for base 0xFFFF_FFFE" + "carry[0] should be 0 for base 0xFFFF_FFFE" ); for i in 1..7 { - let val = trace3.get_main(0, cols::ADD_LIMB_OVERFLOW[i]); + let val = trace3.get_main(0, cols::CARRY[i]); assert_eq!( *val, FE::one(), - "overflow[{i}] should be 1 for base 0xFFFF_FFFE" + "carry[{i}] should be 1 for base 0xFFFF_FFFE" ); } } diff --git a/prover/src/tables/memw_aligned.rs b/prover/src/tables/memw_aligned.rs index 916491dde..0c5746c15 100644 --- a/prover/src/tables/memw_aligned.rs +++ b/prover/src/tables/memw_aligned.rs @@ -4,12 +4,13 @@ //! same old_timestamp. Most operations (aligned memory + all register accesses) //! route here instead of the heavier MEMW table. //! -//! ## Column layout (30 columns) +//! ## Column layout (29 columns) //! //! - `is_register`: Bit -//! - `base_address_high`: Word (32-bit high word) -//! - `base_address_mid`: Half (16-bit mid) -//! - `base_address_low[2]`: Bytes (low 2 bytes) +//! - `base_address[3]`: DWordWHH +//! - `base_address[0]`: Half (low 16 bits) +//! - `base_address[1]`: Half (mid 16 bits) +//! - `base_address[2]`: Word (high 32 bits) //! - `value[8]`: BaseField[8] //! - `timestamp`: DWordWL (2 cols) //! - `write2/4/8`: Bit (access width flags) @@ -18,14 +19,20 @@ //! - `mu_read`, `mu_write`: multiplicity columns //! //! ## Bus Interactions (20) -//! - 1 AND_BYTE[base_address_low[0], mask] → 0 (alignment check) +//! - 1 IS_HALF[base_address[0] + mask] (range check: address span fits in 16 bits) //! - 1 LT[old_timestamp, timestamp, 0] → 1 //! - 16 Memory bus tokens //! - 2 MEMW output interactions (read + write) //! +//! ## Constraints (4 total) +//! - IS_BIT<μ_sum> (1) +//! - w2 => μ_sum (1) +//! - IS_BIT<μ_read> (1) +//! - IS_BIT<μ_write> (1) +//! //! ## Assumptions (caller's responsibility, not enforced here) -//! - MEMW_A-A2: IS_HALF[base_address_mid] -//! - MEMW_A-A3.i: IS_BYTE[base_address_low[i]] for i ∈ [0, 1] +//! - IS_HALF[base_address[i]] for i ∈ [0, 1] +//! - IS_WORD[base_address[2]] use math::field::element::FieldElement; use math::field::traits::{IsField, IsSubFieldOf}; @@ -37,44 +44,43 @@ use stark::traits::TransitionEvaluationContext; use super::memw::MemwOperation; use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField}; +use crate::constraints::templates::IsBitConstraint; /// Maximum number of rows per MEMW_A table chunk. pub const MAX_ROWS: usize = super::max_rows::MEMW_A; // ========================================================================= -// Column indices (30 columns) +// Column indices (29 columns) // ========================================================================= pub mod cols { pub const IS_REGISTER: usize = 0; - /// base_address decomposed: high = addr >> 32 (Word, 32-bit) - pub const BASE_ADDRESS_HIGH: usize = 1; - /// base_address decomposed: mid = (addr >> 16) & 0xFFFF (Half, 16-bit) - pub const BASE_ADDRESS_MID: usize = 2; - /// base_address decomposed: low bytes - /// low[0] = addr & 0xFF, low[1] = (addr >> 8) & 0xFF - pub const BASE_ADDRESS_LOW: [usize; 2] = [3, 4]; + /// base_address: DWordWHH (3 columns) + /// base_address[0] = low half (bits 0-15) + /// base_address[1] = mid half (bits 16-31) + /// base_address[2] = high word (bits 32-63) + pub const BASE_ADDRESS: [usize; 3] = [1, 2, 3]; - pub const VALUE: [usize; 8] = [5, 6, 7, 8, 9, 10, 11, 12]; + pub const VALUE: [usize; 8] = [4, 5, 6, 7, 8, 9, 10, 11]; - pub const TIMESTAMP_0: usize = 13; - pub const TIMESTAMP_1: usize = 14; + pub const TIMESTAMP_0: usize = 12; + pub const TIMESTAMP_1: usize = 13; - pub const WRITE2: usize = 15; - pub const WRITE4: usize = 16; - pub const WRITE8: usize = 17; + pub const WRITE2: usize = 14; + pub const WRITE4: usize = 15; + pub const WRITE8: usize = 16; - pub const OLD: [usize; 8] = [18, 19, 20, 21, 22, 23, 24, 25]; + pub const OLD: [usize; 8] = [17, 18, 19, 20, 21, 22, 23, 24]; /// Single old_timestamp (shared across all bytes, since they're aligned) - pub const OLD_TIMESTAMP_0: usize = 26; - pub const OLD_TIMESTAMP_1: usize = 27; + pub const OLD_TIMESTAMP_0: usize = 25; + pub const OLD_TIMESTAMP_1: usize = 26; - pub const MU_READ: usize = 28; - pub const MU_WRITE: usize = 29; + pub const MU_READ: usize = 27; + pub const MU_WRITE: usize = 28; - pub const NUM_COLUMNS: usize = 30; + pub const NUM_COLUMNS: usize = 29; } // ========================================================================= @@ -96,17 +102,18 @@ pub fn generate_memw_aligned_trace( data[base + cols::IS_REGISTER] = FE::from(op.is_register as u64); - // Decompose base_address + // Decompose base_address as DWordWHH: + // base_address[0] = low half (bits 0-15) + // base_address[1] = mid half (bits 16-31) + // base_address[2] = high word (bits 32-63) let addr = op.base_address; - let high = addr >> 32; - let mid = (addr >> 16) & 0xFFFF; - let low_1 = (addr >> 8) & 0xFF; - let low_0 = addr & 0xFF; + let addr_low_half = addr & 0xFFFF; + let addr_mid_half = (addr >> 16) & 0xFFFF; + let addr_high_word = addr >> 32; - data[base + cols::BASE_ADDRESS_HIGH] = FE::from(high); - data[base + cols::BASE_ADDRESS_MID] = FE::from(mid); - data[base + cols::BASE_ADDRESS_LOW[0]] = FE::from(low_0); - data[base + cols::BASE_ADDRESS_LOW[1]] = FE::from(low_1); + data[base + cols::BASE_ADDRESS[0]] = FE::from(addr_low_half); + data[base + cols::BASE_ADDRESS[1]] = FE::from(addr_mid_half); + data[base + cols::BASE_ADDRESS[2]] = FE::from(addr_high_word); for i in 0..8 { data[base + cols::VALUE[i]] = FE::from(op.value[i]); @@ -145,37 +152,32 @@ 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 - // mask = write2*1 + write4*3 + write8*7 - // This implicitly range-checks low[0] to [0, 256) AND checks alignment. + // IS_HALF[base_address[0] + write2 + 3*write4 + 7*write8] with μ_sum + // Range check: ensures base_address[0] + mask fits in 16 bits, so the + // byte-address span of the access doesn't overflow the low-half field element. + // Alignment itself is the caller's (CPU's) responsibility — see Assumptions above. // ------------------------------------------------------------------------- interactions.push(BusInteraction::sender( - BusId::AndByte, + BusId::IsHalfword, mu_sum.clone(), - vec![ - // x = base_address_low[0] - BusValue::Packed { - start_column: cols::BASE_ADDRESS_LOW[0], - packing: Packing::Direct, + vec![BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::BASE_ADDRESS[0], }, - // y = mask = write2*1 + write4*3 + write8*7 - BusValue::linear(vec![ - LinearTerm::Column { - coefficient: 1, - column: cols::WRITE2, - }, - LinearTerm::Column { - coefficient: 3, - column: cols::WRITE4, - }, - LinearTerm::Column { - coefficient: 7, - column: cols::WRITE8, - }, - ]), - // result = 0 (alignment constraint: low bits must be 0) - BusValue::constant(0), - ], + LinearTerm::Column { + coefficient: 1, + column: cols::WRITE2, + }, + LinearTerm::Column { + coefficient: 3, + column: cols::WRITE4, + }, + LinearTerm::Column { + coefficient: 7, + column: cols::WRITE8, + }, + ])], )); // ------------------------------------------------------------------------- @@ -201,30 +203,24 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // Memory bus interactions (16 total) // ------------------------------------------------------------------------- - // For aligned accesses, address for byte i: - // lo = 2^16 * MID + 2^8 * LOW[1] + LOW[0] + i - // hi = HIGH - // All old_timestamp references use the single old_timestamp columns. + // base_address as DWordWL: + // lo32 = base_address[0] + 2^16 * base_address[1] + // hi32 = base_address[2] + // For aligned accesses, address for byte i: lo32 + i (no carry since aligned) - // Virtual base_address_lo = 2^16 * MID + 2^8 * LOW[1] + LOW[0] - // For byte 0, the address is exactly this. let base_addr_lo = BusValue::linear(vec![ LinearTerm::Column { - coefficient: 1 << 16, - column: cols::BASE_ADDRESS_MID, - }, - LinearTerm::Column { - coefficient: 1 << 8, - column: cols::BASE_ADDRESS_LOW[1], + coefficient: 1, + column: cols::BASE_ADDRESS[0], }, LinearTerm::Column { - coefficient: 1, - column: cols::BASE_ADDRESS_LOW[0], + coefficient: 1 << 16, + column: cols::BASE_ADDRESS[1], }, ]); let base_addr_hi = BusValue::Packed { - start_column: cols::BASE_ADDRESS_HIGH, + start_column: cols::BASE_ADDRESS[2], packing: Packing::Direct, }; @@ -284,20 +280,15 @@ pub fn bus_interactions() -> Vec { let w2_mult = Multiplicity::Sum3(cols::WRITE2, cols::WRITE4, cols::WRITE8); // CM18/19: byte 1 with w2 - // For aligned accesses, adding 1 to the low byte never overflows to hi word - // (since alignment guarantees base_address_lo + width-1 < 2^32). + // For aligned accesses, adding 1 to lo32 never overflows (alignment guarantees it). let addr_1_lo = BusValue::linear(vec![ LinearTerm::Column { - coefficient: 1 << 16, - column: cols::BASE_ADDRESS_MID, - }, - LinearTerm::Column { - coefficient: 1 << 8, - column: cols::BASE_ADDRESS_LOW[1], + coefficient: 1, + column: cols::BASE_ADDRESS[0], }, LinearTerm::Column { - coefficient: 1, - column: cols::BASE_ADDRESS_LOW[0], + coefficient: 1 << 16, + column: cols::BASE_ADDRESS[1], }, LinearTerm::Constant(1), ]); @@ -356,16 +347,12 @@ pub fn bus_interactions() -> Vec { for i in 2..=3 { let addr_i_lo = BusValue::linear(vec![ LinearTerm::Column { - coefficient: 1 << 16, - column: cols::BASE_ADDRESS_MID, - }, - LinearTerm::Column { - coefficient: 1 << 8, - column: cols::BASE_ADDRESS_LOW[1], + coefficient: 1, + column: cols::BASE_ADDRESS[0], }, LinearTerm::Column { - coefficient: 1, - column: cols::BASE_ADDRESS_LOW[0], + coefficient: 1 << 16, + column: cols::BASE_ADDRESS[1], }, LinearTerm::Constant(i as i64), ]); @@ -425,16 +412,12 @@ pub fn bus_interactions() -> Vec { for i in 4..=7 { let addr_i_lo = BusValue::linear(vec![ LinearTerm::Column { - coefficient: 1 << 16, - column: cols::BASE_ADDRESS_MID, - }, - LinearTerm::Column { - coefficient: 1 << 8, - column: cols::BASE_ADDRESS_LOW[1], + coefficient: 1, + column: cols::BASE_ADDRESS[0], }, LinearTerm::Column { - coefficient: 1, - column: cols::BASE_ADDRESS_LOW[0], + coefficient: 1 << 16, + column: cols::BASE_ADDRESS[1], }, LinearTerm::Constant(i as i64), ]); @@ -493,8 +476,6 @@ pub fn bus_interactions() -> Vec { // ------------------------------------------------------------------------- // CO24: Read receiver (from CPU) // ------------------------------------------------------------------------- - // The MEMW output bus fingerprint uses base_address as [lo32, hi32]. - // Reconstruct: lo32 = 2^16*MID + 2^8*LOW[1] + LOW[0], hi32 = HIGH interactions.push(BusInteraction::receiver( BusId::Memw, Multiplicity::Column(cols::MU_READ), @@ -537,7 +518,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::IS_REGISTER, packing: Packing::Direct, }, - // base_address reconstructed as [lo32, hi32] + // base_address as DWordWL: [lo32, hi32] base_addr_lo.clone(), base_addr_hi.clone(), // value[8] @@ -610,7 +591,7 @@ pub fn bus_interactions() -> Vec { start_column: cols::IS_REGISTER, packing: Packing::Direct, }, - // base_address reconstructed + // base_address as DWordWL: [lo32, hi32] base_addr_lo, base_addr_hi, // value[8] @@ -675,7 +656,7 @@ pub fn bus_interactions() -> Vec { } // ========================================================================= -// Constraints (2 algebraic) +// Constraints (4 total) // ========================================================================= /// MEMW_A constraint kinds. @@ -764,7 +745,7 @@ impl TransitionConstraint for MemwAlignedC } } -/// Creates all constraints for the MEMW_A table (2 total). +/// Creates all constraints for the MEMW_A table (4 total). pub fn constraints() -> Vec>> { vec![ Box::new(MemwAlignedConstraint::new( @@ -775,6 +756,8 @@ pub fn constraints() -> Vec= 2); // Check address decomposition for op[1]: addr = 0x1000 - // high = 0, mid = 0, low[1] = 0x10, low[0] = 0x00 - assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS_HIGH), FE::from(0u64)); - assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS_MID), FE::from(0u64)); - assert_eq!( - *trace.get_main(1, cols::BASE_ADDRESS_LOW[1]), - FE::from(0x10u64) - ); + // base_address[0] (low half) = 0x1000 + // base_address[1] (mid half) = 0 + // base_address[2] (high word) = 0 assert_eq!( - *trace.get_main(1, cols::BASE_ADDRESS_LOW[0]), - FE::from(0x00u64) + *trace.get_main(1, cols::BASE_ADDRESS[0]), + FE::from(0x1000u64) ); + assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[1]), FE::from(0u64)); + assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[2]), FE::from(0u64)); } } diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 268d75dee..1bb351583 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -14,7 +14,7 @@ //! ## Memory Tables //! //! - **MEMW**: Memory word read/write table (unaligned/split-timestamp path, 49 cols, 26 interactions) -//! - **MEMW_A**: Memory word read/write table (aligned fast path, 30 cols, 20 interactions) +//! - **MEMW_A**: Memory word read/write table (aligned fast path, 29 cols, 20 interactions) //! - **LOAD**: Memory load with extension table //! - **PAGE**: Paged memory init/final table (one per used page) //! - **REGISTER**: Register init/final table (32 registers × 8 bytes = 256 rows) @@ -51,7 +51,7 @@ pub use types::BusId; /// | Table | Main | Bus | Eff.width | Max rows | /// |---------|------|-----|-----------|----------| /// | MEMW | 49 | 26 | 127 | 2^19 | -/// | MEMW_A | 30 | 20 | 90 | 2^19 * | +/// | MEMW_A | 29 | 20 | 89 | 2^19 * | /// | CPU | 74 | 40 | 194 | 2^19 | /// | DVRM | 34 | 34 | 136 | 2^19 | /// | MUL | 26 | 16 | 74 | 2^20 | @@ -62,7 +62,7 @@ pub use types::BusId; 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) - pub const MEMW_A: usize = 1 << 19; // 524,288 — eff. width 90 + pub const MEMW_A: usize = 1 << 19; // 524,288 — eff. width 89 pub const DVRM: usize = 1 << 19; // 524,288 — eff. width 136 pub const MUL: usize = 1 << 20; // 1,048,576 — eff. width 74 pub const LT: usize = 1 << 21; // 2,097,152 — eff. width 42 diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 6ed876682..14e88942d 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -868,27 +868,34 @@ fn is_aligned_op(op: &MemwOperation) -> bool { /// Collects bitwise lookups from MEMW_A operations. /// /// Per operation: -/// - 1 AND_BYTE for alignment check (low[0] & mask == 0) +/// - 1 IS_HALF for alignment check: IS_HALF[base_address[0] + mask] /// -/// IS_HALFWORD[base_address_mid] and IS_BYTE[base_address_low[1]] are -/// assumptions (MEMW_A-A2, MEMW_A-A3.i) — the caller's (CPU's) responsibility. +/// IS_HALF[base_address[i]] for i ∈ [0, 1] and IS_WORD[base_address[2]] are +/// assumptions — the caller's (CPU's) responsibility. fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec { let mut bitwise_ops = Vec::with_capacity(ops.len()); for op in ops { - let low_0 = (op.base_address & 0xFF) as u8; - let mask: u8 = match op.width { + let low_half = (op.base_address & 0xFFFF) as u32; + let mask: u32 = match op.width { 2 => 1, 4 => 3, 8 => 7, _ => 0, }; - // AND_BYTE[low_0, mask] → expects result 0 - bitwise_ops.push(BitwiseOperation::byte_op( - BitwiseOperationType::AndByte, - low_0, - mask, + // IS_HALF[base_address[0] + mask] + let value = low_half + mask; + debug_assert!( + value <= 0xFFFF, + "misaligned: base_address[0] + mask overflows halfword" + ); + let x = (value & 0xFF) as u8; + let y = ((value >> 8) & 0xFF) as u8; + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + x, + y, )); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index dcc54d935..5186a61b2 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1272,13 +1272,10 @@ fn test_debug_memory_tokens_sb_sh() { let val1 = memw.main_table.get(row, memw_cols::VALUE[1]).to_raw(); let old1 = memw.main_table.get(row, memw_cols::OLD[1]).to_raw(); - // address_add(0) = base + 1, now virtual (computed from base + overflow) - let overflow0 = memw - .main_table - .get(row, memw_cols::ADD_LIMB_OVERFLOW[0]) - .to_raw(); - let addr1_lo = base_lo + 1 - overflow0 * (1u64 << 32); - let addr1_hi = base_hi + overflow0; + // address_add(0) = base + 1, now virtual (computed from base + carry) + let carry0 = memw.main_table.get(row, memw_cols::CARRY[0]).to_raw(); + let addr1_lo = base_lo + 1 - carry0 * (1u64 << 32); + let addr1_hi = base_hi + carry0; // CM16: SEND old token for byte 1 let send_token1: Token = (is_reg, addr1_lo, addr1_hi, old_ts1_lo, old_ts1_hi, old1); diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index ba2de9c3b..542780e51 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -405,16 +405,16 @@ fn test_memw_generated_from_register_ops() { ); // Find the register write to x1 in MEMW_A - // Register address for x1 = 2*1 = 2, decomposed: high=0, mid=0, low=[2,0] + // Register address for x1 = 2*1 = 2, decomposed: base_address[0]=2, base_address[1]=0, base_address[2]=0 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 + // Check for register write: is_register=1, base_address[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::BASE_ADDRESS[0]] == FE::from(2u64) + && row[memw_aligned::cols::BASE_ADDRESS[1]] == FE::zero() + && row[memw_aligned::cols::BASE_ADDRESS[2]] == FE::zero() && row[memw_aligned::cols::MU_WRITE] == FE::one() { // Check value is 300 (lo32 word for register DWordWL packing)