From 0ad5fea2a06952e9f1c5dcf10bd08ef9404fcad1 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:47:06 +0100 Subject: [PATCH 1/2] o1vm/riscv32: implement mod_signed It will be used to implement MInstruction::Rem in a follow-up PR. --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+) 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..6c87d64b8e 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: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = ((x as i32) % (y as i32)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn divmod_signed( &mut self, x: &Self::Variable, From 4e0220dbd6c09aaff3578d8f8a3f322674f4c9f4 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:57:40 +0100 Subject: [PATCH 2/2] o1vm/riscv32im: simplify mod_signed --- o1vm/src/interpreters/riscv32im/witness.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 6c87d64b8e..bb0e0cf6c5 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -521,9 +521,9 @@ impl InterpreterEnv for Env { y: &Self::Variable, position: Self::Position, ) -> Self::Variable { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let res = ((x as i32) % (y as i32)) as u32; + 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