{-# Language GADTs #-}
{-# Language StandaloneDeriving #-}
{-# Language LambdaCase #-}

module EVM.Fetch where

import Prelude hiding (Word)

import EVM.Types    (Addr, w256, W256, hexText, Word, Buffer(..))
import EVM.Symbolic (litWord)
import EVM          (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external)
import qualified EVM.FeeSchedule as FeeSchedule

import qualified EVM

import Control.Lens hiding ((.=))
import Control.Monad.Reader
import Control.Monad.Trans.Maybe
import Data.SBV.Trans.Control
import qualified Data.SBV.Internals as SBV
import Data.SBV.Trans hiding (Word)
import Data.Aeson
import Data.Aeson.Lens
import Data.ByteString (ByteString)
import Data.Text (Text, unpack, pack)
import Network.Wreq
import Network.Wreq.Session (Session)

import qualified Network.Wreq.Session as Session

-- | Abstract representation of an RPC fetch request
data RpcQuery a where
  QueryCode    :: Addr         -> RpcQuery ByteString
  QueryBlock   ::                 RpcQuery Block
  QueryBalance :: Addr         -> RpcQuery W256
  QueryNonce   :: Addr         -> RpcQuery W256
  QuerySlot    :: Addr -> W256 -> RpcQuery W256
  QueryChainId ::                 RpcQuery W256

data BlockNumber = Latest | BlockNumber W256

deriving instance Show (RpcQuery a)

rpc :: String -> [Value] -> Value
rpc :: String -> [Value] -> Value
rpc method :: String
method args :: [Value]
args = [Pair] -> Value
object
  [ "jsonrpc" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= ("2.0" :: String)
  , "id"      Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Scientific -> Value
Number 1
  , "method"  Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
method
  , "params"  Text -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= [Value]
args
  ]

class ToRPC a where
  toRPC :: a -> Value

instance ToRPC Addr where
  toRPC :: Addr -> Value
toRPC = Text -> Value
String (Text -> Value) -> (Addr -> Text) -> Addr -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Text) -> (Addr -> String) -> Addr -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> String
forall a. Show a => a -> String
show

instance ToRPC W256 where
  toRPC :: W256 -> Value
toRPC = Text -> Value
String (Text -> Value) -> (W256 -> Text) -> W256 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Text) -> (W256 -> String) -> W256 -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> String
forall a. Show a => a -> String
show

instance ToRPC Bool where
  toRPC :: Bool -> Value
toRPC = Bool -> Value
Bool

instance ToRPC BlockNumber where
  toRPC :: BlockNumber -> Value
toRPC Latest          = Text -> Value
String "latest"
  toRPC (BlockNumber n :: W256
n) = Text -> Value
String (Text -> Value) -> (String -> Text) -> String -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ W256 -> String
forall a. Show a => a -> String
show W256
n

readText :: Read a => Text -> a
readText :: Text -> a
readText = String -> a
forall a. Read a => String -> a
read (String -> a) -> (Text -> String) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
unpack

fetchQuery
  :: Show a
  => BlockNumber
  -> (Value -> IO (Maybe Value))
  -> RpcQuery a
  -> IO (Maybe a)
fetchQuery :: BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery n :: BlockNumber
n f :: Value -> IO (Maybe Value)
f q :: RpcQuery a
q = do
  Maybe a
x <- case RpcQuery a
q of
    QueryCode addr :: Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_getCode" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe ByteString -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ByteString -> IO (Maybe a))
-> Maybe ByteString -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
hexText (Text -> ByteString) -> (Value -> Text) -> Value -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> ByteString) -> Maybe Value -> Maybe ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QueryNonce addr :: Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_getTransactionCount" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe a)) -> Maybe W256 -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QueryBlock -> do
      Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_getBlockByNumber" [BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n, Bool -> Value
forall a. ToRPC a => a -> Value
toRPC Bool
False])
      Maybe Block -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Block -> IO (Maybe a)) -> Maybe Block -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Maybe Value
m Maybe Value -> (Value -> Maybe Block) -> Maybe Block
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Maybe Block
forall s. (AsValue s, Show s) => s -> Maybe Block
parseBlock
    QueryBalance addr :: Addr
