{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module EVM.Stepper
( Action (..)
, Stepper
, exec
, execFully
, run
, runFully
, wait
, ask
, evm
, evmIO
, enter
, interpret
)
where
import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view)
import Control.Monad.State.Strict (execStateT, runStateT, get)
import Data.Text (Text)
import EVM qualified
import EVM.Exec qualified
import EVM.Fetch qualified as Fetch
import EVM.Types
import Control.Monad.ST (stToIO, RealWorld)
import Control.Monad.IO.Class
import EVM.Effects
data Action t s a where
Exec :: Action t s (VMResult t s)
Wait :: Query t s -> Action t s ()
Ask :: Choose s -> Action Symbolic s ()
EVM :: EVM t s a -> Action t s a
IOAct :: IO a -> Action t s a
type Stepper t s a = Program (Action t s) a
exec :: Stepper t s (VMResult t s)
exec :: forall (t :: VMType) s. Stepper t s (VMResult t s)
exec = Action t s (VMResult t s)
-> ProgramT (Action t s) Identity (VMResult t s)
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action t s (VMResult t s)
forall (t :: VMType) s. Action t s (VMResult t s)
Exec
run :: Stepper t s (VM t s)
run :: forall (t :: VMType) s. Stepper t s (VM t s)
run = Stepper t s (VMResult t s)
forall (t :: VMType) s. Stepper t s (VMResult t s)
exec Stepper t s (VMResult t s)
-> ProgramT (Action t s) Identity (VM t s)
-> ProgramT (Action t s) Identity (VM t s)
forall a b.
ProgramT (Action t s) Identity a
-> ProgramT (Action t s) Identity b
-> ProgramT (Action t s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> EVM t s (VM t s) -> ProgramT (Action t s) Identity (VM t s)
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
evm EVM t s (VM t s)
forall s (m :: * -> *). MonadState s m => m s
get
wait :: Query t s -> Stepper t s ()
wait :: forall (t :: VMType) s. Query t s -> Stepper t s ()
wait = Action t s () -> ProgramT (Action t s) Identity ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action t s () -> ProgramT (Action t s) Identity ())
-> (Query t s -> Action t s ())
-> Query t s
-> ProgramT (Action t s) Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Query t s -> Action t s ()
forall (t :: VMType) s. Query t s -> Action t s ()
Wait
ask :: Choose s -> Stepper Symbolic s ()
ask :: forall s. Choose s -> Stepper 'Symbolic s ()
ask = Action 'Symbolic s () -> ProgramT (Action 'Symbolic s) Identity ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action 'Symbolic s ()
-> ProgramT (Action 'Symbolic s) Identity ())
-> (Choose s -> Action 'Symbolic s ())
-> Choose s
-> ProgramT (Action 'Symbolic s) Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Choose s -> Action 'Symbolic s ()
forall s. Choose s -> Action 'Symbolic s ()
Ask
evm :: EVM t s a -> Stepper t s a
evm :: forall (t :: VMType) s a. EVM t s a -> Stepper t s a
evm = Action t s a -> ProgramT (Action t s) Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action t s a -> ProgramT (Action t s) Identity a)
-> (EVM t s a -> Action t s a)
-> EVM t s a
-> ProgramT (Action t s) Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EVM t s a -> Action t s a
forall (t :: VMType) s a. EVM t s a -> Action t s a
EVM
evmIO :: IO a -> Stepper t s a
evmIO :: forall a (t :: VMType) s. IO a -> Stepper t s a
evmIO = Action t s a -> ProgramT (Action t s) Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action t s a -> ProgramT (Action t s) Identity a)
-> (IO a -> Action t s a)
-> IO a
-> ProgramT (Action t s) Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> Action t s a
forall a (t :: VMType) s. IO a -> Action t s a
IOAct
execFully :: Stepper Concrete s (Either EvmError (Expr Buf))
execFully :: forall s. Stepper 'Concrete s (Either EvmError (Expr 'Buf))
execFully =
Stepper 'Concrete s (VMResult 'Concrete s)
forall (t :: VMType) s. Stepper t s (VMResult t s)
exec Stepper 'Concrete s (VMResult 'Concrete s)
-> (VMResult 'Concrete s
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf)))
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall a b.
ProgramT (Action 'Concrete s) Identity a
-> (a -> ProgramT (Action 'Concrete s) Identity b)
-> ProgramT (Action 'Concrete s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
HandleEffect (Query Query 'Concrete s
q) ->
Query 'Concrete s -> Stepper 'Concrete s ()
forall (t :: VMType) s. Query t s -> Stepper t s ()
wait Query 'Concrete s
q Stepper 'Concrete s ()
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall a b.
ProgramT (Action 'Concrete s) Identity a
-> ProgramT (Action 'Concrete s) Identity b
-> ProgramT (Action 'Concrete s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper 'Concrete s (Either EvmError (Expr 'Buf))
execFully
VMFailure EvmError
x ->
Either EvmError (Expr 'Buf)
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT (Action 'Concrete s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvmError -> Either EvmError (Expr 'Buf)
forall a b. a -> Either a b
Left EvmError
x)
VMSuccess Expr 'Buf
x ->
Either EvmError (Expr 'Buf)
-> ProgramT
(Action 'Concrete s) Identity (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT (Action 'Concrete s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'Buf -> Either EvmError (Expr 'Buf)
forall a b. b -> Either a b
Right Expr 'Buf
x)
runFully :: Stepper t s (VM t s)
runFully :: forall (t :: VMType) s. Stepper t s (VM t s)
runFully = do
VM t s
vm <- Stepper t s (VM t s)
forall (t :: VMType) s. Stepper t s (VM t s)
run
case VM t s
vm.result of
Maybe (VMResult t s)
Nothing -> [Char] -> Stepper t s (VM t s)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"should not occur"
Just (HandleEffect (Query Query t s
q)) ->
Query t s -> Stepper t s ()
forall (t :: VMType) s. Query t s -> Stepper t s ()
wait Query t s
q Stepper t s () -> Stepper t s (VM t s) -> Stepper t s (VM t s)
forall a b.
ProgramT (Action t s) Identity a
-> ProgramT (Action t s) Identity b
-> ProgramT (Action t s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper t s (VM t s)
forall (t :: VMType) s. Stepper t s (VM t s)
runFully
Just (HandleEffect (Choose Choose s
q)) ->
Choose s -> Stepper 'Symbolic s ()
forall s. Choose s -> Stepper 'Symbolic s ()
ask Choose s
q Stepper t s () -> Stepper t s (VM t s) -> Stepper t s (VM t s)
forall a b.
ProgramT (Action t s) Identity a
-> ProgramT (Action t s) Identity b
-> ProgramT (Action t s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper t s (VM t s)
forall (t :: VMType) s. Stepper t s (VM t s)
runFully
Just VMResult t s
_ ->
VM t s -> Stepper t s (VM t s)
forall a. a -> ProgramT (Action t s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VM t s
vm
enter :: Text -> Stepper t s ()
enter :: forall (t :: VMType) s. Text -> Stepper t s ()
enter Text
t = EVM t s () -> Stepper t s ()
forall (t :: VMType) s a. EVM t s a -> Stepper t s a
evm (TraceData -> EVM t s ()
forall (t :: VMType) s. TraceData -> EVM t s ()
EVM.pushTrace (Text -> TraceData
EntryTrace Text
t))
interpret
:: forall m a . (App m)
=> Fetch.Fetcher Concrete m RealWorld
-> VM Concrete RealWorld
-> Stepper Concrete RealWorld a
-> m a
interpret :: forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
interpret Fetcher 'Concrete m RealWorld
fetcher VM 'Concrete RealWorld
vm = ProgramView (Action 'Concrete RealWorld) a -> m a
eval (ProgramView (Action 'Concrete RealWorld) a -> m a)
-> (Stepper 'Concrete RealWorld a
-> ProgramView (Action 'Concrete RealWorld) a)
-> Stepper 'Concrete RealWorld a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper 'Concrete RealWorld a
-> ProgramView (Action 'Concrete RealWorld) a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view
where
eval :: ProgramView (Action Concrete RealWorld) a -> m a
eval :: ProgramView (Action 'Concrete RealWorld) a -> m a
eval (Return a
x) = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
eval (Action 'Concrete RealWorld b
action :>>= b -> Stepper 'Concrete RealWorld a
k) =
case Action 'Concrete RealWorld b
action of
Action 'Concrete RealWorld b
Exec -> do
(VMResult 'Concrete RealWorld
r, VM 'Concrete RealWorld
vm') <- IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> m (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> m (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld))
-> IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> m (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST
RealWorld (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld))
-> ST
RealWorld (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
-> IO (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ StateT
(VM 'Concrete RealWorld)
(ST RealWorld)
(VMResult 'Concrete RealWorld)
-> VM 'Concrete RealWorld
-> ST
RealWorld (VMResult 'Concrete RealWorld, VM 'Concrete RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT
(VM 'Concrete RealWorld)
(ST RealWorld)
(VMResult 'Concrete RealWorld)
forall (t :: VMType) s. VMOps t => EVM t s (VMResult t s)
EVM.Exec.exec VM 'Concrete RealWorld
vm
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
interpret Fetcher 'Concrete m RealWorld
Query 'Concrete RealWorld -> m (EVM 'Concrete RealWorld ())
fetcher VM 'Concrete RealWorld
vm' (b -> Stepper 'Concrete RealWorld a
k b
VMResult 'Concrete RealWorld
r)
Wait Query 'Concrete RealWorld
q -> do
EVM 'Concrete RealWorld ()
m <- Fetcher 'Concrete m RealWorld
Query 'Concrete RealWorld -> m (EVM 'Concrete RealWorld ())
fetcher Query 'Concrete RealWorld
q
VM 'Concrete RealWorld
vm' <- IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld))
-> IO (VM 'Concrete RealWorld) -> m (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (VM 'Concrete RealWorld)
-> IO (VM 'Concrete RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM 'Concrete RealWorld)
-> IO (VM 'Concrete RealWorld))
-> ST RealWorld (VM 'Concrete RealWorld)
-> IO (VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Concrete RealWorld ()
-> VM 'Concrete RealWorld -> ST RealWorld (VM 'Concrete RealWorld)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT EVM 'Concrete RealWorld ()
m VM 'Concrete RealWorld
vm
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
interpret Fetcher 'Concrete m RealWorld
Query 'Concrete RealWorld -> m (EVM 'Concrete RealWorld ())
fetcher VM 'Concrete RealWorld
vm' (b -> Stepper 'Concrete RealWorld a
k ())
IOAct IO b
m -> do
b
r <- IO b -> m b
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO b
m
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
interpret Fetcher 'Concrete m RealWorld
Query 'Concrete RealWorld -> m (EVM 'Concrete RealWorld ())
fetcher VM 'Concrete RealWorld
vm (b -> Stepper 'Concrete RealWorld a
k b
r)
EVM EVM 'Concrete RealWorld b
m -> do
(b
r, VM 'Concrete RealWorld
vm') <- IO (b, VM 'Concrete RealWorld) -> m (b, VM 'Concrete RealWorld)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (b, VM 'Concrete RealWorld) -> m (b, VM 'Concrete RealWorld))
-> IO (b, VM 'Concrete RealWorld) -> m (b, VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ ST RealWorld (b, VM 'Concrete RealWorld)
-> IO (b, VM 'Concrete RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (b, VM 'Concrete RealWorld)
-> IO (b, VM 'Concrete RealWorld))
-> ST RealWorld (b, VM 'Concrete RealWorld)
-> IO (b, VM 'Concrete RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM 'Concrete RealWorld b
-> VM 'Concrete RealWorld
-> ST RealWorld (b, VM 'Concrete RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT EVM 'Concrete RealWorld b
m VM 'Concrete RealWorld
vm
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
forall (m :: * -> *) a.
App m =>
Fetcher 'Concrete m RealWorld
-> VM 'Concrete RealWorld -> Stepper 'Concrete RealWorld a -> m a
interpret Fetcher 'Concrete m RealWorld
Query 'Concrete RealWorld -> m (EVM 'Concrete RealWorld ())
fetcher VM 'Concrete RealWorld
vm' (b -> Stepper 'Concrete RealWorld a
k b
r)