🏗️ Apply.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Apply_results.
Require TezosOfOCaml.Proto_alpha.Baking.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_apply.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_operations.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_interpreter_mli.
  Module Script_interpreter := Script_interpreter_mli.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Ticket_accounting.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Require TezosOfOCaml.Proto_alpha.Ticket_transfer.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_apply.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_verifier.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_apply.

Module Not_enough_endorsements.
  Record record : Set := Build {
    required : int;
    provided : int;
  }.
  Definition with_required required (r : record) :=
    Build required r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(required) provided.
End Not_enough_endorsements.
Definition Not_enough_endorsements := Not_enough_endorsements.record.

Module Set_deposits_limit_too_high.
  Record record : Set := Build {
    limit : Alpha_context.Tez.t;
    max_limit : Alpha_context.Tez.t;
  }.
  Definition with_limit limit (r : record) :=
    Build limit r.(max_limit).
  Definition with_max_limit max_limit (r : record) :=
    Build r.(limit) max_limit.
End Set_deposits_limit_too_high.
Definition Set_deposits_limit_too_high := Set_deposits_limit_too_high.record.

Init function; without side-effects in Coq

Definition init_module1 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.not_enough_endorsements" "Not enough endorsements"
      "The block being validated does not include the required minimum number of endorsements."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : int × int) ⇒
            let '(required, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Wrong number of endorsements ("
                  (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal "), at least "
                      (CamlinternalFormatBasics.Int
                        CamlinternalFormatBasics.Int_i
                        CamlinternalFormatBasics.No_padding
                        CamlinternalFormatBasics.No_precision
                        (CamlinternalFormatBasics.String_literal " are expected"
                          CamlinternalFormatBasics.End_of_format)))))
                "Wrong number of endorsements (%i), at least %i are expected")
              provided required))
      (Data_encoding.obj2
        (Data_encoding.req None None "required" Data_encoding.int31)
        (Data_encoding.req None None "provided" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Not_enough_endorsements" then
            let '{|
              Not_enough_endorsements.required := required;
                Not_enough_endorsements.provided := provided
                |} := cast Not_enough_endorsements payload in
            Some (required, provided)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(required, provided) := function_parameter in
        Build_extensible "Not_enough_endorsements" Not_enough_endorsements
          {| Not_enough_endorsements.required := required;
            Not_enough_endorsements.provided := provided; |}) in
  let description :=
    "The consensus operation uses an invalid slot. This error should not happen: the operation validation should have failed earlier."
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.faulty_validation_wrong_slot"
      "Faulty validation (wrong slot for consensus operation)" description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Faulty_validation_wrong_slot" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Faulty_validation_wrong_slot" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.set_deposits_limit_on_unregistered_delegate"
      "Set deposits limit on an unregistered delegate"
      "Cannot set deposits limit on an unregistered delegate."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (c_value : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot set a deposits limit on the unregistered delegate "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal "." % char
                      CamlinternalFormatBasics.End_of_format)))
                "Cannot set a deposits limit on the unregistered delegate %a.")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) c_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Set_deposits_limit_on_unregistered_delegate" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "Set_deposits_limit_on_unregistered_delegate"
          Signature.public_key_hash c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.set_deposits_limit_too_high"
      "Set deposits limit to a too high value"
      "Cannot set deposits limit such that the active stake overflows."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t)
            ⇒
            let '(limit, max_limit) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot set deposits limit to "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " as it is higher the allowed maximum "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal "." % char
                          CamlinternalFormatBasics.End_of_format)))))
                "Cannot set deposits limit to %a as it is higher the allowed maximum %a.")
              Alpha_context.Tez.pp limit Alpha_context.Tez.pp max_limit))
      (Data_encoding.obj2
        (Data_encoding.req None None "limit" Alpha_context.Tez.encoding)
        (Data_encoding.req None None "max_limit" Alpha_context.Tez.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Set_deposits_limit_too_high" then
            let '{|
              Set_deposits_limit_too_high.limit := limit;
                Set_deposits_limit_too_high.max_limit := max_limit
                |} := cast Set_deposits_limit_too_high payload in
            Some (limit, max_limit)
          else None
        end)
      (fun (function_parameter : Alpha_context.Tez.t × Alpha_context.Tez.t) ⇒
        let '(limit, max_limit) := function_parameter in
        Build_extensible "Set_deposits_limit_too_high"
          Set_deposits_limit_too_high
          {| Set_deposits_limit_too_high.limit := limit;
            Set_deposits_limit_too_high.max_limit := max_limit; |}) in
  let error_while_taking_fees_description :=
    "There was an error while taking the fees, which should not happen and means that the operation's validation was faulty."
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.error_while_taking_fees"
      "Error while taking the fees of a manager operation"
      error_while_taking_fees_description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s")
              error_while_taking_fees_description)) Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Error_while_taking_fees" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Error_while_taking_fees" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.update_consensus_key_on_unregistered_delegate"
      "Update consensus key on an unregistered delegate"
      "Cannot update consensus key an unregistered delegate."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (c_value : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot update the consensus key on the unregistered delegate "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal "." % char
                      CamlinternalFormatBasics.End_of_format)))
                "Cannot update the consensus key on the unregistered delegate %a.")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) c_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Update_consensus_key_on_unregistered_delegate" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "Update_consensus_key_on_unregistered_delegate"
          Signature.public_key_hash c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "contract.empty_transaction" "Empty transaction"
      ("Forbidden to credit 0" ++
        String.String "234"
          (String.String "156"
            (String.String "169" " to a contract without code.")))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (contract : Alpha_context.Contract.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  ("Transactions of 0" ++
                    String.String "234"
                      (String.String "156"
                        (String.String "169"
                          " towards a contract without code are forbidden (")))
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ")."
                      CamlinternalFormatBasics.End_of_format)))
                ("Transactions of 0" ++
                  String.String "234"
                    (String.String "156"
                      (String.String "169"
                        " towards a contract without code are forbidden (%a)."))))
              Alpha_context.Contract.pp contract))
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Alpha_context.Contract.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Empty_transaction" then
            let c_value := cast Alpha_context.Contract.t payload in
            Some c_value
          else None
        end)
      (fun (c_value : Alpha_context.Contract.t) ⇒
        Build_extensible "Empty_transaction" Alpha_context.Contract.t c_value)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.tx_rollup_is_disabled" "Tx rollup is disabled"
      "Cannot originate a tx rollup as it is disabled."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal"
                  CamlinternalFormatBasics.End_of_format)
                "Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal")))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Tx_rollup_feature_disabled" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Tx_rollup_feature_disabled" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.tx_rollup_invalid_transaction_ticket_amount"
      "Amount of transferred ticket is too high"
      "The ticket amount of a rollup transaction must fit in a signed 64-bit integer."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Amount of transferred ticket is too high."
                  CamlinternalFormatBasics.End_of_format)
                "Amount of transferred ticket is too high.")))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Tx_rollup_invalid_transaction_ticket_amount" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Tx_rollup_invalid_transaction_ticket_amount" unit tt)
    in
  let description :=
    "Smart contract rollups will be enabled in a future proposal." in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.sc_rollup_disabled" "Smart contract rollups are disabled"
      description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") description))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Sc_rollup_feature_disabled" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Sc_rollup_feature_disabled" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "internal_operation_replay" "Internal operation replay"
      "An internal operation was emitted twice by a script"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Apply_internal_results.packed_internal_operation) ⇒
            let
              'Apply_internal_results.Internal_operation {|
                Apply_internal_results.internal_operation.nonce := nonce_value
                  |} := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Internal operation "
                  (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal
                      " was emitted twice by a script"
                      CamlinternalFormatBasics.End_of_format)))
                "Internal operation %d was emitted twice by a script")
              nonce_value)) Apply_internal_results.internal_operation_encoding
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Internal_operation_replay" then
            let op :=
              cast Apply_internal_results.packed_internal_operation payload in
            Some op
          else None
        end)
      (fun (op : Apply_internal_results.packed_internal_operation) ⇒
        Build_extensible "Internal_operation_replay"
          Apply_internal_results.packed_internal_operation op) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block.multiple_revelation"
      "Multiple revelations were included in a manager operation"
      "A manager operation should not contain more than one revelation"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Multiple revelations were included in a manager operation"
                  CamlinternalFormatBasics.End_of_format)
                "Multiple revelations were included in a manager operation")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Multiple_revelation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Multiple_revelation" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.zero_frozen_deposits" "Zero frozen deposits"
      "The delegate has zero frozen deposits."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (delegate : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Delegate "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " has zero frozen deposits; it is not allowed to bake/preendorse/endorse."
                      CamlinternalFormatBasics.End_of_format)))
                "Delegate %a has zero frozen deposits; it is not allowed to bake/preendorse/endorse.")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              delegate))
      (Data_encoding.obj1
        (Data_encoding.req None None "delegate"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Zero_frozen_deposits" then
            let delegate := cast Signature.public_key_hash payload in
            Some delegate
          else None
        end)
      (fun (delegate : Signature.public_key_hash) ⇒
        Build_extensible "Zero_frozen_deposits" Signature.public_key_hash
          delegate) in
  Error_monad.register_error_kind Error_monad.Permanent
    "operations.invalid_transfer_to_sc_rollup_from_implicit_account"
    "Invalid transfer to sc rollup"
    "Invalid transfer to sc rollup from implicit account"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid source for transfer operation to smart-contract rollup. Only originated accounts are allowed"
                CamlinternalFormatBasics.End_of_format)
              "Invalid source for transfer operation to smart-contract rollup. Only originated accounts are allowed")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Invalid_transfer_to_sc_rollup_from_implicit_account"
          then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Invalid_transfer_to_sc_rollup_from_implicit_account"
        unit tt).

Definition assert_tx_rollup_feature_enabled (ctxt : Alpha_context.context)
  : M? unit :=
  let level := (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)
    in
  let? sunset :=
    Alpha_context.Raw_level.of_int32
      (Alpha_context.Constants.tx_rollup_sunset_level ctxt) in
  let? '_ :=
    Error_monad.error_when (Alpha_context.Raw_level.op_lteq sunset level)
      (Build_extensible "Tx_rollup_feature_disabled" unit tt) in
  Error_monad.error_unless (Alpha_context.Constants.tx_rollup_enable ctxt)
    (Build_extensible "Tx_rollup_feature_disabled" unit tt).

Definition assert_sc_rollup_feature_enabled (ctxt : Alpha_context.context)
  : M? unit :=
  Error_monad.error_unless (Alpha_context.Constants.sc_rollup_enable ctxt)
    (Build_extensible "Sc_rollup_feature_disabled" unit tt).

