Merge pull request #1427 from o1-labs/feature/mips/divu

Implement `divu`
o1-labs · Dec 6, 2023 · 3b644c5 · 3b644c5
2 parents a1af812 + 846073d
commit 3b644c5
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 2 deletions.
diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs
@@ -1,4 +1,4 @@
-use crate::mips::registers::{REGISTER_CURRENT_IP, REGISTER_NEXT_IP};
+use crate::mips::registers::{REGISTER_CURRENT_IP, REGISTER_HI, REGISTER_LO, REGISTER_NEXT_IP};
 use log::debug;
 use strum_macros::{EnumCount, EnumIter};
 
@@ -636,6 +636,22 @@ pub trait InterpreterEnv {
         position: Self::Position,
     ) -> Self::Variable;
 
+    /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and
+    /// `position_remainder` respectively.
+    ///
+    /// # Safety
+    ///
+    /// There are no constraints on the returned values; callers must manually add constraints to
+    /// ensure that the pair of returned values correspond to the given values `x` and `y`, and
+    /// that they fall within the desired range.
+    unsafe fn divmod(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position_quotient: Self::Position,
+        position_remainder: Self::Position,
+    ) -> (Self::Variable, Self::Variable);
+
     fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable;
 
     fn set_halted(&mut self, flag: Self::Variable);
@@ -786,7 +802,21 @@ pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RTypeInstructi
         RTypeInstruction::Multiply => (),
         RTypeInstruction::MultiplyUnsigned => (),
         RTypeInstruction::Div => (),
-        RTypeInstruction::DivUnsigned => (),
+        RTypeInstruction::DivUnsigned => {
+            let rs = env.read_register(&rs);
+            let rt = env.read_register(&rt);
+            let (quotient, remainder) = {
+                // Fixme: constrain
+                let quotient_pos = env.alloc_scratch();
+                let remainder_pos = env.alloc_scratch();
+                unsafe { env.divmod(&rs, &rt, quotient_pos, remainder_pos) }
+            };
+            env.write_register(&Env::constant(REGISTER_LO as u32), quotient);
+            env.write_register(&Env::constant(REGISTER_HI as u32), remainder);
+            env.set_instruction_pointer(next_instruction_pointer.clone());
+            env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
+            return;
+        }
         RTypeInstruction::Add => {
             let rs = env.read_register(&rs);
             let rt = env.read_register(&rt);

diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs
@@ -310,6 +310,20 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         res
     }
 
+    unsafe fn divmod(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position_quotient: Self::Position,
+        position_remainder: Self::Position,
+    ) -> (Self::Variable, Self::Variable) {
+        let q = x / y;
+        let r = x % y;
+        self.write_column(position_quotient, q.into());
+        self.write_column(position_remainder, r.into());
+        (q, r)
+    }
+
     fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable {
         self.write_column(position, (*x).into());
         *x