🏊 Mempool_validation.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Block_hash.
Require TezosOfOCaml.Environment.V8.Proofs.S.
Require TezosOfOCaml.Proto_alpha.Proofs.Operation_repr.
Require Import TezosOfOCaml.Proto_alpha.Mempool_validation.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.

@TODO 17.11.22 [Proofs.Validate.v] required in proofs, but blacklisted.

(* Require TezosOfOCaml.Proto_alpha.Proofs.Validate. *)
(* Require TezosOfOCaml.Proto_alpha.Proofs.Validate_errors. *)

Module Valid.
  Import Mempool_validation.t.

The validity predicate for the type [Mempool_validation.t].

  Record t (x : Mempool_validation.t) : Prop := {
    predecessor_hash : (* S.HASH.Valid.t x.(predecessor_hash); *) True;
    operation_state : (* Validate.operation_conflict_state.Valid.t  *)
      (* x.(operation_state); *) True;
  }.
End Valid.

The encoding [encoding] is valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.

@TODO 16.11.22 [Proofs.Validate.v] is blacklisted.

Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The function [init_value] is valid

Lemma init_value_is_valid : ∀ ctxt chain_id predecessor_level predecessor_round
  predecessor_hash grandparent_round,
  let '(_, res) := init_value ctxt chain_id predecessor_level predecessor_round
    predecessor_hash grandparent_round
  in Valid.t res.
Proof.

@TODO 16.11.22 Validity predicate is not ready.

Admitted.

The function [remove_operation] is valid

Lemma remove_operation_is_valid : ∀ mempool oph,
  let res := remove_operation mempool oph
  in Valid.t res.
Proof.

@TODO 16.11.22 Validity predicate is not ready.

Admitted.

The function [add_operation] is valid

Lemma add_operation_is_valid op_staropstar opt_conflict_handler
  validate_info t1 pr :
  match add_operation op_staropstar opt_conflict_handler validate_info t1 pr with
  | Pervasives.Ok (t_res, _) ⇒ Valid.t t_res
  | _ ⇒ True
  end.
Proof.

@TODO 16.11.22 Validity predicate is not ready.

Admitted.

The function [merge] is valid

Lemma merge_is_valid conflict_handler existing_mempool new_mempool :
  match merge conflict_handler existing_mempool new_mempool with
  | Pervasives.Ok t_res ⇒ Valid.t t_res
  | _ ⇒ True
  end.
Proof.

@TODO 16.11.22 Validity predicate is not ready.

Admitted.