💸 Operation_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_update_repr.

Module Kind.
  Inductive preendorsement_consensus_kind : Set :=
  | Preendorsement_consensus_kind : preendorsement_consensus_kind.

  Inductive endorsement_consensus_kind : Set :=
  | Endorsement_consensus_kind : endorsement_consensus_kind.

  Inductive consensus : Set :=
  | Preendorsement_kind : consensus
  | Endorsement_kind : consensus.

  Definition preendorsement : Set := consensus.

  Definition endorsement : Set := consensus.

  Inductive dal_attestation : Set :=
  | Dal_attestation_kind : dal_attestation.

  Inductive seed_nonce_revelation : Set :=
  | Seed_nonce_revelation_kind : seed_nonce_revelation.

  Inductive vdf_revelation : Set :=
  | Vdf_revelation_kind : vdf_revelation.

  Inductive double_consensus_operation_evidence : Set :=
  | Double_consensus_operation_evidence : double_consensus_operation_evidence.

  Definition double_endorsement_evidence : Set :=
    double_consensus_operation_evidence.

  Definition double_preendorsement_evidence : Set :=
    double_consensus_operation_evidence.

  Inductive double_baking_evidence : Set :=
  | Double_baking_evidence_kind : double_baking_evidence.

  Inductive activate_account : Set :=
  | Activate_account_kind : activate_account.

  Inductive proposals : Set :=
  | Proposals_kind : proposals.

  Inductive ballot : Set :=
  | Ballot_kind : ballot.

  Inductive reveal : Set :=
  | Reveal_kind : reveal.

  Inductive transaction : Set :=
  | Transaction_kind : transaction.

  Inductive origination : Set :=
  | Origination_kind : origination.

  Inductive delegation : Set :=
  | Delegation_kind : delegation.

  Inductive event : Set :=
  | Event_kind : event.

  Inductive set_deposits_limit : Set :=
  | Set_deposits_limit_kind : set_deposits_limit.

  Inductive increase_paid_storage : Set :=
  | Increase_paid_storage_kind : increase_paid_storage.

  Inductive update_consensus_key : Set :=
  | Update_consensus_key_kind : update_consensus_key.

  Inductive drain_delegate : Set :=
  | Drain_delegate_kind : drain_delegate.

  Inductive failing_noop : Set :=
  | Failing_noop_kind : failing_noop.

  Inductive register_global_constant : Set :=
  | Register_global_constant_kind : register_global_constant.

  Inductive tx_rollup_origination : Set :=
  | Tx_rollup_origination_kind : tx_rollup_origination.

  Inductive tx_rollup_submit_batch : Set :=
  | Tx_rollup_submit_batch_kind : tx_rollup_submit_batch.

  Inductive tx_rollup_commit : Set :=
  | Tx_rollup_commit_kind : tx_rollup_commit.

  Inductive tx_rollup_return_bond : Set :=
  | Tx_rollup_return_bond_kind : tx_rollup_return_bond.

  Inductive tx_rollup_finalize_commitment : Set :=
  | Tx_rollup_finalize_commitment_kind : tx_rollup_finalize_commitment.

  Inductive tx_rollup_remove_commitment : Set :=
  | Tx_rollup_remove_commitment_kind : tx_rollup_remove_commitment.

  Inductive tx_rollup_rejection : Set :=
  | Tx_rollup_rejection_kind : tx_rollup_rejection.

  Inductive tx_rollup_dispatch_tickets : Set :=
  | Tx_rollup_dispatch_tickets_kind : tx_rollup_dispatch_tickets.

  Inductive transfer_ticket : Set :=
  | Transfer_ticket_kind : transfer_ticket.

  Inductive dal_publish_slot_header : Set :=
  | Dal_publish_slot_header_kind : dal_publish_slot_header.

  Inductive sc_rollup_originate : Set :=
  | Sc_rollup_originate_kind : sc_rollup_originate.

  Inductive sc_rollup_add_messages : Set :=
  | Sc_rollup_add_messages_kind : sc_rollup_add_messages.

  Inductive sc_rollup_cement : Set :=
  | Sc_rollup_cement_kind : sc_rollup_cement.

  Inductive sc_rollup_publish : Set :=
  | Sc_rollup_publish_kind : sc_rollup_publish.

  Inductive sc_rollup_refute : Set :=
  | Sc_rollup_refute_kind : sc_rollup_refute.

  Inductive sc_rollup_timeout : Set :=
  | Sc_rollup_timeout_kind : sc_rollup_timeout.

  Inductive sc_rollup_execute_outbox_message : Set :=
  | Sc_rollup_execute_outbox_message_kind : sc_rollup_execute_outbox_message.

  Inductive sc_rollup_recover_bond : Set :=
  | Sc_rollup_recover_bond_kind : sc_rollup_recover_bond.

  Inductive zk_rollup_origination : Set :=
  | Zk_rollup_origination_kind : zk_rollup_origination.

  Inductive zk_rollup_publish : Set :=
  | Zk_rollup_publish_kind : zk_rollup_publish.

  Inductive zk_rollup_update : Set :=
  | Zk_rollup_update_kind : zk_rollup_update.

  Inductive manager : Set :=
  | Reveal_manager_kind : manager
  | Transaction_manager_kind : manager
  | Origination_manager_kind : manager
  | Delegation_manager_kind : manager
  | Event_manager_kind : manager
  | Register_global_constant_manager_kind : manager
  | Set_deposits_limit_manager_kind : manager
  | Increase_paid_storage_manager_kind : manager
  | Update_consensus_key_manager_kind : manager
  | Tx_rollup_origination_manager_kind : manager
  | Tx_rollup_submit_batch_manager_kind : manager
  | Tx_rollup_commit_manager_kind : manager
  | Tx_rollup_return_bond_manager_kind : manager
  | Tx_rollup_finalize_commitment_manager_kind : manager
  | Tx_rollup_remove_commitment_manager_kind : manager
  | Tx_rollup_rejection_manager_kind : manager
  | Tx_rollup_dispatch_tickets_manager_kind : manager
  | Transfer_ticket_manager_kind : manager
  | Dal_publish_slot_header_manager_kind : manager
  | Sc_rollup_originate_manager_kind : manager
  | Sc_rollup_add_messages_manager_kind : manager
  | Sc_rollup_cement_manager_kind : manager
  | Sc_rollup_publish_manager_kind : manager
  | Sc_rollup_refute_manager_kind : manager
  | Sc_rollup_timeout_manager_kind : manager
  | Sc_rollup_execute_outbox_message_manager_kind : manager
  | Sc_rollup_recover_bond_manager_kind : manager
  | Zk_rollup_origination_manager_kind : manager
  | Zk_rollup_publish_manager_kind : manager
  | Zk_rollup_update_manager_kind : manager.
End Kind.

Module Consensus_operation_type.
  Inductive t : Set :=
  | Endorsement : t
  | Preendorsement : t.

  Definition pp (ppf : Format.formatter) (operation_kind : t) : unit :=
    match operation_kind with
    | Endorsement ⇒
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Endorsement"
            CamlinternalFormatBasics.End_of_format) "Endorsement")
    | Preendorsement ⇒
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Preendorsement"
            CamlinternalFormatBasics.End_of_format) "Preendorsement")
    end.
End Consensus_operation_type.

Module consensus_content.
  Record record : Set := Build {
    slot : Slot_repr.t;
    level : Raw_level_repr.t;
    round : Round_repr.t;
    block_payload_hash : Block_payload_hash.t;
  }.
  Definition with_slot slot (r : record) :=
    Build slot r.(level) r.(round) r.(block_payload_hash).
  Definition with_level level (r : record) :=
    Build r.(slot) level r.(round) r.(block_payload_hash).
  Definition with_round round (r : record) :=
    Build r.(slot) r.(level) round r.(block_payload_hash).
  Definition with_block_payload_hash block_payload_hash (r : record) :=
    Build r.(slot) r.(level) r.(round) block_payload_hash.
End consensus_content.
Definition consensus_content := consensus_content.record.

Definition consensus_content_encoding
  : Data_encoding.encoding consensus_content :=
  Data_encoding.conv
    (fun (function_parameter : consensus_content) ⇒
      let '{|
        consensus_content.slot := slot;
          consensus_content.level := level;
          consensus_content.round := round;
          consensus_content.block_payload_hash := block_payload_hash
          |} := function_parameter in
      (slot, level, round, block_payload_hash))
    (fun (function_parameter :
      Slot_repr.t × Raw_level_repr.t × Round_repr.t × Block_payload_hash.t) ⇒
      let '(slot, level, round, block_payload_hash) := function_parameter in
      {| consensus_content.slot := slot; consensus_content.level := level;
        consensus_content.round := round;
        consensus_content.block_payload_hash := block_payload_hash; |}) None
    (Data_encoding.obj4 (Data_encoding.req None None "slot" Slot_repr.encoding)
      (Data_encoding.req None None "level" Raw_level_repr.encoding)
      (Data_encoding.req None None "round" Round_repr.encoding)
      (Data_encoding.req None None "block_payload_hash"
        Block_payload_hash.encoding)).

Definition pp_consensus_content
  (ppf : Format.formatter) (content : consensus_content) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Char_literal "(" % char
        (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
          CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.No_precision
          (CamlinternalFormatBasics.String_literal ", "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal ", "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal ", "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal ")" % char
                        CamlinternalFormatBasics.End_of_format)))))))))
      "(%ld, %a, %a, %a)")
    (Raw_level_repr.to_int32 content.(consensus_content.level)) Round_repr.pp
    content.(consensus_content.round) Slot_repr.pp
    content.(consensus_content.slot) Block_payload_hash.pp_short
    content.(consensus_content.block_payload_hash).

Module Consensus_watermark.
  Inductive consensus_watermark : Set :=
  | Endorsement : Chain_id.t → consensus_watermark
  | Preendorsement : Chain_id.t → consensus_watermark
  | Dal_attestation : Chain_id.t → consensus_watermark.
End Consensus_watermark.

Definition bytes_of_consensus_watermark
  (function_parameter : Consensus_watermark.consensus_watermark) : bytes :=
  match function_parameter with
  | Consensus_watermark.Preendorsement chain_id ⇒
    Bytes.cat (Bytes.of_string (String.String "018" ""))
      (Chain_id.to_bytes chain_id)
  |
    (Consensus_watermark.Dal_attestation chain_id |
    Consensus_watermark.Endorsement chain_id) ⇒
    Bytes.cat (Bytes.of_string (String.String "019" ""))
      (Chain_id.to_bytes chain_id)
  end.

Definition to_watermark (w_value : Consensus_watermark.consensus_watermark)
  : Signature.watermark :=
  Signature.Custom (bytes_of_consensus_watermark w_value).

