🏗️ 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} payload_producer
        (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) r.(fitness)
          payload_producer r.(block_producer) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_block_producer
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} block_producer
        (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) r.(fitness)
          r.(payload_producer) block_producer r.(predecessor_level)
          r.(predecessor_round).
      Definition with_predecessor_level
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} predecessor_level
        (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) r.(fitness)
          r.(payload_producer) r.(block_producer) predecessor_level
          r.(predecessor_round).
      Definition with_predecessor_round
        {t_block_header t_fitness t_payload_producer t_block_producer
          t_predecessor_level t_predecessor_round} predecessor_round
        (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) r.(fitness)
          r.(payload_producer) r.(block_producer) r.(predecessor_level)
          predecessor_round.
    End Application.
    Definition Application_skeleton := Application.record.

    Module Full_construction.
      Record record {block_data_contents predecessor_hash payload_producer
        block_producer round predecessor_level predecessor_round : Set} : Set := Build {
        block_data_contents : block_data_contents;
        predecessor_hash : predecessor_hash;
        payload_producer : payload_producer;
        block_producer : block_producer;
        round : round;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
      }.
      Arguments record : clear implicits.
      Definition with_block_data_contents
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        block_data_contents
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          block_data_contents r.(predecessor_hash) r.(payload_producer)
          r.(block_producer) r.(round) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_predecessor_hash
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        predecessor_hash
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) predecessor_hash r.(payload_producer)
          r.(block_producer) r.(round) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_payload_producer
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        payload_producer
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) r.(predecessor_hash) payload_producer
          r.(block_producer) r.(round) r.(predecessor_level)
          r.(predecessor_round).
      Definition with_block_producer
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        block_producer
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) r.(predecessor_hash) r.(payload_producer)
          block_producer r.(round) r.(predecessor_level) r.(predecessor_round).
      Definition with_round
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        round
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) r.(predecessor_hash) r.(payload_producer)
          r.(block_producer) round r.(predecessor_level) r.(predecessor_round).
      Definition with_predecessor_level
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        predecessor_level
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) r.(predecessor_hash) r.(payload_producer)
          r.(block_producer) r.(round) predecessor_level r.(predecessor_round).
      Definition with_predecessor_round
        {t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round}
        predecessor_round
        (r :
          record t_block_data_contents t_predecessor_hash t_payload_producer
            t_block_producer t_round t_predecessor_level t_predecessor_round) :=
        Build t_block_data_contents t_predecessor_hash t_payload_producer
          t_block_producer t_round t_predecessor_level t_predecessor_round
          r.(block_data_contents) r.(predecessor_hash) r.(payload_producer)
          r.(block_producer) r.(round) r.(predecessor_level) predecessor_round.
    End Full_construction.
    Definition Full_construction_skeleton := Full_construction.record.

    Module Partial_construction.
      Record record {predecessor_level predecessor_fitness : Set} : Set := Build {
        predecessor_level : predecessor_level;
        predecessor_fitness : predecessor_fitness;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor_level
        {t_predecessor_level t_predecessor_fitness} predecessor_level
        (r : record t_predecessor_level t_predecessor_fitness) :=
        Build t_predecessor_level t_predecessor_fitness predecessor_level
          r.(predecessor_fitness).
      Definition with_predecessor_fitness
        {t_predecessor_level t_predecessor_fitness} predecessor_fitness
        (r : record t_predecessor_level t_predecessor_fitness) :=
        Build t_predecessor_level t_predecessor_fitness r.(predecessor_level)
          predecessor_fitness.
    End Partial_construction.
    Definition Partial_construction_skeleton := Partial_construction.record.
  End mode.
End ConstructorRecords_mode.
Import ConstructorRecords_mode.

Reserved Notation "'mode.Application".
Reserved Notation "'mode.Full_construction".
Reserved Notation "'mode.Partial_construction".

Inductive mode : Set :=
| Application : 'mode.Application → mode
| Full_construction : 'mode.Full_construction → mode
| Partial_construction : 'mode.Partial_construction → mode

where "'mode.Application" :=
  (mode.Application_skeleton Alpha_context.Block_header.t
    Alpha_context.Fitness.t Alpha_context.Consensus_key.t
    Alpha_context.Consensus_key.t Alpha_context.Level.t Alpha_context.Round.t)
and "'mode.Full_construction" :=
  (mode.Full_construction_skeleton Alpha_context.Block_header.contents
    Block_hash.t Alpha_context.Consensus_key.t Alpha_context.Consensus_key.t
    Alpha_context.Round.t Alpha_context.Level.t Alpha_context.Round.t)
and "'mode.Partial_construction" :=
  (mode.Partial_construction_skeleton Alpha_context.Raw_level.t
    Alpha_context.Fitness.raw).

Module mode.
  Include ConstructorRecords_mode.mode.
  Definition Application := 'mode.Application.
  Definition Full_construction := 'mode.Full_construction.
  Definition Partial_construction := 'mode.Partial_construction.
End mode.

Module application_state.
  Record record : Set := Build {
    ctxt : Alpha_context.t;
    chain_id : Chain_id.t;
    mode : mode;
    op_count : int;
    migration_balance_updates : Alpha_context.Receipt.balance_updates;
    liquidity_baking_toggle_ema : Alpha_context.Liquidity_baking.Toggle_EMA.t;
    implicit_operations_results :
      list Apply_results.packed_successful_manager_operation_result;
  }.
  Definition with_ctxt ctxt (r : record) :=
    Build ctxt r.(chain_id) r.(mode) r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_chain_id chain_id (r : record) :=
    Build r.(ctxt) chain_id r.(mode) r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_mode mode (r : record) :=
    Build r.(ctxt) r.(chain_id) mode r.(op_count) r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_op_count op_count (r : record) :=
    Build r.(ctxt) r.(chain_id) r.(mode) op_count r.(migration_balance_updates)
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_migration_balance_updates migration_balance_updates
    (r : record) :=
    Build r.(ctxt) r.(chain_id) r.(mode) r.(op_count) migration_balance_updates
      r.(liquidity_baking_toggle_ema) r.(implicit_operations_results).
  Definition with_liquidity_baking_toggle_ema liquidity_baking_toggle_ema
    (r : record) :=
    Build r.(ctxt) r.(chain_id) r.(mode) r.(op_count)
      r.(migration_balance_updates) liquidity_baking_toggle_ema
      r.(implicit_operations_results).
  Definition with_implicit_operations_results implicit_operations_results
    (r : record) :=
    Build r.(ctxt) r.(chain_id) r.(mode) r.(op_count)
      r.(migration_balance_updates) r.(liquidity_baking_toggle_ema)
      implicit_operations_results.
End application_state.
Definition application_state := application_state.record.

Definition record_operation
  (ctxt : Alpha_context.context) (hash_value : Operation_hash.t)
  (operation : Alpha_context.operation) : Alpha_context.context :=
  match
    operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
    with
  | Alpha_context.Single (Alpha_context.Preendorsement _) ⇒ ctxt
  | Alpha_context.Single (Alpha_context.Endorsement _) ⇒ ctxt
  | Alpha_context.Single (Alpha_context.Dal_attestation _) ⇒ ctxt
  |
    (Alpha_context.Single
      (Alpha_context.Failing_noop _ | Alpha_context.Proposals _ |
      Alpha_context.Ballot _ | Alpha_context.Seed_nonce_revelation _ |
      Alpha_context.Vdf_revelation _ |
      Alpha_context.Double_endorsement_evidence _ |
      Alpha_context.Double_preendorsement_evidence _ |
      Alpha_context.Double_baking_evidence _ | Alpha_context.Activate_account _
      | Alpha_context.Drain_delegate _ | Alpha_context.Manager_operation _) |
    Alpha_context.Cons (Alpha_context.Manager_operation _) _) ⇒
    Alpha_context.record_non_consensus_operation_hash ctxt hash_value
  | _ ⇒ unreachable_gadt_branch
  end.

Definition record_preendorsement
  (ctxt : Alpha_context.t) (mode : mode)
  (content : Alpha_context.consensus_content)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let? ctxt :=
    match mode with
    | Full_construction _ ⇒
      match Alpha_context.Consensus.get_preendorsements_quorum_round ctxt with
      | None ⇒
        Alpha_context.Consensus.set_preendorsements_quorum_round ctxt
          content.(Alpha_context.consensus_content.round)
      | Some _ ⇒ return? ctxt
      end
    | (Application _ | Partial_construction _) ⇒ return? ctxt
    end in
  match
    Alpha_context.Slot.Map.(Map.S.find)
      content.(Alpha_context.consensus_content.slot)
      (Alpha_context.Consensus.allowed_preendorsements ctxt) with
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Faulty_validation_wrong_slot" unit tt)
  |
    Some
      ({|
        Raw_context.consensus_pk.delegate := delegate;
          Raw_context.consensus_pk.consensus_pkh := consensus_pkh
          |}, preendorsement_power) ⇒
    let? ctxt :=
      Alpha_context.Consensus.record_preendorsement ctxt
        content.(Alpha_context.consensus_content.slot) preendorsement_power
        content.(Alpha_context.consensus_content.round) in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Preendorsement_result
            {|
              Apply_results.contents_result.Preendorsement_result.balance_updates
                := nil;
              Apply_results.contents_result.Preendorsement_result.delegate :=
                delegate;
              Apply_results.contents_result.Preendorsement_result.consensus_key
                := consensus_pkh;
              Apply_results.contents_result.Preendorsement_result.preendorsement_power
                := preendorsement_power; |})))
  end.

