Skip to content

Commit 7e73f1d

Browse files
msoosethmsooseth
authored
Merge pull request #693 from ethereum/one-more-simp-rule
Better structuring of `simplify`
2 parents 6c2869b + 211783a commit 7e73f1d

File tree

3 files changed

+182
-78
lines changed

3 files changed

+182
-78
lines changed

‎src/EVM/Expr.hs‎

Lines changed: 99 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -61,37 +61,24 @@ op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)
6161
op3 _ concrete (Lit x) (Lit y) (Lit z) = Lit (concrete x y z)
6262
op3 symbolic _ x y z = symbolic x y z
6363

64-
-- | If a given binary op is commutative, then we always force Lits to the lhs if
65-
-- only one argument is a Lit. This makes writing pattern matches in the
66-
-- simplifier easier.
64+
-- | If a given binary op is commutative, then we always order the arguments.
65+
-- This makes writing pattern matches in the simplifier easier.
66+
-- It will also force Lit to be the 1st argument, since Lit is the 1st element of Expr (see Types.hs).
6767
normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
68-
normArgs sym conc l r = case (l, r) of
69-
(Lit _, _) -> doOp l r
70-
(_, Lit _) -> doOp r l
71-
_ -> doOp l r
72-
where
73-
doOp = op2 sym conc
74-
75-
-- Same as `normArgs`, but for commutative operators it orders the arguments canonically
76-
-- This helps in cases when (PEq x1 x2) is comparing x1 and x2 that are equivalent modulo commutativity.
77-
-- In such cases, normArgsOrd will make sure x1 and x2 look the same.
78-
-- NOTE: This is compatible with `Lit` being always on the left, as `Lit` is always
79-
-- less than any other expression
80-
normArgsOrd :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
81-
normArgsOrd sym conc l r = if l <= r then doOp l r else doOp r l
68+
normArgs sym conc l r = if l <= r then doOp l r else doOp r l
8269
where
8370
doOp = op2 sym conc
8471

8572
-- Integers
8673

8774
add :: Expr EWord -> Expr EWord -> Expr EWord
88-
add = normArgsOrd Add (+)
75+
add = normArgs Add (+)
8976

9077
sub :: Expr EWord -> Expr EWord -> Expr EWord
9178
sub = op2 Sub (-)
9279

9380
mul :: Expr EWord -> Expr EWord -> Expr EWord
94-
mul = normArgsOrd Mul (*)
81+
mul = normArgs Mul (*)
9582

9683
div :: Expr EWord -> Expr EWord -> Expr EWord
9784
div = op2 Div (\x y -> if y == 0 then 0 else Prelude.div x y)
@@ -166,21 +153,21 @@ sgt = op2 SGT (\x y ->
166153
in if sx > sy then 1 else 0)
167154

168155
eq :: Expr EWord -> Expr EWord -> Expr EWord
169-
eq = normArgsOrd Eq (\x y -> if x == y then 1 else 0)
156+
eq = normArgs Eq (\x y -> if x == y then 1 else 0)
170157

171158
iszero :: Expr EWord -> Expr EWord
172159
iszero = op1 IsZero (\x -> if x == 0 then 1 else 0)
173160

174161
-- Bits
175162

176163
and :: Expr EWord -> Expr EWord -> Expr EWord
177-
and = normArgsOrd And (.&.)
164+
and = normArgs And (.&.)
178165

179166
or :: Expr EWord -> Expr EWord -> Expr EWord
180-
or = normArgsOrd Or (.|.)
167+
or = normArgs Or (.|.)
181168

182169
xor :: Expr EWord -> Expr EWord -> Expr EWord
183-
xor = normArgsOrd Xor Data.Bits.xor
170+
xor = normArgs Xor Data.Bits.xor
184171