addr -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_getBalance" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe a)) -> Maybe W256 -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QuerySlot addr :: Addr
addr slot :: W256
slot -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_getStorageAt" [Addr -> Value
forall a. ToRPC a => a -> Value
toRPC Addr
addr, W256 -> Value
forall a. ToRPC a => a -> Value
toRPC W256
slot, BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe a)) -> Maybe W256 -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
    QueryChainId -> do
        Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc "eth_chainId" [BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
        Maybe W256 -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe W256 -> IO (Maybe a)) -> Maybe W256 -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> (Value -> Text) -> Value -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Text Value Text -> Value -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Value Text
forall t. AsPrimitive t => Prism' t Text
_String (Value -> W256) -> Maybe Value -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
  Maybe a -> IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
x


parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block
parseBlock :: s -> Maybe Block
parseBlock j :: s
j = do
  Addr
coinbase   <- Text -> Addr
forall a. Read a => Text -> a
readText (Text -> Addr) -> Maybe Text -> Maybe Addr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key "miner" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  SymWord
timestamp  <- Word -> SymWord
litWord (Word -> SymWord) -> (Text -> Word) -> Text -> SymWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Word
forall a. Read a => Text -> a
readText (Text -> SymWord) -> Maybe Text -> Maybe SymWord
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key "timestamp" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  Word
number     <- Text -> Word
forall a. Read a => Text -> a
readText (Text -> Word) -> Maybe Text -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key "number" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  Word
difficulty <- Text -> Word
forall a. Read a => Text -> a
readText (Text -> Word) -> Maybe Text -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Getting (First Text) s Text -> Maybe Text
forall s a. s -> Getting (First a) s a -> Maybe a
^? Text -> Traversal' s Value
forall t. AsValue t => Text -> Traversal' t Value
key "difficulty" ((Value -> Const (First Text) Value) -> s -> Const (First Text) s)
-> ((Text -> Const (First Text) Text)
    -> Value -> Const (First Text) Value)
-> Getting (First Text) s Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const (First Text) Text)
-> Value -> Const (First Text) Value
forall t. AsPrimitive t => Prism' t Text
_String
  -- default codesize, default gas limit, default feescedule
  Block -> Maybe Block
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> Maybe Block) -> Block -> Maybe Block
forall a b. (a -> b) -> a -> b
$ Addr
-> SymWord
-> Word
-> Word
-> Word
-> Word
-> FeeSchedule Integer
-> Block
EVM.Block Addr
coinbase SymWord
timestamp Word
number Word
difficulty 0xffffffff 0xffffffff FeeSchedule Integer
forall n. Num n => FeeSchedule n
FeeSchedule.berlin

fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession url :: Text
url sess :: Session
sess x :: Value
x = do
  Response Value
r <- Response ByteString -> IO (Response Value)
forall (m :: * -> *).
MonadThrow m =>
Response ByteString -> m (Response Value)
asValue (Response ByteString -> IO (Response Value))
-> IO (Response ByteString) -> IO (Response Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Session -> String -> Value -> IO (Response ByteString)
forall a.
Postable a =>
Session -> String -> a -> IO (Response ByteString)
Session.post Session
sess (Text -> String
unpack Text
url) Value
x
  Maybe Value -> IO (Maybe Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Response Value
r Response Value
-> Getting (First Value) (Response Value) Value -> Maybe Value
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Value) (Response Value) Value
forall body0 body1.
Lens (Response body0) (Response body1) body0 body1
responseBody Getting (First Value) (Response Value) Value
-> ((Value -> Const (First Value) Value)
    -> Value -> Const (First Value) Value)
-> Getting (First Value) (Response Value) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Traversal' Value Value
forall t. AsValue t => Text -> Traversal' t Value
key "result")

fetchContractWithSession
  :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession n :: BlockNumber
n url :: Text
url addr :: Addr
addr sess :: Session
sess = MaybeT IO Contract -> IO (Maybe Contract)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO Contract -> IO (Maybe Contract))
-> MaybeT IO Contract -> IO (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ do
  let
    fetch :: Show a => RpcQuery a -> IO (Maybe a)
    fetch :: RpcQuery a -> IO (Maybe a)
fetch = BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess)

  ByteString
theCode    <- IO (Maybe ByteString) -> MaybeT IO ByteString
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe ByteString) -> MaybeT IO ByteString)
-> IO (Maybe ByteString) -> MaybeT IO ByteString
forall a b. (a -> b) -> a -> b
$ RpcQuery ByteString -> IO (Maybe ByteString)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery ByteString
QueryCode Addr
addr)
  W256
theNonce   <- IO (Maybe W256) -> MaybeT IO W256
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe W256) -> MaybeT IO W256)
-> IO (Maybe W256) -> MaybeT IO W256
forall a b. (a -> b) -> a -> b
$ RpcQuery W256 -> IO (Maybe W256)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryNonce Addr
addr)
  W256
