From 297a88a7362532914ed4d13ae580a0071dcca91a Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 21:37:09 +0000 Subject: [PATCH 1/4] Add `equals_zero` helper function --- optimism/src/mips/interpreter.rs | 12 ++++++++++++ optimism/src/mips/witness.rs | 10 ++++++++++ 2 files changed, 22 insertions(+) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index e58ebc547c..15f171de40 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -526,6 +526,18 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns 1 if `x` is 0, or 0 otherwise, storing the result in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned value; callers must assert the relationship with + /// `x`. + unsafe fn equals_zero( + &mut self, + x: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + fn set_halted(&mut self, flag: Self::Variable); fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable { diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index eb9e4b58da..88608825a2 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -227,6 +227,16 @@ impl InterpreterEnv for Env { res } + unsafe fn equals_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()); + res + } + fn set_halted(&mut self, flag: Self::Variable) { if flag == 0 { self.halt = false From cb8cf82ec7695e7271ed0c346163784556e2dfde Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 21:39:14 +0000 Subject: [PATCH 2/4] Add `copy` helper function --- optimism/src/mips/interpreter.rs | 2 ++ optimism/src/mips/witness.rs | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 15f171de40..7f358b7b2d 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -538,6 +538,8 @@ pub trait InterpreterEnv { 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); fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable { diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index 88608825a2..32f1c3964a 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -237,6 +237,11 @@ impl InterpreterEnv for Env { res } + fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable { + self.write_column(position, (*x).into()); + *x + } + fn set_halted(&mut self, flag: Self::Variable) { if flag == 0 { self.halt = false From 2bc2de215dbad7fe82e7b120e333687f447e31d7 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 21:47:45 +0000 Subject: [PATCH 3/4] Implement `beq` --- optimism/src/mips/interpreter.rs | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 7f358b7b2d..3f0941f06a 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -756,7 +756,25 @@ pub fn interpret_itype(env: &mut Env, instr: ITypeInstructi unsafe { env.bitmask(&instruction, 16, 0, pos) } }; match instr { - ITypeInstruction::BranchEq => (), + ITypeInstruction::BranchEq => { + let offset = env.sign_extend(&(immediate * Env::constant(1 << 2)), 18); + let rs = env.read_register(&rs); + let rt = env.read_register(&rt); + let equals = { + // FIXME: Requires constraints + let pos = env.alloc_scratch(); + unsafe { env.equals_zero(&(rs - rt), pos) } + }; + let offset = (Env::constant(1) - equals.clone()) * Env::constant(4) + equals * offset; + let addr = { + let pos = env.alloc_scratch(); + env.copy(&(next_instruction_pointer.clone() + offset), pos) + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); + // REMOVEME: when all itype instructions are implemented. + return; + } ITypeInstruction::BranchNeq => (), ITypeInstruction::BranchLeqZero => (), ITypeInstruction::BranchGtZero => (), From 96b2cfae65e2ebd7470abc7dd109049cd5d266d4 Mon Sep 17 00:00:00 2001 From: mrmr1993 Date: Tue, 5 Dec 2023 22:08:05 +0000 Subject: [PATCH 4/4] Rename `equals_zero` to `test_zero` --- optimism/src/mips/interpreter.rs | 8 ++------ optimism/src/mips/witness.rs | 6 +----- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 3f0941f06a..302730b529 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -532,11 +532,7 @@ pub trait InterpreterEnv { /// /// There are no constraints on the returned value; callers must assert the relationship with /// `x`. - unsafe fn equals_zero( - &mut self, - x: &Self::Variable, - position: Self::Position, - ) -> Self::Variable; + unsafe fn test_zero(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable; fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable; @@ -763,7 +759,7 @@ pub fn interpret_itype(env: &mut Env, instr: ITypeInstructi let equals = { // FIXME: Requires constraints let pos = env.alloc_scratch(); - unsafe { env.equals_zero(&(rs - rt), pos) } + unsafe { env.test_zero(&(rs - rt), pos) } }; let offset = (Env::constant(1) - equals.clone()) * Env::constant(4) + equals * offset; let addr = { diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs index 32f1c3964a..77bfc347d3 100644 --- a/optimism/src/mips/witness.rs +++ b/optimism/src/mips/witness.rs @@ -227,11 +227,7 @@ impl InterpreterEnv for Env { res } - unsafe fn equals_zero( - &mut self, - x: &Self::Variable, - position: Self::Position, - ) -> Self::Variable { + 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()); res