✅ Validate.v

Translated OCaml

File generated by coq-of-ocaml

Since the expected features of preendorsement and endorsement are the same for all operations in the considered block, we compute them once and for all at the begining of the block.

See [expected_features_for_application], [expected_features_for_construction], and [expected_features_for_partial_construction] in the [Consensus] module below.

Module expected_features.
  Record record : Set := Build {
    level : Alpha_context.Raw_level.t;
    round : option Alpha_context.Round.t;
    branch : Block_hash.t;
    payload_hash : Block_payload_hash.t;
  }.
  Definition with_level level (r : record) :=
    Build level r.(round) r.(branch) r.(payload_hash).
  Definition with_round round (r : record) :=
    Build r.(level) round r.(branch) r.(payload_hash).
  Definition with_branch branch (r : record) :=
    Build r.(level) r.(round) branch r.(payload_hash).
  Definition with_payload_hash payload_hash (r : record) :=
    Build r.(level) r.(round) r.(branch) payload_hash.
End expected_features.
Definition expected_features := expected_features.record.

Records for the constructor parameters

Records for the constructor parameters

Inclusion of the module [Map_Make_include]

  Definition key := Map_Make_include.(Map.S.key).

  Definition t := Map_Make_include.(Map.S.t).

  Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).

  Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).

  Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).

  Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).

  Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).

  Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).

  Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).

  Definition merge {a b c : Set} :=
    Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).

  Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).

  Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).

  Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).

  Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).

  Definition iter_e {a trace : Set} :=
    Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).

  Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).

  Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).

  Definition iter_es {a trace : Set} :=
    Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).

  Definition fold {a b : Set} :=
    Map_Make_include.(Map.S.fold) (a := a) (b := b).

  Definition fold_e {a b trace : Set} :=
    Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).

  Definition fold_s {a b : Set} :=
    Map_Make_include.(Map.S.fold_s) (a := a) (b := b).

  Definition fold_es {a b trace : Set} :=
    Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).

  Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).

  Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).

  Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).

  Definition filter_map {a b : Set} :=
    Map_Make_include.(Map.S.filter_map) (a := a) (b := b).

  Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).

  Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).

  Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).

  Definition min_binding {a : Set} :=
    Map_Make_include.(Map.S.min_binding) (a := a).

  Definition min_binding_opt {a : Set} :=
    Map_Make_include.(Map.S.min_binding_opt) (a := a).

  Definition max_binding {a : Set} :=
    Map_Make_include.(Map.S.max_binding) (a := a).

  Definition max_binding_opt {a : Set} :=
    Map_Make_include.(Map.S.max_binding_opt) (a := a).

  Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).

  Definition choose_opt {a : Set} :=
    Map_Make_include.(Map.S.choose_opt) (a := a).

  Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).

  Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).

  Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).

  Definition find_first {a : Set} :=
    Map_Make_include.(Map.S.find_first) (a := a).

  Definition find_first_opt {a : Set} :=
    Map_Make_include.(Map.S.find_first_opt) (a := a).

  Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).

  Definition find_last_opt {a : Set} :=
    Map_Make_include.(Map.S.find_last_opt) (a := a).

  Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).

  Definition mapi {a b : Set} :=
    Map_Make_include.(Map.S.mapi) (a := a) (b := b).

  Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).

  Definition to_rev_seq {a : Set} :=
    Map_Make_include.(Map.S.to_rev_seq) (a := a).

  Definition to_seq_from {a : Set} :=
    Map_Make_include.(Map.S.to_seq_from) (a := a).

  Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).

  Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).

  Definition iter_ep {a _error : Set} :=
    Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).

  Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
    : Data_encoding.encoding (t A) :=
    Data_encoding.conv (fun (map : t A) ⇒ bindings map)
      (fun (l_value : list (key × A)) ⇒
        List.fold_left
          (fun (m_value : t A) ⇒
            fun (function_parameter : key × A) ⇒
              let '(k_value, v_value) := function_parameter in
              add k_value v_value m_value) empty l_value) None
      (Data_encoding.list_value None
        (Data_encoding.tup2
          (Data_encoding.tup2 Alpha_context.Raw_level.encoding
            Alpha_context.Round.encoding) elt_encoding)).

  (* Double_baking_evidence_map *)
  Definition module :=
    {|
      S.INDEXES_MAP.empty _ := empty;
      S.INDEXES_MAP.is_empty _ := is_empty;
      S.INDEXES_MAP.mem _ := mem;
      S.INDEXES_MAP.add _ := add;
      S.INDEXES_MAP.update _ := update;
      S.INDEXES_MAP.singleton _ := singleton;
      S.INDEXES_MAP.remove _ := remove;
      S.INDEXES_MAP.merge _ _ _ := merge;
      S.INDEXES_MAP.union _ := union;
      S.INDEXES_MAP.compare _ := compare;
      S.INDEXES_MAP.equal _ := equal;
      S.INDEXES_MAP.iter _ := iter;
      S.INDEXES_MAP.iter_e _ _ := iter_e;
      S.INDEXES_MAP.iter_s _ := iter_s;
      S.INDEXES_MAP.iter_p _ := iter_p;
      S.INDEXES_MAP.iter_es _ _ := iter_es;
      S.INDEXES_MAP.fold _ _ := fold;
      S.INDEXES_MAP.fold_e _ _ _ := fold_e;
      S.INDEXES_MAP.fold_s _ _ := fold_s;
      S.INDEXES_MAP.fold_es _ _ _ := fold_es;
      S.INDEXES_MAP.for_all _ := for_all;
      S.INDEXES_MAP._exists _ := _exists;
      S.INDEXES_MAP.filter _ := filter;
      S.INDEXES_MAP.filter_map _ _ := filter_map;
      S.INDEXES_MAP.partition _ := partition;
      S.INDEXES_MAP.cardinal _ := cardinal;
      S.INDEXES_MAP.bindings _ := bindings;
      S.INDEXES_MAP.min_binding _ := min_binding;
      S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
      S.INDEXES_MAP.max_binding _ := max_binding;
      S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
      S.INDEXES_MAP.choose _ := choose;
      S.INDEXES_MAP.choose_opt _ := choose_opt;
      S.INDEXES_MAP.split _ := split;
      S.INDEXES_MAP.find _ := find;
      S.INDEXES_MAP.find_opt _ := find_opt;
      S.INDEXES_MAP.find_first _ := find_first;
      S.INDEXES_MAP.find_first_opt _ := find_first_opt;
      S.INDEXES_MAP.find_last _ := find_last;
      S.INDEXES_MAP.find_last_opt _ := find_last_opt;
      S.INDEXES_MAP.map _ _ := map;
      S.INDEXES_MAP.mapi _ _ := mapi;
      S.INDEXES_MAP.to_seq _ := to_seq;
      S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
      S.INDEXES_MAP.to_seq_from _ := to_seq_from;
      S.INDEXES_MAP.add_seq _ := add_seq;
      S.INDEXES_MAP.of_seq _ := of_seq;
      S.INDEXES_MAP.iter_ep _ _ := iter_ep;
      S.INDEXES_MAP.encoding _ := encoding
    |}.
End Double_baking_evidence_map.
Definition Double_baking_evidence_map := Double_baking_evidence_map.module.

