MIPS/Store32: add missing constraint checking the decomposition

o1-labs · Apr 23, 2024 · bb0d63f · bb0d63f
1 parent 8f374c6
commit bb0d63f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 3 deletions.
diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs
@@ -2278,6 +2278,15 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
                     },
                 ]
             };
+            // Checking that v is the correct decomposition.
+            {
+                let res = value
+                    - v0.clone() * Env::constant(1 << 24)
+                    - v1.clone() * Env::constant(1 << 16)
+                    - v2.clone() * Env::constant(1 << 8)
+                    - v3.clone();
+                env.is_zero(&res)
+            };
             env.write_memory(&addr, v0);
             env.write_memory(&(addr.clone() + Env::constant(1)), v1);
             env.write_memory(&(addr.clone() + Env::constant(2)), v2);

diff --git a/optimism/src/mips/tests.rs b/optimism/src/mips/tests.rs
@@ -78,9 +78,10 @@ fn test_mips_number_constraints() {
                 JumpAndLink => assert_num_constraints(&instr, 3),
             },
             IType(itype) => match itype {
-                BranchLeqZero | BranchGtZero | BranchLtZero | BranchGeqZero | Store8 | Store16
-                | Store32 => assert_num_constraints(&instr, 0),
-                BranchEq | BranchNeq => assert_num_constraints(&instr, 2),
+                BranchLeqZero | BranchGtZero | BranchLtZero | BranchGeqZero | Store8 | Store16 => {
+                    assert_num_constraints(&instr, 0)
+                }
+                BranchEq | BranchNeq | Store32 => assert_num_constraints(&instr, 2),
                 AddImmediate
                 | AddImmediateUnsigned
                 | SetLessThanImmediate