Skip to main content

🏗️ Apply.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
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.Cache_memory_helpers.
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.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_interpreter.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Ticket_accounting.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.

Inductive denunciation_kind : Set :=
| Preendorsement : denunciation_kind
| Endorsement : denunciation_kind
| Block : denunciation_kind.

Definition denunciation_kind_encoding
  : Data_encoding.encoding denunciation_kind :=
  Data_encoding.string_enum
    [
      ("preendorsement", Preendorsement);
      ("endorsement", Endorsement);
      ("block", Block)
    ].

Definition pp_denunciation_kind
  (fmt : Format.formatter) (function_parameter : denunciation_kind) : unit :=
  match function_parameter with
  | Preendorsement
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "preendorsement"
          CamlinternalFormatBasics.End_of_format) "preendorsement")
  | Endorsement
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "endorsement"
          CamlinternalFormatBasics.End_of_format) "endorsement")
  | Block
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "baking"
          CamlinternalFormatBasics.End_of_format) "baking")
  end.

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 Invalid_double_baking_evidence.
  Record record : Set := Build {
    hash1 : Block_hash.t;
    level1 : Alpha_context.Raw_level.t;
    round1 : Alpha_context.Round.t;
    hash2 : Block_hash.t;
    level2 : Alpha_context.Raw_level.t;
    round2 : Alpha_context.Round.t;
  }.
  Definition with_hash1 hash1 (r : record) :=
    Build hash1 r.(level1) r.(round1) r.(hash2) r.(level2) r.(round2).
  Definition with_level1 level1 (r : record) :=
    Build r.(hash1) level1 r.(round1) r.(hash2) r.(level2) r.(round2).
  Definition with_round1 round1 (r : record) :=
    Build r.(hash1) r.(level1) round1 r.(hash2) r.(level2) r.(round2).
  Definition with_hash2 hash2 (r : record) :=
    Build r.(hash1) r.(level1) r.(round1) hash2 r.(level2) r.(round2).
  Definition with_level2 level2 (r : record) :=
    Build r.(hash1) r.(level1) r.(round1) r.(hash2) level2 r.(round2).
  Definition with_round2 round2 (r : record) :=
    Build r.(hash1) r.(level1) r.(round1) r.(hash2) r.(level2) round2.
End Invalid_double_baking_evidence.
Definition Invalid_double_baking_evidence :=
  Invalid_double_baking_evidence.record.