Module Double_endorsing_evidence_map.
  Definition Map_Make_include :=
    Map.Make
      (let t : Set :=
        Alpha_context.Raw_level.t × Alpha_context.Round.t × Alpha_context.Slot.t
        in
      let compare
        (function_parameter :
          Alpha_context.Raw_level.t × Alpha_context.Round.t ×
            Alpha_context.Slot.t)
        : Alpha_context.Raw_level.t × Alpha_context.Round.t ×
          Alpha_context.Slot.t → int :=
        let '(l_value, r_value, s_value) := function_parameter in
        fun (function_parameter :
          Alpha_context.Raw_level.t × Alpha_context.Round.t ×
            Alpha_context.Slot.t) ⇒
          let '(l', r', s') := function_parameter in
          Compare.or_else (Alpha_context.Raw_level.compare l_value l')
            (fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Compare.or_else (Alpha_context.Round.compare r_value r')
                (fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Compare.or_else (Alpha_context.Slot.compare s_value s')
                    (fun (function_parameter : unit) ⇒
                      let '_ := function_parameter in
                      0))) in
      {|
        Compare.COMPARABLE.compare := compare
      |}).

Inclusion of the module [Map_Make_include]

  Definition key := Map_Make_include.(Map.S.key).

  Definition t := Map_Make_include.(Map.S.t).

  Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).

  Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).

  Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).

  Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).

  Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).

  Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).

  Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).

  Definition merge {a b c : Set} :=
    Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).

  Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).

  Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).

  Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).

  Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).

  Definition iter_e {a trace : Set} :=
    Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).

  Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).

  Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).

  Definition iter_es {a trace : Set} :=
    Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).

  Definition fold {a b : Set} :=
    Map_Make_include.(Map.S.fold) (a := a) (b := b).

  Definition fold_e {a b trace : Set} :=
    Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).

  Definition fold_s {a b : Set} :=
    Map_Make_include.(Map.S.fold_s) (a := a) (b := b).

  Definition fold_es {a b trace : Set} :=
    Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).

  Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).

  Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).

  Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).

  Definition filter_map {a b : Set} :=
    Map_Make_include.(Map.S.filter_map) (a := a) (b := b).

  Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).

  Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).

  Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).

  Definition min_binding {a : Set} :=
    Map_Make_include.(Map.S.min_binding) (a := a).

  Definition min_binding_opt {a : Set} :=
    Map_Make_include.(Map.S.min_binding_opt) (a := a).

  Definition max_binding {a : Set} :=
    Map_Make_include.(Map.S.max_binding) (a := a).

  Definition max_binding_opt {a : Set} :=
    Map_Make_include.(Map.S.max_binding_opt) (a := a).

  Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).

  Definition choose_opt {a : Set} :=
    Map_Make_include.(Map.S.choose_opt) (a := a).

  Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).

  Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).

  Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).

  Definition find_first {a : Set} :=
    Map_Make_include.(Map.S.find_first) (a := a).

  Definition find_first_opt {a : Set} :=
    Map_Make_include.(Map.S.find_first_opt) (a := a).

  Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).

  Definition find_last_opt {a : Set} :=
    Map_Make_include.(Map.S.find_last_opt) (a := a).

  Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).

  Definition mapi {a b : Set} :=
    Map_Make_include.(Map.S.mapi) (a := a) (b := b).

  Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).

  Definition to_rev_seq {a : Set} :=
    Map_Make_include.(Map.S.to_rev_seq) (a := a).

  Definition to_seq_from {a : Set} :=
    Map_Make_include.(Map.S.to_seq_from) (a := a).

  Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).

  Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).

  Definition iter_ep {a _error : Set} :=
    Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).

  Definition encoding {A : Set} (elt_encoding : Data_encoding.encoding A)
    : Data_encoding.encoding (t A) :=
    Data_encoding.conv (fun (map : t A) ⇒ bindings map)
      (fun (l_value : list (key × A)) ⇒
        List.fold_left
          (fun (m_value : t A) ⇒
            fun (function_parameter : key × A) ⇒
              let '(k_value, v_value) := function_parameter in
              add k_value v_value m_value) empty l_value) None
      (Data_encoding.list_value None
        (Data_encoding.tup2
          (Data_encoding.tup3 Alpha_context.Raw_level.encoding
            Alpha_context.Round.encoding Alpha_context.Slot.encoding)
          elt_encoding)).

  (* Double_endorsing_evidence_map *)
  Definition module :=
    {|
      S.INDEXES_MAP.empty _ := empty;
      S.INDEXES_MAP.is_empty _ := is_empty;
      S.INDEXES_MAP.mem _ := mem;
      S.INDEXES_MAP.add _ := add;
      S.INDEXES_MAP.update _ := update;
      S.INDEXES_MAP.singleton _ := singleton;
      S.INDEXES_MAP.remove _ := remove;
      S.INDEXES_MAP.merge _ _ _ := merge;
      S.INDEXES_MAP.union _ := union;
      S.INDEXES_MAP.compare _ := compare;
      S.INDEXES_MAP.equal _ := equal;
      S.INDEXES_MAP.iter _ := iter;
      S.INDEXES_MAP.iter_e _ _ := iter_e;
      S.INDEXES_MAP.iter_s _ := iter_s;
      S.INDEXES_MAP.iter_p _ := iter_p;
      S.INDEXES_MAP.iter_es _ _ := iter_es;
      S.INDEXES_MAP.fold _ _ := fold;
      S.INDEXES_MAP.fold_e _ _ _ := fold_e;
      S.INDEXES_MAP.fold_s _ _ := fold_s;
      S.INDEXES_MAP.fold_es _ _ _ := fold_es;
      S.INDEXES_MAP.for_all _ := for_all;
      S.INDEXES_MAP._exists _ := _exists;
      S.INDEXES_MAP.filter _ := filter;
      S.INDEXES_MAP.filter_map _ _ := filter_map;
      S.INDEXES_MAP.partition _ := partition;
      S.INDEXES_MAP.cardinal _ := cardinal;
      S.INDEXES_MAP.bindings _ := bindings;
      S.INDEXES_MAP.min_binding _ := min_binding;
      S.INDEXES_MAP.min_binding_opt _ := min_binding_opt;
      S.INDEXES_MAP.max_binding _ := max_binding;
      S.INDEXES_MAP.max_binding_opt _ := max_binding_opt;
      S.INDEXES_MAP.choose _ := choose;
      S.INDEXES_MAP.choose_opt _ := choose_opt;
      S.INDEXES_MAP.split _ := split;
      S.INDEXES_MAP.find _ := find;
      S.INDEXES_MAP.find_opt _ := find_opt;
      S.INDEXES_MAP.find_first _ := find_first;
      S.INDEXES_MAP.find_first_opt _ := find_first_opt;
      S.INDEXES_MAP.find_last _ := find_last;
      S.INDEXES_MAP.find_last_opt _ := find_last_opt;
      S.INDEXES_MAP.map _ _ := map;
      S.INDEXES_MAP.mapi _ _ := mapi;
      S.INDEXES_MAP.to_seq _ := to_seq;
      S.INDEXES_MAP.to_rev_seq _ := to_rev_seq;
      S.INDEXES_MAP.to_seq_from _ := to_seq_from;
      S.INDEXES_MAP.add_seq _ := add_seq;
      S.INDEXES_MAP.of_seq _ := of_seq;
      S.INDEXES_MAP.iter_ep _ _ := iter_ep;
      S.INDEXES_MAP.encoding _ := encoding
    |}.
