From 54edc550095010a9eeda7132e78acaeaeb413022 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Mon, 25 Nov 2024 11:10:35 +0100
Subject: [PATCH 1/2] o1vm/riscv32im: improve documentation reg. semantic of op

---
 o1vm/src/interpreters/riscv32im/interpreter.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs
index b657699967..f13e3aa68e 100644
--- a/o1vm/src/interpreters/riscv32im/interpreter.rs
+++ b/o1vm/src/interpreters/riscv32im/interpreter.rs
@@ -20,6 +20,14 @@
 //! and copied in this file for offline reference.
 //! If you are the author of the above documentations and would like to add or
 //! modify the credits, please open a pull request.
+//!
+//! For each instruction, we provide the format, description, and the
+//! semantic in pseudo-code of the instruction.
+//! When `signed` is mentioned in the pseudo-code, it means that the
+//! operation is performed as a signed operation (i.e. signed(v) where `v` is a
+//! 32 bits value means that `v` must be interpreted as a i32 value in Rust, the
+//! most significant bit being the sign - 1 for negative, 0 for positive).
+//! By default, unsigned operations are performed.
 
 use super::registers::{REGISTER_CURRENT_IP, REGISTER_HEAP_POINTER, REGISTER_NEXT_IP};
 use crate::lookups::{Lookup, LookupTableIDs};

From 964cfeb7ad91aa21475cd0c8784b94800ac7b952 Mon Sep 17 00:00:00 2001
From: Danny Willems <be.danny.willems@gmail.com>
Date: Mon, 25 Nov 2024 11:11:00 +0100
Subject: [PATCH 2/2] o1vm/riscv32im: add semantic for MInstruction

---
 o1vm/src/interpreters/riscv32im/interpreter.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs
index f13e3aa68e..0bc94d1c7e 100644
--- a/o1vm/src/interpreters/riscv32im/interpreter.rs
+++ b/o1vm/src/interpreters/riscv32im/interpreter.rs
@@ -2240,6 +2240,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
 
     match instr {
         MInstruction::Mul => {
+            // x[rd] = x[rs1] * x[rs2]
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2253,6 +2254,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Mulh => {
+            // x[rd] = (signed(x[rs1]) * signed(x[rs2])) >> 32
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2266,6 +2268,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Mulhsu => {
+            // x[rd] = (signed(x[rs1]) * x[rs2]) >> 32
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2279,6 +2282,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Mulhu => {
+            // x[rd] = (x[rs1] * x[rs2]) >> 32
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2292,6 +2296,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Div => {
+            // x[rd] = signed(x[rs1]) / signed(x[rs2])
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2305,6 +2310,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Divu => {
+            // x[rd] = x[rs1] / x[rs2]
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2318,6 +2324,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Rem => {
+            // x[rd] = signed(x[rs1]) % signed(x[rs2])
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain
@@ -2331,6 +2338,7 @@ pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
             env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32));
         }
         MInstruction::Remu => {
+            // x[rd] = x[rs1] % x[rs2]
             let rs1 = env.read_register(&rs1);
             let rs2 = env.read_register(&rs2);
             // FIXME: constrain