Stepper.hs

{-# LANGUAGE ScopedTypeVariables #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , fork
  , evm
  , 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.IO.Class
import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view)
import Control.Monad.ST (stToIO, RealWorld)
import Control.Monad.State.Strict (execStateT, runStateT, get)
import Data.Text (Text)

import EVM qualified
import EVM.Effects
import EVM.Exec qualified
import EVM.Fetch qualified as Fetch
import EVM.Types

-- | 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)
  -- | Embed a VM state transformation
  EVM  :: EVM t s a -> Action t s a
  -- | Wait for a query to be resolved
  Wait :: Query t s -> Action t s ()
  -- | Two things can happen
  Fork :: RunBoth s -> Action Symbolic s ()
  -- | Many (>2) things can happen
  ForkMany :: RunAll s -> Action Symbolic s ()

-- | 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 = singleton Exec

run :: Stepper t s (VM t s)
run = exec >> evm get

wait :: Query t s -> Stepper t s ()
wait = singleton . Wait

fork :: RunBoth s -> Stepper Symbolic s ()
fork = singleton . Fork

forkMany :: RunAll s -> Stepper Symbolic s ()
forkMany = singleton . ForkMany

evm :: EVM t s a -> Stepper t s a
evm = singleton . EVM

-- | Run the VM until final result, resolving all queries
execFully :: Stepper Concrete s (Either EvmError (Expr Buf))
execFully =
  exec >>= \case
    HandleEffect (Query q) ->
      wait q >> execFully
    VMFailure x ->
      pure (Left x)
    VMSuccess x ->
      pure (Right x)

-- | Run the VM until its final state
runFully :: Stepper t s (VM t s)
runFully = do
  vm <- run
  case vm.result of
    Nothing -> internalError "should not occur"
    Just (HandleEffect (Query q)) ->
      wait q >> runFully
    Just (HandleEffect (RunBoth q)) ->
      fork q >> runFully
    Just (HandleEffect (RunAll q)) ->
      forkMany q >> runFully
    Just _ ->
      pure vm

enter :: Text -> Stepper t s ()
enter t = evm (EVM.pushTrace (EntryTrace t))

interpret
  :: forall m a . (App m)
  => Fetch.Fetcher Concrete m RealWorld
  -> VM Concrete RealWorld
  -> Stepper Concrete RealWorld a
  -> m a
interpret fetcher vm = eval . view
  where
    eval :: ProgramView (Action Concrete RealWorld) a -> m a
    eval (Return x) = pure x
    eval (action :>>= k) =
      case action of
        Exec -> do
          conf <- readConfig
          (r, vm') <- liftIO $ stToIO $ runStateT (EVM.Exec.exec conf) vm
          interpret fetcher vm' (k r)
        Wait q -> do
          m <- fetcher q
          vm' <- liftIO $ stToIO $ execStateT m vm
          interpret fetcher vm' (k ())
        EVM m -> do
          (r, vm') <- liftIO $ stToIO $ runStateT m vm
          interpret fetcher vm' (k r)