From 893d2246c6eb76b11adf61ebae872ff7e24303f0 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 12 Oct 2023 12:21:00 +0200
Subject: [PATCH 1/2] Renaming evalprop

---
 src/EVM.hs         |  2 +-
 src/EVM/Expr.hs    | 10 +++++-----
 src/EVM/SymExec.hs |  2 +-
 test/test.hs       |  6 +++---
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index e9e2a79c2..12a2c0e4f 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1266,7 +1266,7 @@ branch cond continue = do
     choosePath :: CodeLocation -> BranchCondition -> EVM s ()
     choosePath loc (Case v) = do
       assign #result Nothing
-      pushTo #constraints $ if v then Expr.evalProp (condSimp ./= Lit 0) else Expr.evalProp (condSimp .== Lit 0)
+      pushTo #constraints $ if v then Expr.simplifyProp (condSimp ./= Lit 0) else Expr.simplifyProp (condSimp .== Lit 0)
       (iteration, _) <- use (#iterations % at loc % non (0,[]))
       stack <- use (#state % #stack)
       assign (#cache % #path % at (loc, iteration)) (Just v)
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
index ff39a0dc6..1837eafdb 100644
--- a/src/EVM/Expr.hs
+++ b/src/EVM/Expr.hs
@@ -978,14 +978,14 @@ simplify e = if (mapExpr go e == e)
 simplifyProps :: [Prop] -> [Prop]
 simplifyProps ps = if canBeSat then simplified else [PBool False]
   where
-    simplified = remRedundantProps . map evalProp . flattenProps $ ps
+    simplified = remRedundantProps . map simplifyProp . flattenProps $ ps
     canBeSat = constFoldProp simplified
 
 -- | Evaluate the provided proposition down to its most concrete result
-evalProp :: Prop -> Prop
-evalProp prop =
+simplifyProp :: Prop -> Prop
+simplifyProp prop =
   let new = mapProp' go (simpInnerExpr prop)
-  in if (new == prop) then prop else evalProp new
+  in if (new == prop) then prop else simplifyProp new
   where
     go :: Prop -> Prop
 
@@ -1305,7 +1305,7 @@ data ConstState = ConstState
 constFoldProp :: [Prop] -> Bool
 constFoldProp ps = oneRun ps (ConstState mempty True)
   where
-    oneRun ps2 startState = (execState (mapM (go . evalProp) ps2) startState).canBeSat
+    oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat
     go :: Prop -> State ConstState ()
     go x = case x of
         PEq (Lit l) a -> do
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 4203ad509..bf72308e2 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -573,7 +573,7 @@ verify solvers opts preState maybepost = do
       let
         -- Filter out any leaves that can be statically shown to be safe
         canViolate = flip filter flattened $
-          \leaf -> case Expr.evalProp (post preState leaf) of
+          \leaf -> case Expr.simplifyProp (post preState leaf) of
             PBool True -> False
             _ -> True
         assumes = preState.constraints
diff --git a/test/test.hs b/test/test.hs
index c40d314c1..7dc1a888e 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -397,14 +397,14 @@ tests = testGroup "hevm"
           Just asList -> do
             let asBuf = Expr.fromList asList
             checkEquiv asBuf input
-    , testProperty "evalProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do
+    , testProperty "simplifyProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do
         let simplified = Expr.simplifyProps [p]
         case simplified of
           [] -> checkEquivProp (PBool True) p
           [val@(PBool _)] -> checkEquivProp val p
           _ -> assertFailure "must evaluate down to a literal bool"
-    , testProperty "evalProp-equivalence-sym" $ \(p) -> ioProperty $ do
-        let simplified = Expr.evalProp p
+    , testProperty "simplifyProp-equivalence-sym" $ \(p) -> ioProperty $ do
+        let simplified = Expr.simplifyProp p
         checkEquivProp simplified p
     , testProperty "simpProp-equivalence-sym" $ \(ps :: [Prop]) -> ioProperty $ do
         let simplified = pand (Expr.simplifyProps ps)

From 4040a3475fe833cb0755bd14b9434216c27685f7 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 18 Oct 2023 12:32:16 +0200
Subject: [PATCH 2/2] Adding CHANGELOG entry

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43a940cbc..ea82a42ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -52,6 +52,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
 - Better simplification of Eq IR elements
 - Run a toplevel constant folding reasoning system on branch conditions
+- `evalProp` is renamed to `simplifyProp` for consistency
 
 ## API Changes