Interpret.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, containing function to interpret Michelson
-- instructions against given context and input stack.
module Michelson.Interpret
  ( ContractEnv (..)
  , InterpreterState (..)
  , isMorleyLogsL
  , MichelsonFailed (..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , noMorleyLogs
  , pickMorleyLogs

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , ContractReturn

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

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

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor, traverseOf, (<<+=))
import Control.Monad.Except (MonadError, throwError)
import Data.Default (Default(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Vinyl (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap)
import Fmt (Buildable(build), Builder, blockListF, prettyLn)

import Michelson.Interpret.Pack (packValue')
import Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Michelson.Runtime.GState
import Michelson.TypeCheck (SomeParamType(..), TcOriginatedContracts, matchTypes)
import Michelson.Typed hiding (Branch(..))
import qualified Michelson.Typed as T
import Michelson.Typed.Origination
  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)
import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (annQ)
import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..))
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, keccak, sha256, sha3, sha512)
import Tezos.Crypto.BLS12381 (checkPairing)
import Util.Peano (LongerThan, Peano)
import Util.PeanoNatural (PeanoNatural(..))
import Util.Sing (eqParamSing)
import Util.TH
import Util.Type
import Util.Typeable

-- | Morley logs for interpreter state that are stored in reverse order.
newtype MorleyLogs = MorleyLogs [Text]
  deriving stock (Eq, Show, Generic)
  deriving newtype Default

pickMorleyLogs :: MorleyLogs -> [Text]
pickMorleyLogs (MorleyLogs logs) = reverse logs

instance Buildable MorleyLogs where
  build = blockListF . pickMorleyLogs

instance NFData MorleyLogs

noMorleyLogs :: MorleyLogs
noMorleyLogs = MorleyLogs []

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

instance NFData RemainingSteps

data InterpreterState = InterpreterState
  { isMorleyLogs :: MorleyLogs
  , isRemainingSteps :: RemainingSteps
  , isOriginationNonce :: OriginationIndex
  , isBigMapCounter :: BigMapCounter
  } deriving stock (Show, Generic)

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

data StkEl t = StkEl
  { seValue :: Value t
  , seVarAnn :: U.VarAnn
  , seNotes :: Notes t
  } deriving stock (Eq, Show)

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

starNotesStkEl :: forall t. Value t -> StkEl t
starNotesStkEl v = StkEl v U.noAnn $ withValueTypeSanity v $ starNotes @t

-- | 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 :: TcOriginatedContracts
  -- ^ Mapping from existing contracts' addresses to their executable
  -- representation.
  , ceSelf :: Address
  -- ^ Address of the interpreted contract.
  , ceSource :: Address
  -- ^ The contract that initiated the current transaction.
  , ceSender :: Address
  -- ^ The contract that initiated the current internal transaction.
  , 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.
  , ceGlobalCounter :: GlobalCounter
  -- ^ A global counter that is used to ensure newly created
  -- contracts have unique addresses.
  , ceLevel :: Natural
  -- ^ Number of blocks before the given one in the chain
  }

-- | Represents @[FAILED]@ state of a Michelson program. Contains
-- value that was on top of the stack when @FAILWITH@ was called.
data MichelsonFailed where
  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed
  MichelsonArithError
    :: (Typeable n, Typeable m, Typeable instr)
    => ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed
  MichelsonGasExhaustion :: MichelsonFailed
  MichelsonFailedTestAssert :: Text -> MichelsonFailed

deriving stock instance Show MichelsonFailed

instance Eq MichelsonFailed 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

instance Buildable MichelsonFailed where
  build =
    \case
      MichelsonFailedWith (v :: T.Value t) ->
        "Reached FAILWITH instruction with " <> formatValue v
      MichelsonArithError v -> build v
      MichelsonGasExhaustion ->
        "Gas limit exceeded on contract execution"
      MichelsonFailedTestAssert t -> build t
    where
      formatValue :: forall t . SingI t => Value t -> Builder
      formatValue v =
        case T.checkOpPresence (sing @t) of
          OpPresent -> "<value with operations>"
          OpAbsent -> build (untypeValue v)

newtype InterpretError = InterpretError (MichelsonFailed, MorleyLogs)
  deriving stock (Generic)

deriving stock instance Show InterpretError

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

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

deriving stock instance Show InterpretResult

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

