Skip to main content

💸 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.Proto_alpha.Environment.
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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_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_repr.
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.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.

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 seed_nonce_revelation : Set :=
  | Seed_nonce_revelation_kind : seed_nonce_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 set_deposits_limit : Set :=
  | Set_deposits_limit_kind : set_deposits_limit.

  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 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 manager : Set :=
  | Reveal_manager_kind : manager
  | Transaction_manager_kind : manager
  | Origination_manager_kind : manager
  | Delegation_manager_kind : manager
  | Register_global_constant_manager_kind : manager
  | Set_deposits_limit_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
  | 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.
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 t : Set :=
  | Endorsement : Chain_id.t t
  | Preendorsement : Chain_id.t t.
End Consensus_watermark.

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

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

Definition of_watermark (function_parameter : Signature.watermark)
  : option Consensus_watermark.t :=
  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)))
      | _None
      end
    else
      None
  | _None
  end.

Definition raw : Set := Operation.t.

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

Module transaction.
  Record record : Set := Build {
    amount : Tez_repr.tez;
    parameters : Script_repr.lazy_expr;
    entrypoint : Entrypoint_repr.t;
    destination : Destination_repr.t;
  }.
  Definition with_amount amount (r : record) :=
    Build amount r.(parameters) r.(entrypoint) r.(destination).
  Definition with_parameters parameters (r : record) :=
    Build r.(amount) parameters r.(entrypoint) r.(destination).
  Definition with_entrypoint entrypoint (r : record) :=
    Build r.(amount) r.(parameters) entrypoint r.(destination).
  Definition with_destination destination (r : record) :=
    Build r.(amount) r.(parameters) r.(entrypoint) destination.
End transaction.
Definition transaction := transaction.record.

Module origination.
  Record record : Set := Build {
    delegate : option Signature.public_key_hash;
    script : Script_repr.t;
    credit : Tez_repr.tez;
  }.
  Definition with_delegate delegate (r : record) :=
    Build delegate r.(script) r.(credit).
  Definition with_script script (r : record) :=
    Build r.(delegate) script r.(credit).
  Definition with_credit credit (r : record) :=
    Build r.(delegate) r.(script) credit.
End origination.
Definition origination := origination.record.

Records for the constructor parameters
Module ConstructorRecords_manager_operation.
  Module manager_operation.
    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 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 Sc_rollup_originate.
      Record record {kind boot_sector : Set} : Set := Build {
        kind : kind;
        boot_sector : boot_sector;
      }.
      Arguments record : clear implicits.
      Definition with_kind {t_kind t_boot_sector} kind
        (r : record t_kind t_boot_sector) :=
        Build t_kind t_boot_sector kind r.(boot_sector).
      Definition with_boot_sector {t_kind t_boot_sector} boot_sector
        (r : record t_kind t_boot_sector) :=
        Build t_kind t_boot_sector r.(kind) boot_sector.
    End Sc_rollup_originate.
    Definition Sc_rollup_originate_skeleton := Sc_rollup_originate.record.

    Module Sc_rollup_add_messages.
      Record record {rollup messages : Set} : Set := Build {
        rollup : rollup;
        messages : messages;
      }.
      Arguments record : clear implicits.
      Definition with_rollup {t_rollup t_messages} rollup
        (r : record t_rollup t_messages) :=
        Build t_rollup t_messages rollup r.(messages).
      Definition with_messages {t_rollup t_messages} messages
        (r : record t_rollup t_messages) :=
        Build t_rollup t_messages r.(rollup) 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.
  End manager_operation.
End ConstructorRecords_manager_operation.
Import ConstructorRecords_manager_operation.

Reserved Notation "'manager_operation.Register_global_constant".
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.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".

Inductive manager_operation : Set :=
| Reveal : Signature.public_key manager_operation
| Transaction : transaction manager_operation
| Origination : 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
| 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
| 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

where "'manager_operation.Register_global_constant" :=
  (manager_operation.Register_global_constant_skeleton Script_repr.lazy_expr)
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.t)
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 Z.t Contract_repr.t Entrypoint_repr.t)
and "'manager_operation.Sc_rollup_originate" :=
  (manager_operation.Sc_rollup_originate_skeleton Sc_rollup_repr.Kind.t string)