Module Wrong_level_for_consensus_operation.
  Record record : Set := Build {
    expected : Alpha_context.Raw_level.t;
    provided : Alpha_context.Raw_level.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Wrong_level_for_consensus_operation.
Definition Wrong_level_for_consensus_operation :=
  Wrong_level_for_consensus_operation.record.

Module Wrong_round_for_consensus_operation.
  Record record : Set := Build {
    expected : Alpha_context.Round.t;
    provided : Alpha_context.Round.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Wrong_round_for_consensus_operation.
Definition Wrong_round_for_consensus_operation :=
  Wrong_round_for_consensus_operation.record.

Module Preendorsement_round_too_high.
  Record record : Set := Build {
    block_round : Alpha_context.Round.t;
    provided : Alpha_context.Round.t;
  }.
  Definition with_block_round block_round (r : record) :=
    Build block_round r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(block_round) provided.
End Preendorsement_round_too_high.
Definition Preendorsement_round_too_high :=
  Preendorsement_round_too_high.record.

Module Wrong_payload_hash_for_consensus_operation.
  Record record : Set := Build {
    expected : Block_payload_hash.t;
    provided : Block_payload_hash.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Wrong_payload_hash_for_consensus_operation.
Definition Wrong_payload_hash_for_consensus_operation :=
  Wrong_payload_hash_for_consensus_operation.record.

Module Consensus_operation_for_future_level.
  Record record : Set := Build {
    expected : Alpha_context.Raw_level.t;
    provided : Alpha_context.Raw_level.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Consensus_operation_for_future_level.
Definition Consensus_operation_for_future_level :=
  Consensus_operation_for_future_level.record.

Module Consensus_operation_for_future_round.
  Record record : Set := Build {
    expected : Alpha_context.Round.t;
    provided : Alpha_context.Round.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Consensus_operation_for_future_round.
Definition Consensus_operation_for_future_round :=
  Consensus_operation_for_future_round.record.

Module Consensus_operation_for_old_level.
  Record record : Set := Build {
    expected : Alpha_context.Raw_level.t;
    provided : Alpha_context.Raw_level.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Consensus_operation_for_old_level.
Definition Consensus_operation_for_old_level :=
  Consensus_operation_for_old_level.record.

Module Consensus_operation_for_old_round.
  Record record : Set := Build {
    expected : Alpha_context.Round.t;
    provided : Alpha_context.Round.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Consensus_operation_for_old_round.
Definition Consensus_operation_for_old_round :=
  Consensus_operation_for_old_round.record.

Module Consensus_operation_on_competing_proposal.
  Record record : Set := Build {
    expected : Block_payload_hash.t;
    provided : Block_payload_hash.t;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Consensus_operation_on_competing_proposal.
Definition Consensus_operation_on_competing_proposal :=
  Consensus_operation_on_competing_proposal.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.

Module Wrong_voting_period.
  Record record : Set := Build {
    expected : int32;
    provided : int32;
  }.
  Definition with_expected expected (r : record) :=
    Build expected r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(expected) provided.
End Wrong_voting_period.
Definition Wrong_voting_period := Wrong_voting_period.record.

Module Inconsistent_denunciation.
  Record record : Set := Build {
    kind : denunciation_kind;
    delegate1 : Signature.public_key_hash;
    delegate2 : Signature.public_key_hash;
  }.
  Definition with_kind kind (r : record) :=
    Build kind r.(delegate1) r.(delegate2).
  Definition with_delegate1 delegate1 (r : record) :=
    Build r.(kind) delegate1 r.(delegate2).
  Definition with_delegate2 delegate2 (r : record) :=
    Build r.(kind) r.(delegate1) delegate2.
End Inconsistent_denunciation.
Definition Inconsistent_denunciation := Inconsistent_denunciation.record.

Module Too_early_denunciation.
  Record record : Set := Build {
    kind : denunciation_kind;
    level : Alpha_context.Raw_level.t;
    current : Alpha_context.Raw_level.t;
  }.
  Definition with_kind kind (r : record) :=
    Build kind r.(level) r.(current).
  Definition with_level level (r : record) :=
    Build r.(kind) level r.(current).
  Definition with_current current (r : record) :=
    Build r.(kind) r.(level) current.
End Too_early_denunciation.
Definition Too_early_denunciation := Too_early_denunciation.record.

Module Outdated_denunciation.
  Record record : Set := Build {
    kind : denunciation_kind;
    level : Alpha_context.Raw_level.t;
    last_cycle : Alpha_context.Cycle.t;
  }.
  Definition with_kind kind (r : record) :=
    Build kind r.(level) r.(last_cycle).
  Definition with_level level (r : record) :=
    Build r.(kind) level r.(last_cycle).
  Definition with_last_cycle last_cycle (r : record) :=
    Build r.(kind) r.(level) last_cycle.
End Outdated_denunciation.
Definition Outdated_denunciation := Outdated_denunciation.record.

Module Invalid_activation.
  Record record : Set := Build {
    pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
  }.
  Definition with_pkh pkh (r : record) :=
    Build pkh.
End Invalid_activation.
Definition Invalid_activation := Invalid_activation.record.

Init function; without side-effects in Coq
Definition init_module1 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operations.wrong_slot" "Wrong slot" "wrong slot"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "wrong slot"
                  CamlinternalFormatBasics.End_of_format) "wrong slot")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_slot_used_for_consensus_operation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Wrong_slot_used_for_consensus_operation" unit tt) in
  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 '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.wrong_consensus_operation_branch"
      "Wrong consensus operation branch"
      "Trying to include an endorsement or preendorsement which points to the wrong block.\n It should be the predecessor for preendorsements and the grandfather for endorsements."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
            let '(e_value, p_value) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Wrong branch "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", expected "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "Wrong branch %a, expected %a") Block_hash.pp p_value
              Block_hash.pp e_value))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Block_hash.encoding)
        (Data_encoding.req None None "provided" Block_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_consensus_operation_branch" then
            let '(e_value, p_value) :=
              cast (Block_hash.t × Block_hash.t) payload in
            Some (e_value, p_value)
          else None
        end)
      (fun (function_parameter : Block_hash.t × Block_hash.t) ⇒
        let '(e_value, p_value) := function_parameter in
        Build_extensible "Wrong_consensus_operation_branch"
          (Block_hash.t × Block_hash.t) (e_value, p_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block.invalid_double_baking_evidence" "Invalid double baking evidence"
      "A double-baking evidence is inconsistent (two distinct level)"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Block_hash.t × Alpha_context.Raw_level.raw_level ×
              Alpha_context.Round.t × Block_hash.t ×
              Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
            let '(hash1, level1, round1, hash2, level2, round2) :=
              function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid double-baking evidence (hash: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " and "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          ", levels/rounds: ("
                          (CamlinternalFormatBasics.Int32
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            (CamlinternalFormatBasics.Char_literal "," % char
                              (CamlinternalFormatBasics.Int32
                                CamlinternalFormatBasics.Int_d
                                CamlinternalFormatBasics.No_padding
                                CamlinternalFormatBasics.No_precision
                                (CamlinternalFormatBasics.String_literal
                                  ") and ("
                                  (CamlinternalFormatBasics.Int32
                                    CamlinternalFormatBasics.Int_d
                                    CamlinternalFormatBasics.No_padding
                                    CamlinternalFormatBasics.No_precision
                                    (CamlinternalFormatBasics.Char_literal
                                      "," % char
                                      (CamlinternalFormatBasics.Int32
                                        CamlinternalFormatBasics.Int_d
                                        CamlinternalFormatBasics.No_padding
                                        CamlinternalFormatBasics.No_precision
                                        (CamlinternalFormatBasics.String_literal
                                          "))"
                                          CamlinternalFormatBasics.End_of_format)))))))))))))
                "Invalid double-baking evidence (hash: %a and %a, levels/rounds: (%ld,%ld) and (%ld,%ld))")
              Block_hash.pp hash1 Block_hash.pp hash2
              (Alpha_context.Raw_level.to_int32 level1)
              (Alpha_context.Round.to_int32 round1)
              (Alpha_context.Raw_level.to_int32 level2)
              (Alpha_context.Round.to_int32 round2)))
      (Data_encoding.obj6
        (Data_encoding.req None None "hash1" Block_hash.encoding)
        (Data_encoding.req None None "level1" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "round1" Alpha_context.Round.encoding)
        (Data_encoding.req None None "hash2" Block_hash.encoding)
        (Data_encoding.req None None "level2" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "round2" Alpha_context.Round.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_double_baking_evidence" then
            let '{|
              Invalid_double_baking_evidence.hash1 := hash1;
                Invalid_double_baking_evidence.level1 := level1;
                Invalid_double_baking_evidence.round1 := round1;
                Invalid_double_baking_evidence.hash2 := hash2;
                Invalid_double_baking_evidence.level2 := level2;
                Invalid_double_baking_evidence.round2 := round2
                |} := cast Invalid_double_baking_evidence payload in
            Some (hash1, level1, round1, hash2, level2, round2)
          else None
        end)
      (fun (function_parameter :
        Block_hash.t × Alpha_context.Raw_level.raw_level × Alpha_context.Round.t
          × Block_hash.t × Alpha_context.Raw_level.raw_level ×
          Alpha_context.Round.t) ⇒
        let '(hash1, level1, round1, hash2, level2, round2) :=
          function_parameter in
        Build_extensible "Invalid_double_baking_evidence"
          Invalid_double_baking_evidence
          {| Invalid_double_baking_evidence.hash1 := hash1;
            Invalid_double_baking_evidence.level1 := level1;
            Invalid_double_baking_evidence.round1 := round1;
            Invalid_double_baking_evidence.hash2 := hash2;
            Invalid_double_baking_evidence.level2 := level2;
            Invalid_double_baking_evidence.round2 := round2; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "wrong_level_for_consensus_operation"
      "Wrong level for consensus operation"
      "Wrong level for consensus operation."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Wrong level for consensus operation (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Wrong level for consensus operation (expected: %a, provided: %a).")
              Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_level_for_consensus_operation" then
            let '{|
              Wrong_level_for_consensus_operation.expected := expected;
                Wrong_level_for_consensus_operation.provided := provided
                |} := cast Wrong_level_for_consensus_operation payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Wrong_level_for_consensus_operation"
          Wrong_level_for_consensus_operation
          {| Wrong_level_for_consensus_operation.expected := expected;
            Wrong_level_for_consensus_operation.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "wrong_round_for_consensus_operation"
      "Wrong round for consensus operation"
      "Wrong round for consensus operation."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Round.t × Alpha_context.Round.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Wrong round for consensus operation (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Wrong round for consensus operation (expected: %a, provided: %a).")
              Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Alpha_context.Round.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Round.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_round_for_consensus_operation" then
            let '{|
              Wrong_round_for_consensus_operation.expected := expected;
                Wrong_round_for_consensus_operation.provided := provided
                |} := cast Wrong_round_for_consensus_operation payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
        ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Wrong_round_for_consensus_operation"
          Wrong_round_for_consensus_operation
          {| Wrong_round_for_consensus_operation.expected := expected;
            Wrong_round_for_consensus_operation.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "preendorsement_round_too_high" "Preendorsement round too high"
      "Preendorsement round too high."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Round.t × Alpha_context.Round.t) ⇒
            let '(block_round, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Preendorsement round too high (block_round: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Preendorsement round too high (block_round: %a, provided: %a).")
              Alpha_context.Round.pp block_round Alpha_context.Round.pp provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "block_round" Alpha_context.Round.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Round.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Preendorsement_round_too_high" then
            let '{|
              Preendorsement_round_too_high.block_round := block_round;
                Preendorsement_round_too_high.provided := provided
                |} := cast Preendorsement_round_too_high payload in
            Some (block_round, provided)
          else None
        end)
      (fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
        ⇒
        let '(block_round, provided) := function_parameter in
        Build_extensible "Preendorsement_round_too_high"
          Preendorsement_round_too_high
          {| Preendorsement_round_too_high.block_round := block_round;
            Preendorsement_round_too_high.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "wrong_payload_hash_for_consensus_operation"
      "Wrong payload hash for consensus operation"
      "Wrong payload hash for consensus operation."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
            ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Wrong payload hash for consensus operation (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Wrong payload hash for consensus operation (expected: %a, provided: %a).")
              Block_payload_hash.pp_short expected Block_payload_hash.pp_short
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Block_payload_hash.encoding)
        (Data_encoding.req None None "provided" Block_payload_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_payload_hash_for_consensus_operation" then
            let '{|
              Wrong_payload_hash_for_consensus_operation.expected := expected;
                Wrong_payload_hash_for_consensus_operation.provided := provided
                |} := cast Wrong_payload_hash_for_consensus_operation payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Wrong_payload_hash_for_consensus_operation"
          Wrong_payload_hash_for_consensus_operation
          {| Wrong_payload_hash_for_consensus_operation.expected := expected;
            Wrong_payload_hash_for_consensus_operation.provided := provided; |})
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "unexpected_endorsement_in_block" "Unexpected endorsement in block"
      "Unexpected endorsement in block."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Unexpected endorsement in block."
                  CamlinternalFormatBasics.End_of_format)
                "Unexpected endorsement in block."))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unexpected_endorsement_in_block" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unexpected_endorsement_in_block" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "unexpected_preendorsement_in_block" "Unexpected preendorsement in block"
      "Unexpected preendorsement in block."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Unexpected preendorsement in block."
                  CamlinternalFormatBasics.End_of_format)
                "Unexpected preendorsement in block."))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unexpected_preendorsement_in_block" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unexpected_preendorsement_in_block" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "consensus_operation_for_future_level"
      "Consensus operation for future level"
      "Consensus operation for future level."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Consensus operation for future level\n (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Consensus operation for future level\n (expected: %a, provided: %a).")
              Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Consensus_operation_for_future_level" then
            let '{|
              Consensus_operation_for_future_level.expected := expected;
                Consensus_operation_for_future_level.provided := provided
                |} := cast Consensus_operation_for_future_level payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Consensus_operation_for_future_level"
          Consensus_operation_for_future_level
          {| Consensus_operation_for_future_level.expected := expected;
            Consensus_operation_for_future_level.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "consensus_operation_for_future_round"
      "Consensus operation for future round"
      "Consensus operation for future round."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Round.t × Alpha_context.Round.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Consensus operation for future round (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Consensus operation for future round (expected: %a, provided: %a).")
              Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected_max" Alpha_context.Round.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Round.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Consensus_operation_for_future_round" then
            let '{|
              Consensus_operation_for_future_round.expected := expected;
                Consensus_operation_for_future_round.provided := provided
                |} := cast Consensus_operation_for_future_round payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
        ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Consensus_operation_for_future_round"
          Consensus_operation_for_future_round
          {| Consensus_operation_for_future_round.expected := expected;
            Consensus_operation_for_future_round.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Outdated
      "consensus_operation_for_old_level" "Consensus operation for old level"
      "Consensus operation for old level."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Consensus operation for old level (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Consensus operation for old level (expected: %a, provided: %a).")
              Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Raw_level.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Consensus_operation_for_old_level" then
            let '{|
              Consensus_operation_for_old_level.expected := expected;
                Consensus_operation_for_old_level.provided := provided
                |} := cast Consensus_operation_for_old_level payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter :
        Alpha_context.Raw_level.t × Alpha_context.Raw_level.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Consensus_operation_for_old_level"
          Consensus_operation_for_old_level
          {| Consensus_operation_for_old_level.expected := expected;
            Consensus_operation_for_old_level.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "consensus_operation_for_old_round" "Consensus operation for old round"
      "Consensus operation for old round."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Alpha_context.Round.t × Alpha_context.Round.t) ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Consensus operation for old round (expected_min: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Consensus operation for old round (expected_min: %a, provided: %a).")
              Alpha_context.Round.pp expected Alpha_context.Round.pp provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected_min" Alpha_context.Round.encoding)
        (Data_encoding.req None None "provided" Alpha_context.Round.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Consensus_operation_for_old_round" then
            let '{|
              Consensus_operation_for_old_round.expected := expected;
                Consensus_operation_for_old_round.provided := provided
                |} := cast Consensus_operation_for_old_round payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Alpha_context.Round.t × Alpha_context.Round.t)
        ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Consensus_operation_for_old_round"
          Consensus_operation_for_old_round
          {| Consensus_operation_for_old_round.expected := expected;
            Consensus_operation_for_old_round.provided := provided; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "consensus_operation_on_competing_proposal"
      "Consensus operation on competing proposal"
      "Consensus operation on competing proposal."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t)
            ⇒
            let '(expected, provided) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Consensus operation on competing proposal (expected: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", provided: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ")."
                          CamlinternalFormatBasics.End_of_format)))))
                "Consensus operation on competing proposal (expected: %a, provided: %a).")
              Block_payload_hash.pp_short expected Block_payload_hash.pp_short
              provided))
      (Data_encoding.obj2
        (Data_encoding.req None None "expected" Block_payload_hash.encoding)
        (Data_encoding.req None None "provided" Block_payload_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Consensus_operation_on_competing_proposal" then
            let '{|
              Consensus_operation_on_competing_proposal.expected := expected;
                Consensus_operation_on_competing_proposal.provided := provided
                |} := cast Consensus_operation_on_competing_proposal payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : Block_payload_hash.t × Block_payload_hash.t) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Consensus_operation_on_competing_proposal"
          Consensus_operation_on_competing_proposal
          {| Consensus_operation_on_competing_proposal.expected := expected;
            Consensus_operation_on_competing_proposal.provided := provided; |})
    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_monad.register_error_kind Error_monad.Branch
      "contract.empty_transaction" "Empty transaction"
      "Forbidden to credit 0\234\156\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\234\156\169 towards a contract without code are forbidden ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ")."
                      CamlinternalFormatBasics.End_of_format)))
                "Transactions of 0\234\156\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_amount"
      "Transaction amount to a transaction rollup must be zero"
      "Because transaction rollups are outside of the delegation mechanism of Tezos, they cannot own Tez, and therefore transactions targeting a transaction rollup must have its amount field set to zero."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Transaction amount to a transaction rollup must be zero."
                  CamlinternalFormatBasics.End_of_format)
                "Transaction amount to a transaction rollup must be zero.")))
      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_amount" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.cannot_transfer_ticket_to_implicit"
      "Cannot transfer ticket to implicit account"
      "Cannot transfer ticket to implicit account" None Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Cannot_transfer_ticket_to_implicit" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Cannot_transfer_ticket_to_implicit" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.tx_rollup_non_internal_transaction"
      "Non-internal transaction to a transaction rollup"
      "Non-internal transactions to a tx rollup are forbidden."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Transaction to a transaction rollup must be internal."
                  CamlinternalFormatBasics.End_of_format)
                "Transaction to a transaction rollup must be internal.")))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Tx_rollup_non_internal_transaction" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Tx_rollup_non_internal_transaction" 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
      "operation.inconsistent_counters" "Inconsistent counters in operation"
      "Inconsistent counters in operation. Counters of an operation must be successive."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Inconsistent counters in operation. Counters of an operation must be successive."
                  CamlinternalFormatBasics.End_of_format)
                "Inconsistent counters in operation. Counters of an operation must be successive.")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inconsistent_counters" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Inconsistent_counters" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.wrong_voting_period" "Wrong voting period"
      "Trying to include a proposal or ballot meant for another voting period"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : int32 × int32) ⇒
            let '(e_value, p_value) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Wrong voting period "
                  (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal ", current is "
                      (CamlinternalFormatBasics.Int32
                        CamlinternalFormatBasics.Int_d
                        CamlinternalFormatBasics.No_padding
                        CamlinternalFormatBasics.No_precision
                        CamlinternalFormatBasics.End_of_format))))
                "Wrong voting period %ld, current is %ld") p_value e_value))
      (Data_encoding.obj2
        (Data_encoding.req None None "current_index" Data_encoding.int32_value)
        (Data_encoding.req None None "provided_index" Data_encoding.int32_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_voting_period" then
            let '{|
              Wrong_voting_period.expected := expected;
                Wrong_voting_period.provided := provided
                |} := cast Wrong_voting_period payload in
            Some (expected, provided)
          else None
        end)
      (fun (function_parameter : int32 × int32) ⇒
        let '(expected, provided) := function_parameter in
        Build_extensible "Wrong_voting_period" Wrong_voting_period
          {| Wrong_voting_period.expected := expected;
            Wrong_voting_period.provided := provided; |}) 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_results.packed_internal_contents) ⇒
            let
              'Apply_results.Internal_contents {|
                Apply_results.internal_contents.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_results.internal_contents_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_results.packed_internal_contents payload in
            Some op
          else None
        end)
      (fun (op : Apply_results.packed_internal_contents) ⇒
        Build_extensible "Internal_operation_replay"
          Apply_results.packed_internal_contents op) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block.invalid_denunciation" "Invalid denunciation"
      "A denunciation is malformed"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (kind_value : denunciation_kind) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Malformed double-"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " evidence"
                      CamlinternalFormatBasics.End_of_format)))
                "Malformed double-%a evidence") pp_denunciation_kind kind_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "kind" denunciation_kind_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_denunciation" then
            let kind_value := cast denunciation_kind payload in
            Some kind_value
          else None
        end)
      (fun (kind_value : denunciation_kind) ⇒
        Build_extensible "Invalid_denunciation" denunciation_kind kind_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block.inconsistent_denunciation" "Inconsistent denunciation"
      "A denunciation operation is inconsistent (two distinct delegates)"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            denunciation_kind × Signature.public_key_hash ×
              Signature.public_key_hash) ⇒
            let '(kind_value, delegate1, delegate2) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Inconsistent double-"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " evidence (distinct delegate: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal " and "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ")" % char
                              CamlinternalFormatBasics.End_of_format)))))))
                "Inconsistent double-%a evidence (distinct delegate: %a and %a)")
              pp_denunciation_kind kind_value
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
              delegate1
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
              delegate2))
      (Data_encoding.obj3
        (Data_encoding.req None None "kind" denunciation_kind_encoding)
        (Data_encoding.req None None "delegate1"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
        (Data_encoding.req None None "delegate2"
          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 "Inconsistent_denunciation" then
            let '{|
              Inconsistent_denunciation.kind := kind_value;
                Inconsistent_denunciation.delegate1 := delegate1;
                Inconsistent_denunciation.delegate2 := delegate2
                |} := cast Inconsistent_denunciation payload in
            Some (kind_value, delegate1, delegate2)
          else None
        end)
      (fun (function_parameter :
        denunciation_kind × Signature.public_key_hash ×
          Signature.public_key_hash) ⇒
        let '(kind_value, delegate1, delegate2) := function_parameter in
        Build_extensible "Inconsistent_denunciation" Inconsistent_denunciation
          {| Inconsistent_denunciation.kind := kind_value;
            Inconsistent_denunciation.delegate1 := delegate1;
            Inconsistent_denunciation.delegate2 := delegate2; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "block.unrequired_denunciation" "Unrequired denunciation"
      "A denunciation is unrequired"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "A valid denunciation cannot be applied: the associated delegate has already been denounced for this level."
                  CamlinternalFormatBasics.End_of_format)
                "A valid denunciation cannot be applied: the associated delegate has already been denounced for this level.")))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unrequired_denunciation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Unrequired_denunciation" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "block.too_early_denunciation" "Too early denunciation"
      "A denunciation is too far in the future"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            denunciation_kind × Alpha_context.Raw_level.t ×
              Alpha_context.Raw_level.t) ⇒
            let '(kind_value, level, current) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "A double-"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " denunciation is too far in the future (current level: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          ", given level: "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ")" % char
                              CamlinternalFormatBasics.End_of_format)))))))
                "A double-%a denunciation is too far in the future (current level: %a, given level: %a)")
              pp_denunciation_kind kind_value Alpha_context.Raw_level.pp current
              Alpha_context.Raw_level.pp level))
      (Data_encoding.obj3
        (Data_encoding.req None None "kind" denunciation_kind_encoding)
        (Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "current" Alpha_context.Raw_level.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_early_denunciation" then
            let '{|
              Too_early_denunciation.kind := kind_value;
                Too_early_denunciation.level := level;
                Too_early_denunciation.current := current
                |} := cast Too_early_denunciation payload in
            Some (kind_value, level, current)
          else None
        end)
      (fun (function_parameter :
        denunciation_kind × Alpha_context.Raw_level.t ×
          Alpha_context.Raw_level.t) ⇒
        let '(kind_value, level, current) := function_parameter in
        Build_extensible "Too_early_denunciation" Too_early_denunciation
          {| Too_early_denunciation.kind := kind_value;
            Too_early_denunciation.level := level;
            Too_early_denunciation.current := current; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "block.outdated_denunciation" "Outdated denunciation"
      "A denunciation is outdated."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            denunciation_kind × Alpha_context.Raw_level.t ×
              Alpha_context.Cycle.t) ⇒
            let '(kind_value, level, last_cycle) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "A double-"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " is outdated (last acceptable cycle: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          ", given level: "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ")" % char
                              CamlinternalFormatBasics.End_of_format)))))))
                "A double-%a is outdated (last acceptable cycle: %a, given level: %a)")
              pp_denunciation_kind kind_value Alpha_context.Cycle.pp last_cycle
              Alpha_context.Raw_level.pp level))
      (Data_encoding.obj3
        (Data_encoding.req None None "kind" denunciation_kind_encoding)
        (Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
        (Data_encoding.req None None "last" Alpha_context.Cycle.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Outdated_denunciation" then
            let '{|
              Outdated_denunciation.kind := kind_value;
                Outdated_denunciation.level := level;
                Outdated_denunciation.last_cycle := last_cycle
                |} := cast Outdated_denunciation payload in
            Some (kind_value, level, last_cycle)
          else None
        end)
      (fun (function_parameter :
        denunciation_kind × Alpha_context.Raw_level.t × Alpha_context.Cycle.t)
        ⇒
        let '(kind_value, level, last_cycle) := function_parameter in
        Build_extensible "Outdated_denunciation" Outdated_denunciation
          {| Outdated_denunciation.kind := kind_value;
            Outdated_denunciation.level := level;
            Outdated_denunciation.last_cycle := last_cycle; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.invalid_activation" "Invalid activation"
      "The given key and secret do not correspond to any existing preallocated contract"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid activation. The public key "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " does not match any commitment."
                      CamlinternalFormatBasics.End_of_format)))
                "Invalid activation. The public key %a does not match any commitment.")
              Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
      (Data_encoding.obj1
        (Data_encoding.req None None "pkh"
          Ed25519.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 "Invalid_activation" then
            let '{| Invalid_activation.pkh := pkh |} :=
              cast Invalid_activation payload in
            Some pkh
          else None
        end)
      (fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
        Build_extensible "Invalid_activation" Invalid_activation
          {| Invalid_activation.pkh := pkh; |}) 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
      "gas_exhausted.init_deserialize"
      "Not enough gas for initial deserialization of script expressions"
      "Gas limit was not high enough to deserialize the transaction parameters or origination script code or initial storage, making the operation impossible to parse within the provided gas bounds."
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Gas_quota_exceeded_init_deserialize" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.inconsistent_sources" "Inconsistent sources in operation pack"
      "The operation pack includes operations from different sources."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf
              "The operation pack includes operations from different sources."))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inconsistent_sources" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Inconsistent_sources" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.failing_noop"
      "Failing_noop operations are not executed by the protocol"
      "The failing_noop operation is an operation that is not and never will be executed by the protocol."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The failing_noop operation cannot be executed by the protocol"
                  CamlinternalFormatBasics.End_of_format)
                "The failing_noop operation cannot be executed by the protocol")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Failing_noop_error" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Failing_noop_error" unit tt) in
  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).

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.fail_when (Alpha_context.Raw_level.op_lteq sunset level)
      (Build_extensible "Tx_rollup_feature_disabled" unit tt) in
  Error_monad.fail_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.fail_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 : Alpha_context.Contract.contract)
  (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.t) :=
  let? ctxt :=
    Alpha_context.Contract.update_script_storage ctxt self storage_value
      lazy_storage_diff in
  Ticket_accounting.update_ticket_balances ctxt self 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 × Apply_results.successful_manager_operation_result ×
      list A) :=
  let? ctxt := Alpha_context.Delegate.set ctxt source delegate in
  return?
    (ctxt,
      (Apply_results.Delegation_result
        {|
          Apply_results.successful_manager_operation_result.Delegation_result.consumed_gas
            := Alpha_context.Gas.consumed before_operation ctxt; |}), nil).