Definition of_watermark (function_parameter : Signature.watermark)
  : option Consensus_watermark.consensus_watermark :=
  match function_parameter with
  | Signature.Custom b_value ⇒
    if (Bytes.length b_value) >i 0 then
      match Bytes.get b_value 0 with
      | "018" % char ⇒
        Option.map
          (fun (chain_id : Chain_id.t) ⇒
            Consensus_watermark.Endorsement chain_id)
          (Chain_id.of_bytes_opt
            (Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
      | "019" % char ⇒
        Option.map
          (fun (chain_id : Chain_id.t) ⇒
            Consensus_watermark.Preendorsement chain_id)
          (Chain_id.of_bytes_opt
            (Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
      | "020" % char ⇒
        Option.map
          (fun (chain_id : Chain_id.t) ⇒
            Consensus_watermark.Dal_attestation chain_id)
          (Chain_id.of_bytes_opt
            (Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
      | _ ⇒ None
      end
    else
      None
  | _ ⇒ None
  end.

Definition raw : Set := Operation.t.

Definition raw_encoding : Data_encoding.t Operation.t := Operation.encoding.

Records for the constructor parameters

Module ConstructorRecords_contents_manager_operation.
  Module contents.
    Module Seed_nonce_revelation.
      Record record {level nonce : Set} : Set := Build {
        level : level;
        nonce : nonce;
      }.
      Arguments record : clear implicits.
      Definition with_level {t_level t_nonce} level
        (r : record t_level t_nonce) :=
        Build t_level t_nonce level r.(nonce).
      Definition with_nonce {t_level t_nonce} nonce
        (r : record t_level t_nonce) :=
        Build t_level t_nonce r.(level) nonce.
    End Seed_nonce_revelation.
    Definition Seed_nonce_revelation_skeleton := Seed_nonce_revelation.record.

    Module Vdf_revelation.
      Record record {solution : Set} : Set := Build {
        solution : solution;
      }.
      Arguments record : clear implicits.
      Definition with_solution {t_solution} solution (r : record t_solution) :=
        Build t_solution solution.
    End Vdf_revelation.
    Definition Vdf_revelation_skeleton := Vdf_revelation.record.

    Module Double_preendorsement_evidence.
      Record record {op1 op2 : Set} : Set := Build {
        op1 : op1;
        op2 : op2;
      }.
      Arguments record : clear implicits.
      Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
        Build t_op1 t_op2 op1 r.(op2).
      Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
        Build t_op1 t_op2 r.(op1) op2.
    End Double_preendorsement_evidence.
    Definition Double_preendorsement_evidence_skeleton :=
      Double_preendorsement_evidence.record.

    Module Double_endorsement_evidence.
      Record record {op1 op2 : Set} : Set := Build {
        op1 : op1;
        op2 : op2;
      }.
      Arguments record : clear implicits.
      Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
        Build t_op1 t_op2 op1 r.(op2).
      Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
        Build t_op1 t_op2 r.(op1) op2.
    End Double_endorsement_evidence.
    Definition Double_endorsement_evidence_skeleton :=
      Double_endorsement_evidence.record.

    Module Double_baking_evidence.
      Record record {bh1 bh2 : Set} : Set := Build {
        bh1 : bh1;
        bh2 : bh2;
      }.
      Arguments record : clear implicits.
      Definition with_bh1 {t_bh1 t_bh2} bh1 (r : record t_bh1 t_bh2) :=
        Build t_bh1 t_bh2 bh1 r.(bh2).
      Definition with_bh2 {t_bh1 t_bh2} bh2 (r : record t_bh1 t_bh2) :=
        Build t_bh1 t_bh2 r.(bh1) bh2.
    End Double_baking_evidence.
    Definition Double_baking_evidence_skeleton := Double_baking_evidence.record.

    Module Activate_account.
      Record record {id activation_code : Set} : Set := Build {
        id : id;
        activation_code : activation_code;
      }.
      Arguments record : clear implicits.
      Definition with_id {t_id t_activation_code} id
        (r : record t_id t_activation_code) :=
        Build t_id t_activation_code id r.(activation_code).
      Definition with_activation_code {t_id t_activation_code} activation_code
        (r : record t_id t_activation_code) :=
        Build t_id t_activation_code r.(id) activation_code.
    End Activate_account.
    Definition Activate_account_skeleton := Activate_account.record.

    Module Proposals.
      Record record {source period proposals : Set} : Set := Build {
        source : source;
        period : period;
        proposals : proposals;
      }.
      Arguments record : clear implicits.
      Definition with_source {t_source t_period t_proposals} source
        (r : record t_source t_period t_proposals) :=
        Build t_source t_period t_proposals source r.(period) r.(proposals).
      Definition with_period {t_source t_period t_proposals} period
        (r : record t_source t_period t_proposals) :=
        Build t_source t_period t_proposals r.(source) period r.(proposals).
      Definition with_proposals {t_source t_period t_proposals} proposals
        (r : record t_source t_period t_proposals) :=
        Build t_source t_period t_proposals r.(source) r.(period) proposals.
    End Proposals.
    Definition Proposals_skeleton := Proposals.record.

    Module Ballot.
      Record record {source period proposal ballot : Set} : Set := Build {
        source : source;
        period : period;
        proposal : proposal;
        ballot : ballot;
      }.
      Arguments record : clear implicits.
      Definition with_source {t_source t_period t_proposal t_ballot} source
        (r : record t_source t_period t_proposal t_ballot) :=
        Build t_source t_period t_proposal t_ballot source r.(period)
          r.(proposal) r.(ballot).
      Definition with_period {t_source t_period t_proposal t_ballot} period
        (r : record t_source t_period t_proposal t_ballot) :=
        Build t_source t_period t_proposal t_ballot r.(source) period
          r.(proposal) r.(ballot).
      Definition with_proposal {t_source t_period t_proposal t_ballot} proposal
        (r : record t_source t_period t_proposal t_ballot) :=
        Build t_source t_period t_proposal t_ballot r.(source) r.(period)
          proposal r.(ballot).
      Definition with_ballot {t_source t_period t_proposal t_ballot} ballot
        (r : record t_source t_period t_proposal t_ballot) :=
        Build t_source t_period t_proposal t_ballot r.(source) r.(period)
          r.(proposal) ballot.
    End Ballot.
    Definition Ballot_skeleton := Ballot.record.

    Module Drain_delegate.
      Record record {consensus_key delegate destination : Set} : Set := Build {
        consensus_key : consensus_key;
        delegate : delegate;
        destination : destination;
      }.
      Arguments record : clear implicits.
      Definition with_consensus_key {t_consensus_key t_delegate t_destination}
        consensus_key (r : record t_consensus_key t_delegate t_destination) :=
        Build t_consensus_key t_delegate t_destination consensus_key
          r.(delegate) r.(destination).
      Definition with_delegate {t_consensus_key t_delegate t_destination}
        delegate (r : record t_consensus_key t_delegate t_destination) :=
        Build t_consensus_key t_delegate t_destination r.(consensus_key)
          delegate r.(destination).
      Definition with_destination {t_consensus_key t_delegate t_destination}
        destination (r : record t_consensus_key t_delegate t_destination) :=
        Build t_consensus_key t_delegate t_destination r.(consensus_key)
          r.(delegate) destination.
    End Drain_delegate.
    Definition Drain_delegate_skeleton := Drain_delegate.record.

    Module Manager_operation.
      Record record {source fee counter operation gas_limit storage_limit : Set} :
        Set := Build {
        source : source;
        fee : fee;
        counter : counter;
        operation : operation;
        gas_limit : gas_limit;
        storage_limit : storage_limit;
      }.
      Arguments record : clear implicits.
      Definition with_source
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
        source
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          source r.(fee) r.(counter) r.(operation) r.(gas_limit)
          r.(storage_limit).
      Definition with_fee
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit} fee
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          r.(source) fee r.(counter) r.(operation) r.(gas_limit)
          r.(storage_limit).
      Definition with_counter
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
        counter
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          r.(source) r.(fee) counter r.(operation) r.(gas_limit)
          r.(storage_limit).
      Definition with_operation
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
        operation
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          r.(source) r.(fee) r.(counter) operation r.(gas_limit)
          r.(storage_limit).
      Definition with_gas_limit
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
        gas_limit
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          r.(source) r.(fee) r.(counter) r.(operation) gas_limit
          r.(storage_limit).
      Definition with_storage_limit
        {t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
        storage_limit
        (r :
          record t_source t_fee t_counter t_operation t_gas_limit
            t_storage_limit) :=
        Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
          r.(source) r.(fee) r.(counter) r.(operation) r.(gas_limit)
          storage_limit.
    End Manager_operation.
    Definition Manager_operation_skeleton := Manager_operation.record.
  End contents.
  Module manager_operation.
    Module Transaction.
      Record record {amount parameters entrypoint destination : Set} : Set := Build {
        amount : amount;
        parameters : parameters;
        entrypoint : entrypoint;
        destination : destination;
      }.
      Arguments record : clear implicits.
      Definition with_amount {t_amount t_parameters t_entrypoint t_destination}
        amount (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination amount
          r.(parameters) r.(entrypoint) r.(destination).
      Definition with_parameters
        {t_amount t_parameters t_entrypoint t_destination} parameters
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          parameters r.(entrypoint) r.(destination).
      Definition with_entrypoint
        {t_amount t_parameters t_entrypoint t_destination} entrypoint
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          r.(parameters) entrypoint r.(destination).
      Definition with_destination
        {t_amount t_parameters t_entrypoint t_destination} destination
        (r : record t_amount t_parameters t_entrypoint t_destination) :=
        Build t_amount t_parameters t_entrypoint t_destination r.(amount)
          r.(parameters) r.(entrypoint) destination.
    End Transaction.
    Definition Transaction_skeleton := Transaction.record.

    Module Origination.
      Record record {delegate script credit : Set} : Set := Build {
        delegate : delegate;
        script : script;
        credit : credit;
      }.
      Arguments record : clear implicits.
      Definition with_delegate {t_delegate t_script t_credit} delegate
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit delegate r.(script) r.(credit).
      Definition with_script {t_delegate t_script t_credit} script
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit r.(delegate) script r.(credit).
      Definition with_credit {t_delegate t_script t_credit} credit
        (r : record t_delegate t_script t_credit) :=
        Build t_delegate t_script t_credit r.(delegate) r.(script) credit.
    End Origination.
    Definition Origination_skeleton := Origination.record.

    Module Register_global_constant.
      Record record {value : Set} : Set := Build {
        value : value;
      }.
      Arguments record : clear implicits.
      Definition with_value {t_value} value (r : record t_value) :=
        Build t_value value.
    End Register_global_constant.
    Definition Register_global_constant_skeleton :=
      Register_global_constant.record.

    Module Increase_paid_storage.
      Record record {amount_in_bytes destination : Set} : Set := Build {
        amount_in_bytes : amount_in_bytes;
        destination : destination;
      }.
      Arguments record : clear implicits.
      Definition with_amount_in_bytes {t_amount_in_bytes t_destination}
        amount_in_bytes (r : record t_amount_in_bytes t_destination) :=
        Build t_amount_in_bytes t_destination amount_in_bytes r.(destination).
      Definition with_destination {t_amount_in_bytes t_destination} destination
        (r : record t_amount_in_bytes t_destination) :=
        Build t_amount_in_bytes t_destination r.(amount_in_bytes) destination.
    End Increase_paid_storage.
    Definition Increase_paid_storage_skeleton := Increase_paid_storage.record.

    Module Tx_rollup_submit_batch.
      Record record {tx_rollup content burn_limit : Set} : Set := Build {
        tx_rollup : tx_rollup;
        content : content;
        burn_limit : burn_limit;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup {t_tx_rollup t_content t_burn_limit} tx_rollup
        (r : record t_tx_rollup t_content t_burn_limit) :=
        Build t_tx_rollup t_content t_burn_limit tx_rollup r.(content)
          r.(burn_limit).
      Definition with_content {t_tx_rollup t_content t_burn_limit} content
        (r : record t_tx_rollup t_content t_burn_limit) :=
        Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) content
          r.(burn_limit).
      Definition with_burn_limit {t_tx_rollup t_content t_burn_limit} burn_limit
        (r : record t_tx_rollup t_content t_burn_limit) :=
        Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) r.(content)
          burn_limit.
    End Tx_rollup_submit_batch.
    Definition Tx_rollup_submit_batch_skeleton := Tx_rollup_submit_batch.record.

    Module Tx_rollup_commit.
      Record record {tx_rollup commitment : Set} : Set := Build {
        tx_rollup : tx_rollup;
        commitment : commitment;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup {t_tx_rollup t_commitment} tx_rollup
        (r : record t_tx_rollup t_commitment) :=
        Build t_tx_rollup t_commitment tx_rollup r.(commitment).
      Definition with_commitment {t_tx_rollup t_commitment} commitment
        (r : record t_tx_rollup t_commitment) :=
        Build t_tx_rollup t_commitment r.(tx_rollup) commitment.
    End Tx_rollup_commit.
    Definition Tx_rollup_commit_skeleton := Tx_rollup_commit.record.

    Module Tx_rollup_return_bond.
      Record record {tx_rollup : Set} : Set := Build {
        tx_rollup : tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup {t_tx_rollup} tx_rollup
        (r : record t_tx_rollup) :=
        Build t_tx_rollup tx_rollup.
    End Tx_rollup_return_bond.
    Definition Tx_rollup_return_bond_skeleton := Tx_rollup_return_bond.record.

    Module Tx_rollup_finalize_commitment.
      Record record {tx_rollup : Set} : Set := Build {
        tx_rollup : tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup {t_tx_rollup} tx_rollup
        (r : record t_tx_rollup) :=
        Build t_tx_rollup tx_rollup.
    End Tx_rollup_finalize_commitment.
    Definition Tx_rollup_finalize_commitment_skeleton :=
      Tx_rollup_finalize_commitment.record.

    Module Tx_rollup_remove_commitment.
      Record record {tx_rollup : Set} : Set := Build {
        tx_rollup : tx_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup {t_tx_rollup} tx_rollup
        (r : record t_tx_rollup) :=
        Build t_tx_rollup tx_rollup.
    End Tx_rollup_remove_commitment.
    Definition Tx_rollup_remove_commitment_skeleton :=
      Tx_rollup_remove_commitment.record.

    Module Tx_rollup_rejection.
      Record record {tx_rollup level message message_position message_path
        message_result_hash message_result_path previous_message_result
        previous_message_result_path proof : Set} : Set := Build {
        tx_rollup : tx_rollup;
        level : level;
        message : message;
        message_position : message_position;
        message_path : message_path;
        message_result_hash : message_result_hash;
        message_result_path : message_result_path;
        previous_message_result : previous_message_result;
        previous_message_result_path : previous_message_result_path;
        proof : proof;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} tx_rollup
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof tx_rollup r.(level) r.(message)
          r.(message_position) r.(message_path) r.(message_result_hash)
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_level
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} level
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) level r.(message)
          r.(message_position) r.(message_path) r.(message_result_hash)
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_message
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} message
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level) message
          r.(message_position) r.(message_path) r.(message_result_hash)
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_message_position
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} message_position
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) message_position r.(message_path) r.(message_result_hash)
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_message_path
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} message_path
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) message_path r.(message_result_hash)
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_message_result_hash
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} message_result_hash
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) r.(message_path) message_result_hash
          r.(message_result_path) r.(previous_message_result)
          r.(previous_message_result_path) r.(proof).
      Definition with_message_result_path
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} message_result_path
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) r.(message_path)
          r.(message_result_hash) message_result_path
          r.(previous_message_result) r.(previous_message_result_path)
          r.(proof).
      Definition with_previous_message_result
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} previous_message_result
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) r.(message_path)
          r.(message_result_hash) r.(message_result_path)
          previous_message_result r.(previous_message_result_path) r.(proof).
      Definition with_previous_message_result_path
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} previous_message_result_path
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) r.(message_path)
          r.(message_result_hash) r.(message_result_path)
          r.(previous_message_result) previous_message_result_path r.(proof).
      Definition with_proof
        {t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof} proof
        (r :
          record t_tx_rollup t_level t_message t_message_position t_message_path
            t_message_result_hash t_message_result_path
            t_previous_message_result t_previous_message_result_path t_proof) :=
        Build t_tx_rollup t_level t_message t_message_position t_message_path
          t_message_result_hash t_message_result_path t_previous_message_result
          t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
          r.(message) r.(message_position) r.(message_path)
          r.(message_result_hash) r.(message_result_path)
          r.(previous_message_result) r.(previous_message_result_path) proof.
    End Tx_rollup_rejection.
    Definition Tx_rollup_rejection_skeleton := Tx_rollup_rejection.record.

    Module Tx_rollup_dispatch_tickets.
      Record record {tx_rollup level context_hash message_index
        message_result_path tickets_info : Set} : Set := Build {
        tx_rollup : tx_rollup;
        level : level;
        context_hash : context_hash;
        message_index : message_index;
        message_result_path : message_result_path;
        tickets_info : tickets_info;
      }.
      Arguments record : clear implicits.
      Definition with_tx_rollup
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} tx_rollup
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info tx_rollup r.(level)
          r.(context_hash) r.(message_index) r.(message_result_path)
          r.(tickets_info).
      Definition with_level
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} level
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info r.(tx_rollup) level
          r.(context_hash) r.(message_index) r.(message_result_path)
          r.(tickets_info).
      Definition with_context_hash
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} context_hash
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
          context_hash r.(message_index) r.(message_result_path)
          r.(tickets_info).
      Definition with_message_index
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} message_index
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
          r.(context_hash) message_index r.(message_result_path)
          r.(tickets_info).
      Definition with_message_result_path
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} message_result_path
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
          r.(context_hash) r.(message_index) message_result_path
          r.(tickets_info).
      Definition with_tickets_info
        {t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info} tickets_info
        (r :
          record t_tx_rollup t_level t_context_hash t_message_index
            t_message_result_path t_tickets_info) :=
        Build t_tx_rollup t_level t_context_hash t_message_index
          t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
          r.(context_hash) r.(message_index) r.(message_result_path)
          tickets_info.
    End Tx_rollup_dispatch_tickets.
    Definition Tx_rollup_dispatch_tickets_skeleton :=
      Tx_rollup_dispatch_tickets.record.

    Module Transfer_ticket.
      Record record {contents ty ticketer amount destination entrypoint : Set} :
        Set := Build {
        contents : contents;
        ty : ty;
        ticketer : ticketer;
        amount : amount;
        destination : destination;
        entrypoint : entrypoint;
      }.
      Arguments record : clear implicits.
      Definition with_contents
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
        contents
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          contents r.(ty) r.(ticketer) r.(amount) r.(destination)
          r.(entrypoint).
      Definition with_ty
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} ty
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          r.(contents) ty r.(ticketer) r.(amount) r.(destination)
          r.(entrypoint).
      Definition with_ticketer
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
        ticketer
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          r.(contents) r.(ty) ticketer r.(amount) r.(destination)
          r.(entrypoint).
      Definition with_amount
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} amount
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          r.(contents) r.(ty) r.(ticketer) amount r.(destination)
          r.(entrypoint).
      Definition with_destination
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
        destination
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          r.(contents) r.(ty) r.(ticketer) r.(amount) destination
          r.(entrypoint).
      Definition with_entrypoint
        {t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
        entrypoint
        (r :
          record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
        Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
          r.(contents) r.(ty) r.(ticketer) r.(amount) r.(destination)
          entrypoint.
    End Transfer_ticket.
    Definition Transfer_ticket_skeleton := Transfer_ticket.record.

    Module Dal_publish_slot_header.
      Record record {slot_header : Set} : Set := Build {
        slot_header : slot_header;
      }.
      Arguments record : clear implicits.
      Definition with_slot_header {t_slot_header} slot_header
        (r : record t_slot_header) :=
        Build t_slot_header slot_header.
    End Dal_publish_slot_header.
    Definition Dal_publish_slot_header_skeleton :=
      Dal_publish_slot_header.record.

    Module Sc_rollup_originate.
      Record record {kind boot_sector origination_proof parameters_ty : Set} :
        Set := Build {
        kind : kind;
        boot_sector : boot_sector;
        origination_proof : origination_proof;
        parameters_ty : parameters_ty;
      }.
      Arguments record : clear implicits.
      Definition with_kind
        {t_kind t_boot_sector t_origination_proof t_parameters_ty} kind
        (r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
        Build t_kind t_boot_sector t_origination_proof t_parameters_ty kind
          r.(boot_sector) r.(origination_proof) r.(parameters_ty).
      Definition with_boot_sector
        {t_kind t_boot_sector t_origination_proof t_parameters_ty} boot_sector
        (r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
        Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
          boot_sector r.(origination_proof) r.(parameters_ty).
      Definition with_origination_proof
        {t_kind t_boot_sector t_origination_proof t_parameters_ty}
        origination_proof
        (r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
        Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
          r.(boot_sector) origination_proof r.(parameters_ty).
      Definition with_parameters_ty
        {t_kind t_boot_sector t_origination_proof t_parameters_ty} parameters_ty
        (r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
        Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
          r.(boot_sector) r.(origination_proof) parameters_ty.
    End Sc_rollup_originate.
    Definition Sc_rollup_originate_skeleton := Sc_rollup_originate.record.

    Module Sc_rollup_add_messages.
      Record record {messages : Set} : Set := Build {
        messages : messages;
      }.
      Arguments record : clear implicits.
      Definition with_messages {t_messages} messages (r : record t_messages) :=
        Build t_messages messages.
    End Sc_rollup_add_messages.
    Definition Sc_rollup_add_messages_skeleton := Sc_rollup_add_messages.record.

    Module Sc_rollup_cement.
      Record record {rollup commitment : Set} : Set := Build {
        rollup : rollup;
        commitment : commitment;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_commitment} rollup
        (r : record t_rollup t_commitment) :=
        Build t_rollup t_commitment rollup r.(commitment).
      Definition with_commitment {t_rollup t_commitment} commitment
        (r : record t_rollup t_commitment) :=
        Build t_rollup t_commitment r.(rollup) commitment.
    End Sc_rollup_cement.
    Definition Sc_rollup_cement_skeleton := Sc_rollup_cement.record.

    Module Sc_rollup_publish.
      Record record {rollup commitment : Set} : Set := Build {
        rollup : rollup;
        commitment : commitment;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_commitment} rollup
        (r : record t_rollup t_commitment) :=
        Build t_rollup t_commitment rollup r.(commitment).
      Definition with_commitment {t_rollup t_commitment} commitment
        (r : record t_rollup t_commitment) :=
        Build t_rollup t_commitment r.(rollup) commitment.
    End Sc_rollup_publish.
    Definition Sc_rollup_publish_skeleton := Sc_rollup_publish.record.

    Module Sc_rollup_refute.
      Record record {rollup opponent refutation : Set} : Set := Build {
        rollup : rollup;
        opponent : opponent;
        refutation : refutation;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_opponent t_refutation} rollup
        (r : record t_rollup t_opponent t_refutation) :=
        Build t_rollup t_opponent t_refutation rollup r.(opponent)
          r.(refutation).
      Definition with_opponent {t_rollup t_opponent t_refutation} opponent
        (r : record t_rollup t_opponent t_refutation) :=
        Build t_rollup t_opponent t_refutation r.(rollup) opponent
          r.(refutation).
      Definition with_refutation {t_rollup t_opponent t_refutation} refutation
        (r : record t_rollup t_opponent t_refutation) :=
        Build t_rollup t_opponent t_refutation r.(rollup) r.(opponent)
          refutation.
    End Sc_rollup_refute.
    Definition Sc_rollup_refute_skeleton := Sc_rollup_refute.record.

    Module Sc_rollup_timeout.
      Record record {rollup stakers : Set} : Set := Build {
        rollup : rollup;
        stakers : stakers;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_stakers} rollup
        (r : record t_rollup t_stakers) :=
        Build t_rollup t_stakers rollup r.(stakers).
      Definition with_stakers {t_rollup t_stakers} stakers
        (r : record t_rollup t_stakers) :=
        Build t_rollup t_stakers r.(rollup) stakers.
    End Sc_rollup_timeout.
    Definition Sc_rollup_timeout_skeleton := Sc_rollup_timeout.record.

    Module Sc_rollup_execute_outbox_message.
      Record record {rollup cemented_commitment output_proof : Set} : Set := Build {
        rollup : rollup;
        cemented_commitment : cemented_commitment;
        output_proof : output_proof;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_cemented_commitment t_output_proof}
        rollup (r : record t_rollup t_cemented_commitment t_output_proof) :=
        Build t_rollup t_cemented_commitment t_output_proof rollup
          r.(cemented_commitment) r.(output_proof).
      Definition with_cemented_commitment
        {t_rollup t_cemented_commitment t_output_proof} cemented_commitment
        (r : record t_rollup t_cemented_commitment t_output_proof) :=
        Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
          cemented_commitment r.(output_proof).
      Definition with_output_proof
        {t_rollup t_cemented_commitment t_output_proof} output_proof
        (r : record t_rollup t_cemented_commitment t_output_proof) :=
        Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
          r.(cemented_commitment) output_proof.
    End Sc_rollup_execute_outbox_message.
    Definition Sc_rollup_execute_outbox_message_skeleton :=
      Sc_rollup_execute_outbox_message.record.

    Module Sc_rollup_recover_bond.
      Record record {sc_rollup : Set} : Set := Build {
        sc_rollup : sc_rollup;
      }.
      Arguments record : clear implicits.
      Definition with_sc_rollup {t_sc_rollup} sc_rollup
        (r : record t_sc_rollup) :=
        Build t_sc_rollup sc_rollup.
    End Sc_rollup_recover_bond.
    Definition Sc_rollup_recover_bond_skeleton := Sc_rollup_recover_bond.record.

    Module Zk_rollup_origination.
      Record record {public_parameters circuits_info init_state nb_ops : Set} :
        Set := Build {
        public_parameters : public_parameters;
        circuits_info : circuits_info;
        init_state : init_state;
        nb_ops : nb_ops;
      }.
      Arguments record : clear implicits.
      Definition with_public_parameters
        {t_public_parameters t_circuits_info t_init_state t_nb_ops}
        public_parameters
        (r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
        Build t_public_parameters t_circuits_info t_init_state t_nb_ops
          public_parameters r.(circuits_info) r.(init_state) r.(nb_ops).
      Definition with_circuits_info
        {t_public_parameters t_circuits_info t_init_state t_nb_ops}
        circuits_info
        (r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
        Build t_public_parameters t_circuits_info t_init_state t_nb_ops
          r.(public_parameters) circuits_info r.(init_state) r.(nb_ops).
      Definition with_init_state
        {t_public_parameters t_circuits_info t_init_state t_nb_ops} init_state
        (r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
        Build t_public_parameters t_circuits_info t_init_state t_nb_ops
          r.(public_parameters) r.(circuits_info) init_state r.(nb_ops).
      Definition with_nb_ops
        {t_public_parameters t_circuits_info t_init_state t_nb_ops} nb_ops
        (r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
        Build t_public_parameters t_circuits_info t_init_state t_nb_ops
          r.(public_parameters) r.(circuits_info) r.(init_state) nb_ops.
    End Zk_rollup_origination.
    Definition Zk_rollup_origination_skeleton := Zk_rollup_origination.record.

    Module Zk_rollup_publish.
      Record record {zk_rollup ops : Set} : Set := Build {
        zk_rollup : zk_rollup;
        ops : ops;
      }.
      Arguments record : clear implicits.
      Definition with_zk_rollup {t_zk_rollup t_ops} zk_rollup
        (r : record t_zk_rollup t_ops) :=
        Build t_zk_rollup t_ops zk_rollup r.(ops).
      Definition with_ops {t_zk_rollup t_ops} ops
        (r : record t_zk_rollup t_ops) :=
        Build t_zk_rollup t_ops r.(zk_rollup) ops.
    End Zk_rollup_publish.
    Definition Zk_rollup_publish_skeleton := Zk_rollup_publish.record.

    Module Zk_rollup_update.
      Record record {zk_rollup update : Set} : Set := Build {
        zk_rollup : zk_rollup;
        update : update;
      }.
      Arguments record : clear implicits.
      Definition with_zk_rollup {t_zk_rollup t_update} zk_rollup
        (r : record t_zk_rollup t_update) :=
        Build t_zk_rollup t_update zk_rollup r.(update).
      Definition with_update {t_zk_rollup t_update} update
        (r : record t_zk_rollup t_update) :=
        Build t_zk_rollup t_update r.(zk_rollup) update.
    End Zk_rollup_update.
    Definition Zk_rollup_update_skeleton := Zk_rollup_update.record.
  End manager_operation.
End ConstructorRecords_contents_manager_operation.
Import ConstructorRecords_contents_manager_operation.

Module protocol_data.
  Record record {contents signature : Set} : Set := Build {
    contents : contents;
    signature : signature;
  }.
  Arguments record : clear implicits.
  Definition with_contents {t_contents t_signature} contents
    (r : record t_contents t_signature) :=
    Build t_contents t_signature contents r.(signature).
  Definition with_signature {t_contents t_signature} signature
    (r : record t_contents t_signature) :=
    Build t_contents t_signature r.(contents) signature.
End protocol_data.
Definition protocol_data_skeleton := protocol_data.record.

Module operation.
  Record record {shell protocol_data : Set} : Set := Build {
    shell : shell;
    protocol_data : protocol_data;
  }.
  Arguments record : clear implicits.
  Definition with_shell {t_shell t_protocol_data} shell
    (r : record t_shell t_protocol_data) :=
    Build t_shell t_protocol_data shell r.(protocol_data).
  Definition with_protocol_data {t_shell t_protocol_data} protocol_data
    (r : record t_shell t_protocol_data) :=
    Build t_shell t_protocol_data r.(shell) protocol_data.
End operation.
Definition operation_skeleton := operation.record.

Reserved Notation "'contents.Seed_nonce_revelation".
Reserved Notation "'contents.Vdf_revelation".
Reserved Notation "'contents.Double_preendorsement_evidence".
Reserved Notation "'contents.Double_endorsement_evidence".
Reserved Notation "'contents.Double_baking_evidence".
Reserved Notation "'contents.Activate_account".
Reserved Notation "'contents.Proposals".
Reserved Notation "'contents.Ballot".
Reserved Notation "'contents.Drain_delegate".
Reserved Notation "'contents.Manager_operation".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'manager_operation.Register_global_constant".
Reserved Notation "'manager_operation.Increase_paid_storage".
Reserved Notation "'manager_operation.Tx_rollup_submit_batch".
Reserved Notation "'manager_operation.Tx_rollup_commit".
Reserved Notation "'manager_operation.Tx_rollup_return_bond".
Reserved Notation "'manager_operation.Tx_rollup_finalize_commitment".
Reserved Notation "'manager_operation.Tx_rollup_remove_commitment".
Reserved Notation "'manager_operation.Tx_rollup_rejection".
Reserved Notation "'manager_operation.Tx_rollup_dispatch_tickets".
Reserved Notation "'manager_operation.Transfer_ticket".
Reserved Notation "'manager_operation.Dal_publish_slot_header".
Reserved Notation "'manager_operation.Sc_rollup_originate".
Reserved Notation "'manager_operation.Sc_rollup_add_messages".
Reserved Notation "'manager_operation.Sc_rollup_cement".
Reserved Notation "'manager_operation.Sc_rollup_publish".
Reserved Notation "'manager_operation.Sc_rollup_refute".
Reserved Notation "'manager_operation.Sc_rollup_timeout".
Reserved Notation "'manager_operation.Sc_rollup_execute_outbox_message".
Reserved Notation "'manager_operation.Sc_rollup_recover_bond".
Reserved Notation "'manager_operation.Zk_rollup_origination".
Reserved Notation "'manager_operation.Zk_rollup_publish".
Reserved Notation "'manager_operation.Zk_rollup_update".
Reserved Notation "'operation".
Reserved Notation "'protocol_data".

Inductive contents_list : Set :=
| Single : contents → contents_list
| Cons : contents → contents_list → contents_list

with contents : Set :=
| Preendorsement : consensus_content → contents
| Endorsement : consensus_content → contents
| Dal_attestation : Dal_attestation_repr.operation → contents
| Seed_nonce_revelation : 'contents.Seed_nonce_revelation → contents
| Vdf_revelation : 'contents.Vdf_revelation → contents
| Double_preendorsement_evidence :
  'contents.Double_preendorsement_evidence → contents
| Double_endorsement_evidence :
  'contents.Double_endorsement_evidence → contents
| Double_baking_evidence : 'contents.Double_baking_evidence → contents
| Activate_account : 'contents.Activate_account → contents
| Proposals : 'contents.Proposals → contents
| Ballot : 'contents.Ballot → contents
| Drain_delegate : 'contents.Drain_delegate → contents
| Failing_noop : string → contents
| Manager_operation : 'contents.Manager_operation → contents

with manager_operation : Set :=
| Reveal : Signature.public_key → manager_operation
| Transaction : 'manager_operation.Transaction → manager_operation
| Origination : 'manager_operation.Origination → manager_operation
| Delegation : option Signature.public_key_hash → manager_operation
| Register_global_constant :
  'manager_operation.Register_global_constant → manager_operation
| Set_deposits_limit : option Tez_repr.t → manager_operation
| Increase_paid_storage :
  'manager_operation.Increase_paid_storage → manager_operation
| Update_consensus_key : Signature.public_key → manager_operation
| Tx_rollup_origination : manager_operation
| Tx_rollup_submit_batch :
  'manager_operation.Tx_rollup_submit_batch → manager_operation
| Tx_rollup_commit : 'manager_operation.Tx_rollup_commit → manager_operation
| Tx_rollup_return_bond :
  'manager_operation.Tx_rollup_return_bond → manager_operation
| Tx_rollup_finalize_commitment :
  'manager_operation.Tx_rollup_finalize_commitment → manager_operation
| Tx_rollup_remove_commitment :
  'manager_operation.Tx_rollup_remove_commitment → manager_operation
| Tx_rollup_rejection :
  'manager_operation.Tx_rollup_rejection → manager_operation
| Tx_rollup_dispatch_tickets :
  'manager_operation.Tx_rollup_dispatch_tickets → manager_operation
| Transfer_ticket : 'manager_operation.Transfer_ticket → manager_operation
| Dal_publish_slot_header :
  'manager_operation.Dal_publish_slot_header → manager_operation
| Sc_rollup_originate :
  'manager_operation.Sc_rollup_originate → manager_operation
| Sc_rollup_add_messages :
  'manager_operation.Sc_rollup_add_messages → manager_operation
| Sc_rollup_cement : 'manager_operation.Sc_rollup_cement → manager_operation
| Sc_rollup_publish : 'manager_operation.Sc_rollup_publish → manager_operation
| Sc_rollup_refute : 'manager_operation.Sc_rollup_refute → manager_operation
| Sc_rollup_timeout : 'manager_operation.Sc_rollup_timeout → manager_operation
| Sc_rollup_execute_outbox_message :
  'manager_operation.Sc_rollup_execute_outbox_message → manager_operation
| Sc_rollup_recover_bond :
  'manager_operation.Sc_rollup_recover_bond → manager_operation
| Zk_rollup_origination :
  'manager_operation.Zk_rollup_origination → manager_operation
| Zk_rollup_publish : 'manager_operation.Zk_rollup_publish → manager_operation
| Zk_rollup_update : 'manager_operation.Zk_rollup_update → manager_operation

where "'protocol_data" :=
  (protocol_data_skeleton contents_list (option Signature.t))
and "'operation" := (operation_skeleton Operation.shell_header 'protocol_data)
and "'contents.Seed_nonce_revelation" :=
  (contents.Seed_nonce_revelation_skeleton Raw_level_repr.t Seed_repr.nonce)
and "'contents.Vdf_revelation" :=
  (contents.Vdf_revelation_skeleton Seed_repr.vdf_solution)
and "'contents.Double_preendorsement_evidence" :=
  (contents.Double_preendorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_endorsement_evidence" :=
  (contents.Double_endorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_baking_evidence" :=
  (contents.Double_baking_evidence_skeleton Block_header_repr.t
    Block_header_repr.t)
and "'contents.Activate_account" :=
  (contents.Activate_account_skeleton
    Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)
    Blinded_public_key_hash.activation_code)
and "'contents.Proposals" :=
  (contents.Proposals_skeleton Signature.public_key_hash int32
    (list Protocol_hash.t))
and "'contents.Ballot" :=
  (contents.Ballot_skeleton Signature.public_key_hash int32 Protocol_hash.t
    Vote_repr.ballot)
and "'contents.Drain_delegate" :=
  (contents.Drain_delegate_skeleton Signature.public_key_hash
    Signature.public_key_hash Signature.public_key_hash)
and "'contents.Manager_operation" :=
  (contents.Manager_operation_skeleton Signature.public_key_hash Tez_repr.tez
    Manager_counter_repr.t manager_operation Gas_limit_repr.Arith.integral Z.t)
and "'manager_operation.Transaction" :=
  (manager_operation.Transaction_skeleton Tez_repr.tez Script_repr.lazy_expr
    Entrypoint_repr.t Contract_repr.t)
and "'manager_operation.Origination" :=
  (manager_operation.Origination_skeleton (option Signature.public_key_hash)
    Script_repr.t Tez_repr.tez)
and "'manager_operation.Register_global_constant" :=
  (manager_operation.Register_global_constant_skeleton Script_repr.lazy_expr)
and "'manager_operation.Increase_paid_storage" :=
  (manager_operation.Increase_paid_storage_skeleton Z.t Contract_hash.t)
and "'manager_operation.Tx_rollup_submit_batch" :=
  (manager_operation.Tx_rollup_submit_batch_skeleton Tx_rollup_repr.t string
    (option Tez_repr.t))
and "'manager_operation.Tx_rollup_commit" :=
  (manager_operation.Tx_rollup_commit_skeleton Tx_rollup_repr.t
    Tx_rollup_commitment_repr.Full.t)
and "'manager_operation.Tx_rollup_return_bond" :=
  (manager_operation.Tx_rollup_return_bond_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_finalize_commitment" :=
  (manager_operation.Tx_rollup_finalize_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_remove_commitment" :=
  (manager_operation.Tx_rollup_remove_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_rejection" :=
  (manager_operation.Tx_rollup_rejection_skeleton Tx_rollup_repr.t
    Tx_rollup_level_repr.t Tx_rollup_message_repr.t int
    Tx_rollup_inbox_repr.Merkle.path Tx_rollup_message_result_hash_repr.t
    Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
    Tx_rollup_message_result_repr.t
    Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
    Tx_rollup_l2_proof.serialized)
and "'manager_operation.Tx_rollup_dispatch_tickets" :=
  (manager_operation.Tx_rollup_dispatch_tickets_skeleton Tx_rollup_repr.t
    Tx_rollup_level_repr.t Context_hash.t int
    Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
    (list Tx_rollup_reveal_repr.t))
and "'manager_operation.Transfer_ticket" :=
  (manager_operation.Transfer_ticket_skeleton Script_repr.lazy_expr
    Script_repr.lazy_expr Contract_repr.t Ticket_amount.t Contract_repr.t
    Entrypoint_repr.t)
and "'manager_operation.Dal_publish_slot_header" :=
  (manager_operation.Dal_publish_slot_header_skeleton Dal_slot_repr.Header.t)
and "'manager_operation.Sc_rollup_originate" :=
  (manager_operation.Sc_rollup_originate_skeleton Sc_rollups.Kind.t string
    string Script_repr.lazy_expr)
and "'manager_operation.Sc_rollup_add_messages" :=
  (manager_operation.Sc_rollup_add_messages_skeleton (list string))
and "'manager_operation.Sc_rollup_cement" :=
  (manager_operation.Sc_rollup_cement_skeleton Sc_rollup_repr.t
    Sc_rollup_commitment_repr.Hash.t)
and "'manager_operation.Sc_rollup_publish" :=
  (manager_operation.Sc_rollup_publish_skeleton Sc_rollup_repr.t
    Sc_rollup_commitment_repr.t)
and "'manager_operation.Sc_rollup_refute" :=
  (manager_operation.Sc_rollup_refute_skeleton Sc_rollup_repr.t
    Signature.public_key_hash (option Sc_rollup_game_repr.refutation))
and "'manager_operation.Sc_rollup_timeout" :=
  (manager_operation.Sc_rollup_timeout_skeleton Sc_rollup_repr.t
    Sc_rollup_game_repr.Index.t)
and "'manager_operation.Sc_rollup_execute_outbox_message" :=
  (manager_operation.Sc_rollup_execute_outbox_message_skeleton Sc_rollup_repr.t
    Sc_rollup_commitment_repr.Hash.t string)
and "'manager_operation.Sc_rollup_recover_bond" :=
  (manager_operation.Sc_rollup_recover_bond_skeleton Sc_rollup_repr.t)
and "'manager_operation.Zk_rollup_origination" :=
  (manager_operation.Zk_rollup_origination_skeleton Plonk.public_parameters
    (Zk_rollup_account_repr.SMap.(Map.S.t) Zk_rollup_account_repr.circuit_info)
    Zk_rollup_state_repr.t int)
and "'manager_operation.Zk_rollup_publish" :=
  (manager_operation.Zk_rollup_publish_skeleton Zk_rollup_repr.t
    (list (Zk_rollup_operation_repr.t × option Zk_rollup_ticket_repr.t)))
and "'manager_operation.Zk_rollup_update" :=
  (manager_operation.Zk_rollup_update_skeleton Zk_rollup_repr.t
    Zk_rollup_update_repr.t).

Module contents.
  Include ConstructorRecords_contents_manager_operation.contents.
  Definition Seed_nonce_revelation := 'contents.Seed_nonce_revelation.
  Definition Vdf_revelation := 'contents.Vdf_revelation.
  Definition Double_preendorsement_evidence :=
    'contents.Double_preendorsement_evidence.
  Definition Double_endorsement_evidence :=
    'contents.Double_endorsement_evidence.
  Definition Double_baking_evidence := 'contents.Double_baking_evidence.
  Definition Activate_account := 'contents.Activate_account.
  Definition Proposals := 'contents.Proposals.
  Definition Ballot := 'contents.Ballot.
  Definition Drain_delegate := 'contents.Drain_delegate.
  Definition Manager_operation := 'contents.Manager_operation.
End contents.
Module manager_operation.
  Include ConstructorRecords_contents_manager_operation.manager_operation.
  Definition Transaction := 'manager_operation.Transaction.
  Definition Origination := 'manager_operation.Origination.
  Definition Register_global_constant :=
    'manager_operation.Register_global_constant.
  Definition Increase_paid_storage := 'manager_operation.Increase_paid_storage.
  Definition Tx_rollup_submit_batch :=
    'manager_operation.Tx_rollup_submit_batch.
  Definition Tx_rollup_commit := 'manager_operation.Tx_rollup_commit.
  Definition Tx_rollup_return_bond := 'manager_operation.Tx_rollup_return_bond.
  Definition Tx_rollup_finalize_commitment :=
    'manager_operation.Tx_rollup_finalize_commitment.
  Definition Tx_rollup_remove_commitment :=
    'manager_operation.Tx_rollup_remove_commitment.
  Definition Tx_rollup_rejection := 'manager_operation.Tx_rollup_rejection.
  Definition Tx_rollup_dispatch_tickets :=
    'manager_operation.Tx_rollup_dispatch_tickets.
  Definition Transfer_ticket := 'manager_operation.Transfer_ticket.
  Definition Dal_publish_slot_header :=
    'manager_operation.Dal_publish_slot_header.
  Definition Sc_rollup_originate := 'manager_operation.Sc_rollup_originate.
  Definition Sc_rollup_add_messages :=
    'manager_operation.Sc_rollup_add_messages.
  Definition Sc_rollup_cement := 'manager_operation.Sc_rollup_cement.
  Definition Sc_rollup_publish := 'manager_operation.Sc_rollup_publish.
  Definition Sc_rollup_refute := 'manager_operation.Sc_rollup_refute.
  Definition Sc_rollup_timeout := 'manager_operation.Sc_rollup_timeout.
  Definition Sc_rollup_execute_outbox_message :=
    'manager_operation.Sc_rollup_execute_outbox_message.
  Definition Sc_rollup_recover_bond :=
    'manager_operation.Sc_rollup_recover_bond.
  Definition Zk_rollup_origination := 'manager_operation.Zk_rollup_origination.
  Definition Zk_rollup_publish := 'manager_operation.Zk_rollup_publish.
  Definition Zk_rollup_update := 'manager_operation.Zk_rollup_update.
End manager_operation.

Definition operation := 'operation.
Definition protocol_data := 'protocol_data.

Definition manager_kind (function_parameter : manager_operation)
  : Kind.manager :=
  match function_parameter with
  | Reveal _ ⇒ Kind.Reveal_manager_kind
  | Transaction _ ⇒ Kind.Transaction_manager_kind
  | Origination _ ⇒ Kind.Origination_manager_kind
  | Delegation _ ⇒ Kind.Delegation_manager_kind
  | Register_global_constant _ ⇒ Kind.Register_global_constant_manager_kind
  | Set_deposits_limit _ ⇒ Kind.Set_deposits_limit_manager_kind
  | Increase_paid_storage _ ⇒ Kind.Increase_paid_storage_manager_kind
  | Update_consensus_key _ ⇒ Kind.Update_consensus_key_manager_kind
  | Tx_rollup_origination ⇒ Kind.Tx_rollup_origination_manager_kind
  | Tx_rollup_submit_batch _ ⇒ Kind.Tx_rollup_submit_batch_manager_kind
  | Tx_rollup_commit _ ⇒ Kind.Tx_rollup_commit_manager_kind
  | Tx_rollup_return_bond _ ⇒ Kind.Tx_rollup_return_bond_manager_kind
  | Tx_rollup_finalize_commitment _ ⇒
    Kind.Tx_rollup_finalize_commitment_manager_kind
  | Tx_rollup_remove_commitment _ ⇒
    Kind.Tx_rollup_remove_commitment_manager_kind
  | Tx_rollup_rejection _ ⇒ Kind.Tx_rollup_rejection_manager_kind
  | Tx_rollup_dispatch_tickets _ ⇒ Kind.Tx_rollup_dispatch_tickets_manager_kind
  | Transfer_ticket _ ⇒ Kind.Transfer_ticket_manager_kind
  | Dal_publish_slot_header _ ⇒ Kind.Dal_publish_slot_header_manager_kind
  | Sc_rollup_originate _ ⇒ Kind.Sc_rollup_originate_manager_kind
  | Sc_rollup_add_messages _ ⇒ Kind.Sc_rollup_add_messages_manager_kind
  | Sc_rollup_cement _ ⇒ Kind.Sc_rollup_cement_manager_kind
  | Sc_rollup_publish _ ⇒ Kind.Sc_rollup_publish_manager_kind
  | Sc_rollup_refute _ ⇒ Kind.Sc_rollup_refute_manager_kind
  | Sc_rollup_timeout _ ⇒ Kind.Sc_rollup_timeout_manager_kind
  | Sc_rollup_execute_outbox_message _ ⇒
    Kind.Sc_rollup_execute_outbox_message_manager_kind
  | Sc_rollup_recover_bond _ ⇒ Kind.Sc_rollup_recover_bond_manager_kind
  | Zk_rollup_origination _ ⇒ Kind.Zk_rollup_origination_manager_kind
  | Zk_rollup_publish _ ⇒ Kind.Zk_rollup_publish_manager_kind
  | Zk_rollup_update _ ⇒ Kind.Zk_rollup_update_manager_kind
  end.

Inductive packed_manager_operation : Set :=
| Manager : manager_operation → packed_manager_operation.

Inductive packed_contents : Set :=
| Contents : contents → packed_contents.

Inductive packed_contents_list : Set :=
| Contents_list : contents_list → packed_contents_list.

Inductive packed_protocol_data : Set :=
| Operation_data : protocol_data → packed_protocol_data.

Module packed_operation.
  Record record : Set := Build {
    shell : Operation.shell_header;
    protocol_data : packed_protocol_data;
  }.
  Definition with_shell shell (r : record) :=
    Build shell r.(protocol_data).
  Definition with_protocol_data protocol_data (r : record) :=
    Build r.(shell) protocol_data.
End packed_operation.
Definition packed_operation := packed_operation.record.

Definition _pack (function_parameter : operation) : packed_operation :=
  let '{|
    operation.shell := shell; operation.protocol_data := protocol_data |} :=
    function_parameter in
  {| packed_operation.shell := shell;
    packed_operation.protocol_data := Operation_data protocol_data; |}.

Fixpoint contents_list_to_list (function_parameter : contents_list)
  : list packed_contents :=
  match function_parameter with
  | Single o_value ⇒ [ Contents o_value ]
  | Cons o_value os ⇒ cons (Contents o_value) (contents_list_to_list os)
  end.

Definition to_list (function_parameter : packed_contents_list)
  : list packed_contents :=
  let 'Contents_list l_value := function_parameter in
  contents_list_to_list l_value.

Fixpoint of_list_internal (function_parameter : list packed_contents)
  : Pervasives.result packed_contents_list string :=
  match function_parameter with
  | [] ⇒ Pervasives.Error "Operation lists should not be empty."
  | cons (Contents o_value) [] ⇒ Pervasives.Ok (Contents_list (Single o_value))
  | cons (Contents o_value) os ⇒
    let? 'Contents_list os := of_list_internal os in
    match (o_value, os) with
    | (Manager_operation _, Single (Manager_operation _)) ⇒
      Pervasives.Ok (Contents_list (Cons o_value os))
    | (Manager_operation _, Cons _ _) ⇒
      Pervasives.Ok (Contents_list (Cons o_value os))
    | _ ⇒
      Pervasives.Error
        "Operation list of length > 1 should only contains manager operations."
    end
  end.

Definition of_list (l_value : list packed_contents) : M? packed_contents_list :=
  match of_list_internal l_value with
  | Pervasives.Ok contents ⇒ Pervasives.Ok contents
  | Pervasives.Error s_value ⇒
    Error_monad.error_value
      (Build_extensible "Contents_list_error" string s_value)
  end.

Definition tx_rollup_operation_tag_offset : int := 150.

Definition tx_rollup_operation_origination_tag : int :=
  tx_rollup_operation_tag_offset +i 0.

Definition tx_rollup_operation_submit_batch_tag : int :=
  tx_rollup_operation_tag_offset +i 1.

Definition tx_rollup_operation_commit_tag : int :=
  tx_rollup_operation_tag_offset +i 2.

Definition tx_rollup_operation_return_bond_tag : int :=
  tx_rollup_operation_tag_offset +i 3.

Definition tx_rollup_operation_finalize_commitment_tag : int :=
  tx_rollup_operation_tag_offset +i 4.

Definition tx_rollup_operation_remove_commitment_tag : int :=
  tx_rollup_operation_tag_offset +i 5.

Definition tx_rollup_operation_rejection_tag : int :=
  tx_rollup_operation_tag_offset +i 6.

Definition tx_rollup_operation_dispatch_tickets_tag : int :=
  tx_rollup_operation_tag_offset +i 7.

Definition transfer_ticket_tag : int := tx_rollup_operation_tag_offset +i 8.

Definition sc_rollup_operation_tag_offset : int := 200.

Definition sc_rollup_operation_origination_tag : int :=
  sc_rollup_operation_tag_offset +i 0.

Definition sc_rollup_operation_add_message_tag : int :=
  sc_rollup_operation_tag_offset +i 1.

Definition sc_rollup_operation_cement_tag : int :=
  sc_rollup_operation_tag_offset +i 2.

Definition sc_rollup_operation_publish_tag : int :=
  sc_rollup_operation_tag_offset +i 3.

Definition sc_rollup_operation_refute_tag : int :=
  sc_rollup_operation_tag_offset +i 4.

Definition sc_rollup_operation_timeout_tag : int :=
  sc_rollup_operation_tag_offset +i 5.

Definition sc_rollup_execute_outbox_message_tag : int :=
  sc_rollup_operation_tag_offset +i 6.

Definition sc_rollup_operation_recover_bond_tag : int :=
  sc_rollup_operation_tag_offset +i 7.

Definition dal_offset : int := 230.

Definition dal_publish_slot_header_tag : int := dal_offset +i 0.

Definition zk_rollup_operation_tag_offset : int := 250.

Definition zk_rollup_operation_create_tag : int :=
  zk_rollup_operation_tag_offset +i 0.

Definition zk_rollup_operation_publish_tag : int :=
  zk_rollup_operation_tag_offset +i 1.

Definition zk_rollup_operation_update_tag : int :=
  zk_rollup_operation_tag_offset +i 2.

Module Encoding.
  Definition case_value {A B : Set}
    (tag : Data_encoding.case_tag) (name : string)
    (args : Data_encoding.encoding A) (proj : B → option A) (inj : A → B)
    : Data_encoding.case B :=
    Data_encoding.case_value (String.capitalize_ascii name) None tag
      (Data_encoding.merge_objs
        (Data_encoding.obj1
          (Data_encoding.req None None "kind" (Data_encoding.constant name)))
        args)
      (fun (x_value : B) ⇒
        match proj x_value with
        | None ⇒ None
        | Some x_value ⇒ Some (tt, x_value)
        end)
      (fun (function_parameter : unit × A) ⇒
        let '(_, x_value) := function_parameter in
        inj x_value).

  Module Manager_operations.

Records for the constructor parameters

    Module ConstructorRecords_case.
      Module case.
        Module MCase.
          Record record {tag name encoding select proj inj : Set} : Set := Build {
            tag : tag;
            name : name;
            encoding : encoding;
            select : select;
            proj : proj;
            inj : inj;
          }.
          Arguments record : clear implicits.
          Definition with_tag {t_tag t_name t_encoding t_select t_proj t_inj}
            tag (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj tag r.(name)
              r.(encoding) r.(select) r.(proj) r.(inj).
          Definition with_name {t_tag t_name t_encoding t_select t_proj t_inj}
            name (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) name
              r.(encoding) r.(select) r.(proj) r.(inj).
          Definition with_encoding
            {t_tag t_name t_encoding t_select t_proj t_inj} encoding
            (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
              encoding r.(select) r.(proj) r.(inj).
          Definition with_select {t_tag t_name t_encoding t_select t_proj t_inj}
            select (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
              r.(encoding) select r.(proj) r.(inj).
          Definition with_proj {t_tag t_name t_encoding t_select t_proj t_inj}
            proj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
              r.(encoding) r.(select) proj r.(inj).
          Definition with_inj {t_tag t_name t_encoding t_select t_proj t_inj}
            inj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
            Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
              r.(encoding) r.(select) r.(proj) inj.
        End MCase.
        Definition MCase_skeleton := MCase.record.
      End case.
    End ConstructorRecords_case.
    Import ConstructorRecords_case.

    Reserved Notation "'case.MCase".

    Inductive case : Set :=
    | MCase : ∀ {a : Set}, 'case.MCase a → case
    
    where "'case.MCase" :=
      (fun (t_a : Set) ⇒ case.MCase_skeleton int string (Data_encoding.t t_a)
        (packed_manager_operation → option manager_operation)
        (manager_operation → t_a) (t_a → manager_operation)).

    Module case.
      Include ConstructorRecords_case.case.
      Definition MCase := 'case.MCase.
    End case.

    Definition reveal_case : case :=
      MCase
        {| case.MCase.tag := 0; case.MCase.name := "reveal";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "public_key"
                Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Reveal _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              | Reveal pkh ⇒ pkh
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj := fun (pkh : Signature.public_key) ⇒ Reveal pkh; |}.

    Definition transaction_case : case :=
      MCase
        {| case.MCase.tag := 1; case.MCase.name := "transaction";
          case.MCase.encoding :=
            Data_encoding.obj3
              (Data_encoding.req None None "amount" Tez_repr.encoding)
              (Data_encoding.req None None "destination" Contract_repr.encoding)
              (Data_encoding.opt None None "parameters"
                (Data_encoding.obj2
                  (Data_encoding.req None None "entrypoint"
                    Entrypoint_repr.smart_encoding)
                  (Data_encoding.req None None "value"
                    Script_repr.lazy_expr_encoding)));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Transaction _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Transaction {|
                  manager_operation.Transaction.amount := amount;
                    manager_operation.Transaction.parameters := parameters;
                    manager_operation.Transaction.entrypoint := entrypoint;
                    manager_operation.Transaction.destination := destination
                    |} ⇒
                let parameters :=
                  if
                    (Script_repr.is_unit_parameter parameters) &&
                    (Entrypoint_repr.is_default entrypoint)
                  then
                    None
                  else
                    Some (entrypoint, parameters) in
                (amount, destination, parameters)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tez_repr.t × Contract_repr.t ×
                option (Entrypoint_repr.t × Script_repr.lazy_expr)) ⇒
              let '(amount, destination, parameters) := function_parameter in
              let '(entrypoint, parameters) :=
                match parameters with
                | None ⇒ (Entrypoint_repr.default, Script_repr.unit_parameter)
                | Some (entrypoint, value_value) ⇒ (entrypoint, value_value)
                end in
              Transaction
                {| manager_operation.Transaction.amount := amount;
                  manager_operation.Transaction.parameters := parameters;
                  manager_operation.Transaction.entrypoint := entrypoint;
                  manager_operation.Transaction.destination := destination; |};
          |}.

    Definition origination_case : case :=
      MCase
        {| case.MCase.tag := 2; case.MCase.name := "origination";
          case.MCase.encoding :=
            Data_encoding.obj3
              (Data_encoding.req None None "balance" Tez_repr.encoding)
              (Data_encoding.opt None None "delegate"
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
              (Data_encoding.req None None "script" Script_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Origination _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Origination {|
                  manager_operation.Origination.delegate := delegate;
                    manager_operation.Origination.script := script;
                    manager_operation.Origination.credit := credit
                    |} ⇒ (credit, delegate, script)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tez_repr.t × option Signature.public_key_hash × Script_repr.t) ⇒
              let '(credit, delegate, script) := function_parameter in
              Origination
                {| manager_operation.Origination.delegate := delegate;
                  manager_operation.Origination.script := script;
                  manager_operation.Origination.credit := credit; |}; |}.

    Definition delegation_case : case :=
      MCase
        {| case.MCase.tag := 3; case.MCase.name := "delegation";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.opt None None "delegate"
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Delegation _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              | Delegation key_value ⇒ key_value
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (key_value : option Signature.public_key_hash) ⇒
              Delegation key_value; |}.

    Definition register_global_constant_case : case :=
      MCase
        {| case.MCase.tag := 4; case.MCase.name := "register_global_constant";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "value"
                Script_repr.lazy_expr_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Register_global_constant _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Register_global_constant {|
                  manager_operation.Register_global_constant.value := value_value
                    |} ⇒ value_value
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (value_value : Script_repr.lazy_expr) ⇒
              Register_global_constant
                {|
                  manager_operation.Register_global_constant.value :=
                    value_value; |}; |}.

    Definition set_deposits_limit_case : case :=
      MCase
        {| case.MCase.tag := 5; case.MCase.name := "set_deposits_limit";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.opt None None "limit" Tez_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Set_deposits_limit _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              | Set_deposits_limit key_value ⇒ key_value
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (key_value : option Tez_repr.t) ⇒ Set_deposits_limit key_value;
          |}.

    Definition increase_paid_storage_case : case :=
      MCase
        {| case.MCase.tag := 9; case.MCase.name := "increase_paid_storage";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "amount" Data_encoding.z_value)
              (Data_encoding.req None None "destination"
                Contract_repr.originated_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Increase_paid_storage _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Increase_paid_storage {|
                  manager_operation.Increase_paid_storage.amount_in_bytes := amount_in_bytes;
                    manager_operation.Increase_paid_storage.destination :=
                      destination
                    |} ⇒ (amount_in_bytes, destination)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter : Z.t × Contract_hash.t) ⇒
              let '(amount_in_bytes, destination) := function_parameter in
              Increase_paid_storage
                {|
                  manager_operation.Increase_paid_storage.amount_in_bytes :=
                    amount_in_bytes;
                  manager_operation.Increase_paid_storage.destination :=
                    destination; |}; |}.

    Definition update_consensus_key_tag : int := 6.

    Definition update_consensus_key_case : case :=
      MCase
        {| case.MCase.tag := update_consensus_key_tag;
          case.MCase.name := "update_consensus_key";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "pk"
                Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Update_consensus_key _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              | Update_consensus_key consensus_pk ⇒ consensus_pk
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (consensus_pk : Signature.public_key) ⇒
              Update_consensus_key consensus_pk; |}.

    Definition tx_rollup_origination_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_origination_tag;
          case.MCase.name := "tx_rollup_origination";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "tx_rollup_origination"
                Data_encoding.unit_value);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager (Tx_rollup_origination as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              | Tx_rollup_origination ⇒ tt
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Tx_rollup_origination; |}.

    Definition tx_rollup_submit_batch_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_submit_batch_tag;
          case.MCase.name := "tx_rollup_submit_batch";
          case.MCase.encoding :=
            Data_encoding.obj3
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
              (Data_encoding.req None None "content"
                (Data_encoding.string' None Data_encoding.Hex))
              (Data_encoding.opt None None "burn_limit" Tez_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_submit_batch _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_submit_batch {|
                  manager_operation.Tx_rollup_submit_batch.tx_rollup := tx_rollup;
                    manager_operation.Tx_rollup_submit_batch.content := content;
                    manager_operation.Tx_rollup_submit_batch.burn_limit :=
                      burn_limit
                    |} ⇒ (tx_rollup, content, burn_limit)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tx_rollup_repr.t × string × option Tez_repr.t) ⇒
              let '(tx_rollup, content, burn_limit) := function_parameter in
              Tx_rollup_submit_batch
                {|
                  manager_operation.Tx_rollup_submit_batch.tx_rollup :=
                    tx_rollup;
                  manager_operation.Tx_rollup_submit_batch.content := content;
                  manager_operation.Tx_rollup_submit_batch.burn_limit :=
                    burn_limit; |}; |}.

    Definition tx_rollup_commit_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_commit_tag;
          case.MCase.name := "tx_rollup_commit";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
              (Data_encoding.req None None "commitment"
                Tx_rollup_commitment_repr.Full.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_commit _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_commit {|
                  manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
                    manager_operation.Tx_rollup_commit.commitment := commitment
                    |} ⇒ (tx_rollup, commitment)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tx_rollup_repr.t × Tx_rollup_commitment_repr.Full.t) ⇒
              let '(tx_rollup, commitment) := function_parameter in
              Tx_rollup_commit
                {| manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
                  manager_operation.Tx_rollup_commit.commitment := commitment;
                  |}; |}.

    Definition tx_rollup_return_bond_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_return_bond_tag;
          case.MCase.name := "tx_rollup_return_bond";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_return_bond _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_return_bond {|
                  manager_operation.Tx_rollup_return_bond.tx_rollup := tx_rollup
                    |} ⇒ tx_rollup
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (tx_rollup : Tx_rollup_repr.t) ⇒
              Tx_rollup_return_bond
                {|
                  manager_operation.Tx_rollup_return_bond.tx_rollup :=
                    tx_rollup; |}; |}.

    Definition tx_rollup_finalize_commitment_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_finalize_commitment_tag;
          case.MCase.name := "tx_rollup_finalize_commitment";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_finalize_commitment _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_finalize_commitment {|
                  manager_operation.Tx_rollup_finalize_commitment.tx_rollup := tx_rollup
                    |} ⇒ tx_rollup
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (tx_rollup : Tx_rollup_repr.t) ⇒
              Tx_rollup_finalize_commitment
                {|
                  manager_operation.Tx_rollup_finalize_commitment.tx_rollup :=
                    tx_rollup; |}; |}.

    Definition tx_rollup_remove_commitment_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_remove_commitment_tag;
          case.MCase.name := "tx_rollup_remove_commitment";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_remove_commitment _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_remove_commitment {|
                  manager_operation.Tx_rollup_remove_commitment.tx_rollup := tx_rollup
                    |} ⇒ tx_rollup
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (tx_rollup : Tx_rollup_repr.t) ⇒
              Tx_rollup_remove_commitment
                {|
                  manager_operation.Tx_rollup_remove_commitment.tx_rollup :=
                    tx_rollup; |}; |}.

    Definition tx_rollup_rejection_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_rejection_tag;
          case.MCase.name := "tx_rollup_rejection";
          case.MCase.encoding :=
            Data_encoding.obj10
              (Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
              (Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
              (Data_encoding.req None None "message"
                Tx_rollup_message_repr.encoding)
              (Data_encoding.req None None "message_position"
                Data_encoding.n_value)
              (Data_encoding.req None None "message_path"
                Tx_rollup_inbox_repr.Merkle.path_encoding)
              (Data_encoding.req None None "message_result_hash"
                Tx_rollup_message_result_hash_repr.encoding)
              (Data_encoding.req None None "message_result_path"
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
              (Data_encoding.req None None "previous_message_result"
                Tx_rollup_message_result_repr.encoding)
              (Data_encoding.req None None "previous_message_result_path"
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
              (Data_encoding.req None None "proof"
                Tx_rollup_l2_proof.serialized_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_rejection _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_rejection {|
                  manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
                    manager_operation.Tx_rollup_rejection.level := level;
                    manager_operation.Tx_rollup_rejection.message := message;
                    manager_operation.Tx_rollup_rejection.message_position :=
                      message_position;
                    manager_operation.Tx_rollup_rejection.message_path :=
                      message_path;
                    manager_operation.Tx_rollup_rejection.message_result_hash :=
                      message_result_hash;
                    manager_operation.Tx_rollup_rejection.message_result_path :=
                      message_result_path;
                    manager_operation.Tx_rollup_rejection.previous_message_result
                      := previous_message_result;
                    manager_operation.Tx_rollup_rejection.previous_message_result_path
                      := previous_message_result_path;
                    manager_operation.Tx_rollup_rejection.proof := proof_value
                    |} ⇒
                (tx_rollup, level, message, (Z.of_int message_position),
                  message_path, message_result_hash, message_result_path,
                  previous_message_result, previous_message_result_path,
                  proof_value)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tx_rollup_repr.t × Tx_rollup_level_repr.level ×
                Tx_rollup_message_repr.t × Z.t ×
                Tx_rollup_inbox_repr.Merkle.path ×
                Tx_rollup_message_result_hash_repr.t ×
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path) ×
                Tx_rollup_message_result_repr.t ×
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path) ×
                Tx_rollup_l2_proof.serialized) ⇒
              let
                '(tx_rollup, level, message, message_position, message_path,
                  message_result_hash, message_result_path,
                  previous_message_result, previous_message_result_path,
                  proof_value) := function_parameter in
              Tx_rollup_rejection
                {| manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
                  manager_operation.Tx_rollup_rejection.level := level;
                  manager_operation.Tx_rollup_rejection.message := message;
                  manager_operation.Tx_rollup_rejection.message_position :=
                    Z.to_int message_position;
                  manager_operation.Tx_rollup_rejection.message_path :=
                    message_path;
                  manager_operation.Tx_rollup_rejection.message_result_hash :=
                    message_result_hash;
                  manager_operation.Tx_rollup_rejection.message_result_path :=
                    message_result_path;
                  manager_operation.Tx_rollup_rejection.previous_message_result
                    := previous_message_result;
                  manager_operation.Tx_rollup_rejection.previous_message_result_path
                    := previous_message_result_path;
                  manager_operation.Tx_rollup_rejection.proof := proof_value; |};
          |}.

    Definition tx_rollup_dispatch_tickets_case : case :=
      MCase
        {| case.MCase.tag := tx_rollup_operation_dispatch_tickets_tag;
          case.MCase.name := "tx_rollup_dispatch_tickets";
          case.MCase.encoding :=
            Data_encoding.obj6
              (Data_encoding.req None None "tx_rollup" Tx_rollup_repr.encoding)
              (Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
              (Data_encoding.req None None "context_hash" Context_hash.encoding)
              (Data_encoding.req None None "message_index" Data_encoding.int31)
              (Data_encoding.req None None "message_result_path"
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
              (Data_encoding.req None None "tickets_info"
                (Data_encoding.list_value None Tx_rollup_reveal_repr.encoding));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_dispatch_tickets _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_dispatch_tickets {|
                  manager_operation.Tx_rollup_dispatch_tickets.tx_rollup := tx_rollup;
                    manager_operation.Tx_rollup_dispatch_tickets.level := level;
                    manager_operation.Tx_rollup_dispatch_tickets.context_hash :=
                      context_hash;
                    manager_operation.Tx_rollup_dispatch_tickets.message_index
                      := message_index;
                    manager_operation.Tx_rollup_dispatch_tickets.message_result_path
                      := message_result_path;
                    manager_operation.Tx_rollup_dispatch_tickets.tickets_info :=
                      tickets_info
                    |} ⇒
                (tx_rollup, level, context_hash, message_index,
                  message_result_path, tickets_info)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tx_rollup_repr.t × Tx_rollup_level_repr.level × Context_hash.t ×
                int × Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path) ×
                list Tx_rollup_reveal_repr.t) ⇒
              let
                '(tx_rollup, level, context_hash, message_index,
                  message_result_path, tickets_info) := function_parameter in
              Tx_rollup_dispatch_tickets
                {|
                  manager_operation.Tx_rollup_dispatch_tickets.tx_rollup :=
                    tx_rollup;
                  manager_operation.Tx_rollup_dispatch_tickets.level := level;
                  manager_operation.Tx_rollup_dispatch_tickets.context_hash :=
                    context_hash;
                  manager_operation.Tx_rollup_dispatch_tickets.message_index :=
                    message_index;
                  manager_operation.Tx_rollup_dispatch_tickets.message_result_path
                    := message_result_path;
                  manager_operation.Tx_rollup_dispatch_tickets.tickets_info :=
                    tickets_info; |}; |}.

    Definition transfer_ticket_case : case :=
      MCase
        {| case.MCase.tag := transfer_ticket_tag;
          case.MCase.name := "transfer_ticket";
          case.MCase.encoding :=
            Data_encoding.obj6
              (Data_encoding.req None None "ticket_contents"
                Script_repr.lazy_expr_encoding)
              (Data_encoding.req None None "ticket_ty"
                Script_repr.lazy_expr_encoding)
              (Data_encoding.req None None "ticket_ticketer"
                Contract_repr.encoding)
              (Data_encoding.req None None "ticket_amount"
                Ticket_amount.encoding)
              (Data_encoding.req None None "destination" Contract_repr.encoding)
              (Data_encoding.req None None "entrypoint"
                Entrypoint_repr.simple_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Transfer_ticket _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Transfer_ticket {|
                  manager_operation.Transfer_ticket.contents := contents;
                    manager_operation.Transfer_ticket.ty := ty_value;
                    manager_operation.Transfer_ticket.ticketer := ticketer;
                    manager_operation.Transfer_ticket.amount := amount;
                    manager_operation.Transfer_ticket.destination := destination;
                    manager_operation.Transfer_ticket.entrypoint := entrypoint
                    |} ⇒
                (contents, ty_value, ticketer, amount, destination, entrypoint)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Script_repr.lazy_expr × Script_repr.lazy_expr × Contract_repr.t ×
                Ticket_amount.t × Contract_repr.t × Entrypoint_repr.t) ⇒
              let
                '(contents, ty_value, ticketer, amount, destination, entrypoint) :=
                function_parameter in
              Transfer_ticket
                {| manager_operation.Transfer_ticket.contents := contents;
                  manager_operation.Transfer_ticket.ty := ty_value;
                  manager_operation.Transfer_ticket.ticketer := ticketer;
                  manager_operation.Transfer_ticket.amount := amount;
                  manager_operation.Transfer_ticket.destination := destination;
                  manager_operation.Transfer_ticket.entrypoint := entrypoint; |};
          |}.

    Definition zk_rollup_origination_case : case :=
      MCase
        {| case.MCase.tag := zk_rollup_operation_create_tag;
          case.MCase.name := "zk_rollup_origination";
          case.MCase.encoding :=
            Data_encoding.obj4
              (Data_encoding.req None None "public_parameters"
                Plonk.public_parameters_encoding)
              (Data_encoding.req None None "circuits_info"
                Zk_rollup_account_repr.circuits_info_encoding)
              (Data_encoding.req None None "init_state"
                Zk_rollup_state_repr.encoding)
              (Data_encoding.req None None "nb_ops" Data_encoding.int31);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Zk_rollup_origination _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Zk_rollup_origination {|
                  manager_operation.Zk_rollup_origination.public_parameters := public_parameters;
                    manager_operation.Zk_rollup_origination.circuits_info :=
                      circuits_info;
                    manager_operation.Zk_rollup_origination.init_state :=
                      init_state;
                    manager_operation.Zk_rollup_origination.nb_ops := nb_ops
                    |} ⇒ (public_parameters, circuits_info, init_state, nb_ops)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Plonk.public_parameters ×
                Zk_rollup_account_repr.SMap.(Map.S.t)
                  Zk_rollup_account_repr.circuit_info × Zk_rollup_state_repr.t ×
                int) ⇒
              let '(public_parameters, circuits_info, init_state, nb_ops) :=
                function_parameter in
              Zk_rollup_origination
                {|
                  manager_operation.Zk_rollup_origination.public_parameters :=
                    public_parameters;
                  manager_operation.Zk_rollup_origination.circuits_info :=
                    circuits_info;
                  manager_operation.Zk_rollup_origination.init_state :=
                    init_state;
                  manager_operation.Zk_rollup_origination.nb_ops := nb_ops; |};
          |}.

    Definition zk_rollup_publish_case : case :=
      MCase
        {| case.MCase.tag := zk_rollup_operation_publish_tag;
          case.MCase.name := "zk_rollup_publish";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "zk_rollup"
                Zk_rollup_repr.Address.encoding)
              (Data_encoding.req None None "op"
                (Data_encoding.list_value None
                  (Data_encoding.tup2 Zk_rollup_operation_repr.encoding
                    (Data_encoding.option_value Zk_rollup_ticket_repr.encoding))));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Zk_rollup_publish _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Zk_rollup_publish {|
                  manager_operation.Zk_rollup_publish.zk_rollup := zk_rollup;
                    manager_operation.Zk_rollup_publish.ops := ops
                    |} ⇒ (zk_rollup, ops)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Zk_rollup_repr.Address.t ×
                list
                  (Zk_rollup_operation_repr.t × option Zk_rollup_ticket_repr.t))
              ⇒
              let '(zk_rollup, ops) := function_parameter in
              Zk_rollup_publish
                {| manager_operation.Zk_rollup_publish.zk_rollup := zk_rollup;
                  manager_operation.Zk_rollup_publish.ops := ops; |}; |}.

    Definition zk_rollup_update_case : case :=
      MCase
        {| case.MCase.tag := zk_rollup_operation_update_tag;
          case.MCase.name := "zk_rollup_update";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "zk_rollup"
                Zk_rollup_repr.Address.encoding)
              (Data_encoding.req None None "update"
                Zk_rollup_update_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Zk_rollup_update _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Zk_rollup_update {|
                  manager_operation.Zk_rollup_update.zk_rollup := zk_rollup;
                    manager_operation.Zk_rollup_update.update := update
                    |} ⇒ (zk_rollup, update)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Zk_rollup_repr.Address.t × Zk_rollup_update_repr.t) ⇒
              let '(zk_rollup, update) := function_parameter in
              Zk_rollup_update
                {| manager_operation.Zk_rollup_update.zk_rollup := zk_rollup;
                  manager_operation.Zk_rollup_update.update := update; |}; |}.

    Definition sc_rollup_originate_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_origination_tag;
          case.MCase.name := "sc_rollup_originate";
          case.MCase.encoding :=
            Data_encoding.obj4
              (Data_encoding.req None None "pvm_kind" Sc_rollups.Kind.encoding)
              (Data_encoding.req None None "boot_sector"
                (Data_encoding.string' None Data_encoding.Hex))
              (Data_encoding.req None None "origination_proof"
                (Data_encoding.string' None Data_encoding.Hex))
              (Data_encoding.req None None "parameters_ty"
                Script_repr.lazy_expr_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_originate _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_originate {|
                  manager_operation.Sc_rollup_originate.kind := kind_value;
                    manager_operation.Sc_rollup_originate.boot_sector :=
                      boot_sector;
                    manager_operation.Sc_rollup_originate.origination_proof :=
                      origination_proof;
                    manager_operation.Sc_rollup_originate.parameters_ty :=
                      parameters_ty
                    |} ⇒
                (kind_value, boot_sector, origination_proof, parameters_ty)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollups.Kind.t × string × string × Script_repr.lazy_expr) ⇒
              let
                '(kind_value, boot_sector, origination_proof, parameters_ty) :=
                function_parameter in
              Sc_rollup_originate
                {| manager_operation.Sc_rollup_originate.kind := kind_value;
                  manager_operation.Sc_rollup_originate.boot_sector :=
                    boot_sector;
                  manager_operation.Sc_rollup_originate.origination_proof :=
                    origination_proof;
                  manager_operation.Sc_rollup_originate.parameters_ty :=
                    parameters_ty; |}; |}.

    Definition dal_publish_slot_header_case : case :=
      MCase
        {| case.MCase.tag := dal_publish_slot_header_tag;
          case.MCase.name := "dal_publish_slot_header";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "slot_header"
                Dal_slot_repr.Header.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Dal_publish_slot_header _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Dal_publish_slot_header {|
                  manager_operation.Dal_publish_slot_header.slot_header := slot_header
                    |} ⇒ slot_header
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (slot_header : Dal_slot_repr.Header.t) ⇒
              Dal_publish_slot_header
                {|
                  manager_operation.Dal_publish_slot_header.slot_header :=
                    slot_header; |}; |}.

    Definition sc_rollup_add_messages_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_add_message_tag;
          case.MCase.name := "sc_rollup_add_messages";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "message"
                (Data_encoding.list_value None
                  (Data_encoding.string' None Data_encoding.Hex)));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_add_messages _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_add_messages {|
                  manager_operation.Sc_rollup_add_messages.messages := messages
                    |} ⇒ messages
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (messages : list string) ⇒
              Sc_rollup_add_messages
                {|
                  manager_operation.Sc_rollup_add_messages.messages := messages;
                  |}; |}.

    Definition sc_rollup_cement_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_cement_tag;
          case.MCase.name := "sc_rollup_cement";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "commitment"
                Sc_rollup_commitment_repr.Hash.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_cement _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_cement {|
                  manager_operation.Sc_rollup_cement.rollup := rollup;
                    manager_operation.Sc_rollup_cement.commitment := commitment
                    |} ⇒ (rollup, commitment)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollup_repr.t × Sc_rollup_commitment_repr.Hash.t) ⇒
              let '(rollup, commitment) := function_parameter in
              Sc_rollup_cement
                {| manager_operation.Sc_rollup_cement.rollup := rollup;
                  manager_operation.Sc_rollup_cement.commitment := commitment;
                  |}; |}.

    Definition sc_rollup_publish_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_publish_tag;
          case.MCase.name := "sc_rollup_publish";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "commitment"
                Sc_rollup_commitment_repr.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_publish _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_publish {|
                  manager_operation.Sc_rollup_publish.rollup := rollup;
                    manager_operation.Sc_rollup_publish.commitment := commitment
                    |} ⇒ (rollup, commitment)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollup_repr.t × Sc_rollup_commitment_repr.t) ⇒
              let '(rollup, commitment) := function_parameter in
              Sc_rollup_publish
                {| manager_operation.Sc_rollup_publish.rollup := rollup;
                  manager_operation.Sc_rollup_publish.commitment := commitment;
                  |}; |}.

    Definition sc_rollup_refute_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_refute_tag;
          case.MCase.name := "sc_rollup_refute";
          case.MCase.encoding :=
            Data_encoding.obj3
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "opponent"
                Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
              (Data_encoding.opt None None "refutation"
                Sc_rollup_game_repr.refutation_encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_refute _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_refute {|
                  manager_operation.Sc_rollup_refute.rollup := rollup;
                    manager_operation.Sc_rollup_refute.opponent := opponent;
                    manager_operation.Sc_rollup_refute.refutation := refutation
                    |} ⇒ (rollup, opponent, refutation)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollup_repr.t × Signature.public_key_hash ×
                option Sc_rollup_game_repr.refutation) ⇒
              let '(rollup, opponent, refutation) := function_parameter in
              Sc_rollup_refute
                {| manager_operation.Sc_rollup_refute.rollup := rollup;
                  manager_operation.Sc_rollup_refute.opponent := opponent;
                  manager_operation.Sc_rollup_refute.refutation := refutation;
                  |}; |}.

    Definition sc_rollup_timeout_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_timeout_tag;
          case.MCase.name := "sc_rollup_timeout";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "stakers"
                Sc_rollup_game_repr.Index.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_timeout _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_timeout {|
                  manager_operation.Sc_rollup_timeout.rollup := rollup;
                    manager_operation.Sc_rollup_timeout.stakers := stakers
                    |} ⇒ (rollup, stakers)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollup_repr.t × Sc_rollup_game_repr.Index.t) ⇒
              let '(rollup, stakers) := function_parameter in
              Sc_rollup_timeout
                {| manager_operation.Sc_rollup_timeout.rollup := rollup;
                  manager_operation.Sc_rollup_timeout.stakers := stakers; |}; |}.

    Definition sc_rollup_execute_outbox_message_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_execute_outbox_message_tag;
          case.MCase.name := "sc_rollup_execute_outbox_message";
          case.MCase.encoding :=
            Data_encoding.obj3
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "cemented_commitment"
                Sc_rollup_commitment_repr.Hash.encoding)
              (Data_encoding.req None None "output_proof"
                (Data_encoding.string' None Data_encoding.Hex));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_execute_outbox_message _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_execute_outbox_message {|
                  manager_operation.Sc_rollup_execute_outbox_message.rollup := rollup;
                    manager_operation.Sc_rollup_execute_outbox_message.cemented_commitment
                      := cemented_commitment;
                    manager_operation.Sc_rollup_execute_outbox_message.output_proof
                      := output_proof
                    |} ⇒ (rollup, cemented_commitment, output_proof)
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Sc_rollup_repr.t × Sc_rollup_commitment_repr.Hash.t × string) ⇒
              let '(rollup, cemented_commitment, output_proof) :=
                function_parameter in
              Sc_rollup_execute_outbox_message
                {|
                  manager_operation.Sc_rollup_execute_outbox_message.rollup :=
                    rollup;
                  manager_operation.Sc_rollup_execute_outbox_message.cemented_commitment
                    := cemented_commitment;
                  manager_operation.Sc_rollup_execute_outbox_message.output_proof
                    := output_proof; |}; |}.

    Definition sc_rollup_recover_bond_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_recover_bond_tag;
          case.MCase.name := "sc_rollup_recover_bond";
          case.MCase.encoding :=
            Data_encoding.obj1
              (Data_encoding.req None None "rollup"
                Sc_rollup_repr.Address.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_recover_bond _) as op) ⇒ Some op
              | _ ⇒ None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_recover_bond {|
                  manager_operation.Sc_rollup_recover_bond.sc_rollup := sc_rollup
                    |} ⇒ sc_rollup
              | _ ⇒ unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (sc_rollup : Sc_rollup_repr.Address.t) ⇒
              Sc_rollup_recover_bond
                {|
                  manager_operation.Sc_rollup_recover_bond.sc_rollup :=
                    sc_rollup; |}; |}.
  End Manager_operations.