185172
not :: Expr EWord -> Expr EWord
186173
not = op1 Not complement
@@ -634,7 +621,7 @@ readStorage' loc store = case readStorage loc store of
634621
-- test for an example where this happens. Note that decomposition solves this, though late in
635622
-- the simplification lifecycle (just before SMT generation, which can be too late)
636623
readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
637-
readStorage w st = go (simplify w) st
624+
readStorage w st = go (simplifyNoLitToKeccak w) (simplifyNoLitToKeccak st)
638625
where
639626
go :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
640627
go _ (GVar _) = internalError "Can't read from a GVar"
@@ -644,21 +631,23 @@ readStorage w st = go (simplify w) st
644631
go slot s@(SStore prevSlot val prev) = case (prevSlot, slot) of
645632
-- if address and slot match then we return the val in this write
646633
_ | prevSlot == slot -> Just val
647-
648-
-- if the slots don't match (see previous guard) and are lits, we can skip this write
649-
(Lit _, Lit _) -> go slot prev
634+
(a, b) | surelyEqual a b -> Just val
635+
(a, b) | surelyNotEqual a b -> go slot prev
650636

651637
-- slot is for a map + map -> skip write
652-
(MappingSlot idA _, MappingSlot idB _) | BS.length idB == 64 && BS.length idA == 64 && idsDontMatch idA idB -> go slot prev
653-
(MappingSlot idA keyA, MappingSlot idB keyB) | BS.length idB == 64 && BS.length idA == 64 && surelyNotEq keyA keyB -> go slot prev
638+
(MappingSlot idA _, MappingSlot idB _) | isMap' idB, isMap' idA, idsDontMatch idA idB -> go slot prev
639+
(MappingSlot idA keyA, MappingSlot idB keyB) | isMap' idB, isMap' idA, surelyNotEqual keyA keyB -> go slot prev
654640

655641
-- special case of array + map -> skip write
656-
(ArraySlotWithOffs idA _, Keccak k) | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev
657-
(ArraySlotZero idA, Keccak k) | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev
642+
(ArraySlotWithOffs idA _, Keccak k) | isMap k, isArray idA -> go slot prev
643+
(ArraySlotWithOffs2 idA _ _, Keccak k) | isMap k, isArray idA -> go slot prev
644+
(ArraySlotZero idA, Keccak k) | isMap k, isArray idA -> go slot prev
658645

659646
-- special case of map + array -> skip write
660-
(Keccak k, ArraySlotWithOffs idA _) | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev
661-
(ArraySlotWithOffs idA _, Keccak k) | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev
647+
(Keccak k, ArraySlotWithOffs idA _) | isMap k, isArray idA -> go slot prev
648+
(Keccak k, ArraySlotWithOffs2 idA _ _) | isMap k, isArray idA -> go slot prev
649+
(ArraySlotWithOffs idA _, Keccak k) | isMap k, isArray idA -> go slot prev
650+
(ArraySlotWithOffs2 idA _ _, Keccak k) | isMap k, isArray idA -> go slot prev
662651

