{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , evmIO
  , enter
  , interpret
  )
where

-- This module is an abstract definition of EVM steppers.
-- Steppers can be run as TTY debuggers or as CLI test runners.
--
-- The implementation uses the operational monad pattern
-- as the framework for monadic interpretation.

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

-- | The instruction type of the operational monad
data Action t s a where

  -- | Keep executing until an intermediate result is reached
  Exec :: Action t s (VMResult t s)

  -- | Wait for a query to be resolved
  Wait :: Query t s -> Action t s ()

  -- | Multiple things can happen
  Ask :: Choose s -> Action Symbolic s ()

  -- | Embed a VM state transformation
  EVM  :: EVM t s a -> Action t s a

  -- | Perform an IO action
  IOAct :: IO a -> Action t s a

-- | Type alias for an operational monad of @Action@
type Stepper t s a = Program (Action t s) a

-- Singleton actions

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

-- | Run the VM until final result, resolving all queries
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)

-- | Run the VM until its final state
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)