End Double_endorsing_evidence_map.
Definition Double_endorsing_evidence_map :=
  Double_endorsing_evidence_map.module.

State used and modified when validating anonymous operations. These fields are used to enforce that we do not validate the same operation multiple times.

Note that as part of {!state}, these maps live in memory. They are not explicitly bounded here, however: - In block validation mode, they are bounded by the number of anonymous operations allowed in the block. - In mempool mode, bounding the number of operations in this map is the responsability of the prevalidator on the shell side.

Static information used to validate manager operations.

State used and modified when validating manager operations.

Module manager_state.
  Record record : Set := Build {
    managers_seen :
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
        Operation_hash.t;
  }.
  Definition with_managers_seen managers_seen (r : record) :=
    Build managers_seen.
End manager_state.
Definition manager_state := manager_state.record.

Definition manager_state_encoding : Data_encoding.encoding manager_state :=
  Data_encoding.def "manager_state" None None
    (Data_encoding.conv
      (fun (function_parameter : manager_state) ⇒
        let '{| manager_state.managers_seen := managers_seen |} :=
          function_parameter in
        managers_seen)
      (fun (managers_seen :
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
          Operation_hash.t) ⇒
        {| manager_state.managers_seen := managers_seen; |}) None
      (Data_encoding.obj1
        (Data_encoding.req None None "managers_seen"
          (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.encoding)
            Operation_hash.encoding)))).

Definition empty_manager_state : manager_state :=
  {|
    manager_state.managers_seen :=
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty);
    |}.

Mode-dependent information needed in final checks.

Module block_finalization_info.
  Record record : Set := Build {
    fitness : Alpha_context.Fitness.t;
    block_producer : Alpha_context.Consensus_key.pk;
    payload_producer : Alpha_context.Consensus_key.pk;
    predecessor_hash : Block_hash.t;
    block_data_contents : Alpha_context.Block_header.contents;
  }.
  Definition with_fitness fitness (r : record) :=
    Build fitness r.(block_producer) r.(payload_producer) r.(predecessor_hash)
      r.(block_data_contents).
  Definition with_block_producer block_producer (r : record) :=
    Build r.(fitness) block_producer r.(payload_producer) r.(predecessor_hash)
      r.(block_data_contents).
  Definition with_payload_producer payload_producer (r : record) :=
    Build r.(fitness) r.(block_producer) payload_producer r.(predecessor_hash)
      r.(block_data_contents).
  Definition with_predecessor_hash predecessor_hash (r : record) :=
    Build r.(fitness) r.(block_producer) r.(payload_producer) predecessor_hash
      r.(block_data_contents).
  Definition with_block_data_contents block_data_contents (r : record) :=
    Build r.(fitness) r.(block_producer) r.(payload_producer)
      r.(predecessor_hash) block_data_contents.
End block_finalization_info.
Definition block_finalization_info := block_finalization_info.record.

Circumstances in which operations are validated, and corresponding information. - [Application] is used for the validation of a preexisting block, often in preparation for its future application. - [Partial_validation] is used to quickly but partially validate a preexisting block, e.g. to quickly decide whether an alternate branch seems viable. In this mode, the initial {!type:context} may come from an ancestor block instead of the predecessor block. Only consensus operations are validated in this mode. - [Construction] is used for the construction of a new block. - [Mempool] is used by the {!module:Mempool} and by the [Partial_construction] mode in {!module:Main}, which may itself be used by RPCs or by another mempool implementation. (The [Mempool] mode is also used by the plugin.)

If you add a new mode, please make sure that it has a way to bound the size of the map {!recfield:manager_state.managers_seen}. Records for the constructor parameters

Validation of consensus operations (validation pass [0]): preendorsement, endorsement, and dal_attestation.

Module Consensus.
  Definition expected_endorsement_features
    (predecessor_level : Alpha_context.Level.t)
    (predecessor_round : Alpha_context.Round.t) (branch : Block_hash.t)
    (payload_hash : Block_payload_hash.t) : expected_features :=
    {|
      expected_features.level :=
        predecessor_level.(Alpha_context.Level.t.level);
      expected_features.round := Some predecessor_round;
      expected_features.branch := branch;
      expected_features.payload_hash := payload_hash; |}.

Expected endorsement features for all modes in which a block is considered: application, partial validation, and construction.

  Definition expected_endorsement_for_block
    (ctxt : Alpha_context.t) (predecessor_level : Alpha_context.Level.t)
    (predecessor_round : Alpha_context.Round.t) : expected_endorsement :=
    match Alpha_context.Consensus.endorsement_branch ctxt with
    | None ⇒ No_expected_branch_for_block_endorsement
    | Some (branch, payload_hash) ⇒
      let expected_features :=
        expected_endorsement_features predecessor_level predecessor_round branch
          payload_hash in
      Expected_endorsement
        {|
          expected_endorsement.Expected_endorsement.expected_features :=
            expected_features; |}
    end.

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

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

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

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

Check that the [apply_testnet_dictator_proposals] function in {!module:Amendment} will not fail.

The current function is designed to be exclusively called by [check_proposals] right below.

@return [Error Testnet_dictator_multiple_proposals] if [proposals] has more than one element.

  Definition check_testnet_dictator_proposals {A : Set}
    (chain_id : Chain_id.t) (proposals : list A) : M ? unit :=
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (Chain_id.op_ltgt chain_id Alpha_context.Constants.mainnet_id)
      in
    match proposals with
    | ([] | cons _ []) ⇒ ok_unit
    | cons _ (cons _ _) ⇒
      Error_monad.error_value
        (Build_extensible "Testnet_dictator_multiple_proposals" unit tt)
    end.

Check that a Proposals operation can be safely applied.

@return [Error Wrong_voting_period_index] if the operation's period and the current period in the {!type:context} do not have the same index.

@return [Error Proposals_from_unregistered_delegate] if the source is not a registered delegate.

@return [Error Empty_proposals] if the list of proposals is empty.

@return [Error Proposals_contain_duplicate] if the list of proposals contains a duplicate element.

@return [Error Wrong_voting_period_kind] if the voting period is not of the Proposal kind.

@return [Error Source_not_in_vote_listings] if the source is not in the vote listings.

@return [Error Too_many_proposals] if the operation causes the source's total number of proposals during the current voting period to exceed {!Constants.max_proposals_per_delegate}.

@return [Error Already_proposed] if one of the proposals has already been proposed by the source in the current voting period.

@return [Error Testnet_dictator_multiple_proposals] if the source is a testnet dictator and the operation contains more than one proposal.