type ContractReturn st =
  (Either MichelsonFailed ([Operation], T.Value st), InterpreterState)

handleContractReturn
  :: (StorageScope st)
  => ContractReturn st -> Either InterpretError InterpretResult
handleContractReturn (ei, s) =
  bimap (InterpretError . (, isMorleyLogs s)) (constructIR . (, s)) 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 starNotesStkEl

-- | 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 cCode $ mkInitStack (liftCallArg epc param) cParamNotes initSt cStoreNotes)
    env
    ist

mkInitStack
  :: T.Value param
  -> T.ParamNotes param
  -> T.Value st
  -> T.Notes st
  -> Rec StkEl (ContractInp param st)
mkInitStack param T.UnsafeParamNotes{..} st stNotes = StkEl
  (T.VPair (param, st))
  U.noAnn
  (T.NTPair U.noAnn (U.convAnn pnRootAnn) U.noAnn [annQ|parameter|] [annQ|storage|] pnNotes stNotes)
    :& 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
  -> BigMapCounter
  -> ContractEnv
  -> ContractReturn st
interpret contract epc param initSt bmCounter env =
  interpret' contract epc param initSt env (initInterpreterState bmCounter env)

initInterpreterState :: BigMapCounter -> ContractEnv -> InterpreterState
initInterpreterState bmCounter env = InterpreterState def (ceMaxSteps env) (OriginationIndex 0) bmCounter

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

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

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

type EvalOp a =
  ExceptT MichelsonFailed
    (ReaderT ContractEnv
       (State InterpreterState)) a

runEvalOp
  :: EvalOp a
  -> ContractEnv
  -> InterpreterState
  -> (Either MichelsonFailed a, InterpreterState)
runEvalOp act env initSt =
  flip runState initSt $ usingReaderT env $ runExceptT act

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 InterpreterStateMonad (ExceptT MichelsonFailed $
                                ReaderT ContractEnv $
                                State InterpreterState) where
  stateInterpreterState f = lift $ lift $ state f

type EvalM m =
  ( MonadReader ContractEnv m
  , InterpreterStateMonad m
  , MonadError MichelsonFailed m
  )

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

-- | 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@(InstrWithNotes _ _ _i1) r = runInstrImpl runInstr i r
runInstr i@(InstrWithVarNotes _ _i1) r = runInstrImpl runInstr i r
runInstr i@(InstrWithVarAnns _ _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@(Fn _ _ _i1) r = runInstrImpl runInstr i r
runInstr i r = do
  rs <- isRemainingSteps <$> getInterpreterState
  if rs == 0
  then throwError 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.
runInstrImpl :: forall m. EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
runInstrImpl runner (WithLoc _ i) r = runner i r
runInstrImpl runner (InstrWithNotes (_ :: Proxy rest) notes instr) inp = do
  out <- runner instr inp
  let zipRec :: Rec Notes topElems -> Rec StkEl (topElems ++ rest) -> Rec StkEl (topElems ++ rest)
      zipRec RNil stkElems = stkElems
      zipRec (stkElemNotes :& xs) (stkElem :& ys) =
        stkElem { seNotes = stkElemNotes } :& zipRec xs ys
  pure $ zipRec notes out
runInstrImpl runner (InstrWithVarNotes _vns i) inp = runner i inp
runInstrImpl runner (InstrWithVarAnns vns i) inp = do
  runner i inp <&> \case
    StkEl v1 _ n1 :& StkEl v2 vn2 n2 :& r -> case vns of
      U.OneVarAnn vn      -> StkEl v1 vn n1 :& StkEl v2 vn2 n2 :& r
      U.TwoVarAnns vn vn' -> StkEl v1 vn n1 :& StkEl v2 vn' n2 :& r
    StkEl v _ n :& r -> case vns of
      U.OneVarAnn vn   -> StkEl v vn n :& r
      U.TwoVarAnns _ _ -> error "Input stack is exhausted but there is still a variable annotation."
    RNil -> error "Input stack is exhausted but there is still variables annotations."
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 runner (Fn _ _ i) r = runner i 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 _ DUP (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 _ (DUPN 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
        -- Discard variable annotations. This is consistent with tezos-client.
        pure $ (duplicateStkEl & seVarAnnL .~ U.noAnn) :& 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 _ SOME ((seValue -> a) :& r) =
  withValueTypeSanity a $
    pure $ starNotesStkEl (VOption (Just a)) :& r
runInstrImpl _ (PUSH v) r = pure $ starNotesStkEl v :& r
runInstrImpl _ NONE r = pure $ starNotesStkEl (VOption Nothing) :& r
runInstrImpl _ UNIT r = pure $ starNotesStkEl VUnit :& r
runInstrImpl runner (IF_NONE _bNone bJust) (StkEl (VOption (Just a)) vn (NTOption _ n) :& r) =
  runner bJust (StkEl a vn n :& 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 $ starNotesStkEl (VPair (a, b)) :& r
runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b)) _ _) :& r) =
  pure $ starNotesStkEl a :& starNotesStkEl b :& r