Definition is_grandparent_endorsement
  (mode : mode) (content : Alpha_context.consensus_content) : bool :=
  match mode with
  |
    Partial_construction {|
      mode.Partial_construction.predecessor_level := predecessor_level |} ⇒
    Alpha_context.Raw_level.op_eq
      (Alpha_context.Raw_level.succ
        content.(Alpha_context.consensus_content.level)) predecessor_level
  | _ ⇒ false
  end.

Definition record_endorsement
  (ctxt : Alpha_context.context) (mode : mode)
  (content : Alpha_context.consensus_content)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let mk_endorsement_result (function_parameter : Alpha_context.Consensus_key.t)
    : int → Apply_results.contents_result_list :=
    let '{|
      Delegate_consensus_key.t.delegate := delegate;
        Delegate_consensus_key.t.consensus_pkh := consensus_pkh
        |} := function_parameter in
    fun (endorsement_power : int) ⇒
      Apply_results.Single_result
        (Apply_results.Endorsement_result
          {|
            Apply_results.contents_result.Endorsement_result.balance_updates :=
              nil;
            Apply_results.contents_result.Endorsement_result.delegate :=
              delegate;
            Apply_results.contents_result.Endorsement_result.consensus_key :=
              consensus_pkh;
            Apply_results.contents_result.Endorsement_result.endorsement_power
              := endorsement_power; |}) in
  if is_grandparent_endorsement mode content then
    let? level :=
      Alpha_context.Level.from_raw ctxt
        content.(Alpha_context.consensus_content.level) in
    let?
      '(ctxt,
        {| Raw_context.consensus_pk.delegate := delegate |} as consensus_key) :=
      Alpha_context.Stake_distribution.slot_owner ctxt level
        content.(Alpha_context.consensus_content.slot) in
    let? ctxt :=
      Alpha_context.Consensus.record_grand_parent_endorsement ctxt delegate in
    return?
      (ctxt,
        (mk_endorsement_result (Alpha_context.Consensus_key.pkh consensus_key) 0))
  else
    match
      Alpha_context.Slot.Map.(Map.S.find)
        content.(Alpha_context.consensus_content.slot)
        (Alpha_context.Consensus.allowed_endorsements ctxt) with
    | None ⇒
      Error_monad.Lwt_result_syntax.tzfail
        (Build_extensible "Faulty_validation_wrong_slot" unit tt)
    | Some (consensus_key, power) ⇒
      let? ctxt :=
        Alpha_context.Consensus.record_endorsement ctxt
          content.(Alpha_context.consensus_content.slot) power in
      return?
        (ctxt,
          (mk_endorsement_result (Alpha_context.Consensus_key.pkh consensus_key)
            power))
    end.

Definition apply_manager_contents_list
  (ctxt : Alpha_context.context)
  (payload_producer : Alpha_context.Consensus_key.t) (chain_id : Chain_id.t)
  (fees_updated_contents_list : fees_updated_contents_list)
  : Alpha_context.context × Apply_results.contents_result_list :=
  let '(ctxt_result, results) :=
    apply_manager_contents_list_rec ctxt payload_producer chain_id
      fees_updated_contents_list in
  match ctxt_result with
  | Failure ⇒ (ctxt, (mark_backtracked results))
  | Success ctxt ⇒
    let ctxt := Alpha_context.Lazy_storage.cleanup_temporaries ctxt in
    (ctxt, results)
  end.