Records for the constructor parameters

  Module ConstructorRecords_case.
    Module case.
      Module Case.
        Record record {tag name encoding select proj inj : Set} : Set := Build {
          tag : tag;
          name : name;
          encoding : encoding;
          select : select;
          proj : proj;
          inj : inj;
        }.
        Arguments record : clear implicits.
        Definition with_tag {t_tag t_name t_encoding t_select t_proj t_inj} tag
          (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj tag r.(name)
            r.(encoding) r.(select) r.(proj) r.(inj).
        Definition with_name {t_tag t_name t_encoding t_select t_proj t_inj}
          name (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) name
            r.(encoding) r.(select) r.(proj) r.(inj).
        Definition with_encoding {t_tag t_name t_encoding t_select t_proj t_inj}
          encoding (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
            encoding r.(select) r.(proj) r.(inj).
        Definition with_select {t_tag t_name t_encoding t_select t_proj t_inj}
          select (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
            r.(encoding) select r.(proj) r.(inj).
        Definition with_proj {t_tag t_name t_encoding t_select t_proj t_inj}
          proj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
            r.(encoding) r.(select) proj r.(inj).
        Definition with_inj {t_tag t_name t_encoding t_select t_proj t_inj} inj
          (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
          Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
            r.(encoding) r.(select) r.(proj) inj.
      End Case.
      Definition Case_skeleton := Case.record.
    End case.
  End ConstructorRecords_case.
  Import ConstructorRecords_case.

  Reserved Notation "'case.Case".

  Inductive case (b : Set) : Set :=
  | Case : ∀ {a : Set}, 'case.Case a → case b
  
  where "'case.Case" :=
    (fun (t_a : Set) ⇒ case.Case_skeleton int string (Data_encoding.t t_a)
      (packed_contents → option contents) (contents → t_a) (t_a → contents)).

  Module case.
    Include ConstructorRecords_case.case.
    Definition Case := 'case.Case.
  End case.

  Arguments Case {_ _}.

  Definition preendorsement_case : case Kind.preendorsement :=
    Case
      {| case.Case.tag := 20; case.Case.name := "preendorsement";
        case.Case.encoding := consensus_content_encoding;
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Preendorsement _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            | Preendorsement preendorsement ⇒ preendorsement
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (preendorsement : consensus_content) ⇒
            Preendorsement preendorsement; |}.

  Definition preendorsement_encoding : Data_encoding.encoding operation :=
    let make {A : Set} (function_parameter : case A)
      : Data_encoding.case contents :=
      let
        'Case {|
          case.Case.tag := tag;
            case.Case.name := name;
            case.Case.encoding := encoding;
            case.Case.select := _;
            case.Case.proj := proj;
            case.Case.inj := inj
            |} := function_parameter in
      let 'existT _ __Case_'a [inj, proj, encoding, name, tag] :=
        existT (A := Set)
          (fun __Case_'a ⇒
            [__Case_'a → contents ** contents → __Case_'a **
              Data_encoding.t __Case_'a ** string ** int]) _
          [inj, proj, encoding, name, tag] in
      case_value (Data_encoding.Tag tag) name encoding
        (fun (o_value : contents) ⇒ Some (proj o_value))
        (fun (x_value : __Case_'a) ⇒ inj x_value) in
    let to_list (function_parameter : contents_list) : contents :=
      match function_parameter with
      | Single o_value ⇒ o_value
      | _ ⇒ unreachable_gadt_branch
      end in
    let of_list (o_value : contents) : contents_list :=
      Single o_value in
    Data_encoding.def "inlined.preendorsement" None None
      (Data_encoding.conv
        (fun (function_parameter : operation) ⇒
          let '{|
            operation.shell := shell;
              operation.protocol_data := {|
                protocol_data.contents := contents;
                  protocol_data.signature := signature
                  |}
              |} := function_parameter in
          (shell, (contents, signature)))
        (fun (function_parameter :
          Operation.shell_header × (contents_list × option Signature.t)) ⇒
          let '(shell, (contents, signature)) := function_parameter in
          {| operation.shell := shell;
            operation.protocol_data :=
              {| protocol_data.contents := contents;
                protocol_data.signature := signature; |}; |}) None
        (Data_encoding.merge_objs Operation.shell_header_encoding
          (Data_encoding.obj2
            (Data_encoding.req None None "operations"
              (Data_encoding.conv to_list of_list None
                (Data_encoding.def "inlined.preendorsement.contents" None None
                  (Data_encoding.union None [ make preendorsement_case ]))))
            (Data_encoding.varopt None None "signature" Signature.encoding)))).

  Definition endorsement_case : case Kind.endorsement :=
    Case
      {| case.Case.tag := 21; case.Case.name := "endorsement";
        case.Case.encoding :=
          Data_encoding.obj4
            (Data_encoding.req None None "slot" Slot_repr.encoding)
            (Data_encoding.req None None "level" Raw_level_repr.encoding)
            (Data_encoding.req None None "round" Round_repr.encoding)
            (Data_encoding.req None None "block_payload_hash"
              Block_payload_hash.encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Endorsement _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            | Endorsement consensus_content ⇒
              (consensus_content.(consensus_content.slot),
                consensus_content.(consensus_content.level),
                consensus_content.(consensus_content.round),
                consensus_content.(consensus_content.block_payload_hash))
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Slot_repr.t × Raw_level_repr.raw_level × Round_repr.t ×
              Block_payload_hash.t) ⇒
            let '(slot, level, round, block_payload_hash) := function_parameter
              in
            Endorsement
              {| consensus_content.slot := slot;
                consensus_content.level := level;
                consensus_content.round := round;
                consensus_content.block_payload_hash := block_payload_hash; |};
        |}.

  Definition endorsement_encoding : Data_encoding.encoding operation :=
    let make {A : Set} (function_parameter : case A)
      : Data_encoding.case contents :=
      let
        'Case {|
          case.Case.tag := tag;
            case.Case.name := name;
            case.Case.encoding := encoding;
            case.Case.select := _;
            case.Case.proj := proj;
            case.Case.inj := inj
            |} := function_parameter in
      let 'existT _ __Case_'a [inj, proj, encoding, name, tag] :=
        existT (A := Set)
          (fun __Case_'a ⇒
            [__Case_'a → contents ** contents → __Case_'a **
              Data_encoding.t __Case_'a ** string ** int]) _
          [inj, proj, encoding, name, tag] in
      case_value (Data_encoding.Tag tag) name encoding
        (fun (o_value : contents) ⇒ Some (proj o_value))
        (fun (x_value : __Case_'a) ⇒ inj x_value) in
    let to_list (function_parameter : contents_list) : contents :=
      match function_parameter with
      | Single o_value ⇒ o_value
      | _ ⇒ unreachable_gadt_branch
      end in
    let of_list (o_value : contents) : contents_list :=
      Single o_value in
    Data_encoding.def "inlined.endorsement" None None
      (Data_encoding.conv
        (fun (function_parameter : operation) ⇒
          let '{|
            operation.shell := shell;
              operation.protocol_data := {|
                protocol_data.contents := contents;
                  protocol_data.signature := signature
                  |}
              |} := function_parameter in
          (shell, (contents, signature)))
        (fun (function_parameter :
          Operation.shell_header × (contents_list × option Signature.t)) ⇒
          let '(shell, (contents, signature)) := function_parameter in
          {| operation.shell := shell;
            operation.protocol_data :=
              {| protocol_data.contents := contents;
                protocol_data.signature := signature; |}; |}) None
        (Data_encoding.merge_objs Operation.shell_header_encoding
          (Data_encoding.obj2
            (Data_encoding.req None None "operations"
              (Data_encoding.conv to_list of_list None
                (Data_encoding.def "inlined.endorsement_mempool.contents" None
                  None (Data_encoding.union None [ make endorsement_case ]))))
            (Data_encoding.varopt None None "signature" Signature.encoding)))).

  Definition dal_attestation_encoding
    : Data_encoding.encoding
      (Signature.public_key_hash × Dal_attestation_repr.t ×
        Raw_level_repr.raw_level) :=
    Data_encoding.obj3
      (Data_encoding.req None None "attestor"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "attestation" Dal_attestation_repr.encoding)
      (Data_encoding.req None None "level" Raw_level_repr.encoding).

  Definition dal_attestation_case : case Kind.dal_attestation :=
    Case
      {| case.Case.tag := 22; case.Case.name := "dal_attestation";
        case.Case.encoding := dal_attestation_encoding;
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Dal_attestation _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Dal_attestation {|
                Dal_attestation_repr.operation.attestor := attestor;
                  Dal_attestation_repr.operation.attestation := attestation;
                  Dal_attestation_repr.operation.level := level
                  |} ⇒ (attestor, attestation, level)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Signature.public_key_hash × Dal_attestation_repr.t ×
              Raw_level_repr.raw_level) ⇒
            let '(attestor, attestation, level) := function_parameter in
            Dal_attestation
              {| Dal_attestation_repr.operation.attestor := attestor;
                Dal_attestation_repr.operation.attestation := attestation;
                Dal_attestation_repr.operation.level := level; |}; |}.

  Definition seed_nonce_revelation_case : case Kind.seed_nonce_revelation :=
    Case
      {| case.Case.tag := 1; case.Case.name := "seed_nonce_revelation";
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.req None None "level" Raw_level_repr.encoding)
            (Data_encoding.req None None "nonce" Seed_repr.nonce_encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Seed_nonce_revelation _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Seed_nonce_revelation {|
                contents.Seed_nonce_revelation.level := level;
                  contents.Seed_nonce_revelation.nonce := nonce_value
                  |} ⇒ (level, nonce_value)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter : Raw_level_repr.raw_level × Seed_repr.nonce)
            ⇒
            let '(level, nonce_value) := function_parameter in
            Seed_nonce_revelation
              {| contents.Seed_nonce_revelation.level := level;
                contents.Seed_nonce_revelation.nonce := nonce_value; |}; |}.

  Definition vdf_revelation_case : case Kind.vdf_revelation :=
    Case
      {| case.Case.tag := 8; case.Case.name := "vdf_revelation";
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.req None None "solution"
              Seed_repr.vdf_solution_encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Vdf_revelation _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            | Vdf_revelation {| contents.Vdf_revelation.solution := solution |}
              ⇒ solution
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (solution : Seed_repr.vdf_solution) ⇒
            Vdf_revelation {| contents.Vdf_revelation.solution := solution; |};
        |}.

  Definition double_preendorsement_evidence_case
    : case Kind.double_preendorsement_evidence :=
    Case
      {| case.Case.tag := 7; case.Case.name := "double_preendorsement_evidence";
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.req None None "op1"
              (Data_encoding.dynamic_size None preendorsement_encoding))
            (Data_encoding.req None None "op2"
              (Data_encoding.dynamic_size None preendorsement_encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Double_preendorsement_evidence _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Double_preendorsement_evidence {|
                contents.Double_preendorsement_evidence.op1 := op1;
                  contents.Double_preendorsement_evidence.op2 := op2
                  |} ⇒ (op1, op2)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter : operation × operation) ⇒
            let '(op1, op2) := function_parameter in
            Double_preendorsement_evidence
              {| contents.Double_preendorsement_evidence.op1 := op1;
                contents.Double_preendorsement_evidence.op2 := op2; |}; |}.

  Definition double_endorsement_evidence_case
    : case Kind.double_endorsement_evidence :=
    Case
      {| case.Case.tag := 2; case.Case.name := "double_endorsement_evidence";
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.req None None "op1"
              (Data_encoding.dynamic_size None endorsement_encoding))
            (Data_encoding.req None None "op2"
              (Data_encoding.dynamic_size None endorsement_encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Double_endorsement_evidence _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Double_endorsement_evidence {|
                contents.Double_endorsement_evidence.op1 := op1;
                  contents.Double_endorsement_evidence.op2 := op2
                  |} ⇒ (op1, op2)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter : operation × operation) ⇒
            let '(op1, op2) := function_parameter in
            Double_endorsement_evidence
              {| contents.Double_endorsement_evidence.op1 := op1;
                contents.Double_endorsement_evidence.op2 := op2; |}; |}.

  Definition double_baking_evidence_case : case Kind.double_baking_evidence :=
    Case
      {| case.Case.tag := 3; case.Case.name := "double_baking_evidence";
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.req None None "bh1"
              (Data_encoding.dynamic_size None Block_header_repr.encoding))
            (Data_encoding.req None None "bh2"
              (Data_encoding.dynamic_size None Block_header_repr.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Double_baking_evidence _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Double_baking_evidence {|
                contents.Double_baking_evidence.bh1 := bh1;
                  contents.Double_baking_evidence.bh2 := bh2
                  |} ⇒ (bh1, bh2)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Block_header_repr.block_header × Block_header_repr.block_header) ⇒
            let '(bh1, bh2) := function_parameter in
            Double_baking_evidence
              {| contents.Double_baking_evidence.bh1 := bh1;
                contents.Double_baking_evidence.bh2 := bh2; |}; |}.

  Definition activate_account_case : case Kind.activate_account :=
    Case
      {| case.Case.tag := 4; case.Case.name := "activate_account";
        case.Case.encoding :=
          Data_encoding.obj2
            (Data_encoding.req None None "pkh"
              Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "secret"
              Blinded_public_key_hash.activation_code_encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Activate_account _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Activate_account {|
                contents.Activate_account.id := id;
                  contents.Activate_account.activation_code := activation_code
                  |} ⇒ (id, activation_code)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) ×
              Blinded_public_key_hash.activation_code) ⇒
            let '(id, activation_code) := function_parameter in
            Activate_account
              {| contents.Activate_account.id := id;
                contents.Activate_account.activation_code := activation_code; |};
        |}.

  Definition proposals_case : case Kind.proposals :=
    Case
      {| case.Case.tag := 5; case.Case.name := "proposals";
        case.Case.encoding :=
          Data_encoding.obj3
            (Data_encoding.req None None "source"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "period" Data_encoding.int32_value)
            (Data_encoding.req None None "proposals"
              (Data_encoding.list_value
                (Some Constants_repr.max_proposals_per_delegate)
                Protocol_hash.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Proposals _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Proposals {|
                contents.Proposals.source := source;
                  contents.Proposals.period := period;
                  contents.Proposals.proposals := proposals
                  |} ⇒ (source, period, proposals)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Signature.public_key_hash × int32 × list Protocol_hash.t) ⇒
            let '(source, period, proposals) := function_parameter in
            Proposals
              {| contents.Proposals.source := source;
                contents.Proposals.period := period;
                contents.Proposals.proposals := proposals; |}; |}.

  Definition ballot_case : case Kind.ballot :=
    Case
      {| case.Case.tag := 6; case.Case.name := "ballot";
        case.Case.encoding :=
          Data_encoding.obj4
            (Data_encoding.req None None "source"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "period" Data_encoding.int32_value)
            (Data_encoding.req None None "proposal" Protocol_hash.encoding)
            (Data_encoding.req None None "ballot" Vote_repr.ballot_encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Ballot _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Ballot {|
                contents.Ballot.source := source;
                  contents.Ballot.period := period;
                  contents.Ballot.proposal := proposal;
                  contents.Ballot.ballot := ballot
                  |} ⇒ (source, period, proposal, ballot)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Signature.public_key_hash × int32 × Protocol_hash.t ×
              Vote_repr.ballot) ⇒
            let '(source, period, proposal, ballot) := function_parameter in
            Ballot
              {| contents.Ballot.source := source;
                contents.Ballot.period := period;
                contents.Ballot.proposal := proposal;
                contents.Ballot.ballot := ballot; |}; |}.

  Definition drain_delegate_case : case Kind.drain_delegate :=
    Case
      {| case.Case.tag := 9; case.Case.name := "drain_delegate";
        case.Case.encoding :=
          Data_encoding.obj3
            (Data_encoding.req None None "consensus_key"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "delegate"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
            (Data_encoding.req None None "destination"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Drain_delegate _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              Drain_delegate {|
                contents.Drain_delegate.consensus_key := consensus_key;
                  contents.Drain_delegate.delegate := delegate;
                  contents.Drain_delegate.destination := destination
                  |} ⇒ (consensus_key, delegate, destination)
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            Signature.public_key_hash × Signature.public_key_hash ×
              Signature.public_key_hash) ⇒
            let '(consensus_key, delegate, destination) := function_parameter in
            Drain_delegate
              {| contents.Drain_delegate.consensus_key := consensus_key;
                contents.Drain_delegate.delegate := delegate;
                contents.Drain_delegate.destination := destination; |}; |}.

  Definition failing_noop_case : case Kind.failing_noop :=
    Case
      {| case.Case.tag := 17; case.Case.name := "failing_noop";
        case.Case.encoding :=
          Data_encoding.obj1
            (Data_encoding.req None None "arbitrary"
              (Data_encoding.string' None Data_encoding.Hex));
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            | Contents ((Failing_noop _) as op) ⇒ Some op
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            | Failing_noop message ⇒ message
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj := fun (message : string) ⇒ Failing_noop message; |}.

  Definition manager_encoding
    : Data_encoding.encoding
      (Signature.public_key_hash × Tez_repr.t × Manager_counter_repr.t ×
        Gas_limit_repr.Arith.integral × Z.t) :=
    Data_encoding.obj5
      (Data_encoding.req None None "source"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "fee" Tez_repr.encoding)
      (Data_encoding.req None None "counter"
        Manager_counter_repr.encoding_for_operation)
      (Data_encoding.req None None "gas_limit"
        (Data_encoding.check_size 10 Gas_limit_repr.Arith.n_integral_encoding))
      (Data_encoding.req None None "storage_limit"
        (Data_encoding.check_size 10 Data_encoding.n_value)).

  Definition extract (function_parameter : contents)
    : Signature.public_key_hash × Tez_repr.tez × Manager_counter_repr.t ×
      Gas_limit_repr.Arith.integral × Z.t :=
    match function_parameter with
    |
      Manager_operation {|
        contents.Manager_operation.source := source;
          contents.Manager_operation.fee := fee;
          contents.Manager_operation.counter := counter;
          contents.Manager_operation.operation := _;
          contents.Manager_operation.gas_limit := gas_limit;
          contents.Manager_operation.storage_limit := storage_limit
          |} ⇒ (source, fee, counter, gas_limit, storage_limit)
    | _ ⇒ unreachable_gadt_branch
    end.

  Definition rebuild
    (function_parameter :
      Signature.public_key_hash × Tez_repr.tez × Manager_counter_repr.t ×
        Gas_limit_repr.Arith.integral × Z.t) : manager_operation → contents :=
    let '(source, fee, counter, gas_limit, storage_limit) := function_parameter
      in
    fun (operation : manager_operation) ⇒
      Manager_operation
        {| contents.Manager_operation.source := source;
          contents.Manager_operation.fee := fee;
          contents.Manager_operation.counter := counter;
          contents.Manager_operation.operation := operation;
          contents.Manager_operation.gas_limit := gas_limit;
          contents.Manager_operation.storage_limit := storage_limit; |}.

  Definition make_manager_case
    (tag : int) (function_parameter : Manager_operations.case)
    : case Kind.manager :=
    let 'Manager_operations.MCase mcase := function_parameter in
    let 'existT _ __MCase_'a mcase :=
      existT (A := Set)
        (fun __MCase_'a ⇒ Manager_operations.case.MCase __MCase_'a) _ mcase in
    Case
      {| case.Case.tag := tag;
        case.Case.name := mcase.(Manager_operations.case.MCase.name);
        case.Case.encoding :=
          Data_encoding.merge_objs manager_encoding
            mcase.(Manager_operations.case.MCase.encoding);
        case.Case.select :=
          fun (function_parameter : packed_contents) ⇒
            match function_parameter with
            |
              Contents
                (Manager_operation
                  ({| contents.Manager_operation.operation := operation |} as op))
              ⇒
              match
                mcase.(Manager_operations.case.MCase.select) (Manager operation)
                with
              | None ⇒ None
              | Some operation ⇒
                Some
                  (Manager_operation
                    (contents.Manager_operation.with_operation operation op))
              end
            | _ ⇒ None
            end;
        case.Case.proj :=
          fun (function_parameter : contents) ⇒
            match function_parameter with
            |
              (Manager_operation {|
                contents.Manager_operation.operation := operation |}) as op
              ⇒
              ((extract op),
                (mcase.(Manager_operations.case.MCase.proj) operation))
            | _ ⇒ unreachable_gadt_branch
            end;
        case.Case.inj :=
          fun (function_parameter :
            (Signature.public_key_hash × Tez_repr.tez × Manager_counter_repr.t ×
              Gas_limit_repr.Arith.integral × Z.t) × __MCase_'a) ⇒
            let '(op, contents) := function_parameter in
            rebuild op (mcase.(Manager_operations.case.MCase.inj) contents); |}.

  Definition reveal_case : case Kind.manager :=
    make_manager_case 107 Manager_operations.reveal_case.

  Definition transaction_case : case Kind.manager :=
    make_manager_case 108 Manager_operations.transaction_case.

  Definition origination_case : case Kind.manager :=
    make_manager_case 109 Manager_operations.origination_case.

  Definition delegation_case : case Kind.manager :=
    make_manager_case 110 Manager_operations.delegation_case.

  Definition register_global_constant_case : case Kind.manager :=
    make_manager_case 111 Manager_operations.register_global_constant_case.

  Definition set_deposits_limit_case : case Kind.manager :=
    make_manager_case 112 Manager_operations.set_deposits_limit_case.

  Definition increase_paid_storage_case : case Kind.manager :=
    make_manager_case 113 Manager_operations.increase_paid_storage_case.

  Definition update_consensus_key_case : case Kind.manager :=
    make_manager_case 114 Manager_operations.update_consensus_key_case.

  Definition tx_rollup_origination_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_tag_offset
      Manager_operations.tx_rollup_origination_case.

  Definition tx_rollup_submit_batch_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_submit_batch_tag
      Manager_operations.tx_rollup_submit_batch_case.

  Definition tx_rollup_commit_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_commit_tag
      Manager_operations.tx_rollup_commit_case.

  Definition tx_rollup_return_bond_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_return_bond_tag
      Manager_operations.tx_rollup_return_bond_case.

  Definition tx_rollup_finalize_commitment_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_finalize_commitment_tag
      Manager_operations.tx_rollup_finalize_commitment_case.

  Definition tx_rollup_remove_commitment_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_remove_commitment_tag
      Manager_operations.tx_rollup_remove_commitment_case.

  Definition tx_rollup_rejection_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_rejection_tag
      Manager_operations.tx_rollup_rejection_case.

  Definition tx_rollup_dispatch_tickets_case : case Kind.manager :=
    make_manager_case tx_rollup_operation_dispatch_tickets_tag
      Manager_operations.tx_rollup_dispatch_tickets_case.

  Definition transfer_ticket_case : case Kind.manager :=
    make_manager_case transfer_ticket_tag
      Manager_operations.transfer_ticket_case.

  Definition dal_publish_slot_header_case : case Kind.manager :=
    make_manager_case dal_publish_slot_header_tag
      Manager_operations.dal_publish_slot_header_case.

  Definition sc_rollup_originate_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_origination_tag
      Manager_operations.sc_rollup_originate_case.

  Definition sc_rollup_add_messages_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_add_message_tag
      Manager_operations.sc_rollup_add_messages_case.

  Definition sc_rollup_cement_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_cement_tag
      Manager_operations.sc_rollup_cement_case.

  Definition sc_rollup_publish_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_publish_tag
      Manager_operations.sc_rollup_publish_case.

  Definition sc_rollup_refute_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_refute_tag
      Manager_operations.sc_rollup_refute_case.

  Definition sc_rollup_timeout_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_timeout_tag
      Manager_operations.sc_rollup_timeout_case.

  Definition sc_rollup_execute_outbox_message_case : case Kind.manager :=
    make_manager_case sc_rollup_execute_outbox_message_tag
      Manager_operations.sc_rollup_execute_outbox_message_case.

  Definition sc_rollup_recover_bond_case : case Kind.manager :=
    make_manager_case sc_rollup_operation_recover_bond_tag
      Manager_operations.sc_rollup_recover_bond_case.

  Definition zk_rollup_origination_case : case Kind.manager :=
    make_manager_case zk_rollup_operation_create_tag
      Manager_operations.zk_rollup_origination_case.

  Definition zk_rollup_publish_case : case Kind.manager :=
    make_manager_case zk_rollup_operation_publish_tag
      Manager_operations.zk_rollup_publish_case.

  Definition zk_rollup_update_case : case Kind.manager :=
    make_manager_case zk_rollup_operation_update_tag
      Manager_operations.zk_rollup_update_case.

  Definition contents_encoding : Data_encoding.encoding packed_contents :=
    let make {A : Set} (case_description : case A)
      : Data_encoding.case packed_contents :=
      let
        'Case {|
          case.Case.tag := tag;
            case.Case.name := name;
            case.Case.encoding := encoding;
            case.Case.select := select;
            case.Case.proj := proj;
            case.Case.inj := inj
            |} := case_description in
      let 'existT _ __Case_'a [inj, proj, select, encoding, name, tag] :=
        existT (A := Set)
          (fun __Case_'a ⇒
            [__Case_'a → contents ** contents → __Case_'a **
              packed_contents → option contents ** Data_encoding.t __Case_'a **
              string ** int]) _ [inj, proj, select, encoding, name, tag] in
      case_value (Data_encoding.Tag tag) name encoding
        (fun (o_value : packed_contents) ⇒
          match select o_value with
          | None ⇒ None
          | Some o_value ⇒ Some (proj o_value)
          end) (fun (x_value : __Case_'a) ⇒ Contents (inj x_value)) in
    Data_encoding.def "operation.alpha.contents" None None
      (Data_encoding.union None
        [
          make endorsement_case;
          make preendorsement_case;
          make dal_attestation_case;
          make seed_nonce_revelation_case;
          make vdf_revelation_case;
          make double_endorsement_evidence_case;
          make double_preendorsement_evidence_case;
          make double_baking_evidence_case;
          make activate_account_case;
          make proposals_case;
          make ballot_case;
          make reveal_case;
          make transaction_case;
          make origination_case;
          make delegation_case;
          make set_deposits_limit_case;
          make increase_paid_storage_case;
          make update_consensus_key_case;
          make drain_delegate_case;
          make failing_noop_case;
          make register_global_constant_case;
          make tx_rollup_origination_case;
          make tx_rollup_submit_batch_case;
          make tx_rollup_commit_case;
          make tx_rollup_return_bond_case;
          make tx_rollup_finalize_commitment_case;
          make tx_rollup_remove_commitment_case;
          make tx_rollup_rejection_case;
          make tx_rollup_dispatch_tickets_case;
          make transfer_ticket_case;
          make dal_publish_slot_header_case;
          make sc_rollup_originate_case;
          make sc_rollup_add_messages_case;
          make sc_rollup_cement_case;
          make sc_rollup_publish_case;
          make sc_rollup_refute_case;
          make sc_rollup_timeout_case;
          make sc_rollup_execute_outbox_message_case;
          make sc_rollup_recover_bond_case;
          make zk_rollup_origination_case;
          make zk_rollup_publish_case;
          make zk_rollup_update_case
        ]).

  Definition contents_list_encoding
    : Data_encoding.encoding packed_contents_list :=
    Data_encoding.conv_with_guard to_list of_list_internal None
      (Data_encoding._Variable.list_value None contents_encoding).

  Definition optional_signature_encoding
    : Data_encoding.encoding (option Signature.t) :=
    Data_encoding.conv
      (fun (function_parameter : option Signature.t) ⇒
        match function_parameter with
        | Some s_value ⇒ s_value
        | None ⇒ Signature.zero
        end)
      (fun (s_value : Signature.t) ⇒
        if Signature.equal s_value Signature.zero then
          None
        else
          Some s_value) None Signature.encoding.

  Definition protocol_data_encoding
    : Data_encoding.encoding packed_protocol_data :=
    Data_encoding.def "operation.alpha.contents_and_signature" None None
      (Data_encoding.conv
        (fun (function_parameter : packed_protocol_data) ⇒
          let
            'Operation_data {|
              protocol_data.contents := contents;
                protocol_data.signature := signature
                |} := function_parameter in
          ((Contents_list contents), signature))
        (fun (function_parameter : packed_contents_list × option Signature.t) ⇒
          let '(Contents_list contents, signature) := function_parameter in
          Operation_data
            {| protocol_data.contents := contents;
              protocol_data.signature := signature; |}) None
        (Data_encoding.obj2
          (Data_encoding.req None None "contents" contents_list_encoding)
          (Data_encoding.req None None "signature" optional_signature_encoding))).

  Definition operation_encoding : Data_encoding.encoding packed_operation :=
    Data_encoding.conv
      (fun (function_parameter : packed_operation) ⇒
        let '{|
          packed_operation.shell := shell;
            packed_operation.protocol_data := protocol_data
            |} := function_parameter in
        (shell, protocol_data))
      (fun (function_parameter : Operation.shell_header × packed_protocol_data)
        ⇒
        let '(shell, protocol_data) := function_parameter in
        {| packed_operation.shell := shell;
          packed_operation.protocol_data := protocol_data; |}) None
      (Data_encoding.merge_objs Operation.shell_header_encoding
        protocol_data_encoding).

  Definition unsigned_operation_encoding
    : Data_encoding.encoding (Operation.shell_header × packed_contents_list) :=
    Data_encoding.def "operation.alpha.unsigned_operation" None None
      (Data_encoding.merge_objs Operation.shell_header_encoding
        (Data_encoding.obj1
          (Data_encoding.req None None "contents" contents_list_encoding))).
End Encoding.

Definition encoding : Data_encoding.encoding packed_operation :=
  Encoding.operation_encoding.

Definition contents_encoding : Data_encoding.encoding packed_contents :=
  Encoding.contents_encoding.

Definition contents_list_encoding
  : Data_encoding.encoding packed_contents_list :=
  Encoding.contents_list_encoding.

Definition protocol_data_encoding
  : Data_encoding.encoding packed_protocol_data :=
  Encoding.protocol_data_encoding.

Definition unsigned_operation_encoding
  : Data_encoding.encoding (Operation.shell_header × packed_contents_list) :=
  Encoding.unsigned_operation_encoding.

Definition raw_value (function_parameter : operation) : Operation.t :=
  let '{|
    operation.shell := shell; operation.protocol_data := protocol_data |} :=
    function_parameter in
  let proto :=
    Data_encoding.Binary.to_bytes_exn None protocol_data_encoding
      (Operation_data protocol_data) in
  {| Operation.t.shell := shell; Operation.t.proto := proto; |}.

Definition consensus_pass : int := 0.

Definition voting_pass : int := 1.

Definition anonymous_pass : int := 2.

Definition manager_pass : int := 3.

[acceptable_pass op] returns either the validation_pass of [op] when defines and None when [op] is [Failing_noop].

Definition acceptable_pass (op : packed_operation) : option int :=
  let 'Operation_data protocol_data := op.(packed_operation.protocol_data) in
  match protocol_data.(protocol_data.contents) with
  | Single (Failing_noop _) ⇒ None
  | Single (Preendorsement _) ⇒ Some consensus_pass
  | Single (Endorsement _) ⇒ Some consensus_pass
  | Single (Dal_attestation _) ⇒ Some consensus_pass
  | Single (Proposals _) ⇒ Some voting_pass
  | Single (Ballot _) ⇒ Some voting_pass
  | Single (Seed_nonce_revelation _) ⇒ Some anonymous_pass
  | Single (Vdf_revelation _) ⇒ Some anonymous_pass
  | Single (Double_endorsement_evidence _) ⇒ Some anonymous_pass
  | Single (Double_preendorsement_evidence _) ⇒ Some anonymous_pass
  | Single (Double_baking_evidence _) ⇒ Some anonymous_pass
  | Single (Activate_account _) ⇒ Some anonymous_pass
  | Single (Drain_delegate _) ⇒ Some anonymous_pass
  | Single (Manager_operation _) ⇒ Some manager_pass
  | Cons (Manager_operation _) _ops ⇒ Some manager_pass
  | _ ⇒ unreachable_gadt_branch
  end.

[compare_by_passes] orders two operations in the reverse order of their acceptable passes.

Definition compare_by_passes (op1 : packed_operation) (op2 : packed_operation)
  : int :=
  match ((acceptable_pass op1), (acceptable_pass op2)) with
  | (Some op1_pass, Some op2_pass) ⇒ Compare.Int.compare op2_pass op1_pass
  | (None, Some _) ⇒ (-1)
  | (Some _, None) ⇒ 1
  | (None, None) ⇒ 0
  end.

Init function; without side-effects in Coq

Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.invalid_signature" "Invalid operation signature"
      "The operation signature is ill-formed or has been made with the wrong public key"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The operation signature is invalid"
                  CamlinternalFormatBasics.End_of_format)
                "The operation signature is invalid"))) Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_signature" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_signature" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.missing_signature" "Missing operation signature"
      "The operation is of a kind that must be signed, but the signature is missing"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The operation requires a signature"
                  CamlinternalFormatBasics.End_of_format)
                "The operation requires a signature"))) Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Missing_signature" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Missing_signature" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent
    "operation.contents_list_error" "Invalid list of operation contents."
    "An operation contents list has an unexpected shape; it should be either a single operation or a non-empty list of manager operations"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (s_value : string) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "An operation contents list has an unexpected shape: "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "An operation contents list has an unexpected shape: %s") s_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "message"
        (Data_encoding.string' None Data_encoding.Hex)))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Contents_list_error" then
          let s_value := cast string payload in
          Some s_value
        else None
      end)
    (fun (s_value : string) ⇒
      Build_extensible "Contents_list_error" string s_value).

