✅ Validate.v

Translated OCaml

File generated by coq-of-ocaml

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.

Records for the constructor parameters

Records for the constructor parameters

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
      |}).

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.

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.

Static information used to validate manager operations.

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);
    |}.

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.

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

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; |}.

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.

Retrieve the expected consensus features for both application and partial validation modes.

Validate an endorsement pointing to the grandparent block. This function will only be called in [Partial_construction] mode.

Validate an endorsement pointing to the predecessor, aka a "normal" endorsement. Only this kind of endorsement may be found during block validation or construction.

Check that the list of proposals is not empty and does not contain duplicates.

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.

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.

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).

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.

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.