Definition apply_manager_operations
  (ctxt : Alpha_context.context)
  (payload_producer : Alpha_context.Consensus_key.t) (chain_id : Chain_id.t)
  (mempool_mode : bool) (contents_list : Alpha_context.contents_list)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let ctxt :=
    if mempool_mode then
      Alpha_context.Gas.reset_block_gas ctxt
    else
      ctxt in
  let? '(ctxt, fees_updated_contents_list) := take_fees ctxt contents_list in
  let '(ctxt, contents_result_list) :=
    apply_manager_contents_list ctxt payload_producer chain_id
      fees_updated_contents_list in
  return? (ctxt, contents_result_list).

Inductive mistake : Set :=
| Double_baking : mistake
| Double_endorsing : mistake.

Definition punish_delegate
  (ctxt : Alpha_context.context) (delegate : Alpha_context.public_key_hash)
  (level : Alpha_context.Level.t) (mistake : mistake)
  (mk_result :
    list
      (Alpha_context.Receipt.balance × Alpha_context.Receipt.balance_update ×
        Alpha_context.Receipt.update_origin) → Apply_results.contents_result)
  (payload_producer : Alpha_context.Consensus_key.t)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let punish :=
    match mistake with
    | Double_baking ⇒ Alpha_context.Delegate.punish_double_baking
    | Double_endorsing ⇒ Alpha_context.Delegate.punish_double_endorsing
    end in
  let? '(ctxt, burned, punish_balance_updates) := punish ctxt delegate level in
  let? '(ctxt, reward_balance_updates) :=
    match Alpha_context.Tez.op_divquestion burned 2 with
    | Pervasives.Ok reward ⇒
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_infinite
          Alpha_context.Token.Double_signing_evidence_rewards)
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract
            (Contract_repr.Implicit
              payload_producer.(Delegate_consensus_key.t.delegate)))) reward
    | Pervasives.Error _ ⇒ return? (ctxt, nil)
    end in
  let balance_updates :=
    Pervasives.op_at reward_balance_updates punish_balance_updates in
  return? (ctxt, (Apply_results.Single_result (mk_result balance_updates))).

Definition punish_double_endorsement_or_preendorsement
  (ctxt : Alpha_context.context) (op1 : Alpha_context.Operation.t)
  (payload_producer : Alpha_context.Consensus_key.t)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let mk_result (balance_updates : Alpha_context.Receipt.balance_updates)
    : Apply_results.contents_result :=
    match
      op1.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
      with
    | Alpha_context.Single (Alpha_context.Preendorsement _) ⇒
      Apply_results.Double_preendorsement_evidence_result balance_updates
    | Alpha_context.Single (Alpha_context.Endorsement _) ⇒
      Apply_results.Double_endorsement_evidence_result balance_updates
    | _ ⇒ unreachable_gadt_branch
    end in
  match
    op1.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
    with
  |
    (Alpha_context.Single (Alpha_context.Preendorsement e1) |
    Alpha_context.Single (Alpha_context.Endorsement e1)) ⇒
    let? level :=
      Alpha_context.Level.from_raw ctxt
        e1.(Alpha_context.consensus_content.level) in
    let? '(ctxt, consensus_pk1) :=
      Alpha_context.Stake_distribution.slot_owner ctxt level
        e1.(Alpha_context.consensus_content.slot) in
    punish_delegate ctxt consensus_pk1.(Raw_context.consensus_pk.delegate) level
      Double_endorsing mk_result payload_producer
  | _ ⇒ unreachable_gadt_branch
  end.

Definition punish_double_baking
  (ctxt : Alpha_context.context) (bh1 : Alpha_context.Block_header.t)
  (payload_producer : Alpha_context.Consensus_key.t)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let? bh1_fitness :=
    Alpha_context.Fitness.from_raw
      bh1.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
    in
  let round1 := Alpha_context.Fitness.round bh1_fitness in
  let? raw_level :=
    Alpha_context.Raw_level.of_int32
      bh1.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level)
    in
  let? level := Alpha_context.Level.from_raw ctxt raw_level in
  let committee_size := Alpha_context.Constants.consensus_committee_size ctxt in
  let? slot1 := Alpha_context.Round.to_slot round1 committee_size in
  let? '(ctxt, consensus_pk1) :=
    Alpha_context.Stake_distribution.slot_owner ctxt level slot1 in
  punish_delegate ctxt consensus_pk1.(Raw_context.consensus_pk.delegate) level
    Double_baking
    (fun (balance_updates : Alpha_context.Receipt.balance_updates) ⇒
      Apply_results.Double_baking_evidence_result balance_updates)
    payload_producer.

