{-# 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

-- | 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 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
   -- 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 = 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"
  -- default codesize, default gas limit, default feescedule
  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

-- smtsolving + (http or zero)
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
         -- Is is possible to satisfy the condition?
         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 ())

-- | 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 :: 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
    -- the condition is unsatisfiable
    CheckSatResult
Unsat -> -- if pathconditions are consistent then the condition must be false
      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 means its possible for condition to hold
    Sat SMTCex
_ -> do -- is its negation also possible?
      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
        -- No. The condition must hold
        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
        -- Yes. Both branches possible
        Sat SMTCex
_ -> BranchCondition -> IO BranchCondition
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BranchCondition
EVM.Types.Unknown
        -- Explore both branches in case of timeout
        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
    -- If the query times out, we simply explore both paths
    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