diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 255b935f12..48e28d8aaa 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -547,6 +547,19 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Return the result of shifting `x` by `by`, storing the result in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned value; callers must assert the relationship with + /// the source variable `x` and the shift amount `by`. + unsafe fn shift_right_arithmetic( + &mut self, + x: &Self::Variable, + by: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns 1 if `x` is 0, or 0 otherwise, storing the result in `position`. /// /// # Safety @@ -698,7 +711,18 @@ pub fn interpret_rtype(env: &mut Env, instr: RTypeInstructi env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); return; } - RTypeInstruction::ShiftRightArithmetic => (), + RTypeInstruction::ShiftRightArithmetic => { + let rt = env.read_register(&rt); + // FIXME: Constrain this value + let shifted = unsafe { + let pos = env.alloc_scratch(); + env.shift_right(&rt, &shamt, pos) + }; + env.write_register(&rd, shifted); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); + return; + } RTypeInstruction::ShiftLeftLogicalVariable => (), RTypeInstruction::ShiftRightLogicalVariable => (), RTypeInstruction::ShiftRightArithmeticVariable => (), diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index 517d02339b..c111c767a8 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -238,6 +238,17 @@ impl InterpreterEnv for Env { res } + unsafe fn shift_right_arithmetic( + &mut self, + x: &Self::Variable, + by: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let res = ((*x as i32) >> by) as u32; + self.write_column(position, res.into()); + res + } + unsafe fn test_zero(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable { let res = if *x == 0 { 1 } else { 0 }; self.write_column(position, res.into());