Unit test for LoadWordLeft

o1vm/src/mips/interpreter.rs

@@ -2079,30 +2079,25 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                 res
             };
 
+            // Corresponds to `(rs & 3)`
             let byte_subaddr = {
                 // FIXME: Requires a range check
                 let pos = env.alloc_scratch();
                 unsafe { env.bitmask(&addr, 2, 0, pos) }
             };
 
-            let overwrite_3 = env.equal(&byte_subaddr, &Env::constant(0));
-            let overwrite_2 = env.equal(&byte_subaddr, &Env::constant(1)) + overwrite_3.clone();
-            let overwrite_1 = env.equal(&byte_subaddr, &Env::constant(2)) + overwrite_2.clone();
-            let overwrite_0 = env.equal(&byte_subaddr, &Env::constant(3)) + overwrite_1.clone();
-
+            // From docs: "EffAddr is the address of the most-significant of
+            //             four consecutive bytes word in memory"
+            // Big-endian: smallest address is the most significant byte
             let m0 = env.read_memory(&addr);
             let m1 = env.read_memory(&(addr.clone() + Env::constant(1)));
             let m2 = env.read_memory(&(addr.clone() + Env::constant(2)));
             let m3 = env.read_memory(&(addr.clone() + Env::constant(3)));
 
-            let [r0, r1, r2, r3] = {
+            // No need to define r0 as bitmask(reg, 32,24,pos) since it is not used
+            let [r1, r2, r3] = {
                 let initial_register_value = env.read_register(&rt);
                 [
-                    {
-                        // FIXME: Requires a range check
-                        let pos = env.alloc_scratch();
-                        unsafe { env.bitmask(&initial_register_value, 32, 24, pos) }
-                    },
                     {
                         // FIXME: Requires a range check
                         let pos = env.alloc_scratch();
@@ -2120,14 +2115,33 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                     },
                 ]
             };
+
+            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));
+
+            // if mod = 0 -> m0 m1 m2 m3
+            // if mod = 1 -> m1 m2 m3 r3
+            // if mod = 2 -> m2 m3 r2 r3
+            // if mod = 3 -> m3 r1 r2 r3
             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)
+                    * (m0 * mod_0.clone()
+                        + m1.clone() * mod_1.clone()
+                        + m2.clone() * mod_2.clone()
+                        + m3.clone() * mod_3.clone())
+                    + Env::constant(1 << 16)
+                        * (m1 * mod_0.clone()
+                            + m2.clone() * mod_1.clone()
+                            + m3.clone() * mod_2.clone()
+                            + r1.clone() * mod_3.clone())
+                    + Env::constant(1 << 8)
+                        * (m2 * mod_0.clone()
+                            + m3.clone() * mod_1.clone()
+                            + r2 * (mod_2.clone() + mod_3.clone()))
+                    + (m3 * mod_0 + r3 * (mod_1 + mod_2 + mod_3));
+
                 let pos = env.alloc_scratch();
                 env.copy(&value, pos)
             };

o1vm/src/mips/tests.rs

@@ -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_lwl_instruction() {
+            // lwl instruction
+            // val := mem << ((rs & 3) * 8)
+            // mask := uint32(0xFFFFFFFF) << ((rs & 3) * 8)
+            // return (rt & ^mask) | val
+
+            // Instruction: 0b100010 10101 00001 0000000001000000
+            // lwl 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(0u32..4000u32);
+            let base = dummy_env.registers[rs];
+            // The effective address
+            let (addr, ovf) = base.overflowing_add(offset);
+            assert!(!ovf);
+
+            let shift_left = (addr & 3) * 8;
+            let mask = 0xFFFFFFFFu32 << shift_left;
+
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+
+            // Here start the (at most 4) bytes we want to load from memory
+            let m0 = mem[addr as usize];
+            let m1 = mem[(addr + 1) as usize];
+            let m2 = mem[(addr + 2) as usize];
+            let m3 = 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_left;
+
+            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::LoadWordLeft);
+
+            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