Do not simplify equality immediately on construction

After some discussion, it turns out it is preferable to keep
simplification code in the simplification functions and do not simplify
equalities directly at construction point.

However, we would still like to normalize equalities, so that constants
are at LHS. Therefore we update the simplification rules, which were
previously written to expect constant on RHS.

src/EVM.hs

@@ -1604,7 +1604,7 @@ cheatActions = Map.fromList
 
   , action "assume(bool)" $
       \sig _ _ input -> case decodeStaticArgs 0 1 input of
-        [c] -> modifying #constraints ((:) (mkPEq (Lit 1) c))
+        [c] -> modifying #constraints ((:) (PEq (Lit 1) c))
         _ -> vmError (BadCheatCode sig)
 
   , action "roll(uint256)" $

src/EVM/Expr.hs

@@ -19,6 +19,7 @@ import Data.List
 import Data.Map.Strict qualified as Map
 import Data.Maybe (mapMaybe, isJust, fromMaybe)
 import Data.Semigroup (Any, Any(..), getAny)
+import Data.Typeable
 import Data.Vector qualified as V
 import Data.Vector (Vector)
 import Data.Vector.Mutable qualified as MV
@@ -200,6 +201,17 @@ sar = op2 SAR (\x y ->
      else
        fromIntegral $ shiftR asSigned (fromIntegral x))
 
+
+-- Props
+
+peq :: (Typeable a) => Expr a -> Expr a -> Prop
+peq (Lit x) (Lit y) = PBool (x == y)
+peq a@(Lit _) b = PEq a b
+peq a b@(Lit _) = PEq b a -- we always put concrete values on LHS
+peq a b
+  | a == b = PBool True
+  | otherwise = PEq a b
+
 -- ** Bufs ** --------------------------------------------------------------------------------------
 
 
@@ -1221,29 +1233,29 @@ simplifyProp prop =
     go (PLEq a (Max _ b)) | a == b = PBool True
     go (PLEq (Sub a b) c) | a == c = PLEq b a
     go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
-    go (PLT (Lit 0) (Eq a b)) = mkPEq a b
+    go (PLT (Lit 0) (Eq a b)) = peq a b
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)
     go (PNeg (PNeg a)) = a
 
     -- solc specific stuff
-    go (PEq (IsZero (IsZero (Eq a b))) (Lit 0)) = PNeg (mkPEq a b)
+    go (PEq (Lit 0) (IsZero (IsZero (Eq a b)))) = PNeg (peq a b)
 
     -- iszero(a) -> (a == 0)
     -- iszero(iszero(a))) -> ~(a == 0) -> a > 0
     -- iszero(iszero(a)) == 0 -> ~~(a == 0) -> a == 0
     -- ~(iszero(iszero(a)) == 0) -> ~~~(a == 0) -> ~(a == 0) -> a > 0
-    go (PNeg (PEq (IsZero (IsZero a)) (Lit 0))) = PLT (Lit 0) a
+    go (PNeg (PEq (Lit 0) (IsZero (IsZero a)))) = PLT (Lit 0) a
 
     -- iszero(a) -> (a == 0)
     -- iszero(a) == 0 -> ~(a == 0)
     -- ~(iszero(a) == 0) -> ~~(a == 0) -> a == 0
-    go (PNeg (PEq (IsZero a) (Lit 0))) = mkPEq (Lit 0) a
+    go (PNeg (PEq (Lit 0) (IsZero a))) = peq (Lit 0) a
 
     -- a < b == 0 -> ~(a < b)
     -- ~(a < b == 0) -> ~~(a < b) -> a < b
-    go (PNeg (PEq (LT a b) (Lit 0x0))) = PLT a b
+    go (PNeg (PEq (Lit 0) (LT a b))) = PLT a b
 
     -- And/Or
     go (PAnd (PBool l) (PBool r)) = PBool (l && r)
@@ -1263,21 +1275,19 @@ simplifyProp prop =
     go (PImpl (PBool False) _) = PBool True
 
     -- Double negation
-    go (PEq (IsZero (Eq a b)) (Lit 0)) = mkPEq a b
-    go (PEq (IsZero (LT a b)) (Lit 0)) = PLT a b
-    go (PEq (IsZero (GT a b)) (Lit 0)) = PGT a b
-    go (PEq (IsZero (LEq a b)) (Lit 0)) = PLEq a b
-    go (PEq (IsZero (GEq a b)) (Lit 0)) = PGEq a b
+    go (PEq (Lit 0) (IsZero (Eq a b))) = peq a b
+    go (PEq (Lit 0) (IsZero (LT a b))) = PLT a b
+    go (PEq (Lit 0) (IsZero (GT a b))) = PGT a b
+    go (PEq (Lit 0) (IsZero (LEq a b))) = PLEq a b
+    go (PEq (Lit 0) (IsZero (GEq a b))) = PGEq a b
 
     -- Eq