runInstrImpl _ (PAIRN 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
      starNotesStkEl (VPair (a, b)) :& r
    go (Succ n@(Succ (Succ _))) (StkEl a _ _ :& r@(_ :& _ :& _)) =
      -- if n>2
      case go n r of
        StkEl combed _ _ :& r' ->
            starNotesStkEl (VPair (a, combed)) :& r'
runInstrImpl _ (UNPAIRN s) (StkEl pair0 _ pairNotes0 :& r) = do
  pure $ go s pair0 pairNotes0 <+> r
  where
    go
      :: forall n pair. ConstraintUnpairN n pair
      => PeanoNatural n -> Value pair -> Notes pair
      -> Rec StkEl (UnpairN n pair)
    go n pair pairNotes =
      case (n, pair, pairNotes) of
        -- if n=2
        (Succ (Succ Zero), VPair (a, b), NTPair _ aFieldAnn bFieldAnn _ _ aNotes bNotes) ->
          -- @UNPAIR n@ converts field annotations into var annotations.
          --
          -- > /* [ @pair pair (int %aa) (int %bb) (int %cc) (int %dd) ] */ ;
          -- > UNPAIR 3
          -- > /* [ @aa int : @bb int : pair (int %cc) (int %dd) ] */ ;
          --
          -- Nested var annotations will be discarded.
          --
          -- > /* [ pair (int @c) (int @a) (int @b) ] */ ;
          -- UNPAIR 3
          -- /* [ int : int : int ] */ ;
          StkEl a (U.convAnn @U.FieldTag @U.VarTag aFieldAnn) aNotes
            :& StkEl b (U.convAnn @U.FieldTag @U.VarTag bFieldAnn) bNotes
            :& RNil
        -- if n>2
        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _)), NTPair _ aFieldAnn _ _ _ aNotes bNotes) ->
          StkEl a (U.convAnn @U.FieldTag @U.VarTag aFieldAnn) aNotes
            :& go n' b bNotes
runInstrImpl _ (AnnCAR _ _) (StkEl (VPair (a, _b)) _ _ :& r) = pure $ starNotesStkEl a :& r
runInstrImpl _ (AnnCDR _ _) (StkEl (VPair (_a, b)) _ _ :& r) = pure $ starNotesStkEl b :& r
runInstrImpl _ (AnnLEFT nt nf1 nf2) ((StkEl a _ na) :& r) =
  withValueTypeSanity a $
    pure $ StkEl (VOr $ Left a) U.noAnn (NTOr nt nf1 nf2 na starNotes) :& r
runInstrImpl _ (AnnRIGHT nt nf1 nf2) ((StkEl b _ nb) :& r) =
  withValueTypeSanity b $
    pure $ StkEl (VOr $ Right b) U.noAnn (NTOr nt nf1 nf2 starNotes nb) :& r
runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) vn (NTOr _ _ _ nl _) :& r) =
  runner bLeft (StkEl a vn nl :& r)
runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) vn (NTOr _ _ _ _ nr) :& r) =
  runner bRight (StkEl a vn nr :& r)
runInstrImpl _ NIL r = pure $ starNotesStkEl (VList []) :& r
runInstrImpl _ CONS (a :& StkEl (VList l) _ _ :& r) = pure $ starNotesStkEl (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)) vn ntl@(NTList _ nhd) :& r) =
  runner bCons (StkEl lh vn nhd :& StkEl (VList lr) vn ntl :& r)
