Add 2 more Expr simplifications related to negative numbers

Author: msooseth

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   controlled via `merge-max-budget`
 
 ## Changed
+- Simplifier now rewrites `Mul(-1, x)` and `~x + 1` to `Sub(0, x)` (canonical negation form)
 - `AbiFunction` and `AbiBytes` parser is now more strict
 - We now check length of AbiArrayDynamic and don't crash in case it's too large
 - SMT queries now run in separate processes, which allows us to better manage

src/EVM/Expr.hs

@@ -1212,6 +1212,10 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | b == c = a
       | otherwise = sub (add a b) c
 
+    -- Negation: ~x + 1 = 0 - x (two's complement)
+    go (Add (Lit 1) (Not b)) = Sub (Lit 0) b
+    go (Add (Lit 1) (Xor (Lit a) b)) | a == maxLit = Sub (Lit 0) b
+
     -- add / sub identities
     go (Add a b)
       | b == (Lit 0) = a
@@ -1271,6 +1275,8 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
     go (Mul a b) = case (a, b) of
                      (Lit 0, _) -> Lit 0
                      (Lit 1, _) -> b
+                     -- Mul by -1 (all 1s) is negation
+                     (Lit v, _) | v == maxLit -> Sub (Lit 0) b
                      _ -> mul a b
 
     -- Some trivial (s)div eliminations

test/EVM/Expr/ExprTests.hs

@@ -279,6 +279,15 @@ basicSimplificationTests = testGroup "Basic simplification tests"
         a = successPath [PEq (Add (Lit 1) (Lit 2)) (Sub (Lit 4) (Lit 1))]
         b = Expr.simplify a
       assertEqual "Must simplify down" (successPath []) b
+  , testCase "simp-mul-neg1" $ do
+      let simp = Expr.simplify $ Mul (Lit Expr.maxLit) (Var "x")
+      assertEqual "mul by -1 is negation" simp (Sub (Lit 0) (Var "x"))
+  , testCase "simp-not-plus1" $ do
+      let simp = Expr.simplify $ Add (Lit 1) (Not (Var "x"))
+      assertEqual "~x + 1 is negation" simp (Sub (Lit 0) (Var "x"))
+  , testCase "simp-xor-maxlit-plus1" $ do
+      let simp = Expr.simplify $ Add (Lit 1) (Xor (Lit Expr.maxLit) (Var "x"))
+      assertEqual "xor(maxLit, x) + 1 is negation" simp (Sub (Lit 0) (Var "x"))
   ]
 
 propSimplificationTests :: TestTree