-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Module, containing function to interpret Michelson
-- instructions against given context and input stack.
module Morley.Michelson.Interpret
  ( ContractEnv (..)
  , InterpreterState (..)
  , MichelsonFailed (..)
  , MichelsonFailureWithStack(..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , buildMorleyLogs
  , MorleyLogsBuilder (..)

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , ContractReturn

  , mkInitStack
  , fromFinalStack
  , InterpretError (..)
  , InterpretResult (..)
  , EvalM
  , InterpreterStateMonad (..)
  , StkEl (..)
  , InstrRunner
  , runInstr
  , runInstrNoGas
  , runUnpack

    -- * Internals
  , initInterpreterState
  , handleContractReturn
  , runInstrImpl
  , assignBigMapIds

    -- * Prisms
  , _MorleyLogs
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor, makePrisms, traverseOf, (<<+=))
import Control.Monad.Except (MonadError, throwError)
import Control.Monad.RWS.Strict (RWS, RWST, runRWS)
import Control.Monad.Writer (MonadWriter, WriterT, tell)
import Data.Default (Default(..))
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Singletons.Decide (decideEquality)
import Data.Vinyl (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap)
import Fmt (Buildable(build), blockListF, pretty, prettyLn, (+|), (|+))
import Unsafe qualified (fromIntegral)

import Morley.Michelson.ErrorPos (ErrorSrcPos(..))
import Morley.Michelson.Interpret.Pack (packValue')
import Morley.Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Morley.Michelson.Runtime.GState
import Morley.Michelson.TypeCheck (eqType)
import Morley.Michelson.Typed hiding (Branch(..))
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Operation
  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)
import Morley.Michelson.Untyped (unAnnotation)
import Morley.Tezos.Address
import Morley.Tezos.Address.Alias
import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez)
import Morley.Tezos.Crypto
  (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,
  sha256, sha3, sha512)
import Morley.Tezos.Crypto.BLS12381 (checkPairing)
import Morley.Util.Peano (LongerThan, Peano)
import Morley.Util.PeanoNatural (PeanoNatural(..))
import Morley.Util.Sing (eqParamSing)
import Morley.Util.Type
import Morley.Util.Typeable

-- | Morley logs appearing as interpreter result.
newtype MorleyLogs = MorleyLogs { unMorleyLogs :: [Text] }
  deriving stock (Show, Eq, Generic)
  deriving newtype (Semigroup, Monoid)
  deriving anyclass (NFData)

instance Buildable MorleyLogs where
  build = blockListF . unMorleyLogs

-- | Morley logs accumulator, for incremental building.
newtype MorleyLogsBuilder = MorleyLogsBuilder (Endo [Text])
  deriving stock (Generic)
  deriving newtype (Default, Semigroup, Monoid)

buildMorleyLogs :: MorleyLogsBuilder -> MorleyLogs
buildMorleyLogs (MorleyLogsBuilder builder) =
  MorleyLogs $ appEndo builder []

instance One MorleyLogsBuilder where
  type OneItem MorleyLogsBuilder = Text
  one log = MorleyLogsBuilder $ Endo (log :)

newtype RemainingSteps = RemainingSteps Word64
  deriving stock (Show, Generic)
  deriving newtype (Eq, Ord, Buildable, Num)

instance NFData RemainingSteps

data InterpreterState = InterpreterState
  { isRemainingSteps :: RemainingSteps
  , isGlobalCounter :: GlobalCounter
  , isBigMapCounter :: BigMapCounter
  } deriving stock (Show, Generic)

instance NFData InterpreterState
makeLensesFor
  [ ("isBigMapCounter", "isBigMapCounterL")
  ]
  ''InterpreterState

makePrisms ''MorleyLogs

newtype StkEl t = StkEl
  { seValue :: Value t
  } deriving stock (Eq, Show)

makeLensesFor
  [ ("seValue", "seValueL")
  ]
  ''StkEl

-- | Environment for contract execution.
data ContractEnv = ContractEnv
  { ceNow :: Timestamp
  -- ^ Timestamp returned by the 'NOW' instruction.
  , ceMaxSteps :: RemainingSteps
  -- ^ Number of steps after which execution unconditionally terminates.
  , ceBalance :: Mutez
  -- ^ Current amount of mutez of the current contract.
  , ceContracts :: Map ContractAddress ContractState
  -- ^ Information stored about the existing contracts.
  , ceSelf :: ContractAddress
  -- ^ Address of the interpreted contract.
  , ceSource :: L1Address
  -- ^ The contract that initiated the current transaction. Note that this
  -- contract should in normal operation be an implicit account.
  , ceSender :: L1Address
  -- ^ The contract that initiated the current internal transaction. This may
  -- either be an implicit account or a smart contract.
  , ceAmount :: Mutez
  -- ^ Amount of the current transaction.
  , ceVotingPowers :: VotingPowers
  -- ^ Distribution of voting power.
  , ceChainId :: ChainId
  -- ^ Identifier of the current chain.
  , ceOperationHash :: Maybe OperationHash
  -- ^ Hash of the currently executed operation, required for
  -- correct contract address computation in @CREATE_CONTRACT@ instruction.
  , ceLevel :: Natural
  -- ^ Number of blocks before the given one in the chain
  , ceErrorSrcPos :: ErrorSrcPos
  -- ^ Current source position information
  , ceMinBlockTime :: Natural
  -- ^ Minimum time between blocks
  }

-- | Errors that can be thrown by the interpreter. The @ext@ type variable
-- allow the downstreams consumer to add additional exceptions.
data MichelsonFailed ext where
  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed ext
    -- ^ Represents @[FAILED]@ state of a Michelson program. Contains
    -- value that was on top of the stack when @FAILWITH@ was called.
  MichelsonArithError
    :: (Typeable n, Typeable m)
    => ArithError (Value n) (Value m) -> MichelsonFailed ext
  MichelsonGasExhaustion :: MichelsonFailed ext
  MichelsonFailedTestAssert :: Text -> MichelsonFailed ext
  MichelsonUnsupported :: Text -> MichelsonFailed ext
  MichelsonExt :: ext -> MichelsonFailed ext