and "'manager_operation.Sc_rollup_add_messages" :=
  (manager_operation.Sc_rollup_add_messages_skeleton Sc_rollup_repr.t
    (list string))
and "'manager_operation.Sc_rollup_cement" :=
  (manager_operation.Sc_rollup_cement_skeleton Sc_rollup_repr.t
    Sc_rollup_repr.Commitment_hash.t)
and "'manager_operation.Sc_rollup_publish" :=
  (manager_operation.Sc_rollup_publish_skeleton Sc_rollup_repr.t
    Sc_rollup_repr.Commitment.t).

Module manager_operation.
  Include ConstructorRecords_manager_operation.manager_operation.
  Definition Register_global_constant :=
    'manager_operation.Register_global_constant.
  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 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.
End manager_operation.

Definition counter : Set := Z.t.

Records for the constructor parameters
Module ConstructorRecords_contents.
  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 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 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.
End ConstructorRecords_contents.
Import ConstructorRecords_contents.

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.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.Manager_operation".
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
| Seed_nonce_revelation : 'contents.Seed_nonce_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
| Failing_noop : string contents
| Manager_operation : 'contents.Manager_operation contents

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.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.Manager_operation" :=
  (contents.Manager_operation_skeleton Signature.public_key_hash Tez_repr.tez
    counter manager_operation Gas_limit_repr.Arith.integral Z.t).

Module contents.
  Include ConstructorRecords_contents.contents.
  Definition Seed_nonce_revelation := 'contents.Seed_nonce_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 Manager_operation := 'contents.Manager_operation.