Definition check_signature
  (key_value : Signature.public_key) (chain_id : Chain_id.t)
  (function_parameter : operation) : M? unit :=
  let '{|
    operation.shell := shell; operation.protocol_data := protocol_data |} :=
    function_parameter in
  let check
    (watermark : Signature.watermark) (contents : packed_contents_list)
    (signature : Signature.t) : M? unit :=
    let unsigned_operation :=
      Data_encoding.Binary.to_bytes_exn None unsigned_operation_encoding
        (shell, contents) in
    if
      Signature.check (Some watermark) key_value signature unsigned_operation
    then
      Pervasives.Ok tt
    else
      Error_monad.error_value (Build_extensible "Invalid_signature" unit tt) in
  match protocol_data.(protocol_data.signature) with
  | None ⇒
    Error_monad.error_value (Build_extensible "Missing_signature" unit tt)
  | Some signature ⇒
    match protocol_data.(protocol_data.contents) with
    | (Single (Preendorsement _)) as contents ⇒
      check (to_watermark (Consensus_watermark.Preendorsement chain_id))
        (Contents_list contents) signature
    | (Single (Endorsement _)) as contents ⇒
      check (to_watermark (Consensus_watermark.Endorsement chain_id))
        (Contents_list contents) signature
    | (Single (Dal_attestation _)) as contents ⇒
      check (to_watermark (Consensus_watermark.Dal_attestation chain_id))
        (Contents_list contents) signature
    |
      Single
        (Failing_noop _ | Proposals _ | Ballot _ | Seed_nonce_revelation _ |
        Vdf_revelation _ | Double_endorsement_evidence _ |
        Double_preendorsement_evidence _ | Double_baking_evidence _ |
        Activate_account _ | Drain_delegate _ | Manager_operation _) ⇒
      check Signature.Generic_operation
        (Contents_list protocol_data.(protocol_data.contents)) signature
    | Cons (Manager_operation _) _ops ⇒
      check Signature.Generic_operation
        (Contents_list protocol_data.(protocol_data.contents)) signature
    | _ ⇒ unreachable_gadt_branch
    end
  end.