-    go (PEq (Eq a b) (Lit 0)) = PNeg (mkPEq a b)
-    go (PEq (Eq a b) (Lit 1)) = mkPEq a b
-    go (PEq (Sub a b) (Lit 0)) = mkPEq a b
-    go (PEq (LT a b) (Lit 0)) = PLEq b a
-    go (PEq (Lit l) (Lit r)) = PBool (l == r)
-    go o@(PEq l r)
-      | l == r = PBool True
-      | otherwise = o
+    go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)
+    go (PEq (Lit 1) (Eq a b)) = peq a b
+    go (PEq (Lit 0) (Sub a b)) = peq a b
+    go (PEq (Lit 0) (LT a b)) = PLEq b a
+    go (PEq l r) = peq l r
+
     go p = p
 
 
@@ -1289,7 +1299,7 @@ simplifyProp prop =
     simpInnerExpr (PGEq a b) = simpInnerExpr (PLEq b a)
     simpInnerExpr (PGT a b) = simpInnerExpr (PLT b a)
     -- simplifies the inner expression
-    simpInnerExpr (PEq a b) = mkPEq (simplify a) (simplify b)
+    simpInnerExpr (PEq a b) = PEq (simplify a) (simplify b)
     simpInnerExpr (PLT a b) = PLT (simplify a) (simplify b)
     simpInnerExpr (PLEq a b) = PLEq (simplify a) (simplify b)
     simpInnerExpr (PNeg a) = PNeg (simpInnerExpr a)

src/EVM/Keccak.hs

@@ -56,12 +56,12 @@ minProp k@(Keccak _) = PGT k (Lit 256)
 minProp _ = internalError "expected keccak expression"
 
 concVal :: Expr EWord -> Prop
-concVal k@(Keccak (ConcreteBuf bs)) = mkPEq (Lit (keccak' bs)) k
+concVal k@(Keccak (ConcreteBuf bs)) = PEq (Lit (keccak' bs)) k
 concVal _ = PBool True
 
 injProp :: (Expr EWord, Expr EWord) -> Prop
 injProp (k1@(Keccak b1), k2@(Keccak b2)) =
-  POr ((b1 .== b2) .&& (bufLength b1 .== bufLength b2)) (PNeg (mkPEq k1 k2))
+  POr ((b1 .== b2) .&& (bufLength b1 .== bufLength b2)) (PNeg (PEq k1 k2))
 injProp _ = internalError "expected keccak expression"
 
 
@@ -94,7 +94,7 @@ compute = \case
   e@(Keccak buf) -> do
     let b = simplify buf
     case keccak b of
-      lit@(Lit _) -> [mkPEq lit e]
+      lit@(Lit _) -> [PEq lit e]
       _ -> []
   _ -> []
 

src/EVM/SMT.hs

@@ -278,7 +278,7 @@ assertPropsNoSimp config psPreConc =
     abstProps = map toProp (Map.toList abstExprToInt)
       where
       toProp :: (Expr EWord, Int) -> Prop
-      toProp (e, num) = mkPEq e (Var (TS.pack ("abst_" ++ (show num))))
+      toProp (e, num) = PEq e (Var (TS.pack ("abst_" ++ (show num))))
 
     -- Props storing info that need declaration(s)
     toDeclarePs     = ps <> keccAssump <> keccComp
@@ -404,11 +404,11 @@ assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
 assertReads props benv senv = concatMap assertRead allReads
   where
     assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]
-    assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (mkPEq (ReadWord idx buf) (Lit 0))]
+    assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))]
     assertRead (idx, Lit sz, buf) =
       fmap
         -- TODO: unsafeInto instead fromIntegral here makes symbolic tests fail
-        (PImpl (PGEq idx (bufLength buf)) . mkPEq (ReadByte idx buf) . LitByte . fromIntegral)
+        (PImpl (PGEq idx (bufLength buf)) . PEq (ReadByte idx buf) . LitByte . fromIntegral)
         [(0::Int)..unsafeInto sz-1]
     assertRead (_, _, _) = internalError "Cannot generate assertions for accesses of symbolic size"
 

