-- 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
  , ContractEnv' (..)
  , InterpreterState (..)
  , MichelsonFailed (..)
  , MichelsonFailureWithStack(..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , buildMorleyLogs
  , MorleyLogsBuilder (..)

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , InterpretReturn
  , ContractReturn
  , RunEvalOpReturn
  , ResultStateLogs(..)

  , mkInitStack
  , InterpretError (..)
  , InterpretResult
  , ContractResult
  , extractValOps
  , EvalM
  , EvalM'
  , InterpreterStateMonad (..)
  , StkEl (.., StkEl)
  , NoStkElMeta(..)
  , seValueL
  , seMetaL
  , InstrRunner
  , runInstr
  , runInstrNoGas
  , runUnpack

    -- * Views
  , ViewLookupError (..)
  , interpretView
  , getViewByName
  , getViewByNameAndType

    -- * Internals
  , initInterpreterState
  , handleReturn
  , runEvalOp
  , runInstrImpl
  , assignBigMapIds
  , mapToStkEl
  , mapToValue
  , mkStkEl
  , mkDuplicateStkEl
  , runEvalOpT
  , interpret'
  , interpretView'
  , StkElMeta(..)
  , EvalOpT (..)
  , EvalOp

    -- * Prisms
  , _MorleyLogs
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor, makePrisms, (<<+=))
import Control.Monad.Except (MonadError, liftEither, throwError)
import Control.Monad.RWS.Strict (RWST, runRWST)
import Control.Monad.Writer (MonadWriter, WriterT, tell)
import Data.Default (Default(..))
import Data.GADT.Compare (GEq(..))
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Singletons (demote)
import Data.Singletons.Decide (decideEquality)
import Data.Vinyl (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap, rtraverse)
import Fmt
  (Buildable(build), blockListF, nameF, pretty, quoteOrIndentF, (++|), (+|), (|+), (|++), (|++^))
import Unsafe qualified (fromIntegral)

import Morley.Michelson.ErrorPos
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.Instr.Constraints
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.Lens
import Morley.Util.MismatchError
import Morley.Util.Peano (LongerThan, Peano)
import Morley.Util.PeanoNatural (PeanoNatural(..))
import Morley.Util.Sing (eqParamSing)
import Morley.Util.Typeable

{- $setup
>>> import Morley.Michelson.ErrorPos
>>> import Morley.Michelson.Typed
>>> import Fmt (pretty)
-}

-- | 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

-- | Represents a value on the stack. Aside from the value itself, it contains
-- arbitrary user-defined metadata. The metadata in question is defined by
-- 'StkElMeta' type class, the interpreter doesn't know anything about it.
--
-- The metadata should not be copied between different stack elements, the only
-- case where it can be copied is when the stack element is copied in its
-- entirety, i.e. when running instructions like @DUP@.
--
-- To create a new t'StkEl' from a value, 'mkStkEl' should always be used. For
-- duplicated stack elements, 'mkDuplicateStkEl' should be used instead, to
-- still give the user an option to override metadata for the duplicated
-- element.
--
-- The data constructor should almost never be used by itself.
data StkEl meta t = MkStkEl
  { seMeta :: meta t
  , seValue :: Value t
  } deriving stock (Eq, Show)

makeLensesWith postfixLFields ''StkEl

instance (forall t. Eq (meta t)) => GEq (StkEl meta) where
  geq se1 se2
    | Just Refl <- geq (seValue se1) (seValue se2)
    , seMeta se1 == seMeta se2
    = Just Refl
    | otherwise = Nothing

-- | Arbitrary stack element metadata that can be constructed in a particular
-- monad. Interpreter doesn't know anything about metadata, and doesn't try to
-- do anything with it. 'mkStkElMeta' describes how to construct metadata for
-- new stack elements based on its value. When a stack element is duplicated,
-- specifically with instructions like @DUP@, old metadata is passed to
-- 'mkStkElMeta' to provide an opportunity to modify it. Implementation is free
-- to either copy it verbatim or ignore the old and generate new.
--
-- See t'StkEl' documentation for an overview of the motivation and design.
type StkElMeta :: (T -> Type) -> (Type -> Type) -> Constraint
class (forall t. Eq (meta t), forall t. Show (meta t)) => StkElMeta meta m where
  -- | How to construct new metadata.
  mkStkElMeta
    :: Maybe (meta t)
    -- ^ For instructions duplicating the value, this @Just meta@ from the
    -- original instruction, @Nothing@ otherwise
    -> Value t
    -- ^ The value for the new stack element.
    -> m (meta t)

-- | Default metadata that does nothing.
data NoStkElMeta t = NoStkElMeta
  deriving stock (Eq, Show)

