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

  , interpret
  , interpretInstr
  , ContractReturn

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

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

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, throwError)
import Data.Default (Default(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Singletons (Sing)
import Data.Vinyl (Rec(..), (<+>))
import Fmt (Buildable(build), Builder, genericF, pretty)

import Michelson.Interpret.Pack (packValue')
import Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Michelson.TypeCheck
  (SomeContract(..), TCError, TcOriginatedContracts, matchTypes, runTypeCheck, typeCheckContract,
  typeCheckValue)
import Michelson.Typed
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, sha256, sha512)
import Util.Peano (LongerThan, Peano, SingNat(SS, SZ))
import Util.TH
import Util.Type
import Util.Typeable

-- | 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.
  , ceChainId :: ChainId
  -- ^ Identifier of the current 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 :: (Typeable t, SingI 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
  MichelsonAmbigousEpRef :: EpName -> EpAddress -> MichelsonFailed

deriving stock instance Show MichelsonFailed

instance Eq MichelsonFailed where
  MichelsonFailedWith v1 == MichelsonFailedWith v2 = v1 `eqParam1` 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
  MichelsonAmbigousEpRef ep1 epAddr1 == MichelsonAmbigousEpRef ep2 epAddr2 =
    ep1 == ep2 && epAddr1 == epAddr2
  MichelsonAmbigousEpRef _ _ == _ = 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
      MichelsonAmbigousEpRef instrEp epAddr ->
        "Ambigous entrypoint reference. `CONTRACT %" <> build instrEp <> "` \
        \called over address " <> build epAddr
    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)

data InterpretError
  = RuntimeFailure (MichelsonFailed, MorleyLogs)
  | IllTypedContract TCError
  | IllTypedParam TCError
  | IllTypedStorage TCError
  deriving stock (Generic)

deriving stock instance Show InterpretError

instance Buildable InterpretError where
  build = genericF

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
  }

-- | Morley logs for interpreter state.
newtype MorleyLogs = MorleyLogs
  { unMorleyLogs :: [Text]
    -- ^ Logs in reverse order.
  } deriving stock (Eq, Show, Generic)
    deriving newtype (Default, Buildable)

instance NFData MorleyLogs

noMorleyLogs :: MorleyLogs
noMorleyLogs = MorleyLogs []

-- | Interpret a contract without performing any side effects.
-- This function uses untyped representation of contract, parameter and storage.
-- Mostly used for testing.
interpretUntyped
  :: U.Contract
  -> U.Value
  -> U.Value
  -> ContractEnv
  -> Either InterpretError InterpretResult
interpretUntyped uContract@U.Contract{..} paramU initStU env = do
  SomeContract (FullContract (instr :: ContractCode cp st) _ _)
      <- first IllTypedContract $ typeCheckContract (ceContracts env) uContract
  -- Do creates dummy scope to somehow overcome this:
  -- GHC internal error: ‘st’ is not in scope during type checking, but it passed the renamer.
  do
    let
      runTC :: forall t. SingI t => U.Value -> Either TCError (Value t)
      runTC =
        runTypeCheck contractParameter (ceContracts env) .
        usingReaderT def .
        typeCheckValue @t

    paramV <- first IllTypedParam $ runTC @cp paramU
    initStV <- first IllTypedStorage $ runTC @st initStU
    handleContractReturn $
      interpret instr epcCallRootUnsafe paramV initStV env

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

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

interpret'
  :: forall cp st arg.
     ContractCode cp st
  -> EntryPointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' instr epc param initSt env ist = first (fmap fromFinalStack) $
  runEvalOp
    (runInstr instr $ mkInitStack (liftCallArg epc param) initSt)
    env
    ist

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

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

interpret
  :: ContractCode cp st
  -> EntryPointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> ContractReturn st
interpret instr epc param initSt env =
  interpret' instr epc param initSt env (initInterpreterState env)

initInterpreterState :: ContractEnv -> InterpreterState
initInterpreterState env = InterpreterState def (ceMaxSteps env)

-- | 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 env instr inpSt =
  fst $
  runEvalOp
    (runInstr instr inpSt)
    env
    InterpreterState{ isMorleyLogs = MorleyLogs [], isRemainingSteps = 9999999999 }

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

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

instance NFData RemainingSteps

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

instance NFData InterpreterState

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

type EvalM m =
  ( MonadReader ContractEnv m
  , MonadState InterpreterState m
  , MonadError MichelsonFailed m
  )

type InstrRunner m =
  forall inp out.
     Instr inp out
  -> Rec (T.Value) inp
  -> m (Rec (T.Value) 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@(InstrWithNotes _ _i1) r = runInstrImpl runInstr i r
runInstr i@(InstrWithVarNotes _ _i1) r = runInstrImpl runInstr i r
runInstr i@Nop r = runInstrImpl runInstr i r
runInstr i@(Nested _) r = runInstrImpl runInstr i r
runInstr i r = do
  rs <- gets isRemainingSteps
  if rs == 0
  then throwError $ MichelsonGasExhaustion
  else do
    modify (\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 :: EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
runInstrImpl runner (InstrWithNotes _ i) r = runner i r
runInstrImpl runner (InstrWithVarNotes _ 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 _ (Ext nop) r = r <$ interpretExt (SomeItStack nop r)
runInstrImpl runner (Nested sq) r = runInstrImpl runner sq r
runInstrImpl runner (DocGroup _ sq) r = runInstrImpl runner sq r
runInstrImpl _ DROP (_ :& r) = pure $ r
runInstrImpl runner (DROPN s) stack =
  case s of
    SZ -> pure stack
    SS s' -> case stack of
      -- 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'.
      (_ :& r) -> runInstrImpl runner (DROPN s') r
runInstrImpl _ DUP (a :& r) = pure $ a :& a :& r
runInstrImpl _ SWAP (a :& b :& r) = pure $ b :& a :& r
runInstrImpl _ (DIG nSing0) input0 =
  pure $ go (nSing0, input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDIG n inp out a =>
      (Sing n, Rec T.Value inp) -> Rec T.Value out
    go = \case
      (SZ, stack) ->  stack
      (SS nSing, b :& r) -> case go (nSing, r) of
        (a :& resTail) -> a :& b :& resTail
runInstrImpl _ (DUG nSing0) input0 =
  pure $ go (nSing0, input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDUG n inp out a =>
      (Sing n, Rec T.Value inp) -> Rec T.Value out
    go = \case
      (SZ, stack) -> stack
      (SS s', a :& b :& r) -> b :& go (s', a :& r)
runInstrImpl _ (PUSH v) r = pure $ v :& r
runInstrImpl _ SOME (a :& r) = pure $ VOption (Just a) :& r
runInstrImpl _ NONE r = pure $ VOption Nothing :& r
runInstrImpl _ UNIT r = pure $ VUnit :& r
runInstrImpl runner (IF_NONE _bNone bJust) (VOption (Just a) :& r) = runner bJust (a :& r)
runInstrImpl runner (IF_NONE bNone _bJust) (VOption Nothing :& r) = runner bNone r
runInstrImpl _ PAIR (a :& b :& r) = pure $ VPair (a, b) :& r
runInstrImpl _ (AnnCAR _) (VPair (a, _b) :& r) = pure $ a :& r
runInstrImpl _ (AnnCDR _) (VPair (_a, b) :& r) = pure $ b :& r
runInstrImpl _ LEFT (a :& r) = pure $ (VOr $ Left a) :& r
runInstrImpl _ RIGHT (b :& r) = pure $ (VOr $ Right b) :& r
runInstrImpl runner (IF_LEFT bLeft _) (VOr (Left a) :& r) = runner bLeft (a :& r)
runInstrImpl runner (IF_LEFT _ bRight) (VOr (Right a) :& r) = runner bRight (a :& r)
-- More here
runInstrImpl _ NIL r = pure $ VList [] :& r
runInstrImpl _ CONS (a :& VList l :& r) = pure $ VList (a : l) :& r
runInstrImpl runner (IF_CONS _ bNil) (VList [] :& r) = runner bNil r
runInstrImpl runner (IF_CONS bCons _) (VList (lh : lr) :& r) = runner bCons (lh :& VList lr :& r)
runInstrImpl _ SIZE (a :& r) = pure $ (VNat $ (fromInteger . toInteger) $ evalSize a) :& r
runInstrImpl _ EMPTY_SET r = pure $ VSet Set.empty :& r
runInstrImpl _ EMPTY_MAP r = pure $ VMap Map.empty :& r
runInstrImpl _ EMPTY_BIG_MAP r = pure $ VBigMap Map.empty :& r
runInstrImpl runner (MAP ops) (a :& r) =
  case ops of
    (code :: Instr (MapOpInp c ': s) (b ': s)) -> do
      -- Evaluation must preserve all stack modifications that @MAP@'s does.
      (newStack, newList) <- foldlM (\(curStack, curList) (val :: T.Value (MapOpInp c)) -> do
        res <- runner code (val :& curStack)
        case res of
          ((nextVal :: T.Value b) :& nextStack) -> pure (nextStack, nextVal : curList))
        (r, []) (mapOpToList @c a)
      pure $ mapOpFromList a (reverse newList) :& newStack
runInstrImpl runner (ITER ops) (a :& r) =
  case ops of
    (code :: Instr (IterOpEl c ': s) s) ->
      case iterOpDetachOne @c a of
        (Just x, xs) -> do
          res <- runner code (x :& r)
          runner (ITER code) (xs :& res)
        (Nothing, _) -> pure r
runInstrImpl _ MEM (a :& b :& r) = pure $ (VBool (evalMem a b)) :& r
runInstrImpl _ GET (a :& b :& r) = pure $ VOption (evalGet a b) :& r
runInstrImpl _ UPDATE (a :& b :& c :& r) = pure $ evalUpd a b c :& r
runInstrImpl runner (IF bTrue _) (VBool True :& r) = runner bTrue r
runInstrImpl runner (IF _ bFalse) (VBool False :& r) = runner bFalse r
runInstrImpl _ (LOOP _) (VBool False :& r) = pure $ r
runInstrImpl runner (LOOP ops) (VBool True :& r) = do
  res <- runner ops r
  runner (LOOP ops) res
runInstrImpl _ (LOOP_LEFT _) (VOr (Right a) :&r) = pure $ a :& r
runInstrImpl runner (LOOP_LEFT ops) (VOr (Left a) :& r) = do
  res <- runner ops (a :& r)
  runner  (LOOP_LEFT ops) res
runInstrImpl _ (LAMBDA lam) r = pure $ lam :& r
runInstrImpl runner EXEC (a :& VLam (T.rfAnyInstr -> lBody) :& r) = do
  res <- runner lBody (a :& RNil)
  pure $ res <+> r
runInstrImpl _ APPLY ((a :: T.Value a) :& VLam lBody :& r) = do
  pure $ 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
    SZ -> runner i stack
    SS s' -> case stack of
      (a :& r) -> (a :&) <$> runInstrImpl runner (DIPN s' i) r
runInstrImpl _ FAILWITH (a :& _) = throwError $ MichelsonFailedWith a
runInstrImpl _ CAST (a :& r) = pure $ a :& r
runInstrImpl _ RENAME (a :& r) = pure $ a :& r
runInstrImpl _ PACK (a :& r) = pure $ (VBytes $ packValue' a) :& r
runInstrImpl _ UNPACK (VBytes a :& r) =
  pure $ (VOption . rightToMaybe $ runUnpack a) :& r
runInstrImpl _ CONCAT (a :& b :& r) = pure $ evalConcat a b :& r
runInstrImpl _ CONCAT' (VList a :& r) = pure $ evalConcat' a :& r
runInstrImpl _ SLICE (VNat o :& VNat l :& s :& r) =
  pure $ VOption (evalSlice o l s) :& r
runInstrImpl _ ISNAT (VInt i :& r) =
  if i < 0
  then pure $ VOption Nothing :& r
  else pure $ 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 $ evalEDivOp l r :& rest
runInstrImpl _ ABS (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Abs) a) :& rest
runInstrImpl _ NEG (a :& rest) = pure $ (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 (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Not) a) :& rest
runInstrImpl _ COMPARE (l :& r :& rest) = pure $ (T.VInt (compareOp l r)) :& rest
runInstrImpl _ EQ (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Eq') a) :& rest
runInstrImpl _ NEQ (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Neq) a) :& rest
runInstrImpl _ LT (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Lt) a) :& rest
runInstrImpl _ GT (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Gt) a) :& rest
runInstrImpl _ LE (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Le) a) :& rest
runInstrImpl _ GE (a :& rest) = pure $ (evalUnaryArithOp (Proxy @Ge) a) :& rest
runInstrImpl _ INT (VNat n :& r) = pure $ (VInt $ toInteger n) :& r
runInstrImpl _ (SELF sepc :: Instr inp out) r = do
  ContractEnv{..} <- ask
  case Proxy @out of
    (_ :: Proxy ('TContract cp ': s)) -> do
      pure $ VContract ceSelf sepc :& r
runInstrImpl _ (CONTRACT (nt :: T.Notes a) instrEpName) (VAddress epAddr :& r) = do
  ContractEnv{..} <- ask
  let T.EpAddress addr addrEpName = epAddr
  epName <- case (instrEpName, addrEpName) of
    (DefEpName, DefEpName) -> pure DefEpName
    (DefEpName, en) -> pure en
    (en, DefEpName) -> pure en
    _ -> throwError $ MichelsonAmbigousEpRef instrEpName epAddr

  pure $ case addr of
    KeyAddress _ ->
      castContract addr epName T.tyImplicitAccountParam :& r
    ContractAddress ca ->
      case Map.lookup ca ceContracts of
        -- Wrapping into 'ParamNotesUnsafe' is safe because originated contract has
        -- valid parameter type. Should be not necessary after [#36].
        Just tc@(U.ParameterType (AsUTypeExt (_ :: Sing tc) tcNotes) rootAnn) ->
          let paramNotes = ParamNotesUnsafe tcNotes rootAnn in
          case T.checkScope @(T.ParameterScope tc) of
            Right Dict -> castContract addr epName paramNotes :& r
            _ -> error $ "Illegal type in parameter of env contract: " <> pretty tc
            -- TODO [#36]: we can do this safely once 'TcOriginatedContracts' stores
            -- typed stuff.
        Nothing -> VOption Nothing :& r
  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 (p :& VMutez mutez :& contract :& r) =
  pure $ VOp (OpTransferTokens $ TransferTokens p mutez contract) :& r
runInstrImpl _ SET_DELEGATE (VOption mbKeyHash :& r) =
  case mbKeyHash of
    Just (VKeyHash k) -> pure $ VOp (OpSetDelegate $ SetDelegate $ Just k) :& r
    Nothing -> pure $ VOp (OpSetDelegate $ SetDelegate $ Nothing) :& r
runInstrImpl _ (CREATE_CONTRACT fullContract)
  (VOption mbKeyHash :& VMutez m :& g :& r) = do
  originator <- ceSelf <$> ask
  let ops = fcCode fullContract
  let resAddr = U.mkContractAddress $ createOrigOp originator mbKeyHash m ops g
  let resEpAddr = EpAddress resAddr def
  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g ops
  pure $ VOp (OpCreateContract resOp)
      :& (VAddress resEpAddr)
      :& r
runInstrImpl _ IMPLICIT_ACCOUNT (VKeyHash k :& r) =
  pure $ VContract (KeyAddress k) sepcPrimitive :& r
runInstrImpl _ NOW r = do
  ContractEnv{..} <- ask
  pure $ (VTimestamp ceNow) :& r
runInstrImpl _ AMOUNT r = do
  ContractEnv{..} <- ask
  pure $ (VMutez ceAmount) :& r
runInstrImpl _ BALANCE r = do
  ContractEnv{..} <- ask
  pure $ (VMutez ceBalance) :& r
runInstrImpl _ CHECK_SIGNATURE (VKey k :& VSignature v :&
  VBytes b :& r) = pure $ (VBool $ checkSignature k v b) :& r
runInstrImpl _ SHA256 (VBytes b :& r) = pure $ (VBytes $ sha256 b) :& r
runInstrImpl _ SHA512 (VBytes b :& r) = pure $ (VBytes $ sha512 b) :& r
runInstrImpl _ BLAKE2B (VBytes b :& r) = pure $ (VBytes $ blake2b b) :& r
runInstrImpl _ HASH_KEY (VKey k :& r) = pure $ (VKeyHash $ hashKey k) :& r
runInstrImpl _ SOURCE r = do
  ContractEnv{..} <- ask
  pure $ (VAddress $ EpAddress ceSource def) :& r
runInstrImpl _ SENDER r = do
  ContractEnv{..} <- ask
  pure $ (VAddress $ EpAddress ceSender def) :& r
runInstrImpl _ ADDRESS (VContract a sepc :& r) =
  pure $ (VAddress $ EpAddress a (sepcName sepc)) :& r
runInstrImpl _ CHAIN_ID r = do
  ContractEnv{..} <- ask
  pure $ VChainId ceChainId :& r

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, Typeable n, Typeable m, EvalM monad)
  => proxy aop
  -> Value n
  -> Value m
  -> monad (Value (ArithRes aop n m))
runArithOp op l r = case evalOp op l r of
  Left  err -> throwError (MichelsonArithError err)
  Right res -> pure 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).
  -- Fortunatelly, the inner decoding logic does not need to know anything about gas use.
  unpackValue' bs

createOrigOp
  :: (SingI param, StorageScope store)
  => Address
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> ContractCode param store
  -> Value' Instr store
  -> U.OriginationOperation
createOrigOp originator mbDelegate bal contract g =
  U.OriginationOperation
    { ooOriginator = originator
    , ooDelegate = unwrapMbKeyHash mbDelegate
    , ooBalance = bal
    , ooStorage = untypeValue g
    , ooContract = convertContractCode contract
    }

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

interpretExt :: EvalM m => SomeItStack -> m ()
interpretExt (SomeItStack (T.PRINT (T.PrintComment pc)) st) = do
  let getEl (Left l) = l
      getEl (Right str) = withStackElem str st show
  modify (\s -> s {isMorleyLogs = MorleyLogs $ mconcat (map getEl pc) : unMorleyLogs (isMorleyLogs s)})

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

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

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

$(deriveGADTNFData ''MichelsonFailed)