Do not simplify equality immediately on construction #546
Conversation
There was a problem hiding this comment.
Thanks Martin! This looks great. Just a small nit:
Since the logic for argument normalisation for Expr operators is in Expr.hs and already has a naming convention, it would make sense to have the same operators for Prop in the same file and with the same naming convention. Therefore, I would suggest moving mkPEq to Expr.hs and renaming it to peq for consistency.
src/EVM/Expr.hs
Outdated
| @@ -1214,29 +1214,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 | |||
There was a problem hiding this comment.
I don't understand this... it's under simplifyProp, why not do mkPEq here? It's the most obvious thing to do I think? I must be not getting something. Under simplify, which simplifies Expr, we have:
go (IsZero (IsZero (Eq x y))) = eq x y
Which is exactly the same idea -- eq will set the LHS, etc. So we seem to be inconsistent.
I don't mind it too much, but I just don't understand. Can you maybe explain what's the rationale and why is that eq ok, but this mkPEq not ok?
There was a problem hiding this comment.
I agree that here it would be good to simplify immediately. Do you agree as well, @zoep?
There was a problem hiding this comment.
I agree that for consistency it would be better to use peq/mkPEq here (though I understand that it doesn't matter so much as it will be simplified in the next iteration)
There was a problem hiding this comment.
Yeah, we would get to it on next iteration, it's true :)
src/EVM/Expr.hs
Outdated
| 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) |
There was a problem hiding this comment.
These are great, thank you so much!
src/EVM/Expr.hs
Outdated
| 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 |
src/EVM/Expr.hs
Outdated
|
|
||
| -- 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 |
There was a problem hiding this comment.
I'd change this to mkPEq
src/EVM/Expr.hs
Outdated
|
|
||
| -- 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) |
There was a problem hiding this comment.
I'd change this to mkPEq
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.
blishko
force-pushed
the
fix-equality-simplification
branch
from
5fb3246
to
b6753d8
Compare
|
Perfect, thanks, merging! |
Description
As @zoep pointed out it might be 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.
Checklist