Definition apply_contents_list
  (ctxt : Alpha_context.t) (chain_id : Chain_id.t) (mode : mode)
  (payload_producer : Alpha_context.Consensus_key.t)
  (contents_list : Alpha_context.contents_list)
  : M? (Alpha_context.context × Apply_results.contents_result_list) :=
  let mempool_mode :=
    match mode with
    | Partial_construction _ ⇒ true
    | (Full_construction _ | Application _) ⇒ false
    end in
  match contents_list with
  | Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
    record_preendorsement ctxt mode consensus_content
  | Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
    record_endorsement ctxt mode consensus_content
  | Alpha_context.Single (Alpha_context.Dal_attestation op) ⇒
    let? ctxt := Dal_apply.apply_attestation ctxt op in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Dal_attestation_result
            {|
              Apply_results.contents_result.Dal_attestation_result.delegate :=
                op.(Alpha_context.Dal.Attestation.operation.attestor); |})))
  |
    Alpha_context.Single
      (Alpha_context.Seed_nonce_revelation {|
        Alpha_context.contents.Seed_nonce_revelation.level := level;
          Alpha_context.contents.Seed_nonce_revelation.nonce := nonce_value
          |}) ⇒
    let? level := Alpha_context.Level.from_raw ctxt level in
    let? ctxt := Alpha_context.Nonce.reveal ctxt level nonce_value in
    let tip := Alpha_context.Constants.seed_nonce_revelation_tip ctxt in
    let contract :=
      Contract_repr.Implicit
        payload_producer.(Delegate_consensus_key.t.delegate) in
    let? '(ctxt, balance_updates) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_infinite
          Alpha_context.Token.Revelation_rewards)
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract contract)) tip in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Seed_nonce_revelation_result balance_updates)))
  |
    Alpha_context.Single
      (Alpha_context.Vdf_revelation {|
        Alpha_context.contents.Vdf_revelation.solution := solution |}) ⇒
    let? ctxt := Alpha_context.Seed.update_seed ctxt solution in
    let tip := Alpha_context.Constants.seed_nonce_revelation_tip ctxt in
    let contract :=
      Contract_repr.Implicit
        payload_producer.(Delegate_consensus_key.t.delegate) in
    let? '(ctxt, balance_updates) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_infinite
          Alpha_context.Token.Revelation_rewards)
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract contract)) tip in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Vdf_revelation_result balance_updates)))
  |
    Alpha_context.Single
      (Alpha_context.Double_preendorsement_evidence {|
        Alpha_context.contents.Double_preendorsement_evidence.op1 := op1;
          Alpha_context.contents.Double_preendorsement_evidence.op2 := _
          |}) ⇒
    punish_double_endorsement_or_preendorsement ctxt op1 payload_producer
  |
    Alpha_context.Single
      (Alpha_context.Double_endorsement_evidence {|
        Alpha_context.contents.Double_endorsement_evidence.op1 := op1;
          Alpha_context.contents.Double_endorsement_evidence.op2 := _
          |}) ⇒
    punish_double_endorsement_or_preendorsement ctxt op1 payload_producer
  |
    Alpha_context.Single
      (Alpha_context.Double_baking_evidence {|
        Alpha_context.contents.Double_baking_evidence.bh1 := bh1;
          Alpha_context.contents.Double_baking_evidence.bh2 := _
          |}) ⇒ punish_double_baking ctxt bh1 payload_producer
  |
    Alpha_context.Single
      (Alpha_context.Activate_account {|
        Alpha_context.contents.Activate_account.id := pkh;
          Alpha_context.contents.Activate_account.activation_code :=
            activation_code
          |}) ⇒
    let blinded_pkh :=
      Blinded_public_key_hash.of_ed25519_pkh activation_code pkh in
    let src := Alpha_context.Token.Collected_commitments blinded_pkh in
    let contract := Contract_repr.Implicit (Signature.Ed25519Hash pkh) in
    let? '(ctxt, amount) := Alpha_context.Token.balance ctxt src in
    let? '(ctxt, bupds) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_container src)
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract contract)) amount in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Activate_account_result bupds)))
  | Alpha_context.Single ((Alpha_context.Proposals _) as contents) ⇒
    Amendment.apply_proposals ctxt chain_id contents
  | Alpha_context.Single ((Alpha_context.Ballot _) as contents) ⇒
    Amendment.apply_ballot ctxt contents
  |
    Alpha_context.Single
      (Alpha_context.Drain_delegate {|
        Alpha_context.contents.Drain_delegate.consensus_key := _;
          Alpha_context.contents.Drain_delegate.delegate := delegate;
          Alpha_context.contents.Drain_delegate.destination := destination
          |}) ⇒
    let? '(ctxt, allocated_destination_contract, fees, drain_balance_updates) :=
      Alpha_context.Delegate.drain ctxt delegate destination in
    let? '(ctxt, fees_balance_updates) :=
      Alpha_context.Token.transfer None ctxt
        (Alpha_context.Token.Source_container
          (Alpha_context.Token.Contract (Contract_repr.Implicit delegate)))
        (Alpha_context.Token.Sink_container
          (Alpha_context.Token.Contract
            (Contract_repr.Implicit
              payload_producer.(Delegate_consensus_key.t.delegate)))) fees in
    let balance_updates :=
      Pervasives.op_at drain_balance_updates fees_balance_updates in
    return?
      (ctxt,
        (Apply_results.Single_result
          (Apply_results.Drain_delegate_result
            {|
              Apply_results.contents_result.Drain_delegate_result.balance_updates
                := balance_updates;
              Apply_results.contents_result.Drain_delegate_result.allocated_destination_contract
                := allocated_destination_contract; |})))
  | Alpha_context.Single (Alpha_context.Failing_noop _) ⇒
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Failing_noop_error" unit tt)
  | Alpha_context.Single (Alpha_context.Manager_operation _) ⇒
    apply_manager_operations ctxt payload_producer chain_id mempool_mode
      contents_list
  | Alpha_context.Cons (Alpha_context.Manager_operation _) _ ⇒
    apply_manager_operations ctxt payload_producer chain_id mempool_mode
      contents_list
  | _ ⇒ unreachable_gadt_branch
  end.

Definition apply_operation
  (application_state_value : application_state)
  (operation_hash : Operation_hash.t)
  (operation : Alpha_context.packed_operation)
  : M? (application_state × Apply_results.packed_operation_metadata) :=
  let apply_operation
    (application_state_value : application_state)
    (packed_operation : Alpha_context.packed_operation)
    (payload_producer : Alpha_context.Consensus_key.t)
    : M? (application_state × Apply_results.packed_operation_metadata) :=
    let '{|
      Alpha_context.packed_operation.shell := shell;
        Alpha_context.packed_operation.protocol_data :=
          Alpha_context.Operation_data unpacked_protocol_data
        |} := packed_operation in
    let operation :=
      {| Alpha_context.operation.shell := shell;
        Alpha_context.operation.protocol_data := unpacked_protocol_data; |} in
    let ctxt :=
      Alpha_context.Origination_nonce.init_value
        application_state_value.(application_state.ctxt) operation_hash in
    let ctxt := record_operation ctxt operation_hash operation in
    let? '(ctxt, result_value) :=
      apply_contents_list ctxt
        application_state_value.(application_state.chain_id)
        application_state_value.(application_state.mode) payload_producer
        operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
      in
    let ctxt := Alpha_context.Gas.set_unlimited ctxt in
    let ctxt := Alpha_context.Origination_nonce.unset ctxt in
    let op_count :=
      Pervasives.succ application_state_value.(application_state.op_count) in
    return?
      ((application_state.with_op_count op_count
        (application_state.with_ctxt ctxt application_state_value)),
        (Apply_results.Operation_metadata
          {| Apply_results.operation_metadata.contents := result_value; |})) in
  match application_state_value.(application_state.mode) with
  | Application {| mode.Application.payload_producer := payload_producer |} ⇒
    apply_operation application_state_value operation payload_producer
  |
    Full_construction {|
      mode.Full_construction.payload_producer := payload_producer |} ⇒
    apply_operation application_state_value operation payload_producer
  | Partial_construction _ ⇒
    apply_operation application_state_value operation
      Alpha_context.Consensus_key.zero
  end.