Definition hash_raw : Operation.t → Operation_hash.t := Operation.hash_value.

Definition hash_value (o_value : operation) : Operation_hash.t :=
  let proto :=
    Data_encoding.Binary.to_bytes_exn None protocol_data_encoding
      (Operation_data o_value.(operation.protocol_data)) in
  Operation.hash_value
    {| Operation.t.shell := o_value.(operation.shell);
      Operation.t.proto := proto; |}.

Definition hash_packed (o_value : packed_operation) : Operation_hash.t :=
  let proto :=
    Data_encoding.Binary.to_bytes_exn None protocol_data_encoding
      o_value.(packed_operation.protocol_data) in
  Operation.hash_value
    {| Operation.t.shell := o_value.(packed_operation.shell);
      Operation.t.proto := proto; |}.

Inductive eq : Set :=
| Eq : eq.

Definition equal_manager_operation_kind
  (op1 : manager_operation) (op2 : manager_operation) : option eq :=
  match (op1, op2) with
  | (Reveal _, Reveal _) ⇒ Some Eq
  | (Reveal _, _) ⇒ None
  | (Transaction _, Transaction _) ⇒ Some Eq
  | (Transaction _, _) ⇒ None
  | (Origination _, Origination _) ⇒ Some Eq
  | (Origination _, _) ⇒ None
  | (Delegation _, Delegation _) ⇒ Some Eq
  | (Delegation _, _) ⇒ None
  | (Register_global_constant _, Register_global_constant _) ⇒ Some Eq
  | (Register_global_constant _, _) ⇒ None
  | (Set_deposits_limit _, Set_deposits_limit _) ⇒ Some Eq
  | (Set_deposits_limit _, _) ⇒ None
  | (Increase_paid_storage _, Increase_paid_storage _) ⇒ Some Eq
  | (Increase_paid_storage _, _) ⇒ None
  | (Update_consensus_key _, Update_consensus_key _) ⇒ Some Eq
  | (Update_consensus_key _, _) ⇒ None
  | (Tx_rollup_origination, Tx_rollup_origination) ⇒ Some Eq
  | (Tx_rollup_origination, _) ⇒ None
  | (Tx_rollup_submit_batch _, Tx_rollup_submit_batch _) ⇒ Some Eq
  | (Tx_rollup_submit_batch _, _) ⇒ None
  | (Tx_rollup_commit _, Tx_rollup_commit _) ⇒ Some Eq
  | (Tx_rollup_commit _, _) ⇒ None
  | (Tx_rollup_return_bond _, Tx_rollup_return_bond _) ⇒ Some Eq
  | (Tx_rollup_return_bond _, _) ⇒ None
  | (Tx_rollup_finalize_commitment _, Tx_rollup_finalize_commitment _) ⇒
    Some Eq
  | (Tx_rollup_finalize_commitment _, _) ⇒ None
  | (Tx_rollup_remove_commitment _, Tx_rollup_remove_commitment _) ⇒ Some Eq
  | (Tx_rollup_remove_commitment _, _) ⇒ None
  | (Tx_rollup_rejection _, Tx_rollup_rejection _) ⇒ Some Eq
  | (Tx_rollup_rejection _, _) ⇒ None
  | (Tx_rollup_dispatch_tickets _, Tx_rollup_dispatch_tickets _) ⇒ Some Eq
  | (Tx_rollup_dispatch_tickets _, _) ⇒ None
  | (Transfer_ticket _, Transfer_ticket _) ⇒ Some Eq
  | (Transfer_ticket _, _) ⇒ None
  | (Dal_publish_slot_header _, Dal_publish_slot_header _) ⇒ Some Eq
  | (Dal_publish_slot_header _, _) ⇒ None
  | (Sc_rollup_originate _, Sc_rollup_originate _) ⇒ Some Eq
  | (Sc_rollup_originate _, _) ⇒ None
  | (Sc_rollup_add_messages _, Sc_rollup_add_messages _) ⇒ Some Eq
  | (Sc_rollup_add_messages _, _) ⇒ None
  | (Sc_rollup_cement _, Sc_rollup_cement _) ⇒ Some Eq
  | (Sc_rollup_cement _, _) ⇒ None
  | (Sc_rollup_publish _, Sc_rollup_publish _) ⇒ Some Eq
  | (Sc_rollup_publish _, _) ⇒ None
  | (Sc_rollup_refute _, Sc_rollup_refute _) ⇒ Some Eq
  | (Sc_rollup_refute _, _) ⇒ None
  | (Sc_rollup_timeout _, Sc_rollup_timeout _) ⇒ Some Eq
  | (Sc_rollup_timeout _, _) ⇒ None
  | (Sc_rollup_execute_outbox_message _, Sc_rollup_execute_outbox_message _) ⇒
    Some Eq
  | (Sc_rollup_execute_outbox_message _, _) ⇒ None
  | (Sc_rollup_recover_bond _, Sc_rollup_recover_bond _) ⇒ Some Eq
  | (Sc_rollup_recover_bond _, _) ⇒ None
  | (Zk_rollup_origination _, Zk_rollup_origination _) ⇒ Some Eq
  | (Zk_rollup_origination _, _) ⇒ None
  | (Zk_rollup_publish _, Zk_rollup_publish _) ⇒ Some Eq
  | (Zk_rollup_publish _, _) ⇒ None
  | (Zk_rollup_update _, Zk_rollup_update _) ⇒ Some Eq
  | (Zk_rollup_update _, _) ⇒ None
  end.