663652
-- Fixed SMALL value will never match Keccak (well, it might, but that's VERY low chance)
664653
(Lit a, Keccak _) | a < 256 -> go slot prev
@@ -669,47 +658,58 @@ readStorage w st = go (simplify w) st
669658
-- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero
670659
-- for our purposes. This lets us completely simplify reads from write
671660
-- chains involving writes to arrays at literal offsets.
672-
(Lit a, Add (Lit b) (Keccak _) ) | a < 256, b < maxW32 -> go slot prev
673-
(Add (Lit a) (Keccak _) , Lit b) | b < 256, a < maxW32 -> go slot prev
674-
675-
--- NOTE these are needed to succeed in rewriting arrays with a variable index
676-
-- (Lit a, Add (Keccak _) (Var _) ) | a < 256 -> go slot prev
677-
-- (Add (Keccak _) (Var _) , Lit b) | b < 256 -> go slot prev
661+
(Lit a, Add (Lit b) (Keccak _)) | a < 256, b < maxW32 -> go slot prev
662+
(Add (Lit a) (Keccak _) ,Lit b) | b < 256, a < maxW32 -> go slot prev
678663

679664
-- Finding two Keccaks that are < 256 away from each other should be VERY hard
680665
-- This simplification allows us to deal with maps of structs
681666
(Add (Lit a2) (Keccak _), Add (Lit b2) (Keccak _)) | a2 /= b2, abs (a2-b2) < 256 -> go slot prev
682667
(Add (Lit a2) (Keccak _), (Keccak _)) | a2 > 0, a2 < 256 -> go slot prev
683668
((Keccak _), Add (Lit b2) (Keccak _)) | b2 > 0, b2 < 256 -> go slot prev
684669

685-
-- case of array + array, but different id's or different concrete offsets
686670
-- zero offs vs zero offs
687-
(ArraySlotZero idA, ArraySlotZero idB) | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev
671+
(ArraySlotZero idA, ArraySlotZero idB) | isArray idA, isArray idB, idA /= idB -> go slot prev
672+
688673
-- zero offs vs non-zero offs
689-
(ArraySlotZero idA, ArraySlotWithOffs idB _) | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev
690-
(ArraySlotZero idA, ArraySlotWithOffs idB (Lit offB)) | BS.length idA == 32, BS.length idB == 32, offB /= 0 -> go slot prev
691-
-- non-zero offs vs zero offs
692-
(ArraySlotWithOffs idA _, ArraySlotZero idB) | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev
693-
(ArraySlotWithOffs idA (Lit offA), ArraySlotZero idB) | BS.length idA == 32, BS.length idB == 32, offA /= 0 -> go slot prev
694-
-- non-zero offs vs non-zero offs
695-
(ArraySlotWithOffs idA _, ArraySlotWithOffs idB _) | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev
674+
(ArraySlotZero idA, ArraySlotWithOffs idB _) | isArray idA, isArray idB, idA /= idB -> go slot prev
675+
(ArraySlotZero idA, ArraySlotWithOffs idB (Lit offB)) | isArray idA, idA == idB, offB /= 0 -> go slot prev
676+
(ArraySlotZero idA, ArraySlotWithOffs2 idB _ _) | isArray idA, isArray idB, idA /= idB -> go slot prev
696677

697-
(ArraySlotWithOffs idA offA, ArraySlotWithOffs idB offB) | BS.length idA == 32, BS.length idB == 32, surelyNotEq offA offB -> go slot prev
678+
-- non-zero offs vs zero offs
679+
(ArraySlotWithOffs idA _, ArraySlotZero idB) | isArray idA, isArray idB, idA /= idB -> go slot prev
680+
(ArraySlotWithOffs idA (Lit offA), ArraySlotZero idB) | isArray idA, idA == idB, offA /= 0 -> go slot prev
681+
682+
-- non-zero offs vs non-zero offs, different ids
683+
(ArraySlotWithOffs idA _, ArraySlotWithOffs idB _) | isArray idA, isArray idB, idA /= idB -> go slot prev
684+
685+
-- non-zero offs vs non-zero offs, same ids
686+
(ArraySlotWithOffs idA a, ArraySlotWithOffs idB b) | isArray idA, idA == idB,
687+
surelyNotEqual a b -> go slot prev
688+
(ArraySlotWithOffs idB offB2, ArraySlotWithOffs2 idA offA1 offA2) | isArray idA, idA == idB,
689+
surelyNotEqual (Add (Lit offA1) offA2) offB2 -> go slot prev
690+
(ArraySlotWithOffs2 idA offA1 offA2, ArraySlotWithOffs idB offB2) | isArray idA, idA == idB,
691+
surelyNotEqual (Add (Lit offA1) offA2) offB2 -> go slot prev
692+
(ArraySlotWithOffs2 idA offA1 offA2, ArraySlotWithOffs2 idB offB1 offB2) | isArray idA, idA == idB,
693+
surelyNotEqual (Add (Lit offA1) offA2) (Add (Lit offB1) offB2) -> go slot prev
698694

699695
-- we are unable to determine statically whether or not we can safely move deeper in the write chain, so return an abstract term
700696
_ -> Just $ SLoad slot s
701697

702-
surelyNotEq :: Expr a -> Expr a -> Bool
703-
surelyNotEq (Lit a) (Lit b) = a /= b
704-
-- never equal: x+y (y is concrete) vs x+z (z is concrete), y!=z
705-
surelyNotEq (Add (Lit l1) v1) (Add (Lit l2) v2) = l1 /= l2 && v1 == v2
706-
-- never equal: x+y (y is concrete, non-zero) vs x
707-
surelyNotEq v1 (Add (Lit l2) v2) = l2 /= 0 && v1 == v2
708-
surelyNotEq (Add (Lit l1) v1) v2 = l1 /= 0 && v1 == v2
709-
surelyNotEq _ _ = False
710-
711698
maxW32 :: W256
712699
maxW32 = into (maxBound :: Word32)
700+
isArray :: ByteString -> Bool
701+
isArray b = BS.length b == 32
702+
isMap :: Expr Buf -> Bool
703+
isMap b = bufLength b == Lit 64
704+
isMap' :: ByteString -> Bool
705+
isMap' b = BS.length b == 64
706+
surelyNotEqual :: Expr EWord -> Expr EWord -> Bool
707+
surelyNotEqual a b = case (simplifyNoLitToKeccak (Sub a b)) of
708+
Lit k | k > 0 -> True
709+
_ -> False
710+
surelyEqual :: Expr EWord -> Expr EWord -> Bool
711+
surelyEqual a b = simplifyNoLitToKeccak (Sub a b) == Lit 0
712+
713713

714714
-- storage slots for maps are determined by (keccak (bytes32(key) ++ bytes32(id)))
715715
pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord
@@ -720,10 +720,12 @@ pattern MappingSlot idx key = Keccak (WriteWord (Lit 0) key (ConcreteBuf idx))
720720
pattern ArraySlotWithOffs :: ByteString -> Expr EWord -> Expr EWord
721721
pattern ArraySlotWithOffs id offset = Add offset (Keccak (ConcreteBuf id))
722722

723+
pattern ArraySlotWithOffs2 :: ByteString -> W256 -> Expr EWord -> Expr EWord
724+
pattern ArraySlotWithOffs2 id offs1 offs2 = Add (Lit offs1) (Add offs2 (Keccak (ConcreteBuf id)))
725+
723726
-- special pattern to match the 0th element because the `Add` term gets simplified out
724727
pattern ArraySlotZero :: ByteString -> Expr EWord
725728
pattern ArraySlotZero id = Keccak (ConcreteBuf id)
726-
727729
-- checks if two mapping ids match or not
728730
idsDontMatch :: ByteString -> ByteString -> Bool
729731
idsDontMatch a b = BS.length a >= 64 && BS.length b >= 64 && diff32to64Byte a b
@@ -738,8 +740,8 @@ slotPos :: Word8 -> ByteString
738740
slotPos pos = BS.pack ((replicate 31 (0::Word8))++[pos])
739741

740742
-- | Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)
741-
structureArraySlots :: Expr a -> Expr a
742-
structureArraySlots e = mapExpr go e
743+
litToKeccak :: Expr a -> Expr a
744+
litToKeccak e = mapExpr go e
743745
where
744746
go :: Expr a -> Expr a
745747
go orig@(Lit key) = case litToArrayPreimage key of
@@ -833,6 +835,7 @@ safeToDecompose inp = if result /= Mixed then Just () else Nothing
833835
Lit 64 -> setMap e
834836
_ -> setMixed e
835837
go e@(SLoad (ArraySlotWithOffs x _) _) = if BS.length x == 32 then setArray e else setMixed e
838+
go e@(SLoad (ArraySlotWithOffs2 x _ _) _) = if BS.length x == 32 then setArray e else setMixed e
836839
go e@(SLoad (Lit x) _) | x < 256 = setSmall e
837840
go e@(SLoad _ _) = setMixed e
838841
go e@(SStore (MappingSlot x _) _ _) = if BS.length x == 64 then setMap e else setMixed e
@@ -841,6 +844,7 @@ safeToDecompose inp = if result /= Mixed then Just () else Nothing
841844
Lit 64 -> setMap e
842845
_ -> setMixed e
843846
go e@(SStore (ArraySlotWithOffs x _) _ _) = if BS.length x == 32 then setArray e else setMixed e
847+
go e@(SStore (ArraySlotWithOffs2 x _ _) _ _) = if BS.length x == 32 then setArray e else setMixed e
844848
go e@(SStore (Lit x) _ _) | x < 256 = setSmall e
845849
go e@(SStore _ _ _) = setMixed e
846850
go _ = pure ()
@@ -914,6 +918,7 @@ decomposeStorage = go
914918
(MappingSlot idx key) | BS.length idx == 64 -> Just (Just $ idxToWord idx, key)
915919
-- arrays
916920
(ArraySlotWithOffs idx offset) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, offset)
921+
(ArraySlotWithOffs2 idx offs1 offs2) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, Add (Lit offs1) offs2)
917922
(ArraySlotZero idx) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, Lit 0)
918923
_ -> Nothing
919924

