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

-- | Executor and typechecker of a contract in Morley language.

module Morley.Michelson.Runtime
  (
    -- * High level interface for end user
    originateContract
  , runContract
  , transfer
  , runCode
  , runView
  , RunCodeParameters(..)
  , runCodeParameters
  , resolveRunCodeBigMaps
  , mkBigMapFinder
  , CommonRunOptions(..)
  , ContractSpecification (..)
  , ContractSimpleOriginationData(..)

  -- * Other helpers
  , parseContract
  , parseExpandContract
  , readAndParseContract
  , prepareContract

  -- * Re-exports
  , ContractState (..)
  , VotingPowers
  , mkVotingPowers
  , mkVotingPowersFromMap
  , TxData (..)
  , TxParam (..)

  -- * For testing
  , ExecutorOp (..)
  , ExecutorRes (..)
  , erGState
  , erUpdates
  , erInterpretResults
  , erRemainingSteps
  , ExecutorError' (..)
  , ExecutorErrorPrim (..)
  , ExecutorError
  , ExecutorM
  , runExecutorM
  , runExecutorMWithDB
  , executeGlobalOperations
  , executeGlobalOrigination
  , executeOrigination
  , executeTransfer
  , ExecutorState(..)
  , esGState
  , esRemainingSteps
  , esSourceAddress
  , esLog
  , esOperationHash
  , esPrevCounters
  , ExecutorLog(..)
  , SomeInterpretResult(..)
  , elInterpreterResults
  , elUpdates
  ) where

import Control.Lens (assign, at, each, ix, makeLenses, to, (.=), (<>=))
import Control.Monad.Except (Except, liftEither, runExcept, throwError)
import Data.Coerce (coerce)
import Data.Constraint (Dict(..), (\\))
import Data.Default (Default(..))
import Data.HashSet qualified as HS
import Data.Semigroup.Generic (GenericSemigroupMonoid(..))
import Data.Singletons (demote)
import Data.Text.IO (getContents)
import Data.Text.IO.Utf8 qualified as Utf8 (readFile)
import Data.Type.Equality (pattern Refl)
import Data.Typeable (cast)
import Fmt (Buildable(build), blockListF, fmt, indentF, nameF, pretty, unlinesF, (+|), (|+))
import Text.Megaparsec (parse)

import Morley.Michelson.Interpret
import Morley.Michelson.Macro (ParsedOp, expandContract)
import Morley.Michelson.Parser qualified as P
import Morley.Michelson.Runtime.Dummy
import Morley.Michelson.Runtime.GState
import Morley.Michelson.Runtime.RunCode
import Morley.Michelson.Runtime.TxData
import Morley.Michelson.TypeCheck
import Morley.Michelson.TypeCheck.Helpers (checkContractDeprecations, checkSingDeprecations)
import Morley.Michelson.Typed
  (Constrained(..), CreateContract(..), EntrypointCallT, EpName, Operation'(..),
  SomeContractAndStorage(..), SomeStorage, TransferTokens(..), sing)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Operation
import Morley.Michelson.Untyped (Contract)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Morley.Tezos.Address.Alias
import Morley.Tezos.Address.Kinds
import Morley.Tezos.Core
  (Mutez, Timestamp(..), getCurrentTime, unsafeAddMutez, unsafeSubMutez, zeroMutez)
import Morley.Tezos.Crypto (KeyHash)
import Morley.Util.Interpolate (itu)
import Morley.Util.MismatchError
import Morley.Util.Named

----------------------------------------------------------------------------
-- Auxiliary types
----------------------------------------------------------------------------

-- | Operations executed by interpreter.
-- In our model one Michelson's operation (@operation@ type in Michelson)
-- corresponds to 0 or 1 interpreter operation.
--
-- Note: 'Address' is not part of 'TxData', because 'TxData' is
-- supposed to be provided by the user, while 'Address' can be
-- computed by our code.
data ExecutorOp
  = OriginateOp OriginationOperation
  -- ^ Originate a contract.
  | TransferOp TransferOperation
  -- ^ Transfer tokens to the address.
  | SetDelegateOp SetDelegateOperation
  -- ^ Set the delegate of a contract.
  | EmitOp EmitOperation
  -- ^ Emit contract event.
  deriving stock (Show)

instance Buildable ExecutorOp where
  build = \case
    TransferOp op -> build op
    OriginateOp op -> build op
    SetDelegateOp op -> build op
    EmitOp op -> build op

data SomeInterpretResult = forall st. SomeInterpretResult
  { unSomeInterpretResult :: InterpretResult st
  }

deriving stock instance Show SomeInterpretResult

-- | Result of a single execution of interpreter.
data ExecutorRes = ExecutorRes
  { _erGState :: GState
  -- ^ New 'GState'.
  , _erUpdates :: [GStateUpdate]
  -- ^ Updates applied to 'GState'.
  , _erInterpretResults :: [(Address, SomeInterpretResult)]
  -- ^ During execution a contract can print logs and in the end it returns
  -- a pair. All logs and returned values are kept until all called contracts
  -- are executed. In the end they are printed.
  , _erRemainingSteps :: RemainingSteps
  -- ^ Now much gas all remaining executions can consume.
  } deriving stock Show

data ExecutorEnv = ExecutorEnv
  { _eeNow :: Timestamp
  , _eeLevel :: Natural
  , _eeMinBlockTime :: Natural
  , _eeTcOpts :: TypeCheckOptions
  , _eeCallChain :: [ExecutorOp]
  }
  deriving stock (Generic)

data ExecutorState = ExecutorState
  { _esGState :: GState
  , _esRemainingSteps :: RemainingSteps
  , _esSourceAddress :: Maybe L1Address
  , _esLog :: ExecutorLog
  , _esOperationHash :: ~OperationHash
  , _esPrevCounters :: HashSet GlobalCounter
  }
  deriving stock (Show, Generic)

data ExecutorLog = ExecutorLog
  { _elUpdates :: [GStateUpdate]
  , _elInterpreterResults :: [(Address, SomeInterpretResult)]
  }
  deriving stock (Show, Generic)
  deriving (Semigroup, Monoid) via GenericSemigroupMonoid ExecutorLog

