Skip to content

Expr: Canonicalize transformations #929

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 15, 2025
Merged

Expr: Canonicalize transformations #929

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
171 changes: 81 additions & 90 deletions src/EVM/Expr.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1049,6 +1049,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
go (IsZero (IsZero (IsZero a))) = iszero a
go (IsZero (IsZero (LT x y))) = lt x y
go (IsZero (IsZero (Eq x y))) = eq x y
go (IsZero (IsZero a)) = lt (Lit 0) a
go (IsZero (Xor x y)) = eq x y
go (IsZero a) = iszero a

Expand All @@ -1062,6 +1063,47 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
| a == b = Lit 1
| otherwise = eq a b

-- COMPARISONS
-- First special cases

-- we write at least 32, so if x <= 32, it's FALSE
go o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit x))
| x <= 32 = Lit 0
| otherwise = o
-- we write at least 32, so if x < 32, it's TRUE
go o@(EVM.Types.LT (Lit x) (BufLength (WriteWord {})))
| x < 32 = Lit 1
| otherwise = o

-- If a >= b then the value of the `Max` expression can never be < b
go o@(LT (Max (Lit a) _) (Lit b))
| a >= b = Lit 0
| otherwise = o
go o@(SLT (Sub (Max (Lit a) _) (Lit b)) (Lit c))
= let sa, sb, sc :: Int256
sa = fromIntegral a
sb = fromIntegral b
sc = fromIntegral c
in if sa >= sb && sa - sb >= sc
then Lit 0
else o

-- normalize all comparisons in terms of (S)LT
go (EVM.Types.GT a b) = lt b a
go (EVM.Types.GEq a b) = iszero (lt a b)
go (EVM.Types.LEq a b) = iszero (lt b a)
go (SGT a b) = slt b a

-- LT
go (EVM.Types.LT _ (Lit 0)) = Lit 0
go (EVM.Types.LT a (Lit 1)) = iszero a
go (EVM.Types.LT a b) = lt a b

-- SLT
go (SLT _ (Lit a)) | a == minLitSigned = Lit 0
go (SLT (Lit a) _) | a == maxLitSigned = Lit 0
go (SLT a b) = slt a b

-- redundant ITE
go (ITE (Lit x) a b)
| x == 0 = b
Expand Down Expand Up @@ -1221,15 +1263,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
| otherwise = t
go (ITE (Or a b@(Lit _)) t f) = ITE (Or b a) t f

-- we write at least 32, so if x <= 32, it's FALSE
go o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit x))
| x <= 32 = Lit 0
| otherwise = o
-- we write at least 32, so if x < 32, it's TRUE
go o@(EVM.Types.LT (Lit x) (BufLength (WriteWord {})))
| x < 32 = Lit 1
| otherwise = o

-- Double NOT is a no-op, since it's a bitwise inversion
go (EVM.Types.Not (EVM.Types.Not a)) = a

Expand Down Expand Up @@ -1261,35 +1294,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
-- NOTE: we can't simplify (Lit 0)^k. If k is 0 it's 1, otherwise it's 0.
-- this is encoded in SMT.hs instead, via an SMT "ite"

-- If a >= b then the value of the `Max` expression can never be < b
go o@(LT (Max (Lit a) _) (Lit b))
| a >= b = Lit 0
| otherwise = o
go o@(SLT (Sub (Max (Lit a) _) (Lit b)) (Lit c))
= let sa, sb, sc :: Int256
sa = fromIntegral a
sb = fromIntegral b
sc = fromIntegral c
in if sa >= sb && sa - sb >= sc
then Lit 0
else o

-- normalize all comparisons in terms of (S)LT
go (EVM.Types.GT a b) = lt b a
go (EVM.Types.GEq a b) = leq b a
go (EVM.Types.LEq a b) = iszero (lt b a)
go (SGT a b) = slt b a

-- LT
go (EVM.Types.LT _ (Lit 0)) = Lit 0
go (EVM.Types.LT a (Lit 1)) = iszero a
go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)
go (EVM.Types.LT a b) = lt a b

-- SLT
go (SLT _ (Lit a)) | a == minLitSigned = Lit 0
go (SLT (Lit a) _) | a == maxLitSigned = Lit 0
go (SLT a b) = slt a b

-- simple div/mod/add/sub
go (Div o1 o2) = EVM.Expr.div o1 o2
Expand Down Expand Up @@ -1319,6 +1323,16 @@ simplifyProp prop =
let new = mapProp' go (simpInnerExpr prop)
in if (new == prop) then prop else simplifyProp new
where
isBoolLike :: Expr EWord -> Bool
isBoolLike = \case
LT{} -> True
SLT{} -> True
Eq{} -> True
IsZero{} -> True
GT{} -> internalError "Should not encounter GT at this point!"
LEq{} -> internalError "Should not encounter LEq at this point!"
GEq{} -> internalError "Should not encounter GEq at this point!"
_ -> False
go :: Prop -> Prop