instance Applicative m => StkElMeta NoStkElMeta m where
  mkStkElMeta _ _ = pure NoStkElMeta

-- | Make an entirely new t'StkEl' from a value.
mkStkEl :: forall meta t m. (Applicative m, StkElMeta meta m) => Value t -> m (StkEl meta t)
mkStkEl val = flip MkStkEl val <$> mkStkElMeta Nothing val

-- | Make a duplicate t'StkEl', constructing metadata via 'mkStkElMeta'.
mkDuplicateStkEl
  :: forall meta t m. (Applicative m, StkElMeta meta m)
  => StkEl meta t -> m (StkEl meta t)
mkDuplicateStkEl MkStkEl{..} = flip MkStkEl seValue <$> mkStkElMeta (Just seMeta) seValue

pattern StkEl :: Value t -> StkEl meta t
pattern StkEl x <- MkStkEl _ x
{-# COMPLETE StkEl #-}

-- | Helper function to convert a record of @Value@ to @StkEl@.
mapToStkEl
  :: forall meta inp m. (Applicative m, StkElMeta meta m)
  => Rec Value inp -> m (Rec (StkEl meta) inp)
mapToStkEl = rtraverse $ mkStkEl

-- | Helper function to convert a record of @StkEl@ to @Value@.
mapToValue :: Rec (StkEl meta) inp -> Rec Value inp
mapToValue = rmap seValue

type ContractEnv :: Type
type ContractEnv = ContractEnv' EvalOp

-- | Environment for contract execution. Parametrized by the execution monad,
-- i.e. 'EvalOp' by default, but downstream consumers may define their own if
-- using low-level runners.
data ContractEnv' m = 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 :: ContractAddress -> m (Maybe 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
  , ceMetaWrapper :: forall i o. Instr i o -> Instr i o
  -- ^ Saves outer wrapping 'Meta' and 'WithLoc' while traversing the tree,
  -- used internally when reiterating on 'LOOP' and other similar instructions.
  -- If unsure, initialize it with 'id'.
  }

-- | 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) => 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" ++| quoteOrIndentF 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)

{- | Pretty-printer for 'MichelsonFailureWithStack'.

>>> let pos = ErrorSrcPos $ SrcPos (Pos 123) (Pos 456)
>>> let largeValue = VList $ replicate 10 VUnit

>>> pretty $ MichelsonFailureWithStack @Void MichelsonGasExhaustion pos
Gas limit exceeded on contract execution at line 124 char 457.

>>> pretty $ MichelsonFailureWithStack @Void (MichelsonFailedWith VUnit) pos
Reached FAILWITH instruction with 'Unit' at line 124 char 457.

>>> pretty $ MichelsonFailureWithStack @Void (MichelsonFailedWith largeValue) pos
Reached FAILWITH instruction with
  { Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit }
at line 124 char 457.

>>> pretty $ MichelsonFailureWithStack @Void (MichelsonFailedWith $ VPair (largeValue, largeValue)) pos
Reached FAILWITH instruction with
  Pair
    { Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit }
    { Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit; Unit }
at line 124 char 457.
-}
instance Buildable ext => Buildable (MichelsonFailureWithStack ext) where
  build (MichelsonFailureWithStack err loc)
    | SrcPos (Pos row) (Pos col) <- unErrorSrcPos loc
    = "" ++| err |++ "at line" ++| build (row + 1) |++ "char" ++| build (col + 1) <> "." |++ ""

data InterpretError ext = InterpretError
  { ieLogs :: MorleyLogs
  , ieFailure :: MichelsonFailureWithStack ext
  } deriving stock (Generic)

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

instance Buildable ext => Buildable (InterpretError ext) where
  build InterpretError{..} = pretty ieFailure

data ResultStateLogs res = ResultStateLogs
  { rslResult :: res
  , rslState :: InterpreterState
  , rslLogs :: MorleyLogs
  } deriving stock (Functor, Foldable, Traversable, Show, Generic)
    deriving anyclass NFData

-- | Pure result of an interpretation, i.e. return value, final interpreter
-- state and execution logs.
type InterpretResult ty = ResultStateLogs (Value ty)

-- | Pure result of contract interpretation. A specialized version of
-- 'InterpretResult'.
type ContractResult ty = InterpretResult (ContractOut1 ty)

-- | Result of 'runEvalOp'. Essentially, return value (possibly failing), state
-- and logs.
type RunEvalOpReturn a = ResultStateLogs (Either (MichelsonFailureWithStack Void) a)

-- | Result of 'interpretView'. A version of 'RunEvalOpReturn' specialized to 'Value'.
type InterpretReturn ty = RunEvalOpReturn (Value ty)

