all test passed

ceno_zkvm/src/chip_handler/general.rs

@@ -180,7 +180,6 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
             16 => self.assert_u16(name_fn, expr),
             8 => self.assert_byte(name_fn, expr),
             5 => self.assert_u5(name_fn, expr),
-            1 => self.assert_bit(name_fn, expr),
             c => panic!("Unsupported bit range {c}"),
         }
     }
@@ -316,18 +315,19 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
     }
 
     /// less_than
-    pub(crate) fn less_than<N, NR, const MAX_U16_LIMB: usize>(
+    pub(crate) fn less_than<N, NR>(
         &mut self,
         name_fn: N,
         lhs: Expression<E>,
         rhs: Expression<E>,
         assert_less_than: Option<bool>,
+        max_num_u16_limbs: usize,
     ) -> Result<IsLtConfig, ZKVMError>
     where
         NR: Into<String> + Display + Clone,
         N: FnOnce() -> NR,
     {
-        IsLtConfig::construct_circuit(self, name_fn, lhs, rhs, assert_less_than, MAX_U16_LIMB)
+        IsLtConfig::construct_circuit(self, name_fn, lhs, rhs, assert_less_than, max_num_u16_limbs)
     }
 
     pub(crate) fn is_equal(

ceno_zkvm/src/chip_handler/memory.rs

@@ -50,7 +50,13 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> MemoryChipOpera
             cb.write_record(|| "write_record", write_record)?;
 
             // assert prev_ts < current_ts
-            let lt_cfg = cb.less_than::<_, _, UINT_LIMBS>(|| "prev_ts < ts", prev_ts, ts.clone(), Some(true))?;
+            let lt_cfg = cb.less_than(
+                || "prev_ts < ts",
+                prev_ts,
+                ts.clone(),
+                Some(true),
+                UINT_LIMBS,
+            )?;
 
             let next_ts = ts + 1.into();
 
@@ -96,11 +102,12 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> MemoryChipOpera
             cb.read_record(|| "read_record", read_record)?;
             cb.write_record(|| "write_record", write_record)?;
 
-            let lt_cfg = cb.less_than::<_, _, UINT_LIMBS>(
+            let lt_cfg = cb.less_than(
                 || "prev_ts < ts",
                 prev_ts,
                 ts.clone(),
                 Some(true),
+                UINT_LIMBS,
             )?;
 
             let next_ts = ts + 1.into();

ceno_zkvm/src/chip_handler/register.rs

@@ -51,11 +51,12 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
             cb.write_record(|| "write_record", write_record)?;
 
             // assert prev_ts < current_ts
-            let lt_cfg = cb.less_than::<_, _, UINT_LIMBS>(
+            let lt_cfg = cb.less_than(
                 || "prev_ts < ts",
                 prev_ts,
                 ts.clone(),
                 Some(true),
+                UINT_LIMBS,
             )?;
 
             let next_ts = ts + 1.into();
@@ -101,11 +102,12 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
             cb.read_record(|| "read_record", read_record)?;
             cb.write_record(|| "write_record", write_record)?;
 
-            let lt_cfg = cb.less_than::<_, _, UINT_LIMBS>(
+            let lt_cfg = cb.less_than(
                 || "prev_ts < ts",
                 prev_ts,
                 ts.clone(),
                 Some(true),
+                UINT_LIMBS,
             )?;
 
             let next_ts = ts + 1.into();

ceno_zkvm/src/gadgets/is_lt.rs

@@ -95,7 +95,6 @@ impl IsLtConfig {
     }
 
     pub fn cal_diff(is_lt: bool, max_num_u16_limbs: usize, lhs: u64, rhs: u64) -> u64 {
-        println!("max_num_u16_limbs {max_num_u16_limbs}");
         let diff = if is_lt {
             1u64 << (u16::BITS as usize * max_num_u16_limbs)
         } else {

ceno_zkvm/src/instructions/riscv/arith.rs

@@ -440,6 +440,10 @@ mod test {
             .unwrap()
             .unwrap();
 
+        let a = Value::<'_, u32>::new_unchecked(u32::MAX);
+        let b = Value::<'_, u32>::new_unchecked(u32::MAX);
+        let (c_limb, _, _) = a.mul(&b, &mut LkMultiplicity::default(), true);
+
         // values assignment
         let (raw_witin, _) = MulInstruction::assign_instances(
             &config,
@@ -448,9 +452,9 @@ mod test {
                 3,
                 MOCK_PC_MUL,
                 MOCK_PROGRAM[2],
-                4294901760,
-                4294901760,
-                Change::new(0, 0),
+                a.as_u64() as u32,
+                b.as_u64() as u32,
+                Change::new(0, Value::<u32>::from_limb_unchecked(c_limb).as_u64() as u32),
                 0,
             )],
         )

ceno_zkvm/src/instructions/riscv/divu.rs

@@ -124,15 +124,19 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
         config
             .inter_mul_value
             .assign_carries(instance, &mul_carries);
+        config.inter_mul_value.assign_carries_auxiliary(
+            instance,
+            lkm,
+            &mul_carries,
+            max_carry_value,
+        )?;
+
         config.remainder.assign_limbs(instance, r.as_u16_limbs());
 
         config
             .dividend
             .assign_limbs(instance, dividend.as_u16_limbs());
         config.dividend.assign_carries(instance, &add_carries);
-        config
-            .dividend
-            .assign_carries_auxiliary(instance, lkm, &add_carries, max_carry_value)?;
 
         config
             .is_zero
@@ -204,6 +208,7 @@ mod test {
             verify("dividend > divisor", 10, 11, 0);
             verify("remainder", 11, 2, 5);
             verify("u32::MAX", u32::MAX, u32::MAX, 1);
+            verify("div u32::MAX", 3, u32::MAX, 0);
             verify("u32::MAX div by 2", u32::MAX, 2, u32::MAX / 2);
             verify("div by zero", 10, 0, u32::MAX);
             verify("mul carry", 1202729773, 171818539, 7);

ceno_zkvm/src/lib.rs

@@ -1,8 +1,6 @@
 #![feature(box_patterns)]
 #![feature(stmt_expr_attributes)]
 #![feature(variant_count)]
-#![allow(incomplete_features)]
-#![feature(generic_const_exprs)]
 
 pub mod error;
 pub mod instructions;

ceno_zkvm/src/scheme/mock_prover.rs

@@ -768,7 +768,7 @@ mod tests {
         fn construct_circuit(cb: &mut CircuitBuilder<GoldilocksExt2>) -> Result<Self, ZKVMError> {
             let a = cb.create_witin(|| "a")?;
             let b = cb.create_witin(|| "b")?;
-            let lt_wtns = cb.less_than::<_, _, 1>(|| "lt", a.expr(), b.expr(), Some(true))?;
+            let lt_wtns = cb.less_than(|| "lt", a.expr(), b.expr(), Some(true), 1)?;
             Ok(Self { a, b, lt_wtns })
         }
 
@@ -888,7 +888,7 @@ mod tests {
         fn construct_circuit(cb: &mut CircuitBuilder<GoldilocksExt2>) -> Result<Self, ZKVMError> {
             let a = cb.create_witin(|| "a")?;
             let b = cb.create_witin(|| "b")?;
-            let lt_wtns = cb.less_than::<_, _, 1>(|| "lt", a.expr(), b.expr(), None)?;
+            let lt_wtns = cb.less_than(|| "lt", a.expr(), b.expr(), None, 1)?;
             Ok(Self { a, b, lt_wtns })
         }
 

ceno_zkvm/src/uint.rs

@@ -26,6 +26,7 @@ use std::{
 pub use strum::IntoEnumIterator;
 use strum_macros::EnumIter;
 use sumcheck::util::ceil_log2;
+use util::max_degree_2_carry_value;
 
 #[derive(Clone, EnumIter, Debug)]
 pub enum UintLimb<E: ExtensionField> {
@@ -562,10 +563,11 @@ pub struct Value<'a, T: Into<u64> + From<u32> + Copy + Default> {
 // TODO generalize to support non 16 bit limbs
 // TODO optimize api with fixed size array
 impl<'a, T: Into<u64> + From<u32> + Copy + Default> Value<'a, T> {
-    const LIMBS: usize = {
-        let u16_bytes = (u16::BITS / 8) as usize;
-        mem::size_of::<T>() / u16_bytes
-    };
+    const M: usize = { mem::size_of::<T>() * 8 };
+
+    const C: usize = 16;
+
+    const LIMBS: usize = (Self::M + 15) / 16;
 
     pub fn new(val: T, lkm: &mut LkMultiplicity) -> Self {
         let uint = Value::<T> {
@@ -699,30 +701,31 @@ impl<'a, T: Into<u64> + From<u32> + Copy + Default> Value<'a, T> {
         let mut c_limbs = vec![0u16; num_limbs];
         let mut carries = vec![0u64; num_limbs];
         // TODO FIXME: support full size multiplication
-        let tx = vec![0u64; num_limbs];
+        let mut tmp = vec![0u64; num_limbs];
         a_limbs.iter().enumerate().for_each(|(i, &a_limb)| {
             b_limbs.iter().enumerate().for_each(|(j, &b_limb)| {
                 let idx = i + j;
                 if idx < num_limbs {
-                    let (c, overflow_mul) = a_limb.overflowing_mul(b_limb);
-                    let (ret, overflow_add) = c_limbs[idx].overflowing_add(c);
-
-                    c_limbs[idx] = ret;
-                    carries[idx] += overflow_add as u64;
-                    if overflow_mul {
-                        carries[idx] += ((a_limb as u32 * b_limb as u32) / (1 << 16)) as u64;
-                    }
+                    tmp[idx] += a_limb as u64 * b_limb as u64;
                 }
             })
         });
-        // complete the computation by adding prev_carry
-        (1..num_limbs).for_each(|i| {
-            if carries[i - 1] > 0 {
-                let (ret, overflow) = c_limbs[i].overflowing_add(carries[i - 1]);
-                c_limbs[i] = ret;
-                carries[i] += overflow as u64;
-            }
-        });
+
+        tmp.iter()
+            .into_iter()
+            .zip(c_limbs.iter_mut())
+            .enumerate()
+            .for_each(|(i, (tmp, limb))| {
+                // tmp + prev_carry - carry * Self::LIMB_BASE_MUL
+                let mut tmp = *tmp;
+                if i > 0 {
+                    tmp = tmp + carries[i - 1];
+                }
+                // update carry
+                carries[i] = tmp >> Self::C;
+                // update limb
+                *limb = (tmp - (carries[i] << Self::C)) as u16;
+            });
 
         if !with_overflow {
             // If the outcome overflows, `with_overflow` can't be false
@@ -733,10 +736,8 @@ impl<'a, T: Into<u64> + From<u32> + Copy + Default> Value<'a, T> {
         // range check
         c_limbs.iter().for_each(|c| lkm.assert_ux::<16>(*c as u64));
         // calculate max possible carry value
-        let max_carry_value: u64 = u16::MAX as u64 * u16::MAX as u64 // 2^C * 2^C
-        * (2 * Self::LIMBS - 1) as u64; // max number of limbs for degree 2 mul
 
-        (c_limbs, carries, max_carry_value)
+        (c_limbs, carries, max_degree_2_carry_value(Self::M, Self::C))
     }
 }
 

ceno_zkvm/src/uint/arithmetic.rs

@@ -114,12 +114,7 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
         let Some(carries) = &c.carries else {
             return Err(ZKVMError::CircuitError);
         };
-        println!(
-            "MAX_DEGREE_2_MUL_CARRY_BITS {:?} Self::MAX_DEGREE_2_MUL_CARRY_BITS_POW2 {:?} Self::MAX_DEGREE_2_MUL_CARRY_U16_LIMB {:?}",
-            Self::MAX_DEGREE_2_MUL_CARRY_BITS,
-            Self::MAX_DEGREE_2_MUL_CARRY_VALUE,
-            Self::MAX_DEGREE_2_MUL_CARRY_U16_LIMB
-        );
+
         c.carries_auxiliray_lt_config = Some(
             carries
                 .iter()
@@ -1090,36 +1085,32 @@ mod tests {
 
         #[test]
         fn test_mul_overflow() {
+            let a = Value::<'_, u32>::new_unchecked(u32::MAX);
+            let b = Value::<'_, u32>::new_unchecked(u32::MAX);
+            let (c_limb, c_carry, _) = a.mul(&b, &mut LkMultiplicity::default(), true);
             let witness_values: Vec<ArcMultilinearExtension<E>> = vec![
                 // alloc a = 2^16 + (2^16 -1) * 2^16
                 vec![u16::MAX as u64, u16::MAX as u64],
                 // alloc b = 2^16 + (2^16 - 1) * 2^16
                 vec![u16::MAX as u64, u16::MAX as u64],
                 // mul_c = a * b,
                 // alloc c [1, 0xfffe, 0xffff, 0] with lo part only
-                vec![1, 0xfffe],
+                c_limb.iter().map(|v| *v as u64).collect_vec(),
                 // c carry
-                vec![0x1fffd, 0],
+                c_carry.iter().map(|v| *v as u64).collect_vec(),
                 // each carry alloc with diff
-                calculate_carry_diff::<32, 16>(vec![0x1fffd, 0]),
+                calculate_carry_diff::<32, 16>(c_carry.to_vec()),
             ]
             .concat()
             .into_arc_mle();
 
-            let a = Value::<'_, u32>::new_unchecked(u32::MAX);
-            let b = Value::<'_, u32>::new_unchecked(u32::MAX);
-            let (limb, carry, max_carry_value) = a.mul(&b, &mut LkMultiplicity::default(), false);
-            println!(
-                "limb {:?} carry {:?} max_carry_value {max_carry_value}",
-                limb, carry
-            );
             let mut cs = ConstraintSystem::new(|| "test_mul_add");
             let mut cb = CircuitBuilder::<E>::new(&mut cs);
 
             let mut uint_a = UIntLimbs::<32, 16, E>::new(|| "uint_a", &mut cb).unwrap();
             let mut uint_b = UIntLimbs::<32, 16, E>::new(|| "uint_b", &mut cb).unwrap();
             let _ = uint_a
-                .mul(|| "mul_add", &mut cb, &mut uint_b, false)
+                .mul(|| "mul_add", &mut cb, &mut uint_b, true)
                 .unwrap();
 
             MockProver::assert_satisfied(&cb, &witness_values, None);

ceno_zkvm/src/uint/constants.rs

@@ -1,6 +1,6 @@
 use crate::utils::const_min;
 
-use super::UIntLimbs;
+use super::{util::max_degree_2_carry_value, UIntLimbs};
 
 pub const RANGE_CHIP_BIT_WIDTH: usize = 16;
 pub const BYTE_BIT_WIDTH: usize = 8;
@@ -29,13 +29,7 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
     pub const N_RANGE_CELLS: usize = Self::NUM_CELLS * Self::N_RANGE_CELLS_PER_CELL;
 
     /// Max carry value during degree 2 limb multiplication
-    pub const MAX_DEGREE_2_MUL_CARRY_VALUE: u64 = {
-        assert!(M <= u64::BITS as usize);
-        let max_carry_value: u128 = ((1 << C) - 1) as u128 * ((1 << C) - 1 ) as u128 // 2^C * 2^C
-            * (2 * Self::NUM_CELLS - 1) as u128; // max number of limbs for degree 2 mul
-        assert!(max_carry_value <= u64::MAX as u128);
-        max_carry_value as u64
-    };
+    pub const MAX_DEGREE_2_MUL_CARRY_VALUE: u64 = max_degree_2_carry_value(Self::M, Self::C);
 
     /// Min bits to cover MAX_DEGREE_2_MUL_CARRY_VALUE
     pub const MAX_DEGREE_2_MUL_CARRY_BITS: usize = {