fix(bug): soundness and constraints for formal verification

vm/src/chips/chips/alu/divrem/constraints.rs

@@ -167,6 +167,22 @@ where
                 }
             }
 
+            // For word operations, constrain the upper limbs of b and c to be proper sign/zero
+            // extension. Without b's constraint, a prover can pick a large quotient q such that
+            // c×q overflows into b[2]/b[3], satisfying c×q+r=b with an incorrect quotient.
+            // Without c's constraint, a prover can set c[2]!=0 while c[0]=c[1]=0, making
+            // is_c_0 false while the actual 32-bit divisor is zero, bypassing div-by-zero.
+            for i in WORD_SIZE / 2..WORD_SIZE {
+                builder.when(is_word_operation.clone()).assert_eq(
+                    local_b[i],
+                    local_b_neg * CB::F::from_canonical_u16(u16::MAX),
+                );
+                builder.when(is_word_operation.clone()).assert_eq(
+                    local_c[i],
+                    local_c_neg * CB::F::from_canonical_u16(u16::MAX),
+                );
+            }
+
             // Set up `quotient_comp` and `remainder_comp`.
             // `quotient_comp` is defined as following:
             // - `quotient` for 64-bit operations and signed word operations.
@@ -562,6 +578,11 @@ where
                     local_remainder_lt_gadget,
                     local_remainder_check_multiplicity.into(),
                 );
+                // Enforce that the LT relation actually holds (bit = 1 means a < b).
+                // Without this, a prover could set bit = 0 and claim remainder >= divisor.
+                builder
+                    .when(local_remainder_check_multiplicity)
+                    .assert_one(local_remainder_lt_gadget.bit);
             }
 
             // Check that the MSBs are correct.
@@ -587,6 +608,7 @@ where
                     (local_b_msb, local_b[WORD_SIZE / 2 - 1].into()),
                     (local_c_msb, local_c[WORD_SIZE / 2 - 1].into()),
                     (local_rem_msb, local_remainder[WORD_SIZE / 2 - 1].into()),
+                    (local_quot_msb, local_quotient[WORD_SIZE / 2 - 1].into()),
                 ];
                 for msb_pair in msb_pairs_word.iter() {
                     let (msb, byte) = msb_pair;

vm/src/chips/chips/alu/lt/constraints.rs

@@ -7,7 +7,7 @@ use crate::{
     machine::builder::{ChipBuilder, ChipLookupBuilder},
 };
 use core::borrow::Borrow;
-use p3_air::Air;
+use p3_air::{Air, AirBuilder};
 use p3_field::Field;
 use p3_matrix::Matrix;
 
@@ -47,6 +47,11 @@ where
             builder.assert_zero(a[2]);
             builder.assert_zero(a[3]);
 
+            // a[0] must equal the comparison result bit
+            builder
+                .when(is_real.clone())
+                .assert_eq(a[0], lt_signed.result.bit);
+
             // SLT looked
             let lt_op_code = *is_slt * CB::F::from_canonical_u32(Opcode::SLT as u32)
                 + *is_slt_u * CB::F::from_canonical_u32(Opcode::SLTU as u32);

vm/src/chips/chips/alu/lt/tests.rs

@@ -141,3 +141,31 @@ fn test_lt_chip_simple_eval() {
     assert_eq!(builder.public_values().len(), 119);
     assert_eq!(builder.num_lookups(), 4);
 }
+
+/// SLT: -1 < 1 should be true (a[0] = 1); exercises the signed comparison path
+#[test]
+fn test_rv64_slt_negative_less_than_positive() {
+    let instructions = vec![
+        Instruction::new(Opcode::ADD, 10, 0, (-1i64) as u64, false, true),
+        Instruction::new(Opcode::ADD, 11, 0, 1, false, true),
+        Instruction::new(Opcode::SLT, 12, 10, 11, false, false),
+        Instruction::new(Opcode::ADD, 10, 0, 0, false, true),
+        Instruction::new(Opcode::ECALL, 0, 0, 0, false, false),
+    ];
+    let program = Program::new(instructions, 0x10000, 0x10000);
+    run_test(program, "SLT: negative < positive");
+}
+
+/// SLTU: u64::MAX < u64::MAX should be false (a[0] = 0); exercises the equal case
+#[test]
+fn test_rv64_sltu_max_values() {
+    let instructions = vec![
+        Instruction::new(Opcode::ADD, 10, 0, u64::MAX, false, true),
+        Instruction::new(Opcode::ADD, 11, 0, u64::MAX, false, true),
+        Instruction::new(Opcode::SLTU, 12, 10, 11, false, false),
+        Instruction::new(Opcode::ADD, 10, 0, 0, false, true),
+        Instruction::new(Opcode::ECALL, 0, 0, 0, false, false),
+    ];
+    let program = Program::new(instructions, 0x10000, 0x10000);
+    run_test(program, "SLTU: max == max");
+}

vm/src/chips/chips/alu/sll/constraints.rs

@@ -65,6 +65,14 @@ where
                 is_real.clone(),
             );
 