makeLenses ''ExecutorRes
makeLenses ''ExecutorEnv
makeLenses ''ExecutorState
makeLenses ''ExecutorLog

-- | 'ExecutorErrorPrim', enriched by the list of operations that succeeded
-- before the error.
data ExecutorError' a = ExecutorError
  { eeCallStack :: [ExecutorOp]
  , eeError :: ExecutorErrorPrim a
  } deriving stock (Show, Functor, Foldable, Traversable)

-- | Errors that can happen during contract interpreting.
-- Type parameter @a@ determines how contracts will be represented
-- in these errors, e.g. 'Address'.
data ExecutorErrorPrim a
  = EEUnknownContract a
  -- ^ The interpreted contract hasn't been originated.
  | EEInterpreterFailed a (InterpretError Void)
  -- ^ Interpretation of Michelson contract failed.
  | EEViewLookupError a ViewLookupError
  -- ^ Error looking up view while trying to call it.
  | EEViewArgTcError a TcError
  -- ^ Error type-checking untyped view argument.
  | EEUnknownAddressAlias SomeAlias
  -- ^ The given alias isn't associated with any address
  -- OR is associated with an address of an unexpected kind
  -- (e.g. we expected an implicit address and found a contract address, or vice-versa).
  | EEUnknownL1AddressAlias Text
  -- ^ The given alias is not associated with any address.
  | EEAmbiguousAlias Text ImplicitAddress ContractAddress
  -- ^ The given alias is ambiguous, i.e. it is associated with __both__ an
  -- implicit address and a contract address.
  | EEUnknownSender a
  -- ^ Sender address is unknown.
  | EEUnknownManager a
  -- ^ Manager address is unknown.
  | EENotEnoughFunds a Mutez
  -- ^ Sender doesn't have enough funds.
  | EEEmptyImplicitContract a
  -- ^ Sender is an implicit address with the balance of 0. We mimic
  -- @octez-client@ in calling it "Empty implicit contract".
  | EEZeroTransaction a
  -- ^ Sending 0tz towards an address.
  | EEFailedToApplyUpdates GStateUpdateError
  -- ^ Failed to apply updates to GState.
  | EEIllTypedParameter a TcError
  -- ^ Contract parameter is ill-typed.
  | EEDeprecatedType TcError
  -- ^ Found deprecated types.
  | EEUnexpectedParameterType a (MismatchError T.T)
  -- ^ Contract parameter is well-typed, but its type does
  -- not match the entrypoint's type.
  | EEUnknownEntrypoint EpName
  -- ^ Specified entrypoint to run is not found.
  | EETransactionFromContract a Mutez
  -- ^ A transaction from an originated contract was attempted as a global operation.
  | EEWrongParameterType a
  -- ^ Type of parameter in transfer to an implicit account is not Unit.
  | EEOperationReplay ExecutorOp
  -- ^ An attempt to perform the operation duplicated with @DUP@ instruction.
  | EEGlobalOperationSourceNotImplicit Address
  -- ^ Attempted to initiate global operation from a non-implicit address.
  | EEGlobalEmitOp
  -- ^ Trying to run emit operation as a global operation, which should be impossible.
  deriving stock (Show, Functor, Foldable, Traversable)

