move div relative code to DivConfig

ceno_zkvm/src/gadgets/div.rs

@@ -16,24 +16,29 @@ use super::IsLtConfig;
 #[derive(Debug, Clone)]
 pub struct DivConfig<E: ExtensionField> {
     pub dividend: UInt<E>,
-    pub r_lt: IsLtConfig,
+    pub divisor: UInt<E>,
+    pub(crate) quotient: UInt<E>,
+    pub remainder: UInt<E>,
+
     pub intermediate_mul: UInt<E>,
+    pub r_lt: IsLtConfig,
 }
 
 impl<E: ExtensionField> DivConfig<E> {
     /// giving divisor, quotient, and remainder
     /// deriving dividend and respective constrains
-    /// NOTE once divisor is zero, then constrain will always failed
     pub fn construct_circuit<NR: Into<String> + Display + Clone, N: FnOnce() -> NR>(
         circuit_builder: &mut CircuitBuilder<E>,
         name_fn: N,
-        divisor: &mut UInt<E>,
-        quotient: &mut UInt<E>,
-        remainder: &UInt<E>,
     ) -> Result<Self, ZKVMError> {
         circuit_builder.namespace(name_fn, |cb| {
+            // quotient = dividend / divisor + remainder => dividend = divisor * quotient + r
+            let mut divisor = UInt::new_unchecked(|| "divisor", cb)?;
+            let mut quotient = UInt::new(|| "quotient", cb)?;
+            let remainder = UInt::new(|| "remainder", cb)?;
+
             let (dividend, intermediate_mul) =
-                divisor.mul_add(|| "", cb, quotient, remainder, true)?;
+                divisor.mul_add(|| "", cb, &mut quotient, &remainder, true)?;
 
             // remainder range check
             let r_lt = cb.less_than(
@@ -45,6 +50,9 @@ impl<E: ExtensionField> DivConfig<E> {
             )?;
             Ok(Self {
                 dividend,
+                divisor,
+                quotient,
+                remainder,
                 intermediate_mul,
                 r_lt,
             })
@@ -59,8 +67,13 @@ impl<E: ExtensionField> DivConfig<E> {
         quotient: &Value<'a, u32>,
         remainder: &Value<'a, u32>,
     ) -> Result<(), ZKVMError> {
-        let (dividend, intermediate) = divisor.mul_add(quotient, remainder, lkm, true);
+        self.divisor.assign_limbs(instance, divisor.as_u16_limbs());
+        self.quotient
+            .assign_limbs(instance, quotient.as_u16_limbs());
+        self.remainder
+            .assign_limbs(instance, remainder.as_u16_limbs());
 
+        let (dividend, intermediate) = divisor.mul_add(quotient, remainder, lkm, true);
         self.r_lt
             .assign_instance(instance, lkm, remainder.as_u64(), divisor.as_u64())?;
         self.intermediate_mul

ceno_zkvm/src/instructions/riscv/divu.rs

@@ -15,12 +15,6 @@ use std::marker::PhantomData;
 
 pub struct ArithConfig<E: ExtensionField> {
     r_insn: RInstructionConfig<E>,
-
-    dividend: UInt<E>,
-    divisor: UInt<E>,
-    pub(crate) outcome: UInt<E>,
-
-    remainder: UInt<E>,
     div_config: DivConfig<E>,
     is_zero: IsZeroConfig,
 }
@@ -44,26 +38,20 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
         circuit_builder: &mut CircuitBuilder<E>,
     ) -> Result<Self::InstructionConfig, ZKVMError> {
         // outcome = dividend / divisor + remainder => dividend = divisor * outcome + r
-        let mut divisor = UInt::new_unchecked(|| "divisor", circuit_builder)?;
-        let mut outcome = UInt::new(|| "outcome", circuit_builder)?;
-        let r = UInt::new(|| "remainder", circuit_builder)?;
+        // let mut divisor = UInt::new_unchecked(|| "divisor", circuit_builder)?;
+        // let mut outcome = UInt::new(|| "outcome", circuit_builder)?;
+        // let r = UInt::new(|| "remainder", circuit_builder)?;
 
-        let div_config = DivConfig::construct_circuit(
-            circuit_builder,
-            || "divu",
-            &mut divisor,
-            &mut outcome,
-            &r,
-        )?;
+        let div_config = DivConfig::construct_circuit(circuit_builder, || "divu")?;
 
         // div by zero check
         let is_zero = IsZeroConfig::construct_circuit(
             circuit_builder,
             || "divisor_zero_check",
-            divisor.value(),
+            div_config.divisor.value(),
         )?;
 
-        let outcome_value = outcome.value();
+        let outcome_value = div_config.quotient.value();
         circuit_builder
             .condition_require_equal(
                 || "outcome_is_zero",
@@ -78,16 +66,13 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
             circuit_builder,
             I::INST_KIND,
             div_config.dividend.register_expr(),
-            divisor.register_expr(),
-            outcome.register_expr(),
+            div_config.divisor.register_expr(),
+            div_config.quotient.register_expr(),
         )?;
 
         Ok(ArithConfig {
             r_insn,
-            dividend: div_config.dividend.clone(),
-            divisor,
-            outcome,
-            remainder: r,
+
             div_config,
             is_zero,
         })
@@ -115,21 +100,11 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
 
         // assignment
         config.r_insn.assign_instance(instance, lkm, step)?;
-        config
-            .divisor
-            .assign_limbs(instance, divisor.as_u16_limbs());
-        config
-            .outcome
-            .assign_limbs(instance, outcome.as_u16_limbs());
 
-        let (dividend, _) = divisor.mul_add(&outcome, &r, lkm, true);
         config
             .div_config
             .assign_instance(instance, lkm, &divisor, &outcome, &r)?;
 
-        config.dividend.assign_add_outcome(instance, &dividend);
-        config.remainder.assign_limbs(instance, r.as_u16_limbs());
-
         config
             .is_zero
             .assign_instance(instance, (rs2 as u64).into())?;
@@ -190,7 +165,8 @@ mod test {
                 UInt::from_const_unchecked(Value::new_unchecked(outcome).as_u16_limbs().to_vec());
 
             config
-                .outcome
+                .div_config
+                .quotient
                 .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written)
                 .unwrap();