💸 Operation_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_update_repr.
Module Kind.
Inductive preendorsement_consensus_kind : Set :=
| Preendorsement_consensus_kind : preendorsement_consensus_kind.
Inductive endorsement_consensus_kind : Set :=
| Endorsement_consensus_kind : endorsement_consensus_kind.
Inductive consensus : Set :=
| Preendorsement_kind : consensus
| Endorsement_kind : consensus.
Definition preendorsement : Set := consensus.
Definition endorsement : Set := consensus.
Inductive dal_attestation : Set :=
| Dal_attestation_kind : dal_attestation.
Inductive seed_nonce_revelation : Set :=
| Seed_nonce_revelation_kind : seed_nonce_revelation.
Inductive vdf_revelation : Set :=
| Vdf_revelation_kind : vdf_revelation.
Inductive double_consensus_operation_evidence : Set :=
| Double_consensus_operation_evidence : double_consensus_operation_evidence.
Definition double_endorsement_evidence : Set :=
double_consensus_operation_evidence.
Definition double_preendorsement_evidence : Set :=
double_consensus_operation_evidence.
Inductive double_baking_evidence : Set :=
| Double_baking_evidence_kind : double_baking_evidence.
Inductive activate_account : Set :=
| Activate_account_kind : activate_account.
Inductive proposals : Set :=
| Proposals_kind : proposals.
Inductive ballot : Set :=
| Ballot_kind : ballot.
Inductive reveal : Set :=
| Reveal_kind : reveal.
Inductive transaction : Set :=
| Transaction_kind : transaction.
Inductive origination : Set :=
| Origination_kind : origination.
Inductive delegation : Set :=
| Delegation_kind : delegation.
Inductive event : Set :=
| Event_kind : event.
Inductive set_deposits_limit : Set :=
| Set_deposits_limit_kind : set_deposits_limit.
Inductive increase_paid_storage : Set :=
| Increase_paid_storage_kind : increase_paid_storage.
Inductive update_consensus_key : Set :=
| Update_consensus_key_kind : update_consensus_key.
Inductive drain_delegate : Set :=
| Drain_delegate_kind : drain_delegate.
Inductive failing_noop : Set :=
| Failing_noop_kind : failing_noop.
Inductive register_global_constant : Set :=
| Register_global_constant_kind : register_global_constant.
Inductive tx_rollup_origination : Set :=
| Tx_rollup_origination_kind : tx_rollup_origination.
Inductive tx_rollup_submit_batch : Set :=
| Tx_rollup_submit_batch_kind : tx_rollup_submit_batch.
Inductive tx_rollup_commit : Set :=
| Tx_rollup_commit_kind : tx_rollup_commit.
Inductive tx_rollup_return_bond : Set :=
| Tx_rollup_return_bond_kind : tx_rollup_return_bond.
Inductive tx_rollup_finalize_commitment : Set :=
| Tx_rollup_finalize_commitment_kind : tx_rollup_finalize_commitment.
Inductive tx_rollup_remove_commitment : Set :=
| Tx_rollup_remove_commitment_kind : tx_rollup_remove_commitment.
Inductive tx_rollup_rejection : Set :=
| Tx_rollup_rejection_kind : tx_rollup_rejection.
Inductive tx_rollup_dispatch_tickets : Set :=
| Tx_rollup_dispatch_tickets_kind : tx_rollup_dispatch_tickets.
Inductive transfer_ticket : Set :=
| Transfer_ticket_kind : transfer_ticket.
Inductive dal_publish_slot_header : Set :=
| Dal_publish_slot_header_kind : dal_publish_slot_header.
Inductive sc_rollup_originate : Set :=
| Sc_rollup_originate_kind : sc_rollup_originate.
Inductive sc_rollup_add_messages : Set :=
| Sc_rollup_add_messages_kind : sc_rollup_add_messages.
Inductive sc_rollup_cement : Set :=
| Sc_rollup_cement_kind : sc_rollup_cement.
Inductive sc_rollup_publish : Set :=
| Sc_rollup_publish_kind : sc_rollup_publish.
Inductive sc_rollup_refute : Set :=
| Sc_rollup_refute_kind : sc_rollup_refute.
Inductive sc_rollup_timeout : Set :=
| Sc_rollup_timeout_kind : sc_rollup_timeout.
Inductive sc_rollup_execute_outbox_message : Set :=
| Sc_rollup_execute_outbox_message_kind : sc_rollup_execute_outbox_message.
Inductive sc_rollup_recover_bond : Set :=
| Sc_rollup_recover_bond_kind : sc_rollup_recover_bond.
Inductive zk_rollup_origination : Set :=
| Zk_rollup_origination_kind : zk_rollup_origination.
Inductive zk_rollup_publish : Set :=
| Zk_rollup_publish_kind : zk_rollup_publish.
Inductive zk_rollup_update : Set :=
| Zk_rollup_update_kind : zk_rollup_update.
Inductive manager : Set :=
| Reveal_manager_kind : manager
| Transaction_manager_kind : manager
| Origination_manager_kind : manager
| Delegation_manager_kind : manager
| Event_manager_kind : manager
| Register_global_constant_manager_kind : manager
| Set_deposits_limit_manager_kind : manager
| Increase_paid_storage_manager_kind : manager
| Update_consensus_key_manager_kind : manager
| Tx_rollup_origination_manager_kind : manager
| Tx_rollup_submit_batch_manager_kind : manager
| Tx_rollup_commit_manager_kind : manager
| Tx_rollup_return_bond_manager_kind : manager
| Tx_rollup_finalize_commitment_manager_kind : manager
| Tx_rollup_remove_commitment_manager_kind : manager
| Tx_rollup_rejection_manager_kind : manager
| Tx_rollup_dispatch_tickets_manager_kind : manager
| Transfer_ticket_manager_kind : manager
| Dal_publish_slot_header_manager_kind : manager
| Sc_rollup_originate_manager_kind : manager
| Sc_rollup_add_messages_manager_kind : manager
| Sc_rollup_cement_manager_kind : manager
| Sc_rollup_publish_manager_kind : manager
| Sc_rollup_refute_manager_kind : manager
| Sc_rollup_timeout_manager_kind : manager
| Sc_rollup_execute_outbox_message_manager_kind : manager
| Sc_rollup_recover_bond_manager_kind : manager
| Zk_rollup_origination_manager_kind : manager
| Zk_rollup_publish_manager_kind : manager
| Zk_rollup_update_manager_kind : manager.
End Kind.
Module Consensus_operation_type.
Inductive t : Set :=
| Endorsement : t
| Preendorsement : t.
Definition pp (ppf : Format.formatter) (operation_kind : t) : unit :=
match operation_kind with
| Endorsement ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Endorsement"
CamlinternalFormatBasics.End_of_format) "Endorsement")
| Preendorsement ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Preendorsement"
CamlinternalFormatBasics.End_of_format) "Preendorsement")
end.
End Consensus_operation_type.
Module consensus_content.
Record record : Set := Build {
slot : Slot_repr.t;
level : Raw_level_repr.t;
round : Round_repr.t;
block_payload_hash : Block_payload_hash.t;
}.
Definition with_slot slot (r : record) :=
Build slot r.(level) r.(round) r.(block_payload_hash).
Definition with_level level (r : record) :=
Build r.(slot) level r.(round) r.(block_payload_hash).
Definition with_round round (r : record) :=
Build r.(slot) r.(level) round r.(block_payload_hash).
Definition with_block_payload_hash block_payload_hash (r : record) :=
Build r.(slot) r.(level) r.(round) block_payload_hash.
End consensus_content.
Definition consensus_content := consensus_content.record.
Definition consensus_content_encoding
: Data_encoding.encoding consensus_content :=
Data_encoding.conv
(fun (function_parameter : consensus_content) ⇒
let '{|
consensus_content.slot := slot;
consensus_content.level := level;
consensus_content.round := round;
consensus_content.block_payload_hash := block_payload_hash
|} := function_parameter in
(slot, level, round, block_payload_hash))
(fun (function_parameter :
Slot_repr.t × Raw_level_repr.t × Round_repr.t × Block_payload_hash.t) ⇒
let '(slot, level, round, block_payload_hash) := function_parameter in
{| consensus_content.slot := slot; consensus_content.level := level;
consensus_content.round := round;
consensus_content.block_payload_hash := block_payload_hash; |}) None
(Data_encoding.obj4 (Data_encoding.req None None "slot" Slot_repr.encoding)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "round" Round_repr.encoding)
(Data_encoding.req None None "block_payload_hash"
Block_payload_hash.encoding)).
Definition pp_consensus_content
(ppf : Format.formatter) (content : consensus_content) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "(" % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))))
"(%ld, %a, %a, %a)")
(Raw_level_repr.to_int32 content.(consensus_content.level)) Round_repr.pp
content.(consensus_content.round) Slot_repr.pp
content.(consensus_content.slot) Block_payload_hash.pp_short
content.(consensus_content.block_payload_hash).
Module Consensus_watermark.
Inductive consensus_watermark : Set :=
| Endorsement : Chain_id.t → consensus_watermark
| Preendorsement : Chain_id.t → consensus_watermark
| Dal_attestation : Chain_id.t → consensus_watermark.
End Consensus_watermark.
Definition bytes_of_consensus_watermark
(function_parameter : Consensus_watermark.consensus_watermark) : bytes :=
match function_parameter with
| Consensus_watermark.Preendorsement chain_id ⇒
Bytes.cat (Bytes.of_string (String.String "018" ""))
(Chain_id.to_bytes chain_id)
|
(Consensus_watermark.Dal_attestation chain_id |
Consensus_watermark.Endorsement chain_id) ⇒
Bytes.cat (Bytes.of_string (String.String "019" ""))
(Chain_id.to_bytes chain_id)
end.
Definition to_watermark (w_value : Consensus_watermark.consensus_watermark)
: Signature.watermark :=
Signature.Custom (bytes_of_consensus_watermark w_value).
Definition of_watermark (function_parameter : Signature.watermark)
: option Consensus_watermark.consensus_watermark :=
match function_parameter with
| Signature.Custom b_value ⇒
if (Bytes.length b_value) >i 0 then
match Bytes.get b_value 0 with
| "018" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Endorsement chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| "019" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Preendorsement chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| "020" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Dal_attestation chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| _ ⇒ None
end
else
None
| _ ⇒ None
end.
Definition raw : Set := Operation.t.
Definition raw_encoding : Data_encoding.t Operation.t := Operation.encoding.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Manager_counter_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_proof.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_update_repr.
Module Kind.
Inductive preendorsement_consensus_kind : Set :=
| Preendorsement_consensus_kind : preendorsement_consensus_kind.
Inductive endorsement_consensus_kind : Set :=
| Endorsement_consensus_kind : endorsement_consensus_kind.
Inductive consensus : Set :=
| Preendorsement_kind : consensus
| Endorsement_kind : consensus.
Definition preendorsement : Set := consensus.
Definition endorsement : Set := consensus.
Inductive dal_attestation : Set :=
| Dal_attestation_kind : dal_attestation.
Inductive seed_nonce_revelation : Set :=
| Seed_nonce_revelation_kind : seed_nonce_revelation.
Inductive vdf_revelation : Set :=
| Vdf_revelation_kind : vdf_revelation.
Inductive double_consensus_operation_evidence : Set :=
| Double_consensus_operation_evidence : double_consensus_operation_evidence.
Definition double_endorsement_evidence : Set :=
double_consensus_operation_evidence.
Definition double_preendorsement_evidence : Set :=
double_consensus_operation_evidence.
Inductive double_baking_evidence : Set :=
| Double_baking_evidence_kind : double_baking_evidence.
Inductive activate_account : Set :=
| Activate_account_kind : activate_account.
Inductive proposals : Set :=
| Proposals_kind : proposals.
Inductive ballot : Set :=
| Ballot_kind : ballot.
Inductive reveal : Set :=
| Reveal_kind : reveal.
Inductive transaction : Set :=
| Transaction_kind : transaction.
Inductive origination : Set :=
| Origination_kind : origination.
Inductive delegation : Set :=
| Delegation_kind : delegation.
Inductive event : Set :=
| Event_kind : event.
Inductive set_deposits_limit : Set :=
| Set_deposits_limit_kind : set_deposits_limit.
Inductive increase_paid_storage : Set :=
| Increase_paid_storage_kind : increase_paid_storage.
Inductive update_consensus_key : Set :=
| Update_consensus_key_kind : update_consensus_key.
Inductive drain_delegate : Set :=
| Drain_delegate_kind : drain_delegate.
Inductive failing_noop : Set :=
| Failing_noop_kind : failing_noop.
Inductive register_global_constant : Set :=
| Register_global_constant_kind : register_global_constant.
Inductive tx_rollup_origination : Set :=
| Tx_rollup_origination_kind : tx_rollup_origination.
Inductive tx_rollup_submit_batch : Set :=
| Tx_rollup_submit_batch_kind : tx_rollup_submit_batch.
Inductive tx_rollup_commit : Set :=
| Tx_rollup_commit_kind : tx_rollup_commit.
Inductive tx_rollup_return_bond : Set :=
| Tx_rollup_return_bond_kind : tx_rollup_return_bond.
Inductive tx_rollup_finalize_commitment : Set :=
| Tx_rollup_finalize_commitment_kind : tx_rollup_finalize_commitment.
Inductive tx_rollup_remove_commitment : Set :=
| Tx_rollup_remove_commitment_kind : tx_rollup_remove_commitment.
Inductive tx_rollup_rejection : Set :=
| Tx_rollup_rejection_kind : tx_rollup_rejection.
Inductive tx_rollup_dispatch_tickets : Set :=
| Tx_rollup_dispatch_tickets_kind : tx_rollup_dispatch_tickets.
Inductive transfer_ticket : Set :=
| Transfer_ticket_kind : transfer_ticket.
Inductive dal_publish_slot_header : Set :=
| Dal_publish_slot_header_kind : dal_publish_slot_header.
Inductive sc_rollup_originate : Set :=
| Sc_rollup_originate_kind : sc_rollup_originate.
Inductive sc_rollup_add_messages : Set :=
| Sc_rollup_add_messages_kind : sc_rollup_add_messages.
Inductive sc_rollup_cement : Set :=
| Sc_rollup_cement_kind : sc_rollup_cement.
Inductive sc_rollup_publish : Set :=
| Sc_rollup_publish_kind : sc_rollup_publish.
Inductive sc_rollup_refute : Set :=
| Sc_rollup_refute_kind : sc_rollup_refute.
Inductive sc_rollup_timeout : Set :=
| Sc_rollup_timeout_kind : sc_rollup_timeout.
Inductive sc_rollup_execute_outbox_message : Set :=
| Sc_rollup_execute_outbox_message_kind : sc_rollup_execute_outbox_message.
Inductive sc_rollup_recover_bond : Set :=
| Sc_rollup_recover_bond_kind : sc_rollup_recover_bond.
Inductive zk_rollup_origination : Set :=
| Zk_rollup_origination_kind : zk_rollup_origination.
Inductive zk_rollup_publish : Set :=
| Zk_rollup_publish_kind : zk_rollup_publish.
Inductive zk_rollup_update : Set :=
| Zk_rollup_update_kind : zk_rollup_update.
Inductive manager : Set :=
| Reveal_manager_kind : manager
| Transaction_manager_kind : manager
| Origination_manager_kind : manager
| Delegation_manager_kind : manager
| Event_manager_kind : manager
| Register_global_constant_manager_kind : manager
| Set_deposits_limit_manager_kind : manager
| Increase_paid_storage_manager_kind : manager
| Update_consensus_key_manager_kind : manager
| Tx_rollup_origination_manager_kind : manager
| Tx_rollup_submit_batch_manager_kind : manager
| Tx_rollup_commit_manager_kind : manager
| Tx_rollup_return_bond_manager_kind : manager
| Tx_rollup_finalize_commitment_manager_kind : manager
| Tx_rollup_remove_commitment_manager_kind : manager
| Tx_rollup_rejection_manager_kind : manager
| Tx_rollup_dispatch_tickets_manager_kind : manager
| Transfer_ticket_manager_kind : manager
| Dal_publish_slot_header_manager_kind : manager
| Sc_rollup_originate_manager_kind : manager
| Sc_rollup_add_messages_manager_kind : manager
| Sc_rollup_cement_manager_kind : manager
| Sc_rollup_publish_manager_kind : manager
| Sc_rollup_refute_manager_kind : manager
| Sc_rollup_timeout_manager_kind : manager
| Sc_rollup_execute_outbox_message_manager_kind : manager
| Sc_rollup_recover_bond_manager_kind : manager
| Zk_rollup_origination_manager_kind : manager
| Zk_rollup_publish_manager_kind : manager
| Zk_rollup_update_manager_kind : manager.
End Kind.
Module Consensus_operation_type.
Inductive t : Set :=
| Endorsement : t
| Preendorsement : t.
Definition pp (ppf : Format.formatter) (operation_kind : t) : unit :=
match operation_kind with
| Endorsement ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Endorsement"
CamlinternalFormatBasics.End_of_format) "Endorsement")
| Preendorsement ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Preendorsement"
CamlinternalFormatBasics.End_of_format) "Preendorsement")
end.
End Consensus_operation_type.
Module consensus_content.
Record record : Set := Build {
slot : Slot_repr.t;
level : Raw_level_repr.t;
round : Round_repr.t;
block_payload_hash : Block_payload_hash.t;
}.
Definition with_slot slot (r : record) :=
Build slot r.(level) r.(round) r.(block_payload_hash).
Definition with_level level (r : record) :=
Build r.(slot) level r.(round) r.(block_payload_hash).
Definition with_round round (r : record) :=
Build r.(slot) r.(level) round r.(block_payload_hash).
Definition with_block_payload_hash block_payload_hash (r : record) :=
Build r.(slot) r.(level) r.(round) block_payload_hash.
End consensus_content.
Definition consensus_content := consensus_content.record.
Definition consensus_content_encoding
: Data_encoding.encoding consensus_content :=
Data_encoding.conv
(fun (function_parameter : consensus_content) ⇒
let '{|
consensus_content.slot := slot;
consensus_content.level := level;
consensus_content.round := round;
consensus_content.block_payload_hash := block_payload_hash
|} := function_parameter in
(slot, level, round, block_payload_hash))
(fun (function_parameter :
Slot_repr.t × Raw_level_repr.t × Round_repr.t × Block_payload_hash.t) ⇒
let '(slot, level, round, block_payload_hash) := function_parameter in
{| consensus_content.slot := slot; consensus_content.level := level;
consensus_content.round := round;
consensus_content.block_payload_hash := block_payload_hash; |}) None
(Data_encoding.obj4 (Data_encoding.req None None "slot" Slot_repr.encoding)
(Data_encoding.req None None "level" Raw_level_repr.encoding)
(Data_encoding.req None None "round" Round_repr.encoding)
(Data_encoding.req None None "block_payload_hash"
Block_payload_hash.encoding)).
Definition pp_consensus_content
(ppf : Format.formatter) (content : consensus_content) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "(" % char
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))))
"(%ld, %a, %a, %a)")
(Raw_level_repr.to_int32 content.(consensus_content.level)) Round_repr.pp
content.(consensus_content.round) Slot_repr.pp
content.(consensus_content.slot) Block_payload_hash.pp_short
content.(consensus_content.block_payload_hash).
Module Consensus_watermark.
Inductive consensus_watermark : Set :=
| Endorsement : Chain_id.t → consensus_watermark
| Preendorsement : Chain_id.t → consensus_watermark
| Dal_attestation : Chain_id.t → consensus_watermark.
End Consensus_watermark.
Definition bytes_of_consensus_watermark
(function_parameter : Consensus_watermark.consensus_watermark) : bytes :=
match function_parameter with
| Consensus_watermark.Preendorsement chain_id ⇒
Bytes.cat (Bytes.of_string (String.String "018" ""))
(Chain_id.to_bytes chain_id)
|
(Consensus_watermark.Dal_attestation chain_id |
Consensus_watermark.Endorsement chain_id) ⇒
Bytes.cat (Bytes.of_string (String.String "019" ""))
(Chain_id.to_bytes chain_id)
end.
Definition to_watermark (w_value : Consensus_watermark.consensus_watermark)
: Signature.watermark :=
Signature.Custom (bytes_of_consensus_watermark w_value).
Definition of_watermark (function_parameter : Signature.watermark)
: option Consensus_watermark.consensus_watermark :=
match function_parameter with
| Signature.Custom b_value ⇒
if (Bytes.length b_value) >i 0 then
match Bytes.get b_value 0 with
| "018" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Endorsement chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| "019" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Preendorsement chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| "020" % char ⇒
Option.map
(fun (chain_id : Chain_id.t) ⇒
Consensus_watermark.Dal_attestation chain_id)
(Chain_id.of_bytes_opt
(Bytes.sub b_value 1 ((Bytes.length b_value) -i 1)))
| _ ⇒ None
end
else
None
| _ ⇒ None
end.
Definition raw : Set := Operation.t.
Definition raw_encoding : Data_encoding.t Operation.t := Operation.encoding.
Records for the constructor parameters
Module ConstructorRecords_contents_manager_operation.
Module contents.
Module Seed_nonce_revelation.
Record record {level nonce : Set} : Set := Build {
level : level;
nonce : nonce;
}.
Arguments record : clear implicits.
Definition with_level {t_level t_nonce} level
(r : record t_level t_nonce) :=
Build t_level t_nonce level r.(nonce).
Definition with_nonce {t_level t_nonce} nonce
(r : record t_level t_nonce) :=
Build t_level t_nonce r.(level) nonce.
End Seed_nonce_revelation.
Definition Seed_nonce_revelation_skeleton := Seed_nonce_revelation.record.
Module Vdf_revelation.
Record record {solution : Set} : Set := Build {
solution : solution;
}.
Arguments record : clear implicits.
Definition with_solution {t_solution} solution (r : record t_solution) :=
Build t_solution solution.
End Vdf_revelation.
Definition Vdf_revelation_skeleton := Vdf_revelation.record.
Module Double_preendorsement_evidence.
Record record {op1 op2 : Set} : Set := Build {
op1 : op1;
op2 : op2;
}.
Arguments record : clear implicits.
Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 op1 r.(op2).
Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 r.(op1) op2.
End Double_preendorsement_evidence.
Definition Double_preendorsement_evidence_skeleton :=
Double_preendorsement_evidence.record.
Module Double_endorsement_evidence.
Record record {op1 op2 : Set} : Set := Build {
op1 : op1;
op2 : op2;
}.
Arguments record : clear implicits.
Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 op1 r.(op2).
Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 r.(op1) op2.
End Double_endorsement_evidence.
Definition Double_endorsement_evidence_skeleton :=
Double_endorsement_evidence.record.
Module Double_baking_evidence.
Record record {bh1 bh2 : Set} : Set := Build {
bh1 : bh1;
bh2 : bh2;
}.
Arguments record : clear implicits.
Definition with_bh1 {t_bh1 t_bh2} bh1 (r : record t_bh1 t_bh2) :=
Build t_bh1 t_bh2 bh1 r.(bh2).
Definition with_bh2 {t_bh1 t_bh2} bh2 (r : record t_bh1 t_bh2) :=
Build t_bh1 t_bh2 r.(bh1) bh2.
End Double_baking_evidence.
Definition Double_baking_evidence_skeleton := Double_baking_evidence.record.
Module Activate_account.
Record record {id activation_code : Set} : Set := Build {
id : id;
activation_code : activation_code;
}.
Arguments record : clear implicits.
Definition with_id {t_id t_activation_code} id
(r : record t_id t_activation_code) :=
Build t_id t_activation_code id r.(activation_code).
Definition with_activation_code {t_id t_activation_code} activation_code
(r : record t_id t_activation_code) :=
Build t_id t_activation_code r.(id) activation_code.
End Activate_account.
Definition Activate_account_skeleton := Activate_account.record.
Module Proposals.
Record record {source period proposals : Set} : Set := Build {
source : source;
period : period;
proposals : proposals;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_period t_proposals} source
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals source r.(period) r.(proposals).
Definition with_period {t_source t_period t_proposals} period
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals r.(source) period r.(proposals).
Definition with_proposals {t_source t_period t_proposals} proposals
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals r.(source) r.(period) proposals.
End Proposals.
Definition Proposals_skeleton := Proposals.record.
Module Ballot.
Record record {source period proposal ballot : Set} : Set := Build {
source : source;
period : period;
proposal : proposal;
ballot : ballot;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_period t_proposal t_ballot} source
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot source r.(period)
r.(proposal) r.(ballot).
Definition with_period {t_source t_period t_proposal t_ballot} period
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) period
r.(proposal) r.(ballot).
Definition with_proposal {t_source t_period t_proposal t_ballot} proposal
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) r.(period)
proposal r.(ballot).
Definition with_ballot {t_source t_period t_proposal t_ballot} ballot
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) r.(period)
r.(proposal) ballot.
End Ballot.
Definition Ballot_skeleton := Ballot.record.
Module Drain_delegate.
Record record {consensus_key delegate destination : Set} : Set := Build {
consensus_key : consensus_key;
delegate : delegate;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_consensus_key {t_consensus_key t_delegate t_destination}
consensus_key (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination consensus_key
r.(delegate) r.(destination).
Definition with_delegate {t_consensus_key t_delegate t_destination}
delegate (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination r.(consensus_key)
delegate r.(destination).
Definition with_destination {t_consensus_key t_delegate t_destination}
destination (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination r.(consensus_key)
r.(delegate) destination.
End Drain_delegate.
Definition Drain_delegate_skeleton := Drain_delegate.record.
Module Manager_operation.
Record record {source fee counter operation gas_limit storage_limit : Set} :
Set := Build {
source : source;
fee : fee;
counter : counter;
operation : operation;
gas_limit : gas_limit;
storage_limit : storage_limit;
}.
Arguments record : clear implicits.
Definition with_source
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
source
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
source r.(fee) r.(counter) r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_fee
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit} fee
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) fee r.(counter) r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_counter
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
counter
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) counter r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_operation
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
operation
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) operation r.(gas_limit)
r.(storage_limit).
Definition with_gas_limit
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
gas_limit
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) r.(operation) gas_limit
r.(storage_limit).
Definition with_storage_limit
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
storage_limit
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) r.(operation) r.(gas_limit)
storage_limit.
End Manager_operation.
Definition Manager_operation_skeleton := Manager_operation.record.
End contents.
Module manager_operation.
Module Transaction.
Record record {amount parameters entrypoint destination : Set} : Set := Build {
amount : amount;
parameters : parameters;
entrypoint : entrypoint;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_amount {t_amount t_parameters t_entrypoint t_destination}
amount (r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination amount
r.(parameters) r.(entrypoint) r.(destination).
Definition with_parameters
{t_amount t_parameters t_entrypoint t_destination} parameters
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
parameters r.(entrypoint) r.(destination).
Definition with_entrypoint
{t_amount t_parameters t_entrypoint t_destination} entrypoint
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
r.(parameters) entrypoint r.(destination).
Definition with_destination
{t_amount t_parameters t_entrypoint t_destination} destination
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
r.(parameters) r.(entrypoint) destination.
End Transaction.
Definition Transaction_skeleton := Transaction.record.
Module Origination.
Record record {delegate script credit : Set} : Set := Build {
delegate : delegate;
script : script;
credit : credit;
}.
Arguments record : clear implicits.
Definition with_delegate {t_delegate t_script t_credit} delegate
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit delegate r.(script) r.(credit).
Definition with_script {t_delegate t_script t_credit} script
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit r.(delegate) script r.(credit).
Definition with_credit {t_delegate t_script t_credit} credit
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit r.(delegate) r.(script) credit.
End Origination.
Definition Origination_skeleton := Origination.record.
Module Register_global_constant.
Record record {value : Set} : Set := Build {
value : value;
}.
Arguments record : clear implicits.
Definition with_value {t_value} value (r : record t_value) :=
Build t_value value.
End Register_global_constant.
Definition Register_global_constant_skeleton :=
Register_global_constant.record.
Module Increase_paid_storage.
Record record {amount_in_bytes destination : Set} : Set := Build {
amount_in_bytes : amount_in_bytes;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_amount_in_bytes {t_amount_in_bytes t_destination}
amount_in_bytes (r : record t_amount_in_bytes t_destination) :=
Build t_amount_in_bytes t_destination amount_in_bytes r.(destination).
Definition with_destination {t_amount_in_bytes t_destination} destination
(r : record t_amount_in_bytes t_destination) :=
Build t_amount_in_bytes t_destination r.(amount_in_bytes) destination.
End Increase_paid_storage.
Definition Increase_paid_storage_skeleton := Increase_paid_storage.record.
Module Tx_rollup_submit_batch.
Record record {tx_rollup content burn_limit : Set} : Set := Build {
tx_rollup : tx_rollup;
content : content;
burn_limit : burn_limit;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup t_content t_burn_limit} tx_rollup
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit tx_rollup r.(content)
r.(burn_limit).
Definition with_content {t_tx_rollup t_content t_burn_limit} content
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) content
r.(burn_limit).
Definition with_burn_limit {t_tx_rollup t_content t_burn_limit} burn_limit
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) r.(content)
burn_limit.
End Tx_rollup_submit_batch.
Definition Tx_rollup_submit_batch_skeleton := Tx_rollup_submit_batch.record.
Module Tx_rollup_commit.
Record record {tx_rollup commitment : Set} : Set := Build {
tx_rollup : tx_rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup t_commitment} tx_rollup
(r : record t_tx_rollup t_commitment) :=
Build t_tx_rollup t_commitment tx_rollup r.(commitment).
Definition with_commitment {t_tx_rollup t_commitment} commitment
(r : record t_tx_rollup t_commitment) :=
Build t_tx_rollup t_commitment r.(tx_rollup) commitment.
End Tx_rollup_commit.
Definition Tx_rollup_commit_skeleton := Tx_rollup_commit.record.
Module Tx_rollup_return_bond.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_return_bond.
Definition Tx_rollup_return_bond_skeleton := Tx_rollup_return_bond.record.
Module Tx_rollup_finalize_commitment.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_finalize_commitment.
Definition Tx_rollup_finalize_commitment_skeleton :=
Tx_rollup_finalize_commitment.record.
Module Tx_rollup_remove_commitment.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_remove_commitment.
Definition Tx_rollup_remove_commitment_skeleton :=
Tx_rollup_remove_commitment.record.
Module Tx_rollup_rejection.
Record record {tx_rollup level message message_position message_path
message_result_hash message_result_path previous_message_result
previous_message_result_path proof : Set} : Set := Build {
tx_rollup : tx_rollup;
level : level;
message : message;
message_position : message_position;
message_path : message_path;
message_result_hash : message_result_hash;
message_result_path : message_result_path;
previous_message_result : previous_message_result;
previous_message_result_path : previous_message_result_path;
proof : proof;
}.
Arguments record : clear implicits.
Definition with_tx_rollup
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} tx_rollup
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof tx_rollup r.(level) r.(message)
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_level
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} level
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) level r.(message)
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level) message
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_position
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_position
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) message_position r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) message_path r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_result_hash
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_result_hash
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path) message_result_hash
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_result_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_result_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) message_result_path
r.(previous_message_result) r.(previous_message_result_path)
r.(proof).
Definition with_previous_message_result
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} previous_message_result
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
previous_message_result r.(previous_message_result_path) r.(proof).
Definition with_previous_message_result_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} previous_message_result_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
r.(previous_message_result) previous_message_result_path r.(proof).
Definition with_proof
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} proof
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
r.(previous_message_result) r.(previous_message_result_path) proof.
End Tx_rollup_rejection.
Definition Tx_rollup_rejection_skeleton := Tx_rollup_rejection.record.
Module Tx_rollup_dispatch_tickets.
Record record {tx_rollup level context_hash message_index
message_result_path tickets_info : Set} : Set := Build {
tx_rollup : tx_rollup;
level : level;
context_hash : context_hash;
message_index : message_index;
message_result_path : message_result_path;
tickets_info : tickets_info;
}.
Arguments record : clear implicits.
Definition with_tx_rollup
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} tx_rollup
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info tx_rollup r.(level)
r.(context_hash) r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_level
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} level
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) level
r.(context_hash) r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_context_hash
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} context_hash
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
context_hash r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_message_index
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} message_index
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) message_index r.(message_result_path)
r.(tickets_info).
Definition with_message_result_path
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} message_result_path
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) r.(message_index) message_result_path
r.(tickets_info).
Definition with_tickets_info
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} tickets_info
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) r.(message_index) r.(message_result_path)
tickets_info.
End Tx_rollup_dispatch_tickets.
Definition Tx_rollup_dispatch_tickets_skeleton :=
Tx_rollup_dispatch_tickets.record.
Module Transfer_ticket.
Record record {contents ty ticketer amount destination entrypoint : Set} :
Set := Build {
contents : contents;
ty : ty;
ticketer : ticketer;
amount : amount;
destination : destination;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_contents
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
contents
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
contents r.(ty) r.(ticketer) r.(amount) r.(destination)
r.(entrypoint).
Definition with_ty
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} ty
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) ty r.(ticketer) r.(amount) r.(destination)
r.(entrypoint).
Definition with_ticketer
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
ticketer
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) ticketer r.(amount) r.(destination)
r.(entrypoint).
Definition with_amount
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} amount
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) amount r.(destination)
r.(entrypoint).
Definition with_destination
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
destination
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) r.(amount) destination
r.(entrypoint).
Definition with_entrypoint
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
entrypoint
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) r.(amount) r.(destination)
entrypoint.
End Transfer_ticket.
Definition Transfer_ticket_skeleton := Transfer_ticket.record.
Module Dal_publish_slot_header.
Record record {slot_header : Set} : Set := Build {
slot_header : slot_header;
}.
Arguments record : clear implicits.
Definition with_slot_header {t_slot_header} slot_header
(r : record t_slot_header) :=
Build t_slot_header slot_header.
End Dal_publish_slot_header.
Definition Dal_publish_slot_header_skeleton :=
Dal_publish_slot_header.record.
Module Sc_rollup_originate.
Record record {kind boot_sector origination_proof parameters_ty : Set} :
Set := Build {
kind : kind;
boot_sector : boot_sector;
origination_proof : origination_proof;
parameters_ty : parameters_ty;
}.
Arguments record : clear implicits.
Definition with_kind
{t_kind t_boot_sector t_origination_proof t_parameters_ty} kind
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty kind
r.(boot_sector) r.(origination_proof) r.(parameters_ty).
Definition with_boot_sector
{t_kind t_boot_sector t_origination_proof t_parameters_ty} boot_sector
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
boot_sector r.(origination_proof) r.(parameters_ty).
Definition with_origination_proof
{t_kind t_boot_sector t_origination_proof t_parameters_ty}
origination_proof
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
r.(boot_sector) origination_proof r.(parameters_ty).
Definition with_parameters_ty
{t_kind t_boot_sector t_origination_proof t_parameters_ty} parameters_ty
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
r.(boot_sector) r.(origination_proof) parameters_ty.
End Sc_rollup_originate.
Definition Sc_rollup_originate_skeleton := Sc_rollup_originate.record.
Module Sc_rollup_add_messages.
Record record {messages : Set} : Set := Build {
messages : messages;
}.
Arguments record : clear implicits.
Definition with_messages {t_messages} messages (r : record t_messages) :=
Build t_messages messages.
End Sc_rollup_add_messages.
Definition Sc_rollup_add_messages_skeleton := Sc_rollup_add_messages.record.
Module Sc_rollup_cement.
Record record {rollup commitment : Set} : Set := Build {
rollup : rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_commitment} rollup
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment rollup r.(commitment).
Definition with_commitment {t_rollup t_commitment} commitment
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment r.(rollup) commitment.
End Sc_rollup_cement.
Definition Sc_rollup_cement_skeleton := Sc_rollup_cement.record.
Module Sc_rollup_publish.
Record record {rollup commitment : Set} : Set := Build {
rollup : rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_commitment} rollup
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment rollup r.(commitment).
Definition with_commitment {t_rollup t_commitment} commitment
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment r.(rollup) commitment.
End Sc_rollup_publish.
Definition Sc_rollup_publish_skeleton := Sc_rollup_publish.record.
Module Sc_rollup_refute.
Record record {rollup opponent refutation : Set} : Set := Build {
rollup : rollup;
opponent : opponent;
refutation : refutation;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_opponent t_refutation} rollup
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation rollup r.(opponent)
r.(refutation).
Definition with_opponent {t_rollup t_opponent t_refutation} opponent
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation r.(rollup) opponent
r.(refutation).
Definition with_refutation {t_rollup t_opponent t_refutation} refutation
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation r.(rollup) r.(opponent)
refutation.
End Sc_rollup_refute.
Definition Sc_rollup_refute_skeleton := Sc_rollup_refute.record.
Module Sc_rollup_timeout.
Record record {rollup stakers : Set} : Set := Build {
rollup : rollup;
stakers : stakers;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_stakers} rollup
(r : record t_rollup t_stakers) :=
Build t_rollup t_stakers rollup r.(stakers).
Definition with_stakers {t_rollup t_stakers} stakers
(r : record t_rollup t_stakers) :=
Build t_rollup t_stakers r.(rollup) stakers.
End Sc_rollup_timeout.
Definition Sc_rollup_timeout_skeleton := Sc_rollup_timeout.record.
Module Sc_rollup_execute_outbox_message.
Record record {rollup cemented_commitment output_proof : Set} : Set := Build {
rollup : rollup;
cemented_commitment : cemented_commitment;
output_proof : output_proof;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_cemented_commitment t_output_proof}
rollup (r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof rollup
r.(cemented_commitment) r.(output_proof).
Definition with_cemented_commitment
{t_rollup t_cemented_commitment t_output_proof} cemented_commitment
(r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
cemented_commitment r.(output_proof).
Definition with_output_proof
{t_rollup t_cemented_commitment t_output_proof} output_proof
(r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
r.(cemented_commitment) output_proof.
End Sc_rollup_execute_outbox_message.
Definition Sc_rollup_execute_outbox_message_skeleton :=
Sc_rollup_execute_outbox_message.record.
Module Sc_rollup_recover_bond.
Record record {sc_rollup : Set} : Set := Build {
sc_rollup : sc_rollup;
}.
Arguments record : clear implicits.
Definition with_sc_rollup {t_sc_rollup} sc_rollup
(r : record t_sc_rollup) :=
Build t_sc_rollup sc_rollup.
End Sc_rollup_recover_bond.
Definition Sc_rollup_recover_bond_skeleton := Sc_rollup_recover_bond.record.
Module Zk_rollup_origination.
Record record {public_parameters circuits_info init_state nb_ops : Set} :
Set := Build {
public_parameters : public_parameters;
circuits_info : circuits_info;
init_state : init_state;
nb_ops : nb_ops;
}.
Arguments record : clear implicits.
Definition with_public_parameters
{t_public_parameters t_circuits_info t_init_state t_nb_ops}
public_parameters
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
public_parameters r.(circuits_info) r.(init_state) r.(nb_ops).
Definition with_circuits_info
{t_public_parameters t_circuits_info t_init_state t_nb_ops}
circuits_info
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) circuits_info r.(init_state) r.(nb_ops).
Definition with_init_state
{t_public_parameters t_circuits_info t_init_state t_nb_ops} init_state
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) r.(circuits_info) init_state r.(nb_ops).
Definition with_nb_ops
{t_public_parameters t_circuits_info t_init_state t_nb_ops} nb_ops
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) r.(circuits_info) r.(init_state) nb_ops.
End Zk_rollup_origination.
Definition Zk_rollup_origination_skeleton := Zk_rollup_origination.record.
Module Zk_rollup_publish.
Record record {zk_rollup ops : Set} : Set := Build {
zk_rollup : zk_rollup;
ops : ops;
}.
Arguments record : clear implicits.
Definition with_zk_rollup {t_zk_rollup t_ops} zk_rollup
(r : record t_zk_rollup t_ops) :=
Build t_zk_rollup t_ops zk_rollup r.(ops).
Definition with_ops {t_zk_rollup t_ops} ops
(r : record t_zk_rollup t_ops) :=
Build t_zk_rollup t_ops r.(zk_rollup) ops.
End Zk_rollup_publish.
Definition Zk_rollup_publish_skeleton := Zk_rollup_publish.record.
Module Zk_rollup_update.
Record record {zk_rollup update : Set} : Set := Build {
zk_rollup : zk_rollup;
update : update;
}.
Arguments record : clear implicits.
Definition with_zk_rollup {t_zk_rollup t_update} zk_rollup
(r : record t_zk_rollup t_update) :=
Build t_zk_rollup t_update zk_rollup r.(update).
Definition with_update {t_zk_rollup t_update} update
(r : record t_zk_rollup t_update) :=
Build t_zk_rollup t_update r.(zk_rollup) update.
End Zk_rollup_update.
Definition Zk_rollup_update_skeleton := Zk_rollup_update.record.
End manager_operation.
End ConstructorRecords_contents_manager_operation.
Import ConstructorRecords_contents_manager_operation.
Module protocol_data.
Record record {contents signature : Set} : Set := Build {
contents : contents;
signature : signature;
}.
Arguments record : clear implicits.
Definition with_contents {t_contents t_signature} contents
(r : record t_contents t_signature) :=
Build t_contents t_signature contents r.(signature).
Definition with_signature {t_contents t_signature} signature
(r : record t_contents t_signature) :=
Build t_contents t_signature r.(contents) signature.
End protocol_data.
Definition protocol_data_skeleton := protocol_data.record.
Module operation.
Record record {shell protocol_data : Set} : Set := Build {
shell : shell;
protocol_data : protocol_data;
}.
Arguments record : clear implicits.
Definition with_shell {t_shell t_protocol_data} shell
(r : record t_shell t_protocol_data) :=
Build t_shell t_protocol_data shell r.(protocol_data).
Definition with_protocol_data {t_shell t_protocol_data} protocol_data
(r : record t_shell t_protocol_data) :=
Build t_shell t_protocol_data r.(shell) protocol_data.
End operation.
Definition operation_skeleton := operation.record.
Reserved Notation "'contents.Seed_nonce_revelation".
Reserved Notation "'contents.Vdf_revelation".
Reserved Notation "'contents.Double_preendorsement_evidence".
Reserved Notation "'contents.Double_endorsement_evidence".
Reserved Notation "'contents.Double_baking_evidence".
Reserved Notation "'contents.Activate_account".
Reserved Notation "'contents.Proposals".
Reserved Notation "'contents.Ballot".
Reserved Notation "'contents.Drain_delegate".
Reserved Notation "'contents.Manager_operation".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'manager_operation.Register_global_constant".
Reserved Notation "'manager_operation.Increase_paid_storage".
Reserved Notation "'manager_operation.Tx_rollup_submit_batch".
Reserved Notation "'manager_operation.Tx_rollup_commit".
Reserved Notation "'manager_operation.Tx_rollup_return_bond".
Reserved Notation "'manager_operation.Tx_rollup_finalize_commitment".
Reserved Notation "'manager_operation.Tx_rollup_remove_commitment".
Reserved Notation "'manager_operation.Tx_rollup_rejection".
Reserved Notation "'manager_operation.Tx_rollup_dispatch_tickets".
Reserved Notation "'manager_operation.Transfer_ticket".
Reserved Notation "'manager_operation.Dal_publish_slot_header".
Reserved Notation "'manager_operation.Sc_rollup_originate".
Reserved Notation "'manager_operation.Sc_rollup_add_messages".
Reserved Notation "'manager_operation.Sc_rollup_cement".
Reserved Notation "'manager_operation.Sc_rollup_publish".
Reserved Notation "'manager_operation.Sc_rollup_refute".
Reserved Notation "'manager_operation.Sc_rollup_timeout".
Reserved Notation "'manager_operation.Sc_rollup_execute_outbox_message".
Reserved Notation "'manager_operation.Sc_rollup_recover_bond".
Reserved Notation "'manager_operation.Zk_rollup_origination".
Reserved Notation "'manager_operation.Zk_rollup_publish".
Reserved Notation "'manager_operation.Zk_rollup_update".
Reserved Notation "'operation".
Reserved Notation "'protocol_data".
Inductive contents_list : Set :=
| Single : contents → contents_list
| Cons : contents → contents_list → contents_list
with contents : Set :=
| Preendorsement : consensus_content → contents
| Endorsement : consensus_content → contents
| Dal_attestation : Dal_attestation_repr.operation → contents
| Seed_nonce_revelation : 'contents.Seed_nonce_revelation → contents
| Vdf_revelation : 'contents.Vdf_revelation → contents
| Double_preendorsement_evidence :
'contents.Double_preendorsement_evidence → contents
| Double_endorsement_evidence :
'contents.Double_endorsement_evidence → contents
| Double_baking_evidence : 'contents.Double_baking_evidence → contents
| Activate_account : 'contents.Activate_account → contents
| Proposals : 'contents.Proposals → contents
| Ballot : 'contents.Ballot → contents
| Drain_delegate : 'contents.Drain_delegate → contents
| Failing_noop : string → contents
| Manager_operation : 'contents.Manager_operation → contents
with manager_operation : Set :=
| Reveal : Signature.public_key → manager_operation
| Transaction : 'manager_operation.Transaction → manager_operation
| Origination : 'manager_operation.Origination → manager_operation
| Delegation : option Signature.public_key_hash → manager_operation
| Register_global_constant :
'manager_operation.Register_global_constant → manager_operation
| Set_deposits_limit : option Tez_repr.t → manager_operation
| Increase_paid_storage :
'manager_operation.Increase_paid_storage → manager_operation
| Update_consensus_key : Signature.public_key → manager_operation
| Tx_rollup_origination : manager_operation
| Tx_rollup_submit_batch :
'manager_operation.Tx_rollup_submit_batch → manager_operation
| Tx_rollup_commit : 'manager_operation.Tx_rollup_commit → manager_operation
| Tx_rollup_return_bond :
'manager_operation.Tx_rollup_return_bond → manager_operation
| Tx_rollup_finalize_commitment :
'manager_operation.Tx_rollup_finalize_commitment → manager_operation
| Tx_rollup_remove_commitment :
'manager_operation.Tx_rollup_remove_commitment → manager_operation
| Tx_rollup_rejection :
'manager_operation.Tx_rollup_rejection → manager_operation
| Tx_rollup_dispatch_tickets :
'manager_operation.Tx_rollup_dispatch_tickets → manager_operation
| Transfer_ticket : 'manager_operation.Transfer_ticket → manager_operation
| Dal_publish_slot_header :
'manager_operation.Dal_publish_slot_header → manager_operation
| Sc_rollup_originate :
'manager_operation.Sc_rollup_originate → manager_operation
| Sc_rollup_add_messages :
'manager_operation.Sc_rollup_add_messages → manager_operation
| Sc_rollup_cement : 'manager_operation.Sc_rollup_cement → manager_operation
| Sc_rollup_publish : 'manager_operation.Sc_rollup_publish → manager_operation
| Sc_rollup_refute : 'manager_operation.Sc_rollup_refute → manager_operation
| Sc_rollup_timeout : 'manager_operation.Sc_rollup_timeout → manager_operation
| Sc_rollup_execute_outbox_message :
'manager_operation.Sc_rollup_execute_outbox_message → manager_operation
| Sc_rollup_recover_bond :
'manager_operation.Sc_rollup_recover_bond → manager_operation
| Zk_rollup_origination :
'manager_operation.Zk_rollup_origination → manager_operation
| Zk_rollup_publish : 'manager_operation.Zk_rollup_publish → manager_operation
| Zk_rollup_update : 'manager_operation.Zk_rollup_update → manager_operation
where "'protocol_data" :=
(protocol_data_skeleton contents_list (option Signature.t))
and "'operation" := (operation_skeleton Operation.shell_header 'protocol_data)
and "'contents.Seed_nonce_revelation" :=
(contents.Seed_nonce_revelation_skeleton Raw_level_repr.t Seed_repr.nonce)
and "'contents.Vdf_revelation" :=
(contents.Vdf_revelation_skeleton Seed_repr.vdf_solution)
and "'contents.Double_preendorsement_evidence" :=
(contents.Double_preendorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_endorsement_evidence" :=
(contents.Double_endorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_baking_evidence" :=
(contents.Double_baking_evidence_skeleton Block_header_repr.t
Block_header_repr.t)
and "'contents.Activate_account" :=
(contents.Activate_account_skeleton
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)
Blinded_public_key_hash.activation_code)
and "'contents.Proposals" :=
(contents.Proposals_skeleton Signature.public_key_hash int32
(list Protocol_hash.t))
and "'contents.Ballot" :=
(contents.Ballot_skeleton Signature.public_key_hash int32 Protocol_hash.t
Vote_repr.ballot)
and "'contents.Drain_delegate" :=
(contents.Drain_delegate_skeleton Signature.public_key_hash
Signature.public_key_hash Signature.public_key_hash)
and "'contents.Manager_operation" :=
(contents.Manager_operation_skeleton Signature.public_key_hash Tez_repr.tez
Manager_counter_repr.t manager_operation Gas_limit_repr.Arith.integral Z.t)
and "'manager_operation.Transaction" :=
(manager_operation.Transaction_skeleton Tez_repr.tez Script_repr.lazy_expr
Entrypoint_repr.t Contract_repr.t)
and "'manager_operation.Origination" :=
(manager_operation.Origination_skeleton (option Signature.public_key_hash)
Script_repr.t Tez_repr.tez)
and "'manager_operation.Register_global_constant" :=
(manager_operation.Register_global_constant_skeleton Script_repr.lazy_expr)
and "'manager_operation.Increase_paid_storage" :=
(manager_operation.Increase_paid_storage_skeleton Z.t Contract_hash.t)
and "'manager_operation.Tx_rollup_submit_batch" :=
(manager_operation.Tx_rollup_submit_batch_skeleton Tx_rollup_repr.t string
(option Tez_repr.t))
and "'manager_operation.Tx_rollup_commit" :=
(manager_operation.Tx_rollup_commit_skeleton Tx_rollup_repr.t
Tx_rollup_commitment_repr.Full.t)
and "'manager_operation.Tx_rollup_return_bond" :=
(manager_operation.Tx_rollup_return_bond_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_finalize_commitment" :=
(manager_operation.Tx_rollup_finalize_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_remove_commitment" :=
(manager_operation.Tx_rollup_remove_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_rejection" :=
(manager_operation.Tx_rollup_rejection_skeleton Tx_rollup_repr.t
Tx_rollup_level_repr.t Tx_rollup_message_repr.t int
Tx_rollup_inbox_repr.Merkle.path Tx_rollup_message_result_hash_repr.t
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
Tx_rollup_message_result_repr.t
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
Tx_rollup_l2_proof.serialized)
and "'manager_operation.Tx_rollup_dispatch_tickets" :=
(manager_operation.Tx_rollup_dispatch_tickets_skeleton Tx_rollup_repr.t
Tx_rollup_level_repr.t Context_hash.t int
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
(list Tx_rollup_reveal_repr.t))
and "'manager_operation.Transfer_ticket" :=
(manager_operation.Transfer_ticket_skeleton Script_repr.lazy_expr
Script_repr.lazy_expr Contract_repr.t Ticket_amount.t Contract_repr.t
Entrypoint_repr.t)
and "'manager_operation.Dal_publish_slot_header" :=
(manager_operation.Dal_publish_slot_header_skeleton Dal_slot_repr.Header.t)
and "'manager_operation.Sc_rollup_originate" :=
(manager_operation.Sc_rollup_originate_skeleton Sc_rollups.Kind.t string
string Script_repr.lazy_expr)
and "'manager_operation.Sc_rollup_add_messages" :=
(manager_operation.Sc_rollup_add_messages_skeleton (list string))
and "'manager_operation.Sc_rollup_cement" :=
(manager_operation.Sc_rollup_cement_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.Hash.t)
and "'manager_operation.Sc_rollup_publish" :=
(manager_operation.Sc_rollup_publish_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.t)
and "'manager_operation.Sc_rollup_refute" :=
(manager_operation.Sc_rollup_refute_skeleton Sc_rollup_repr.t
Signature.public_key_hash (option Sc_rollup_game_repr.refutation))
and "'manager_operation.Sc_rollup_timeout" :=
(manager_operation.Sc_rollup_timeout_skeleton Sc_rollup_repr.t
Sc_rollup_game_repr.Index.t)
and "'manager_operation.Sc_rollup_execute_outbox_message" :=
(manager_operation.Sc_rollup_execute_outbox_message_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.Hash.t string)
and "'manager_operation.Sc_rollup_recover_bond" :=
(manager_operation.Sc_rollup_recover_bond_skeleton Sc_rollup_repr.t)
and "'manager_operation.Zk_rollup_origination" :=
(manager_operation.Zk_rollup_origination_skeleton Plonk.public_parameters
(Zk_rollup_account_repr.SMap.(Map.S.t) Zk_rollup_account_repr.circuit_info)
Zk_rollup_state_repr.t int)
and "'manager_operation.Zk_rollup_publish" :=
(manager_operation.Zk_rollup_publish_skeleton Zk_rollup_repr.t
(list (Zk_rollup_operation_repr.t × option Zk_rollup_ticket_repr.t)))
and "'manager_operation.Zk_rollup_update" :=
(manager_operation.Zk_rollup_update_skeleton Zk_rollup_repr.t
Zk_rollup_update_repr.t).
Module contents.
Include ConstructorRecords_contents_manager_operation.contents.
Definition Seed_nonce_revelation := 'contents.Seed_nonce_revelation.
Definition Vdf_revelation := 'contents.Vdf_revelation.
Definition Double_preendorsement_evidence :=
'contents.Double_preendorsement_evidence.
Definition Double_endorsement_evidence :=
'contents.Double_endorsement_evidence.
Definition Double_baking_evidence := 'contents.Double_baking_evidence.
Definition Activate_account := 'contents.Activate_account.
Definition Proposals := 'contents.Proposals.
Definition Ballot := 'contents.Ballot.
Definition Drain_delegate := 'contents.Drain_delegate.
Definition Manager_operation := 'contents.Manager_operation.
End contents.
Module manager_operation.
Include ConstructorRecords_contents_manager_operation.manager_operation.
Definition Transaction := 'manager_operation.Transaction.
Definition Origination := 'manager_operation.Origination.
Definition Register_global_constant :=
'manager_operation.Register_global_constant.
Definition Increase_paid_storage := 'manager_operation.Increase_paid_storage.
Definition Tx_rollup_submit_batch :=
'manager_operation.Tx_rollup_submit_batch.
Definition Tx_rollup_commit := 'manager_operation.Tx_rollup_commit.
Definition Tx_rollup_return_bond := 'manager_operation.Tx_rollup_return_bond.
Definition Tx_rollup_finalize_commitment :=
'manager_operation.Tx_rollup_finalize_commitment.
Definition Tx_rollup_remove_commitment :=
'manager_operation.Tx_rollup_remove_commitment.
Definition Tx_rollup_rejection := 'manager_operation.Tx_rollup_rejection.
Definition Tx_rollup_dispatch_tickets :=
'manager_operation.Tx_rollup_dispatch_tickets.
Definition Transfer_ticket := 'manager_operation.Transfer_ticket.
Definition Dal_publish_slot_header :=
'manager_operation.Dal_publish_slot_header.
Definition Sc_rollup_originate := 'manager_operation.Sc_rollup_originate.
Definition Sc_rollup_add_messages :=
'manager_operation.Sc_rollup_add_messages.
Definition Sc_rollup_cement := 'manager_operation.Sc_rollup_cement.
Definition Sc_rollup_publish := 'manager_operation.Sc_rollup_publish.
Definition Sc_rollup_refute := 'manager_operation.Sc_rollup_refute.
Definition Sc_rollup_timeout := 'manager_operation.Sc_rollup_timeout.
Definition Sc_rollup_execute_outbox_message :=
'manager_operation.Sc_rollup_execute_outbox_message.
Definition Sc_rollup_recover_bond :=
'manager_operation.Sc_rollup_recover_bond.
Definition Zk_rollup_origination := 'manager_operation.Zk_rollup_origination.
Definition Zk_rollup_publish := 'manager_operation.Zk_rollup_publish.
Definition Zk_rollup_update := 'manager_operation.Zk_rollup_update.
End manager_operation.
Definition operation := 'operation.
Definition protocol_data := 'protocol_data.
Definition manager_kind (function_parameter : manager_operation)
: Kind.manager :=
match function_parameter with
| Reveal _ ⇒ Kind.Reveal_manager_kind
| Transaction _ ⇒ Kind.Transaction_manager_kind
| Origination _ ⇒ Kind.Origination_manager_kind
| Delegation _ ⇒ Kind.Delegation_manager_kind
| Register_global_constant _ ⇒ Kind.Register_global_constant_manager_kind
| Set_deposits_limit _ ⇒ Kind.Set_deposits_limit_manager_kind
| Increase_paid_storage _ ⇒ Kind.Increase_paid_storage_manager_kind
| Update_consensus_key _ ⇒ Kind.Update_consensus_key_manager_kind
| Tx_rollup_origination ⇒ Kind.Tx_rollup_origination_manager_kind
| Tx_rollup_submit_batch _ ⇒ Kind.Tx_rollup_submit_batch_manager_kind
| Tx_rollup_commit _ ⇒ Kind.Tx_rollup_commit_manager_kind
| Tx_rollup_return_bond _ ⇒ Kind.Tx_rollup_return_bond_manager_kind
| Tx_rollup_finalize_commitment _ ⇒
Kind.Tx_rollup_finalize_commitment_manager_kind
| Tx_rollup_remove_commitment _ ⇒
Kind.Tx_rollup_remove_commitment_manager_kind
| Tx_rollup_rejection _ ⇒ Kind.Tx_rollup_rejection_manager_kind
| Tx_rollup_dispatch_tickets _ ⇒ Kind.Tx_rollup_dispatch_tickets_manager_kind
| Transfer_ticket _ ⇒ Kind.Transfer_ticket_manager_kind
| Dal_publish_slot_header _ ⇒ Kind.Dal_publish_slot_header_manager_kind
| Sc_rollup_originate _ ⇒ Kind.Sc_rollup_originate_manager_kind
| Sc_rollup_add_messages _ ⇒ Kind.Sc_rollup_add_messages_manager_kind
| Sc_rollup_cement _ ⇒ Kind.Sc_rollup_cement_manager_kind
| Sc_rollup_publish _ ⇒ Kind.Sc_rollup_publish_manager_kind
| Sc_rollup_refute _ ⇒ Kind.Sc_rollup_refute_manager_kind
| Sc_rollup_timeout _ ⇒ Kind.Sc_rollup_timeout_manager_kind
| Sc_rollup_execute_outbox_message _ ⇒
Kind.Sc_rollup_execute_outbox_message_manager_kind
| Sc_rollup_recover_bond _ ⇒ Kind.Sc_rollup_recover_bond_manager_kind
| Zk_rollup_origination _ ⇒ Kind.Zk_rollup_origination_manager_kind
| Zk_rollup_publish _ ⇒ Kind.Zk_rollup_publish_manager_kind
| Zk_rollup_update _ ⇒ Kind.Zk_rollup_update_manager_kind
end.
Inductive packed_manager_operation : Set :=
| Manager : manager_operation → packed_manager_operation.
Inductive packed_contents : Set :=
| Contents : contents → packed_contents.
Inductive packed_contents_list : Set :=
| Contents_list : contents_list → packed_contents_list.
Inductive packed_protocol_data : Set :=
| Operation_data : protocol_data → packed_protocol_data.
Module packed_operation.
Record record : Set := Build {
shell : Operation.shell_header;
protocol_data : packed_protocol_data;
}.
Definition with_shell shell (r : record) :=
Build shell r.(protocol_data).
Definition with_protocol_data protocol_data (r : record) :=
Build r.(shell) protocol_data.
End packed_operation.
Definition packed_operation := packed_operation.record.
Definition _pack (function_parameter : operation) : packed_operation :=
let '{|
operation.shell := shell; operation.protocol_data := protocol_data |} :=
function_parameter in
{| packed_operation.shell := shell;
packed_operation.protocol_data := Operation_data protocol_data; |}.
Fixpoint contents_list_to_list (function_parameter : contents_list)
: list packed_contents :=
match function_parameter with
| Single o_value ⇒ [ Contents o_value ]
| Cons o_value os ⇒ cons (Contents o_value) (contents_list_to_list os)
end.
Definition to_list (function_parameter : packed_contents_list)
: list packed_contents :=
let 'Contents_list l_value := function_parameter in
contents_list_to_list l_value.
Fixpoint of_list_internal (function_parameter : list packed_contents)
: Pervasives.result packed_contents_list string :=
match function_parameter with
| [] ⇒ Pervasives.Error "Operation lists should not be empty."
| cons (Contents o_value) [] ⇒ Pervasives.Ok (Contents_list (Single o_value))
| cons (Contents o_value) os ⇒
let? 'Contents_list os := of_list_internal os in
match (o_value, os) with
| (Manager_operation _, Single (Manager_operation _)) ⇒
Pervasives.Ok (Contents_list (Cons o_value os))
| (Manager_operation _, Cons _ _) ⇒
Pervasives.Ok (Contents_list (Cons o_value os))
| _ ⇒
Pervasives.Error
"Operation list of length > 1 should only contains manager operations."
end
end.
Definition of_list (l_value : list packed_contents) : M? packed_contents_list :=
match of_list_internal l_value with
| Pervasives.Ok contents ⇒ Pervasives.Ok contents
| Pervasives.Error s_value ⇒
Error_monad.error_value
(Build_extensible "Contents_list_error" string s_value)
end.
Definition tx_rollup_operation_tag_offset : int := 150.
Definition tx_rollup_operation_origination_tag : int :=
tx_rollup_operation_tag_offset +i 0.
Definition tx_rollup_operation_submit_batch_tag : int :=
tx_rollup_operation_tag_offset +i 1.
Definition tx_rollup_operation_commit_tag : int :=
tx_rollup_operation_tag_offset +i 2.
Definition tx_rollup_operation_return_bond_tag : int :=
tx_rollup_operation_tag_offset +i 3.
Definition tx_rollup_operation_finalize_commitment_tag : int :=
tx_rollup_operation_tag_offset +i 4.
Definition tx_rollup_operation_remove_commitment_tag : int :=
tx_rollup_operation_tag_offset +i 5.
Definition tx_rollup_operation_rejection_tag : int :=
tx_rollup_operation_tag_offset +i 6.
Definition tx_rollup_operation_dispatch_tickets_tag : int :=
tx_rollup_operation_tag_offset +i 7.
Definition transfer_ticket_tag : int := tx_rollup_operation_tag_offset +i 8.
Definition sc_rollup_operation_tag_offset : int := 200.
Definition sc_rollup_operation_origination_tag : int :=
sc_rollup_operation_tag_offset +i 0.
Definition sc_rollup_operation_add_message_tag : int :=
sc_rollup_operation_tag_offset +i 1.
Definition sc_rollup_operation_cement_tag : int :=
sc_rollup_operation_tag_offset +i 2.
Definition sc_rollup_operation_publish_tag : int :=
sc_rollup_operation_tag_offset +i 3.
Definition sc_rollup_operation_refute_tag : int :=
sc_rollup_operation_tag_offset +i 4.
Definition sc_rollup_operation_timeout_tag : int :=
sc_rollup_operation_tag_offset +i 5.
Definition sc_rollup_execute_outbox_message_tag : int :=
sc_rollup_operation_tag_offset +i 6.
Definition sc_rollup_operation_recover_bond_tag : int :=
sc_rollup_operation_tag_offset +i 7.
Definition dal_offset : int := 230.
Definition dal_publish_slot_header_tag : int := dal_offset +i 0.
Definition zk_rollup_operation_tag_offset : int := 250.
Definition zk_rollup_operation_create_tag : int :=
zk_rollup_operation_tag_offset +i 0.
Definition zk_rollup_operation_publish_tag : int :=
zk_rollup_operation_tag_offset +i 1.
Definition zk_rollup_operation_update_tag : int :=
zk_rollup_operation_tag_offset +i 2.
Module Encoding.
Definition case_value {A B : Set}
(tag : Data_encoding.case_tag) (name : string)
(args : Data_encoding.encoding A) (proj : B → option A) (inj : A → B)
: Data_encoding.case B :=
Data_encoding.case_value (String.capitalize_ascii name) None tag
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "kind" (Data_encoding.constant name)))
args)
(fun (x_value : B) ⇒
match proj x_value with
| None ⇒ None
| Some x_value ⇒ Some (tt, x_value)
end)
(fun (function_parameter : unit × A) ⇒
let '(_, x_value) := function_parameter in
inj x_value).
Module Manager_operations.
Module contents.
Module Seed_nonce_revelation.
Record record {level nonce : Set} : Set := Build {
level : level;
nonce : nonce;
}.
Arguments record : clear implicits.
Definition with_level {t_level t_nonce} level
(r : record t_level t_nonce) :=
Build t_level t_nonce level r.(nonce).
Definition with_nonce {t_level t_nonce} nonce
(r : record t_level t_nonce) :=
Build t_level t_nonce r.(level) nonce.
End Seed_nonce_revelation.
Definition Seed_nonce_revelation_skeleton := Seed_nonce_revelation.record.
Module Vdf_revelation.
Record record {solution : Set} : Set := Build {
solution : solution;
}.
Arguments record : clear implicits.
Definition with_solution {t_solution} solution (r : record t_solution) :=
Build t_solution solution.
End Vdf_revelation.
Definition Vdf_revelation_skeleton := Vdf_revelation.record.
Module Double_preendorsement_evidence.
Record record {op1 op2 : Set} : Set := Build {
op1 : op1;
op2 : op2;
}.
Arguments record : clear implicits.
Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 op1 r.(op2).
Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 r.(op1) op2.
End Double_preendorsement_evidence.
Definition Double_preendorsement_evidence_skeleton :=
Double_preendorsement_evidence.record.
Module Double_endorsement_evidence.
Record record {op1 op2 : Set} : Set := Build {
op1 : op1;
op2 : op2;
}.
Arguments record : clear implicits.
Definition with_op1 {t_op1 t_op2} op1 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 op1 r.(op2).
Definition with_op2 {t_op1 t_op2} op2 (r : record t_op1 t_op2) :=
Build t_op1 t_op2 r.(op1) op2.
End Double_endorsement_evidence.
Definition Double_endorsement_evidence_skeleton :=
Double_endorsement_evidence.record.
Module Double_baking_evidence.
Record record {bh1 bh2 : Set} : Set := Build {
bh1 : bh1;
bh2 : bh2;
}.
Arguments record : clear implicits.
Definition with_bh1 {t_bh1 t_bh2} bh1 (r : record t_bh1 t_bh2) :=
Build t_bh1 t_bh2 bh1 r.(bh2).
Definition with_bh2 {t_bh1 t_bh2} bh2 (r : record t_bh1 t_bh2) :=
Build t_bh1 t_bh2 r.(bh1) bh2.
End Double_baking_evidence.
Definition Double_baking_evidence_skeleton := Double_baking_evidence.record.
Module Activate_account.
Record record {id activation_code : Set} : Set := Build {
id : id;
activation_code : activation_code;
}.
Arguments record : clear implicits.
Definition with_id {t_id t_activation_code} id
(r : record t_id t_activation_code) :=
Build t_id t_activation_code id r.(activation_code).
Definition with_activation_code {t_id t_activation_code} activation_code
(r : record t_id t_activation_code) :=
Build t_id t_activation_code r.(id) activation_code.
End Activate_account.
Definition Activate_account_skeleton := Activate_account.record.
Module Proposals.
Record record {source period proposals : Set} : Set := Build {
source : source;
period : period;
proposals : proposals;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_period t_proposals} source
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals source r.(period) r.(proposals).
Definition with_period {t_source t_period t_proposals} period
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals r.(source) period r.(proposals).
Definition with_proposals {t_source t_period t_proposals} proposals
(r : record t_source t_period t_proposals) :=
Build t_source t_period t_proposals r.(source) r.(period) proposals.
End Proposals.
Definition Proposals_skeleton := Proposals.record.
Module Ballot.
Record record {source period proposal ballot : Set} : Set := Build {
source : source;
period : period;
proposal : proposal;
ballot : ballot;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_period t_proposal t_ballot} source
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot source r.(period)
r.(proposal) r.(ballot).
Definition with_period {t_source t_period t_proposal t_ballot} period
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) period
r.(proposal) r.(ballot).
Definition with_proposal {t_source t_period t_proposal t_ballot} proposal
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) r.(period)
proposal r.(ballot).
Definition with_ballot {t_source t_period t_proposal t_ballot} ballot
(r : record t_source t_period t_proposal t_ballot) :=
Build t_source t_period t_proposal t_ballot r.(source) r.(period)
r.(proposal) ballot.
End Ballot.
Definition Ballot_skeleton := Ballot.record.
Module Drain_delegate.
Record record {consensus_key delegate destination : Set} : Set := Build {
consensus_key : consensus_key;
delegate : delegate;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_consensus_key {t_consensus_key t_delegate t_destination}
consensus_key (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination consensus_key
r.(delegate) r.(destination).
Definition with_delegate {t_consensus_key t_delegate t_destination}
delegate (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination r.(consensus_key)
delegate r.(destination).
Definition with_destination {t_consensus_key t_delegate t_destination}
destination (r : record t_consensus_key t_delegate t_destination) :=
Build t_consensus_key t_delegate t_destination r.(consensus_key)
r.(delegate) destination.
End Drain_delegate.
Definition Drain_delegate_skeleton := Drain_delegate.record.
Module Manager_operation.
Record record {source fee counter operation gas_limit storage_limit : Set} :
Set := Build {
source : source;
fee : fee;
counter : counter;
operation : operation;
gas_limit : gas_limit;
storage_limit : storage_limit;
}.
Arguments record : clear implicits.
Definition with_source
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
source
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
source r.(fee) r.(counter) r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_fee
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit} fee
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) fee r.(counter) r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_counter
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
counter
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) counter r.(operation) r.(gas_limit)
r.(storage_limit).
Definition with_operation
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
operation
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) operation r.(gas_limit)
r.(storage_limit).
Definition with_gas_limit
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
gas_limit
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) r.(operation) gas_limit
r.(storage_limit).
Definition with_storage_limit
{t_source t_fee t_counter t_operation t_gas_limit t_storage_limit}
storage_limit
(r :
record t_source t_fee t_counter t_operation t_gas_limit
t_storage_limit) :=
Build t_source t_fee t_counter t_operation t_gas_limit t_storage_limit
r.(source) r.(fee) r.(counter) r.(operation) r.(gas_limit)
storage_limit.
End Manager_operation.
Definition Manager_operation_skeleton := Manager_operation.record.
End contents.
Module manager_operation.
Module Transaction.
Record record {amount parameters entrypoint destination : Set} : Set := Build {
amount : amount;
parameters : parameters;
entrypoint : entrypoint;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_amount {t_amount t_parameters t_entrypoint t_destination}
amount (r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination amount
r.(parameters) r.(entrypoint) r.(destination).
Definition with_parameters
{t_amount t_parameters t_entrypoint t_destination} parameters
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
parameters r.(entrypoint) r.(destination).
Definition with_entrypoint
{t_amount t_parameters t_entrypoint t_destination} entrypoint
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
r.(parameters) entrypoint r.(destination).
Definition with_destination
{t_amount t_parameters t_entrypoint t_destination} destination
(r : record t_amount t_parameters t_entrypoint t_destination) :=
Build t_amount t_parameters t_entrypoint t_destination r.(amount)
r.(parameters) r.(entrypoint) destination.
End Transaction.
Definition Transaction_skeleton := Transaction.record.
Module Origination.
Record record {delegate script credit : Set} : Set := Build {
delegate : delegate;
script : script;
credit : credit;
}.
Arguments record : clear implicits.
Definition with_delegate {t_delegate t_script t_credit} delegate
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit delegate r.(script) r.(credit).
Definition with_script {t_delegate t_script t_credit} script
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit r.(delegate) script r.(credit).
Definition with_credit {t_delegate t_script t_credit} credit
(r : record t_delegate t_script t_credit) :=
Build t_delegate t_script t_credit r.(delegate) r.(script) credit.
End Origination.
Definition Origination_skeleton := Origination.record.
Module Register_global_constant.
Record record {value : Set} : Set := Build {
value : value;
}.
Arguments record : clear implicits.
Definition with_value {t_value} value (r : record t_value) :=
Build t_value value.
End Register_global_constant.
Definition Register_global_constant_skeleton :=
Register_global_constant.record.
Module Increase_paid_storage.
Record record {amount_in_bytes destination : Set} : Set := Build {
amount_in_bytes : amount_in_bytes;
destination : destination;
}.
Arguments record : clear implicits.
Definition with_amount_in_bytes {t_amount_in_bytes t_destination}
amount_in_bytes (r : record t_amount_in_bytes t_destination) :=
Build t_amount_in_bytes t_destination amount_in_bytes r.(destination).
Definition with_destination {t_amount_in_bytes t_destination} destination
(r : record t_amount_in_bytes t_destination) :=
Build t_amount_in_bytes t_destination r.(amount_in_bytes) destination.
End Increase_paid_storage.
Definition Increase_paid_storage_skeleton := Increase_paid_storage.record.
Module Tx_rollup_submit_batch.
Record record {tx_rollup content burn_limit : Set} : Set := Build {
tx_rollup : tx_rollup;
content : content;
burn_limit : burn_limit;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup t_content t_burn_limit} tx_rollup
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit tx_rollup r.(content)
r.(burn_limit).
Definition with_content {t_tx_rollup t_content t_burn_limit} content
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) content
r.(burn_limit).
Definition with_burn_limit {t_tx_rollup t_content t_burn_limit} burn_limit
(r : record t_tx_rollup t_content t_burn_limit) :=
Build t_tx_rollup t_content t_burn_limit r.(tx_rollup) r.(content)
burn_limit.
End Tx_rollup_submit_batch.
Definition Tx_rollup_submit_batch_skeleton := Tx_rollup_submit_batch.record.
Module Tx_rollup_commit.
Record record {tx_rollup commitment : Set} : Set := Build {
tx_rollup : tx_rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup t_commitment} tx_rollup
(r : record t_tx_rollup t_commitment) :=
Build t_tx_rollup t_commitment tx_rollup r.(commitment).
Definition with_commitment {t_tx_rollup t_commitment} commitment
(r : record t_tx_rollup t_commitment) :=
Build t_tx_rollup t_commitment r.(tx_rollup) commitment.
End Tx_rollup_commit.
Definition Tx_rollup_commit_skeleton := Tx_rollup_commit.record.
Module Tx_rollup_return_bond.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_return_bond.
Definition Tx_rollup_return_bond_skeleton := Tx_rollup_return_bond.record.
Module Tx_rollup_finalize_commitment.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_finalize_commitment.
Definition Tx_rollup_finalize_commitment_skeleton :=
Tx_rollup_finalize_commitment.record.
Module Tx_rollup_remove_commitment.
Record record {tx_rollup : Set} : Set := Build {
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_tx_rollup {t_tx_rollup} tx_rollup
(r : record t_tx_rollup) :=
Build t_tx_rollup tx_rollup.
End Tx_rollup_remove_commitment.
Definition Tx_rollup_remove_commitment_skeleton :=
Tx_rollup_remove_commitment.record.
Module Tx_rollup_rejection.
Record record {tx_rollup level message message_position message_path
message_result_hash message_result_path previous_message_result
previous_message_result_path proof : Set} : Set := Build {
tx_rollup : tx_rollup;
level : level;
message : message;
message_position : message_position;
message_path : message_path;
message_result_hash : message_result_hash;
message_result_path : message_result_path;
previous_message_result : previous_message_result;
previous_message_result_path : previous_message_result_path;
proof : proof;
}.
Arguments record : clear implicits.
Definition with_tx_rollup
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} tx_rollup
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof tx_rollup r.(level) r.(message)
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_level
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} level
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) level r.(message)
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level) message
r.(message_position) r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_position
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_position
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) message_position r.(message_path) r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) message_path r.(message_result_hash)
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_result_hash
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_result_hash
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path) message_result_hash
r.(message_result_path) r.(previous_message_result)
r.(previous_message_result_path) r.(proof).
Definition with_message_result_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} message_result_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) message_result_path
r.(previous_message_result) r.(previous_message_result_path)
r.(proof).
Definition with_previous_message_result
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} previous_message_result
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
previous_message_result r.(previous_message_result_path) r.(proof).
Definition with_previous_message_result_path
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} previous_message_result_path
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
r.(previous_message_result) previous_message_result_path r.(proof).
Definition with_proof
{t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof} proof
(r :
record t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path
t_previous_message_result t_previous_message_result_path t_proof) :=
Build t_tx_rollup t_level t_message t_message_position t_message_path
t_message_result_hash t_message_result_path t_previous_message_result
t_previous_message_result_path t_proof r.(tx_rollup) r.(level)
r.(message) r.(message_position) r.(message_path)
r.(message_result_hash) r.(message_result_path)
r.(previous_message_result) r.(previous_message_result_path) proof.
End Tx_rollup_rejection.
Definition Tx_rollup_rejection_skeleton := Tx_rollup_rejection.record.
Module Tx_rollup_dispatch_tickets.
Record record {tx_rollup level context_hash message_index
message_result_path tickets_info : Set} : Set := Build {
tx_rollup : tx_rollup;
level : level;
context_hash : context_hash;
message_index : message_index;
message_result_path : message_result_path;
tickets_info : tickets_info;
}.
Arguments record : clear implicits.
Definition with_tx_rollup
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} tx_rollup
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info tx_rollup r.(level)
r.(context_hash) r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_level
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} level
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) level
r.(context_hash) r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_context_hash
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} context_hash
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
context_hash r.(message_index) r.(message_result_path)
r.(tickets_info).
Definition with_message_index
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} message_index
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) message_index r.(message_result_path)
r.(tickets_info).
Definition with_message_result_path
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} message_result_path
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) r.(message_index) message_result_path
r.(tickets_info).
Definition with_tickets_info
{t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info} tickets_info
(r :
record t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info) :=
Build t_tx_rollup t_level t_context_hash t_message_index
t_message_result_path t_tickets_info r.(tx_rollup) r.(level)
r.(context_hash) r.(message_index) r.(message_result_path)
tickets_info.
End Tx_rollup_dispatch_tickets.
Definition Tx_rollup_dispatch_tickets_skeleton :=
Tx_rollup_dispatch_tickets.record.
Module Transfer_ticket.
Record record {contents ty ticketer amount destination entrypoint : Set} :
Set := Build {
contents : contents;
ty : ty;
ticketer : ticketer;
amount : amount;
destination : destination;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_contents
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
contents
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
contents r.(ty) r.(ticketer) r.(amount) r.(destination)
r.(entrypoint).
Definition with_ty
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} ty
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) ty r.(ticketer) r.(amount) r.(destination)
r.(entrypoint).
Definition with_ticketer
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
ticketer
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) ticketer r.(amount) r.(destination)
r.(entrypoint).
Definition with_amount
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint} amount
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) amount r.(destination)
r.(entrypoint).
Definition with_destination
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
destination
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) r.(amount) destination
r.(entrypoint).
Definition with_entrypoint
{t_contents t_ty t_ticketer t_amount t_destination t_entrypoint}
entrypoint
(r :
record t_contents t_ty t_ticketer t_amount t_destination t_entrypoint) :=
Build t_contents t_ty t_ticketer t_amount t_destination t_entrypoint
r.(contents) r.(ty) r.(ticketer) r.(amount) r.(destination)
entrypoint.
End Transfer_ticket.
Definition Transfer_ticket_skeleton := Transfer_ticket.record.
Module Dal_publish_slot_header.
Record record {slot_header : Set} : Set := Build {
slot_header : slot_header;
}.
Arguments record : clear implicits.
Definition with_slot_header {t_slot_header} slot_header
(r : record t_slot_header) :=
Build t_slot_header slot_header.
End Dal_publish_slot_header.
Definition Dal_publish_slot_header_skeleton :=
Dal_publish_slot_header.record.
Module Sc_rollup_originate.
Record record {kind boot_sector origination_proof parameters_ty : Set} :
Set := Build {
kind : kind;
boot_sector : boot_sector;
origination_proof : origination_proof;
parameters_ty : parameters_ty;
}.
Arguments record : clear implicits.
Definition with_kind
{t_kind t_boot_sector t_origination_proof t_parameters_ty} kind
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty kind
r.(boot_sector) r.(origination_proof) r.(parameters_ty).
Definition with_boot_sector
{t_kind t_boot_sector t_origination_proof t_parameters_ty} boot_sector
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
boot_sector r.(origination_proof) r.(parameters_ty).
Definition with_origination_proof
{t_kind t_boot_sector t_origination_proof t_parameters_ty}
origination_proof
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
r.(boot_sector) origination_proof r.(parameters_ty).
Definition with_parameters_ty
{t_kind t_boot_sector t_origination_proof t_parameters_ty} parameters_ty
(r : record t_kind t_boot_sector t_origination_proof t_parameters_ty) :=
Build t_kind t_boot_sector t_origination_proof t_parameters_ty r.(kind)
r.(boot_sector) r.(origination_proof) parameters_ty.
End Sc_rollup_originate.
Definition Sc_rollup_originate_skeleton := Sc_rollup_originate.record.
Module Sc_rollup_add_messages.
Record record {messages : Set} : Set := Build {
messages : messages;
}.
Arguments record : clear implicits.
Definition with_messages {t_messages} messages (r : record t_messages) :=
Build t_messages messages.
End Sc_rollup_add_messages.
Definition Sc_rollup_add_messages_skeleton := Sc_rollup_add_messages.record.
Module Sc_rollup_cement.
Record record {rollup commitment : Set} : Set := Build {
rollup : rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_commitment} rollup
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment rollup r.(commitment).
Definition with_commitment {t_rollup t_commitment} commitment
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment r.(rollup) commitment.
End Sc_rollup_cement.
Definition Sc_rollup_cement_skeleton := Sc_rollup_cement.record.
Module Sc_rollup_publish.
Record record {rollup commitment : Set} : Set := Build {
rollup : rollup;
commitment : commitment;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_commitment} rollup
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment rollup r.(commitment).
Definition with_commitment {t_rollup t_commitment} commitment
(r : record t_rollup t_commitment) :=
Build t_rollup t_commitment r.(rollup) commitment.
End Sc_rollup_publish.
Definition Sc_rollup_publish_skeleton := Sc_rollup_publish.record.
Module Sc_rollup_refute.
Record record {rollup opponent refutation : Set} : Set := Build {
rollup : rollup;
opponent : opponent;
refutation : refutation;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_opponent t_refutation} rollup
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation rollup r.(opponent)
r.(refutation).
Definition with_opponent {t_rollup t_opponent t_refutation} opponent
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation r.(rollup) opponent
r.(refutation).
Definition with_refutation {t_rollup t_opponent t_refutation} refutation
(r : record t_rollup t_opponent t_refutation) :=
Build t_rollup t_opponent t_refutation r.(rollup) r.(opponent)
refutation.
End Sc_rollup_refute.
Definition Sc_rollup_refute_skeleton := Sc_rollup_refute.record.
Module Sc_rollup_timeout.
Record record {rollup stakers : Set} : Set := Build {
rollup : rollup;
stakers : stakers;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_stakers} rollup
(r : record t_rollup t_stakers) :=
Build t_rollup t_stakers rollup r.(stakers).
Definition with_stakers {t_rollup t_stakers} stakers
(r : record t_rollup t_stakers) :=
Build t_rollup t_stakers r.(rollup) stakers.
End Sc_rollup_timeout.
Definition Sc_rollup_timeout_skeleton := Sc_rollup_timeout.record.
Module Sc_rollup_execute_outbox_message.
Record record {rollup cemented_commitment output_proof : Set} : Set := Build {
rollup : rollup;
cemented_commitment : cemented_commitment;
output_proof : output_proof;
}.
Arguments record : clear implicits.
Definition with_rollup {t_rollup t_cemented_commitment t_output_proof}
rollup (r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof rollup
r.(cemented_commitment) r.(output_proof).
Definition with_cemented_commitment
{t_rollup t_cemented_commitment t_output_proof} cemented_commitment
(r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
cemented_commitment r.(output_proof).
Definition with_output_proof
{t_rollup t_cemented_commitment t_output_proof} output_proof
(r : record t_rollup t_cemented_commitment t_output_proof) :=
Build t_rollup t_cemented_commitment t_output_proof r.(rollup)
r.(cemented_commitment) output_proof.
End Sc_rollup_execute_outbox_message.
Definition Sc_rollup_execute_outbox_message_skeleton :=
Sc_rollup_execute_outbox_message.record.
Module Sc_rollup_recover_bond.
Record record {sc_rollup : Set} : Set := Build {
sc_rollup : sc_rollup;
}.
Arguments record : clear implicits.
Definition with_sc_rollup {t_sc_rollup} sc_rollup
(r : record t_sc_rollup) :=
Build t_sc_rollup sc_rollup.
End Sc_rollup_recover_bond.
Definition Sc_rollup_recover_bond_skeleton := Sc_rollup_recover_bond.record.
Module Zk_rollup_origination.
Record record {public_parameters circuits_info init_state nb_ops : Set} :
Set := Build {
public_parameters : public_parameters;
circuits_info : circuits_info;
init_state : init_state;
nb_ops : nb_ops;
}.
Arguments record : clear implicits.
Definition with_public_parameters
{t_public_parameters t_circuits_info t_init_state t_nb_ops}
public_parameters
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
public_parameters r.(circuits_info) r.(init_state) r.(nb_ops).
Definition with_circuits_info
{t_public_parameters t_circuits_info t_init_state t_nb_ops}
circuits_info
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) circuits_info r.(init_state) r.(nb_ops).
Definition with_init_state
{t_public_parameters t_circuits_info t_init_state t_nb_ops} init_state
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) r.(circuits_info) init_state r.(nb_ops).
Definition with_nb_ops
{t_public_parameters t_circuits_info t_init_state t_nb_ops} nb_ops
(r : record t_public_parameters t_circuits_info t_init_state t_nb_ops) :=
Build t_public_parameters t_circuits_info t_init_state t_nb_ops
r.(public_parameters) r.(circuits_info) r.(init_state) nb_ops.
End Zk_rollup_origination.
Definition Zk_rollup_origination_skeleton := Zk_rollup_origination.record.
Module Zk_rollup_publish.
Record record {zk_rollup ops : Set} : Set := Build {
zk_rollup : zk_rollup;
ops : ops;
}.
Arguments record : clear implicits.
Definition with_zk_rollup {t_zk_rollup t_ops} zk_rollup
(r : record t_zk_rollup t_ops) :=
Build t_zk_rollup t_ops zk_rollup r.(ops).
Definition with_ops {t_zk_rollup t_ops} ops
(r : record t_zk_rollup t_ops) :=
Build t_zk_rollup t_ops r.(zk_rollup) ops.
End Zk_rollup_publish.
Definition Zk_rollup_publish_skeleton := Zk_rollup_publish.record.
Module Zk_rollup_update.
Record record {zk_rollup update : Set} : Set := Build {
zk_rollup : zk_rollup;
update : update;
}.
Arguments record : clear implicits.
Definition with_zk_rollup {t_zk_rollup t_update} zk_rollup
(r : record t_zk_rollup t_update) :=
Build t_zk_rollup t_update zk_rollup r.(update).
Definition with_update {t_zk_rollup t_update} update
(r : record t_zk_rollup t_update) :=
Build t_zk_rollup t_update r.(zk_rollup) update.
End Zk_rollup_update.
Definition Zk_rollup_update_skeleton := Zk_rollup_update.record.
End manager_operation.
End ConstructorRecords_contents_manager_operation.
Import ConstructorRecords_contents_manager_operation.
Module protocol_data.
Record record {contents signature : Set} : Set := Build {
contents : contents;
signature : signature;
}.
Arguments record : clear implicits.
Definition with_contents {t_contents t_signature} contents
(r : record t_contents t_signature) :=
Build t_contents t_signature contents r.(signature).
Definition with_signature {t_contents t_signature} signature
(r : record t_contents t_signature) :=
Build t_contents t_signature r.(contents) signature.
End protocol_data.
Definition protocol_data_skeleton := protocol_data.record.
Module operation.
Record record {shell protocol_data : Set} : Set := Build {
shell : shell;
protocol_data : protocol_data;
}.
Arguments record : clear implicits.
Definition with_shell {t_shell t_protocol_data} shell
(r : record t_shell t_protocol_data) :=
Build t_shell t_protocol_data shell r.(protocol_data).
Definition with_protocol_data {t_shell t_protocol_data} protocol_data
(r : record t_shell t_protocol_data) :=
Build t_shell t_protocol_data r.(shell) protocol_data.
End operation.
Definition operation_skeleton := operation.record.
Reserved Notation "'contents.Seed_nonce_revelation".
Reserved Notation "'contents.Vdf_revelation".
Reserved Notation "'contents.Double_preendorsement_evidence".
Reserved Notation "'contents.Double_endorsement_evidence".
Reserved Notation "'contents.Double_baking_evidence".
Reserved Notation "'contents.Activate_account".
Reserved Notation "'contents.Proposals".
Reserved Notation "'contents.Ballot".
Reserved Notation "'contents.Drain_delegate".
Reserved Notation "'contents.Manager_operation".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'manager_operation.Register_global_constant".
Reserved Notation "'manager_operation.Increase_paid_storage".
Reserved Notation "'manager_operation.Tx_rollup_submit_batch".
Reserved Notation "'manager_operation.Tx_rollup_commit".
Reserved Notation "'manager_operation.Tx_rollup_return_bond".
Reserved Notation "'manager_operation.Tx_rollup_finalize_commitment".
Reserved Notation "'manager_operation.Tx_rollup_remove_commitment".
Reserved Notation "'manager_operation.Tx_rollup_rejection".
Reserved Notation "'manager_operation.Tx_rollup_dispatch_tickets".
Reserved Notation "'manager_operation.Transfer_ticket".
Reserved Notation "'manager_operation.Dal_publish_slot_header".
Reserved Notation "'manager_operation.Sc_rollup_originate".
Reserved Notation "'manager_operation.Sc_rollup_add_messages".
Reserved Notation "'manager_operation.Sc_rollup_cement".
Reserved Notation "'manager_operation.Sc_rollup_publish".
Reserved Notation "'manager_operation.Sc_rollup_refute".
Reserved Notation "'manager_operation.Sc_rollup_timeout".
Reserved Notation "'manager_operation.Sc_rollup_execute_outbox_message".
Reserved Notation "'manager_operation.Sc_rollup_recover_bond".
Reserved Notation "'manager_operation.Zk_rollup_origination".
Reserved Notation "'manager_operation.Zk_rollup_publish".
Reserved Notation "'manager_operation.Zk_rollup_update".
Reserved Notation "'operation".
Reserved Notation "'protocol_data".
Inductive contents_list : Set :=
| Single : contents → contents_list
| Cons : contents → contents_list → contents_list
with contents : Set :=
| Preendorsement : consensus_content → contents
| Endorsement : consensus_content → contents
| Dal_attestation : Dal_attestation_repr.operation → contents
| Seed_nonce_revelation : 'contents.Seed_nonce_revelation → contents
| Vdf_revelation : 'contents.Vdf_revelation → contents
| Double_preendorsement_evidence :
'contents.Double_preendorsement_evidence → contents
| Double_endorsement_evidence :
'contents.Double_endorsement_evidence → contents
| Double_baking_evidence : 'contents.Double_baking_evidence → contents
| Activate_account : 'contents.Activate_account → contents
| Proposals : 'contents.Proposals → contents
| Ballot : 'contents.Ballot → contents
| Drain_delegate : 'contents.Drain_delegate → contents
| Failing_noop : string → contents
| Manager_operation : 'contents.Manager_operation → contents
with manager_operation : Set :=
| Reveal : Signature.public_key → manager_operation
| Transaction : 'manager_operation.Transaction → manager_operation
| Origination : 'manager_operation.Origination → manager_operation
| Delegation : option Signature.public_key_hash → manager_operation
| Register_global_constant :
'manager_operation.Register_global_constant → manager_operation
| Set_deposits_limit : option Tez_repr.t → manager_operation
| Increase_paid_storage :
'manager_operation.Increase_paid_storage → manager_operation
| Update_consensus_key : Signature.public_key → manager_operation
| Tx_rollup_origination : manager_operation
| Tx_rollup_submit_batch :
'manager_operation.Tx_rollup_submit_batch → manager_operation
| Tx_rollup_commit : 'manager_operation.Tx_rollup_commit → manager_operation
| Tx_rollup_return_bond :
'manager_operation.Tx_rollup_return_bond → manager_operation
| Tx_rollup_finalize_commitment :
'manager_operation.Tx_rollup_finalize_commitment → manager_operation
| Tx_rollup_remove_commitment :
'manager_operation.Tx_rollup_remove_commitment → manager_operation
| Tx_rollup_rejection :
'manager_operation.Tx_rollup_rejection → manager_operation
| Tx_rollup_dispatch_tickets :
'manager_operation.Tx_rollup_dispatch_tickets → manager_operation
| Transfer_ticket : 'manager_operation.Transfer_ticket → manager_operation
| Dal_publish_slot_header :
'manager_operation.Dal_publish_slot_header → manager_operation
| Sc_rollup_originate :
'manager_operation.Sc_rollup_originate → manager_operation
| Sc_rollup_add_messages :
'manager_operation.Sc_rollup_add_messages → manager_operation
| Sc_rollup_cement : 'manager_operation.Sc_rollup_cement → manager_operation
| Sc_rollup_publish : 'manager_operation.Sc_rollup_publish → manager_operation
| Sc_rollup_refute : 'manager_operation.Sc_rollup_refute → manager_operation
| Sc_rollup_timeout : 'manager_operation.Sc_rollup_timeout → manager_operation
| Sc_rollup_execute_outbox_message :
'manager_operation.Sc_rollup_execute_outbox_message → manager_operation
| Sc_rollup_recover_bond :
'manager_operation.Sc_rollup_recover_bond → manager_operation
| Zk_rollup_origination :
'manager_operation.Zk_rollup_origination → manager_operation
| Zk_rollup_publish : 'manager_operation.Zk_rollup_publish → manager_operation
| Zk_rollup_update : 'manager_operation.Zk_rollup_update → manager_operation
where "'protocol_data" :=
(protocol_data_skeleton contents_list (option Signature.t))
and "'operation" := (operation_skeleton Operation.shell_header 'protocol_data)
and "'contents.Seed_nonce_revelation" :=
(contents.Seed_nonce_revelation_skeleton Raw_level_repr.t Seed_repr.nonce)
and "'contents.Vdf_revelation" :=
(contents.Vdf_revelation_skeleton Seed_repr.vdf_solution)
and "'contents.Double_preendorsement_evidence" :=
(contents.Double_preendorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_endorsement_evidence" :=
(contents.Double_endorsement_evidence_skeleton 'operation 'operation)
and "'contents.Double_baking_evidence" :=
(contents.Double_baking_evidence_skeleton Block_header_repr.t
Block_header_repr.t)
and "'contents.Activate_account" :=
(contents.Activate_account_skeleton
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)
Blinded_public_key_hash.activation_code)
and "'contents.Proposals" :=
(contents.Proposals_skeleton Signature.public_key_hash int32
(list Protocol_hash.t))
and "'contents.Ballot" :=
(contents.Ballot_skeleton Signature.public_key_hash int32 Protocol_hash.t
Vote_repr.ballot)
and "'contents.Drain_delegate" :=
(contents.Drain_delegate_skeleton Signature.public_key_hash
Signature.public_key_hash Signature.public_key_hash)
and "'contents.Manager_operation" :=
(contents.Manager_operation_skeleton Signature.public_key_hash Tez_repr.tez
Manager_counter_repr.t manager_operation Gas_limit_repr.Arith.integral Z.t)
and "'manager_operation.Transaction" :=
(manager_operation.Transaction_skeleton Tez_repr.tez Script_repr.lazy_expr
Entrypoint_repr.t Contract_repr.t)
and "'manager_operation.Origination" :=
(manager_operation.Origination_skeleton (option Signature.public_key_hash)
Script_repr.t Tez_repr.tez)
and "'manager_operation.Register_global_constant" :=
(manager_operation.Register_global_constant_skeleton Script_repr.lazy_expr)
and "'manager_operation.Increase_paid_storage" :=
(manager_operation.Increase_paid_storage_skeleton Z.t Contract_hash.t)
and "'manager_operation.Tx_rollup_submit_batch" :=
(manager_operation.Tx_rollup_submit_batch_skeleton Tx_rollup_repr.t string
(option Tez_repr.t))
and "'manager_operation.Tx_rollup_commit" :=
(manager_operation.Tx_rollup_commit_skeleton Tx_rollup_repr.t
Tx_rollup_commitment_repr.Full.t)
and "'manager_operation.Tx_rollup_return_bond" :=
(manager_operation.Tx_rollup_return_bond_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_finalize_commitment" :=
(manager_operation.Tx_rollup_finalize_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_remove_commitment" :=
(manager_operation.Tx_rollup_remove_commitment_skeleton Tx_rollup_repr.t)
and "'manager_operation.Tx_rollup_rejection" :=
(manager_operation.Tx_rollup_rejection_skeleton Tx_rollup_repr.t
Tx_rollup_level_repr.t Tx_rollup_message_repr.t int
Tx_rollup_inbox_repr.Merkle.path Tx_rollup_message_result_hash_repr.t
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
Tx_rollup_message_result_repr.t
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
Tx_rollup_l2_proof.serialized)
and "'manager_operation.Tx_rollup_dispatch_tickets" :=
(manager_operation.Tx_rollup_dispatch_tickets_skeleton Tx_rollup_repr.t
Tx_rollup_level_repr.t Context_hash.t int
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path)
(list Tx_rollup_reveal_repr.t))
and "'manager_operation.Transfer_ticket" :=
(manager_operation.Transfer_ticket_skeleton Script_repr.lazy_expr
Script_repr.lazy_expr Contract_repr.t Ticket_amount.t Contract_repr.t
Entrypoint_repr.t)
and "'manager_operation.Dal_publish_slot_header" :=
(manager_operation.Dal_publish_slot_header_skeleton Dal_slot_repr.Header.t)
and "'manager_operation.Sc_rollup_originate" :=
(manager_operation.Sc_rollup_originate_skeleton Sc_rollups.Kind.t string
string Script_repr.lazy_expr)
and "'manager_operation.Sc_rollup_add_messages" :=
(manager_operation.Sc_rollup_add_messages_skeleton (list string))
and "'manager_operation.Sc_rollup_cement" :=
(manager_operation.Sc_rollup_cement_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.Hash.t)
and "'manager_operation.Sc_rollup_publish" :=
(manager_operation.Sc_rollup_publish_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.t)
and "'manager_operation.Sc_rollup_refute" :=
(manager_operation.Sc_rollup_refute_skeleton Sc_rollup_repr.t
Signature.public_key_hash (option Sc_rollup_game_repr.refutation))
and "'manager_operation.Sc_rollup_timeout" :=
(manager_operation.Sc_rollup_timeout_skeleton Sc_rollup_repr.t
Sc_rollup_game_repr.Index.t)
and "'manager_operation.Sc_rollup_execute_outbox_message" :=
(manager_operation.Sc_rollup_execute_outbox_message_skeleton Sc_rollup_repr.t
Sc_rollup_commitment_repr.Hash.t string)
and "'manager_operation.Sc_rollup_recover_bond" :=
(manager_operation.Sc_rollup_recover_bond_skeleton Sc_rollup_repr.t)
and "'manager_operation.Zk_rollup_origination" :=
(manager_operation.Zk_rollup_origination_skeleton Plonk.public_parameters
(Zk_rollup_account_repr.SMap.(Map.S.t) Zk_rollup_account_repr.circuit_info)
Zk_rollup_state_repr.t int)
and "'manager_operation.Zk_rollup_publish" :=
(manager_operation.Zk_rollup_publish_skeleton Zk_rollup_repr.t
(list (Zk_rollup_operation_repr.t × option Zk_rollup_ticket_repr.t)))
and "'manager_operation.Zk_rollup_update" :=
(manager_operation.Zk_rollup_update_skeleton Zk_rollup_repr.t
Zk_rollup_update_repr.t).
Module contents.
Include ConstructorRecords_contents_manager_operation.contents.
Definition Seed_nonce_revelation := 'contents.Seed_nonce_revelation.
Definition Vdf_revelation := 'contents.Vdf_revelation.
Definition Double_preendorsement_evidence :=
'contents.Double_preendorsement_evidence.
Definition Double_endorsement_evidence :=
'contents.Double_endorsement_evidence.
Definition Double_baking_evidence := 'contents.Double_baking_evidence.
Definition Activate_account := 'contents.Activate_account.
Definition Proposals := 'contents.Proposals.
Definition Ballot := 'contents.Ballot.
Definition Drain_delegate := 'contents.Drain_delegate.
Definition Manager_operation := 'contents.Manager_operation.
End contents.
Module manager_operation.
Include ConstructorRecords_contents_manager_operation.manager_operation.
Definition Transaction := 'manager_operation.Transaction.
Definition Origination := 'manager_operation.Origination.
Definition Register_global_constant :=
'manager_operation.Register_global_constant.
Definition Increase_paid_storage := 'manager_operation.Increase_paid_storage.
Definition Tx_rollup_submit_batch :=
'manager_operation.Tx_rollup_submit_batch.
Definition Tx_rollup_commit := 'manager_operation.Tx_rollup_commit.
Definition Tx_rollup_return_bond := 'manager_operation.Tx_rollup_return_bond.
Definition Tx_rollup_finalize_commitment :=
'manager_operation.Tx_rollup_finalize_commitment.
Definition Tx_rollup_remove_commitment :=
'manager_operation.Tx_rollup_remove_commitment.
Definition Tx_rollup_rejection := 'manager_operation.Tx_rollup_rejection.
Definition Tx_rollup_dispatch_tickets :=
'manager_operation.Tx_rollup_dispatch_tickets.
Definition Transfer_ticket := 'manager_operation.Transfer_ticket.
Definition Dal_publish_slot_header :=
'manager_operation.Dal_publish_slot_header.
Definition Sc_rollup_originate := 'manager_operation.Sc_rollup_originate.
Definition Sc_rollup_add_messages :=
'manager_operation.Sc_rollup_add_messages.
Definition Sc_rollup_cement := 'manager_operation.Sc_rollup_cement.
Definition Sc_rollup_publish := 'manager_operation.Sc_rollup_publish.
Definition Sc_rollup_refute := 'manager_operation.Sc_rollup_refute.
Definition Sc_rollup_timeout := 'manager_operation.Sc_rollup_timeout.
Definition Sc_rollup_execute_outbox_message :=
'manager_operation.Sc_rollup_execute_outbox_message.
Definition Sc_rollup_recover_bond :=
'manager_operation.Sc_rollup_recover_bond.
Definition Zk_rollup_origination := 'manager_operation.Zk_rollup_origination.
Definition Zk_rollup_publish := 'manager_operation.Zk_rollup_publish.
Definition Zk_rollup_update := 'manager_operation.Zk_rollup_update.
End manager_operation.
Definition operation := 'operation.
Definition protocol_data := 'protocol_data.
Definition manager_kind (function_parameter : manager_operation)
: Kind.manager :=
match function_parameter with
| Reveal _ ⇒ Kind.Reveal_manager_kind
| Transaction _ ⇒ Kind.Transaction_manager_kind
| Origination _ ⇒ Kind.Origination_manager_kind
| Delegation _ ⇒ Kind.Delegation_manager_kind
| Register_global_constant _ ⇒ Kind.Register_global_constant_manager_kind
| Set_deposits_limit _ ⇒ Kind.Set_deposits_limit_manager_kind
| Increase_paid_storage _ ⇒ Kind.Increase_paid_storage_manager_kind
| Update_consensus_key _ ⇒ Kind.Update_consensus_key_manager_kind
| Tx_rollup_origination ⇒ Kind.Tx_rollup_origination_manager_kind
| Tx_rollup_submit_batch _ ⇒ Kind.Tx_rollup_submit_batch_manager_kind
| Tx_rollup_commit _ ⇒ Kind.Tx_rollup_commit_manager_kind
| Tx_rollup_return_bond _ ⇒ Kind.Tx_rollup_return_bond_manager_kind
| Tx_rollup_finalize_commitment _ ⇒
Kind.Tx_rollup_finalize_commitment_manager_kind
| Tx_rollup_remove_commitment _ ⇒
Kind.Tx_rollup_remove_commitment_manager_kind
| Tx_rollup_rejection _ ⇒ Kind.Tx_rollup_rejection_manager_kind
| Tx_rollup_dispatch_tickets _ ⇒ Kind.Tx_rollup_dispatch_tickets_manager_kind
| Transfer_ticket _ ⇒ Kind.Transfer_ticket_manager_kind
| Dal_publish_slot_header _ ⇒ Kind.Dal_publish_slot_header_manager_kind
| Sc_rollup_originate _ ⇒ Kind.Sc_rollup_originate_manager_kind
| Sc_rollup_add_messages _ ⇒ Kind.Sc_rollup_add_messages_manager_kind
| Sc_rollup_cement _ ⇒ Kind.Sc_rollup_cement_manager_kind
| Sc_rollup_publish _ ⇒ Kind.Sc_rollup_publish_manager_kind
| Sc_rollup_refute _ ⇒ Kind.Sc_rollup_refute_manager_kind
| Sc_rollup_timeout _ ⇒ Kind.Sc_rollup_timeout_manager_kind
| Sc_rollup_execute_outbox_message _ ⇒
Kind.Sc_rollup_execute_outbox_message_manager_kind
| Sc_rollup_recover_bond _ ⇒ Kind.Sc_rollup_recover_bond_manager_kind
| Zk_rollup_origination _ ⇒ Kind.Zk_rollup_origination_manager_kind
| Zk_rollup_publish _ ⇒ Kind.Zk_rollup_publish_manager_kind
| Zk_rollup_update _ ⇒ Kind.Zk_rollup_update_manager_kind
end.
Inductive packed_manager_operation : Set :=
| Manager : manager_operation → packed_manager_operation.
Inductive packed_contents : Set :=
| Contents : contents → packed_contents.
Inductive packed_contents_list : Set :=
| Contents_list : contents_list → packed_contents_list.
Inductive packed_protocol_data : Set :=
| Operation_data : protocol_data → packed_protocol_data.
Module packed_operation.
Record record : Set := Build {
shell : Operation.shell_header;
protocol_data : packed_protocol_data;
}.
Definition with_shell shell (r : record) :=
Build shell r.(protocol_data).
Definition with_protocol_data protocol_data (r : record) :=
Build r.(shell) protocol_data.
End packed_operation.
Definition packed_operation := packed_operation.record.
Definition _pack (function_parameter : operation) : packed_operation :=
let '{|
operation.shell := shell; operation.protocol_data := protocol_data |} :=
function_parameter in
{| packed_operation.shell := shell;
packed_operation.protocol_data := Operation_data protocol_data; |}.
Fixpoint contents_list_to_list (function_parameter : contents_list)
: list packed_contents :=
match function_parameter with
| Single o_value ⇒ [ Contents o_value ]
| Cons o_value os ⇒ cons (Contents o_value) (contents_list_to_list os)
end.
Definition to_list (function_parameter : packed_contents_list)
: list packed_contents :=
let 'Contents_list l_value := function_parameter in
contents_list_to_list l_value.
Fixpoint of_list_internal (function_parameter : list packed_contents)
: Pervasives.result packed_contents_list string :=
match function_parameter with
| [] ⇒ Pervasives.Error "Operation lists should not be empty."
| cons (Contents o_value) [] ⇒ Pervasives.Ok (Contents_list (Single o_value))
| cons (Contents o_value) os ⇒
let? 'Contents_list os := of_list_internal os in
match (o_value, os) with
| (Manager_operation _, Single (Manager_operation _)) ⇒
Pervasives.Ok (Contents_list (Cons o_value os))
| (Manager_operation _, Cons _ _) ⇒
Pervasives.Ok (Contents_list (Cons o_value os))
| _ ⇒
Pervasives.Error
"Operation list of length > 1 should only contains manager operations."
end
end.
Definition of_list (l_value : list packed_contents) : M? packed_contents_list :=
match of_list_internal l_value with
| Pervasives.Ok contents ⇒ Pervasives.Ok contents
| Pervasives.Error s_value ⇒
Error_monad.error_value
(Build_extensible "Contents_list_error" string s_value)
end.
Definition tx_rollup_operation_tag_offset : int := 150.
Definition tx_rollup_operation_origination_tag : int :=
tx_rollup_operation_tag_offset +i 0.
Definition tx_rollup_operation_submit_batch_tag : int :=
tx_rollup_operation_tag_offset +i 1.
Definition tx_rollup_operation_commit_tag : int :=
tx_rollup_operation_tag_offset +i 2.
Definition tx_rollup_operation_return_bond_tag : int :=
tx_rollup_operation_tag_offset +i 3.
Definition tx_rollup_operation_finalize_commitment_tag : int :=
tx_rollup_operation_tag_offset +i 4.
Definition tx_rollup_operation_remove_commitment_tag : int :=
tx_rollup_operation_tag_offset +i 5.
Definition tx_rollup_operation_rejection_tag : int :=
tx_rollup_operation_tag_offset +i 6.
Definition tx_rollup_operation_dispatch_tickets_tag : int :=
tx_rollup_operation_tag_offset +i 7.
Definition transfer_ticket_tag : int := tx_rollup_operation_tag_offset +i 8.
Definition sc_rollup_operation_tag_offset : int := 200.
Definition sc_rollup_operation_origination_tag : int :=
sc_rollup_operation_tag_offset +i 0.
Definition sc_rollup_operation_add_message_tag : int :=
sc_rollup_operation_tag_offset +i 1.
Definition sc_rollup_operation_cement_tag : int :=
sc_rollup_operation_tag_offset +i 2.
Definition sc_rollup_operation_publish_tag : int :=
sc_rollup_operation_tag_offset +i 3.
Definition sc_rollup_operation_refute_tag : int :=
sc_rollup_operation_tag_offset +i 4.
Definition sc_rollup_operation_timeout_tag : int :=
sc_rollup_operation_tag_offset +i 5.
Definition sc_rollup_execute_outbox_message_tag : int :=
sc_rollup_operation_tag_offset +i 6.
Definition sc_rollup_operation_recover_bond_tag : int :=
sc_rollup_operation_tag_offset +i 7.
Definition dal_offset : int := 230.
Definition dal_publish_slot_header_tag : int := dal_offset +i 0.
Definition zk_rollup_operation_tag_offset : int := 250.
Definition zk_rollup_operation_create_tag : int :=
zk_rollup_operation_tag_offset +i 0.
Definition zk_rollup_operation_publish_tag : int :=
zk_rollup_operation_tag_offset +i 1.
Definition zk_rollup_operation_update_tag : int :=
zk_rollup_operation_tag_offset +i 2.
Module Encoding.
Definition case_value {A B : Set}
(tag : Data_encoding.case_tag) (name : string)
(args : Data_encoding.encoding A) (proj : B → option A) (inj : A → B)
: Data_encoding.case B :=
Data_encoding.case_value (String.capitalize_ascii name) None tag
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "kind" (Data_encoding.constant name)))
args)
(fun (x_value : B) ⇒
match proj x_value with
| None ⇒ None
| Some x_value ⇒ Some (tt, x_value)
end)
(fun (function_parameter : unit × A) ⇒
let '(_, x_value) := function_parameter in
inj x_value).
Module Manager_operations.
Records for the constructor parameters
Module ConstructorRecords_case.
Module case.
Module MCase.
Record record {tag name encoding select proj inj : Set} : Set := Build {
tag : tag;
name : name;
encoding : encoding;
select : select;
proj : proj;
inj : inj;
}.
Arguments record : clear implicits.
Definition with_tag {t_tag t_name t_encoding t_select t_proj t_inj}
tag (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj tag r.(name)
r.(encoding) r.(select) r.(proj) r.(inj).
Definition with_name {t_tag t_name t_encoding t_select t_proj t_inj}
name (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) name
r.(encoding) r.(select) r.(proj) r.(inj).
Definition with_encoding
{t_tag t_name t_encoding t_select t_proj t_inj} encoding
(r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
encoding r.(select) r.(proj) r.(inj).
Definition with_select {t_tag t_name t_encoding t_select t_proj t_inj}
select (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) select r.(proj) r.(inj).
Definition with_proj {t_tag t_name t_encoding t_select t_proj t_inj}
proj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) r.(select) proj r.(inj).
Definition with_inj {t_tag t_name t_encoding t_select t_proj t_inj}
inj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) r.(select) r.(proj) inj.
End MCase.
Definition MCase_skeleton := MCase.record.
End case.
End ConstructorRecords_case.
Import ConstructorRecords_case.
Reserved Notation "'case.MCase".
Inductive case : Set :=
| MCase : ∀ {a : Set}, 'case.MCase a → case
where "'case.MCase" :=
(fun (t_a : Set) ⇒ case.MCase_skeleton int string (Data_encoding.t t_a)
(packed_manager_operation → option manager_operation)
(manager_operation → t_a) (t_a → manager_operation)).
Module case.
Include ConstructorRecords_case.case.
Definition MCase := 'case.MCase.
End case.
Definition reveal_case : case :=
MCase
{| case.MCase.tag := 0; case.MCase.name := "reveal";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "public_key"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Reveal _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Reveal pkh ⇒ pkh
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj := fun (pkh : Signature.public_key) ⇒ Reveal pkh; |}.
Definition transaction_case : case :=
MCase
{| case.MCase.tag := 1; case.MCase.name := "transaction";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "amount" Tez_repr.encoding)
(Data_encoding.req None None "destination" Contract_repr.encoding)
(Data_encoding.opt None None "parameters"
(Data_encoding.obj2
(Data_encoding.req None None "entrypoint"
Entrypoint_repr.smart_encoding)
(Data_encoding.req None None "value"
Script_repr.lazy_expr_encoding)));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Transaction _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Transaction {|
manager_operation.Transaction.amount := amount;
manager_operation.Transaction.parameters := parameters;
manager_operation.Transaction.entrypoint := entrypoint;
manager_operation.Transaction.destination := destination
|} ⇒
let parameters :=
if
(Script_repr.is_unit_parameter parameters) &&
(Entrypoint_repr.is_default entrypoint)
then
None
else
Some (entrypoint, parameters) in
(amount, destination, parameters)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tez_repr.t × Contract_repr.t ×
option (Entrypoint_repr.t × Script_repr.lazy_expr)) ⇒
let '(amount, destination, parameters) := function_parameter in
let '(entrypoint, parameters) :=
match parameters with
| None ⇒ (Entrypoint_repr.default, Script_repr.unit_parameter)
| Some (entrypoint, value_value) ⇒ (entrypoint, value_value)
end in
Transaction
{| manager_operation.Transaction.amount := amount;
manager_operation.Transaction.parameters := parameters;
manager_operation.Transaction.entrypoint := entrypoint;
manager_operation.Transaction.destination := destination; |};
|}.
Definition origination_case : case :=
MCase
{| case.MCase.tag := 2; case.MCase.name := "origination";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "balance" Tez_repr.encoding)
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "script" Script_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Origination _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Origination {|
manager_operation.Origination.delegate := delegate;
manager_operation.Origination.script := script;
manager_operation.Origination.credit := credit
|} ⇒ (credit, delegate, script)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tez_repr.t × option Signature.public_key_hash × Script_repr.t) ⇒
let '(credit, delegate, script) := function_parameter in
Origination
{| manager_operation.Origination.delegate := delegate;
manager_operation.Origination.script := script;
manager_operation.Origination.credit := credit; |}; |}.
Definition delegation_case : case :=
MCase
{| case.MCase.tag := 3; case.MCase.name := "delegation";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Delegation _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Delegation key_value ⇒ key_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (key_value : option Signature.public_key_hash) ⇒
Delegation key_value; |}.
Definition register_global_constant_case : case :=
MCase
{| case.MCase.tag := 4; case.MCase.name := "register_global_constant";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "value"
Script_repr.lazy_expr_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Register_global_constant _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Register_global_constant {|
manager_operation.Register_global_constant.value := value_value
|} ⇒ value_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (value_value : Script_repr.lazy_expr) ⇒
Register_global_constant
{|
manager_operation.Register_global_constant.value :=
value_value; |}; |}.
Definition set_deposits_limit_case : case :=
MCase
{| case.MCase.tag := 5; case.MCase.name := "set_deposits_limit";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.opt None None "limit" Tez_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Set_deposits_limit _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Set_deposits_limit key_value ⇒ key_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (key_value : option Tez_repr.t) ⇒ Set_deposits_limit key_value;
|}.
Definition increase_paid_storage_case : case :=
MCase
{| case.MCase.tag := 9; case.MCase.name := "increase_paid_storage";
case.MCase.encoding :=
Data_encoding.obj2
(Data_encoding.req None None "amount" Data_encoding.z_value)
(Data_encoding.req None None "destination"
Contract_repr.originated_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Increase_paid_storage _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Increase_paid_storage {|
manager_operation.Increase_paid_storage.amount_in_bytes := amount_in_bytes;
manager_operation.Increase_paid_storage.destination :=
destination
|} ⇒ (amount_in_bytes, destination)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter : Z.t × Contract_hash.t) ⇒
let '(amount_in_bytes, destination) := function_parameter in
Increase_paid_storage
{|
manager_operation.Increase_paid_storage.amount_in_bytes :=
amount_in_bytes;
manager_operation.Increase_paid_storage.destination :=
destination; |}; |}.
Definition update_consensus_key_tag : int := 6.
Definition update_consensus_key_case : case :=
MCase
{| case.MCase.tag := update_consensus_key_tag;
case.MCase.name := "update_consensus_key";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "pk"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Update_consensus_key _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Update_consensus_key consensus_pk ⇒ consensus_pk
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (consensus_pk : Signature.public_key) ⇒
Update_consensus_key consensus_pk; |}.
Definition tx_rollup_origination_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_origination_tag;
case.MCase.name := "tx_rollup_origination";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "tx_rollup_origination"
Data_encoding.unit_value);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager (Tx_rollup_origination as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Tx_rollup_origination ⇒ tt
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Tx_rollup_origination; |}.
Definition tx_rollup_submit_batch_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_submit_batch_tag;
case.MCase.name := "tx_rollup_submit_batch";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "content"
(Data_encoding.string' None Data_encoding.Hex))
(Data_encoding.opt None None "burn_limit" Tez_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_submit_batch _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_submit_batch {|
manager_operation.Tx_rollup_submit_batch.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_submit_batch.content := content;
manager_operation.Tx_rollup_submit_batch.burn_limit :=
burn_limit
|} ⇒ (tx_rollup, content, burn_limit)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tx_rollup_repr.t × string × option Tez_repr.t) ⇒
let '(tx_rollup, content, burn_limit) := function_parameter in
Tx_rollup_submit_batch
{|
manager_operation.Tx_rollup_submit_batch.tx_rollup :=
tx_rollup;
manager_operation.Tx_rollup_submit_batch.content := content;
manager_operation.Tx_rollup_submit_batch.burn_limit :=
burn_limit; |}; |}.
Definition tx_rollup_commit_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_commit_tag;
case.MCase.name := "tx_rollup_commit";
case.MCase.encoding :=
Data_encoding.obj2
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "commitment"
Tx_rollup_commitment_repr.Full.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_commit _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_commit {|
manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_commit.commitment := commitment
|} ⇒ (tx_rollup, commitment)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tx_rollup_repr.t × Tx_rollup_commitment_repr.Full.t) ⇒
let '(tx_rollup, commitment) := function_parameter in
Tx_rollup_commit
{| manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_commit.commitment := commitment;
|}; |}.
Definition tx_rollup_return_bond_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_return_bond_tag;
case.MCase.name := "tx_rollup_return_bond";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_return_bond _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_return_bond {|
manager_operation.Tx_rollup_return_bond.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_return_bond
{|
manager_operation.Tx_rollup_return_bond.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_finalize_commitment_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_finalize_commitment_tag;
case.MCase.name := "tx_rollup_finalize_commitment";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_finalize_commitment _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_finalize_commitment {|
manager_operation.Tx_rollup_finalize_commitment.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_finalize_commitment
{|
manager_operation.Tx_rollup_finalize_commitment.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_remove_commitment_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_remove_commitment_tag;
case.MCase.name := "tx_rollup_remove_commitment";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_remove_commitment _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_remove_commitment {|
manager_operation.Tx_rollup_remove_commitment.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_remove_commitment
{|
manager_operation.Tx_rollup_remove_commitment.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_rejection_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_rejection_tag;
case.MCase.name := "tx_rollup_rejection";
case.MCase.encoding :=
Data_encoding.obj10
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "message"
Tx_rollup_message_repr.encoding)
(Data_encoding.req None None "message_position"
Data_encoding.n_value)
(Data_encoding.req None None "message_path"
Tx_rollup_inbox_repr.Merkle.path_encoding)
(Data_encoding.req None None "message_result_hash"
Tx_rollup_message_result_hash_repr.encoding)
(Data_encoding.req None None "message_result_path"
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
(Data_encoding.req None None "previous_message_result"
Tx_rollup_message_result_repr.encoding)
(Data_encoding.req None None "previous_message_result_path"
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
(Data_encoding.req None None "proof"
Tx_rollup_l2_proof.serialized_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_rejection _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_rejection {|
manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_rejection.level := level;
manager_operation.Tx_rollup_rejection.message := message;
manager_operation.Tx_rollup_rejection.message_position :=
message_position;
manager_operation.Tx_rollup_rejection.message_path :=
message_path;
manager_operation.Tx_rollup_rejection.message_result_hash :=
message_result_hash;
manager_operation.Tx_rollup_rejection.message_result_path :=
&nb
Module case.
Module MCase.
Record record {tag name encoding select proj inj : Set} : Set := Build {
tag : tag;
name : name;
encoding : encoding;
select : select;
proj : proj;
inj : inj;
}.
Arguments record : clear implicits.
Definition with_tag {t_tag t_name t_encoding t_select t_proj t_inj}
tag (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj tag r.(name)
r.(encoding) r.(select) r.(proj) r.(inj).
Definition with_name {t_tag t_name t_encoding t_select t_proj t_inj}
name (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) name
r.(encoding) r.(select) r.(proj) r.(inj).
Definition with_encoding
{t_tag t_name t_encoding t_select t_proj t_inj} encoding
(r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
encoding r.(select) r.(proj) r.(inj).
Definition with_select {t_tag t_name t_encoding t_select t_proj t_inj}
select (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) select r.(proj) r.(inj).
Definition with_proj {t_tag t_name t_encoding t_select t_proj t_inj}
proj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) r.(select) proj r.(inj).
Definition with_inj {t_tag t_name t_encoding t_select t_proj t_inj}
inj (r : record t_tag t_name t_encoding t_select t_proj t_inj) :=
Build t_tag t_name t_encoding t_select t_proj t_inj r.(tag) r.(name)
r.(encoding) r.(select) r.(proj) inj.
End MCase.
Definition MCase_skeleton := MCase.record.
End case.
End ConstructorRecords_case.
Import ConstructorRecords_case.
Reserved Notation "'case.MCase".
Inductive case : Set :=
| MCase : ∀ {a : Set}, 'case.MCase a → case
where "'case.MCase" :=
(fun (t_a : Set) ⇒ case.MCase_skeleton int string (Data_encoding.t t_a)
(packed_manager_operation → option manager_operation)
(manager_operation → t_a) (t_a → manager_operation)).
Module case.
Include ConstructorRecords_case.case.
Definition MCase := 'case.MCase.
End case.
Definition reveal_case : case :=
MCase
{| case.MCase.tag := 0; case.MCase.name := "reveal";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "public_key"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Reveal _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Reveal pkh ⇒ pkh
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj := fun (pkh : Signature.public_key) ⇒ Reveal pkh; |}.
Definition transaction_case : case :=
MCase
{| case.MCase.tag := 1; case.MCase.name := "transaction";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "amount" Tez_repr.encoding)
(Data_encoding.req None None "destination" Contract_repr.encoding)
(Data_encoding.opt None None "parameters"
(Data_encoding.obj2
(Data_encoding.req None None "entrypoint"
Entrypoint_repr.smart_encoding)
(Data_encoding.req None None "value"
Script_repr.lazy_expr_encoding)));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Transaction _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Transaction {|
manager_operation.Transaction.amount := amount;
manager_operation.Transaction.parameters := parameters;
manager_operation.Transaction.entrypoint := entrypoint;
manager_operation.Transaction.destination := destination
|} ⇒
let parameters :=
if
(Script_repr.is_unit_parameter parameters) &&
(Entrypoint_repr.is_default entrypoint)
then
None
else
Some (entrypoint, parameters) in
(amount, destination, parameters)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tez_repr.t × Contract_repr.t ×
option (Entrypoint_repr.t × Script_repr.lazy_expr)) ⇒
let '(amount, destination, parameters) := function_parameter in
let '(entrypoint, parameters) :=
match parameters with
| None ⇒ (Entrypoint_repr.default, Script_repr.unit_parameter)
| Some (entrypoint, value_value) ⇒ (entrypoint, value_value)
end in
Transaction
{| manager_operation.Transaction.amount := amount;
manager_operation.Transaction.parameters := parameters;
manager_operation.Transaction.entrypoint := entrypoint;
manager_operation.Transaction.destination := destination; |};
|}.
Definition origination_case : case :=
MCase
{| case.MCase.tag := 2; case.MCase.name := "origination";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "balance" Tez_repr.encoding)
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "script" Script_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Origination _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Origination {|
manager_operation.Origination.delegate := delegate;
manager_operation.Origination.script := script;
manager_operation.Origination.credit := credit
|} ⇒ (credit, delegate, script)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tez_repr.t × option Signature.public_key_hash × Script_repr.t) ⇒
let '(credit, delegate, script) := function_parameter in
Origination
{| manager_operation.Origination.delegate := delegate;
manager_operation.Origination.script := script;
manager_operation.Origination.credit := credit; |}; |}.
Definition delegation_case : case :=
MCase
{| case.MCase.tag := 3; case.MCase.name := "delegation";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.opt None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Delegation _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Delegation key_value ⇒ key_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (key_value : option Signature.public_key_hash) ⇒
Delegation key_value; |}.
Definition register_global_constant_case : case :=
MCase
{| case.MCase.tag := 4; case.MCase.name := "register_global_constant";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "value"
Script_repr.lazy_expr_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Register_global_constant _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Register_global_constant {|
manager_operation.Register_global_constant.value := value_value
|} ⇒ value_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (value_value : Script_repr.lazy_expr) ⇒
Register_global_constant
{|
manager_operation.Register_global_constant.value :=
value_value; |}; |}.
Definition set_deposits_limit_case : case :=
MCase
{| case.MCase.tag := 5; case.MCase.name := "set_deposits_limit";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.opt None None "limit" Tez_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Set_deposits_limit _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Set_deposits_limit key_value ⇒ key_value
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (key_value : option Tez_repr.t) ⇒ Set_deposits_limit key_value;
|}.
Definition increase_paid_storage_case : case :=
MCase
{| case.MCase.tag := 9; case.MCase.name := "increase_paid_storage";
case.MCase.encoding :=
Data_encoding.obj2
(Data_encoding.req None None "amount" Data_encoding.z_value)
(Data_encoding.req None None "destination"
Contract_repr.originated_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Increase_paid_storage _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Increase_paid_storage {|
manager_operation.Increase_paid_storage.amount_in_bytes := amount_in_bytes;
manager_operation.Increase_paid_storage.destination :=
destination
|} ⇒ (amount_in_bytes, destination)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter : Z.t × Contract_hash.t) ⇒
let '(amount_in_bytes, destination) := function_parameter in
Increase_paid_storage
{|
manager_operation.Increase_paid_storage.amount_in_bytes :=
amount_in_bytes;
manager_operation.Increase_paid_storage.destination :=
destination; |}; |}.
Definition update_consensus_key_tag : int := 6.
Definition update_consensus_key_case : case :=
MCase
{| case.MCase.tag := update_consensus_key_tag;
case.MCase.name := "update_consensus_key";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "pk"
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding));
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Update_consensus_key _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Update_consensus_key consensus_pk ⇒ consensus_pk
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (consensus_pk : Signature.public_key) ⇒
Update_consensus_key consensus_pk; |}.
Definition tx_rollup_origination_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_origination_tag;
case.MCase.name := "tx_rollup_origination";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "tx_rollup_origination"
Data_encoding.unit_value);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager (Tx_rollup_origination as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
| Tx_rollup_origination ⇒ tt
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Tx_rollup_origination; |}.
Definition tx_rollup_submit_batch_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_submit_batch_tag;
case.MCase.name := "tx_rollup_submit_batch";
case.MCase.encoding :=
Data_encoding.obj3
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "content"
(Data_encoding.string' None Data_encoding.Hex))
(Data_encoding.opt None None "burn_limit" Tez_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_submit_batch _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_submit_batch {|
manager_operation.Tx_rollup_submit_batch.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_submit_batch.content := content;
manager_operation.Tx_rollup_submit_batch.burn_limit :=
burn_limit
|} ⇒ (tx_rollup, content, burn_limit)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tx_rollup_repr.t × string × option Tez_repr.t) ⇒
let '(tx_rollup, content, burn_limit) := function_parameter in
Tx_rollup_submit_batch
{|
manager_operation.Tx_rollup_submit_batch.tx_rollup :=
tx_rollup;
manager_operation.Tx_rollup_submit_batch.content := content;
manager_operation.Tx_rollup_submit_batch.burn_limit :=
burn_limit; |}; |}.
Definition tx_rollup_commit_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_commit_tag;
case.MCase.name := "tx_rollup_commit";
case.MCase.encoding :=
Data_encoding.obj2
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "commitment"
Tx_rollup_commitment_repr.Full.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_commit _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_commit {|
manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_commit.commitment := commitment
|} ⇒ (tx_rollup, commitment)
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (function_parameter :
Tx_rollup_repr.t × Tx_rollup_commitment_repr.Full.t) ⇒
let '(tx_rollup, commitment) := function_parameter in
Tx_rollup_commit
{| manager_operation.Tx_rollup_commit.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_commit.commitment := commitment;
|}; |}.
Definition tx_rollup_return_bond_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_return_bond_tag;
case.MCase.name := "tx_rollup_return_bond";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_return_bond _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_return_bond {|
manager_operation.Tx_rollup_return_bond.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_return_bond
{|
manager_operation.Tx_rollup_return_bond.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_finalize_commitment_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_finalize_commitment_tag;
case.MCase.name := "tx_rollup_finalize_commitment";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_finalize_commitment _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_finalize_commitment {|
manager_operation.Tx_rollup_finalize_commitment.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_finalize_commitment
{|
manager_operation.Tx_rollup_finalize_commitment.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_remove_commitment_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_remove_commitment_tag;
case.MCase.name := "tx_rollup_remove_commitment";
case.MCase.encoding :=
Data_encoding.obj1
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_remove_commitment _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_remove_commitment {|
manager_operation.Tx_rollup_remove_commitment.tx_rollup := tx_rollup
|} ⇒ tx_rollup
| _ ⇒ unreachable_gadt_branch
end;
case.MCase.inj :=
fun (tx_rollup : Tx_rollup_repr.t) ⇒
Tx_rollup_remove_commitment
{|
manager_operation.Tx_rollup_remove_commitment.tx_rollup :=
tx_rollup; |}; |}.
Definition tx_rollup_rejection_case : case :=
MCase
{| case.MCase.tag := tx_rollup_operation_rejection_tag;
case.MCase.name := "tx_rollup_rejection";
case.MCase.encoding :=
Data_encoding.obj10
(Data_encoding.req None None "rollup" Tx_rollup_repr.encoding)
(Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
(Data_encoding.req None None "message"
Tx_rollup_message_repr.encoding)
(Data_encoding.req None None "message_position"
Data_encoding.n_value)
(Data_encoding.req None None "message_path"
Tx_rollup_inbox_repr.Merkle.path_encoding)
(Data_encoding.req None None "message_result_hash"
Tx_rollup_message_result_hash_repr.encoding)
(Data_encoding.req None None "message_result_path"
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
(Data_encoding.req None None "previous_message_result"
Tx_rollup_message_result_repr.encoding)
(Data_encoding.req None None "previous_message_result_path"
Tx_rollup_commitment_repr.Merkle.(Merkle_list.T.path_encoding))
(Data_encoding.req None None "proof"
Tx_rollup_l2_proof.serialized_encoding);
case.MCase.select :=
fun (function_parameter : packed_manager_operation) ⇒
match function_parameter with
| Manager ((Tx_rollup_rejection _) as op) ⇒ Some op
| _ ⇒ None
end;
case.MCase.proj :=
fun (function_parameter : manager_operation) ⇒
match function_parameter with
|
Tx_rollup_rejection {|
manager_operation.Tx_rollup_rejection.tx_rollup := tx_rollup;
manager_operation.Tx_rollup_rejection.level := level;
manager_operation.Tx_rollup_rejection.message := message;
manager_operation.Tx_rollup_rejection.message_position :=
message_position;
manager_operation.Tx_rollup_rejection.message_path :=
message_path;
manager_operation.Tx_rollup_rejection.message_result_hash :=
message_result_hash;
manager_operation.Tx_rollup_rejection.message_result_path :=
&nb