Unit test for StoreWordLeft

o1vm/src/mips/interpreter.rs

@@ -2374,15 +2374,17 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                 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();
+            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));
 
+            // From docs: "EffAddr is the address of the most-significant of
+            // four consecutive bytes forming a word in memory"
             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)));
+            // No need to define m3 as mem(addr+3) because it is never used in swl
 
             let [r0, r1, r2, r3] = {
                 let initial_register_value = env.read_register(&rt);
@@ -2410,35 +2412,43 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                 ]
             };
 
+            // if mod = 0 -> r0 r1 r2 r3
+            // if mod = 1 -> m0 r0 r1 r2
+            // if mod = 2 -> m0 m1 r0 r1
+            // if mod = 3 -> m0 m1 m2 r0
             let v0 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_0.clone() * r0 + (Env::constant(1) - overwrite_0) * m0),
+                    &(r0.clone() * mod_0.clone()
+                        + m0 * (mod_1.clone() + mod_2.clone() + mod_3.clone())),
                     pos,
                 )
             };
             let v1 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_1.clone() * r1 + (Env::constant(1) - overwrite_1) * m1),
+                    &(r1.clone() * mod_0.clone()
+                        + r0.clone() * mod_1.clone()
+                        + m1 * (mod_2.clone() + mod_3.clone())),
                     pos,
                 )
             };
             let v2 = {
                 let pos = env.alloc_scratch();
                 env.copy(
-                    &(overwrite_2.clone() * r2 + (Env::constant(1) - overwrite_2) * m2),
+                    &(r2.clone() * mod_0.clone()
+                        + r1.clone() * mod_1.clone()
+                        + r0.clone() * mod_2.clone()
+                        + m2 * mod_3.clone()),
                     pos,
                 )
             };
             let v3 = {
                 let pos = env.alloc_scratch();
-                env.copy(
-                    &(overwrite_3.clone() * r3 + (Env::constant(1) - overwrite_3) * m3),
-                    pos,
-                )
+                env.copy(&(r3 * mod_0 + r2 * mod_1 + r1 * mod_2 + r0 * mod_3), pos)
             };
 
+            // Big-endian: most significant bytes into smaller addresses
             env.write_memory(&addr, v0);
             env.write_memory(&(addr.clone() + Env::constant(1)), v1);
             env.write_memory(&(addr.clone() + Env::constant(2)), v2);

o1vm/src/mips/tests.rs

@@ -454,6 +454,82 @@ mod unit {
             interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
             assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
         }
+
+        #[test]
+        fn test_unit_swl_instruction() {
+            // swl instruction
+            // case 0x2a: swl
+            //            val := rt >> ((rs & 3) * 8)
+            //            mask := uint32(0xFFFFFFFF) >> ((rs & 3) * 8)
+            //            return (mem & ^mask) | val
+
+            // Instruction: 0b101010 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);
+
+            // Number of bytes that will be kept on the right of memory
+            let shift_left = (addr & 3) * 8;
+
+            // This is the partial value that will be stored into memory
+            let val = dummy_env.registers[dst] >> shift_left;
+
+            let mask = 0xFFFFFFFFu32 >> shift_left;
+
+            // Initial value of the memory
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+            let v0 = mem[addr as usize];
+            let v1 = mem[(addr + 1) as usize];
+            let v2 = mem[(addr + 2) as usize];
+            let v3 = mem[(addr + 3) as usize];
+
+            // Big endian: small addresses of memory represent more significant
+            let memory =
+                ((v0 as u32) << 24) + ((v1 as u32) << 16) + ((v2 as u32) << 8) + (v3 as u32);
+
+            let exp_v = (memory & !mask) | val;
+
+            write_instruction(
+                &mut dummy_env,
+                InstructionParts {
+                    op_code: 0b101010,
+                    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::StoreWordLeft);
+
+            // Check the memory after the instruction
+            let mem = &dummy_env.memory[0];
+            let mem = &mem.1;
+            let v0 = mem[addr as usize];
+            let v1 = mem[(addr + 1) as usize];
+            let v2 = mem[(addr + 2) as usize];
+            let v3 = mem[(addr + 3) as usize];
+
+            assert_eq!(v0, bitmask(exp_v, 32, 24) as u8);
+            assert_eq!(v1, bitmask(exp_v, 24, 16) as u8);
+            assert_eq!(v2, bitmask(exp_v, 16, 8) as u8);
+            assert_eq!(v3, 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