-- | Result of 'interpret'. A version of 'InterpretReturn' specialized to 'ContractOut1'.
type ContractReturn st = InterpretReturn (ContractOut1 st)

-- | On failure, attach logs to failure, but throw away the final state.
handleReturn
  :: InterpretReturn res
  -> Either (InterpretError Void) (ResultStateLogs (Value res))
handleReturn rsl@ResultStateLogs{..} = first (InterpretError rslLogs) . sequence $ rsl

-- | Reset 'ceMetaWrapper` after it is used with an instr.
withMetaWrapper :: forall ext meta m. EvalM' ext m => InstrRunner meta m -> InstrRunner meta m
withMetaWrapper runner instr s = do
  ContractEnv{ceMetaWrapper} <- ask
  local (\env -> env {ceMetaWrapper = id}) $
    runner (ceMetaWrapper instr) s

-- | Extract list of operations from 'ContractOut1' 'Value'.
extractValOps :: Value (ContractOut1 st) -> ([Operation], Value st)
extractValOps (VPair x) = first fromVal x

interpret'
  :: forall cp st arg m. (Monad m)
  => Contract cp st
  -> EntrypointCallT cp arg
  -> Value arg
  -> Value st
  -> ContractEnv' (EvalOpT m)
  -> InterpreterState
  -> m (ContractReturn st)
interpret' Contract{..} epc param initSt env ist = (fmap . fmap) (\(StkEl val :& RNil) -> val) <$>
  runEvalOpT
    (runInstr (unContractCode cCode) =<< mapToStkEl @NoStkElMeta initStack)
    env
    ist
  where
    initStack = mkInitStack (liftCallArg epc param) initSt

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

interpret
  :: Contract cp st
  -> EntrypointCallT cp arg
  -> Value arg
  -> Value st
  -> GlobalCounter
  -> BigMapCounter
  -> ContractEnv
  -> ContractReturn st
