From eaff46e884825cde5034815951328617b2ef191a Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Wed, 25 Mar 2026 11:21:33 -0300 Subject: [PATCH 1/3] update cpu table --- prover/src/constraints/cpu.rs | 86 +++++++++++++------------ prover/src/tables/cpu.rs | 90 ++++++++++++++------------- prover/src/tests/constraints_tests.rs | 14 ++--- prover/src/tests/cpu_tests.rs | 4 +- 4 files changed, 102 insertions(+), 92 deletions(-) diff --git a/prover/src/constraints/cpu.rs b/prover/src/constraints/cpu.rs index 1f0ec3744..f1d9b0304 100644 --- a/prover/src/constraints/cpu.rs +++ b/prover/src/constraints/cpu.rs @@ -86,9 +86,9 @@ pub const BIT_FLAG_COLUMNS: &[usize] = &[ cols::ECALL, cols::EBREAK, // Sign bits - cols::RV1_SIGN_BIT, - cols::ARG2_SIGN_BIT, - cols::RES_SIGN_BIT, + cols::RV1_EXT_BIT, + cols::RV2_EXT_BIT, + cols::RES_EXT_BIT, // Computed flags cols::IS_EQUAL, cols::BRANCH_COND, @@ -391,7 +391,7 @@ impl TransitionConstraint for Arg1LowerCon } } -/// Constraint: arg1[4:8] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_sign_bit * signed +/// Constraint: arg1[4:8] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_ext_bit * signed /// /// Upper 32 bits of arg1 depends on word_instr and sign extension. pub struct Arg1UpperConstraint { @@ -418,15 +418,15 @@ impl Arg1UpperConstraint { .get_main_evaluation_element(0, cols::WORD_INSTR) .clone(); let signed = step.get_main_evaluation_element(0, cols::SIGNED).clone(); - let rv1_sign_bit = step - .get_main_evaluation_element(0, cols::RV1_SIGN_BIT) + let rv1_ext_bit = step + .get_main_evaluation_element(0, cols::RV1_EXT_BIT) .clone(); let one = FieldElement::::one(); let mask_32: FieldElement = FieldElement::from((1u64 << 32) - 1); // 2^32 - 1 - // Expected: rv1_upper * (1 - word_instr) + mask_32 * rv1_sign_bit * signed - let expected = rv1_upper * (one - &word_instr) + mask_32 * rv1_sign_bit * signed; + // Expected: rv1_upper * (1 - word_instr) + mask_32 * rv1_ext_bit * signed + let expected = rv1_upper * (one - &word_instr) + mask_32 * rv1_ext_bit * signed; // Constraint: arg1_hi - expected = 0 arg1_hi - expected @@ -435,7 +435,7 @@ impl Arg1UpperConstraint { impl TransitionConstraint for Arg1UpperConstraint { fn degree(&self) -> usize { - // rv1_sign_bit * signed * word_instr has degree 3 + // rv1_ext_bit * signed * word_instr has degree 3 3 } @@ -569,19 +569,25 @@ pub fn create_slt_res_zero_constraints( } // ========================================================================= -// Sign Bit Constraints +// Extension Bit Constraints (SIGN template from spec) // ========================================================================= -/// Constraint: sign bits are zero when word_instr = 0 +/// Constraint: ext_bit must be zero when word_instr = 0 /// -/// (rv1_sign_bit + arg2_sign_bit + res_sign_bit) * (1 - word_instr) = 0 -pub struct SignBitZeroConstraint { +/// (1 - word_instr) * ext_bit = 0 +/// +/// One instance per extension bit (rv1_ext_bit, rv2_ext_bit, res_ext_bit). +pub struct ExtBitZeroConstraint { constraint_idx: usize, + ext_bit_col: usize, } -impl SignBitZeroConstraint { - pub fn new(constraint_idx: usize) -> Self { - Self { constraint_idx } +impl ExtBitZeroConstraint { + pub fn new(constraint_idx: usize, ext_bit_col: usize) -> Self { + Self { + constraint_idx, + ext_bit_col, + } } fn compute(&self, step: &TableView) -> FieldElement @@ -589,14 +595,8 @@ impl SignBitZeroConstraint { F: IsSubFieldOf, E: IsField, { - let rv1_sign_bit = step - .get_main_evaluation_element(0, cols::RV1_SIGN_BIT) - .clone(); - let arg2_sign_bit = step - .get_main_evaluation_element(0, cols::ARG2_SIGN_BIT) - .clone(); - let res_sign_bit = step - .get_main_evaluation_element(0, cols::RES_SIGN_BIT) + let ext_bit = step + .get_main_evaluation_element(0, self.ext_bit_col) .clone(); let word_instr = step .get_main_evaluation_element(0, cols::WORD_INSTR) @@ -604,12 +604,12 @@ impl SignBitZeroConstraint { let one = FieldElement::::one(); - // (sum of sign bits) * (1 - word_instr) = 0 - (rv1_sign_bit + arg2_sign_bit + res_sign_bit) * (one - word_instr) + // (1 - word_instr) * ext_bit = 0 + (one - word_instr) * ext_bit } } -impl TransitionConstraint for SignBitZeroConstraint { +impl TransitionConstraint for ExtBitZeroConstraint { fn degree(&self) -> usize { 2 } @@ -874,7 +874,7 @@ impl TransitionConstraint for Arg2LowerCon } } -/// Constraint: arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*arg2_sign_bit*(2^32-1)) + (1-BEQ-BLT-STORE)*imm[1] +/// Constraint: arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*rv2_ext_bit*(2^32-1)) + (1-BEQ-BLT-STORE)*imm[1] /// /// arg2 upper 32 bits with sign extension logic. pub struct Arg2UpperConstraint { @@ -912,13 +912,13 @@ impl Arg2UpperConstraint { let blt = step.get_main_evaluation_element(0, cols::BLT); let word_instr = step.get_main_evaluation_element(0, cols::WORD_INSTR); let signed = step.get_main_evaluation_element(0, cols::SIGNED); - let arg2_sign_bit = step.get_main_evaluation_element(0, cols::ARG2_SIGN_BIT); + let rv2_ext_bit = step.get_main_evaluation_element(0, cols::RV2_EXT_BIT); let one = FieldElement::::one(); let mask_32: FieldElement = FieldElement::from((1u64 << 32) - 1); - // rv2_term = (1 - word_instr) * rv2[2] + signed * arg2_sign_bit * (2^32 - 1) - let rv2_term = (&one - word_instr) * rv2_upper + signed * arg2_sign_bit * &mask_32; + // rv2_term = (1 - word_instr) * rv2[2] + signed * rv2_ext_bit * (2^32 - 1) + let rv2_term = (&one - word_instr) * rv2_upper + signed * rv2_ext_bit * &mask_32; // expected = (1-LOAD) * rv2_term + (1-BEQ-BLT-STORE) * imm[1] // STORE now gets rv2_term (with sign extension), not imm @@ -931,7 +931,7 @@ impl Arg2UpperConstraint { impl TransitionConstraint for Arg2UpperConstraint { fn degree(&self) -> usize { - // (1-LOAD) * signed * arg2_sign_bit has degree 3 + // (1-LOAD) * signed * rv2_ext_bit has degree 3 3 } @@ -1029,7 +1029,7 @@ impl TransitionConstraint for RvdLowerCons } } -/// Constraint: (1-LOAD) * (rvd[1] - ((1-word_instr)*res[4:] + res_sign_bit*(2^32-1))) = 0 +/// Constraint: (1-LOAD) * (rvd[1] - ((1-word_instr)*res[4:] + res_ext_bit*(2^32-1))) = 0 /// /// When not LOAD, rvd upper 32 bits equals res upper with sign extension. /// For LOAD: rvd is the loaded value, not res (which is the address). @@ -1056,13 +1056,13 @@ impl RvdUpperConstraint { let load = step.get_main_evaluation_element(0, cols::LOAD); let word_instr = step.get_main_evaluation_element(0, cols::WORD_INSTR); - let res_sign_bit = step.get_main_evaluation_element(0, cols::RES_SIGN_BIT); + let res_ext_bit = step.get_main_evaluation_element(0, cols::RES_EXT_BIT); let one = FieldElement::::one(); let mask_32: FieldElement = FieldElement::from((1u64 << 32) - 1); - // expected = (1 - word_instr) * res_hi + res_sign_bit * (2^32 - 1) - let expected = (&one - word_instr) * res_hi + res_sign_bit * mask_32; + // expected = (1 - word_instr) * res_hi + res_ext_bit * (2^32 - 1) + let expected = (&one - word_instr) * res_hi + res_ext_bit * mask_32; // (1 - LOAD) * (rvd[1] - expected) = 0 (one - load) * (rvd_1 - expected) @@ -1265,14 +1265,14 @@ pub fn create_jalr_constraints(constraint_idx_start: usize) -> (Vec ( other.push(Box::new(c)); } - // Sign bit zero constraint - other.push(Box::new(SignBitZeroConstraint::new(next_idx))); + // Extension bit zero constraints (SIGN template: !word_instr => ext_bit = 0) + other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RV1_EXT_BIT))); + next_idx += 1; + other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RV2_EXT_BIT))); + next_idx += 1; + other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RES_EXT_BIT))); next_idx += 1; // Next PC (non-branching) constraints diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 7ef2893f0..8f49b6fe4 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -25,7 +25,7 @@ //! ### Auxiliary //! - `rv1`: DWordWHH (3 cols) - value of register rs1 //! - `rv2`: DWordWHH (3 cols) - value of register rs2 -//! - `rv1_sign_bit`, `arg2_sign_bit`, `res_sign_bit`: Bit (for word instruction extension) +//! - `rv1_ext_bit`, `rv2_ext_bit`, `res_ext_bit`: Bit (for word instruction extension) //! - `arg1`: DWordBL (8 cols) - extended rv1 //! - `arg2`: DWordBL (8 cols) - multiplexed rv2/imm //! - `res`: DWordBL (8 cols) - ALU result @@ -47,8 +47,7 @@ //! - MUL: for multiplication //! - DIVREM: for division/remainder //! - MEMW: for register and memory access -//! - MSB16: for sign bit extraction -//! - MSB8: for 32-bit sign bit extraction +//! - MSB16: for sign/extension bit extraction (rv1, rv2, res) //! - ZERO: for equality check //! - BRANCH: for branch target calculation //! - ECALL: for system calls @@ -188,8 +187,8 @@ pub mod cols { /// rv2[2]: Register rs2 value (Word - bits 32-63) [DWordWHH] pub const RV2_2: usize = 44; - /// rv1_sign_bit: Sign bit of rv1 as 32-bit word (for word_instr extension) - pub const RV1_SIGN_BIT: usize = 45; + /// rv1_ext_bit: Sign bit of rv1 as 32-bit word (for word_instr sign extension) + pub const RV1_EXT_BIT: usize = 45; /// arg1[0..8]: Extended rv1 as DWordBL (8 bytes) pub const ARG1_0: usize = 46; @@ -201,8 +200,8 @@ pub mod cols { pub const ARG1_6: usize = 52; pub const ARG1_7: usize = 53; - /// arg2_sign_bit: Sign bit of rv2 as 32-bit word (bit 31 of rv2; used to define arg2's extension) - pub const ARG2_SIGN_BIT: usize = 54; + /// rv2_ext_bit: Sign bit of rv2 as 32-bit word (bit 31 of rv2; used for arg2 sign extension) + pub const RV2_EXT_BIT: usize = 54; /// arg2[0..8]: Extended rv2/imm as DWordBL (8 bytes) pub const ARG2_0: usize = 55; @@ -214,8 +213,8 @@ pub mod cols { pub const ARG2_6: usize = 61; pub const ARG2_7: usize = 62; - /// res_sign_bit: Sign bit of res as 32-bit word - pub const RES_SIGN_BIT: usize = 63; + /// res_ext_bit: Sign bit of res as 32-bit word (for rvd sign extension) + pub const RES_EXT_BIT: usize = 63; /// res[0..8]: ALU result as DWordBL (8 bytes) pub const RES_0: usize = 64; @@ -346,7 +345,7 @@ impl CpuOperation { /// Compute arg1 from rv1 based on word_instr and signed flags. /// - /// Per spec constraint: arg1[4:] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_sign_bit * signed + /// Per spec constraint: arg1[4:] = rv1[2] * (1 - word_instr) + (2^32 - 1) * rv1_ext_bit * signed /// /// For 64-bit instructions: pass through full rv1 /// For unsigned word instructions: zero-extend from 32 bits @@ -369,7 +368,7 @@ impl CpuOperation { /// Compute arg2 following the spec formula exactly (CPU-CE62/CE63). /// /// arg2[:4] = (1-LOAD)*rv2[:2] + (1-BEQ-BLT-STORE)*imm[0] - /// arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*arg2_sign_bit*(2^32-1)) + /// arg2[4:] = (1-LOAD)*((1-word_instr)*rv2[2] + signed*rv2_ext_bit*(2^32-1)) /// + (1-BEQ-BLT-STORE)*imm[1] /// /// Per CPU-A2, the decode guarantees that at most one of rv2/imm is non-zero @@ -411,7 +410,7 @@ impl CpuOperation { /// /// According to spec constraints: /// - rvd[0] = res[:4] (lower 32 bits of res) - /// - rvd[1] = (1 - word_instr) * res[4:] + res_sign_bit * (2^32 - 1) + /// - rvd[1] = (1 - word_instr) * res[4:] + res_ext_bit * (2^32 - 1) /// /// For LOAD: rvd comes from the executor (loaded value), not this method. /// For all other operations: rvd is computed from res with sign extension. @@ -421,8 +420,8 @@ impl CpuOperation { if self.decode.word_instr { // Sign extend from 32 bits - let res_sign_bit = Self::sign_bit_32(res); - if res_sign_bit { + let res_ext_bit = Self::sign_bit_32(res); + if res_ext_bit { // Upper 32 bits = 0xFFFF_FFFF (sign extension) res_lo | (0xFFFF_FFFF_u64 << 32) } else { @@ -555,7 +554,7 @@ impl CpuOperation { hi, )); - // rv2[1] for arg2_sign_bit + // rv2[1] for rv2_ext_bit let rv2_half = ((self.rv2 >> 16) & 0xFFFF) as u16; let lo = (rv2_half & 0xFF) as u8; let hi = ((rv2_half >> 8) & 0xFF) as u8; @@ -565,11 +564,12 @@ impl CpuOperation { hi, )); - // res[3] for res_sign_bit (MSB8 on byte at bits 24-31) - let res_byte = ((self.res >> 24) & 0xFF) as u8; - lookups.push(BitwiseOperation::single_byte( - BitwiseOperationType::Msb8, - res_byte, + // res::DWordHL[1] for res_ext_bit (MSB16 on half at bits 16-31) + let res_half = ((self.res >> 16) & 0xFFFF) as u16; + lookups.push(BitwiseOperation::halfword( + BitwiseOperationType::Msb16, + (res_half & 0xFF) as u8, + (res_half >> 8) as u8, )); } @@ -827,9 +827,9 @@ pub fn generate_cpu_trace( data[base + cols::RV2_2] = FE::from(op.rv2 >> 32); // bits 32-63 (Word) // Sign bits - only set when word_instr=1, per spec constraint ext_sign_bits - // The constraint enforces: (rv1_sign_bit + arg2_sign_bit + res_sign_bit) * (1 - word_instr) = 0 - let rv1_sign_bit = d.word_instr && CpuOperation::sign_bit_32(op.rv1); - data[base + cols::RV1_SIGN_BIT] = FE::from(rv1_sign_bit as u64); + // The constraint enforces: (rv1_ext_bit + rv2_ext_bit + res_ext_bit) * (1 - word_instr) = 0 + let rv1_ext_bit = d.word_instr && CpuOperation::sign_bit_32(op.rv1); + data[base + cols::RV1_EXT_BIT] = FE::from(rv1_ext_bit as u64); // Compute and store arg1 as DWordBL (8 bytes) let arg1 = op.compute_arg1(); @@ -839,16 +839,16 @@ pub fn generate_cpu_trace( // Compute and store arg2 let arg2 = op.compute_arg2(); - let arg2_sign_bit = d.word_instr && CpuOperation::sign_bit_32(op.rv2); - data[base + cols::ARG2_SIGN_BIT] = FE::from(arg2_sign_bit as u64); + let rv2_ext_bit = d.word_instr && CpuOperation::sign_bit_32(op.rv2); + data[base + cols::RV2_EXT_BIT] = FE::from(rv2_ext_bit as u64); for i in 0..8 { data[base + cols::ARG2[i]] = FE::from((arg2 >> (i * 8)) & 0xFF); } // Result - computed from arg1/arg2 for ADD/SUB to satisfy constraints let res = op.compute_res(); - let res_sign_bit = d.word_instr && CpuOperation::sign_bit_32(res); - data[base + cols::RES_SIGN_BIT] = FE::from(res_sign_bit as u64); + let res_ext_bit = d.word_instr && CpuOperation::sign_bit_32(res); + data[base + cols::RES_EXT_BIT] = FE::from(res_ext_bit as u64); for i in 0..8 { data[base + cols::RES[i]] = FE::from((res >> (i * 8)) & 0xFF); } @@ -1096,10 +1096,10 @@ pub fn bus_interactions() -> Vec { } // ------------------------------------------------------------------------- - // MSB16 interactions for sign bit extraction + // SIGN template: MSB16 interactions for extension bit extraction // ------------------------------------------------------------------------- - // MSB16[rv1[1]] -> rv1_sign_bit, multiplicity = word_instr - // rv1[1] is a Half (bits 16-31), containing the sign bit at position 31 + // SIGN(rv1[1], word_instr) -> rv1_ext_bit + // rv1[1] is a Half (bits 16-31), MSB16 extracts bit 31 interactions.push(BusInteraction::sender( BusId::Msb16, Multiplicity::Column(cols::WORD_INSTR), @@ -1109,13 +1109,13 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }, BusValue::Packed { - start_column: cols::RV1_SIGN_BIT, + start_column: cols::RV1_EXT_BIT, packing: Packing::Direct, }, ], )); - // MSB16[rv2[1]] -> arg2_sign_bit, multiplicity = word_instr + // SIGN(rv2[1], word_instr) -> rv2_ext_bit interactions.push(BusInteraction::sender( BusId::Msb16, Multiplicity::Column(cols::WORD_INSTR), @@ -1125,27 +1125,33 @@ pub fn bus_interactions() -> Vec { packing: Packing::Direct, }, BusValue::Packed { - start_column: cols::ARG2_SIGN_BIT, + start_column: cols::RV2_EXT_BIT, packing: Packing::Direct, }, ], )); // ------------------------------------------------------------------------- - // MSB8 interaction for res sign bit extraction + // MSB16 interaction for res sign bit extraction // ------------------------------------------------------------------------- - // MSB8[res[3]] -> res_sign_bit, multiplicity = word_instr - // res[3] is the byte at bits 24-31, containing the sign bit at position 31 + // MSB16[res::DWordHL[1]] -> res_ext_bit, multiplicity = word_instr + // res::DWordHL[1] is the half at bits 16-31 = res[2] + 256*res[3] interactions.push(BusInteraction::sender( - BusId::Msb8, + BusId::Msb16, Multiplicity::Column(cols::WORD_INSTR), vec![ + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::RES[2], + }, + LinearTerm::Column { + coefficient: 256, + column: cols::RES[3], + }, + ]), BusValue::Packed { - start_column: cols::RES[3], - packing: Packing::Direct, - }, - BusValue::Packed { - start_column: cols::RES_SIGN_BIT, + start_column: cols::RES_EXT_BIT, packing: Packing::Direct, }, ], diff --git a/prover/src/tests/constraints_tests.rs b/prover/src/tests/constraints_tests.rs index 85a41dff2..9d5ae5ef3 100644 --- a/prover/src/tests/constraints_tests.rs +++ b/prover/src/tests/constraints_tests.rs @@ -514,7 +514,7 @@ fn test_dword_bl_repack_formula() { use crate::constraints::cpu::{ Arg1LowerConstraint, Arg1UpperConstraint, BIT_FLAG_COLUMNS, BranchCondConstraint, - EbreakConstraint, NUM_CPU_CONSTRAINTS, NextPcAddConstraint, SignBitZeroConstraint, + EbreakConstraint, NUM_CPU_CONSTRAINTS, NextPcAddConstraint, ExtBitZeroConstraint, create_add_constraints, create_all_cpu_constraints, create_is_bit_constraints, create_slt_res_zero_constraints, }; @@ -600,8 +600,8 @@ fn test_arg1_upper_constraint_degree() { } #[test] -fn test_sign_bit_zero_constraint_degree() { - let c = SignBitZeroConstraint::new(0); +fn test_ext_bit_zero_constraint_degree() { + let c = ExtBitZeroConstraint::new(0, cpu_cols::RV1_EXT_BIT); assert_eq!(c.degree(), 2); } @@ -625,11 +625,11 @@ fn test_create_all_cpu_constraints() { assert_eq!(is_bit.len(), 32); // ADD constraints: 2 (ADD+LOAD) + 2 (STORE: arg1+imm) + 2 (SUB+BEQ) + 2 (JALR) = 8 assert_eq!(add.len(), 8); - // Other: branch_cond(1) + ebreak(1) + rv1_zero_forcing(3) + rv2_zero_forcing(3) + arg1(2) + arg2(2) + rvd(2) + slt_zero(7) + sign_bit_zero(1) + next_pc(2) = 24 - assert_eq!(other.len(), 24); + // Other: branch_cond(1) + ebreak(1) + rv1_zero_forcing(3) + rv2_zero_forcing(3) + arg1(2) + arg2(2) + rvd(2) + slt_zero(7) + ext_bit_zero(3) + next_pc(2) = 26 + assert_eq!(other.len(), 26); - // Total should be 32 + 8 + 24 = 64 - assert_eq!(total, 64); + // Total should be 32 + 8 + 26 = 66 + assert_eq!(total, 66); assert_eq!(total, NUM_CPU_CONSTRAINTS); } diff --git a/prover/src/tests/cpu_tests.rs b/prover/src/tests/cpu_tests.rs index a8e08dab9..cdbdcd153 100644 --- a/prover/src/tests/cpu_tests.rs +++ b/prover/src/tests/cpu_tests.rs @@ -301,8 +301,8 @@ fn test_trace_generation_sign_bits() { let trace = generate_cpu_trace(&ops); let row0 = trace.main_table.get_row(0); - assert_eq!(row0[cols::RV1_SIGN_BIT], FE::one()); - assert_eq!(row0[cols::RES_SIGN_BIT], FE::one()); + assert_eq!(row0[cols::RV1_EXT_BIT], FE::one()); + assert_eq!(row0[cols::RES_EXT_BIT], FE::one()); } #[test] From 58244793c4e2c06f720543742a46a108eecbc8bf Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Wed, 25 Mar 2026 11:28:32 -0300 Subject: [PATCH 2/3] fmt --- prover/src/constraints/cpu.rs | 15 ++++++++++++--- prover/src/tests/constraints_tests.rs | 2 +- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/prover/src/constraints/cpu.rs b/prover/src/constraints/cpu.rs index f1d9b0304..a3dc3e8ee 100644 --- a/prover/src/constraints/cpu.rs +++ b/prover/src/constraints/cpu.rs @@ -1362,11 +1362,20 @@ pub fn create_all_cpu_constraints() -> ( } // Extension bit zero constraints (SIGN template: !word_instr => ext_bit = 0) - other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RV1_EXT_BIT))); + other.push(Box::new(ExtBitZeroConstraint::new( + next_idx, + cols::RV1_EXT_BIT, + ))); next_idx += 1; - other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RV2_EXT_BIT))); + other.push(Box::new(ExtBitZeroConstraint::new( + next_idx, + cols::RV2_EXT_BIT, + ))); next_idx += 1; - other.push(Box::new(ExtBitZeroConstraint::new(next_idx, cols::RES_EXT_BIT))); + other.push(Box::new(ExtBitZeroConstraint::new( + next_idx, + cols::RES_EXT_BIT, + ))); next_idx += 1; // Next PC (non-branching) constraints diff --git a/prover/src/tests/constraints_tests.rs b/prover/src/tests/constraints_tests.rs index 9d5ae5ef3..3881c611e 100644 --- a/prover/src/tests/constraints_tests.rs +++ b/prover/src/tests/constraints_tests.rs @@ -514,7 +514,7 @@ fn test_dword_bl_repack_formula() { use crate::constraints::cpu::{ Arg1LowerConstraint, Arg1UpperConstraint, BIT_FLAG_COLUMNS, BranchCondConstraint, - EbreakConstraint, NUM_CPU_CONSTRAINTS, NextPcAddConstraint, ExtBitZeroConstraint, + EbreakConstraint, ExtBitZeroConstraint, NUM_CPU_CONSTRAINTS, NextPcAddConstraint, create_add_constraints, create_all_cpu_constraints, create_is_bit_constraints, create_slt_res_zero_constraints, }; From ccdaa32c1aae8076e4978a5f942fe9b24cd8591e Mon Sep 17 00:00:00 2001 From: Joaquin Carletti Date: Wed, 25 Mar 2026 11:32:30 -0300 Subject: [PATCH 3/3] fix comments --- prover/src/tables/cpu.rs | 6 +++--- prover/src/tests/cpu_tests.rs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 8f49b6fe4..e29ae1d57 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -826,8 +826,8 @@ pub fn generate_cpu_trace( data[base + cols::RV2_1] = FE::from((op.rv2 >> 16) & 0xFFFF); // bits 16-31 (Half) data[base + cols::RV2_2] = FE::from(op.rv2 >> 32); // bits 32-63 (Word) - // Sign bits - only set when word_instr=1, per spec constraint ext_sign_bits - // The constraint enforces: (rv1_ext_bit + rv2_ext_bit + res_ext_bit) * (1 - word_instr) = 0 + // Extension bits - only set when word_instr=1, per SIGN template + // The constraint enforces: (1 - word_instr) * ext_bit = 0 for each ext bit let rv1_ext_bit = d.word_instr && CpuOperation::sign_bit_32(op.rv1); data[base + cols::RV1_EXT_BIT] = FE::from(rv1_ext_bit as u64); @@ -1132,7 +1132,7 @@ pub fn bus_interactions() -> Vec { )); // ------------------------------------------------------------------------- - // MSB16 interaction for res sign bit extraction + // MSB16 interaction for res extension bit extraction // ------------------------------------------------------------------------- // MSB16[res::DWordHL[1]] -> res_ext_bit, multiplicity = word_instr // res::DWordHL[1] is the half at bits 16-31 = res[2] + 256*res[3] diff --git a/prover/src/tests/cpu_tests.rs b/prover/src/tests/cpu_tests.rs index cdbdcd153..d2c240293 100644 --- a/prover/src/tests/cpu_tests.rs +++ b/prover/src/tests/cpu_tests.rs @@ -286,7 +286,7 @@ fn test_trace_generation_res_dwordbl() { } #[test] -fn test_trace_generation_sign_bits() { +fn test_trace_generation_ext_bits() { let ops = ops4(CpuOperation { decode: DecodeEntry { word_instr: true,