Inductive execution_arg : Set :=
| Typed_arg : {a : Set},
  Alpha_context.Script.location Script_typed_ir.ty a execution_arg
| Untyped_arg : Alpha_context.Script.expr execution_arg.

Definition apply_transaction_to_implicit
  (ctxt : Alpha_context.context) (contract : Alpha_context.Contract.t)
  (parameter : execution_arg) (entrypoint : Alpha_context.Entrypoint.t)
  (before_operation : Alpha_context.context)
  (balance_updates : Alpha_context.Receipt.balance_updates)
  (allocated_destination_contract : bool)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result) :=
  let is_unit :=
    match parameter with
    | Typed_arg _ Script_typed_ir.Unit_t _true
    | Typed_arg _ _ _false
    | Untyped_arg parameter
      match Micheline.root_value parameter with
      | Micheline.Prim _ Michelson_v1_primitives.D_Unit [] _true
      | _false
      end
    end in
  let? ctxt :=
    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
    if is_unit then
      return? ctxt
    else
      Error_monad.error_value
        (Build_extensible "Bad_contract_parameter" Alpha_context.Contract.t
          contract) in
  let result_value :=
    Apply_results.Transaction_result
      (Apply_results.Transaction_to_contract_result
        {|
          Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
            := None;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
            := None;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
            := balance_updates;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
            := nil;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
            := Alpha_context.Gas.consumed before_operation ctxt;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
            := Z.zero;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
            := Z.zero;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
            := allocated_destination_contract; |}) in
  return? (ctxt, result_value).