Definition update_script_storage_and_ticket_balances
  (ctxt : Alpha_context.context) (self_contract : Contract_hash.t)
  (storage_value : Alpha_context.Script.expr)
  (lazy_storage_diff : option Alpha_context.Lazy_storage.diffs)
  (ticket_diffs : Ticket_token_map.t Z.t)
  (operations : list Script_typed_ir.packed_internal_operation)
  : M? (Z.t × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Contract.update_script_storage ctxt self_contract
      storage_value lazy_storage_diff in
  let self_contract := Contract_repr.Originated self_contract in
  Ticket_accounting.update_ticket_balances ctxt self_contract ticket_diffs
    operations.

Definition apply_delegation {A : Set}
  (ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
  (delegate : option Alpha_context.public_key_hash)
  (before_operation : Alpha_context.context)
  : M? (Alpha_context.context × Alpha_context.Gas.Arith.fp × list A) :=
  let? ctxt := Alpha_context.Contract.Delegate.set ctxt source delegate in
  return? (ctxt, (Alpha_context.Gas.consumed before_operation ctxt), nil).

Inductive execution_arg (loc : Set) : Set :=
| Typed_arg : ∀ {a : Set},
  loc → Script_typed_ir.ty → a → execution_arg loc
| Untyped_arg : Alpha_context.Script.expr → execution_arg loc.

Arguments Typed_arg {_ _}.
Arguments Untyped_arg {_}.

Definition apply_transaction_to_implicit {A : Set}
  (ctxt : Alpha_context.context) (source : Contract_repr.t)
  (amount : Alpha_context.Tez.t) (pkh : Alpha_context.public_key_hash)
  (before_operation : Alpha_context.context)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_transaction_result × list A) :=
  let contract := Contract_repr.Implicit pkh in
  let? '_ :=
    Error_monad.error_when
      (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
      (Build_extensible "Empty_transaction" Alpha_context.Contract.t contract)
    in
  let already_allocated := Alpha_context.Contract.allocated ctxt contract in
  let? '(ctxt, balance_updates) :=
    Alpha_context.Token.transfer None ctxt
      (Alpha_context.Token.Source_container
        (Alpha_context.Token.Contract source))
      (Alpha_context.Token.Sink_container
        (Alpha_context.Token.Contract contract)) amount in
  let result_value :=
    Apply_internal_results.Transaction_to_contract_result
      {|
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
          := None;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
          := None;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
          := balance_updates;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
          := nil;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
          := nil;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
          := Alpha_context.Gas.consumed before_operation ctxt;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
          := Z.zero;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
          := Z.zero;
        Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
          := Pervasives.not already_allocated; |} in
  return? (ctxt, result_value, nil).

Definition apply_transaction_to_smart_contract
  (ctxt : Alpha_context.context) (source : Contract_repr.t)
  (contract_hash : Contract_hash.t) (amount : Alpha_context.Tez.t)
  (entrypoint : Alpha_context.Entrypoint.t)
  (before_operation : Alpha_context.context) (payer : Signature.public_key_hash)
  (chain_id : Chain_id.t) (internal : bool)
  (parameter : execution_arg Alpha_context.Script.location)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_transaction_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let contract := Contract_repr.Originated contract_hash in
  let? '(ctxt, balance_updates) :=
    Alpha_context.Token.transfer None ctxt
      (Alpha_context.Token.Source_container
        (Alpha_context.Token.Contract source))
      (Alpha_context.Token.Sink_container
        (Alpha_context.Token.Contract contract)) amount in
  let? '(ctxt, cache_key, script) := Script_cache.find ctxt contract_hash in
  match script with
  | None ⇒
    Error_monad.tzfail
      (Build_extensible "Non_existing_contract" Alpha_context.Contract.t
        contract)
  | Some (script, script_ir) ⇒
    let? balance := Alpha_context.Contract.get_balance ctxt contract in
    let now := Script_timestamp.now ctxt in
    let level :=
      Script_int.abs
        (Script_int.of_int32
          (Alpha_context.Raw_level.to_int32
            (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)))
      in
    let step_constants :=
      {| Script_typed_ir.step_constants.source := source;
        Script_typed_ir.step_constants.payer := payer;
        Script_typed_ir.step_constants.self := contract_hash;
        Script_typed_ir.step_constants.amount := amount;
        Script_typed_ir.step_constants.balance := balance;
        Script_typed_ir.step_constants.chain_id := chain_id;
        Script_typed_ir.step_constants.now := now;
        Script_typed_ir.step_constants.level := level; |} in
    let execute :=
      match parameter with
      | Untyped_arg parameter ⇒
        let parameter := cast Alpha_context.Script.expr parameter in
        fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
          Script_interpreter.execute x_1 x_2 x_3 x_4 x_5 x_6 x_7 parameter
      | Typed_arg location parameter_ty parameter ⇒
        let 'existT _ __Typed_arg_'a [parameter, parameter_ty, location] :=
          cast_exists (Es := Set)
            (fun __Typed_arg_'a ⇒
              [__Typed_arg_'a ** Script_typed_ir.ty **
                Alpha_context.Script.location])
            [parameter, parameter_ty, location] in
        fun x_1 x_2 x_3 x_4 x_5 x_6 x_7 ⇒
          Script_interpreter.execute_with_typed_parameter x_1 x_2 x_3 x_4 x_5
            x_6 x_7 parameter_ty location parameter
      end in
    let cached_script := Some script_ir in
    let?
      '({|
        Script_interpreter.execution_result.script := updated_cached_script;
          Script_interpreter.execution_result.code_size := updated_size;
          Script_interpreter.execution_result.storage := storage_value;
          Script_interpreter.execution_result.lazy_storage_diff :=
            lazy_storage_diff;
          Script_interpreter.execution_result.operations := operations;
          Script_interpreter.execution_result.ticket_diffs := ticket_diffs;
          Script_interpreter.execution_result.ticket_receipt := ticket_receipt
          |}, ctxt) :=
      execute None ctxt cached_script Script_ir_unparser.Optimized
        step_constants script entrypoint internal in
    let? '(ticket_table_size_diff, ctxt) :=
      update_script_storage_and_ticket_balances ctxt contract_hash storage_value
        lazy_storage_diff ticket_diffs operations in
    let? '(ticket_paid_storage_diff, ctxt) :=
      Alpha_context.Ticket_balance.adjust_storage_space ctxt
        ticket_table_size_diff in
    let? '(ctxt, new_size, contract_paid_storage_size_diff) :=
      Alpha_context.Fees.record_paid_storage_space ctxt contract_hash in
    let? originated_contracts :=
      Alpha_context.Contract.originated_from_current_nonce before_operation ctxt
      in
    let? ctxt :=
      Script_cache.update ctxt cache_key
        ((Alpha_context.Script.t.with_storage
          (Alpha_context.Script.lazy_expr_value storage_value) script),
          updated_cached_script) updated_size in
    let result_value :=
      Apply_internal_results.Transaction_to_contract_result
        {|
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
            := Some storage_value;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
            := lazy_storage_diff;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
            := balance_updates;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
            := ticket_receipt;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
            := originated_contracts;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
            := Alpha_context.Gas.consumed before_operation ctxt;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
            := new_size;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
            := contract_paid_storage_size_diff +Z ticket_paid_storage_diff;
          Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
            := false; |} in
    return? (ctxt, result_value, operations)
  end.

Definition apply_transaction_to_tx_rollup {A B : Set}
  (ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
  (parameters :
    Script_typed_ir.pair (Script_typed_ir.ticket A)
      Script_typed_ir.tx_rollup_l2_address)
  (payer : Alpha_context.public_key_hash)
  (dst_rollup : Alpha_context.Tx_rollup.t) (since : Alpha_context.context)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_internal_operation_result × list B) :=
  let? '_ := assert_tx_rollup_feature_enabled ctxt in
  let '{|
    Tx_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
      Tx_rollup_parameters.deposit_parameters.l2_destination := l2_destination
      |} := Tx_rollup_parameters.get_deposit_parameters parameters_ty parameters
    in
  let? '(ticket_size, ctxt) := Ticket_scanner.ex_ticket_size ctxt ex_ticket in
  let limit := Alpha_context.Constants.tx_rollup_max_ticket_payload_size ctxt in
  let? '_ :=
    Error_monad.fail_when (Saturation_repr.op_gtexclamation ticket_size limit)
      (Build_extensible "Ticket_payload_size_limit_exceeded"
        Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded
        {|
          Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.payload_size
            := ticket_size;
          Tx_rollup_errors_repr.Ticket_payload_size_limit_exceeded.limit :=
            limit; |}) in
  let '(ex_token, ticket_amount) :=
    Ticket_scanner.ex_token_and_amount_of_ex_ticket ex_ticket in
  let? '(ticket_hash, ctxt) :=
    Ticket_balance_key.of_ex_token ctxt
      (Alpha_context.Destination.Tx_rollup dst_rollup) ex_token in
  let? ticket_amount :=
    Option.value_e
      (Option.bind (Script_int.to_int64 ticket_amount) Tx_rollup_l2_qty.of_int64)
      (Error_monad.trace_of_error
        (Build_extensible "Tx_rollup_invalid_transaction_ticket_amount" unit tt))
    in
  let? '_ :=
    Error_monad.error_when
      (Tx_rollup_l2_qty.op_lteq ticket_amount Tx_rollup_l2_qty.zero)
      (Build_extensible "Forbidden_zero_ticket_quantity" unit tt) in
  let '(deposit, message_size) :=
    Alpha_context.Tx_rollup_message.make_deposit payer l2_destination
      ticket_hash ticket_amount in
  let? '(ctxt, state_value) := Alpha_context.Tx_rollup_state.get ctxt dst_rollup
    in
  let? cost :=
    Alpha_context.Tx_rollup_state.burn_cost None state_value message_size in
  let? '(ctxt, balance_updates) :=
    Alpha_context.Token.transfer None ctxt
      (Alpha_context.Token.Source_container
        (Alpha_context.Token.Contract (Contract_repr.Implicit payer)))
      (Alpha_context.Token.Sink_infinite Alpha_context.Token.Burned) cost in
  let? '(ctxt, state_value, paid_storage_size_diff) :=
    Alpha_context.Tx_rollup_inbox.append_message ctxt dst_rollup state_value
      deposit in
  let? ctxt := Alpha_context.Tx_rollup_state.update ctxt dst_rollup state_value
    in
  let result_value :=
    Apply_internal_results.ITransaction_result
      (Apply_internal_results.Transaction_to_tx_rollup_result
        {|
          Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
            := ticket_hash;
          Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
            := balance_updates;
          Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
            := Alpha_context.Gas.consumed since ctxt;
          Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
            := paid_storage_size_diff; |}) in
  return? (ctxt, result_value, nil).

