🌌 Alpha_context.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_repr.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_storage.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Dal_endorsement_repr.
Require TezosOfOCaml.Proto_alpha.Dal_errors_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_cycles.
Require TezosOfOCaml.Proto_alpha.Delegate_missed_endorsements_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_sampler.
Require TezosOfOCaml.Proto_alpha.Delegate_slashed_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.
Require TezosOfOCaml.Proto_alpha.Init_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_storage.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Sapling_validator.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_arith.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_refutation_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_builder.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.
Definition t : Set := Raw_context.t.
Definition context : Set := t.
Module BASIC_DATA.
Record signature {t : Set} : Set := {
t := t;
op_eq : t → t → bool;
op_ltgt : t → t → bool;
op_lt : t → t → bool;
op_lteq : t → t → bool;
op_gteq : t → t → bool;
op_gt : t → t → bool;
compare : t → t → int;
equal : t → t → bool;
max : t → t → t;
min : t → t → t;
encoding : Data_encoding.t t;
pp : Format.formatter → t → unit;
}.
End BASIC_DATA.
Definition BASIC_DATA := @BASIC_DATA.signature.
Arguments BASIC_DATA {_}.
Module Tez := Tez_repr.
Module Period := Period_repr.
Module Timestamp.
Include Time_repr.
Definition current : Raw_context.t → Time.t := Raw_context.current_timestamp.
Definition predecessor : Raw_context.t → Time.t :=
Raw_context.predecessor_timestamp.
End Timestamp.
Module Slot := Slot_repr.
Module Sc_rollup_repr := Sc_rollup_repr.
Module Sc_rollup.
Module Tick := Sc_rollup_tick_repr.
Include Sc_rollup_repr.
Include Sc_rollup_PVM_sig.
Module ArithPVM := Sc_rollup_arith.
Module Wasm_2_0_0PVM := Sc_rollup_wasm.V2_0_0.
Module Inbox_message := Sc_rollup_inbox_message_repr.
Module Inbox.
Include Sc_rollup_inbox_repr.
Include Sc_rollup_inbox_storage.
End Inbox.
Module Proof := Sc_rollup_proof_repr.
Module Game := Sc_rollup_game_repr.
Module Commitment.
Include Sc_rollup_commitment_repr.
Include Sc_rollup_commitment_storage.
End Commitment.
Module Stake_storage.
Include Sc_rollup_stake_storage.
End Stake_storage.
Module Refutation_storage := Sc_rollup_refutation_storage.
Include Sc_rollup_storage.
Include Sc_rollups.
Module Outbox.
Include Sc_rollup_outbox_storage.
Module Message := Sc_rollup_outbox_message_repr.
End Outbox.
Module Errors := Sc_rollup_errors.
End Sc_rollup.
Module Dal.
Module Slot_index.
Include Dal_slot_repr.Index.
End Slot_index.
Module Endorsement.
Include Dal_endorsement_repr.
Include Raw_context.Dal.
End Endorsement.
Module Page.
Include Dal_slot_repr.Page.
End Page.
Module Slot.
Include Dal_slot_repr.
Include Dal_slot_storage.
Include Raw_context.Dal.
End Slot.
Module Slots_history := Dal_slot_repr.Slots_history.
Module Slots_storage := Dal_slot_storage.
End Dal.
Module Dal_errors := Dal_errors_repr.
Module Zk_rollup.
Include Zk_rollup_repr.
Module State := Zk_rollup_state_repr.
Module Account := Zk_rollup_account_repr.
Module Operation := Zk_rollup_operation_repr.
Module Ticket := Zk_rollup_ticket_repr.
Module Errors := Zk_rollup_errors.
Include Zk_rollup_storage.
End Zk_rollup.
Module Entrypoint := Entrypoint_repr.
Include Operation_repr.
Module Operation.
Definition t : Set := operation.
Definition packed : Set := packed_operation.
Definition unsigned_encoding
: Data_encoding.t (Operation.shell_header × packed_contents_list) :=
unsigned_operation_encoding.
Include Operation_repr.
End Operation.
Module Block_header := Block_header_repr.
Module Vote.
Include Vote_repr.
Include Vote_storage.
End Vote.
Module Block_payload.
Include Block_payload_repr.
End Block_payload.
Module First_level_of_protocol.
Definition get : Raw_context.t → M? Raw_level_repr.t :=
Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.get).
End First_level_of_protocol.
Module Ratio := Ratio_repr.
Module Raw_level := Raw_level_repr.
Module Cycle := Cycle_repr.
Module Fees := Fees_storage.
Definition public_key : Set := Signature.public_key.
Definition public_key_hash : Set := Signature.public_key_hash.
Definition signature : Set := Signature.t.
Module Constants.
Include Constants_repr.
Include Constants_storage.
Module Parametric := Constants_parametric_repr.
Definition round_durations (ctxt : Raw_context.t) : Round_repr.Durations.t :=
Raw_context.round_durations ctxt.
Definition all (ctxt : Raw_context.t) : t :=
all_of_parametric (parametric_value ctxt).
End Constants.
Module Voting_period.
Include Voting_period_repr.
Include Voting_period_storage.
End Voting_period.
Module Round.
Include Round_repr.
Definition round_durations : Set := Durations.t.
Definition pp_round_durations : Format.formatter → Durations.t → unit :=
Durations.pp.
Definition round_durations_encoding : Data_encoding.encoding Durations.t :=
Durations.encoding.
Definition round_duration
: Round_repr.Durations.t → Round_repr.round → Period_repr.t :=
Round_repr.Durations.round_duration.
Definition update (ctxt : Raw_context.t) (round : Round_repr.round)
: M? Raw_context.t :=
Storage.Block_round.(Storage.Simple_single_data_storage.update) ctxt round.
Definition get (ctxt : Raw_context.t) : M? Round_repr.round :=
Storage.Block_round.(Storage.Simple_single_data_storage.get) ctxt.
End Round.
Module Gas.
Include Gas_limit_repr.
Definition set_limit
: Raw_context.t → Gas_limit_repr.Arith.t → Raw_context.t :=
Raw_context.set_gas_limit.
Definition consume_limit_in_block
: Raw_context.t → Gas_limit_repr.Arith.t → M? Raw_context.t :=
Raw_context.consume_gas_limit_in_block.
Definition set_unlimited : Raw_context.t → Raw_context.t :=
Raw_context.set_gas_unlimited.
Definition consume
: Raw_context.t → Gas_limit_repr.cost → M? Raw_context.t :=
Raw_context.consume_gas.
Definition consume_from (available_gas : Arith.fp) (cost : cost)
: M? Arith.fp :=
match raw_consume available_gas cost with
| Some remaining_gas ⇒ return? remaining_gas
| None ⇒
Error_monad.error_value
(Build_extensible "Operation_quota_exceeded" unit tt)
end.
Definition remaining_operation_gas
: Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.remaining_operation_gas.
Definition update_remaining_operation_gas
: Raw_context.t → Gas_limit_repr.Arith.fp → Raw_context.t :=
Raw_context.update_remaining_operation_gas.
Definition reset_block_gas (ctxt : Raw_context.t) : Raw_context.t :=
let gas := Arith.fp_value (Constants.hard_gas_limit_per_block ctxt) in
Raw_context.update_remaining_block_gas ctxt gas.
Definition level : Raw_context.t → Gas_limit_repr.t := Raw_context.gas_level.
Definition consumed
: Raw_context.t → Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.gas_consumed.
Definition block_level : Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.block_gas_level.
Definition cost_of_repr {A : Set} (cost : A) : A := cost.
End Gas.
Module Script.
Include Michelson_v1_primitives.
Include Script_repr.
Inductive consume_deserialization_gas : Set :=
| Always : consume_deserialization_gas
| When_needed : consume_deserialization_gas.
Definition force_decode_in_context
(consume_deserialization_gas : consume_deserialization_gas)
(ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
: M? (Script_repr.expr × Raw_context.t) :=
let gas_cost :=
match consume_deserialization_gas with
| Always ⇒ Script_repr.stable_force_decode_cost lexpr
| When_needed ⇒ Script_repr.force_decode_cost lexpr
end in
let? ctxt := Raw_context.consume_gas ctxt gas_cost in
let? v_value := Script_repr.force_decode lexpr in
return? (v_value, ctxt).
Definition force_bytes_in_context
(ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
: M? (bytes × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt (Script_repr.force_bytes_cost lexpr) in
let? v_value := Script_repr.force_bytes lexpr in
return? (v_value, ctxt).
Definition consume_decoding_gas
(available_gas : Gas.Arith.fp) (lexpr : Script_repr.lazy_expr)
: M? Gas.Arith.fp :=
let gas_cost := Script_repr.stable_force_decode_cost lexpr in
Gas.consume_from available_gas gas_cost.
End Script.
Module Level.
Include Level_repr.
Include Level_storage.
End Level.
Module Lazy_storage.
Module Kind := Lazy_storage_kind.
Module IdSet := Kind.IdSet.
Include Lazy_storage_diff.
End Lazy_storage.
Module Origination_nonce.
Definition init_value : Raw_context.t → Operation_hash.t → Raw_context.t :=
Raw_context.init_origination_nonce.
Definition unset : Raw_context.t → Raw_context.t :=
Raw_context.unset_origination_nonce.
End Origination_nonce.
Module Destination := Destination_repr.
Module Contract.
Include Contract_repr.
Include Contract_storage.
Definition is_manager_key_revealed
: Raw_context.t → Signature.public_key_hash → M? bool :=
Contract_manager_storage.is_manager_key_revealed.
Definition check_public_key
: Signature.public_key → Signature.public_key_hash → M? unit :=
Contract_manager_storage.check_public_key.
Definition reveal_manager_key
: option bool → Raw_context.t → Signature.public_key_hash →
Signature.public_key → M? Raw_context.t :=
Contract_manager_storage.reveal_manager_key.
Definition get_manager_key
: option Error_monad._error → Raw_context.t → Signature.public_key_hash →
M? Signature.public_key := Contract_manager_storage.get_manager_key.
Module Delegate.
Definition find
: Raw_context.t → Contract_repr.t →
M? (option Signature.public_key_hash) := Contract_delegate_storage.find.
Include Delegate_storage.Contract.
End Delegate.
End Contract.
Module Tx_rollup_level := Tx_rollup_level_repr.
Module Tx_rollup_commitment_hash := Tx_rollup_commitment_repr.Hash.
Module Tx_rollup_message_result_hash := Tx_rollup_message_result_hash_repr.
Module Tx_rollup.
Include Tx_rollup_repr.
Include Tx_rollup_storage.
End Tx_rollup.
Module Tx_rollup_state.
Include Tx_rollup_state_repr.
Include Tx_rollup_state_storage.
End Tx_rollup_state.
Module Tx_rollup_withdraw := Tx_rollup_withdraw_repr.
Module Tx_rollup_withdraw_list_hash := Tx_rollup_withdraw_list_hash_repr.
Module Tx_rollup_message_result := Tx_rollup_message_result_repr.
Module Tx_rollup_reveal.
Include Tx_rollup_reveal_repr.
Include Tx_rollup_reveal_storage.
End Tx_rollup_reveal.
Module Tx_rollup_message.
Include Tx_rollup_message_repr.
Definition make_message (msg : t) : t × int := (msg, (size_value msg)).
Definition make_batch (string_value : string) : t × int :=
make_message (Tx_rollup_message_repr.Batch string_value).
Definition make_deposit
(sender : Signature.public_key_hash)
(destination : Tx_rollup_l2_address.Indexable.value)
(ticket_hash : Ticket_hash_repr.t) (amount : Tx_rollup_l2_qty.t)
: t × int :=
make_message
(Tx_rollup_message_repr.Deposit
{| Tx_rollup_message_repr.deposit.sender := sender;
Tx_rollup_message_repr.deposit.destination := destination;
Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
Tx_rollup_message_repr.deposit.amount := amount; |}).
End Tx_rollup_message.
Module Tx_rollup_message_hash := Tx_rollup_message_hash_repr.
Module Tx_rollup_inbox.
Include Tx_rollup_inbox_repr.
Include Tx_rollup_inbox_storage.
End Tx_rollup_inbox.
Module Tx_rollup_commitment.
Include Tx_rollup_commitment_repr.
Include Tx_rollup_commitment_storage.
End Tx_rollup_commitment.
Module Tx_rollup_hash := Tx_rollup_hash_builder.
Module Tx_rollup_errors := Tx_rollup_errors_repr.
Module Global_constants_storage := Global_constants_storage.
Module Big_map.
Module Big_map := Lazy_storage_kind.Big_map.
Module Id.
Definition t : Set := Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t).
Definition encoding
: Data_encoding.t Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.encoding).
Definition rpc_arg
: RPC_arg.arg Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.rpc_arg).
Definition parse_z
: Z.t → Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.parse_z).
Definition unparse_to_z
: Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) → Z.t :=
Big_map.Id.(Lazy_storage_kind.ID.unparse_to_z).
End Id.
Definition fresh (temporary : bool) (c_value : Raw_context.t)
: M? (Raw_context.t × Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)) :=
(Lazy_storage.fresh (a := Big_map.alloc) (u := Big_map.updates))
Lazy_storage_kind.Big_map temporary c_value.
Definition mem
(c_value : Raw_context.t) (m_value : Storage.Big_map.id)
(k_value : Script_expr_hash.t) : M? (Raw_context.t × bool) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.mem)
(c_value, m_value) k_value.
Definition get_opt
(c_value : Raw_context.t) (m_value : Storage.Big_map.id)
(k_value : Script_expr_hash.t)
: M? (Raw_context.t × option Script_repr.expr) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.find)
(c_value, m_value) k_value.
Definition list_key_values
(offset : option int) (length : option int) (c_value : Raw_context.t)
(m_value : Storage.Big_map.id)
: M? (Raw_context.t × list (Script_expr_hash.t × Script_repr.expr)) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.list_key_values)
offset length (c_value, m_value).
Definition _exists
(c_value : Raw_context.t)
(id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
: M? (Raw_context.t × option (Script_repr.expr × Script_repr.expr)) :=
let? c_value :=
Raw_context.consume_gas c_value (Gas_limit_repr.read_bytes_cost 0) in
let? kt :=
Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.find) c_value
id in
match kt with
| None ⇒ return? (c_value, None)
| Some kt ⇒
let? kv :=
Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.get)
c_value id in
return? (c_value, (Some (kt, kv)))
end.
Definition update : Set := Big_map.update.
Definition updates : Set := Big_map.updates.
Definition alloc : Set := Big_map.alloc.
End Big_map.
Module Sapling.
Module Sapling_state := Lazy_storage_kind.Sapling_state.
Module Id.
Definition t : Set :=
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t).
Definition encoding
: Data_encoding.t
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.encoding).
Definition rpc_arg
: RPC_arg.arg Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.rpc_arg).
Definition parse_z
: Z.t → Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.parse_z).
Definition unparse_to_z
: Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) → Z.t :=
Sapling_state.Id.(Lazy_storage_kind.ID.unparse_to_z).
End Id.
Include Sapling_repr.
Include Sapling_storage.
Include Sapling_validator.
Definition fresh (temporary : bool) (c_value : Raw_context.t)
: M?
(Raw_context.t ×
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t)) :=
(Lazy_storage.fresh (a := Sapling_state.alloc) (u := Sapling_state.updates))
Lazy_storage_kind.Sapling_state temporary c_value.
Definition updates : Set := Sapling_state.updates.
Definition alloc : Set := Sapling_state.alloc.
Module Legacy.
Include Sapling.UTXO.Legacy.
Definition transaction_get_memo_size (transaction : transaction)
: option int :=
match
transaction.(Sapling.Legacy.transaction.outputs)
with
| [] ⇒ None
| cons {| Sapling.UTXO.output.ciphertext := ciphertext |} _ ⇒
Some (Sapling.Ciphertext.get_memo_size ciphertext)
end.
Definition transaction_in_memory_size (transaction : transaction)
: Saturation_repr.t := transaction_in_memory_size (cast transaction).
Definition verify_update
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(transaction : transaction) (key_value : string)
: M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
verify_update ctxt state_value (cast transaction) key_value.
End Legacy.
End Sapling.
Module Bond_id.
Include Bond_id_repr.
End Bond_id.
Module Receipt := Receipt_repr.
Module Consensus_key := Delegate_consensus_key.
Module Delegate.
Include Delegate_storage.
Include Delegate_missed_endorsements_storage.
Include Delegate_slashed_deposits_storage.
Include Delegate_cycles.
Definition deposits : Set := Storage.deposits.
Definition last_cycle_before_deactivation
: Raw_context.t → Signature.public_key_hash → M? Cycle_repr.t :=
Delegate_activation_storage.last_cycle_before_deactivation.
Definition prepare_stake_distribution : Raw_context.t → M? Raw_context.t :=
Stake_storage.prepare_stake_distribution.
Definition delegated_contracts
: Raw_context.t → Signature.public_key_hash → M? (list Contract_repr.t) :=
Contract_delegate_storage.delegated_contracts.
Definition deactivated
: Raw_context.t → Signature.public_key_hash → M? bool :=
Delegate_activation_storage.is_inactive.
Module Consensus_key := Delegate_consensus_key.
End Delegate.
Module Stake_distribution.
Definition snapshot_value : Raw_context.t → M? Raw_context.t :=
Stake_storage.snapshot_value.
Definition compute_snapshot_index
: Raw_context.t → Cycle_repr.t → int → M? int :=
Delegate_sampler.compute_snapshot_index.
Definition baking_rights_owner
: Raw_context.t → Level_repr.t → Round_repr.round →
M? (Raw_context.t × Slot_repr.t × Delegate_consensus_key.pk) :=
Delegate_sampler.baking_rights_owner.
Definition slot_owner
: Raw_context.t → Level_repr.t → Slot_repr.t →
M? (Raw_context.t × Delegate_consensus_key.pk) :=
Delegate_sampler.slot_owner.
End Stake_distribution.
Module Nonce := Nonce_storage.
Module Seed.
Include Seed_repr.
Include Seed_storage.
End Seed.
Module Fitness.
Definition raw : Set := Environment.V7.Fitness.t.
Include Fitness_repr.
End Fitness.
Module Bootstrap := Bootstrap_storage.
Module Commitment.
Include Commitment_repr.
Include Commitment_storage.
End Commitment.
Module Migration := Migration_repr.
Module Consensus.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_repr.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Commitment_storage.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Dal_endorsement_repr.
Require TezosOfOCaml.Proto_alpha.Dal_errors_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_cycles.
Require TezosOfOCaml.Proto_alpha.Delegate_missed_endorsements_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_sampler.
Require TezosOfOCaml.Proto_alpha.Delegate_slashed_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Destination_repr.
Require TezosOfOCaml.Proto_alpha.Entrypoint_repr.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Fitness_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Global_constants_storage.
Require TezosOfOCaml.Proto_alpha.Init_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_storage.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Sapling_validator.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_arith.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_refutation_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_builder.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt_repr.
Require TezosOfOCaml.Proto_alpha.Ticket_storage.
Require TezosOfOCaml.Proto_alpha.Time_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_errors_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_hash_builder.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_reveal_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_list_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_ticket_repr.
Definition t : Set := Raw_context.t.
Definition context : Set := t.
Module BASIC_DATA.
Record signature {t : Set} : Set := {
t := t;
op_eq : t → t → bool;
op_ltgt : t → t → bool;
op_lt : t → t → bool;
op_lteq : t → t → bool;
op_gteq : t → t → bool;
op_gt : t → t → bool;
compare : t → t → int;
equal : t → t → bool;
max : t → t → t;
min : t → t → t;
encoding : Data_encoding.t t;
pp : Format.formatter → t → unit;
}.
End BASIC_DATA.
Definition BASIC_DATA := @BASIC_DATA.signature.
Arguments BASIC_DATA {_}.
Module Tez := Tez_repr.
Module Period := Period_repr.
Module Timestamp.
Include Time_repr.
Definition current : Raw_context.t → Time.t := Raw_context.current_timestamp.
Definition predecessor : Raw_context.t → Time.t :=
Raw_context.predecessor_timestamp.
End Timestamp.
Module Slot := Slot_repr.
Module Sc_rollup_repr := Sc_rollup_repr.
Module Sc_rollup.
Module Tick := Sc_rollup_tick_repr.
Include Sc_rollup_repr.
Include Sc_rollup_PVM_sig.
Module ArithPVM := Sc_rollup_arith.
Module Wasm_2_0_0PVM := Sc_rollup_wasm.V2_0_0.
Module Inbox_message := Sc_rollup_inbox_message_repr.
Module Inbox.
Include Sc_rollup_inbox_repr.
Include Sc_rollup_inbox_storage.
End Inbox.
Module Proof := Sc_rollup_proof_repr.
Module Game := Sc_rollup_game_repr.
Module Commitment.
Include Sc_rollup_commitment_repr.
Include Sc_rollup_commitment_storage.
End Commitment.
Module Stake_storage.
Include Sc_rollup_stake_storage.
End Stake_storage.
Module Refutation_storage := Sc_rollup_refutation_storage.
Include Sc_rollup_storage.
Include Sc_rollups.
Module Outbox.
Include Sc_rollup_outbox_storage.
Module Message := Sc_rollup_outbox_message_repr.
End Outbox.
Module Errors := Sc_rollup_errors.
End Sc_rollup.
Module Dal.
Module Slot_index.
Include Dal_slot_repr.Index.
End Slot_index.
Module Endorsement.
Include Dal_endorsement_repr.
Include Raw_context.Dal.
End Endorsement.
Module Page.
Include Dal_slot_repr.Page.
End Page.
Module Slot.
Include Dal_slot_repr.
Include Dal_slot_storage.
Include Raw_context.Dal.
End Slot.
Module Slots_history := Dal_slot_repr.Slots_history.
Module Slots_storage := Dal_slot_storage.
End Dal.
Module Dal_errors := Dal_errors_repr.
Module Zk_rollup.
Include Zk_rollup_repr.
Module State := Zk_rollup_state_repr.
Module Account := Zk_rollup_account_repr.
Module Operation := Zk_rollup_operation_repr.
Module Ticket := Zk_rollup_ticket_repr.
Module Errors := Zk_rollup_errors.
Include Zk_rollup_storage.
End Zk_rollup.
Module Entrypoint := Entrypoint_repr.
Include Operation_repr.
Module Operation.
Definition t : Set := operation.
Definition packed : Set := packed_operation.
Definition unsigned_encoding
: Data_encoding.t (Operation.shell_header × packed_contents_list) :=
unsigned_operation_encoding.
Include Operation_repr.
End Operation.
Module Block_header := Block_header_repr.
Module Vote.
Include Vote_repr.
Include Vote_storage.
End Vote.
Module Block_payload.
Include Block_payload_repr.
End Block_payload.
Module First_level_of_protocol.
Definition get : Raw_context.t → M? Raw_level_repr.t :=
Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.get).
End First_level_of_protocol.
Module Ratio := Ratio_repr.
Module Raw_level := Raw_level_repr.
Module Cycle := Cycle_repr.
Module Fees := Fees_storage.
Definition public_key : Set := Signature.public_key.
Definition public_key_hash : Set := Signature.public_key_hash.
Definition signature : Set := Signature.t.
Module Constants.
Include Constants_repr.
Include Constants_storage.
Module Parametric := Constants_parametric_repr.
Definition round_durations (ctxt : Raw_context.t) : Round_repr.Durations.t :=
Raw_context.round_durations ctxt.
Definition all (ctxt : Raw_context.t) : t :=
all_of_parametric (parametric_value ctxt).
End Constants.
Module Voting_period.
Include Voting_period_repr.
Include Voting_period_storage.
End Voting_period.
Module Round.
Include Round_repr.
Definition round_durations : Set := Durations.t.
Definition pp_round_durations : Format.formatter → Durations.t → unit :=
Durations.pp.
Definition round_durations_encoding : Data_encoding.encoding Durations.t :=
Durations.encoding.
Definition round_duration
: Round_repr.Durations.t → Round_repr.round → Period_repr.t :=
Round_repr.Durations.round_duration.
Definition update (ctxt : Raw_context.t) (round : Round_repr.round)
: M? Raw_context.t :=
Storage.Block_round.(Storage.Simple_single_data_storage.update) ctxt round.
Definition get (ctxt : Raw_context.t) : M? Round_repr.round :=
Storage.Block_round.(Storage.Simple_single_data_storage.get) ctxt.
End Round.
Module Gas.
Include Gas_limit_repr.
Definition set_limit
: Raw_context.t → Gas_limit_repr.Arith.t → Raw_context.t :=
Raw_context.set_gas_limit.
Definition consume_limit_in_block
: Raw_context.t → Gas_limit_repr.Arith.t → M? Raw_context.t :=
Raw_context.consume_gas_limit_in_block.
Definition set_unlimited : Raw_context.t → Raw_context.t :=
Raw_context.set_gas_unlimited.
Definition consume
: Raw_context.t → Gas_limit_repr.cost → M? Raw_context.t :=
Raw_context.consume_gas.
Definition consume_from (available_gas : Arith.fp) (cost : cost)
: M? Arith.fp :=
match raw_consume available_gas cost with
| Some remaining_gas ⇒ return? remaining_gas
| None ⇒
Error_monad.error_value
(Build_extensible "Operation_quota_exceeded" unit tt)
end.
Definition remaining_operation_gas
: Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.remaining_operation_gas.
Definition update_remaining_operation_gas
: Raw_context.t → Gas_limit_repr.Arith.fp → Raw_context.t :=
Raw_context.update_remaining_operation_gas.
Definition reset_block_gas (ctxt : Raw_context.t) : Raw_context.t :=
let gas := Arith.fp_value (Constants.hard_gas_limit_per_block ctxt) in
Raw_context.update_remaining_block_gas ctxt gas.
Definition level : Raw_context.t → Gas_limit_repr.t := Raw_context.gas_level.
Definition consumed
: Raw_context.t → Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.gas_consumed.
Definition block_level : Raw_context.t → Gas_limit_repr.Arith.fp :=
Raw_context.block_gas_level.
Definition cost_of_repr {A : Set} (cost : A) : A := cost.
End Gas.
Module Script.
Include Michelson_v1_primitives.
Include Script_repr.
Inductive consume_deserialization_gas : Set :=
| Always : consume_deserialization_gas
| When_needed : consume_deserialization_gas.
Definition force_decode_in_context
(consume_deserialization_gas : consume_deserialization_gas)
(ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
: M? (Script_repr.expr × Raw_context.t) :=
let gas_cost :=
match consume_deserialization_gas with
| Always ⇒ Script_repr.stable_force_decode_cost lexpr
| When_needed ⇒ Script_repr.force_decode_cost lexpr
end in
let? ctxt := Raw_context.consume_gas ctxt gas_cost in
let? v_value := Script_repr.force_decode lexpr in
return? (v_value, ctxt).
Definition force_bytes_in_context
(ctxt : Raw_context.t) (lexpr : Script_repr.lazy_expr)
: M? (bytes × Raw_context.t) :=
let? ctxt :=
Raw_context.consume_gas ctxt (Script_repr.force_bytes_cost lexpr) in
let? v_value := Script_repr.force_bytes lexpr in
return? (v_value, ctxt).
Definition consume_decoding_gas
(available_gas : Gas.Arith.fp) (lexpr : Script_repr.lazy_expr)
: M? Gas.Arith.fp :=
let gas_cost := Script_repr.stable_force_decode_cost lexpr in
Gas.consume_from available_gas gas_cost.
End Script.
Module Level.
Include Level_repr.
Include Level_storage.
End Level.
Module Lazy_storage.
Module Kind := Lazy_storage_kind.
Module IdSet := Kind.IdSet.
Include Lazy_storage_diff.
End Lazy_storage.
Module Origination_nonce.
Definition init_value : Raw_context.t → Operation_hash.t → Raw_context.t :=
Raw_context.init_origination_nonce.
Definition unset : Raw_context.t → Raw_context.t :=
Raw_context.unset_origination_nonce.
End Origination_nonce.
Module Destination := Destination_repr.
Module Contract.
Include Contract_repr.
Include Contract_storage.
Definition is_manager_key_revealed
: Raw_context.t → Signature.public_key_hash → M? bool :=
Contract_manager_storage.is_manager_key_revealed.
Definition check_public_key
: Signature.public_key → Signature.public_key_hash → M? unit :=
Contract_manager_storage.check_public_key.
Definition reveal_manager_key
: option bool → Raw_context.t → Signature.public_key_hash →
Signature.public_key → M? Raw_context.t :=
Contract_manager_storage.reveal_manager_key.
Definition get_manager_key
: option Error_monad._error → Raw_context.t → Signature.public_key_hash →
M? Signature.public_key := Contract_manager_storage.get_manager_key.
Module Delegate.
Definition find
: Raw_context.t → Contract_repr.t →
M? (option Signature.public_key_hash) := Contract_delegate_storage.find.
Include Delegate_storage.Contract.
End Delegate.
End Contract.
Module Tx_rollup_level := Tx_rollup_level_repr.
Module Tx_rollup_commitment_hash := Tx_rollup_commitment_repr.Hash.
Module Tx_rollup_message_result_hash := Tx_rollup_message_result_hash_repr.
Module Tx_rollup.
Include Tx_rollup_repr.
Include Tx_rollup_storage.
End Tx_rollup.
Module Tx_rollup_state.
Include Tx_rollup_state_repr.
Include Tx_rollup_state_storage.
End Tx_rollup_state.
Module Tx_rollup_withdraw := Tx_rollup_withdraw_repr.
Module Tx_rollup_withdraw_list_hash := Tx_rollup_withdraw_list_hash_repr.
Module Tx_rollup_message_result := Tx_rollup_message_result_repr.
Module Tx_rollup_reveal.
Include Tx_rollup_reveal_repr.
Include Tx_rollup_reveal_storage.
End Tx_rollup_reveal.
Module Tx_rollup_message.
Include Tx_rollup_message_repr.
Definition make_message (msg : t) : t × int := (msg, (size_value msg)).
Definition make_batch (string_value : string) : t × int :=
make_message (Tx_rollup_message_repr.Batch string_value).
Definition make_deposit
(sender : Signature.public_key_hash)
(destination : Tx_rollup_l2_address.Indexable.value)
(ticket_hash : Ticket_hash_repr.t) (amount : Tx_rollup_l2_qty.t)
: t × int :=
make_message
(Tx_rollup_message_repr.Deposit
{| Tx_rollup_message_repr.deposit.sender := sender;
Tx_rollup_message_repr.deposit.destination := destination;
Tx_rollup_message_repr.deposit.ticket_hash := ticket_hash;
Tx_rollup_message_repr.deposit.amount := amount; |}).
End Tx_rollup_message.
Module Tx_rollup_message_hash := Tx_rollup_message_hash_repr.
Module Tx_rollup_inbox.
Include Tx_rollup_inbox_repr.
Include Tx_rollup_inbox_storage.
End Tx_rollup_inbox.
Module Tx_rollup_commitment.
Include Tx_rollup_commitment_repr.
Include Tx_rollup_commitment_storage.
End Tx_rollup_commitment.
Module Tx_rollup_hash := Tx_rollup_hash_builder.
Module Tx_rollup_errors := Tx_rollup_errors_repr.
Module Global_constants_storage := Global_constants_storage.
Module Big_map.
Module Big_map := Lazy_storage_kind.Big_map.
Module Id.
Definition t : Set := Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t).
Definition encoding
: Data_encoding.t Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.encoding).
Definition rpc_arg
: RPC_arg.arg Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.rpc_arg).
Definition parse_z
: Z.t → Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) :=
Big_map.Id.(Lazy_storage_kind.ID.parse_z).
Definition unparse_to_z
: Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t) → Z.t :=
Big_map.Id.(Lazy_storage_kind.ID.unparse_to_z).
End Id.
Definition fresh (temporary : bool) (c_value : Raw_context.t)
: M? (Raw_context.t × Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)) :=
(Lazy_storage.fresh (a := Big_map.alloc) (u := Big_map.updates))
Lazy_storage_kind.Big_map temporary c_value.
Definition mem
(c_value : Raw_context.t) (m_value : Storage.Big_map.id)
(k_value : Script_expr_hash.t) : M? (Raw_context.t × bool) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.mem)
(c_value, m_value) k_value.
Definition get_opt
(c_value : Raw_context.t) (m_value : Storage.Big_map.id)
(k_value : Script_expr_hash.t)
: M? (Raw_context.t × option Script_repr.expr) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.find)
(c_value, m_value) k_value.
Definition list_key_values
(offset : option int) (length : option int) (c_value : Raw_context.t)
(m_value : Storage.Big_map.id)
: M? (Raw_context.t × list (Script_expr_hash.t × Script_repr.expr)) :=
Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.list_key_values)
offset length (c_value, m_value).
Definition _exists
(c_value : Raw_context.t)
(id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
: M? (Raw_context.t × option (Script_repr.expr × Script_repr.expr)) :=
let? c_value :=
Raw_context.consume_gas c_value (Gas_limit_repr.read_bytes_cost 0) in
let? kt :=
Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.find) c_value
id in
match kt with
| None ⇒ return? (c_value, None)
| Some kt ⇒
let? kv :=
Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.get)
c_value id in
return? (c_value, (Some (kt, kv)))
end.
Definition update : Set := Big_map.update.
Definition updates : Set := Big_map.updates.
Definition alloc : Set := Big_map.alloc.
End Big_map.
Module Sapling.
Module Sapling_state := Lazy_storage_kind.Sapling_state.
Module Id.
Definition t : Set :=
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t).
Definition encoding
: Data_encoding.t
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.encoding).
Definition rpc_arg
: RPC_arg.arg Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.rpc_arg).
Definition parse_z
: Z.t → Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) :=
Sapling_state.Id.(Lazy_storage_kind.ID.parse_z).
Definition unparse_to_z
: Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t) → Z.t :=
Sapling_state.Id.(Lazy_storage_kind.ID.unparse_to_z).
End Id.
Include Sapling_repr.
Include Sapling_storage.
Include Sapling_validator.
Definition fresh (temporary : bool) (c_value : Raw_context.t)
: M?
(Raw_context.t ×
Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t)) :=
(Lazy_storage.fresh (a := Sapling_state.alloc) (u := Sapling_state.updates))
Lazy_storage_kind.Sapling_state temporary c_value.
Definition updates : Set := Sapling_state.updates.
Definition alloc : Set := Sapling_state.alloc.
Module Legacy.
Include Sapling.UTXO.Legacy.
Definition transaction_get_memo_size (transaction : transaction)
: option int :=
match
transaction.(Sapling.Legacy.transaction.outputs)
with
| [] ⇒ None
| cons {| Sapling.UTXO.output.ciphertext := ciphertext |} _ ⇒
Some (Sapling.Ciphertext.get_memo_size ciphertext)
end.
Definition transaction_in_memory_size (transaction : transaction)
: Saturation_repr.t := transaction_in_memory_size (cast transaction).
Definition verify_update
(ctxt : Raw_context.t) (state_value : Sapling_storage.state)
(transaction : transaction) (key_value : string)
: M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
verify_update ctxt state_value (cast transaction) key_value.
End Legacy.
End Sapling.
Module Bond_id.
Include Bond_id_repr.
End Bond_id.
Module Receipt := Receipt_repr.
Module Consensus_key := Delegate_consensus_key.
Module Delegate.
Include Delegate_storage.
Include Delegate_missed_endorsements_storage.
Include Delegate_slashed_deposits_storage.
Include Delegate_cycles.
Definition deposits : Set := Storage.deposits.
Definition last_cycle_before_deactivation
: Raw_context.t → Signature.public_key_hash → M? Cycle_repr.t :=
Delegate_activation_storage.last_cycle_before_deactivation.
Definition prepare_stake_distribution : Raw_context.t → M? Raw_context.t :=
Stake_storage.prepare_stake_distribution.
Definition delegated_contracts
: Raw_context.t → Signature.public_key_hash → M? (list Contract_repr.t) :=
Contract_delegate_storage.delegated_contracts.
Definition deactivated
: Raw_context.t → Signature.public_key_hash → M? bool :=
Delegate_activation_storage.is_inactive.
Module Consensus_key := Delegate_consensus_key.
End Delegate.
Module Stake_distribution.
Definition snapshot_value : Raw_context.t → M? Raw_context.t :=
Stake_storage.snapshot_value.
Definition compute_snapshot_index
: Raw_context.t → Cycle_repr.t → int → M? int :=
Delegate_sampler.compute_snapshot_index.
Definition baking_rights_owner
: Raw_context.t → Level_repr.t → Round_repr.round →
M? (Raw_context.t × Slot_repr.t × Delegate_consensus_key.pk) :=
Delegate_sampler.baking_rights_owner.
Definition slot_owner
: Raw_context.t → Level_repr.t → Slot_repr.t →
M? (Raw_context.t × Delegate_consensus_key.pk) :=
Delegate_sampler.slot_owner.
End Stake_distribution.
Module Nonce := Nonce_storage.
Module Seed.
Include Seed_repr.
Include Seed_storage.
End Seed.
Module Fitness.
Definition raw : Set := Environment.V7.Fitness.t.
Include Fitness_repr.
End Fitness.
Module Bootstrap := Bootstrap_storage.
Module Commitment.
Include Commitment_repr.
Include Commitment_storage.
End Commitment.
Module Migration := Migration_repr.
Module Consensus.
Inclusion of the module [Raw_context.Consensus]
Definition allowed_endorsements :=
Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_endorsements).
Definition allowed_preendorsements :=
Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_preendorsements).
Definition current_endorsement_power :=
Raw_context.Consensus.(Raw_context.CONSENSUS.current_endorsement_power).
Definition initialize_consensus_operation :=
Raw_context.Consensus.(Raw_context.CONSENSUS.initialize_consensus_operation).
Definition record_grand_parent_endorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_grand_parent_endorsement).
Definition record_endorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_endorsement).
Definition record_preendorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_preendorsement).
Definition endorsements_seen :=
Raw_context.Consensus.(Raw_context.CONSENSUS.endorsements_seen).
Definition get_preendorsements_quorum_round :=
Raw_context.Consensus.(Raw_context.CONSENSUS.get_preendorsements_quorum_round).
Definition set_preendorsements_quorum_round :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_preendorsements_quorum_round).
Definition locked_round_evidence :=
Raw_context.Consensus.(Raw_context.CONSENSUS.locked_round_evidence).
Definition set_endorsement_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch).
Definition endorsement_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.endorsement_branch).
Definition set_grand_parent_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch).
Definition grand_parent_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.grand_parent_branch).
Definition load_endorsement_branch (ctxt : Raw_context.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.find)
ctxt in
match function_parameter with
| Some endorsement_branch ⇒
return?
(Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch)
ctxt endorsement_branch)
| None ⇒ return? ctxt
end.
Definition store_endorsement_branch
(ctxt : Raw_context.t)
(branch :
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.value))
: Raw_context.t :=
let ctxt := set_endorsement_branch ctxt branch in
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.add)
ctxt branch.
Definition load_grand_parent_branch (ctxt : Raw_context.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.find)
ctxt in
match function_parameter with
| Some grand_parent_branch ⇒
return?
(Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch)
ctxt grand_parent_branch)
| None ⇒ return? ctxt
end.
Definition store_grand_parent_branch
(ctxt : Raw_context.t)
(branch :
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.value))
: Raw_context.t :=
let ctxt := set_grand_parent_branch ctxt branch in
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.add)
ctxt branch.
End Consensus.
Definition prepare_first_block
: Chain_id.t → Context.t →
(Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t)) →
int32 → Time.t → M? Raw_context.t := Init_storage.prepare_first_block.
Definition prepare
(ctxt : Context.t) (level : Int32.t) (predecessor_timestamp : Time.t)
(timestamp : Time.t)
: M?
(Raw_context.t × Receipt_repr.balance_updates ×
list Migration_repr.origination_result) :=
let? '(ctxt, balance_updates, origination_results) :=
Init_storage.prepare ctxt level predecessor_timestamp timestamp in
let? ctxt := Consensus.load_endorsement_branch ctxt in
let? ctxt := Consensus.load_grand_parent_branch ctxt in
return? (ctxt, balance_updates, origination_results).
Definition finalize
(message : option string) (c_value : Raw_context.t) (fitness : Environment.V7.Fitness.t)
: M? Updater.validation_result :=
let? last_allowed_fork_level := Level.last_allowed_fork_level c_value in
let context_value := Raw_context.recover c_value in
return?
{| Updater.validation_result.context := context_value;
Updater.validation_result.fitness := fitness;
Updater.validation_result.message := message;
Updater.validation_result.max_operations_ttl :=
(Raw_context.constants c_value).(Constants_parametric_repr.t.max_operations_time_to_live);
Updater.validation_result.last_allowed_fork_level :=
Raw_level.to_int32 last_allowed_fork_level; |}.
Definition current_context (c_value : Raw_context.t) : Context.t :=
Raw_context.recover c_value.
Definition record_non_consensus_operation_hash
: Raw_context.t → Operation_hash.t → Raw_context.t :=
Raw_context.record_non_consensus_operation_hash.
Definition non_consensus_operations : Raw_context.t → list Operation_hash.t :=
Raw_context.non_consensus_operations.
Definition record_dictator_proposal_seen : Raw_context.t → Raw_context.t :=
Raw_context.record_dictator_proposal_seen.
Definition dictator_proposal_seen : Raw_context.t → bool :=
Raw_context.dictator_proposal_seen.
Definition activate : Raw_context.t → Protocol_hash.t → Raw_context.t :=
Raw_context.activate.
Definition reset_internal_nonce : Raw_context.t → Raw_context.t :=
Raw_context.reset_internal_nonce.
Definition fresh_internal_nonce : Raw_context.t → M? (Raw_context.t × int) :=
Raw_context.fresh_internal_nonce.
Definition record_internal_nonce : Raw_context.t → int → Raw_context.t :=
Raw_context.record_internal_nonce.
Definition internal_nonce_already_recorded : Raw_context.t → int → bool :=
Raw_context.internal_nonce_already_recorded.
Definition description : Storage_description.t Raw_context.t :=
Raw_context.description.
Module Parameters := Parameters_repr.
Module Liquidity_baking.
Include Liquidity_baking_repr.
Include Liquidity_baking_storage.
End Liquidity_baking.
Module Ticket_hash.
Include Ticket_hash_repr.
Include Ticket_hash_builder.
End Ticket_hash.
Module Ticket_balance.
Include Ticket_storage.
End Ticket_balance.
Module Ticket_receipt.
Include Ticket_receipt_repr.
End Ticket_receipt.
Module Token := Token.
Module Cache := Cache_repr.
Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_endorsements).
Definition allowed_preendorsements :=
Raw_context.Consensus.(Raw_context.CONSENSUS.allowed_preendorsements).
Definition current_endorsement_power :=
Raw_context.Consensus.(Raw_context.CONSENSUS.current_endorsement_power).
Definition initialize_consensus_operation :=
Raw_context.Consensus.(Raw_context.CONSENSUS.initialize_consensus_operation).
Definition record_grand_parent_endorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_grand_parent_endorsement).
Definition record_endorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_endorsement).
Definition record_preendorsement :=
Raw_context.Consensus.(Raw_context.CONSENSUS.record_preendorsement).
Definition endorsements_seen :=
Raw_context.Consensus.(Raw_context.CONSENSUS.endorsements_seen).
Definition get_preendorsements_quorum_round :=
Raw_context.Consensus.(Raw_context.CONSENSUS.get_preendorsements_quorum_round).
Definition set_preendorsements_quorum_round :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_preendorsements_quorum_round).
Definition locked_round_evidence :=
Raw_context.Consensus.(Raw_context.CONSENSUS.locked_round_evidence).
Definition set_endorsement_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch).
Definition endorsement_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.endorsement_branch).
Definition set_grand_parent_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch).
Definition grand_parent_branch :=
Raw_context.Consensus.(Raw_context.CONSENSUS.grand_parent_branch).
Definition load_endorsement_branch (ctxt : Raw_context.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.find)
ctxt in
match function_parameter with
| Some endorsement_branch ⇒
return?
(Raw_context.Consensus.(Raw_context.CONSENSUS.set_endorsement_branch)
ctxt endorsement_branch)
| None ⇒ return? ctxt
end.
Definition store_endorsement_branch
(ctxt : Raw_context.t)
(branch :
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.value))
: Raw_context.t :=
let ctxt := set_endorsement_branch ctxt branch in
Storage.Tenderbake.Endorsement_branch.(Storage_sigs.Single_data_storage.add)
ctxt branch.
Definition load_grand_parent_branch (ctxt : Raw_context.t)
: M? Raw_context.t :=
let? function_parameter :=
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.find)
ctxt in
match function_parameter with
| Some grand_parent_branch ⇒
return?
(Raw_context.Consensus.(Raw_context.CONSENSUS.set_grand_parent_branch)
ctxt grand_parent_branch)
| None ⇒ return? ctxt
end.
Definition store_grand_parent_branch
(ctxt : Raw_context.t)
(branch :
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.value))
: Raw_context.t :=
let ctxt := set_grand_parent_branch ctxt branch in
Storage.Tenderbake.Grand_parent_branch.(Storage_sigs.Single_data_storage.add)
ctxt branch.
End Consensus.
Definition prepare_first_block
: Chain_id.t → Context.t →
(Raw_context.t → Script_repr.t →
M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t)) →
int32 → Time.t → M? Raw_context.t := Init_storage.prepare_first_block.
Definition prepare
(ctxt : Context.t) (level : Int32.t) (predecessor_timestamp : Time.t)
(timestamp : Time.t)
: M?
(Raw_context.t × Receipt_repr.balance_updates ×
list Migration_repr.origination_result) :=
let? '(ctxt, balance_updates, origination_results) :=
Init_storage.prepare ctxt level predecessor_timestamp timestamp in
let? ctxt := Consensus.load_endorsement_branch ctxt in
let? ctxt := Consensus.load_grand_parent_branch ctxt in
return? (ctxt, balance_updates, origination_results).
Definition finalize
(message : option string) (c_value : Raw_context.t) (fitness : Environment.V7.Fitness.t)
: M? Updater.validation_result :=
let? last_allowed_fork_level := Level.last_allowed_fork_level c_value in
let context_value := Raw_context.recover c_value in
return?
{| Updater.validation_result.context := context_value;
Updater.validation_result.fitness := fitness;
Updater.validation_result.message := message;
Updater.validation_result.max_operations_ttl :=
(Raw_context.constants c_value).(Constants_parametric_repr.t.max_operations_time_to_live);
Updater.validation_result.last_allowed_fork_level :=
Raw_level.to_int32 last_allowed_fork_level; |}.
Definition current_context (c_value : Raw_context.t) : Context.t :=
Raw_context.recover c_value.
Definition record_non_consensus_operation_hash
: Raw_context.t → Operation_hash.t → Raw_context.t :=
Raw_context.record_non_consensus_operation_hash.
Definition non_consensus_operations : Raw_context.t → list Operation_hash.t :=
Raw_context.non_consensus_operations.
Definition record_dictator_proposal_seen : Raw_context.t → Raw_context.t :=
Raw_context.record_dictator_proposal_seen.
Definition dictator_proposal_seen : Raw_context.t → bool :=
Raw_context.dictator_proposal_seen.
Definition activate : Raw_context.t → Protocol_hash.t → Raw_context.t :=
Raw_context.activate.
Definition reset_internal_nonce : Raw_context.t → Raw_context.t :=
Raw_context.reset_internal_nonce.
Definition fresh_internal_nonce : Raw_context.t → M? (Raw_context.t × int) :=
Raw_context.fresh_internal_nonce.
Definition record_internal_nonce : Raw_context.t → int → Raw_context.t :=
Raw_context.record_internal_nonce.
Definition internal_nonce_already_recorded : Raw_context.t → int → bool :=
Raw_context.internal_nonce_already_recorded.
Definition description : Storage_description.t Raw_context.t :=
Raw_context.description.
Module Parameters := Parameters_repr.
Module Liquidity_baking.
Include Liquidity_baking_repr.
Include Liquidity_baking_storage.
End Liquidity_baking.
Module Ticket_hash.
Include Ticket_hash_repr.
Include Ticket_hash_builder.
End Ticket_hash.
Module Ticket_balance.
Include Ticket_storage.
End Ticket_balance.
Module Ticket_receipt.
Include Ticket_receipt_repr.
End Ticket_receipt.
Module Token := Token.
Module Cache := Cache_repr.