EVM.Stepper

Documentation

data Action t s a where

The instruction type of the operational monad

Constructors

Exec :: Action t s (VMResult t s)

Keep executing until an intermediate result is reached

Wait :: Query t s -> Action t s ()

Wait for a query to be resolved

Ask :: Choose s -> Action Symbolic s ()

Multiple things can happen

EVM :: EVM t s a -> Action t s a

Embed a VM state transformation

IOAct :: IO a -> Action t s a

Perform an IO action

type Stepper t s a = Program (Action t s) a

Type alias for an operational monad of Action

exec :: Stepper t s (VMResult t s)

execFully :: Stepper Concrete s (Either EvmError (Expr Buf))

Run the VM until final result, resolving all queries

run :: Stepper t s (VM t s)

runFully :: Stepper t s (VM t s)

Run the VM until its final state

wait :: Query t s -> Stepper t s ()

ask :: Choose s -> Stepper Symbolic s ()

evm :: EVM t s a -> Stepper t s a

evmIO :: IO a -> Stepper t s a

enter :: Text -> Stepper t s ()

interpret :: forall m a. App m => Fetcher Concrete m RealWorld -> VM Concrete RealWorld -> Stepper Concrete RealWorld a -> m a