Skip to main content

✅ Validate.v

Translated OCaml

Gitlab , 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
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.

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_slot_availability_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_slot_availability_seen).
  Definition with_preendorsements_seen preendorsements_seen (r : record) :=
    Build r.(predecessor_level) preendorsements_seen r.(endorsements_seen)
      r.(grandparent_endorsements_seen) r.(dal_slot_availability_seen).
  Definition with_endorsements_seen endorsements_seen (r : record) :=
    Build r.(predecessor_level) r.(preendorsements_seen) endorsements_seen
      r.(grandparent_endorsements_seen) r.(dal_slot_availability_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_slot_availability_seen).
  Definition with_dal_slot_availability_seen dal_slot_availability_seen
    (r : record) :=
    Build r.(predecessor_level) r.(preendorsements_seen) r.(endorsements_seen)
      r.(grandparent_endorsements_seen) dal_slot_availability_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_slot_availability_seen :=
              dal_slot_availability_seen
            |} := function_parameter in
        (predecessor_level, preendorsements_seen, endorsements_seen,
          grandparent_endorsements_seen, dal_slot_availability_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_slot_availability_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_slot_availability_seen :=
            dal_slot_availability_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_slot_availability_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_slot_availability_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
      |}).

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

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.
Circumstances in which operations are validated: - [Application] is used for the validation of preexisting block. Corresponds to [Application] of {!Main.validation_mode}. - [Partial_validation] is used to partially validate preexisting block. Corresponds to [Partial_validation] of {!Main.validation_mode}. - [Construction] is used for the construction of a new block. Corresponds to [Full_construction] of {!Main.validation_mode}. - [Mempool] is used by the mempool (either directly or through the plugin). Corresponds to [Partial_construction] of {!Main.validation_mode}.
If you add a new mode, please make sure that it has a way to bound the size of the map {!recfield: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 : application_info mode
| Partial_validation : application_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_slot_availability.
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_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
    | NoneNo_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.

  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
      | NoneNo_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 expectedcheck_round kind_value expected consensus_content
    | Noneok_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
    | Noneok_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 oph'
        Pervasives.Error
          (Validate_errors.Operation_conflict
            {|
              Validate_errors.operation_conflict.Operation_conflict.existing :=
                oph';
              Validate_errors.operation_conflict.Operation_conflict.new_operation
                := oph; |})
      | Noneok_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
      | MempoolNone
      | (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_tzresult_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
    | Noneok_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
    | Noneok_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_endorsementblock_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_slot_availability
    (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_slot_availability _endorser slot_availability) ⇒
      let? '_ :=
        Dal_apply.validate_data_availability vi.(info.ctxt) slot_availability in
      Error_monad.Lwt_tzresult_syntax.return_unit
    | _unreachable_gadt_branch
    end.

  Definition check_dal_slot_availability_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_slot_availability endorser _slot_availability) ⇒
      match
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find_opt)
          endorser
          vs.(operation_conflict_state.consensus_state).(consensus_state.dal_slot_availability_seen)
        with
      | Noneok_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_slot_availability_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_slot_availability;
            Validate_errors.Consensus.Conflicting_consensus_operation.conflict
              := conflict; |})
    end.

  Definition add_dal_slot_availability
    (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_slot_availability endorser _slot_availability) ⇒
      operation_conflict_state.with_consensus_state
        (consensus_state.with_dal_slot_availability_seen
          (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
            endorser oph
            vs.(operation_conflict_state.consensus_state).(consensus_state.dal_slot_availability_seen))
          vs.(operation_conflict_state.consensus_state)) vs
    | _unreachable_gadt_branch
    end.

  Definition remove_dal_slot_availability
    (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_slot_availability endorser _slot_availability) ⇒
      let dal_slot_availability_seen :=
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.remove)
          endorser
          vs.(operation_conflict_state.consensus_state).(consensus_state.dal_slot_availability_seen)
        in
      operation_conflict_state.with_consensus_state
        (consensus_state.with_dal_slot_availability_seen
          dal_slot_availability_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
      | NoneError_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.
Check that [record_proposals] below will not fail.
This function is designed to be exclusively called by [validate_proposals] further down this file.
@return [Error 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? '_ :=
      Internal_errors.do_assert
        (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.

  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.Tzresult_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.Proposalok_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.

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

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

Check that a Proposals operation can be safely applied.
@return [Error Wrong_voting_period_index] if the operation's period and the [context]'s current period 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 Already_proposed] if one of the proposals has already been proposed by the source.
@return [Error Too_many_proposals] if the total count of proposals submitted by the source in previous blocks, in previously validated operations of the current block/mempool, and in the operation to validate, exceeds {!Constants.max_proposals_per_delegate}.
@return [Error Conflict_already_proposed] if one of the operation's proposals has already been submitted by the source in the current block/mempool.
@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_tzresult_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_tzresult_syntax.return_unit
    | _unreachable_gadt_branch
    end.

Check that a Proposals operation is compatible with previously validated voting operations in the current block/mempool..
@return [Error Conflicting_proposals] if the current block/mempool already contains a same source Proposals operation.
  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
      | NoneError_monad.Tzresult_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.

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 Conflicting_ballot] if the source has already submitted a ballot in the current block/mempool.
@return [Error Wrong_voting_period_index] if the operation's period and the [context]'s current period 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 [context]'s current proposal.
@return [Error Already_submitted_a_ballot] if the source has already voted.
@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 voting operations in the current block/mempool.
@return [Error Conflicting_ballot] if the [delegate] has already submitted a ballot in the current block/mempool.
  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
      | Noneok_unit
      | Some oph'
        Pervasives.Error
          (Validate_errors.Operation_conflict
            {|
              Validate_errors.operation_conflict.Operation_conflict.existing :=
                oph';
              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_tzresult_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
      | Noneok_unit
      | Some oph'
        Pervasives.Error
          (Validate_errors.Operation_conflict
            {|
              Validate_errors.operation_conflict.Operation_conflict.existing :=
                oph';
              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)) &&
          ((Pervasives.not
            (Block_payload_hash.equal
              e1.(Alpha_context.consensus_content.block_payload_hash)
              e2.(Alpha_context.consensus_content.block_payload_hash))) &&
          (Operation_hash.op_lt op1_hash op2_hash))))
          (Build_extensible "Invalid_denunciation"
            Validate_errors.Anonymous.denunciation_kind denunciation_kind) in
      let? level :=
        Alpha_context.Level.from_raw vi.(info.ctxt)
          e1.(Alpha_context.consensus_content.level) in
      let? '_ :=
        check_denunciation_age