Unit test for LoadWordRight

o1vm/src/mips/interpreter.rs

@@ -2153,20 +2153,29 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                 unsafe { env.bitmask(&addr, 2, 0, pos) }
             };
 
-            let overwrite_0 = env.equal(&byte_subaddr, &Env::constant(3));
-            let overwrite_1 = env.equal(&byte_subaddr, &Env::constant(2)) + overwrite_0.clone();
-            let overwrite_2 = env.equal(&byte_subaddr, &Env::constant(1)) + overwrite_1.clone();
-            let overwrite_3 = env.equal(&byte_subaddr, &Env::constant(0)) + overwrite_2.clone();
+            let mod_0 = env.equal(&byte_subaddr, &Env::constant(0));
+            let mod_1 = env.equal(&byte_subaddr, &Env::constant(1));
+            let mod_2 = env.equal(&byte_subaddr, &Env::constant(2));
+            let mod_3 = env.equal(&byte_subaddr, &Env::constant(3));
 
-            // The `-3` here feels odd, but simulates the `<< 24` in cannon, and matches the
+            // The `-3` here feels odd, but simulates the `>> 24` in cannon, and matches the
             // behavior defined in the spec.
+            //
             // See e.g. 'MIPS IV Instruction Set' Rev 3.2, Table A-31 for reference.
+            // Because we shift the bytes in memory to the right, we need to access smaller
+            // addresses of memory.
+            //
+            // From docs: "EffAddr is the address of the least-significant of
+            //             four consecutive bytes word in memory"
+            //
+            // Big-endian notation here
             let m0 = env.read_memory(&(addr.clone() - Env::constant(3)));
             let m1 = env.read_memory(&(addr.clone() - Env::constant(2)));
             let m2 = env.read_memory(&(addr.clone() - Env::constant(1)));
             let m3 = env.read_memory(&addr);
 