interpret contract epc param initSt globalCounter bmCounter env = runIdentity $
  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 Value inp
  -> Either (MichelsonFailureWithStack Void) (Rec 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 Value inp
  -> Either (MichelsonFailureWithStack Void) (Rec (StkEl NoStkElMeta) out)
interpretInstrAnnotated env instr inpSt =
  rslResult $
  runEvalOp
    (runInstr instr =<< mapToStkEl @NoStkElMeta inpSt)
    env
    InterpreterState
      { isRemainingSteps = 9999999999
      , isBigMapCounter = 0
      , isGlobalCounter = 0
      }

data SomeItStack meta where
  SomeItStack :: ExtInstr inp -> Rec (StkEl meta) inp -> SomeItStack meta

-- | The main interpreter monad, used by the higher-level functions like
-- 'interpret' and 'interpretView'.
--
-- Downstream consumers which use 'runInstrImpl' directly may define their own
-- monad similar to this one, or alternatively use 'EvalOpT' with the slightly
-- lower-level functions, e.g. `interpret'` and `interpretView'`.
type EvalOp = EvalOpT Identity

-- | The main interpreter monad transformer. Provides a more convenient way of
-- enriching the interpreter monad without redefining it entirely.
--
-- This is a newtype and not a type synonym due to the reader environment, i.e.
-- t'ContractEnv', being parameterized by the interpreter monad.
newtype EvalOpT m a = EvalOpT
  (ExceptT (MichelsonFailureWithStack Void)
    (RWST (ContractEnv' (EvalOpT m)) MorleyLogsBuilder InterpreterState m) a)
  deriving newtype
    ( MonadError (MichelsonFailureWithStack Void)
    , MonadState InterpreterState
    , InterpreterStateMonad
    , MonadWriter MorleyLogsBuilder
    , MonadReader (ContractEnv' (EvalOpT m))
    , Monad
    , Applicative
    , Functor
    , MonadIO
    )

instance MonadTrans EvalOpT where
  lift = EvalOpT . lift . lift

runEvalOp :: EvalOp a -> ContractEnv -> InterpreterState -> RunEvalOpReturn a
runEvalOp = runIdentity ... runEvalOpT

runEvalOpT
  :: Monad m
  => EvalOpT m a
  -> ContractEnv' (EvalOpT m)
  -> InterpreterState
  -> m (RunEvalOpReturn a)
runEvalOpT (EvalOpT act) env initSt = do
  (rslResult, rslState, buildMorleyLogs -> rslLogs) <- runRWST (runExceptT act) env initSt
  pure ResultStateLogs{..}

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) m
  , InterpreterStateMonad m
  , MonadWriter MorleyLogsBuilder m
  , MonadError (MichelsonFailureWithStack ext) m
  )

type EvalM m = EvalM' Void m

type InstrRunner meta m =
  forall inp out.
     Instr inp out
  -> Rec (StkEl meta) inp
  -> m (Rec (StkEl meta) 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 :: forall ext meta m. (StkElMeta meta m, EvalM' ext m) => InstrRunner meta 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 NoStkElMeta m
runInstrNoGas = runInstrImpl runInstrNoGas

(<:&>) :: Functor f => f (a r) -> Rec a rs -> f (Rec a (r : rs))
m <:&> r = fmap (:& r) m
infixr 7 <:&>

-- | 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 meta m. (EvalM' ext m, StkElMeta meta m)
  => InstrRunner meta m -> InstrRunner meta m
runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
runInstrImpl runner (WithLoc ics i) r = do
    -- Add wrapper which will be used later on in loop-like instr.
    let updateEnv env@ContractEnv{..}
          = env { ceErrorSrcPos = ics, ceMetaWrapper = ceMetaWrapper . WithLoc ics }
    local updateEnv $ runner i r
runInstrImpl runner (Meta meta i) r = do
    -- Add wrapper which will be used later on in loop-like instr.
    let updateEnv env@ContractEnv{..}
          = env { ceMetaWrapper = ceMetaWrapper . Meta meta }
    local updateEnv $ runner i r
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 <- seValueL assignBigMapIds' =<< mkDuplicateStkEl 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 meta) inp -> m (Rec (StkEl meta) 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 <- seValueL assignBigMapIds' =<< mkDuplicateStkEl 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 @_ @_ @_ @a s) input0 =
  pure $ go s input0
  where
    go :: forall (n :: Peano) inp out. ConstraintDIG n inp out a
       => PeanoNatural n -> Rec (StkEl meta) inp -> Rec (StkEl meta) out
    go Zero stack = stack
    go (Succ n') (b :& r) =
      case go n' r of
        a :& resTail -> a :& b :& resTail
runInstrImpl _ (DUG @_ @_ @_ @a s) input0 =
  pure $ go s input0
  where
    go :: forall (n :: Peano) inp out. ConstraintDUG n inp out a
       => PeanoNatural n -> Rec (StkEl meta) inp -> Rec (StkEl meta) out
    go Zero stack = stack
    go (Succ n') (a :& b :& r) = b :& go n' (a :& r)
runInstrImpl _ AnnSOME{} ((seValue -> a) :& r) =
  withValueTypeSanity a $
    mkStkEl (VOption (Just a)) <:&> r
runInstrImpl _ (AnnPUSH _ v) r = mkStkEl v <:&> r
runInstrImpl _ AnnNONE{} r = mkStkEl (VOption Nothing) <:&> r
runInstrImpl _ AnnUNIT{} r = mkStkEl VUnit <:&> r
runInstrImpl runner (IF_NONE _bNone bJust) (StkEl (VOption (Just a)) :& r) =
  runner bJust =<< mkStkEl 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) =
  mkStkEl (VPair (a, b)) <:&> r
runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b))) :& r) = do
  el1 <- mkStkEl a
  el2 <- mkStkEl b
  pure $ el1 :& el2 :& r
runInstrImpl _ (AnnPAIRN _ s) stack = go s stack
  where
    go :: forall n inp. ConstraintPairN n inp
       => PeanoNatural n
       -> Rec (StkEl meta) inp
       -> m (Rec (StkEl meta) (PairN n inp))
    go (Succ (Succ Zero)) (StkEl a :& StkEl b :& r) =
      -- if n=2
      mkStkEl (VPair (a, b)) <:&> r
    go (Succ n@(Succ (Succ _))) (StkEl a :& r@(_ :& _ :& _)) =
      -- if n>2
      go n r >>= \case
        StkEl combed :& r' ->
            mkStkEl (VPair (a, combed)) <:&> r'
runInstrImpl _ (UNPAIRN s) (StkEl pair0 :& r) = do
  r' <- go s pair0
  pure $ r' <+> r
  where
    go
      :: forall n pair. ConstraintUnpairN n pair
      => PeanoNatural n -> Value pair
      -> m (Rec (StkEl meta) (UnpairN n pair))
    go n pair =
      case (n, pair) of
        -- if n=2
        (Succ (Succ Zero), VPair (a, b)) -> do
          el1 <- mkStkEl a
          el2 <- mkStkEl b
          pure $ el1 :& el2 :& RNil
        -- if n>2
        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _))) ->
          liftA2 (:&) (mkStkEl a) (go n' b)
runInstrImpl _ AnnCAR{} (StkEl (VPair (a, _b)) :& r) = mkStkEl a <:&> r
runInstrImpl _ AnnCDR{} (StkEl (VPair (_a, b)) :& r) = mkStkEl b <:&> r
runInstrImpl _ AnnLEFT{} ((StkEl a) :& r) =
  withValueTypeSanity a $
    mkStkEl (VOr $ Left a) <:&> r
runInstrImpl _ AnnRIGHT{} ((StkEl b) :& r) =
  withValueTypeSanity b $
    mkStkEl (VOr $ Right b) <:&> r
runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) :& r) =
  runner bLeft =<< mkStkEl a <:&> r
runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) :& r) =
  runner bRight =<< mkStkEl a <:&> r
runInstrImpl _ AnnNIL{} r = mkStkEl (VList []) <:&> r
runInstrImpl _ AnnCONS{} (a :& StkEl (VList l) :& r) = mkStkEl (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) = do
  el1 <- mkStkEl lh
  el2 <- mkStkEl (VList lr)
  runner bCons $ el1 :& el2 :& r
runInstrImpl _ AnnSIZE{} (a :& r) =
   mkStkEl (VNat $ Unsafe.fromIntegral @Int @Natural $ evalSize $ seValue a) <:&> r
runInstrImpl _ AnnEMPTY_SET{} r = mkStkEl (VSet Set.empty) <:&> r
runInstrImpl _ AnnEMPTY_MAP{} r = mkStkEl (VMap Map.empty) <:&> r
runInstrImpl _ AnnEMPTY_BIG_MAP{} r = do
  bigMap <- assignBigMapIds' $ VBigMap Nothing Map.empty
  mkStkEl 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 meta (MapOpInp c)) -> do
    res <- runner code (val :& curStack)
    case res of
      ((seValue -> nextVal :: Value b) :& nextStack) -> pure (nextStack, nextVal : curList))
    (r, []) =<< traverse mkStkEl (mapOpToList @c a)
  mkStkEl (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 =<< mkStkEl x <:&> r
      withMetaWrapper runner (ITER code) =<< mkStkEl xs <:&> res
    (Nothing, _) -> pure r
runInstrImpl _ AnnMEM{} (a :& b :& r) = mkStkEl (VBool (evalMem (seValue a) (seValue b))) <:&> r
runInstrImpl _ AnnGET{} (a :& b :& r) = mkStkEl (VOption (evalGet (seValue a) (seValue b))) <:&> r
runInstrImpl _ (AnnGETN _ s) (StkEl pair :& r) = do
  mkStkEl (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) =
  mkStkEl (evalUpd (seValue a) (seValue b) c) <:&> r
runInstrImpl _ (AnnUPDATEN _ s) (StkEl (val :: Value val) :& StkEl pair :& r) = do
  mkStkEl (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) = do
  el1 <- mkStkEl (VOption (evalGet key collection))
  el2 <- mkStkEl (evalUpd key valMb collection)
  pure $ el1 :& el2 :& 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
  withMetaWrapper runner (LOOP ops) res
runInstrImpl _ (LOOP_LEFT _) (StkEl (VOr (Right a)) :& r) = mkStkEl a <:&> r
runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) :& r) = do
  res <- runner ops =<< mkStkEl a <:&> r
  withMetaWrapper runner (LOOP_LEFT ops) res
runInstrImpl _ (AnnLAMBDA _ lam) r = mkStkEl (mkVLam lam) <:&> r
runInstrImpl _ (AnnLAMBDA_REC _ lam) r = mkStkEl (mkVLamRec lam) <:&> r
runInstrImpl runner AnnEXEC{} (a :& self@(StkEl (VLam code)) :& r) =
  case code of
    LambdaCode (rfAnyInstr -> lBody) -> do
      res <- runner lBody (a :& RNil)
      pure $ res <+> r
    LambdaCodeRec (rfAnyInstr -> lBody) -> do
      res <- runner lBody (a :& self :& RNil)
      pure $ res <+> r