Definition apply_origination {A B : Set}
  (ctxt : Alpha_context.context) (storage_type : Script_typed_ir.ty)
  (storage_value : A)
  (unparsed_code : Micheline.canonical Alpha_context.Script.prim)
  (contract_hash : Contract_hash.t)
  (delegate : option Alpha_context.public_key_hash) (source : Contract_repr.t)
  (credit : Alpha_context.Tez.t) (before_operation : Alpha_context.context)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_origination_result × list B) :=
  let? '(to_duplicate, ctxt) :=
    Script_ir_translator.collect_lazy_storage ctxt storage_type storage_value in
  let to_update := Script_ir_translator.no_lazy_storage_id in
  let? '(storage_value, lazy_storage_diff, ctxt) :=
    Script_ir_translator.extract_lazy_storage_diff ctxt
      Script_ir_unparser.Optimized false to_duplicate to_update storage_type
      storage_value in
  let? '(storage_value, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      storage_type storage_value in
  let storage_value := Alpha_context.Script.lazy_expr_value storage_value in
  let? '(code, ctxt) :=
    Script_ir_translator.unparse_code ctxt Script_ir_unparser.Optimized
      (Micheline.root_value unparsed_code) in
  let code := Alpha_context.Script.lazy_expr_value code in
  let script :=
    {| Alpha_context.Script.t.code := code;
      Alpha_context.Script.t.storage := storage_value; |} in
  let? ctxt :=
    Alpha_context.Contract.raw_originate ctxt false contract_hash
      (script, lazy_storage_diff) in
  let contract := Contract_repr.Originated contract_hash in
  let? ctxt :=
    match delegate with
    | None ⇒ return? ctxt
    | Some delegate ⇒
      Alpha_context.Contract.Delegate.init_value ctxt contract delegate
    end in
  let? '(ctxt, balance_updates) :=
    Alpha_context.Token.transfer None ctxt
      (Alpha_context.Token.Source_container
        (Alpha_context.Token.Contract source))
      (Alpha_context.Token.Sink_container
        (Alpha_context.Token.Contract contract)) credit in
  let? '(ctxt, size_value, paid_storage_size_diff) :=
    Alpha_context.Fees.record_paid_storage_space ctxt contract_hash in
  let result_value :=
    {|
      Apply_internal_results.successful_origination_result.lazy_storage_diff :=
        lazy_storage_diff;
      Apply_internal_results.successful_origination_result.balance_updates :=
        balance_updates;
      Apply_internal_results.successful_origination_result.originated_contracts
        := [ contract_hash ];
      Apply_internal_results.successful_origination_result.consumed_gas :=
        Alpha_context.Gas.consumed before_operation ctxt;
      Apply_internal_results.successful_origination_result.storage_size :=
        size_value;
      Apply_internal_results.successful_origination_result.paid_storage_size_diff
        := paid_storage_size_diff; |} in
  return? (ctxt, result_value, nil).