Definition equal_contents_kind (op1 : contents) (op2 : contents) : option eq :=
  match (op1, op2) with
  | (Preendorsement _, Preendorsement _) ⇒ Some Eq
  | (Preendorsement _, _) ⇒ None
  | (Endorsement _, Endorsement _) ⇒ Some Eq
  | (Endorsement _, _) ⇒ None
  | (Dal_attestation _, Dal_attestation _) ⇒ Some Eq
  | (Dal_attestation _, _) ⇒ None
  | (Seed_nonce_revelation _, Seed_nonce_revelation _) ⇒ Some Eq
  | (Seed_nonce_revelation _, _) ⇒ None
  | (Vdf_revelation _, Vdf_revelation _) ⇒ Some Eq
  | (Vdf_revelation _, _) ⇒ None
  | (Double_endorsement_evidence _, Double_endorsement_evidence _) ⇒ Some Eq
  | (Double_endorsement_evidence _, _) ⇒ None
  | (Double_preendorsement_evidence _, Double_preendorsement_evidence _) ⇒
    Some Eq
  | (Double_preendorsement_evidence _, _) ⇒ None
  | (Double_baking_evidence _, Double_baking_evidence _) ⇒ Some Eq
  | (Double_baking_evidence _, _) ⇒ None
  | (Activate_account _, Activate_account _) ⇒ Some Eq
  | (Activate_account _, _) ⇒ None
  | (Proposals _, Proposals _) ⇒ Some Eq
  | (Proposals _, _) ⇒ None
  | (Ballot _, Ballot _) ⇒ Some Eq
  | (Ballot _, _) ⇒ None
  | (Drain_delegate _, Drain_delegate _) ⇒ Some Eq
  | (Drain_delegate _, _) ⇒ None
  | (Failing_noop _, Failing_noop _) ⇒ Some Eq
  | (Failing_noop _, _) ⇒ None
  | (Manager_operation op1, Manager_operation op2) ⇒
    match
      equal_manager_operation_kind op1.(contents.Manager_operation.operation)
        op2.(contents.Manager_operation.operation) with
    | None ⇒ None
    | Some Eq ⇒ Some Eq
    end
  | (Manager_operation _, _) ⇒ None
  end.