@return [Error Operation.Missing_signature] or [Error Operation.Invalid_signature] if the operation is unsigned or incorrectly signed.

  Definition check_proposals
    (vi : info) (check_signature : bool) (operation : Alpha_context.operation)
    : M ? unit :=
    match
      operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
      with
    |
      Alpha_context.Single
        (Alpha_context.Proposals {|
          Alpha_context.contents.Proposals.source := source;
            Alpha_context.contents.Proposals.period := period;
            Alpha_context.contents.Proposals.proposals := proposals
            |}) ⇒
      let ? current_period :=
        Alpha_context.Voting_period.get_current vi.(info.ctxt) in
      let ? '_ :=
        check_period_index
          current_period.(Alpha_context.Voting_period.voting_period.index)
          period in
      let ? '_ :=
        if
          Amendment.is_testnet_dictator vi.(info.ctxt) vi.(info.chain_id) source
        then
          let ? '_ :=
            check_testnet_dictator_proposals vi.(info.chain_id) proposals in
          Error_monad.Lwt_result_syntax.return_unit
        else
          let ? '_ := check_proposals_source_is_registered vi.(info.ctxt) source
            in
          let ? '_ := check_proposal_list_sanity proposals in
          let ? '_ := check_period_kind_for_proposals current_period in
          let ? '_ := check_in_listings vi.(info.ctxt) source in
          let ? count_in_ctxt :=
            Alpha_context.Vote.get_delegate_proposal_count vi.(info.ctxt) source
            in
          let proposals_length := List.length proposals in
          let ? '_ := check_count count_in_ctxt proposals_length in
          check_already_proposed vi.(info.ctxt) source proposals in
      if check_signature then
        let ? public_key :=
          Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
        Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
          operation
      else
        Error_monad.Lwt_result_syntax.return_unit
    | _ ⇒ unreachable_gadt_branch
    end.

Check that a Proposals operation is compatible with previously validated operations in the current block/mempool.

@return [Error Operation_conflict] if the current block/mempool already contains a Proposals operation from the same source (regardless of whether this source is a testnet dictator or an ordinary manager).

Check that a Ballot operation can be safely applied.

@return [Error Ballot_from_unregistered_delegate] if the source is not a registered delegate.

@return [Error Wrong_voting_period_index] if the operation's period and the current period in the {!type:context} do not have the same index.

@return [Error Wrong_voting_period_kind] if the voting period is not of the Exploration or Promotion kind.

@return [Error Ballot_for_wrong_proposal] if the operation's proposal is different from the current proposal in the context.

@return [Error Already_submitted_a_ballot] if the source has already voted during the current voting period.

@return [Error Source_not_in_vote_listings] if the source is not in the vote listings.

@return [Error Operation.Missing_signature] or [Error Operation.Invalid_signature] if the operation is unsigned or incorrectly signed.

  Definition check_ballot
    (vi : info) (check_signature : bool) (operation : Alpha_context.operation)
    : M ? unit :=
    match
      operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
      with
    |
      Alpha_context.Single
        (Alpha_context.Ballot {|
          Alpha_context.contents.Ballot.source := source;
            Alpha_context.contents.Ballot.period := period;
            Alpha_context.contents.Ballot.proposal := proposal;
            Alpha_context.contents.Ballot.ballot := _
            |}) ⇒
      let ? '_ := check_ballot_source_is_registered vi.(info.ctxt) source in
      let ? current_period :=
        Alpha_context.Voting_period.get_current vi.(info.ctxt) in
      let ? '_ :=
        check_period_index
          current_period.(Alpha_context.Voting_period.voting_period.index)
          period in
      let ? '_ := check_period_kind_for_ballot current_period in
      let ? '_ := check_current_proposal vi.(info.ctxt) proposal in
      let ? '_ := check_source_has_not_already_voted vi.(info.ctxt) source in
      let ? '_ := check_in_listings vi.(info.ctxt) source in
      Error_monad.when_ check_signature
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          let ? public_key :=
            Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source in
          Alpha_context.Operation.check_signature public_key vi.(info.chain_id)
            operation)
    | _ ⇒ unreachable_gadt_branch
    end.

Check that a Ballot operation is compatible with previously validated operations in the current block/mempool.

@return [Error Operation_conflict] if the current block/mempool already contains a Ballot operation from the same source.

State that simulates changes from individual operations that have an effect on future operations inside the same batch.

  Module batch_state.
    Record record : Set := Build {
      balance : Alpha_context.Tez.t;
      is_allocated : bool;
      total_gas_used : Alpha_context.Gas.Arith.fp;
    }.
    Definition with_balance balance (r : record) :=
      Build balance r.(is_allocated) r.(total_gas_used).
    Definition with_is_allocated is_allocated (r : record) :=
      Build r.(balance) is_allocated r.(total_gas_used).
    Definition with_total_gas_used total_gas_used (r : record) :=
      Build r.(balance) r.(is_allocated) total_gas_used.
  End batch_state.
  Definition batch_state := batch_state.record.

Check a few simple properties of the batch, and return the initial {!batch_state} and the contract public key.

Invariants checked: - All operations in a batch have the same source. - The source's contract is allocated. - The counters in a batch are successive, and the first of them is the source's next expected counter. - A batch contains at most one Reveal operation that must occur in first position. - The source's public key has been revealed (either before the considered batch, or during its first operation).