Definition apply_internal_operation_contents
  (ctxt_before_op : Alpha_context.context)
  (payer : Alpha_context.public_key_hash) (source : Alpha_context.Contract.t)
  (chain_id : Chain_id.t)
  (operation : Script_typed_ir.internal_operation_contents)
  : M?
    (Alpha_context.context ×
      Apply_internal_results.successful_internal_operation_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let? '_ := Alpha_context.Contract.must_exist ctxt_before_op source in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt_before_op
      Michelson_v1_gas.Cost_of.manager_operation in
  match operation with
  |
    Script_typed_ir.Transaction_to_implicit {|
      Script_typed_ir.internal_operation_contents.Transaction_to_implicit.destination
        := pkh;
        Script_typed_ir.internal_operation_contents.Transaction_to_implicit.amount
          := amount
        |} ⇒
    let? '(ctxt, res, ops) :=
      apply_transaction_to_implicit ctxt source amount pkh ctxt_before_op in
    return? (ctxt, (Apply_internal_results.ITransaction_result res), ops)
  |
    Script_typed_ir.Transaction_to_smart_contract {|
      Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
        := contract_hash;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
          := amount;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
          := entrypoint;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
          := location;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
          := parameters_ty;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
          := typed_parameters;
        Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
          := _
        |} ⇒
    let? '(ctxt, res, ops) :=
      apply_transaction_to_smart_contract ctxt source contract_hash amount
        entrypoint ctxt_before_op payer chain_id true
        (Typed_arg location parameters_ty typed_parameters) in
    return? (ctxt, (Apply_internal_results.ITransaction_result res), ops)
  |
    Script_typed_ir.Transaction_to_tx_rollup {|
      Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.destination
        := destination;
        Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.parameters_ty
          := parameters_ty;
        Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.parameters
          := parameters;
        Script_typed_ir.internal_operation_contents.Transaction_to_tx_rollup.unparsed_parameters
          := _
        |} ⇒
    apply_transaction_to_tx_rollup ctxt parameters_ty parameters payer
      destination ctxt_before_op
  |
    Script_typed_ir.Transaction_to_sc_rollup {|
      Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.destination
        := destination;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.entrypoint
          := _;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.parameters_ty
          := _;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.parameters
          := _;
        Script_typed_ir.internal_operation_contents.Transaction_to_sc_rollup.unparsed_parameters
          := payload
        |} ⇒
    let? '_ := assert_sc_rollup_feature_enabled ctxt in
    let? sender :=
      match source with
      | Contract_repr.Implicit _ ⇒
        Error_monad.error_value
          (Build_extensible
            "Invalid_transfer_to_sc_rollup_from_implicit_account" unit tt)
      | Contract_repr.Originated hash_value ⇒ return? hash_value
      end in
    let? '(inbox_after, _size, ctxt) :=
      Alpha_context.Sc_rollup.Inbox.add_deposit ctxt payload sender payer
        destination in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_internal_results.Transaction_to_sc_rollup_result
        {|
          Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
            := consumed_gas;
          Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
            := inbox_after; |} in
    return?
      (ctxt, (Apply_internal_results.ITransaction_result result_value), nil)
  |
    Script_typed_ir.Event {|
      Script_typed_ir.internal_operation_contents.Event.ty := _;
        Script_typed_ir.internal_operation_contents.Event.tag := _;
        Script_typed_ir.internal_operation_contents.Event.unparsed_data := _
        |} ⇒
    return?
      (ctxt,
        (Apply_internal_results.IEvent_result
          {|
            Apply_internal_results.successful_internal_operation_result.IEvent_result.consumed_gas
              := Alpha_context.Gas.consumed ctxt_before_op ctxt; |}), nil)
  |
    Script_typed_ir.Transaction_to_zk_rollup {|
      Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.destination
        := destination;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.parameters_ty
          := parameters_ty;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.parameters
          := parameters;
        Script_typed_ir.internal_operation_contents.Transaction_to_zk_rollup.unparsed_parameters
          := _
        |} ⇒
    Zk_rollup_apply.transaction_to_zk_rollup ctxt parameters_ty parameters
      destination ctxt_before_op
  |
    Script_typed_ir.Origination {|
      Script_typed_ir.internal_operation_contents.Origination.delegate := delegate;
        Script_typed_ir.internal_operation_contents.Origination.code :=
          unparsed_code;
        Script_typed_ir.internal_operation_contents.Origination.unparsed_storage
          := _;
        Script_typed_ir.internal_operation_contents.Origination.credit := credit;
        Script_typed_ir.internal_operation_contents.Origination.preorigination
          := preorigination;
        Script_typed_ir.internal_operation_contents.Origination.storage_type :=
          storage_type;
        Script_typed_ir.internal_operation_contents.Origination.storage :=
          storage_value
        |} ⇒
    let? '(ctxt, origination_result, ops) :=
      apply_origination ctxt storage_type storage_value unparsed_code
        preorigination delegate source credit ctxt_before_op in
    return?
      (ctxt, (Apply_internal_results.IOrigination_result origination_result),
        ops)
  | Script_typed_ir.Delegation delegate ⇒
    let? '(ctxt, consumed_gas, ops) :=
      apply_delegation ctxt source delegate ctxt_before_op in
    return?
      (ctxt,
        (Apply_internal_results.IDelegation_result
          {|
            Apply_internal_results.successful_internal_operation_result.IDelegation_result.consumed_gas
              := consumed_gas; |}), ops)
  end.

Definition apply_manager_operation
  (ctxt_before_op : Alpha_context.context)
  (source : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
  (operation : Alpha_context.manager_operation)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let source_contract := Contract_repr.Implicit source in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt_before_op
      Michelson_v1_gas.Cost_of.manager_operation in
  let consume_deserialization_gas := Alpha_context.Script.Always in
  match operation with
  | Alpha_context.Reveal pk ⇒
    let? '_ := Alpha_context.Contract.must_be_allocated ctxt source_contract in
    let? ctxt :=
      Alpha_context.Contract.reveal_manager_key (Some false) ctxt source pk in
    return?
      (ctxt,
        (Apply_results.Reveal_result
          {|
            Apply_results.successful_manager_operation_result.Reveal_result.consumed_gas
              := Alpha_context.Gas.consumed ctxt_before_op ctxt; |}), nil)
  |
    Alpha_context.Transaction {|
      Alpha_context.manager_operation.Transaction.amount := amount;
        Alpha_context.manager_operation.Transaction.parameters := parameters;
        Alpha_context.manager_operation.Transaction.entrypoint := entrypoint;
        Alpha_context.manager_operation.Transaction.destination :=
          Contract_repr.Implicit pkh
        |} ⇒
    let? '(parameters, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt parameters in
    let? '_ :=
      match Micheline.root_value parameters with
      | Micheline.Prim _ Michelson_v1_primitives.D_Unit [] _ ⇒
        Result.return_unit
      | _ ⇒
        Error_monad.error_value
          (Build_extensible "Bad_contract_parameter" Alpha_context.Contract.t
            source_contract)
      end in
    let? '_ :=
      if Alpha_context.Entrypoint.is_default entrypoint then
        Result.return_unit
      else
        Error_monad.error_value
          (Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
            entrypoint) in
    let? '(ctxt, res, ops) :=
      apply_transaction_to_implicit ctxt source_contract amount pkh
        ctxt_before_op in
    return? (ctxt, (Apply_results.Transaction_result res), ops)
  |
    Alpha_context.Transaction {|
      Alpha_context.manager_operation.Transaction.amount := amount;
        Alpha_context.manager_operation.Transaction.parameters := parameters;
        Alpha_context.manager_operation.Transaction.entrypoint := entrypoint;
        Alpha_context.manager_operation.Transaction.destination :=
          Contract_repr.Originated contract_hash
        |} ⇒
    let? '(parameters, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt parameters in
    let? '(ctxt, res, ops) :=
      apply_transaction_to_smart_contract ctxt source_contract contract_hash
        amount entrypoint ctxt_before_op source chain_id false
        (Untyped_arg parameters) in
    return? (ctxt, (Apply_results.Transaction_result res), ops)
  |
    Alpha_context.Tx_rollup_dispatch_tickets {|
      Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.tx_rollup :=
        tx_rollup;
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.level :=
          level;
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.context_hash
          := context_hash;
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.message_index
          := message_index;
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.message_result_path
          := message_result_path;
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.tickets_info
          := tickets_info
        |} ⇒
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '(ctxt, commitment) :=
      Alpha_context.Tx_rollup_commitment.get_finalized ctxt tx_rollup
        state_value level in
    let? '(ctxt, already_revealed) :=
      Alpha_context.Tx_rollup_reveal.mem ctxt tx_rollup level message_index in
    let? '_ :=
      Error_monad.error_when already_revealed
        (Build_extensible "Withdrawals_already_dispatched" unit tt) in
    let? '(rev_withdraw_list, rev_ex_token_and_hash_list, ctxt) :=
      List.fold_left_es
        (fun (function_parameter :
          list Alpha_context.Tx_rollup_withdraw.order ×
            list
              (Alpha_context.Tx_rollup_withdraw.order × Ticket_token.ex_token) ×
            Alpha_context.context) ⇒
          let '(acc_withdraw, acc_value, ctxt) := function_parameter in
          fun (function_parameter : Alpha_context.Tx_rollup_reveal.t) ⇒
            let '{|
              Alpha_context.Tx_rollup_reveal.t.contents := contents;
                Alpha_context.Tx_rollup_reveal.t.ty := ty_value;
                Alpha_context.Tx_rollup_reveal.t.ticketer := ticketer;
                Alpha_context.Tx_rollup_reveal.t.amount := amount;
                Alpha_context.Tx_rollup_reveal.t.claimer := claimer
                |} := function_parameter in
            let? '_ :=
              Error_monad.error_when
                (Tx_rollup_l2_qty.op_lteq amount Tx_rollup_l2_qty.zero)
                (Build_extensible "Forbidden_zero_ticket_quantity" unit tt) in
            let? '(ctxt, ticket_token) :=
              Ticket_transfer.parse_ticket consume_deserialization_gas ticketer
                contents ty_value ctxt in
            let? '(ticket_hash, ctxt) :=
              Ticket_balance_key.of_ex_token ctxt
                (Alpha_context.Destination.Tx_rollup tx_rollup) ticket_token in
            let withdrawal :=
              {| Alpha_context.Tx_rollup_withdraw.order.claimer := claimer;
                Alpha_context.Tx_rollup_withdraw.order.ticket_hash :=
                  ticket_hash;
                Alpha_context.Tx_rollup_withdraw.order.amount := amount; |} in
            return?
              ((cons withdrawal acc_withdraw),
                (cons (withdrawal, ticket_token) acc_value), ctxt))
        (nil, nil, ctxt) tickets_info in
    let? '(ctxt, withdraw_list_hash) :=
      Alpha_context.Tx_rollup_hash.withdraw_list ctxt
        (List.rev rev_withdraw_list) in
    let? ctxt :=
      Alpha_context.Tx_rollup_commitment.check_message_result ctxt
        commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.commitment)
        (Alpha_context.Tx_rollup_commitment.Result
          {| Tx_rollup_message_result_repr.t.context_hash := context_hash;
            Tx_rollup_message_result_repr.t.withdraw_list_hash :=
              withdraw_list_hash; |}) message_result_path message_index in
    let? ctxt :=
      Alpha_context.Tx_rollup_reveal.record ctxt tx_rollup level message_index
      in
    let adjust_ticket_balance (function_parameter : Alpha_context.context × Z.t)
      : Alpha_context.Tx_rollup_withdraw.order × Ticket_token.ex_token →
      M? (Alpha_context.context × Z.t) :=
      let '(ctxt, acc_diff) := function_parameter in
      fun (function_parameter :
        Alpha_context.Tx_rollup_withdraw.order × Ticket_token.ex_token) ⇒
        let
          '({|
            Alpha_context.Tx_rollup_withdraw.order.claimer := claimer;
              Alpha_context.Tx_rollup_withdraw.order.ticket_hash :=
                tx_rollup_ticket_hash;
              Alpha_context.Tx_rollup_withdraw.order.amount := amount
              |}, ticket_token) := function_parameter in
        let? amount :=
          (fun x_1 ⇒
            Option.value_e x_1
              (Error_monad.trace_of_error
                (Build_extensible "Forbidden_zero_ticket_quantity" unit tt)))
            (Ticket_amount.of_zint (Tx_rollup_l2_qty.to_z amount)) in
        let? '(claimer_ticket_hash, ctxt) :=
          Ticket_balance_key.of_ex_token ctxt
            (Alpha_context.Destination.Contract (Contract_repr.Implicit claimer))
            ticket_token in
        let? '(ctxt, diff_value) :=
          Ticket_transfer.transfer_ticket_with_hashes ctxt tx_rollup_ticket_hash
            claimer_ticket_hash amount in
        return? (ctxt, (acc_diff +Z diff_value)) in
    let? '(ctxt, paid_storage_size_diff) :=
      List.fold_left_es adjust_ticket_balance (ctxt, Z.zero)
        rev_ex_token_and_hash_list in
    let result_value :=
      Apply_results.Tx_rollup_dispatch_tickets_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
            := paid_storage_size_diff; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Transfer_ticket {|
      Alpha_context.manager_operation.Transfer_ticket.contents := contents;
        Alpha_context.manager_operation.Transfer_ticket.ty := ty_value;
        Alpha_context.manager_operation.Transfer_ticket.ticketer := ticketer;
        Alpha_context.manager_operation.Transfer_ticket.amount := amount;
        Alpha_context.manager_operation.Transfer_ticket.destination :=
          destination;
        Alpha_context.manager_operation.Transfer_ticket.entrypoint := entrypoint
        |} ⇒
    match destination with
    | Contract_repr.Implicit _ ⇒
      let? '_ :=
        Error_monad.error_unless
          (Alpha_context.Entrypoint.op_eq entrypoint
            Alpha_context.Entrypoint.default)
          (Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
            entrypoint) in
      let? '(ctxt, ticket) :=
        Ticket_transfer.parse_ticket consume_deserialization_gas ticketer
          contents ty_value ctxt in
      let? '(ctxt, paid_storage_size_diff) :=
        Ticket_transfer.transfer_ticket ctxt
          (Alpha_context.Destination.Contract source_contract)
          (Alpha_context.Destination.Contract destination) ticket amount in
      return?
        (ctxt,
          (Apply_results.Transfer_ticket_result
            {|
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.balance_updates
                := nil;
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.consumed_gas
                := Alpha_context.Gas.consumed ctxt_before_op ctxt;
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
                := paid_storage_size_diff; |}), nil)
    | Contract_repr.Originated destination_hash ⇒
      let? '(ctxt, token, op) :=
        Ticket_transfer.parse_ticket_and_operation consume_deserialization_gas
          ticketer contents ty_value source_contract destination_hash entrypoint
          amount ctxt in
      let? '(ctxt, paid_storage_size_diff) :=
        Ticket_transfer.transfer_ticket ctxt
          (Alpha_context.Destination.Contract source_contract)
          (Alpha_context.Destination.Contract destination) token amount in
      return?
        (ctxt,
          (Apply_results.Transfer_ticket_result
            {|
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.balance_updates
                := nil;
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.consumed_gas
                := Alpha_context.Gas.consumed ctxt_before_op ctxt;
              Apply_results.successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
                := paid_storage_size_diff; |}), [ op ])
    end
  |
    Alpha_context.Origination {|
      Alpha_context.manager_operation.Origination.delegate := delegate;
        Alpha_context.manager_operation.Origination.script := script;
        Alpha_context.manager_operation.Origination.credit := credit
        |} ⇒
    let? '(ctxt, contract) :=
      Alpha_context.Contract.fresh_contract_from_current_nonce ctxt in
    let? '(_unparsed_storage, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt script.(Alpha_context.Script.t.storage) in
    let? '(unparsed_code, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt script.(Alpha_context.Script.t.code) in
    let? '(Script_ir_translator.Ex_script parsed_script, ctxt) :=
      Script_ir_translator.parse_script
        (Script_ir_translator_config.make None None false tt) ctxt false script
      in
    let
      'Script_typed_ir.Script {|
        Script_typed_ir.script.Script.storage := storage_value;
          Script_typed_ir.script.Script.storage_type := storage_type;
          Script_typed_ir.script.Script.views := views
          |} := parsed_script in
    let views_result :=
      Script_ir_translator.parse_views
        (Script_ir_translator_config.make None None false tt) ctxt storage_type
        views in
    let? '(_typed_views, ctxt) :=
      Error_monad.trace_value
        (Build_extensible "Ill_typed_contract"
          (Alpha_context.Script.expr × Script_tc_errors.type_map)
          (unparsed_code, nil)) views_result in
    let? '(ctxt, origination_result, ops) :=
      apply_origination ctxt storage_type storage_value unparsed_code contract
        delegate source_contract credit ctxt_before_op in
    return? (ctxt, (Apply_results.Origination_result origination_result), ops)
  | Alpha_context.Delegation delegate ⇒
    let? '(ctxt, consumed_gas, ops) :=
      apply_delegation ctxt source_contract delegate ctxt_before_op in
    return?
      (ctxt,
        (Apply_results.Delegation_result
          {|
            Apply_results.successful_manager_operation_result.Delegation_result.consumed_gas
              := consumed_gas; |}), ops)
  |
    Alpha_context.Register_global_constant {|
      Alpha_context.manager_operation.Register_global_constant.value := value_value
        |} ⇒
    let? '(expr, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt value_value in
    let? '(ctxt, address, size_value) :=
      Alpha_context.Global_constants_storage.register ctxt expr in
    let '(ctxt, paid_size) :=
      Alpha_context.Fees.record_global_constant_storage_space ctxt size_value in
    let result_value :=
      Apply_results.Register_global_constant_result
        {|
          Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant
            := paid_size;
          Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address
            := address; |} in
    return? (ctxt, result_value, nil)
  | Alpha_context.Set_deposits_limit limit ⇒
    let? '_ :=
      match limit with
      | None ⇒ Result.return_unit
      | Some limit ⇒
        let frozen_deposits_percentage :=
          Alpha_context.Constants.frozen_deposits_percentage ctxt in
        let max_limit :=
          Alpha_context.Tez.of_mutez_exn
            ((Int64.of_int frozen_deposits_percentage) ×i64
            (Int64.max_int /i64 100)) in
        Error_monad.error_when (Alpha_context.Tez.op_gt limit max_limit)
          (Build_extensible "Set_deposits_limit_too_high"
            Set_deposits_limit_too_high
            {| Set_deposits_limit_too_high.limit := limit;
              Set_deposits_limit_too_high.max_limit := max_limit; |})
      end in
    let is_registered := Alpha_context.Delegate.registered ctxt source in
    let? '_ :=
      Error_monad.error_unless is_registered
        (Build_extensible "Set_deposits_limit_on_unregistered_delegate"
          Alpha_context.public_key_hash source) in
    let ctxt :=
      Alpha_context.Delegate.set_frozen_deposits_limit ctxt source limit in
    return?
      (ctxt,
        (Apply_results.Set_deposits_limit_result
          {|
            Apply_results.successful_manager_operation_result.Set_deposits_limit_result.consumed_gas
              := Alpha_context.Gas.consumed ctxt_before_op ctxt; |}), nil)
  |
    Alpha_context.Increase_paid_storage {|
      Alpha_context.manager_operation.Increase_paid_storage.amount_in_bytes :=
        amount_in_bytes;
        Alpha_context.manager_operation.Increase_paid_storage.destination :=
          destination
        |} ⇒
    let? ctxt :=
      Alpha_context.Contract.increase_paid_storage ctxt destination
        amount_in_bytes in
    let payer :=
      Alpha_context.Token.Source_container
        (Alpha_context.Token.Contract (Contract_repr.Implicit source)) in
    let? '(ctxt, storage_bus) :=
      Alpha_context.Fees.burn_storage_increase_fees None ctxt payer
        amount_in_bytes in
    let result_value :=
      Apply_results.Increase_paid_storage_result
        {|
          Apply_results.successful_manager_operation_result.Increase_paid_storage_result.balance_updates
            := storage_bus;
          Apply_results.successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt; |} in
    return? (ctxt, result_value, nil)
  | Alpha_context.Update_consensus_key pk ⇒
    let is_registered := Alpha_context.Delegate.registered ctxt source in
    let? '_ :=
      Error_monad.error_unless is_registered
        (Build_extensible "Update_consensus_key_on_unregistered_delegate"
          Alpha_context.public_key_hash source) in
    let? ctxt :=
      Alpha_context.Delegate.Consensus_key.register_update ctxt source pk in
    return?
      (ctxt,
        (Apply_results.Update_consensus_key_result
          {|
            Apply_results.successful_manager_operation_result.Update_consensus_key_result.consumed_gas
              := Alpha_context.Gas.consumed ctxt_before_op ctxt; |}), nil)
  | Alpha_context.Tx_rollup_origination ⇒
    let? '(ctxt, originated_tx_rollup) := Alpha_context.Tx_rollup.originate ctxt
      in
    let result_value :=
      Apply_results.Tx_rollup_origination_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
            := originated_tx_rollup; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_submit_batch {|
      Alpha_context.manager_operation.Tx_rollup_submit_batch.tx_rollup := tx_rollup;
        Alpha_context.manager_operation.Tx_rollup_submit_batch.content :=
          content;
        Alpha_context.manager_operation.Tx_rollup_submit_batch.burn_limit :=
          burn_limit
        |} ⇒
    let '(message, message_size) :=
      Alpha_context.Tx_rollup_message.make_batch content in
    let? cost := Tx_rollup_gas.hash_cost message_size in
    let? ctxt := Alpha_context.Gas.consume ctxt cost in
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '(ctxt, state_value, paid_storage_size_diff) :=
      Alpha_context.Tx_rollup_inbox.append_message ctxt tx_rollup state_value
        message in
    let? cost :=
      Alpha_context.Tx_rollup_state.burn_cost burn_limit state_value
        message_size in
    let? '(ctxt, balance_updates) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_container
          (Alpha_context.Token.Contract source_contract))
        (Alpha_context.Token.Sink_infinite Alpha_context.Token.Burned) cost in
    let? ctxt := Alpha_context.Tx_rollup_state.update ctxt tx_rollup state_value
      in
    let result_value :=
      Apply_results.Tx_rollup_submit_batch_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
            := balance_updates;
          Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
            := paid_storage_size_diff; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_commit {|
      Alpha_context.manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
        Alpha_context.manager_operation.Tx_rollup_commit.commitment :=
          commitment
        |} ⇒
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '(ctxt, balance_updates) :=
      let? '(ctxt, pending) :=
        Alpha_context.Tx_rollup_commitment.has_bond ctxt tx_rollup source in
      if Pervasives.not pending then
        let bond_id := Bond_id_repr.Tx_rollup_bond_id tx_rollup in
        Alpha_context.Token.transfer None ctxt
          (Alpha_context.Token.Source_container
            (Alpha_context.Token.Contract source_contract))
          (Alpha_context.Token.Sink_container
            (Alpha_context.Token.Frozen_bonds source_contract bond_id))
          (Alpha_context.Constants.tx_rollup_commitment_bond ctxt)
      else
        return? (ctxt, nil) in
    let? '(ctxt, state_value, to_slash) :=
      Alpha_context.Tx_rollup_commitment.add_commitment ctxt tx_rollup
        state_value source commitment in
    let? '(ctxt, burn_update) :=
      match to_slash with
      | Some pkh ⇒
        let committer := Contract_repr.Implicit pkh in
        let? '(ctxt, slashed) :=
          Alpha_context.Tx_rollup_commitment.slash_bond ctxt tx_rollup pkh in
        if slashed then
          let bid := Bond_id_repr.Tx_rollup_bond_id tx_rollup in
          let? '(ctxt, burn) :=
            Alpha_context.Token.balance ctxt
              (Alpha_context.Token.Frozen_bonds committer bid) in
          Alpha_context.Token.transfer None ctxt
            (Alpha_context.Token.Source_container
              (Alpha_context.Token.Frozen_bonds committer bid))
            (Alpha_context.Token.Sink_infinite
              Alpha_context.Token.Tx_rollup_rejection_punishments) burn
        else
          return? (ctxt, nil)
      | None ⇒ return? (ctxt, nil)
      end in
    let? ctxt := Alpha_context.Tx_rollup_state.update ctxt tx_rollup state_value
      in
    let result_value :=
      Apply_results.Tx_rollup_commit_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_commit_result.balance_updates
            := Pervasives.op_at burn_update balance_updates;
          Apply_results.successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_return_bond {|
      Alpha_context.manager_operation.Tx_rollup_return_bond.tx_rollup := tx_rollup
        |} ⇒
    let? ctxt :=
      Alpha_context.Tx_rollup_commitment.remove_bond ctxt tx_rollup source in
    let bond_id := Bond_id_repr.Tx_rollup_bond_id tx_rollup in
    let? '(ctxt, bond) :=
      Alpha_context.Token.balance ctxt
        (Alpha_context.Token.Frozen_bonds source_contract bond_id) in
    let? '(ctxt, balance_updates) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_container
          (Alpha_context.Token.Frozen_bonds source_contract bond_id))
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract source_contract)) bond in
    let result_value :=
      Apply_results.Tx_rollup_return_bond_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
            := balance_updates;
          Apply_results.successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_finalize_commitment {|
      Alpha_context.manager_operation.Tx_rollup_finalize_commitment.tx_rollup :=
        tx_rollup
        |} ⇒
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '(ctxt, state_value, level) :=
      Alpha_context.Tx_rollup_commitment.finalize_commitment ctxt tx_rollup
        state_value in
    let? ctxt := Alpha_context.Tx_rollup_state.update ctxt tx_rollup state_value
      in
    let result_value :=
      Apply_results.Tx_rollup_finalize_commitment_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
            := level; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_remove_commitment {|
      Alpha_context.manager_operation.Tx_rollup_remove_commitment.tx_rollup :=
        tx_rollup
        |} ⇒
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '(ctxt, state_value, level) :=
      Alpha_context.Tx_rollup_commitment.remove_commitment ctxt tx_rollup
        state_value in
    let? ctxt := Alpha_context.Tx_rollup_state.update ctxt tx_rollup state_value
      in
    let result_value :=
      Apply_results.Tx_rollup_remove_commitment_result
        {|
          Apply_results.successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt;
          Apply_results.successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
            := level; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Tx_rollup_rejection {|
      Alpha_context.manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
        Alpha_context.manager_operation.Tx_rollup_rejection.level := level;
        Alpha_context.manager_operation.Tx_rollup_rejection.message := message;
        Alpha_context.manager_operation.Tx_rollup_rejection.message_position :=
          message_position;
        Alpha_context.manager_operation.Tx_rollup_rejection.message_path :=
          message_path;
        Alpha_context.manager_operation.Tx_rollup_rejection.message_result_hash
          := message_result_hash;
        Alpha_context.manager_operation.Tx_rollup_rejection.message_result_path
          := message_result_path;
        Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result
          := previous_message_result;
        Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result_path
          := previous_message_result_path;
        Alpha_context.manager_operation.Tx_rollup_rejection.proof := proof_value
        |} ⇒
    let? '(ctxt, state_value) :=
      Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
    let? '_ :=
      Alpha_context.Tx_rollup_state.check_level_can_be_rejected state_value
        level in
    let? '(ctxt, commitment) :=
      Alpha_context.Tx_rollup_commitment.get ctxt tx_rollup state_value level in
    let? '_ :=
      Error_monad.error_when
        ((message_position <i 0) ||
        (commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.commitment).(Alpha_context.Tx_rollup_commitment.template.messages).(Alpha_context.Tx_rollup_commitment.Compact.excerpt.count)
        ≤i message_position))
        (Build_extensible "Wrong_message_position"
          Alpha_context.Tx_rollup_errors.Wrong_message_position
          {|
            Alpha_context.Tx_rollup_errors.Wrong_message_position.level :=
              commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.commitment).(Alpha_context.Tx_rollup_commitment.template.level);
            Alpha_context.Tx_rollup_errors.Wrong_message_position.position :=
              message_position;
            Alpha_context.Tx_rollup_errors.Wrong_message_position.length :=
              commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.commitment).(Alpha_context.Tx_rollup_commitment.template.messages).(Alpha_context.Tx_rollup_commitment.Compact.excerpt.count);
            |}) in
    let? ctxt :=
      Alpha_context.Tx_rollup_inbox.check_message_hash ctxt level tx_rollup
        message_position message message_path in
    let? ctxt :=
      Alpha_context.Tx_rollup_commitment.check_agreed_and_disputed_results ctxt
        tx_rollup state_value commitment previous_message_result
        previous_message_result_path message_result_hash message_position
        message_result_path in
    let parameters :=
      {|
        Tx_rollup_l2_apply.parameters.tx_rollup_max_withdrawals_per_batch :=
          Alpha_context.Constants.tx_rollup_max_withdrawals_per_batch ctxt; |}
      in
    let proof_length := Tx_rollup_l2_proof.length proof_value in
    match Tx_rollup_l2_proof.proof_of_serialized_opt proof_value with
    | Some proof_value ⇒
      let? ctxt :=
        Tx_rollup_l2_verifier.verify_proof ctxt parameters message proof_value
          proof_length previous_message_result message_result_hash
          (Alpha_context.Constants.tx_rollup_rejection_max_proof_size ctxt) in
      let? '(ctxt, state_value) :=
        Alpha_context.Tx_rollup_commitment.reject_commitment ctxt tx_rollup
          state_value level in
      let? '(ctxt, slashed) :=
        Alpha_context.Tx_rollup_commitment.slash_bond ctxt tx_rollup
          commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.committer)
        in
      let? '(ctxt, balance_updates) :=
        if slashed then
          let committer :=
            Contract_repr.Implicit
              commitment.(Alpha_context.Tx_rollup_commitment.Submitted_commitment.t.committer)
            in
          let bid := Bond_id_repr.Tx_rollup_bond_id tx_rollup in
          let? '(ctxt, burn) :=
            Alpha_context.Token.balance ctxt
              (Alpha_context.Token.Frozen_bonds committer bid) in
          let? reward := Alpha_context.Tez.op_divquestion burn 2 in
          let? '(ctxt, burn_update) :=
            Alpha_context.Token.transfer None ctxt
              (Alpha_context.Token.Source_container
                (Alpha_context.Token.Frozen_bonds committer bid))
              (Alpha_context.Token.Sink_infinite
                Alpha_context.Token.Tx_rollup_rejection_punishments) burn in
          let? '(ctxt, reward_update) :=
            Alpha_context.Token.transfer None ctxt
              (Alpha_context.Token.Source_infinite
                Alpha_context.Token.Tx_rollup_rejection_rewards)
              (Alpha_context.Token.Sink_container
                (Alpha_context.Token.Contract source_contract)) reward in
          return? (ctxt, (Pervasives.op_at burn_update reward_update))
        else
          return? (ctxt, nil) in
      let? ctxt :=
        Alpha_context.Tx_rollup_state.update ctxt tx_rollup state_value in
      let result_value :=
        Apply_results.Tx_rollup_rejection_result
          {|
            Apply_results.successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
              := balance_updates;
            Apply_results.successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
              := Alpha_context.Gas.consumed ctxt_before_op ctxt; |} in
      return? (ctxt, result_value, nil)
    | None ⇒ Error_monad.tzfail (Build_extensible "Proof_undecodable" unit tt)
    end
  |
    Alpha_context.Dal_publish_slot_header {|
      Alpha_context.manager_operation.Dal_publish_slot_header.slot_header :=
        slot_header
        |} ⇒
    let? ctxt := Dal_apply.apply_publish_slot_header ctxt slot_header in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Dal_publish_slot_header_result
        {|
          Apply_results.successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
            := consumed_gas; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_originate {|
      Alpha_context.manager_operation.Sc_rollup_originate.kind := kind_value;
        Alpha_context.manager_operation.Sc_rollup_originate.boot_sector :=
          boot_sector;
        Alpha_context.manager_operation.Sc_rollup_originate.origination_proof :=
          origination_proof;
        Alpha_context.manager_operation.Sc_rollup_originate.parameters_ty :=
          parameters_ty
        |} ⇒
    let?
      '({|
        Sc_rollup_operations.origination_result.address := address;
          Sc_rollup_operations.origination_result.size := size_value;
          Sc_rollup_operations.origination_result.genesis_commitment_hash :=
            genesis_commitment_hash
          |}, ctxt) :=
      Sc_rollup_operations.originate ctxt kind_value boot_sector
        origination_proof parameters_ty in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_originate_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.address
            := address;
          Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
            := genesis_commitment_hash;
          Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.size
            := size_value; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_add_messages {|
      Alpha_context.manager_operation.Sc_rollup_add_messages.messages := messages
        |} ⇒
    let? '(inbox_after, _size, ctxt) :=
      Alpha_context.Sc_rollup.Inbox.add_external_messages ctxt messages in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_add_messages_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
            := inbox_after; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_cement {|
      Alpha_context.manager_operation.Sc_rollup_cement.rollup := rollup;
        Alpha_context.manager_operation.Sc_rollup_cement.commitment :=
          commitment
        |} ⇒
    let? '(ctxt, commitment) :=
      Alpha_context.Sc_rollup.Stake_storage.cement_commitment ctxt rollup
        commitment in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_cement_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
            := commitment.(Alpha_context.Sc_rollup.Commitment.t.inbox_level); |}
      in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_publish {|
      Alpha_context.manager_operation.Sc_rollup_publish.rollup := rollup;
        Alpha_context.manager_operation.Sc_rollup_publish.commitment :=
          commitment
        |} ⇒
    let? '(staked_hash, published_at_level, ctxt, balance_updates) :=
      Alpha_context.Sc_rollup.Stake_storage.publish_commitment ctxt rollup
        source commitment in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_publish_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
            := staked_hash;
          Apply_results.successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
            := published_at_level;
          Apply_results.successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
            := balance_updates; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_refute {|
      Alpha_context.manager_operation.Sc_rollup_refute.rollup := rollup;
        Alpha_context.manager_operation.Sc_rollup_refute.opponent := opponent;
        Alpha_context.manager_operation.Sc_rollup_refute.refutation :=
          refutation
        |} ⇒
    let player_value := source in
    let? '(game_result, ctxt) :=
      match refutation with
      | None ⇒
        let? ctxt :=
          Alpha_context.Sc_rollup.Refutation_storage.start_game ctxt rollup
            player_value opponent in
        return? (None, ctxt)
      | Some refutation ⇒
        Alpha_context.Sc_rollup.Refutation_storage.game_move ctxt rollup
          player_value opponent refutation
      end in
    let? '(game_status, ctxt, balance_updates) :=
      match game_result with
      | None ⇒ return? (Alpha_context.Sc_rollup.Game.Ongoing, ctxt, nil)
      | Some game_result ⇒
        let stakers := Alpha_context.Sc_rollup.Game.Index.make source opponent
          in
        Alpha_context.Sc_rollup.Refutation_storage.apply_game_result ctxt rollup
          stakers game_result
      end in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_refute_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_refute_result.game_status
            := game_status;
          Apply_results.successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
            := balance_updates; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_timeout {|
      Alpha_context.manager_operation.Sc_rollup_timeout.rollup := rollup;
        Alpha_context.manager_operation.Sc_rollup_timeout.stakers := stakers
        |} ⇒
    let? '(game_result, ctxt) :=
      Alpha_context.Sc_rollup.Refutation_storage.timeout ctxt rollup stakers in
    let? '(game_status, ctxt, balance_updates) :=
      Alpha_context.Sc_rollup.Refutation_storage.apply_game_result ctxt rollup
        stakers game_result in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_timeout_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_timeout_result.game_status
            := game_status;
          Apply_results.successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
            := balance_updates; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Sc_rollup_execute_outbox_message {|
      Alpha_context.manager_operation.Sc_rollup_execute_outbox_message.rollup :=
        rollup;
        Alpha_context.manager_operation.Sc_rollup_execute_outbox_message.cemented_commitment
          := cemented_commitment;
        Alpha_context.manager_operation.Sc_rollup_execute_outbox_message.output_proof
          := output_proof
        |} ⇒
    let?
      '({|
        Sc_rollup_operations.execute_outbox_message_result.paid_storage_size_diff :=
          paid_storage_size_diff;
          Sc_rollup_operations.execute_outbox_message_result.operations :=
            operations
          |}, ctxt) :=
      Sc_rollup_operations.execute_outbox_message ctxt rollup
        cemented_commitment source output_proof in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before_op ctxt in
    let result_value :=
      Apply_results.Sc_rollup_execute_outbox_message_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
            := nil;
          Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
            := consumed_gas;
          Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
            := paid_storage_size_diff; |} in
    return? (ctxt, result_value, operations)
  |
    Alpha_context.Sc_rollup_recover_bond {|
      Alpha_context.manager_operation.Sc_rollup_recover_bond.sc_rollup := sc_rollup
        |} ⇒
    let? '(ctxt, balance_updates) :=
      Alpha_context.Sc_rollup.Stake_storage.withdraw_stake ctxt sc_rollup source
      in
    let result_value :=
      Apply_results.Sc_rollup_recover_bond_result
        {|
          Apply_results.successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
            := balance_updates;
          Apply_results.successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
            := Alpha_context.Gas.consumed ctxt_before_op ctxt; |} in
    return? (ctxt, result_value, nil)
  |
    Alpha_context.Zk_rollup_origination {|
      Alpha_context.manager_operation.Zk_rollup_origination.public_parameters :=
        public_parameters;
        Alpha_context.manager_operation.Zk_rollup_origination.circuits_info :=
          circuits_info;
        Alpha_context.manager_operation.Zk_rollup_origination.init_state :=
          init_state;
        Alpha_context.manager_operation.Zk_rollup_origination.nb_ops := nb_ops
        |} ⇒
    Zk_rollup_apply.originate ctxt_before_op ctxt public_parameters
      circuits_info init_state nb_ops
  |
    Alpha_context.Zk_rollup_publish {|
      Alpha_context.manager_operation.Zk_rollup_publish.zk_rollup := zk_rollup;
        Alpha_context.manager_operation.Zk_rollup_publish.ops := ops
        |} ⇒ Zk_rollup_apply.publish ctxt_before_op ctxt zk_rollup ops
  |
    Alpha_context.Zk_rollup_update {|
      Alpha_context.manager_operation.Zk_rollup_update.zk_rollup := zk_rollup;
        Alpha_context.manager_operation.Zk_rollup_update.update := update
        |} ⇒ Zk_rollup_apply.update ctxt_before_op ctxt zk_rollup update
  end.

