{-# LANGUAGE DataKinds #-}
module EVM.Fetch where
import EVM (initialContract, unknownContract)
import EVM.ABI
import EVM.FeeSchedule (feeSchedule)
import EVM.Format (hexText)
import EVM.SMT
import EVM.Solvers
import EVM.Types
import EVM (emptyContract)
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
import Control.Monad.IO.Class
import EVM.Effects
data RpcQuery a where
QueryCode :: Addr -> RpcQuery BS.ByteString
QueryBlock :: RpcQuery Block
QueryBalance :: Addr -> RpcQuery W256
QueryNonce :: Addr -> RpcQuery W64
QuerySlot :: Addr -> W256 -> RpcQuery W256
QueryChainId :: RpcQuery W256
data BlockNumber = Latest | BlockNumber W256
deriving (Int -> BlockNumber -> ShowS
[BlockNumber] -> ShowS
BlockNumber -> String
(Int -> BlockNumber -> ShowS)
-> (BlockNumber -> String)
-> ([BlockNumber] -> ShowS)
-> Show BlockNumber
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BlockNumber -> ShowS
showsPrec :: Int -> BlockNumber -> ShowS
$cshow :: BlockNumber -> String
show :: BlockNumber -> String
$cshowList :: [BlockNumber] -> ShowS
showList :: [BlockNumber] -> ShowS
Show, BlockNumber -> BlockNumber -> Bool
(BlockNumber -> BlockNumber -> Bool)
-> (BlockNumber -> BlockNumber -> Bool) -> Eq BlockNumber
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BlockNumber -> BlockNumber -> Bool
== :: BlockNumber -> BlockNumber -> Bool
$c/= :: BlockNumber -> BlockNumber -> Bool
/= :: BlockNumber -> BlockNumber -> Bool
Eq)
deriving instance Show (RpcQuery a)
type RpcInfo = Maybe (BlockNumber, Text)
rpc :: String -> [Value] -> Value
rpc :: String -> [Value] -> Value
rpc String
method [Value]
args = [Pair] -> Value
object
[ Key
"jsonrpc" Key -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= (String
"2.0" :: String)
, Key
"id" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Scientific -> Value
Number Scientific
1
, Key
"method" Key -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String
method
, Key
"params" Key -> [Value] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= [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 BlockNumber
Latest = Text -> Value
String Text
"latest"
toRPC (EVM.Fetch.BlockNumber 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 :: forall a. Read a => 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 :: 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 (String -> [Value] -> Value
rpc String
"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 a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Maybe Text
t <- Optic' A_Prism NoIx Value Text -> Value -> Maybe Text
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String (Value -> Maybe Text) -> Maybe Value -> Maybe (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
Text -> a
Text -> ByteString
hexText (Text -> a) -> Maybe Text -> Maybe a
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 (String -> [Value] -> Value
rpc String
"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 a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Maybe Text
t <- Optic' A_Prism NoIx Value Text -> Value -> Maybe Text
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String (Value -> Maybe Text) -> Maybe Value -> Maybe (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
Text -> a
forall a. Read a => Text -> a
readText (Text -> a) -> Maybe Text -> Maybe a
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 (String -> [Value] -> Value
rpc String
"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 a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Maybe Value
m Maybe Value -> (Value -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Maybe a
Value -> Maybe Block
forall s. (AsValue s, Show s) => s -> Maybe Block
parseBlock
QueryBalance Addr
addr -> do
Maybe Value
m <- Value -> IO (Maybe Value)
f (String -> [Value] -> Value
rpc String
"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 a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Maybe Text
t <- Optic' A_Prism NoIx Value Text -> Value -> Maybe Text
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String (Value -> Maybe Text) -> Maybe Value -> Maybe (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
Text -> a
forall a. Read a => Text -> a
readText (Text -> a) -> Maybe Text -> Maybe a
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 (String -> [Value] -> Value
rpc String
"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 a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Maybe Text
t <- Optic' A_Prism NoIx Value Text -> Value -> Maybe Text
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String (Value -> Maybe Text) -> Maybe Value -> Maybe (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
Text -> a
forall a. Read a => Text -> a
readText (Text -> a) -> Maybe Text -> Maybe a
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 (String -> [Value] -> Value
rpc String
"eth_chainId" [BlockNumber -> Value
forall a. ToRPC a => a -> Value
toRPC BlockNumber
n])
Maybe a -> IO (Maybe a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO (Maybe a)) -> Maybe a -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Maybe Text
t <- Optic' A_Prism NoIx Value Text -> Value -> Maybe Text
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String (Value -> Maybe Text) -> Maybe Value -> Maybe (Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Value
m
Text -> a
forall a. Read a => Text -> a
readText (Text -> a) -> Maybe Text -> Maybe a
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
Expr 'EAddr
coinbase <- Addr -> Expr 'EAddr
LitAddr (Addr -> Expr 'EAddr) -> (Text -> Addr) -> Text -> Expr 'EAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Addr
forall a. Read a => Text -> a
readText (Text -> Expr 'EAddr) -> Maybe Text -> Maybe (Expr 'EAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"miner" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
Expr 'EWord
timestamp <- W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Text -> W256) -> Text -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> W256
forall a. Read a => Text -> a
readText (Text -> Expr 'EWord) -> Maybe Text -> Maybe (Expr 'EWord)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"timestamp" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
W256
number <- Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> Maybe Text -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"number" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
Word64
gasLimit <- Text -> Word64
forall a. Read a => Text -> a
readText (Text -> Word64) -> Maybe Text -> Maybe Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"gasLimit" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
let
baseFee :: Maybe W256
baseFee = Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> Maybe Text -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"baseFeePerGas" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
mixhash :: Maybe W256
mixhash = Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> Maybe Text -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"mixHash" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
prevRandao :: Maybe W256
prevRandao = Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> Maybe Text -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"prevRandao" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
forall t. AsValue t => Prism' t Text
_String
difficulty :: Maybe W256
difficulty = Text -> W256
forall a. Read a => Text -> a
readText (Text -> W256) -> Maybe Text -> Maybe W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> s
j s -> Optic' An_AffineTraversal NoIx s Text -> Maybe Text
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? Key -> AffineTraversal' s Value
forall t. AsValue t => Key -> AffineTraversal' t Value
key Key
"difficulty" AffineTraversal' s Value
-> Optic' A_Prism NoIx Value Text
-> Optic' An_AffineTraversal NoIx s Text
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
% Optic' A_Prism NoIx Value Text
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)
_ -> String -> W256
forall a. HasCallStack => String -> a
internalError String
"block contains both difficulty and prevRandao"
Block -> Maybe Block
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Block -> Maybe Block) -> Block -> Maybe Block
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr
-> Expr 'EWord
-> W256
-> W256
-> Word64
-> W256
-> W256
-> FeeSchedule Word64
-> Block
Block Expr 'EAddr
coinbase Expr 'EWord
timestamp W256
number W256
prd Word64
gasLimit (W256 -> Maybe W256 -> W256
forall a. a -> Maybe a -> a
fromMaybe W256
0 Maybe W256
baseFee) W256
0xffffffff FeeSchedule Word64
forall n. Num n => FeeSchedule n
feeSchedule
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 <- 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 a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Response Value
r Response Value
-> Optic' An_AffineTraversal NoIx (Response Value) Value
-> Maybe Value
forall k s (is :: IxList) a.
Is k An_AffineFold =>
s -> Optic' k is s a -> Maybe a
^? (LensVL (Response Value) (Response Value) Value Value
-> Lens (Response Value) (Response Value) Value Value
forall s t a b. LensVL s t a b -> Lens s t a b
lensVL (Value -> f Value) -> Response Value -> f (Response Value)
forall body0 body1 (f :: * -> *).
Functor f =>
(body0 -> f body1) -> Response body0 -> f (Response body1)
LensVL (Response Value) (Response Value) Value Value
responseBody) Lens (Response Value) (Response Value) Value Value
-> Optic An_AffineTraversal NoIx Value Value Value Value
-> Optic' An_AffineTraversal NoIx (Response Value) Value
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
% Key -> Optic An_AffineTraversal NoIx Value Value Value Value
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 = 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 :: forall a. Show a => 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
code <- 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)
W64
nonce <- IO (Maybe W64) -> MaybeT IO W64
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe W64) -> MaybeT IO W64)
-> IO (Maybe W64) -> MaybeT IO W64
forall a b. (a -> b) -> a -> b
$ RpcQuery W64 -> IO (Maybe W64)
forall a. Show a => RpcQuery a -> IO (Maybe a)
fetch (Addr -> RpcQuery W64
QueryNonce Addr
addr)
W256
balance <- 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 a. a -> MaybeT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Contract -> MaybeT IO Contract) -> Contract -> MaybeT IO Contract
forall a b. (a -> b) -> a -> b
$
ContractCode -> Contract
initialContract (RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
code))
Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx Contract Contract (Maybe W64) (Maybe W64)
-> Maybe W64 -> Contract -> Contract
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic A_Lens NoIx Contract Contract (Maybe W64) (Maybe W64)
#nonce (W64 -> Maybe W64
forall a. a -> Maybe a
Just W64
nonce)
Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx Contract Contract (Expr 'EWord) (Expr 'EWord)
-> Expr 'EWord -> Contract -> Contract
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic A_Lens NoIx Contract Contract (Expr 'EWord) (Expr 'EWord)
#balance (W256 -> Expr 'EWord
Lit W256
balance)
Contract -> (Contract -> Contract) -> Contract
forall a b. a -> (a -> b) -> b
& Optic A_Lens NoIx Contract Contract Bool Bool
-> Bool -> Contract -> Contract
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic A_Lens NoIx Contract Contract Bool 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 =
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 BlockNumber
n Text
url 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 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
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
Latest (Text -> Session -> Value -> IO (Maybe Value)
fetchWithSession Text
url Session
sess) RpcQuery W256
QueryChainId
http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
http :: forall (t :: VMType) (m :: * -> *) s.
Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
http Natural
smtjobs Maybe Natural
smttimeout BlockNumber
n Text
url Query t s
q =
Solver
-> Natural
-> Maybe Natural
-> (SolverGroup -> m (EVM t s ()))
-> m (EVM t s ())
forall (m :: * -> *) a.
App m =>
Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
withSolvers Solver
Z3 Natural
smtjobs Maybe Natural
smttimeout ((SolverGroup -> m (EVM t s ())) -> m (EVM t s ()))
-> (SolverGroup -> m (EVM t s ())) -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$ \SolverGroup
s ->
SolverGroup -> RpcInfo -> Fetcher t m s
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
oracle SolverGroup
s ((BlockNumber, Text) -> RpcInfo
forall a. a -> Maybe a
Just (BlockNumber
n, Text
url)) Query t s
q
zero :: Natural -> Maybe Natural -> Fetcher t m s
zero :: forall (t :: VMType) (m :: * -> *) s.
Natural -> Maybe Natural -> Fetcher t m s
zero Natural
smtjobs Maybe Natural
smttimeout Query t s
q =
Solver
-> Natural
-> Maybe Natural
-> (SolverGroup -> m (EVM t s ()))
-> m (EVM t s ())
forall (m :: * -> *) a.
App m =>
Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
withSolvers Solver
Z3 Natural
smtjobs Maybe Natural
smttimeout ((SolverGroup -> m (EVM t s ())) -> m (EVM t s ()))
-> (SolverGroup -> m (EVM t s ())) -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$ \SolverGroup
s ->
SolverGroup -> RpcInfo -> Fetcher t m s
forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
oracle SolverGroup
s RpcInfo
forall a. Maybe a
Nothing Query t s
q
oracle :: SolverGroup -> RpcInfo -> Fetcher t m s
oracle :: forall (t :: VMType) (m :: * -> *) s.
SolverGroup -> RpcInfo -> Fetcher t m s
oracle SolverGroup
solvers RpcInfo
info Query t s
q = do
case Query t s
q of
PleaseDoFFI [String]
vals ByteString -> EVM t s ()
continue -> case [String]
vals of
String
cmd : [String]
args -> do
(ExitCode
_, String
stdout', String
_) <- IO (ExitCode, String, String) -> m (ExitCode, String, String)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ExitCode, String, String) -> m (ExitCode, String, String))
-> IO (ExitCode, String, String) -> m (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
cmd [String]
args String
""
EVM t s () -> m (EVM t s ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM t s () -> m (EVM t s ()))
-> (AbiValue -> EVM t s ()) -> AbiValue -> m (EVM t s ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> EVM t s ()
continue (ByteString -> EVM t s ())
-> (AbiValue -> ByteString) -> AbiValue -> EVM t s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbiValue -> ByteString
encodeAbiValue (AbiValue -> m (EVM t s ())) -> AbiValue -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$
Vector AbiValue -> AbiValue
AbiTuple ([AbiValue] -> Vector AbiValue
forall a. [a] -> Vector a
RegularVector.fromList [ ByteString -> AbiValue
AbiBytesDynamic (ByteString -> AbiValue)
-> (String -> ByteString) -> String -> AbiValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ByteString
hexText (Text -> ByteString) -> (String -> Text) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack (String -> AbiValue) -> String -> AbiValue
forall a b. (a -> b) -> a -> b
$ String
stdout'])
[String]
_ -> String -> m (EVM t s ())
forall a. HasCallStack => String -> a
internalError ([String] -> String
forall a. Show a => a -> String
show [String]
vals)
PleaseAskSMT Expr 'EWord
branchcondition [Prop]
pathconditions BranchCondition -> EVM 'Symbolic s ()
continue -> do
let pathconds :: Prop
pathconds = (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall b a. (b -> a -> b) -> b -> [a] -> b
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 t s ()
BranchCondition -> EVM 'Symbolic s ()
continue (BranchCondition -> EVM t s ())
-> m BranchCondition -> m (EVM t s ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverGroup -> Prop -> Prop -> m BranchCondition
forall (m :: * -> *).
App m =>
SolverGroup -> Prop -> Prop -> m BranchCondition
checkBranch SolverGroup
solvers (Expr 'EWord
branchcondition Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= (W256 -> Expr 'EWord
Lit W256
0)) Prop
pathconds
PleaseFetchContract Addr
addr BaseState
base Contract -> EVM t s ()
continue -> do
Maybe Contract
contract <- case RpcInfo
info of
RpcInfo
Nothing -> let
c :: Contract
c = case BaseState
base of
BaseState
AbstractBase -> Expr 'EAddr -> Contract
unknownContract (Addr -> Expr 'EAddr
LitAddr Addr
addr)
BaseState
EmptyBase -> Contract
emptyContract
in Maybe Contract -> m (Maybe Contract)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Contract -> m (Maybe Contract))
-> Maybe Contract -> m (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ Contract -> Maybe Contract
forall a. a -> Maybe a
Just Contract
c
Just (BlockNumber
n, Text
url) -> IO (Maybe Contract) -> m (Maybe Contract)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Contract) -> m (Maybe Contract))
-> IO (Maybe Contract) -> m (Maybe Contract)
forall a b. (a -> b) -> a -> b
$ BlockNumber -> Text -> Addr -> IO (Maybe Contract)
fetchContractFrom BlockNumber
n Text
url Addr
addr
case Maybe Contract
contract of
Just Contract
x -> EVM t s () -> m (EVM t s ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EVM t s () -> m (EVM t s ())) -> EVM t s () -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$ Contract -> EVM t s ()
continue Contract
x
Maybe Contract
Nothing -> String -> m (EVM t s ())
forall a. HasCallStack => String -> a
internalError (String -> m (EVM t s ())) -> String -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$ String
"oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query t s -> String
forall a. Show a => a -> String
show Query t s
q
PleaseFetchSlot Addr
addr W256
slot W256 -> EVM t s ()
continue ->
case RpcInfo
info of
RpcInfo
Nothing -> EVM t s () -> m (EVM t s ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> EVM t s ()
continue W256
0)
Just (BlockNumber
n, Text
url) ->
IO (EVM t s ()) -> m (EVM t s ())
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (EVM t s ()) -> m (EVM t s ()))
-> IO (EVM t s ()) -> m (EVM t s ())
forall a b. (a -> b) -> a -> b
$ BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
fetchSlotFrom BlockNumber
n Text
url Addr
addr W256
slot IO (Maybe W256)
-> (Maybe W256 -> IO (EVM t s ())) -> IO (EVM t s ())
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just W256
x -> EVM t s () -> IO (EVM t s ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> EVM t s ()
continue W256
x)
Maybe W256
Nothing ->
String -> IO (EVM t s ())
forall a. HasCallStack => String -> a
internalError (String -> IO (EVM t s ())) -> String -> IO (EVM t s ())
forall a b. (a -> b) -> a -> b
$ String
"oracle error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Query t s -> String
forall a. Show a => a -> String
show Query t s
q
type Fetcher t m s = App m => Query t s -> m (EVM t s ())
checkBranch :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition
checkBranch :: forall (m :: * -> *).
App m =>
SolverGroup -> Prop -> Prop -> m BranchCondition
checkBranch SolverGroup
solvers Prop
branchcondition Prop
pathconditions = do
Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
IO BranchCondition -> m BranchCondition
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO BranchCondition -> m BranchCondition)
-> IO BranchCondition -> m BranchCondition
forall a b. (a -> b) -> a -> b
$ SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers (Config -> [Prop] -> SMT2
assertProps Config
conf [(Prop
branchcondition Prop -> Prop -> Prop
.&& Prop
pathconditions)]) IO CheckSatResult
-> (CheckSatResult -> IO BranchCondition) -> IO BranchCondition
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
CheckSatResult
Unsat ->
BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BranchCondition -> IO BranchCondition)
-> BranchCondition -> IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
Case Bool
False
Sat SMTCex
_ -> do
SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
solvers (Config -> [Prop] -> SMT2
assertProps Config
conf [(Prop
pathconditions Prop -> Prop -> Prop
.&& (Prop -> Prop
PNeg Prop
branchcondition))]) IO CheckSatResult
-> (CheckSatResult -> IO BranchCondition) -> IO BranchCondition
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
CheckSatResult
Unsat -> BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BranchCondition -> IO BranchCondition)
-> BranchCondition -> IO BranchCondition
forall a b. (a -> b) -> a -> b
$ Bool -> BranchCondition
Case Bool
True
Sat SMTCex
_ -> BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
CheckSatResult
EVM.Solvers.Unknown -> BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
Error Text
e -> String -> IO BranchCondition
forall a. HasCallStack => String -> a
internalError (String -> IO BranchCondition) -> String -> IO BranchCondition
forall a b. (a -> b) -> a -> b
$ String
"SMT Solver pureed with an error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
e
CheckSatResult
EVM.Solvers.Unknown -> BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
Error Text
e -> String -> IO BranchCondition
forall a. HasCallStack => String -> a
internalError (String -> IO BranchCondition) -> String -> IO BranchCondition
forall a b. (a -> b) -> a -> b
$ String
"SMT Solver pureed with an error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
e