Definition may_start_new_cycle (ctxt : Alpha_context.context)
  : M?
    (Alpha_context.context × Alpha_context.Receipt.balance_updates ×
      list Alpha_context.public_key_hash) :=
  let? dawn := Alpha_context.Level.dawn_of_a_new_cycle ctxt in
  match dawn with
  | None ⇒ return? (ctxt, nil, nil)
  | Some last_cycle ⇒
    let? '(ctxt, balance_updates, deactivated) :=
      Alpha_context.Delegate.cycle_end ctxt last_cycle in
    let? ctxt := Alpha_context.Bootstrap.cycle_end ctxt last_cycle in
    return? (ctxt, balance_updates, deactivated)
  end.

Definition apply_liquidity_baking_subsidy
  (ctxt : Alpha_context.context)
  (toggle_vote : Alpha_context.Liquidity_baking.liquidity_baking_toggle_vote)
  : M?
    (Alpha_context.context ×
      list Apply_results.packed_successful_manager_operation_result ×
      Alpha_context.Liquidity_baking.Toggle_EMA.t) :=
  Alpha_context.Liquidity_baking.on_subsidy_allowed ctxt toggle_vote
    (fun (ctxt : Alpha_context.context) ⇒
      fun (liquidity_baking_cpmm_contract_hash : Contract_hash.t) ⇒
        let liquidity_baking_cpmm_contract :=
          Contract_repr.Originated liquidity_baking_cpmm_contract_hash in
        let ctxt :=
          Alpha_context.Gas.set_limit ctxt
            (Alpha_context.Gas.Arith.integral_exn
              ((Alpha_context.Gas.Arith.integral_to_z
                (Alpha_context.Constants.hard_gas_limit_per_block ctxt)) /Z
              (Z.of_int 20))) in
        let backtracking_ctxt := ctxt in
        let function_parameter :=
          let liquidity_baking_subsidy :=
            Alpha_context.Constants.liquidity_baking_subsidy ctxt in
          let? '(ctxt, balance_updates) :=
            Alpha_context.Token.transfer (Some Alpha_context.Receipt.Subsidy)
              ctxt
              (Alpha_context.Token.Source_infinite
                Alpha_context.Token.Liquidity_baking_subsidies)
              (Alpha_context.Token.Sink_container
                (Alpha_context.Token.Contract liquidity_baking_cpmm_contract))
              liquidity_baking_subsidy in
          let? '(ctxt, cache_key, script) :=
            Script_cache.find ctxt liquidity_baking_cpmm_contract_hash in
          match script with
          | None ⇒
            Error_monad.tzfail
              (Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
                Alpha_context.Entrypoint.default)
          | Some (script, script_ir) ⇒
            let? balance :=
              Alpha_context.Contract.get_balance ctxt
                liquidity_baking_cpmm_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 :=
                  liquidity_baking_cpmm_contract;
                Script_typed_ir.step_constants.payer :=
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero);
                Script_typed_ir.step_constants.self :=
                  liquidity_baking_cpmm_contract_hash;
                Script_typed_ir.step_constants.amount :=
                  liquidity_baking_subsidy;
                Script_typed_ir.step_constants.balance := balance;
                Script_typed_ir.step_constants.chain_id := Chain_id.zero;
                Script_typed_ir.step_constants.now := now;
                Script_typed_ir.step_constants.level := level; |} 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) :=
              Script_interpreter.execute_with_typed_parameter None ctxt
                (Some script_ir) Script_ir_unparser.Optimized step_constants
                script Alpha_context.Entrypoint.default Script_typed_ir.Unit_t
                Micheline.dummy_location tt false in
            match operations with
            | cons _ _ ⇒ return? (backtracking_ctxt, nil)
            | [] ⇒
              let? '(ticket_table_size_diff, ctxt) :=
                update_script_storage_and_ticket_balances ctxt
                  liquidity_baking_cpmm_contract_hash storage_value
                  lazy_storage_diff ticket_diffs operations in
              let? '(ctxt, new_size, paid_storage_size_diff) :=
                Alpha_context.Fees.record_paid_storage_space ctxt
                  liquidity_baking_cpmm_contract_hash in
              let? '(ticket_paid_storage_diff, ctxt) :=
                Alpha_context.Ticket_balance.adjust_storage_space ctxt
                  ticket_table_size_diff in
              let consumed_gas :=
                Alpha_context.Gas.consumed backtracking_ctxt 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_results.Transaction_result
                  (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
                        := nil;
                      Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
                        := consumed_gas;
                      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
                        := paid_storage_size_diff +Z ticket_paid_storage_diff;
                      Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                        := false; |}) in
              let ctxt := Alpha_context.Gas.set_unlimited ctxt in
              return?
                (ctxt, [ Apply_results.Successful_manager_result result_value ])
            end
          end in
        match function_parameter with
        | Pervasives.Ok (ctxt, results) ⇒ Pervasives.Ok (ctxt, results)
        | Pervasives.Error _ ⇒
          let ctxt := Alpha_context.Gas.set_unlimited backtracking_ctxt in
          Pervasives.Ok (ctxt, nil)
        end).

Definition are_endorsements_required
  (ctxt : Alpha_context.context) (level : Alpha_context.Raw_level.raw_level)
  : M? bool :=
  let? first_level := Alpha_context.First_level_of_protocol.get ctxt in
  let level_position_in_protocol :=
    Alpha_context.Raw_level.diff_value level first_level in
  return? (level_position_in_protocol >i32 1).

