✅ Validate.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_apply.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_apply.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Operation_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.
Require TezosOfOCaml.Proto_alpha.Validate_errors.
Since the expected features of preendorsement and endorsement are
the same for all operations in the considered block, we compute
them once and for all at the begining of the block.
See [expected_features_for_application],
[expected_features_for_construction], and
[expected_features_for_partial_construction] in the [Consensus]
module below.
Module expected_features.
Record record : Set := Build {
level : Alpha_context.Raw_level.t;
round : option Alpha_context.Round.t;
branch : Block_hash.t;
payload_hash : Block_payload_hash.t;
}.
Definition with_level level (r : record) :=
Build level r.(round) r.(branch) r.(payload_hash).
Definition with_round round (r : record) :=
Build r.(level) round r.(branch) r.(payload_hash).
Definition with_branch branch (r : record) :=
Build r.(level) r.(round) branch r.(payload_hash).
Definition with_payload_hash payload_hash (r : record) :=
Build r.(level) r.(round) r.(branch) payload_hash.
End expected_features.
Definition expected_features := expected_features.record.
Record record : Set := Build {
level : Alpha_context.Raw_level.t;
round : option Alpha_context.Round.t;
branch : Block_hash.t;
payload_hash : Block_payload_hash.t;
}.
Definition with_level level (r : record) :=
Build level r.(round) r.(branch) r.(payload_hash).
Definition with_round round (r : record) :=
Build r.(level) round r.(branch) r.(payload_hash).
Definition with_branch branch (r : record) :=
Build r.(level) r.(round) branch r.(payload_hash).
Definition with_payload_hash payload_hash (r : record) :=
Build r.(level) r.(round) r.(branch) payload_hash.
End expected_features.
Definition expected_features := expected_features.record.
Records for the constructor parameters
Module ConstructorRecords_expected_preendorsement.
Module expected_preendorsement.
Module Expected_preendorsement.
Record record {expected_features block_round : Set} : Set := Build {
expected_features : expected_features;
block_round : block_round;
}.
Arguments record : clear implicits.
Definition with_expected_features {t_expected_features t_block_round}
expected_features (r : record t_expected_features t_block_round) :=
Build t_expected_features t_block_round expected_features
r.(block_round).
Definition with_block_round {t_expected_features t_block_round}
block_round (r : record t_expected_features t_block_round) :=
Build t_expected_features t_block_round r.(expected_features)
block_round.
End Expected_preendorsement.
Definition Expected_preendorsement_skeleton :=
Expected_preendorsement.record.
Module No_expected_branch_for_partial_construction_preendorsement.
Record record {expected_level : Set} : Set := Build {
expected_level : expected_level;
}.
Arguments record : clear implicits.
Definition with_expected_level {t_expected_level} expected_level
(r : record t_expected_level) :=
Build t_expected_level expected_level.
End No_expected_branch_for_partial_construction_preendorsement.
Definition
No_expected_branch_for_partial_construction_preendorsement_skeleton :=
No_expected_branch_for_partial_construction_preendorsement.record.
End expected_preendorsement.
End ConstructorRecords_expected_preendorsement.
Import ConstructorRecords_expected_preendorsement.
Reserved Notation "'expected_preendorsement.Expected_preendorsement".
Reserved Notation
"'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement".
Inductive expected_preendorsement : Set :=
| Expected_preendorsement :
'expected_preendorsement.Expected_preendorsement → expected_preendorsement
| No_locked_round_for_block_validation_preendorsement : expected_preendorsement
| Fresh_proposal_for_construction_preendorsement : expected_preendorsement
| No_expected_branch_for_partial_construction_preendorsement :
'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement
→ expected_preendorsement
| No_predecessor_info_cannot_validate_preendorsement : expected_preendorsement
where "'expected_preendorsement.Expected_preendorsement" :=
(expected_preendorsement.Expected_preendorsement_skeleton expected_features
(option Alpha_context.Round.t))
and "'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement"
:=
(expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement_skeleton
Alpha_context.Raw_level.t).
Module expected_preendorsement.
Include ConstructorRecords_expected_preendorsement.expected_preendorsement.
Definition Expected_preendorsement :=
'expected_preendorsement.Expected_preendorsement.
Definition No_expected_branch_for_partial_construction_preendorsement :=
'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.
End expected_preendorsement.
Module expected_preendorsement.
Module Expected_preendorsement.
Record record {expected_features block_round : Set} : Set := Build {
expected_features : expected_features;
block_round : block_round;
}.
Arguments record : clear implicits.
Definition with_expected_features {t_expected_features t_block_round}
expected_features (r : record t_expected_features t_block_round) :=
Build t_expected_features t_block_round expected_features
r.(block_round).
Definition with_block_round {t_expected_features t_block_round}
block_round (r : record t_expected_features t_block_round) :=
Build t_expected_features t_block_round r.(expected_features)
block_round.
End Expected_preendorsement.
Definition Expected_preendorsement_skeleton :=
Expected_preendorsement.record.
Module No_expected_branch_for_partial_construction_preendorsement.
Record record {expected_level : Set} : Set := Build {
expected_level : expected_level;
}.
Arguments record : clear implicits.
Definition with_expected_level {t_expected_level} expected_level
(r : record t_expected_level) :=
Build t_expected_level expected_level.
End No_expected_branch_for_partial_construction_preendorsement.
Definition
No_expected_branch_for_partial_construction_preendorsement_skeleton :=
No_expected_branch_for_partial_construction_preendorsement.record.
End expected_preendorsement.
End ConstructorRecords_expected_preendorsement.
Import ConstructorRecords_expected_preendorsement.
Reserved Notation "'expected_preendorsement.Expected_preendorsement".
Reserved Notation
"'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement".
Inductive expected_preendorsement : Set :=
| Expected_preendorsement :
'expected_preendorsement.Expected_preendorsement → expected_preendorsement
| No_locked_round_for_block_validation_preendorsement : expected_preendorsement
| Fresh_proposal_for_construction_preendorsement : expected_preendorsement
| No_expected_branch_for_partial_construction_preendorsement :
'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement
→ expected_preendorsement
| No_predecessor_info_cannot_validate_preendorsement : expected_preendorsement
where "'expected_preendorsement.Expected_preendorsement" :=
(expected_preendorsement.Expected_preendorsement_skeleton expected_features
(option Alpha_context.Round.t))
and "'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement"
:=
(expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement_skeleton
Alpha_context.Raw_level.t).
Module expected_preendorsement.
Include ConstructorRecords_expected_preendorsement.expected_preendorsement.
Definition Expected_preendorsement :=
'expected_preendorsement.Expected_preendorsement.
Definition No_expected_branch_for_partial_construction_preendorsement :=
'expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.
End expected_preendorsement.
Records for the constructor parameters
Module ConstructorRecords_expected_endorsement.
Module expected_endorsement.
Module Expected_endorsement.
Record record {expected_features : Set} : Set := Build {
expected_features : expected_features;
}.
Arguments record : clear implicits.
Definition with_expected_features {t_expected_features} expected_features
(r : record t_expected_features) :=
Build t_expected_features expected_features.
End Expected_endorsement.
Definition Expected_endorsement_skeleton := Expected_endorsement.record.
Module No_expected_branch_for_partial_construction_endorsement.
Record record {expected_level : Set} : Set := Build {
expected_level : expected_level;
}.
Arguments record : clear implicits.
Definition with_expected_level {t_expected_level} expected_level
(r : record t_expected_level) :=
Build t_expected_level expected_level.
End No_expected_branch_for_partial_construction_endorsement.
Definition No_expected_branch_for_partial_construction_endorsement_skeleton
:= No_expected_branch_for_partial_construction_endorsement.record.
End expected_endorsement.
End ConstructorRecords_expected_endorsement.
Import ConstructorRecords_expected_endorsement.
Reserved Notation "'expected_endorsement.Expected_endorsement".
Reserved Notation
"'expected_endorsement.No_expected_branch_for_partial_construction_endorsement".
Inductive expected_endorsement : Set :=
| Expected_endorsement :
'expected_endorsement.Expected_endorsement → expected_endorsement
| No_expected_branch_for_block_endorsement : expected_endorsement
| No_expected_branch_for_partial_construction_endorsement :
'expected_endorsement.No_expected_branch_for_partial_construction_endorsement
→ expected_endorsement
| No_predecessor_info_cannot_validate_endorsement : expected_endorsement
where "'expected_endorsement.Expected_endorsement" :=
(expected_endorsement.Expected_endorsement_skeleton expected_features)
and "'expected_endorsement.No_expected_branch_for_partial_construction_endorsement"
:=
(expected_endorsement.No_expected_branch_for_partial_construction_endorsement_skeleton
Alpha_context.Raw_level.t).
Module expected_endorsement.
Include ConstructorRecords_expected_endorsement.expected_endorsement.
Definition Expected_endorsement := 'expected_endorsement.Expected_endorsement.
Definition No_expected_branch_for_partial_construction_endorsement :=
'expected_endorsement.No_expected_branch_for_partial_construction_endorsement.
End expected_endorsement.
Module all_expected_consensus_features.
Record record : Set := Build {
expected_preendorsement : expected_preendorsement;
expected_endorsement : expected_endorsement;
expected_grandparent_endorsement_for_partial_construction :
option expected_features;
}.
Definition with_expected_preendorsement expected_preendorsement
(r : record) :=
Build expected_preendorsement r.(expected_endorsement)
r.(expected_grandparent_endorsement_for_partial_construction).
Definition with_expected_endorsement expected_endorsement (r : record) :=
Build r.(expected_preendorsement) expected_endorsement
r.(expected_grandparent_endorsement_for_partial_construction).
Definition with_expected_grandparent_endorsement_for_partial_construction
expected_grandparent_endorsement_for_partial_construction (r : record) :=
Build r.(expected_preendorsement) r.(expected_endorsement)
expected_grandparent_endorsement_for_partial_construction.
End all_expected_consensus_features.
Definition all_expected_consensus_features :=
all_expected_consensus_features.record.
Module consensus_info.
Record record : Set := Build {
all_expected_features : all_expected_consensus_features;
preendorsement_slot_map :
Alpha_context.Slot.Map.(Map.S.t) (Alpha_context.Consensus_key.pk × int);
endorsement_slot_map :
Alpha_context.Slot.Map.(Map.S.t) (Alpha_context.Consensus_key.pk × int);
}.
Definition with_all_expected_features all_expected_features (r : record) :=
Build all_expected_features r.(preendorsement_slot_map)
r.(endorsement_slot_map).
Definition with_preendorsement_slot_map preendorsement_slot_map
(r : record) :=
Build r.(all_expected_features) preendorsement_slot_map
r.(endorsement_slot_map).
Definition with_endorsement_slot_map endorsement_slot_map (r : record) :=
Build r.(all_expected_features) r.(preendorsement_slot_map)
endorsement_slot_map.
End consensus_info.
Definition consensus_info := consensus_info.record.
Definition init_consensus_info
(ctxt : Alpha_context.t)
(all_expected_features : all_expected_consensus_features) : consensus_info :=
{| consensus_info.all_expected_features := all_expected_features;
consensus_info.preendorsement_slot_map :=
Alpha_context.Consensus.allowed_preendorsements ctxt;
consensus_info.endorsement_slot_map :=
Alpha_context.Consensus.allowed_endorsements ctxt; |}.
Definition Consensus_content_map :=
Map.Make
(let t : Set := Alpha_context.consensus_content in
let compare (function_parameter : Alpha_context.consensus_content)
: Alpha_context.consensus_content → int :=
let '{|
Alpha_context.consensus_content.slot := slot;
Alpha_context.consensus_content.level := level;
Alpha_context.consensus_content.round := round;
Alpha_context.consensus_content.block_payload_hash :=
block_payload_hash
|} := function_parameter in
fun (function_parameter : Alpha_context.consensus_content) ⇒
let '{|
Alpha_context.consensus_content.slot := slot';
Alpha_context.consensus_content.level := level';
Alpha_context.consensus_content.round := round';
Alpha_context.consensus_content.block_payload_hash :=
block_payload_hash'
|} := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare level level')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Slot.compare slot slot')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare round round')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else
(Block_payload_hash.compare block_payload_hash
block_payload_hash')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0)))) in
{|
Compare.COMPARABLE.compare := compare
|}).
Module consensus_state.
Record record : Set := Build {
predecessor_level : Alpha_context.Raw_level.t;
preendorsements_seen : Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
endorsements_seen : Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
grandparent_endorsements_seen :
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
dal_attestation_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_predecessor_level predecessor_level (r : record) :=
Build predecessor_level r.(preendorsements_seen) r.(endorsements_seen)
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_preendorsements_seen preendorsements_seen (r : record) :=
Build r.(predecessor_level) preendorsements_seen r.(endorsements_seen)
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_endorsements_seen endorsements_seen (r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) endorsements_seen
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_grandparent_endorsements_seen grandparent_endorsements_seen
(r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) r.(endorsements_seen)
grandparent_endorsements_seen r.(dal_attestation_seen).
Definition with_dal_attestation_seen dal_attestation_seen (r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) r.(endorsements_seen)
r.(grandparent_endorsements_seen) dal_attestation_seen.
End consensus_state.
Definition consensus_state := consensus_state.record.
Definition slot_map_encoding {A : Set}
(element_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (Alpha_context.Slot.Map.(Map.S.t) A) :=
Data_encoding.conv
(fun (slot_map : Alpha_context.Slot.Map.(Map.S.t) A) ⇒
Alpha_context.Slot.Map.(Map.S.bindings) slot_map)
(fun (l_value : list (Alpha_context.Slot.t × A)) ⇒
List.fold_left
(fun (m_value : Alpha_context.Slot.Map.(Map.S.t) A) ⇒
fun (function_parameter : Alpha_context.Slot.t × A) ⇒
let '(k_value, v_value) := function_parameter in
Alpha_context.Slot.Map.(Map.S.add) k_value v_value m_value)
Alpha_context.Slot.Map.(Map.S.empty) l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Slot.encoding element_encoding)).
Definition consensus_state_encoding : Data_encoding.encoding consensus_state :=
Data_encoding.def "consensus_state" None None
(Data_encoding.conv
(fun (function_parameter : consensus_state) ⇒
let '{|
consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen := preendorsements_seen;
consensus_state.endorsements_seen := endorsements_seen;
consensus_state.grandparent_endorsements_seen :=
grandparent_endorsements_seen;
consensus_state.dal_attestation_seen := dal_attestation_seen
|} := function_parameter in
(predecessor_level, preendorsements_seen, endorsements_seen,
grandparent_endorsements_seen, dal_attestation_seen))
(fun (function_parameter :
Alpha_context.Raw_level.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
let
'(predecessor_level, preendorsements_seen, endorsements_seen,
grandparent_endorsements_seen, dal_attestation_seen) :=
function_parameter in
{| consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen := preendorsements_seen;
consensus_state.endorsements_seen := endorsements_seen;
consensus_state.grandparent_endorsements_seen :=
grandparent_endorsements_seen;
consensus_state.dal_attestation_seen := dal_attestation_seen; |}) None
(Data_encoding.obj5
(Data_encoding.req None None "predecessor_level"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "preendorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "endorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "grandparent_endorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "dal_attestation_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Definition init_consensus_state (predecessor_level : Alpha_context.Raw_level.t)
: consensus_state :=
{| consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.endorsements_seen := Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.grandparent_endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.dal_attestation_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Module voting_state.
Record record : Set := Build {
proposals_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
ballots_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_proposals_seen proposals_seen (r : record) :=
Build proposals_seen r.(ballots_seen).
Definition with_ballots_seen ballots_seen (r : record) :=
Build r.(proposals_seen) ballots_seen.
End voting_state.
Definition voting_state := voting_state.record.
Definition voting_state_encoding : Data_encoding.encoding voting_state :=
Data_encoding.def "voting_state" None None
(Data_encoding.conv
(fun (function_parameter : voting_state) ⇒
let '{|
voting_state.proposals_seen := proposals_seen;
voting_state.ballots_seen := ballots_seen
|} := function_parameter in
(proposals_seen, ballots_seen))
(fun (function_parameter :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t ×
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
let '(proposals_seen, ballots_seen) := function_parameter in
{| voting_state.proposals_seen := proposals_seen;
voting_state.ballots_seen := ballots_seen; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "proposals_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "ballots_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Module Double_baking_evidence_map.
Definition Map_Make_include :=
Map.Make
(let t : Set := Alpha_context.Raw_level.t × Alpha_context.Round.t in
let compare
(function_parameter : Alpha_context.Raw_level.t × Alpha_context.Round.t)
: Alpha_context.Raw_level.t × Alpha_context.Round.t → int :=
let '(l_value, r_value) := function_parameter in
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t) ⇒
let '(l', r') := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare l_value l')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare r_value r')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0)) in
{|
Compare.COMPARABLE.compare := compare
|}).
Module expected_endorsement.
Module Expected_endorsement.
Record record {expected_features : Set} : Set := Build {
expected_features : expected_features;
}.
Arguments record : clear implicits.
Definition with_expected_features {t_expected_features} expected_features
(r : record t_expected_features) :=
Build t_expected_features expected_features.
End Expected_endorsement.
Definition Expected_endorsement_skeleton := Expected_endorsement.record.
Module No_expected_branch_for_partial_construction_endorsement.
Record record {expected_level : Set} : Set := Build {
expected_level : expected_level;
}.
Arguments record : clear implicits.
Definition with_expected_level {t_expected_level} expected_level
(r : record t_expected_level) :=
Build t_expected_level expected_level.
End No_expected_branch_for_partial_construction_endorsement.
Definition No_expected_branch_for_partial_construction_endorsement_skeleton
:= No_expected_branch_for_partial_construction_endorsement.record.
End expected_endorsement.
End ConstructorRecords_expected_endorsement.
Import ConstructorRecords_expected_endorsement.
Reserved Notation "'expected_endorsement.Expected_endorsement".
Reserved Notation
"'expected_endorsement.No_expected_branch_for_partial_construction_endorsement".
Inductive expected_endorsement : Set :=
| Expected_endorsement :
'expected_endorsement.Expected_endorsement → expected_endorsement
| No_expected_branch_for_block_endorsement : expected_endorsement
| No_expected_branch_for_partial_construction_endorsement :
'expected_endorsement.No_expected_branch_for_partial_construction_endorsement
→ expected_endorsement
| No_predecessor_info_cannot_validate_endorsement : expected_endorsement
where "'expected_endorsement.Expected_endorsement" :=
(expected_endorsement.Expected_endorsement_skeleton expected_features)
and "'expected_endorsement.No_expected_branch_for_partial_construction_endorsement"
:=
(expected_endorsement.No_expected_branch_for_partial_construction_endorsement_skeleton
Alpha_context.Raw_level.t).
Module expected_endorsement.
Include ConstructorRecords_expected_endorsement.expected_endorsement.
Definition Expected_endorsement := 'expected_endorsement.Expected_endorsement.
Definition No_expected_branch_for_partial_construction_endorsement :=
'expected_endorsement.No_expected_branch_for_partial_construction_endorsement.
End expected_endorsement.
Module all_expected_consensus_features.
Record record : Set := Build {
expected_preendorsement : expected_preendorsement;
expected_endorsement : expected_endorsement;
expected_grandparent_endorsement_for_partial_construction :
option expected_features;
}.
Definition with_expected_preendorsement expected_preendorsement
(r : record) :=
Build expected_preendorsement r.(expected_endorsement)
r.(expected_grandparent_endorsement_for_partial_construction).
Definition with_expected_endorsement expected_endorsement (r : record) :=
Build r.(expected_preendorsement) expected_endorsement
r.(expected_grandparent_endorsement_for_partial_construction).
Definition with_expected_grandparent_endorsement_for_partial_construction
expected_grandparent_endorsement_for_partial_construction (r : record) :=
Build r.(expected_preendorsement) r.(expected_endorsement)
expected_grandparent_endorsement_for_partial_construction.
End all_expected_consensus_features.
Definition all_expected_consensus_features :=
all_expected_consensus_features.record.
Module consensus_info.
Record record : Set := Build {
all_expected_features : all_expected_consensus_features;
preendorsement_slot_map :
Alpha_context.Slot.Map.(Map.S.t) (Alpha_context.Consensus_key.pk × int);
endorsement_slot_map :
Alpha_context.Slot.Map.(Map.S.t) (Alpha_context.Consensus_key.pk × int);
}.
Definition with_all_expected_features all_expected_features (r : record) :=
Build all_expected_features r.(preendorsement_slot_map)
r.(endorsement_slot_map).
Definition with_preendorsement_slot_map preendorsement_slot_map
(r : record) :=
Build r.(all_expected_features) preendorsement_slot_map
r.(endorsement_slot_map).
Definition with_endorsement_slot_map endorsement_slot_map (r : record) :=
Build r.(all_expected_features) r.(preendorsement_slot_map)
endorsement_slot_map.
End consensus_info.
Definition consensus_info := consensus_info.record.
Definition init_consensus_info
(ctxt : Alpha_context.t)
(all_expected_features : all_expected_consensus_features) : consensus_info :=
{| consensus_info.all_expected_features := all_expected_features;
consensus_info.preendorsement_slot_map :=
Alpha_context.Consensus.allowed_preendorsements ctxt;
consensus_info.endorsement_slot_map :=
Alpha_context.Consensus.allowed_endorsements ctxt; |}.
Definition Consensus_content_map :=
Map.Make
(let t : Set := Alpha_context.consensus_content in
let compare (function_parameter : Alpha_context.consensus_content)
: Alpha_context.consensus_content → int :=
let '{|
Alpha_context.consensus_content.slot := slot;
Alpha_context.consensus_content.level := level;
Alpha_context.consensus_content.round := round;
Alpha_context.consensus_content.block_payload_hash :=
block_payload_hash
|} := function_parameter in
fun (function_parameter : Alpha_context.consensus_content) ⇒
let '{|
Alpha_context.consensus_content.slot := slot';
Alpha_context.consensus_content.level := level';
Alpha_context.consensus_content.round := round';
Alpha_context.consensus_content.block_payload_hash :=
block_payload_hash'
|} := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare level level')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Slot.compare slot slot')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare round round')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else
(Block_payload_hash.compare block_payload_hash
block_payload_hash')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0)))) in
{|
Compare.COMPARABLE.compare := compare
|}).
Module consensus_state.
Record record : Set := Build {
predecessor_level : Alpha_context.Raw_level.t;
preendorsements_seen : Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
endorsements_seen : Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
grandparent_endorsements_seen :
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t;
dal_attestation_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_predecessor_level predecessor_level (r : record) :=
Build predecessor_level r.(preendorsements_seen) r.(endorsements_seen)
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_preendorsements_seen preendorsements_seen (r : record) :=
Build r.(predecessor_level) preendorsements_seen r.(endorsements_seen)
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_endorsements_seen endorsements_seen (r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) endorsements_seen
r.(grandparent_endorsements_seen) r.(dal_attestation_seen).
Definition with_grandparent_endorsements_seen grandparent_endorsements_seen
(r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) r.(endorsements_seen)
grandparent_endorsements_seen r.(dal_attestation_seen).
Definition with_dal_attestation_seen dal_attestation_seen (r : record) :=
Build r.(predecessor_level) r.(preendorsements_seen) r.(endorsements_seen)
r.(grandparent_endorsements_seen) dal_attestation_seen.
End consensus_state.
Definition consensus_state := consensus_state.record.
Definition slot_map_encoding {A : Set}
(element_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (Alpha_context.Slot.Map.(Map.S.t) A) :=
Data_encoding.conv
(fun (slot_map : Alpha_context.Slot.Map.(Map.S.t) A) ⇒
Alpha_context.Slot.Map.(Map.S.bindings) slot_map)
(fun (l_value : list (Alpha_context.Slot.t × A)) ⇒
List.fold_left
(fun (m_value : Alpha_context.Slot.Map.(Map.S.t) A) ⇒
fun (function_parameter : Alpha_context.Slot.t × A) ⇒
let '(k_value, v_value) := function_parameter in
Alpha_context.Slot.Map.(Map.S.add) k_value v_value m_value)
Alpha_context.Slot.Map.(Map.S.empty) l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Slot.encoding element_encoding)).
Definition consensus_state_encoding : Data_encoding.encoding consensus_state :=
Data_encoding.def "consensus_state" None None
(Data_encoding.conv
(fun (function_parameter : consensus_state) ⇒
let '{|
consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen := preendorsements_seen;
consensus_state.endorsements_seen := endorsements_seen;
consensus_state.grandparent_endorsements_seen :=
grandparent_endorsements_seen;
consensus_state.dal_attestation_seen := dal_attestation_seen
|} := function_parameter in
(predecessor_level, preendorsements_seen, endorsements_seen,
grandparent_endorsements_seen, dal_attestation_seen))
(fun (function_parameter :
Alpha_context.Raw_level.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Alpha_context.Slot.Map.(Map.S.t) Operation_hash.t ×
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
let
'(predecessor_level, preendorsements_seen, endorsements_seen,
grandparent_endorsements_seen, dal_attestation_seen) :=
function_parameter in
{| consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen := preendorsements_seen;
consensus_state.endorsements_seen := endorsements_seen;
consensus_state.grandparent_endorsements_seen :=
grandparent_endorsements_seen;
consensus_state.dal_attestation_seen := dal_attestation_seen; |}) None
(Data_encoding.obj5
(Data_encoding.req None None "predecessor_level"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "preendorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "endorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "grandparent_endorsements_seen"
(slot_map_encoding Operation_hash.encoding))
(Data_encoding.req None None "dal_attestation_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Definition init_consensus_state (predecessor_level : Alpha_context.Raw_level.t)
: consensus_state :=
{| consensus_state.predecessor_level := predecessor_level;
consensus_state.preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.endorsements_seen := Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.grandparent_endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.empty);
consensus_state.dal_attestation_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Module voting_state.
Record record : Set := Build {
proposals_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
ballots_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_proposals_seen proposals_seen (r : record) :=
Build proposals_seen r.(ballots_seen).
Definition with_ballots_seen ballots_seen (r : record) :=
Build r.(proposals_seen) ballots_seen.
End voting_state.
Definition voting_state := voting_state.record.
Definition voting_state_encoding : Data_encoding.encoding voting_state :=
Data_encoding.def "voting_state" None None
(Data_encoding.conv
(fun (function_parameter : voting_state) ⇒
let '{|
voting_state.proposals_seen := proposals_seen;
voting_state.ballots_seen := ballots_seen
|} := function_parameter in
(proposals_seen, ballots_seen))
(fun (function_parameter :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t ×
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
let '(proposals_seen, ballots_seen) := function_parameter in
{| voting_state.proposals_seen := proposals_seen;
voting_state.ballots_seen := ballots_seen; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "proposals_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "ballots_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Module Double_baking_evidence_map.
Definition Map_Make_include :=
Map.Make
(let t : Set := Alpha_context.Raw_level.t × Alpha_context.Round.t in
let compare
(function_parameter : Alpha_context.Raw_level.t × Alpha_context.Round.t)
: Alpha_context.Raw_level.t × Alpha_context.Round.t → int :=
let '(l_value, r_value) := function_parameter in
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t) ⇒
let '(l', r') := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare l_value l')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare r_value r')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0)) in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Map_Make_include]
Definition key := Map_Make_include.(Map.S.key).
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv (fun (map : t A) ⇒ bindings map)
(fun (l_value : list (key × A)) ⇒
List.fold_left
(fun (m_value : t A) ⇒
fun (function_parameter : key × A) ⇒
let '(k_value, v_value) := function_parameter in
add k_value v_value m_value) empty l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.tup2 Alpha_context.Raw_level.encoding
Alpha_context.Round.encoding) elt_encoding)).
(* Double_baking_evidence_map *)
Definition module :=
{|
S.INDEXES_MAP.empty _ := empty;
S.INDEXES_MAP.is_empty _ := is_empty;
S.INDEXES_MAP.mem _ := mem;
S.INDEXES_MAP.add _ := add;
S.INDEXES_MAP.update _ := update;
S.INDEXES_MAP.singleton _ := singleton;
S.INDEXES_MAP.remove _ := remove;
S.INDEXES_MAP.merge _ _ _ := merge;
S.INDEXES_MAP.union _ := union;
S.INDEXES_MAP.compare _ := compare;
S.INDEXES_MAP.equal _ := equal;
S.INDEXES_MAP.iter _ := iter;
S.INDEXES_MAP.iter_e _ _ := iter_e;
S.INDEXES_MAP.iter_s _ := iter_s;
S.INDEXES_MAP.iter_p _ := iter_p;
S.INDEXES_MAP.iter_es _ _ := iter_es;
S.INDEXES_MAP.fold _ _ := fold;
S.INDEXES_MAP.fold_e _ _ _ := fold_e;
S.INDEXES_MAP.fold_s _ _ := fold_s;
S.INDEXES_MAP.fold_es _ _ _ := fold_es;
S.INDEXES_MAP.for_all _ := for_all;
S.INDEXES_MAP._exists _ := _exists;
S.INDEXES_MAP.filter _ := filter;
S.INDEXES_MAP.filter_map _ _ := filter_map;
S.INDEXES_MAP.partition _ := partition;
S.INDEXES_MAP.cardinal _ := cardinal;
S.INDEXES_MAP.bindings _ := bindings;
S.INDEXES_MAP.min_binding _ := min_binding;
S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
S.INDEXES_MAP.max_binding _ := max_binding;
S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
S.INDEXES_MAP.choose _ := choose;
S.INDEXES_MAP.choose_opt _ := choose_opt;
S.INDEXES_MAP.split _ := split;
S.INDEXES_MAP.find _ := find;
S.INDEXES_MAP.find_opt _ := find_opt;
S.INDEXES_MAP.find_first _ := find_first;
S.INDEXES_MAP.find_first_opt _ := find_first_opt;
S.INDEXES_MAP.find_last _ := find_last;
S.INDEXES_MAP.find_last_opt _ := find_last_opt;
S.INDEXES_MAP.map _ _ := map;
S.INDEXES_MAP.mapi _ _ := mapi;
S.INDEXES_MAP.to_seq _ := to_seq;
S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
S.INDEXES_MAP.to_seq_from _ := to_seq_from;
S.INDEXES_MAP.add_seq _ := add_seq;
S.INDEXES_MAP.of_seq _ := of_seq;
S.INDEXES_MAP.iter_ep _ _ := iter_ep;
S.INDEXES_MAP.encoding _ := encoding
|}.
End Double_baking_evidence_map.
Definition Double_baking_evidence_map := Double_baking_evidence_map.module.
Module Double_endorsing_evidence_map.
Definition Map_Make_include :=
Map.Make
(let t : Set :=
Alpha_context.Raw_level.t × Alpha_context.Round.t × Alpha_context.Slot.t
in
let compare
(function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t)
: Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t → int :=
let '(l_value, r_value, s_value) := function_parameter in
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t) ⇒
let '(l', r', s') := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare l_value l')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare r_value r')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Slot.compare s_value s')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0))) in
{|
Compare.COMPARABLE.compare := compare
|}).
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv (fun (map : t A) ⇒ bindings map)
(fun (l_value : list (key × A)) ⇒
List.fold_left
(fun (m_value : t A) ⇒
fun (function_parameter : key × A) ⇒
let '(k_value, v_value) := function_parameter in
add k_value v_value m_value) empty l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.tup2 Alpha_context.Raw_level.encoding
Alpha_context.Round.encoding) elt_encoding)).
(* Double_baking_evidence_map *)
Definition module :=
{|
S.INDEXES_MAP.empty _ := empty;
S.INDEXES_MAP.is_empty _ := is_empty;
S.INDEXES_MAP.mem _ := mem;
S.INDEXES_MAP.add _ := add;
S.INDEXES_MAP.update _ := update;
S.INDEXES_MAP.singleton _ := singleton;
S.INDEXES_MAP.remove _ := remove;
S.INDEXES_MAP.merge _ _ _ := merge;
S.INDEXES_MAP.union _ := union;
S.INDEXES_MAP.compare _ := compare;
S.INDEXES_MAP.equal _ := equal;
S.INDEXES_MAP.iter _ := iter;
S.INDEXES_MAP.iter_e _ _ := iter_e;
S.INDEXES_MAP.iter_s _ := iter_s;
S.INDEXES_MAP.iter_p _ := iter_p;
S.INDEXES_MAP.iter_es _ _ := iter_es;
S.INDEXES_MAP.fold _ _ := fold;
S.INDEXES_MAP.fold_e _ _ _ := fold_e;
S.INDEXES_MAP.fold_s _ _ := fold_s;
S.INDEXES_MAP.fold_es _ _ _ := fold_es;
S.INDEXES_MAP.for_all _ := for_all;
S.INDEXES_MAP._exists _ := _exists;
S.INDEXES_MAP.filter _ := filter;
S.INDEXES_MAP.filter_map _ _ := filter_map;
S.INDEXES_MAP.partition _ := partition;
S.INDEXES_MAP.cardinal _ := cardinal;
S.INDEXES_MAP.bindings _ := bindings;
S.INDEXES_MAP.min_binding _ := min_binding;
S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
S.INDEXES_MAP.max_binding _ := max_binding;
S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
S.INDEXES_MAP.choose _ := choose;
S.INDEXES_MAP.choose_opt _ := choose_opt;
S.INDEXES_MAP.split _ := split;
S.INDEXES_MAP.find _ := find;
S.INDEXES_MAP.find_opt _ := find_opt;
S.INDEXES_MAP.find_first _ := find_first;
S.INDEXES_MAP.find_first_opt _ := find_first_opt;
S.INDEXES_MAP.find_last _ := find_last;
S.INDEXES_MAP.find_last_opt _ := find_last_opt;
S.INDEXES_MAP.map _ _ := map;
S.INDEXES_MAP.mapi _ _ := mapi;
S.INDEXES_MAP.to_seq _ := to_seq;
S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
S.INDEXES_MAP.to_seq_from _ := to_seq_from;
S.INDEXES_MAP.add_seq _ := add_seq;
S.INDEXES_MAP.of_seq _ := of_seq;
S.INDEXES_MAP.iter_ep _ _ := iter_ep;
S.INDEXES_MAP.encoding _ := encoding
|}.
End Double_baking_evidence_map.
Definition Double_baking_evidence_map := Double_baking_evidence_map.module.
Module Double_endorsing_evidence_map.
Definition Map_Make_include :=
Map.Make
(let t : Set :=
Alpha_context.Raw_level.t × Alpha_context.Round.t × Alpha_context.Slot.t
in
let compare
(function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t)
: Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t → int :=
let '(l_value, r_value, s_value) := function_parameter in
fun (function_parameter :
Alpha_context.Raw_level.t × Alpha_context.Round.t ×
Alpha_context.Slot.t) ⇒
let '(l', r', s') := function_parameter in
Compare.or_else (Alpha_context.Raw_level.compare l_value l')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Round.compare r_value r')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Compare.or_else (Alpha_context.Slot.compare s_value s')
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
0))) in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Map_Make_include]
Definition key := Map_Make_include.(Map.S.key).
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv (fun (map : t A) ⇒ bindings map)
(fun (l_value : list (key × A)) ⇒
List.fold_left
(fun (m_value : t A) ⇒
fun (function_parameter : key × A) ⇒
let '(k_value, v_value) := function_parameter in
add k_value v_value m_value) empty l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.tup3 Alpha_context.Raw_level.encoding
Alpha_context.Round.encoding Alpha_context.Slot.encoding)
elt_encoding)).
(* Double_endorsing_evidence_map *)
Definition module :=
{|
S.INDEXES_MAP.empty _ := empty;
S.INDEXES_MAP.is_empty _ := is_empty;
S.INDEXES_MAP.mem _ := mem;
S.INDEXES_MAP.add _ := add;
S.INDEXES_MAP.update _ := update;
S.INDEXES_MAP.singleton _ := singleton;
S.INDEXES_MAP.remove _ := remove;
S.INDEXES_MAP.merge _ _ _ := merge;
S.INDEXES_MAP.union _ := union;
S.INDEXES_MAP.compare _ := compare;
S.INDEXES_MAP.equal _ := equal;
S.INDEXES_MAP.iter _ := iter;
S.INDEXES_MAP.iter_e _ _ := iter_e;
S.INDEXES_MAP.iter_s _ := iter_s;
S.INDEXES_MAP.iter_p _ := iter_p;
S.INDEXES_MAP.iter_es _ _ := iter_es;
S.INDEXES_MAP.fold _ _ := fold;
S.INDEXES_MAP.fold_e _ _ _ := fold_e;
S.INDEXES_MAP.fold_s _ _ := fold_s;
S.INDEXES_MAP.fold_es _ _ _ := fold_es;
S.INDEXES_MAP.for_all _ := for_all;
S.INDEXES_MAP._exists _ := _exists;
S.INDEXES_MAP.filter _ := filter;
S.INDEXES_MAP.filter_map _ _ := filter_map;
S.INDEXES_MAP.partition _ := partition;
S.INDEXES_MAP.cardinal _ := cardinal;
S.INDEXES_MAP.bindings _ := bindings;
S.INDEXES_MAP.min_binding _ := min_binding;
S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
S.INDEXES_MAP.max_binding _ := max_binding;
S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
S.INDEXES_MAP.choose _ := choose;
S.INDEXES_MAP.choose_opt _ := choose_opt;
S.INDEXES_MAP.split _ := split;
S.INDEXES_MAP.find _ := find;
S.INDEXES_MAP.find_opt _ := find_opt;
S.INDEXES_MAP.find_first _ := find_first;
S.INDEXES_MAP.find_first_opt _ := find_first_opt;
S.INDEXES_MAP.find_last _ := find_last;
S.INDEXES_MAP.find_last_opt _ := find_last_opt;
S.INDEXES_MAP.map _ _ := map;
S.INDEXES_MAP.mapi _ _ := mapi;
S.INDEXES_MAP.to_seq _ := to_seq;
S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
S.INDEXES_MAP.to_seq_from _ := to_seq_from;
S.INDEXES_MAP.add_seq _ := add_seq;
S.INDEXES_MAP.of_seq _ := of_seq;
S.INDEXES_MAP.iter_ep _ _ := iter_ep;
S.INDEXES_MAP.encoding _ := encoding
|}.
End Double_endorsing_evidence_map.
Definition Double_endorsing_evidence_map :=
Double_endorsing_evidence_map.module.
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (t A) :=
Data_encoding.conv (fun (map : t A) ⇒ bindings map)
(fun (l_value : list (key × A)) ⇒
List.fold_left
(fun (m_value : t A) ⇒
fun (function_parameter : key × A) ⇒
let '(k_value, v_value) := function_parameter in
add k_value v_value m_value) empty l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2
(Data_encoding.tup3 Alpha_context.Raw_level.encoding
Alpha_context.Round.encoding Alpha_context.Slot.encoding)
elt_encoding)).
(* Double_endorsing_evidence_map *)
Definition module :=
{|
S.INDEXES_MAP.empty _ := empty;
S.INDEXES_MAP.is_empty _ := is_empty;
S.INDEXES_MAP.mem _ := mem;
S.INDEXES_MAP.add _ := add;
S.INDEXES_MAP.update _ := update;
S.INDEXES_MAP.singleton _ := singleton;
S.INDEXES_MAP.remove _ := remove;
S.INDEXES_MAP.merge _ _ _ := merge;
S.INDEXES_MAP.union _ := union;
S.INDEXES_MAP.compare _ := compare;
S.INDEXES_MAP.equal _ := equal;
S.INDEXES_MAP.iter _ := iter;
S.INDEXES_MAP.iter_e _ _ := iter_e;
S.INDEXES_MAP.iter_s _ := iter_s;
S.INDEXES_MAP.iter_p _ := iter_p;
S.INDEXES_MAP.iter_es _ _ := iter_es;
S.INDEXES_MAP.fold _ _ := fold;
S.INDEXES_MAP.fold_e _ _ _ := fold_e;
S.INDEXES_MAP.fold_s _ _ := fold_s;
S.INDEXES_MAP.fold_es _ _ _ := fold_es;
S.INDEXES_MAP.for_all _ := for_all;
S.INDEXES_MAP._exists _ := _exists;
S.INDEXES_MAP.filter _ := filter;
S.INDEXES_MAP.filter_map _ _ := filter_map;
S.INDEXES_MAP.partition _ := partition;
S.INDEXES_MAP.cardinal _ := cardinal;
S.INDEXES_MAP.bindings _ := bindings;
S.INDEXES_MAP.min_binding _ := min_binding;
S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
S.INDEXES_MAP.max_binding _ := max_binding;
S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
S.INDEXES_MAP.choose _ := choose;
S.INDEXES_MAP.choose_opt _ := choose_opt;
S.INDEXES_MAP.split _ := split;
S.INDEXES_MAP.find _ := find;
S.INDEXES_MAP.find_opt _ := find_opt;
S.INDEXES_MAP.find_first _ := find_first;
S.INDEXES_MAP.find_first_opt _ := find_first_opt;
S.INDEXES_MAP.find_last _ := find_last;
S.INDEXES_MAP.find_last_opt _ := find_last_opt;
S.INDEXES_MAP.map _ _ := map;
S.INDEXES_MAP.mapi _ _ := mapi;
S.INDEXES_MAP.to_seq _ := to_seq;
S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
S.INDEXES_MAP.to_seq_from _ := to_seq_from;
S.INDEXES_MAP.add_seq _ := add_seq;
S.INDEXES_MAP.of_seq _ := of_seq;
S.INDEXES_MAP.iter_ep _ _ := iter_ep;
S.INDEXES_MAP.encoding _ := encoding
|}.
End Double_endorsing_evidence_map.
Definition Double_endorsing_evidence_map :=
Double_endorsing_evidence_map.module.
State used and modified when validating anonymous operations.
These fields are used to enforce that we do not validate the same
operation multiple times.
Note that as part of {!state}, these maps live
in memory. They are not explicitly bounded here, however:
- In block validation mode, they are bounded by the number of
anonymous operations allowed in the block.
- In mempool mode, bounding the number of operations in this map
is the responsability of the prevalidator on the shell side.
Module anonymous_state.
Record record : Set := Build {
activation_pkhs_seen :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
double_baking_evidences_seen :
Double_baking_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t;
double_endorsing_evidences_seen :
Double_endorsing_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t;
seed_nonce_levels_seen :
Alpha_context.Raw_level.Map.(Map.S.t) Operation_hash.t;
vdf_solution_seen : option Operation_hash.t;
}.
Definition with_activation_pkhs_seen activation_pkhs_seen (r : record) :=
Build activation_pkhs_seen r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_double_baking_evidences_seen double_baking_evidences_seen
(r : record) :=
Build r.(activation_pkhs_seen) double_baking_evidences_seen
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_double_endorsing_evidences_seen
double_endorsing_evidences_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
double_endorsing_evidences_seen r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_seed_nonce_levels_seen seed_nonce_levels_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) seed_nonce_levels_seen
r.(vdf_solution_seen).
Definition with_vdf_solution_seen vdf_solution_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
vdf_solution_seen.
End anonymous_state.
Definition anonymous_state := anonymous_state.record.
Definition raw_level_map_encoding {A : Set}
(elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (Alpha_context.Raw_level.Map.(Map.S.t) A) :=
Data_encoding.conv
(fun (map : Alpha_context.Raw_level.Map.(Map.S.t) A) ⇒
Alpha_context.Raw_level.Map.(Map.S.bindings) map)
(fun (l_value : list (Raw_level_repr.t × A)) ⇒
List.fold_left
(fun (m_value : Alpha_context.Raw_level.Map.(Map.S.t) A) ⇒
fun (function_parameter : Raw_level_repr.t × A) ⇒
let '(k_value, v_value) := function_parameter in
Alpha_context.Raw_level.Map.(Map.S.add) k_value v_value m_value)
Alpha_context.Raw_level.Map.(Map.S.empty) l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Raw_level.encoding elt_encoding)).
Definition anonymous_state_encoding : Data_encoding.encoding anonymous_state :=
Data_encoding.def "anonymous_state" None None
(Data_encoding.conv
(fun (function_parameter : anonymous_state) ⇒
let '{|
anonymous_state.activation_pkhs_seen := activation_pkhs_seen;
anonymous_state.double_baking_evidences_seen :=
double_baking_evidences_seen;
anonymous_state.double_endorsing_evidences_seen :=
double_endorsing_evidences_seen;
anonymous_state.seed_nonce_levels_seen := seed_nonce_levels_seen;
anonymous_state.vdf_solution_seen := vdf_solution_seen
|} := function_parameter in
(activation_pkhs_seen, double_baking_evidences_seen,
double_endorsing_evidences_seen, seed_nonce_levels_seen,
vdf_solution_seen))
(fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t ×
Double_baking_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t ×
Double_endorsing_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t ×
Alpha_context.Raw_level.Map.(Map.S.t) Operation_hash.t ×
option Operation_hash.t) ⇒
let
'(activation_pkhs_seen, double_baking_evidences_seen,
double_endorsing_evidences_seen, seed_nonce_levels_seen,
vdf_solution_seen) := function_parameter in
{| anonymous_state.activation_pkhs_seen := activation_pkhs_seen;
anonymous_state.double_baking_evidences_seen :=
double_baking_evidences_seen;
anonymous_state.double_endorsing_evidences_seen :=
double_endorsing_evidences_seen;
anonymous_state.seed_nonce_levels_seen := seed_nonce_levels_seen;
anonymous_state.vdf_solution_seen := vdf_solution_seen; |}) None
(Data_encoding.obj5
(Data_encoding.req None None "activation_pkhs_seen"
(Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "double_baking_evidences_seen"
(Double_baking_evidence_map.(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "double_endorsing_evidences_seen"
(Double_endorsing_evidence_map.(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "seed_nonce_levels_seen"
(raw_level_map_encoding Operation_hash.encoding))
(Data_encoding.opt None None "vdf_solution_seen" Operation_hash.encoding))).
Definition empty_anonymous_state : anonymous_state :=
{|
anonymous_state.activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
anonymous_state.double_baking_evidences_seen :=
Double_baking_evidence_map.(S.INDEXES_MAP.empty);
anonymous_state.double_endorsing_evidences_seen :=
Double_endorsing_evidence_map.(S.INDEXES_MAP.empty);
anonymous_state.seed_nonce_levels_seen :=
Alpha_context.Raw_level.Map.(Map.S.empty);
anonymous_state.vdf_solution_seen := None; |}.
Record record : Set := Build {
activation_pkhs_seen :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
double_baking_evidences_seen :
Double_baking_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t;
double_endorsing_evidences_seen :
Double_endorsing_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t;
seed_nonce_levels_seen :
Alpha_context.Raw_level.Map.(Map.S.t) Operation_hash.t;
vdf_solution_seen : option Operation_hash.t;
}.
Definition with_activation_pkhs_seen activation_pkhs_seen (r : record) :=
Build activation_pkhs_seen r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_double_baking_evidences_seen double_baking_evidences_seen
(r : record) :=
Build r.(activation_pkhs_seen) double_baking_evidences_seen
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_double_endorsing_evidences_seen
double_endorsing_evidences_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
double_endorsing_evidences_seen r.(seed_nonce_levels_seen)
r.(vdf_solution_seen).
Definition with_seed_nonce_levels_seen seed_nonce_levels_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) seed_nonce_levels_seen
r.(vdf_solution_seen).
Definition with_vdf_solution_seen vdf_solution_seen (r : record) :=
Build r.(activation_pkhs_seen) r.(double_baking_evidences_seen)
r.(double_endorsing_evidences_seen) r.(seed_nonce_levels_seen)
vdf_solution_seen.
End anonymous_state.
Definition anonymous_state := anonymous_state.record.
Definition raw_level_map_encoding {A : Set}
(elt_encoding : Data_encoding.encoding A)
: Data_encoding.encoding (Alpha_context.Raw_level.Map.(Map.S.t) A) :=
Data_encoding.conv
(fun (map : Alpha_context.Raw_level.Map.(Map.S.t) A) ⇒
Alpha_context.Raw_level.Map.(Map.S.bindings) map)
(fun (l_value : list (Raw_level_repr.t × A)) ⇒
List.fold_left
(fun (m_value : Alpha_context.Raw_level.Map.(Map.S.t) A) ⇒
fun (function_parameter : Raw_level_repr.t × A) ⇒
let '(k_value, v_value) := function_parameter in
Alpha_context.Raw_level.Map.(Map.S.add) k_value v_value m_value)
Alpha_context.Raw_level.Map.(Map.S.empty) l_value) None
(Data_encoding.list_value None
(Data_encoding.tup2 Alpha_context.Raw_level.encoding elt_encoding)).
Definition anonymous_state_encoding : Data_encoding.encoding anonymous_state :=
Data_encoding.def "anonymous_state" None None
(Data_encoding.conv
(fun (function_parameter : anonymous_state) ⇒
let '{|
anonymous_state.activation_pkhs_seen := activation_pkhs_seen;
anonymous_state.double_baking_evidences_seen :=
double_baking_evidences_seen;
anonymous_state.double_endorsing_evidences_seen :=
double_endorsing_evidences_seen;
anonymous_state.seed_nonce_levels_seen := seed_nonce_levels_seen;
anonymous_state.vdf_solution_seen := vdf_solution_seen
|} := function_parameter in
(activation_pkhs_seen, double_baking_evidences_seen,
double_endorsing_evidences_seen, seed_nonce_levels_seen,
vdf_solution_seen))
(fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t ×
Double_baking_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t ×
Double_endorsing_evidence_map.(S.INDEXES_MAP.t) Operation_hash.t ×
Alpha_context.Raw_level.Map.(Map.S.t) Operation_hash.t ×
option Operation_hash.t) ⇒
let
'(activation_pkhs_seen, double_baking_evidences_seen,
double_endorsing_evidences_seen, seed_nonce_levels_seen,
vdf_solution_seen) := function_parameter in
{| anonymous_state.activation_pkhs_seen := activation_pkhs_seen;
anonymous_state.double_baking_evidences_seen :=
double_baking_evidences_seen;
anonymous_state.double_endorsing_evidences_seen :=
double_endorsing_evidences_seen;
anonymous_state.seed_nonce_levels_seen := seed_nonce_levels_seen;
anonymous_state.vdf_solution_seen := vdf_solution_seen; |}) None
(Data_encoding.obj5
(Data_encoding.req None None "activation_pkhs_seen"
(Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "double_baking_evidences_seen"
(Double_baking_evidence_map.(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "double_endorsing_evidences_seen"
(Double_endorsing_evidence_map.(S.INDEXES_MAP.encoding)
Operation_hash.encoding))
(Data_encoding.req None None "seed_nonce_levels_seen"
(raw_level_map_encoding Operation_hash.encoding))
(Data_encoding.opt None None "vdf_solution_seen" Operation_hash.encoding))).
Definition empty_anonymous_state : anonymous_state :=
{|
anonymous_state.activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
anonymous_state.double_baking_evidences_seen :=
Double_baking_evidence_map.(S.INDEXES_MAP.empty);
anonymous_state.double_endorsing_evidences_seen :=
Double_endorsing_evidence_map.(S.INDEXES_MAP.empty);
anonymous_state.seed_nonce_levels_seen :=
Alpha_context.Raw_level.Map.(Map.S.empty);
anonymous_state.vdf_solution_seen := None; |}.
Static information used to validate manager operations.
Module manager_info.
Record record : Set := Build {
hard_storage_limit_per_operation : Z.t;
hard_gas_limit_per_operation : Alpha_context.Gas.Arith.integral;
}.
Definition with_hard_storage_limit_per_operation
hard_storage_limit_per_operation (r : record) :=
Build hard_storage_limit_per_operation r.(hard_gas_limit_per_operation).
Definition with_hard_gas_limit_per_operation hard_gas_limit_per_operation
(r : record) :=
Build r.(hard_storage_limit_per_operation) hard_gas_limit_per_operation.
End manager_info.
Definition manager_info := manager_info.record.
Definition init_manager_info (ctxt : Alpha_context.context) : manager_info :=
{|
manager_info.hard_storage_limit_per_operation :=
Alpha_context.Constants.hard_storage_limit_per_operation ctxt;
manager_info.hard_gas_limit_per_operation :=
Alpha_context.Constants.hard_gas_limit_per_operation ctxt; |}.
Record record : Set := Build {
hard_storage_limit_per_operation : Z.t;
hard_gas_limit_per_operation : Alpha_context.Gas.Arith.integral;
}.
Definition with_hard_storage_limit_per_operation
hard_storage_limit_per_operation (r : record) :=
Build hard_storage_limit_per_operation r.(hard_gas_limit_per_operation).
Definition with_hard_gas_limit_per_operation hard_gas_limit_per_operation
(r : record) :=
Build r.(hard_storage_limit_per_operation) hard_gas_limit_per_operation.
End manager_info.
Definition manager_info := manager_info.record.
Definition init_manager_info (ctxt : Alpha_context.context) : manager_info :=
{|
manager_info.hard_storage_limit_per_operation :=
Alpha_context.Constants.hard_storage_limit_per_operation ctxt;
manager_info.hard_gas_limit_per_operation :=
Alpha_context.Constants.hard_gas_limit_per_operation ctxt; |}.
State used and modified when validating manager operations.
Module manager_state.
Record record : Set := Build {
managers_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_managers_seen managers_seen (r : record) :=
Build managers_seen.
End manager_state.
Definition manager_state := manager_state.record.
Definition manager_state_encoding : Data_encoding.encoding manager_state :=
Data_encoding.def "manager_state" None None
(Data_encoding.conv
(fun (function_parameter : manager_state) ⇒
let '{| manager_state.managers_seen := managers_seen |} :=
function_parameter in
managers_seen)
(fun (managers_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
{| manager_state.managers_seen := managers_seen; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "managers_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Definition empty_manager_state : manager_state :=
{|
manager_state.managers_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Record record : Set := Build {
managers_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t;
}.
Definition with_managers_seen managers_seen (r : record) :=
Build managers_seen.
End manager_state.
Definition manager_state := manager_state.record.
Definition manager_state_encoding : Data_encoding.encoding manager_state :=
Data_encoding.def "manager_state" None None
(Data_encoding.conv
(fun (function_parameter : manager_state) ⇒
let '{| manager_state.managers_seen := managers_seen |} :=
function_parameter in
managers_seen)
(fun (managers_seen :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Operation_hash.t) ⇒
{| manager_state.managers_seen := managers_seen; |}) None
(Data_encoding.obj1
(Data_encoding.req None None "managers_seen"
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
Operation_hash.encoding)))).
Definition empty_manager_state : manager_state :=
{|
manager_state.managers_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Mode-dependent information needed in final checks.
Module block_finalization_info.
Record record : Set := Build {
fitness : Alpha_context.Fitness.t;
block_producer : Alpha_context.Consensus_key.pk;
payload_producer : Alpha_context.Consensus_key.pk;
predecessor_hash : Block_hash.t;
block_data_contents : Alpha_context.Block_header.contents;
}.
Definition with_fitness fitness (r : record) :=
Build fitness r.(block_producer) r.(payload_producer) r.(predecessor_hash)
r.(block_data_contents).
Definition with_block_producer block_producer (r : record) :=
Build r.(fitness) block_producer r.(payload_producer) r.(predecessor_hash)
r.(block_data_contents).
Definition with_payload_producer payload_producer (r : record) :=
Build r.(fitness) r.(block_producer) payload_producer r.(predecessor_hash)
r.(block_data_contents).
Definition with_predecessor_hash predecessor_hash (r : record) :=
Build r.(fitness) r.(block_producer) r.(payload_producer) predecessor_hash
r.(block_data_contents).
Definition with_block_data_contents block_data_contents (r : record) :=
Build r.(fitness) r.(block_producer) r.(payload_producer)
r.(predecessor_hash) block_data_contents.
End block_finalization_info.
Definition block_finalization_info := block_finalization_info.record.
Record record : Set := Build {
fitness : Alpha_context.Fitness.t;
block_producer : Alpha_context.Consensus_key.pk;
payload_producer : Alpha_context.Consensus_key.pk;
predecessor_hash : Block_hash.t;
block_data_contents : Alpha_context.Block_header.contents;
}.
Definition with_fitness fitness (r : record) :=
Build fitness r.(block_producer) r.(payload_producer) r.(predecessor_hash)
r.(block_data_contents).
Definition with_block_producer block_producer (r : record) :=
Build r.(fitness) block_producer r.(payload_producer) r.(predecessor_hash)
r.(block_data_contents).
Definition with_payload_producer payload_producer (r : record) :=
Build r.(fitness) r.(block_producer) payload_producer r.(predecessor_hash)
r.(block_data_contents).
Definition with_predecessor_hash predecessor_hash (r : record) :=
Build r.(fitness) r.(block_producer) r.(payload_producer) predecessor_hash
r.(block_data_contents).
Definition with_block_data_contents block_data_contents (r : record) :=
Build r.(fitness) r.(block_producer) r.(payload_producer)
r.(predecessor_hash) block_data_contents.
End block_finalization_info.
Definition block_finalization_info := block_finalization_info.record.
Circumstances in which operations are validated, and corresponding
information.
- [Application] is used for the validation of a preexisting block,
often in preparation for its future application.
- [Partial_validation] is used to quickly but partially validate a
preexisting block, e.g. to quickly decide whether an alternate
branch seems viable. In this mode, the initial {!type:context} may
come from an ancestor block instead of the predecessor block. Only
consensus operations are validated in this mode.
- [Construction] is used for the construction of a new block.
- [Mempool] is used by the {!module:Mempool} and by the
[Partial_construction] mode in {!module:Main}, which may itself be
used by RPCs or by another mempool implementation. (The [Mempool]
mode is also used by the plugin.)
If you add a new mode, please make sure that it has a way to bound
the size of the map {!recfield:manager_state.managers_seen}. Records for the constructor parameters
Module ConstructorRecords_mode.
Module mode.
Module Construction.
Record record {predecessor_round predecessor_hash round
block_data_contents block_producer payload_producer : Set} : Set := Build {
predecessor_round : predecessor_round;
predecessor_hash : predecessor_hash;
round : round;
block_data_contents : block_data_contents;
block_producer : block_producer;
payload_producer : payload_producer;
}.
Arguments record : clear implicits.
Definition with_predecessor_round
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} predecessor_round
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
predecessor_round r.(predecessor_hash) r.(round)
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_predecessor_hash
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} predecessor_hash
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) predecessor_hash r.(round)
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_round
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} round
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) round
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_block_data_contents
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} block_data_contents
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
block_data_contents r.(block_producer) r.(payload_producer).
Definition with_block_producer
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} block_producer
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
r.(block_data_contents) block_producer r.(payload_producer).
Definition with_payload_producer
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} payload_producer
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
r.(block_data_contents) r.(block_producer) payload_producer.
End Construction.
Definition Construction_skeleton := Construction.record.
End mode.
End ConstructorRecords_mode.
Import ConstructorRecords_mode.
Reserved Notation "'mode.Construction".
Inductive mode : Set :=
| Application : block_finalization_info → mode
| Partial_validation : block_finalization_info → mode
| Construction : 'mode.Construction → mode
| Mempool : mode
where "'mode.Construction" :=
(mode.Construction_skeleton Alpha_context.Round.t Block_hash.t
Alpha_context.Round.t Alpha_context.Block_header.contents
Alpha_context.Consensus_key.pk Alpha_context.Consensus_key.pk).
Module mode.
Include ConstructorRecords_mode.mode.
Definition Construction := 'mode.Construction.
End mode.
Module info.
Record record : Set := Build {
ctxt : Alpha_context.t;
mode : mode;
chain_id : Chain_id.t;
current_level : Alpha_context.Level.t;
consensus_info : consensus_info;
manager_info : manager_info;
}.
Definition with_ctxt ctxt (r : record) :=
Build ctxt r.(mode) r.(chain_id) r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_mode mode (r : record) :=
Build r.(ctxt) mode r.(chain_id) r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_chain_id chain_id (r : record) :=
Build r.(ctxt) r.(mode) chain_id r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_current_level current_level (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) current_level r.(consensus_info)
r.(manager_info).
Definition with_consensus_info consensus_info (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) r.(current_level) consensus_info
r.(manager_info).
Definition with_manager_info manager_info (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) r.(current_level) r.(consensus_info)
manager_info.
End info.
Definition info := info.record.
Module operation_conflict_state.
Record record : Set := Build {
consensus_state : consensus_state;
voting_state : voting_state;
anonymous_state : anonymous_state;
manager_state : manager_state;
}.
Definition with_consensus_state consensus_state (r : record) :=
Build consensus_state r.(voting_state) r.(anonymous_state)
r.(manager_state).
Definition with_voting_state voting_state (r : record) :=
Build r.(consensus_state) voting_state r.(anonymous_state)
r.(manager_state).
Definition with_anonymous_state anonymous_state (r : record) :=
Build r.(consensus_state) r.(voting_state) anonymous_state
r.(manager_state).
Definition with_manager_state manager_state (r : record) :=
Build r.(consensus_state) r.(voting_state) r.(anonymous_state)
manager_state.
End operation_conflict_state.
Definition operation_conflict_state := operation_conflict_state.record.
Definition operation_conflict_state_encoding
: Data_encoding.encoding operation_conflict_state :=
Data_encoding.def "operation_conflict_state" None None
(Data_encoding.conv
(fun (function_parameter : operation_conflict_state) ⇒
let '{|
operation_conflict_state.consensus_state := consensus_state;
operation_conflict_state.voting_state := voting_state;
operation_conflict_state.anonymous_state := anonymous_state;
operation_conflict_state.manager_state := manager_state
|} := function_parameter in
(consensus_state, voting_state, anonymous_state, manager_state))
(fun (function_parameter :
consensus_state × voting_state × anonymous_state × manager_state) ⇒
let '(consensus_state, voting_state, anonymous_state, manager_state) :=
function_parameter in
{| operation_conflict_state.consensus_state := consensus_state;
operation_conflict_state.voting_state := voting_state;
operation_conflict_state.anonymous_state := anonymous_state;
operation_conflict_state.manager_state := manager_state; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "consensus_state" consensus_state_encoding)
(Data_encoding.req None None "voting_state" voting_state_encoding)
(Data_encoding.req None None "anonymous_state" anonymous_state_encoding)
(Data_encoding.req None None "manager_state" manager_state_encoding))).
Module block_state.
Record record : Set := Build {
op_count : int;
remaining_block_gas : Alpha_context.Gas.Arith.fp;
recorded_operations_rev : list Operation_hash.t;
last_op_validation_pass : option int;
locked_round_evidence : option (Alpha_context.Round.t × int);
endorsement_power : int;
}.
Definition with_op_count op_count (r : record) :=
Build op_count r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_remaining_block_gas remaining_block_gas (r : record) :=
Build r.(op_count) remaining_block_gas r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_recorded_operations_rev recorded_operations_rev
(r : record) :=
Build r.(op_count) r.(remaining_block_gas) recorded_operations_rev
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_last_op_validation_pass last_op_validation_pass
(r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
last_op_validation_pass r.(locked_round_evidence) r.(endorsement_power).
Definition with_locked_round_evidence locked_round_evidence (r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) locked_round_evidence r.(endorsement_power).
Definition with_endorsement_power endorsement_power (r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence) endorsement_power.
End block_state.
Definition block_state := block_state.record.
Module validation_state.
Record record : Set := Build {
info : info;
operation_state : operation_conflict_state;
block_state : block_state;
}.
Definition with_info info (r : record) :=
Build info r.(operation_state) r.(block_state).
Definition with_operation_state operation_state (r : record) :=
Build r.(info) operation_state r.(block_state).
Definition with_block_state block_state (r : record) :=
Build r.(info) r.(operation_state) block_state.
End validation_state.
Definition validation_state := validation_state.record.
Definition ok_unit {A : Set} : Pervasives.result unit A :=
Error_monad.Result_syntax.return_unit.
Definition init_info_aux
(ctxt : Alpha_context.t) (mode : mode) (chain_id : Chain_id.t)
(all_expected_consensus_characteristics : all_expected_consensus_features)
: info :=
{| info.ctxt := ctxt; info.mode := mode; info.chain_id := chain_id;
info.current_level := Alpha_context.Level.current ctxt;
info.consensus_info :=
init_consensus_info ctxt all_expected_consensus_characteristics;
info.manager_info := init_manager_info ctxt; |}.
Definition empty_voting_state : voting_state :=
{|
voting_state.proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
voting_state.ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Definition init_operation_conflict_state
(predecessor_level : Alpha_context.Raw_level.t) : operation_conflict_state :=
{|
operation_conflict_state.consensus_state :=
init_consensus_state predecessor_level;
operation_conflict_state.voting_state := empty_voting_state;
operation_conflict_state.anonymous_state := empty_anonymous_state;
operation_conflict_state.manager_state := empty_manager_state; |}.
Definition init_block_state (vi : info) : block_state :=
{| block_state.op_count := 0;
block_state.remaining_block_gas :=
Alpha_context.Gas.Arith.fp_value
(Alpha_context.Constants.hard_gas_limit_per_block vi.(info.ctxt));
block_state.recorded_operations_rev := nil;
block_state.last_op_validation_pass := None;
block_state.locked_round_evidence := None;
block_state.endorsement_power := 0; |}.
Definition get_initial_ctxt (function_parameter : validation_state)
: Alpha_context.t :=
let '{| validation_state.info := info_value |} := function_parameter in
info_value.(info.ctxt).
Module mode.
Module Construction.
Record record {predecessor_round predecessor_hash round
block_data_contents block_producer payload_producer : Set} : Set := Build {
predecessor_round : predecessor_round;
predecessor_hash : predecessor_hash;
round : round;
block_data_contents : block_data_contents;
block_producer : block_producer;
payload_producer : payload_producer;
}.
Arguments record : clear implicits.
Definition with_predecessor_round
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} predecessor_round
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
predecessor_round r.(predecessor_hash) r.(round)
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_predecessor_hash
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} predecessor_hash
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) predecessor_hash r.(round)
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_round
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} round
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) round
r.(block_data_contents) r.(block_producer) r.(payload_producer).
Definition with_block_data_contents
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} block_data_contents
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
block_data_contents r.(block_producer) r.(payload_producer).
Definition with_block_producer
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} block_producer
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
r.(block_data_contents) block_producer r.(payload_producer).
Definition with_payload_producer
{t_predecessor_round t_predecessor_hash t_round t_block_data_contents
t_block_producer t_payload_producer} payload_producer
(r :
record t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer) :=
Build t_predecessor_round t_predecessor_hash t_round
t_block_data_contents t_block_producer t_payload_producer
r.(predecessor_round) r.(predecessor_hash) r.(round)
r.(block_data_contents) r.(block_producer) payload_producer.
End Construction.
Definition Construction_skeleton := Construction.record.
End mode.
End ConstructorRecords_mode.
Import ConstructorRecords_mode.
Reserved Notation "'mode.Construction".
Inductive mode : Set :=
| Application : block_finalization_info → mode
| Partial_validation : block_finalization_info → mode
| Construction : 'mode.Construction → mode
| Mempool : mode
where "'mode.Construction" :=
(mode.Construction_skeleton Alpha_context.Round.t Block_hash.t
Alpha_context.Round.t Alpha_context.Block_header.contents
Alpha_context.Consensus_key.pk Alpha_context.Consensus_key.pk).
Module mode.
Include ConstructorRecords_mode.mode.
Definition Construction := 'mode.Construction.
End mode.
Module info.
Record record : Set := Build {
ctxt : Alpha_context.t;
mode : mode;
chain_id : Chain_id.t;
current_level : Alpha_context.Level.t;
consensus_info : consensus_info;
manager_info : manager_info;
}.
Definition with_ctxt ctxt (r : record) :=
Build ctxt r.(mode) r.(chain_id) r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_mode mode (r : record) :=
Build r.(ctxt) mode r.(chain_id) r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_chain_id chain_id (r : record) :=
Build r.(ctxt) r.(mode) chain_id r.(current_level) r.(consensus_info)
r.(manager_info).
Definition with_current_level current_level (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) current_level r.(consensus_info)
r.(manager_info).
Definition with_consensus_info consensus_info (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) r.(current_level) consensus_info
r.(manager_info).
Definition with_manager_info manager_info (r : record) :=
Build r.(ctxt) r.(mode) r.(chain_id) r.(current_level) r.(consensus_info)
manager_info.
End info.
Definition info := info.record.
Module operation_conflict_state.
Record record : Set := Build {
consensus_state : consensus_state;
voting_state : voting_state;
anonymous_state : anonymous_state;
manager_state : manager_state;
}.
Definition with_consensus_state consensus_state (r : record) :=
Build consensus_state r.(voting_state) r.(anonymous_state)
r.(manager_state).
Definition with_voting_state voting_state (r : record) :=
Build r.(consensus_state) voting_state r.(anonymous_state)
r.(manager_state).
Definition with_anonymous_state anonymous_state (r : record) :=
Build r.(consensus_state) r.(voting_state) anonymous_state
r.(manager_state).
Definition with_manager_state manager_state (r : record) :=
Build r.(consensus_state) r.(voting_state) r.(anonymous_state)
manager_state.
End operation_conflict_state.
Definition operation_conflict_state := operation_conflict_state.record.
Definition operation_conflict_state_encoding
: Data_encoding.encoding operation_conflict_state :=
Data_encoding.def "operation_conflict_state" None None
(Data_encoding.conv
(fun (function_parameter : operation_conflict_state) ⇒
let '{|
operation_conflict_state.consensus_state := consensus_state;
operation_conflict_state.voting_state := voting_state;
operation_conflict_state.anonymous_state := anonymous_state;
operation_conflict_state.manager_state := manager_state
|} := function_parameter in
(consensus_state, voting_state, anonymous_state, manager_state))
(fun (function_parameter :
consensus_state × voting_state × anonymous_state × manager_state) ⇒
let '(consensus_state, voting_state, anonymous_state, manager_state) :=
function_parameter in
{| operation_conflict_state.consensus_state := consensus_state;
operation_conflict_state.voting_state := voting_state;
operation_conflict_state.anonymous_state := anonymous_state;
operation_conflict_state.manager_state := manager_state; |}) None
(Data_encoding.obj4
(Data_encoding.req None None "consensus_state" consensus_state_encoding)
(Data_encoding.req None None "voting_state" voting_state_encoding)
(Data_encoding.req None None "anonymous_state" anonymous_state_encoding)
(Data_encoding.req None None "manager_state" manager_state_encoding))).
Module block_state.
Record record : Set := Build {
op_count : int;
remaining_block_gas : Alpha_context.Gas.Arith.fp;
recorded_operations_rev : list Operation_hash.t;
last_op_validation_pass : option int;
locked_round_evidence : option (Alpha_context.Round.t × int);
endorsement_power : int;
}.
Definition with_op_count op_count (r : record) :=
Build op_count r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_remaining_block_gas remaining_block_gas (r : record) :=
Build r.(op_count) remaining_block_gas r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_recorded_operations_rev recorded_operations_rev
(r : record) :=
Build r.(op_count) r.(remaining_block_gas) recorded_operations_rev
r.(last_op_validation_pass) r.(locked_round_evidence)
r.(endorsement_power).
Definition with_last_op_validation_pass last_op_validation_pass
(r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
last_op_validation_pass r.(locked_round_evidence) r.(endorsement_power).
Definition with_locked_round_evidence locked_round_evidence (r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) locked_round_evidence r.(endorsement_power).
Definition with_endorsement_power endorsement_power (r : record) :=
Build r.(op_count) r.(remaining_block_gas) r.(recorded_operations_rev)
r.(last_op_validation_pass) r.(locked_round_evidence) endorsement_power.
End block_state.
Definition block_state := block_state.record.
Module validation_state.
Record record : Set := Build {
info : info;
operation_state : operation_conflict_state;
block_state : block_state;
}.
Definition with_info info (r : record) :=
Build info r.(operation_state) r.(block_state).
Definition with_operation_state operation_state (r : record) :=
Build r.(info) operation_state r.(block_state).
Definition with_block_state block_state (r : record) :=
Build r.(info) r.(operation_state) block_state.
End validation_state.
Definition validation_state := validation_state.record.
Definition ok_unit {A : Set} : Pervasives.result unit A :=
Error_monad.Result_syntax.return_unit.
Definition init_info_aux
(ctxt : Alpha_context.t) (mode : mode) (chain_id : Chain_id.t)
(all_expected_consensus_characteristics : all_expected_consensus_features)
: info :=
{| info.ctxt := ctxt; info.mode := mode; info.chain_id := chain_id;
info.current_level := Alpha_context.Level.current ctxt;
info.consensus_info :=
init_consensus_info ctxt all_expected_consensus_characteristics;
info.manager_info := init_manager_info ctxt; |}.
Definition empty_voting_state : voting_state :=
{|
voting_state.proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
voting_state.ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
|}.
Definition init_operation_conflict_state
(predecessor_level : Alpha_context.Raw_level.t) : operation_conflict_state :=
{|
operation_conflict_state.consensus_state :=
init_consensus_state predecessor_level;
operation_conflict_state.voting_state := empty_voting_state;
operation_conflict_state.anonymous_state := empty_anonymous_state;
operation_conflict_state.manager_state := empty_manager_state; |}.
Definition init_block_state (vi : info) : block_state :=
{| block_state.op_count := 0;
block_state.remaining_block_gas :=
Alpha_context.Gas.Arith.fp_value
(Alpha_context.Constants.hard_gas_limit_per_block vi.(info.ctxt));
block_state.recorded_operations_rev := nil;
block_state.last_op_validation_pass := None;
block_state.locked_round_evidence := None;
block_state.endorsement_power := 0; |}.
Definition get_initial_ctxt (function_parameter : validation_state)
: Alpha_context.t :=
let '{| validation_state.info := info_value |} := function_parameter in
info_value.(info.ctxt).
Validation of consensus operations (validation pass [0]):
preendorsement, endorsement, and dal_attestation.
Module Consensus.
Definition expected_endorsement_features
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) (branch : Block_hash.t)
(payload_hash : Block_payload_hash.t) : expected_features :=
{|
expected_features.level :=
predecessor_level.(Alpha_context.Level.t.level);
expected_features.round := Some predecessor_round;
expected_features.branch := branch;
expected_features.payload_hash := payload_hash; |}.
Definition expected_endorsement_features
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) (branch : Block_hash.t)
(payload_hash : Block_payload_hash.t) : expected_features :=
{|
expected_features.level :=
predecessor_level.(Alpha_context.Level.t.level);
expected_features.round := Some predecessor_round;
expected_features.branch := branch;
expected_features.payload_hash := payload_hash; |}.
Expected endorsement features for all modes in which a block is
considered: application, partial validation, and construction.
Definition expected_endorsement_for_block
(ctxt : Alpha_context.t) (predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) : expected_endorsement :=
match Alpha_context.Consensus.endorsement_branch ctxt with
| None ⇒ No_expected_branch_for_block_endorsement
| Some (branch, payload_hash) ⇒
let expected_features :=
expected_endorsement_features predecessor_level predecessor_round branch
payload_hash in
Expected_endorsement
{|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features; |}
end.
(ctxt : Alpha_context.t) (predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t) : expected_endorsement :=
match Alpha_context.Consensus.endorsement_branch ctxt with
| None ⇒ No_expected_branch_for_block_endorsement
| Some (branch, payload_hash) ⇒
let expected_features :=
expected_endorsement_features predecessor_level predecessor_round branch
payload_hash in
Expected_endorsement
{|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features; |}
end.
Retrieve the expected consensus features for both application and
partial validation modes.
Definition expected_features_for_application
(ctxt : Alpha_context.context) (fitness : Alpha_context.Fitness.t)
(payload_hash : Block_payload_hash.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(predecessor_hash : Block_hash.t) : all_expected_consensus_features :=
let expected_preendorsement :=
match Alpha_context.Fitness.locked_round fitness with
| None ⇒ No_locked_round_for_block_validation_preendorsement
| Some locked_round ⇒
let expected_features :=
{|
expected_features.level :=
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level);
expected_features.round := Some locked_round;
expected_features.branch := predecessor_hash;
expected_features.payload_hash := payload_hash; |} in
let block_round := Some (Alpha_context.Fitness.round fitness) in
Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
block_round; |}
end in
let expected_endorsement :=
expected_endorsement_for_block ctxt predecessor_level predecessor_round in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= None; |}.
Definition expected_features_for_construction
(ctxt : Alpha_context.context) (round : Alpha_context.Round.t)
(payload_hash : Block_payload_hash.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(predecessor_hash : Block_hash.t) : all_expected_consensus_features :=
let expected_preendorsement :=
if Block_payload_hash.op_eq payload_hash Block_payload_hash.zero then
Fresh_proposal_for_construction_preendorsement
else
let expected_features :=
{|
expected_features.level :=
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level);
expected_features.round := None;
expected_features.branch := predecessor_hash;
expected_features.payload_hash := payload_hash; |} in
Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
Some round; |} in
let expected_endorsement :=
expected_endorsement_for_block ctxt predecessor_level predecessor_round in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= None; |}.
Definition expected_features_for_partial_construction
(ctxt : Alpha_context.t) (predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(grandparent_round : Alpha_context.Round.t)
: all_expected_consensus_features :=
let '(expected_preendorsement, expected_endorsement) :=
match Alpha_context.Consensus.endorsement_branch ctxt with
| None ⇒
let expected_level := predecessor_level.(Alpha_context.Level.t.level) in
((No_expected_branch_for_partial_construction_preendorsement
{|
expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.expected_level
:= expected_level; |}),
(No_expected_branch_for_partial_construction_endorsement
{|
expected_endorsement.No_expected_branch_for_partial_construction_endorsement.expected_level
:= expected_level; |}))
| Some (branch, payload_hash) ⇒
let expected_features :=
expected_endorsement_features predecessor_level predecessor_round
branch payload_hash in
((Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round := None;
|}),
(Expected_endorsement
{|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features; |}))
end in
let expected_grandparent_endorsement_for_partial_construction :=
match
((Alpha_context.Consensus.grand_parent_branch ctxt),
(Alpha_context.Raw_level.pred
predecessor_level.(Alpha_context.Level.t.level))) with
| ((None, _) | (_, None)) ⇒ None
| (Some (branch, payload_hash), Some level) ⇒
Some
{| expected_features.level := level;
expected_features.round := Some grandparent_round;
expected_features.branch := branch;
expected_features.payload_hash := payload_hash; |}
end in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= expected_grandparent_endorsement_for_partial_construction; |}.
Definition check_frozen_deposits_are_positive
(ctxt : Alpha_context.context)
(delegate_pkh : Alpha_context.public_key_hash) : M? unit :=
let? frozen_deposits :=
Alpha_context.Delegate.frozen_deposits ctxt delegate_pkh in
Error_monad.fail_unless
(Alpha_context.Tez.op_gt frozen_deposits.(Storage.deposits.current_amount)
Alpha_context.Tez.zero)
(Build_extensible "Zero_frozen_deposits" Alpha_context.public_key_hash
delegate_pkh).
Definition check_level_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let expected := expected_features.(expected_features.level) in
let provided := consensus_content.(Alpha_context.consensus_content.level) in
Error_monad.error_unless (Alpha_context.Raw_level.equal expected provided)
(if Alpha_context.Raw_level.op_gt expected provided then
Build_extensible "Consensus_operation_for_old_level"
Validate_errors.Consensus.Consensus_operation_for_old_level
{|
Validate_errors.Consensus.Consensus_operation_for_old_level.kind :=
kind_value;
Validate_errors.Consensus.Consensus_operation_for_old_level.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_old_level.provided
:= provided; |}
else
Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= kind_value;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= provided; |}).
Definition check_round
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected : Alpha_context.Round.t)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let provided := consensus_content.(Alpha_context.consensus_content.round) in
Error_monad.error_unless (Alpha_context.Round.equal expected provided)
(if Alpha_context.Round.op_gt expected provided then
Build_extensible "Consensus_operation_for_old_round"
Validate_errors.Consensus.Consensus_operation_for_old_round
{|
Validate_errors.Consensus.Consensus_operation_for_old_round.kind :=
kind_value;
Validate_errors.Consensus.Consensus_operation_for_old_round.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_old_round.provided
:= provided; |}
else
Build_extensible "Consensus_operation_for_future_round"
Validate_errors.Consensus.Consensus_operation_for_future_round
{|
Validate_errors.Consensus.Consensus_operation_for_future_round.kind
:= kind_value;
Validate_errors.Consensus.Consensus_operation_for_future_round.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_future_round.provided
:= provided; |}).
Definition check_round_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
match expected_features.(expected_features.round) with
| Some expected ⇒ check_round kind_value expected consensus_content
| None ⇒ ok_unit
end.
Definition check_branch_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(operation : Alpha_context.operation) : M? unit :=
let expected := expected_features.(expected_features.branch) in
let provided :=
operation.(Alpha_context.operation.shell).(Operation.shell_header.branch)
in
Error_monad.error_unless (Block_hash.equal expected provided)
(Build_extensible "Wrong_consensus_operation_branch"
Validate_errors.Consensus.Wrong_consensus_operation_branch
{|
Validate_errors.Consensus.Wrong_consensus_operation_branch.kind :=
kind_value;
Validate_errors.Consensus.Wrong_consensus_operation_branch.expected :=
expected;
Validate_errors.Consensus.Wrong_consensus_operation_branch.provided :=
provided; |}).
Definition check_payload_hash_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let expected := expected_features.(expected_features.payload_hash) in
let provided :=
consensus_content.(Alpha_context.consensus_content.block_payload_hash) in
Error_monad.error_unless (Block_payload_hash.equal expected provided)
(Build_extensible "Wrong_payload_hash_for_consensus_operation"
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation
{|
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.kind
:= kind_value;
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.expected
:= expected;
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.provided
:= provided; |}).
Definition check_consensus_features
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected : expected_features)
(consensus_content : Alpha_context.consensus_content)
(operation : Alpha_context.operation) : M? unit :=
let? '_ := check_level_equal kind_value expected consensus_content in
let? '_ := check_round_equal kind_value expected consensus_content in
let? '_ := check_branch_equal kind_value expected operation in
check_payload_hash_equal kind_value expected consensus_content.
Definition get_expected_preendorsements_features
(consensus_info : consensus_info)
(consensus_content : Alpha_context.consensus_content)
: M? (expected_features × option Alpha_context.Round.t) :=
match
consensus_info.(consensus_info.all_expected_features).(all_expected_consensus_features.expected_preendorsement)
with
|
Expected_preendorsement {|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
block_round
|} ⇒ return? (expected_features, block_round)
|
(No_locked_round_for_block_validation_preendorsement |
Fresh_proposal_for_construction_preendorsement) ⇒
Error_monad.error_value
(Build_extensible "Unexpected_preendorsement_in_block" unit tt)
|
No_expected_branch_for_partial_construction_preendorsement {|
expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.expected_level
:= expected_level
|} ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= Validate_errors.Consensus.Preendorsement;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected_level;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= consensus_content.(Alpha_context.consensus_content.level); |})
| No_predecessor_info_cannot_validate_preendorsement ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_not_allowed" unit tt)
end.
Definition check_round_not_too_high
(block_round : option Alpha_context.Round.t)
(provided : Alpha_context.Round.t) : M? unit :=
match block_round with
| None ⇒ ok_unit
| Some block_round ⇒
Error_monad.error_unless (Alpha_context.Round.op_lt provided block_round)
(Build_extensible "Preendorsement_round_too_high"
Validate_errors.Consensus.Preendorsement_round_too_high
{|
Validate_errors.Consensus.Preendorsement_round_too_high.block_round
:= block_round;
Validate_errors.Consensus.Preendorsement_round_too_high.provided :=
provided; |})
end.
Definition get_delegate_details {A : Set}
(slot_map : Alpha_context.Slot.Map.(Map.S.t) A)
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(consensus_content : Alpha_context.consensus_content) : M? A :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Wrong_slot_used_for_consensus_operation"
Validate_errors.Consensus.Wrong_slot_used_for_consensus_operation
{|
Validate_errors.Consensus.Wrong_slot_used_for_consensus_operation.kind
:= kind_value; |}))
(Alpha_context.Slot.Map.(Map.S.find)
consensus_content.(Alpha_context.consensus_content.slot) slot_map).
Definition check_preendorsement
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? int :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let kind_value := Validate_errors.Consensus.Preendorsement in
let? '(expected_features, block_round) :=
get_expected_preendorsements_features vi.(info.consensus_info)
consensus_content in
let? '_ :=
check_round_not_too_high block_round
consensus_content.(Alpha_context.consensus_content.round) in
let? '_ :=
check_consensus_features kind_value expected_features consensus_content
operation in
let? '(consensus_key, voting_power) :=
get_delegate_details
vi.(info.consensus_info).(consensus_info.preendorsement_slot_map)
kind_value consensus_content in
let? '_ :=
check_frozen_deposits_are_positive vi.(info.ctxt)
consensus_key.(Raw_context.consensus_pk.delegate) in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
return? voting_power
| _ ⇒ unreachable_gadt_branch
end.
Definition check_preendorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
with
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
| None ⇒ ok_unit
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_preendorsement_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Preendorsement;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_preendorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation) : operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_preendorsements_seen preendorsements_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition may_update_locked_round_evidence
(block_state_value : block_state) (mode : mode)
(consensus_content : Alpha_context.consensus_content) (voting_power : int)
: block_state :=
let locked_round_evidence :=
match mode with
| Mempool ⇒ None
| (Application _ | Partial_validation _ | Construction _) ⇒
match block_state_value.(block_state.locked_round_evidence) with
| None ⇒
Some
(consensus_content.(Alpha_context.consensus_content.round),
voting_power)
| Some (_stored_round, evidences) ⇒
Some
(consensus_content.(Alpha_context.consensus_content.round),
(evidences +i voting_power))
end
end in
block_state.with_locked_round_evidence locked_round_evidence
block_state_value.
Definition remove_preendorsement
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_preendorsements_seen preendorsements_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
(ctxt : Alpha_context.context) (fitness : Alpha_context.Fitness.t)
(payload_hash : Block_payload_hash.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(predecessor_hash : Block_hash.t) : all_expected_consensus_features :=
let expected_preendorsement :=
match Alpha_context.Fitness.locked_round fitness with
| None ⇒ No_locked_round_for_block_validation_preendorsement
| Some locked_round ⇒
let expected_features :=
{|
expected_features.level :=
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level);
expected_features.round := Some locked_round;
expected_features.branch := predecessor_hash;
expected_features.payload_hash := payload_hash; |} in
let block_round := Some (Alpha_context.Fitness.round fitness) in
Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
block_round; |}
end in
let expected_endorsement :=
expected_endorsement_for_block ctxt predecessor_level predecessor_round in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= None; |}.
Definition expected_features_for_construction
(ctxt : Alpha_context.context) (round : Alpha_context.Round.t)
(payload_hash : Block_payload_hash.t)
(predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(predecessor_hash : Block_hash.t) : all_expected_consensus_features :=
let expected_preendorsement :=
if Block_payload_hash.op_eq payload_hash Block_payload_hash.zero then
Fresh_proposal_for_construction_preendorsement
else
let expected_features :=
{|
expected_features.level :=
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level);
expected_features.round := None;
expected_features.branch := predecessor_hash;
expected_features.payload_hash := payload_hash; |} in
Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
Some round; |} in
let expected_endorsement :=
expected_endorsement_for_block ctxt predecessor_level predecessor_round in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= None; |}.
Definition expected_features_for_partial_construction
(ctxt : Alpha_context.t) (predecessor_level : Alpha_context.Level.t)
(predecessor_round : Alpha_context.Round.t)
(grandparent_round : Alpha_context.Round.t)
: all_expected_consensus_features :=
let '(expected_preendorsement, expected_endorsement) :=
match Alpha_context.Consensus.endorsement_branch ctxt with
| None ⇒
let expected_level := predecessor_level.(Alpha_context.Level.t.level) in
((No_expected_branch_for_partial_construction_preendorsement
{|
expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.expected_level
:= expected_level; |}),
(No_expected_branch_for_partial_construction_endorsement
{|
expected_endorsement.No_expected_branch_for_partial_construction_endorsement.expected_level
:= expected_level; |}))
| Some (branch, payload_hash) ⇒
let expected_features :=
expected_endorsement_features predecessor_level predecessor_round
branch payload_hash in
((Expected_preendorsement
{|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round := None;
|}),
(Expected_endorsement
{|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features; |}))
end in
let expected_grandparent_endorsement_for_partial_construction :=
match
((Alpha_context.Consensus.grand_parent_branch ctxt),
(Alpha_context.Raw_level.pred
predecessor_level.(Alpha_context.Level.t.level))) with
| ((None, _) | (_, None)) ⇒ None
| (Some (branch, payload_hash), Some level) ⇒
Some
{| expected_features.level := level;
expected_features.round := Some grandparent_round;
expected_features.branch := branch;
expected_features.payload_hash := payload_hash; |}
end in
{|
all_expected_consensus_features.expected_preendorsement :=
expected_preendorsement;
all_expected_consensus_features.expected_endorsement :=
expected_endorsement;
all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction
:= expected_grandparent_endorsement_for_partial_construction; |}.
Definition check_frozen_deposits_are_positive
(ctxt : Alpha_context.context)
(delegate_pkh : Alpha_context.public_key_hash) : M? unit :=
let? frozen_deposits :=
Alpha_context.Delegate.frozen_deposits ctxt delegate_pkh in
Error_monad.fail_unless
(Alpha_context.Tez.op_gt frozen_deposits.(Storage.deposits.current_amount)
Alpha_context.Tez.zero)
(Build_extensible "Zero_frozen_deposits" Alpha_context.public_key_hash
delegate_pkh).
Definition check_level_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let expected := expected_features.(expected_features.level) in
let provided := consensus_content.(Alpha_context.consensus_content.level) in
Error_monad.error_unless (Alpha_context.Raw_level.equal expected provided)
(if Alpha_context.Raw_level.op_gt expected provided then
Build_extensible "Consensus_operation_for_old_level"
Validate_errors.Consensus.Consensus_operation_for_old_level
{|
Validate_errors.Consensus.Consensus_operation_for_old_level.kind :=
kind_value;
Validate_errors.Consensus.Consensus_operation_for_old_level.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_old_level.provided
:= provided; |}
else
Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= kind_value;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= provided; |}).
Definition check_round
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected : Alpha_context.Round.t)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let provided := consensus_content.(Alpha_context.consensus_content.round) in
Error_monad.error_unless (Alpha_context.Round.equal expected provided)
(if Alpha_context.Round.op_gt expected provided then
Build_extensible "Consensus_operation_for_old_round"
Validate_errors.Consensus.Consensus_operation_for_old_round
{|
Validate_errors.Consensus.Consensus_operation_for_old_round.kind :=
kind_value;
Validate_errors.Consensus.Consensus_operation_for_old_round.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_old_round.provided
:= provided; |}
else
Build_extensible "Consensus_operation_for_future_round"
Validate_errors.Consensus.Consensus_operation_for_future_round
{|
Validate_errors.Consensus.Consensus_operation_for_future_round.kind
:= kind_value;
Validate_errors.Consensus.Consensus_operation_for_future_round.expected
:= expected;
Validate_errors.Consensus.Consensus_operation_for_future_round.provided
:= provided; |}).
Definition check_round_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
match expected_features.(expected_features.round) with
| Some expected ⇒ check_round kind_value expected consensus_content
| None ⇒ ok_unit
end.
Definition check_branch_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(operation : Alpha_context.operation) : M? unit :=
let expected := expected_features.(expected_features.branch) in
let provided :=
operation.(Alpha_context.operation.shell).(Operation.shell_header.branch)
in
Error_monad.error_unless (Block_hash.equal expected provided)
(Build_extensible "Wrong_consensus_operation_branch"
Validate_errors.Consensus.Wrong_consensus_operation_branch
{|
Validate_errors.Consensus.Wrong_consensus_operation_branch.kind :=
kind_value;
Validate_errors.Consensus.Wrong_consensus_operation_branch.expected :=
expected;
Validate_errors.Consensus.Wrong_consensus_operation_branch.provided :=
provided; |}).
Definition check_payload_hash_equal
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected_features : expected_features)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let expected := expected_features.(expected_features.payload_hash) in
let provided :=
consensus_content.(Alpha_context.consensus_content.block_payload_hash) in
Error_monad.error_unless (Block_payload_hash.equal expected provided)
(Build_extensible "Wrong_payload_hash_for_consensus_operation"
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation
{|
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.kind
:= kind_value;
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.expected
:= expected;
Validate_errors.Consensus.Wrong_payload_hash_for_consensus_operation.provided
:= provided; |}).
Definition check_consensus_features
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(expected : expected_features)
(consensus_content : Alpha_context.consensus_content)
(operation : Alpha_context.operation) : M? unit :=
let? '_ := check_level_equal kind_value expected consensus_content in
let? '_ := check_round_equal kind_value expected consensus_content in
let? '_ := check_branch_equal kind_value expected operation in
check_payload_hash_equal kind_value expected consensus_content.
Definition get_expected_preendorsements_features
(consensus_info : consensus_info)
(consensus_content : Alpha_context.consensus_content)
: M? (expected_features × option Alpha_context.Round.t) :=
match
consensus_info.(consensus_info.all_expected_features).(all_expected_consensus_features.expected_preendorsement)
with
|
Expected_preendorsement {|
expected_preendorsement.Expected_preendorsement.expected_features :=
expected_features;
expected_preendorsement.Expected_preendorsement.block_round :=
block_round
|} ⇒ return? (expected_features, block_round)
|
(No_locked_round_for_block_validation_preendorsement |
Fresh_proposal_for_construction_preendorsement) ⇒
Error_monad.error_value
(Build_extensible "Unexpected_preendorsement_in_block" unit tt)
|
No_expected_branch_for_partial_construction_preendorsement {|
expected_preendorsement.No_expected_branch_for_partial_construction_preendorsement.expected_level
:= expected_level
|} ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= Validate_errors.Consensus.Preendorsement;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected_level;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= consensus_content.(Alpha_context.consensus_content.level); |})
| No_predecessor_info_cannot_validate_preendorsement ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_not_allowed" unit tt)
end.
Definition check_round_not_too_high
(block_round : option Alpha_context.Round.t)
(provided : Alpha_context.Round.t) : M? unit :=
match block_round with
| None ⇒ ok_unit
| Some block_round ⇒
Error_monad.error_unless (Alpha_context.Round.op_lt provided block_round)
(Build_extensible "Preendorsement_round_too_high"
Validate_errors.Consensus.Preendorsement_round_too_high
{|
Validate_errors.Consensus.Preendorsement_round_too_high.block_round
:= block_round;
Validate_errors.Consensus.Preendorsement_round_too_high.provided :=
provided; |})
end.
Definition get_delegate_details {A : Set}
(slot_map : Alpha_context.Slot.Map.(Map.S.t) A)
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(consensus_content : Alpha_context.consensus_content) : M? A :=
Result.of_option
(Error_monad.trace_of_error
(Build_extensible "Wrong_slot_used_for_consensus_operation"
Validate_errors.Consensus.Wrong_slot_used_for_consensus_operation
{|
Validate_errors.Consensus.Wrong_slot_used_for_consensus_operation.kind
:= kind_value; |}))
(Alpha_context.Slot.Map.(Map.S.find)
consensus_content.(Alpha_context.consensus_content.slot) slot_map).
Definition check_preendorsement
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? int :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let kind_value := Validate_errors.Consensus.Preendorsement in
let? '(expected_features, block_round) :=
get_expected_preendorsements_features vi.(info.consensus_info)
consensus_content in
let? '_ :=
check_round_not_too_high block_round
consensus_content.(Alpha_context.consensus_content.round) in
let? '_ :=
check_consensus_features kind_value expected_features consensus_content
operation in
let? '(consensus_key, voting_power) :=
get_delegate_details
vi.(info.consensus_info).(consensus_info.preendorsement_slot_map)
kind_value consensus_content in
let? '_ :=
check_frozen_deposits_are_positive vi.(info.ctxt)
consensus_key.(Raw_context.consensus_pk.delegate) in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
return? voting_power
| _ ⇒ unreachable_gadt_branch
end.
Definition check_preendorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
with
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
| None ⇒ ok_unit
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_preendorsement_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Preendorsement;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_preendorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation) : operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_preendorsements_seen preendorsements_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition may_update_locked_round_evidence
(block_state_value : block_state) (mode : mode)
(consensus_content : Alpha_context.consensus_content) (voting_power : int)
: block_state :=
let locked_round_evidence :=
match mode with
| Mempool ⇒ None
| (Application _ | Partial_validation _ | Construction _) ⇒
match block_state_value.(block_state.locked_round_evidence) with
| None ⇒
Some
(consensus_content.(Alpha_context.consensus_content.round),
voting_power)
| Some (_stored_round, evidences) ⇒
Some
(consensus_content.(Alpha_context.consensus_content.round),
(evidences +i voting_power))
end
end in
block_state.with_locked_round_evidence locked_round_evidence
block_state_value.
Definition remove_preendorsement
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let preendorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.preendorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_preendorsements_seen preendorsements_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Validate an endorsement pointing to the grandparent block. This
function will only be called in [Partial_construction] mode.
Definition check_grandparent_endorsement
(vi : info) (check_signature : bool) (expected : expected_features)
(operation : Alpha_context.operation)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let kind_value := Validate_errors.Consensus.Grandparent_endorsement in
let? level :=
Alpha_context.Level.from_raw vi.(info.ctxt)
consensus_content.(Alpha_context.consensus_content.level) in
let? '(_ctxt, consensus_key) :=
Alpha_context.Stake_distribution.slot_owner vi.(info.ctxt) level
consensus_content.(Alpha_context.consensus_content.slot) in
let? '_ :=
check_consensus_features kind_value expected consensus_content operation
in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
Error_monad.Lwt_result_syntax.return_unit.
Definition add_grandparent_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
operation_conflict_state.with_consensus_state
(consensus_state.with_grandparent_endorsements_seen
(Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen))
vs.(operation_conflict_state.consensus_state)) vs.
Definition check_grandparent_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end.
Definition remove_grandparent_endorsement
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
let grandparent_endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_grandparent_endorsements_seen
grandparent_endorsements_seen
vs.(operation_conflict_state.consensus_state)) vs.
Definition get_expected_endorsements_features
(consensus_info : consensus_info)
(consensus_content : Alpha_context.consensus_content)
: M? expected_features :=
match
consensus_info.(consensus_info.all_expected_features).(all_expected_consensus_features.expected_endorsement)
with
|
Expected_endorsement {|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features
|} ⇒ return? expected_features
| No_expected_branch_for_block_endorsement ⇒
Error_monad.error_value
(Build_extensible "Unexpected_endorsement_in_block" unit tt)
|
No_expected_branch_for_partial_construction_endorsement {|
expected_endorsement.No_expected_branch_for_partial_construction_endorsement.expected_level
:= expected_level
|} ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= Validate_errors.Consensus.Endorsement;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected_level;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= consensus_content.(Alpha_context.consensus_content.level); |})
| No_predecessor_info_cannot_validate_endorsement ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_not_allowed" unit tt)
end.
Inductive endorsement_kind : Set :=
| Grandparent_endorsement : endorsement_kind
| Normal_endorsement : int → endorsement_kind.
(vi : info) (check_signature : bool) (expected : expected_features)
(operation : Alpha_context.operation)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let kind_value := Validate_errors.Consensus.Grandparent_endorsement in
let? level :=
Alpha_context.Level.from_raw vi.(info.ctxt)
consensus_content.(Alpha_context.consensus_content.level) in
let? '(_ctxt, consensus_key) :=
Alpha_context.Stake_distribution.slot_owner vi.(info.ctxt) level
consensus_content.(Alpha_context.consensus_content.slot) in
let? '_ :=
check_consensus_features kind_value expected consensus_content operation
in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
Error_monad.Lwt_result_syntax.return_unit.
Definition add_grandparent_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
operation_conflict_state.with_consensus_state
(consensus_state.with_grandparent_endorsements_seen
(Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen))
vs.(operation_conflict_state.consensus_state)) vs.
Definition check_grandparent_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end.
Definition remove_grandparent_endorsement
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
let grandparent_endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.grandparent_endorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_grandparent_endorsements_seen
grandparent_endorsements_seen
vs.(operation_conflict_state.consensus_state)) vs.
Definition get_expected_endorsements_features
(consensus_info : consensus_info)
(consensus_content : Alpha_context.consensus_content)
: M? expected_features :=
match
consensus_info.(consensus_info.all_expected_features).(all_expected_consensus_features.expected_endorsement)
with
|
Expected_endorsement {|
expected_endorsement.Expected_endorsement.expected_features :=
expected_features
|} ⇒ return? expected_features
| No_expected_branch_for_block_endorsement ⇒
Error_monad.error_value
(Build_extensible "Unexpected_endorsement_in_block" unit tt)
|
No_expected_branch_for_partial_construction_endorsement {|
expected_endorsement.No_expected_branch_for_partial_construction_endorsement.expected_level
:= expected_level
|} ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_for_future_level"
Validate_errors.Consensus.Consensus_operation_for_future_level
{|
Validate_errors.Consensus.Consensus_operation_for_future_level.kind
:= Validate_errors.Consensus.Endorsement;
Validate_errors.Consensus.Consensus_operation_for_future_level.expected
:= expected_level;
Validate_errors.Consensus.Consensus_operation_for_future_level.provided
:= consensus_content.(Alpha_context.consensus_content.level); |})
| No_predecessor_info_cannot_validate_endorsement ⇒
Error_monad.error_value
(Build_extensible "Consensus_operation_not_allowed" unit tt)
end.
Inductive endorsement_kind : Set :=
| Grandparent_endorsement : endorsement_kind
| Normal_endorsement : int → endorsement_kind.
Validate an endorsement pointing to the predecessor, aka a
"normal" endorsement. Only this kind of endorsement may be found
during block validation or construction.
Definition check_normal_endorsement
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? int :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
let kind_value := Validate_errors.Consensus.Endorsement in
let? expected_features :=
get_expected_endorsements_features vi.(info.consensus_info)
consensus_content in
let? '_ :=
check_consensus_features kind_value expected_features consensus_content
operation in
let? '(consensus_key, voting_power) :=
get_delegate_details
vi.(info.consensus_info).(consensus_info.endorsement_slot_map)
kind_value consensus_content in
let? '_ :=
check_frozen_deposits_are_positive vi.(info.ctxt)
consensus_key.(Raw_context.consensus_pk.delegate) in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
return? voting_power
| _ ⇒ unreachable_gadt_branch
end.
Definition check_normal_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end.
Definition add_normal_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
operation_conflict_state.with_consensus_state
(consensus_state.with_endorsements_seen
(Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen))
vs.(operation_conflict_state.consensus_state)) vs.
Definition remove_normal_endorsement
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
let endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_endorsements_seen endorsements_seen
vs.(operation_conflict_state.consensus_state)) vs.
Definition check_endorsement
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? endorsement_kind :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
match
(vi.(info.consensus_info).(consensus_info.all_expected_features).(all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction),
match
vi.(info.consensus_info).(consensus_info.all_expected_features).(all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction)
with
| Some expected_grandparent_endorsement ⇒
Alpha_context.Raw_level.op_eq
consensus_content.(Alpha_context.consensus_content.level)
expected_grandparent_endorsement.(expected_features.level)
| _ ⇒ false
end) with
| (Some expected_grandparent_endorsement, true) ⇒
let? '_ :=
check_grandparent_endorsement vi check_signature
expected_grandparent_endorsement operation consensus_content in
return? Grandparent_endorsement
| (_, _) ⇒
let? voting_power :=
check_normal_endorsement vi check_signature operation in
return? (Normal_endorsement voting_power)
end
| _ ⇒ unreachable_gadt_branch
end.
Definition is_normal_endorsement_assuming_valid
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content) : bool :=
Alpha_context.Raw_level.equal
vs.(operation_conflict_state.consensus_state).(consensus_state.predecessor_level)
consensus_content.(Alpha_context.consensus_content.level).
Definition check_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
if is_normal_endorsement_assuming_valid vs consensus_content then
check_normal_endorsement_conflict vs oph consensus_content
else
check_grandparent_endorsement_conflict vs oph consensus_content
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_endorsement_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Endorsement;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation) (endorsement_kind : endorsement_kind)
: operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
match endorsement_kind with
| Grandparent_endorsement ⇒
add_grandparent_endorsement vs oph consensus_content
| Normal_endorsement _voting_power ⇒
add_normal_endorsement vs oph consensus_content
end
| _ ⇒ unreachable_gadt_branch
end.
Definition may_update_endorsement_power
(block_state_value : block_state) (function_parameter : endorsement_kind)
: block_state :=
match function_parameter with
| Grandparent_endorsement ⇒ block_state_value
| Normal_endorsement voting_power ⇒
block_state.with_endorsement_power
(block_state_value.(block_state.endorsement_power) +i voting_power)
block_state_value
end.
Definition remove_endorsement
(vs : operation_conflict_state) (op : Alpha_context.operation)
: operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
if is_normal_endorsement_assuming_valid vs consensus_content then
remove_normal_endorsement vs consensus_content
else
remove_grandparent_endorsement vs consensus_content
| _ ⇒ unreachable_gadt_branch
end.
Definition check_dal_attestation
(vi : info) (operation : Alpha_context.operation) : M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Dal_attestation op) ⇒
let? '_ := Dal_apply.validate_attestation vi.(info.ctxt) op in
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
Definition check_dal_attestation_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
attestor
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_dal_attestation_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Dal_attestation;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_dal_attestation
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
operation_conflict_state.with_consensus_state
(consensus_state.with_dal_attestation_seen
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
attestor oph
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen))
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_dal_attestation
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
let dal_attestation_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
attestor
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_dal_attestation_seen dal_attestation_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_construction_preendorsement_round_consistency
(vi : info) (block_state_value : block_state)
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let? '(expected_features, _block_round) :=
get_expected_preendorsements_features vi.(info.consensus_info)
consensus_content in
match expected_features.(expected_features.round) with
| Some _ ⇒ Error_monad.Result_syntax.return_unit
| None ⇒
match block_state_value.(block_state.locked_round_evidence) with
| None ⇒ Error_monad.Result_syntax.return_unit
| Some (expected, _power) ⇒
check_round kind_value expected consensus_content
end
end.
Definition validate_preendorsement
(check_signature : bool) (info_value : info)
(operation_state : operation_conflict_state)
(block_state_value : block_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : M? validation_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let? voting_power :=
check_preendorsement info_value check_signature operation in
let? '_ :=
check_construction_preendorsement_round_consistency info_value
block_state_value Validate_errors.Consensus.Preendorsement
consensus_content in
let? '_ :=
wrap_preendorsement_conflict
(check_preendorsement_conflict operation_state oph operation) in
let block_state_value :=
may_update_locked_round_evidence block_state_value
info_value.(info.mode) consensus_content voting_power in
let operation_state := add_preendorsement operation_state oph operation in
return?
{| validation_state.info := info_value;
validation_state.operation_state := operation_state;
validation_state.block_state := block_state_value; |}
| _ ⇒ unreachable_gadt_branch
end.
Definition validate_endorsement
(check_signature : bool) (info_value : info)
(operation_state : operation_conflict_state)
(block_state_value : block_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : M? validation_state :=
let? kind_value := check_endorsement info_value check_signature operation in
let? '_ :=
wrap_endorsement_conflict
(check_endorsement_conflict operation_state oph operation) in
let block_state_value :=
may_update_endorsement_power block_state_value kind_value in
let operation_state :=
add_endorsement operation_state oph operation kind_value in
return?
{| validation_state.info := info_value;
validation_state.operation_state := operation_state;
validation_state.block_state := block_state_value; |}.
End Consensus.
Module Voting.
Definition check_period_index (expected : int32) (period_index : int32)
: M? unit :=
Error_monad.error_unless (expected =i32 period_index)
(Build_extensible "Wrong_voting_period_index"
Validate_errors.Voting.Wrong_voting_period_index
{|
Validate_errors.Voting.Wrong_voting_period_index.expected := expected;
Validate_errors.Voting.Wrong_voting_period_index.provided :=
period_index; |}).
Definition check_proposals_source_is_registered
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let is_registered := Alpha_context.Delegate.registered ctxt source in
Error_monad.fail_unless is_registered
(Build_extensible "Proposals_from_unregistered_delegate"
Alpha_context.public_key_hash source).
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? int :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
let kind_value := Validate_errors.Consensus.Endorsement in
let? expected_features :=
get_expected_endorsements_features vi.(info.consensus_info)
consensus_content in
let? '_ :=
check_consensus_features kind_value expected_features consensus_content
operation in
let? '(consensus_key, voting_power) :=
get_delegate_details
vi.(info.consensus_info).(consensus_info.endorsement_slot_map)
kind_value consensus_content in
let? '_ :=
check_frozen_deposits_are_positive vi.(info.ctxt)
consensus_key.(Raw_context.consensus_pk.delegate) in
let? '_ :=
if check_signature then
Alpha_context.Operation.check_signature
consensus_key.(Raw_context.consensus_pk.consensus_pk)
vi.(info.chain_id) operation
else
ok_unit in
return? voting_power
| _ ⇒ unreachable_gadt_branch
end.
Definition check_normal_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
Alpha_context.Slot.Map.(Map.S.find_opt)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end.
Definition add_normal_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
operation_conflict_state.with_consensus_state
(consensus_state.with_endorsements_seen
(Alpha_context.Slot.Map.(Map.S.add)
consensus_content.(Alpha_context.consensus_content.slot) oph
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen))
vs.(operation_conflict_state.consensus_state)) vs.
Definition remove_normal_endorsement
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content)
: operation_conflict_state :=
let endorsements_seen :=
Alpha_context.Slot.Map.(Map.S.remove)
consensus_content.(Alpha_context.consensus_content.slot)
vs.(operation_conflict_state.consensus_state).(consensus_state.endorsements_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_endorsements_seen endorsements_seen
vs.(operation_conflict_state.consensus_state)) vs.
Definition check_endorsement
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? endorsement_kind :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
match
(vi.(info.consensus_info).(consensus_info.all_expected_features).(all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction),
match
vi.(info.consensus_info).(consensus_info.all_expected_features).(all_expected_consensus_features.expected_grandparent_endorsement_for_partial_construction)
with
| Some expected_grandparent_endorsement ⇒
Alpha_context.Raw_level.op_eq
consensus_content.(Alpha_context.consensus_content.level)
expected_grandparent_endorsement.(expected_features.level)
| _ ⇒ false
end) with
| (Some expected_grandparent_endorsement, true) ⇒
let? '_ :=
check_grandparent_endorsement vi check_signature
expected_grandparent_endorsement operation consensus_content in
return? Grandparent_endorsement
| (_, _) ⇒
let? voting_power :=
check_normal_endorsement vi check_signature operation in
return? (Normal_endorsement voting_power)
end
| _ ⇒ unreachable_gadt_branch
end.
Definition is_normal_endorsement_assuming_valid
(vs : operation_conflict_state)
(consensus_content : Alpha_context.consensus_content) : bool :=
Alpha_context.Raw_level.equal
vs.(operation_conflict_state.consensus_state).(consensus_state.predecessor_level)
consensus_content.(Alpha_context.consensus_content.level).
Definition check_endorsement_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
if is_normal_endorsement_assuming_valid vs consensus_content then
check_normal_endorsement_conflict vs oph consensus_content
else
check_grandparent_endorsement_conflict vs oph consensus_content
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_endorsement_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Endorsement;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_endorsement
(vs : operation_conflict_state) (oph : Operation_hash.t)
(op : Alpha_context.operation) (endorsement_kind : endorsement_kind)
: operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
match endorsement_kind with
| Grandparent_endorsement ⇒
add_grandparent_endorsement vs oph consensus_content
| Normal_endorsement _voting_power ⇒
add_normal_endorsement vs oph consensus_content
end
| _ ⇒ unreachable_gadt_branch
end.
Definition may_update_endorsement_power
(block_state_value : block_state) (function_parameter : endorsement_kind)
: block_state :=
match function_parameter with
| Grandparent_endorsement ⇒ block_state_value
| Normal_endorsement voting_power ⇒
block_state.with_endorsement_power
(block_state_value.(block_state.endorsement_power) +i voting_power)
block_state_value
end.
Definition remove_endorsement
(vs : operation_conflict_state) (op : Alpha_context.operation)
: operation_conflict_state :=
match
op.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Endorsement consensus_content) ⇒
if is_normal_endorsement_assuming_valid vs consensus_content then
remove_normal_endorsement vs consensus_content
else
remove_grandparent_endorsement vs consensus_content
| _ ⇒ unreachable_gadt_branch
end.
Definition check_dal_attestation
(vi : info) (operation : Alpha_context.operation) : M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Dal_attestation op) ⇒
let? '_ := Dal_apply.validate_attestation vi.(info.ctxt) op in
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
Definition check_dal_attestation_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
attestor
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_dal_attestation_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_consensus_operation"
Validate_errors.Consensus.Conflicting_consensus_operation
{|
Validate_errors.Consensus.Conflicting_consensus_operation.kind :=
Validate_errors.Consensus.Dal_attestation;
Validate_errors.Consensus.Conflicting_consensus_operation.conflict
:= conflict; |})
end.
Definition add_dal_attestation
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
operation_conflict_state.with_consensus_state
(consensus_state.with_dal_attestation_seen
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
attestor oph
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen))
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_dal_attestation
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Dal_attestation {|
Alpha_context.Dal.Attestation.operation.attestor := attestor;
Alpha_context.Dal.Attestation.operation.attestation := _;
Alpha_context.Dal.Attestation.operation.level := _
|}) ⇒
let dal_attestation_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
attestor
vs.(operation_conflict_state.consensus_state).(consensus_state.dal_attestation_seen)
in
operation_conflict_state.with_consensus_state
(consensus_state.with_dal_attestation_seen dal_attestation_seen
vs.(operation_conflict_state.consensus_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_construction_preendorsement_round_consistency
(vi : info) (block_state_value : block_state)
(kind_value : Validate_errors.Consensus.consensus_operation_kind)
(consensus_content : Alpha_context.consensus_content) : M? unit :=
let? '(expected_features, _block_round) :=
get_expected_preendorsements_features vi.(info.consensus_info)
consensus_content in
match expected_features.(expected_features.round) with
| Some _ ⇒ Error_monad.Result_syntax.return_unit
| None ⇒
match block_state_value.(block_state.locked_round_evidence) with
| None ⇒ Error_monad.Result_syntax.return_unit
| Some (expected, _power) ⇒
check_round kind_value expected consensus_content
end
end.
Definition validate_preendorsement
(check_signature : bool) (info_value : info)
(operation_state : operation_conflict_state)
(block_state_value : block_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : M? validation_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
| Alpha_context.Single (Alpha_context.Preendorsement consensus_content) ⇒
let? voting_power :=
check_preendorsement info_value check_signature operation in
let? '_ :=
check_construction_preendorsement_round_consistency info_value
block_state_value Validate_errors.Consensus.Preendorsement
consensus_content in
let? '_ :=
wrap_preendorsement_conflict
(check_preendorsement_conflict operation_state oph operation) in
let block_state_value :=
may_update_locked_round_evidence block_state_value
info_value.(info.mode) consensus_content voting_power in
let operation_state := add_preendorsement operation_state oph operation in
return?
{| validation_state.info := info_value;
validation_state.operation_state := operation_state;
validation_state.block_state := block_state_value; |}
| _ ⇒ unreachable_gadt_branch
end.
Definition validate_endorsement
(check_signature : bool) (info_value : info)
(operation_state : operation_conflict_state)
(block_state_value : block_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : M? validation_state :=
let? kind_value := check_endorsement info_value check_signature operation in
let? '_ :=
wrap_endorsement_conflict
(check_endorsement_conflict operation_state oph operation) in
let block_state_value :=
may_update_endorsement_power block_state_value kind_value in
let operation_state :=
add_endorsement operation_state oph operation kind_value in
return?
{| validation_state.info := info_value;
validation_state.operation_state := operation_state;
validation_state.block_state := block_state_value; |}.
End Consensus.
Module Voting.
Definition check_period_index (expected : int32) (period_index : int32)
: M? unit :=
Error_monad.error_unless (expected =i32 period_index)
(Build_extensible "Wrong_voting_period_index"
Validate_errors.Voting.Wrong_voting_period_index
{|
Validate_errors.Voting.Wrong_voting_period_index.expected := expected;
Validate_errors.Voting.Wrong_voting_period_index.provided :=
period_index; |}).
Definition check_proposals_source_is_registered
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let is_registered := Alpha_context.Delegate.registered ctxt source in
Error_monad.fail_unless is_registered
(Build_extensible "Proposals_from_unregistered_delegate"
Alpha_context.public_key_hash source).
Check that the list of proposals is not empty and does not contain
duplicates.
Definition check_proposal_list_sanity (proposals : list Protocol_hash.t)
: M? unit :=
let? '_ :=
match proposals with
| [] ⇒
Error_monad.error_value (Build_extensible "Empty_proposals" unit tt)
| cons _ _ ⇒ ok_unit
end in
let? '_ :=
List.fold_left_e
(fun (previous_elements : Protocol_hash._Set.(S.INDEXES_SET.t)) ⇒
fun (proposal : Protocol_hash.t) ⇒
let? '_ :=
Error_monad.error_when
(Protocol_hash._Set.(S.INDEXES_SET.mem) proposal
previous_elements)
(Build_extensible "Proposals_contain_duplicate"
Validate_errors.Voting.Proposals_contain_duplicate
{|
Validate_errors.Voting.Proposals_contain_duplicate.proposal
:= proposal; |}) in
return?
(Protocol_hash._Set.(S.INDEXES_SET.add) proposal previous_elements))
Protocol_hash._Set.(S.INDEXES_SET.empty) proposals in
Error_monad.Result_syntax.return_unit.
Definition check_period_kind_for_proposals
(current_period : Alpha_context.Voting_period.voting_period) : M? unit :=
match current_period.(Alpha_context.Voting_period.voting_period.kind) with
| Alpha_context.Voting_period.Proposal ⇒ ok_unit
|
(Alpha_context.Voting_period.Exploration |
Alpha_context.Voting_period.Cooldown |
Alpha_context.Voting_period.Promotion |
Alpha_context.Voting_period.Adoption) as current ⇒
Error_monad.error_value
(Build_extensible "Wrong_voting_period_kind"
Validate_errors.Voting.Wrong_voting_period_kind
{| Validate_errors.Voting.Wrong_voting_period_kind.current := current;
Validate_errors.Voting.Wrong_voting_period_kind.expected :=
[ Alpha_context.Voting_period.Proposal ]; |})
end.
Definition check_in_listings
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let in_listings := Alpha_context.Vote.in_listings ctxt source in
Error_monad.fail_unless in_listings
(Build_extensible "Source_not_in_vote_listings" unit tt).
Definition check_count (count_in_ctxt : int) (proposals_length : int)
: M? unit :=
let? '_ :=
Internal_errors.do_assert
(count_in_ctxt ≤i Alpha_context.Constants.max_proposals_per_delegate)
in
Error_monad.error_unless
((count_in_ctxt +i proposals_length) ≤i
Alpha_context.Constants.max_proposals_per_delegate)
(Build_extensible "Too_many_proposals"
Validate_errors.Voting.Too_many_proposals
{|
Validate_errors.Voting.Too_many_proposals.previous_count :=
count_in_ctxt;
Validate_errors.Voting.Too_many_proposals.operation_count :=
proposals_length; |}).
Definition check_already_proposed
(ctxt : Alpha_context.context) (proposer : Alpha_context.public_key_hash)
(proposals : list Alpha_context.Vote.proposal) : M? unit :=
List.iter_es
(fun (proposal : Alpha_context.Vote.proposal) ⇒
let already_proposed :=
Alpha_context.Vote.has_proposed ctxt proposer proposal in
Error_monad.fail_when already_proposed
(Build_extensible "Already_proposed"
Validate_errors.Voting.Already_proposed
{| Validate_errors.Voting.Already_proposed.proposal := proposal; |}))
proposals.
: M? unit :=
let? '_ :=
match proposals with
| [] ⇒
Error_monad.error_value (Build_extensible "Empty_proposals" unit tt)
| cons _ _ ⇒ ok_unit
end in
let? '_ :=
List.fold_left_e
(fun (previous_elements : Protocol_hash._Set.(S.INDEXES_SET.t)) ⇒
fun (proposal : Protocol_hash.t) ⇒
let? '_ :=
Error_monad.error_when
(Protocol_hash._Set.(S.INDEXES_SET.mem) proposal
previous_elements)
(Build_extensible "Proposals_contain_duplicate"
Validate_errors.Voting.Proposals_contain_duplicate
{|
Validate_errors.Voting.Proposals_contain_duplicate.proposal
:= proposal; |}) in
return?
(Protocol_hash._Set.(S.INDEXES_SET.add) proposal previous_elements))
Protocol_hash._Set.(S.INDEXES_SET.empty) proposals in
Error_monad.Result_syntax.return_unit.
Definition check_period_kind_for_proposals
(current_period : Alpha_context.Voting_period.voting_period) : M? unit :=
match current_period.(Alpha_context.Voting_period.voting_period.kind) with
| Alpha_context.Voting_period.Proposal ⇒ ok_unit
|
(Alpha_context.Voting_period.Exploration |
Alpha_context.Voting_period.Cooldown |
Alpha_context.Voting_period.Promotion |
Alpha_context.Voting_period.Adoption) as current ⇒
Error_monad.error_value
(Build_extensible "Wrong_voting_period_kind"
Validate_errors.Voting.Wrong_voting_period_kind
{| Validate_errors.Voting.Wrong_voting_period_kind.current := current;
Validate_errors.Voting.Wrong_voting_period_kind.expected :=
[ Alpha_context.Voting_period.Proposal ]; |})
end.
Definition check_in_listings
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let in_listings := Alpha_context.Vote.in_listings ctxt source in
Error_monad.fail_unless in_listings
(Build_extensible "Source_not_in_vote_listings" unit tt).
Definition check_count (count_in_ctxt : int) (proposals_length : int)
: M? unit :=
let? '_ :=
Internal_errors.do_assert
(count_in_ctxt ≤i Alpha_context.Constants.max_proposals_per_delegate)
in
Error_monad.error_unless
((count_in_ctxt +i proposals_length) ≤i
Alpha_context.Constants.max_proposals_per_delegate)
(Build_extensible "Too_many_proposals"
Validate_errors.Voting.Too_many_proposals
{|
Validate_errors.Voting.Too_many_proposals.previous_count :=
count_in_ctxt;
Validate_errors.Voting.Too_many_proposals.operation_count :=
proposals_length; |}).
Definition check_already_proposed
(ctxt : Alpha_context.context) (proposer : Alpha_context.public_key_hash)
(proposals : list Alpha_context.Vote.proposal) : M? unit :=
List.iter_es
(fun (proposal : Alpha_context.Vote.proposal) ⇒
let already_proposed :=
Alpha_context.Vote.has_proposed ctxt proposer proposal in
Error_monad.fail_when already_proposed
(Build_extensible "Already_proposed"
Validate_errors.Voting.Already_proposed
{| Validate_errors.Voting.Already_proposed.proposal := proposal; |}))
proposals.
Check that the [apply_testnet_dictator_proposals] function in
{!module:Amendment} will not fail.
The current function is designed to be exclusively called by
[check_proposals] right below.
@return [Error Testnet_dictator_multiple_proposals] if
[proposals] has more than one element.
Definition check_testnet_dictator_proposals {A : Set}
(chain_id : Chain_id.t) (proposals : list A) : M? unit :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Chain_id.op_ltgt chain_id Alpha_context.Constants.mainnet_id)
in
match proposals with
| ([] | cons _ []) ⇒ ok_unit
| cons _ (cons _ _) ⇒
Error_monad.error_value
(Build_extensible "Testnet_dictator_multiple_proposals" unit tt)
end.
(chain_id : Chain_id.t) (proposals : list A) : M? unit :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (Chain_id.op_ltgt chain_id Alpha_context.Constants.mainnet_id)
in
match proposals with
| ([] | cons _ []) ⇒ ok_unit
| cons _ (cons _ _) ⇒
Error_monad.error_value
(Build_extensible "Testnet_dictator_multiple_proposals" unit tt)
end.
Check that a Proposals operation can be safely applied.
@return [Error Wrong_voting_period_index] if the operation's
period and the current period in the {!type:context} do not have
the same index.
@return [Error Proposals_from_unregistered_delegate] if the
source is not a registered delegate.
@return [Error Empty_proposals] if the list of proposals is empty.
@return [Error Proposals_contain_duplicate] if the list of
proposals contains a duplicate element.
@return [Error Wrong_voting_period_kind] if the voting period is
not of the Proposal kind.
@return [Error Source_not_in_vote_listings] if the source is not
in the vote listings.
@return [Error Too_many_proposals] if the operation causes the
source's total number of proposals during the current voting
period to exceed {!Constants.max_proposals_per_delegate}.
@return [Error Already_proposed] if one of the proposals has
already been proposed by the source in the current voting period.
@return [Error Testnet_dictator_multiple_proposals] if the
source is a testnet dictator and the operation contains more than
one proposal.
@return [Error Operation.Missing_signature] or [Error
Operation.Invalid_signature] if the operation is unsigned or
incorrectly signed.
Definition check_proposals
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source;
Alpha_context.contents.Proposals.period := period;
Alpha_context.contents.Proposals.proposals := proposals
|}) ⇒
let? current_period :=
Alpha_context.Voting_period.get_current vi.(info.ctxt) in
let? '_ :=
check_period_index
current_period.(Alpha_context.Voting_period.voting_period.index)
period in
let? '_ :=
if
Amendment.is_testnet_dictator vi.(info.ctxt) vi.(info.chain_id) source
then
let? '_ :=
check_testnet_dictator_proposals vi.(info.chain_id) proposals in
Error_monad.Lwt_result_syntax.return_unit
else
let? '_ := check_proposals_source_is_registered vi.(info.ctxt) source
in
let? '_ := check_proposal_list_sanity proposals in
let? '_ := check_period_kind_for_proposals current_period in
let? '_ := check_in_listings vi.(info.ctxt) source in
let? count_in_ctxt :=
Alpha_context.Vote.get_delegate_proposal_count vi.(info.ctxt) source
in
let proposals_length := List.length proposals in
let? '_ := check_count count_in_ctxt proposals_length in
check_already_proposed vi.(info.ctxt) source proposals in
if check_signature then
let? public_key :=
Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
operation
else
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source;
Alpha_context.contents.Proposals.period := period;
Alpha_context.contents.Proposals.proposals := proposals
|}) ⇒
let? current_period :=
Alpha_context.Voting_period.get_current vi.(info.ctxt) in
let? '_ :=
check_period_index
current_period.(Alpha_context.Voting_period.voting_period.index)
period in
let? '_ :=
if
Amendment.is_testnet_dictator vi.(info.ctxt) vi.(info.chain_id) source
then
let? '_ :=
check_testnet_dictator_proposals vi.(info.chain_id) proposals in
Error_monad.Lwt_result_syntax.return_unit
else
let? '_ := check_proposals_source_is_registered vi.(info.ctxt) source
in
let? '_ := check_proposal_list_sanity proposals in
let? '_ := check_period_kind_for_proposals current_period in
let? '_ := check_in_listings vi.(info.ctxt) source in
let? count_in_ctxt :=
Alpha_context.Vote.get_delegate_proposal_count vi.(info.ctxt) source
in
let proposals_length := List.length proposals in
let? '_ := check_count count_in_ctxt proposals_length in
check_already_proposed vi.(info.ctxt) source proposals in
if check_signature then
let? public_key :=
Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
operation
else
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
Check that a Proposals operation is compatible with previously
validated operations in the current block/mempool.
@return [Error Operation_conflict] if the current block/mempool
already contains a Proposals operation from the same source
(regardless of whether this source is a testnet dictator or an
ordinary manager).
Definition check_proposals_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
source
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
with
| None ⇒ Error_monad.Result_syntax.return_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_proposals_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_proposals"
Validate_errors.operation_conflict conflict)
end.
Definition add_proposals
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
let proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
source oph
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
in
let voting_state :=
voting_state.with_proposals_seen proposals_seen
vs.(operation_conflict_state.voting_state) in
operation_conflict_state.with_voting_state voting_state vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_proposals
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
let proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
source
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
in
operation_conflict_state.with_voting_state
(voting_state.with_proposals_seen proposals_seen
vs.(operation_conflict_state.voting_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_ballot_source_is_registered
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let is_registered := Alpha_context.Delegate.registered ctxt source in
Error_monad.fail_unless is_registered
(Build_extensible "Ballot_from_unregistered_delegate"
Alpha_context.public_key_hash source).
Definition check_period_kind_for_ballot
(current_period : Alpha_context.Voting_period.voting_period) : M? unit :=
match current_period.(Alpha_context.Voting_period.voting_period.kind) with
|
(Alpha_context.Voting_period.Exploration |
Alpha_context.Voting_period.Promotion) ⇒ ok_unit
|
(Alpha_context.Voting_period.Cooldown |
Alpha_context.Voting_period.Proposal |
Alpha_context.Voting_period.Adoption) as current ⇒
Error_monad.error_value
(Build_extensible "Wrong_voting_period_kind"
Validate_errors.Voting.Wrong_voting_period_kind
{| Validate_errors.Voting.Wrong_voting_period_kind.current := current;
Validate_errors.Voting.Wrong_voting_period_kind.expected :=
[
Alpha_context.Voting_period.Exploration;
Alpha_context.Voting_period.Promotion
]; |})
end.
Definition check_current_proposal
(ctxt : Alpha_context.context) (op_proposal : Protocol_hash.t) : M? unit :=
let? current_proposal := Alpha_context.Vote.get_current_proposal ctxt in
Error_monad.fail_unless (Protocol_hash.equal op_proposal current_proposal)
(Build_extensible "Ballot_for_wrong_proposal"
Validate_errors.Voting.Ballot_for_wrong_proposal
{|
Validate_errors.Voting.Ballot_for_wrong_proposal.current :=
current_proposal;
Validate_errors.Voting.Ballot_for_wrong_proposal.submitted :=
op_proposal; |}).
Definition check_source_has_not_already_voted
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let has_ballot := Alpha_context.Vote.has_recorded_ballot ctxt source in
Error_monad.fail_when has_ballot
(Build_extensible "Already_submitted_a_ballot" unit tt).
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
source
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
with
| None ⇒ Error_monad.Result_syntax.return_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_proposals_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_proposals"
Validate_errors.operation_conflict conflict)
end.
Definition add_proposals
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
let proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
source oph
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
in
let voting_state :=
voting_state.with_proposals_seen proposals_seen
vs.(operation_conflict_state.voting_state) in
operation_conflict_state.with_voting_state voting_state vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_proposals
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Proposals {|
Alpha_context.contents.Proposals.source := source |}) ⇒
let proposals_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
source
vs.(operation_conflict_state.voting_state).(voting_state.proposals_seen)
in
operation_conflict_state.with_voting_state
(voting_state.with_proposals_seen proposals_seen
vs.(operation_conflict_state.voting_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_ballot_source_is_registered
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let is_registered := Alpha_context.Delegate.registered ctxt source in
Error_monad.fail_unless is_registered
(Build_extensible "Ballot_from_unregistered_delegate"
Alpha_context.public_key_hash source).
Definition check_period_kind_for_ballot
(current_period : Alpha_context.Voting_period.voting_period) : M? unit :=
match current_period.(Alpha_context.Voting_period.voting_period.kind) with
|
(Alpha_context.Voting_period.Exploration |
Alpha_context.Voting_period.Promotion) ⇒ ok_unit
|
(Alpha_context.Voting_period.Cooldown |
Alpha_context.Voting_period.Proposal |
Alpha_context.Voting_period.Adoption) as current ⇒
Error_monad.error_value
(Build_extensible "Wrong_voting_period_kind"
Validate_errors.Voting.Wrong_voting_period_kind
{| Validate_errors.Voting.Wrong_voting_period_kind.current := current;
Validate_errors.Voting.Wrong_voting_period_kind.expected :=
[
Alpha_context.Voting_period.Exploration;
Alpha_context.Voting_period.Promotion
]; |})
end.
Definition check_current_proposal
(ctxt : Alpha_context.context) (op_proposal : Protocol_hash.t) : M? unit :=
let? current_proposal := Alpha_context.Vote.get_current_proposal ctxt in
Error_monad.fail_unless (Protocol_hash.equal op_proposal current_proposal)
(Build_extensible "Ballot_for_wrong_proposal"
Validate_errors.Voting.Ballot_for_wrong_proposal
{|
Validate_errors.Voting.Ballot_for_wrong_proposal.current :=
current_proposal;
Validate_errors.Voting.Ballot_for_wrong_proposal.submitted :=
op_proposal; |}).
Definition check_source_has_not_already_voted
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
: M? unit :=
let has_ballot := Alpha_context.Vote.has_recorded_ballot ctxt source in
Error_monad.fail_when has_ballot
(Build_extensible "Already_submitted_a_ballot" unit tt).
Check that a Ballot operation can be safely applied.
@return [Error Ballot_from_unregistered_delegate] if the source
is not a registered delegate.
@return [Error Wrong_voting_period_index] if the operation's
period and the current period in the {!type:context} do not have
the same index.
@return [Error Wrong_voting_period_kind] if the voting period is
not of the Exploration or Promotion kind.
@return [Error Ballot_for_wrong_proposal] if the operation's
proposal is different from the current proposal in the context.
@return [Error Already_submitted_a_ballot] if the source has
already voted during the current voting period.
@return [Error Source_not_in_vote_listings] if the source is not
in the vote listings.
@return [Error Operation.Missing_signature] or [Error
Operation.Invalid_signature] if the operation is unsigned or
incorrectly signed.
Definition check_ballot
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source;
Alpha_context.contents.Ballot.period := period;
Alpha_context.contents.Ballot.proposal := proposal;
Alpha_context.contents.Ballot.ballot := _
|}) ⇒
let? '_ := check_ballot_source_is_registered vi.(info.ctxt) source in
let? current_period :=
Alpha_context.Voting_period.get_current vi.(info.ctxt) in
let? '_ :=
check_period_index
current_period.(Alpha_context.Voting_period.voting_period.index)
period in
let? '_ := check_period_kind_for_ballot current_period in
let? '_ := check_current_proposal vi.(info.ctxt) proposal in
let? '_ := check_source_has_not_already_voted vi.(info.ctxt) source in
let? '_ := check_in_listings vi.(info.ctxt) source in
Error_monad.when_ check_signature
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
let? public_key :=
Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
operation)
| _ ⇒ unreachable_gadt_branch
end.
(vi : info) (check_signature : bool) (operation : Alpha_context.operation)
: M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source;
Alpha_context.contents.Ballot.period := period;
Alpha_context.contents.Ballot.proposal := proposal;
Alpha_context.contents.Ballot.ballot := _
|}) ⇒
let? '_ := check_ballot_source_is_registered vi.(info.ctxt) source in
let? current_period :=
Alpha_context.Voting_period.get_current vi.(info.ctxt) in
let? '_ :=
check_period_index
current_period.(Alpha_context.Voting_period.voting_period.index)
period in
let? '_ := check_period_kind_for_ballot current_period in
let? '_ := check_current_proposal vi.(info.ctxt) proposal in
let? '_ := check_source_has_not_already_voted vi.(info.ctxt) source in
let? '_ := check_in_listings vi.(info.ctxt) source in
Error_monad.when_ check_signature
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
let? public_key :=
Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
operation)
| _ ⇒ unreachable_gadt_branch
end.
Check that a Ballot operation is compatible with previously
validated operations in the current block/mempool.
@return [Error Operation_conflict] if the current block/mempool
already contains a Ballot operation from the same source.
Definition check_ballot_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
source
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_ballot_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_ballot"
Validate_errors.operation_conflict conflict)
end.
Definition add_ballot
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
let ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
source oph
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
in
let voting_state :=
voting_state.with_ballots_seen ballots_seen
vs.(operation_conflict_state.voting_state) in
operation_conflict_state.with_voting_state voting_state vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_ballot
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
let ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
source
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
in
operation_conflict_state.with_voting_state
(voting_state.with_ballots_seen ballots_seen
vs.(operation_conflict_state.voting_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
End Voting.
Module Anonymous.
Definition check_activate_account
(vi : info) (operation : Alpha_context.operation) : M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh;
Alpha_context.contents.Activate_account.activation_code :=
activation_code
|}) ⇒
let blinded_pkh :=
Blinded_public_key_hash.of_ed25519_pkh activation_code edpkh in
let _exists := Alpha_context.Commitment._exists vi.(info.ctxt) blinded_pkh
in
let? '_ :=
Error_monad.error_unless _exists
(Build_extensible "Invalid_activation"
Validate_errors.Anonymous.Invalid_activation
{| Validate_errors.Anonymous.Invalid_activation.pkh := edpkh; |}) in
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
Definition check_activate_account_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
match
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
edpkh
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_activate_account_conflict
(operation : Alpha_context.operation)
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
Error_monad.error_value
(Build_extensible "Conflicting_activation"
Validate_errors.Anonymous.Conflicting_activation
{| Validate_errors.Anonymous.Conflicting_activation.edpkh := edpkh;
Validate_errors.Anonymous.Conflicting_activation.conflict :=
conflict; |})
| _ ⇒ unreachable_gadt_branch
end
end.
Definition add_activate_account
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
let activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
edpkh oph
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
in
operation_conflict_state.with_anonymous_state
(anonymous_state.with_activation_pkhs_seen activation_pkhs_seen
vs.(operation_conflict_state.anonymous_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_activate_account
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
let activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
edpkh
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
in
operation_conflict_state.with_anonymous_state
(anonymous_state.with_activation_pkhs_seen activation_pkhs_seen
vs.(operation_conflict_state.anonymous_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_denunciation_age
(vi : info) (kind_value : Validate_errors.Anonymous.denunciation_kind)
(given_level : Alpha_context.Raw_level.t) : M? unit :=
let current_cycle := vi.(info.current_level).(Alpha_context.Level.t.cycle)
in
let? res := Alpha_context.Level.from_raw vi.(info.ctxt) given_level in
let given_cycle := res.(Alpha_context.Level.t.cycle) in
let max_slashing_period :=
Alpha_context.Constants.max_slashing_period vi.(info.ctxt) in
let? last_slashable_cycle :=
Alpha_context.Cycle.add given_cycle max_slashing_period in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Cycle.op_lteq given_cycle current_cycle)
(Build_extensible "Too_early_denunciation"
Validate_errors.Anonymous.Too_early_denunciation
{|
Validate_errors.Anonymous.Too_early_denunciation.kind := kind_value;
Validate_errors.Anonymous.Too_early_denunciation.level :=
given_level;
Validate_errors.Anonymous.Too_early_denunciation.current :=
vi.(info.current_level).(Alpha_context.Level.t.level); |}) in
Error_monad.error_unless
(Alpha_context.Cycle.op_gt last_slashable_cycle current_cycle)
(Build_extensible "Outdated_denunciation"
Validate_errors.Anonymous.Outdated_denunciation
{| Validate_errors.Anonymous.Outdated_denunciation.kind := kind_value;
Validate_errors.Anonymous.Outdated_denunciation.level := given_level;
Validate_errors.Anonymous.Outdated_denunciation.last_cycle :=
last_slashable_cycle; |}).
Definition check_double_endorsing_evidence
(denunciation_kind : Validate_errors.Anonymous.denunciation_kind)
(vi : info) (op1 : Alpha_context.Operation.t)
(op2 : Alpha_context.Operation.t) : M? unit :=
match
(op1.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents),
op2.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents))
with
|
((Alpha_context.Single (Alpha_context.Preendorsement e1),
Alpha_context.Single (Alpha_context.Preendorsement e2)) |
(Alpha_context.Single (Alpha_context.Endorsement e1),
Alpha_context.Single (Alpha_context.Endorsement e2))) ⇒
let op1_hash := Alpha_context.Operation.hash_value op1 in
let op2_hash := Alpha_context.Operation.hash_value op2 in
let? '_ :=
Error_monad.error_unless
((Alpha_context.Raw_level.op_eq
e1.(Alpha_context.consensus_content.level)
e2.(Alpha_context.consensus_content.level)) &&
((Alpha_context.Round.op_eq e1.(Alpha_context.consensus_content.round)
e2.(Alpha_context.consensus_content.round)) &&
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
source
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_ballot_conflict
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
Error_monad.error_value
(Build_extensible "Conflicting_ballot"
Validate_errors.operation_conflict conflict)
end.
Definition add_ballot
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
let ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
source oph
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
in
let voting_state :=
voting_state.with_ballots_seen ballots_seen
vs.(operation_conflict_state.voting_state) in
operation_conflict_state.with_voting_state voting_state vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_ballot
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Ballot {|
Alpha_context.contents.Ballot.source := source |}) ⇒
let ballots_seen :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
source
vs.(operation_conflict_state.voting_state).(voting_state.ballots_seen)
in
operation_conflict_state.with_voting_state
(voting_state.with_ballots_seen ballots_seen
vs.(operation_conflict_state.voting_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
End Voting.
Module Anonymous.
Definition check_activate_account
(vi : info) (operation : Alpha_context.operation) : M? unit :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh;
Alpha_context.contents.Activate_account.activation_code :=
activation_code
|}) ⇒
let blinded_pkh :=
Blinded_public_key_hash.of_ed25519_pkh activation_code edpkh in
let _exists := Alpha_context.Commitment._exists vi.(info.ctxt) blinded_pkh
in
let? '_ :=
Error_monad.error_unless _exists
(Build_extensible "Invalid_activation"
Validate_errors.Anonymous.Invalid_activation
{| Validate_errors.Anonymous.Invalid_activation.pkh := edpkh; |}) in
Error_monad.Lwt_result_syntax.return_unit
| _ ⇒ unreachable_gadt_branch
end.
Definition check_activate_account_conflict
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation)
: Pervasives.result unit Validate_errors.operation_conflict :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
match
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
edpkh
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
with
| None ⇒ ok_unit
| Some existing ⇒
Pervasives.Error
(Validate_errors.Operation_conflict
{|
Validate_errors.operation_conflict.Operation_conflict.existing :=
existing;
Validate_errors.operation_conflict.Operation_conflict.new_operation
:= oph; |})
end
| _ ⇒ unreachable_gadt_branch
end.
Definition wrap_activate_account_conflict
(operation : Alpha_context.operation)
(function_parameter :
Pervasives.result unit Validate_errors.operation_conflict) : M? unit :=
match function_parameter with
| Pervasives.Ok _ ⇒ ok_unit
| Pervasives.Error conflict ⇒
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
Error_monad.error_value
(Build_extensible "Conflicting_activation"
Validate_errors.Anonymous.Conflicting_activation
{| Validate_errors.Anonymous.Conflicting_activation.edpkh := edpkh;
Validate_errors.Anonymous.Conflicting_activation.conflict :=
conflict; |})
| _ ⇒ unreachable_gadt_branch
end
end.
Definition add_activate_account
(vs : operation_conflict_state) (oph : Operation_hash.t)
(operation : Alpha_context.operation) : operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
let activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
edpkh oph
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
in
operation_conflict_state.with_anonymous_state
(anonymous_state.with_activation_pkhs_seen activation_pkhs_seen
vs.(operation_conflict_state.anonymous_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition remove_activate_account
(vs : operation_conflict_state) (operation : Alpha_context.operation)
: operation_conflict_state :=
match
operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
with
|
Alpha_context.Single
(Alpha_context.Activate_account {|
Alpha_context.contents.Activate_account.id := edpkh |}) ⇒
let activation_pkhs_seen :=
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
edpkh
vs.(operation_conflict_state.anonymous_state).(anonymous_state.activation_pkhs_seen)
in
operation_conflict_state.with_anonymous_state
(anonymous_state.with_activation_pkhs_seen activation_pkhs_seen
vs.(operation_conflict_state.anonymous_state)) vs
| _ ⇒ unreachable_gadt_branch
end.
Definition check_denunciation_age
(vi : info) (kind_value : Validate_errors.Anonymous.denunciation_kind)
(given_level : Alpha_context.Raw_level.t) : M? unit :=
let current_cycle := vi.(info.current_level).(Alpha_context.Level.t.cycle)
in
let? res := Alpha_context.Level.from_raw vi.(info.ctxt) given_level in
let given_cycle := res.(Alpha_context.Level.t.cycle) in
let max_slashing_period :=
Alpha_context.Constants.max_slashing_period vi.(info.ctxt) in
let? last_slashable_cycle :=
Alpha_context.Cycle.add given_cycle max_slashing_period in
let? '_ :=
Error_monad.error_unless
(Alpha_context.Cycle.op_lteq given_cycle current_cycle)
(Build_extensible "Too_early_denunciation"
Validate_errors.Anonymous.Too_early_denunciation
{|
Validate_errors.Anonymous.Too_early_denunciation.kind := kind_value;
Validate_errors.Anonymous.Too_early_denunciation.level :=
given_level;
Validate_errors.Anonymous.Too_early_denunciation.current :=
vi.(info.current_level).(Alpha_context.Level.t.level); |}) in
Error_monad.error_unless
(Alpha_context.Cycle.op_gt last_slashable_cycle current_cycle)
(Build_extensible "Outdated_denunciation"
Validate_errors.Anonymous.Outdated_denunciation
{| Validate_errors.Anonymous.Outdated_denunciation.kind := kind_value;
Validate_errors.Anonymous.Outdated_denunciation.level := given_level;
Validate_errors.Anonymous.Outdated_denunciation.last_cycle :=
last_slashable_cycle; |}).
Definition check_double_endorsing_evidence
(denunciation_kind : Validate_errors.Anonymous.denunciation_kind)
(vi : info) (op1 : Alpha_context.Operation.t)
(op2 : Alpha_context.Operation.t) : M? unit :=
match
(op1.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents),
op2.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents))
with
|
((Alpha_context.Single (Alpha_context.Preendorsement e1),
Alpha_context.Single (Alpha_context.Preendorsement e2)) |
(Alpha_context.Single (Alpha_context.Endorsement e1),
Alpha_context.Single (Alpha_context.Endorsement e2))) ⇒
let op1_hash := Alpha_context.Operation.hash_value op1 in
let op2_hash := Alpha_context.Operation.hash_value op2 in
let? '_ :=
Error_monad.error_unless
((Alpha_context.Raw_level.op_eq
e1.(Alpha_context.consensus_content.level)
e2.(Alpha_context.consensus_content.level)) &&
((Alpha_context.Round.op_eq e1.(Alpha_context.consensus_content.round)
e2.(Alpha_context.consensus_content.round)) &&