@@ -952,9 +957,10 @@ decomposeStorage = go
952957
-- | Simple recursive match based AST simplification
953958
-- Note: may not terminate!
954959
simplify :: Expr a -> Expr a
955-
simplify e = if (mapExpr go e == e)
956-
then e
957-
else simplify (mapExpr go (structureArraySlots e))
960+
simplify e = untilFixpoint (simplifyNoLitToKeccak . litToKeccak) e
961+
962+
simplifyNoLitToKeccak :: Expr a -> Expr a
963+
simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
958964
where
959965
go :: Expr a -> Expr a
960966

@@ -1037,6 +1043,7 @@ simplify e = if (mapExpr go e == e)
10371043
| otherwise = Lit 0
10381044
go (EVM.Types.LT _ (Lit 0)) = Lit 0
10391045
go (EVM.Types.LT a (Lit 1)) = iszero a
1046+
go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)
10401047

10411048
-- normalize all comparisons in terms of LT
10421049
go (EVM.Types.GT a b) = lt b a
@@ -1120,16 +1127,29 @@ simplify e = if (mapExpr go e == e)
11201127
go (Add (Lit a) (Add (Lit b) x)) = add (Lit (a+b)) x
11211128
go (Mul (Lit a) (Mul (Lit b) x)) = mul (Lit (a*b)) x
11221129
go (Xor (Lit a) (Xor (Lit b) x)) = EVM.Expr.xor (Lit (Data.Bits.xor a b)) x
1130+
go (Add (Add a b) c) = add (l !! 0) (add (l !! 1) (l !! 2))
1131+
where l = sort [a, b, c]
11231132
go (Add a (Add b c)) = add (l !! 0) (add (l !! 1) (l !! 2))
11241133
where l = sort [a, b, c]
1134+
go (Mul (Mul a b) c) = mul (l !! 0) (mul (l !! 1) (l !! 2))
1135+
where l = sort [a, b, c]
11251136
go (Mul a (Mul b c)) = mul (l !! 0) (mul (l !! 1) (l !! 2))
11261137
where l = sort [a, b, c]
1138+
go (Xor (Xor a b) c) = x (l !! 0) (x (l !! 1) (l !! 2))
1139+
where l = sort [a, b, c]
1140+
x = EVM.Expr.xor
11271141
go (Xor a (Xor b c)) = x (l !! 0) (x (l !! 1) (l !! 2))
11281142
where l = sort [a, b, c]
11291143
x = EVM.Expr.xor
1144+
go (Or (Or a b) c) = o (l !! 0) (o (l !! 1) (l !! 2))
1145+
where l = sort [a, b, c]
1146+
o = EVM.Expr.or
11301147
go (Or a (Or b c)) = o (l !! 0) (o (l !! 1) (l !! 2))
11311148
where l = sort [a, b, c]
11321149
o = EVM.Expr.or
1150+
go (And (And a b) c) = an (l !! 0) (an (l !! 1) (l !! 2))
1151+
where l = sort [a, b, c]
1152+
an = EVM.Expr.and
11331153
go (And a (And b c)) = an (l !! 0) (an (l !! 1) (l !! 2))
11341154
where l = sort [a, b, c]
11351155
an = EVM.Expr.and
@@ -1259,9 +1279,11 @@ simplifyProp prop =
12591279
where
12601280
go :: Prop -> Prop
12611281