runInstrImpl _ SIZE (a :& r) = pure $ starNotesStkEl (VNat $ (fromInteger . toInteger) $ evalSize $ seValue a) :& r
runInstrImpl _ EMPTY_SET r = pure $ starNotesStkEl (VSet Set.empty) :& r
runInstrImpl _ EMPTY_MAP r = pure $ starNotesStkEl (VMap Map.empty) :& r
runInstrImpl _ EMPTY_BIG_MAP r = do
  bigMap <- assignBigMapIds' $ VBigMap Nothing Map.empty
  pure $ starNotesStkEl bigMap :& r
runInstrImpl runner (MAP (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl a vn n :& 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 vn (mapOpNotes n)) <$> mapOpToList @c a)
  pure $ starNotesStkEl (mapOpFromList a (reverse newList)) :& newStack
runInstrImpl runner (ITER (code :: Instr (IterOpEl c ': s) s)) (StkEl a vn n :& r) =
  case iterOpDetachOne @c a of
    (Just x, xs) -> do
      res <- runner code (StkEl x vn (iterOpNotes n) :& r)
      runner (ITER code) (StkEl xs vn n :& res)
    (Nothing, _) -> pure r
runInstrImpl _ MEM (a :& b :& r) = pure $ starNotesStkEl (VBool (evalMem (seValue a) (seValue b))) :& r
runInstrImpl _ GET (a :& b :& r) = pure $ starNotesStkEl (VOption (evalGet (seValue a) (seValue b))) :& r
runInstrImpl _ (GETN s) (StkEl pair _ _ :& r) = do
  pure $ starNotesStkEl (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 _ UPDATE (a :& b :& StkEl c _ _ :& r) =
  pure $ starNotesStkEl (evalUpd (seValue a) (seValue b) c) :& r
runInstrImpl _ (UPDATEN s) (StkEl (val :: Value val) _ _  :& StkEl pair _ _ :& r) = do
  pure $ starNotesStkEl (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 _ GET_AND_UPDATE (StkEl key _ _ :& StkEl valMb _ _ :& StkEl collection _ _ :& r) =
  pure $
    starNotesStkEl (VOption (evalGet key collection))
    :& starNotesStkEl (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 $ starNotesStkEl a :& r
runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) vn (NTOr _ _ _ nl _) :& r) = do
  res <- runner ops (StkEl a vn nl :& r)
  runner (LOOP_LEFT ops) res
runInstrImpl _ (LAMBDA lam) r = pure $ starNotesStkEl lam :& r
runInstrImpl runner EXEC (a :& StkEl (VLam (T.rfAnyInstr -> lBody)) _ _ :& r) = do
  res <- runner lBody (a :& RNil)
  pure $ res <+> r
runInstrImpl _ APPLY (StkEl (a :: T.Value a) _ _ :& StkEl (VLam lBody) _ _ :& r) = do
  pure $ starNotesStkEl (VLam (T.rfMapAnyInstr doApply lBody)) :& 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 :& _) = throwError $ MichelsonFailedWith (seValue a)
runInstrImpl _ CAST (StkEl a _ _ :& r) = pure $ starNotesStkEl a :& r
runInstrImpl _ RENAME (StkEl a _ _ :& r) = pure $ starNotesStkEl a :& r
runInstrImpl _ PACK ((seValue -> a) :& r) = pure $ starNotesStkEl (VBytes $ packValue' a) :& r
runInstrImpl _ UNPACK (StkEl (VBytes a) _ _ :& r) =
  pure $ starNotesStkEl (VOption . rightToMaybe $ runUnpack a) :& r
runInstrImpl _ CONCAT (a :& b :& r) = pure $ starNotesStkEl (evalConcat (seValue a) (seValue b)) :& r
runInstrImpl _ CONCAT' (StkEl (VList a) _ _ :& r) = pure $ starNotesStkEl (evalConcat' a) :& r
runInstrImpl _ SLICE (StkEl (VNat o) _ _ :& StkEl (VNat l) _ _ :& StkEl s _ _ :& r) =
  pure $ starNotesStkEl (VOption (evalSlice o l s)) :& r
runInstrImpl _ ISNAT (StkEl (VInt i) _ _ :& r) =
  if i < 0
  then pure $ starNotesStkEl (VOption Nothing) :& r
  else pure $ starNotesStkEl (VOption (Just (VNat $ fromInteger i))) :& r
runInstrImpl _ ADD (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Add) l r
runInstrImpl _ SUB (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Sub) l r
runInstrImpl _ MUL (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Mul) l r
runInstrImpl _ EDIV (l :& r :& rest) = pure $ starNotesStkEl (evalEDivOp (seValue l) (seValue r)) :& rest
runInstrImpl _ ABS ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Abs) a) :& rest
runInstrImpl _ NEG ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Neg) a) :& rest
runInstrImpl _ LSL (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsl) x s
runInstrImpl _ LSR (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsr) x s
runInstrImpl _ OR (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Or) l r
runInstrImpl _ AND (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @And) l r
runInstrImpl _ XOR (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Xor) l r
runInstrImpl _ NOT ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Not) a) :& rest
runInstrImpl _ COMPARE ((seValue -> l) :& (seValue -> r) :& rest) =
  pure $ starNotesStkEl (T.VInt (compareOp l r)) :& rest
