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

  , interpret
  , interpretInstr
  , ContractReturn
  , handleContractReturn


  , interpretUntyped
  , InterpretError (..)
  , InterpretResult (..)
  , runInstr
  , runInstrNoGas
  , runUnpack
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (throwError)
import Data.Default (Default(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Singletons (SingI(..))
import Data.Typeable ((:~:)(..))
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(..), SomeNotedValue(..), TCError, TCTypeError(..), TcOriginatedContracts, eqType,
  matchTypes, runTypeCheck, typeCheckContract, typeCheckValue)
import Michelson.Typed
import qualified Michelson.Typed as T
import Michelson.Typed.Convert (convertContract, untypeValue)
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, Sing(SS, SZ))
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) => ArithError (CValue n) (CValue 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' Instr 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
  | UnexpectedParamType TCTypeError
  | UnexpectedStorageType TCTypeError
  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 interpreter state
newtype MorleyLogs = MorleyLogs
  { unMorleyLogs :: [Text]
  } deriving stock (Eq, Show)
    deriving newtype (Default, Buildable)

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 :: Contract cp st) _ _)
      <- first IllTypedContract $ typeCheckContract (ceContracts env) uContract
  withUType para $ \(sgp, ntp) ->
    withUType stor $ \(sgs, nts) -> do
      paramV :::: ((_ :: Sing cp1), _)
          <- first IllTypedParam $ runTypeCheck para (ceContracts env) $ usingReaderT def $
               typeCheckValue paramU (sgp, ntp)
      initStV :::: ((_ :: Sing st1), _)
          <- first IllTypedStorage $ runTypeCheck para (ceContracts env) $ usingReaderT def $
               typeCheckValue initStU (sgs, nts)
      Refl <- first UnexpectedStorageType $ eqType @st @st1
      Refl <- first UnexpectedParamType   $ eqType @cp @cp1
      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 constructIR $
  bimap (,isMorleyLogs s) (,s) ei