deriving stock instance Show ext => Show (MichelsonFailed ext)

instance Eq ext => Eq (MichelsonFailed ext) where
  MichelsonFailedWith v1 == MichelsonFailedWith v2 = v1 `eqParamSing` v2
  MichelsonFailedWith _ == _ = False
  MichelsonArithError ae1 == MichelsonArithError ae2 = ae1 `eqParam2` ae2
  MichelsonArithError _ == _ = False
  MichelsonGasExhaustion == MichelsonGasExhaustion = True
  MichelsonGasExhaustion == _ = False
  MichelsonFailedTestAssert t1 == MichelsonFailedTestAssert t2 = t1 == t2
  MichelsonFailedTestAssert _ == _ = False
  MichelsonUnsupported i1 == MichelsonUnsupported i2 = i1 == i2
  MichelsonUnsupported _ == _ = False
  MichelsonExt i1 == MichelsonExt i2 = i1 == i2
  MichelsonExt _ == _ = False

instance Buildable ext => Buildable (MichelsonFailed ext) where
  build =
    \case
      MichelsonFailedWith v ->
        "Reached FAILWITH instruction with " +| v |+ ""
      MichelsonArithError v -> build v
      MichelsonGasExhaustion ->
        "Gas limit exceeded on contract execution"
      MichelsonFailedTestAssert t -> build t
      MichelsonUnsupported instr ->
        build instr <> " instruction is not supported."
      MichelsonExt x -> build x

-- | Carries a 'MichelsonFailed' @ext@ error and the 'ErrorSrcPos' at which it was raised
data MichelsonFailureWithStack ext = MichelsonFailureWithStack
  { mfwsFailed :: MichelsonFailed ext
  , mfwsErrorSrcPos :: ErrorSrcPos
  } deriving stock (Show, Generic, Eq)

instance Buildable ext => Buildable (MichelsonFailureWithStack ext) where
  build (MichelsonFailureWithStack err loc) = build err <> " at " <> build loc

newtype InterpretError ext = InterpretError (MichelsonFailureWithStack ext, MorleyLogs)
  deriving stock (Generic)

deriving stock instance Show ext => Show (InterpretError ext)

instance Buildable ext => Buildable (InterpretError ext) where
  build (InterpretError (mf, _)) = prettyLn mf

data InterpretResult where
  InterpretResult
    :: ( StorageScope st )
    => { iurOps :: [Operation]
       , iurNewStorage :: T.Value st
       , iurNewState   :: InterpreterState
       , iurMorleyLogs :: MorleyLogs
       }
    -> InterpretResult

deriving stock instance Show InterpretResult