src/EVM/SymExec.hs

@@ -101,7 +101,7 @@ extractCex (Cex c) = Just c
 extractCex _ = Nothing
 
 bool :: Expr EWord -> Prop
-bool e = POr (mkPEq (Lit 1) e) (mkPEq (Lit 0) e)
+bool e = POr (PEq (Lit 1) e) (PEq (Lit 0) e)
 
 -- | Abstract calldata argument generation
 symAbiArg :: Text -> AbiType -> CalldataFragment
@@ -420,7 +420,7 @@ getExpr solvers c signature' concreteArgs opts = do
 checkAssertions :: [Word256] -> Postcondition s
 checkAssertions errs _ = \case
   Failure _ _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs)
-  Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . mkPEq b . ConcreteBuf . panicMsg) errs)
+  Failure _ _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)
   _ -> PBool True
 
 -- | By default hevm only checks for user-defined assertions
@@ -483,7 +483,7 @@ flattenExpr = go []
   where
     go :: [Prop] -> Expr End -> [Expr End]
     go pcs = \case
-      ITE c t f -> go (PNeg ((mkPEq (Lit 0) c)) : pcs) t <> go (mkPEq (Lit 0) c : pcs) f
+      ITE c t f -> go (PNeg ((PEq (Lit 0) c)) : pcs) t <> go (PEq (Lit 0) c : pcs) f
       Success ps trace msg store -> [Success (nubOrd $ ps <> pcs) trace msg store]
       Failure ps trace e -> [Failure (nubOrd $ ps <> pcs) trace e]
       Partial ps trace p -> [Partial (nubOrd $ ps <> pcs) trace p]
@@ -514,8 +514,8 @@ reachable solvers e = do
     go conf pcs = \case
       ITE c t f -> do
         (tres, fres) <- concurrently
-          (go conf (mkPEq (Lit 1) c : pcs) t)
-          (go conf (mkPEq (Lit 0) c : pcs) f)
+          (go conf (PEq (Lit 1) c : pcs) t)
+          (go conf (PEq (Lit 0) c : pcs) f)
         let subexpr = case (snd tres, snd fres) of
               (Just t', Just f') -> Just $ ITE c t' f'
               (Just t', Nothing) -> Just t'

src/EVM/Traversals.hs

@@ -211,7 +211,7 @@ foldExpr f acc expr = acc <> (go expr)
 mapProp :: (forall a . Expr a -> Expr a) -> Prop -> Prop
 mapProp f = \case
   PBool b -> PBool b
-  PEq a b -> mkPEq (mapExpr f (f a)) (mapExpr f (f b))
+  PEq a b -> PEq (mapExpr f (f a)) (mapExpr f (f b))
   PLT a b -> PLT (mapExpr f (f a)) (mapExpr f (f b))
   PGT a b -> PGT (mapExpr f (f a)) (mapExpr f (f b))
   PLEq a b -> PLEq (mapExpr f (f a)) (mapExpr f (f b))
@@ -612,7 +612,7 @@ mapPropM f = \case
   PEq a b -> do
     a' <- mapExprM f a
     b' <- mapExprM f b
-    pure $ mkPEq a' b'
+    pure $ PEq a' b'
   PLT a b -> do
     a' <- mapExprM f a
     b' <- mapExprM f b

src/EVM/Types.hs

@@ -432,14 +432,6 @@ data Prop where
   PBool :: Bool -> Prop
 deriving instance (Show Prop)
 
-mkPEq :: (Typeable a) => Expr a -> Expr a -> Prop
-mkPEq (Lit x) (Lit y) = PBool (x == y)
-mkPEq a@(Lit _) b = PEq a b
-mkPEq a b@(Lit _) = PEq b a -- we always put concrete values on LHS
-mkPEq a b
-  | a == b = PBool True
-  | otherwise = PEq a b
-
 infixr 3 .&&
 (.&&) :: Prop -> Prop -> Prop
 x .&& y = PAnd x y
@@ -460,9 +452,9 @@ x .>= y = PGEq x y
 
 infix 4 .==, ./=
 (.==) :: (Typeable a) => Expr a -> Expr a -> Prop
-x .== y = mkPEq x y
+x .== y = PEq x y
 (./=) :: (Typeable a) => Expr a -> Expr a -> Prop
-x ./= y = PNeg (mkPEq x y)
+x ./= y = PNeg (PEq x y)
 
 pand :: [Prop] -> Prop
 pand = foldl' PAnd (PBool True)