runInstrImpl _ i@AnnAPPLY{} (StkEl (a :: 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 -> mkStkEl (VLam $ LambdaCode (rfMapAnyInstr doApply lBody)) <:&> r
      LambdaCodeRec lBody ->
        let res = RfNormal $ PUSH a `Seq` PAIR `Seq` LAMBDA_REC lBody `Seq` SWAP `Seq` EXEC
        in mkStkEl (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) = mkStkEl (VBytes $ packValue' a) <:&> r
runInstrImpl _ AnnUNPACK{} (StkEl (VBytes a) :& r) =
  mkStkEl (VOption . rightToMaybe $ runUnpack a) <:&> r
runInstrImpl _ AnnCONCAT{} (a :& b :& r) = mkStkEl (evalConcat (seValue a) (seValue b)) <:&> r
runInstrImpl _ AnnCONCAT'{} (StkEl (VList a) :& r) = mkStkEl (evalConcat' a) <:&> r
runInstrImpl _ AnnSLICE{} (StkEl (VNat o) :& StkEl (VNat l) :& StkEl s :& r) =
  mkStkEl (VOption (evalSlice o l s)) <:&> r
runInstrImpl _ AnnISNAT{} (StkEl (VInt i) :& r) =
  if i < 0
  then mkStkEl (VOption Nothing) <:&> r
  else mkStkEl (VOption (Just (VNat $ fromInteger i))) <:&> r
runInstrImpl _ AnnADD{} (l :& r :& rest) = runArithOp (Proxy @Add) l r <:&> rest
runInstrImpl _ AnnSUB{} (l :& r :& rest) = runArithOp (Proxy @Sub) l r <:&> rest
runInstrImpl _ AnnSUB_MUTEZ{} (l :& r :& rest) = runArithOp (Proxy @SubMutez) l r <:&> rest
runInstrImpl _ AnnMUL{} (l :& r :& rest) = runArithOp (Proxy @Mul) l r <:&> rest
runInstrImpl _ AnnEDIV{} (l :& r :& rest) = runArithOp (Proxy @EDiv) l r <:&> rest
runInstrImpl _ AnnABS{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Abs) a) <:&> rest
runInstrImpl _ AnnNEG{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Neg) a) <:&> rest
runInstrImpl _ AnnLSL{} (x :& s :& rest) = runArithOp (Proxy @Lsl) x s <:&> rest
runInstrImpl _ AnnLSR{} (x :& s :& rest) = runArithOp (Proxy @Lsr) x s <:&> rest
runInstrImpl _ AnnOR{} (l :& r :& rest) = runArithOp (Proxy @Or) l r <:&> rest
runInstrImpl _ AnnAND{} (l :& r :& rest) = runArithOp (Proxy @And) l r <:&> rest
runInstrImpl _ AnnXOR{} (l :& r :& rest) = runArithOp (Proxy @Xor) l r <:&> rest
runInstrImpl _ AnnNOT{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Not) a) <:&> rest
runInstrImpl _ AnnCOMPARE{} ((seValue -> l) :& (seValue -> r) :& rest) =
  mkStkEl (VInt (compareOp l r)) <:&> rest
runInstrImpl _ AnnEQ{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Eq') a) <:&> rest
runInstrImpl _ AnnNEQ{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Neq) a) <:&> rest
runInstrImpl _ AnnLT{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Lt) a) <:&> rest
runInstrImpl _ AnnGT{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Gt) a) <:&> rest
runInstrImpl _ AnnLE{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Le) a) <:&> rest
runInstrImpl _ AnnGE{} ((seValue -> a) :& rest) =
  mkStkEl (evalUnaryArithOp (Proxy @Ge) a) <:&> rest
runInstrImpl _ AnnINT{} (StkEl a :& r) =
  mkStkEl (evalToIntOp a) <:&> r
runInstrImpl _ AnnNAT{} (StkEl a :& r) =
  mkStkEl (evalToNatOp a) <:&> r
runInstrImpl _ AnnBYTES{} (StkEl a :& r) =
  mkStkEl (evalToBytesOp a) <:&> r
