diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs
index 2b02d708eb..ba1633e1a7 100644
--- a/o1vm/src/interpreters/riscv32im/constraints.rs
+++ b/o1vm/src/interpreters/riscv32im/constraints.rs
@@ -344,6 +344,15 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         self.variable(position)
     }
 
+    unsafe fn mul_hi_signed_unsigned(
+        &mut self,
+        _x: &Self::Variable,
+        _y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable {
+        self.variable(position)
+    }
+
     unsafe fn div_signed(
         &mut self,
         _x: &Self::Variable,
diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs
index 1797dde93e..59fa7a6bd2 100644
--- a/o1vm/src/interpreters/riscv32im/interpreter.rs
+++ b/o1vm/src/interpreters/riscv32im/interpreter.rs
@@ -1257,6 +1257,20 @@ pub trait InterpreterEnv {
         position: Self::Position,
     ) -> Self::Variable;
 
+    /// Returns `((x * y) >> 32`, 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_hi_signed_unsigned(
+        &mut self,
+        x: &Self::Variable,
+        y: &Self::Variable,
+        position: Self::Position,
+    ) -> Self::Variable;
+
     /// Returns `x / y`, storing the results in `position`.
     ///
     /// # Safety
diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs
index 61d2868886..e9a976ca13 100644
--- a/o1vm/src/interpreters/riscv32im/witness.rs
+++ b/o1vm/src/interpreters/riscv32im/witness.rs
@@ -486,6 +486,21 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
         res
     }
 
+    unsafe fn mul_hi_signed_unsigned(
+        &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 i64)) as u64;
+        let res = (res >> 32) as u32;
+        let res = res as u64;
+        self.write_column(position, res);
+        res
+    }
+
     unsafe fn div_signed(
         &mut self,
         x: &Self::Variable,