runInstrImpl _ EQ ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Eq') a) :& rest
runInstrImpl _ NEQ ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Neq) a) :& rest
runInstrImpl _ LT ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Lt) a) :& rest
runInstrImpl _ GT ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Gt) a) :& rest
runInstrImpl _ LE ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Le) a) :& rest
runInstrImpl _ GE ((seValue -> a) :& rest) =
  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Ge) a) :& rest
runInstrImpl _ INT (StkEl a _ _ :& r) =
  pure $ starNotesStkEl (evalToIntOp a) :& r
runInstrImpl _ (SELF sepc :: Instr inp out) r = do
  ContractEnv{..} <- ask
  case Proxy @out of
    (_ :: Proxy ('TContract cp ': s)) -> do
      pure $ starNotesStkEl (VContract ceSelf sepc) :& r
runInstrImpl _ (CONTRACT (nt :: T.Notes a) instrEpName) (StkEl (VAddress epAddr) _ _ :& r) = do
  ContractEnv{..} <- ask
  let T.EpAddress addr addrEpName = 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 U.noAnn (NTOption U.noAnn $ NTContract U.noAnn nt) :& r
  pure $ withNotes $ case mepName of
    Nothing -> VOption Nothing
    Just epName ->
      case addr of
        KeyAddress _ -> castContract addr epName T.tyImplicitAccountParam
        ContractAddress ca ->
          case Map.lookup ca ceContracts of
            Just (SomeParamType _ paramNotes) -> castContract addr epName paramNotes
            Nothing -> VOption Nothing
  where
  castContract
    :: forall p. T.ParameterScope p
    => Address -> 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 na epc <- T.mkEntrypointCall epName param
    Right (Refl, _) <- pure $ matchTypes nt na
    return $ VContract addr (T.SomeEpc epc)

runInstrImpl _ TRANSFER_TOKENS
  (StkEl p _ _ :& StkEl (VMutez mutez) _ _ :& StkEl contract _ _ :& r) =
  pure $ starNotesStkEl (VOp (OpTransferTokens $ TransferTokens p mutez contract)) :& r
runInstrImpl _ SET_DELEGATE (StkEl (VOption mbKeyHash) _ _ :& r) =
  case mbKeyHash of
    Just (VKeyHash k) -> pure $ starNotesStkEl (VOp (OpSetDelegate $ SetDelegate $ Just k)) :& r
    Nothing -> pure $ starNotesStkEl (VOp (OpSetDelegate $ SetDelegate $ Nothing)) :& r
runInstrImpl _ (CREATE_CONTRACT contract)
  (StkEl (VOption mbKeyHash) _ _ :& StkEl (VMutez m) _ _ :& StkEl g _ _ :& r) = do
  originator <- ceSelf <$> ask

  originationNonce <- isOriginationNonce <$> getInterpreterState
  globalCounter <- asks ceGlobalCounter
  opHash <- ceOperationHash <$> ask
  modifyInterpreterState $ \iState ->
    iState { isOriginationNonce = OriginationIndex $ (unOriginationIndex $ isOriginationNonce iState) + 1 }
  let ops = cCode contract
  let resAddr =
        case opHash of
          Just hash -> mkContractAddress hash originationNonce globalCounter
          Nothing ->
            mkContractAddress
              (mkOriginationOperationHash (createOrigOp originator mbKeyHash m contract g))
              -- 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.
              originationNonce
              globalCounter
  let resEpAddr = EpAddress resAddr DefEpName
  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g ops
  pure $ starNotesStkEl (VOp (OpCreateContract resOp))
      :& starNotesStkEl (VAddress resEpAddr)
      :& r
