💸 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 :=
                   &nb