Merge pull request #1410 from o1-labs/feature/stlu

Implement `slt` and `sltu`
o1-labs · Dec 6, 2023 · 758b5be · 758b5be
2 parents b1f600a + 36d59fe
commit 758b5be
Show file tree

Hide file tree

Showing 2 changed files with 75 additions and 2 deletions.
diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs
@@ -542,6 +542,33 @@ pub trait InterpreterEnv {
     /// `x`.
     unsafe fn test_zero(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable;
 
+    /// Returns 1 if `x < y` as unsigned integers, or 0 otherwise, storing the result in
+    /// `position`.
+    ///
+    /// # Safety
+    ///
+    /// There are no constraints on the returned value; callers must assert that the value
+    /// correctly represents the relationship between `x` and `y`
+    unsafe fn test_less_than(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable;
+
+    /// Returns 1 if `x < y` as signed integers, or 0 otherwise, storing the result in `position`.
+    ///
+    /// # Safety
+    ///
+    /// There are no constraints on the returned value; callers must assert that the value
+    /// correctly represents the relationship between `x` and `y`
+    unsafe fn test_less_than_signed(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable;
+
     fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable;
 
     fn set_halted(&mut self, flag: Self::Variable);
@@ -674,8 +701,32 @@ pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RTypeInstructi
         RTypeInstruction::Or => (),
         RTypeInstruction::Xor => (),
         RTypeInstruction::Nor => (),
-        RTypeInstruction::SetLessThan => (),
-        RTypeInstruction::SetLessThanUnsigned => (),
+        RTypeInstruction::SetLessThan => {
+            let rs = env.read_register(&rs);
+            let rt = env.read_register(&rt);
+            let res = {
+                // FIXME: Constrain
+                let pos = env.alloc_scratch();
+                unsafe { env.test_less_than_signed(&rs, &rt, pos) }
+            };
+            env.write_register(&rd, res);
+            env.set_instruction_pointer(next_instruction_pointer.clone());
+            env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
+            return;
+        }
+        RTypeInstruction::SetLessThanUnsigned => {
+            let rs = env.read_register(&rs);
+            let rt = env.read_register(&rt);
+            let res = {
+                // FIXME: Constrain
+                let pos = env.alloc_scratch();
+                unsafe { env.test_less_than(&rs, &rt, pos) }
+            };
+            env.write_register(&rd, res);
+            env.set_instruction_pointer(next_instruction_pointer.clone());
+            env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
+            return;
+        }
         RTypeInstruction::MultiplyToRegister => (),
         RTypeInstruction::CountLeadingOnes => (),
         RTypeInstruction::CountLeadingZeros => (),

diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs
@@ -233,6 +233,28 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         res
     }
 
+    unsafe fn test_less_than(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable {
+        let res = if *x < *y { 1 } else { 0 };
+        self.write_column(position, res.into());
+        res
+    }
+
+    unsafe fn test_less_than_signed(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable {
+        let res = if (*x as i32) < (*y as i32) { 1 } else { 0 };
+        self.write_column(position, res.into());
+        res
+    }
+
     fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable {
         self.write_column(position, (*x).into());
         *x