{-# LANGUAGE DataKinds #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , evmIO
  , entering
  , 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 (StateT, execState, runState, runStateT)
import Data.Text (Text)

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

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

  -- | Keep executing until an intermediate result is reached
  Exec :: Action VMResult

  -- | Keep executing until an intermediate state is reached
  Run :: Action VM

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

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

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

  -- | Perform an IO action
  IOAct :: StateT VM IO a -> Action a -- they should all just be this?

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

-- Singleton actions

exec :: Stepper VMResult
exec :: Stepper VMResult
exec = Action VMResult -> Stepper VMResult
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VMResult
Exec

run :: Stepper VM
run :: Stepper VM
run = Action VM -> Stepper VM
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VM
Run

wait :: Query -> Stepper ()
wait :: Query -> Stepper ()
wait = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Query -> Action ()) -> Query -> Stepper ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Query -> Action ()
Wait

ask :: Choose -> Stepper ()
ask :: Choose -> Stepper ()
ask = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Choose -> Action ()) -> Choose -> Stepper ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Choose -> Action ()
Ask

evm :: EVM a -> Stepper a
evm :: forall a. EVM a -> Stepper a
evm = Action a -> ProgramT Action Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> ProgramT Action Identity a)
-> (EVM a -> Action a) -> EVM a -> ProgramT Action Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EVM a -> Action a
forall a. EVM a -> Action a
EVM

evmIO :: StateT VM IO a -> Stepper a
evmIO :: forall a. StateT VM IO a -> Stepper a
evmIO = Action a -> ProgramT Action Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> ProgramT Action Identity a)
-> (StateT VM IO a -> Action a)
-> StateT VM IO a
-> ProgramT Action Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT VM IO a -> Action a
forall a. StateT VM IO a -> Action a
IOAct

-- | Run the VM until final result, resolving all queries
execFully :: Stepper (Either EvmError (Expr Buf))
execFully :: Stepper (Either EvmError (Expr 'Buf))
execFully =
  Stepper VMResult
exec Stepper VMResult
-> (VMResult -> Stepper (Either EvmError (Expr 'Buf)))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> (a -> ProgramT Action Identity b) -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    HandleEffect (Query Query
q) ->
      Query -> Stepper ()
wait Query
q Stepper ()
-> Stepper (Either EvmError (Expr 'Buf))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper (Either EvmError (Expr 'Buf))
execFully
    HandleEffect (Choose Choose
q) ->
      Choose -> Stepper ()
ask Choose
q Stepper ()
-> Stepper (Either EvmError (Expr 'Buf))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper (Either EvmError (Expr 'Buf))
execFully
    VMFailure EvmError
x ->
      Either EvmError (Expr 'Buf)
-> Stepper (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT Action 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)
-> Stepper (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT Action 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)
    Unfinished PartialExec
x
      -> [Char] -> Stepper (Either EvmError (Expr 'Buf))
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Stepper (Either EvmError (Expr 'Buf)))
-> [Char] -> Stepper (Either EvmError (Expr 'Buf))
forall a b. (a -> b) -> a -> b
$ [Char]
"partial execution encountered during concrete execution: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> PartialExec -> [Char]
forall a. Show a => a -> [Char]
show PartialExec
x

-- | Run the VM until its final state
runFully :: Stepper VM
runFully :: Stepper VM
runFully = do
  VM
vm <- Stepper VM
run
  case VM
vm.result of
    Maybe VMResult
Nothing -> [Char] -> Stepper VM
forall a. HasCallStack => [Char] -> a
internalError [Char]
"should not occur"
    Just (HandleEffect (Query Query
q)) ->
      Query -> Stepper ()
wait Query
q Stepper () -> Stepper VM -> Stepper VM
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper VM
runFully
    Just (HandleEffect (Choose Choose
q)) ->
      Choose -> Stepper ()
ask Choose
q Stepper () -> Stepper VM -> Stepper VM
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper VM
runFully
    Just VMResult
_ ->
      VM -> Stepper VM
forall a. a -> ProgramT Action Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VM
vm

entering :: Text -> Stepper a -> Stepper a
entering :: forall a. Text -> Stepper a -> Stepper a
entering Text
t Stepper a
stepper = do
  EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm (TraceData -> EVM ()
EVM.pushTrace (Text -> TraceData
EntryTrace Text
t))
  a
x <- Stepper a
stepper
  EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm EVM ()
EVM.popTrace
  a -> Stepper a
forall a. a -> ProgramT Action Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

enter :: Text -> Stepper ()
enter :: Text -> Stepper ()
enter Text
t = EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm (TraceData -> EVM ()
EVM.pushTrace (Text -> TraceData
EntryTrace Text
t))

interpret :: Fetch.Fetcher -> VM -> Stepper a -> IO a
interpret :: forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm = ProgramView Action a -> IO a
forall a. ProgramView Action a -> IO a
eval (ProgramView Action a -> IO a)
-> (Stepper a -> ProgramView Action a) -> Stepper a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper a -> ProgramView Action a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view
  where
    eval :: ProgramView Action a -> IO a
    eval :: forall a. ProgramView Action a -> IO a
eval (Return a
x) = a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    eval (Action b
action :>>= b -> ProgramT Action Identity a
k) =
      case Action b
action of
        Action b
Exec ->
          let (VMResult
r, VM
vm') = State VM VMResult -> VM -> (VMResult, VM)
forall s a. State s a -> s -> (a, s)
runState State VM VMResult
EVM.Exec.exec VM
vm
          in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
VMResult
r)
        Action b
Run ->
          let vm' :: VM
vm' = State VM VM -> VM -> VM
forall s a. State s a -> s -> s
execState State VM VM
EVM.Exec.run VM
vm
          in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
VM
vm')
        Wait (PleaseAskSMT (Lit W256
c) [Prop]
_ BranchCondition -> EVM ()
continue) ->
          let (()
r, VM
vm') = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case (W256
c W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0))) VM
vm
          in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
()
r)
        Wait Query
q -> do
          EVM ()
m <- Fetcher
fetcher Query
q
          let vm' :: VM
vm' = EVM () -> VM -> VM
forall s a. State s a -> s -> s
execState EVM ()
m VM
vm
          Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k ())
        Ask Choose
_ ->
          [Char] -> IO a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot make choices with this interpreter"
        IOAct StateT VM IO b
m -> do
          (b
r, VM
vm') <- StateT VM IO b -> VM -> IO (b, VM)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT VM IO b
m VM
vm
          Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
r)
        EVM EVM b
m ->
          let (b
r, VM
vm') = EVM b -> VM -> (b, VM)
forall s a. State s a -> s -> (a, s)
runState EVM b
m VM
vm
          in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
r)