diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 5f8236aed7..67bfa46fea 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -353,6 +353,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mod_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 438abaa065..7e0826abad 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1271,6 +1271,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `x % y`, storing the results in `position`. + /// + /// # 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 mod_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 895ab46e1c..bb0e0cf6c5 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -515,6 +515,20 @@ impl InterpreterEnv for Env { res } + unsafe fn mod_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = (x % y) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn divmod_signed( &mut self, x: &Self::Variable,