Definition apply_transaction_to_smart_contract
  (ctxt : Alpha_context.context) (source : Alpha_context.Contract.t)
  (contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
  (entrypoint : Alpha_context.Entrypoint.t)
  (before_operation : Alpha_context.context)
  (payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
  (mode : Script_ir_translator.unparsing_mode) (internal : bool)
  (script_ir : Script_ir_translator.ex_script) (script : Alpha_context.Script.t)
  (parameter : execution_arg) (cache_key : Script_cache.identifier)
  (balance_updates : Alpha_context.Receipt.balance_updates)
  (allocated_destination_contract : bool)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let? balance := Alpha_context.Contract.get_balance ctxt contract in
  let now := Alpha_context.Script_timestamp.now ctxt in
  let level :=
    Alpha_context.Script_int.abs
      (Alpha_context.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 :=
        Alpha_context.Contract.implicit_contract payer;
      Script_typed_ir.step_constants.self := contract;
      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
      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
      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
        |}, ctxt) :=
    execute None ctxt cached_script mode step_constants script entrypoint
      internal in
  let? '(ticket_table_size_diff, ctxt) :=
    update_script_storage_and_ticket_balances ctxt contract 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 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_results.Transaction_result
      (Apply_results.Transaction_to_contract_result
        {|
          Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
            := Some storage_value;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
            := lazy_storage_diff;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
            := balance_updates;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
            := originated_contracts;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
            := Alpha_context.Gas.consumed before_operation ctxt;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
            := new_size;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
            := contract_paid_storage_size_diff +Z ticket_paid_storage_diff;
          Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
            := allocated_destination_contract; |}) in
  return? (ctxt, result_value, operations).

Definition apply_transaction
  (ctxt : Alpha_context.context) (parameter : execution_arg)
  (source : Alpha_context.Contract.t)
  (contract : Alpha_context.Contract.contract) (amount : Alpha_context.Tez.t)
  (entrypoint : Alpha_context.Entrypoint.t)
  (before_operation : Alpha_context.context)
  (payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
  (mode : Script_ir_translator.unparsing_mode) (internal : bool)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let? allocated_destination_contract :=
    match Alpha_context.Contract.is_implicit contract with
    | None
      let? '_ :=
        if Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero then
          Alpha_context.Contract.must_exist ctxt contract
        else
          Error_monad.return_unit in
      Error_monad.return_false
    | Some _
      let? '_ :=
        Error_monad.error_when
          (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
          (Build_extensible "Empty_transaction" Alpha_context.Contract.contract
            contract) in
      Error_monad.op_gtpipeeqquestion
        (Alpha_context.Contract.allocated ctxt contract) Pervasives.not
    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)) amount in
  let? '(ctxt, cache_key, script) := Script_cache.find ctxt contract in
  match script with
  | None
    let? '(ctxt, result_value) :=
      apply_transaction_to_implicit ctxt contract parameter entrypoint
        before_operation balance_updates allocated_destination_contract in
    return? (ctxt, result_value, nil)
  | Some (script, script_ir)
    apply_transaction_to_smart_contract ctxt source contract amount entrypoint
      before_operation payer chain_id mode internal script_ir script parameter
      cache_key balance_updates allocated_destination_contract
  end.

Definition ex_ticket_size
  (ctxt : Alpha_context.context) (function_parameter : Ticket_scanner.ex_ticket)
  : M? (Alpha_context.context × int) :=
  let 'Ticket_scanner.Ex_ticket ty ticket := function_parameter in
  let? ty := Script_typed_ir.ticket_t Micheline.dummy_location ty in
  let? '(ty', ctxt) :=
    Script_ir_translator.unparse_ty Micheline.dummy_location ctxt ty in
  let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
  let ty_size := Saturation_repr.to_int ty_size in
  let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
  let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
  let '(val_nodes, val_size) := Script_typed_ir_size.value_size ty ticket in
  let val_size := Saturation_repr.to_int val_size in
  let val_size_cost := Script_typed_ir_size_costs.nodes_cost val_nodes in
  let? ctxt := Alpha_context.Gas.consume ctxt val_size_cost in
  return? (ctxt, (ty_size +i val_size)).