Note that currently, the [op] batch contains only one signature, so all operations in the batch are required to originate from the same manager. This may change in the future, in order to allow several managers to group-sign a sequence of operations.

  Definition check_sanity_and_find_public_key
    (vi : info) (contents_list : Alpha_context.contents_list)
    : M ? (batch_state × Alpha_context.public_key ) :=
    let check_source_and_counter
      (expected_source : Signature.public_key_hash)
      (source : Signature.public_key_hash)
      (previous_counter : Alpha_context.Manager_counter.t)
      (counter : Alpha_context.Manager_counter.t) : M ? unit :=
      let ? '_ :=
        Error_monad.error_unless
          (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
            expected_source source)
          (Build_extensible "Inconsistent_sources" unit tt) in
      Error_monad.error_unless
        (Alpha_context.Manager_counter.op_eq
          (Alpha_context.Manager_counter.succ previous_counter) counter)
        (Build_extensible "Inconsistent_counters" unit tt) in
    let fix check_batch_tail_sanity
      (expected_source : Alpha_context.public_key_hash)
      (previous_counter : Alpha_context.Manager_counter.t)
      (function_parameter : Alpha_context.contents_list) : M ? unit :=
      match function_parameter with
      |
        Alpha_context.Single
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.operation :=
              Alpha_context.Reveal _key
              |}) ⇒
        Error_monad.error_value
          (Build_extensible "Incorrect_reveal_position" unit tt)
      |
        Alpha_context.Cons
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.operation :=
              Alpha_context.Reveal _key
              |}) _res ⇒
        Error_monad.error_value
          (Build_extensible "Incorrect_reveal_position" unit tt)
      |
        Alpha_context.Single
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter
              |}) ⇒
        check_source_and_counter expected_source source previous_counter counter
      |
        Alpha_context.Cons
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter
              |}) rest ⇒
        let ? '_ :=
          check_source_and_counter expected_source source previous_counter
            counter in
        check_batch_tail_sanity source counter rest
      | _ ⇒ unreachable_gadt_branch
      end in
    let check_batch (contents_list : Alpha_context.contents_list)
      : M ?
        (Alpha_context.public_key_hash × option Alpha_context.public_key ×
          Alpha_context.Manager_counter.t ) :=
      match contents_list with
      |
        Alpha_context.Single
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter;
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Reveal key_value
              |}) ⇒ return ? (source, (Some key_value), counter)
      |
        Alpha_context.Single
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter
              |}) ⇒ return ? (source, None, counter)
      |
        Alpha_context.Cons
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter;
              Alpha_context.contents.Manager_operation.operation :=
                Alpha_context.Reveal key_value
              |}) rest ⇒
        let ? '_ := check_batch_tail_sanity source counter rest in
        return ? (source, (Some key_value), counter)
      |
        Alpha_context.Cons
          (Alpha_context.Manager_operation {|
            Alpha_context.contents.Manager_operation.source := source;
              Alpha_context.contents.Manager_operation.counter := counter
              |}) rest ⇒
        let ? '_ := check_batch_tail_sanity source counter rest in
        return ? (source, None, counter)
      | _ ⇒ unreachable_gadt_branch
      end in
    let ? '(source , revealed_key , first_counter ) := check_batch contents_list in
    let ? balance :=
      Alpha_context.Contract.check_allocated_and_get_balance vi.(info.ctxt)
        source in
    let ? '_ :=
      Alpha_context.Contract.check_counter_increment vi.(info.ctxt) source
        first_counter in
    let ? pk :=
      match revealed_key with
      | Some pk ⇒ return ? pk
      | None ⇒
        Alpha_context.Contract.get_manager_key None vi.(info.ctxt) source
      end in
    let initial_batch_state :=
      {| batch_state.balance := balance; batch_state.is_allocated := true;
        batch_state.total_gas_used := Alpha_context.Gas.Arith.zero; |} in
    return ? (initial_batch_state, pk).

  Definition check_gas_limit
    (info_value : info) (gas_limit : Alpha_context.Gas.Arith.integral)
    : M ? unit :=
    Alpha_context.Gas.check_gas_limit
      info_value.(info.manager_info).(manager_info.hard_gas_limit_per_operation)
      gas_limit.

  Definition check_storage_limit (vi : info) (storage_limit : Z.t) : M ? unit :=
    Error_monad.error_unless
      ((storage_limit ≤Z
      vi.(info.manager_info).(manager_info.hard_storage_limit_per_operation)) &&
      (storage_limit ≥Z Z.zero))
      (Build_extensible "Storage_limit_too_high" unit tt).

  Definition assert_tx_rollup_feature_enabled (vi : info) : M ? unit :=
    let ? sunset :=
      Alpha_context.Raw_level.of_int32
        (Alpha_context.Constants.tx_rollup_sunset_level vi.(info.ctxt)) in
    Error_monad.error_unless
      ((Alpha_context.Constants.tx_rollup_enable vi.(info.ctxt)) &&
      (Alpha_context.Raw_level.op_lt
        vi.(info.current_level).(Alpha_context.Level.t.level) sunset))
      (Build_extensible "Tx_rollup_feature_disabled" unit tt).

  Definition assert_sc_rollup_feature_enabled (vi : info) : M ? unit :=
    Error_monad.error_unless
      (Alpha_context.Constants.sc_rollup_enable vi.(info.ctxt))
      (Build_extensible "Sc_rollup_feature_disabled" unit tt).

  Definition assert_not_zero_messages {A : Set} (messages : list A) : M ? unit :=
    match messages with
    | [] ⇒
      Error_monad.error_value
        (Build_extensible "Sc_rollup_add_zero_messages" unit tt)
    | _ ⇒ ok_unit
    end.

  Definition assert_zk_rollup_feature_enabled (vi : info) : M ? unit :=
    Error_monad.error_unless
      (Alpha_context.Constants.zk_rollup_enable vi.(info.ctxt))
      (Build_extensible "Zk_rollup_feature_disabled" unit tt).

  Definition consume_decoding_gas
    (remaining_gas : Alpha_context.Gas.Arith.fp)
    (lexpr : Alpha_context.Script.lazy_expr) : M ? Alpha_context.Gas.Arith.fp :=
    Error_monad.record_trace
      (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
      (Alpha_context.Script.consume_decoding_gas remaining_gas lexpr).

  Definition validate_tx_rollup_submit_batch
    (vi : info) (remaining_gas : Alpha_context.Gas.Arith.fp) (content : string)
    : M ? unit :=
    let ? '_ := assert_tx_rollup_feature_enabled vi in
    let '(_message, message_size) :=
      Alpha_context.Tx_rollup_message.make_batch content in
    let ? cost := Tx_rollup_gas.hash_cost message_size in
    let size_limit :=
      Alpha_context.Constants.tx_rollup_hard_size_limit_per_message
        vi.(info.ctxt) in
    let ? '_ := Alpha_context.Gas.consume_from remaining_gas cost in
    Error_monad.error_unless (message_size ≤i size_limit)
      (Build_extensible "Message_size_exceeds_limit" unit tt).

  Definition validate_tx_rollup_dispatch_tickets
    (vi : info) (remaining_gas : Alpha_context.Gas.Arith.fp)
    (operation : Alpha_context.manager_operation) : M ? unit :=
    let ? '_ := assert_tx_rollup_feature_enabled vi in
    match operation with
    |
      Alpha_context.Tx_rollup_dispatch_tickets {|
        Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.message_result_path
          := message_result_path;
          Alpha_context.manager_operation.Tx_rollup_dispatch_tickets.tickets_info
            := tickets_info
          |} ⇒
      let '{|
        Alpha_context.Constants.Parametric.tx_rollup.max_messages_per_inbox :=
          max_messages_per_inbox;
          Alpha_context.Constants.Parametric.tx_rollup.max_withdrawals_per_batch
            := max_withdrawals_per_batch
          |} := Alpha_context.Constants.tx_rollup vi.(info.ctxt) in
      let ? '_ :=
        Alpha_context.Tx_rollup_errors.check_path_depth
          Alpha_context.Tx_rollup_errors.Commitment
          (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
            message_result_path) max_messages_per_inbox in
      let ? '_ :=
        Error_monad.error_when (Compare.List_length_with.op_eq tickets_info 0)
          (Build_extensible "No_withdrawals_to_dispatch" unit tt) in
      let ? '_ :=
        Error_monad.error_when
          (Compare.List_length_with.op_gt tickets_info max_withdrawals_per_batch)
          (Build_extensible "Too_many_withdrawals" unit tt) in
      let ? '_ :=
        Error_monad.record_trace
          (Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt)
          (List.fold_left_e
            (fun (remaining_gas : Alpha_context.Gas.Arith.fp) ⇒
              fun (function_parameter : Alpha_context.Tx_rollup_reveal.t) ⇒
                let '{|
                  Alpha_context.Tx_rollup_reveal.t.contents := contents;
                    Alpha_context.Tx_rollup_reveal.t.ty := ty_value
                    |} := function_parameter in
                let ? remaining_gas :=
                  Alpha_context.Script.consume_decoding_gas remaining_gas
                    contents in
                Alpha_context.Script.consume_decoding_gas remaining_gas ty_value)
            remaining_gas tickets_info) in
      Error_monad.Result_syntax.return_unit
    | _ ⇒ unreachable_gadt_branch
    end.

  Definition validate_tx_rollup_rejection
    (vi : info) (operation : Alpha_context.manager_operation) : M ? unit :=
    let ? '_ := assert_tx_rollup_feature_enabled vi in
    match operation with
    |
      Alpha_context.Tx_rollup_rejection {|
        Alpha_context.manager_operation.Tx_rollup_rejection.message_path :=
          message_path;
          Alpha_context.manager_operation.Tx_rollup_rejection.message_result_path
            := message_result_path;
          Alpha_context.manager_operation.Tx_rollup_rejection.previous_message_result_path
            := previous_message_result_path
          |} ⇒
      let '{|
        Alpha_context.Constants.Parametric.tx_rollup.max_messages_per_inbox :=
          max_messages_per_inbox
          |} := Alpha_context.Constants.tx_rollup vi.(info.ctxt) in
      let ? '_ :=
        Alpha_context.Tx_rollup_errors.check_path_depth
          Alpha_context.Tx_rollup_errors.Inbox
          (Alpha_context.Tx_rollup_inbox.Merkle.path_depth message_path)
          max_messages_per_inbox in
      let ? '_ :=
        Alpha_context.Tx_rollup_errors.check_path_depth
          Alpha_context.Tx_rollup_errors.Commitment
          (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
            message_result_path) max_messages_per_inbox in
      Alpha_context.Tx_rollup_errors.check_path_depth
        Alpha_context.Tx_rollup_errors.Commitment
        (Alpha_context.Tx_rollup_commitment.Merkle.(Merkle_list.T.path_depth)
          previous_message_result_path) max_messages_per_inbox
    | _ ⇒ unreachable_gadt_branch
    end.

  Definition may_trace_gas_limit_too_high {A : Set} (info_value : info)
    : M ? A → M ? A :=
    match info_value.(info.mode) with
    | (Application _ | Partial_validation _ | Construction _) ⇒
      fun (x_value : M ? A) ⇒ x_value
    | Mempool ⇒
      Error_monad.record_trace (Build_extensible "Gas_limit_too_high" unit tt)
    end.

  Definition check_contents
    (vi : info) (batch_state_value : batch_state)
    (contents : Alpha_context.contents)
    (remaining_block_gas : Alpha_context.Gas.Arith.t) : M ? batch_state :=
    match contents with
    |
      Alpha_context.Manager_operation {|
        Alpha_context.contents.Manager_operation.source := source;
          Alpha_context.contents.Manager_operation.fee := fee;
          Alpha_context.contents.Manager_operation.counter := _;
          Alpha_context.contents.Manager_operation.operation := operation;
          Alpha_context.contents.Manager_operation.gas_limit := gas_limit;
          Alpha_context.contents.Manager_operation.storage_limit :=
            storage_limit
          |} ⇒
      let ? '_ := check_gas_limit vi gas_limit in
      let total_gas_used :=
        Alpha_context.Gas.Arith.add
          batch_state_value.(batch_state.total_gas_used)
          (Alpha_context.Gas.Arith.fp_value gas_limit) in
      let ? '_ :=
        may_trace_gas_limit_too_high vi
          (Error_monad.error_unless
            (Alpha_context.Gas.Arith.op_lteq
              (Alpha_context.Gas.Arith.fp_value total_gas_used)
              remaining_block_gas)
            (Build_extensible "Block_quota_exceeded" unit tt)) in
      let ? remaining_gas :=
        Error_monad.record_trace
          (Build_extensible "Insufficient_gas_for_manager" unit tt)
          (Alpha_context.Gas.consume_from
            (Alpha_context.Gas.Arith.fp_value gas_limit)
            Michelson_v1_gas.Cost_of.manager_operation) in
      let ? '_ := check_storage_limit vi storage_limit in
      let ? '_ :=
        Error_monad.error_unless batch_state_value.(batch_state.is_allocated)
          (Build_extensible "Empty_implicit_contract"
            Alpha_context.public_key_hash source) in
      let ? '_ :=
        match operation with
        | Alpha_context.Reveal pk ⇒
          Alpha_context.Contract.check_public_key pk source
        |
          Alpha_context.Transaction {|
            Alpha_context.manager_operation.Transaction.parameters := parameters
              |} ⇒
          let ? '_ := consume_decoding_gas remaining_gas parameters in
          Error_monad.Result_syntax.return_unit
        |
          Alpha_context.Origination {|
            Alpha_context.manager_operation.Origination.script := script |}
          ⇒
          let ? remaining_gas :=
            consume_decoding_gas remaining_gas
              script.(Alpha_context.Script.t.code) in
          let ? '_ :=
            consume_decoding_gas remaining_gas
              script.(Alpha_context.Script.t.storage) in
          Error_monad.Result_syntax.return_unit
        |
          Alpha_context.Register_global_constant {|
            Alpha_context.manager_operation.Register_global_constant.value := value_value
              |} ⇒
          let ? '_ := consume_decoding_gas remaining_gas value_value in
          Error_monad.Result_syntax.return_unit
        |
          (Alpha_context.Delegation _ | Alpha_context.Set_deposits_limit _ |
          Alpha_context.Increase_paid_storage _ |
          Alpha_context.Update_consensus_key _) ⇒
          Error_monad.Result_syntax.return_unit
        | Alpha_context.Tx_rollup_origination ⇒
          assert_tx_rollup_feature_enabled vi
        |
          Alpha_context.Tx_rollup_submit_batch {|
            Alpha_context.manager_operation.Tx_rollup_submit_batch.content := content
              |} ⇒ validate_tx_rollup_submit_batch vi remaining_gas content
        |
          (Alpha_context.Tx_rollup_commit _ |
          Alpha_context.Tx_rollup_return_bond _ |
          Alpha_context.Tx_rollup_finalize_commitment _ |
          Alpha_context.Tx_rollup_remove_commitment _) ⇒
          assert_tx_rollup_feature_enabled vi
        |
          Alpha_context.Transfer_ticket {|
            Alpha_context.manager_operation.Transfer_ticket.contents := contents;
              Alpha_context.manager_operation.Transfer_ticket.ty := ty_value
              |} ⇒
          let ? '_ := assert_tx_rollup_feature_enabled vi in
          let ? remaining_gas := consume_decoding_gas remaining_gas contents in
          let ? '_ := consume_decoding_gas remaining_gas ty_value in
          Error_monad.Result_syntax.return_unit
        | Alpha_context.Tx_rollup_dispatch_tickets _ ⇒
          validate_tx_rollup_dispatch_tickets vi remaining_gas operation
        | Alpha_context.Tx_rollup_rejection _ ⇒
          validate_tx_rollup_rejection vi operation
        |
          (Alpha_context.Sc_rollup_originate _ |
          Alpha_context.Sc_rollup_cement _ | Alpha_context.Sc_rollup_publish _ |
          Alpha_context.Sc_rollup_refute _ | Alpha_context.Sc_rollup_timeout _ |
          Alpha_context.Sc_rollup_execute_outbox_message _) ⇒
          assert_sc_rollup_feature_enabled vi
        |
          Alpha_context.Sc_rollup_add_messages {|
            Alpha_context.manager_operation.Sc_rollup_add_messages.messages := messages
              |} ⇒
          let ? '_ := assert_sc_rollup_feature_enabled vi in
          assert_not_zero_messages messages
        | Alpha_context.Sc_rollup_recover_bond _ ⇒
          assert_sc_rollup_feature_enabled vi
        |
          Alpha_context.Dal_publish_slot_header {|
            Alpha_context.manager_operation.Dal_publish_slot_header.slot_header :=
              slot_header
              |} ⇒
          Dal_apply.validate_publish_slot_header vi.(info.ctxt) slot_header
        |
          (Alpha_context.Zk_rollup_origination _ |
          Alpha_context.Zk_rollup_publish _ | Alpha_context.Zk_rollup_update _)
          ⇒ assert_zk_rollup_feature_enabled vi
        end in
      let ? '(balance , is_allocated ) :=
        Alpha_context.Contract.simulate_spending vi.(info.ctxt)
          batch_state_value.(batch_state.balance) fee source in
      return ?
        {| batch_state.balance := balance;
          batch_state.is_allocated := is_allocated;
          batch_state.total_gas_used := total_gas_used; |}
    | _ ⇒ unreachable_gadt_branch
    end.