Definition record_endorsing_participation (ctxt : Alpha_context.context)
  : M? Alpha_context.context :=
  let validators := Alpha_context.Consensus.allowed_endorsements ctxt in
  Alpha_context.Slot.Map.(Map.S.fold_es)
    (fun (initial_slot : Alpha_context.Slot.t) ⇒
      fun (function_parameter : Alpha_context.Consensus_key.pk × int) ⇒
        let '(consensus_pk, power) := function_parameter in
        fun (ctxt : Alpha_context.context) ⇒
          let participation :=
            if
              Alpha_context.Slot._Set.(_Set.S.mem) initial_slot
                (Alpha_context.Consensus.endorsements_seen ctxt)
            then
              Alpha_context.Delegate.Participated
            else
              Alpha_context.Delegate.Didn't_participate in
          Alpha_context.Delegate.record_endorsing_participation ctxt
            consensus_pk.(Raw_context.consensus_pk.delegate) participation power)
    validators ctxt.

Definition begin_application
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (migration_balance_updates : Alpha_context.Receipt.balance_updates)
  (migration_operation_results : list Alpha_context.Migration.origination_result)
  (predecessor_fitness : Alpha_context.Fitness.raw)
  (block_header : Alpha_context.Block_header.t) : M? application_state :=
  let? fitness :=
    Alpha_context.Fitness.from_raw
      block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.fitness)
    in
  let level :=
    block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.level)
    in
  let? predecessor_round :=
    Alpha_context.Fitness.round_from_raw predecessor_fitness in
  let? predecessor_level := Alpha_context.Raw_level.of_int32 (Int32.pred level)
    in
  let? predecessor_level := Alpha_context.Level.from_raw ctxt predecessor_level
    in
  let round := Alpha_context.Fitness.round fitness in
  let current_level := Alpha_context.Level.current ctxt in
  let? '(ctxt, _slot, block_producer) :=
    Alpha_context.Stake_distribution.baking_rights_owner ctxt current_level
      round in
  let? '(ctxt, _slot, payload_producer) :=
    Alpha_context.Stake_distribution.baking_rights_owner ctxt current_level
      block_header.(Alpha_context.Block_header.t.protocol_data).(Alpha_context.Block_header.protocol_data.contents).(Alpha_context.Block_header.contents.payload_round)
    in
  let toggle_vote :=
    block_header.(Alpha_context.Block_header.t.protocol_data).(Alpha_context.Block_header.protocol_data.contents).(Alpha_context.Block_header.contents.liquidity_baking_toggle_vote)
    in
  let?
    '(ctxt, liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
    apply_liquidity_baking_subsidy ctxt toggle_vote in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_start_of_level ctxt in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_info_per_level ctxt
      block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.timestamp)
      block_header.(Alpha_context.Block_header.t.shell).(Block_header.shell_header.predecessor)
    in
  let mode :=
    Application
      {| mode.Application.block_header := block_header;
        mode.Application.fitness := fitness;
        mode.Application.payload_producer :=
          Alpha_context.Consensus_key.pkh payload_producer;
        mode.Application.block_producer :=
          Alpha_context.Consensus_key.pkh block_producer;
        mode.Application.predecessor_level := predecessor_level;
        mode.Application.predecessor_round := predecessor_round; |} in
  return?
    {| application_state.ctxt := ctxt; application_state.chain_id := chain_id;
      application_state.mode := mode; application_state.op_count := 0;
      application_state.migration_balance_updates := migration_balance_updates;
      application_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      application_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition begin_full_construction
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (migration_balance_updates : Alpha_context.Receipt.balance_updates)
  (migration_operation_results : list Alpha_context.Migration.origination_result)
  (predecessor_timestamp : Time.t) (predecessor_level : Alpha_context.Level.t)
  (predecessor_round : Alpha_context.Round.t) (predecessor_hash : Block_hash.t)
  (timestamp : Time.t)
  (block_data_contents : Alpha_context.Block_header.contents)
  : M? application_state :=
  let round_durations := Alpha_context.Constants.round_durations ctxt in
  let? round :=
    Alpha_context.Round.round_of_timestamp round_durations predecessor_timestamp
      predecessor_round timestamp in
  let current_level := Alpha_context.Level.current ctxt in
  let? '(ctxt, _slot, block_producer) :=
    Alpha_context.Stake_distribution.baking_rights_owner ctxt current_level
      round in
  let? '(ctxt, _slot, payload_producer) :=
    Alpha_context.Stake_distribution.baking_rights_owner ctxt current_level
      block_data_contents.(Alpha_context.Block_header.contents.payload_round) in
  let toggle_vote :=
    block_data_contents.(Alpha_context.Block_header.contents.liquidity_baking_toggle_vote)
    in
  let?
    '(ctxt, liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
    apply_liquidity_baking_subsidy ctxt toggle_vote in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_start_of_level ctxt in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_info_per_level ctxt timestamp
      predecessor_hash in
  let mode :=
    Full_construction
      {| mode.Full_construction.block_data_contents := block_data_contents;
        mode.Full_construction.predecessor_hash := predecessor_hash;
        mode.Full_construction.payload_producer :=
          Alpha_context.Consensus_key.pkh payload_producer;
        mode.Full_construction.block_producer :=
          Alpha_context.Consensus_key.pkh block_producer;
        mode.Full_construction.round := round;
        mode.Full_construction.predecessor_level := predecessor_level;
        mode.Full_construction.predecessor_round := predecessor_round; |} in
  return?
    {| application_state.ctxt := ctxt; application_state.chain_id := chain_id;
      application_state.mode := mode; application_state.op_count := 0;
      application_state.migration_balance_updates := migration_balance_updates;
      application_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      application_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition begin_partial_construction
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (migration_balance_updates : Alpha_context.Receipt.balance_updates)
  (migration_operation_results : list Alpha_context.Migration.origination_result)
  (predecessor_level : Alpha_context.Raw_level.t)
  (predecessor_timestamp : Alpha_context.Timestamp.time)
  (predecessor_hash : Block_hash.t)
  (predecessor_fitness : Alpha_context.Fitness.raw) : M? application_state :=
  let toggle_vote := Liquidity_baking_repr.LB_pass in
  let?
    '(ctxt, liquidity_baking_operations_results, liquidity_baking_toggle_ema) :=
    apply_liquidity_baking_subsidy ctxt toggle_vote in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_start_of_level ctxt in
  let? '(_inbox, _diff, ctxt) :=
    let minimal_block_delay := Alpha_context.Constants.minimal_block_delay ctxt
      in
    let? timestamp :=
      Alpha_context.Timestamp.op_plusquestion predecessor_timestamp
        minimal_block_delay in
    let predecessor := predecessor_hash in
    Alpha_context.Sc_rollup.Inbox.add_info_per_level ctxt timestamp predecessor
    in
  let mode :=
    Partial_construction
      {| mode.Partial_construction.predecessor_level := predecessor_level;
        mode.Partial_construction.predecessor_fitness := predecessor_fitness; |}
    in
  return?
    {| application_state.ctxt := ctxt; application_state.chain_id := chain_id;
      application_state.mode := mode; application_state.op_count := 0;
      application_state.migration_balance_updates := migration_balance_updates;
      application_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      application_state.implicit_operations_results :=
        Pervasives.op_at
          (Apply_results.pack_migration_operation_results
            migration_operation_results) liquidity_baking_operations_results; |}.

Definition finalize_application
  (ctxt : Alpha_context.context)
  (block_data_contents : Alpha_context.Block_header.contents)
  (round : Alpha_context.Round.t) (predecessor_hash : Block_hash.t)
  (liquidity_baking_toggle_ema : Alpha_context.Liquidity_baking.Toggle_EMA.t)
  (implicit_operations_results :
    list Apply_results.packed_successful_manager_operation_result)
  (migration_balance_updates :
    list
      (Alpha_context.Receipt.balance × Alpha_context.Receipt.balance_update ×
        Alpha_context.Receipt.update_origin))
  (block_producer : Alpha_context.Consensus_key.t)
  (payload_producer : Alpha_context.Consensus_key.t)
  : M? (Alpha_context.context × Apply_results.block_metadata) :=
  let level := Alpha_context.Level.current ctxt in
  let endorsing_power := Alpha_context.Consensus.current_endorsement_power ctxt
    in
  let? required_endorsements :=
    are_endorsements_required ctxt level.(Alpha_context.Level.t.level) in
  let block_payload_hash :=
    Alpha_context.Block_payload.hash_value predecessor_hash
      block_data_contents.(Alpha_context.Block_header.contents.payload_round)
      (Alpha_context.non_consensus_operations ctxt) in
  let level := Alpha_context.Level.current ctxt in
  let ctxt :=
    match Alpha_context.Consensus.endorsement_branch ctxt with
    | Some predecessor_branch ⇒
      Alpha_context.Consensus.store_grand_parent_branch ctxt predecessor_branch
    | None ⇒ ctxt
    end in
  let ctxt :=
    Alpha_context.Consensus.store_endorsement_branch ctxt
      (predecessor_hash, block_payload_hash) in
  let? ctxt := Alpha_context.Round.update ctxt round in
  let? ctxt :=
    match
      block_data_contents.(Alpha_context.Block_header.contents.seed_nonce_hash)
      with
    | None ⇒ return? ctxt
    | Some nonce_hash ⇒
      Alpha_context.Nonce.record_hash ctxt
        {| Storage.Cycle.unrevealed_nonce.nonce_hash := nonce_hash;
          Storage.Cycle.unrevealed_nonce.delegate :=
            block_producer.(Delegate_consensus_key.t.delegate); |}
    end in
  let? '(ctxt, reward_bonus) :=
    if required_endorsements then
      let? ctxt := record_endorsing_participation ctxt in
      let? rewards_bonus := Baking.bonus_baking_reward ctxt endorsing_power in
      return? (ctxt, (Some rewards_bonus))
    else
      return? (ctxt, None) in
  let baking_reward := Alpha_context.Constants.baking_reward_fixed_portion ctxt
    in
  let? '(ctxt, baking_receipts) :=
    Alpha_context.Delegate.record_baking_activity_and_pay_rewards_and_fees ctxt
      payload_producer.(Delegate_consensus_key.t.delegate)
      block_producer.(Delegate_consensus_key.t.delegate) baking_reward
      reward_bonus in
  let? ctxt :=
    if Alpha_context.Level.may_compute_randao ctxt then
      Alpha_context.Seed.compute_randao ctxt
    else
      return? ctxt in
  let? ctxt :=
    if Alpha_context.Level.may_snapshot_stake_distribution ctxt then
      Alpha_context.Stake_distribution.snapshot_value ctxt
    else
      return? ctxt in
  let? '(ctxt, cycle_end_balance_updates, deactivated) :=
    may_start_new_cycle ctxt in
  let? ctxt := Amendment.may_start_new_voting_period ctxt in
  let? '(ctxt, dal_attestation) := Dal_apply.finalisation ctxt in
  let? '(_inbox, _diff, ctxt) :=
    Alpha_context.Sc_rollup.Inbox.add_end_of_level ctxt in
  let balance_updates :=
    Pervasives.op_at migration_balance_updates
      (Pervasives.op_at baking_receipts cycle_end_balance_updates) in
  let consumed_gas :=
    Alpha_context.Gas.Arith.sub
      (Alpha_context.Gas.Arith.fp_value
        (Alpha_context.Constants.hard_gas_limit_per_block ctxt))
      (Alpha_context.Gas.block_level ctxt) in
  Error_monad.Lwt_result_syntax.op_letplus
    (Alpha_context.Voting_period.get_rpc_current_info ctxt)
    (fun voting_period_info ⇒
      let receipt :=
        {| Apply_results.block_metadata.proposer := payload_producer;
          Apply_results.block_metadata.baker := block_producer;
          Apply_results.block_metadata.level_info := level;
          Apply_results.block_metadata.voting_period_info := voting_period_info;
          Apply_results.block_metadata.nonce_hash :=
            block_data_contents.(Alpha_context.Block_header.contents.seed_nonce_hash);
          Apply_results.block_metadata.consumed_gas := consumed_gas;
          Apply_results.block_metadata.deactivated := deactivated;
          Apply_results.block_metadata.balance_updates := balance_updates;
          Apply_results.block_metadata.liquidity_baking_toggle_ema :=
            liquidity_baking_toggle_ema;
          Apply_results.block_metadata.implicit_operations_results :=
            implicit_operations_results;
          Apply_results.block_metadata.dal_attestation := dal_attestation; |} in
      (ctxt, receipt)).

Init function; without side-effects in Coq

Definition init_module2 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "apply.missing_shell_header"
    "Missing shell_header during finalisation of a block"
    "During finalisation of a block header in Application mode or Full construction mode, a shell header should be provided so that a cache nonce can be computed."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "No shell header provided during the finalisation of a block."
                CamlinternalFormatBasics.End_of_format)
              "No shell header provided during the finalisation of a block.")))
    Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Missing_shell_header" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Missing_shell_header" unit tt).