Definition apply_transaction_to_tx_rollup {A B : Set}
  (ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
  (parameters : A) (amount : Alpha_context.Tez.t)
  (entrypoint : Alpha_context.Entrypoint.t)
  (payer : Alpha_context.public_key_hash)
  (dst_rollup : Alpha_context.Tx_rollup.t) (since : Alpha_context.context)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list B) :=
  let? '_ := assert_tx_rollup_feature_enabled ctxt in
  let? '_ :=
    Error_monad.fail_unless
      (Alpha_context.Tez.op_eq amount Alpha_context.Tez.zero)
      (Build_extensible "Tx_rollup_invalid_transaction_amount" unit tt) in
  if
    Alpha_context.Entrypoint.op_eq entrypoint
      Alpha_context.Tx_rollup.deposit_entrypoint
  then
    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? '(ctxt, ticket_size) := 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 (ticket_size >i 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_token.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 (Alpha_context.Script_int.to_int64 ticket_amount)
          Tx_rollup_l2_qty.of_int64)
        (Error_monad.trace_of_error
          (Build_extensible "Tx_rollup_invalid_transaction_amount" 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
            (Alpha_context.Contract.implicit_contract 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_results.Transaction_result
        (Apply_results.Transaction_to_tx_rollup_result
          {|
            Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
              := ticket_hash;
            Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
              := balance_updates;
            Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
              := Alpha_context.Gas.consumed since ctxt;
            Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
              := paid_storage_size_diff; |}) in
    return? (ctxt, result_value, nil)
  else
    Error_monad.fail
      (Build_extensible "No_such_entrypoint" Alpha_context.Entrypoint.t
        entrypoint).

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 : Alpha_context.Contract.t)
  (delegate : option Signature.public_key_hash)
  (source : Alpha_context.Contract.t) (credit : Alpha_context.Tez.t)
  (before_operation : Alpha_context.context)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_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_translator.Optimized false to_duplicate to_update storage_type
      storage_value in
  let? '(storage_value, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_translator.Optimized
      storage_type storage_value in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost storage_value) in
  let storage_value :=
    Alpha_context.Script.lazy_expr_value
      (Micheline.strip_locations storage_value) in
  let? '(code, ctxt) :=
    Script_ir_translator.unparse_code ctxt Script_ir_translator.Optimized
      (Micheline.root_value unparsed_code) in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost code) in
  let code :=
    Alpha_context.Script.lazy_expr_value (Micheline.strip_locations 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
      (script, lazy_storage_diff) in
  let? ctxt :=
    match delegate with
    | Nonereturn? ctxt
    | Some delegateAlpha_context.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 in
  let result_value :=
    Apply_results.Origination_result
      {|
        Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
          := lazy_storage_diff;
        Apply_results.successful_manager_operation_result.Origination_result.balance_updates
          := balance_updates;
        Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
          := [ contract ];
        Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
          := Alpha_context.Gas.consumed before_operation ctxt;
        Apply_results.successful_manager_operation_result.Origination_result.storage_size
          := size_value;
        Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
          := paid_storage_size_diff; |} in
  return? (ctxt, result_value, nil).

Definition prepare_apply_manager_operation_content
  (ctxt : Alpha_context.context) (source : Alpha_context.Contract.contract)
  (gas_consumed_in_precheck : option Alpha_context.Gas.cost)
  : M?
    (Alpha_context.context × Alpha_context.context ×
      Alpha_context.Script.consume_deserialization_gas) :=
  let before_operation := ctxt in
  let? '_ := Alpha_context.Contract.must_exist ctxt source in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt Michelson_v1_gas.Cost_of.manager_operation in
  let? ctxt :=
    match gas_consumed_in_precheck with
    | NonePervasives.Ok ctxt
    | Some gasAlpha_context.Gas.consume ctxt gas
    end in
  let consume_deserialization_gas := Alpha_context.Script.When_needed in
  return? (ctxt, before_operation, consume_deserialization_gas).

Definition apply_internal_manager_operation_content
  (ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
  (payer : Alpha_context.public_key_hash) (source : Alpha_context.Contract.t)
  (chain_id : Chain_id.t)
  (gas_consumed_in_precheck : option Alpha_context.Gas.cost)
  (operation : Script_typed_ir.manager_operation)
  : M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list Script_typed_ir.packed_internal_operation) :=
  let? '(ctxt, before_operation, consume_deserialization_gas) :=
    prepare_apply_manager_operation_content ctxt source gas_consumed_in_precheck
    in
  match operation with
  |
    Script_typed_ir.Transaction {|
      Script_typed_ir.manager_operation.Transaction.transaction := {|
        Alpha_context.transaction.amount := amount;
          Alpha_context.transaction.parameters := _;
          Alpha_context.transaction.entrypoint := entrypoint;
          Alpha_context.transaction.destination :=
            Alpha_context.Destination.Contract contract
          |};
        Script_typed_ir.manager_operation.Transaction.location := location;
        Script_typed_ir.manager_operation.Transaction.parameters_ty :=
          parameters_ty;
        Script_typed_ir.manager_operation.Transaction.parameters :=
          typed_parameters
        |} ⇒
    let? '(ctxt, manager_result, operations) :=
      apply_transaction ctxt (Typed_arg location parameters_ty typed_parameters)
        source contract amount entrypoint before_operation payer chain_id mode
        true in
    return? (ctxt, manager_result, operations)
  |
    Script_typed_ir.Transaction {|
      Script_typed_ir.manager_operation.Transaction.transaction := {|
        Alpha_context.transaction.amount := amount;
          Alpha_context.transaction.parameters := _;
          Alpha_context.transaction.entrypoint := entrypoint;
          Alpha_context.transaction.destination :=
            Alpha_context.Destination.Tx_rollup dst
          |};
        Script_typed_ir.manager_operation.Transaction.location := _;
        Script_typed_ir.manager_operation.Transaction.parameters_ty :=
          parameters_ty;
        Script_typed_ir.manager_operation.Transaction.parameters := parameters
        |} ⇒
    apply_transaction_to_tx_rollup ctxt parameters_ty parameters amount
      entrypoint payer dst before_operation
  |
    Script_typed_ir.Origination {|
      Script_typed_ir.manager_operation.Origination.origination := {|
        Alpha_context.origination.delegate := delegate;
          Alpha_context.origination.script := script;
          Alpha_context.origination.credit := credit
          |};
        Script_typed_ir.manager_operation.Origination.preorigination := contract;
        Script_typed_ir.manager_operation.Origination.storage_type :=
          storage_type;
        Script_typed_ir.manager_operation.Origination.storage := storage_value
        |} ⇒
    let? '(unparsed_code, ctxt) :=
      Alpha_context.Script.force_decode_in_context consume_deserialization_gas
        ctxt script.(Alpha_context.Script.t.code) in
    apply_origination ctxt storage_type storage_value unparsed_code contract
      delegate source credit before_operation
  | Script_typed_ir.Delegation delegate
    apply_delegation ctxt source delegate before_operation
  end.

Axiom apply_external_manager_operation_content :
  Alpha_context.context Script_ir_translator.unparsing_mode
  Alpha_context.public_key_hash Chain_id.t
  option Alpha_context.Gas.cost Alpha_context.manager_operation
  M?
    (Alpha_context.context × Apply_results.successful_manager_operation_result ×
      list Script_typed_ir.packed_internal_operation).

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

#[bypass_check(guard)]
Definition apply_internal_manager_operations
  (ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
  (payer : Alpha_context.public_key_hash) (chain_id : Chain_id.t)
  (ops : list Script_typed_ir.packed_internal_operation)
  : success_or_failure ×
    list Apply_results.packed_internal_manager_operation_result :=
  let fix apply
    (ctxt : Alpha_context.context)
    (applied : list Apply_results.packed_internal_manager_operation_result)
    (worklist : list Script_typed_ir.packed_internal_operation) {struct ctxt}
    : success_or_failure ×
      list Apply_results.packed_internal_manager_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 op_res := Apply_results.contents_of_internal_operation op in
      let function_parameter :=
        if Alpha_context.internal_nonce_already_recorded ctxt nonce_value then
          Error_monad.fail
            (Build_extensible "Internal_operation_replay"
              Apply_results.packed_internal_contents
              (Apply_results.Internal_contents op_res))
        else
          let ctxt := Alpha_context.record_internal_nonce ctxt nonce_value in
          apply_internal_manager_operation_content ctxt mode payer source
            chain_id None operation in
      match function_parameter with
      | Pervasives.Error errors
        let result_value :=
          Apply_results.pack_internal_manager_operation_result op
            (Apply_results.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_results.pack_internal_manager_operation_result op
                (Apply_results.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_results.pack_internal_manager_operation_result op
              (Apply_results.Applied result_value)) applied)
          (Pervasives.op_at emitted rest)
      end
    end in
  apply ctxt nil ops.

Definition precheck_manager_contents
  (ctxt : Alpha_context.context) (op : Alpha_context.contents)
  (only_batch : bool)
  : M? (Alpha_context.context × Apply_results.precheck_result) :=
  match op with
  |
    Alpha_context.Manager_operation {|
      Alpha_context.contents.Manager_operation.source := source;
        Alpha_context.contents.Manager_operation.fee := fee;
        Alpha_context.contents.Manager_operation.counter := counter;
        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 :=
      (if only_batch then
        Error_monad.record_trace (Build_extensible "Gas_limit_too_high" unit tt)
      else
        fun (errs : M? Alpha_context.context) ⇒ errs)
        (Alpha_context.Gas.consume_limit_in_block ctxt gas_limit) in
    let ctxt := Alpha_context.Gas.set_limit ctxt gas_limit in
    let ctxt_before := ctxt in
    let? '_ := Alpha_context.Fees.check_storage_limit ctxt storage_limit in
    let source_contract := Alpha_context.Contract.implicit_contract source in
    let? '_ := Alpha_context.Contract.must_be_allocated ctxt source_contract in
    let? '_ :=
      Alpha_context.Contract.check_counter_increment ctxt source counter in
    let consume_deserialization_gas := Alpha_context.Script.Always in
    let? ctxt :=
      match operation with
      | Alpha_context.Reveal pk
        Alpha_context.Contract.reveal_manager_key ctxt source pk
      |
        Alpha_context.Transaction {|
          Alpha_context.transaction.parameters := parameters;
            Alpha_context.transaction.destination := destination
            |} ⇒
        let? '_ :=
          Error_monad.fail_when
            match destination with
            | Alpha_context.Destination.Tx_rollup _true
            | _false
            end (Build_extensible "Tx_rollup_non_internal_transaction" unit tt)
          in
        Error_monad.record_trace
          (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
          (let? '(_arg, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt parameters in
          return? ctxt)
      |
        Alpha_context.Origination {|
          Alpha_context.origination.script := script |} ⇒
        Error_monad.record_trace
          (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
          (let? '(_code, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt
              script.(Alpha_context.Script.t.code) in
          let? '(_storage, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt
              script.(Alpha_context.Script.t.storage) in
          return? ctxt)
      |
        Alpha_context.Register_global_constant {|
          Alpha_context.manager_operation.Register_global_constant.value := value_value
            |} ⇒
        Error_monad.record_trace
          (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
          (let? '(_value, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt value_value in
          return? ctxt)
      | (Alpha_context.Delegation _ | Alpha_context.Set_deposits_limit _) ⇒
        return? ctxt
      | Alpha_context.Tx_rollup_origination
        let? '_ := assert_tx_rollup_feature_enabled ctxt in
        return? ctxt
      |
        Alpha_context.Tx_rollup_submit_batch {|
          Alpha_context.manager_operation.Tx_rollup_submit_batch.content := content
            |} ⇒
        let? '_ := assert_tx_rollup_feature_enabled ctxt in
        let size_limit :=
          Alpha_context.Constants.tx_rollup_hard_size_limit_per_message ctxt in
        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? '_ :=
          Error_monad.fail_unless (message_size i size_limit)
            (Build_extensible "Message_size_exceeds_limit" unit tt) in
        return? ctxt
      |
        (Alpha_context.Tx_rollup_commit _ |
        Alpha_context.Tx_rollup_return_bond _ |
        Alpha_context.Tx_rollup_finalize_commitment _ |
        Alpha_context.Tx_rollup_remove_commitment _) ⇒
        let? '_ := assert_tx_rollup_feature_enabled ctxt in
        return? ctxt
      |
        Alpha_context.Transfer_ticket {|
          Alpha_context.manager_operation.Transfer_ticket.contents := contents;
            Alpha_context.manager_operation.Transfer_ticket.ty := ty
            |} ⇒
        let? '_ := assert_tx_rollup_feature_enabled ctxt in
        Error_monad.record_trace
          (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
          (let? '(_contents, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt contents in
          let? '(_ty, ctxt) :=
            Alpha_context.Script.force_decode_in_context
              consume_deserialization_gas ctxt ty in
          return? ctxt)
      |
        Alpha_context.Tx_rollup_dispatch_tickets {|
          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? '_ := assert_tx_rollup_feature_enabled ctxt in
        let '{|
          Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
            tx_rollup_max_messages_per_inbox;
            Alpha_context.Constants.parametric.tx_rollup_max_withdrawals_per_batch
              := tx_rollup_max_withdrawals_per_batch
            |} := Alpha_context.Constants.parametric_value ctxt in
        let? '_ :=
          Alpha_context.Tx_rollup_errors.check_path_depth
            Alpha_context.Tx_rollup_errors.Commitment
            (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
              message_result_path) tx_rollup_max_messages_per_inbox in
        let? '_ :=
          Error_monad.error_when (Compare.List_length_with.op_eq tickets_info 0)
            (Build_extensible "No_withdrawals_to_dispatch" unit tt) in
        let? '_ :=
          Error_monad.error_when
            (Compare.List_length_with.op_gt tickets_info
              tx_rollup_max_withdrawals_per_batch)
            (Build_extensible "Too_many_withdrawals" unit tt) in
        let? ctxt :=
          Error_monad.record_trace
            (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
            (List.fold_left_e
              (fun (ctxt : Alpha_context.context) ⇒
                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
                      |} := function_parameter in
                  let? '(_contents, ctxt) :=
                    Alpha_context.Script.force_decode_in_context
                      consume_deserialization_gas ctxt contents in
                  let? '(_ty, ctxt) :=
                    Alpha_context.Script.force_decode_in_context
                      consume_deserialization_gas ctxt ty in
                  return? ctxt) ctxt tickets_info) in
        return? ctxt
      |
        Alpha_context.Tx_rollup_rejection {|
          Alpha_context.manager_operation.Tx_rollup_rejection.message_path :=
            message_path;
            Alpha_context.manager_operation.Tx_rollup_rejection.message_result_path
              := message_result_path;
            Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result_path
              := previous_message_result_path
            |} ⇒
        let? '_ := assert_tx_rollup_feature_enabled ctxt in
        let '{|
          Alpha_context.Constants.parametric.tx_rollup_max_messages_per_inbox :=
            tx_rollup_max_messages_per_inbox
            |} := Alpha_context.Constants.parametric_value ctxt in
        let? '_ :=
          Alpha_context.Tx_rollup_errors.check_path_depth
            Alpha_context.Tx_rollup_errors.Inbox
            (Alpha_context.Tx_rollup_inbox.Merkle.path_depth message_path)
            tx_rollup_max_messages_per_inbox in
        let? '_ :=
          Alpha_context.Tx_rollup_errors.check_path_depth
            Alpha_context.Tx_rollup_errors.Commitment
            (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
              message_result_path) tx_rollup_max_messages_per_inbox in
        let? '_ :=
          Alpha_context.Tx_rollup_errors.check_path_depth
            Alpha_context.Tx_rollup_errors.Commitment
            (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
              previous_message_result_path) tx_rollup_max_messages_per_inbox in
        return? ctxt
      |
        (Alpha_context.Sc_rollup_originate _ |
        Alpha_context.Sc_rollup_add_messages _ |
        Alpha_context.Sc_rollup_cement _ | Alpha_context.Sc_rollup_publish _) ⇒
        let? '_ := assert_sc_rollup_feature_enabled ctxt in
        return? ctxt
      end in
    let? ctxt := Alpha_context.Contract.increment_counter ctxt source 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_container Alpha_context.Token.Block_fees) fee
      in
    let consumed_gas := Alpha_context.Gas.consumed ctxt_before ctxt in
    return?
      (ctxt,
        {| Apply_results.precheck_result.consumed_gas := consumed_gas;
          Apply_results.precheck_result.balance_updates := balance_updates; |})
  | _unreachable_gadt_branch
  end.

[burn_storage_fees ctxt smopr storage_limit payer] burns the storage fees associated to an 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_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
        (Alpha_context.Contract.implicit_contract payer)) in
  match smopr with
  |
    Apply_results.Transaction_result
      (Apply_results.Transaction_to_contract_result payload) ⇒
    let consumed :=
      payload.(Apply_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_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_results.successful_transaction_result.Transaction_to_contract_result.balance_updates)
          origination_bus) in
    return?
      (ctxt, storage_limit,
        (Apply_results.Transaction_result
          (Apply_results.Transaction_to_contract_result
            {|
              Apply_results.successful_transaction_result.Transaction_to_contract_result.storage
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
                := balance_updates;
              Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.storage_size);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff);
              Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
                :=
                payload.(Apply_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract);
              |})))
  |
    Apply_results.Transaction_result
      (Apply_results.Transaction_to_tx_rollup_result payload) ⇒
    let consumed :=
      payload.(Apply_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_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates)
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Transaction_result
          (Apply_results.Transaction_to_tx_rollup_result
            (Apply_results.successful_transaction_result.Transaction_to_tx_rollup_result.with_balance_updates
              balance_updates payload))))
  | Apply_results.Origination_result payload
    let consumed :=
      payload.(Apply_results.successful_manager_operation_result.Origination_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) :=
      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
          payload.(Apply_results.successful_manager_operation_result.Origination_result.balance_updates))
      in
    return?
      (ctxt, storage_limit,
        (Apply_results.Origination_result
          {|
            Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff
              :=
              payload.(Apply_results.successful_manager_operation_result.Origination_result.lazy_storage_diff);
            Apply_results.successful_manager_operation_result.Origination_result.balance_updates
              := balance_updates;
            Apply_results.successful_manager_operation_result.Origination_result.originated_contracts
              :=
              payload.(Apply_results.successful_manager_operation_result.Origination_result.originated_contracts);
            Apply_results.successful_manager_operation_result.Origination_result.consumed_gas
              :=
              payload.(Apply_results.successful_manager_operation_result.Origination_result.consumed_gas);
            Apply_results.successful_manager_operation_result.Origination_result.storage_size
              :=
              payload.(Apply_results.successful_manager_operation_result.Origination_result.storage_size);
            Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff
              :=
              payload.(Apply_results.successful_manager_operation_result.Origination_result.paid_storage_size_diff);
            |}))
  | (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 _
    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.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)
  end.

