diff --git a/vm/src/chips/chips/alu/divrem/constraints.rs b/vm/src/chips/chips/alu/divrem/constraints.rs index 5fbe702e..eaef0b44 100644 --- a/vm/src/chips/chips/alu/divrem/constraints.rs +++ b/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; diff --git a/vm/src/chips/chips/alu/lt/constraints.rs b/vm/src/chips/chips/alu/lt/constraints.rs index c2b9df9d..3293c69a 100644 --- a/vm/src/chips/chips/alu/lt/constraints.rs +++ b/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); diff --git a/vm/src/chips/chips/alu/lt/tests.rs b/vm/src/chips/chips/alu/lt/tests.rs index daf39f0e..784a48b7 100644 --- a/vm/src/chips/chips/alu/lt/tests.rs +++ b/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"); +} diff --git a/vm/src/chips/chips/alu/sll/constraints.rs b/vm/src/chips/chips/alu/sll/constraints.rs index 543a2b3b..b343beb9 100644 --- a/vm/src/chips/chips/alu/sll/constraints.rs +++ b/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), diff --git a/vm/src/chips/chips/alu/sr/constraints.rs b/vm/src/chips/chips/alu/sr/constraints.rs index e374aa3d..cca45c33 100644 --- a/vm/src/chips/chips/alu/sr/constraints.rs +++ b/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 { diff --git a/vm/src/chips/chips/alu/sr/tests.rs b/vm/src/chips/chips/alu/sr/tests.rs index ed077fe7..ea75bead 100644 --- a/vm/src/chips/chips/alu/sr/tests.rs +++ b/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"); +} diff --git a/vm/src/chips/chips/riscv_cpu/jump/columns.rs b/vm/src/chips/chips/riscv_cpu/jump/columns.rs index 15cb3ffe..8ccd75e9 100644 --- a/vm/src/chips/chips/riscv_cpu/jump/columns.rs +++ b/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::>(); #[derive(AlignedBorrow, Clone, Copy, Debug, Default)] #[repr(C)] -pub struct JumpCols(PhantomData); +pub struct JumpCols { + /// Bit 0 of (rs1 + imm) for JALR. Witnesses that next_pc = (rs1 + imm) & !1. + pub jalr_lsb: T, +} diff --git a/vm/src/chips/chips/riscv_cpu/jump/constraints.rs b/vm/src/chips/chips/riscv_cpu/jump/constraints.rs index e49ab892..9e48d4fd 100644 --- a/vm/src/chips/chips/riscv_cpu/jump/constraints.rs +++ b/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 CpuChip { ); // 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, diff --git a/vm/src/chips/chips/riscv_cpu/jump/traces.rs b/vm/src/chips/chips/riscv_cpu/jump/traces.rs index ece71d61..512de2bb 100644 --- a/vm/src/chips/chips/riscv_cpu/jump/traces.rs +++ b/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 CpuChip { /// Populate columns related to jumping. pub(crate) fn populate_jump( &self, + cols: &mut CpuCols, event: &CpuEvent, + blu_events: &mut impl ByteRecordBehavior, alu_events: &mut HashMap>, ) { if event.instruction.is_jump_instruction() { @@ -33,12 +37,21 @@ impl CpuChip { .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() diff --git a/vm/src/chips/chips/riscv_cpu/traces.rs b/vm/src/chips/chips/riscv_cpu/traces.rs index b7efaa2d..9b5f9303 100644 --- a/vm/src/chips/chips/riscv_cpu/traces.rs +++ b/vm/src/chips/chips/riscv_cpu/traces.rs @@ -290,7 +290,7 @@ impl CpuChip { 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); diff --git a/vm/src/chips/chips/riscv_memory/read_write/columns.rs b/vm/src/chips/chips/riscv_memory/read_write/columns.rs index 5fb52ce4..8d582d1f 100644 --- a/vm/src/chips/chips/riscv_memory/read_write/columns.rs +++ b/vm/src/chips/chips/riscv_memory/read_write/columns.rs @@ -35,10 +35,6 @@ pub struct MemoryChipValueCols { /// The 4th limb is constrained to be zero. pub addr_word: Word, - /// 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, - /// 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 { pub is_sd: T, // New for RV64 pub op_a_access: MemoryReadWriteCols, - pub op_b_access: MemoryReadCols, - pub op_c_access: MemoryReadCols, + pub op_b_access: Word, + pub op_c_access: Word, } impl MemoryInstructionCols { @@ -168,18 +164,18 @@ impl MemoryInstructionCols { // 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 MemoryInstructionCols { /// Gets the value of the second operand. pub fn op_b_val(&self) -> Word { - *self.op_b_access.value() + self.op_b_access } /// Gets the value of the third operand. pub fn op_c_val(&self) -> Word { - *self.op_c_access.value() + self.op_c_access } } diff --git a/vm/src/chips/chips/riscv_memory/read_write/constraints.rs b/vm/src/chips/chips/riscv_memory/read_write/constraints.rs index 83d3f6fa..04d54b55 100644 --- a/vm/src/chips/chips/riscv_memory/read_write/constraints.rs +++ b/vm/src/chips/chips/riscv_memory/read_write/constraints.rs @@ -193,7 +193,7 @@ impl MemoryReadWriteChip { let inv_8 = CB::F::from_canonical_u8(8).inverse(); builder.looking_byte( CB::Expr::from_canonical_u8(ByteOpcode::BitRange as u8), - (CB::Expr::ZERO + local.addr_word.0[0] - offset_sum) * CB::Expr::from(inv_8), + (CB::Expr::ZERO + local.addr_word.0[0] - offset_sum.clone()) * CB::Expr::from(inv_8), CB::Expr::from_canonical_u8(13), CB::Expr::ZERO, is_mem.clone(), @@ -216,14 +216,15 @@ impl MemoryReadWriteChip { ); // ---- C3: Timestamp + Regional Lookup ---- + // addr_aligned is computed inline as addr_word - offset, avoiding a free witness column. // eval_memory_access handles timestamp monotonicity and 9-element Regional lookup. builder.eval_memory_access( local.chunk, local.clk + CB::F::from_canonical_u32(MemoryAccessPosition::Memory as u32), [ - local.addr_aligned.0[0], - local.addr_aligned.0[1], - local.addr_aligned.0[2], + CB::Expr::ZERO + local.addr_word.0[0] - offset_sum, + local.addr_word.0[1].into(), + local.addr_word.0[2].into(), ], &local.memory_access, is_mem.clone(), @@ -280,8 +281,22 @@ impl MemoryReadWriteChip { CB::Expr::ZERO + bit0 * byte1 + (CB::Expr::ONE - bit0) * byte0, ); - // Range check: selected_limb_low_byte ∈ [0, 255] - builder.slice_range_check_u8(&[local.selected_limb_low_byte], is_byte_load.clone()); + // Range check: both bytes of selected_limb ∈ [0, 255]. + // The high byte is never a witness column — it is computed inline as + // (selected_limb - selected_limb_low_byte) * inv_256. Without this check + // a prover can supply a fake selected_limb_low_byte that makes the high + // byte an arbitrary field element, breaking the u8 bound on selected_byte. + let high_byte: CB::Expr = (CB::Expr::ZERO + local.selected_limb + - local.selected_limb_low_byte) + * CB::Expr::from(inv_256); + builder.looking_rangecheck( + ByteOpcode::U8Range, + CB::Expr::ZERO, + CB::Expr::ZERO, + local.selected_limb_low_byte, + high_byte, + is_byte_load.clone(), + ); // LB/LBU: unsigned_mem_val = [selected_byte, 0, 0, 0] let byte_word = Word([ diff --git a/vm/src/chips/chips/riscv_memory/read_write/traces.rs b/vm/src/chips/chips/riscv_memory/read_write/traces.rs index 9ed4d842..02e9067b 100644 --- a/vm/src/chips/chips/riscv_memory/read_write/traces.rs +++ b/vm/src/chips/chips/riscv_memory/read_write/traces.rs @@ -32,7 +32,7 @@ use crate::{ chip::ChipBehavior, estimator::{EventCapture, EventSizeCapture}, }, - primitives::consts::{MEMORY_RW_DATAPAR, WORD_BYTE_SIZE}, + primitives::consts::MEMORY_RW_DATAPAR, }; use hashbrown::HashMap; use p3_field::{Field, PrimeField32}; @@ -183,14 +183,6 @@ impl MemoryReadWriteChip { let memory_addr = event.b.wrapping_add(event.c); // addr_word = Word from ALU ADD result (4×u16 limbs) cols.addr_word = memory_addr.into(); - let aligned_addr = memory_addr - memory_addr % WORD_BYTE_SIZE as u64; - cols.addr_aligned = Word::from(aligned_addr); - assert_eq!( - cols.addr_aligned[3], - F::ZERO, - "memory address must be less than 2^48", - ); - // Add ALU ADD event let add_event = AluEvent { clk: event.clk, @@ -288,8 +280,8 @@ impl MemoryReadWriteChip { let selected_byte = if bit0 == 1 { high_byte } else { low_byte }; cols.selected_byte = F::from_canonical_u8(selected_byte); - // Range check for selected_limb_low_byte - blu_events.add_u8_range_check(low_byte, 0); + // Range check both bytes of selected_limb. + blu_events.add_u8_range_check(low_byte, high_byte); // unsigned_mem_val = [selected_byte, 0, 0, 0] cols.unsigned_mem_val = Word([