{-# LANGUAGE DataKinds #-}
module EVM.Keccak (keccakAssumptions) where
import Prelude hiding (Word, LT, GT)
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Monad.State
import EVM.Types
import EVM.Traversals
data BuilderState = BuilderState
{ BuilderState -> Set (Expr 'EWord)
keccaks :: Set (Expr EWord) }
deriving (Int -> BuilderState -> ShowS
[BuilderState] -> ShowS
BuilderState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BuilderState] -> ShowS
$cshowList :: [BuilderState] -> ShowS
show :: BuilderState -> String
$cshow :: BuilderState -> String
showsPrec :: Int -> BuilderState -> ShowS
$cshowsPrec :: Int -> BuilderState -> ShowS
Show)
initState :: BuilderState
initState :: BuilderState
initState = BuilderState { $sel:keccaks:BuilderState :: Set (Expr 'EWord)
keccaks = forall a. Set a
Set.empty }
go :: forall a. Expr a -> State BuilderState (Expr a)
go :: forall (a :: EType). Expr a -> State BuilderState (Expr a)
go = \case
e :: Expr a
e@(Keccak Expr 'Buf
_) -> do
BuilderState
s <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ BuilderState
s{$sel:keccaks:BuilderState :: Set (Expr 'EWord)
keccaks=forall a. Ord a => a -> Set a -> Set a
Set.insert Expr a
e BuilderState
s.keccaks}
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
Expr a
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
findKeccakExpr :: forall a. Expr a -> State BuilderState (Expr a)
findKeccakExpr :: forall (a :: EType). Expr a -> State BuilderState (Expr a)
findKeccakExpr Expr a
e = forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM forall (a :: EType). Expr a -> State BuilderState (Expr a)
go Expr a
e
findKeccakProp :: Prop -> State BuilderState Prop
findKeccakProp :: Prop -> State BuilderState Prop
findKeccakProp Prop
p = forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> State BuilderState (Expr a)
go Prop
p
findKeccakPropsExprs :: [Prop] -> [Expr Buf] -> [Expr Storage]-> State BuilderState ()
findKeccakPropsExprs :: [Prop]
-> [Expr 'Buf]
-> [Expr 'Storage]
-> StateT BuilderState Identity ()
findKeccakPropsExprs [Prop]
ps [Expr 'Buf]
bufs [Expr 'Storage]
stores = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> State BuilderState Prop
findKeccakProp [Prop]
ps;
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (a :: EType). Expr a -> State BuilderState (Expr a)
findKeccakExpr [Expr 'Buf]
bufs;
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (a :: EType). Expr a -> State BuilderState (Expr a)
findKeccakExpr [Expr 'Storage]
stores
combine :: [a] -> [(a,a)]
combine :: forall a. [a] -> [(a, a)]
combine [a]
lst = forall {b}. [b] -> [[(b, b)]] -> [(b, b)]
combine' [a]
lst []
where
combine' :: [b] -> [[(b, b)]] -> [(b, b)]
combine' [] [[(b, b)]]
acc = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(b, b)]]
acc
combine' (b
x:[b]
xs) [[(b, b)]]
acc =
let xcomb :: [(b, b)]
xcomb = [ (b
x, b
y) | b
y <- [b]
xs] in
[b] -> [[(b, b)]] -> [(b, b)]
combine' [b]
xs ([(b, b)]
xcombforall a. a -> [a] -> [a]
:[[(b, b)]]
acc)
minProp :: Expr EWord -> Prop
minProp :: Expr 'EWord -> Prop
minProp k :: Expr 'EWord
k@(Keccak Expr 'Buf
_) = Expr 'EWord -> Expr 'EWord -> Prop
PGT Expr 'EWord
k (W256 -> Expr 'EWord
Lit W256
50)
minProp Expr 'EWord
_ = forall a. HasCallStack => String -> a
error String
"Internal error: expected keccak expression"
injProp :: (Expr EWord, Expr EWord) -> Prop
injProp :: (Expr 'EWord, Expr 'EWord) -> Prop
injProp (k1 :: Expr 'EWord
k1@(Keccak Expr 'Buf
b1), k2 :: Expr 'EWord
k2@(Keccak Expr 'Buf
b2)) =
Prop -> Prop -> Prop
POr (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'Buf
b1 Expr 'Buf
b2) (Prop -> Prop
PNeg (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
k1 Expr 'EWord
k2))
injProp (Expr 'EWord, Expr 'EWord)
_ = forall a. HasCallStack => String -> a
error String
"Internal error: expected keccak expression"
keccakAssumptions :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop]
keccakAssumptions :: [Prop] -> [Expr 'Buf] -> [Expr 'Storage] -> [Prop]
keccakAssumptions [Prop]
ps [Expr 'Buf]
bufs [Expr 'Storage]
stores = [Prop]
injectivity forall a. Semigroup a => a -> a -> a
<> [Prop]
minValue
where
(()
_, BuilderState
st) = forall s a. State s a -> s -> (a, s)
runState ([Prop]
-> [Expr 'Buf]
-> [Expr 'Storage]
-> StateT BuilderState Identity ()
findKeccakPropsExprs [Prop]
ps [Expr 'Buf]
bufs [Expr 'Storage]
stores) BuilderState
initState
injectivity :: [Prop]
injectivity = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr 'EWord, Expr 'EWord) -> Prop
injProp forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [(a, a)]
combine (forall a. Set a -> [a]
Set.toList BuilderState
st.keccaks)
minValue :: [Prop]
minValue = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'EWord -> Prop
minProp (forall a. Set a -> [a]
Set.toList BuilderState
st.keccaks)