Definition apply_manager_contents
  (ctxt : Alpha_context.context) (mode : Script_ir_translator.unparsing_mode)
  (chain_id : Chain_id.t)
  (gas_consumed_in_precheck : option Alpha_context.Gas.cost)
  (op : Alpha_context.contents)
  : success_or_failure × Apply_results.manager_operation_result ×
    list Apply_results.packed_internal_manager_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_external_manager_operation_content ctxt mode source chain_id
        gas_consumed_in_precheck operation in
    match function_parameter with
    | Pervasives.Ok (ctxt, operation_results, internal_operations)
      let function_parameter :=
        apply_internal_manager_operations ctxt mode source chain_id
          internal_operations in
      match function_parameter with
      | (Success ctxt, internal_operations_results)
        let function_parameter :=
          burn_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_results.packed_internal_manager_operation_result)
                ⇒
                let '(ctxt, storage_limit, res) := function_parameter in
                fun (imopr :
                  Apply_results.packed_internal_manager_operation_result) ⇒
                  let
                    'Apply_results.Internal_manager_operation_result op mopr :=
                    imopr in
                  match mopr with
                  | Apply_results.Applied smopr
                    let? '(ctxt, storage_limit, smopr) :=
                      burn_storage_fees ctxt smopr storage_limit source in
                    let imopr :=
                      Apply_results.Internal_manager_operation_result op
                        (Apply_results.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_results.Applied operation_results),
              (List.rev internal_operations_results))
          | Pervasives.Error errors
            (Failure,
              (Apply_results.Backtracked operation_results (Some errors)),
              internal_operations_results)
          end
        | Pervasives.Error errors
          (Failure, (Apply_results.Backtracked operation_results (Some errors)),
            internal_operations_results)
        end
      | (Failure, internal_operations_results)
        (Failure, (Apply_results.Applied operation_results),
          internal_operations_results)
      end
    | Pervasives.Error errors
      (Failure,
        (Apply_results.Failed (Alpha_context.manager_kind operation) errors),
        nil)
    end
  | _unreachable_gadt_branch
  end.