interpret'
  :: forall cp st arg.
     Contract cp st
  -> EntryPointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' instr epc param initSt env ist = first (fmap toRes) $
  runEvalOp
    (runInstr instr (T.VPair (liftParam param, initSt) :& RNil))
    env
    ist
  where
    liftParam :: T.Value arg -> T.Value cp
    liftParam = compileEpLiftSequence (epcLiftSequence epc)

    toRes
      :: (Rec (T.Value' instr) '[ 'TPair ('TList 'TOperation) st ])
      -> ([T.Operation' instr], T.Value' instr st)
    toRes (T.VPair (T.VList ops_, newSt) :& RNil) =
      (map (\(T.VOp op) -> op) ops_, newSt)

interpret
  :: Contract 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 (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)
  deriving newtype (Eq, Ord, Buildable, Num)

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

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

-- | Function to change amount of remaining steps stored in State monad
runInstr
  :: Instr inp out
  -> Rec (T.Value) inp
  -> EvalOp (Rec (T.Value) out)
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
  :: forall a b . T.Instr a b -> Rec T.Value a -> EvalOp (Rec T.Value b)
runInstrNoGas = runInstrImpl runInstrNoGas


-- | Function to interpret Michelson instruction(s) against given stack.
runInstrImpl
    :: (forall inp1 out1 .
           Instr inp1 out1
        -> Rec (T.Value) inp1
        -> EvalOp (Rec T.Value out1)
    ) ->
       (forall inp out .
           Instr inp out
        -> Rec (T.Value) inp
        -> EvalOp (Rec T.Value out)
      )
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 $ VC (CvNat $ (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
      newList <- mapM (\(val :: T.Value (MapOpInp c)) -> do
        res <- runner code (val :& r)
        case res of
          ((newVal :: T.Value b) :& _) -> pure newVal)
        $ mapOpToList @c a
      pure $ mapOpFromList a newList :& r
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 (VC a :& b :& r) = pure $ VC (CvBool (evalMem a b)) :& r
runInstrImpl _ GET (VC a :& b :& r) = pure $ VOption (evalGet a b) :& r
runInstrImpl _ UPDATE (VC a :& b :& c :& r) = pure $ evalUpd a b c :& r
runInstrImpl runner (IF bTrue _) (VC (CvBool True) :& r) = runner bTrue r
runInstrImpl runner (IF _ bFalse) (VC (CvBool False) :& r) = runner bFalse r
runInstrImpl _ (LOOP _) (VC (CvBool False) :& r) = pure $ r
runInstrImpl runner (LOOP ops) (VC (CvBool 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 $ (VC $ CvBytes $ packValue' a) :& r
runInstrImpl _ UNPACK (VC (CvBytes 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 (VC (CvNat o) :& VC (CvNat l) :& s :& r) =
  pure $ VOption (evalSlice o l s) :& r
runInstrImpl _ ISNAT (VC (CvInt i) :& r) =
  if i < 0
  then pure $ VOption Nothing :& r
  else pure $ VOption (Just $ VC (CvNat $ fromInteger i)) :& r
runInstrImpl _ ADD (VC l :& VC r :& rest) =
  (:& rest) <$> runArithOp (Proxy @Add) l r
runInstrImpl _ SUB (VC l :& VC r :& rest) = (:& rest) <$> runArithOp (Proxy @Sub) l r
runInstrImpl _ MUL (VC l :& VC r :& rest) = (:& rest) <$> runArithOp (Proxy @Mul) l r
runInstrImpl _ EDIV (VC l :& VC r :& rest) = pure $ evalEDivOp l r :& rest
runInstrImpl _ ABS (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Abs) a) :& rest
runInstrImpl _ NEG (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Neg) a) :& rest
runInstrImpl _ LSL (VC x :& VC s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsl) x s
runInstrImpl _ LSR (VC x :& VC s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsr) x s
runInstrImpl _ OR (VC l :& VC r :& rest) = (:& rest) <$> runArithOp (Proxy @Or) l r
runInstrImpl _ AND (VC l :& VC r :& rest) = (:& rest) <$> runArithOp (Proxy @And) l r
runInstrImpl _ XOR (VC l :& VC r :& rest) = (:& rest) <$> runArithOp (Proxy @Xor) l r
runInstrImpl _ NOT (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Not) a) :& rest
runInstrImpl _ COMPARE (l :& r :& rest) = pure $ T.VC (T.CvInt (compareOp l r)) :& rest
runInstrImpl _ EQ (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Eq') a) :& rest
runInstrImpl _ NEQ (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Neq) a) :& rest
runInstrImpl _ LT (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Lt) a) :& rest
runInstrImpl _ GT (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Gt) a) :& rest
runInstrImpl _ LE (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Le) a) :& rest
runInstrImpl _ GE (VC a :& rest) = pure $ VC (evalUnaryArithOp (Proxy @Ge) a) :& rest
runInstrImpl _ INT (VC (CvNat n) :& r) = pure $ VC (CvInt $ 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) (VC (CvAddress 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@(AsUType tcSing (ParamNotesUnsafe -> tcNotes)) ->
          case (T.checkOpPresence tcSing, T.checkNestedBigMapsPresence tcSing) of
            (OpAbsent, NestedBigMapsAbsent) -> castContract addr epName (tcSing, tcNotes) :& 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 -> (Sing p, 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 :& VC (CvMutez mutez) :& contract :& r) =
  pure $ VOp (OpTransferTokens $ TransferTokens p mutez contract) :& r
runInstrImpl _ SET_DELEGATE (VOption mbKeyHash :& r) =
  case mbKeyHash of
    Just (VC (CvKeyHash k)) -> pure $ VOp (OpSetDelegate $ SetDelegate $ Just k) :& r
    Nothing -> pure $ VOp (OpSetDelegate $ SetDelegate $ Nothing) :& r
runInstrImpl _ (CREATE_CONTRACT fullContract)
  (VOption mbKeyHash :& (VC (CvMutez 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)
      :& (VC (CvAddress resEpAddr))
      :& r
runInstrImpl _ IMPLICIT_ACCOUNT (VC (CvKeyHash k) :& r) =
  pure $ VContract (KeyAddress k) sepcPrimitive :& r
runInstrImpl _ NOW r = do
  ContractEnv{..} <- ask
  pure $ VC (CvTimestamp ceNow) :& r
runInstrImpl _ AMOUNT r = do
  ContractEnv{..} <- ask
  pure $ VC (CvMutez ceAmount) :& r
runInstrImpl _ BALANCE r = do
  ContractEnv{..} <- ask
  pure $ VC (CvMutez ceBalance) :& r
runInstrImpl _ CHECK_SIGNATURE (VKey k :& VSignature v :&
  VC (CvBytes b) :& r) = pure $ VC (CvBool $ checkSignature k v b) :& r
runInstrImpl _ SHA256 (VC (CvBytes b) :& r) = pure $ VC (CvBytes $ sha256 b) :& r
runInstrImpl _ SHA512 (VC (CvBytes b) :& r) = pure $ VC (CvBytes $ sha512 b) :& r
runInstrImpl _ BLAKE2B (VC (CvBytes b) :& r) = pure $ VC (CvBytes $ blake2b b) :& r
runInstrImpl _ HASH_KEY (VKey k :& r) = pure $ VC (CvKeyHash $ hashKey k) :& r
runInstrImpl _ STEPS_TO_QUOTA r = do
  RemainingSteps x <- gets isRemainingSteps
  pure $ VC (CvNat $ (fromInteger . toInteger) x) :& r
runInstrImpl _ SOURCE r = do
  ContractEnv{..} <- ask
  pure $ VC (CvAddress $ EpAddress ceSource def) :& r
runInstrImpl _ SENDER r = do
  ContractEnv{..} <- ask
  pure $ VC (CvAddress $ EpAddress ceSender def) :& r
runInstrImpl _ ADDRESS (VContract a sepc :& r) =
  pure $ VC (CvAddress $ 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)
  => proxy aop
  -> CValue n
  -> CValue m
  -> EvalOp (T.Value' instr ('Tc (ArithRes aop n m)))
runArithOp op l r = case evalOp op l r of
  Left  err -> throwError (MichelsonArithError err)
  Right res -> pure (T.VC 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 ('Tc 'U.CKeyHash))
  -> Mutez
  -> Contract 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 = convertContract contract
    }

unwrapMbKeyHash :: Maybe (T.Value ('Tc 'U.CKeyHash)) -> Maybe KeyHash
unwrapMbKeyHash mbKeyHash = mbKeyHash <&> \(T.VC (CvKeyHash keyHash)) -> keyHash

interpretExt :: SomeItStack -> EvalOp ()
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

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