runInstrImpl _ IMPLICIT_ACCOUNT (StkEl (VKeyHash k) _ _ :& r) =
  pure $ (starNotesStkEl (VContract (KeyAddress k) sepcPrimitive)) :& r
runInstrImpl _ NOW r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VTimestamp ceNow) :& r
runInstrImpl _ AMOUNT r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VMutez ceAmount) :& r
runInstrImpl _ BALANCE r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VMutez ceBalance) :& r
runInstrImpl _ VOTING_POWER (StkEl (VKeyHash k) _ _ :& r) = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VNat $ vpPick k ceVotingPowers) :& r
runInstrImpl _ TOTAL_VOTING_POWER r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VNat $ vpTotal ceVotingPowers) :& r
runInstrImpl _ CHECK_SIGNATURE
  (StkEl (VKey k) _ _ :& StkEl (VSignature v) _ _ :& StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBool $ checkSignature k v b) :& r
runInstrImpl _ SHA256 (StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBytes $ sha256 b) :& r
runInstrImpl _ SHA512 (StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBytes $ sha512 b) :& r
runInstrImpl _ BLAKE2B (StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBytes $ blake2b b) :& r
runInstrImpl _ SHA3 (StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBytes $ sha3 b) :& r
runInstrImpl _ KECCAK (StkEl (VBytes b) _ _ :& r) =
  pure $ starNotesStkEl (VBytes $ keccak b) :& r
runInstrImpl _ HASH_KEY (StkEl (VKey k) _ _ :& r) =
  pure $ starNotesStkEl (VKeyHash $ hashKey k) :& r
runInstrImpl _ PAIRING_CHECK (StkEl (VList pairs) _ _ :& r) = do
  let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]
  pure $ starNotesStkEl (VBool $ checkPairing pairs') :& r
runInstrImpl _ SOURCE r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VAddress $ EpAddress ceSource DefEpName) :& r
runInstrImpl _ SENDER r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VAddress $ EpAddress ceSender DefEpName) :& r
runInstrImpl _ ADDRESS (StkEl (VContract a sepc) _ _ :& r) =
  pure $ starNotesStkEl (VAddress $ EpAddress a (sepcName sepc)) :& r
runInstrImpl _ CHAIN_ID r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VChainId ceChainId) :& r
runInstrImpl _ LEVEL r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VNat ceLevel) :& r
runInstrImpl _ SELF_ADDRESS r = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VAddress $ EpAddress ceSelf DefEpName) :& r
runInstrImpl _ TICKET (StkEl dat _ _ :& StkEl (VNat am) _ _ :& r) = do
  ContractEnv{..} <- ask
  pure $ starNotesStkEl (VTicket ceSelf dat am) :& r
runInstrImpl _ READ_TICKET (te@(StkEl (VTicket addr dat am) _ _) :& r) = do
  pure $
    starNotesStkEl
      (VPair (VAddress (EpAddress addr DefEpName), (VPair (dat, VNat am))))
    :& te :& r
runInstrImpl _ SPLIT_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 $ starNotesStkEl result :& r
runInstrImpl _ JOIN_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 $ starNotesStkEl result :& r

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, EvalM 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 -> throwError (MichelsonArithError err)
  Right res -> pure $ starNotesStkEl 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)
  => Address
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> Contract param store
  -> Value' Instr store
  -> OriginationOperation
createOrigOp originator mbDelegate bal contract storage =
  OriginationOperation
    { ooOriginator = originator
    , ooDelegate = unwrapMbKeyHash mbDelegate
    , ooBalance = bal
    , ooStorage = storage
    , ooContract = contract
    }

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

interpretExt :: EvalM 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 (show . seValue)
      getMorleyLogs (MorleyLogs logs) = logs
  modifyInterpreterState (\s -> s {isMorleyLogs = MorleyLogs $ mconcat (map getEl pc) : getMorleyLogs (isMorleyLogs s)})

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)
    throwError $ 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 m => Value t -> m (Value t)
assignBigMapIds' val = do
  bigMapCounter0 <- view isBigMapCounterL <$> getInterpreterState
  let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds 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 => Value t -> m (Value t)
assignBigMapIds =
  dfsTraverseValue \case
    VBigMap _ vBigMap -> do
      bigMapId <- bigMapCounter <<+= 1
      pure $ VBigMap (Just bigMapId) vBigMap
    v -> pure v

(deriveGADTNFData ''MichelsonFailed)