diff --git a/ceno_zkvm/src/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/divu.rs index 87afa7484..139ac4999 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/divu.rs @@ -44,7 +44,7 @@ impl Instruction for ArithInstruction Instruction for ShiftImmInstructio // Goal is to constrain: // rs1 == rd_written * imm + remainder let remainder = UInt::new(|| "remainder", circuit_builder)?; - let (rd_imm_mul, rs1) = rd_written.mul_add( + let (rs1, rd_imm_mul) = rd_written.mul_add( || "rd_written * imm +remainder ", circuit_builder, &mut imm, @@ -76,15 +76,14 @@ impl Instruction for ShiftImmInstructio step: &StepRecord, ) -> Result<(), ZKVMError> { let rd_written = Value::new(step.rd().unwrap().value.after, lk_multiplicity); - let imm = Value::new(step.insn().imm_or_funct7(), lk_multiplicity); - // TODO design MulAdd gadget and refactor this to there - let remainder = { + let (remainder, imm) = { let rs1_read = step.rs1().unwrap().value; let imm = step.insn().imm_or_funct7(); - let result = rs1_read.wrapping_div(imm); - let remainder = rs1_read.wrapping_sub(result * imm); - Value::new(remainder, lk_multiplicity) + ( + Value::new(rs1_read % imm, lk_multiplicity), + Value::new(imm, lk_multiplicity), + ) }; let (rs1, rd_imm_mul) = rd_written.mul_add(&imm, &remainder, lk_multiplicity, true); diff --git a/ceno_zkvm/src/uint/arithmetic.rs b/ceno_zkvm/src/uint/arithmetic.rs index a9d0ca415..027ca4257 100644 --- a/ceno_zkvm/src/uint/arithmetic.rs +++ b/ceno_zkvm/src/uint/arithmetic.rs @@ -271,10 +271,7 @@ impl UIntLimbs { ) -> Result<(UIntLimbs, UIntLimbs), ZKVMError> { circuit_builder.namespace(name_fn, |cb| { let c = self.internal_mul(cb, multiplier, with_overflow, is_hi_limb)?; - Ok(( - c.clone(), - c.internal_add(cb, &addend.expr(), with_overflow)?, - )) + Ok((c.internal_add(cb, &addend.expr(), with_overflow)?, c)) }) }