theBalance <- IO (Maybe W256) -> MaybeT IO W256
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe W256) -> MaybeT IO W256)
-> IO (Maybe W256) -> MaybeT IO W256
forall a b. (a -> b) -> a -> b
$ RpcQuery W256 -> IO (Maybe W256)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryBalance Addr
addr)

  Contract -> MaybeT IO Contract
forall (m :: * -> *) a. Monad m => a -> m a
return (Contract -> MaybeT IO Contract) -> Contract -> MaybeT IO Contract
forall a b. (a -> b) -> a -> b
$
    ContractCode -> Contract
initialContract (Buffer -> ContractCode
EVM.RuntimeCode (ByteString -> Buffer
ConcreteBuffer ByteString
theCode))
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Word Word -> Word -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Word Word
Lens' Contract Word
nonce    (W256 -> Word
w256 W256
theNonce)
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Word Word -> Word -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Word Word
Lens' Contract Word
balance  (W256 -> Word
w256 W256
theBalance)
      Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Bool Bool -> Bool -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Bool Bool
Lens' Contract Bool
external Bool
True

fetchSlotWithSession
  :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession n :: BlockNumber
n url :: Text
url sess :: Session
sess addr :: Addr
addr slot :: W256
slot =
  (W256 -> Word) -> Maybe W256 -> Maybe Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap W256 -> Word
w256 (Maybe W256 -> Maybe Word) -> IO (Maybe W256) -> IO (Maybe Word)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery W256 -> IO (Maybe W256)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) (Addr -> W256 -> RpcQuery W256
QuerySlot Addr
addr W256
slot)

fetchBlockWithSession
  :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession :: BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession n :: BlockNumber
n url :: Text
url sess :: Session
sess =
  BlockNumber
-> (Value -> IO (Maybe Value))
-> RpcQuery Block
-> IO (Maybe Block)
forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
n (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) RpcQuery Block
QueryBlock

fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
fetchBlockFrom n :: BlockNumber
n url :: Text
url =
  (Session -> IO (Maybe Block)) -> IO (Maybe Block)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession BlockNumber
n Text
url)

fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom n :: BlockNumber
n url :: Text
url addr :: Addr
addr =
  (Session -> IO (Maybe Contract)) -> IO (Maybe Contract)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession BlockNumber
n Text
url Addr
addr)

fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom n :: BlockNumber
n url :: Text
url addr :: Addr
addr slot :: W256
slot =
  (Session -> IO (Maybe Word)) -> IO (Maybe Word)
forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (\s :: Session
s -> BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
fetchSlotWithSession BlockNumber
n Text
url Session
s Addr
addr W256
slot)

http :: BlockNumber -> Text -> Fetcher
http :: BlockNumber -> Text -> Fetcher
http n :: BlockNumber
n url :: Text
url = Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle Maybe State
forall a. Maybe a
Nothing ((BlockNumber, Text) -> Maybe (BlockNumber, Text)
forall a. a -> Maybe a
Just (BlockNumber
n, Text
url)) Bool
True

zero :: Fetcher
zero :: Fetcher
zero = Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle Maybe State
forall a. Maybe a
Nothing Maybe (BlockNumber, Text)
forall a. Maybe a
Nothing Bool
True

-- smtsolving + (http or zero)
oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle :: Maybe State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher
oracle smtstate :: Maybe State
smtstate info :: Maybe (BlockNumber, Text)
info ensureConsistency :: Bool
ensureConsistency q :: Query
q = do
  case Query
q of
    EVM.PleaseAskSMT branchcondition :: SBool
branchcondition pathconditions :: [SBool]
pathconditions continue :: BranchCondition -> EVM ()
continue ->
      case Maybe State
smtstate of
        Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ BranchCondition -> EVM ()
continue BranchCondition
EVM.Unknown
        Just state :: State