1262-
-- LT/LEq comparisons
1282+
-- Rewrite PGT/GEq to PLT/PLEq
12631283
go (PGT a b) = PLT b a
12641284
go (PGEq a b) = PLEq b a
1285+
1286+
-- PLT/PLEq comparisons
12651287
go (PLT (Var _) (Lit 0)) = PBool False
12661288
go (PLEq (Lit 0) _) = PBool True
12671289
go (PLEq (WAddr _) (Lit 1461501637330902918203684832716283019655932542975)) = PBool True
@@ -1289,8 +1311,14 @@ simplifyProp prop =
12891311
-- Empty buf
12901312
go (PEq (Lit 0) (BufLength k)) = peq k (ConcreteBuf "")
12911313

1314+
-- PEq rewrites (notice -- GT/GEq is always rewritten to LT by simplify)
1315+
go (PEq (Lit 1) (IsZero (LT a b))) = PLT a b
1316+
go (PEq (Lit 1) (IsZero (LEq a b))) = PLEq a b
1317+
go (PEq (Lit 0) (IsZero a)) = PLT (Lit 0) a
1318+
go (PEq a1 (Add a2 y)) | a1 == a2 = peq y (Lit 0)
1319+
12921320
-- solc specific stuff
1293-
go (PEq (Lit 0) (IsZero (IsZero (Eq a b)))) = PNeg (peq a b)
1321+
go (PLT (Lit 0) (IsZero (Eq a b))) = PNeg (peq a b)
12941322