This would be [fold_left_es (check_contents vi) batch_state contents_list] if [contents_list] were an ordinary [list].

Increment [vs.op_count] for all operations, and record non-consensus operation hashes in [vs.recorded_operations_rev].

Definition record_operation
  (vs : block_state) (ophash : Operation_hash.t)
  (validation_pass_opt : option int) : block_state :=
  let op_count := vs.(block_state.op_count) +i 1 in
  match
    (validation_pass_opt,
      match validation_pass_opt with
      | Some n_value ⇒ n_value =i Operation_repr.consensus_pass
      | _ ⇒ false
      end) with
  | (Some n_value, true) ⇒ block_state.with_op_count op_count vs
  | (_, _) ⇒
    block_state.with_recorded_operations_rev
      (cons ophash vs.(block_state.recorded_operations_rev))
      (block_state.with_op_count op_count vs)
  end.

Definition validate_operation (op_staroptstar : option bool)
  : validation_state → Operation_hash.t → Alpha_context.packed_operation →
  M ? validation_state :=
  let check_signature :=
    match op_staroptstar with
    | Some op_starsthstar ⇒ op_starsthstar
    | None ⇒ true
    end in
  fun (function_parameter : validation_state) ⇒
    let '{|
      validation_state.info := info_value;
        validation_state.operation_state := operation_state;
        validation_state.block_state := block_state_value
        |} := function_parameter in
    fun (oph : Operation_hash.t) ⇒
      fun (packed_operation : Alpha_context.packed_operation) ⇒
        let '{|
          Alpha_context.packed_operation.shell := shell;
            Alpha_context.packed_operation.protocol_data :=
              Alpha_context.Operation_data protocol_data
            |} := packed_operation in
        let validation_pass_opt :=
          Alpha_context.Operation.acceptable_pass packed_operation in
        let ? block_state_value :=
          check_validation_pass_consistency info_value block_state_value
            validation_pass_opt in
        let block_state_value :=
          record_operation block_state_value oph validation_pass_opt in
        let operation :=
          {| Alpha_context.operation.shell := shell;
            Alpha_context.operation.protocol_data := protocol_data; |} in
        match
          ((info_value.(info.mode), validation_pass_opt),
            match (info_value.(info.mode), validation_pass_opt) with
            | (Partial_validation _, Some n_value) ⇒
              n_value ≠i Operation_repr.consensus_pass
            | _ ⇒ false
            end) with
        | ((Partial_validation _, Some n_value), true) ⇒
          return ?
            {| validation_state.info := info_value;
              validation_state.operation_state := operation_state;
              validation_state.block_state := block_state_value; |}
        |
          (((Partial_validation _, _) | (Mempool, _) | (Construction _, _) |
          (Application _, _)), _) ⇒
          match
            operation.(Alpha_context.operation.protocol_data).(Alpha_context.protocol_data.contents)
            with
          | Alpha_context.Single (Alpha_context.Preendorsement _) ⇒
            Consensus.validate_preendorsement check_signature info_value
              operation_state block_state_value oph operation
          | Alpha_context.Single (Alpha_context.Endorsement _) ⇒
            Consensus.validate_endorsement check_signature info_value
              operation_state block_state_value oph operation
          | Alpha_context.Single (Alpha_context.Dal_attestation _) ⇒
            let ? '_ := Consensus.check_dal_attestation info_value operation in
            let ? '_ :=
              Consensus.wrap_dal_attestation_conflict
                (Consensus.check_dal_attestation_conflict operation_state oph
                  operation) in
            let operation_state :=
              Consensus.add_dal_attestation operation_state oph operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Proposals _) ⇒
            let ? '_ :=
              Voting.check_proposals info_value check_signature operation in
            let ? '_ :=
              Voting.wrap_proposals_conflict
                (Voting.check_proposals_conflict operation_state oph operation)
              in
            let operation_state :=
              Voting.add_proposals operation_state oph operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Ballot _) ⇒
            let ? '_ := Voting.check_ballot info_value check_signature operation
              in
            let ? '_ :=
              Voting.wrap_ballot_conflict
                (Voting.check_ballot_conflict operation_state oph operation) in
            let operation_state :=
              Voting.add_ballot operation_state oph operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Activate_account _) ⇒
            let ? '_ := Anonymous.check_activate_account info_value operation in
            let ? '_ :=
              Anonymous.wrap_activate_account_conflict operation
                (Anonymous.check_activate_account_conflict operation_state oph
                  operation) in
            let operation_state :=
              Anonymous.add_activate_account operation_state oph operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          |
            Alpha_context.Single
              (Alpha_context.Double_preendorsement_evidence _) ⇒
            let ? '_ :=
              Anonymous.check_double_preendorsement_evidence info_value
                operation in
            let ? '_ :=
              Anonymous.wrap_denunciation_conflict
                Validate_errors.Anonymous.Preendorsement
                (Anonymous.check_double_preendorsement_evidence_conflict
                  operation_state oph operation) in
            let operation_state :=
              Anonymous.add_double_preendorsement_evidence operation_state oph
                operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Double_endorsement_evidence _)
            ⇒
            let ? '_ :=
              Anonymous.check_double_endorsement_evidence info_value operation
              in
            let ? '_ :=
              Anonymous.wrap_denunciation_conflict
                Validate_errors.Anonymous.Endorsement
                (Anonymous.check_double_endorsement_evidence_conflict
                  operation_state oph operation) in
            let operation_state :=
              Anonymous.add_double_endorsement_evidence operation_state oph
                operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Double_baking_evidence _) ⇒
            let ? '_ :=
              Anonymous.check_double_baking_evidence info_value operation in
            let ? '_ :=
              Anonymous.wrap_denunciation_conflict
                Validate_errors.Anonymous.Block
                (Anonymous.check_double_baking_evidence_conflict operation_state
                  oph operation) in
            let operation_state :=
              Anonymous.add_double_baking_evidence operation_state oph operation
              in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Drain_delegate _) ⇒
            let ? '_ :=
              Anonymous.check_drain_delegate info_value check_signature
                operation in
            let ? '_ :=
              Anonymous.wrap_drain_delegate_conflict operation
                (Anonymous.check_drain_delegate_conflict operation_state oph
                  operation) in
            let operation_state :=
              Anonymous.add_drain_delegate operation_state oph operation in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Seed_nonce_revelation _) ⇒
            let ? '_ :=
              Anonymous.check_seed_nonce_revelation info_value operation in
            let ? '_ :=
              Anonymous.wrap_seed_nonce_revelation_conflict
                (Anonymous.check_seed_nonce_revelation_conflict operation_state
                  oph operation) in
            let operation_state :=
              Anonymous.add_seed_nonce_revelation operation_state oph operation
              in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Vdf_revelation _) ⇒
            let ? '_ := Anonymous.check_vdf_revelation info_value operation in
            let ? '_ :=
              Anonymous.wrap_vdf_revelation_conflict
                (Anonymous.check_vdf_revelation_conflict operation_state oph) in
            let operation_state :=
              Anonymous.add_vdf_revelation operation_state oph in
            return ?
              {| validation_state.info := info_value;
                validation_state.operation_state := operation_state;
                validation_state.block_state := block_state_value; |}
          | Alpha_context.Single (Alpha_context.Manager_operation _) ⇒
            Manager.validate_manager_operation check_signature info_value
              operation_state block_state_value oph operation
          | Alpha_context.Cons (Alpha_context.Manager_operation _) _ ⇒
            Manager.validate_manager_operation check_signature info_value
              operation_state block_state_value oph operation
          | Alpha_context.Single (Alpha_context.Failing_noop _) ⇒
            Error_monad.Lwt_result_syntax.tzfail
              (Build_extensible "Failing_noop_error" unit tt)
          | _ ⇒ unreachable_gadt_branch
          end
        end.