Definition skipped_operation_result
  (operation : Alpha_context.manager_operation)
  : Apply_results.manager_operation_result :=
  match operation with
  | Alpha_context.Reveal _
    Apply_results.Applied
      (Apply_results.Reveal_result
        {|
          Apply_results.successful_manager_operation_result.Reveal_result.consumed_gas
            := Alpha_context.Gas.Arith.zero; |})
  | _Apply_results.Skipped (Alpha_context.manager_kind operation)
  end.

Axiom mark_skipped :
  Signature.public_key_hash Alpha_context.Level.t
  Apply_results.prechecked_contents_list Apply_results.contents_result_list.

Check that counters are consistent, i.e. that they are successive within a batch. Fail with a {b permanent} error otherwise. TODO: https://gitlab.com/tezos/tezos/-/issues/2301 Remove when format of operation is changed to save space.
Definition check_counters_consistency
  (contents_list : Alpha_context.contents_list) : M? unit :=
  let check_counter (previous_counter : option Z.t) (counter : Z.t) : M? unit :=
    match previous_counter with
    | NoneError_monad.return_unit
    | Some previous_counter
      let expected := Z.succ previous_counter in
      if expected =Z counter then
        Error_monad.return_unit
      else
        Error_monad.fail (Build_extensible "Inconsistent_counters" unit tt)
    end in
  let fix check_counters_rec
    (previous_counter : option Alpha_context.counter)
    (contents_list : Alpha_context.contents_list) : M? unit :=
    match contents_list with
    |
      Alpha_context.Single
        (Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.counter := counter |}) ⇒
      check_counter previous_counter counter
    |
      Alpha_context.Cons
        (Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.counter := counter |})
        rest
      let? '_ := check_counter previous_counter counter in
      check_counters_rec (Some counter) rest
    | _unreachable_gadt_branch
    end in
  check_counters_rec None contents_list.

