{-# Language GADTs #-}
{-# Language DataKinds #-}
module EVM.Fetch where
import Prelude hiding (Word)
import EVM.ABI
import EVM.SMT
import EVM.Solvers
import EVM.Types
import EVM.Format (hexText)
import EVM (initialContract)
import qualified EVM.FeeSchedule as FeeSchedule
import Optics.Core
import Control.Monad.Trans.Maybe
import Data.Aeson hiding (Error)
import Data.Aeson.Optics
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)
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 (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 (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 (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
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
x
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
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
error [Char]
"Internal Error: block contains both difficulty and prevRandao"
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
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 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 (m :: * -> *) a. Monad m => a -> m a
return 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
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
error (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
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
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
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 (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)
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 = Query -> IO (EVM ())
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
CheckSatResult
Unsat ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
Case Bool
False
Sat SMTCex
_ ->
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
CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
Case Bool
True
Sat SMTCex
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return BranchCondition
EVM.Types.Unknown
CheckSatResult
EVM.Solvers.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 returned with an error: " forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack Text
e
CheckSatResult
EVM.Solvers.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 returned with an error: " forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
T.unpack Text
e