o1vm/MIPSinterpreter: is_zero change

o1-labs · Oct 24, 2024 · 7d650a4 · 7d650a4
1 parent f0aa273
commit 7d650a4
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 15 deletions.
diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs
@@ -213,6 +213,22 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         self.variable(position)
     }
 
+    fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable {
+        let res = {
+            let pos = self.alloc_scratch();
+            unsafe { self.test_zero(x, pos) }
+        };
+        let x_inv_or_zero = {
+            let pos = self.alloc_scratch();
+            unsafe { self.inverse_or_zero(x, pos) }
+        };
+        // If x = 0, then res = 1 and x_inv_or_zero = 0
+        // If x <> 0, then res = 0 and x_inv_or_zero = x^(-1)
+        self.add_constraint(x.clone() * x_inv_or_zero.clone() + res.clone() - Self::constant(1));
+        self.add_constraint(x.clone() * res.clone());
+        res
+    }
+
     unsafe fn inverse_or_zero(
         &mut self,
         _x: &Self::Variable,

diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs
@@ -698,21 +698,7 @@ pub trait InterpreterEnv {
         position: Self::Position,
     ) -> Self::Variable;
 
-    fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable {
-        let res = {
-            let pos = self.alloc_scratch();
-            unsafe { self.test_zero(x, pos) }
-        };
-        let x_inv_or_zero = {
-            let pos = self.alloc_scratch();
-            unsafe { self.inverse_or_zero(x, pos) }
-        };
-        // If x = 0, then res = 1 and x_inv_or_zero = 0
-        // If x <> 0, then res = 0 and x_inv_or_zero = x^(-1)
-        self.add_constraint(x.clone() * x_inv_or_zero.clone() + res.clone() - Self::constant(1));
-        self.add_constraint(x.clone() * res.clone());
-        res
-    }
+    fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable;
 
     /// Returns 1 if `x` is equal to `y`, or 0 otherwise, storing the result in `position`.
     fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable;

diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs
@@ -361,6 +361,23 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI
         }
     }
 
+    fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable {
+        // write the result
+        let pos = self.alloc_scratch();
+        let res = if *x == 0 { 1 } else { 0 };
+        self.write_column(pos, res);
+        // write the non deterministic advice inv_or_zero
+        let pos = self.alloc_scratch();
+        let inv_or_zero = if *x == 0 {
+            Fp::zero()
+        } else {
+            Fp::inverse(&Fp::from(*x)).unwrap()
+        };
+        self.write_field_column(pos, inv_or_zero);
+        // return the result
+        res
+    }
+
     fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable {
         // We replicate is_zero(x-y), but working on field elt,
         // to avoid subtraction overflow in the witness interpreter for u32