Inductive success_or_failure : Set :=
| Success : Alpha_context.context → success_or_failure
| Failure : success_or_failure.

#[bypass_check(guard)]
Definition apply_internal_operations
  (ctxt : Alpha_context.context) (payer : Alpha_context.public_key_hash)
  (chain_id : Chain_id.t) (ops : list Script_typed_ir.packed_internal_operation)
  : success_or_failure ×
    list Apply_internal_results.packed_internal_operation_result :=
  let fix apply
    (ctxt : Alpha_context.context)
    (applied : list Apply_internal_results.packed_internal_operation_result)
    (worklist : list Script_typed_ir.packed_internal_operation) {struct ctxt}
    : success_or_failure ×
      list Apply_internal_results.packed_internal_operation_result :=
    match worklist with
    | [] ⇒ ((Success ctxt), (List.rev applied))
    |
      cons
        (Script_typed_ir.Internal_operation
          ({|
            Script_typed_ir.internal_operation.source := source;
              Script_typed_ir.internal_operation.operation := operation;
              Script_typed_ir.internal_operation.nonce := nonce_value
              |} as op)) rest ⇒
      let function_parameter :=
        if Alpha_context.internal_nonce_already_recorded ctxt nonce_value then
          let op_res := Apply_internal_results.internal_operation_value op in
          Error_monad.tzfail
            (Build_extensible "Internal_operation_replay"
              Apply_internal_results.packed_internal_operation
              (Apply_internal_results.Internal_operation op_res))
        else
          let ctxt := Alpha_context.record_internal_nonce ctxt nonce_value in
          apply_internal_operation_contents ctxt payer source chain_id operation
        in
      match function_parameter with
      | Pervasives.Error errors ⇒
        let result_value :=
          Apply_internal_results.pack_internal_operation_result op
            (Apply_operation_result.Failed
              (Script_typed_ir.manager_kind
                op.(Script_typed_ir.internal_operation.operation)) errors) in
        let skipped :=
          List.rev_map
            (fun (function_parameter :
              Script_typed_ir.packed_internal_operation) ⇒
              let 'Script_typed_ir.Internal_operation op := function_parameter
                in
              Apply_internal_results.pack_internal_operation_result op
                (Apply_operation_result.Skipped
                  (Script_typed_ir.manager_kind
                    op.(Script_typed_ir.internal_operation.operation)))) rest in
        (Failure,
          (List.rev (Pervasives.op_at skipped (cons result_value applied))))
      | Pervasives.Ok (ctxt, result_value, emitted) ⇒
        apply ctxt
          (cons
            (Apply_internal_results.pack_internal_operation_result op
              (Apply_operation_result.Applied result_value)) applied)
          (Pervasives.op_at emitted rest)
      end
    end in
  apply ctxt nil ops.