12951323
-- iszero(a) -> (a == 0)
12961324
-- iszero(iszero(a))) -> ~(a == 0) -> a > 0
@@ -1324,18 +1352,16 @@ simplifyProp prop =
13241352
go (PImpl (PBool True) b) = b
13251353
go (PImpl (PBool False) _) = PBool True
13261354

1327-
-- Double negation
1328-
go (PEq (Lit 0) (IsZero (Eq a b))) = peq a b
1329-
go (PEq (Lit 0) (IsZero (LT a b))) = PLT a b
1330-
go (PEq (Lit 0) (IsZero (GT a b))) = PGT a b
1331-
go (PEq (Lit 0) (IsZero (LEq a b))) = PLEq a b
1332-
go (PEq (Lit 0) (IsZero (GEq a b))) = PGEq a b
1355+
-- Double negation (no need for GT/GEq, as it's rewritten to LT/LEq)
1356+
go (PLT (Lit 0) (LT a b)) = PLT a b
1357+
go (PLT (Lit 0) (LEq a b)) = PLEq a b
13331358

13341359
-- Eq
13351360
go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)
13361361
go (PEq (Lit 1) (Eq a b)) = peq a b
13371362
go (PEq (Lit 0) (Sub a b)) = peq a b
13381363
go (PEq (Lit 0) (LT a b)) = PLEq b a
1364+
go (PEq (Lit 0) (LEq a b)) = PLT b a
13391365
go (PEq l r) = peq l r
13401366

13411367
go p = p
@@ -1656,7 +1682,7 @@ constPropagate ps =
16561682

16571683
-- Concretize & simplify Keccak expressions until fixed-point.
16581684
concKeccakSimpExpr :: Expr a -> Expr a
1659-
concKeccakSimpExpr orig = untilFixpoint ((mapExpr concKeccakOnePass) . simplify) orig
1685+
concKeccakSimpExpr orig = untilFixpoint (simplifyNoLitToKeccak . (mapExpr concKeccakOnePass)) (simplify orig)
16601686

16611687
-- Only concretize Keccak in Props
16621688
-- Needed because if it also simplified, we may not find some simplification errors, as

0 commit comments

Comments
 (0)