Fixpoint equal_contents_kind_list (op1 : contents_list) (op2 : contents_list)
  : option eq :=
  match (op1, op2) with
  | (Single op1, Single op2) ⇒ equal_contents_kind op1 op2
  | (Single _, Cons _ _) ⇒ None
  | (Cons _ _, Single _) ⇒ None
  | (Cons op1 ops1, Cons op2 ops2) ⇒
    match equal_contents_kind op1 op2 with
    | None ⇒ None
    | Some Eq ⇒
      match equal_contents_kind_list ops1 ops2 with
      | None ⇒ None
      | Some Eq ⇒ Some Eq
      end
    end
  end.

Definition equal (op1 : operation) (op2 : operation) : option eq :=
  if
    Pervasives.not (Operation_hash.equal (hash_value op1) (hash_value op2))
  then
    None
  else
    equal_contents_kind_list
      op1.(operation.protocol_data).(protocol_data.contents)
      op2.(operation.protocol_data).(protocol_data.contents).

Parameter consensus_pass_type : Set.

Parameter voting_pass_type : Set.

Parameter anonymous_pass_type : Set.

Parameter manager_pass_type : Set.

Parameter noop_pass_type : Set.

Module Pass.
  Inductive t : Set :=
  | Consensus : t
  | Voting : t
  | Anonymous : t
  | Manager : t
  | Noop : t.
End Pass.

Pass comparison.

Definition compare_inner_pass (pass1 : Pass.t) (pass2 : Pass.t) : int :=
  match (pass1, pass2) with
  | (Pass.Consensus, (Pass.Voting | Pass.Anonymous | Pass.Manager | Pass.Noop))
    ⇒ 1
  | ((Pass.Voting | Pass.Anonymous | Pass.Manager | Pass.Noop), Pass.Consensus)
    ⇒ (-1)
  | (Pass.Voting, (Pass.Anonymous | Pass.Manager | Pass.Noop)) ⇒ 1
  | ((Pass.Anonymous | Pass.Manager | Pass.Noop), Pass.Voting) ⇒ (-1)
  | (Pass.Anonymous, (Pass.Manager | Pass.Noop)) ⇒ 1
  | ((Pass.Manager | Pass.Noop), Pass.Anonymous) ⇒ (-1)
  | (Pass.Manager, Pass.Noop) ⇒ 1
  | (Pass.Noop, Pass.Manager) ⇒ (-1)
  |
    ((Pass.Consensus, Pass.Consensus) | (Pass.Voting, Pass.Voting) |
    (Pass.Anonymous, Pass.Anonymous) | (Pass.Manager, Pass.Manager) |
    (Pass.Noop, Pass.Noop)) ⇒ 0
  end.

[round_infos] is the pair of a [level] convert into {!int32} and [round] convert into an {!int}.

By convention, if the [round] is from an operation round that failed to convert in a {!int}, the value of [round] is (-1).

Module round_infos.
  Record record : Set := Build {
    level : int32;
    round : int;
  }.
  Definition with_level level (r : record) :=
    Build level r.(round).
  Definition with_round round (r : record) :=
    Build r.(level) round.
End round_infos.
Definition round_infos := round_infos.record.

[endorsement_infos] is the pair of a {!round_infos} and a [slot] convert into an {!int}.

Module endorsement_infos.
  Record record : Set := Build {
    round : round_infos;
    slot : int;
  }.
  Definition with_round round (r : record) :=
    Build round r.(slot).
  Definition with_slot slot (r : record) :=
    Build r.(round) slot.
End endorsement_infos.
Definition endorsement_infos := endorsement_infos.record.

[double_baking_infos] is the pair of a {!round_infos} and a {!block_header} hash.

Module double_baking_infos.
  Record record : Set := Build {
    round : round_infos;
    bh_hash : Block_hash.t;
  }.
  Definition with_round round (r : record) :=
    Build round r.(bh_hash).
  Definition with_bh_hash bh_hash (r : record) :=
    Build r.(round) bh_hash.
End double_baking_infos.
Definition double_baking_infos := double_baking_infos.record.

Compute a {!round_infos} from a {consensus_content} of a valid operation. Hence, the [round] must convert in {!int}.

Precondition: [c] comes from a valid operation. The [round] from a valid operation should succeed to convert in {!int}. Hence, for the unreachable path where the convertion failed, we put (-1) as [round] value.

Definition round_infos_from_consensus_content (c_value : consensus_content)
  : round_infos :=
  let level := Raw_level_repr.to_int32 c_value.(consensus_content.level) in
  match Round_repr.to_int c_value.(consensus_content.round) with
  | Pervasives.Ok round ⇒
    {| round_infos.level := level; round_infos.round := round; |}
  | Pervasives.Error _ ⇒
    {| round_infos.level := level; round_infos.round := (-1); |}
  end.

Compute a {!endorsement_infos} from a {!consensus_content}. It is used to compute the weight of {!Endorsement} and {!Preendorsement}.

Precondition: [c] comes from a valid operation. The {!Endorsement} or {!Preendorsement} is valid, so its [round] must succeed to convert into an {!int}. Hence, for the unreachable path where the convertion fails, we put (-1) as [round] value (see {!round_infos_from_consensus_content}).

Definition endorsement_infos_from_consensus_content
  (c_value : consensus_content) : endorsement_infos :=
  let slot := Slot_repr.to_int c_value.(consensus_content.slot) in
  let round := round_infos_from_consensus_content c_value in
  {| endorsement_infos.round := round; endorsement_infos.slot := slot; |}.

Compute a {!double_baking_infos} and a {!Block_header_repr.hash} from a {!Block_header_repr.t}. It is used to compute the weight of a {!Double_baking_evidence}.

Precondition: [bh] comes from a valid operation. The {!Double_baking_envidence} is valid, so its fitness from its first denounced block header must succeed, and the round from this fitness must convert in a {!int}. Hence, for the unreachable paths where either the convertion fails or the fitness is not retrievable, we put (-1) as [round] value.

Definition consensus_infos_and_hash_from_block_header (bh : Block_header_repr.t)
  : double_baking_infos :=
  let level := bh.(Block_header_repr.t.shell).(Block_header.shell_header.level)
    in
  let bh_hash := Block_header_repr.hash_value bh in
  let round :=
    match
      Fitness_repr.from_raw
        bh.(Block_header_repr.t.shell).(Block_header.shell_header.fitness) with
    | Pervasives.Ok bh_fitness ⇒
      match Round_repr.to_int (Fitness_repr.round bh_fitness) with
      | Pervasives.Ok round ⇒
        {| round_infos.level := level; round_infos.round := round; |}
      | Pervasives.Error _ ⇒
        {| round_infos.level := level; round_infos.round := (-1); |}
      end
    | Pervasives.Error _ ⇒
      {| round_infos.level := level; round_infos.round := (-1); |}
    end in
  {| double_baking_infos.round := round; double_baking_infos.bh_hash := bh_hash;
    |}.

The weight of an operation.

Given an operation, its [weight] carries on static information that is used to compare it to an operation of the same pass. Operation weight are defined by validation pass.

The [weight] of an {!Endorsement} or {!Preendorsement} depends on its {!endorsement_infos}.

The [weight] of a {!Dal_attestation} depends on the pair of the size of its bitset, {!Dal_attestation_repr.t}, and the signature of its attestor {! Signature.Public_key_hash.t}.

The [weight] of a voting operation depends on the pair of its [period] and [source].

The [weight] of a {!Vdf_revelation} depends on its [solution].

The [weight] of a {!Seed_nonce_revelation} depends on its [level] converted in {!int32}.

The [weight] of a {!Double_preendorsement} or {!Double_endorsement} depends on the [level] and [round] of their first denounciated operations. The [level] and [round] are wrapped in a {!round_infos}.

The [weight] of a {!Double_baking} depends on the [level], [round] and [hash] of its first denounciated block_header. the [level] and [round] are wrapped in a {!double_baking_infos}.

The [weight] of an {!Activate_account} depends on its public key hash.

The [weight] of an {!Drain_delegate} depends on the public key hash of the delegate.

The [weight] of {!Manager_operation} depends on its [fee] and [gas_limit] ratio expressed in {!Q.t}.

Inductive weight : Set :=
| Weight_endorsement : endorsement_infos → weight
| Weight_preendorsement : endorsement_infos → weight
| Weight_dal_attestation : Signature.public_key_hash × int × int32 → weight
| Weight_proposals : int32 → Signature.public_key_hash → weight
| Weight_ballot : int32 → Signature.public_key_hash → weight
| Weight_seed_nonce_revelation : int32 → weight
| Weight_vdf_revelation : Seed_repr.vdf_solution → weight
| Weight_double_preendorsement : round_infos → weight
| Weight_double_endorsement : round_infos → weight
| Weight_double_baking : double_baking_infos → weight
| Weight_activate_account :
  Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → weight