Definition burn_transaction_storage_fees
  (ctxt : Alpha_context.context)
  (trr : Apply_internal_results.successful_transaction_result)
  (storage_limit : Z.t) (payer : Alpha_context.Token.source)
  : M?
    (Alpha_context.context × Z.t ×
      Apply_internal_results.successful_transaction_result) :=
  match trr with
  | Apply_internal_results.Transaction_to_contract_result payload ⇒
    let consumed :=
      payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let? '(ctxt, storage_limit, origination_bus) :=
      if
        payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract)
      then
        Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer
      else
        return? (ctxt, storage_limit, nil) in
    let balance_updates :=
      Pervasives.op_at storage_bus
        (Pervasives.op_at
          payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates)
          origination_bus) in
    return?
      (ctxt, storage_limit,
        (Apply_internal_results.Transaction_to_contract_result
          {|
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
              := balance_updates;
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff);
            Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
              :=
              payload.(Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract);
            |}))
  | Apply_internal_results.Transaction_to_tx_rollup_result payload ⇒
    let consumed :=
      payload.(Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_internal_results.Transaction_to_tx_rollup_result
          (Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.with_balance_updates
            balance_updates payload)))
  | Apply_internal_results.Transaction_to_sc_rollup_result _ ⇒
    return? (ctxt, storage_limit, trr)
  | Apply_internal_results.Transaction_to_zk_rollup_result payload ⇒
    let consumed :=
      payload.(Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_internal_results.Transaction_to_zk_rollup_result
          (Apply_internal_results.successful_transaction_result.Transaction_to_zk_rollup_result.with_balance_updates
            balance_updates payload)))
  end.