state -> (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
         let pathconds :: SBool
pathconds = [SBool] -> SBool
sAnd [SBool]
pathconditions
         -- Is is possible to satisfy the condition?
         BranchCondition -> EVM ()
continue (BranchCondition -> EVM ())
-> QueryT IO BranchCondition -> QueryT IO (EVM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBool -> SBool -> Bool -> QueryT IO BranchCondition
checkBranch SBool
pathconds SBool
branchcondition Bool
ensureConsistency

    -- if we are using a symbolic storage model,
    -- we generate a new array to the fetched contract here
    EVM.PleaseFetchContract addr :: Addr
addr model :: StorageModel
model continue :: Contract -> EVM ()
continue -> do
      Maybe Contract
contract <- case Maybe (BlockNumber, Text)
info of
                    Nothing -> Maybe Contract -> IO (Maybe Contract)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Contract -> IO (Maybe Contract))
-> Maybe Contract -> IO (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ Contract -> Maybe Contract
forall a. a -> Maybe a
Just (Contract -> Maybe Contract) -> Contract -> Maybe Contract
forall a b. (a -> b) -> a -> b
$ ContractCode -> Contract
initialContract (Buffer -> ContractCode
EVM.RuntimeCode Buffer
forall a. Monoid a => a
mempty)
                    Just (n :: BlockNumber
n, url :: Text
url) -> BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr
      case Maybe Contract
contract of
        Just x :: Contract
x -> case StorageModel
model of
          EVM.ConcreteS -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue Contract
x
          EVM.InitialS  -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
             Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> SArray (WordN 256) (WordN 256) -> Storage
forall a b. (a -> b) -> a -> b
$ WordN 256
-> [(SBV (WordN 256), SBV (WordN 256))]
-> SArray (WordN 256) (WordN 256)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, SymVal b) =>
b -> [(SBV a, SBV b)] -> array a b
SBV.sListArray 0 [])
          EVM.SymbolicS -> case Maybe State
smtstate of
            Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
                               Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] (SArray (WordN 256) (WordN 256) -> Storage)
-> SArray (WordN 256) (WordN 256) -> Storage
forall a b. (a -> b) -> a -> b
$ WordN 256
-> [(SBV (WordN 256), SBV (WordN 256))]
-> SArray (WordN 256) (WordN 256)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, SymVal b) =>
b -> [(SBV a, SBV b)] -> array a b
SBV.sListArray 0 []))

            Just state :: State
