small changes

jasmin-lang · Sep 26, 2023 · bc03c42 · bc03c42
1 parent e6cc5d8
commit bc03c42
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -19,6 +19,8 @@
      `hi = #MULX_hi(x, y);` is equivalent to `hi, _ = #MULX(x, y);`
   but no extra register is used for the low half of the result.
 
+- For arm-m4: `x = (y << n) - z` is transformed into x = #RSB(z, y<< n).
+
 ## Bug fixes
 
 - Type-checking rejects wrongly casted primitive operators

diff --git a/proofs/compiler/arm_lowering.v b/proofs/compiler/arm_lowering.v
@@ -239,7 +239,7 @@ Definition lower_Papp2_op
       Some (ADD, e0, [:: e1 ])
   | Omul (Op_w _) =>
       Some (MUL, e0, [:: e1 ])
-  | Osub (Op_w ws) =>
+  | Osub (Op_w _) =>
       if is_mul e1 is Some (x, y)
       then Some (MLS, x, [:: y; e0 ])
       else