-- Rewrite PGT/GEq to PLT/PLEq
Expand All @@ -1341,54 +1355,44 @@ simplifyProp prop =
go (PLEq (Sub a b) c) | a == c = PLEq b a
go (PLEq a (Lit 0)) = peq (Lit 0) a
go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
go (PLT (Lit 0) (Eq a b)) = peq a b
go (PLEq a b) = pleq a b

-- when it's PLT but comparison on the RHS then it's just (PEq 1 RHS)
go (PLT (Lit 0) (a@LT {})) = peq (Lit 1) a
go (PLT (Lit 0) (a@LEq {})) = peq (Lit 1) a
go (PLT (Lit 0) (a@SLT {})) = peq (Lit 1) a
go (PLT (Lit 0) (a@GT {})) = peq (Lit 1) a
go (PLT (Lit 0) (a@GEq {})) = peq (Lit 1) a
go (PLT (Lit 0) (a@SGT {})) = peq (Lit 1) a

go (PLT (Lit 0) e)
| isBoolLike e = peq (Lit 1) e

-- all possible simplifications for PLT and PLEq have to be covered by this point
go p@(PLT {}) = p
go p@(PLEq {}) = p

go (PEq (Lit 1) (Eq a b)) = peq a b
go (PEq (Lit 1) (LT a b)) = PLT a b
go (PEq (Lit 1) (IsZero e)) = PEq (Lit 0) e

go (PEq (Lit 0) (IsZero e))
| isBoolLike e = PEq (Lit 1) e
go (PEq (Lit 0) (IsZero e)) = PNeg (PEq (Lit 0) e)
go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)
go (PEq (Lit 0) (LT a b)) = PLEq b a

go (PEq (Lit 0) (Sub a b)) = peq a b
go (PEq (Lit 0) (Or a b)) = peq (Lit 0) a `PAnd` peq (Lit 0) b
go (PEq a1 (Add a2 y)) | a1 == a2 = peq (Lit 0) y
go (PEq l r) = peq l r

go (POr (PLEq a1 (Lit b)) (PLEq (Lit c) a2)) | a1 == a2 && c == b+1 = PBool True

-- negations
go (PNeg (PBool b)) = PBool (Prelude.not b)
go (PNeg (PNeg a)) = a
go (PNeg (PGT a b)) = PLEq a b
go (PNeg (PGEq a b)) = PLT a b
go (PNeg (PLT a b)) = PGEq a b
go (PNeg (PLEq a b)) = PGT a b
go (PNeg (PLT a b)) = PLEq b a
go (PNeg (PLEq a b)) = PLT b a
go (PNeg (PAnd a b)) = POr (PNeg a) (PNeg b)
go (PNeg (POr a b)) = PAnd (PNeg a) (PNeg b)
go (PNeg (PEq (Lit 1) (IsZero b))) = PEq (Lit 0) (IsZero b)

go (PEq (Lit 0) (Or a b)) = peq (Lit 0) a `PAnd` peq (Lit 0) b

-- PEq rewrites (notice -- GT/GEq is always rewritten to LT by simplify)
go (PEq (Lit 1) (IsZero (LT a b))) = PLEq b a
go (PEq (Lit 1) (IsZero (LEq a b))) = PLT b a
go (PEq (Lit 0) (IsZero a)) = PLT (Lit 0) a
go (PEq a1 (Add a2 y)) | a1 == a2 = peq (Lit 0) y

-- solc specific stuff
go (PLT (Lit 0) (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 (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 (Lit 0) (IsZero a))) = peq (Lit 0) a

-- a < b == 0 -> ~(a < b)
-- ~(a < b == 0) -> ~~(a < b) -> a < b
go (PNeg (PEq (Lit 0) (LT a b))) = PLT a b
go (PNeg (PEq (Lit 1) e))
| isBoolLike e = PEq (Lit 0) e
go (PNeg (PEq (Lit 0) e))
| isBoolLike e = PEq (Lit 1) e

-- And/Or
go (PAnd (PBool l) (PBool r)) = PBool (l && r)
Expand All @@ -1407,19 +1411,6 @@ simplifyProp prop =
go (PImpl (PBool True) b) = b
go (PImpl (PBool False) _) = PBool True

-- Double negation (no need for GT/GEq, as it's rewritten to LT/LEq)

-- Eq
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 (Lit 0) (LEq a b)) = PLT b a
go (PEq (Lit 1) (LT a b)) = PLT a b
go (PEq (Lit 1) (LEq a b)) = PLEq a b
go (PEq (Lit 1) (GT a b)) = PGT a b
go (PEq (Lit 1) (GEq a b)) = PGEq a b
go (PEq l r) = peq l r

go p = p

Expand Down