Definition are_endorsements_required (vi : info) : M ? bool :=
  Error_monad.Lwt_result_syntax.op_letplus
    (Alpha_context.First_level_of_protocol.get vi.(info.ctxt))
    (fun first_level ⇒
      let level_position_in_protocol :=
        Alpha_context.Raw_level.diff_value
          vi.(info.current_level).(Alpha_context.Level.t.level) first_level in
      level_position_in_protocol >i32 1).

Definition check_endorsement_power (vi : info) (bs : block_state) : M ? unit :=
  let required := Alpha_context.Constants.consensus_threshold vi.(info.ctxt) in
  let provided := bs.(block_state.endorsement_power) in
  Error_monad.error_unless (provided ≥i required)
    (Build_extensible "Not_enough_endorsements"
      Validate_errors.Block.Not_enough_endorsements
      {| Validate_errors.Block.Not_enough_endorsements.required := required;
        Validate_errors.Block.Not_enough_endorsements.provided := provided; |}).

Definition finalize_validate_block_header
  (vi : info) (vs : block_state)
  (checkable_payload_hash : Alpha_context.Block_header.checkable_payload_hash)
  (block_header_contents : Alpha_context.Block_header.contents)
  (round : Alpha_context.Round.t) (fitness : Alpha_context.Fitness.t)
  : M ? unit :=
  let locked_round_evidence :=
    Option.map
      (fun (function_parameter : Alpha_context.Round.t × int) ⇒
        let '(preendorsement_round, preendorsement_count) := function_parameter
          in
        {|
          Alpha_context.Block_header.locked_round_evidence.preendorsement_round
            := preendorsement_round;
          Alpha_context.Block_header.locked_round_evidence.preendorsement_count
            := preendorsement_count; |}) vs.(block_state.locked_round_evidence)
    in
  Alpha_context.Block_header.finalize_validate_block_header
    block_header_contents round fitness checkable_payload_hash
    locked_round_evidence
    (Alpha_context.Constants.consensus_threshold vi.(info.ctxt)).