Definition finalize_with_commit_message
  (ctxt : Alpha_context.context) (cache_nonce : Alpha_context.Cache.cache_nonce)
  (fitness : Alpha_context.Fitness.t) (round : Alpha_context.Round.t)
  (op_count : int) : M? Updater.validation_result :=
  let ctxt := Alpha_context.Cache.Admin.sync ctxt cache_nonce in
  let raw_level :=
    Alpha_context.Raw_level.to_int32
      (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level) in
  let commit_message :=
    Format.asprintf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "lvl "
          (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.String_literal ", fit:"
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.String_literal ", round "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", "
                      (CamlinternalFormatBasics.Int
                        CamlinternalFormatBasics.Int_d
                        CamlinternalFormatBasics.No_padding
                        CamlinternalFormatBasics.No_precision
                        (CamlinternalFormatBasics.String_literal " ops"
                          CamlinternalFormatBasics.End_of_format)))))))))
        "lvl %ld, fit:%a, round %a, %d ops") raw_level Alpha_context.Fitness.pp
      fitness Alpha_context.Round.pp round op_count in
  let? validation_result :=
    Alpha_context.finalize (Some commit_message) ctxt
      (Alpha_context.Fitness.to_raw fitness) in
  return? validation_result.

Definition finalize_block
  (application_state_value : application_state)
  (shell_header_opt : option Alpha_context.Block_header.shell_header)
  : M? (Updater.validation_result × Apply_results.block_metadata) :=
  let '{|
    application_state.ctxt := ctxt;
      application_state.op_count := op_count;
      application_state.migration_balance_updates := migration_balance_updates;
      application_state.liquidity_baking_toggle_ema :=
        liquidity_baking_toggle_ema;
      application_state.implicit_operations_results :=
        implicit_operations_results
      |} := application_state_value in
  match application_state_value.(application_state.mode) with
  |
    Full_construction {|
      mode.Full_construction.block_data_contents := block_data_contents;
        mode.Full_construction.predecessor_hash := predecessor_hash;
        mode.Full_construction.payload_producer := payload_producer;
        mode.Full_construction.block_producer := block_producer;
        mode.Full_construction.round := round;
        mode.Full_construction.predecessor_level := _;
        mode.Full_construction.predecessor_round := predecessor_round
        |} ⇒
    let? 'shell_header :=
      Option.value_e shell_header_opt
        (Error_monad.trace_of_error
          (Build_extensible "Missing_shell_header" unit tt)) in
    let cache_nonce :=
      Alpha_context.Cache.cache_nonce_from_block_header shell_header
        block_data_contents in
    let locked_round_evidence :=
      Option.map
        (fun (function_parameter : Alpha_context.Round.t × int) ⇒
          let '(preendorsement_round, preendorsement_count) :=
            function_parameter in
          {|
            Alpha_context.Block_header.locked_round_evidence.preendorsement_round
              := preendorsement_round;
            Alpha_context.Block_header.locked_round_evidence.preendorsement_count
              := preendorsement_count; |})
        (Alpha_context.Consensus.locked_round_evidence ctxt) in
    let locked_round :=
      match locked_round_evidence with
      | None ⇒ None
      |
        Some {|
          Alpha_context.Block_header.locked_round_evidence.preendorsement_round :=
            preendorsement_round
            |} ⇒ Some preendorsement_round
      end in
    let level :=
      (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level) in
    let? fitness :=
      Alpha_context.Fitness.create level locked_round predecessor_round round in
    let? '(ctxt, receipt) :=
      finalize_application ctxt block_data_contents round predecessor_hash
        liquidity_baking_toggle_ema implicit_operations_results
        migration_balance_updates block_producer payload_producer in
    let? result_value :=
      finalize_with_commit_message ctxt cache_nonce fitness round op_count in
    return? (result_value, receipt)
  |
    Partial_construction {|
      mode.Partial_construction.predecessor_fitness := predecessor_fitness
        |} ⇒
    let? voting_period_info :=
      Alpha_context.Voting_period.get_rpc_current_info ctxt in
    let level_info := Alpha_context.Level.current ctxt in
    let? result_value := Alpha_context.finalize None ctxt predecessor_fitness in
    return?
      (result_value,
        {|
          Apply_results.block_metadata.proposer :=
            Alpha_context.Consensus_key.zero;
          Apply_results.block_metadata.baker :=
            Alpha_context.Consensus_key.zero;
          Apply_results.block_metadata.level_info := level_info;
          Apply_results.block_metadata.voting_period_info := voting_period_info;
          Apply_results.block_metadata.nonce_hash := None;
          Apply_results.block_metadata.consumed_gas :=
            Alpha_context.Gas.Arith.zero;
          Apply_results.block_metadata.deactivated := nil;
          Apply_results.block_metadata.balance_updates :=
            migration_balance_updates;
          Apply_results.block_metadata.liquidity_baking_toggle_ema :=
            liquidity_baking_toggle_ema;
          Apply_results.block_metadata.implicit_operations_results :=
            implicit_operations_results;
          Apply_results.block_metadata.dal_attestation := None; |})
  |
    Application {|
      mode.Application.block_header := {|
        Alpha_context.Block_header.t.shell := shell;
          Alpha_context.Block_header.t.protocol_data := protocol_data
          |};
        mode.Application.fitness := fitness;
        mode.Application.payload_producer := payload_producer;
        mode.Application.block_producer := block_producer
        |} ⇒
    let round := Alpha_context.Fitness.round fitness in
    let cache_nonce :=
      Alpha_context.Cache.cache_nonce_from_block_header shell
        protocol_data.(Alpha_context.Block_header.protocol_data.contents) in
    let? '(ctxt, receipt) :=
      finalize_application ctxt
        protocol_data.(Alpha_context.Block_header.protocol_data.contents) round
        shell.(Block_header.shell_header.predecessor)
        liquidity_baking_toggle_ema implicit_operations_results
        migration_balance_updates block_producer payload_producer in
    let? result_value :=
      finalize_with_commit_message ctxt cache_nonce fitness round op_count in
    return? (result_value, receipt)
  end.

Definition value_of_key
  (ctxt : Alpha_context.context) (k_value : Context.cache_key)
  : M? Context.cache_value :=
  Alpha_context.Cache.Admin.value_of_key ctxt k_value.