runInstrImpl runner (AnnVIEW (Anns2' _ (_ :: Notes ret)) name)
                    (StkEl (viewArg :: Value arg) :& StkEl (VAddress epAddr) :& r) = do
  res :: Value ('TOption ret) <- VOption <$> runMaybeT do
    EpAddress addr@ContractAddress{} _ <- pure epAddr
    ContractState
      { csContract = viewedContract
      , csStorage = viewedContractStorage
      , csBalance = viewedContractBalance
      } <- MaybeT $ asks ceContracts >>= ($ addr)
    view' <- hoistMaybe $ rightToMaybe $ getViewByNameAndType viewedContract name
    let viewEnv ContractEnv{..} = ContractEnv
          { ceAmount = zeroMutez
          , ceSelf = addr
          , ceSender = Constrained ceSelf
          , ceBalance = viewedContractBalance
          , ..
          }
    lift $ interpretView' runner viewEnv view' viewedContractStorage viewArg
  mkStkEl res <:&> r

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

      let withNotes v = mkStkEl v <:&> r
      withNotes . VOption =<< case mepName of
        Nothing -> pure Nothing
        Just epName -> case addr of
          ImplicitAddress{} -> pure $ case sing @a of
            STTicket{} -> castContract addr epName $ starParamNotes @a
            STUnit -> castContract addr epName $ starParamNotes @a
            _ -> Nothing
          ContractAddress{} -> runMaybeT do
            ContractState{csContract} <- MaybeT $ ceContracts addr
            hoistMaybe $ castContract addr epName (cParamNotes csContract)
          SmartRollupAddress{} ->
            throwMichelson $ MichelsonUnsupported "sr1 addresses with CONTRACT"
  where
    castContract
      :: forall p kind. (ParameterScope p)
      => KindedAddress kind -> EpName -> ParamNotes p -> Maybe (Value ('TContract a))
    castContract addr epName param = do
      -- As we are within Maybe monad, pattern-match failure results in Nothing
      MkEntrypointCallRes (_ :: Notes a') epc <- mkEntrypointCall epName param
      Right Refl <- pure $ eqType @a @a'
      pure $ VContract (MkAddress addr) (SomeEpc epc)

runInstrImpl _ AnnTRANSFER_TOKENS{}
  (StkEl p :& StkEl (VMutez mutez) :& StkEl contract :& r) = do
    incrementCounter
    globalCounter <- isGlobalCounter <$> getInterpreterState
    mkStkEl (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) -> mkStkEl (VOp (OpSetDelegate $ SetDelegate (Just k) globalCounter)) <:&> r
    Nothing -> mkStkEl (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
  el1 <- mkStkEl (VOp (OpCreateContract resOp))
  el2 <- mkStkEl (VAddress resEpAddr)
  pure $ el1 :& el2 :& r
runInstrImpl _ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash k) :& r) =
  mkStkEl (VContract (MkAddress $ ImplicitAddress k) sepcPrimitive) <:&> r
runInstrImpl _ AnnNOW{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VTimestamp ceNow) <:&> r
runInstrImpl _ AnnAMOUNT{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VMutez ceAmount) <:&> r
runInstrImpl _ AnnBALANCE{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VMutez ceBalance) <:&> r
runInstrImpl _ AnnVOTING_POWER{} (StkEl (VKeyHash k) :& r) = do
  ContractEnv{..} <- ask
  mkStkEl (VNat $ vpPick k ceVotingPowers) <:&> r
runInstrImpl _ AnnTOTAL_VOTING_POWER{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VNat $ vpTotal ceVotingPowers) <:&> r
runInstrImpl _ AnnCHECK_SIGNATURE{}
  (StkEl (VKey k) :& StkEl (VSignature v) :& StkEl (VBytes b) :& r) =
  mkStkEl (VBool $ checkSignature k v b) <:&> r
runInstrImpl _ AnnSHA256{} (StkEl (VBytes b) :& r) =
  mkStkEl (VBytes $ sha256 b) <:&> r
runInstrImpl _ AnnSHA512{} (StkEl (VBytes b) :& r) =
  mkStkEl (VBytes $ sha512 b) <:&> r
runInstrImpl _ AnnBLAKE2B{} (StkEl (VBytes b) :& r) =
  mkStkEl (VBytes $ blake2b b) <:&> r
runInstrImpl _ AnnSHA3{} (StkEl (VBytes b) :& r) =
  mkStkEl (VBytes $ sha3 b) <:&> r
runInstrImpl _ AnnKECCAK{} (StkEl (VBytes b) :& r) =
  mkStkEl (VBytes $ keccak b) <:&> r
runInstrImpl _ AnnHASH_KEY{} (StkEl (VKey k) :& r) =
  mkStkEl (VKeyHash $ hashKey k) <:&> r
runInstrImpl _ AnnPAIRING_CHECK{} (StkEl (VList pairs) :& r) = do
  let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]
  mkStkEl (VBool $ checkPairing pairs') <:&> r
runInstrImpl _ AnnSOURCE{} r = do
  ContractEnv{ceSource=Constrained ceSource} <- ask
  mkStkEl (VAddress $ EpAddress ceSource DefEpName) <:&> r
runInstrImpl _ AnnSENDER{} r = do
  ContractEnv{ceSender=Constrained ceSender} <- ask
  mkStkEl (VAddress $ EpAddress ceSender DefEpName) <:&> r
runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =
  mkStkEl (VAddress $ EpAddress' a (sepcName sepc)) <:&> r
runInstrImpl _ AnnCHAIN_ID{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VChainId ceChainId) <:&> r
runInstrImpl _ AnnLEVEL{} r = do
  ContractEnv{..} <- ask
  mkStkEl (VNat ceLevel) <:&> r
runInstrImpl _ AnnSELF_ADDRESS{} r = do
  ContractEnv{..} <- ask
  mkStkEl (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
  mkStkEl result <:&> r
runInstrImpl _ AnnTICKET_DEPRECATED{} (StkEl dat :& StkEl (VNat am) :& r) = do
  ContractEnv{..} <- ask
  mkStkEl (VTicket (MkAddress ceSelf) dat am) <:&> r
runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do
  mkStkEl
      (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)
  mkStkEl 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)
  mkStkEl 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))
  mkStkEl 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
  mkStkEl (VNat ceMinBlockTime) <:&> r
runInstrImpl _ (AnnEMIT _ (unAnnotation -> emTag) mNotes) ((StkEl emValue) :& r) = do
  incrementCounter
  emCounter <- isGlobalCounter <$> getInterpreterState
  let emNotes = fromMaybe starNotes mNotes
  mkStkEl (VOp (OpEmit Emit{..})) <:&> r

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

-- | Unpacks given raw data into a typed value.
runUnpack
  :: forall t. (UnpackedValScope t)
  => ByteString
  -> Either UnpackError (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

data ViewLookupError
  = ViewNotFound ViewName
  | ViewArgMismatch (MismatchError T)
  | ViewRetMismatch (MismatchError T)
  deriving stock Show

instance Buildable ViewLookupError where
  build = \case
    ViewNotFound name -> "View '" +| name |+ "' not found"
    ViewArgMismatch err -> nameF "View argument type mismatch" err
    ViewRetMismatch err -> nameF "View return type mismatch" err

-- | Interpret a contract's view for given t'ContractEnv' and initial
-- 'InterpreterState'. It is assumed t'ContractEnv' is suitable for the view
-- call, that is, the view is executed exactly in the env that's passed here.
interpretView
  :: View arg st ret
  -> Value st
  -> Value arg
  -> ContractEnv
  -> InterpreterState
  -> InterpretReturn ret
interpretView view' st argument = runEvalOp $
  interpretView' (runInstr @_ @NoStkElMeta) id view' st argument

-- | Attempt to find a view with a given name and given type in a given
-- contract.
getViewByNameAndType
  :: forall arg ret cp st. (SingI arg, SingI ret)
  => Contract cp st -> ViewName -> Either ViewLookupError (View arg st ret)
getViewByNameAndType contract name = do
  SomeView (view'@View{} :: View arg' st ret') <- liftEither $ getViewByName contract name
  let retMismatch = ViewRetMismatch MkMismatchError
        { meActual = demote @ret', meExpected = demote @ret }
      argMismatch = ViewArgMismatch MkMismatchError
        { meActual = demote @arg', meExpected = demote @arg }
  Refl <- liftEither $ maybeToRight argMismatch $ sing @arg `decideEquality` sing @arg'
  Refl <- liftEither $ maybeToRight retMismatch $ sing @ret `decideEquality` sing @ret'
  pure view'

-- | Attempt to find a view with a given name in a given contract.
getViewByName :: Contract cp st -> ViewName -> Either ViewLookupError (SomeView st)
getViewByName contract name =
  liftEither $ maybeToRight (ViewNotFound name) $ lookupView name (cViews contract)

-- | 'EvalM' view interpretation helper.
interpretView'
  :: forall ret st m arg ext meta. (StkElMeta meta m, EvalM' ext m)
  => (forall inp out. Instr inp out -> Rec (StkEl meta) inp -> m (Rec (StkEl meta) out))
  -> (ContractEnv' m -> ContractEnv' m)
  -> View arg st ret
  -> Value st
  -> Value arg
  -> m (Value ret)
interpretView' runner env View{vCode} storage argument = do
  resSt <- local env $ runInstrImpl runner vCode =<<
    mkStkEl @meta (VPair (argument, storage)) <:&> RNil
  let StkEl res :& RNil = resSt
  pure res

createOrigOp
  :: (ParameterScope param, StorageScope store, L1AddressKind kind)
  => KindedAddress kind
  -> Maybe ContractAlias
  -> Maybe (Value '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 (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash mbKeyHash = mbKeyHash <&> \(VKeyHash keyHash) -> keyHash

interpretExt
  :: forall ext meta m. (StkElMeta meta m, EvalM' ext m)
  => InstrRunner meta m -> SomeItStack meta -> m ()
interpretExt _ (SomeItStack (PRINT (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 (TEST_ASSERT (TestAssert nm pc instr)) st) = do
  ost <- runInstrImpl runner instr st
  let ((seValue -> fromVal -> succeeded) :& _) = ost
  unless succeeded $ do
    interpretExt runner (SomeItStack (PRINT pc) st)
    throwMichelson $ MichelsonFailedTestAssert $ "TEST_ASSERT " <> nm <> " failed"

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

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

assignBigMapIds' :: forall ext m t. 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)