+            let not_sllw = is_sll;
+            for i in 0..4 {
+                builder.when(shift_u16[i]).assert_eq(
+                    c_bits[4] + c_bits[5] * CB::F::from_canonical_u32(2) * not_sllw,
+                    CB::F::from_canonical_u32(i as u32),
+                );
+                builder.assert_bool(shift_u16[i]);
+            }
             builder.when(is_real.clone()).assert_eq(
                 shift_u16[0] + shift_u16[1] + shift_u16[2] + shift_u16[3],
                 CB::F::from_canonical_u32(1),

vm/src/chips/chips/alu/sr/constraints.rs

@@ -64,6 +64,10 @@ where
             // Constrain is_w_imm = (is_srlw + is_sraw) * imm_c
             builder.assert_eq(is_w_imm, is_word.clone() * imm_c);
 
+            // Bind scalar c to c_for_lookup[0] so the shift amount used in computation
+            // matches the operand visible to the CPU via the multiset lookup.
+            builder.assert_eq(c, c_for_lookup[0].into());
+
             // Check that c_bits are the 6 lowest bits of c (Var types - no clone needed)
             for i in 0..6 {
                 builder.assert_bool(c_bits[i]);
@@ -120,7 +124,8 @@ where
                 one.clone(),
             );
 
-            // Check that lower_limb < 2^bit_shift and higher_limb < 2^(16 - bit_shift)
+            // Check that lower_limb < 2^bit_shift and higher_limb < 2^(16 - bit_shift),
+            // and tie b[i] to its decomposition: b[i] = lower_limb[i] + higher_limb[i] * 2^bit_shift.
             let sixteen: CB::Expr = CB::F::from_canonical_u32(16).into();
             for i in 0..WORD_SIZE {
                 builder.looking_byte(
@@ -137,6 +142,12 @@ where
                     zero.clone(),
                     is_real.clone(),
                 );
+                // Carry equation: b[i] * v_0123 = higher_limb[i] * 2^16 + lower_limb[i] * v_0123
+                // (v_0123 = 2^(16 - bit_shift), so this reduces to b[i] = lower_limb[i] + higher_limb[i] * 2^bit_shift)
+                builder.assert_eq(
+                    b[i] * v_0123,
+                    higher_limb[i] * CB::F::from_canonical_u32(1 << 16) + lower_limb[i] * v_0123,
+                );
             }
 
             // Check limb_result = higher_limb + lower_limb[i+1] * v_0123
@@ -185,7 +196,28 @@ where
                 }
             }
 
