Merge pull request #1343 from o1-labs/feature/mips-interpreter-skeleton

Skeleton of the VM interpreter
o1-labs · Nov 30, 2023 · 5db877a · 5db877a
2 parents 8c5977d + 26e9f9b
commit 5db877a
Show file tree

Hide file tree

Showing 2 changed files with 128 additions and 4 deletions.
diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs
@@ -93,3 +93,107 @@ pub enum ITypeInstruction {
     StoreWordLeft,                // swl
     StoreWordRight,               // swr
 }
+
+pub trait InterpreterEnv {
+    type Variable: Clone + std::ops::Add<Self::Variable, Output = Self::Variable>;
+
+    fn constant(x: u32) -> Self::Variable;
+
+    fn set_halted(&mut self, flag: Self::Variable);
+}
+
+pub fn interpret_instruction<Env: InterpreterEnv>(env: &mut Env, instr: Instruction) {
+    match instr {
+        Instruction::RType(instr) => interpret_rtype(env, instr),
+        Instruction::JType(instr) => interpret_jtype(env, instr),
+        Instruction::IType(instr) => interpret_itype(env, instr),
+    }
+}
+
+pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RTypeInstruction) {
+    match instr {
+        RTypeInstruction::ShiftLeftLogical => (),
+        RTypeInstruction::ShiftRightLogical => (),
+        RTypeInstruction::ShiftRightArithmetic => (),
+        RTypeInstruction::ShiftLeftLogicalVariable => (),
+        RTypeInstruction::ShiftRightLogicalVariable => (),
+        RTypeInstruction::ShiftRightArithmeticVariable => (),
+        RTypeInstruction::JumpRegister => (),
+        RTypeInstruction::JumpAndLinkRegister => (),
+        RTypeInstruction::SyscallMmap => (),
+        RTypeInstruction::SyscallExitGroup => (),
+        RTypeInstruction::SyscallReadPreimage => (),
+        RTypeInstruction::SyscallReadOther => (),
+        RTypeInstruction::SyscallWriteHint => (),
+        RTypeInstruction::SyscallWritePreimage => (),
+        RTypeInstruction::SyscallWriteOther => (),
+        RTypeInstruction::SyscallFcntl => (),
+        RTypeInstruction::SyscallOther => (),
+        RTypeInstruction::MoveZero => (),
+        RTypeInstruction::MoveNonZero => (),
+        RTypeInstruction::Sync => (),
+        RTypeInstruction::MoveFromHi => (),
+        RTypeInstruction::MoveToHi => (),
+        RTypeInstruction::MoveFromLo => (),
+        RTypeInstruction::MoveToLo => (),
+        RTypeInstruction::Multiply => (),
+        RTypeInstruction::MultiplyUnsigned => (),
+        RTypeInstruction::Div => (),
+        RTypeInstruction::DivUnsigned => (),
+        RTypeInstruction::Add => (),
+        RTypeInstruction::AddUnsigned => (),
+        RTypeInstruction::Sub => (),
+        RTypeInstruction::SubUnsigned => (),
+        RTypeInstruction::And => (),
+        RTypeInstruction::Or => (),
+        RTypeInstruction::Xor => (),
+        RTypeInstruction::Nor => (),
+        RTypeInstruction::SetLessThan => (),
+        RTypeInstruction::SetLessThanUnsigned => (),
+        RTypeInstruction::MultiplyToRegister => (),
+        RTypeInstruction::CountLeadingOnes => (),
+        RTypeInstruction::CountLeadingZeros => (),
+    };
+    // TODO: Don't halt.
+    env.set_halted(Env::constant(1));
+}
+
+pub fn interpret_jtype<Env: InterpreterEnv>(env: &mut Env, instr: JTypeInstruction) {
+    match instr {
+        JTypeInstruction::Jump => (),
+        JTypeInstruction::JumpAndLink => (),
+    };
+    // TODO: Don't halt.
+    env.set_halted(Env::constant(1));
+}
+
+pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstruction) {
+    match instr {
+        ITypeInstruction::BranchEq => (),
+        ITypeInstruction::BranchNeq => (),
+        ITypeInstruction::BranchLeqZero => (),
+        ITypeInstruction::BranchGtZero => (),
+        ITypeInstruction::AddImmediate => (),
+        ITypeInstruction::AddImmediateUnsigned => (),
+        ITypeInstruction::SetLessThanImmediate => (),
+        ITypeInstruction::SetLessThanImmediateUnsigned => (),
+        ITypeInstruction::AndImmediate => (),
+        ITypeInstruction::OrImmediate => (),
+        ITypeInstruction::XorImmediate => (),
+        ITypeInstruction::LoadUpperImmediate => (),
+        ITypeInstruction::Load8 => (),
+        ITypeInstruction::Load16 => (),
+        ITypeInstruction::Load32 => (),
+        ITypeInstruction::Load8Unsigned => (),
+        ITypeInstruction::Load16Unsigned => (),
+        ITypeInstruction::LoadWordLeft => (),
+        ITypeInstruction::LoadWordRight => (),
+        ITypeInstruction::Store8 => (),
+        ITypeInstruction::Store16 => (),
+        ITypeInstruction::Store32 => (),
+        ITypeInstruction::StoreWordLeft => (),
+        ITypeInstruction::StoreWordRight => (),
+    };
+    // TODO: Don't halt.
+    env.set_halted(Env::constant(1));
+}
diff --git a/optimism/src/mips/witness.rs b/optimism/src/mips/witness.rs
@@ -4,7 +4,9 @@ use crate::{
         PAGE_SIZE,
     },
     mips::{
-        interpreter::{self, ITypeInstruction, Instruction, JTypeInstruction, RTypeInstruction},
+        interpreter::{
+            self, ITypeInstruction, Instruction, InterpreterEnv, JTypeInstruction, RTypeInstruction,
+        },
         registers::Registers,
     },
     preimage_oracle::PreImageOracle,
@@ -93,6 +95,24 @@ fn memory_size(total: usize) -> String {
     }
 }
 
+impl<Fp: Field> InterpreterEnv for Env<Fp> {
+    type Variable = u32;
+
+    fn constant(x: u32) -> Self::Variable {
+        x
+    }
+
+    fn set_halted(&mut self, flag: Self::Variable) {
+        if flag == 0 {
+            self.halt = false
+        } else if flag == 1 {
+            self.halt = true
+        } else {
+            panic!("Bad value for flag in set_halted: {}", flag);
+        }
+    }
+}
+
 impl<Fp: Field> Env<Fp> {
     pub fn create(page_size: usize, state: State, preimage_oracle: PreImageOracle) -> Self {
         let initial_instruction_pointer = state.pc;
@@ -270,7 +290,8 @@ impl<Fp: Field> Env<Fp> {
     }
 
     pub fn step(&mut self, config: VmConfiguration, metadata: &Meta, start: &Start) {
-        println!("instruction: {:?}", self.decode_instruction());
+        let instruction = self.decode_instruction();
+        println!("instruction: {:?}", instruction);
 
         self.pp_info(config.info_at, metadata, start);
 
@@ -280,8 +301,7 @@ impl<Fp: Field> Env<Fp> {
             return;
         }
 
-        // TODO
-        self.halt = true;
+        interpreter::interpret_instruction(self, instruction);
     }
 
     fn should_trigger_at(&self, at: StepFrequency) -> bool {