Unit test for StoreWordRight

o1vm/src/mips/interpreter.rs

@@ -2464,18 +2464,25 @@ 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
             // behavior defined in the spec.
             // See e.g. 'MIPS IV Instruction Set' Rev 3.2, Table A-31 for reference.
-            let m0 = env.read_memory(&(addr.clone() - Env::constant(3)));
+            //
+            // "EffAddr is the address of the least-significant of four consecutive bytes
+            // forming a word in memory"
+            //
+            // Because we shift the bytes in memory to the right, we need to access smaller
+            // addresses of memory.
+            // Big-endian notation here
             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);
+            // No need to compute m0 as mem(addr-3) because it is not used here
 
             let [r0, r1, r2, r3] = {
                 let initial_register_value = env.read_register(&rt);
@@ -2503,31 +2510,47 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                 ]
             };
 
+            // if mod = 0 -> r3 m1 m2 m3
+            // if mod = 1 -> r2 r3 m2 m3
+            // if mod = 2 -> r1 r2 r3 m3
+            // if mod = 3 -> r0 r1 r2 r3
             let v0 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_0.clone() * r0 + (Env::constant(1) - overwrite_0) * m0),
+                    &(r3.clone() * mod_0.clone()
+                        + r2.clone() * mod_1.clone()
+                        + r1.clone() * mod_2.clone()
+                        + r0 * mod_3.clone()),
                     pos,
                 )
             };
             let v1 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_1.clone() * r1 + (Env::constant(1) - overwrite_1) * m1),
+                    &(m1 * mod_0.clone()
+                        + r3.clone() * mod_1.clone()
+                        + r2.clone() * mod_2.clone()
+                        + r1 * mod_3.clone()),
                     pos,
                 )
             };
+            // if mod = 0 -> r3 m1 m2 m3
+            // if mod = 1 -> r2 r3 m2 m3
+            // if mod = 2 -> r1 r2 r3 m3
+            // if mod = 3 -> r0 r1 r2 r3
             let v2 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_2.clone() * r2 + (Env::constant(1) - overwrite_2) * m2),
+                    &(m2 * (mod_0.clone() + mod_1.clone())
+                        + r3.clone() * mod_2.clone()
+                        + r2 * mod_3.clone()),
                     pos,
                 )
             };
             let v3 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_3.clone() * r3 + (Env::constant(1) - overwrite_3) * m3),
+                    &(m3 * (mod_0.clone() + mod_1.clone() + mod_2.clone()) + r3 * mod_3),
                     pos,
                 )
             };

o1vm/src/mips/tests.rs

@@ -454,6 +454,81 @@ mod unit {
             interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
             assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
         }
+
+        #[test]
+        fn test_unit_swr_instruction() {
+            // swr instruction
+            // case 0x2e: swr
+            //            val := rt << (24 - (rs&3)*8)
+            //            mask := uint32(0xFFFFFFFF) << (24 - (rs&3)*8)
+            //            return (mem & ^mask) | val
+
+            // Instruction: 0b101110 10101 00001 0000000001000000
+            // swl 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(1000u32..4000u32);
+            let base = dummy_env.registers[rs];
+            // The effective address
+            let (addr, ovf) = base.overflowing_add(offset);
+            assert!(!ovf);
+
+            let shift_right = 24 - (addr & 3) * 8;
+
+            // This is the partial value that will be stored into memory
+            let val = dummy_env.registers[dst] << shift_right;
+
+            let mask = 0xFFFFFFFFu32 << shift_right;
+
+            // Initial value of the memory
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+            let m0 = mem[(addr - 3) as usize];
+            let m1 = mem[(addr - 2) as usize];
+            let m2 = mem[(addr - 1) as usize];
+            let m3 = mem[addr 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 exp_v = (memory & !mask) | val;
+
+            write_instruction(
+                &mut dummy_env,
+                InstructionParts {
+                    op_code: 0b101110,
+                    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::StoreWordRight);
+
+            // Check the memory after the instruction
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+            let m0 = mem[(addr - 3) as usize];
+            let m1 = mem[(addr - 2) as usize];
+            let m2 = mem[(addr - 1) as usize];
+            let m3 = mem[addr as usize];
+
+            assert_eq!(m0, bitmask(exp_v, 32, 24) as u8);
+            assert_eq!(m1, bitmask(exp_v, 24, 16) as u8);
+            assert_eq!(m2, bitmask(exp_v, 16, 8) as u8);
+            assert_eq!(m3, bitmask(exp_v, 8, 0) as u8);
+        }
     }
 }
 

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