constructIR ::
  (StorageScope st) =>
  (([Operation], Value' Instr st), InterpreterState, MorleyLogs) ->
  InterpretResult
constructIR ((ops, val), st, logs) =
  InterpretResult
  { iurOps = ops
  , iurNewStorage = val
  , iurNewState = st
  , iurMorleyLogs = logs
  }

type ContractReturn st =
  (Either (MichelsonFailureWithStack Void) ([Operation], T.Value st), (InterpreterState, MorleyLogs))

handleContractReturn
  :: (StorageScope st)
  => ContractReturn st -> Either (InterpretError Void) InterpretResult
handleContractReturn (ei, (s, l)) =
  bimap (InterpretError . (, l)) (constructIR . (, s, l)) ei

-- | Helper function to convert a record of @Value@ to @StkEl@. These will be
-- created with @starNotes@.
mapToStkEl :: Rec T.Value inp -> Rec StkEl inp
mapToStkEl = rmap StkEl

-- | Helper function to convert a record of @StkEl@ to @Value@. Any present
-- notes will be discarded.
mapToValue :: Rec StkEl inp -> Rec T.Value inp
mapToValue = rmap seValue

interpret'
  :: forall cp st arg.
     Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' Contract{..} epc param initSt env ist = first (fmap fromFinalStack) $
  runEvalOp
    (runInstr (unContractCode cCode) $ mkInitStack (liftCallArg epc param) initSt)
    env
    ist

mkInitStack
  :: T.Value param
  -> T.Value st
  -> Rec StkEl (ContractInp param st)
mkInitStack param st = StkEl
  (T.VPair (param, st))
    :& RNil

fromFinalStack :: Rec StkEl (ContractOut st) -> ([T.Operation], T.Value st)
fromFinalStack (StkEl (T.VPair (T.VList ops, st)) :& RNil) =
  (map (\(T.VOp op) -> op) ops, st)

interpret
  :: Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> GlobalCounter
  -> BigMapCounter
  -> ContractEnv
  -> ContractReturn st
interpret contract epc param initSt globalCounter bmCounter env =
  interpret' contract epc param initSt env (initInterpreterState globalCounter bmCounter env)

initInterpreterState :: GlobalCounter -> BigMapCounter -> ContractEnv -> InterpreterState
initInterpreterState globalCounter bmCounter env =
  InterpreterState (ceMaxSteps env) globalCounter bmCounter

-- | Interpret an instruction in vacuum, putting no extra constraints on
-- its execution.
--
-- Mostly for testing purposes.
interpretInstr
  :: ContractEnv
  -> Instr inp out
  -> Rec T.Value inp
  -> Either (MichelsonFailureWithStack Void) (Rec T.Value out)
interpretInstr = fmap mapToValue ... interpretInstrAnnotated

-- | Interpret an instruction in vacuum, putting no extra constraints on
-- its execution while preserving its annotations.
--
-- Mostly for testing purposes.
interpretInstrAnnotated
  :: ContractEnv
  -> Instr inp out
  -> Rec T.Value inp
  -> Either (MichelsonFailureWithStack Void) (Rec StkEl out)
interpretInstrAnnotated env instr inpSt =
  fst $
  runEvalOp
    (runInstr instr $ mapToStkEl inpSt)
    env
    InterpreterState
      { isRemainingSteps = 9999999999
      , isBigMapCounter = 0
      , isGlobalCounter = 0
      }

data SomeItStack where
  SomeItStack :: T.ExtInstr inp -> Rec StkEl inp -> SomeItStack

type EvalOp =
  ExceptT (MichelsonFailureWithStack Void) $
  RWS ContractEnv MorleyLogsBuilder InterpreterState

runEvalOp
  :: EvalOp a
  -> ContractEnv
  -> InterpreterState
  -> (Either (MichelsonFailureWithStack Void) a, (InterpreterState, MorleyLogs))
runEvalOp act env initSt =
  let (res, is, logs) = runRWS (runExceptT act) env initSt
  in (res, (is, buildMorleyLogs logs))

class Monad m => InterpreterStateMonad m where
  getInterpreterState :: m InterpreterState
  getInterpreterState = stateInterpreterState (\s -> (s, s))

  putInterpreterState :: InterpreterState -> m ()
  putInterpreterState s = stateInterpreterState (\_ -> ((), s))

  stateInterpreterState :: (InterpreterState -> (a, InterpreterState)) -> m a
  stateInterpreterState f = do
    s <- getInterpreterState
    let (a, s') = f s
    a <$ putInterpreterState s'

  modifyInterpreterState :: (InterpreterState -> InterpreterState) -> m ()
  modifyInterpreterState f = stateInterpreterState (((), ) . f)

instance Monad m => InterpreterStateMonad (StateT InterpreterState m) where
  stateInterpreterState = state
instance (Monad m, Monoid w) => InterpreterStateMonad (RWST r w InterpreterState m) where
  stateInterpreterState = state

instance InterpreterStateMonad m => InterpreterStateMonad (ReaderT r m) where
  stateInterpreterState = lift . stateInterpreterState
instance (InterpreterStateMonad m, Monoid w) => InterpreterStateMonad (WriterT w m) where
  stateInterpreterState = lift . stateInterpreterState
instance {-# OVERLAPPABLE #-} InterpreterStateMonad m => InterpreterStateMonad (StateT w m) where
  stateInterpreterState = lift . stateInterpreterState
instance {-# OVERLAPPABLE #-}
         (InterpreterStateMonad m, Monoid w) => InterpreterStateMonad (RWST r w s m) where
  stateInterpreterState = lift . stateInterpreterState
instance InterpreterStateMonad m => InterpreterStateMonad (ExceptT e m) where
  stateInterpreterState = lift . stateInterpreterState

type EvalM' ext m =
  ( MonadReader ContractEnv m
  , InterpreterStateMonad m
  , MonadWriter MorleyLogsBuilder m
  , MonadError (MichelsonFailureWithStack ext) m
  )

type EvalM m = EvalM' Void m

type InstrRunner m =
  forall inp out.
     Instr inp out
  -> Rec StkEl inp
  -> m (Rec StkEl out)

throwMichelson :: EvalM' ext m => MichelsonFailed ext -> m a
throwMichelson mf = asks ceErrorSrcPos >>= throwError . MichelsonFailureWithStack mf

-- | Function to change amount of remaining steps stored in State monad.
runInstr :: EvalM m => InstrRunner m
runInstr i@(Seq _i1 _i2) r = runInstrImpl runInstr i r
runInstr i@(WithLoc _ _) r = runInstrImpl runInstr i r
runInstr i@(Meta _ _i1) r = runInstrImpl runInstr i r
runInstr i@Nop r = runInstrImpl runInstr i r
runInstr i@(Nested _) r = runInstrImpl runInstr i r
runInstr i@(DocGroup _ _i1) r = runInstrImpl runInstr i r
runInstr i r = do
  rs <- isRemainingSteps <$> getInterpreterState
  if rs == 0
  then throwMichelson MichelsonGasExhaustion
  else do
    modifyInterpreterState (\s -> s {isRemainingSteps = rs - 1})
    runInstrImpl runInstr i r

runInstrNoGas :: EvalM m => InstrRunner m
runInstrNoGas = runInstrImpl runInstrNoGas

-- | Function to interpret Michelson instruction(s) against given stack.
-- The @ext@ type variable specifies additional exceptions that can be thrown from the inner
-- runner function (via 'MichelsonExt'). In Morley, it's set to 'Void', but downstream consumers
-- may use other type here.
runInstrImpl :: forall ext m. EvalM' ext m => InstrRunner m -> InstrRunner m
runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
runInstrImpl runner (WithLoc ics i) r = local (\env -> env{ceErrorSrcPos = ics}) $ runner i r
runInstrImpl runner (Meta _ i) r = runner i r
runInstrImpl runner (FrameInstr (_ :: Proxy s) i) r = do
  let (inp, end) = rsplit @_ @_ @s r
  out <- runInstrImpl runner i inp
  return (out <+> end)
runInstrImpl _ Nop r = pure $ r
runInstrImpl runner (Ext nop) r = r <$ interpretExt runner (SomeItStack nop r)
runInstrImpl runner (Nested sq) r = runner sq r
runInstrImpl runner (DocGroup _ sq) r = runInstrImpl runner sq r
runInstrImpl _ DROP (_ :& r) = pure $ r
runInstrImpl runner (DROPN n) stack =
  case n of
    Zero    -> pure stack
    Succ s' -> case stack of
      (_ :& r) -> runInstrImpl runner (DROPN s') r
      -- Note: we intentionally do not use `runner` to recursively
      -- interpret `DROPN` here.
      -- All these recursive calls together correspond to a single
      -- Michelson instruction call.
      -- This recursion is implementation detail of `DROPN`.
      -- The same reasoning applies to other instructions parameterized
      -- by a natural number like 'DIPN'.
runInstrImpl _ AnnDUP{} (stkEl :& r) = do
  -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).
  duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl
  pure $ duplicateStkEl :& stkEl :& r
runInstrImpl _ (AnnDUPN _ s) stack = go s stack
  where
    go :: forall (n :: Peano) inp out a. ConstraintDUPN n inp out a
       => PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
    go (Succ Zero) stk@(stkEl :& _) = do
        -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).
        duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl
        pure $ duplicateStkEl :& stk
    go (Succ n@(Succ _)) (b :& r) =
      go n r <&> \case
        (a :& resTail) -> a :& b :& resTail
runInstrImpl _ SWAP (a :& b :& r) = pure $ b :& a :& r
runInstrImpl _ (DIG s) input0 =
  pure $ go s input0
  where
    go :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a
       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
    go Zero stack = stack
    go (Succ n') (b :& r) =
      case go n' r of
        a :& resTail -> a :& b :& resTail
runInstrImpl _ (DUG s) input0 =
  pure $ go s input0
  where
    go :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a
       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
    go Zero stack = stack
    go (Succ n') (a :& b :& r) = b :& go n' (a :& r)
runInstrImpl _ AnnSOME{} ((seValue -> a) :& r) =
  withValueTypeSanity a $
    pure $ StkEl (VOption (Just a)) :& r
runInstrImpl _ (AnnPUSH _ v) r = pure $ StkEl v :& r
runInstrImpl _ AnnNONE{} r = pure $ StkEl (VOption Nothing) :& r
runInstrImpl _ AnnUNIT{} r = pure $ StkEl VUnit :& r
runInstrImpl runner (IF_NONE _bNone bJust) (StkEl (VOption (Just a)) :& r) =
  runner bJust (StkEl a :& r)
runInstrImpl runner (IF_NONE bNone _bJust) (StkEl (VOption Nothing) :& r) =
  runner bNone r
runInstrImpl _ NEVER inp = case inp of {}
runInstrImpl _ (AnnPAIR{}) ((StkEl a) :& (StkEl b) :& r) =
  pure $ StkEl (VPair (a, b)) :& r
runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b))) :& r) =
  pure $ StkEl a :& StkEl b :& r
runInstrImpl _ (AnnPAIRN _ s) stack = pure $ go s stack
  where
    go :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
    go (Succ (Succ Zero)) (StkEl a :& StkEl b :& r) =
      -- if n=2
      StkEl (VPair (a, b)) :& r
    go (Succ n@(Succ (Succ _))) (StkEl a :& r@(_ :& _ :& _)) =
      -- if n>2
      case go n r of
        StkEl combed :& r' ->
            StkEl (VPair (a, combed)) :& r'
runInstrImpl _ (UNPAIRN s) (StkEl pair0 :& r) = do
  pure $ go s pair0 <+> r
  where
    go
      :: forall n pair. ConstraintUnpairN n pair
      => PeanoNatural n -> Value pair
      -> Rec StkEl (UnpairN n pair)
    go n pair =
      case (n, pair) of
        -- if n=2
        (Succ (Succ Zero), VPair (a, b)) ->
          StkEl a
            :& StkEl b
            :& RNil
        -- if n>2
        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _))) ->
          StkEl a
            :& go n' b
