From 36d59fe2d8b2048b0d22e4af3fc7eec6b47578aa Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 22:13:49 +0000 Subject: [PATCH] Implement `slt` and `sltu` --- optimism/src/mips/interpreter.rs | 55 ++++++++++++++++++++++++++++++-- optimism/src/mips/witness.rs | 22 +++++++++++++ 2 files changed, 75 insertions(+), 2 deletions(-) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 83d750cd23..a6091417b9 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -534,6 +534,33 @@ pub trait InterpreterEnv { /// `x`. unsafe fn test_zero(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable; + /// Returns 1 if `x < y` as unsigned integers, or 0 otherwise, storing the result in + /// `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned value; callers must assert that the value + /// correctly represents the relationship between `x` and `y` + unsafe fn test_less_than( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + + /// Returns 1 if `x < y` as signed integers, or 0 otherwise, storing the result in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned value; callers must assert that the value + /// correctly represents the relationship between `x` and `y` + unsafe fn test_less_than_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable; fn set_halted(&mut self, flag: Self::Variable); @@ -666,8 +693,32 @@ pub fn interpret_rtype(env: &mut Env, instr: RTypeInstructi RTypeInstruction::Or => (), RTypeInstruction::Xor => (), RTypeInstruction::Nor => (), - RTypeInstruction::SetLessThan => (), - RTypeInstruction::SetLessThanUnsigned => (), + RTypeInstruction::SetLessThan => { + let rs = env.read_register(&rs); + let rt = env.read_register(&rt); + let res = { + // FIXME: Constrain + let pos = env.alloc_scratch(); + unsafe { env.test_less_than_signed(&rs, &rt, pos) } + }; + env.write_register(&rd, res); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); + return; + } + RTypeInstruction::SetLessThanUnsigned => { + let rs = env.read_register(&rs); + let rt = env.read_register(&rt); + let res = { + // FIXME: Constrain + let pos = env.alloc_scratch(); + unsafe { env.test_less_than(&rs, &rt, pos) } + }; + env.write_register(&rd, res); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); + return; + } RTypeInstruction::MultiplyToRegister => (), RTypeInstruction::CountLeadingOnes => (), RTypeInstruction::CountLeadingZeros => (), diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index 77bfc347d3..e23be202be 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -233,6 +233,28 @@ impl InterpreterEnv for Env { res } + unsafe fn test_less_than( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let res = if *x < *y { 1 } else { 0 }; + self.write_column(position, res.into()); + res + } + + unsafe fn test_less_than_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let res = if (*x as i32) < (*y as i32) { 1 } else { 0 }; + self.write_column(position, res.into()); + res + } + fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable { self.write_column(position, (*x).into()); *x