-            // TODO: constrain 32-bit operations (SRLW/SRAW)
+            // Constrain 32-bit operations (SRLW/SRAW): a[0] and a[1]
+            let half = WORD_SIZE / 2;
+            for i in 0..half {
+                for j in 0..(half - 1 - i) {
+                    builder
+                        .when(is_word.clone())
+                        .when(shift_u16[i])
+                        .assert_eq(a[j], limb_result[i + j]);
+                }
+
+                builder.when(is_word.clone()).when(shift_u16[i]).assert_eq(
+                    a[half - 1 - i],
+                    higher_limb[half - 1] + (b_msb.msb * base - sra_msb_v0123),
+                );
+
+                for j in (half - i)..half {
+                    builder
+                        .when(is_word.clone())
+                        .when(shift_u16[i])
+                        .assert_eq(a[j], b_msb.msb * base_minus_one);
+                }
+            }
 
             // For word operations, the upper bits should be sign-extended
             for i in WORD_SIZE / 2..WORD_SIZE {

vm/src/chips/chips/alu/sr/tests.rs

@@ -99,3 +99,17 @@ fn test_rv64_srlw() {
 fn test_rv64_sraw() {
     run_test(create_sraw_program(), "SRAW");
 }
+
+/// SRAW: 0x80000000 >> 16 — exercises shift_u16[1] (a[0] is assigned from limb_result[1])
+#[test]
+fn test_rv64_sraw_word_cross_boundary() {
+    let instructions = vec![
+        Instruction::new(Opcode::ADD, 10, 0, 0x80000000, false, true),
+        Instruction::new(Opcode::ADD, 11, 0, 16, false, true),
+        Instruction::new(Opcode::SRAW, 12, 10, 11, false, false),
+        Instruction::new(Opcode::ADD, 10, 0, 0, false, true),
+        Instruction::new(Opcode::ECALL, 0, 0, 0, false, false),
+    ];
+    let program = Program::new(instructions, 0x10000, 0x10000);
+    run_test(program, "SRAW: word boundary");
+}

vm/src/chips/chips/riscv_cpu/jump/columns.rs

@@ -1,8 +1,11 @@
 use pico_derive::AlignedBorrow;
-use std::{marker::PhantomData, mem::size_of};
+use std::mem::size_of;
 
 pub const NUM_JUMP_COLS: usize = size_of::<JumpCols<u8>>();
 
 #[derive(AlignedBorrow, Clone, Copy, Debug, Default)]
 #[repr(C)]
-pub struct JumpCols<F>(PhantomData<F>);
+pub struct JumpCols<T> {
+    /// Bit 0 of (rs1 + imm) for JALR. Witnesses that next_pc = (rs1 + imm) & !1.
+    pub jalr_lsb: T,
+}

vm/src/chips/chips/riscv_cpu/jump/constraints.rs

@@ -1,7 +1,7 @@
 use super::super::{columns::CpuCols, CpuChip};
 use crate::{
     compiler::{riscv::opcode::Opcode, word::Word},
-    machine::builder::{ChipBuilder, ChipLookupBuilder, ChipWordBuilder},
+    machine::builder::{ChipBuilder, ChipLookupBuilder, ChipRangeBuilder, ChipWordBuilder},
 };
 use p3_air::AirBuilder;
 use p3_field::{Field, FieldAlgebra};
@@ -81,9 +81,32 @@ impl<F: Field> CpuChip<F> {
         );
 
         // Verify that the new pc is calculated correctly for JALR instructions.
+        // RISC-V spec: target = (rs1 + imm) & !1 (clear bit 0).
+        // We witness jalr_lsb = bit 0 of (rs1 + imm) and verify:
+        //   jalr_lsb ∈ {0, 1},
+        //   next_pc[0] is even  (via inverse-multiply range check),
+        //   rs1 + imm = next_pc + jalr_lsb  (via ALU ADD).
+        let jalr_lsb: CB::Expr = local.opcode_specific.jump().jalr_lsb.into();
+
+        builder
+            .when(local.opcode_selector.is_jalr)
+            .assert_bool(jalr_lsb.clone());
+
+        // Prove next_pc[0] is even: next_pc[0] * inv(2) must be a valid u16.
+        // If next_pc[0] were odd, next_pc[0] * inv(2) mod p ≈ p/2, which exceeds u16 range.
+        let two_inv: CB::Expr = F::from_canonical_u32(2).inverse().into();
+        let half_low: CB::Expr = local.next_pc[0].into() * two_inv;
+        builder.slice_range_check_u16(&[half_low], local.opcode_selector.is_jalr);
+
+        let sum_as_word = Word([
+            local.next_pc[0].into() + jalr_lsb,
+            local.next_pc[1].into(),
+            local.next_pc[2].into(),
+            F::ZERO.into(),
+        ]);
         builder.looking_alu(
             CB::Expr::from_canonical_u32(Opcode::ADD as u32),
-            next_pc_as_word.clone(),
+            sum_as_word,
             local.op_b_val(),
             local.op_c_val(),
             local.opcode_selector.is_jalr,

vm/src/chips/chips/riscv_cpu/jump/traces.rs

@@ -1,6 +1,8 @@
-use super::super::CpuChip;
+use super::super::{columns::CpuCols, CpuChip};
 use crate::{
-    chips::chips::{alu::event::AluEvent, riscv_cpu::event::CpuEvent},
+    chips::chips::{
+        alu::event::AluEvent, byte::event::ByteRecordBehavior, riscv_cpu::event::CpuEvent,
+    },
     compiler::riscv::opcode::Opcode,
 };
 use hashbrown::HashMap;
@@ -10,7 +12,9 @@ impl<F: Field> CpuChip<F> {
     /// Populate columns related to jumping.
     pub(crate) fn populate_jump(
         &self,
+        cols: &mut CpuCols<F>,
         event: &CpuEvent,
+        blu_events: &mut impl ByteRecordBehavior,
         alu_events: &mut HashMap<Opcode, Vec<AluEvent>>,
     ) {
         if event.instruction.is_jump_instruction() {
@@ -33,12 +37,21 @@ impl<F: Field> CpuChip<F> {
                         .or_insert(vec![add_event]);
                 }
                 Opcode::JALR => {
-                    let next_pc = event.b.wrapping_add(event.c);
+                    // sum = rs1 + imm (unmasked); next_pc = sum & !1 (= event.next_pc).
+                    let sum = event.b.wrapping_add(event.c);
+                    let jalr_lsb = (sum & 1) as u32;
+                    // next_pc[0] is the low 16-bit limb of event.next_pc; it is always even.
+                    let next_pc_low = event.next_pc as u16;
 
+                    cols.opcode_specific.jump_mut().jalr_lsb = F::from_canonical_u32(jalr_lsb);
+                    // next_pc[0] / 2 feeds the u16 range check that proves next_pc[0] is even.
+                    blu_events.add_u16_range_check(next_pc_low >> 1);
+
+                    // The ALU event proves sum = b + c (i.e. next_pc + jalr_lsb = rs1 + imm).
                     let add_event = AluEvent {
                         clk: event.clk,
                         opcode: Opcode::ADD,
-                        a: next_pc,
+                        a: sum,
                         b: event.b,
                         c: event.c,
                         ..Default::default()

vm/src/chips/chips/riscv_cpu/traces.rs

@@ -290,7 +290,7 @@ impl<F: PrimeField32> CpuChip<F> {
         cols.num_extra_clk = num_extra_clk;
 
         self.populate_branch(cols, event, &mut new_alu_events);
-        self.populate_jump(event, &mut new_alu_events);
+        self.populate_jump(cols, event, blu_events, &mut new_alu_events);
         self.populate_auipc(event, &mut new_alu_events);
         let is_halt = self.populate_ecall(cols, event, blu_events);
 

vm/src/chips/chips/riscv_memory/read_write/columns.rs

@@ -35,10 +35,6 @@ pub struct MemoryChipValueCols<F> {
     /// The 4th limb is constrained to be zero.
     pub addr_word: Word<F>,
 
-    /// This is the aligned memory address used for memory lookups, it's muliple of 8, since uint64.
-    /// TODO: add constraints to fix soundness
-    pub addr_aligned: Word<F>,
-
     /// The 3 binary offset bits: addr[0] & 1, (addr[0]>>1) & 1, (addr[0]>>2) & 1.
     /// These replace the old one-hot offset_is_one/two/three flags.
     pub offset_bit: [F; 3],
@@ -140,8 +136,8 @@ pub struct MemoryInstructionCols<T> {
     pub is_sd: T, // New for RV64
 
     pub op_a_access: MemoryReadWriteCols<T>,
-    pub op_b_access: MemoryReadCols<T>,
-    pub op_c_access: MemoryReadCols<T>,
+    pub op_b_access: Word<T>,
+    pub op_c_access: Word<T>,
 }
 
 impl<F: Field> MemoryInstructionCols<F> {
@@ -168,18 +164,18 @@ impl<F: Field> MemoryInstructionCols<F> {
         // For u64 upgrade: values are no longer narrowed to u32.
         // op_a/b/c are now native u64 → Word (4×u16).
         *self.op_a_access.value_mut() = event.a.into();
-        *self.op_b_access.value_mut() = event.b.into();
-        *self.op_c_access.value_mut() = event.c.into();
+        self.op_b_access = event.b.into();
+        self.op_c_access = event.c.into();
 
         // Set memory accesses for a, b, and c.
         if let Some(record) = event.a_record {
             *self.op_a_access.value_mut() = record.value().into();
         }
         if let Some(MemoryRecordEnum::Read(record)) = event.b_record {
-            *self.op_b_access.value_mut() = record.value.into();
+            self.op_b_access = record.value.into();
         }
         if let Some(MemoryRecordEnum::Read(record)) = event.c_record {
-            *self.op_c_access.value_mut() = record.value.into();
+            self.op_c_access = record.value.into();
         }
     }
 }
@@ -192,12 +188,12 @@ impl<T: Copy> MemoryInstructionCols<T> {
 
     /// Gets the value of the second operand.
     pub fn op_b_val(&self) -> Word<T> {
-        *self.op_b_access.value()
+        self.op_b_access
     }
 
     /// Gets the value of the third operand.
     pub fn op_c_val(&self) -> Word<T> {
-        *self.op_c_access.value()
+        self.op_c_access
     }
 }