🏗️ Apply_results.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Definition successful_transaction_result : Set :=
Apply_internal_results.successful_transaction_result.
Definition successful_origination_result : Set :=
Apply_internal_results.successful_origination_result.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Apply_internal_results.
Require TezosOfOCaml.Proto_alpha.Apply_operation_result.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Definition successful_transaction_result : Set :=
Apply_internal_results.successful_transaction_result.
Definition successful_origination_result : Set :=
Apply_internal_results.successful_origination_result.
Records for the constructor parameters
Module ConstructorRecords_successful_manager_operation_result.
Module successful_manager_operation_result.
Module Reveal_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Reveal_result.
Definition Reveal_result_skeleton := Reveal_result.record.
Module Delegation_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Delegation_result.
Definition Delegation_result_skeleton := Delegation_result.record.
Module Register_global_constant_result.
Record record {balance_updates consumed_gas size_of_constant
global_address : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
size_of_constant : size_of_constant;
global_address : global_address;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
balance_updates
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address balance_updates r.(consumed_gas) r.(size_of_constant)
r.(global_address).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
consumed_gas
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) consumed_gas r.(size_of_constant)
r.(global_address).
Definition with_size_of_constant
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
size_of_constant
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) r.(consumed_gas) size_of_constant
r.(global_address).
Definition with_global_address
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
global_address
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) r.(consumed_gas)
r.(size_of_constant) global_address.
End Register_global_constant_result.
Definition Register_global_constant_result_skeleton :=
Register_global_constant_result.record.
Module Set_deposits_limit_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Set_deposits_limit_result.
Definition Set_deposits_limit_result_skeleton :=
Set_deposits_limit_result.record.
Module Increase_paid_storage_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Increase_paid_storage_result.
Definition Increase_paid_storage_result_skeleton :=
Increase_paid_storage_result.record.
Module Update_consensus_key_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Update_consensus_key_result.
Definition Update_consensus_key_result_skeleton :=
Update_consensus_key_result.record.
Module Tx_rollup_origination_result.
Record record {balance_updates consumed_gas originated_tx_rollup : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
originated_tx_rollup : originated_tx_rollup;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_originated_tx_rollup}
balance_updates
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
balance_updates r.(consumed_gas) r.(originated_tx_rollup).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_originated_tx_rollup} consumed_gas
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
r.(balance_updates) consumed_gas r.(originated_tx_rollup).
Definition with_originated_tx_rollup
{t_balance_updates t_consumed_gas t_originated_tx_rollup}
originated_tx_rollup
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
r.(balance_updates) r.(consumed_gas) originated_tx_rollup.
End Tx_rollup_origination_result.
Definition Tx_rollup_origination_result_skeleton :=
Tx_rollup_origination_result.record.
Module Tx_rollup_submit_batch_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Tx_rollup_submit_batch_result.
Definition Tx_rollup_submit_batch_result_skeleton :=
Tx_rollup_submit_batch_result.record.
Module Tx_rollup_commit_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_commit_result.
Definition Tx_rollup_commit_result_skeleton :=
Tx_rollup_commit_result.record.
Module Tx_rollup_return_bond_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_return_bond_result.
Definition Tx_rollup_return_bond_result_skeleton :=
Tx_rollup_return_bond_result.record.
Module Tx_rollup_finalize_commitment_result.
Record record {balance_updates consumed_gas level : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
level : level;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level balance_updates
r.(consumed_gas) r.(level).
Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
consumed_gas r.(level).
Definition with_level {t_balance_updates t_consumed_gas t_level} level
(r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
r.(consumed_gas) level.
End Tx_rollup_finalize_commitment_result.
Definition Tx_rollup_finalize_commitment_result_skeleton :=
Tx_rollup_finalize_commitment_result.record.
Module Tx_rollup_remove_commitment_result.
Record record {balance_updates consumed_gas level : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
level : level;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level balance_updates
r.(consumed_gas) r.(level).
Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
consumed_gas r.(level).
Definition with_level {t_balance_updates t_consumed_gas t_level} level
(r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
r.(consumed_gas) level.
End Tx_rollup_remove_commitment_result.
Definition Tx_rollup_remove_commitment_result_skeleton :=
Tx_rollup_remove_commitment_result.record.
Module Tx_rollup_rejection_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_rejection_result.
Definition Tx_rollup_rejection_result_skeleton :=
Tx_rollup_rejection_result.record.
Module Tx_rollup_dispatch_tickets_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Tx_rollup_dispatch_tickets_result.
Definition Tx_rollup_dispatch_tickets_result_skeleton :=
Tx_rollup_dispatch_tickets_result.record.
Module Transfer_ticket_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Transfer_ticket_result.
Definition Transfer_ticket_result_skeleton := Transfer_ticket_result.record.
Module Dal_publish_slot_header_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Dal_publish_slot_header_result.
Definition Dal_publish_slot_header_result_skeleton :=
Dal_publish_slot_header_result.record.
Module Sc_rollup_originate_result.
Record record {balance_updates address genesis_commitment_hash
consumed_gas size : Set} : Set := Build {
balance_updates : balance_updates;
address : address;
genesis_commitment_hash : genesis_commitment_hash;
consumed_gas : consumed_gas;
size : size;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} balance_updates
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size balance_updates r.(address)
r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
Definition with_address
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} address
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) address
r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
Definition with_genesis_commitment_hash
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} genesis_commitment_hash
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
genesis_commitment_hash r.(consumed_gas) r.(size).
Definition with_consumed_gas
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} consumed_gas
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
r.(genesis_commitment_hash) consumed_gas r.(size).
Definition with_size
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} size
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
r.(genesis_commitment_hash) r.(consumed_gas) size.
End Sc_rollup_originate_result.
Definition Sc_rollup_originate_result_skeleton :=
Sc_rollup_originate_result.record.
Module Sc_rollup_add_messages_result.
Record record {consumed_gas inbox_after : Set} : Set := Build {
consumed_gas : consumed_gas;
inbox_after : inbox_after;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas t_inbox_after} consumed_gas
(r : record t_consumed_gas t_inbox_after) :=
Build t_consumed_gas t_inbox_after consumed_gas r.(inbox_after).
Definition with_inbox_after {t_consumed_gas t_inbox_after} inbox_after
(r : record t_consumed_gas t_inbox_after) :=
Build t_consumed_gas t_inbox_after r.(consumed_gas) inbox_after.
End Sc_rollup_add_messages_result.
Definition Sc_rollup_add_messages_result_skeleton :=
Sc_rollup_add_messages_result.record.
Module Sc_rollup_cement_result.
Record record {consumed_gas inbox_level : Set} : Set := Build {
consumed_gas : consumed_gas;
inbox_level : inbox_level;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas t_inbox_level} consumed_gas
(r : record t_consumed_gas t_inbox_level) :=
Build t_consumed_gas t_inbox_level consumed_gas r.(inbox_level).
Definition with_inbox_level {t_consumed_gas t_inbox_level} inbox_level
(r : record t_consumed_gas t_inbox_level) :=
Build t_consumed_gas t_inbox_level r.(consumed_gas) inbox_level.
End Sc_rollup_cement_result.
Definition Sc_rollup_cement_result_skeleton :=
Sc_rollup_cement_result.record.
Module Sc_rollup_publish_result.
Record record {consumed_gas staked_hash published_at_level balance_updates
: Set} : Set := Build {
consumed_gas : consumed_gas;
staked_hash : staked_hash;
published_at_level : published_at_level;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
consumed_gas
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates consumed_gas r.(staked_hash) r.(published_at_level)
r.(balance_updates).
Definition with_staked_hash
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
staked_hash
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) staked_hash r.(published_at_level)
r.(balance_updates).
Definition with_published_at_level
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
published_at_level
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) r.(staked_hash) published_at_level
r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
balance_updates
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) r.(staked_hash)
r.(published_at_level) balance_updates.
End Sc_rollup_publish_result.
Definition Sc_rollup_publish_result_skeleton :=
Sc_rollup_publish_result.record.
Module Sc_rollup_refute_result.
Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
consumed_gas : consumed_gas;
game_status : game_status;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_game_status t_balance_updates} consumed_gas
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates consumed_gas
r.(game_status) r.(balance_updates).
Definition with_game_status
{t_consumed_gas t_game_status t_balance_updates} game_status
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
game_status r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_game_status t_balance_updates} balance_updates
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
r.(game_status) balance_updates.
End Sc_rollup_refute_result.
Definition Sc_rollup_refute_result_skeleton :=
Sc_rollup_refute_result.record.
Module Sc_rollup_timeout_result.
Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
consumed_gas : consumed_gas;
game_status : game_status;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_game_status t_balance_updates} consumed_gas
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates consumed_gas
r.(game_status) r.(balance_updates).
Definition with_game_status
{t_consumed_gas t_game_status t_balance_updates} game_status
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
game_status r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_game_status t_balance_updates} balance_updates
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
r.(game_status) balance_updates.
End Sc_rollup_timeout_result.
Definition Sc_rollup_timeout_result_skeleton :=
Sc_rollup_timeout_result.record.
Module Sc_rollup_execute_outbox_message_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Sc_rollup_execute_outbox_message_result.
Definition Sc_rollup_execute_outbox_message_result_skeleton :=
Sc_rollup_execute_outbox_message_result.record.
Module Sc_rollup_recover_bond_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Sc_rollup_recover_bond_result.
Definition Sc_rollup_recover_bond_result_skeleton :=
Sc_rollup_recover_bond_result.record.
Module Zk_rollup_origination_result.
Record record {balance_updates originated_zk_rollup consumed_gas
storage_size : Set} : Set := Build {
balance_updates : balance_updates;
originated_zk_rollup : originated_zk_rollup;
consumed_gas : consumed_gas;
storage_size : storage_size;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
balance_updates
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size balance_updates r.(originated_zk_rollup)
r.(consumed_gas) r.(storage_size).
Definition with_originated_zk_rollup
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
originated_zk_rollup
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) originated_zk_rollup
r.(consumed_gas) r.(storage_size).
Definition with_consumed_gas
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
consumed_gas
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) r.(originated_zk_rollup)
consumed_gas r.(storage_size).
Definition with_storage_size
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
storage_size
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) r.(originated_zk_rollup)
r.(consumed_gas) storage_size.
End Zk_rollup_origination_result.
Definition Zk_rollup_origination_result_skeleton :=
Zk_rollup_origination_result.record.
Module Zk_rollup_publish_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Zk_rollup_publish_result.
Definition Zk_rollup_publish_result_skeleton :=
Zk_rollup_publish_result.record.
Module Zk_rollup_update_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Zk_rollup_update_result.
Definition Zk_rollup_update_result_skeleton :=
Zk_rollup_update_result.record.
End successful_manager_operation_result.
End ConstructorRecords_successful_manager_operation_result.
Import ConstructorRecords_successful_manager_operation_result.
Reserved Notation "'successful_manager_operation_result.Reveal_result".
Reserved Notation "'successful_manager_operation_result.Delegation_result".
Reserved Notation
"'successful_manager_operation_result.Register_global_constant_result".
Reserved Notation
"'successful_manager_operation_result.Set_deposits_limit_result".
Reserved Notation
"'successful_manager_operation_result.Increase_paid_storage_result".
Reserved Notation
"'successful_manager_operation_result.Update_consensus_key_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_origination_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_submit_batch_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_commit_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_return_bond_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_finalize_commitment_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_remove_commitment_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_rejection_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result".
Reserved Notation "'successful_manager_operation_result.Transfer_ticket_result".
Reserved Notation
"'successful_manager_operation_result.Dal_publish_slot_header_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_originate_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_add_messages_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_cement_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_publish_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_refute_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_timeout_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_recover_bond_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_origination_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_publish_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_update_result".
Inductive successful_manager_operation_result : Set :=
| Reveal_result :
'successful_manager_operation_result.Reveal_result →
successful_manager_operation_result
| Transaction_result :
successful_transaction_result → successful_manager_operation_result
| Origination_result :
successful_origination_result → successful_manager_operation_result
| Delegation_result :
'successful_manager_operation_result.Delegation_result →
successful_manager_operation_result
| Register_global_constant_result :
'successful_manager_operation_result.Register_global_constant_result →
successful_manager_operation_result
| Set_deposits_limit_result :
'successful_manager_operation_result.Set_deposits_limit_result →
successful_manager_operation_result
| Increase_paid_storage_result :
'successful_manager_operation_result.Increase_paid_storage_result →
successful_manager_operation_result
| Update_consensus_key_result :
'successful_manager_operation_result.Update_consensus_key_result →
successful_manager_operation_result
| Tx_rollup_origination_result :
'successful_manager_operation_result.Tx_rollup_origination_result →
successful_manager_operation_result
| Tx_rollup_submit_batch_result :
'successful_manager_operation_result.Tx_rollup_submit_batch_result →
successful_manager_operation_result
| Tx_rollup_commit_result :
'successful_manager_operation_result.Tx_rollup_commit_result →
successful_manager_operation_result
| Tx_rollup_return_bond_result :
'successful_manager_operation_result.Tx_rollup_return_bond_result →
successful_manager_operation_result
| Tx_rollup_finalize_commitment_result :
'successful_manager_operation_result.Tx_rollup_finalize_commitment_result →
successful_manager_operation_result
| Tx_rollup_remove_commitment_result :
'successful_manager_operation_result.Tx_rollup_remove_commitment_result →
successful_manager_operation_result
| Tx_rollup_rejection_result :
'successful_manager_operation_result.Tx_rollup_rejection_result →
successful_manager_operation_result
| Tx_rollup_dispatch_tickets_result :
'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result →
successful_manager_operation_result
| Transfer_ticket_result :
'successful_manager_operation_result.Transfer_ticket_result →
successful_manager_operation_result
| Dal_publish_slot_header_result :
'successful_manager_operation_result.Dal_publish_slot_header_result →
successful_manager_operation_result
| Sc_rollup_originate_result :
'successful_manager_operation_result.Sc_rollup_originate_result →
successful_manager_operation_result
| Sc_rollup_add_messages_result :
'successful_manager_operation_result.Sc_rollup_add_messages_result →
successful_manager_operation_result
| Sc_rollup_cement_result :
'successful_manager_operation_result.Sc_rollup_cement_result →
successful_manager_operation_result
| Sc_rollup_publish_result :
'successful_manager_operation_result.Sc_rollup_publish_result →
successful_manager_operation_result
| Sc_rollup_refute_result :
'successful_manager_operation_result.Sc_rollup_refute_result →
successful_manager_operation_result
| Sc_rollup_timeout_result :
'successful_manager_operation_result.Sc_rollup_timeout_result →
successful_manager_operation_result
| Sc_rollup_execute_outbox_message_result :
'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result
→ successful_manager_operation_result
| Sc_rollup_recover_bond_result :
'successful_manager_operation_result.Sc_rollup_recover_bond_result →
successful_manager_operation_result
| Zk_rollup_origination_result :
'successful_manager_operation_result.Zk_rollup_origination_result →
successful_manager_operation_result
| Zk_rollup_publish_result :
'successful_manager_operation_result.Zk_rollup_publish_result →
successful_manager_operation_result
| Zk_rollup_update_result :
'successful_manager_operation_result.Zk_rollup_update_result →
successful_manager_operation_result
where "'successful_manager_operation_result.Reveal_result" :=
(successful_manager_operation_result.Reveal_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Delegation_result" :=
(successful_manager_operation_result.Delegation_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Register_global_constant_result" :=
(successful_manager_operation_result.Register_global_constant_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t
Script_expr_hash.t)
and "'successful_manager_operation_result.Set_deposits_limit_result" :=
(successful_manager_operation_result.Set_deposits_limit_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Increase_paid_storage_result" :=
(successful_manager_operation_result.Increase_paid_storage_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Update_consensus_key_result" :=
(successful_manager_operation_result.Update_consensus_key_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_origination_result" :=
(successful_manager_operation_result.Tx_rollup_origination_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup.t)
and "'successful_manager_operation_result.Tx_rollup_submit_batch_result" :=
(successful_manager_operation_result.Tx_rollup_submit_batch_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Tx_rollup_commit_result" :=
(successful_manager_operation_result.Tx_rollup_commit_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_return_bond_result" :=
(successful_manager_operation_result.Tx_rollup_return_bond_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result"
:=
(successful_manager_operation_result.Tx_rollup_finalize_commitment_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_remove_commitment_result" :=
(successful_manager_operation_result.Tx_rollup_remove_commitment_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_rejection_result" :=
(successful_manager_operation_result.Tx_rollup_rejection_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result" :=
(successful_manager_operation_result.Tx_rollup_dispatch_tickets_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Transfer_ticket_result" :=
(successful_manager_operation_result.Transfer_ticket_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Dal_publish_slot_header_result" :=
(successful_manager_operation_result.Dal_publish_slot_header_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Sc_rollup_originate_result" :=
(successful_manager_operation_result.Sc_rollup_originate_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Sc_rollup.Address.t
Alpha_context.Sc_rollup.Commitment.Hash.t Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_add_messages_result" :=
(successful_manager_operation_result.Sc_rollup_add_messages_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Inbox.t)
and "'successful_manager_operation_result.Sc_rollup_cement_result" :=
(successful_manager_operation_result.Sc_rollup_cement_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Raw_level.t)
and "'successful_manager_operation_result.Sc_rollup_publish_result" :=
(successful_manager_operation_result.Sc_rollup_publish_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Commitment.Hash.t
Alpha_context.Raw_level.t Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_refute_result" :=
(successful_manager_operation_result.Sc_rollup_refute_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_timeout_result" :=
(successful_manager_operation_result.Sc_rollup_timeout_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result"
:=
(successful_manager_operation_result.Sc_rollup_execute_outbox_message_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_recover_bond_result" :=
(successful_manager_operation_result.Sc_rollup_recover_bond_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Zk_rollup_origination_result" :=
(successful_manager_operation_result.Zk_rollup_origination_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Zk_rollup.t
Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_publish_result" :=
(successful_manager_operation_result.Zk_rollup_publish_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_update_result" :=
(successful_manager_operation_result.Zk_rollup_update_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t).
Module successful_manager_operation_result.
Include ConstructorRecords_successful_manager_operation_result.successful_manager_operation_result.
Definition Reveal_result :=
'successful_manager_operation_result.Reveal_result.
Definition Delegation_result :=
'successful_manager_operation_result.Delegation_result.
Definition Register_global_constant_result :=
'successful_manager_operation_result.Register_global_constant_result.
Definition Set_deposits_limit_result :=
'successful_manager_operation_result.Set_deposits_limit_result.
Definition Increase_paid_storage_result :=
'successful_manager_operation_result.Increase_paid_storage_result.
Definition Update_consensus_key_result :=
'successful_manager_operation_result.Update_consensus_key_result.
Definition Tx_rollup_origination_result :=
'successful_manager_operation_result.Tx_rollup_origination_result.
Definition Tx_rollup_submit_batch_result :=
'successful_manager_operation_result.Tx_rollup_submit_batch_result.
Definition Tx_rollup_commit_result :=
'successful_manager_operation_result.Tx_rollup_commit_result.
Definition Tx_rollup_return_bond_result :=
'successful_manager_operation_result.Tx_rollup_return_bond_result.
Definition Tx_rollup_finalize_commitment_result :=
'successful_manager_operation_result.Tx_rollup_finalize_commitment_result.
Definition Tx_rollup_remove_commitment_result :=
'successful_manager_operation_result.Tx_rollup_remove_commitment_result.
Definition Tx_rollup_rejection_result :=
'successful_manager_operation_result.Tx_rollup_rejection_result.
Definition Tx_rollup_dispatch_tickets_result :=
'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.
Definition Transfer_ticket_result :=
'successful_manager_operation_result.Transfer_ticket_result.
Definition Dal_publish_slot_header_result :=
'successful_manager_operation_result.Dal_publish_slot_header_result.
Definition Sc_rollup_originate_result :=
'successful_manager_operation_result.Sc_rollup_originate_result.
Definition Sc_rollup_add_messages_result :=
'successful_manager_operation_result.Sc_rollup_add_messages_result.
Definition Sc_rollup_cement_result :=
'successful_manager_operation_result.Sc_rollup_cement_result.
Definition Sc_rollup_publish_result :=
'successful_manager_operation_result.Sc_rollup_publish_result.
Definition Sc_rollup_refute_result :=
'successful_manager_operation_result.Sc_rollup_refute_result.
Definition Sc_rollup_timeout_result :=
'successful_manager_operation_result.Sc_rollup_timeout_result.
Definition Sc_rollup_execute_outbox_message_result :=
'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.
Definition Sc_rollup_recover_bond_result :=
'successful_manager_operation_result.Sc_rollup_recover_bond_result.
Definition Zk_rollup_origination_result :=
'successful_manager_operation_result.Zk_rollup_origination_result.
Definition Zk_rollup_publish_result :=
'successful_manager_operation_result.Zk_rollup_publish_result.
Definition Zk_rollup_update_result :=
'successful_manager_operation_result.Zk_rollup_update_result.
End successful_manager_operation_result.
Definition migration_origination_result_to_successful_manager_operation_result
(function_parameter : Alpha_context.Migration.origination_result)
: successful_manager_operation_result :=
let '{|
Alpha_context.Migration.origination_result.balance_updates := balance_updates;
Alpha_context.Migration.origination_result.originated_contracts :=
originated_contracts;
Alpha_context.Migration.origination_result.storage_size := storage_size;
Alpha_context.Migration.origination_result.paid_storage_size_diff :=
paid_storage_size_diff
|} := function_parameter in
Origination_result
{|
Apply_internal_results.successful_origination_result.lazy_storage_diff :=
None;
Apply_internal_results.successful_origination_result.balance_updates :=
balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas :=
Alpha_context.Gas.Arith.zero;
Apply_internal_results.successful_origination_result.storage_size :=
storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |}.
Inductive packed_successful_manager_operation_result : Set :=
| Successful_manager_result :
successful_manager_operation_result →
packed_successful_manager_operation_result.
Definition pack_migration_operation_results
(results : list Alpha_context.Migration.origination_result)
: list packed_successful_manager_operation_result :=
List.map
(fun (el : Alpha_context.Migration.origination_result) ⇒
Successful_manager_result
(migration_origination_result_to_successful_manager_operation_result el))
results.
Definition manager_operation_result : Set :=
Apply_operation_result.operation_result Alpha_context.Kind.manager
successful_manager_operation_result.
Module Manager_result.
Module successful_manager_operation_result.
Module Reveal_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Reveal_result.
Definition Reveal_result_skeleton := Reveal_result.record.
Module Delegation_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Delegation_result.
Definition Delegation_result_skeleton := Delegation_result.record.
Module Register_global_constant_result.
Record record {balance_updates consumed_gas size_of_constant
global_address : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
size_of_constant : size_of_constant;
global_address : global_address;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
balance_updates
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address balance_updates r.(consumed_gas) r.(size_of_constant)
r.(global_address).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
consumed_gas
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) consumed_gas r.(size_of_constant)
r.(global_address).
Definition with_size_of_constant
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
size_of_constant
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) r.(consumed_gas) size_of_constant
r.(global_address).
Definition with_global_address
{t_balance_updates t_consumed_gas t_size_of_constant t_global_address}
global_address
(r :
record t_balance_updates t_consumed_gas t_size_of_constant
t_global_address) :=
Build t_balance_updates t_consumed_gas t_size_of_constant
t_global_address r.(balance_updates) r.(consumed_gas)
r.(size_of_constant) global_address.
End Register_global_constant_result.
Definition Register_global_constant_result_skeleton :=
Register_global_constant_result.record.
Module Set_deposits_limit_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Set_deposits_limit_result.
Definition Set_deposits_limit_result_skeleton :=
Set_deposits_limit_result.record.
Module Increase_paid_storage_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Increase_paid_storage_result.
Definition Increase_paid_storage_result_skeleton :=
Increase_paid_storage_result.record.
Module Update_consensus_key_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Update_consensus_key_result.
Definition Update_consensus_key_result_skeleton :=
Update_consensus_key_result.record.
Module Tx_rollup_origination_result.
Record record {balance_updates consumed_gas originated_tx_rollup : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
originated_tx_rollup : originated_tx_rollup;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_originated_tx_rollup}
balance_updates
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
balance_updates r.(consumed_gas) r.(originated_tx_rollup).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_originated_tx_rollup} consumed_gas
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
r.(balance_updates) consumed_gas r.(originated_tx_rollup).
Definition with_originated_tx_rollup
{t_balance_updates t_consumed_gas t_originated_tx_rollup}
originated_tx_rollup
(r : record t_balance_updates t_consumed_gas t_originated_tx_rollup) :=
Build t_balance_updates t_consumed_gas t_originated_tx_rollup
r.(balance_updates) r.(consumed_gas) originated_tx_rollup.
End Tx_rollup_origination_result.
Definition Tx_rollup_origination_result_skeleton :=
Tx_rollup_origination_result.record.
Module Tx_rollup_submit_batch_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Tx_rollup_submit_batch_result.
Definition Tx_rollup_submit_batch_result_skeleton :=
Tx_rollup_submit_batch_result.record.
Module Tx_rollup_commit_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_commit_result.
Definition Tx_rollup_commit_result_skeleton :=
Tx_rollup_commit_result.record.
Module Tx_rollup_return_bond_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_return_bond_result.
Definition Tx_rollup_return_bond_result_skeleton :=
Tx_rollup_return_bond_result.record.
Module Tx_rollup_finalize_commitment_result.
Record record {balance_updates consumed_gas level : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
level : level;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level balance_updates
r.(consumed_gas) r.(level).
Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
consumed_gas r.(level).
Definition with_level {t_balance_updates t_consumed_gas t_level} level
(r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
r.(consumed_gas) level.
End Tx_rollup_finalize_commitment_result.
Definition Tx_rollup_finalize_commitment_result_skeleton :=
Tx_rollup_finalize_commitment_result.record.
Module Tx_rollup_remove_commitment_result.
Record record {balance_updates consumed_gas level : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
level : level;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas t_level}
balance_updates (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level balance_updates
r.(consumed_gas) r.(level).
Definition with_consumed_gas {t_balance_updates t_consumed_gas t_level}
consumed_gas (r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
consumed_gas r.(level).
Definition with_level {t_balance_updates t_consumed_gas t_level} level
(r : record t_balance_updates t_consumed_gas t_level) :=
Build t_balance_updates t_consumed_gas t_level r.(balance_updates)
r.(consumed_gas) level.
End Tx_rollup_remove_commitment_result.
Definition Tx_rollup_remove_commitment_result_skeleton :=
Tx_rollup_remove_commitment_result.record.
Module Tx_rollup_rejection_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Tx_rollup_rejection_result.
Definition Tx_rollup_rejection_result_skeleton :=
Tx_rollup_rejection_result.record.
Module Tx_rollup_dispatch_tickets_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Tx_rollup_dispatch_tickets_result.
Definition Tx_rollup_dispatch_tickets_result_skeleton :=
Tx_rollup_dispatch_tickets_result.record.
Module Transfer_ticket_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Transfer_ticket_result.
Definition Transfer_ticket_result_skeleton := Transfer_ticket_result.record.
Module Dal_publish_slot_header_result.
Record record {consumed_gas : Set} : Set := Build {
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas} consumed_gas
(r : record t_consumed_gas) :=
Build t_consumed_gas consumed_gas.
End Dal_publish_slot_header_result.
Definition Dal_publish_slot_header_result_skeleton :=
Dal_publish_slot_header_result.record.
Module Sc_rollup_originate_result.
Record record {balance_updates address genesis_commitment_hash
consumed_gas size : Set} : Set := Build {
balance_updates : balance_updates;
address : address;
genesis_commitment_hash : genesis_commitment_hash;
consumed_gas : consumed_gas;
size : size;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} balance_updates
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size balance_updates r.(address)
r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
Definition with_address
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} address
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) address
r.(genesis_commitment_hash) r.(consumed_gas) r.(size).
Definition with_genesis_commitment_hash
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} genesis_commitment_hash
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
genesis_commitment_hash r.(consumed_gas) r.(size).
Definition with_consumed_gas
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} consumed_gas
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
r.(genesis_commitment_hash) consumed_gas r.(size).
Definition with_size
{t_balance_updates t_address t_genesis_commitment_hash t_consumed_gas
t_size} size
(r :
record t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size) :=
Build t_balance_updates t_address t_genesis_commitment_hash
t_consumed_gas t_size r.(balance_updates) r.(address)
r.(genesis_commitment_hash) r.(consumed_gas) size.
End Sc_rollup_originate_result.
Definition Sc_rollup_originate_result_skeleton :=
Sc_rollup_originate_result.record.
Module Sc_rollup_add_messages_result.
Record record {consumed_gas inbox_after : Set} : Set := Build {
consumed_gas : consumed_gas;
inbox_after : inbox_after;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas t_inbox_after} consumed_gas
(r : record t_consumed_gas t_inbox_after) :=
Build t_consumed_gas t_inbox_after consumed_gas r.(inbox_after).
Definition with_inbox_after {t_consumed_gas t_inbox_after} inbox_after
(r : record t_consumed_gas t_inbox_after) :=
Build t_consumed_gas t_inbox_after r.(consumed_gas) inbox_after.
End Sc_rollup_add_messages_result.
Definition Sc_rollup_add_messages_result_skeleton :=
Sc_rollup_add_messages_result.record.
Module Sc_rollup_cement_result.
Record record {consumed_gas inbox_level : Set} : Set := Build {
consumed_gas : consumed_gas;
inbox_level : inbox_level;
}.
Arguments record : clear implicits.
Definition with_consumed_gas {t_consumed_gas t_inbox_level} consumed_gas
(r : record t_consumed_gas t_inbox_level) :=
Build t_consumed_gas t_inbox_level consumed_gas r.(inbox_level).
Definition with_inbox_level {t_consumed_gas t_inbox_level} inbox_level
(r : record t_consumed_gas t_inbox_level) :=
Build t_consumed_gas t_inbox_level r.(consumed_gas) inbox_level.
End Sc_rollup_cement_result.
Definition Sc_rollup_cement_result_skeleton :=
Sc_rollup_cement_result.record.
Module Sc_rollup_publish_result.
Record record {consumed_gas staked_hash published_at_level balance_updates
: Set} : Set := Build {
consumed_gas : consumed_gas;
staked_hash : staked_hash;
published_at_level : published_at_level;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
consumed_gas
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates consumed_gas r.(staked_hash) r.(published_at_level)
r.(balance_updates).
Definition with_staked_hash
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
staked_hash
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) staked_hash r.(published_at_level)
r.(balance_updates).
Definition with_published_at_level
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
published_at_level
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) r.(staked_hash) published_at_level
r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_staked_hash t_published_at_level t_balance_updates}
balance_updates
(r :
record t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates) :=
Build t_consumed_gas t_staked_hash t_published_at_level
t_balance_updates r.(consumed_gas) r.(staked_hash)
r.(published_at_level) balance_updates.
End Sc_rollup_publish_result.
Definition Sc_rollup_publish_result_skeleton :=
Sc_rollup_publish_result.record.
Module Sc_rollup_refute_result.
Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
consumed_gas : consumed_gas;
game_status : game_status;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_game_status t_balance_updates} consumed_gas
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates consumed_gas
r.(game_status) r.(balance_updates).
Definition with_game_status
{t_consumed_gas t_game_status t_balance_updates} game_status
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
game_status r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_game_status t_balance_updates} balance_updates
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
r.(game_status) balance_updates.
End Sc_rollup_refute_result.
Definition Sc_rollup_refute_result_skeleton :=
Sc_rollup_refute_result.record.
Module Sc_rollup_timeout_result.
Record record {consumed_gas game_status balance_updates : Set} : Set := Build {
consumed_gas : consumed_gas;
game_status : game_status;
balance_updates : balance_updates;
}.
Arguments record : clear implicits.
Definition with_consumed_gas
{t_consumed_gas t_game_status t_balance_updates} consumed_gas
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates consumed_gas
r.(game_status) r.(balance_updates).
Definition with_game_status
{t_consumed_gas t_game_status t_balance_updates} game_status
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
game_status r.(balance_updates).
Definition with_balance_updates
{t_consumed_gas t_game_status t_balance_updates} balance_updates
(r : record t_consumed_gas t_game_status t_balance_updates) :=
Build t_consumed_gas t_game_status t_balance_updates r.(consumed_gas)
r.(game_status) balance_updates.
End Sc_rollup_timeout_result.
Definition Sc_rollup_timeout_result_skeleton :=
Sc_rollup_timeout_result.record.
Module Sc_rollup_execute_outbox_message_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Sc_rollup_execute_outbox_message_result.
Definition Sc_rollup_execute_outbox_message_result_skeleton :=
Sc_rollup_execute_outbox_message_result.record.
Module Sc_rollup_recover_bond_result.
Record record {balance_updates consumed_gas : Set} : Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
}.
Arguments record : clear implicits.
Definition with_balance_updates {t_balance_updates t_consumed_gas}
balance_updates (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas balance_updates r.(consumed_gas).
Definition with_consumed_gas {t_balance_updates t_consumed_gas}
consumed_gas (r : record t_balance_updates t_consumed_gas) :=
Build t_balance_updates t_consumed_gas r.(balance_updates) consumed_gas.
End Sc_rollup_recover_bond_result.
Definition Sc_rollup_recover_bond_result_skeleton :=
Sc_rollup_recover_bond_result.record.
Module Zk_rollup_origination_result.
Record record {balance_updates originated_zk_rollup consumed_gas
storage_size : Set} : Set := Build {
balance_updates : balance_updates;
originated_zk_rollup : originated_zk_rollup;
consumed_gas : consumed_gas;
storage_size : storage_size;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
balance_updates
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size balance_updates r.(originated_zk_rollup)
r.(consumed_gas) r.(storage_size).
Definition with_originated_zk_rollup
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
originated_zk_rollup
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) originated_zk_rollup
r.(consumed_gas) r.(storage_size).
Definition with_consumed_gas
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
consumed_gas
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) r.(originated_zk_rollup)
consumed_gas r.(storage_size).
Definition with_storage_size
{t_balance_updates t_originated_zk_rollup t_consumed_gas t_storage_size}
storage_size
(r :
record t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size) :=
Build t_balance_updates t_originated_zk_rollup t_consumed_gas
t_storage_size r.(balance_updates) r.(originated_zk_rollup)
r.(consumed_gas) storage_size.
End Zk_rollup_origination_result.
Definition Zk_rollup_origination_result_skeleton :=
Zk_rollup_origination_result.record.
Module Zk_rollup_publish_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Zk_rollup_publish_result.
Definition Zk_rollup_publish_result_skeleton :=
Zk_rollup_publish_result.record.
Module Zk_rollup_update_result.
Record record {balance_updates consumed_gas paid_storage_size_diff : Set} :
Set := Build {
balance_updates : balance_updates;
consumed_gas : consumed_gas;
paid_storage_size_diff : paid_storage_size_diff;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
balance_updates
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
balance_updates r.(consumed_gas) r.(paid_storage_size_diff).
Definition with_consumed_gas
{t_balance_updates t_consumed_gas t_paid_storage_size_diff} consumed_gas
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) consumed_gas r.(paid_storage_size_diff).
Definition with_paid_storage_size_diff
{t_balance_updates t_consumed_gas t_paid_storage_size_diff}
paid_storage_size_diff
(r : record t_balance_updates t_consumed_gas t_paid_storage_size_diff) :=
Build t_balance_updates t_consumed_gas t_paid_storage_size_diff
r.(balance_updates) r.(consumed_gas) paid_storage_size_diff.
End Zk_rollup_update_result.
Definition Zk_rollup_update_result_skeleton :=
Zk_rollup_update_result.record.
End successful_manager_operation_result.
End ConstructorRecords_successful_manager_operation_result.
Import ConstructorRecords_successful_manager_operation_result.
Reserved Notation "'successful_manager_operation_result.Reveal_result".
Reserved Notation "'successful_manager_operation_result.Delegation_result".
Reserved Notation
"'successful_manager_operation_result.Register_global_constant_result".
Reserved Notation
"'successful_manager_operation_result.Set_deposits_limit_result".
Reserved Notation
"'successful_manager_operation_result.Increase_paid_storage_result".
Reserved Notation
"'successful_manager_operation_result.Update_consensus_key_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_origination_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_submit_batch_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_commit_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_return_bond_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_finalize_commitment_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_remove_commitment_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_rejection_result".
Reserved Notation
"'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result".
Reserved Notation "'successful_manager_operation_result.Transfer_ticket_result".
Reserved Notation
"'successful_manager_operation_result.Dal_publish_slot_header_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_originate_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_add_messages_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_cement_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_publish_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_refute_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_timeout_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result".
Reserved Notation
"'successful_manager_operation_result.Sc_rollup_recover_bond_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_origination_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_publish_result".
Reserved Notation
"'successful_manager_operation_result.Zk_rollup_update_result".
Inductive successful_manager_operation_result : Set :=
| Reveal_result :
'successful_manager_operation_result.Reveal_result →
successful_manager_operation_result
| Transaction_result :
successful_transaction_result → successful_manager_operation_result
| Origination_result :
successful_origination_result → successful_manager_operation_result
| Delegation_result :
'successful_manager_operation_result.Delegation_result →
successful_manager_operation_result
| Register_global_constant_result :
'successful_manager_operation_result.Register_global_constant_result →
successful_manager_operation_result
| Set_deposits_limit_result :
'successful_manager_operation_result.Set_deposits_limit_result →
successful_manager_operation_result
| Increase_paid_storage_result :
'successful_manager_operation_result.Increase_paid_storage_result →
successful_manager_operation_result
| Update_consensus_key_result :
'successful_manager_operation_result.Update_consensus_key_result →
successful_manager_operation_result
| Tx_rollup_origination_result :
'successful_manager_operation_result.Tx_rollup_origination_result →
successful_manager_operation_result
| Tx_rollup_submit_batch_result :
'successful_manager_operation_result.Tx_rollup_submit_batch_result →
successful_manager_operation_result
| Tx_rollup_commit_result :
'successful_manager_operation_result.Tx_rollup_commit_result →
successful_manager_operation_result
| Tx_rollup_return_bond_result :
'successful_manager_operation_result.Tx_rollup_return_bond_result →
successful_manager_operation_result
| Tx_rollup_finalize_commitment_result :
'successful_manager_operation_result.Tx_rollup_finalize_commitment_result →
successful_manager_operation_result
| Tx_rollup_remove_commitment_result :
'successful_manager_operation_result.Tx_rollup_remove_commitment_result →
successful_manager_operation_result
| Tx_rollup_rejection_result :
'successful_manager_operation_result.Tx_rollup_rejection_result →
successful_manager_operation_result
| Tx_rollup_dispatch_tickets_result :
'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result →
successful_manager_operation_result
| Transfer_ticket_result :
'successful_manager_operation_result.Transfer_ticket_result →
successful_manager_operation_result
| Dal_publish_slot_header_result :
'successful_manager_operation_result.Dal_publish_slot_header_result →
successful_manager_operation_result
| Sc_rollup_originate_result :
'successful_manager_operation_result.Sc_rollup_originate_result →
successful_manager_operation_result
| Sc_rollup_add_messages_result :
'successful_manager_operation_result.Sc_rollup_add_messages_result →
successful_manager_operation_result
| Sc_rollup_cement_result :
'successful_manager_operation_result.Sc_rollup_cement_result →
successful_manager_operation_result
| Sc_rollup_publish_result :
'successful_manager_operation_result.Sc_rollup_publish_result →
successful_manager_operation_result
| Sc_rollup_refute_result :
'successful_manager_operation_result.Sc_rollup_refute_result →
successful_manager_operation_result
| Sc_rollup_timeout_result :
'successful_manager_operation_result.Sc_rollup_timeout_result →
successful_manager_operation_result
| Sc_rollup_execute_outbox_message_result :
'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result
→ successful_manager_operation_result
| Sc_rollup_recover_bond_result :
'successful_manager_operation_result.Sc_rollup_recover_bond_result →
successful_manager_operation_result
| Zk_rollup_origination_result :
'successful_manager_operation_result.Zk_rollup_origination_result →
successful_manager_operation_result
| Zk_rollup_publish_result :
'successful_manager_operation_result.Zk_rollup_publish_result →
successful_manager_operation_result
| Zk_rollup_update_result :
'successful_manager_operation_result.Zk_rollup_update_result →
successful_manager_operation_result
where "'successful_manager_operation_result.Reveal_result" :=
(successful_manager_operation_result.Reveal_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Delegation_result" :=
(successful_manager_operation_result.Delegation_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Register_global_constant_result" :=
(successful_manager_operation_result.Register_global_constant_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t
Script_expr_hash.t)
and "'successful_manager_operation_result.Set_deposits_limit_result" :=
(successful_manager_operation_result.Set_deposits_limit_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Increase_paid_storage_result" :=
(successful_manager_operation_result.Increase_paid_storage_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Update_consensus_key_result" :=
(successful_manager_operation_result.Update_consensus_key_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_origination_result" :=
(successful_manager_operation_result.Tx_rollup_origination_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup.t)
and "'successful_manager_operation_result.Tx_rollup_submit_batch_result" :=
(successful_manager_operation_result.Tx_rollup_submit_batch_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Tx_rollup_commit_result" :=
(successful_manager_operation_result.Tx_rollup_commit_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_return_bond_result" :=
(successful_manager_operation_result.Tx_rollup_return_bond_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_finalize_commitment_result"
:=
(successful_manager_operation_result.Tx_rollup_finalize_commitment_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_remove_commitment_result" :=
(successful_manager_operation_result.Tx_rollup_remove_commitment_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp
Alpha_context.Tx_rollup_level.t)
and "'successful_manager_operation_result.Tx_rollup_rejection_result" :=
(successful_manager_operation_result.Tx_rollup_rejection_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result" :=
(successful_manager_operation_result.Tx_rollup_dispatch_tickets_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Transfer_ticket_result" :=
(successful_manager_operation_result.Transfer_ticket_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Dal_publish_slot_header_result" :=
(successful_manager_operation_result.Dal_publish_slot_header_result_skeleton
Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Sc_rollup_originate_result" :=
(successful_manager_operation_result.Sc_rollup_originate_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Sc_rollup.Address.t
Alpha_context.Sc_rollup.Commitment.Hash.t Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_add_messages_result" :=
(successful_manager_operation_result.Sc_rollup_add_messages_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Inbox.t)
and "'successful_manager_operation_result.Sc_rollup_cement_result" :=
(successful_manager_operation_result.Sc_rollup_cement_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Raw_level.t)
and "'successful_manager_operation_result.Sc_rollup_publish_result" :=
(successful_manager_operation_result.Sc_rollup_publish_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Commitment.Hash.t
Alpha_context.Raw_level.t Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_refute_result" :=
(successful_manager_operation_result.Sc_rollup_refute_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_timeout_result" :=
(successful_manager_operation_result.Sc_rollup_timeout_result_skeleton
Alpha_context.Gas.Arith.fp Alpha_context.Sc_rollup.Game.status
Alpha_context.Receipt.balance_updates)
and "'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result"
:=
(successful_manager_operation_result.Sc_rollup_execute_outbox_message_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Sc_rollup_recover_bond_result" :=
(successful_manager_operation_result.Sc_rollup_recover_bond_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp)
and "'successful_manager_operation_result.Zk_rollup_origination_result" :=
(successful_manager_operation_result.Zk_rollup_origination_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Zk_rollup.t
Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_publish_result" :=
(successful_manager_operation_result.Zk_rollup_publish_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t)
and "'successful_manager_operation_result.Zk_rollup_update_result" :=
(successful_manager_operation_result.Zk_rollup_update_result_skeleton
Alpha_context.Receipt.balance_updates Alpha_context.Gas.Arith.fp Z.t).
Module successful_manager_operation_result.
Include ConstructorRecords_successful_manager_operation_result.successful_manager_operation_result.
Definition Reveal_result :=
'successful_manager_operation_result.Reveal_result.
Definition Delegation_result :=
'successful_manager_operation_result.Delegation_result.
Definition Register_global_constant_result :=
'successful_manager_operation_result.Register_global_constant_result.
Definition Set_deposits_limit_result :=
'successful_manager_operation_result.Set_deposits_limit_result.
Definition Increase_paid_storage_result :=
'successful_manager_operation_result.Increase_paid_storage_result.
Definition Update_consensus_key_result :=
'successful_manager_operation_result.Update_consensus_key_result.
Definition Tx_rollup_origination_result :=
'successful_manager_operation_result.Tx_rollup_origination_result.
Definition Tx_rollup_submit_batch_result :=
'successful_manager_operation_result.Tx_rollup_submit_batch_result.
Definition Tx_rollup_commit_result :=
'successful_manager_operation_result.Tx_rollup_commit_result.
Definition Tx_rollup_return_bond_result :=
'successful_manager_operation_result.Tx_rollup_return_bond_result.
Definition Tx_rollup_finalize_commitment_result :=
'successful_manager_operation_result.Tx_rollup_finalize_commitment_result.
Definition Tx_rollup_remove_commitment_result :=
'successful_manager_operation_result.Tx_rollup_remove_commitment_result.
Definition Tx_rollup_rejection_result :=
'successful_manager_operation_result.Tx_rollup_rejection_result.
Definition Tx_rollup_dispatch_tickets_result :=
'successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.
Definition Transfer_ticket_result :=
'successful_manager_operation_result.Transfer_ticket_result.
Definition Dal_publish_slot_header_result :=
'successful_manager_operation_result.Dal_publish_slot_header_result.
Definition Sc_rollup_originate_result :=
'successful_manager_operation_result.Sc_rollup_originate_result.
Definition Sc_rollup_add_messages_result :=
'successful_manager_operation_result.Sc_rollup_add_messages_result.
Definition Sc_rollup_cement_result :=
'successful_manager_operation_result.Sc_rollup_cement_result.
Definition Sc_rollup_publish_result :=
'successful_manager_operation_result.Sc_rollup_publish_result.
Definition Sc_rollup_refute_result :=
'successful_manager_operation_result.Sc_rollup_refute_result.
Definition Sc_rollup_timeout_result :=
'successful_manager_operation_result.Sc_rollup_timeout_result.
Definition Sc_rollup_execute_outbox_message_result :=
'successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.
Definition Sc_rollup_recover_bond_result :=
'successful_manager_operation_result.Sc_rollup_recover_bond_result.
Definition Zk_rollup_origination_result :=
'successful_manager_operation_result.Zk_rollup_origination_result.
Definition Zk_rollup_publish_result :=
'successful_manager_operation_result.Zk_rollup_publish_result.
Definition Zk_rollup_update_result :=
'successful_manager_operation_result.Zk_rollup_update_result.
End successful_manager_operation_result.
Definition migration_origination_result_to_successful_manager_operation_result
(function_parameter : Alpha_context.Migration.origination_result)
: successful_manager_operation_result :=
let '{|
Alpha_context.Migration.origination_result.balance_updates := balance_updates;
Alpha_context.Migration.origination_result.originated_contracts :=
originated_contracts;
Alpha_context.Migration.origination_result.storage_size := storage_size;
Alpha_context.Migration.origination_result.paid_storage_size_diff :=
paid_storage_size_diff
|} := function_parameter in
Origination_result
{|
Apply_internal_results.successful_origination_result.lazy_storage_diff :=
None;
Apply_internal_results.successful_origination_result.balance_updates :=
balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas :=
Alpha_context.Gas.Arith.zero;
Apply_internal_results.successful_origination_result.storage_size :=
storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |}.
Inductive packed_successful_manager_operation_result : Set :=
| Successful_manager_result :
successful_manager_operation_result →
packed_successful_manager_operation_result.
Definition pack_migration_operation_results
(results : list Alpha_context.Migration.origination_result)
: list packed_successful_manager_operation_result :=
List.map
(fun (el : Alpha_context.Migration.origination_result) ⇒
Successful_manager_result
(migration_origination_result_to_successful_manager_operation_result el))
results.
Definition manager_operation_result : Set :=
Apply_operation_result.operation_result Alpha_context.Kind.manager
successful_manager_operation_result.
Module Manager_result.
Records for the constructor parameters
Module ConstructorRecords_case.
Module case.
Module MCase.
Record record {op_case encoding kind select proj inj t : Set} : Set := Build {
op_case : op_case;
encoding : encoding;
kind : kind;
select : select;
proj : proj;
inj : inj;
t : t;
}.
Arguments record : clear implicits.
Definition with_op_case
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} op_case
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t op_case
r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) r.(t).
Definition with_encoding
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} encoding
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) encoding r.(kind) r.(select) r.(proj) r.(inj) r.(t).
Definition with_kind
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} kind
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) kind r.(select) r.(proj) r.(inj) r.(t).
Definition with_select
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} select
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) select r.(proj) r.(inj) r.(t).
Definition with_proj
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} proj
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) proj r.(inj) r.(t).
Definition with_inj
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} inj
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) inj r.(t).
Definition with_t
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} t
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) t.
End MCase.
Definition MCase_skeleton := MCase.record.
End case.
End ConstructorRecords_case.
Import ConstructorRecords_case.
Reserved Notation "'case.MCase".
Inductive case (kind : Set) : Set :=
| MCase : ∀ {a : Set}, 'case.MCase a → case kind
where "'case.MCase" :=
(fun (t_a : Set) ⇒ case.MCase_skeleton
Alpha_context.Operation.Encoding.Manager_operations.case
(Data_encoding.t t_a) Alpha_context.Kind.manager
(packed_successful_manager_operation_result →
option successful_manager_operation_result)
(successful_manager_operation_result → t_a)
(t_a → successful_manager_operation_result)
(Data_encoding.t manager_operation_result)).
Module case.
Include ConstructorRecords_case.case.
Definition MCase := 'case.MCase.
End case.
Arguments MCase {_ _}.
Definition make {A B : Set}
(op_case : Alpha_context.Operation.Encoding.Manager_operations.case)
(encoding : Data_encoding.encoding A)
(kind_value : Alpha_context.Kind.manager)
(select :
packed_successful_manager_operation_result →
option successful_manager_operation_result)
(proj : successful_manager_operation_result → A)
(inj : A → successful_manager_operation_result) : case B :=
let
'Alpha_context.Operation.Encoding.Manager_operations.MCase {|
Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name := name
|} := op_case in
let t_value :=
Data_encoding.def
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"operation.alpha.operation_result."
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"operation.alpha.operation_result.%s") name) None None
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Applied" None (Data_encoding.Tag 0)
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "status"
(Data_encoding.constant
"applied")))
encoding)
(fun (o_value :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match o_value with
|
(Apply_operation_result.Skipped _ |
Apply_operation_result.Failed _ _ |
Apply_operation_result.Backtracked _ _)
⇒ None
| Apply_operation_result.Applied o_value ⇒
let o_value :=
cast
successful_manager_operation_result
o_value in
match
select
(Successful_manager_result
o_value)
with
| None ⇒ None
| Some o_value ⇒
Some (tt, (proj o_value))
end
end)
(fun (function_parameter : unit × A) ⇒
let '(_, x_value) := function_parameter in
Apply_operation_result.Applied (inj x_value));
Data_encoding.case_value "Failed" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "status"
(Data_encoding.constant "failed"))
(Data_encoding.req None None "errors"
Apply_operation_result.trace_encoding))
(fun (function_parameter :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match function_parameter with
| Apply_operation_result.Failed _ errs ⇒
Some (tt, errs)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Error_monad.trace Error_monad._error) ⇒
let '(_, errs) := function_parameter in
Apply_operation_result.Failed kind_value errs);
Data_encoding.case_value "Skipped" None (Data_encoding.Tag 2)
(Data_encoding.obj1
(Data_encoding.req None None "status"
(Data_encoding.constant "skipped")))
(fun (function_parameter :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match function_parameter with
| Apply_operation_result.Skipped _ ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Apply_operation_result.Skipped kind_value);
Data_encoding.case_value "Backtracked" None (Data_encoding.Tag 3)
(Data_encoding.merge_objs
(Data_encoding.obj2
(Data_encoding.req None None "status"
(Data_encoding.constant
"backtracked"))
(Data_encoding.opt None None "errors"
Apply_operation_result.trace_encoding))
encoding)
(fun (o_value :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match o_value with
|
(Apply_operation_result.Skipped _ |
Apply_operation_result.Failed _ _ |
Apply_operation_result.Applied _) ⇒
None
|
Apply_operation_result.Backtracked
o_value errs ⇒
let '[errs, o_value] :=
cast
[option
(Error_monad.trace
Error_monad._error)
**
successful_manager_operation_result]
[errs, o_value] in
match
select
(Successful_manager_result
o_value)
with
| None ⇒ None
| Some o_value ⇒
Some
((tt, errs),
(proj
o_value))
end
end)
(fun (function_parameter :
(unit ×
option
(Error_monad.trace
Error_monad._error))
× A) ⇒
let '((_, errs), x_value) := function_parameter
in
Apply_operation_result.Backtracked (inj x_value)
errs)
]) in
MCase
{| case.MCase.op_case := op_case; case.MCase.encoding := encoding;
case.MCase.kind := kind_value; case.MCase.select := select;
case.MCase.proj := proj; case.MCase.inj := inj; case.MCase.t := t_value;
|}.
Definition reveal_case : case Alpha_context.Kind.reveal :=
make Alpha_context.Operation.Encoding.Manager_operations.reveal_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Reveal_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Reveal_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Reveal_result {|
successful_manager_operation_result.Reveal_result.consumed_gas := consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Reveal_result
{|
successful_manager_operation_result.Reveal_result.consumed_gas :=
consumed_gas; |}).
Definition transaction_contract_variant_cases
: Data_encoding.encoding
Apply_internal_results.successful_transaction_result :=
Data_encoding.union None
[
Data_encoding.case_value "To_contract" None (Data_encoding.Tag 0)
(Data_encoding.obj9
(Data_encoding.opt None None "storage"
Alpha_context.Script.expr_encoding)
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "ticket_updates"
Ticket_receipt.encoding nil)
(Data_encoding.dft None None "originated_contracts"
(Data_encoding.list_value None
Alpha_context.Contract.originated_encoding) nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size"
Data_encoding.z_value Z.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero)
(Data_encoding.dft None None
"allocated_destination_contract"
Data_encoding.bool_value false)
(Data_encoding.opt None None "lazy_storage_diff"
Alpha_context.Lazy_storage.encoding))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_contract_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
:= storage_value;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:=
lazy_storage_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:=
balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
:=
ticket_receipt;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:=
originated_contracts;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:=
consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:=
storage_size;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:=
paid_storage_size_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:=
allocated_destination_contract
|} ⇒
Some
(storage_value, balance_updates, ticket_receipt,
originated_contracts, consumed_gas,
storage_size, paid_storage_size_diff,
allocated_destination_contract,
lazy_storage_diff)
| _ ⇒ None
end)
(fun (function_parameter :
option Alpha_context.Script.expr ×
Alpha_context.Receipt.balance_updates ×
Ticket_receipt.t × list Contract_hash.t ×
Alpha_context.Gas.Arith.fp × Z.t × Z.t × bool ×
option Alpha_context.Lazy_storage.diffs) ⇒
let
'(storage_value, balance_updates, ticket_receipt,
originated_contracts, consumed_gas,
storage_size, paid_storage_size_diff,
allocated_destination_contract,
lazy_storage_diff) := function_parameter in
Apply_internal_results.Transaction_to_contract_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
:= storage_value;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
:= ticket_receipt;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= storage_size;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= paid_storage_size_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |});
Data_encoding.case_value "To_tx_rollup" None (Data_encoding.Tag 1)
(Data_encoding.obj4
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "ticket_hash"
Alpha_context.Ticket_hash.encoding)
(Data_encoding.req None None "paid_storage_size_diff"
Data_encoding.n_value))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_tx_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:=
balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:=
consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:=
paid_storage_size_diff
|} ⇒
Some
(balance_updates, consumed_gas, ticket_hash,
paid_storage_size_diff)
| _ ⇒ None
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Gas.Arith.fp ×
Alpha_context.Ticket_hash.t × Z.t) ⇒
let
'(balance_updates, consumed_gas, ticket_hash,
paid_storage_size_diff) := function_parameter in
Apply_internal_results.Transaction_to_tx_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |});
Data_encoding.case_value "To_sc_rollup" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_after"
Alpha_context.Sc_rollup.Inbox.encoding))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_sc_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
:=
inbox_after
|} ⇒ Some (consumed_gas, inbox_after)
| _ ⇒ None
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t)
⇒
let '(consumed_gas, inbox_after) := function_parameter in
Apply_internal_results.Transaction_to_sc_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
:= inbox_after; |})
].
Definition transaction_case : case Alpha_context.Kind.transaction :=
make Alpha_context.Operation.Encoding.Manager_operations.transaction_case
transaction_contract_variant_cases
Alpha_context.Kind.Transaction_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Transaction_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
| Transaction_result x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end)
(fun (x_value : Apply_internal_results.successful_transaction_result) ⇒
Transaction_result x_value).
Definition origination_case : case Alpha_context.Kind.origination :=
make Alpha_context.Operation.Encoding.Manager_operations.origination_case
(Data_encoding.obj6
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "originated_contracts"
(Data_encoding.list_value None
Alpha_context.Contract.originated_encoding) nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero)
(Data_encoding.opt None None "lazy_storage_diff"
Alpha_context.Lazy_storage.encoding))
Alpha_context.Kind.Origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Origination_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Origination_result {|
Apply_internal_results.successful_origination_result.lazy_storage_diff :=
lazy_storage_diff;
Apply_internal_results.successful_origination_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_origination_result.storage_size
:= storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒
(balance_updates, originated_contracts, consumed_gas, storage_size,
paid_storage_size_diff, lazy_storage_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × list Contract_hash.t ×
Alpha_context.Gas.Arith.fp × Z.t × Z.t ×
option Alpha_context.Lazy_storage.diffs) ⇒
let
'(balance_updates, originated_contracts, consumed_gas, storage_size,
paid_storage_size_diff, lazy_storage_diff) := function_parameter in
Origination_result
{|
Apply_internal_results.successful_origination_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_internal_results.successful_origination_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas :=
consumed_gas;
Apply_internal_results.successful_origination_result.storage_size :=
storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition register_global_constant_case
: case Alpha_context.Kind.register_global_constant :=
make
Alpha_context.Operation.Encoding.Manager_operations.register_global_constant_case
(Data_encoding.obj4
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
(Data_encoding.req None None "global_address" Script_expr_hash.encoding))
Alpha_context.Kind.Register_global_constant_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Register_global_constant_result _) as op)
⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Register_global_constant_result {|
successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Register_global_constant_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Register_global_constant_result.size_of_constant
:= size_of_constant;
successful_manager_operation_result.Register_global_constant_result.global_address
:= global_address
|} ⇒
(balance_updates, consumed_gas, size_of_constant, global_address)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t
× Script_expr_hash.t) ⇒
let
'(balance_updates, consumed_gas, size_of_constant, global_address) :=
function_parameter in
Register_global_constant_result
{|
successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Register_global_constant_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Register_global_constant_result.size_of_constant
:= size_of_constant;
successful_manager_operation_result.Register_global_constant_result.global_address
:= global_address; |}).
Definition delegation_case : case Alpha_context.Kind.delegation :=
make Alpha_context.Operation.Encoding.Manager_operations.delegation_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Delegation_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Delegation_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Delegation_result {|
successful_manager_operation_result.Delegation_result.consumed_gas :=
consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Delegation_result
{|
successful_manager_operation_result.Delegation_result.consumed_gas
:= consumed_gas; |}).
Definition update_consensus_key_case
: case Alpha_context.Kind.update_consensus_key :=
make
Alpha_context.Operation.Encoding.Manager_operations.update_consensus_key_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Update_consensus_key_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Update_consensus_key_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Update_consensus_key_result {|
successful_manager_operation_result.Update_consensus_key_result.consumed_gas
:= consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Update_consensus_key_result
{|
successful_manager_operation_result.Update_consensus_key_result.consumed_gas
:= consumed_gas; |}).
Definition set_deposits_limit_case
: case Alpha_context.Kind.set_deposits_limit :=
make
Alpha_context.Operation.Encoding.Manager_operations.set_deposits_limit_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Set_deposits_limit_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Set_deposits_limit_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Set_deposits_limit_result {|
successful_manager_operation_result.Set_deposits_limit_result.consumed_gas :=
consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Set_deposits_limit_result
{|
successful_manager_operation_result.Set_deposits_limit_result.consumed_gas
:= consumed_gas; |}).
Definition increase_paid_storage_case
: case Alpha_context.Kind.increase_paid_storage :=
make
Alpha_context.Operation.Encoding.Manager_operations.increase_paid_storage_case
(Data_encoding.obj2
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Increase_paid_storage_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Increase_paid_storage_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Increase_paid_storage_result {|
successful_manager_operation_result.Increase_paid_storage_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Increase_paid_storage_result
{|
successful_manager_operation_result.Increase_paid_storage_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_origination_case
: case Alpha_context.Kind.tx_rollup_origination :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_origination_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "originated_rollup"
Alpha_context.Tx_rollup.encoding))
Alpha_context.Kind.Tx_rollup_origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_origination_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_origination_result {|
successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
:= originated_tx_rollup
|} ⇒ (balance_updates, consumed_gas, originated_tx_rollup)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup.t) ⇒
let '(balance_updates, consumed_gas, originated_tx_rollup) :=
function_parameter in
Tx_rollup_origination_result
{|
successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
:= originated_tx_rollup; |}).
Definition tx_rollup_submit_batch_case
: case Alpha_context.Kind.tx_rollup_submit_batch :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_submit_batch_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "paid_storage_size_diff"
Data_encoding.n_value))
Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_submit_batch_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_submit_batch_result {|
successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Tx_rollup_submit_batch_result
{|
successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition tx_rollup_commit_case : case Alpha_context.Kind.tx_rollup_commit :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_commit_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_commit_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_commit_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_commit_result {|
successful_manager_operation_result.Tx_rollup_commit_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_commit_result
{|
successful_manager_operation_result.Tx_rollup_commit_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_return_bond_case
: case Alpha_context.Kind.tx_rollup_return_bond :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_return_bond_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_return_bond_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_return_bond_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_return_bond_result {|
successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_return_bond_result
{|
successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_finalize_commitment_case
: case Alpha_context.Kind.tx_rollup_finalize_commitment :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_finalize_commitment_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "level"
Alpha_context.Tx_rollup_level.encoding))
Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_finalize_commitment_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_finalize_commitment_result {|
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
:= level
|} ⇒ (balance_updates, consumed_gas, level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup_level.t) ⇒
let '(balance_updates, consumed_gas, level) := function_parameter in
Tx_rollup_finalize_commitment_result
{|
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
:= level; |}).
Definition tx_rollup_remove_commitment_case
: case Alpha_context.Kind.tx_rollup_remove_commitment :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_remove_commitment_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "level"
Alpha_context.Tx_rollup_level.encoding))
Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_remove_commitment_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_remove_commitment_result {|
successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
:= level
|} ⇒ (balance_updates, consumed_gas, level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup_level.t) ⇒
let '(balance_updates, consumed_gas, level) := function_parameter in
Tx_rollup_remove_commitment_result
{|
successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
:= level; |}).
Definition tx_rollup_rejection_case
: case Alpha_context.Kind.tx_rollup_rejection :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_rejection_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_rejection_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_rejection_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_rejection_result {|
successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_rejection_result
{|
successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_dispatch_tickets_case
: case Alpha_context.Kind.tx_rollup_dispatch_tickets :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_dispatch_tickets_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_dispatch_tickets_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_dispatch_tickets_result {|
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Tx_rollup_dispatch_tickets_result
{|
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition transfer_ticket_case : case Alpha_context.Kind.transfer_ticket :=
make
Alpha_context.Operation.Encoding.Manager_operations.transfer_ticket_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Transfer_ticket_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Transfer_ticket_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Transfer_ticket_result {|
successful_manager_operation_result.Transfer_ticket_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Transfer_ticket_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Transfer_ticket_result
{|
successful_manager_operation_result.Transfer_ticket_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Transfer_ticket_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition dal_publish_slot_header_case
: case Alpha_context.Kind.dal_publish_slot_header :=
make
Alpha_context.Operation.Encoding.Manager_operations.dal_publish_slot_header_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Dal_publish_slot_header_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Dal_publish_slot_header_result _) as op)
⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Dal_publish_slot_header_result {|
successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
:= consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Dal_publish_slot_header_result
{|
successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
:= consumed_gas; |}).
Definition zk_rollup_origination_case
: case Alpha_context.Kind.zk_rollup_origination :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_origination_case
(Data_encoding.obj4
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.req None None "originated_zk_rollup"
Alpha_context.Zk_rollup.Address.encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Zk_rollup_origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_origination_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_origination_result {|
successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size
|} ⇒
(balance_updates, originated_zk_rollup, consumed_gas, storage_size)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Zk_rollup.Address.t × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let
'(balance_updates, originated_zk_rollup, consumed_gas, storage_size) :=
function_parameter in
Zk_rollup_origination_result
{|
successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size; |}).
Definition zk_rollup_publish_case
: case Alpha_context.Kind.zk_rollup_publish :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_publish_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Zk_rollup_publish_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_publish_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_publish_result {|
successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Zk_rollup_publish_result
{|
successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition zk_rollup_update_case : case Alpha_context.Kind.zk_rollup_update :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_update_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Zk_rollup_update_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_update_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_update_result {|
successful_manager_operation_result.Zk_rollup_update_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Zk_rollup_update_result
{|
successful_manager_operation_result.Zk_rollup_update_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition sc_rollup_originate_case
: case Alpha_context.Kind.sc_rollup_originate :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_originate_case
(Data_encoding.obj5
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.req None None "address"
Alpha_context.Sc_rollup.Address.encoding)
(Data_encoding.req None None "genesis_commitment_hash"
Alpha_context.Sc_rollup.Commitment.Hash.encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Sc_rollup_originate_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_originate_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_originate_result {|
successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_originate_result.address
:= address;
successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
:= genesis_commitment_hash;
successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_originate_result.size
:= size_value
|} ⇒
(balance_updates, address, genesis_commitment_hash, consumed_gas,
size_value)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Sc_rollup.Address.t ×
Alpha_context.Sc_rollup.Commitment.Hash.t × Alpha_context.Gas.Arith.fp
× Z.t) ⇒
let
'(balance_updates, address, genesis_commitment_hash, consumed_gas,
size_value) := function_parameter in
Sc_rollup_originate_result
{|
successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_originate_result.address
:= address;
successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
:= genesis_commitment_hash;
successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_originate_result.size
:= size_value; |}).
Definition sc_rollup_add_messages_case
: case Alpha_context.Kind.sc_rollup_add_messages :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_add_messages_case
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_after"
Alpha_context.Sc_rollup.Inbox.encoding))
Alpha_context.Kind.Sc_rollup_add_messages_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_add_messages_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_add_messages_result {|
successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
:= inbox_after
|} ⇒ (consumed_gas, inbox_after)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t) ⇒
let '(consumed_gas, inbox_after) := function_parameter in
Sc_rollup_add_messages_result
{|
successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
:= inbox_after; |}).
Definition sc_rollup_cement_case : case Alpha_context.Kind.sc_rollup_cement :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_cement_case
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_level"
Alpha_context.Raw_level.encoding))
Alpha_context.Kind.Sc_rollup_cement_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_cement_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_cement_result {|
successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
:= inbox_level
|} ⇒ (consumed_gas, inbox_level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Raw_level.t) ⇒
let '(consumed_gas, inbox_level) := function_parameter in
Sc_rollup_cement_result
{|
successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
:= inbox_level; |}).
Definition sc_rollup_publish_case
: case Alpha_context.Kind.sc_rollup_publish :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_publish_case
(Data_encoding.obj4
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "staked_hash"
Alpha_context.Sc_rollup.Commitment.Hash.encoding)
(Data_encoding.req None None "published_at_level"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_publish_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_publish_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_publish_result {|
successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
:= staked_hash;
successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
:= published_at_level;
successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
:= balance_updates
|} ⇒
(consumed_gas, staked_hash, published_at_level, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Commitment.Hash.t ×
Alpha_context.Raw_level.t × Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, staked_hash, published_at_level, balance_updates) :=
function_parameter in
Sc_rollup_publish_result
{|
successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
:= staked_hash;
successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
:= published_at_level;
successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_refute_case : case Alpha_context.Kind.sc_rollup_refute :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_refute_case
(Data_encoding.obj3
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "game_status"
Alpha_context.Sc_rollup.Game.status_encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_refute_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_refute_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_refute_result {|
successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_refute_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
:= balance_updates
|} ⇒ (consumed_gas, game_status, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, game_status, balance_updates) := function_parameter
in
Sc_rollup_refute_result
{|
successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_refute_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_timeout_case
: case Alpha_context.Kind.sc_rollup_timeout :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_timeout_case
(Data_encoding.obj3
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "game_status"
Alpha_context.Sc_rollup.Game.status_encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_timeout_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_timeout_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_timeout_result {|
successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_timeout_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
:= balance_updates
|} ⇒ (consumed_gas, game_status, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, game_status, balance_updates) := function_parameter
in
Sc_rollup_timeout_result
{|
successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_timeout_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_execute_outbox_message_case
: case Alpha_context.Kind.sc_rollup_execute_outbox_message :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_execute_outbox_message_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Sc_rollup_execute_outbox_message_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_execute_outbox_message_result {|
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Sc_rollup_execute_outbox_message_result
{|
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition sc_rollup_recover_bond_case
: case Alpha_context.Kind.sc_rollup_recover_bond :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_recover_bond_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_recover_bond_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_recover_bond_result {|
successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Sc_rollup_recover_bond_result
{|
successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
:= consumed_gas; |}).
End Manager_result.
Definition successful_manager_operation_result_encoding
: Data_encoding.t packed_successful_manager_operation_result :=
let make {kind : Set} (mcase : Manager_result.case kind)
: Data_encoding.case packed_successful_manager_operation_result :=
let 'Manager_result.MCase res_case := mcase in
let 'existT _ __MCase_'a res_case :=
existT (A := Set) (fun __MCase_'a ⇒ Manager_result.case.MCase __MCase_'a)
_ res_case in
let 'Alpha_context.Operation.Encoding.Manager_operations.MCase op_case :=
res_case.(Manager_result.case.MCase.op_case) in
Data_encoding.case_value
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)
None
(Data_encoding.Tag
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.tag))
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "kind"
(Data_encoding.constant
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name))))
res_case.(Manager_result.case.MCase.encoding))
(fun (res : packed_successful_manager_operation_result) ⇒
match res_case.(Manager_result.case.MCase.select) res with
| Some res ⇒ Some (tt, (res_case.(Manager_result.case.MCase.proj) res))
| None ⇒ None
end)
(fun (function_parameter : unit × __MCase_'a) ⇒
let '(_, res) := function_parameter in
Successful_manager_result (res_case.(Manager_result.case.MCase.inj) res))
in
Data_encoding.def "operation.alpha.successful_manager_operation_result" None
None
(Data_encoding.union None
[
make Manager_result.reveal_case;
make Manager_result.transaction_case;
make Manager_result.origination_case;
make Manager_result.delegation_case;
make Manager_result.update_consensus_key_case;
make Manager_result.set_deposits_limit_case;
make Manager_result.increase_paid_storage_case;
make Manager_result.sc_rollup_originate_case
]).
Module case.
Module MCase.
Record record {op_case encoding kind select proj inj t : Set} : Set := Build {
op_case : op_case;
encoding : encoding;
kind : kind;
select : select;
proj : proj;
inj : inj;
t : t;
}.
Arguments record : clear implicits.
Definition with_op_case
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} op_case
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t op_case
r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) r.(t).
Definition with_encoding
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} encoding
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) encoding r.(kind) r.(select) r.(proj) r.(inj) r.(t).
Definition with_kind
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} kind
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) kind r.(select) r.(proj) r.(inj) r.(t).
Definition with_select
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} select
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) select r.(proj) r.(inj) r.(t).
Definition with_proj
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} proj
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) proj r.(inj) r.(t).
Definition with_inj
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} inj
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) inj r.(t).
Definition with_t
{t_op_case t_encoding t_kind t_select t_proj t_inj t_t} t
(r : record t_op_case t_encoding t_kind t_select t_proj t_inj t_t) :=
Build t_op_case t_encoding t_kind t_select t_proj t_inj t_t
r.(op_case) r.(encoding) r.(kind) r.(select) r.(proj) r.(inj) t.
End MCase.
Definition MCase_skeleton := MCase.record.
End case.
End ConstructorRecords_case.
Import ConstructorRecords_case.
Reserved Notation "'case.MCase".
Inductive case (kind : Set) : Set :=
| MCase : ∀ {a : Set}, 'case.MCase a → case kind
where "'case.MCase" :=
(fun (t_a : Set) ⇒ case.MCase_skeleton
Alpha_context.Operation.Encoding.Manager_operations.case
(Data_encoding.t t_a) Alpha_context.Kind.manager
(packed_successful_manager_operation_result →
option successful_manager_operation_result)
(successful_manager_operation_result → t_a)
(t_a → successful_manager_operation_result)
(Data_encoding.t manager_operation_result)).
Module case.
Include ConstructorRecords_case.case.
Definition MCase := 'case.MCase.
End case.
Arguments MCase {_ _}.
Definition make {A B : Set}
(op_case : Alpha_context.Operation.Encoding.Manager_operations.case)
(encoding : Data_encoding.encoding A)
(kind_value : Alpha_context.Kind.manager)
(select :
packed_successful_manager_operation_result →
option successful_manager_operation_result)
(proj : successful_manager_operation_result → A)
(inj : A → successful_manager_operation_result) : case B :=
let
'Alpha_context.Operation.Encoding.Manager_operations.MCase {|
Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name := name
|} := op_case in
let t_value :=
Data_encoding.def
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"operation.alpha.operation_result."
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))
"operation.alpha.operation_result.%s") name) None None
(Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
[
Data_encoding.case_value "Applied" None (Data_encoding.Tag 0)
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "status"
(Data_encoding.constant
"applied")))
encoding)
(fun (o_value :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match o_value with
|
(Apply_operation_result.Skipped _ |
Apply_operation_result.Failed _ _ |
Apply_operation_result.Backtracked _ _)
⇒ None
| Apply_operation_result.Applied o_value ⇒
let o_value :=
cast
successful_manager_operation_result
o_value in
match
select
(Successful_manager_result
o_value)
with
| None ⇒ None
| Some o_value ⇒
Some (tt, (proj o_value))
end
end)
(fun (function_parameter : unit × A) ⇒
let '(_, x_value) := function_parameter in
Apply_operation_result.Applied (inj x_value));
Data_encoding.case_value "Failed" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "status"
(Data_encoding.constant "failed"))
(Data_encoding.req None None "errors"
Apply_operation_result.trace_encoding))
(fun (function_parameter :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match function_parameter with
| Apply_operation_result.Failed _ errs ⇒
Some (tt, errs)
| _ ⇒ None
end)
(fun (function_parameter :
unit × Error_monad.trace Error_monad._error) ⇒
let '(_, errs) := function_parameter in
Apply_operation_result.Failed kind_value errs);
Data_encoding.case_value "Skipped" None (Data_encoding.Tag 2)
(Data_encoding.obj1
(Data_encoding.req None None "status"
(Data_encoding.constant "skipped")))
(fun (function_parameter :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match function_parameter with
| Apply_operation_result.Skipped _ ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Apply_operation_result.Skipped kind_value);
Data_encoding.case_value "Backtracked" None (Data_encoding.Tag 3)
(Data_encoding.merge_objs
(Data_encoding.obj2
(Data_encoding.req None None "status"
(Data_encoding.constant
"backtracked"))
(Data_encoding.opt None None "errors"
Apply_operation_result.trace_encoding))
encoding)
(fun (o_value :
Apply_operation_result.operation_result
Alpha_context.Kind.manager
successful_manager_operation_result)
⇒
match o_value with
|
(Apply_operation_result.Skipped _ |
Apply_operation_result.Failed _ _ |
Apply_operation_result.Applied _) ⇒
None
|
Apply_operation_result.Backtracked
o_value errs ⇒
let '[errs, o_value] :=
cast
[option
(Error_monad.trace
Error_monad._error)
**
successful_manager_operation_result]
[errs, o_value] in
match
select
(Successful_manager_result
o_value)
with
| None ⇒ None
| Some o_value ⇒
Some
((tt, errs),
(proj
o_value))
end
end)
(fun (function_parameter :
(unit ×
option
(Error_monad.trace
Error_monad._error))
× A) ⇒
let '((_, errs), x_value) := function_parameter
in
Apply_operation_result.Backtracked (inj x_value)
errs)
]) in
MCase
{| case.MCase.op_case := op_case; case.MCase.encoding := encoding;
case.MCase.kind := kind_value; case.MCase.select := select;
case.MCase.proj := proj; case.MCase.inj := inj; case.MCase.t := t_value;
|}.
Definition reveal_case : case Alpha_context.Kind.reveal :=
make Alpha_context.Operation.Encoding.Manager_operations.reveal_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Reveal_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Reveal_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Reveal_result {|
successful_manager_operation_result.Reveal_result.consumed_gas := consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Reveal_result
{|
successful_manager_operation_result.Reveal_result.consumed_gas :=
consumed_gas; |}).
Definition transaction_contract_variant_cases
: Data_encoding.encoding
Apply_internal_results.successful_transaction_result :=
Data_encoding.union None
[
Data_encoding.case_value "To_contract" None (Data_encoding.Tag 0)
(Data_encoding.obj9
(Data_encoding.opt None None "storage"
Alpha_context.Script.expr_encoding)
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "ticket_updates"
Ticket_receipt.encoding nil)
(Data_encoding.dft None None "originated_contracts"
(Data_encoding.list_value None
Alpha_context.Contract.originated_encoding) nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size"
Data_encoding.z_value Z.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero)
(Data_encoding.dft None None
"allocated_destination_contract"
Data_encoding.bool_value false)
(Data_encoding.opt None None "lazy_storage_diff"
Alpha_context.Lazy_storage.encoding))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_contract_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
:= storage_value;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:=
lazy_storage_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:=
balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
:=
ticket_receipt;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:=
originated_contracts;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:=
consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:=
storage_size;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:=
paid_storage_size_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:=
allocated_destination_contract
|} ⇒
Some
(storage_value, balance_updates, ticket_receipt,
originated_contracts, consumed_gas,
storage_size, paid_storage_size_diff,
allocated_destination_contract,
lazy_storage_diff)
| _ ⇒ None
end)
(fun (function_parameter :
option Alpha_context.Script.expr ×
Alpha_context.Receipt.balance_updates ×
Ticket_receipt.t × list Contract_hash.t ×
Alpha_context.Gas.Arith.fp × Z.t × Z.t × bool ×
option Alpha_context.Lazy_storage.diffs) ⇒
let
'(storage_value, balance_updates, ticket_receipt,
originated_contracts, consumed_gas,
storage_size, paid_storage_size_diff,
allocated_destination_contract,
lazy_storage_diff) := function_parameter in
Apply_internal_results.Transaction_to_contract_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage
:= storage_value;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.ticket_receipt
:= ticket_receipt;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.storage_size
:= storage_size;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.paid_storage_size_diff
:= paid_storage_size_diff;
Apply_internal_results.successful_transaction_result.Transaction_to_contract_result.allocated_destination_contract
:= allocated_destination_contract; |});
Data_encoding.case_value "To_tx_rollup" None (Data_encoding.Tag 1)
(Data_encoding.obj4
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "ticket_hash"
Alpha_context.Ticket_hash.encoding)
(Data_encoding.req None None "paid_storage_size_diff"
Data_encoding.n_value))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_tx_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:=
balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:=
consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:=
paid_storage_size_diff
|} ⇒
Some
(balance_updates, consumed_gas, ticket_hash,
paid_storage_size_diff)
| _ ⇒ None
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Gas.Arith.fp ×
Alpha_context.Ticket_hash.t × Z.t) ⇒
let
'(balance_updates, consumed_gas, ticket_hash,
paid_storage_size_diff) := function_parameter in
Apply_internal_results.Transaction_to_tx_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.ticket_hash
:= ticket_hash;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_tx_rollup_result.paid_storage_size_diff
:= paid_storage_size_diff; |});
Data_encoding.case_value "To_sc_rollup" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding
Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_after"
Alpha_context.Sc_rollup.Inbox.encoding))
(fun (function_parameter :
Apply_internal_results.successful_transaction_result) ⇒
match function_parameter with
|
Apply_internal_results.Transaction_to_sc_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
:=
inbox_after
|} ⇒ Some (consumed_gas, inbox_after)
| _ ⇒ None
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t)
⇒
let '(consumed_gas, inbox_after) := function_parameter in
Apply_internal_results.Transaction_to_sc_rollup_result
{|
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_transaction_result.Transaction_to_sc_rollup_result.inbox_after
:= inbox_after; |})
].
Definition transaction_case : case Alpha_context.Kind.transaction :=
make Alpha_context.Operation.Encoding.Manager_operations.transaction_case
transaction_contract_variant_cases
Alpha_context.Kind.Transaction_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Transaction_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
| Transaction_result x_value ⇒ x_value
| _ ⇒ unreachable_gadt_branch
end)
(fun (x_value : Apply_internal_results.successful_transaction_result) ⇒
Transaction_result x_value).
Definition origination_case : case Alpha_context.Kind.origination :=
make Alpha_context.Operation.Encoding.Manager_operations.origination_case
(Data_encoding.obj6
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "originated_contracts"
(Data_encoding.list_value None
Alpha_context.Contract.originated_encoding) nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero)
(Data_encoding.opt None None "lazy_storage_diff"
Alpha_context.Lazy_storage.encoding))
Alpha_context.Kind.Origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Origination_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Origination_result {|
Apply_internal_results.successful_origination_result.lazy_storage_diff :=
lazy_storage_diff;
Apply_internal_results.successful_origination_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas
:= consumed_gas;
Apply_internal_results.successful_origination_result.storage_size
:= storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒
(balance_updates, originated_contracts, consumed_gas, storage_size,
paid_storage_size_diff, lazy_storage_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × list Contract_hash.t ×
Alpha_context.Gas.Arith.fp × Z.t × Z.t ×
option Alpha_context.Lazy_storage.diffs) ⇒
let
'(balance_updates, originated_contracts, consumed_gas, storage_size,
paid_storage_size_diff, lazy_storage_diff) := function_parameter in
Origination_result
{|
Apply_internal_results.successful_origination_result.lazy_storage_diff
:= lazy_storage_diff;
Apply_internal_results.successful_origination_result.balance_updates
:= balance_updates;
Apply_internal_results.successful_origination_result.originated_contracts
:= originated_contracts;
Apply_internal_results.successful_origination_result.consumed_gas :=
consumed_gas;
Apply_internal_results.successful_origination_result.storage_size :=
storage_size;
Apply_internal_results.successful_origination_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition register_global_constant_case
: case Alpha_context.Kind.register_global_constant :=
make
Alpha_context.Operation.Encoding.Manager_operations.register_global_constant_case
(Data_encoding.obj4
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "storage_size" Data_encoding.z_value Z.zero)
(Data_encoding.req None None "global_address" Script_expr_hash.encoding))
Alpha_context.Kind.Register_global_constant_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Register_global_constant_result _) as op)
⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Register_global_constant_result {|
successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Register_global_constant_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Register_global_constant_result.size_of_constant
:= size_of_constant;
successful_manager_operation_result.Register_global_constant_result.global_address
:= global_address
|} ⇒
(balance_updates, consumed_gas, size_of_constant, global_address)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t
× Script_expr_hash.t) ⇒
let
'(balance_updates, consumed_gas, size_of_constant, global_address) :=
function_parameter in
Register_global_constant_result
{|
successful_manager_operation_result.Register_global_constant_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Register_global_constant_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Register_global_constant_result.size_of_constant
:= size_of_constant;
successful_manager_operation_result.Register_global_constant_result.global_address
:= global_address; |}).
Definition delegation_case : case Alpha_context.Kind.delegation :=
make Alpha_context.Operation.Encoding.Manager_operations.delegation_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Delegation_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Delegation_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Delegation_result {|
successful_manager_operation_result.Delegation_result.consumed_gas :=
consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Delegation_result
{|
successful_manager_operation_result.Delegation_result.consumed_gas
:= consumed_gas; |}).
Definition update_consensus_key_case
: case Alpha_context.Kind.update_consensus_key :=
make
Alpha_context.Operation.Encoding.Manager_operations.update_consensus_key_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Update_consensus_key_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Update_consensus_key_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Update_consensus_key_result {|
successful_manager_operation_result.Update_consensus_key_result.consumed_gas
:= consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Update_consensus_key_result
{|
successful_manager_operation_result.Update_consensus_key_result.consumed_gas
:= consumed_gas; |}).
Definition set_deposits_limit_case
: case Alpha_context.Kind.set_deposits_limit :=
make
Alpha_context.Operation.Encoding.Manager_operations.set_deposits_limit_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Set_deposits_limit_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Set_deposits_limit_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Set_deposits_limit_result {|
successful_manager_operation_result.Set_deposits_limit_result.consumed_gas :=
consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Set_deposits_limit_result
{|
successful_manager_operation_result.Set_deposits_limit_result.consumed_gas
:= consumed_gas; |}).
Definition increase_paid_storage_case
: case Alpha_context.Kind.increase_paid_storage :=
make
Alpha_context.Operation.Encoding.Manager_operations.increase_paid_storage_case
(Data_encoding.obj2
(Data_encoding.dft None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding nil)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Increase_paid_storage_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Increase_paid_storage_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Increase_paid_storage_result {|
successful_manager_operation_result.Increase_paid_storage_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Increase_paid_storage_result
{|
successful_manager_operation_result.Increase_paid_storage_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Increase_paid_storage_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_origination_case
: case Alpha_context.Kind.tx_rollup_origination :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_origination_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "originated_rollup"
Alpha_context.Tx_rollup.encoding))
Alpha_context.Kind.Tx_rollup_origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_origination_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_origination_result {|
successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
:= originated_tx_rollup
|} ⇒ (balance_updates, consumed_gas, originated_tx_rollup)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup.t) ⇒
let '(balance_updates, consumed_gas, originated_tx_rollup) :=
function_parameter in
Tx_rollup_origination_result
{|
successful_manager_operation_result.Tx_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_origination_result.originated_tx_rollup
:= originated_tx_rollup; |}).
Definition tx_rollup_submit_batch_case
: case Alpha_context.Kind.tx_rollup_submit_batch :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_submit_batch_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "paid_storage_size_diff"
Data_encoding.n_value))
Alpha_context.Kind.Tx_rollup_submit_batch_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_submit_batch_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_submit_batch_result {|
successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Tx_rollup_submit_batch_result
{|
successful_manager_operation_result.Tx_rollup_submit_batch_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_submit_batch_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_submit_batch_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition tx_rollup_commit_case : case Alpha_context.Kind.tx_rollup_commit :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_commit_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_commit_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_commit_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_commit_result {|
successful_manager_operation_result.Tx_rollup_commit_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_commit_result
{|
successful_manager_operation_result.Tx_rollup_commit_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_commit_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_return_bond_case
: case Alpha_context.Kind.tx_rollup_return_bond :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_return_bond_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_return_bond_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_return_bond_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_return_bond_result {|
successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_return_bond_result
{|
successful_manager_operation_result.Tx_rollup_return_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_return_bond_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_finalize_commitment_case
: case Alpha_context.Kind.tx_rollup_finalize_commitment :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_finalize_commitment_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "level"
Alpha_context.Tx_rollup_level.encoding))
Alpha_context.Kind.Tx_rollup_finalize_commitment_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_finalize_commitment_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_finalize_commitment_result {|
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
:= level
|} ⇒ (balance_updates, consumed_gas, level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup_level.t) ⇒
let '(balance_updates, consumed_gas, level) := function_parameter in
Tx_rollup_finalize_commitment_result
{|
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_finalize_commitment_result.level
:= level; |}).
Definition tx_rollup_remove_commitment_case
: case Alpha_context.Kind.tx_rollup_remove_commitment :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_remove_commitment_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "level"
Alpha_context.Tx_rollup_level.encoding))
Alpha_context.Kind.Tx_rollup_remove_commitment_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_remove_commitment_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_remove_commitment_result {|
successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
:= level
|} ⇒ (balance_updates, consumed_gas, level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp ×
Alpha_context.Tx_rollup_level.t) ⇒
let '(balance_updates, consumed_gas, level) := function_parameter in
Tx_rollup_remove_commitment_result
{|
successful_manager_operation_result.Tx_rollup_remove_commitment_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_remove_commitment_result.level
:= level; |}).
Definition tx_rollup_rejection_case
: case Alpha_context.Kind.tx_rollup_rejection :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_rejection_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Tx_rollup_rejection_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Tx_rollup_rejection_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_rejection_result {|
successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Tx_rollup_rejection_result
{|
successful_manager_operation_result.Tx_rollup_rejection_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_rejection_result.consumed_gas
:= consumed_gas; |}).
Definition tx_rollup_dispatch_tickets_case
: case Alpha_context.Kind.tx_rollup_dispatch_tickets :=
make
Alpha_context.Operation.Encoding.Manager_operations.tx_rollup_dispatch_tickets_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Tx_rollup_dispatch_tickets_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Tx_rollup_dispatch_tickets_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Tx_rollup_dispatch_tickets_result {|
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Tx_rollup_dispatch_tickets_result
{|
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Tx_rollup_dispatch_tickets_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition transfer_ticket_case : case Alpha_context.Kind.transfer_ticket :=
make
Alpha_context.Operation.Encoding.Manager_operations.transfer_ticket_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Transfer_ticket_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Transfer_ticket_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Transfer_ticket_result {|
successful_manager_operation_result.Transfer_ticket_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Transfer_ticket_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Transfer_ticket_result
{|
successful_manager_operation_result.Transfer_ticket_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Transfer_ticket_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Transfer_ticket_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition dal_publish_slot_header_case
: case Alpha_context.Kind.dal_publish_slot_header :=
make
Alpha_context.Operation.Encoding.Manager_operations.dal_publish_slot_header_case
(Data_encoding.obj1
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Dal_publish_slot_header_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Dal_publish_slot_header_result _) as op)
⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Dal_publish_slot_header_result {|
successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
:= consumed_gas
|} ⇒ consumed_gas
| _ ⇒ unreachable_gadt_branch
end)
(fun (consumed_gas : Alpha_context.Gas.Arith.fp) ⇒
Dal_publish_slot_header_result
{|
successful_manager_operation_result.Dal_publish_slot_header_result.consumed_gas
:= consumed_gas; |}).
Definition zk_rollup_origination_case
: case Alpha_context.Kind.zk_rollup_origination :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_origination_case
(Data_encoding.obj4
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.req None None "originated_zk_rollup"
Alpha_context.Zk_rollup.Address.encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Zk_rollup_origination_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_origination_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_origination_result {|
successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size
|} ⇒
(balance_updates, originated_zk_rollup, consumed_gas, storage_size)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Zk_rollup.Address.t × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let
'(balance_updates, originated_zk_rollup, consumed_gas, storage_size) :=
function_parameter in
Zk_rollup_origination_result
{|
successful_manager_operation_result.Zk_rollup_origination_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_origination_result.originated_zk_rollup
:= originated_zk_rollup;
successful_manager_operation_result.Zk_rollup_origination_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_origination_result.storage_size
:= storage_size; |}).
Definition zk_rollup_publish_case
: case Alpha_context.Kind.zk_rollup_publish :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_publish_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Zk_rollup_publish_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_publish_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_publish_result {|
successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Zk_rollup_publish_result
{|
successful_manager_operation_result.Zk_rollup_publish_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_publish_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition zk_rollup_update_case : case Alpha_context.Kind.zk_rollup_update :=
make
Alpha_context.Operation.Encoding.Manager_operations.zk_rollup_update_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Zk_rollup_update_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Zk_rollup_update_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Zk_rollup_update_result {|
successful_manager_operation_result.Zk_rollup_update_result.balance_updates :=
balance_updates;
successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Zk_rollup_update_result
{|
successful_manager_operation_result.Zk_rollup_update_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Zk_rollup_update_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Zk_rollup_update_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition sc_rollup_originate_case
: case Alpha_context.Kind.sc_rollup_originate :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_originate_case
(Data_encoding.obj5
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.req None None "address"
Alpha_context.Sc_rollup.Address.encoding)
(Data_encoding.req None None "genesis_commitment_hash"
Alpha_context.Sc_rollup.Commitment.Hash.encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "size" Data_encoding.z_value))
Alpha_context.Kind.Sc_rollup_originate_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_originate_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_originate_result {|
successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_originate_result.address
:= address;
successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
:= genesis_commitment_hash;
successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_originate_result.size
:= size_value
|} ⇒
(balance_updates, address, genesis_commitment_hash, consumed_gas,
size_value)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates ×
Alpha_context.Sc_rollup.Address.t ×
Alpha_context.Sc_rollup.Commitment.Hash.t × Alpha_context.Gas.Arith.fp
× Z.t) ⇒
let
'(balance_updates, address, genesis_commitment_hash, consumed_gas,
size_value) := function_parameter in
Sc_rollup_originate_result
{|
successful_manager_operation_result.Sc_rollup_originate_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_originate_result.address
:= address;
successful_manager_operation_result.Sc_rollup_originate_result.genesis_commitment_hash
:= genesis_commitment_hash;
successful_manager_operation_result.Sc_rollup_originate_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_originate_result.size
:= size_value; |}).
Definition sc_rollup_add_messages_case
: case Alpha_context.Kind.sc_rollup_add_messages :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_add_messages_case
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_after"
Alpha_context.Sc_rollup.Inbox.encoding))
Alpha_context.Kind.Sc_rollup_add_messages_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_add_messages_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_add_messages_result {|
successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
:= inbox_after
|} ⇒ (consumed_gas, inbox_after)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Inbox.t) ⇒
let '(consumed_gas, inbox_after) := function_parameter in
Sc_rollup_add_messages_result
{|
successful_manager_operation_result.Sc_rollup_add_messages_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_add_messages_result.inbox_after
:= inbox_after; |}).
Definition sc_rollup_cement_case : case Alpha_context.Kind.sc_rollup_cement :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_cement_case
(Data_encoding.obj2
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "inbox_level"
Alpha_context.Raw_level.encoding))
Alpha_context.Kind.Sc_rollup_cement_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_cement_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_cement_result {|
successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
:= inbox_level
|} ⇒ (consumed_gas, inbox_level)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Raw_level.t) ⇒
let '(consumed_gas, inbox_level) := function_parameter in
Sc_rollup_cement_result
{|
successful_manager_operation_result.Sc_rollup_cement_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_cement_result.inbox_level
:= inbox_level; |}).
Definition sc_rollup_publish_case
: case Alpha_context.Kind.sc_rollup_publish :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_publish_case
(Data_encoding.obj4
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "staked_hash"
Alpha_context.Sc_rollup.Commitment.Hash.encoding)
(Data_encoding.req None None "published_at_level"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_publish_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_publish_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_publish_result {|
successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
:= staked_hash;
successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
:= published_at_level;
successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
:= balance_updates
|} ⇒
(consumed_gas, staked_hash, published_at_level, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Commitment.Hash.t ×
Alpha_context.Raw_level.t × Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, staked_hash, published_at_level, balance_updates) :=
function_parameter in
Sc_rollup_publish_result
{|
successful_manager_operation_result.Sc_rollup_publish_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_publish_result.staked_hash
:= staked_hash;
successful_manager_operation_result.Sc_rollup_publish_result.published_at_level
:= published_at_level;
successful_manager_operation_result.Sc_rollup_publish_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_refute_case : case Alpha_context.Kind.sc_rollup_refute :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_refute_case
(Data_encoding.obj3
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "game_status"
Alpha_context.Sc_rollup.Game.status_encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_refute_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_refute_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_refute_result {|
successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_refute_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
:= balance_updates
|} ⇒ (consumed_gas, game_status, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, game_status, balance_updates) := function_parameter
in
Sc_rollup_refute_result
{|
successful_manager_operation_result.Sc_rollup_refute_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_refute_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_refute_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_timeout_case
: case Alpha_context.Kind.sc_rollup_timeout :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_timeout_case
(Data_encoding.obj3
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.req None None "game_status"
Alpha_context.Sc_rollup.Game.status_encoding)
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding))
Alpha_context.Kind.Sc_rollup_timeout_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_timeout_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_timeout_result {|
successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas :=
consumed_gas;
successful_manager_operation_result.Sc_rollup_timeout_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
:= balance_updates
|} ⇒ (consumed_gas, game_status, balance_updates)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Gas.Arith.fp × Alpha_context.Sc_rollup.Game.status ×
Alpha_context.Receipt.balance_updates) ⇒
let '(consumed_gas, game_status, balance_updates) := function_parameter
in
Sc_rollup_timeout_result
{|
successful_manager_operation_result.Sc_rollup_timeout_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_timeout_result.game_status
:= game_status;
successful_manager_operation_result.Sc_rollup_timeout_result.balance_updates
:= balance_updates; |}).
Definition sc_rollup_execute_outbox_message_case
: case Alpha_context.Kind.sc_rollup_execute_outbox_message :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_execute_outbox_message_case
(Data_encoding.obj3
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero)
(Data_encoding.dft None None "paid_storage_size_diff"
Data_encoding.z_value Z.zero))
Alpha_context.Kind.Sc_rollup_execute_outbox_message_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
|
Successful_manager_result
((Sc_rollup_execute_outbox_message_result _) as op) ⇒ Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_execute_outbox_message_result {|
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
:= paid_storage_size_diff
|} ⇒ (balance_updates, consumed_gas, paid_storage_size_diff)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp × Z.t)
⇒
let '(balance_updates, consumed_gas, paid_storage_size_diff) :=
function_parameter in
Sc_rollup_execute_outbox_message_result
{|
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.consumed_gas
:= consumed_gas;
successful_manager_operation_result.Sc_rollup_execute_outbox_message_result.paid_storage_size_diff
:= paid_storage_size_diff; |}).
Definition sc_rollup_recover_bond_case
: case Alpha_context.Kind.sc_rollup_recover_bond :=
make
Alpha_context.Operation.Encoding.Manager_operations.sc_rollup_recover_bond_case
(Data_encoding.obj2
(Data_encoding.req None None "balance_updates"
Alpha_context.Receipt.balance_updates_encoding)
(Data_encoding.dft None None "consumed_milligas"
Alpha_context.Gas.Arith.n_fp_encoding Alpha_context.Gas.Arith.zero))
Alpha_context.Kind.Sc_rollup_recover_bond_manager_kind
(fun (function_parameter : packed_successful_manager_operation_result) ⇒
match function_parameter with
| Successful_manager_result ((Sc_rollup_recover_bond_result _) as op) ⇒
Some op
| _ ⇒ None
end)
(fun (function_parameter : successful_manager_operation_result) ⇒
match function_parameter with
|
Sc_rollup_recover_bond_result {|
successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
:= consumed_gas
|} ⇒ (balance_updates, consumed_gas)
| _ ⇒ unreachable_gadt_branch
end)
(fun (function_parameter :
Alpha_context.Receipt.balance_updates × Alpha_context.Gas.Arith.fp) ⇒
let '(balance_updates, consumed_gas) := function_parameter in
Sc_rollup_recover_bond_result
{|
successful_manager_operation_result.Sc_rollup_recover_bond_result.balance_updates
:= balance_updates;
successful_manager_operation_result.Sc_rollup_recover_bond_result.consumed_gas
:= consumed_gas; |}).
End Manager_result.
Definition successful_manager_operation_result_encoding
: Data_encoding.t packed_successful_manager_operation_result :=
let make {kind : Set} (mcase : Manager_result.case kind)
: Data_encoding.case packed_successful_manager_operation_result :=
let 'Manager_result.MCase res_case := mcase in
let 'existT _ __MCase_'a res_case :=
existT (A := Set) (fun __MCase_'a ⇒ Manager_result.case.MCase __MCase_'a)
_ res_case in
let 'Alpha_context.Operation.Encoding.Manager_operations.MCase op_case :=
res_case.(Manager_result.case.MCase.op_case) in
Data_encoding.case_value
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name)
None
(Data_encoding.Tag
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.tag))
(Data_encoding.merge_objs
(Data_encoding.obj1
(Data_encoding.req None None "kind"
(Data_encoding.constant
op_case.(Alpha_context.Operation.Encoding.Manager_operations.case.MCase.name))))
res_case.(Manager_result.case.MCase.encoding))
(fun (res : packed_successful_manager_operation_result) ⇒
match res_case.(Manager_result.case.MCase.select) res with
| Some res ⇒ Some (tt, (res_case.(Manager_result.case.MCase.proj) res))
| None ⇒ None
end)
(fun (function_parameter : unit × __MCase_'a) ⇒
let '(_, res) := function_parameter in
Successful_manager_result (res_case.(Manager_result.case.MCase.inj) res))
in
Data_encoding.def "operation.alpha.successful_manager_operation_result" None
None
(Data_encoding.union None
[
make Manager_result.reveal_case;
make Manager_result.transaction_case;
make Manager_result.origination_case;
make Manager_result.delegation_case;
make Manager_result.update_consensus_key_case;
make Manager_result.set_deposits_limit_case;
make Manager_result.increase_paid_storage_case;
make Manager_result.sc_rollup_originate_case
]).
Records for the constructor parameters
Module ConstructorRecords_contents_result.
Module contents_result.
Module Preendorsement_result.
Record record {balance_updates delegate consensus_key preendorsement_power
: Set} : Set := Build {
balance_updates : balance_updates;
delegate : delegate;
consensus_key : consensus_key;
preendorsement_power : preendorsement_power;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
balance_updates
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power balance_updates r.(delegate) r.(consensus_key)
r.(preendorsement_power).
Definition with_delegate
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
delegate
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) delegate r.(consensus_key)
r.(preendorsement_power).
Definition with_consensus_key
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
consensus_key
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) r.(delegate) consensus_key
r.(preendorsement_power).
Definition with_preendorsement_power
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
preendorsement_power
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) r.(delegate)
r.(consensus_key) preendorsement_power.
End Preendorsement_result.
Definition Preendorsement_result_skeleton := Preendorsement_result.record.
Module Endorsement_result.
Record record {balance_updates delegate consensus_key endorsement_power :
Set} : Set := Build {
balance_updates : balance_updates;
delegate : delegate;
consensus_key : consensus_key;
endorsement_power : endorsement_power;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_delegate t_consensus_key t_endorsement_power}
balance_updates
(r :
record t_balance_updates t_delegate t_consensus_key
t_endorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key t_endorsement_power
balance_updates r.(delegate) r.(consensus_key) r.(endorsement_power).
Definition with_delegate
{t_balance_updates t_delegate t_consensus_key t_endorsement_power}
delegate
(r :
record t_balance_updates
Module contents_result.
Module Preendorsement_result.
Record record {balance_updates delegate consensus_key preendorsement_power
: Set} : Set := Build {
balance_updates : balance_updates;
delegate : delegate;
consensus_key : consensus_key;
preendorsement_power : preendorsement_power;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
balance_updates
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power balance_updates r.(delegate) r.(consensus_key)
r.(preendorsement_power).
Definition with_delegate
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
delegate
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) delegate r.(consensus_key)
r.(preendorsement_power).
Definition with_consensus_key
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
consensus_key
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) r.(delegate) consensus_key
r.(preendorsement_power).
Definition with_preendorsement_power
{t_balance_updates t_delegate t_consensus_key t_preendorsement_power}
preendorsement_power
(r :
record t_balance_updates t_delegate t_consensus_key
t_preendorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key
t_preendorsement_power r.(balance_updates) r.(delegate)
r.(consensus_key) preendorsement_power.
End Preendorsement_result.
Definition Preendorsement_result_skeleton := Preendorsement_result.record.
Module Endorsement_result.
Record record {balance_updates delegate consensus_key endorsement_power :
Set} : Set := Build {
balance_updates : balance_updates;
delegate : delegate;
consensus_key : consensus_key;
endorsement_power : endorsement_power;
}.
Arguments record : clear implicits.
Definition with_balance_updates
{t_balance_updates t_delegate t_consensus_key t_endorsement_power}
balance_updates
(r :
record t_balance_updates t_delegate t_consensus_key
t_endorsement_power) :=
Build t_balance_updates t_delegate t_consensus_key t_endorsement_power
balance_updates r.(delegate) r.(consensus_key) r.(endorsement_power).
Definition with_delegate
{t_balance_updates t_delegate t_consensus_key t_endorsement_power}
delegate
(r :
record t_balance_updates