runInstrImpl _ AnnCAR{} (StkEl (VPair (a, _b)) :& r) = pure $ StkEl a :& r
runInstrImpl _ AnnCDR{} (StkEl (VPair (_a, b)) :& r) = pure $ StkEl b :& r
runInstrImpl _ AnnLEFT{} ((StkEl a) :& r) =
  withValueTypeSanity a $
    pure $ StkEl (VOr $ Left a) :& r
runInstrImpl _ AnnRIGHT{} ((StkEl b) :& r) =
  withValueTypeSanity b $
    pure $ StkEl (VOr $ Right b) :& r
runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) :& r) =
  runner bLeft (StkEl a :& r)
runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) :& r) =
  runner bRight (StkEl a :& r)
runInstrImpl _ AnnNIL{} r = pure $ StkEl (VList []) :& r
runInstrImpl _ AnnCONS{} (a :& StkEl (VList l) :& r) = pure $ StkEl (VList (seValue a : l)) :& r
runInstrImpl runner (IF_CONS _ bNil) (StkEl (VList []) :& r) = runner bNil r
runInstrImpl runner (IF_CONS bCons _) (StkEl (VList (lh : lr)) :& r) =
  runner bCons (StkEl lh :& StkEl (VList lr) :& r)
runInstrImpl _ AnnSIZE{} (a :& r) = pure $ StkEl (VNat $ Unsafe.fromIntegral @Int @Natural $ evalSize $ seValue a) :& r
runInstrImpl _ AnnEMPTY_SET{} r = pure $ StkEl (VSet Set.empty) :& r
runInstrImpl _ AnnEMPTY_MAP{} r = pure $ StkEl (VMap Map.empty) :& r
runInstrImpl _ AnnEMPTY_BIG_MAP{} r = do
  bigMap <- assignBigMapIds' $ VBigMap Nothing Map.empty
  pure $ StkEl bigMap :& r
