From 845fae3462c98b1cd28f933e03f5bc4850670737 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 22:36:18 +0000 Subject: [PATCH] Implement `srl` --- optimism/src/mips/interpreter.rs | 26 +++++++++++++++++++++++++- optimism/src/mips/witness.rs | 11 +++++++++++ 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 1688798677..8f55f38c04 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -526,6 +526,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( + &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 @@ -665,7 +678,18 @@ pub fn interpret_rtype(env: &mut Env, instr: RTypeInstructi env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); return; } - RTypeInstruction::ShiftRightLogical => (), + RTypeInstruction::ShiftRightLogical => { + 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::ShiftRightArithmetic => (), RTypeInstruction::ShiftLeftLogicalVariable => (), RTypeInstruction::ShiftRightLogicalVariable => (), diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index eeea858713..795a647d65 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -227,6 +227,17 @@ impl InterpreterEnv for Env { res } + unsafe fn shift_right( + &mut self, + x: &Self::Variable, + by: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let res = x >> by; + 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());