{-# LANGUAGE DataKinds #-}

module EVM.Fetch where

import EVM (initialContract)
import EVM.ABI
import EVM.FeeSchedule qualified as FeeSchedule
import EVM.Format (hexText)
import EVM.SMT
import EVM.Solvers
import EVM.Types

import Optics.Core

import Control.Monad.Trans.Maybe
import Data.Aeson hiding (Error)
import Data.Aeson.Optics
import Data.ByteString qualified as BS
import Data.Text (Text, unpack, pack)
import Data.Maybe (fromMaybe)
import Data.List (foldl')
import Data.Text qualified as T
import Data.Vector qualified as RegularVector
import Network.Wreq
import Network.Wreq.Session (Session)
import Network.Wreq.Session qualified as Session
import Numeric.Natural (Natural)
import System.Process

-- | 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 =
  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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
          Maybe Text
t <- forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview forall t. AsValue t => Prism' t Text
_String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
          Text -> ByteString
hexText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
t
    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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
          Maybe Text
t <- forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview forall t. AsValue t => Prism' t Text
_String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
          forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
t
    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 (f :: * -> *) a. Applicative f => a -> f a
pure 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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
          Maybe Text
t <- forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview forall t. AsValue t => Prism' t Text
_String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
          forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
t
    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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
          Maybe Text
t <- forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview forall t. AsValue t => Prism' t Text
_String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
          forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
t
    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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
          Maybe Text
t <- forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview forall t. AsValue t => Prism' t Text
_String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
          forall a. Read a => Text -> a
readText forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Text
t

parseBlock :: (AsValue s, Show s) => s -> Maybe 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"miner" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"timestamp" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"number" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"gasLimit" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"baseFeePerGas" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"mixHash" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"prevRandao" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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 k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"difficulty" forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% 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
internalError [Char]
"block contains both difficulty and prevRandao"
  -- default codesize, default gas limit, default feescedule
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Addr
-> Expr 'EWord
-> W256
-> W256
-> Word64
-> W256
-> W256
-> FeeSchedule Word64
-> Block
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 (f :: * -> *) a. Applicative f => a -> f a
pure (Response Value
r forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? (forall s t a b. LensVL s t a b -> Lens s t a b
lensVL forall body0 body1.
Lens (Response body0) (Response body1) body0 body1
responseBody) forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% forall t. AsValue t => Key -> AffineTraversal' 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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    ContractCode -> Contract
initialContract (RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
theCode))
      forall a b. a -> (a -> b) -> b
& forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set forall a. IsLabel "nonce" a => a
#nonce    W256
theNonce
      forall a b. a -> (a -> b) -> b
& forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set forall a. IsLabel "balance" a => a
#balance  W256
theBalance
      forall a b. a -> (a -> b) -> b
& forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set forall a. IsLabel "external" a => a
#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 = do
  Session
sess <- IO Session
Session.newAPISession
  BlockNumber -> Text -> Session -> IO (Maybe Block)
fetchBlockWithSession BlockNumber
n Text
url Session
sess

fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr = do
  Session
sess <- IO Session
Session.newAPISession
  BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
fetchContractWithSession BlockNumber
n Text
url Addr
addr Session
sess

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 = do
  Session
sess <- IO Session
Session.newAPISession
  BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
fetchSlotWithSession BlockNumber
n Text
url Session
sess Addr
addr W256
slot

fetchChainIdFrom :: Text -> IO (Maybe W256)
fetchChainIdFrom :: Text -> IO (Maybe W256)
fetchChainIdFrom Text
url = do
  Session
sess <- IO Session
Session.newAPISession
  forall a.
Show a =>
BlockNumber
-> (Value -> IO (Maybe Value)) -> RpcQuery a -> IO (Maybe a)
fetchQuery BlockNumber
Latest (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) RpcQuery W256
QueryChainId

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
    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
internalError (forall a. Show a => a -> [Char]
show [[Char]]
vals)

    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
    PleaseFetchContract Addr
addr Contract -> EVM ()
continue -> do
      Maybe Contract
contract <- case RpcInfo
info of
                    RpcInfo
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
RuntimeCode (ByteString -> RuntimeCode
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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Contract -> EVM ()
continue Contract
x
        Maybe Contract
Nothing -> forall a. HasCallStack => [Char] -> a
internalError forall a b. (a -> b) -> a -> b
$ [Char]
"oracle error: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Query
q

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

type Fetcher = 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 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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
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 (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
Case Bool
True
        -- Yes. Both branches possible
        Sat SMTCex
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
        -- Explore both branches in case of timeout
        CheckSatResult
EVM.Solvers.Unknown -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
        Error Text
e -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: SMT Solver pureed 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
EVM.Solvers.Unknown -> forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
    Error Text
e -> forall a. HasCallStack => [Char] -> a
internalError forall a b. (a -> b) -> a -> b
$ [Char]
"SMT Solver pureed with an error: " forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack Text
e