-            let [r0, r1, r2, r3] = {
+            // No need to compute r3 as bitmask(reg,8,0,pos) as it is not used
+            let [r0, r1, r2] = {
                 let initial_register_value = env.read_register(&rt);
                 [
                     {
@@ -2184,22 +2193,27 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                         let pos = env.alloc_scratch();
                         unsafe { env.bitmask(&initial_register_value, 16, 8, pos) }
                     },
-                    {
-                        // FIXME: Requires a range check
-                        let pos = env.alloc_scratch();
-                        unsafe { env.bitmask(&initial_register_value, 8, 0, pos) }
-                    },
                 ]
             };
 
+            // if mod = 0 -> r0 r1 r2 m0
+            // if mod = 1 -> r0 r1 m0 m1
+            // if mod = 2 -> r0 m0 m1 m2
+            // if mod = 3 -> m0 m1 m2 m3
             let value = {
-                let value = ((overwrite_0.clone() * m0 + (Env::constant(1) - overwrite_0) * r0)
-                    * Env::constant(1 << 24))
-                    + ((overwrite_1.clone() * m1 + (Env::constant(1) - overwrite_1) * r1)
-                        * Env::constant(1 << 16))
-                    + ((overwrite_2.clone() * m2 + (Env::constant(1) - overwrite_2) * r2)
-                        * Env::constant(1 << 8))
-                    + (overwrite_3.clone() * m3 + (Env::constant(1) - overwrite_3) * r3);
+                let value = Env::constant(1 << 24)
+                    * (r0 * (mod_0.clone() + mod_1.clone() + mod_2.clone())
+                        + m0.clone() * mod_3.clone())
+                    + Env::constant(1 << 16)
+                        * (r1 * (mod_0.clone() + mod_1.clone())
+                            + m0.clone() * mod_2.clone()
+                            + m1.clone() * mod_3.clone())
+                    + Env::constant(1 << 8)
+                        * (r2 * mod_0.clone()
+                            + m0.clone() * mod_1.clone()
+                            + m1.clone() * mod_2.clone()
+                            + m2.clone() * mod_3.clone())
+                    + (m0 * mod_0 + m1 * mod_1 + m2 * mod_2 + m3 * mod_3);
                 let pos = env.alloc_scratch();
                 env.copy(&value, pos)
             };

o1vm/src/mips/tests.rs

@@ -155,8 +155,8 @@ mod unit {
     {
         let dummy_preimage_oracle = OnDiskPreImageOracle;
         let mut env = WEnv {
-            // Set it to 2 to run 1 instruction that access registers if
-            instruction_counter: 2,
+            // Set it to an arbitrary "large" number
+            instruction_counter: 10,
             // Only 8kb of memory (two PAGE_ADDRESS_SIZE)
             memory: vec![
                 // Read/write memory
@@ -454,6 +454,67 @@ mod unit {
             interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
             assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
         }
+
+        #[test]
+        fn test_unit_lwr_instruction() {
+            // lwr instruction
+            // val := mem >> (24 - (rs&3)*8)
+            // mask := uint32(0xFFFFFFFF) >> (24 - (rs&3)*8)
+            // return (rt & ^mask) | val
+
+            // Instruction: 0b100110 10101 00001 0000000001000000
+            // lwr rt offset(21)
+
+            let mut rng = o1_utils::tests::make_test_rng(None);
+            let mut dummy_env = dummy_env(&mut rng);
+
+            // Values used in the instruction
+            let rs = 21;
+            let dst = 1;
+            let offset = sign_extend(64, 16);
+
+            // Set the base address to a small number so dummy_env does not ovf
+            dummy_env.registers[rs] = rng.gen_range(4u32..4000u32);
+            let base = dummy_env.registers[rs];
+            // The effective address
+            let (addr, ovf) = base.overflowing_add(offset);
+            assert!(!ovf);
+
+            let shift_right = 24 - (dummy_env.registers[rs] & 3) * 8;
+            let mask = 0xFFFFFFFF >> shift_right;
+
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+
+            // Here starts the least significant byte of the word we will load
+            let m3 = mem[addr as usize];
+            let m2 = mem[(addr - 1) as usize];
+            let m1 = mem[(addr - 2) as usize];
+            let m0 = mem[(addr - 3) as usize];
+
+            // Big endian: small addresses of memory represent more significant
+            let memory =
+                ((m0 as u32) << 24) + ((m1 as u32) << 16) + ((m2 as u32) << 8) + (m3 as u32);
+
+            let val = memory >> shift_right;
+
+            let exp_v = (dummy_env.registers[dst] & !mask) | val;
+
+            write_instruction(
+                &mut dummy_env,
+                InstructionParts {
+                    op_code: 0b100010,
+                    rs: rs as u32,  // where base address is obtained from
+                    rt: dst as u32, // destination
+                    rd: 0b00000,
+                    shamt: 0b00001, // offset = 64
+                    funct: 0b000000,
+                },
+            );
+            interpret_itype(&mut dummy_env, ITypeInstruction::LoadWordRight);
+
+            assert_eq!(dummy_env.registers[dst], exp_v);
+        }
     }
 }
 

o1vm/src/mips/witness.rs

@@ -616,7 +616,8 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI
     fn report_exit(&mut self, exit_code: &Self::Variable) {
         println!(
             "Exited with code {} at step {}",
-            *exit_code, self.instruction_counter
+            *exit_code,
+            self.instruction_counter_normalized()
         );
     }
 
@@ -1064,6 +1065,18 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
         (opcode, instruction)
     }
 
+    /// Because MAX_NB_REG_ACC = 7 and MAX_NB_MEM_ACC = 12, at most the same
+    /// instruction will increase the instruction counter by MAX_ACC = 19.
+    ///
+    /// NOTE: actually, in practice it will be less than that, as there is no
+    ///       single instruction that performs all of them.
+    ///
+    /// This means that the actual number of instructions executed will result
+    /// from dividing the instruction counter by MAX_ACC (floor).
+    pub fn instruction_counter_normalized(&self) -> u64 {
+        self.instruction_counter / MAX_ACC
+    }
+
     /// Updates the instruction counter, accounting for the maximum number of
     /// register and memory accesses per instruction.
     /// Because MAX_NB_REG_ACC = 7 and MAX_NB_MEM_ACC = 12, at most the same
@@ -1079,7 +1092,7 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
     /// the real instruction counter and multiply it by MAX_ACC to have a unique
     /// representation of each step (which is helpful for debugging).
     pub fn update_instruction_counter(&mut self) {
-        self.instruction_counter = ((self.instruction_counter / MAX_ACC) + 1) * MAX_ACC;
+        self.instruction_counter = (self.instruction_counter_normalized() + 1) * MAX_ACC;
     }
 
     /// Execute a single step of the MIPS program.
@@ -1101,7 +1114,8 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
             self.halt = true;
             println!(
                 "Halted as requested at step={} instruction={:?}",
-                self.instruction_counter, opcode
+                self.instruction_counter_normalized(),
+                opcode
             );
             return opcode;
         }
@@ -1114,15 +1128,15 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
         if self.halt {
             println!(
                 "Halted at step={} instruction={:?}",
-                self.instruction_counter / MAX_ACC,
+                self.instruction_counter_normalized(),
                 opcode
             );
         }
         opcode
     }
 
     fn should_trigger_at(&self, at: &StepFrequency) -> bool {
-        let m: u64 = self.instruction_counter;
+        let m: u64 = self.instruction_counter_normalized();
         match at {
             StepFrequency::Never => false,
             StepFrequency::Always => true,
@@ -1198,7 +1212,8 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
             let _ = serde_json::to_writer(&mut writer, &s);
             info!(
                 "Snapshot state in {}, step {}",
-                filename, self.instruction_counter
+                filename,
+                self.instruction_counter_normalized()
             );
             writer.flush().expect("Flush writer failing")
         }
@@ -1208,7 +1223,7 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> {
         if self.should_trigger_at(at) {
             let elapsed = start.time.elapsed();
             // Compute the step number removing the MAX_ACC factor
-            let step = self.instruction_counter / MAX_ACC;
+            let step = self.instruction_counter_normalized();
             let pc = self.registers.current_instruction_pointer;
 
             // Get the 32-bits opcode