SRAI

ceno_zkvm/src/chip_handler/general.rs

@@ -168,7 +168,13 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
         NR: Into<String>,
         N: FnOnce() -> NR,
     {
-        self.namespace(|| "require_equal", |cb| cb.cs.require_zero(name_fn, a - b))
+        self.namespace(
+            || "require_equal",
+            |cb| {
+                cb.cs
+                    .require_zero(name_fn, a.to_monomial_form() - b.to_monomial_form())
+            },
+        )
     }
 
     pub fn require_one<NR, N>(&mut self, name_fn: N, expr: Expression<E>) -> Result<(), ZKVMError>

ceno_zkvm/src/expression.rs

@@ -757,7 +757,9 @@ pub mod fmt {
     ) -> String {
         match expression {
             Expression::WitIn(wit_in) => {
-                wtns.push(*wit_in);
+                if !wtns.contains(wit_in) {
+                    wtns.push(*wit_in);
+                }
                 format!("WitIn({})", wit_in)
             }
             Expression::Challenge(id, pow, scaler, offset) => {

ceno_zkvm/src/instructions/riscv/config.rs

@@ -18,11 +18,11 @@ pub struct MsbConfig {
     pub high_limb_no_msb: WitIn,
 }
 
-pub struct MsbInput<'a> {
-    pub limbs: &'a [u8],
+pub struct MsbInput<'a, T> {
+    pub limbs: &'a [T],
 }
 
-impl MsbInput<'_> {
+impl MsbInput<'_, u8> {
     pub fn assign<F: SmallField>(
         &self,
         instance: &mut [MaybeUninit<F>],
@@ -43,6 +43,28 @@ impl MsbInput<'_> {
     }
 }
 
+impl MsbInput<'_, u16> {
+    pub fn assign<F: SmallField>(
+        &self,
+        instance: &mut [MaybeUninit<F>],
+        config: &MsbConfig,
+        lk_multiplicity: &mut LkMultiplicity,
+    ) -> (u16, u16) {
+        let n_limbs = self.limbs.len();
+        assert!(n_limbs > 0);
+        let high_limb = self.limbs[n_limbs - 1];
+        let msb = high_limb >> 15;
+        assert!(msb == 0 || msb == 1);
+        set_val!(instance, config.msb, { i64_to_base::<F>(msb as i64) });
+        let high_limb_no_msb = high_limb & 0b0111_1111_1111_1111;
+        set_val!(instance, config.high_limb_no_msb, {
+            i64_to_base::<F>(high_limb_no_msb as i64)
+        });
+        lk_multiplicity.assert_ux::<16>((high_limb_no_msb as u64) * 2);
+        (msb, high_limb_no_msb)
+    }
+}
+
 #[derive(Clone)]
 pub struct UIntLtuConfig {
     pub indexes: Vec<WitIn>,