Merge branch 'sai/branch-gteu' into sai/pass-fibb7-test

book/src/SUMMARY.md

@@ -17,7 +17,7 @@
 - [Commitments](./fundamentals/zkbook_commitment.md)
 - [Polynomial Commitments](./plonk/polynomial_commitments.md)
   - [Inner Product Argument](./plonk/inner_product.md)
-  - [Different Functionnalities](./plonk/inner_product_api.md)
+  - [Different Functionalities](./plonk/inner_product_api.md)
 - [Two Party Computation](./fundamentals/zkbook_2pc/overview.md)
   - [Garbled Circuits](./fundamentals/zkbook_2pc/gc.md)
     - [Basics](./fundamentals/zkbook_2pc/basics.md)

book/src/plonk/zkpm.md

@@ -58,7 +58,7 @@ $$
   = Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)]$$
 
 
-The modified permuation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows.
+The modified permutation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows.
 
 * For all $h \in H$, $L_1(h)(Z(h) - 1) = 0$
 * For all $h \in \blue{H\setminus \{h_{n-k}, \ldots, h_n\}}$, $$\begin{aligned}  & Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\

o1vm/README-optimism.md

@@ -3,7 +3,7 @@
 Install the first dependencies:
 ```
 sudo apt update
-# chrony will ensure the system clock is open to date
+# chrony will ensure the system clock is up to date
 sudo apt install build-essential git vim chrony ufw -y
 ```
 

o1vm/src/interpreters/riscv32im/constraints.rs

@@ -77,8 +77,8 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         // No-op, witness only
     }
 
-    fn check_boolean(_x: &Self::Variable) {
-        // No-op, witness only
+    fn assert_boolean(&mut self, x: &Self::Variable) {
+        self.add_constraint(x.clone() * x.clone() - x.clone());
     }
 
     fn add_lookup(&mut self, lookup: Lookup<Self::Variable>) {

o1vm/src/interpreters/riscv32im/interpreter.rs

@@ -598,14 +598,8 @@ pub trait InterpreterEnv {
         self.add_constraint(x - y);
     }
 
-    /// Check that the witness value `x` is a boolean (`0` or `1`); otherwise abort.
-    fn check_boolean(x: &Self::Variable);
-
     /// Assert that the value `x` is boolean, and add a constraint in the proof system.
-    fn assert_boolean(&mut self, x: Self::Variable) {
-        Self::check_boolean(&x);
-        self.add_constraint(x.clone() * x.clone() - x);
-    }
+    fn assert_boolean(&mut self, x: &Self::Variable);
 
     fn add_lookup(&mut self, lookup: Lookup<Self::Variable>);
 
@@ -2138,11 +2132,8 @@ pub fn interpret_stype<Env: InterpreterEnv>(env: &mut Env, instr: SInstruction)
 /// Following the documentation found
 /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf)
 pub fn interpret_sbtype<Env: InterpreterEnv>(env: &mut Env, instr: SBInstruction) {
-    /* fetch instruction pointer from the program state */
     let instruction_pointer = env.get_instruction_pointer();
-    /* compute the next instruction ptr and add one, as well record raml lookup */
     let next_instruction_pointer = env.get_next_instruction_pointer();
-    /* read instruction from ip address */
     let instruction = {
         let v0 = env.read_memory(&instruction_pointer);
         let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1)));
@@ -2153,13 +2144,11 @@ pub fn interpret_sbtype<Env: InterpreterEnv>(env: &mut Env, instr: SBInstruction
             + (v1 * Env::constant(1 << 8))
             + v0
     };
-    /* fetch opcode from instruction bit 0 - 6 for a total len of 7 */
-
     let opcode = {
         let pos = env.alloc_scratch();
         unsafe { env.bitmask(&instruction, 7, 0, pos) }
     };
-    /* verify opcode is 7 bits */
+
     env.range_check8(&opcode, 7);
 
     let funct3 = {
@@ -2186,7 +2175,7 @@ pub fn interpret_sbtype<Env: InterpreterEnv>(env: &mut Env, instr: SBInstruction
             unsafe { env.bitmask(&instruction, 8, 7, pos) }
         };
 
-        env.range_check8(&imm11, 1);
+        env.assert_boolean(&imm11);
 
         let imm1_4 = {
             let pos = env.alloc_scratch();
@@ -2204,7 +2193,7 @@ pub fn interpret_sbtype<Env: InterpreterEnv>(env: &mut Env, instr: SBInstruction
             let pos = env.alloc_scratch();
             unsafe { env.bitmask(&instruction, 32, 31, pos) }
         };
-        env.range_check8(&imm12, 1);
+        env.assert_boolean(&imm12);
 
         // check correctness of decomposition of SB type function
         env.add_constraint(

o1vm/src/interpreters/riscv32im/witness.rs

@@ -88,8 +88,8 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         assert_eq!(*x, *y);
     }
 
-    fn check_boolean(x: &Self::Variable) {
-        if !(*x == 0 || *x == 1) {
+    fn assert_boolean(&mut self, x: &Self::Variable) {
+        if *x != 0 && *x != 1 {
             panic!("The value {} is not a boolean", *x);
         }
     }