Definition burn_origination_storage_fees
  (ctxt : Alpha_context.context)
  (function_parameter : Apply_internal_results.successful_origination_result)
  : Z.t → Alpha_context.Token.source →
  M?
    (Alpha_context.context × Z.t ×
      Apply_internal_results.successful_origination_result) :=
  let '{|
    Apply_internal_results.successful_origination_result.lazy_storage_diff :=
      lazy_storage_diff;
      Apply_internal_results.successful_origination_result.balance_updates :=
        balance_updates;
      Apply_internal_results.successful_origination_result.originated_contracts
        := originated_contracts;
      Apply_internal_results.successful_origination_result.consumed_gas :=
        consumed_gas;
      Apply_internal_results.successful_origination_result.storage_size :=
        storage_size;
      Apply_internal_results.successful_origination_result.paid_storage_size_diff
        := paid_storage_size_diff
      |} := function_parameter in
  fun (storage_limit : Z.t) ⇒
    fun (payer : Alpha_context.Token.source) ⇒
      let consumed := paid_storage_size_diff in
      let? '(ctxt, storage_limit, storage_bus) :=
        Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
          consumed in
      let? '(ctxt, storage_limit, origination_bus) :=
        Alpha_context.Fees.burn_origination_fees None ctxt storage_limit payer
        in
      let balance_updates :=
        Pervasives.op_at storage_bus
          (Pervasives.op_at origination_bus balance_updates) in
      return?
        (ctxt, storage_limit,
          {|
            Apply_internal_results.successful_origination_result.lazy_storage_diff
              := lazy_storage_diff;
            Apply_internal_results.successful_origination_result.balance_updates
              := balance_updates;
            Apply_internal_results.successful_origination_result.originated_contracts
              := originated_contracts;
            Apply_internal_results.successful_origination_result.consumed_gas :=
              consumed_gas;
            Apply_internal_results.successful_origination_result.storage_size :=
              storage_size;
            Apply_internal_results.successful_origination_result.paid_storage_size_diff
              := paid_storage_size_diff; |}).

[burn_manager_storage_fees ctxt smopr storage_limit payer] burns the storage fees associated to an external operation result [smopr]. Returns an updated context, an updated storage limit with the space consumed by the operation subtracted, and [smopr] with the relevant balance updates included.

Definition burn_manager_storage_fees
  (ctxt : Alpha_context.context)
  (smopr : Apply_results.successful_manager_operation_result)
  (storage_limit : Z.t) (payer : Alpha_context.public_key_hash)
  : M?
    (Alpha_context.context × Z.t ×
      Apply_results.successful_manager_operation_result) :=
  let payer :=
    Alpha_context.Token.Source_container
      (Alpha_context.Token.Contract (Contract_repr.Implicit payer)) in
  match smopr with
  | Apply_results.Transaction_result transaction_result ⇒
    let? '(ctxt, storage_limit, transaction_result) :=
      burn_transaction_storage_fees ctxt transaction_result storage_limit payer
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Transaction_result transaction_result))
  | Apply_results.Origination_result origination_result ⇒
    let? '(ctxt, storage_limit, origination_result) :=
      burn_origination_storage_fees ctxt origination_result storage_limit payer
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Origination_result origination_result))
  | (Apply_results.Reveal_result _ | Apply_results.Delegation_result _) ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Register_global_constant_result payload ⇒
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Register_global_constant_result
          {|
            Apply_results.successful_manager_operation_result.Register_global_constant_result.balance_updates
              := balance_updates;
            Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas
              :=
              payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.consumed_gas);
            Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant
              :=
              payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.size_of_constant);
            Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address
              :=
              payload.(Apply_results.successful_manager_operation_result.Register_global_constant_result.global_address);
            |}))
  |
    (Apply_results.Set_deposits_limit_result _ |
    Apply_results.Update_consensus_key_result _) ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Increase_paid_storage_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Tx_rollup_origination_result payload ⇒
    let? '(ctxt, storage_limit, origination_bus) :=
      Alpha_context.Fees.burn_tx_rollup_origination_fees None ctxt storage_limit
        payer in
    let balance_updates :=
      Pervasives.op_at origination_bus
        payload.(Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Tx_rollup_origination_result
          (Apply_results.successful_manager_operation_result.Tx_rollup_origination_result.with_balance_updates
            balance_updates payload)))
  |
    (Apply_results.Tx_rollup_return_bond_result _ |
    Apply_results.Tx_rollup_remove_commitment_result _ |
    Apply_results.Tx_rollup_rejection_result _ |
    Apply_results.Tx_rollup_finalize_commitment_result _ |
    Apply_results.Tx_rollup_commit_result _) ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Transfer_ticket_result payload ⇒
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at
        payload.(Apply_results.successful_manager_operation_result.Transfer_ticket_result.balance_updates)
        storage_bus in
    return?
      (ctxt, storage_limit,
        (Apply_results.Transfer_ticket_result
          (Apply_results.successful_manager_operation_result.Transfer_ticket_result.with_balance_updates
            balance_updates payload)))
  | Apply_results.Tx_rollup_submit_batch_result payload ⇒
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Tx_rollup_submit_batch_result
          (Apply_results.successful_manager_operation_result.Tx_rollup_submit_batch_result.with_balance_updates
            balance_updates payload)))
  | Apply_results.Tx_rollup_dispatch_tickets_result payload ⇒
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Tx_rollup_dispatch_tickets_result
          (Apply_results.successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.with_balance_updates
            balance_updates payload)))
  | Apply_results.Dal_publish_slot_header_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Sc_rollup_originate_result payload ⇒
    let? '(ctxt, storage_limit, balance_updates) :=
      Alpha_context.Fees.burn_sc_rollup_origination_fees None ctxt storage_limit
        payer
        payload.(Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.size)
      in
    let result_value :=
      Apply_results.Sc_rollup_originate_result
        (Apply_results.successful_manager_operation_result.Sc_rollup_originate_result.with_balance_updates
          balance_updates payload) in
    return? (ctxt, storage_limit, result_value)
  | Apply_results.Sc_rollup_add_messages_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Sc_rollup_cement_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Sc_rollup_publish_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Sc_rollup_refute_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Sc_rollup_timeout_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  |
    Apply_results.Sc_rollup_execute_outbox_message_result
      ({|
        Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
          := balance_updates;
          Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
            := paid_storage_size_diff
          |} as payload) ⇒
    let consumed := paid_storage_size_diff in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates := Pervasives.op_at storage_bus balance_updates in
    return?
      (ctxt, storage_limit,
        (Apply_results.Sc_rollup_execute_outbox_message_result
          (Apply_results.successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.with_balance_updates
            balance_updates payload)))
  | Apply_results.Sc_rollup_recover_bond_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_results.Zk_rollup_origination_result payload ⇒
    let? '(ctxt, storage_limit, balance_updates) :=
      Alpha_context.Fees.burn_zk_rollup_origination_fees None ctxt storage_limit
        payer
        payload.(Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.storage_size)
      in
    let result_value :=
      Apply_results.Zk_rollup_origination_result
        (Apply_results.successful_manager_operation_result.Zk_rollup_origination_result.with_balance_updates
          balance_updates payload) in
    return? (ctxt, storage_limit, result_value)
  | Apply_results.Zk_rollup_publish_result payload ⇒
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff)
      in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates :=
      Pervasives.op_at storage_bus
        payload.(Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Zk_rollup_publish_result
          (Apply_results.successful_manager_operation_result.Zk_rollup_publish_result.with_balance_updates
            balance_updates payload)))
  |
    Apply_results.Zk_rollup_update_result
      ({|
        Apply_results.successful_manager_operation_result.Zk_rollup_update_result.balance_updates
          := balance_updates;
          Apply_results.successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
            := paid_storage_size_diff
          |} as payload) ⇒
    let consumed := paid_storage_size_diff in
    let? '(ctxt, storage_limit, storage_bus) :=
      Alpha_context.Fees.burn_storage_fees None ctxt storage_limit payer
        consumed in
    let balance_updates := Pervasives.op_at storage_bus balance_updates in
    return?
      (ctxt, storage_limit,
        (Apply_results.Zk_rollup_update_result
          (Apply_results.successful_manager_operation_result.Zk_rollup_update_result.with_balance_updates
            balance_updates payload)))
  end.

[burn_internal_storage_fees ctxt smopr storage_limit payer] burns the storage fees associated to an internal operation result [smopr]. Returns an updated context, an updated storage limit with the space consumed by the operation subtracted, and [smopr] with the relevant balance updates included.

Definition burn_internal_storage_fees
  (ctxt : Alpha_context.context)
  (smopr : Apply_internal_results.successful_internal_operation_result)
  (storage_limit : Z.t) (payer : Alpha_context.public_key_hash)
  : M?
    (Alpha_context.context × Z.t ×
      Apply_internal_results.successful_internal_operation_result) :=
  let payer :=
    Alpha_context.Token.Source_container
      (Alpha_context.Token.Contract (Contract_repr.Implicit payer)) in
  match smopr with
  | Apply_internal_results.ITransaction_result transaction_result ⇒
    let? '(ctxt, storage_limit, transaction_result) :=
      burn_transaction_storage_fees ctxt transaction_result storage_limit payer
      in
    return?
      (ctxt, storage_limit,
        (Apply_internal_results.ITransaction_result transaction_result))
  | Apply_internal_results.IOrigination_result origination_result ⇒
    let? '(ctxt, storage_limit, origination_result) :=
      burn_origination_storage_fees ctxt origination_result storage_limit payer
      in
    return?
      (ctxt, storage_limit,
        (Apply_internal_results.IOrigination_result origination_result))
  | Apply_internal_results.IDelegation_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  | Apply_internal_results.IEvent_result _ ⇒
    return? (ctxt, storage_limit, smopr)
  end.

Definition apply_manager_contents
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (op : Alpha_context.contents)
  : success_or_failure × Apply_results.manager_operation_result ×
    list Apply_internal_results.packed_internal_operation_result :=
  match op with
  |
    Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.source := source;
        Alpha_context.contents.Manager_operation.operation := operation;
        Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
        Alpha_context.contents.Manager_operation.storage_limit := storage_limit
        |} ⇒
    let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
    let function_parameter :=
      apply_manager_operation ctxt source chain_id operation in
    match function_parameter with
    | Pervasives.Ok (ctxt, operation_results, internal_operations) ⇒
      let function_parameter :=
        apply_internal_operations ctxt source chain_id internal_operations in
      match function_parameter with
      | (Success ctxt, internal_operations_results) ⇒
        let function_parameter :=
          burn_manager_storage_fees ctxt operation_results storage_limit source
          in
        match function_parameter with
        | Pervasives.Ok (ctxt, storage_limit, operation_results) ⇒
          let function_parameter :=
            List.fold_left_es
              (fun (function_parameter :
                Alpha_context.context × Z.t ×
                  list Apply_internal_results.packed_internal_operation_result)
                ⇒
                let '(ctxt, storage_limit, res) := function_parameter in
                fun (imopr :
                  Apply_internal_results.packed_internal_operation_result) ⇒
                  let
                    'Apply_internal_results.Internal_operation_result op mopr :=
                    imopr in
                  match mopr with
                  | Apply_operation_result.Applied smopr ⇒
                    let? '(ctxt, storage_limit, smopr) :=
                      burn_internal_storage_fees ctxt smopr storage_limit source
                      in
                    let imopr :=
                      Apply_internal_results.Internal_operation_result op
                        (Apply_operation_result.Applied smopr) in
                    return? (ctxt, storage_limit, (cons imopr res))
                  | _ ⇒ return? (ctxt, storage_limit, (cons imopr res))
                  end) (ctxt, storage_limit, nil) internal_operations_results in
          match function_parameter with
          | Pervasives.Ok (ctxt, _, internal_operations_results) ⇒
            ((Success ctxt), (Apply_operation_result.Applied operation_results),
              (List.rev internal_operations_results))
          | Pervasives.Error errors ⇒
            (Failure,
              (Apply_operation_result.Backtracked operation_results
                (Some errors)), internal_operations_results)
          end
        | Pervasives.Error errors ⇒
          (Failure,
            (Apply_operation_result.Backtracked operation_results (Some errors)),
            internal_operations_results)
        end
      | (Failure, internal_operations_results) ⇒
        (Failure, (Apply_operation_result.Applied operation_results),
          internal_operations_results)
      end
    | Pervasives.Error errors ⇒
      (Failure,
        (Apply_operation_result.Failed (Alpha_context.manager_kind operation)
          errors), nil)
    end
  | _ ⇒ unreachable_gadt_branch
  end.

