{-# Language GADTs #-}
{-# Language DataKinds #-}

module EVM.Fetch where

import Prelude hiding (Word)

import EVM.ABI
import EVM.Types    (Addr, W256, hexText, Expr(Lit), Expr(..), Prop(..), (.&&), (./=))
import EVM.SMT
import EVM.Solvers
import EVM          (EVM, Contract, Block, initialContract, nonce, balance, external)
import qualified EVM.FeeSchedule as FeeSchedule

import qualified EVM

import Control.Lens hiding ((.=))
import Control.Monad.Trans.Maybe
import Data.Aeson hiding (Error)
import Data.Aeson.Lens
import qualified Data.ByteString as BS
import Data.Text (Text, unpack, pack)
import Data.Maybe (fromMaybe)
import Data.List (foldl')
import qualified Data.Text as T

import qualified Data.Vector as RegularVector
import Network.Wreq
import Network.Wreq.Session (Session)
import System.Process

import qualified Network.Wreq.Session as Session
import Numeric.Natural (Natural)

-- | Abstract representation of an RPC fetch request
data RpcQuery a where
  QueryCode    :: Addr         -> RpcQuery BS.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 (Int -> BlockNumber -> ShowS
[BlockNumber] -> ShowS
BlockNumber -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [BlockNumber] -> ShowS
$cshowList :: [BlockNumber] -> ShowS
show :: BlockNumber -> [Char]
$cshow :: BlockNumber -> [Char]
showsPrec :: Int -> BlockNumber -> ShowS
$cshowsPrec :: Int -> BlockNumber -> ShowS
Show, BlockNumber -> BlockNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BlockNumber -> BlockNumber -> Bool
$c/= :: BlockNumber -> BlockNumber -> Bool
== :: BlockNumber -> BlockNumber -> Bool
$c== :: BlockNumber -> BlockNumber -> Bool
Eq)

deriving instance Show (RpcQuery a)

type RpcInfo = Maybe (BlockNumber, Text)

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

class ToRPC a where
  toRPC :: a -> Value

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

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

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

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

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

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


parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block
parseBlock :: forall s. (AsValue s, Show s) => s -> Maybe Block
parseBlock s
j = do
  Addr
coinbase   <- forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"miner" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
  Expr 'EWord
timestamp  <- W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"timestamp" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
  W256
number     <- forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"number" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
  Word64
gasLimit   <- forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"gasLimit" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
  let
   baseFee :: Maybe W256
baseFee = forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"baseFeePerGas" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
   -- It seems unclear as to whether this field should still be called mixHash or renamed to prevRandao
   -- According to https://github.com/ethereum/EIPs/blob/master/EIPS/eip-4399.md it should be renamed
   -- but alchemy is still returning mixHash
   mixhash :: Maybe W256
mixhash = forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"mixHash" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
   prevRandao :: Maybe W256
prevRandao = forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"prevRandao" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
   difficulty :: Maybe W256
difficulty = forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j forall s a. s -> Getting (First a) s a -> Maybe a
^? forall t. AsValue t => Key -> Traversal' t Value
key Key
"difficulty" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. AsValue t => Prism' t Text
_String
   prd :: W256
prd = case (Maybe W256
prevRandao, Maybe W256
mixhash, Maybe W256
difficulty) of
     (Just W256
p, Maybe W256
_, Maybe W256
_) -> W256
p
     (Maybe W256
Nothing, Just W256
mh, Just W256
0x0) -> W256
mh
     (Maybe W256
Nothing, Just W256
_, Just W256
d) -> W256
d
     (Maybe W256, Maybe W256, Maybe W256)
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: block contains both difficulty and prevRandao"
  -- default codesize, default gas limit, default feescedule
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Addr
-> Expr 'EWord
-> W256
-> W256
-> Word64
-> W256
-> W256
-> FeeSchedule Word64
-> Block
EVM.Block Addr
coinbase Expr 'EWord
timestamp W256
number W256
prd Word64
gasLimit (forall a. a -> Maybe a -> a
fromMaybe W256
0 Maybe W256
baseFee) W256
0xffffffff forall n. Num n => FeeSchedule n
FeeSchedule.berlin

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

fetchContractWithSession
  :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession BlockNumber
n Text
url Addr
addr Session
sess = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
  let
    fetch :: Show a => RpcQuery a -> IO (Maybe a)
    fetch :: forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch = 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    <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery ByteString
QueryCode Addr
addr)
  W256
theNonce   <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryNonce Addr
addr)
  W256
theBalance <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W256
QueryBalance Addr
addr)

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

fetchSlotWithSession
  :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchSlotWithSession BlockNumber
n Text
url Session
sess Addr
addr W256
slot =
  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 BlockNumber
n Text
url Session
sess =
  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 BlockNumber
n Text
url =
  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 BlockNumber
n Text
url Addr
addr =
  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 W256)
fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
fetchSlotFrom BlockNumber
n Text
url Addr
addr W256
slot =
  forall a. (Session -> IO a) -> IO a
Session.withAPISession
    (\Session
s -> BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchSlotWithSession BlockNumber
n Text
url Session
s Addr
addr W256
slot)