Returns an updated context, and a list of prechecked contents containing balance updates for fees related to each manager operation in [contents_list].
Definition precheck_manager_contents_list
  (ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
  (mempool_mode : bool)
  : M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
  let fix rec_precheck_manager_contents_list
    (ctxt : Alpha_context.context) (contents_list : Alpha_context.contents_list)
    : M? (Alpha_context.context × Apply_results.prechecked_contents_list) :=
    match contents_list with
    | Alpha_context.Single contents
      let? '(ctxt, result_value) :=
        precheck_manager_contents ctxt contents mempool_mode in
      return?
        (ctxt,
          (Apply_results.PrecheckedSingle
            {| Apply_results.prechecked_contents.contents := contents;
              Apply_results.prechecked_contents.result := result_value; |}))
    | Alpha_context.Cons contents rest
      let? '(ctxt, result_value) :=
        precheck_manager_contents ctxt contents mempool_mode in
      let? '(ctxt, results_rest) := rec_precheck_manager_contents_list ctxt rest
        in
      return?
        (ctxt,
          (Apply_results.PrecheckedCons
            {| Apply_results.prechecked_contents.contents := contents;
              Apply_results.prechecked_contents.result := result_value; |}
            results_rest))
    end in
  let ctxt :=
    if mempool_mode then
      Alpha_context.Gas.reset_block_gas ctxt
    else
      ctxt in
  let? '_ := check_counters_consistency contents_list in
  rec_precheck_manager_contents_list ctxt contents_list.

Definition find_manager_public_key
  (ctxt : Alpha_context.context) (op : Alpha_context.contents_list)
  : M? Signature.public_key :=
  let check_same_manager {A : Set}
    (function_parameter : Signature.public_key_hash × option A)
    : option (Signature.public_key_hash × option A)
    M? (Signature.public_key_hash × option A) :=
    let '(source, source_key) := function_parameter in
    fun (manager : option (Signature.public_key_hash × option A)) ⇒
      match manager with
      | Nonereturn? (source, source_key)
      | Some (manager, manager_key)
        if
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) source
            manager
        then
          return? (source, (Option.either manager_key source_key))
        else
          Error_monad.error_value
            (Build_extensible "Inconsistent_sources" unit tt)
      end in
  let fix find_source
    (contents_list : Alpha_context.contents_list)
    (manager : option (Signature.public_key_hash × option Signature.public_key))
    : M? (Signature.public_key_hash × option Signature.public_key) :=
    let source (function_parameter : Alpha_context.contents)
      : Signature.public_key_hash × option Signature.public_key :=
      match function_parameter with
      |
        Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.source := source;
            Alpha_context.contents.Manager_operation.operation :=
              Alpha_context.Reveal key_value
            |} ⇒ (source, (Some key_value))
      |
        Alpha_context.Manager_operation {|
          Alpha_context.contents.Manager_operation.source := source |} ⇒
        (source, None)
      | _unreachable_gadt_branch
      end in
    match contents_list with
    | Alpha_context.Single opcheck_same_manager (source op) manager
    | Alpha_context.Cons op rest
      let? manager := check_same_manager (source op) manager in
      find_source rest (Some manager)
    end in
  let? '(source, source_key) := find_source op None in
  match source_key with
  | Some key_valuereturn? key_value
  | NoneAlpha_context.Contract.get_manager_key None ctxt source
  end.

Definition check_manager_signature
  (ctxt : Alpha_context.context) (chain_id : Chain_id.t)
  (op : Alpha_context.contents_list) (raw_operation : Alpha_context.operation)
  : M? unit :=
  let? public_key := find_manager_public_key ctxt op in
  Alpha_context.Operation.check_signature public_key chain_id raw_operation.

Axiom apply_manager_contents_list_rec :
  Alpha_context.context Script_ir_translator.unparsing_mode
  Alpha_context.public_key_hash Chain_id.t
  Apply_results.prechecked_contents_list
  success_or_failure × Apply_results.contents_result_list.

Axiom mark_backtracked :
  Apply_results.contents_result_list Apply_results.contents_result_list.

Records for the constructor parameters
Module ConstructorRecords_apply_mode.
  Module apply_mode.
    Module Application.
      Record record {predecessor_block payload_hash locked_round
        predecessor_level predecessor_round round : Set} : Set := Build {
        predecessor_block : predecessor_block;
        payload_hash : payload_hash;
        locked_round : locked_round;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
        round : round;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor_block
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} predecessor_block
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round predecessor_block
          r.(payload_hash) r.(locked_round) r.(predecessor_level)
          r.(predecessor_round) r.(round).
      Definition with_payload_hash
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} payload_hash
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
          payload_hash r.(locked_round) r.(predecessor_level)
          r.(predecessor_round) r.(round).
      Definition with_locked_round
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} locked_round
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
          r.(payload_hash) locked_round r.(predecessor_level)
          r.(predecessor_round) r.(round).
      Definition with_predecessor_level
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} predecessor_level
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
          r.(payload_hash) r.(locked_round) predecessor_level
          r.(predecessor_round) r.(round).
      Definition with_predecessor_round
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} predecessor_round
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
          r.(payload_hash) r.(locked_round) r.(predecessor_level)
          predecessor_round r.(round).
      Definition with_round
        {t_predecessor_block t_payload_hash t_locked_round t_predecessor_level
          t_predecessor_round t_round} round
        (r :
          record t_predecessor_block t_payload_hash t_locked_round
            t_predecessor_level t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_locked_round
          t_predecessor_level t_predecessor_round t_round r.(predecessor_block)
          r.(payload_hash) r.(locked_round) r.(predecessor_level)
          r.(predecessor_round) round.
    End Application.
    Definition Application_skeleton := Application.record.

    Module Full_construction.
      Record record {predecessor_block payload_hash predecessor_level
        predecessor_round round : Set} : Set := Build {
        predecessor_block : predecessor_block;
        payload_hash : payload_hash;
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
        round : round;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor_block
        {t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round} predecessor_block
        (r :
          record t_predecessor_block t_payload_hash t_predecessor_level
            t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round predecessor_block r.(payload_hash)
          r.(predecessor_level) r.(predecessor_round) r.(round).
      Definition with_payload_hash
        {t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round} payload_hash
        (r :
          record t_predecessor_block t_payload_hash t_predecessor_level
            t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round r.(predecessor_block) payload_hash
          r.(predecessor_level) r.(predecessor_round) r.(round).
      Definition with_predecessor_level
        {t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round} predecessor_level
        (r :
          record t_predecessor_block t_payload_hash t_predecessor_level
            t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
          predecessor_level r.(predecessor_round) r.(round).
      Definition with_predecessor_round
        {t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round} predecessor_round
        (r :
          record t_predecessor_block t_payload_hash t_predecessor_level
            t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
          r.(predecessor_level) predecessor_round r.(round).
      Definition with_round
        {t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round} round
        (r :
          record t_predecessor_block t_payload_hash t_predecessor_level
            t_predecessor_round t_round) :=
        Build t_predecessor_block t_payload_hash t_predecessor_level
          t_predecessor_round t_round r.(predecessor_block) r.(payload_hash)
          r.(predecessor_level) r.(predecessor_round) round.
    End Full_construction.
    Definition Full_construction_skeleton := Full_construction.record.

    Module Partial_construction.
      Record record {predecessor_level predecessor_round grand_parent_round :
        Set} : Set := Build {
        predecessor_level : predecessor_level;
        predecessor_round : predecessor_round;
        grand_parent_round : grand_parent_round;
      }.
      Arguments record : clear implicits.
      Definition with_predecessor_level
        {t_predecessor_level t_predecessor_round t_grand_parent_round}
        predecessor_level
        (r :
          record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
        Build t_predecessor_level t_predecessor_round t_grand_parent_round
          predecessor_level r.(predecessor_round) r.(grand_parent_round).
      Definition with_predecessor_round
        {t_predecessor_level t_predecessor_round t_grand_parent_round}
        predecessor_round
        (r :
          record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
        Build t_predecessor_level t_predecessor_round t_grand_parent_round
          r.(predecessor_level) predecessor_round r.(grand_parent_round).
      Definition with_grand_parent_round
        {t_predecessor_level t_predecessor_round t_grand_parent_round}
        grand_parent_round
        (r :
          record t_predecessor_level t_predecessor_round t_grand_parent_round) :=
        Build t_predecessor_level t_predecessor_round t_grand_parent_round
          r.(predecessor_level) r.(predecessor_round) grand_parent_round.
    End Partial_construction.
    Definition Partial_construction_skeleton := Partial_construction.record.
  End apply_mode.
End ConstructorRecords_apply_mode.
Import ConstructorRecords_apply_mode.

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

Inductive apply_mode : Set :=
| Application : 'apply_mode.Application apply_mode
| Full_construction : 'apply_mode.Full_construction apply_mode
| Partial_construction : 'apply_mode.Partial_construction apply_mode

where "'apply_mode.Application" :=
  (apply_mode.Application_skeleton Block_hash.t Block_payload_hash.t
    (option Alpha_context.Round.t) Alpha_context.Level.t Alpha_context.Round.t
    Alpha_context.Round.t)
and "'apply_mode.Full_construction" :=
  (apply_mode.Full_construction_skeleton Block_hash.t Block_payload_hash.t
    Alpha_context.Level.t Alpha_context.Round.t Alpha_context.Round.t)
and "'apply_mode.Partial_construction" :=
  (apply_mode.Partial_construction_skeleton Alpha_context.Level.t
    Alpha_context.Round.t Alpha_context.Round.t).

Module apply_mode.
  Include ConstructorRecords_apply_mode.apply_mode.
  Definition Application := 'apply_mode.Application.
  Definition Full_construction := 'apply_mode.Full_construction.
  Definition Partial_construction := 'apply_mode.Partial_construction.
End apply_mode.

Definition get_predecessor_level (function_parameter : apply_mode)
  : Alpha_context.Level.t :=
  match function_parameter with
  |
    (Application {|
      apply_mode.Application.predecessor_level := predecessor_level |} |
    Full_construction {|
      apply_mode.Full_construction.predecessor_level := predecessor_level |}
    |
    Partial_construction {|
      apply_mode.Partial_construction.predecessor_level := predecessor_level
        |}) ⇒ predecessor_level
  end.

Definition record_operation
  (ctxt : Alpha_context.context) (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.Failing_noop _ | Alpha_context.Proposals _ |