instance (Buildable a) => Buildable (ExecutorErrorPrim a) where
  build =
    \case
      EEUnknownAddressAlias (SomeAlias (alias :: Alias kind)) ->
        [itu|The alias '#{alias}' is not associated to a #{kind} address|]
        where
          kind = demote @kind \\ aliasKindSanity alias :: AddressKind
      EEUnknownL1AddressAlias aliasText ->
        [itu|The alias '#{aliasText}' is not associated with any address|]
      EEAmbiguousAlias aliasText implicitAddr contractAddr ->
        [itu|
        The alias '#{aliasText}' is assigned to both:
          * a contract address: #{contractAddr}
          * and an implicit address: #{implicitAddr}
        Use '#{contractPrefix}:#{aliasText}' or '#{implicitPrefix}:#{aliasText}' to disambiguate.
        |]
      EEUnknownContract addr -> "The contract is not originated " +| addr |+ ""
      EEInterpreterFailed addr err ->
        "Michelson interpreter failed for contract " +| addr |+ ": " +| err |+ ""
      EEViewLookupError addr err ->
        nameF ("View lookup for contract " +| addr |+ " failed") $ build err
      EEViewArgTcError addr err ->
        nameF ("Typechecking view argument for contract " +| addr |+ " failed") $ build err
      EEUnknownSender addr -> "The sender address is unknown " +| addr |+ ""
      EEUnknownManager addr -> "The manager address is unknown " +| addr |+ ""
      EENotEnoughFunds addr amount ->
        "The sender (" +| addr |+
        ") doesn't have enough funds (has only " +| amount |+ ")"
      EEEmptyImplicitContract addr ->
        "Empty implicit contract (" +| addr |+ ")"
      EEZeroTransaction addr ->
        "Transaction of 0ꜩ towards a key address " +| addr |+ " which has no code is prohibited"
      EEFailedToApplyUpdates err -> "Failed to update GState: " +| err |+ ""
      EEIllTypedParameter _ err -> "The contract parameter is ill-typed: " +| err |+ ""
      EEDeprecatedType err -> nameF "Deprecation error" $ build err
      EEUnexpectedParameterType _ merr ->
        "The contract parameter is well-typed, but did not match the contract's entrypoint's type.\n"
        +| merr |+ ""
      EEUnknownEntrypoint epName -> "The contract does not contain entrypoint '" +| epName |+ "'"
      EETransactionFromContract addr amount ->
        "Global transaction of funds (" +| amount |+ ") from an originated contract (" +| addr |+ ") is prohibited."
      EEWrongParameterType addr ->
        "Bad contract parameter for: " +| addr |+ ""
      EEOperationReplay op ->
        "Operation replay attempt:\n" +| indentF 2 (build op) |+ ""
      EEGlobalOperationSourceNotImplicit addr ->
        "Attempted to initiate global operation from a non-implicit address " +| addr |+ ""
      EEGlobalEmitOp ->
        "Attempted to run emit event as a global operation, this should be impossible."

-- | To reduce friction between 'ExecutorError'' and 'ExecutorErrorPrim', this
-- instance will try to run 'fromException' for both.
instance (Typeable a, Show a, Buildable a) => Exception (ExecutorErrorPrim a) where
  displayException = pretty
  fromException (SomeException exc) = cast exc <|> fmap eeError (cast exc)

instance (Buildable a) => Buildable (ExecutorError' a) where
  build ExecutorError{..} = unlinesF
    [ build eeError
    , nameF "While running" $ unlinesF $ build <$> eeCallStack
    ]

type ExecutorError = ExecutorError' Address

instance (Typeable a, Show a, Buildable a) => Exception (ExecutorError' a) where
  displayException = pretty

----------------------------------------------------------------------------
-- Interface
----------------------------------------------------------------------------

-- | Parse a contract from 'Text'.
parseContract
  :: P.MichelsonSource -> Text -> Either P.ParserException (U.Contract' ParsedOp)
parseContract source =
  first P.ParserException . parse P.program (pretty source)

-- | Parse a contract from 'Text' and expand macros.
parseExpandContract
  :: P.MichelsonSource -> Text -> Either P.ParserException Contract
parseExpandContract = fmap expandContract ... parseContract

-- | Read and parse a contract from give path or `stdin` (if the
-- argument is 'Nothing'). The contract is not expanded.
readAndParseContract :: Maybe FilePath -> IO (U.Contract' ParsedOp)
readAndParseContract mFilename = do
  code <- readCode mFilename
  either throwM pure $ parseContract (toSrc mFilename) code
  where
    readCode :: Maybe FilePath -> IO Text
    readCode = maybe getContents Utf8.readFile

    toSrc :: Maybe FilePath -> P.MichelsonSource
    toSrc = maybe P.MSUnspecified P.MSFile

-- | Read a contract using 'readAndParseContract', expand and
-- flatten. The contract is not type checked.
prepareContract :: Maybe FilePath -> IO Contract
prepareContract mFile = expandContract <$> readAndParseContract mFile

-- | Originate a contract. Returns the address of the originated
-- contract.
originateContract
  :: "dbPath" :! FilePath
  -> "tcOpts" :? TypeCheckOptions
  -> "originator" :? ImplicitAddress
  -> "alias" :? ContractAlias
  -> "delegate" :? KeyHash
  -> "csod" :! ContractSimpleOriginationData U.Contract
  -> "verbose" :? Bool
  -> IO ContractAddress
originateContract
  (arg #dbPath -> croDBPath)
  (argDef #tcOpts def -> croTCOpts)
  originator
  alias
  (argF #delegate -> mbDelegate)
  (arg #csod -> csod)
  (argDef #verbose False -> croVerbose)
  = do
  origination <- either throwM pure $
    mkOrigination croTCOpts csod originator alias ! #delegate mbDelegate
  let croDryRun = False
  fmap snd $ runExecutorMWithDB def{croDBPath, croDryRun, croVerbose, croTCOpts} $
    executeGlobalOrigination origination

-- | Run a contract. The contract is originated first (if it's not
-- already) and then we pretend that we send a transaction to it.
runContract
  :: CommonRunOptions
  -> ContractSimpleOriginationData U.Contract
  -> TxData
  -> IO SomeStorage
runContract cro@CommonRunOptions{..} csOrig txData = do
  origination <- either throwM pure $ mkOrigination croTCOpts csOrig ! def
  (_, newSt) <- runExecutorMWithDB cro do
    -- Here we are safe to bypass executeGlobalOperations for origination,
    -- since origination can't generate more operations.
    addr <- executeGlobalOrigination origination
    let transferOp = TransferOp $ TransferOperation (MkAddress addr) txData 1
    void $ executeGlobalOperations [transferOp]
    getContractStorage addr
  return newSt
  where
    getContractStorage :: ContractAddress -> ExecutorM SomeStorage
    getContractStorage addr = do
      addrs <- use (esGState . gsContractAddressesL)
      case addrs ^. at addr of
        Nothing -> error $ pretty addr <> " is unknown"
        Just ContractState{..} -> return $ SomeStorage csStorage

data ContractSpecification a
  = ContractSpecAddressOrAlias ContractAddressOrAlias
  | ContractSpecOrigination a
  deriving stock (Functor, Foldable, Traversable)

data ContractSimpleOriginationData a = ContractSimpleOriginationData
  { csodContract :: a
  , csodStorage :: U.Value
  , csodBalance :: Mutez
  }
  deriving stock (Functor, Foldable, Traversable)

data CommonRunOptions = CommonRunOptions
  { croNow :: Maybe Timestamp
  , croLevel :: Natural
  , croMinBlockTime :: Natural
  , croMaxSteps :: RemainingSteps
  , croDBPath :: FilePath
  , croTCOpts :: TypeCheckOptions
  , croVerbose :: Bool
  , croDryRun :: Bool
  }

instance Default CommonRunOptions where
  def = CommonRunOptions
    { croNow = Nothing
    , croLevel = 0
    , croMinBlockTime = dummyMinBlockTime
    , croMaxSteps = dummyMaxSteps
    , croDBPath = "db.json"
    , croTCOpts = def
    , croVerbose = False
    , croDryRun = True
    }

-- | Run a contract view. The contract is originated first (if it's not already)
-- and then we pretend that we send a transaction to it.
runView
  :: CommonRunOptions
  -> ContractSpecification (ContractSimpleOriginationData U.Contract)
  -> U.ViewName
  -> SomeAddressOrAlias
  -> TxParam
  -> IO T.SomeValue
runView cro@CommonRunOptions{..} contractOrAddr viewName sender' viewArg = do
  origination <- traverse (either throwM pure . (mkOrigination croTCOpts ! def)) contractOrAddr
  (_, newSt) <- runExecutorMWithDB cro do
      addr <- case origination of
        ContractSpecAddressOrAlias addr -> resolveContractAddress addr
        ContractSpecOrigination origOp -> executeGlobalOrigination origOp
      -- Here we are safe to bypass executeGlobalOperations for origination,
      -- since origination can't generate more operations.
      sender <- resolveAddress sender'
      callView sender addr viewName viewArg
  return newSt

mkOrigination
  :: TypeCheckOptions
  -> ContractSimpleOriginationData U.Contract
  -> "originator" :? ImplicitAddress
  -> "alias" :? ContractAlias
  -> "delegate" :? Maybe KeyHash
  -> Either TcError OriginationOperation
mkOrigination tcOpts ContractSimpleOriginationData{..}
  (argDef #originator genesisAddress -> ooOriginator)
  (argF #alias -> ooAlias)
  (argDef #delegate (Just dummyDelegate) -> ooDelegate)
  = do
  SomeContractAndStorage ooContract ooStorage <- typeCheckingWith tcOpts $
    typeCheckContractAndStorage csodContract csodStorage
  pure OriginationOperation
    { ooBalance = csodBalance
    , ooCounter = 0
    , ..
    }

-- | We hardcode some random key hash here as delegate to make sure that:
--
-- 1. Contract's address won't clash with already originated one (because it may
-- have different storage value which may be confusing).
--
-- 2. If one uses this functionality twice with the same contract and other
-- data, the contract will have the same address.
dummyDelegate :: KeyHash
dummyDelegate =  let ImplicitAddress kh = [ta|tz1YCABRTa6H8PLKx2EtDWeCGPaKxUhNgv47|] in kh

-- | Construct 'BigMapFinder' using the current executor context.
mkBigMapFinder :: ExecutorM BigMapFinder
mkBigMapFinder = do
  pureState <- get

  pure \bigMapId ->
    pureState ^?
      esGState . gsContractAddressesL . each . to getContractStorage .
        to (getBigMapsWithId bigMapId) . each
  where
    getContractStorage :: ContractState -> T.SomeValue
    getContractStorage (ContractState _ _ storage _) = T.SomeValue storage

    getBigMapsWithId :: Natural -> T.SomeValue -> [T.SomeVBigMap]
    getBigMapsWithId bigMapId (T.SomeValue val) =
      T.dfsFoldMapValue
        (\v -> case v of
            T.VBigMap (Just bigMapId') _ | bigMapId' == bigMapId -> [T.SomeVBigMap v]
            _ -> []
        )
        val

-- | Send a transaction to given address with given parameters.
transfer
  :: CommonRunOptions
  -> SomeAddressOrAlias
  -> TxData
  -> IO ()
transfer cro destination txData = do
  -- TODO [#905]: simplify with convertAddress
  void $ runExecutorMWithDB @[EmitOperation] cro $ do
    Constrained destAddr <- resolveAddress destination
    executeGlobalOperations [TransferOp $ TransferOperation (MkAddress destAddr) txData 0]

----------------------------------------------------------------------------
-- Executor
----------------------------------------------------------------------------

-- | A monad in which contract executor runs.
type ExecutorM =
  ReaderT ExecutorEnv
    (StateT ExecutorState
      (Except ExecutorError)
    )

-- | Run some executor action, returning its result and final executor state in 'ExecutorRes'.
--
-- The action has access to the hash of currently executed global operation, in order to construct
-- addresses of originated contracts. It is expected that the action uses @#isGlobalOp :! True@
-- to specify this hash. Otherwise it is initialized with 'error'.
runExecutorM
  :: Timestamp
  -> Natural
  -> Natural
  -> RemainingSteps
  -> TypeCheckOptions
  -> GState
  -> ExecutorM a
  -> Either ExecutorError (ExecutorRes, a)
runExecutorM now level minBlockTime remainingSteps tcOpts gState action =
  fmap preResToRes
    $ runExcept
    $ runStateT (runReaderT action $ ExecutorEnv now level minBlockTime tcOpts mempty)
      initialState
  where
    initialOpHash = error "Initial OperationHash touched"

    initialState = ExecutorState
      { _esGState = gState
      , _esRemainingSteps = remainingSteps
      , _esSourceAddress = Nothing
      , _esLog = mempty
      , _esOperationHash = initialOpHash
      , _esPrevCounters = mempty
      }

    preResToRes :: (a, ExecutorState) -> (ExecutorRes, a)
    preResToRes (r, ExecutorState{..}) =
      ( ExecutorRes
          { _erGState = _esGState
          , _erUpdates = _esLog ^. elUpdates
          , _erInterpretResults = _esLog ^. elInterpreterResults
          , _erRemainingSteps = _esRemainingSteps
          }
      , r
      )

-- | Run some executor action, reading state from the DB on disk.
--
-- If 'croDryRun' is @False@, the final state is written back to the disk.
--
-- If the executor fails with t'ExecutorError' it will be thrown as an exception.
runExecutorMWithDB
  :: CommonRunOptions
  -> ExecutorM a
  -> IO (ExecutorRes, a)
runExecutorMWithDB (CommonRunOptions mNow level minBlockTime steps dbPath tcOpts verbose dryRun) action = do
  gState <- readGState dbPath
  now <- maybe getCurrentTime pure mNow
  (res@ExecutorRes{..}, a) <- either throwM pure $
    runExecutorM now level minBlockTime steps tcOpts gState action

  unless dryRun $
    writeGState dbPath _erGState

  mapM_ printInterpretResult _erInterpretResults
  when (verbose && not (null _erUpdates)) $ do
    putTextLn $ fmt $ nameF "Updates" (blockListF _erUpdates)
    putTextLn $ "Remaining gas: " <> pretty _erRemainingSteps <> "."

  return (res, a)
  where
    printInterpretResult
      :: (Address, SomeInterpretResult) -> IO ()
    printInterpretResult
      (addr, SomeInterpretResult ResultStateLogs{..}) = do
      putTextLn $ "Executed contract " <> pretty addr
      () <- case rslResult of
        T.VPair (ops@T.VList{}, res)
          | _ :: T.Value ('T.TList ops) <- ops
          , T.STOperation <- T.sing @ops \\ T.valueTypeSanity ops
          -> do
              putTextLn $ case T.fromVal @[T.Operation] ops of
                [] -> "It didn't return any operations."
                xs -> fmt $ nameF "It returned operations" (blockListF xs)
              putTextLn $ "It returned: " <> pretty res <> "."
        _ -> putTextLn $ "It returned: " <> pretty rslResult <> "."
      let MorleyLogs logs = rslLogs
      unless (null logs) $ do
        putTextLn "And produced logs:"
        mapM_ putTextLn logs
      putTextLn "" -- extra break line to separate logs from two sequence contracts

-- | Resolves 'SomeAddressOrAlias' type to an address.
resolveAddress
  :: SomeAddressOrAlias
  -> ExecutorM L1Address
resolveAddress = \case
  SAOAKindUnspecified aliasText -> do
    implicitAddrMb <- preuse $ esGState . gsImplicitAddressAliasesL . ix (ImplicitAlias aliasText)
    contractAddrMb <- preuse $ esGState . gsContractAddressAliasesL . ix (ContractAlias aliasText)
    case (implicitAddrMb, contractAddrMb) of
      (Nothing, Nothing) -> throwEE $ EEUnknownL1AddressAlias aliasText
      (Just implicitAddr, Nothing) -> pure $ Constrained implicitAddr
      (Nothing, Just contractAddr) -> pure $ Constrained contractAddr
      (Just implicitAddr, Just contractAddr) -> throwEE $ EEAmbiguousAlias aliasText implicitAddr contractAddr
  SAOAKindSpecified (AddressResolved (addr@ContractAddress{})) -> pure $ Constrained addr
  SAOAKindSpecified (AddressResolved (addr@ImplicitAddress{})) -> pure $ Constrained addr
  SAOAKindSpecified (AddressAlias alias) -> do
    addrMb <- preuse $
      case alias of
        ImplicitAlias{} -> esGState . gsImplicitAddressAliasesL . ix alias . to Constrained
        ContractAlias{} -> esGState . gsContractAddressAliasesL . ix alias . to Constrained
    case addrMb of
      Just addr -> pure addr
      Nothing -> throwEE $ EEUnknownAddressAlias $ SomeAlias alias

-- | Resolves 'ContractAddressOrAlias' type to an address.
resolveContractAddress
  :: ContractAddressOrAlias
  -- TODO [#905] or [#889]: Change the return type to `L1Address`
  -> ExecutorM ContractAddress
resolveContractAddress ct = case ct of
  AddressResolved r -> pure r
  AddressAlias alias -> resolveAddress (SAOAKindSpecified ct) >>= \case
    Constrained result -> case result of
      ContractAddress{} -> pure result
      ImplicitAddress{} -> throwEE $ EEUnknownAddressAlias (SomeAlias alias)

-- | Execute a list of global operations, returning a list of generated events.
executeGlobalOperations
  :: [ExecutorOp]
  -> ExecutorM [EmitOperation]
executeGlobalOperations = concatMapM $ \op -> executeMany (#isGlobalOp :! True) [op]
  where
    -- Execute a list of operations and additional operations they return, until there are none.
    executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM [EmitOperation]
    executeMany isGlobalOp = \case
        [] -> pure []
        (op:opsTail) -> addStackEntry op do
          case op of
            OriginateOp origination -> do
              void $ executeOrigination isGlobalOp origination
              executeMany (#isGlobalOp :! False) opsTail
            SetDelegateOp operation -> do
              executeDelegation isGlobalOp operation
              executeMany (#isGlobalOp :! False) opsTail
            TransferOp transferOperation -> do
              moreOps <- executeTransfer isGlobalOp transferOperation
              executeMany (#isGlobalOp :! False) $ moreOps <> opsTail
            EmitOp emitOperation -> do
              liftM2 (:) (executeEmit isGlobalOp emitOperation) $
                executeMany (#isGlobalOp :! False) opsTail

-- | Execute a global origination operation.
executeGlobalOrigination :: OriginationOperation -> ExecutorM ContractAddress
executeGlobalOrigination = executeOrigination ! #isGlobalOp True

-- | Execute an origination operation.
executeOrigination
  :: "isGlobalOp" :! Bool
  -> OriginationOperation
  -> ExecutorM ContractAddress
executeOrigination (arg #isGlobalOp -> isGlobalOp) origination@(OriginationOperation{..}) = do
  when isGlobalOp $ do
    beginGlobalOperation
    assign esOperationHash $ mkOriginationOperationHash origination

  checkOperationReplay $ OriginateOp origination

  tcOpts <- view eeTcOpts

  when (tcStrict tcOpts) $
    liftEE $ first EEDeprecatedType $ checkContractDeprecations ooContract

  opHash <- use esOperationHash

  gs <- use esGState

  -- Add big_map IDS to storage
  let bigMapCounter0 = gs ^. gsBigMapCounterL
  let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds False ooStorage) bigMapCounter0

  let contractState = ContractState ooBalance ooContract storageWithIds ooDelegate

  let originatorAddress = ooOriginator

  originatorBalance <- case lookupBalance originatorAddress gs of
    Nothing -> throwEE $ EEUnknownManager $ MkAddress ooOriginator
    Just oldBalance
      | oldBalance < ooBalance ->
        throwEE $ EENotEnoughFunds (MkAddress ooOriginator) oldBalance
      | otherwise ->
        -- Subtraction is safe because we have checked its
        -- precondition in guard.
        return $ oldBalance `unsafeSubMutez` ooBalance
  let
    address = mkContractAddress opHash ooCounter
    updates =
      catMaybes
        [ liftA2 GSAddContractAddressAlias ooAlias (Just address)
        , Just $ GSAddContractAddress address contractState
        , Just $ GSSetBalance originatorAddress originatorBalance
        , Just GSIncrementCounter
        , if bigMapCounter0 == bigMapCounter1
            then Nothing
            else Just $ GSSetBigMapCounter bigMapCounter1
        ]

  case applyUpdates updates gs of
    Left err -> throwEE $ EEFailedToApplyUpdates err
    Right newGS -> do
      esGState .= newGS
      esLog <>= ExecutorLog updates []

      return address

-- | Execute delegation operation.
executeDelegation
  :: "isGlobalOp" :! Bool
  -> SetDelegateOperation
  -> ExecutorM ()
executeDelegation (arg #isGlobalOp -> isGlobalOp) delegation@SetDelegateOperation{..} = do
  when isGlobalOp $ do
    beginGlobalOperation
    assign esOperationHash $ mkDelegationOperationHash delegation

  checkOperationReplay $ SetDelegateOp delegation

  gs <- use esGState

  Constrained address <- pure sdoContract

  let updates = [GSSetDelegate address sdoDelegate]
  case applyUpdates updates gs of
    Left err -> throwEE $ EEFailedToApplyUpdates err
    Right newGS -> do
      esGState .= newGS
      esLog <>= ExecutorLog updates []

      return ()

-- | Execute delegation operation.
executeEmit
  :: "isGlobalOp" :! Bool
  -> EmitOperation
  -> ExecutorM EmitOperation
executeEmit (arg #isGlobalOp -> isGlobalOp) op = do
  when isGlobalOp $ throwEE EEGlobalEmitOp
  checkOperationReplay $ EmitOp op
  pure op

mkContractEnv
  :: ("balance" :! Mutez)
  -> ("self" :! ContractAddress)
  -> ("sender" :! L1Address)
  -> ("amount" :! Mutez)
  -> ("useOpHash" :! Bool)
  -> ExecutorM ContractEnv
mkContractEnv
  (arg #balance -> ceBalance)
  (arg #self -> ceSelf)
  (arg #sender -> ceSender)
  (arg #amount -> ceAmount)
  (arg #useOpHash -> useOpHash) = do
  ceNow <- view eeNow
  ceLevel <- view eeLevel
  ceMinBlockTime <- view eeMinBlockTime
  ceOperationHash <- if useOpHash then Just <$> use esOperationHash else pure Nothing
  GState
    { gsChainId = ceChainId
    , gsContractAddresses=ceContractsMap
    , gsVotingPowers = ceVotingPowers
    } <- use esGState
  ceMaxSteps <- use esRemainingSteps
  ceSource <- fromMaybe ceSender <$> use esSourceAddress
  pure ContractEnv
    { ceErrorSrcPos = def
    , ceMetaWrapper = id
    , ceContracts = \addr -> pure $ ceContractsMap ^. at addr
    , ..
    }

-- | Typeckeck if necessary and assign big map ids to a parameter.
prepareParameter
  :: forall arg. T.SingI arg
  => ContractAddress
  -> TxParam
  -> "typedParamError" :! (Address -> MismatchError T.T -> ExecutorErrorPrim Address)
  -> "untypedParamError" :! (Address -> TcError -> ExecutorErrorPrim Address)
  -> ExecutorM (T.Value arg, BigMapCounter)
prepareParameter addr tdParameter
  (arg #typedParamError -> tyParErr)
  (arg #untypedParamError -> unTyParErr)
  = do
  tcOpts <- view eeTcOpts
  gs <- use esGState
  let existingContracts = extractAllContracts gs
  when (tcStrict tcOpts) $ liftEE $ first EEDeprecatedType $ checkSingDeprecations (sing @arg)
  -- If the parameter has already been typechecked, simply check if
  -- its type matches the contract's entrypoint's type.
  -- Otherwise (e.g. if it was parsed from stdin via the CLI),
  -- we need to typecheck the parameter.
  typedParameter <-
    case tdParameter of
      TxTypedParam (typedVal :: T.Value t) ->
        T.castM @t @arg typedVal $
          throwEE . tyParErr (MkAddress addr)
      TxUntypedParam untypedVal ->
        liftEE $ first (unTyParErr $ MkAddress addr) $
          typeCheckingWith tcOpts $
            typeVerifyParameter @arg existingContracts untypedVal

  pure $ runState (assignBigMapIds False typedParameter) $ gs ^. gsBigMapCounterL

-- | Execute a transfer operation.
--
-- Note: we're handling both XTZ and ticket transfers here to avoid code
-- duplication. We assume that if an implicit account sends tickets via
-- 'TxTypedParam', it should be interpreted as @transfer_ticket@ manager
-- operation, and not a regular transfer.
--
-- Note that this only works for 'TxTypedParam', as for ticket transfers between
-- implicit accounts we can't know the exact type of the ticket to transfer if
-- the value is untyped.
executeTransfer
  :: "isGlobalOp" :! Bool
  -> TransferOperation
  -> ExecutorM [ExecutorOp]
executeTransfer (arg #isGlobalOp -> isGlobalOp) transferOperation
  | TransferOperation addr' txData _ <- transferOperation
  , MkAddress (addr :: KindedAddress kind) <- addr'
  , TxData{tdSenderAddress=Constrained senderAddr,..} <- txData
  = do
    when isGlobalOp $
      beginGlobalOperation

    gs <- use esGState
    remainingSteps <- use esRemainingSteps
    sourceAddr <- fromMaybe (tdSenderAddress txData) <$> use esSourceAddress

    let globalCounter = gsCounter gs
    let addresses :: Map (KindedAddress kind) (AddressStateFam kind)
        addresses = gs ^. addressesL addr
    let isZeroTransfer = tdAmount == zeroMutez
    let senderBalance = lookupBalance senderAddr gs

    checkOperationReplay $ TransferOp transferOperation

    -- Implicit addresses can't be senders with a balance of 0tz even when the transfer amount
    -- is zero.
    case isImplicitAddress senderAddr of
      Nothing -> do
        when (isGlobalOp && not isZeroTransfer) $
          throwEE $ EETransactionFromContract (MkAddress senderAddr) tdAmount

      Just Refl -> do
        case senderBalance of
          Nothing -> throwEE $ EEEmptyImplicitContract $ MkAddress senderAddr
          Just balance | balance == zeroMutez ->
            throwEE $ EEEmptyImplicitContract $ MkAddress senderAddr
          _ -> pass

    case isImplicitAddress addr of
      Nothing -> pass
      Just Refl -> do
        when (badParamToImplicitAccount tdParameter) $
          throwEE $ EEWrongParameterType $ MkAddress addr

        -- Transferring 0 XTZ to a key address is prohibited.
        when (isZeroTransfer && isUnitParam tdParameter) $
          throwEE $ EEZeroTransaction $ MkAddress addr

    mDecreaseSenderBalance <- case senderBalance of
      _ | isZeroTransfer -> pure Nothing
      Nothing -> throwEE $ EEUnknownSender $ MkAddress senderAddr
      Just balance
        | balance < tdAmount ->
          throwEE $ EENotEnoughFunds (MkAddress senderAddr) balance
        | otherwise -> do
          -- Subtraction is safe because we have checked its
          -- precondition in guard.
          let newBal = balance `unsafeSubMutez` tdAmount
          pure $ Just $ GSSetBalance senderAddr newBal

    let mDecreaseSenderTickets :: Maybe GStateUpdate
          | Just Refl <- isImplicitAddress senderAddr
          -- if an implicit account sends tickets, it can't forge them, so it
          -- must own them.
          = uncurry (GSRemoveTickets senderAddr) <$> sentTickets
          | otherwise = Nothing
        sentTickets :: Maybe (TicketKey, Natural)
          | TxTypedParam v@T.VTicket{} <- tdParameter
          = Just $ toTicketKey v
          | otherwise = Nothing

    let commonFinishup
          :: Dict (L1AddressKind kind)
          -- NB: this is a Dict and not a constraint because GHC desugars these
          -- let-bindings such that it expects this constraint at the definition
          -- site.
          -> [GStateUpdate]
          -> [T.Operation]
          -> Maybe SomeInterpretResult
          -> RemainingSteps
          -> ExecutorM [ExecutorOp]
        commonFinishup Dict otherUpdates sideEffects maybeInterpretRes newRemSteps = do
          let
            -- According to the reference implementation, counter is incremented for transfers as well.
            updates = catMaybes [mDecreaseSenderBalance, mDecreaseSenderTickets] <> otherUpdates
              <> [GSIncrementCounter]

          newGState <- liftEE $ first EEFailedToApplyUpdates $ applyUpdates updates gs

          esGState .= newGState
          esRemainingSteps .= newRemSteps
          esSourceAddress .= Just sourceAddr

          esLog <>= ExecutorLog updates
            ( maybe
                mempty
                (one . (MkAddress addr,))
                maybeInterpretRes
            )

          mapM (convertOp addr) $ sideEffects
        onlyUpdates :: Dict (L1AddressKind kind) -> [GStateUpdate] -> ExecutorM [ExecutorOp]
        onlyUpdates dict updates = commonFinishup dict updates [] Nothing remainingSteps

    case addr of
      SmartRollupAddress{} ->
        throwEE $ EEUnknownContract (MkAddress addr)
      ImplicitAddress{} -> case addresses ^. at addr of
        Nothing -> onlyUpdates Dict . one $
          GSAddImplicitAddress addr tdAmount $ maybeToList sentTickets
        Just ImplicitState{..} -> do
          let
            -- Calculate the account's new balance.
            --
            -- Note: `unsafeAddMutez` can't overflow if global state is correct
            -- (because we can't create money out of nowhere)
            newBalance = isBalance `unsafeAddMutez` tdAmount
            updBalance
              | tdAmount == zeroMutez = Nothing
              | otherwise = Just $ GSSetBalance addr newBalance
            updTickets = uncurry (GSAddTickets addr) <$> sentTickets
          onlyUpdates Dict $ catMaybes [updBalance, updTickets]
      ContractAddress{} -> case addresses ^. at addr of
        Nothing -> throwEE $ EEUnknownContract (MkAddress addr)
        Just ContractState{..} -> do
          let
            -- Calculate the contract's new balance.
            --
            -- Note: `unsafeAddMutez` can't overflow if global state is
            -- correct (because we can't create money out of nowhere)
            newBalance = csBalance `unsafeAddMutez` tdAmount
            epName = tdEntrypoint

          T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)
            <- T.mkEntrypointCall epName (T.cParamNotes csContract)
              & maybe (throwEE $ EEUnknownEntrypoint epName) pure

          (typedParameterWithIds, bigMapCounter1) <- prepareParameter addr tdParameter
            ! #typedParamError EEUnexpectedParameterType
            ! #untypedParamError EEIllTypedParameter

          -- I'm not entirely sure why we need to pattern match on `()` here,
          -- but, if we don't, we get a compiler error that I suspect is somehow related
          -- to the existential types we're matching on a few lines above.
          --
          -- • Couldn't match type ‘a0’
          --                  with ‘(InterpretResult, RemainingSteps, [Operation], [GStateUpdate])’
          --     ‘a0’ is untouchable inside the constraints: StorageScope st1
          () <- when isGlobalOp $ esOperationHash .= case isImplicitAddress senderAddr of
            Just Refl | Just (tKey, tAmount) <- sentTickets
              -- transfer_ticket is only used when sender is implicit address,
              -- contracts use regular transfer to send tickets.
              -> mkTransferTicketOperationHash tKey tAmount (MkAddress addr) tdEntrypoint
            _ -> mkTransferOperationHash addr typedParameterWithIds tdEntrypoint tdAmount

          contractEnv <- mkContractEnv
            ! #balance newBalance
            ! #self addr
            ! #sender (Constrained senderAddr)
            ! #amount tdAmount
            ! #useOpHash True

          iur@(ResultStateLogs
            { rslResult = extractValOps -> (sideEffects, newValue)
            , rslState = InterpreterState newRemainingSteps globalCounter2 bigMapCounter2
            })
            <- liftEE $ first (EEInterpreterFailed (MkAddress addr)) $
                handleReturn $
                  interpret
                    csContract
                    epc
                    typedParameterWithIds
                    csStorage
                    (gsCounter gs)
                    bigMapCounter1
                    contractEnv

          let
            updBalance
              | newBalance == csBalance = Nothing
              | otherwise = Just $ GSSetBalance addr newBalance
            updStorage
              | SomeValue newValue == SomeValue csStorage = Nothing
              | otherwise = Just $ GSSetStorageValue addr newValue
            updBigMapCounter
              | gs ^. gsBigMapCounterL == bigMapCounter2 = Nothing
              | otherwise = Just $ GSSetBigMapCounter bigMapCounter2
            updGlobalCounter
              | globalCounter == globalCounter2 = Nothing
              | otherwise = Just $ GSUpdateCounter globalCounter2
            updates = catMaybes
              [ updBalance
              , updStorage
              , updBigMapCounter
              , updGlobalCounter
              ]
          commonFinishup Dict updates sideEffects (Just $ SomeInterpretResult iur)
            newRemainingSteps

-- | Execute a view.
callView
  :: L1Address
  -> ContractAddress
  -> U.ViewName
  -> TxParam
  -> ExecutorM T.SomeValue
callView sender addr viewName viewArg = do
  ContractState{..} <-
    use (esGState . gsContractAddressesL . at addr)
    >>= maybe (throwEE $ EEUnknownContract (MkAddress addr)) pure

  T.SomeView (view'@T.View{} :: T.View viewArg st viewRet)
    <- liftEE $ first (EEViewLookupError (Constrained addr)) $ getViewByName csContract viewName

  (typedParameterWithIds, bigMapCounter1) <- prepareParameter addr viewArg
    ! #typedParamError (\a -> EEViewLookupError a . ViewArgMismatch)
    ! #untypedParamError EEViewArgTcError

  contractEnv <- mkContractEnv
    ! #balance csBalance
    ! #self addr
    ! #sender sender
    ! #amount zeroMutez
    ! #useOpHash False

  counter <- use $ esGState . gsCounterL
  remainingSteps <- use esRemainingSteps

  iur@ResultStateLogs{..} <-
    liftEE $ first (EEInterpreterFailed (MkAddress addr)) $
      handleReturn $ interpretView
        view'
        csStorage
        typedParameterWithIds
        contractEnv
        (InterpreterState remainingSteps counter bigMapCounter1)

  esLog <>= ExecutorLog [] (one . (MkAddress addr, ) $ SomeInterpretResult iur)

  pure . SomeValue $ rslResult


----------------------------------------------------------------------------
-- Simple helpers
----------------------------------------------------------------------------

checkOperationReplay :: ExecutorOp -> ExecutorM ()
checkOperationReplay op = do
  let
    opCounter = op & \case
      OriginateOp OriginationOperation{..} -> ooCounter
      TransferOp TransferOperation{..} -> toCounter
      SetDelegateOp SetDelegateOperation{..} -> sdoCounter
      EmitOp (EmitOperation _ T.Emit{..}) -> emCounter
  prevCounters <- use esPrevCounters
  when (opCounter `HS.member` prevCounters) $
    throwEE $ EEOperationReplay op
  esPrevCounters <>= one opCounter

-- The argument is the address of the contract that generated this operation.
convertOp :: L1AddressKind kind => KindedAddress kind -> T.Operation -> ExecutorM ExecutorOp
convertOp interpretedAddr =
  \case
    OpTransferTokens tt ->
      pure $ case ttContract tt of
        T.VContract destAddress sepc ->
          let txData =
                TxData
                  { tdSenderAddress = Constrained interpretedAddr
                  , tdEntrypoint = T.sepcName sepc
                  , tdParameter = TxTypedParam (ttTransferArgument tt)
                  , tdAmount = ttAmount tt
                  }
              transferOperation =
                TransferOperation
                  { toDestination = destAddress
                  , toTxData = txData
                  , toCounter = ttCounter tt
                  }
          in TransferOp transferOperation
    OpSetDelegate T.SetDelegate{..} -> pure $ SetDelegateOp SetDelegateOperation
      { sdoContract = Constrained interpretedAddr
      , sdoDelegate = sdMbKeyHash
      , sdoCounter = sdCounter
      }
    OpCreateContract CreateContract{ccOriginator=Constrained ccOriginator, ..} ->
      pure $ OriginateOp OriginationOperation
        { ooOriginator = ccOriginator
        , ooDelegate = ccDelegate
        , ooBalance = ccBalance
        , ooStorage = ccStorageVal
        , ooContract = ccContract
        , ooCounter = ccCounter
        , ooAlias = Nothing
        }
    OpEmit emit -> case interpretedAddr of
      ContractAddress{} -> pure $ EmitOp $ EmitOperation interpretedAddr emit
      _ -> throwEE $ EEUnknownContract $ MkAddress interpretedAddr

-- | Reset source address before executing a global operation.
beginGlobalOperation :: ExecutorM ()
beginGlobalOperation =
  esSourceAddress .= Nothing

-- | Return True if the param is not Unit or ticket.
badParamToImplicitAccount :: TxParam -> Bool
badParamToImplicitAccount (TxTypedParam T.VTicket{})   = False
badParamToImplicitAccount param = not $ isUnitParam param

-- | Return True if parameter is @Unit@.
isUnitParam :: TxParam -> Bool
isUnitParam (TxTypedParam T.VUnit)       = True
isUnitParam (TxUntypedParam U.ValueUnit) = True
isUnitParam _ = False

getContractStack :: ExecutorM [ExecutorOp]
getContractStack = reverse <$> view eeCallChain

throwEE :: ExecutorErrorPrim Address -> ExecutorM r
throwEE err = throwError . flip ExecutorError err =<< getContractStack

liftEE :: Either (ExecutorErrorPrim Address) r -> ExecutorM r
liftEE x = do
  stack <- getContractStack
  liftEither . first (ExecutorError stack) $ x

addStackEntry :: ExecutorOp -> ExecutorM a -> ExecutorM a
addStackEntry entry = local (eeCallChain %~ coerce (entry :))