From 37085d1e6f204fff1134865efd83ff7066729167 Mon Sep 17 00:00:00 2001 From: KimiWu Date: Tue, 8 Oct 2024 14:37:46 +0800 Subject: [PATCH] fix eq check of expected outcome --- ceno_zkvm/src/gadgets/div.rs | 2 +- ceno_zkvm/src/instructions/riscv/divu.rs | 12 +++++++++--- ceno_zkvm/src/instructions/riscv/shift.rs | 11 ++++++----- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/ceno_zkvm/src/gadgets/div.rs b/ceno_zkvm/src/gadgets/div.rs index be7f52494..ed5f4bb1d 100644 --- a/ceno_zkvm/src/gadgets/div.rs +++ b/ceno_zkvm/src/gadgets/div.rs @@ -33,7 +33,7 @@ impl DivConfig { ) -> Result { circuit_builder.namespace(name_fn, |cb| { // quotient = dividend / divisor + remainder => dividend = divisor * quotient + r - let mut divisor = UInt::new_unchecked(|| "divisor", cb)?; + let mut divisor = UInt::new(|| "divisor", cb)?; let mut quotient = UInt::new(|| "quotient", cb)?; let remainder = UInt::new(|| "remainder", cb)?; diff --git a/ceno_zkvm/src/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/divu.rs index 710253ac2..dffbea7b5 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/divu.rs @@ -129,7 +129,7 @@ mod test { Value, }; - fn verify(name: &'static str, dividend: Word, divisor: Word, outcome: Word) { + fn verify(name: &'static str, dividend: Word, divisor: Word, exp_outcome: Word) { let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb @@ -140,6 +140,11 @@ mod test { .unwrap() .unwrap(); + let outcome = if divisor == 0 { + u32::MAX + } else { + dividend / divisor + }; // values assignment let (raw_witin, _) = DivUInstruction::assign_instances( &config, @@ -156,8 +161,9 @@ mod test { ) .unwrap(); - let expected_rd_written = - UInt::from_const_unchecked(Value::new_unchecked(outcome).as_u16_limbs().to_vec()); + let expected_rd_written = UInt::from_const_unchecked( + Value::new_unchecked(exp_outcome).as_u16_limbs().to_vec(), + ); config .div_config diff --git a/ceno_zkvm/src/instructions/riscv/shift.rs b/ceno_zkvm/src/instructions/riscv/shift.rs index 1741a735a..b831cc67b 100644 --- a/ceno_zkvm/src/instructions/riscv/shift.rs +++ b/ceno_zkvm/src/instructions/riscv/shift.rs @@ -215,9 +215,10 @@ mod tests { let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); - let (prefix, mock_pc, mock_program_op) = match I::INST_KIND { - InsnKind::SLL => ("SLL", MOCK_PC_SLL, MOCK_PROGRAM[19]), - InsnKind::SRL => ("SRL", MOCK_PC_SRL, MOCK_PROGRAM[20]), + let shift = rs2_read & 0b11111; + let (prefix, mock_pc, mock_program_op, rd_written) = match I::INST_KIND { + InsnKind::SLL => ("SLL", MOCK_PC_SLL, MOCK_PROGRAM[19], rs1_read << shift), + InsnKind::SRL => ("SRL", MOCK_PC_SRL, MOCK_PROGRAM[20], rs1_read >> shift), _ => unreachable!(), }; @@ -236,7 +237,7 @@ mod tests { config .rd_written .require_equal( - || "assert_rd_written", + || format!("{prefix}_({name})_assert_rd_written"), &mut cb, &UInt::from_const_unchecked( Value::new_unchecked(expected_rd_written) @@ -255,7 +256,7 @@ mod tests { mock_program_op, rs1_read, rs2_read, - Change::new(0, expected_rd_written), + Change::new(0, rd_written), 0, )], )