{-# LANGUAGE DataKinds #-}
{- |
    Module: EVM.Keccak
    Description: Expr passes to determine Keccak assumptions
-}

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"

-- Takes a list of props, find all keccak occurences and generates two kinds of assumptions:
--   1. Minimum output value: That the output of the invocation is greater than
--      50 (needed to avoid spurious counterexamples due to storage collisions
--      with solidity mappings & value type storage slots)
--   2. Injectivity: That keccak is an injective function (we avoid quantifiers
--      here by making this claim for each unique pair of keccak invocations
--      discovered in the input expressions)
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)