state ->
              (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
                SArray (WordN 256) (WordN 256)
store <- Maybe (SBV (WordN 256))
-> QueryT IO (SArray (WordN 256) (WordN 256))
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
freshArray_ Maybe (SBV (WordN 256))
forall a. Maybe a
Nothing
                EVM () -> QueryT IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue (Contract -> EVM ()) -> Contract -> EVM ()
forall a b. (a -> b) -> a -> b
$ Contract
x
                  Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& ASetter Contract Contract Storage Storage
-> Storage -> Contract -> Contract
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Contract Contract Storage Storage
Lens' Contract Storage
EVM.storage ([(SymWord, SymWord)] -> SArray (WordN 256) (WordN 256) -> Storage
EVM.Symbolic [] SArray (WordN 256) (WordN 256)
store)
        Nothing -> String -> IO (EVM ())
forall a. HasCallStack => String -> a
error ("oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query -> String
forall a. Show a => a -> String
show Query
q)

    EVM.PleaseMakeUnique val :: SBV a
val pathconditions :: [SBool]
pathconditions continue :: IsUnique a -> EVM ()
continue ->
          case Maybe State
smtstate of
            Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (EVM () -> IO (EVM ())) -> EVM () -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
Multiple
            Just state :: State
state -> (ReaderT State IO (EVM ()) -> State -> IO (EVM ()))
-> State -> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT State IO (EVM ()) -> State -> IO (EVM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT State
state (ReaderT State IO (EVM ()) -> IO (EVM ()))
-> ReaderT State IO (EVM ()) -> IO (EVM ())
forall a b. (a -> b) -> a -> b
$ QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
SBV.runQueryT (QueryT IO (EVM ()) -> ReaderT State IO (EVM ()))
-> QueryT IO (EVM ()) -> ReaderT State IO (EVM ())
forall a b. (a -> b) -> a -> b
$ do
              SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ [SBool]
pathconditions [SBool] -> [SBool] -> [SBool]
forall a. Semigroup a => a -> a -> a
<> [SBV a
val SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
val] -- dummy proposition just to make sure `val` is defined when we do `getValue` later.
              QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO (EVM ())) -> QueryT IO (EVM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Sat -> do
                  a
val' <- SBV a -> QueryT IO a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SBV a
val
                  CheckSatResult
s    <- SBool -> QueryT IO CheckSatResult
checksat (SBV a
val SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
val')
                  case CheckSatResult
s of
                    Unsat -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue (IsUnique a -> EVM ()) -> IsUnique a -> EVM ()
forall a b. (a -> b) -> a -> b
$ a -> IsUnique a
forall a. a -> IsUnique a
Unique a
val'
                    _ -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
Multiple
                Unsat -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
InconsistentU
                Unk -> EVM () -> QueryT IO (EVM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM () -> QueryT IO (EVM ())) -> EVM () -> QueryT IO (EVM ())
forall a b. (a -> b) -> a -> b
$ IsUnique a -> EVM ()
continue IsUnique a
forall a. IsUnique a
TimeoutU
                DSat _ -> String -> QueryT IO (EVM ())
forall a. HasCallStack => String -> a
error "unexpected DSAT"


    EVM.PleaseFetchSlot addr :: Addr
addr slot :: Word
slot continue :: Word -> EVM ()
continue ->
      case Maybe (BlockNumber, Text)
info of
        Nothing -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Word -> EVM ()
continue 0)
        Just (n :: BlockNumber
n, url :: Text
url) ->
         BlockNumber -> Text -> Addr -> W256 -> IO (Maybe Word)
fetchSlotFrom BlockNumber
n Text
url Addr
addr (Word -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
slot) IO (Maybe Word) -> (Maybe Word -> IO (EVM ())) -> IO (EVM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
           Just x :: Word
x  -> EVM () -> IO (EVM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Word -> EVM ()
continue Word
x)
           Nothing ->
             String -> IO (EVM ())
forall a. HasCallStack => String -> a
error ("oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query -> String
forall a. Show a => a -> String
show Query
q)

type Fetcher = EVM.Query -> IO (EVM ())

checksat :: SBool -> Query CheckSatResult
checksat :: SBool -> QueryT IO CheckSatResult
checksat b :: SBool
b = do Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
                SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
b
                CheckSatResult
m <- QueryT IO CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                Int -> QueryT IO ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
                CheckSatResult -> QueryT IO CheckSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckSatResult
m

-- | Checks which branches are satisfiable, checking the pathconditions for consistency
-- if the third argument is true.
-- When in debug mode, we do not want to be able to navigate to dead paths,
-- but for normal execution paths with inconsistent pathconditions
-- will be pruned anyway.
checkBranch :: SBool -> SBool -> Bool -> Query EVM.BranchCondition
checkBranch :: SBool -> SBool -> Bool -> QueryT IO BranchCondition
checkBranch pathconds :: SBool
pathconds branchcondition :: SBool
branchcondition False = do
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
pathconds
  SBool -> QueryT IO CheckSatResult
checksat SBool
branchcondition QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     -- the condition is unsatisfiable
     Unsat -> -- if pathconditions are consistent then the condition must be false
            BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
     -- Sat means its possible for condition to hold
     Sat -> -- is its negation also possible?
            SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               -- No. The condition must hold
               Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
True
               -- Yes. Both branches possible
               Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               -- Explore both branches in case of timeout
               Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               DSat _ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error "checkBranch: unexpected SMT result"
     -- If the query times out, we simply explore both paths
     Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
     DSat _ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error "checkBranch: unexpected SMT result"

checkBranch pathconds :: SBool
pathconds branchcondition :: SBool
branchcondition True = do
  SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
pathconds
  SBool -> QueryT IO CheckSatResult
checksat SBool
branchcondition QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     -- the condition is unsatisfiable
     Unsat -> -- are the pathconditions even consistent?
              SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                -- No. We are on an inconsistent path.
                Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Inconsistent
                -- Yes. The condition must be false.
                Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
                -- Assume the negated condition is still possible.
                Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
                DSat _ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error "checkBranch: unexpected SMT result"
     -- Sat means its possible for condition to hold
     Sat -> -- is its negation also possible?
            SBool -> QueryT IO CheckSatResult
checksat (SBool -> SBool
sNot SBool
branchcondition) QueryT IO CheckSatResult
-> (CheckSatResult -> QueryT IO BranchCondition)
-> QueryT IO BranchCondition
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               -- No. The condition must hold
               Unsat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return (BranchCondition -> QueryT IO BranchCondition)
-> BranchCondition -> QueryT IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
True
               -- Yes. Both branches possible
               Sat -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               -- Explore both branches in case of timeout
               Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               DSat _ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error "checkBranch: unexpected SMT result"

     -- If the query times out, we simply explore both paths
     Unk -> BranchCondition -> QueryT IO BranchCondition
forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
     DSat _ -> String -> QueryT IO BranchCondition
forall a. HasCallStack => String -> a
error "Internal Error: unexpected SMT result"