End contents.

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
  | Tx_rollup_originationKind.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
  | 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
  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 oscons (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 contentsPervasives.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.

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
        | NoneNone
        | Some x_valueSome (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 pkhpkh
              | _unreachable_gadt_branch
              end;
          case.MCase.inj := fun (pkh : Signature.public_key) ⇒ Reveal pkh; |}.

    Definition transaction_tag : int := 1.

    Definition transaction_case : case :=
      MCase
        {| case.MCase.tag := transaction_tag; 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"
                Destination_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 {|
                  transaction.amount := amount;
                    transaction.parameters := parameters;
                    transaction.entrypoint := entrypoint;
                    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 × Destination_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
                {| transaction.amount := amount;
                  transaction.parameters := parameters;
                  transaction.entrypoint := entrypoint;
                  transaction.destination := destination; |}; |}.

    Definition origination_tag : int := 2.

    Definition origination_case : case :=
      MCase
        {| case.MCase.tag := origination_tag; 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 {|
                  origination.delegate := delegate;
                    origination.script := script;
                    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
                {| origination.delegate := delegate;
                  origination.script := script; origination.credit := credit; |};
          |}.

    Definition delegation_tag : int := 3.

    Definition delegation_case : case :=
      MCase
        {| case.MCase.tag := delegation_tag; 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_valuekey_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_valuekey_value
              | _unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (key_value : option Tez_repr.t) ⇒ Set_deposits_limit key_value;
          |}.

    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_originationtt
              | _unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Tx_rollup_origination; |}.

    Definition tx_rollup_batch_content : Data_encoding.encoding string :=
      Data_encoding.conv Bytes.of_string Bytes.to_string None
        Data_encoding.bytes_value.

    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" tx_rollup_batch_content)
              (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.encoding);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Tx_rollup_rejection _) as op) ⇒ Some op
              | _None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Tx_rollup_rejection {|
                  manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
                    manager_operation.Tx_rollup_rejection.level := level;
                    manager_operation.Tx_rollup_rejection.message := message;
                    manager_operation.Tx_rollup_rejection.message_position :=
                      message_position;
                    manager_operation.Tx_rollup_rejection.message_path :=
                      message_path;
                    manager_operation.Tx_rollup_rejection.message_result_hash :=
                      message_result_hash;
                    manager_operation.Tx_rollup_rejection.message_result_path :=
                      message_result_path;
                    manager_operation.Tx_rollup_rejection.previous_message_result
                      := previous_message_result;
                    manager_operation.Tx_rollup_rejection.previous_message_result_path
                      := previous_message_result_path;
                    manager_operation.Tx_rollup_rejection.proof := proof
                    |} ⇒
                (tx_rollup, level, message, (Z.of_int message_position),
                  message_path, message_result_hash, message_result_path,
                  previous_message_result, previous_message_result_path, proof)
              | _unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter :
              Tx_rollup_repr.t × Tx_rollup_level_repr.level ×
                Tx_rollup_message_repr.t × Z.t ×
                Tx_rollup_inbox_repr.Merkle.path ×
                Tx_rollup_message_result_hash_repr.t ×
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path) ×
                Tx_rollup_message_result_repr.t ×
                Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path) ×
                Tx_rollup_l2_proof.t) ⇒
              let
                '(tx_rollup, level, message, message_position, message_path,
                  message_result_hash, message_result_path,
                  previous_message_result, previous_message_result_path, proof) :=
                function_parameter in
              Tx_rollup_rejection
                {| manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
                  manager_operation.Tx_rollup_rejection.level := level;
                  manager_operation.Tx_rollup_rejection.message := message;
                  manager_operation.Tx_rollup_rejection.message_position :=
                    Z.to_int message_position;
                  manager_operation.Tx_rollup_rejection.message_path :=
                    message_path;
                  manager_operation.Tx_rollup_rejection.message_result_hash :=
                    message_result_hash;
                  manager_operation.Tx_rollup_rejection.message_result_path :=
                    message_result_path;
                  manager_operation.Tx_rollup_rejection.previous_message_result
                    := previous_message_result;
                  manager_operation.Tx_rollup_rejection.previous_message_result_path
                    := previous_message_result_path;
                  manager_operation.Tx_rollup_rejection.proof := proof; |}; |}.

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

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

    Definition sc_rollup_originate_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_origination_tag;
          case.MCase.name := "sc_rollup_originate";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "kind" Sc_rollup_repr.Kind.encoding)
              (Data_encoding.req None None "boot_sector"
                Data_encoding.string_value);
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_originate _) as op) ⇒ Some op
              | _None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_originate {|
                  manager_operation.Sc_rollup_originate.kind := kind_value;
                    manager_operation.Sc_rollup_originate.boot_sector :=
                      boot_sector
                    |} ⇒ (kind_value, boot_sector)
              | _unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter : Sc_rollup_repr.Kind.t × string) ⇒
              let '(kind_value, boot_sector) := function_parameter in
              Sc_rollup_originate
                {| manager_operation.Sc_rollup_originate.kind := kind_value;
                  manager_operation.Sc_rollup_originate.boot_sector :=
                    boot_sector; |}; |}.

    Definition sc_rollup_add_messages_case : case :=
      MCase
        {| case.MCase.tag := sc_rollup_operation_add_message_tag;
          case.MCase.name := "sc_rollup_add_messages";
          case.MCase.encoding :=
            Data_encoding.obj2
              (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
              (Data_encoding.req None None "message"
                (Data_encoding.list_value None Data_encoding.string_value));
          case.MCase.select :=
            fun (function_parameter : packed_manager_operation) ⇒
              match function_parameter with
              | Manager ((Sc_rollup_add_messages _) as op) ⇒ Some op
              | _None
              end;
          case.MCase.proj :=
            fun (function_parameter : manager_operation) ⇒
              match function_parameter with
              |
                Sc_rollup_add_messages {|
                  manager_operation.Sc_rollup_add_messages.rollup := rollup;
                    manager_operation.Sc_rollup_add_messages.messages :=
                      messages
                    |} ⇒ (rollup, messages)
              | _unreachable_gadt_branch
              end;
          case.MCase.inj :=
            fun (function_parameter : Sc_rollup_repr.t × list string) ⇒
              let '(rollup, messages) := function_parameter in
              Sc_rollup_add_messages
                {| manager_operation.Sc_rollup_add_messages.rollup := rollup;
                  manager_operation.Sc_rollup_add_messages.messages := messages;
                  |}; |}.

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

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

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

  Reserved Notation "'case.Case".

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

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

  Arguments Case {_ _}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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