http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher
http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher
http Natural
smtjobs Maybe Natural
smttimeout BlockNumber
n Text
url Query
q =
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
smtjobs Maybe Natural
smttimeout forall a b. (a -> b) -> a -> b
$ \SolverGroup
s ->
    SolverGroup -> RpcInfo -> Fetcher
oracle SolverGroup
s (forall a. a -> Maybe a
Just (BlockNumber
n, Text
url)) Query
q

zero :: Natural -> Maybe Natural -> Fetcher
zero :: Natural -> Maybe Natural -> Fetcher
zero Natural
smtjobs Maybe Natural
smttimeout Query
q =
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
smtjobs Maybe Natural
smttimeout forall a b. (a -> b) -> a -> b
$ \SolverGroup
s ->
    SolverGroup -> RpcInfo -> Fetcher
oracle SolverGroup
s forall a. Maybe a
Nothing Query
q

-- smtsolving + (http or zero)
oracle :: SolverGroup -> RpcInfo -> Fetcher
oracle :: SolverGroup -> RpcInfo -> Fetcher
oracle SolverGroup
solvers RpcInfo
info Query
q = do
  case Query
q of
    EVM.PleaseDoFFI [[Char]]
vals ByteString -> EVM ()
continue -> case [[Char]]
vals of
       [Char]
cmd : [[Char]]
args -> do
          (ExitCode
_, [Char]
stdout', [Char]
_) <- [Char] -> [[Char]] -> [Char] -> IO (ExitCode, [Char], [Char])
readProcessWithExitCode [Char]
cmd [[Char]]
args [Char]
""
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> EVM ()
continue forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbiValue -> ByteString
encodeAbiValue forall a b. (a -> b) -> a -> b
$
            Vector AbiValue -> AbiValue
AbiTuple (forall a. [a] -> Vector a
RegularVector.fromList [ ByteString -> AbiValue
AbiBytesDynamic forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ByteString
hexText forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
pack forall a b. (a -> b) -> a -> b
$ [Char]
stdout'])
       [[Char]]
_ -> forall a. HasCallStack => [Char] -> a
error (forall a. Show a => a -> [Char]
show [[Char]]
vals)

    EVM.PleaseAskSMT Expr 'EWord
branchcondition [Prop]
pathconditions BranchCondition -> EVM ()
continue -> do
         let pathconds :: Prop
pathconds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True) [Prop]
pathconditions
         -- Is is possible to satisfy the condition?
         BranchCondition -> EVM ()
continue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverGroup -> Prop -> Prop -> IO BranchCondition
checkBranch SolverGroup
solvers (Expr 'EWord
branchcondition forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= (W256 -> Expr 'EWord
Lit W256
0)) Prop
pathconds

    -- if we are using a symbolic storage model,
    -- we generate a new array to the fetched contract here
    EVM.PleaseFetchContract Addr
addr Contract -> EVM ()
continue -> do
      Maybe Contract
contract <- case RpcInfo
info of
                    RpcInfo
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ContractCode -> Contract
initialContract (RuntimeCode -> ContractCode
EVM.RuntimeCode (ByteString -> RuntimeCode
EVM.ConcreteRuntimeCode ByteString
""))
                    Just (BlockNumber
n, Text
url) -> BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr
      case Maybe Contract
contract of
        Just Contract
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue Contract
x
        Maybe Contract
Nothing -> forall a. HasCallStack => [Char] -> a
error ([Char]
"oracle error: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Query
q)

    --EVM.PleaseMakeUnique val pathconditions continue ->
          --case smtstate of
            --Nothing -> return $ continue Multiple
            --Just state -> flip runReaderT state $ SBV.runQueryT $ do
              --constrain $ sAnd $ pathconditions <> [val .== val] -- dummy proposition just to make sure `val` is defined when we do `getValue` later.
              --checkSat >>= \case
                --Sat -> do
                  --val' <- getValue val
                  --s    <- checksat (val ./= literal val')
                  --case s of
                    --Unsat -> pure $ continue $ Unique val'
                    --_ -> pure $ continue Multiple
                --Unsat -> pure $ continue InconsistentU
                --Unk -> pure $ continue TimeoutU
                --DSat _ -> error "unexpected DSAT"


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

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

-- | 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 :: SolverGroup -> Prop -> Prop -> IO EVM.BranchCondition
checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
checkBranch SolverGroup
solvers Prop
branchcondition Prop
pathconditions = do
  SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers ([Prop] -> SMT2
assertProps [(Prop
branchcondition Prop -> Prop -> Prop
.&& Prop
pathconditions)]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     -- the condition is unsatisfiable
     CheckSatResult
Unsat -> -- if pathconditions are consistent then the condition must be false
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
False
     -- Sat means its possible for condition to hold
     Sat SMTCex
_ -> -- is its negation also possible?
            SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers ([Prop] -> SMT2
assertProps [(Prop
pathconditions Prop -> Prop -> Prop
.&& (Prop -> Prop
PNeg Prop
branchcondition))]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               -- No. The condition must hold
               CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
EVM.Case Bool
True
               -- Yes. Both branches possible
               Sat SMTCex
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               -- Explore both branches in case of timeout
               CheckSatResult
Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
               Error Text
e -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: SMT Solver returned with an error: " forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack Text
e
     -- If the query times out, we simply explore both paths
     CheckSatResult
Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Unknown
     Error Text
e -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: SMT Solver returned with an error: " forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack Text
e