runInstrImpl runner (AnnMAP _ (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl a :& r) = do
  -- Evaluation must preserve all stack modifications that @MAP@'s does.
  (newStack, newList) <- foldlM (\(curStack, curList) (val :: StkEl (MapOpInp c)) -> do
    res <- runner code (val :& curStack)
    case res of
      ((seValue -> nextVal :: T.Value b) :& nextStack) -> pure (nextStack, nextVal : curList))
    (r, []) ((\el -> StkEl el) <$> mapOpToList @c a)
  pure $ StkEl (mapOpFromList a (reverse newList)) :& newStack
runInstrImpl runner (ITER (code :: Instr (IterOpEl c ': s) s)) (StkEl a :& r) =
  case iterOpDetachOne @c a of
    (Just x, xs) -> do
      res <- runner code (StkEl x :& r)
      runner (ITER code) (StkEl xs :& res)
    (Nothing, _) -> pure r
runInstrImpl _ AnnMEM{} (a :& b :& r) = pure $ StkEl (VBool (evalMem (seValue a) (seValue b))) :& r
runInstrImpl _ AnnGET{} (a :& b :& r) = pure $ StkEl (VOption (evalGet (seValue a) (seValue b))) :& r
runInstrImpl _ (AnnGETN _ s) (StkEl pair :& r) = do
  pure $ StkEl (go s pair) :& r
  where
    go
      :: forall ix a. ConstraintGetN ix a
      => PeanoNatural ix -> Value a
      -> Value (GetN ix a)
    go Zero            a                   = a
    go (Succ Zero)      (VPair (left, _))  = left
    go (Succ (Succ n')) (VPair (_, right)) = go n' right
runInstrImpl _ AnnUPDATE{} (a :& b :& StkEl c :& r) =
  pure $ StkEl (evalUpd (seValue a) (seValue b) c) :& r
runInstrImpl _ (AnnUPDATEN _ s) (StkEl (val :: Value val) :& StkEl pair :& r) = do
  pure $ StkEl (go s pair) :& r
  where
    go
      :: forall ix pair. ConstraintUpdateN ix pair
      => PeanoNatural ix -> Value pair -> Value (UpdateN ix val pair)
    go Zero             _                      = val
    go (Succ Zero)      (VPair (_, right))     = VPair (val, right)
    go (Succ (Succ n')) (VPair (left, right))  = VPair (left, go n' right)
runInstrImpl _ AnnGET_AND_UPDATE{} (StkEl key :& StkEl valMb :& StkEl collection :& r) =
  pure $
    StkEl (VOption (evalGet key collection))
    :& StkEl (evalUpd key valMb collection)
    :& r
runInstrImpl runner (IF bTrue _) (StkEl (VBool True) :& r) = runner bTrue r
runInstrImpl runner (IF _ bFalse) (StkEl (VBool False) :& r) = runner bFalse r
runInstrImpl _ (LOOP _) (StkEl (VBool False) :& r) = pure $ r
runInstrImpl runner (LOOP ops) (StkEl (VBool True) :& r) = do
  res <- runner ops r
  runner (LOOP ops) res
runInstrImpl _ (LOOP_LEFT _) (StkEl (VOr (Right a)) :& r) = pure $ StkEl a :& r
runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) :& r) = do
  res <- runner ops (StkEl a :& r)
  runner (LOOP_LEFT ops) res
runInstrImpl _ (AnnLAMBDA _ lam) r = pure $ StkEl (mkVLam lam) :& r
runInstrImpl _ (AnnLAMBDA_REC _ lam) r = pure $ StkEl (mkVLamRec lam) :& r
runInstrImpl runner AnnEXEC{} (a :& self@(StkEl (VLam code)) :& r) =
  case code of
    LambdaCode (T.rfAnyInstr -> lBody) -> do
      res <- runner lBody (a :& RNil)
      pure $ res <+> r
    LambdaCodeRec (T.rfAnyInstr -> lBody) -> do
      res <- runner lBody (a :& self :& RNil)
      pure $ res <+> r
runInstrImpl _ i@AnnAPPLY{} (StkEl (a :: T.Value a) :& StkEl (VLam code) :& r)
  | _ :: Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s) <- i
  , _ :: LambdaCode' Instr ('TPair a b) c <- code
  = case code of
      LambdaCode lBody -> pure $ StkEl (VLam $ LambdaCode (T.rfMapAnyInstr doApply lBody)) :& r
      LambdaCodeRec lBody ->
        let res = RfNormal $ PUSH a `Seq` PAIR `Seq` LAMBDA_REC lBody `Seq` SWAP `Seq` EXEC
        in pure $ StkEl (VLam $ LambdaCode res) :& r
  where
    doApply :: Instr ('TPair a i ': s) o -> Instr (i ': s) o
    doApply b = PUSH a `Seq` PAIR `Seq` Nested b
runInstrImpl runner (DIP i) (a :& r) = do
  res <- runner i r
  pure $ a :& res
runInstrImpl runner (DIPN s i) stack =
  case s of
    Zero -> runner i stack
    Succ s' -> case stack of
      (a :& r) -> (a :&) <$> runInstrImpl runner (DIPN s' i) r
runInstrImpl _ FAILWITH (a :& _) = throwMichelson $ MichelsonFailedWith (seValue a)
runInstrImpl _ AnnCAST{} s = pure s
runInstrImpl _ AnnRENAME{} s = pure s
runInstrImpl _ AnnPACK{} ((seValue -> a) :& r) = pure $ StkEl (VBytes $ packValue' a) :& r
runInstrImpl _ AnnUNPACK{} (StkEl (VBytes a) :& r) =
  pure $ StkEl (VOption . rightToMaybe $ runUnpack a) :& r
runInstrImpl _ AnnCONCAT{} (a :& b :& r) = pure $ StkEl (evalConcat (seValue a) (seValue b)) :& r
runInstrImpl _ AnnCONCAT'{} (StkEl (VList a) :& r) = pure $ StkEl (evalConcat' a) :& r
runInstrImpl _ AnnSLICE{} (StkEl (VNat o) :& StkEl (VNat l) :& StkEl s :& r) =
  pure $ StkEl (VOption (evalSlice o l s)) :& r
runInstrImpl _ AnnISNAT{} (StkEl (VInt i) :& r) =
  if i < 0
  then pure $ StkEl (VOption Nothing) :& r
  else pure $ StkEl (VOption (Just (VNat $ fromInteger i))) :& r
runInstrImpl _ AnnADD{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Add) l r
runInstrImpl _ AnnSUB{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Sub) l r
runInstrImpl _ AnnSUB_MUTEZ{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @SubMutez) l r
runInstrImpl _ AnnMUL{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Mul) l r
runInstrImpl _ AnnEDIV{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @EDiv) l r
runInstrImpl _ AnnABS{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Abs) a) :& rest
runInstrImpl _ AnnNEG{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Neg) a) :& rest
runInstrImpl _ AnnLSL{} (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsl) x s
runInstrImpl _ AnnLSR{} (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsr) x s
runInstrImpl _ AnnOR{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Or) l r
runInstrImpl _ AnnAND{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @And) l r
runInstrImpl _ AnnXOR{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Xor) l r
runInstrImpl _ AnnNOT{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Not) a) :& rest
runInstrImpl _ AnnCOMPARE{} ((seValue -> l) :& (seValue -> r) :& rest) =
  pure $ StkEl (T.VInt (compareOp l r)) :& rest
runInstrImpl _ AnnEQ{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Eq') a) :& rest
runInstrImpl _ AnnNEQ{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Neq) a) :& rest
runInstrImpl _ AnnLT{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Lt) a) :& rest
runInstrImpl _ AnnGT{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Gt) a) :& rest
runInstrImpl _ AnnLE{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Le) a) :& rest
runInstrImpl _ AnnGE{} ((seValue -> a) :& rest) =
  pure $ StkEl (evalUnaryArithOp (Proxy @Ge) a) :& rest
