From ebcd6bb5bfd09720c9a6c28ddae34ea4f593d45b Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:22:33 +0100 Subject: [PATCH 1/2] o1vm/riscv32: implement mul_lo_signed --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 11dee8a230..82b9cd5105 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -336,6 +336,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mul_lo_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 1e41918b20..2cd83827a1 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1215,6 +1215,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `(x * y) & ((1 << 32) - 1))`, 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 mul_lo_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` /// and `position_lo` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 0418852ae9..658048bf99 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -456,6 +456,21 @@ impl InterpreterEnv for Env { res } + unsafe fn mul_lo_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) as i64) * ((y as i32) as i64)) as u64; + let res = (res & ((1 << 32) - 1)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_hi_lo_signed( &mut self, x: &Self::Variable, From 95098af4c18c79cc880f1e2da0dd76399b470423 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:46:42 +0100 Subject: [PATCH 2/2] o1vm/riscv32im: simplify mul_lo_signed implementation --- 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 658048bf99..3484ad0a10 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -462,9 +462,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) as i64) * ((y as i32) as i64)) as u64; + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = ((x as i64) * (y as i64)) as u64; let res = (res & ((1 << 32) - 1)) as u32; let res = res as u64; self.write_column(position, res);