An individual manager operation (either standalone or inside a batch) together with the balance update corresponding to the transfer of its fee.

Module fees_updated_contents.
  Record record : Set := Build {
    contents : Alpha_context.contents;
    balance_updates : Alpha_context.Receipt.balance_updates;
  }.
  Definition with_contents contents (r : record) :=
    Build contents r.(balance_updates).
  Definition with_balance_updates balance_updates (r : record) :=
    Build r.(contents) balance_updates.
End fees_updated_contents.
Definition fees_updated_contents := fees_updated_contents.record.

Inductive fees_updated_contents_list : Set :=
| FeesUpdatedSingle : fees_updated_contents → fees_updated_contents_list
| FeesUpdatedCons :
  fees_updated_contents → fees_updated_contents_list →
  fees_updated_contents_list.

Fixpoint mark_skipped
  (payload_producer : Alpha_context.Consensus_key.t)
  (level : Alpha_context.Level.t)
  (fees_updated_contents_list : fees_updated_contents_list)
  : Apply_results.contents_result_list :=
  match fees_updated_contents_list with
  |
    FeesUpdatedSingle {|
      fees_updated_contents.contents :=
        Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.operation := operation
            |};
        fees_updated_contents.balance_updates := balance_updates
        |} ⇒
    Apply_results.Single_result
      (Apply_results.Manager_operation_result
        {|
          Apply_results.contents_result.Manager_operation_result.balance_updates
            := balance_updates;
          Apply_results.contents_result.Manager_operation_result.operation_result
            :=
            Apply_operation_result.Skipped
              (Alpha_context.manager_kind operation);
          Apply_results.contents_result.Manager_operation_result.internal_operation_results
            := nil; |})
  |
    FeesUpdatedCons {|
      fees_updated_contents.contents :=
        Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.operation := operation
            |};
        fees_updated_contents.balance_updates := balance_updates
        |} rest ⇒
    Apply_results.Cons_result
      (Apply_results.Manager_operation_result
        {|
          Apply_results.contents_result.Manager_operation_result.balance_updates
            := balance_updates;
          Apply_results.contents_result.Manager_operation_result.operation_result
            :=
            Apply_operation_result.Skipped
              (Alpha_context.manager_kind operation);
          Apply_results.contents_result.Manager_operation_result.internal_operation_results
            := nil; |}) (mark_skipped payload_producer level rest)
  | _ ⇒ unreachable_gadt_branch
  end.

Return balance updates for fees, and an updated context that accounts for: - fees spending, - counter incrementation, - consumption of each operation's [gas_limit] from the available block gas.

The operation should already have been validated by {!Validate.validate_operation}. The latter is responsible for ensuring that the operation is solvable, i.e. its fees can be taken, i.e. [take_fees] cannot return an error.

Definition take_fees
  (ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
  : M? (Alpha_context.context × fees_updated_contents_list) :=
  let fix take_fees_rec
    (ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
    : M? (Alpha_context.context × fees_updated_contents_list) :=
    let contents_effects (contents : Alpha_context.contents)
      : M? (Alpha_context.context × fees_updated_contents) :=
      match contents with
      |
        Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.source := source;
            Alpha_context.contents.Manager_operation.fee := fee;
            Alpha_context.contents.Manager_operation.gas_limit := gas_limit
            |} ⇒
        let? ctxt := Alpha_context.Gas.consume_limit_in_block ctxt gas_limit in
        let? ctxt := Alpha_context.Contract.increment_counter ctxt source in
        Error_monad.Lwt_result_syntax.op_letplus
          (Alpha_context.Token.transfer None ctxt
            (Alpha_context.Token.Source_container
              (Alpha_context.Token.Contract (Contract_repr.Implicit source)))
            (Alpha_context.Token.Sink_container Alpha_context.Token.Block_fees)
            fee)
          (fun function_parameter ⇒
            let '(ctxt, balance_updates) := function_parameter in
            (ctxt,
              {| fees_updated_contents.contents := contents;
                fees_updated_contents.balance_updates := balance_updates; |}))
      | _ ⇒ unreachable_gadt_branch
      end in
    match contents_list with
    | Alpha_context.Single contents ⇒
      Error_monad.Lwt_result_syntax.op_letplus (contents_effects contents)
        (fun function_parameter ⇒
          let '(ctxt, fees_updated_contents) := function_parameter in
          (ctxt, (FeesUpdatedSingle fees_updated_contents)))
    | Alpha_context.Cons contents rest ⇒
      let? '(ctxt, fees_updated_contents) := contents_effects contents in
      Error_monad.Lwt_result_syntax.op_letplus (take_fees_rec ctxt rest)
        (fun function_parameter ⇒
          let '(ctxt, result_rest) := function_parameter in
          (ctxt, (FeesUpdatedCons fees_updated_contents result_rest)))
    end in
  let result_value := take_fees_rec ctxt contents_list in
  Error_monad.record_trace (Build_extensible "Error_while_taking_fees" unit tt)
    result_value.

Fixpoint apply_manager_contents_list_rec
  (ctxt : Alpha_context.context)
  (payload_producer : Alpha_context.Consensus_key.t) (chain_id : Chain_id.t)
  (fees_updated_contents_list : fees_updated_contents_list)
  : success_or_failure × Apply_results.contents_result_list :=
  let level := Alpha_context.Level.current ctxt in
  match fees_updated_contents_list with
  |
    FeesUpdatedSingle {|
      fees_updated_contents.contents := (Alpha_context.Manager_operation _) as op;
        fees_updated_contents.balance_updates := balance_updates
        |} ⇒
    let '(ctxt_result, operation_result, internal_operation_results) :=
      apply_manager_contents ctxt chain_id op in
    let result_value :=
      Apply_results.Manager_operation_result
        {|
          Apply_results.contents_result.Manager_operation_result.balance_updates
            := balance_updates;
          Apply_results.contents_result.Manager_operation_result.operation_result
            := operation_result;
          Apply_results.contents_result.Manager_operation_result.internal_operation_results
            := internal_operation_results; |} in
    (ctxt_result, (Apply_results.Single_result result_value))
  |
    FeesUpdatedCons {|
      fees_updated_contents.contents := (Alpha_context.Manager_operation _) as op;
        fees_updated_contents.balance_updates := balance_updates
        |} rest ⇒
    let function_parameter := apply_manager_contents ctxt chain_id op in
    match function_parameter with
    | (Failure, operation_result, internal_operation_results) ⇒
      let result_value :=
        Apply_results.Manager_operation_result
          {|
            Apply_results.contents_result.Manager_operation_result.balance_updates
              := balance_updates;
            Apply_results.contents_result.Manager_operation_result.operation_result
              := operation_result;
            Apply_results.contents_result.Manager_operation_result.internal_operation_results
              := internal_operation_results; |} in
      (Failure,
        (Apply_results.Cons_result result_value
          (mark_skipped payload_producer level rest)))
    | (Success ctxt, operation_result, internal_operation_results) ⇒
      let result_value :=
        Apply_results.Manager_operation_result
          {|
            Apply_results.contents_result.Manager_operation_result.balance_updates
              := balance_updates;
            Apply_results.contents_result.Manager_operation_result.operation_result
              := operation_result;
            Apply_results.contents_result.Manager_operation_result.internal_operation_results
              := internal_operation_results; |} in
      let '(ctxt_result, results) :=
        apply_manager_contents_list_rec ctxt payload_producer chain_id rest in
      (ctxt_result, (Apply_results.Cons_result result_value results))
    end
  | _ ⇒ unreachable_gadt_branch
  end.

Definition mark_backtracked (results : Apply_results.contents_result_list)
  : Apply_results.contents_result_list :=
  let mark_results (results : Apply_results.contents_result)
    : Apply_results.contents_result :=
    let mark_manager_operation_result
      (function_parameter : Apply_results.manager_operation_result)
      : Apply_results.manager_operation_result :=
      match function_parameter with
      |
        (Apply_operation_result.Failed _ _ | Apply_operation_result.Skipped _ |
        Apply_operation_result.Backtracked _ _) as result_value ⇒ result_value
      | Apply_operation_result.Applied result_value ⇒
        Apply_operation_result.Backtracked result_value None
      end in
    let mark_internal_operation_result
      (function_parameter : Apply_internal_results.internal_operation_result)
      : Apply_internal_results.internal_operation_result :=
      match function_parameter with
      |
        (Apply_operation_result.Failed _ _ | Apply_operation_result.Skipped _ |
        Apply_operation_result.Backtracked _ _) as result_value ⇒ result_value
      | Apply_operation_result.Applied result_value ⇒
        Apply_operation_result.Backtracked result_value None
      end in
    let mark_internal_operation_results
      (function_parameter :
        Apply_internal_results.packed_internal_operation_result)
      : Apply_internal_results.packed_internal_operation_result :=
      let
        'Apply_internal_results.Internal_operation_result kind_value
          result_value := function_parameter in
      Apply_internal_results.Internal_operation_result kind_value
        (mark_internal_operation_result result_value) in
    match results with
    | Apply_results.Manager_operation_result op ⇒
      Apply_results.Manager_operation_result
        {|
          Apply_results.contents_result.Manager_operation_result.balance_updates
            :=
            op.(Apply_results.contents_result.Manager_operation_result.balance_updates);
          Apply_results.contents_result.Manager_operation_result.operation_result
            :=
            mark_manager_operation_result
              op.(Apply_results.contents_result.Manager_operation_result.operation_result);
          Apply_results.contents_result.Manager_operation_result.internal_operation_results
            :=
            List.map mark_internal_operation_results
              op.(Apply_results.contents_result.Manager_operation_result.internal_operation_results);
          |}
    | _ ⇒ unreachable_gadt_branch
    end in
  let fix traverse_apply_results
    (function_parameter : Apply_results.contents_result_list)
    : Apply_results.contents_result_list :=
    match function_parameter with
    | Apply_results.Single_result res ⇒
      Apply_results.Single_result (mark_results res)
    | Apply_results.Cons_result res rest ⇒
      Apply_results.Cons_result (mark_results res) (traverse_apply_results rest)
    end in
  traverse_apply_results results.

Records for the constructor parameters

Module ConstructorRecords_mode.
  Module mode.
    Module Application.
      Record record {block_header fitness payload_producer block_producer
        predecessor_level predecessor_round : Set} : Set := Build {
        block_header : block_header;
        fitness : fitness;
        payload_producer : payload_producer;
        block_producer : block_producer;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
      }.
      Arguments record : clear implicits.
      Definition with_block_header
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} block_header
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round block_header r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_fitness
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} fitness
        (r :
          record t_block_header t_fitness t_payload_producer t_block_producer
            t_predecessor_level t_predecessor_round) :=
        Build t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round r.(block_header) fitness
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_payload_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round}