🖼️ Raw_context.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Definition Int_set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Module Raw_consensus.
Module t.
Record record : Set := Build {
current_endorsement_power : int;
allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int);
allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int);
grand_parent_endorsements_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t);
endorsements_seen : Slot_repr._Set.(_Set.S.t);
preendorsements_seen : Slot_repr._Set.(_Set.S.t);
locked_round_evidence : option (Round_repr.t × int);
preendorsements_quorum_round : option Round_repr.t;
endorsement_branch : option (Block_hash.t × Block_payload_hash.t);
grand_parent_branch : option (Block_hash.t × Block_payload_hash.t);
}.
Definition with_current_endorsement_power current_endorsement_power
(r : record) :=
Build current_endorsement_power r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_allowed_endorsements allowed_endorsements (r : record) :=
Build r.(current_endorsement_power) allowed_endorsements
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_allowed_preendorsements allowed_preendorsements
(r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
allowed_preendorsements r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_grand_parent_endorsements_seen
grand_parent_endorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) grand_parent_endorsements_seen
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_endorsements_seen endorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
endorsements_seen r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_preendorsements_seen preendorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) preendorsements_seen r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_locked_round_evidence locked_round_evidence (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) locked_round_evidence
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_preendorsements_quorum_round preendorsements_quorum_round
(r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
preendorsements_quorum_round r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_endorsement_branch endorsement_branch (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) endorsement_branch
r.(grand_parent_branch).
Definition with_grand_parent_branch grand_parent_branch (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
grand_parent_branch.
End t.
Definition t := t.record.
Definition empty : t :=
{| t.current_endorsement_power := 0;
t.allowed_endorsements := Slot_repr.Map.(Map.S.empty);
t.allowed_preendorsements := Slot_repr.Map.(Map.S.empty);
t.grand_parent_endorsements_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty);
t.endorsements_seen := Slot_repr._Set.(_Set.S.empty);
t.preendorsements_seen := Slot_repr._Set.(_Set.S.empty);
t.locked_round_evidence := None; t.preendorsements_quorum_round := None;
t.endorsement_branch := None; t.grand_parent_branch := None; |}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Period_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.State_hash.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Definition Int_set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Module Raw_consensus.
Module t.
Record record : Set := Build {
current_endorsement_power : int;
allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int);
allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int);
grand_parent_endorsements_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t);
endorsements_seen : Slot_repr._Set.(_Set.S.t);
preendorsements_seen : Slot_repr._Set.(_Set.S.t);
locked_round_evidence : option (Round_repr.t × int);
preendorsements_quorum_round : option Round_repr.t;
endorsement_branch : option (Block_hash.t × Block_payload_hash.t);
grand_parent_branch : option (Block_hash.t × Block_payload_hash.t);
}.
Definition with_current_endorsement_power current_endorsement_power
(r : record) :=
Build current_endorsement_power r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_allowed_endorsements allowed_endorsements (r : record) :=
Build r.(current_endorsement_power) allowed_endorsements
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_allowed_preendorsements allowed_preendorsements
(r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
allowed_preendorsements r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_grand_parent_endorsements_seen
grand_parent_endorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) grand_parent_endorsements_seen
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_endorsements_seen endorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
endorsements_seen r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_preendorsements_seen preendorsements_seen (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) preendorsements_seen r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_locked_round_evidence locked_round_evidence (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) locked_round_evidence
r.(preendorsements_quorum_round) r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_preendorsements_quorum_round preendorsements_quorum_round
(r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
preendorsements_quorum_round r.(endorsement_branch)
r.(grand_parent_branch).
Definition with_endorsement_branch endorsement_branch (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) endorsement_branch
r.(grand_parent_branch).
Definition with_grand_parent_branch grand_parent_branch (r : record) :=
Build r.(current_endorsement_power) r.(allowed_endorsements)
r.(allowed_preendorsements) r.(grand_parent_endorsements_seen)
r.(endorsements_seen) r.(preendorsements_seen) r.(locked_round_evidence)
r.(preendorsements_quorum_round) r.(endorsement_branch)
grand_parent_branch.
End t.
Definition t := t.record.
Definition empty : t :=
{| t.current_endorsement_power := 0;
t.allowed_endorsements := Slot_repr.Map.(Map.S.empty);
t.allowed_preendorsements := Slot_repr.Map.(Map.S.empty);
t.grand_parent_endorsements_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty);
t.endorsements_seen := Slot_repr._Set.(_Set.S.empty);
t.preendorsements_seen := Slot_repr._Set.(_Set.S.empty);
t.locked_round_evidence := None; t.preendorsements_quorum_round := None;
t.endorsement_branch := None; t.grand_parent_branch := None; |}.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
Error_monad.register_error_kind Error_monad.Branch
"operation.double_inclusion_of_consensus_operation"
"Double inclusion of consensus operation"
"double inclusion of consensus operation"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Double inclusion of consensus operation"
CamlinternalFormatBasics.End_of_format)
"Double inclusion of consensus operation"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Double_inclusion_of_consensus_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Double_inclusion_of_consensus_operation" unit tt).
Definition record_grand_parent_endorsement
(t_value : t) (pkh : Signature.public_key_hash) : M? t :=
let? '_ :=
Error_monad.error_when
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.mem)
pkh t_value.(t.grand_parent_endorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
return?
(t.with_grand_parent_endorsements_seen
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
pkh t_value.(t.grand_parent_endorsements_seen)) t_value).
Definition record_endorsement
(t_value : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
let? '_ :=
Error_monad.error_when
(Slot_repr._Set.(_Set.S.mem) initial_slot t_value.(t.endorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
return?
(t.with_endorsements_seen
(Slot_repr._Set.(_Set.S.add) initial_slot t_value.(t.endorsements_seen))
(t.with_current_endorsement_power
(t_value.(t.current_endorsement_power) +i power) t_value)).
Definition record_preendorsement
(initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
(t_value : t) : M? t :=
let? '_ :=
Error_monad.error_when
(Slot_repr._Set.(_Set.S.mem) initial_slot
t_value.(t.preendorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
let locked_round_evidence :=
match t_value.(t.locked_round_evidence) with
| None ⇒ Some (round, power)
| Some (_stored_round, evidences) ⇒ Some (round, (evidences +i power))
end in
return?
(t.with_locked_round_evidence locked_round_evidence
(t.with_preendorsements_seen
(Slot_repr._Set.(_Set.S.add) initial_slot
t_value.(t.preendorsements_seen)) t_value)).
Definition set_preendorsements_quorum_round
(round : Round_repr.t) (t_value : t) : t :=
match t_value.(t.preendorsements_quorum_round) with
| Some round' ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Round_repr.equal round round') in
t_value
| None ⇒ t.with_preendorsements_quorum_round (Some round) t_value
end.
Definition initialize_with_endorsements_and_preendorsements
(allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int))
(allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int)) (t_value : t)
: t :=
t.with_allowed_preendorsements allowed_preendorsements
(t.with_allowed_endorsements allowed_endorsements t_value).
Definition locked_round_evidence (t_value : t)
: option (Round_repr.t × int) := t_value.(t.locked_round_evidence).
Definition endorsement_branch (t_value : t)
: option (Block_hash.t × Block_payload_hash.t) :=
t_value.(t.endorsement_branch).
Definition grand_parent_branch (t_value : t)
: option (Block_hash.t × Block_payload_hash.t) :=
t_value.(t.grand_parent_branch).
Definition set_endorsement_branch
(t_value : t) (endorsement_branch : Block_hash.t × Block_payload_hash.t)
: t := t.with_endorsement_branch (Some endorsement_branch) t_value.
Definition set_grand_parent_branch
(t_value : t) (grand_parent_branch : Block_hash.t × Block_payload_hash.t)
: t := t.with_grand_parent_branch (Some grand_parent_branch) t_value.
End Raw_consensus.
Module back.
Record record : Set := Build {
context : Context.t;
constants : Constants_repr.parametric;
round_durations : Round_repr.Durations.t;
cycle_eras : Level_repr.cycle_eras;
level : Level_repr.t;
predecessor_timestamp : Time.t;
timestamp : Time.t;
fees : Tez_repr.t;
origination_nonce : option Origination_nonce.t;
temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t;
internal_nonce : int;
internal_nonces_used : Int_set.(_Set.S.t);
remaining_block_gas : Gas_limit_repr.Arith.fp;
unlimited_operation_gas : bool;
consensus : Raw_consensus.t;
non_consensus_operations_rev : list Operation_hash.t;
sampler_state :
Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash));
stake_distribution_for_current_cycle :
option
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t);
tx_rollup_current_messages :
Tx_rollup_repr.Map.(Map.S.t) Tx_rollup_inbox_repr.Merkle.tree;
sc_rollup_current_messages :
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.t) Context.tree;
}.
Definition with_context context (r : record) :=
Build context r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_constants constants (r : record) :=
Build r.(context) constants r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_round_durations round_durations (r : record) :=
Build r.(context) r.(constants) round_durations r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_cycle_eras cycle_eras (r : record) :=
Build r.(context) r.(constants) r.(round_durations) cycle_eras r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_level level (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) level
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_predecessor_timestamp predecessor_timestamp (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
predecessor_timestamp r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_timestamp timestamp (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) timestamp r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_fees fees (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) fees r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_origination_nonce origination_nonce (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) origination_nonce
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_temporary_lazy_storage_ids temporary_lazy_storage_ids
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
temporary_lazy_storage_ids r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_internal_nonce internal_nonce (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) internal_nonce r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_internal_nonces_used internal_nonces_used (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) internal_nonces_used
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_remaining_block_gas remaining_block_gas (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
remaining_block_gas r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_unlimited_operation_gas unlimited_operation_gas
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) unlimited_operation_gas r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_consensus consensus (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) consensus
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_non_consensus_operations_rev non_consensus_operations_rev
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
non_consensus_operations_rev r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_sampler_state sampler_state (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) sampler_state
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_stake_distribution_for_current_cycle
stake_distribution_for_current_cycle (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
stake_distribution_for_current_cycle r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_tx_rollup_current_messages tx_rollup_current_messages
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) tx_rollup_current_messages
r.(sc_rollup_current_messages).
Definition with_sc_rollup_current_messages sc_rollup_current_messages
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
sc_rollup_current_messages.
End back.
Definition back := back.record.
Module t.
Record record : Set := Build {
remaining_operation_gas : Gas_limit_repr.Arith.fp;
back : back;
}.
Definition with_remaining_operation_gas remaining_operation_gas
(r : record) :=
Build remaining_operation_gas r.(back).
Definition with_back back (r : record) :=
Build r.(remaining_operation_gas) back.
End t.
Definition t := t.record.
Definition root : Set := t.
Definition context_value (ctxt : t) : Context.t := ctxt.(t.back).(back.context).
Definition current_level (ctxt : t) : Level_repr.t :=
ctxt.(t.back).(back.level).
Definition predecessor_timestamp (ctxt : t) : Time.t :=
ctxt.(t.back).(back.predecessor_timestamp).
Definition current_timestamp (ctxt : t) : Time.t :=
ctxt.(t.back).(back.timestamp).
Definition round_durations (ctxt : t) : Round_repr.Durations.t :=
ctxt.(t.back).(back.round_durations).
Definition cycle_eras (ctxt : t) : Level_repr.cycle_eras :=
ctxt.(t.back).(back.cycle_eras).
Definition constants (ctxt : t) : Constants_repr.parametric :=
ctxt.(t.back).(back.constants).
Definition recover (ctxt : t) : Context.t := ctxt.(t.back).(back.context).
Definition fees (ctxt : t) : Tez_repr.t := ctxt.(t.back).(back.fees).
Definition origination_nonce (ctxt : t) : option Origination_nonce.t :=
ctxt.(t.back).(back.origination_nonce).
Definition internal_nonce (ctxt : t) : int :=
ctxt.(t.back).(back.internal_nonce).
Definition internal_nonces_used (ctxt : t) : Int_set.(_Set.S.t) :=
ctxt.(t.back).(back.internal_nonces_used).
Definition remaining_block_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
ctxt.(t.back).(back.remaining_block_gas).
Definition unlimited_operation_gas (ctxt : t) : bool :=
ctxt.(t.back).(back.unlimited_operation_gas).
Definition temporary_lazy_storage_ids (ctxt : t)
: Lazy_storage_kind.Temp_ids.t :=
ctxt.(t.back).(back.temporary_lazy_storage_ids).
Definition remaining_operation_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
ctxt.(t.remaining_operation_gas).
Definition non_consensus_operations_rev (ctxt : t) : list Operation_hash.t :=
ctxt.(t.back).(back.non_consensus_operations_rev).
Definition sampler_state (ctxt : t)
: Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) :=
ctxt.(t.back).(back.sampler_state).
Definition update_back (ctxt : t) (back : back) : t := t.with_back back ctxt.
Definition update_remaining_block_gas
(ctxt : t) (remaining_block_gas : Gas_limit_repr.Arith.fp) : t :=
update_back ctxt
(back.with_remaining_block_gas remaining_block_gas ctxt.(t.back)).
Definition update_remaining_operation_gas
(ctxt : t) (remaining_operation_gas : Gas_limit_repr.Arith.fp) : t :=
t.with_remaining_operation_gas remaining_operation_gas ctxt.
Definition update_unlimited_operation_gas
(ctxt : t) (unlimited_operation_gas : bool) : t :=
update_back ctxt
(back.with_unlimited_operation_gas unlimited_operation_gas ctxt.(t.back)).
Definition update_context (ctxt : t) (context_value : Context.t) : t :=
update_back ctxt (back.with_context context_value ctxt.(t.back)).
Definition update_constants (ctxt : t) (constants : Constants_repr.parametric)
: t := update_back ctxt (back.with_constants constants ctxt.(t.back)).
Definition update_origination_nonce
(ctxt : t) (origination_nonce : option Origination_nonce.t) : t :=
update_back ctxt (back.with_origination_nonce origination_nonce ctxt.(t.back)).
Definition update_internal_nonce (ctxt : t) (internal_nonce : int) : t :=
update_back ctxt (back.with_internal_nonce internal_nonce ctxt.(t.back)).
Definition update_internal_nonces_used
(ctxt : t) (internal_nonces_used : Int_set.(_Set.S.t)) : t :=
update_back ctxt
(back.with_internal_nonces_used internal_nonces_used ctxt.(t.back)).
Definition update_fees (ctxt : t) (fees : Tez_repr.t) : t :=
update_back ctxt (back.with_fees fees ctxt.(t.back)).
Definition update_temporary_lazy_storage_ids
(ctxt : t) (temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t) : t :=
update_back ctxt
(back.with_temporary_lazy_storage_ids temporary_lazy_storage_ids
ctxt.(t.back)).
Definition update_non_consensus_operations_rev
(ctxt : t) (non_consensus_operations_rev : list Operation_hash.t) : t :=
update_back ctxt
(back.with_non_consensus_operations_rev non_consensus_operations_rev
ctxt.(t.back)).
Definition update_sampler_state
(ctxt : t)
(sampler_state :
Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash))) : t :=
update_back ctxt (back.with_sampler_state sampler_state ctxt.(t.back)).
Error_monad.register_error_kind Error_monad.Branch
"operation.double_inclusion_of_consensus_operation"
"Double inclusion of consensus operation"
"double inclusion of consensus operation"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Double inclusion of consensus operation"
CamlinternalFormatBasics.End_of_format)
"Double inclusion of consensus operation"))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Double_inclusion_of_consensus_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Double_inclusion_of_consensus_operation" unit tt).
Definition record_grand_parent_endorsement
(t_value : t) (pkh : Signature.public_key_hash) : M? t :=
let? '_ :=
Error_monad.error_when
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.mem)
pkh t_value.(t.grand_parent_endorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
return?
(t.with_grand_parent_endorsements_seen
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
pkh t_value.(t.grand_parent_endorsements_seen)) t_value).
Definition record_endorsement
(t_value : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
let? '_ :=
Error_monad.error_when
(Slot_repr._Set.(_Set.S.mem) initial_slot t_value.(t.endorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
return?
(t.with_endorsements_seen
(Slot_repr._Set.(_Set.S.add) initial_slot t_value.(t.endorsements_seen))
(t.with_current_endorsement_power
(t_value.(t.current_endorsement_power) +i power) t_value)).
Definition record_preendorsement
(initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
(t_value : t) : M? t :=
let? '_ :=
Error_monad.error_when
(Slot_repr._Set.(_Set.S.mem) initial_slot
t_value.(t.preendorsements_seen))
(Build_extensible "Double_inclusion_of_consensus_operation" unit tt) in
let locked_round_evidence :=
match t_value.(t.locked_round_evidence) with
| None ⇒ Some (round, power)
| Some (_stored_round, evidences) ⇒ Some (round, (evidences +i power))
end in
return?
(t.with_locked_round_evidence locked_round_evidence
(t.with_preendorsements_seen
(Slot_repr._Set.(_Set.S.add) initial_slot
t_value.(t.preendorsements_seen)) t_value)).
Definition set_preendorsements_quorum_round
(round : Round_repr.t) (t_value : t) : t :=
match t_value.(t.preendorsements_quorum_round) with
| Some round' ⇒
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Round_repr.equal round round') in
t_value
| None ⇒ t.with_preendorsements_quorum_round (Some round) t_value
end.
Definition initialize_with_endorsements_and_preendorsements
(allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int))
(allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int)) (t_value : t)
: t :=
t.with_allowed_preendorsements allowed_preendorsements
(t.with_allowed_endorsements allowed_endorsements t_value).
Definition locked_round_evidence (t_value : t)
: option (Round_repr.t × int) := t_value.(t.locked_round_evidence).
Definition endorsement_branch (t_value : t)
: option (Block_hash.t × Block_payload_hash.t) :=
t_value.(t.endorsement_branch).
Definition grand_parent_branch (t_value : t)
: option (Block_hash.t × Block_payload_hash.t) :=
t_value.(t.grand_parent_branch).
Definition set_endorsement_branch
(t_value : t) (endorsement_branch : Block_hash.t × Block_payload_hash.t)
: t := t.with_endorsement_branch (Some endorsement_branch) t_value.
Definition set_grand_parent_branch
(t_value : t) (grand_parent_branch : Block_hash.t × Block_payload_hash.t)
: t := t.with_grand_parent_branch (Some grand_parent_branch) t_value.
End Raw_consensus.
Module back.
Record record : Set := Build {
context : Context.t;
constants : Constants_repr.parametric;
round_durations : Round_repr.Durations.t;
cycle_eras : Level_repr.cycle_eras;
level : Level_repr.t;
predecessor_timestamp : Time.t;
timestamp : Time.t;
fees : Tez_repr.t;
origination_nonce : option Origination_nonce.t;
temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t;
internal_nonce : int;
internal_nonces_used : Int_set.(_Set.S.t);
remaining_block_gas : Gas_limit_repr.Arith.fp;
unlimited_operation_gas : bool;
consensus : Raw_consensus.t;
non_consensus_operations_rev : list Operation_hash.t;
sampler_state :
Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash));
stake_distribution_for_current_cycle :
option
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t);
tx_rollup_current_messages :
Tx_rollup_repr.Map.(Map.S.t) Tx_rollup_inbox_repr.Merkle.tree;
sc_rollup_current_messages :
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.t) Context.tree;
}.
Definition with_context context (r : record) :=
Build context r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_constants constants (r : record) :=
Build r.(context) constants r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_round_durations round_durations (r : record) :=
Build r.(context) r.(constants) round_durations r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_cycle_eras cycle_eras (r : record) :=
Build r.(context) r.(constants) r.(round_durations) cycle_eras r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_level level (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) level
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_predecessor_timestamp predecessor_timestamp (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
predecessor_timestamp r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_timestamp timestamp (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) timestamp r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_fees fees (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) fees r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_origination_nonce origination_nonce (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) origination_nonce
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_temporary_lazy_storage_ids temporary_lazy_storage_ids
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
temporary_lazy_storage_ids r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_internal_nonce internal_nonce (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) internal_nonce r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_internal_nonces_used internal_nonces_used (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) internal_nonces_used
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_remaining_block_gas remaining_block_gas (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
remaining_block_gas r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_unlimited_operation_gas unlimited_operation_gas
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) unlimited_operation_gas r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_consensus consensus (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) consensus
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_non_consensus_operations_rev non_consensus_operations_rev
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
non_consensus_operations_rev r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_sampler_state sampler_state (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) sampler_state
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_stake_distribution_for_current_cycle
stake_distribution_for_current_cycle (r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
stake_distribution_for_current_cycle r.(tx_rollup_current_messages)
r.(sc_rollup_current_messages).
Definition with_tx_rollup_current_messages tx_rollup_current_messages
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) tx_rollup_current_messages
r.(sc_rollup_current_messages).
Definition with_sc_rollup_current_messages sc_rollup_current_messages
(r : record) :=
Build r.(context) r.(constants) r.(round_durations) r.(cycle_eras) r.(level)
r.(predecessor_timestamp) r.(timestamp) r.(fees) r.(origination_nonce)
r.(temporary_lazy_storage_ids) r.(internal_nonce) r.(internal_nonces_used)
r.(remaining_block_gas) r.(unlimited_operation_gas) r.(consensus)
r.(non_consensus_operations_rev) r.(sampler_state)
r.(stake_distribution_for_current_cycle) r.(tx_rollup_current_messages)
sc_rollup_current_messages.
End back.
Definition back := back.record.
Module t.
Record record : Set := Build {
remaining_operation_gas : Gas_limit_repr.Arith.fp;
back : back;
}.
Definition with_remaining_operation_gas remaining_operation_gas
(r : record) :=
Build remaining_operation_gas r.(back).
Definition with_back back (r : record) :=
Build r.(remaining_operation_gas) back.
End t.
Definition t := t.record.
Definition root : Set := t.
Definition context_value (ctxt : t) : Context.t := ctxt.(t.back).(back.context).
Definition current_level (ctxt : t) : Level_repr.t :=
ctxt.(t.back).(back.level).
Definition predecessor_timestamp (ctxt : t) : Time.t :=
ctxt.(t.back).(back.predecessor_timestamp).
Definition current_timestamp (ctxt : t) : Time.t :=
ctxt.(t.back).(back.timestamp).
Definition round_durations (ctxt : t) : Round_repr.Durations.t :=
ctxt.(t.back).(back.round_durations).
Definition cycle_eras (ctxt : t) : Level_repr.cycle_eras :=
ctxt.(t.back).(back.cycle_eras).
Definition constants (ctxt : t) : Constants_repr.parametric :=
ctxt.(t.back).(back.constants).
Definition recover (ctxt : t) : Context.t := ctxt.(t.back).(back.context).
Definition fees (ctxt : t) : Tez_repr.t := ctxt.(t.back).(back.fees).
Definition origination_nonce (ctxt : t) : option Origination_nonce.t :=
ctxt.(t.back).(back.origination_nonce).
Definition internal_nonce (ctxt : t) : int :=
ctxt.(t.back).(back.internal_nonce).
Definition internal_nonces_used (ctxt : t) : Int_set.(_Set.S.t) :=
ctxt.(t.back).(back.internal_nonces_used).
Definition remaining_block_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
ctxt.(t.back).(back.remaining_block_gas).
Definition unlimited_operation_gas (ctxt : t) : bool :=
ctxt.(t.back).(back.unlimited_operation_gas).
Definition temporary_lazy_storage_ids (ctxt : t)
: Lazy_storage_kind.Temp_ids.t :=
ctxt.(t.back).(back.temporary_lazy_storage_ids).
Definition remaining_operation_gas (ctxt : t) : Gas_limit_repr.Arith.fp :=
ctxt.(t.remaining_operation_gas).
Definition non_consensus_operations_rev (ctxt : t) : list Operation_hash.t :=
ctxt.(t.back).(back.non_consensus_operations_rev).
Definition sampler_state (ctxt : t)
: Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) :=
ctxt.(t.back).(back.sampler_state).
Definition update_back (ctxt : t) (back : back) : t := t.with_back back ctxt.
Definition update_remaining_block_gas
(ctxt : t) (remaining_block_gas : Gas_limit_repr.Arith.fp) : t :=
update_back ctxt
(back.with_remaining_block_gas remaining_block_gas ctxt.(t.back)).
Definition update_remaining_operation_gas
(ctxt : t) (remaining_operation_gas : Gas_limit_repr.Arith.fp) : t :=
t.with_remaining_operation_gas remaining_operation_gas ctxt.
Definition update_unlimited_operation_gas
(ctxt : t) (unlimited_operation_gas : bool) : t :=
update_back ctxt
(back.with_unlimited_operation_gas unlimited_operation_gas ctxt.(t.back)).
Definition update_context (ctxt : t) (context_value : Context.t) : t :=
update_back ctxt (back.with_context context_value ctxt.(t.back)).
Definition update_constants (ctxt : t) (constants : Constants_repr.parametric)
: t := update_back ctxt (back.with_constants constants ctxt.(t.back)).
Definition update_origination_nonce
(ctxt : t) (origination_nonce : option Origination_nonce.t) : t :=
update_back ctxt (back.with_origination_nonce origination_nonce ctxt.(t.back)).
Definition update_internal_nonce (ctxt : t) (internal_nonce : int) : t :=
update_back ctxt (back.with_internal_nonce internal_nonce ctxt.(t.back)).
Definition update_internal_nonces_used
(ctxt : t) (internal_nonces_used : Int_set.(_Set.S.t)) : t :=
update_back ctxt
(back.with_internal_nonces_used internal_nonces_used ctxt.(t.back)).
Definition update_fees (ctxt : t) (fees : Tez_repr.t) : t :=
update_back ctxt (back.with_fees fees ctxt.(t.back)).
Definition update_temporary_lazy_storage_ids
(ctxt : t) (temporary_lazy_storage_ids : Lazy_storage_kind.Temp_ids.t) : t :=
update_back ctxt
(back.with_temporary_lazy_storage_ids temporary_lazy_storage_ids
ctxt.(t.back)).
Definition update_non_consensus_operations_rev
(ctxt : t) (non_consensus_operations_rev : list Operation_hash.t) : t :=
update_back ctxt
(back.with_non_consensus_operations_rev non_consensus_operations_rev
ctxt.(t.back)).
Definition update_sampler_state
(ctxt : t)
(sampler_state :
Cycle_repr.Map.(Map.S.t)
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash))) : t :=
update_back ctxt (back.with_sampler_state sampler_state ctxt.(t.back)).
Init function; without side-effects in Coq
Definition init_module2 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"too_many_internal_operations" "Too many internal operations"
"A transaction exceeded the hard limit of internal operations it can emit"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_many_internal_operations" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_many_internal_operations" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"gas_exhausted.operation" "Gas quota exceeded for the operation"
"A script or one of its callee took more time than the operation said it would"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Operation_quota_exceeded" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Operation_quota_exceeded" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary "gas_exhausted.block"
"Gas quota exceeded for the block"
"The sum of gas consumed by all the operations in the block exceeds the hard gas limit per block"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Block_quota_exceeded" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Block_quota_exceeded" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"delegate.stake_distribution_not_set" "Stake distribution not set"
"The stake distribution for the current cycle is not set."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The stake distribution for the current cycle is not set."
CamlinternalFormatBasics.End_of_format)
"The stake distribution for the current cycle is not set.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Stake_distribution_not_set" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Stake_distribution_not_set" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent "sampler_already_set"
"Sampler already set"
"Internal error: Raw_context.set_sampler_for_cycle was called twice for a given cycle"
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Cycle_repr.cycle) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Internal error: sampler already set for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Internal error: sampler already set for cycle %a.") Cycle_repr.pp
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "cycle" Cycle_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sampler_already_set" then
let c_value := cast Cycle_repr.t payload in
Some c_value
else None
end)
(fun (c_value : Cycle_repr.cycle) ⇒
Build_extensible "Sampler_already_set" Cycle_repr.cycle c_value).
Definition fresh_internal_nonce (ctxt : t) : M? (t × int) :=
if (internal_nonce ctxt) ≥i 65535 then
Error_monad.error_value
(Build_extensible "Too_many_internal_operations" unit tt)
else
return?
((update_internal_nonce ctxt ((internal_nonce ctxt) +i 1)),
(internal_nonce ctxt)).
Definition reset_internal_nonce (ctxt : t) : t :=
let ctxt := update_internal_nonce ctxt 0 in
update_internal_nonces_used ctxt Int_set.(_Set.S.empty).
Definition record_internal_nonce (ctxt : t) (k_value : Compare.Int.t) : t :=
update_internal_nonces_used ctxt
(Int_set.(_Set.S.add) k_value (internal_nonces_used ctxt)).
Definition internal_nonce_already_recorded (ctxt : t) (k_value : Compare.Int.t)
: bool := Int_set.(_Set.S.mem) k_value (internal_nonces_used ctxt).
Definition get_collected_fees (ctxt : t) : Tez_repr.t := fees ctxt.
Definition credit_collected_fees_only_call_from_token
(ctxt : t) (fees' : Tez_repr.t) : M? t :=
let previous := get_collected_fees ctxt in
let? fees := Tez_repr.op_plusquestion previous fees' in
return? (update_fees ctxt fees).
Definition spend_collected_fees_only_call_from_token
(ctxt : t) (fees' : Tez_repr.t) : M? t :=
let previous := get_collected_fees ctxt in
let? fees := Tez_repr.op_minusquestion previous fees' in
return? (update_fees ctxt fees).
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"too_many_internal_operations" "Too many internal operations"
"A transaction exceeded the hard limit of internal operations it can emit"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_many_internal_operations" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Too_many_internal_operations" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"gas_exhausted.operation" "Gas quota exceeded for the operation"
"A script or one of its callee took more time than the operation said it would"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Operation_quota_exceeded" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Operation_quota_exceeded" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary "gas_exhausted.block"
"Gas quota exceeded for the block"
"The sum of gas consumed by all the operations in the block exceeds the hard gas limit per block"
None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Block_quota_exceeded" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Block_quota_exceeded" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"delegate.stake_distribution_not_set" "Stake distribution not set"
"The stake distribution for the current cycle is not set."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The stake distribution for the current cycle is not set."
CamlinternalFormatBasics.End_of_format)
"The stake distribution for the current cycle is not set.")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Stake_distribution_not_set" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Stake_distribution_not_set" unit tt) in
Error_monad.register_error_kind Error_monad.Permanent "sampler_already_set"
"Sampler already set"
"Internal error: Raw_context.set_sampler_for_cycle was called twice for a given cycle"
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Cycle_repr.cycle) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Internal error: sampler already set for cycle "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Internal error: sampler already set for cycle %a.") Cycle_repr.pp
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "cycle" Cycle_repr.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sampler_already_set" then
let c_value := cast Cycle_repr.t payload in
Some c_value
else None
end)
(fun (c_value : Cycle_repr.cycle) ⇒
Build_extensible "Sampler_already_set" Cycle_repr.cycle c_value).
Definition fresh_internal_nonce (ctxt : t) : M? (t × int) :=
if (internal_nonce ctxt) ≥i 65535 then
Error_monad.error_value
(Build_extensible "Too_many_internal_operations" unit tt)
else
return?
((update_internal_nonce ctxt ((internal_nonce ctxt) +i 1)),
(internal_nonce ctxt)).
Definition reset_internal_nonce (ctxt : t) : t :=
let ctxt := update_internal_nonce ctxt 0 in
update_internal_nonces_used ctxt Int_set.(_Set.S.empty).
Definition record_internal_nonce (ctxt : t) (k_value : Compare.Int.t) : t :=
update_internal_nonces_used ctxt
(Int_set.(_Set.S.add) k_value (internal_nonces_used ctxt)).
Definition internal_nonce_already_recorded (ctxt : t) (k_value : Compare.Int.t)
: bool := Int_set.(_Set.S.mem) k_value (internal_nonces_used ctxt).
Definition get_collected_fees (ctxt : t) : Tez_repr.t := fees ctxt.
Definition credit_collected_fees_only_call_from_token
(ctxt : t) (fees' : Tez_repr.t) : M? t :=
let previous := get_collected_fees ctxt in
let? fees := Tez_repr.op_plusquestion previous fees' in
return? (update_fees ctxt fees).
Definition spend_collected_fees_only_call_from_token
(ctxt : t) (fees' : Tez_repr.t) : M? t :=
let previous := get_collected_fees ctxt in
let? fees := Tez_repr.op_minusquestion previous fees' in
return? (update_fees ctxt fees).
Init function; without side-effects in Coq
Definition init_module3 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"undefined_operation_nonce" "Ill timed access to the origination nonce"
"An origination was attempted out of the scope of a manager operation" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Undefined_operation_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Undefined_operation_nonce" unit tt).
Definition init_origination_nonce (ctxt : t) (operation_hash : Operation_hash.t)
: t :=
let origination_nonce := Some (Origination_nonce.initial operation_hash) in
update_origination_nonce ctxt origination_nonce.
Definition increment_origination_nonce (ctxt : t)
: M? (t × Origination_nonce.t) :=
match origination_nonce ctxt with
| None ⇒
Error_monad.error_value
(Build_extensible "Undefined_operation_nonce" unit tt)
| Some cur_origination_nonce ⇒
let origination_nonce := Some (Origination_nonce.incr cur_origination_nonce)
in
let ctxt := update_origination_nonce ctxt origination_nonce in
return? (ctxt, cur_origination_nonce)
end.
Definition get_origination_nonce (ctxt : t) : M? Origination_nonce.t :=
match origination_nonce ctxt with
| None ⇒
Error_monad.error_value
(Build_extensible "Undefined_operation_nonce" unit tt)
| Some origination_nonce ⇒ return? origination_nonce
end.
Definition unset_origination_nonce (ctxt : t) : t :=
update_origination_nonce ctxt None.
Error_monad.register_error_kind Error_monad.Permanent
"undefined_operation_nonce" "Ill timed access to the origination nonce"
"An origination was attempted out of the scope of a manager operation" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Undefined_operation_nonce" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Undefined_operation_nonce" unit tt).
Definition init_origination_nonce (ctxt : t) (operation_hash : Operation_hash.t)
: t :=
let origination_nonce := Some (Origination_nonce.initial operation_hash) in
update_origination_nonce ctxt origination_nonce.
Definition increment_origination_nonce (ctxt : t)
: M? (t × Origination_nonce.t) :=
match origination_nonce ctxt with
| None ⇒
Error_monad.error_value
(Build_extensible "Undefined_operation_nonce" unit tt)
| Some cur_origination_nonce ⇒
let origination_nonce := Some (Origination_nonce.incr cur_origination_nonce)
in
let ctxt := update_origination_nonce ctxt origination_nonce in
return? (ctxt, cur_origination_nonce)
end.
Definition get_origination_nonce (ctxt : t) : M? Origination_nonce.t :=
match origination_nonce ctxt with
| None ⇒
Error_monad.error_value
(Build_extensible "Undefined_operation_nonce" unit tt)
| Some origination_nonce ⇒ return? origination_nonce
end.
Definition unset_origination_nonce (ctxt : t) : t :=
update_origination_nonce ctxt None.
Init function; without side-effects in Coq
Definition init_module4 : unit :=
Error_monad.register_error_kind Error_monad.Permanent "gas_limit_too_high"
"Gas limit out of protocol hard bounds"
"A transaction tried to exceed the hard limit on gas" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_limit_too_high" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_limit_too_high" unit tt).
Definition gas_level (ctxt : t) : Gas_limit_repr.t :=
if unlimited_operation_gas ctxt then
Gas_limit_repr.Unaccounted
else
Gas_limit_repr.Limited
{| Gas_limit_repr.t.Limited.remaining := remaining_operation_gas ctxt; |}.
Definition block_gas_level : t → Gas_limit_repr.Arith.fp :=
remaining_block_gas.
Definition check_gas_limit_is_valid
(ctxt : t) (remaining : Gas_limit_repr.Arith.t) : M? unit :=
if
(Gas_limit_repr.Arith.op_gt remaining
(constants ctxt).(Constants_repr.parametric.hard_gas_limit_per_operation))
|| (Gas_limit_repr.Arith.op_lt remaining Gas_limit_repr.Arith.zero)
then
Error_monad.error_value (Build_extensible "Gas_limit_too_high" unit tt)
else
Result.return_unit.
Definition consume_gas_limit_in_block
(ctxt : t) (limit : Gas_limit_repr.Arith.t) : M? t :=
let? '_ := check_gas_limit_is_valid ctxt limit in
let block_gas := block_gas_level ctxt in
let limit := Gas_limit_repr.Arith.fp_value limit in
if Gas_limit_repr.Arith.op_gt limit block_gas then
Error_monad.error_value (Build_extensible "Block_quota_exceeded" unit tt)
else
let level := Gas_limit_repr.Arith.sub (block_gas_level ctxt) limit in
let ctxt := update_remaining_block_gas ctxt level in
Pervasives.Ok ctxt.
Definition set_gas_limit (ctxt : t) (remaining : Gas_limit_repr.Arith.t) : t :=
let remaining_operation_gas := Gas_limit_repr.Arith.fp_value remaining in
let ctxt := update_unlimited_operation_gas ctxt false in
t.with_remaining_operation_gas remaining_operation_gas ctxt.
Definition set_gas_unlimited (ctxt : t) : t :=
update_unlimited_operation_gas ctxt true.
Definition consume_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? t :=
match Gas_limit_repr.raw_consume (remaining_operation_gas ctxt) cost with
| Some gas_counter ⇒
Pervasives.Ok (update_remaining_operation_gas ctxt gas_counter)
| None ⇒
if unlimited_operation_gas ctxt then
return? ctxt
else
Error_monad.error_value
(Build_extensible "Operation_quota_exceeded" unit tt)
end.
Definition check_enough_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? unit :=
let? function_parameter := consume_gas ctxt cost in
let '_ := function_parameter in
Result.return_unit.
Definition gas_consumed (since : t) (until : t) : Gas_limit_repr.Arith.t :=
match ((gas_level since), (gas_level until)) with
|
(Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := before |},
Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := after |})
⇒ Gas_limit_repr.Arith.sub before after
| (_, _) ⇒ Gas_limit_repr.Arith.zero
end.
Inductive missing_key_kind : Set :=
| Get : missing_key_kind
| _Set : missing_key_kind
| Del : missing_key_kind
| Copy : missing_key_kind.
Inductive storage_error : Set :=
| Incompatible_protocol_version : string → storage_error
| Missing_key : list string → missing_key_kind → storage_error
| Existing_key : list string → storage_error
| Corrupted_data : list string → storage_error.
Definition storage_error_encoding : Data_encoding.encoding storage_error :=
Data_encoding.union None
[
Data_encoding.case_value "Incompatible_protocol_version" None
(Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "incompatible_protocol_version"
Data_encoding.string_value))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Incompatible_protocol_version arg ⇒ Some arg
| _ ⇒ None
end) (fun (arg : string) ⇒ Incompatible_protocol_version arg);
Data_encoding.case_value "Missing_key" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "missing_key"
(Data_encoding.list_value None Data_encoding.string_value))
(Data_encoding.req None None "function"
(Data_encoding.string_enum
[
("get", Get);
("set", _Set);
("del", Del);
("copy", Copy)
])))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Missing_key key_value f_value ⇒ Some (key_value, f_value)
| _ ⇒ None
end)
(fun (function_parameter : list string × missing_key_kind) ⇒
let '(key_value, f_value) := function_parameter in
Missing_key key_value f_value);
Data_encoding.case_value "Existing_key" None (Data_encoding.Tag 2)
(Data_encoding.obj1
(Data_encoding.req None None "existing_key"
(Data_encoding.list_value None Data_encoding.string_value)))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Existing_key key_value ⇒ Some key_value
| _ ⇒ None
end) (fun (key_value : list string) ⇒ Existing_key key_value);
Data_encoding.case_value "Corrupted_data" None (Data_encoding.Tag 3)
(Data_encoding.obj1
(Data_encoding.req None None "corrupted_data"
(Data_encoding.list_value None Data_encoding.string_value)))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Corrupted_data key_value ⇒ Some key_value
| _ ⇒ None
end) (fun (key_value : list string) ⇒ Corrupted_data key_value)
].
Definition pp_storage_error
(ppf : Format.formatter) (function_parameter : storage_error) : unit :=
match function_parameter with
| Incompatible_protocol_version version ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Found a context with an unexpected version '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Found a context with an unexpected version '%s'.") version
| Missing_key key_value Get ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Missing key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format))) "Missing key '%s'.")
(String.concat "/" key_value)
| Missing_key key_value _Set ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot set undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot set undefined key '%s'.") (String.concat "/" key_value)
| Missing_key key_value Del ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot delete undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot delete undefined key '%s'.") (String.concat "/" key_value)
| Missing_key key_value Copy ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot copy undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot copy undefined key '%s'.") (String.concat "/" key_value)
| Existing_key key_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot initialize defined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot initialize defined key '%s'.") (String.concat "/" key_value)
| Corrupted_data key_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Failed to parse the data at '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Failed to parse the data at '%s'.") (String.concat "/" key_value)
end.
Error_monad.register_error_kind Error_monad.Permanent "gas_limit_too_high"
"Gas limit out of protocol hard bounds"
"A transaction tried to exceed the hard limit on gas" None
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_limit_too_high" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_limit_too_high" unit tt).
Definition gas_level (ctxt : t) : Gas_limit_repr.t :=
if unlimited_operation_gas ctxt then
Gas_limit_repr.Unaccounted
else
Gas_limit_repr.Limited
{| Gas_limit_repr.t.Limited.remaining := remaining_operation_gas ctxt; |}.
Definition block_gas_level : t → Gas_limit_repr.Arith.fp :=
remaining_block_gas.
Definition check_gas_limit_is_valid
(ctxt : t) (remaining : Gas_limit_repr.Arith.t) : M? unit :=
if
(Gas_limit_repr.Arith.op_gt remaining
(constants ctxt).(Constants_repr.parametric.hard_gas_limit_per_operation))
|| (Gas_limit_repr.Arith.op_lt remaining Gas_limit_repr.Arith.zero)
then
Error_monad.error_value (Build_extensible "Gas_limit_too_high" unit tt)
else
Result.return_unit.
Definition consume_gas_limit_in_block
(ctxt : t) (limit : Gas_limit_repr.Arith.t) : M? t :=
let? '_ := check_gas_limit_is_valid ctxt limit in
let block_gas := block_gas_level ctxt in
let limit := Gas_limit_repr.Arith.fp_value limit in
if Gas_limit_repr.Arith.op_gt limit block_gas then
Error_monad.error_value (Build_extensible "Block_quota_exceeded" unit tt)
else
let level := Gas_limit_repr.Arith.sub (block_gas_level ctxt) limit in
let ctxt := update_remaining_block_gas ctxt level in
Pervasives.Ok ctxt.
Definition set_gas_limit (ctxt : t) (remaining : Gas_limit_repr.Arith.t) : t :=
let remaining_operation_gas := Gas_limit_repr.Arith.fp_value remaining in
let ctxt := update_unlimited_operation_gas ctxt false in
t.with_remaining_operation_gas remaining_operation_gas ctxt.
Definition set_gas_unlimited (ctxt : t) : t :=
update_unlimited_operation_gas ctxt true.
Definition consume_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? t :=
match Gas_limit_repr.raw_consume (remaining_operation_gas ctxt) cost with
| Some gas_counter ⇒
Pervasives.Ok (update_remaining_operation_gas ctxt gas_counter)
| None ⇒
if unlimited_operation_gas ctxt then
return? ctxt
else
Error_monad.error_value
(Build_extensible "Operation_quota_exceeded" unit tt)
end.
Definition check_enough_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M? unit :=
let? function_parameter := consume_gas ctxt cost in
let '_ := function_parameter in
Result.return_unit.
Definition gas_consumed (since : t) (until : t) : Gas_limit_repr.Arith.t :=
match ((gas_level since), (gas_level until)) with
|
(Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := before |},
Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := after |})
⇒ Gas_limit_repr.Arith.sub before after
| (_, _) ⇒ Gas_limit_repr.Arith.zero
end.
Inductive missing_key_kind : Set :=
| Get : missing_key_kind
| _Set : missing_key_kind
| Del : missing_key_kind
| Copy : missing_key_kind.
Inductive storage_error : Set :=
| Incompatible_protocol_version : string → storage_error
| Missing_key : list string → missing_key_kind → storage_error
| Existing_key : list string → storage_error
| Corrupted_data : list string → storage_error.
Definition storage_error_encoding : Data_encoding.encoding storage_error :=
Data_encoding.union None
[
Data_encoding.case_value "Incompatible_protocol_version" None
(Data_encoding.Tag 0)
(Data_encoding.obj1
(Data_encoding.req None None "incompatible_protocol_version"
Data_encoding.string_value))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Incompatible_protocol_version arg ⇒ Some arg
| _ ⇒ None
end) (fun (arg : string) ⇒ Incompatible_protocol_version arg);
Data_encoding.case_value "Missing_key" None (Data_encoding.Tag 1)
(Data_encoding.obj2
(Data_encoding.req None None "missing_key"
(Data_encoding.list_value None Data_encoding.string_value))
(Data_encoding.req None None "function"
(Data_encoding.string_enum
[
("get", Get);
("set", _Set);
("del", Del);
("copy", Copy)
])))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Missing_key key_value f_value ⇒ Some (key_value, f_value)
| _ ⇒ None
end)
(fun (function_parameter : list string × missing_key_kind) ⇒
let '(key_value, f_value) := function_parameter in
Missing_key key_value f_value);
Data_encoding.case_value "Existing_key" None (Data_encoding.Tag 2)
(Data_encoding.obj1
(Data_encoding.req None None "existing_key"
(Data_encoding.list_value None Data_encoding.string_value)))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Existing_key key_value ⇒ Some key_value
| _ ⇒ None
end) (fun (key_value : list string) ⇒ Existing_key key_value);
Data_encoding.case_value "Corrupted_data" None (Data_encoding.Tag 3)
(Data_encoding.obj1
(Data_encoding.req None None "corrupted_data"
(Data_encoding.list_value None Data_encoding.string_value)))
(fun (function_parameter : storage_error) ⇒
match function_parameter with
| Corrupted_data key_value ⇒ Some key_value
| _ ⇒ None
end) (fun (key_value : list string) ⇒ Corrupted_data key_value)
].
Definition pp_storage_error
(ppf : Format.formatter) (function_parameter : storage_error) : unit :=
match function_parameter with
| Incompatible_protocol_version version ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Found a context with an unexpected version '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Found a context with an unexpected version '%s'.") version
| Missing_key key_value Get ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Missing key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format))) "Missing key '%s'.")
(String.concat "/" key_value)
| Missing_key key_value _Set ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot set undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot set undefined key '%s'.") (String.concat "/" key_value)
| Missing_key key_value Del ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot delete undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot delete undefined key '%s'.") (String.concat "/" key_value)
| Missing_key key_value Copy ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Cannot copy undefined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot copy undefined key '%s'.") (String.concat "/" key_value)
| Existing_key key_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot initialize defined key '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Cannot initialize defined key '%s'.") (String.concat "/" key_value)
| Corrupted_data key_value ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Failed to parse the data at '"
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal "'."
CamlinternalFormatBasics.End_of_format)))
"Failed to parse the data at '%s'.") (String.concat "/" key_value)
end.
Init function; without side-effects in Coq
Definition init_module5 : unit :=
Error_monad.register_error_kind Error_monad.Permanent "context.storage_error"
"Storage error (fatal internal error)"
"An error that should never happen unless something has been deleted or corrupted in the database."
(Some
(fun (ppf : Format.formatter) ⇒
fun (err : storage_error) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "Storage error:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>Storage error:@ %a@]") pp_storage_error err))
storage_error_encoding
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Storage_error" then
let err := cast storage_error payload in
Some err
else None
end)
(fun (err : storage_error) ⇒
Build_extensible "Storage_error" storage_error err).
Definition storage_error_value {A : Set} (err : storage_error) : M? A :=
Error_monad.error_value (Build_extensible "Storage_error" storage_error err).
Definition version_key : list string := [ "version" ].
Definition version_value : string := "alpha_current".
Definition version : string := "v1".
Definition cycle_eras_key : list string := [ version; "cycle_eras" ].
Definition constants_key : list string := [ version; "constants" ].
Definition protocol_param_key : list string := [ "protocol_parameters" ].
Definition get_cycle_eras (ctxt : Context.t) : M? Level_repr.cycle_eras :=
let function_parameter := Context.find ctxt cycle_eras_key in
match function_parameter with
| None ⇒ storage_error_value (Missing_key cycle_eras_key Get)
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt Level_repr.cycle_eras_encoding
bytes_value with
| None ⇒ storage_error_value (Corrupted_data cycle_eras_key)
| Some cycle_eras ⇒ return? cycle_eras
end
end.
Definition set_cycle_eras {A : Set}
(ctxt : Context.t) (cycle_eras : Level_repr.cycle_eras)
: Pervasives.result Context.t A :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None Level_repr.cycle_eras_encoding
cycle_eras in
Error_monad.op_gtpipeeq (Context.add ctxt cycle_eras_key bytes_value)
Error_monad.ok.
Error_monad.register_error_kind Error_monad.Permanent "context.storage_error"
"Storage error (fatal internal error)"
"An error that should never happen unless something has been deleted or corrupted in the database."
(Some
(fun (ppf : Format.formatter) ⇒
fun (err : storage_error) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal "Storage error:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>Storage error:@ %a@]") pp_storage_error err))
storage_error_encoding
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Storage_error" then
let err := cast storage_error payload in
Some err
else None
end)
(fun (err : storage_error) ⇒
Build_extensible "Storage_error" storage_error err).
Definition storage_error_value {A : Set} (err : storage_error) : M? A :=
Error_monad.error_value (Build_extensible "Storage_error" storage_error err).
Definition version_key : list string := [ "version" ].
Definition version_value : string := "alpha_current".
Definition version : string := "v1".
Definition cycle_eras_key : list string := [ version; "cycle_eras" ].
Definition constants_key : list string := [ version; "constants" ].
Definition protocol_param_key : list string := [ "protocol_parameters" ].
Definition get_cycle_eras (ctxt : Context.t) : M? Level_repr.cycle_eras :=
let function_parameter := Context.find ctxt cycle_eras_key in
match function_parameter with
| None ⇒ storage_error_value (Missing_key cycle_eras_key Get)
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt Level_repr.cycle_eras_encoding
bytes_value with
| None ⇒ storage_error_value (Corrupted_data cycle_eras_key)
| Some cycle_eras ⇒ return? cycle_eras
end
end.
Definition set_cycle_eras {A : Set}
(ctxt : Context.t) (cycle_eras : Level_repr.cycle_eras)
: Pervasives.result Context.t A :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None Level_repr.cycle_eras_encoding
cycle_eras in
Error_monad.op_gtpipeeq (Context.add ctxt cycle_eras_key bytes_value)
Error_monad.ok.
Init function; without side-effects in Coq
Definition init_module6 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"context.failed_to_parse_parameter" "Failed to parse parameter"
"The protocol parameters are not valid JSON."
(Some
(fun (ppf : Format.formatter) ⇒
fun (bytes_value : Bytes.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal
"Cannot parse the protocol parameter:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>Cannot parse the protocol parameter:@ %s@]")
(Bytes.to_string bytes_value)))
(Data_encoding.obj1
(Data_encoding.req None None "contents" Data_encoding.bytes_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_parse_parameter" then
let data := cast bytes payload in
Some data
else None
end)
(fun (data : Bytes.t) ⇒
Build_extensible "Failed_to_parse_parameter" Bytes.t data) in
Error_monad.register_error_kind Error_monad.Temporary
"context.failed_to_decode_parameter" "Failed to decode parameter"
"Unexpected JSON object."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Data_encoding.json × string) ⇒
let '(json_value, msg) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal
"Cannot decode the protocol parameter:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[<v 2>Cannot decode the protocol parameter:@ %s@ %a@]") msg
Data_encoding.Json.pp json_value))
(Data_encoding.obj2
(Data_encoding.req None None "contents" Data_encoding.json_value)
(Data_encoding.req None None "error" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_decode_parameter" then
let '(json_value, msg) :=
cast (Data_encoding.json × string) payload in
Some (json_value, msg)
else None
end)
(fun (function_parameter : Data_encoding.json × string) ⇒
let '(json_value, msg) := function_parameter in
Build_extensible "Failed_to_decode_parameter"
(Data_encoding.json × string) (json_value, msg)).
Definition get_proto_param (ctxt : Context.t)
: M? (Parameters_repr.t × Context.t) :=
let function_parameter := Context.find ctxt protocol_param_key in
match function_parameter with
| None ⇒ Pervasives.failwith "Missing protocol parameters."
| Some bytes_value ⇒
match Data_encoding.Binary.of_bytes_opt Data_encoding.json_value bytes_value
with
| None ⇒
Error_monad.fail
(Build_extensible "Failed_to_parse_parameter" Context.value bytes_value)
| Some json_value ⇒
let ctxt := Context.remove ctxt protocol_param_key in
let 'param :=
Data_encoding.Json.destruct None Parameters_repr.encoding json_value in
let? '_ := Parameters_repr.check_params param in
return? (param, ctxt)
end
end.
Definition add_constants
(ctxt : Context.t) (constants : Constants_repr.parametric) : Context.t :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None Constants_repr.parametric_encoding
constants in
Context.add ctxt constants_key bytes_value.
Definition get_constants {A : Set} (ctxt : Context.t)
: Pervasives.result Constants_repr.parametric A :=
let function_parameter := Context.find ctxt constants_key in
match function_parameter with
| None ⇒
Pervasives.failwith "Internal error: cannot read constants in context."
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt Constants_repr.parametric_encoding
bytes_value with
| None ⇒
Pervasives.failwith "Internal error: cannot parse constants in context."
| Some constants ⇒ return? constants
end
end.
Definition patch_constants
(ctxt : t) (f_value : Constants_repr.parametric → Constants_repr.parametric)
: t :=
let constants := f_value (constants ctxt) in
let context_value := add_constants (context_value ctxt) constants in
let ctxt := update_context ctxt context_value in
update_constants ctxt constants.
Definition check_inited (ctxt : Context.t) : M? unit :=
let function_parameter := Context.find ctxt version_key in
match function_parameter with
| None ⇒ Pervasives.failwith "Internal error: un-initialized context."
| Some bytes_value ⇒
let s_value := Bytes.to_string bytes_value in
if Compare.String.(Compare.S.op_eq) s_value version_value then
Result.return_unit
else
storage_error_value (Incompatible_protocol_version s_value)
end.
Definition check_cycle_eras
(cycle_eras : Level_repr.cycle_eras) (constants : Constants_repr.parametric)
: unit :=
let current_era := Level_repr.current_era cycle_eras in
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(current_era.(Level_repr.cycle_era.blocks_per_cycle) =i32
constants.(Constants_repr.parametric.blocks_per_cycle)) in
(* ❌ Assert instruction is not handled. *)
assert unit
(current_era.(Level_repr.cycle_era.blocks_per_commitment) =i32
constants.(Constants_repr.parametric.blocks_per_commitment)).
Definition prepare
(level : int32) (predecessor_timestamp : Time.t) (timestamp : Time.t)
(ctxt : Context.t) : M? t :=
let? level := Raw_level_repr.of_int32 level in
let? '_ := check_inited ctxt in
let? constants := get_constants ctxt in
let? round_durations :=
Round_repr.Durations.create
constants.(Constants_repr.parametric.minimal_block_delay)
constants.(Constants_repr.parametric.delay_increment_per_round) in
let? cycle_eras := get_cycle_eras ctxt in
let '_ := check_cycle_eras cycle_eras constants in
let level := Level_repr.level_from_raw cycle_eras level in
return?
{| t.remaining_operation_gas := Gas_limit_repr.Arith.zero;
t.back :=
{| back.context := ctxt; back.constants := constants;
back.round_durations := round_durations;
back.cycle_eras := cycle_eras; back.level := level;
back.predecessor_timestamp := predecessor_timestamp;
back.timestamp := timestamp; back.fees := Tez_repr.zero;
back.origination_nonce := None;
back.temporary_lazy_storage_ids :=
Lazy_storage_kind.Temp_ids.init_value; back.internal_nonce := 0;
back.internal_nonces_used := Int_set.(_Set.S.empty);
back.remaining_block_gas :=
Gas_limit_repr.Arith.fp_value
constants.(Constants_repr.parametric.hard_gas_limit_per_block);
back.unlimited_operation_gas := true;
back.consensus := Raw_consensus.empty;
back.non_consensus_operations_rev := nil;
back.sampler_state := Cycle_repr.Map.(Map.S.empty);
back.stake_distribution_for_current_cycle := None;
back.tx_rollup_current_messages := Tx_rollup_repr.Map.(Map.S.empty);
back.sc_rollup_current_messages :=
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.empty); |}; |}.
Inductive previous_protocol : Set :=
| Genesis : Parameters_repr.t → previous_protocol
| Ithaca_012 : previous_protocol.
Definition check_and_update_protocol_version (ctxt : Context.t)
: M? (previous_protocol × Context.t) :=
let? '(previous_proto, ctxt) :=
let function_parameter := Context.find ctxt version_key in
match function_parameter with
| None ⇒
Pervasives.failwith
"Internal error: un-initialized context in check_first_block."
| Some bytes_value ⇒
let s_value := Bytes.to_string bytes_value in
if Compare.String.(Compare.S.op_eq) s_value version_value then
Pervasives.failwith "Internal error: previously initialized context."
else
if Compare.String.(Compare.S.op_eq) s_value "genesis" then
let? '(param, ctxt) := get_proto_param ctxt in
return? ((Genesis param), ctxt)
else
if Compare.String.(Compare.S.op_eq) s_value "ithaca_012" then
return? (Ithaca_012, ctxt)
else
storage_error_value (Incompatible_protocol_version s_value)
end in
let ctxt := Context.add ctxt version_key (Bytes.of_string version_value) in
return? (previous_proto, ctxt).
Definition get_previous_protocol_constants (ctxt : Context.t)
: Constants_repr.Proto_previous.parametric :=
let function_parameter := Context.find ctxt constants_key in
match function_parameter with
| None ⇒
Pervasives.failwith
"Internal error: cannot read previous protocol constants in context."
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt
Constants_repr.Proto_previous.parametric_encoding bytes_value with
| None ⇒
Pervasives.failwith
"Internal error: cannot parse previous protocol constants in context."
| Some constants ⇒ constants
end
end.
Definition prepare_first_block
(level : int32) (timestamp : Time.t) (ctxt : Context.t)
: M? (previous_protocol × t) :=
let? '(previous_proto, ctxt) := check_and_update_protocol_version ctxt in
let? ctxt :=
match previous_proto with
| Genesis param ⇒
let? first_level := Raw_level_repr.of_int32 level in
let cycle_era :=
{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := Cycle_repr.root_value;
Level_repr.cycle_era.blocks_per_cycle :=
param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_cycle);
Level_repr.cycle_era.blocks_per_commitment :=
param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_commitment);
|} in
let? cycle_eras := Level_repr.create_cycle_eras [ cycle_era ] in
let? ctxt := set_cycle_eras ctxt cycle_eras in
Error_monad.op_gtpipeeq
(add_constants ctxt param.(Parameters_repr.t.constants)) Error_monad.ok
| Ithaca_012 ⇒
let c_value := get_previous_protocol_constants ctxt in
let cycles_per_voting_period :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_voting_period)
/i32 c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle)
in
let tx_rollup_finality_period := 60000 in
let constants :=
{|
Constants_repr.parametric.preserved_cycles :=
c_value.(Constants_repr.Proto_previous.parametric.preserved_cycles);
Constants_repr.parametric.blocks_per_cycle :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle);
Constants_repr.parametric.blocks_per_commitment :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_commitment);
Constants_repr.parametric.blocks_per_stake_snapshot :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_stake_snapshot);
Constants_repr.parametric.cycles_per_voting_period :=
cycles_per_voting_period;
Constants_repr.parametric.hard_gas_limit_per_operation :=
c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_operation);
Constants_repr.parametric.hard_gas_limit_per_block :=
c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_block);
Constants_repr.parametric.proof_of_work_threshold :=
c_value.(Constants_repr.Proto_previous.parametric.proof_of_work_threshold);
Constants_repr.parametric.tokens_per_roll :=
c_value.(Constants_repr.Proto_previous.parametric.tokens_per_roll);
Constants_repr.parametric.seed_nonce_revelation_tip :=
c_value.(Constants_repr.Proto_previous.parametric.seed_nonce_revelation_tip);
Constants_repr.parametric.origination_size :=
c_value.(Constants_repr.Proto_previous.parametric.origination_size);
Constants_repr.parametric.baking_reward_fixed_portion :=
c_value.(Constants_repr.Proto_previous.parametric.baking_reward_fixed_portion);
Constants_repr.parametric.baking_reward_bonus_per_slot :=
c_value.(Constants_repr.Proto_previous.parametric.baking_reward_bonus_per_slot);
Constants_repr.parametric.endorsing_reward_per_slot :=
c_value.(Constants_repr.Proto_previous.parametric.endorsing_reward_per_slot);
Constants_repr.parametric.cost_per_byte :=
c_value.(Constants_repr.Proto_previous.parametric.cost_per_byte);
Constants_repr.parametric.hard_storage_limit_per_operation :=
c_value.(Constants_repr.Proto_previous.parametric.hard_storage_limit_per_operation);
Constants_repr.parametric.quorum_min :=
c_value.(Constants_repr.Proto_previous.parametric.quorum_min);
Constants_repr.parametric.quorum_max :=
c_value.(Constants_repr.Proto_previous.parametric.quorum_max);
Constants_repr.parametric.min_proposal_quorum :=
c_value.(Constants_repr.Proto_previous.parametric.min_proposal_quorum);
Constants_repr.parametric.liquidity_baking_subsidy :=
c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_subsidy);
Constants_repr.parametric.liquidity_baking_sunset_level :=
c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_sunset_level);
Constants_repr.parametric.liquidity_baking_toggle_ema_threshold :=
1000000000;
Constants_repr.parametric.max_operations_time_to_live :=
c_value.(Constants_repr.Proto_previous.parametric.max_operations_time_to_live);
Constants_repr.parametric.minimal_block_delay :=
c_value.(Constants_repr.Proto_previous.parametric.minimal_block_delay);
Constants_repr.parametric.delay_increment_per_round :=
c_value.(Constants_repr.Proto_previous.parametric.delay_increment_per_round);
Constants_repr.parametric.minimal_participation_ratio :=
c_value.(Constants_repr.Proto_previous.parametric.minimal_participation_ratio);
Constants_repr.parametric.consensus_committee_size :=
c_value.(Constants_repr.Proto_previous.parametric.consensus_committee_size);
Constants_repr.parametric.consensus_threshold :=
c_value.(Constants_repr.Proto_previous.parametric.consensus_threshold);
Constants_repr.parametric.max_slashing_period :=
c_value.(Constants_repr.Proto_previous.parametric.max_slashing_period);
Constants_repr.parametric.frozen_deposits_percentage :=
c_value.(Constants_repr.Proto_previous.parametric.frozen_deposits_percentage);
Constants_repr.parametric.double_baking_punishment :=
c_value.(Constants_repr.Proto_previous.parametric.double_baking_punishment);
Constants_repr.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement
:=
c_value.(Constants_repr.Proto_previous.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement);
Constants_repr.parametric.initial_seed := None;
Constants_repr.parametric.cache_script_size := 100000000;
Constants_repr.parametric.cache_stake_distribution_cycles := 8;
Constants_repr.parametric.cache_sampler_state_cycles := 8;
Constants_repr.parametric.tx_rollup_enable := true;
Constants_repr.parametric.tx_rollup_origination_size := 60000;
Constants_repr.parametric.tx_rollup_hard_size_limit_per_inbox :=
100000;
Constants_repr.parametric.tx_rollup_hard_size_limit_per_message :=
5000;
Constants_repr.parametric.tx_rollup_commitment_bond :=
Tez_repr.of_mutez_exn 10000000000;
Constants_repr.parametric.tx_rollup_finality_period :=
tx_rollup_finality_period;
Constants_repr.parametric.tx_rollup_withdraw_period :=
tx_rollup_finality_period;
Constants_repr.parametric.tx_rollup_max_inboxes_count :=
tx_rollup_finality_period +i 100;
Constants_repr.parametric.tx_rollup_max_messages_per_inbox := 1010;
Constants_repr.parametric.tx_rollup_max_commitments_count :=
(2 ×i tx_rollup_finality_period) +i 100;
Constants_repr.parametric.tx_rollup_cost_per_byte_ema_factor := 120;
Constants_repr.parametric.tx_rollup_max_ticket_payload_size := 2048;
Constants_repr.parametric.tx_rollup_max_withdrawals_per_batch := 15;
Constants_repr.parametric.tx_rollup_rejection_max_proof_size := 30000;
Constants_repr.parametric.tx_rollup_sunset_level := 3473409;
Constants_repr.parametric.sc_rollup_enable := false;
Constants_repr.parametric.sc_rollup_origination_size := 6314;
Constants_repr.parametric.sc_rollup_challenge_window_in_blocks :=
20160;
Constants_repr.parametric.sc_rollup_max_available_messages := 1000000;
|} in
let ctxt := add_constants ctxt constants in
return? ctxt
end in
let? ctxt := prepare level timestamp timestamp ctxt in
return? (previous_proto, ctxt).
Definition activate (ctxt : t) (h_value : Protocol_hash.t) : t :=
Error_monad.op_gtpipeeq (Updater.activate (context_value ctxt) h_value)
(update_context ctxt).
Definition key : Set := list string.
Definition value : Set := bytes.
Definition tree : Set := Context.tree.
Definition T {t : Set} : Set :=
Raw_context_intf.T (root := root) (t := t) (tree := tree).
Definition mem (ctxt : t) (k_value : Context.key) : bool :=
Context.mem (context_value ctxt) k_value.
Definition mem_tree (ctxt : t) (k_value : Context.key) : bool :=
Context.mem_tree (context_value ctxt) k_value.
Definition get (ctxt : t) (k_value : Context.key) : M? Context.value :=
let function_parameter := Context.find (context_value ctxt) k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition get_tree (ctxt : t) (k_value : Context.key) : M? Context.tree :=
let function_parameter := Context.find_tree (context_value ctxt) k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition find (ctxt : t) (k_value : Context.key) : option Context.value :=
Context.find (context_value ctxt) k_value.
Definition find_tree (ctxt : t) (k_value : Context.key) : option Context.tree :=
Context.find_tree (context_value ctxt) k_value.
Definition add (ctxt : t) (k_value : Context.key) (v_value : Context.value)
: t :=
Error_monad.op_gtpipeeq (Context.add (context_value ctxt) k_value v_value)
(update_context ctxt).
Definition add_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
: t :=
Error_monad.op_gtpipeeq
(Context.add_tree (context_value ctxt) k_value v_value)
(update_context ctxt).
Definition init_value
(ctxt : t) (k_value : Context.key) (v_value : Context.value) : M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
let context_value := Context.add (context_value ctxt) k_value v_value in
return? (update_context ctxt context_value)
end.
Definition init_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
: M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
let context_value := Context.add_tree (context_value ctxt) k_value v_value
in
return? (update_context ctxt context_value)
end.
Definition update (ctxt : t) (k_value : Context.key) (v_value : Context.value)
: M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
let context_value := Context.add (context_value ctxt) k_value v_value in
return? (update_context ctxt context_value)
end.
Definition update_tree
(ctxt : t) (k_value : Context.key) (v_value : Context.tree) : M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
let context_value := Context.add_tree (context_value ctxt) k_value v_value
in
return? (update_context ctxt context_value)
end.
Definition remove_existing (ctxt : t) (k_value : Context.key) : M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒
let context_value := Context.remove (context_value ctxt) k_value in
return? (update_context ctxt context_value)
end.
Definition remove_existing_tree (ctxt : t) (k_value : Context.key) : M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒
let context_value := Context.remove (context_value ctxt) k_value in
return? (update_context ctxt context_value)
end.
Definition remove (ctxt : t) (k_value : Context.key) : t :=
Error_monad.op_gtpipeeq (Context.remove (context_value ctxt) k_value)
(update_context ctxt).
Definition add_or_remove
(ctxt : t) (k_value : Context.key) (function_parameter : option Context.value)
: t :=
match function_parameter with
| None ⇒ remove ctxt k_value
| Some v_value ⇒ add ctxt k_value v_value
end.
Definition add_or_remove_tree
(ctxt : t) (k_value : Context.key) (function_parameter : option Context.tree)
: t :=
match function_parameter with
| None ⇒ remove ctxt k_value
| Some v_value ⇒ add_tree ctxt k_value v_value
end.
Definition list_value
(ctxt : t) (offset : option int) (length : option int) (k_value : Context.key)
: list (string × Context.tree) :=
Context.list_value (context_value ctxt) offset length k_value.
Definition fold {A : Set}
(depth : option Context.depth) (ctxt : t) (k_value : Context.key)
(order : Variant.t) (init_value : A)
(f_value : Context.key → Context.tree → A → A) : A :=
Context.fold depth (context_value ctxt) k_value order init_value f_value.
Definition config_value (ctxt : t) : Context.config :=
Context.config_value (context_value ctxt).
Module Tree.
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"context.failed_to_parse_parameter" "Failed to parse parameter"
"The protocol parameters are not valid JSON."
(Some
(fun (ppf : Format.formatter) ⇒
fun (bytes_value : Bytes.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal
"Cannot parse the protocol parameter:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))
"@[<v 2>Cannot parse the protocol parameter:@ %s@]")
(Bytes.to_string bytes_value)))
(Data_encoding.obj1
(Data_encoding.req None None "contents" Data_encoding.bytes_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_parse_parameter" then
let data := cast bytes payload in
Some data
else None
end)
(fun (data : Bytes.t) ⇒
Build_extensible "Failed_to_parse_parameter" Bytes.t data) in
Error_monad.register_error_kind Error_monad.Temporary
"context.failed_to_decode_parameter" "Failed to decode parameter"
"Unexpected JSON object."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Data_encoding.json × string) ⇒
let '(json_value, msg) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Formatting_gen
(CamlinternalFormatBasics.Open_box
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "<v 2>"
CamlinternalFormatBasics.End_of_format) "<v 2>"))
(CamlinternalFormatBasics.String_literal
"Cannot decode the protocol parameter:"
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Formatting_lit
(CamlinternalFormatBasics.Break "@ " 1 0)
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Formatting_lit
CamlinternalFormatBasics.Close_box
CamlinternalFormatBasics.End_of_format)))))))
"@[<v 2>Cannot decode the protocol parameter:@ %s@ %a@]") msg
Data_encoding.Json.pp json_value))
(Data_encoding.obj2
(Data_encoding.req None None "contents" Data_encoding.json_value)
(Data_encoding.req None None "error" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failed_to_decode_parameter" then
let '(json_value, msg) :=
cast (Data_encoding.json × string) payload in
Some (json_value, msg)
else None
end)
(fun (function_parameter : Data_encoding.json × string) ⇒
let '(json_value, msg) := function_parameter in
Build_extensible "Failed_to_decode_parameter"
(Data_encoding.json × string) (json_value, msg)).
Definition get_proto_param (ctxt : Context.t)
: M? (Parameters_repr.t × Context.t) :=
let function_parameter := Context.find ctxt protocol_param_key in
match function_parameter with
| None ⇒ Pervasives.failwith "Missing protocol parameters."
| Some bytes_value ⇒
match Data_encoding.Binary.of_bytes_opt Data_encoding.json_value bytes_value
with
| None ⇒
Error_monad.fail
(Build_extensible "Failed_to_parse_parameter" Context.value bytes_value)
| Some json_value ⇒
let ctxt := Context.remove ctxt protocol_param_key in
let 'param :=
Data_encoding.Json.destruct None Parameters_repr.encoding json_value in
let? '_ := Parameters_repr.check_params param in
return? (param, ctxt)
end
end.
Definition add_constants
(ctxt : Context.t) (constants : Constants_repr.parametric) : Context.t :=
let bytes_value :=
Data_encoding.Binary.to_bytes_exn None Constants_repr.parametric_encoding
constants in
Context.add ctxt constants_key bytes_value.
Definition get_constants {A : Set} (ctxt : Context.t)
: Pervasives.result Constants_repr.parametric A :=
let function_parameter := Context.find ctxt constants_key in
match function_parameter with
| None ⇒
Pervasives.failwith "Internal error: cannot read constants in context."
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt Constants_repr.parametric_encoding
bytes_value with
| None ⇒
Pervasives.failwith "Internal error: cannot parse constants in context."
| Some constants ⇒ return? constants
end
end.
Definition patch_constants
(ctxt : t) (f_value : Constants_repr.parametric → Constants_repr.parametric)
: t :=
let constants := f_value (constants ctxt) in
let context_value := add_constants (context_value ctxt) constants in
let ctxt := update_context ctxt context_value in
update_constants ctxt constants.
Definition check_inited (ctxt : Context.t) : M? unit :=
let function_parameter := Context.find ctxt version_key in
match function_parameter with
| None ⇒ Pervasives.failwith "Internal error: un-initialized context."
| Some bytes_value ⇒
let s_value := Bytes.to_string bytes_value in
if Compare.String.(Compare.S.op_eq) s_value version_value then
Result.return_unit
else
storage_error_value (Incompatible_protocol_version s_value)
end.
Definition check_cycle_eras
(cycle_eras : Level_repr.cycle_eras) (constants : Constants_repr.parametric)
: unit :=
let current_era := Level_repr.current_era cycle_eras in
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit
(current_era.(Level_repr.cycle_era.blocks_per_cycle) =i32
constants.(Constants_repr.parametric.blocks_per_cycle)) in
(* ❌ Assert instruction is not handled. *)
assert unit
(current_era.(Level_repr.cycle_era.blocks_per_commitment) =i32
constants.(Constants_repr.parametric.blocks_per_commitment)).
Definition prepare
(level : int32) (predecessor_timestamp : Time.t) (timestamp : Time.t)
(ctxt : Context.t) : M? t :=
let? level := Raw_level_repr.of_int32 level in
let? '_ := check_inited ctxt in
let? constants := get_constants ctxt in
let? round_durations :=
Round_repr.Durations.create
constants.(Constants_repr.parametric.minimal_block_delay)
constants.(Constants_repr.parametric.delay_increment_per_round) in
let? cycle_eras := get_cycle_eras ctxt in
let '_ := check_cycle_eras cycle_eras constants in
let level := Level_repr.level_from_raw cycle_eras level in
return?
{| t.remaining_operation_gas := Gas_limit_repr.Arith.zero;
t.back :=
{| back.context := ctxt; back.constants := constants;
back.round_durations := round_durations;
back.cycle_eras := cycle_eras; back.level := level;
back.predecessor_timestamp := predecessor_timestamp;
back.timestamp := timestamp; back.fees := Tez_repr.zero;
back.origination_nonce := None;
back.temporary_lazy_storage_ids :=
Lazy_storage_kind.Temp_ids.init_value; back.internal_nonce := 0;
back.internal_nonces_used := Int_set.(_Set.S.empty);
back.remaining_block_gas :=
Gas_limit_repr.Arith.fp_value
constants.(Constants_repr.parametric.hard_gas_limit_per_block);
back.unlimited_operation_gas := true;
back.consensus := Raw_consensus.empty;
back.non_consensus_operations_rev := nil;
back.sampler_state := Cycle_repr.Map.(Map.S.empty);
back.stake_distribution_for_current_cycle := None;
back.tx_rollup_current_messages := Tx_rollup_repr.Map.(Map.S.empty);
back.sc_rollup_current_messages :=
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.empty); |}; |}.
Inductive previous_protocol : Set :=
| Genesis : Parameters_repr.t → previous_protocol
| Ithaca_012 : previous_protocol.
Definition check_and_update_protocol_version (ctxt : Context.t)
: M? (previous_protocol × Context.t) :=
let? '(previous_proto, ctxt) :=
let function_parameter := Context.find ctxt version_key in
match function_parameter with
| None ⇒
Pervasives.failwith
"Internal error: un-initialized context in check_first_block."
| Some bytes_value ⇒
let s_value := Bytes.to_string bytes_value in
if Compare.String.(Compare.S.op_eq) s_value version_value then
Pervasives.failwith "Internal error: previously initialized context."
else
if Compare.String.(Compare.S.op_eq) s_value "genesis" then
let? '(param, ctxt) := get_proto_param ctxt in
return? ((Genesis param), ctxt)
else
if Compare.String.(Compare.S.op_eq) s_value "ithaca_012" then
return? (Ithaca_012, ctxt)
else
storage_error_value (Incompatible_protocol_version s_value)
end in
let ctxt := Context.add ctxt version_key (Bytes.of_string version_value) in
return? (previous_proto, ctxt).
Definition get_previous_protocol_constants (ctxt : Context.t)
: Constants_repr.Proto_previous.parametric :=
let function_parameter := Context.find ctxt constants_key in
match function_parameter with
| None ⇒
Pervasives.failwith
"Internal error: cannot read previous protocol constants in context."
| Some bytes_value ⇒
match
Data_encoding.Binary.of_bytes_opt
Constants_repr.Proto_previous.parametric_encoding bytes_value with
| None ⇒
Pervasives.failwith
"Internal error: cannot parse previous protocol constants in context."
| Some constants ⇒ constants
end
end.
Definition prepare_first_block
(level : int32) (timestamp : Time.t) (ctxt : Context.t)
: M? (previous_protocol × t) :=
let? '(previous_proto, ctxt) := check_and_update_protocol_version ctxt in
let? ctxt :=
match previous_proto with
| Genesis param ⇒
let? first_level := Raw_level_repr.of_int32 level in
let cycle_era :=
{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := Cycle_repr.root_value;
Level_repr.cycle_era.blocks_per_cycle :=
param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_cycle);
Level_repr.cycle_era.blocks_per_commitment :=
param.(Parameters_repr.t.constants).(Constants_repr.parametric.blocks_per_commitment);
|} in
let? cycle_eras := Level_repr.create_cycle_eras [ cycle_era ] in
let? ctxt := set_cycle_eras ctxt cycle_eras in
Error_monad.op_gtpipeeq
(add_constants ctxt param.(Parameters_repr.t.constants)) Error_monad.ok
| Ithaca_012 ⇒
let c_value := get_previous_protocol_constants ctxt in
let cycles_per_voting_period :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_voting_period)
/i32 c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle)
in
let tx_rollup_finality_period := 60000 in
let constants :=
{|
Constants_repr.parametric.preserved_cycles :=
c_value.(Constants_repr.Proto_previous.parametric.preserved_cycles);
Constants_repr.parametric.blocks_per_cycle :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_cycle);
Constants_repr.parametric.blocks_per_commitment :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_commitment);
Constants_repr.parametric.blocks_per_stake_snapshot :=
c_value.(Constants_repr.Proto_previous.parametric.blocks_per_stake_snapshot);
Constants_repr.parametric.cycles_per_voting_period :=
cycles_per_voting_period;
Constants_repr.parametric.hard_gas_limit_per_operation :=
c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_operation);
Constants_repr.parametric.hard_gas_limit_per_block :=
c_value.(Constants_repr.Proto_previous.parametric.hard_gas_limit_per_block);
Constants_repr.parametric.proof_of_work_threshold :=
c_value.(Constants_repr.Proto_previous.parametric.proof_of_work_threshold);
Constants_repr.parametric.tokens_per_roll :=
c_value.(Constants_repr.Proto_previous.parametric.tokens_per_roll);
Constants_repr.parametric.seed_nonce_revelation_tip :=
c_value.(Constants_repr.Proto_previous.parametric.seed_nonce_revelation_tip);
Constants_repr.parametric.origination_size :=
c_value.(Constants_repr.Proto_previous.parametric.origination_size);
Constants_repr.parametric.baking_reward_fixed_portion :=
c_value.(Constants_repr.Proto_previous.parametric.baking_reward_fixed_portion);
Constants_repr.parametric.baking_reward_bonus_per_slot :=
c_value.(Constants_repr.Proto_previous.parametric.baking_reward_bonus_per_slot);
Constants_repr.parametric.endorsing_reward_per_slot :=
c_value.(Constants_repr.Proto_previous.parametric.endorsing_reward_per_slot);
Constants_repr.parametric.cost_per_byte :=
c_value.(Constants_repr.Proto_previous.parametric.cost_per_byte);
Constants_repr.parametric.hard_storage_limit_per_operation :=
c_value.(Constants_repr.Proto_previous.parametric.hard_storage_limit_per_operation);
Constants_repr.parametric.quorum_min :=
c_value.(Constants_repr.Proto_previous.parametric.quorum_min);
Constants_repr.parametric.quorum_max :=
c_value.(Constants_repr.Proto_previous.parametric.quorum_max);
Constants_repr.parametric.min_proposal_quorum :=
c_value.(Constants_repr.Proto_previous.parametric.min_proposal_quorum);
Constants_repr.parametric.liquidity_baking_subsidy :=
c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_subsidy);
Constants_repr.parametric.liquidity_baking_sunset_level :=
c_value.(Constants_repr.Proto_previous.parametric.liquidity_baking_sunset_level);
Constants_repr.parametric.liquidity_baking_toggle_ema_threshold :=
1000000000;
Constants_repr.parametric.max_operations_time_to_live :=
c_value.(Constants_repr.Proto_previous.parametric.max_operations_time_to_live);
Constants_repr.parametric.minimal_block_delay :=
c_value.(Constants_repr.Proto_previous.parametric.minimal_block_delay);
Constants_repr.parametric.delay_increment_per_round :=
c_value.(Constants_repr.Proto_previous.parametric.delay_increment_per_round);
Constants_repr.parametric.minimal_participation_ratio :=
c_value.(Constants_repr.Proto_previous.parametric.minimal_participation_ratio);
Constants_repr.parametric.consensus_committee_size :=
c_value.(Constants_repr.Proto_previous.parametric.consensus_committee_size);
Constants_repr.parametric.consensus_threshold :=
c_value.(Constants_repr.Proto_previous.parametric.consensus_threshold);
Constants_repr.parametric.max_slashing_period :=
c_value.(Constants_repr.Proto_previous.parametric.max_slashing_period);
Constants_repr.parametric.frozen_deposits_percentage :=
c_value.(Constants_repr.Proto_previous.parametric.frozen_deposits_percentage);
Constants_repr.parametric.double_baking_punishment :=
c_value.(Constants_repr.Proto_previous.parametric.double_baking_punishment);
Constants_repr.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement
:=
c_value.(Constants_repr.Proto_previous.parametric.ratio_of_frozen_deposits_slashed_per_double_endorsement);
Constants_repr.parametric.initial_seed := None;
Constants_repr.parametric.cache_script_size := 100000000;
Constants_repr.parametric.cache_stake_distribution_cycles := 8;
Constants_repr.parametric.cache_sampler_state_cycles := 8;
Constants_repr.parametric.tx_rollup_enable := true;
Constants_repr.parametric.tx_rollup_origination_size := 60000;
Constants_repr.parametric.tx_rollup_hard_size_limit_per_inbox :=
100000;
Constants_repr.parametric.tx_rollup_hard_size_limit_per_message :=
5000;
Constants_repr.parametric.tx_rollup_commitment_bond :=
Tez_repr.of_mutez_exn 10000000000;
Constants_repr.parametric.tx_rollup_finality_period :=
tx_rollup_finality_period;
Constants_repr.parametric.tx_rollup_withdraw_period :=
tx_rollup_finality_period;
Constants_repr.parametric.tx_rollup_max_inboxes_count :=
tx_rollup_finality_period +i 100;
Constants_repr.parametric.tx_rollup_max_messages_per_inbox := 1010;
Constants_repr.parametric.tx_rollup_max_commitments_count :=
(2 ×i tx_rollup_finality_period) +i 100;
Constants_repr.parametric.tx_rollup_cost_per_byte_ema_factor := 120;
Constants_repr.parametric.tx_rollup_max_ticket_payload_size := 2048;
Constants_repr.parametric.tx_rollup_max_withdrawals_per_batch := 15;
Constants_repr.parametric.tx_rollup_rejection_max_proof_size := 30000;
Constants_repr.parametric.tx_rollup_sunset_level := 3473409;
Constants_repr.parametric.sc_rollup_enable := false;
Constants_repr.parametric.sc_rollup_origination_size := 6314;
Constants_repr.parametric.sc_rollup_challenge_window_in_blocks :=
20160;
Constants_repr.parametric.sc_rollup_max_available_messages := 1000000;
|} in
let ctxt := add_constants ctxt constants in
return? ctxt
end in
let? ctxt := prepare level timestamp timestamp ctxt in
return? (previous_proto, ctxt).
Definition activate (ctxt : t) (h_value : Protocol_hash.t) : t :=
Error_monad.op_gtpipeeq (Updater.activate (context_value ctxt) h_value)
(update_context ctxt).
Definition key : Set := list string.
Definition value : Set := bytes.
Definition tree : Set := Context.tree.
Definition T {t : Set} : Set :=
Raw_context_intf.T (root := root) (t := t) (tree := tree).
Definition mem (ctxt : t) (k_value : Context.key) : bool :=
Context.mem (context_value ctxt) k_value.
Definition mem_tree (ctxt : t) (k_value : Context.key) : bool :=
Context.mem_tree (context_value ctxt) k_value.
Definition get (ctxt : t) (k_value : Context.key) : M? Context.value :=
let function_parameter := Context.find (context_value ctxt) k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition get_tree (ctxt : t) (k_value : Context.key) : M? Context.tree :=
let function_parameter := Context.find_tree (context_value ctxt) k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition find (ctxt : t) (k_value : Context.key) : option Context.value :=
Context.find (context_value ctxt) k_value.
Definition find_tree (ctxt : t) (k_value : Context.key) : option Context.tree :=
Context.find_tree (context_value ctxt) k_value.
Definition add (ctxt : t) (k_value : Context.key) (v_value : Context.value)
: t :=
Error_monad.op_gtpipeeq (Context.add (context_value ctxt) k_value v_value)
(update_context ctxt).
Definition add_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
: t :=
Error_monad.op_gtpipeeq
(Context.add_tree (context_value ctxt) k_value v_value)
(update_context ctxt).
Definition init_value
(ctxt : t) (k_value : Context.key) (v_value : Context.value) : M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
let context_value := Context.add (context_value ctxt) k_value v_value in
return? (update_context ctxt context_value)
end.
Definition init_tree (ctxt : t) (k_value : Context.key) (v_value : Context.tree)
: M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
let context_value := Context.add_tree (context_value ctxt) k_value v_value
in
return? (update_context ctxt context_value)
end.
Definition update (ctxt : t) (k_value : Context.key) (v_value : Context.value)
: M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
let context_value := Context.add (context_value ctxt) k_value v_value in
return? (update_context ctxt context_value)
end.
Definition update_tree
(ctxt : t) (k_value : Context.key) (v_value : Context.tree) : M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
let context_value := Context.add_tree (context_value ctxt) k_value v_value
in
return? (update_context ctxt context_value)
end.
Definition remove_existing (ctxt : t) (k_value : Context.key) : M? t :=
let function_parameter := Context.mem (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒
let context_value := Context.remove (context_value ctxt) k_value in
return? (update_context ctxt context_value)
end.
Definition remove_existing_tree (ctxt : t) (k_value : Context.key) : M? t :=
let function_parameter := Context.mem_tree (context_value ctxt) k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒
let context_value := Context.remove (context_value ctxt) k_value in
return? (update_context ctxt context_value)
end.
Definition remove (ctxt : t) (k_value : Context.key) : t :=
Error_monad.op_gtpipeeq (Context.remove (context_value ctxt) k_value)
(update_context ctxt).
Definition add_or_remove
(ctxt : t) (k_value : Context.key) (function_parameter : option Context.value)
: t :=
match function_parameter with
| None ⇒ remove ctxt k_value
| Some v_value ⇒ add ctxt k_value v_value
end.
Definition add_or_remove_tree
(ctxt : t) (k_value : Context.key) (function_parameter : option Context.tree)
: t :=
match function_parameter with
| None ⇒ remove ctxt k_value
| Some v_value ⇒ add_tree ctxt k_value v_value
end.
Definition list_value
(ctxt : t) (offset : option int) (length : option int) (k_value : Context.key)
: list (string × Context.tree) :=
Context.list_value (context_value ctxt) offset length k_value.
Definition fold {A : Set}
(depth : option Context.depth) (ctxt : t) (k_value : Context.key)
(order : Variant.t) (init_value : A)
(f_value : Context.key → Context.tree → A → A) : A :=
Context.fold depth (context_value ctxt) k_value order init_value f_value.
Definition config_value (ctxt : t) : Context.config :=
Context.config_value (context_value ctxt).
Module Tree.
Inclusion of the module [Context.Tree]
Definition mem := Context.Tree.(Context.TREE.mem).
Definition mem_tree := Context.Tree.(Context.TREE.mem_tree).
Definition find := Context.Tree.(Context.TREE.find).
Definition find_tree := Context.Tree.(Context.TREE.find_tree).
Definition list_value := Context.Tree.(Context.TREE.list_value).
Definition length := Context.Tree.(Context.TREE.length).
Definition add := Context.Tree.(Context.TREE.add).
Definition add_tree := Context.Tree.(Context.TREE.add_tree).
Definition remove := Context.Tree.(Context.TREE.remove).
Definition fold {a : Set} := Context.Tree.(Context.TREE.fold) (a := a).
Definition config_value := Context.Tree.(Context.TREE.config_value).
(* Definition empty := Context.Tree.(Context.TREE.empty). *)
Definition is_empty := Context.Tree.(Context.TREE.is_empty).
Definition kind_value := Context.Tree.(Context.TREE.kind_value).
Definition to_value := Context.Tree.(Context.TREE.to_value).
Definition of_value := Context.Tree.(Context.TREE.of_value).
Definition hash_value := Context.Tree.(Context.TREE.hash_value).
Definition equal := Context.Tree.(Context.TREE.equal).
Definition clear := Context.Tree.(Context.TREE.clear).
Definition empty (ctxt : t) : Context.tree :=
Context.Tree.(Context.TREE.empty) (context_value ctxt).
Definition get (t_value : Context.tree) (k_value : Context.key)
: M? Context.value :=
let function_parameter := find t_value k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition get_tree (t_value : Context.tree) (k_value : Context.key)
: M? Context.tree :=
let function_parameter := find_tree t_value k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition init_value
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒ Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
end.
Definition init_tree
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
: M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
end.
Definition update
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒ Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
end.
Definition update_tree
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
: M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
end.
Definition remove_existing (t_value : Context.tree) (k_value : Context.key)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒ Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
end.
Definition remove_existing_tree
(t_value : Context.tree) (k_value : Context.key) : M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒ Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
end.
Definition add_or_remove
(t_value : Context.tree) (k_value : Context.key)
(function_parameter : option Context.value) : Context.tree :=
match function_parameter with
| None ⇒ remove t_value k_value
| Some v_value ⇒ add t_value k_value v_value
end.
Definition add_or_remove_tree
(t_value : Context.tree) (k_value : Context.key)
(function_parameter : option Context.tree) : Context.tree :=
match function_parameter with
| None ⇒ remove t_value k_value
| Some v_value ⇒ add_tree t_value k_value v_value
end.
(* Tree *)
Definition module :=
{|
Raw_context_intf.TREE.mem := mem;
Raw_context_intf.TREE.mem_tree := mem_tree;
Raw_context_intf.TREE.get := get;
Raw_context_intf.TREE.get_tree := get_tree;
Raw_context_intf.TREE.find := find;
Raw_context_intf.TREE.find_tree := find_tree;
Raw_context_intf.TREE.list_value := list_value;
Raw_context_intf.TREE.init_value := init_value;
Raw_context_intf.TREE.init_tree := init_tree;
Raw_context_intf.TREE.update := update;
Raw_context_intf.TREE.update_tree := update_tree;
Raw_context_intf.TREE.add := add;
Raw_context_intf.TREE.add_tree := add_tree;
Raw_context_intf.TREE.remove := remove;
Raw_context_intf.TREE.remove_existing := remove_existing;
Raw_context_intf.TREE.remove_existing_tree := remove_existing_tree;
Raw_context_intf.TREE.add_or_remove := add_or_remove;
Raw_context_intf.TREE.add_or_remove_tree := add_or_remove_tree;
Raw_context_intf.TREE.fold _ := fold;
Raw_context_intf.TREE.config_value := config_value;
Raw_context_intf.TREE.empty := empty;
Raw_context_intf.TREE.is_empty := is_empty;
Raw_context_intf.TREE.kind_value := kind_value;
Raw_context_intf.TREE.to_value := to_value;
Raw_context_intf.TREE.hash_value := hash_value;
Raw_context_intf.TREE.equal := equal;
Raw_context_intf.TREE.clear := clear
|}.
End Tree.
Definition Tree : Raw_context_intf.TREE (t := t) (tree := tree) := Tree.module.
Definition verify_tree_proof {A : Set}
(proof : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: Pervasives.result (Context.tree × A) Variant.t :=
Context.verify_tree_proof proof f_value.
Definition verify_stream_proof {A : Set}
(proof : Context.Proof.t Context.Proof.stream)
(f_value : Context.tree → Context.tree × A)
: Pervasives.result (Context.tree × A) Variant.t :=
Context.verify_stream_proof proof f_value.
Definition equal_config : Context.config → Context.config → bool :=
Context.equal_config.
Definition project {A : Set} (x_value : A) : A := x_value.
Definition absolute_key {A B : Set} (function_parameter : A) : B → B :=
let '_ := function_parameter in
fun (k_value : B) ⇒ k_value.
Definition description : Storage_description.t root :=
Storage_description.create tt.
Definition fold_map_temporary_lazy_storage_ids {A : Set}
(ctxt : t)
(f_value : Lazy_storage_kind.Temp_ids.t → Lazy_storage_kind.Temp_ids.t × A)
: t × A :=
(fun (function_parameter : Lazy_storage_kind.Temp_ids.t × A) ⇒
let '(temporary_lazy_storage_ids, x_value) := function_parameter in
((update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids),
x_value)) (f_value (temporary_lazy_storage_ids ctxt)).
Definition map_temporary_lazy_storage_ids_s
(ctxt : t)
(f_value : Lazy_storage_kind.Temp_ids.t → t × Lazy_storage_kind.Temp_ids.t)
: t :=
let '(ctxt, temporary_lazy_storage_ids) :=
f_value (temporary_lazy_storage_ids ctxt) in
update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids.
Module Cache.
Definition key : Set := Context.cache_key.
Definition value : Set := Context.cache_value.
Definition key_of_identifier : int → string → Context.cache_key :=
Context.Cache.(Context.CACHE.key_of_identifier).
Definition identifier_of_key : Context.cache_key → string :=
Context.Cache.(Context.CACHE.identifier_of_key).
Definition pp (fmt : Format.formatter) (ctxt : t) : unit :=
Context.Cache.(Context.CACHE.pp) fmt (context_value ctxt).
Definition find (c_value : t) (k_value : Context.cache_key)
: option Context.cache_value :=
Context.Cache.(Context.CACHE.find) (context_value c_value) k_value.
Definition set_cache_layout (c_value : t) (layout : list int) : t :=
let ctxt :=
Context.Cache.(Context.CACHE.set_cache_layout) (context_value c_value)
layout in
update_context c_value ctxt.
Definition update
(c_value : t) (k_value : Context.cache_key)
(v_value : option (Context.cache_value × int)) : t :=
update_context c_value
(Context.Cache.(Context.CACHE.update) (context_value c_value) k_value
v_value).
Definition sync (c_value : t) (cache_nonce : Bytes.t) : t :=
let ctxt :=
Context.Cache.(Context.CACHE.sync) (context_value c_value) cache_nonce in
update_context c_value ctxt.
Definition clear (c_value : t) : t :=
update_context c_value
(Context.Cache.(Context.CACHE.clear) (context_value c_value)).
Definition list_keys (c_value : t) (cache_index : int)
: option (list (Context.cache_key × int)) :=
Context.Cache.(Context.CACHE.list_keys) (context_value c_value) cache_index.
Definition key_rank (c_value : t) (key_value : Context.cache_key)
: option int :=
Context.Cache.(Context.CACHE.key_rank) (context_value c_value) key_value.
Definition cache_size_limit (c_value : t) (cache_index : int) : option int :=
Context.Cache.(Context.CACHE.cache_size_limit) (context_value c_value)
cache_index.
Definition cache_size (c_value : t) (cache_index : int) : option int :=
Context.Cache.(Context.CACHE.cache_size) (context_value c_value) cache_index.
Definition future_cache_expectation (c_value : t) (time_in_blocks : int)
: t :=
update_context c_value
(Context.Cache.(Context.CACHE.future_cache_expectation)
(context_value c_value) time_in_blocks).
(* Cache *)
Definition module :=
{|
Context.CACHE.key_of_identifier := key_of_identifier;
Context.CACHE.identifier_of_key := identifier_of_key;
Context.CACHE.pp := pp;
Context.CACHE.find := find;
Context.CACHE.set_cache_layout := set_cache_layout;
Context.CACHE.update := update;
Context.CACHE.sync := sync;
Context.CACHE.clear := clear;
Context.CACHE.list_keys := list_keys;
Context.CACHE.key_rank := key_rank;
Context.CACHE.cache_size_limit := cache_size_limit;
Context.CACHE.cache_size := cache_size;
Context.CACHE.future_cache_expectation := future_cache_expectation
|}.
End Cache.
Definition Cache := Cache.module.
Definition record_non_consensus_operation_hash
(ctxt : t) (operation_hash : Operation_hash.t) : t :=
update_non_consensus_operations_rev ctxt
(cons operation_hash (non_consensus_operations_rev ctxt)).
Definition non_consensus_operations (ctxt : t) : list Operation_hash.t :=
List.rev (non_consensus_operations_rev ctxt).
Definition init_sampler_for_cycle
(ctxt : t) (cycle : Cycle_repr.t) (seed_value : Seed_repr.seed)
(state_value : Sampler.t (Signature.public_key × Signature.public_key_hash))
: M? t :=
let map := sampler_state ctxt in
if Cycle_repr.Map.(Map.S.mem) cycle map then
Error_monad.error_value
(Build_extensible "Sampler_already_set" Cycle_repr.t cycle)
else
let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
let ctxt := update_sampler_state ctxt map in
return? ctxt.
Definition sampler_for_cycle {A : Set}
(read :
t →
Pervasives.result
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) A)
(ctxt : t) (cycle : Cycle_repr.t)
: Pervasives.result
(t × Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) A :=
let map := sampler_state ctxt in
match Cycle_repr.Map.(Map.S.find) cycle map with
| Some (seed_value, state_value) ⇒ return? (ctxt, seed_value, state_value)
| None ⇒
let? '(seed_value, state_value) := read ctxt in
let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
let ctxt := update_sampler_state ctxt map in
return? (ctxt, seed_value, state_value)
end.
Definition stake_distribution_for_current_cycle (ctxt : t)
: M?
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) :=
match ctxt.(t.back).(back.stake_distribution_for_current_cycle) with
| None ⇒
Error_monad.error_value
(Build_extensible "Stake_distribution_not_set" unit tt)
| Some s_value ⇒ return? s_value
end.
Definition init_stake_distribution_for_current_cycle
(ctxt : t)
(stake_distribution_for_current_cycle :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) : t :=
update_back ctxt
(back.with_stake_distribution_for_current_cycle
(Some stake_distribution_for_current_cycle) ctxt.(t.back)).
Module CONSENSUS.
Record signature {t : Set} {slot_map : Set → Set} {slot_set slot round : Set}
: Set := {
t := t;
slot_map := slot_map;
slot_set := slot_set;
slot := slot;
round := round;
allowed_endorsements :
t → slot_map (Signature.public_key × Signature.public_key_hash × int);
allowed_preendorsements :
t → slot_map (Signature.public_key × Signature.public_key_hash × int);
current_endorsement_power : t → int;
initialize_consensus_operation :
t → slot_map (Signature.public_key × Signature.public_key_hash × int) →
slot_map (Signature.public_key × Signature.public_key_hash × int) → t;
record_grand_parent_endorsement : t → Signature.public_key_hash → M? t;
record_endorsement : t → slot → int → M? t;
record_preendorsement : t → slot → int → round → M? t;
endorsements_seen : t → slot_set;
get_preendorsements_quorum_round : t → option round;
set_preendorsements_quorum_round : t → round → t;
locked_round_evidence : t → option (round × int);
set_endorsement_branch : t → Block_hash.t × Block_payload_hash.t → t;
endorsement_branch : t → option (Block_hash.t × Block_payload_hash.t);
set_grand_parent_branch : t → Block_hash.t × Block_payload_hash.t → t;
grand_parent_branch : t → option (Block_hash.t × Block_payload_hash.t);
}.
End CONSENSUS.
Definition CONSENSUS := @CONSENSUS.signature.
Arguments CONSENSUS {_ _ _ _ _}.
Module Consensus.
Definition allowed_endorsements (ctxt : t)
: Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_endorsements).
Definition allowed_preendorsements (ctxt : t)
: Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_preendorsements).
Definition current_endorsement_power (ctxt : t) : int :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.current_endorsement_power).
Definition get_preendorsements_quorum_round (ctxt : t)
: option Round_repr.t :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.preendorsements_quorum_round).
Definition locked_round_evidence (ctxt : t) : option (Round_repr.t × int) :=
Raw_consensus.locked_round_evidence ctxt.(t.back).(back.consensus).
Definition update_consensus_with
(ctxt : t) (f_value : Raw_consensus.t → Raw_consensus.t) : t :=
t.with_back
(back.with_consensus (f_value ctxt.(t.back).(back.consensus))
ctxt.(t.back)) ctxt.
Definition update_consensus_with_tzresult {A : Set}
(ctxt : t)
(f_value : Raw_consensus.t → Pervasives.result Raw_consensus.t A)
: Pervasives.result t A :=
let? consensus := f_value ctxt.(t.back).(back.consensus) in
return? (t.with_back (back.with_consensus consensus ctxt.(t.back)) ctxt).
Definition initialize_consensus_operation
(ctxt : t)
(allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int))
(allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int)) : t :=
update_consensus_with ctxt
(Raw_consensus.initialize_with_endorsements_and_preendorsements
allowed_endorsements allowed_preendorsements).
Definition record_grand_parent_endorsement
(ctxt : t) (pkh : Signature.public_key_hash) : M? t :=
update_consensus_with_tzresult ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.record_grand_parent_endorsement ctxt pkh).
Definition record_preendorsement
(ctxt : t) (initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
: M? t :=
update_consensus_with_tzresult ctxt
(Raw_consensus.record_preendorsement initial_slot power round).
Definition record_endorsement
(ctxt : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
update_consensus_with_tzresult ctxt
(fun x_1 ⇒ Raw_consensus.record_endorsement x_1 initial_slot power).
Definition endorsements_seen (ctxt : t) : Slot_repr._Set.(_Set.S.t) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.endorsements_seen).
Definition set_preendorsements_quorum_round (ctxt : t) (round : Round_repr.t)
: t :=
update_consensus_with ctxt
(Raw_consensus.set_preendorsements_quorum_round round).
Definition endorsement_branch (ctxt : t)
: option (Block_hash.t × Block_payload_hash.t) :=
Raw_consensus.endorsement_branch ctxt.(t.back).(back.consensus).
Definition set_endorsement_branch
(ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
update_consensus_with ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.set_endorsement_branch ctxt branch).
Definition grand_parent_branch (ctxt : t)
: option (Block_hash.t × Block_payload_hash.t) :=
Raw_consensus.grand_parent_branch ctxt.(t.back).(back.consensus).
Definition set_grand_parent_branch
(ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
update_consensus_with ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.set_grand_parent_branch ctxt branch).
(* Consensus *)
Definition module :=
{|
CONSENSUS.allowed_endorsements := allowed_endorsements;
CONSENSUS.allowed_preendorsements := allowed_preendorsements;
CONSENSUS.current_endorsement_power := current_endorsement_power;
CONSENSUS.initialize_consensus_operation := initialize_consensus_operation;
CONSENSUS.record_grand_parent_endorsement :=
record_grand_parent_endorsement;
CONSENSUS.record_endorsement := record_endorsement;
CONSENSUS.record_preendorsement := record_preendorsement;
CONSENSUS.endorsements_seen := endorsements_seen;
CONSENSUS.get_preendorsements_quorum_round :=
get_preendorsements_quorum_round;
CONSENSUS.set_preendorsements_quorum_round :=
set_preendorsements_quorum_round;
CONSENSUS.locked_round_evidence := locked_round_evidence;
CONSENSUS.set_endorsement_branch := set_endorsement_branch;
CONSENSUS.endorsement_branch := endorsement_branch;
CONSENSUS.set_grand_parent_branch := set_grand_parent_branch;
CONSENSUS.grand_parent_branch := grand_parent_branch
|}.
End Consensus.
Definition Consensus
: CONSENSUS (t := t) (slot_map := fun (a : Set) ⇒ Slot_repr.Map.(Map.S.t) a)
(slot_set := Slot_repr._Set.(_Set.S.t)) (slot := Slot_repr.t)
(round := Round_repr.t) := Consensus.module.
Module Tx_rollup.
Definition add_message
(ctxt : t) (rollup : Tx_rollup_repr.Hash.t)
(message : Tx_rollup_message_hash_repr.t)
: t × Tx_rollup_inbox_repr.Merkle.root :=
let root_value :=
Pervasives.ref_value
(Tx_rollup_inbox_repr.Merkle.root_value
Tx_rollup_inbox_repr.Merkle.empty) in
let updater (element : option Tx_rollup_inbox_repr.Merkle.tree)
: option Tx_rollup_inbox_repr.Merkle.tree :=
let tree_value :=
Option.value_value element Tx_rollup_inbox_repr.Merkle.empty in
let tree_value :=
Tx_rollup_inbox_repr.Merkle.add_message tree_value message in
let '_ :=
Pervasives.op_coloneq root_value
(Tx_rollup_inbox_repr.Merkle.root_value tree_value) in
Some tree_value in
let map :=
Tx_rollup_repr.Map.(Map.S.update) rollup updater
ctxt.(t.back).(back.tx_rollup_current_messages) in
let back := back.with_tx_rollup_current_messages map ctxt.(t.back) in
((t.with_back back ctxt), (Pervasives.op_exclamation root_value)).
End Tx_rollup.
Module Sc_rollup_in_memory_inbox.
Definition current_messages (ctxt : t) (rollup : Sc_rollup_repr.Address.t)
: tree :=
(fun (function_parameter : option Context.tree) ⇒
match function_parameter with
| None ⇒ Tree.(Raw_context_intf.TREE.empty) ctxt
| Some tree_value ⇒ tree_value
end)
(Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.find) rollup
ctxt.(t.back).(back.sc_rollup_current_messages)).
Definition set_current_messages
(ctxt : t) (rollup : Sc_rollup_repr.Address.t) (tree_value : Context.tree)
: t :=
let sc_rollup_current_messages :=
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.add) rollup tree_value
ctxt.(t.back).(back.sc_rollup_current_messages) in
let back :=
back.with_sc_rollup_current_messages sc_rollup_current_messages
ctxt.(t.back) in
t.with_back back ctxt.
End Sc_rollup_in_memory_inbox.
Definition mem_tree := Context.Tree.(Context.TREE.mem_tree).
Definition find := Context.Tree.(Context.TREE.find).
Definition find_tree := Context.Tree.(Context.TREE.find_tree).
Definition list_value := Context.Tree.(Context.TREE.list_value).
Definition length := Context.Tree.(Context.TREE.length).
Definition add := Context.Tree.(Context.TREE.add).
Definition add_tree := Context.Tree.(Context.TREE.add_tree).
Definition remove := Context.Tree.(Context.TREE.remove).
Definition fold {a : Set} := Context.Tree.(Context.TREE.fold) (a := a).
Definition config_value := Context.Tree.(Context.TREE.config_value).
(* Definition empty := Context.Tree.(Context.TREE.empty). *)
Definition is_empty := Context.Tree.(Context.TREE.is_empty).
Definition kind_value := Context.Tree.(Context.TREE.kind_value).
Definition to_value := Context.Tree.(Context.TREE.to_value).
Definition of_value := Context.Tree.(Context.TREE.of_value).
Definition hash_value := Context.Tree.(Context.TREE.hash_value).
Definition equal := Context.Tree.(Context.TREE.equal).
Definition clear := Context.Tree.(Context.TREE.clear).
Definition empty (ctxt : t) : Context.tree :=
Context.Tree.(Context.TREE.empty) (context_value ctxt).
Definition get (t_value : Context.tree) (k_value : Context.key)
: M? Context.value :=
let function_parameter := find t_value k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition get_tree (t_value : Context.tree) (k_value : Context.key)
: M? Context.tree :=
let function_parameter := find_tree t_value k_value in
match function_parameter with
| None ⇒ storage_error_value (Missing_key k_value Get)
| Some v_value ⇒ return? v_value
end.
Definition init_value
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒ Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
end.
Definition init_tree
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
: M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| true ⇒ storage_error_value (Existing_key k_value)
| _ ⇒
Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
end.
Definition update
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.value)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒ Error_monad.op_gtpipeeq (add t_value k_value v_value) Error_monad.ok
end.
Definition update_tree
(t_value : Context.tree) (k_value : Context.key) (v_value : Context.tree)
: M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value _Set)
| _ ⇒
Error_monad.op_gtpipeeq (add_tree t_value k_value v_value) Error_monad.ok
end.
Definition remove_existing (t_value : Context.tree) (k_value : Context.key)
: M? Context.tree :=
let function_parameter := mem t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒ Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
end.
Definition remove_existing_tree
(t_value : Context.tree) (k_value : Context.key) : M? Context.tree :=
let function_parameter := mem_tree t_value k_value in
match function_parameter with
| false ⇒ storage_error_value (Missing_key k_value Del)
| _ ⇒ Error_monad.op_gtpipeeq (remove t_value k_value) Error_monad.ok
end.
Definition add_or_remove
(t_value : Context.tree) (k_value : Context.key)
(function_parameter : option Context.value) : Context.tree :=
match function_parameter with
| None ⇒ remove t_value k_value
| Some v_value ⇒ add t_value k_value v_value
end.
Definition add_or_remove_tree
(t_value : Context.tree) (k_value : Context.key)
(function_parameter : option Context.tree) : Context.tree :=
match function_parameter with
| None ⇒ remove t_value k_value
| Some v_value ⇒ add_tree t_value k_value v_value
end.
(* Tree *)
Definition module :=
{|
Raw_context_intf.TREE.mem := mem;
Raw_context_intf.TREE.mem_tree := mem_tree;
Raw_context_intf.TREE.get := get;
Raw_context_intf.TREE.get_tree := get_tree;
Raw_context_intf.TREE.find := find;
Raw_context_intf.TREE.find_tree := find_tree;
Raw_context_intf.TREE.list_value := list_value;
Raw_context_intf.TREE.init_value := init_value;
Raw_context_intf.TREE.init_tree := init_tree;
Raw_context_intf.TREE.update := update;
Raw_context_intf.TREE.update_tree := update_tree;
Raw_context_intf.TREE.add := add;
Raw_context_intf.TREE.add_tree := add_tree;
Raw_context_intf.TREE.remove := remove;
Raw_context_intf.TREE.remove_existing := remove_existing;
Raw_context_intf.TREE.remove_existing_tree := remove_existing_tree;
Raw_context_intf.TREE.add_or_remove := add_or_remove;
Raw_context_intf.TREE.add_or_remove_tree := add_or_remove_tree;
Raw_context_intf.TREE.fold _ := fold;
Raw_context_intf.TREE.config_value := config_value;
Raw_context_intf.TREE.empty := empty;
Raw_context_intf.TREE.is_empty := is_empty;
Raw_context_intf.TREE.kind_value := kind_value;
Raw_context_intf.TREE.to_value := to_value;
Raw_context_intf.TREE.hash_value := hash_value;
Raw_context_intf.TREE.equal := equal;
Raw_context_intf.TREE.clear := clear
|}.
End Tree.
Definition Tree : Raw_context_intf.TREE (t := t) (tree := tree) := Tree.module.
Definition verify_tree_proof {A : Set}
(proof : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: Pervasives.result (Context.tree × A) Variant.t :=
Context.verify_tree_proof proof f_value.
Definition verify_stream_proof {A : Set}
(proof : Context.Proof.t Context.Proof.stream)
(f_value : Context.tree → Context.tree × A)
: Pervasives.result (Context.tree × A) Variant.t :=
Context.verify_stream_proof proof f_value.
Definition equal_config : Context.config → Context.config → bool :=
Context.equal_config.
Definition project {A : Set} (x_value : A) : A := x_value.
Definition absolute_key {A B : Set} (function_parameter : A) : B → B :=
let '_ := function_parameter in
fun (k_value : B) ⇒ k_value.
Definition description : Storage_description.t root :=
Storage_description.create tt.
Definition fold_map_temporary_lazy_storage_ids {A : Set}
(ctxt : t)
(f_value : Lazy_storage_kind.Temp_ids.t → Lazy_storage_kind.Temp_ids.t × A)
: t × A :=
(fun (function_parameter : Lazy_storage_kind.Temp_ids.t × A) ⇒
let '(temporary_lazy_storage_ids, x_value) := function_parameter in
((update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids),
x_value)) (f_value (temporary_lazy_storage_ids ctxt)).
Definition map_temporary_lazy_storage_ids_s
(ctxt : t)
(f_value : Lazy_storage_kind.Temp_ids.t → t × Lazy_storage_kind.Temp_ids.t)
: t :=
let '(ctxt, temporary_lazy_storage_ids) :=
f_value (temporary_lazy_storage_ids ctxt) in
update_temporary_lazy_storage_ids ctxt temporary_lazy_storage_ids.
Module Cache.
Definition key : Set := Context.cache_key.
Definition value : Set := Context.cache_value.
Definition key_of_identifier : int → string → Context.cache_key :=
Context.Cache.(Context.CACHE.key_of_identifier).
Definition identifier_of_key : Context.cache_key → string :=
Context.Cache.(Context.CACHE.identifier_of_key).
Definition pp (fmt : Format.formatter) (ctxt : t) : unit :=
Context.Cache.(Context.CACHE.pp) fmt (context_value ctxt).
Definition find (c_value : t) (k_value : Context.cache_key)
: option Context.cache_value :=
Context.Cache.(Context.CACHE.find) (context_value c_value) k_value.
Definition set_cache_layout (c_value : t) (layout : list int) : t :=
let ctxt :=
Context.Cache.(Context.CACHE.set_cache_layout) (context_value c_value)
layout in
update_context c_value ctxt.
Definition update
(c_value : t) (k_value : Context.cache_key)
(v_value : option (Context.cache_value × int)) : t :=
update_context c_value
(Context.Cache.(Context.CACHE.update) (context_value c_value) k_value
v_value).
Definition sync (c_value : t) (cache_nonce : Bytes.t) : t :=
let ctxt :=
Context.Cache.(Context.CACHE.sync) (context_value c_value) cache_nonce in
update_context c_value ctxt.
Definition clear (c_value : t) : t :=
update_context c_value
(Context.Cache.(Context.CACHE.clear) (context_value c_value)).
Definition list_keys (c_value : t) (cache_index : int)
: option (list (Context.cache_key × int)) :=
Context.Cache.(Context.CACHE.list_keys) (context_value c_value) cache_index.
Definition key_rank (c_value : t) (key_value : Context.cache_key)
: option int :=
Context.Cache.(Context.CACHE.key_rank) (context_value c_value) key_value.
Definition cache_size_limit (c_value : t) (cache_index : int) : option int :=
Context.Cache.(Context.CACHE.cache_size_limit) (context_value c_value)
cache_index.
Definition cache_size (c_value : t) (cache_index : int) : option int :=
Context.Cache.(Context.CACHE.cache_size) (context_value c_value) cache_index.
Definition future_cache_expectation (c_value : t) (time_in_blocks : int)
: t :=
update_context c_value
(Context.Cache.(Context.CACHE.future_cache_expectation)
(context_value c_value) time_in_blocks).
(* Cache *)
Definition module :=
{|
Context.CACHE.key_of_identifier := key_of_identifier;
Context.CACHE.identifier_of_key := identifier_of_key;
Context.CACHE.pp := pp;
Context.CACHE.find := find;
Context.CACHE.set_cache_layout := set_cache_layout;
Context.CACHE.update := update;
Context.CACHE.sync := sync;
Context.CACHE.clear := clear;
Context.CACHE.list_keys := list_keys;
Context.CACHE.key_rank := key_rank;
Context.CACHE.cache_size_limit := cache_size_limit;
Context.CACHE.cache_size := cache_size;
Context.CACHE.future_cache_expectation := future_cache_expectation
|}.
End Cache.
Definition Cache := Cache.module.
Definition record_non_consensus_operation_hash
(ctxt : t) (operation_hash : Operation_hash.t) : t :=
update_non_consensus_operations_rev ctxt
(cons operation_hash (non_consensus_operations_rev ctxt)).
Definition non_consensus_operations (ctxt : t) : list Operation_hash.t :=
List.rev (non_consensus_operations_rev ctxt).
Definition init_sampler_for_cycle
(ctxt : t) (cycle : Cycle_repr.t) (seed_value : Seed_repr.seed)
(state_value : Sampler.t (Signature.public_key × Signature.public_key_hash))
: M? t :=
let map := sampler_state ctxt in
if Cycle_repr.Map.(Map.S.mem) cycle map then
Error_monad.error_value
(Build_extensible "Sampler_already_set" Cycle_repr.t cycle)
else
let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
let ctxt := update_sampler_state ctxt map in
return? ctxt.
Definition sampler_for_cycle {A : Set}
(read :
t →
Pervasives.result
(Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) A)
(ctxt : t) (cycle : Cycle_repr.t)
: Pervasives.result
(t × Seed_repr.seed ×
Sampler.t (Signature.public_key × Signature.public_key_hash)) A :=
let map := sampler_state ctxt in
match Cycle_repr.Map.(Map.S.find) cycle map with
| Some (seed_value, state_value) ⇒ return? (ctxt, seed_value, state_value)
| None ⇒
let? '(seed_value, state_value) := read ctxt in
let map := Cycle_repr.Map.(Map.S.add) cycle (seed_value, state_value) map in
let ctxt := update_sampler_state ctxt map in
return? (ctxt, seed_value, state_value)
end.
Definition stake_distribution_for_current_cycle (ctxt : t)
: M?
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) :=
match ctxt.(t.back).(back.stake_distribution_for_current_cycle) with
| None ⇒
Error_monad.error_value
(Build_extensible "Stake_distribution_not_set" unit tt)
| Some s_value ⇒ return? s_value
end.
Definition init_stake_distribution_for_current_cycle
(ctxt : t)
(stake_distribution_for_current_cycle :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) : t :=
update_back ctxt
(back.with_stake_distribution_for_current_cycle
(Some stake_distribution_for_current_cycle) ctxt.(t.back)).
Module CONSENSUS.
Record signature {t : Set} {slot_map : Set → Set} {slot_set slot round : Set}
: Set := {
t := t;
slot_map := slot_map;
slot_set := slot_set;
slot := slot;
round := round;
allowed_endorsements :
t → slot_map (Signature.public_key × Signature.public_key_hash × int);
allowed_preendorsements :
t → slot_map (Signature.public_key × Signature.public_key_hash × int);
current_endorsement_power : t → int;
initialize_consensus_operation :
t → slot_map (Signature.public_key × Signature.public_key_hash × int) →
slot_map (Signature.public_key × Signature.public_key_hash × int) → t;
record_grand_parent_endorsement : t → Signature.public_key_hash → M? t;
record_endorsement : t → slot → int → M? t;
record_preendorsement : t → slot → int → round → M? t;
endorsements_seen : t → slot_set;
get_preendorsements_quorum_round : t → option round;
set_preendorsements_quorum_round : t → round → t;
locked_round_evidence : t → option (round × int);
set_endorsement_branch : t → Block_hash.t × Block_payload_hash.t → t;
endorsement_branch : t → option (Block_hash.t × Block_payload_hash.t);
set_grand_parent_branch : t → Block_hash.t × Block_payload_hash.t → t;
grand_parent_branch : t → option (Block_hash.t × Block_payload_hash.t);
}.
End CONSENSUS.
Definition CONSENSUS := @CONSENSUS.signature.
Arguments CONSENSUS {_ _ _ _ _}.
Module Consensus.
Definition allowed_endorsements (ctxt : t)
: Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_endorsements).
Definition allowed_preendorsements (ctxt : t)
: Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.allowed_preendorsements).
Definition current_endorsement_power (ctxt : t) : int :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.current_endorsement_power).
Definition get_preendorsements_quorum_round (ctxt : t)
: option Round_repr.t :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.preendorsements_quorum_round).
Definition locked_round_evidence (ctxt : t) : option (Round_repr.t × int) :=
Raw_consensus.locked_round_evidence ctxt.(t.back).(back.consensus).
Definition update_consensus_with
(ctxt : t) (f_value : Raw_consensus.t → Raw_consensus.t) : t :=
t.with_back
(back.with_consensus (f_value ctxt.(t.back).(back.consensus))
ctxt.(t.back)) ctxt.
Definition update_consensus_with_tzresult {A : Set}
(ctxt : t)
(f_value : Raw_consensus.t → Pervasives.result Raw_consensus.t A)
: Pervasives.result t A :=
let? consensus := f_value ctxt.(t.back).(back.consensus) in
return? (t.with_back (back.with_consensus consensus ctxt.(t.back)) ctxt).
Definition initialize_consensus_operation
(ctxt : t)
(allowed_endorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int))
(allowed_preendorsements :
Slot_repr.Map.(Map.S.t)
(Signature.public_key × Signature.public_key_hash × int)) : t :=
update_consensus_with ctxt
(Raw_consensus.initialize_with_endorsements_and_preendorsements
allowed_endorsements allowed_preendorsements).
Definition record_grand_parent_endorsement
(ctxt : t) (pkh : Signature.public_key_hash) : M? t :=
update_consensus_with_tzresult ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.record_grand_parent_endorsement ctxt pkh).
Definition record_preendorsement
(ctxt : t) (initial_slot : Slot_repr.t) (power : int) (round : Round_repr.t)
: M? t :=
update_consensus_with_tzresult ctxt
(Raw_consensus.record_preendorsement initial_slot power round).
Definition record_endorsement
(ctxt : t) (initial_slot : Slot_repr.t) (power : int) : M? t :=
update_consensus_with_tzresult ctxt
(fun x_1 ⇒ Raw_consensus.record_endorsement x_1 initial_slot power).
Definition endorsements_seen (ctxt : t) : Slot_repr._Set.(_Set.S.t) :=
ctxt.(t.back).(back.consensus).(Raw_consensus.t.endorsements_seen).
Definition set_preendorsements_quorum_round (ctxt : t) (round : Round_repr.t)
: t :=
update_consensus_with ctxt
(Raw_consensus.set_preendorsements_quorum_round round).
Definition endorsement_branch (ctxt : t)
: option (Block_hash.t × Block_payload_hash.t) :=
Raw_consensus.endorsement_branch ctxt.(t.back).(back.consensus).
Definition set_endorsement_branch
(ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
update_consensus_with ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.set_endorsement_branch ctxt branch).
Definition grand_parent_branch (ctxt : t)
: option (Block_hash.t × Block_payload_hash.t) :=
Raw_consensus.grand_parent_branch ctxt.(t.back).(back.consensus).
Definition set_grand_parent_branch
(ctxt : t) (branch : Block_hash.t × Block_payload_hash.t) : t :=
update_consensus_with ctxt
(fun (ctxt : Raw_consensus.t) ⇒
Raw_consensus.set_grand_parent_branch ctxt branch).
(* Consensus *)
Definition module :=
{|
CONSENSUS.allowed_endorsements := allowed_endorsements;
CONSENSUS.allowed_preendorsements := allowed_preendorsements;
CONSENSUS.current_endorsement_power := current_endorsement_power;
CONSENSUS.initialize_consensus_operation := initialize_consensus_operation;
CONSENSUS.record_grand_parent_endorsement :=
record_grand_parent_endorsement;
CONSENSUS.record_endorsement := record_endorsement;
CONSENSUS.record_preendorsement := record_preendorsement;
CONSENSUS.endorsements_seen := endorsements_seen;
CONSENSUS.get_preendorsements_quorum_round :=
get_preendorsements_quorum_round;
CONSENSUS.set_preendorsements_quorum_round :=
set_preendorsements_quorum_round;
CONSENSUS.locked_round_evidence := locked_round_evidence;
CONSENSUS.set_endorsement_branch := set_endorsement_branch;
CONSENSUS.endorsement_branch := endorsement_branch;
CONSENSUS.set_grand_parent_branch := set_grand_parent_branch;
CONSENSUS.grand_parent_branch := grand_parent_branch
|}.
End Consensus.
Definition Consensus
: CONSENSUS (t := t) (slot_map := fun (a : Set) ⇒ Slot_repr.Map.(Map.S.t) a)
(slot_set := Slot_repr._Set.(_Set.S.t)) (slot := Slot_repr.t)
(round := Round_repr.t) := Consensus.module.
Module Tx_rollup.
Definition add_message
(ctxt : t) (rollup : Tx_rollup_repr.Hash.t)
(message : Tx_rollup_message_hash_repr.t)
: t × Tx_rollup_inbox_repr.Merkle.root :=
let root_value :=
Pervasives.ref_value
(Tx_rollup_inbox_repr.Merkle.root_value
Tx_rollup_inbox_repr.Merkle.empty) in
let updater (element : option Tx_rollup_inbox_repr.Merkle.tree)
: option Tx_rollup_inbox_repr.Merkle.tree :=
let tree_value :=
Option.value_value element Tx_rollup_inbox_repr.Merkle.empty in
let tree_value :=
Tx_rollup_inbox_repr.Merkle.add_message tree_value message in
let '_ :=
Pervasives.op_coloneq root_value
(Tx_rollup_inbox_repr.Merkle.root_value tree_value) in
Some tree_value in
let map :=
Tx_rollup_repr.Map.(Map.S.update) rollup updater
ctxt.(t.back).(back.tx_rollup_current_messages) in
let back := back.with_tx_rollup_current_messages map ctxt.(t.back) in
((t.with_back back ctxt), (Pervasives.op_exclamation root_value)).
End Tx_rollup.
Module Sc_rollup_in_memory_inbox.
Definition current_messages (ctxt : t) (rollup : Sc_rollup_repr.Address.t)
: tree :=
(fun (function_parameter : option Context.tree) ⇒
match function_parameter with
| None ⇒ Tree.(Raw_context_intf.TREE.empty) ctxt
| Some tree_value ⇒ tree_value
end)
(Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.find) rollup
ctxt.(t.back).(back.sc_rollup_current_messages)).
Definition set_current_messages
(ctxt : t) (rollup : Sc_rollup_repr.Address.t) (tree_value : Context.tree)
: t :=
let sc_rollup_current_messages :=
Sc_rollup_repr.Address.Map.(S.INDEXES_MAP.add) rollup tree_value
ctxt.(t.back).(back.sc_rollup_current_messages) in
let back :=
back.with_sc_rollup_current_messages sc_rollup_current_messages
ctxt.(t.back) in
t.with_back back ctxt.
End Sc_rollup_in_memory_inbox.
Explicit module to present this file as a record in Coq and reduce the size
of the generated Coq code.
Module M.
Definition t : Set := root.
Definition mem : t → Context.key → bool := mem.
Definition mem_tree : t → Context.key → bool := mem_tree.
Definition get : t → Context.key → M? Context.value := get.
Definition get_tree : t → Context.key → M? Context.tree := get_tree.
Definition find : t → Context.key → option Context.value := find.
Definition find_tree : t → Context.key → option Context.tree := find_tree.
Definition list_value
: t → option int → option int → Context.key →
list (string × Context.tree) := list_value.
Definition init_value : t → Context.key → Context.value → M? t :=
init_value.
Definition init_tree : t → Context.key → Context.tree → M? t := init_tree.
Definition update : t → Context.key → Context.value → M? t := update.
Definition update_tree : t → Context.key → Context.tree → M? t :=
update_tree.
Definition add : t → Context.key → Context.value → t := add.
Definition add_tree : t → Context.key → Context.tree → t := add_tree.
Definition remove : t → Context.key → t := remove.
Definition remove_existing : t → Context.key → M? t := remove_existing.
Definition remove_existing_tree : t → Context.key → M? t :=
remove_existing_tree.
Definition add_or_remove : t → Context.key → option Context.value → t :=
add_or_remove.
Definition add_or_remove_tree
: t → Context.key → option Context.tree → t := add_or_remove_tree.
Definition fold {A : Set}
: option Context.depth → t → Context.key → Variant.t → A →
(Context.key → Context.tree → A → A) → A := fold.
Definition config_value : t → Context.config := config_value.
Definition Tree := Tree.
Definition verify_tree_proof {A : Set}
: Context.Proof.t Context.Proof.tree →
(Context.tree → Context.tree × A) →
Pervasives.result (Context.tree × A) Variant.t := verify_tree_proof.
Definition verify_stream_proof {A : Set}
: Context.Proof.t Context.Proof.stream →
(Context.tree → Context.tree × A) →
Pervasives.result (Context.tree × A) Variant.t := verify_stream_proof.
Definition equal_config : Context.config → Context.config → bool :=
equal_config.
Definition project : t → root := project.
Definition absolute_key : t → key → key := absolute_key.
Definition consume_gas : t → Gas_limit_repr.cost → M? t := consume_gas.
Definition check_enough_gas : t → Gas_limit_repr.cost → M? unit :=
check_enough_gas.
Definition description : Storage_description.t t := description.
(* M *)
Definition module :=
{|
Raw_context_intf.T.mem := mem;
Raw_context_intf.T.mem_tree := mem_tree;
Raw_context_intf.T.get := get;
Raw_context_intf.T.get_tree := get_tree;
Raw_context_intf.T.find := find;
Raw_context_intf.T.find_tree := find_tree;
Raw_context_intf.T.list_value := list_value;
Raw_context_intf.T.init_value := init_value;
Raw_context_intf.T.init_tree := init_tree;
Raw_context_intf.T.update := update;
Raw_context_intf.T.update_tree := update_tree;
Raw_context_intf.T.add := add;
Raw_context_intf.T.add_tree := add_tree;
Raw_context_intf.T.remove := remove;
Raw_context_intf.T.remove_existing := remove_existing;
Raw_context_intf.T.remove_existing_tree := remove_existing_tree;
Raw_context_intf.T.add_or_remove := add_or_remove;
Raw_context_intf.T.add_or_remove_tree := add_or_remove_tree;
Raw_context_intf.T.fold _ := fold;
Raw_context_intf.T.config_value := config_value;
Raw_context_intf.T.Tree := Tree;
Raw_context_intf.T.verify_tree_proof _ := verify_tree_proof;
Raw_context_intf.T.verify_stream_proof _ := verify_stream_proof;
Raw_context_intf.T.equal_config := equal_config;
Raw_context_intf.T.project := project;
Raw_context_intf.T.absolute_key := absolute_key;
Raw_context_intf.T.consume_gas := consume_gas;
Raw_context_intf.T.check_enough_gas := check_enough_gas;
Raw_context_intf.T.description := description
|}.
End M.
Definition M : T (t := root) := M.module.
Definition t : Set := root.
Definition mem : t → Context.key → bool := mem.
Definition mem_tree : t → Context.key → bool := mem_tree.
Definition get : t → Context.key → M? Context.value := get.
Definition get_tree : t → Context.key → M? Context.tree := get_tree.
Definition find : t → Context.key → option Context.value := find.
Definition find_tree : t → Context.key → option Context.tree := find_tree.
Definition list_value
: t → option int → option int → Context.key →
list (string × Context.tree) := list_value.
Definition init_value : t → Context.key → Context.value → M? t :=
init_value.
Definition init_tree : t → Context.key → Context.tree → M? t := init_tree.
Definition update : t → Context.key → Context.value → M? t := update.
Definition update_tree : t → Context.key → Context.tree → M? t :=
update_tree.
Definition add : t → Context.key → Context.value → t := add.
Definition add_tree : t → Context.key → Context.tree → t := add_tree.
Definition remove : t → Context.key → t := remove.
Definition remove_existing : t → Context.key → M? t := remove_existing.
Definition remove_existing_tree : t → Context.key → M? t :=
remove_existing_tree.
Definition add_or_remove : t → Context.key → option Context.value → t :=
add_or_remove.
Definition add_or_remove_tree
: t → Context.key → option Context.tree → t := add_or_remove_tree.
Definition fold {A : Set}
: option Context.depth → t → Context.key → Variant.t → A →
(Context.key → Context.tree → A → A) → A := fold.
Definition config_value : t → Context.config := config_value.
Definition Tree := Tree.
Definition verify_tree_proof {A : Set}
: Context.Proof.t Context.Proof.tree →
(Context.tree → Context.tree × A) →
Pervasives.result (Context.tree × A) Variant.t := verify_tree_proof.
Definition verify_stream_proof {A : Set}
: Context.Proof.t Context.Proof.stream →
(Context.tree → Context.tree × A) →
Pervasives.result (Context.tree × A) Variant.t := verify_stream_proof.
Definition equal_config : Context.config → Context.config → bool :=
equal_config.
Definition project : t → root := project.
Definition absolute_key : t → key → key := absolute_key.
Definition consume_gas : t → Gas_limit_repr.cost → M? t := consume_gas.
Definition check_enough_gas : t → Gas_limit_repr.cost → M? unit :=
check_enough_gas.
Definition description : Storage_description.t t := description.
(* M *)
Definition module :=
{|
Raw_context_intf.T.mem := mem;
Raw_context_intf.T.mem_tree := mem_tree;
Raw_context_intf.T.get := get;
Raw_context_intf.T.get_tree := get_tree;
Raw_context_intf.T.find := find;
Raw_context_intf.T.find_tree := find_tree;
Raw_context_intf.T.list_value := list_value;
Raw_context_intf.T.init_value := init_value;
Raw_context_intf.T.init_tree := init_tree;
Raw_context_intf.T.update := update;
Raw_context_intf.T.update_tree := update_tree;
Raw_context_intf.T.add := add;
Raw_context_intf.T.add_tree := add_tree;
Raw_context_intf.T.remove := remove;
Raw_context_intf.T.remove_existing := remove_existing;
Raw_context_intf.T.remove_existing_tree := remove_existing_tree;
Raw_context_intf.T.add_or_remove := add_or_remove;
Raw_context_intf.T.add_or_remove_tree := add_or_remove_tree;
Raw_context_intf.T.fold _ := fold;
Raw_context_intf.T.config_value := config_value;
Raw_context_intf.T.Tree := Tree;
Raw_context_intf.T.verify_tree_proof _ := verify_tree_proof;
Raw_context_intf.T.verify_stream_proof _ := verify_stream_proof;
Raw_context_intf.T.equal_config := equal_config;
Raw_context_intf.T.project := project;
Raw_context_intf.T.absolute_key := absolute_key;
Raw_context_intf.T.consume_gas := consume_gas;
Raw_context_intf.T.check_enough_gas := check_enough_gas;
Raw_context_intf.T.description := description
|}.
End M.
Definition M : T (t := root) := M.module.