| Weight_drain_delegate : Signature.public_key_hash → weight
| Weight_manager : Q.t → Signature.public_key_hash → weight
| Weight_noop : weight.

The weight of an operation is the pair of its pass and weight.

Inductive operation_weight : Set :=
| W : Pass.t → weight → operation_weight.

The {!weight} of a batch of {!Manager_operation} depends on the sum of all [fee] and the sum of all [gas_limit].

Precondition: [op] is a valid manager operation: its sum of accumulated [fee] must succeed. Hence, in the unreachable path where the [fee] sum fails, we put [Tez_repr.zero] as its value.

#[bypass_check(guard)]
Definition cumulate_fee_and_gas_of_manager (op : contents_list)
  : Tez_repr.t × Gas_limit_repr.Arith.integral :=
  let add_without_error (acc_value : Tez_repr.t) (y_value : Tez_repr.t)
    : Tez_repr.t :=
    match Tez_repr.op_plusquestion acc_value y_value with
    | Pervasives.Ok v_value ⇒ v_value
    | Pervasives.Error _ ⇒ acc_value
    end in
  let fix loop
    (fees_acc : Tez_repr.t) (gas_limit_acc : Gas_limit_repr.Arith.t)
    (function_parameter : contents_list) {struct function_parameter}
    : Tez_repr.t × Gas_limit_repr.Arith.t :=
    match function_parameter with
    |
      Single
        (Manager_operation {|
          contents.Manager_operation.fee := fee;
            contents.Manager_operation.gas_limit := gas_limit
            |}) ⇒
      let total_fees := add_without_error fees_acc fee in
      let total_gas_limit := Gas_limit_repr.Arith.add gas_limit_acc gas_limit in
      (total_fees, total_gas_limit)
    |
      Cons
        (Manager_operation {|
          contents.Manager_operation.fee := fee;
            contents.Manager_operation.gas_limit := gas_limit
            |}) manops ⇒
      let fees_acc := add_without_error fees_acc fee in
      let gas_limit_acc := Gas_limit_repr.Arith.add gas_limit gas_limit_acc in
      loop fees_acc gas_limit_acc manops
    | _ ⇒ unreachable_gadt_branch
    end in
  loop Tez_repr.zero Gas_limit_repr.Arith.zero op.

The {!weight} of a {!Manager_operation} as well as a batch of operations is the ratio in {!int64} between its [fee] and [gas_limit] as computed by {!cumulate_fee_and_gas_of_manager} converted in {!Q.t}. We assume that the manager operation valid, thus its gas limit can never be zero. We treat this case the same as gas_limit = 1 for the sake of simplicity.

Definition weight_manager (op : contents_list)
  : Q.t × Signature.public_key_hash :=
  let '(fee, glimit) := cumulate_fee_and_gas_of_manager op in
  let source :=
    match op with
    |
      Cons (Manager_operation {| contents.Manager_operation.source := source |})
        _ ⇒ source
    |
      Single
        (Manager_operation {| contents.Manager_operation.source := source |}) ⇒
      source
    | _ ⇒ unreachable_gadt_branch
    end in
  let fee_f := Q.of_int64 (Tez_repr.to_mutez fee) in
  if Gas_limit_repr.Arith.op_eq glimit Gas_limit_repr.Arith.zero then
    (fee_f, source)
  else
    let gas_f := Q.of_bigint (Gas_limit_repr.Arith.integral_to_z glimit) in
    ((Q.op_div fee_f gas_f), source).

Computing the {!operation_weight} of an operation. [weight_of (Failing_noop _)] is unreachable, for completness we define a Weight_noop which carrries no information.

Definition weight_of (op : packed_operation) : operation_weight :=
  let 'Operation_data protocol_data := op.(packed_operation.protocol_data) in
  match protocol_data.(protocol_data.contents) with
  | Single (Failing_noop _) ⇒ W Pass.Noop Weight_noop
  | Single (Preendorsement consensus_content) ⇒
    W Pass.Consensus
      (Weight_preendorsement
        (endorsement_infos_from_consensus_content consensus_content))
  | Single (Endorsement consensus_content) ⇒
    W Pass.Consensus
      (Weight_endorsement
        (endorsement_infos_from_consensus_content consensus_content))
  |
    Single
      (Dal_attestation {|
        Dal_attestation_repr.operation.attestor := attestor;
          Dal_attestation_repr.operation.attestation := attestation;
          Dal_attestation_repr.operation.level := level
          |}) ⇒
    W Pass.Consensus
      (Weight_dal_attestation
        (attestor, (Dal_attestation_repr.occupied_size_in_bits attestation),
          (Raw_level_repr.to_int32 level)))
  |
    Single
      (Proposals {|
        contents.Proposals.source := source;
          contents.Proposals.period := period
          |}) ⇒ W Pass.Voting (Weight_proposals period source)
  |
    Single
      (Ballot {|
        contents.Ballot.source := source;
          contents.Ballot.period := period
          |}) ⇒ W Pass.Voting (Weight_ballot period source)
  |
    Single
      (Seed_nonce_revelation {| contents.Seed_nonce_revelation.level := level |})
    ⇒
    W Pass.Anonymous
      (Weight_seed_nonce_revelation (Raw_level_repr.to_int32 level))
  | Single (Vdf_revelation {| contents.Vdf_revelation.solution := solution |})
    ⇒ W Pass.Anonymous (Weight_vdf_revelation solution)
  |
    Single
      (Double_endorsement_evidence {|
        contents.Double_endorsement_evidence.op1 := op1 |}) ⇒
    match op1.(operation.protocol_data).(protocol_data.contents) with
    | Single (Endorsement consensus_content) ⇒
      W Pass.Anonymous
        (Weight_double_endorsement
          (round_infos_from_consensus_content consensus_content))
    | _ ⇒ unreachable_gadt_branch
    end
  |
    Single
      (Double_preendorsement_evidence {|
        contents.Double_preendorsement_evidence.op1 := op1 |}) ⇒
    match op1.(operation.protocol_data).(protocol_data.contents) with
    | Single (Preendorsement consensus_content) ⇒
      W Pass.Anonymous
        (Weight_double_preendorsement
          (round_infos_from_consensus_content consensus_content))
    | _ ⇒ unreachable_gadt_branch
    end
  |
    Single
      (Double_baking_evidence {| contents.Double_baking_evidence.bh1 := bh1 |})
    ⇒
    let double_baking_infos := consensus_infos_and_hash_from_block_header bh1 in
    W Pass.Anonymous (Weight_double_baking double_baking_infos)
  | Single (Activate_account {| contents.Activate_account.id := id |}) ⇒
    W Pass.Anonymous (Weight_activate_account id)
  | Single (Drain_delegate {| contents.Drain_delegate.delegate := delegate |})
    ⇒ W Pass.Anonymous (Weight_drain_delegate delegate)
  | (Single (Manager_operation _)) as ops ⇒
    let '(manweight, src) := weight_manager ops in
    W Pass.Manager (Weight_manager manweight src)
  | (Cons (Manager_operation _) _) as ops ⇒
    let '(manweight, src) := weight_manager ops in
    W Pass.Manager (Weight_manager manweight src)
  | _ ⇒ unreachable_gadt_branch
  end.

compare a pair of elements in lexicographic order.

Definition compare_pair_in_lexico_order {A B C D : Set}
  (cmp_fst : A → B → int) (cmp_snd : C → D → int)
  (function_parameter : A × C) : B × D → int :=
  let '(a1, b1) := function_parameter in
  fun (function_parameter : B × D) ⇒
    let '(a2, b2) := function_parameter in
    let resa := cmp_fst a1 a2 in
    if resa ≠i 0 then
      resa
    else
      cmp_snd b1 b2.

compare in reverse order.

Definition compare_reverse {a : Set}
  (cmp : a → a → int) (a_value : a) (b_value : a) : int :=
  cmp b_value a_value.

Two {!round_infos} compares as the pair of [level, round] in lexicographic order: the one with the greater [level] being the greater [round_infos]. When levels are the same, the one with the greater [round] being the better.

The greater {!round_infos} is the farther to the current state when part of the weight of a valid consensus operation.

The best {!round_infos} is the nearer to the current state when part of the weight of a valid denunciation.

In both case, that is the greater according to the lexicographic order.

Precondition: the {!round_infos} are from valid operation. They have been computed by either {!round_infos_from_consensus_content} or {!consensus_infos_and_hash_from_block_header}. Both input parameter from valid operations and put (-1) to the [round] in the unreachable path where the original round fails to convert in {!int}.

Definition compare_round_infos (infos1 : round_infos) (infos2 : round_infos)
  : int :=
  compare_pair_in_lexico_order Compare.Int32.(Compare.S.compare)
    Compare.Int.compare (infos1.(round_infos.level), infos1.(round_infos.round))
    (infos2.(round_infos.level), infos2.(round_infos.round)).

When comparing {!Endorsement} to {!Preendorsement} or {!Double_endorsement_evidence} to {!Double_preendorsement}, in case of {!round_infos} equality, the position is relevant to compute the order.

Inductive prioritized_position : Set :=
| Nopos : prioritized_position
| Fstpos : prioritized_position
| Sndpos : prioritized_position.

Comparison of two {!round_infos} with priority in case of {!round_infos} equality.

Definition compare_round_infos_with_prioritized_position
  (prioritized_position : prioritized_position) (infos1 : round_infos)
  (infos2 : round_infos) : int :=
  let cmp := compare_round_infos infos1 infos2 in
  if cmp ≠i 0 then
    cmp
  else
    match prioritized_position with
    | Fstpos ⇒ 1
    | Sndpos ⇒ (-1)
    | Nopos ⇒ 0
    end.

When comparing consensus operation with {!endorsement_infos}, in case of equality of their {!round_infos}, either they are of the same kind and their [slot] have to be compared in the reverse order, otherwise the {!Endorsement} is better and [prioritized_position] gives its position.

Definition compare_prioritized_position_or_slot
  (prioritized_position : prioritized_position) : int → int → int :=
  match prioritized_position with
  | Nopos ⇒ compare_reverse Compare.Int.compare
  | Fstpos ⇒
    fun (function_parameter : int) ⇒
      let '_ := function_parameter in
      fun (function_parameter : int) ⇒
        let '_ := function_parameter in
        1
  | Sndpos ⇒
    fun (function_parameter : int) ⇒
      let '_ := function_parameter in
      fun (function_parameter : int) ⇒
        let '_ := function_parameter in
        (-1)
  end.

Two {!endorsement_infos} are compared by their {!round_infos}. When their {!round_infos} are equal, they are compared according to their priority or their [slot], see {!compare_prioritized_position_or_slot} for more details.

Definition compare_endorsement_infos
  (prioritized_position : prioritized_position) (infos1 : endorsement_infos)
  (infos2 : endorsement_infos) : int :=
  compare_pair_in_lexico_order compare_round_infos
    (compare_prioritized_position_or_slot prioritized_position)
    (infos1.(endorsement_infos.round), infos1.(endorsement_infos.slot))
    (infos2.(endorsement_infos.round), infos2.(endorsement_infos.slot)).

Two {!double_baking_infos} are compared as their {!round_infos}. When their {!round_infos} are equal, they are compared as the hashes of their first denounced block header.

Definition compare_baking_infos
  (infos1 : double_baking_infos) (infos2 : double_baking_infos) : int :=
  compare_pair_in_lexico_order compare_round_infos Block_hash.compare
    (infos1.(double_baking_infos.round), infos1.(double_baking_infos.bh_hash))
    (infos2.(double_baking_infos.round), infos2.(double_baking_infos.bh_hash)).

Two valid {!Dal_attestation} are compared in the lexicographic order of their pairs of bitsets size and attestor hash.

Definition compare_dal_attestation
  (function_parameter : Signature.public_key_hash × int × int32)
  : Signature.public_key_hash × int × int32 → int :=
  let '(attestor1, endorsements1, level1) := function_parameter in
  fun (function_parameter : Signature.public_key_hash × int × int32) ⇒
    let '(attestor2, endorsements2, level2) := function_parameter in
    compare_pair_in_lexico_order
      (compare_pair_in_lexico_order Compare.Int32.(Compare.S.compare)
        Compare.Int.compare)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare)
      ((level1, endorsements1), attestor1) ((level2, endorsements2), attestor2).

Comparing consensus operations by their [weight] uses the comparison on {!endorsement_infos} for {!Endorsement} and {!Preendorsement}: see {!endorsement_infos} for more details.

{!Dal_attestation} is smaller than the other kinds of consensus operations. Two valid {!Dal_attestation} are compared by {!compare_dal_attestation}.

Definition compare_consensus_weight (w1 : weight) (w2 : weight) : int :=
  match (w1, w2) with
  | (Weight_endorsement infos1, Weight_endorsement infos2) ⇒
    compare_endorsement_infos Nopos infos1 infos2
  | (Weight_preendorsement infos1, Weight_preendorsement infos2) ⇒
    compare_endorsement_infos Nopos infos1 infos2
  | (Weight_endorsement infos1, Weight_preendorsement infos2) ⇒
    compare_endorsement_infos Fstpos infos1 infos2
  | (Weight_preendorsement infos1, Weight_endorsement infos2) ⇒
    compare_endorsement_infos Sndpos infos1 infos2
  |
    (Weight_dal_attestation (attestor1, size1, lvl1),
      Weight_dal_attestation (attestor2, size2, lvl2)) ⇒
    compare_dal_attestation (attestor1, size1, lvl1) (attestor2, size2, lvl2)
  | (Weight_dal_attestation _, (Weight_endorsement _ | Weight_preendorsement _))
    ⇒ (-1)
  | ((Weight_endorsement _ | Weight_preendorsement _), Weight_dal_attestation _)
    ⇒ 1
  | _ ⇒ unreachable_gadt_branch
  end.

Two valid voting operations of the same kind are compared in the lexicographic order of their pair of [period] and [source]. When compared to each other, the {!Proposals} is better.

Definition compare_vote_weight (w1 : weight) (w2 : weight) : int :=
  let cmp
    (i1 : int32) (source1 : Signature.public_key_hash) (i2 : int32)
    (source2 : Signature.public_key_hash) : int :=
    compare_pair_in_lexico_order Compare.Int32.(Compare.S.compare)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare)
      (i1, source1) (i2, source2) in
  match (w1, w2) with
  | (Weight_proposals i1 source1, Weight_proposals i2 source2) ⇒
    cmp i1 source1 i2 source2
  | (Weight_ballot i1 source1, Weight_ballot i2 source2) ⇒
    cmp i1 source1 i2 source2
  | (Weight_ballot _ _, Weight_proposals _ _) ⇒ (-1)
  | (Weight_proposals _ _, Weight_ballot _ _) ⇒ 1
  | _ ⇒ unreachable_gadt_branch
  end.

Comparing two {!Double_endorsement_evidence}, or two {!Double_preendorsement_evidence}, or comparing them to each other is comparing their {!round_infos}, see {!compare_round_infos} for more details.

Comparing two {!Double_baking_evidence} is comparing as their {!double_baking_infos}, see {!compare_double_baking_infos} for more details.

Two {!Seed_nonce_revelation} are compared by their [level].

Two {!Vdf_revelation} are compared by their [solution].

Two {!Activate_account} are compared as their [id].

When comparing different kind of anonymous operations, the order is as follows: {!Double_preendorsement_evidence} > {!Double_endorsement_evidence} > {!Double_baking_evidence} > {!Vdf_revelation} > {!Seed_nonce_revelation} > {!Activate_account}.

Definition compare_anonymous_weight (w1 : weight) (w2 : weight) : int :=
  match (w1, w2) with
  | (Weight_double_preendorsement infos1, Weight_double_preendorsement infos2)
    ⇒ compare_round_infos infos1 infos2
  | (Weight_double_preendorsement infos1, Weight_double_endorsement infos2) ⇒
    compare_round_infos_with_prioritized_position Fstpos infos1 infos2
  | (Weight_double_endorsement infos1, Weight_double_preendorsement infos2) ⇒
    compare_round_infos_with_prioritized_position Sndpos infos1 infos2
  | (Weight_double_endorsement infos1, Weight_double_endorsement infos2) ⇒
    compare_round_infos infos1 infos2
  |
    ((Weight_double_baking _ | Weight_seed_nonce_revelation _ |
    Weight_vdf_revelation _ | Weight_activate_account _ |
    Weight_drain_delegate _),
      (Weight_double_preendorsement _ | Weight_double_endorsement _)) ⇒ (-1)
  |
    ((Weight_double_preendorsement _ | Weight_double_endorsement _),
      (Weight_double_baking _ | Weight_seed_nonce_revelation _ |
      Weight_vdf_revelation _ | Weight_activate_account _ |
      Weight_drain_delegate _)) ⇒ 1
  | (Weight_double_baking infos1, Weight_double_baking infos2) ⇒
    compare_baking_infos infos1 infos2
  |
    ((Weight_seed_nonce_revelation _ | Weight_vdf_revelation _ |
    Weight_activate_account _ | Weight_drain_delegate _), Weight_double_baking _)
    ⇒ (-1)
  |
    (Weight_double_baking _,
      (Weight_seed_nonce_revelation _ | Weight_vdf_revelation _ |
      Weight_activate_account _ | Weight_drain_delegate _)) ⇒ 1
  | (Weight_vdf_revelation solution1, Weight_vdf_revelation solution2) ⇒
    Seed_repr.compare_vdf_solution solution1 solution2
  |
    ((Weight_seed_nonce_revelation _ | Weight_activate_account _ |
    Weight_drain_delegate _), Weight_vdf_revelation _) ⇒ (-1)
  |
    (Weight_vdf_revelation _,
      (Weight_seed_nonce_revelation _ | Weight_activate_account _ |
      Weight_drain_delegate _)) ⇒ 1
  | (Weight_seed_nonce_revelation l1, Weight_seed_nonce_revelation l2) ⇒
    Compare.Int32.(Compare.S.compare) l1 l2
  |
    ((Weight_activate_account _ | Weight_drain_delegate _),
      Weight_seed_nonce_revelation _) ⇒ (-1)
  |
    (Weight_seed_nonce_revelation _,
      (Weight_activate_account _ | Weight_drain_delegate _)) ⇒ 1
  | (Weight_activate_account pkh1, Weight_activate_account pkh2) ⇒
    Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkh1 pkh2
  | (Weight_drain_delegate _, Weight_activate_account _) ⇒ (-1)
  | (Weight_activate_account _, Weight_drain_delegate _) ⇒ 1
  | (Weight_drain_delegate pkh1, Weight_drain_delegate pkh2) ⇒
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkh1 pkh2
  | _ ⇒ unreachable_gadt_branch
  end.

Two {!Manager_operation} are compared in the lexicographic order of their pair of their [fee]/[gas] ratio -- as computed by {!weight_manager} -- and their [source].

Definition compare_manager_weight (weight1 : weight) (weight2 : weight) : int :=
  match (weight1, weight2) with
  | (Weight_manager manweight1 source1, Weight_manager manweight2 source2) ⇒
    compare_pair_in_lexico_order Compare.Q.(Compare.S.compare)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare)
      (manweight1, source1) (manweight2, source2)
  | _ ⇒ unreachable_gadt_branch
  end.

Two {!operation_weight} are compared by their [pass], see {!compare_inner_pass} for more details. When they have the same [pass], they are compared by their [weight].

Definition compare_operation_weight
  (w1 : operation_weight) (w2 : operation_weight) : int :=
  match (w1, w2) with
  | (W Pass.Consensus w1, W Pass.Consensus w2) ⇒ compare_consensus_weight w1 w2
  | (W Pass.Voting w1, W Pass.Voting w2) ⇒ compare_vote_weight w1 w2
  | (W Pass.Anonymous w1, W Pass.Anonymous w2) ⇒ compare_anonymous_weight w1 w2
  | (W Pass.Manager w1, W Pass.Manager w2) ⇒ compare_manager_weight w1 w2
  | (W pass1 _, W pass2 _) ⇒ compare_inner_pass pass1 pass2
  end.

Two valid operations are compared as their {!operation_weight}, see {!compare_operation_weight} for more details.

When they are equal according to their {!operation_weight} comparison, they compare as their hash. Hence, [compare] returns [0] only when the hashes of both operations are equal.

Preconditions: [oph1] is the hash of [op1]; [oph2] the one of [op2]; and [op1] and [op2] are both valid.

Definition compare (function_parameter : Operation_hash.t × packed_operation)
  : Operation_hash.t × packed_operation → int :=
  let '(oph1, op1) := function_parameter in
  fun (function_parameter : Operation_hash.t × packed_operation) ⇒
    let '(oph2, op2) := function_parameter in
    let cmp_h := Operation_hash.compare oph1 oph2 in
    if cmp_h =i 0 then
      0
    else
      let cmp := compare_operation_weight (weight_of op1) (weight_of op2) in
      if cmp =i 0 then
        cmp_h
      else
        cmp.