Definition compute_payload_hash
  (block_state_value : block_state)
  (block_header_contents : Alpha_context.Block_header.contents)
  (predecessor_hash : Block_hash.t) : Block_payload_hash.t :=
  Alpha_context.Block_payload.hash_value predecessor_hash
    block_header_contents.(Alpha_context.Block_header.contents.payload_round)
    (List.rev block_state_value.(block_state.recorded_operations_rev)).

Definition finalize_block (function_parameter : validation_state) : M ? unit :=
  let '{|
    validation_state.info := info_value;
      validation_state.block_state := block_state_value
      |} := function_parameter in
  match info_value.(info.mode) with
  |
    Application {|
      block_finalization_info.fitness := fitness;
        block_finalization_info.predecessor_hash := predecessor_hash;
        block_finalization_info.block_data_contents := block_data_contents
        |} ⇒
    let ? are_endorsements_required := are_endorsements_required info_value in
    let ? '_ :=
      if are_endorsements_required then
        check_endorsement_power info_value block_state_value
      else
        ok_unit in
    let block_payload_hash :=
      compute_payload_hash block_state_value block_data_contents
        predecessor_hash in
    let round := Alpha_context.Fitness.round fitness in
    let ? '_ :=
      finalize_validate_block_header info_value block_state_value
        (Alpha_context.Block_header.Expected_payload_hash block_payload_hash)
        block_data_contents round fitness in
    Error_monad.Lwt_result_syntax.return_unit
  | Partial_validation _ ⇒
    let ? are_endorsements_required := are_endorsements_required info_value in
    let ? '_ :=
      if are_endorsements_required then
        check_endorsement_power info_value block_state_value
      else
        ok_unit in
    Error_monad.Lwt_result_syntax.return_unit
  |
    Construction {|
      mode.Construction.predecessor_round := predecessor_round;
        mode.Construction.predecessor_hash := predecessor_hash;
        mode.Construction.round := round;
        mode.Construction.block_data_contents := block_data_contents
        |} ⇒
    let block_payload_hash :=
      compute_payload_hash block_state_value block_data_contents
        predecessor_hash in
    let locked_round_evidence :=
      block_state_value.(block_state.locked_round_evidence) in
    let checkable_payload_hash :=
      match locked_round_evidence with
      | Some _ ⇒
        Alpha_context.Block_header.Expected_payload_hash block_payload_hash
      | None ⇒ Alpha_context.Block_header.No_check
      end in
    let ? are_endorsements_required := are_endorsements_required info_value in
    let ? '_ :=
      if are_endorsements_required then
        check_endorsement_power info_value block_state_value
      else
        ok_unit in
    let ? fitness :=
      let locked_round :=
        match locked_round_evidence with
        | None ⇒ None
        | Some (preendorsement_round, _power) ⇒ Some preendorsement_round
        end in
      let level :=
        (Alpha_context.Level.current info_value.(info.ctxt)).(Alpha_context.Level.t.level)
        in
      let ? fitness :=
        Alpha_context.Fitness.create level locked_round predecessor_round round
        in
      return ? fitness in
    let ? '_ :=
      finalize_validate_block_header info_value block_state_value
        checkable_payload_hash block_data_contents round fitness in
    Error_monad.Lwt_result_syntax.return_unit
  | Mempool ⇒ Error_monad.Lwt_result_syntax.return_unit
  end.