runInstrImpl _ AnnINT{} (StkEl a :& r) =
  pure $ StkEl (evalToIntOp a) :& r
runInstrImpl runner (AnnVIEW (Anns2' _ (_ :: Notes ret)) name)
                    (StkEl (arg :: Value arg) :& StkEl (VAddress epAddr) :& r) = do
  ContractEnv{..} <- ask
  res :: Value ('TOption ret) <- VOption <$> runMaybeT do
    EpAddress addr@ContractAddress{} _ <- pure epAddr
    Just viewedContractState <- pure $ Map.lookup addr ceContracts
    ContractState
      { csContract = viewedContract
      , csStorage = viewedContractStorage
      } <- pure viewedContractState
    Just view_ <- pure $ lookupView name (cViews viewedContract)
    SomeView (View{ vCode } :: View arg' st ret') <- pure view_
    Just Refl <- pure $ sing @arg `decideEquality` sing @arg'
    Just Refl <- pure $ sing @ret `decideEquality` sing @ret'
    resSt <- lift $
      local (mkViewEnv addr viewedContractState) $
        runInstrImpl runner vCode $
          StkEl (VPair (arg, viewedContractStorage)) :& RNil
    let StkEl res :& RNil = resSt
    return res
  pure (StkEl res :& r)
  where
    mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv
    mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv
      { ceBalance = csBalance viewedContractState
      , ceSender = Constrained ceSelf
      , ceSelf = calledAddr
      , ceSource
      , ceAmount = zeroMutez
      , ceContracts
      , ceNow, ceMaxSteps, ceVotingPowers, ceChainId, ceOperationHash, ceLevel
      , ceErrorSrcPos, ceMinBlockTime
      }

runInstrImpl _ (AnnSELF _ sepc :: Instr inp out) r = do
  ContractEnv{..} <- ask
  case Proxy @out of
    (_ :: Proxy ('TContract cp ': s)) -> do
      pure $ StkEl (VContract (MkAddress ceSelf) sepc) :& r
runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: T.Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do
  ContractEnv{..} <- ask
  T.EpAddress' (Constrained addr) addrEpName <- pure epAddr
  let mepName =
        case (instrEpName, addrEpName) of
          (DefEpName, DefEpName) -> Just DefEpName
          (DefEpName, en) -> Just en
          (en, DefEpName) -> Just en
          _ -> Nothing

  let withNotes v = StkEl v :& r
  withNotes <$> case mepName of
    Nothing -> pure $ VOption Nothing
    Just epName -> case addr of
      ImplicitAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam
      ContractAddress{} -> pure $
        case Map.lookup addr ceContracts of
          Just ContractState{..} ->
            castContract addr epName (cParamNotes csContract)
          Nothing -> VOption Nothing
      TxRollupAddress{} ->
        -- TODO [#838]: support transaction rollups on the emulator
        throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"
  where
  castContract
    :: forall p kind. (T.ParameterScope p)
    => KindedAddress kind -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
  castContract addr epName param = VOption $ do
    -- As we are within Maybe monad, pattern-match failure results in Nothing
    MkEntrypointCallRes (_ :: Notes a') epc <- T.mkEntrypointCall epName param
    Right Refl <- pure $ eqType @a @a'
    return $ VContract (MkAddress addr) (T.SomeEpc epc)

runInstrImpl _ AnnTRANSFER_TOKENS{}
  (StkEl p :& StkEl (VMutez mutez) :& StkEl contract :& r) = do
    incrementCounter
    globalCounter <- isGlobalCounter <$> getInterpreterState
    pure $ StkEl (VOp (OpTransferTokens $ TransferTokens p mutez contract globalCounter)) :& r
runInstrImpl _ AnnSET_DELEGATE{} (StkEl (VOption mbKeyHash) :& r) = do
  incrementCounter
  globalCounter <- isGlobalCounter <$> getInterpreterState
  case mbKeyHash of
    Just (VKeyHash k) -> pure $ StkEl (VOp (OpSetDelegate $ SetDelegate (Just k) globalCounter)) :& r
    Nothing -> pure $ StkEl (VOp (OpSetDelegate $ SetDelegate Nothing globalCounter)) :& r
runInstrImpl _ (AnnCREATE_CONTRACT _ contract)
  (StkEl (VOption mbKeyHash) :& StkEl (VMutez m) :& StkEl g :& r) = do
  originator <- ceSelf <$> ask
  opHash <- ceOperationHash <$> ask
  incrementCounter
  globalCounter <- isGlobalCounter <$> getInterpreterState
  let resAddr =
        case opHash of
          Just hash -> mkContractAddress hash globalCounter
          Nothing ->
            mkContractAddress
              (mkOriginationOperationHash $
                  createOrigOp originator Nothing mbKeyHash m contract g globalCounter
              )
              -- If opHash is Nothing it means that interpreter is running in some kind of test
              -- context, therefore we generate dummy contract address with its own origination
              -- operation.
              globalCounter
  let resEpAddr = EpAddress resAddr DefEpName
  let resOp = CreateContract
        (Constrained originator) (unwrapMbKeyHash mbKeyHash) m g contract globalCounter
  pure $ StkEl (VOp (OpCreateContract resOp))
      :& StkEl (VAddress resEpAddr)
      :& r
runInstrImpl _ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash k) :& r) =
  pure $ (StkEl (VContract (MkAddress $ ImplicitAddress k) sepcPrimitive)) :& r
runInstrImpl _ AnnNOW{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VTimestamp ceNow) :& r
runInstrImpl _ AnnAMOUNT{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VMutez ceAmount) :& r
runInstrImpl _ AnnBALANCE{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VMutez ceBalance) :& r
runInstrImpl _ AnnVOTING_POWER{} (StkEl (VKeyHash k) :& r) = do
  ContractEnv{..} <- ask
  pure $ StkEl (VNat $ vpPick k ceVotingPowers) :& r
runInstrImpl _ AnnTOTAL_VOTING_POWER{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VNat $ vpTotal ceVotingPowers) :& r
runInstrImpl _ AnnCHECK_SIGNATURE{}
  (StkEl (VKey k) :& StkEl (VSignature v) :& StkEl (VBytes b) :& r) =
  pure $ StkEl (VBool $ checkSignature k v b) :& r
runInstrImpl _ AnnSHA256{} (StkEl (VBytes b) :& r) =
  pure $ StkEl (VBytes $ sha256 b) :& r
runInstrImpl _ AnnSHA512{} (StkEl (VBytes b) :& r) =
  pure $ StkEl (VBytes $ sha512 b) :& r
runInstrImpl _ AnnBLAKE2B{} (StkEl (VBytes b) :& r) =
  pure $ StkEl (VBytes $ blake2b b) :& r
runInstrImpl _ AnnSHA3{} (StkEl (VBytes b) :& r) =
  pure $ StkEl (VBytes $ sha3 b) :& r
runInstrImpl _ AnnKECCAK{} (StkEl (VBytes b) :& r) =
  pure $ StkEl (VBytes $ keccak b) :& r
runInstrImpl _ AnnHASH_KEY{} (StkEl (VKey k) :& r) =
  pure $ StkEl (VKeyHash $ hashKey k) :& r
runInstrImpl _ AnnPAIRING_CHECK{} (StkEl (VList pairs) :& r) = do
  let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]
  pure $ StkEl (VBool $ checkPairing pairs') :& r
runInstrImpl _ AnnSOURCE{} r = do
  ContractEnv{ceSource=Constrained ceSource} <- ask
  pure $ StkEl (VAddress $ EpAddress ceSource DefEpName) :& r
runInstrImpl _ AnnSENDER{} r = do
  ContractEnv{ceSender=Constrained ceSender} <- ask
  pure $ StkEl (VAddress $ EpAddress ceSender DefEpName) :& r
runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =
  pure $ StkEl (VAddress $ EpAddress' a (sepcName sepc)) :& r
runInstrImpl _ AnnCHAIN_ID{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VChainId ceChainId) :& r
runInstrImpl _ AnnLEVEL{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VNat ceLevel) :& r
runInstrImpl _ AnnSELF_ADDRESS{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VAddress $ EpAddress ceSelf DefEpName) :& r
runInstrImpl _ AnnTICKET{} (StkEl dat :& StkEl (VNat am) :& r) = do
  ContractEnv{..} <- ask
  let result = VOption do
        guard (am /= 0)
        pure $ VTicket (MkAddress ceSelf) dat am
  pure $ StkEl (result) :& r
runInstrImpl _ AnnTICKET_DEPRECATED{} (StkEl dat :& StkEl (VNat am) :& r) = do
  ContractEnv{..} <- ask
  pure $ StkEl (VTicket (MkAddress ceSelf) dat am) :& r
runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do
  pure $
    StkEl
      (VPair (VAddress (EpAddress' addr DefEpName), (VPair (dat, VNat am))))
    :& te :& r
runInstrImpl _ AnnSPLIT_TICKET{}
    (StkEl tv@(VTicket addr dat am) :&
     StkEl (VPair (VNat am1, VNat am2)) :& r) = do
  let result = withValueTypeSanity tv $ VOption do
        guard (am1 + am2 == am)
        return $ VPair (VTicket addr dat am1, VTicket addr dat am2)
  pure $ StkEl result :& r
runInstrImpl _ AnnJOIN_TICKETS{}
  (StkEl (VPair (tv1@(VTicket addr1 dat1 am1), VTicket addr2 dat2 am2)) :& r) = do
  let result = withValueTypeSanity tv1 $ VOption do
        guard (addr1 == addr2)
        guard (dat1 == dat2)
        return $ VTicket addr1 dat1 (am1 + am2)
  pure $ StkEl result :& r
runInstrImpl _ AnnOPEN_CHEST{}
  (StkEl (VChestKey ck) :& StkEl (VChest c) :& StkEl (VNat nat) :& r) = do
  let result = case mkTLTime nat of
        Right time -> case openChest c ck time of
          Correct bytes -> VOr (Left (VBytes bytes))
          BogusOpening  -> VOr (Right (VBool True))
          BogusCipher   -> VOr (Right (VBool False))
        Left _ -> VOr (Right (VBool True))
  pure $ StkEl result :& r
runInstrImpl _ AnnSAPLING_EMPTY_STATE{} _ = throwMichelson $ MichelsonUnsupported "SAPLING_EMPTY_STATE"
runInstrImpl _ AnnSAPLING_VERIFY_UPDATE{} _ = throwMichelson $ MichelsonUnsupported "SAPLING_VERIFY_UPDATE"
runInstrImpl _ AnnMIN_BLOCK_TIME{} r = do
  ContractEnv{..} <- ask
  pure $ StkEl (VNat ceMinBlockTime) :& r
runInstrImpl _ (AnnEMIT _ (unAnnotation -> emTag) mNotes) ((StkEl emValue) :& r) = do
  incrementCounter
  emCounter <- isGlobalCounter <$> getInterpreterState
  let emNotes = fromMaybe starNotes mNotes
  pure $ StkEl (VOp (OpEmit Emit{..})) :& r

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, EvalM' ext monad)
  => proxy aop
  -> StkEl n
  -> StkEl m
  -> monad (StkEl (ArithRes aop n m))
runArithOp op l r = case evalOp op (seValue l) (seValue r) of
  Left  err -> throwMichelson $ MichelsonArithError err
  Right res -> pure $ StkEl res

-- | Unpacks given raw data into a typed value.
runUnpack
  :: forall t. (UnpackedValScope t)
  => ByteString
  -> Either UnpackError (T.Value t)
runUnpack bs =
  -- TODO [TM-80]: Gas consumption here should depend on unpacked data size
  -- and size of resulting expression, errors would also spend some (all equally).
  -- Fortunately, the inner decoding logic does not need to know anything about gas use.
  unpackValue' bs

createOrigOp
  :: (ParameterScope param, StorageScope store, L1AddressKind kind)
  => KindedAddress kind
  -> Maybe ContractAlias
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> Contract param store
  -> Value' Instr store
  -> GlobalCounter
  -> OriginationOperation
createOrigOp originator mbAlias mbDelegate bal contract storage counter =
  OriginationOperation
    { ooOriginator = originator
    , ooDelegate = unwrapMbKeyHash mbDelegate
    , ooBalance = bal
    , ooStorage = storage
    , ooContract = contract
    , ooCounter = counter
    , ooAlias = mbAlias
    }

unwrapMbKeyHash :: Maybe (T.Value 'T.TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash mbKeyHash = mbKeyHash <&> \(VKeyHash keyHash) -> keyHash

interpretExt :: EvalM' ext m => InstrRunner m -> SomeItStack -> m ()
interpretExt _ (SomeItStack (T.PRINT (T.PrintComment pc)) st) = do
  let getEl (Left l) = l
      getEl (Right str) = withStackElem str st (pretty . seValue)
  tell . one $ mconcat (map getEl pc)

interpretExt runner (SomeItStack (T.TEST_ASSERT (T.TestAssert nm pc instr)) st) = do
  ost <- runInstrImpl runner instr st
  let ((seValue -> T.fromVal -> succeeded) :& _) = ost
  unless succeeded $ do
    interpretExt runner (SomeItStack (T.PRINT pc) st)
    throwMichelson $ MichelsonFailedTestAssert $ "TEST_ASSERT " <> nm <> " failed"

interpretExt _ (SomeItStack T.DOC_ITEM{} _) = pass
interpretExt _ (SomeItStack T.COMMENT_ITEM{} _) = pass
interpretExt _ (SomeItStack T.STACKTYPE{} _) = pass

-- | Access given stack reference (in CPS style).
withStackElem
  :: forall st a.
     T.StackRef st
  -> Rec StkEl st
  -> (forall t. StkEl t -> a)
  -> a
withStackElem (T.StackRef sn) vals cont =
  loop (vals, sn)
  where
    loop
      :: forall s (n :: Peano). (LongerThan s n)
      => (Rec StkEl s, PeanoNatural n) -> a
    loop = \case
      (e :& _, Zero) -> cont e
      (_ :& es, Succ n) -> loop (es, n)

assignBigMapIds' :: EvalM' ext m => Value t -> m (Value t)
assignBigMapIds' val = do
  bigMapCounter0 <- view isBigMapCounterL <$> getInterpreterState
  let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds True val) bigMapCounter0
  modifyInterpreterState (set isBigMapCounterL bigMapCounter1)
  pure storageWithIds

-- | All big_maps stored in a chain have a globally unique ID.
--
-- We use this function to assign a new ID whenever a big_map is created.
assignBigMapIds
  :: (MonadState BigMapCounter m)
  => Bool
  -- ^ If true, assign a new ID even if the bigmap already has one.
  -- Otherwise, assign IDs only to bigmaps that don't have one yet.
  -> Value t -> m (Value t)
assignBigMapIds overwriteExistingId =
  dfsTraverseValue def{ dsValueStep = \case
      VBigMap existingId vBigMap | overwriteExistingId || isNothing existingId -> do
        bigMapId <- bigMapCounter <<+= 1
        pure $ VBigMap (Just bigMapId) vBigMap
      v -> pure v
    }

incrementCounter :: (InterpreterStateMonad m) => m ()
incrementCounter = modifyInterpreterState $ \iState ->
      iState { isGlobalCounter = isGlobalCounter iState + 1 }

instance NFData ext => NFData (MichelsonFailed ext) where
  rnf = \case
    MichelsonFailedWith x -> rnf x
    MichelsonArithError x -> rnf x
    MichelsonGasExhaustion -> ()
    MichelsonFailedTestAssert x -> rnf x
    MichelsonUnsupported x -> rnf x
    MichelsonExt x -> rnf x

instance NFData ext => NFData (MichelsonFailureWithStack ext)