🕶️ Blinded_public_key_hash.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.

Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

Lemma H_is_valid : S.HASH.Valid.t (fun _ ⇒ True) Blinded_public_key_hash.H.
  apply Blake2B.Make_is_valid.
Qed.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Blinded_public_key_hash.encoding.
  apply H_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[Blinded_public_key_hash.compare] is valid.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ : Blinded_public_key_hash.t ⇒ True) id Blinded_public_key_hash.compare.
Proof.
  apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma Index_is_valid
  : Storage_description.INDEX.Valid.t (fun _ ⇒ True) Blinded_public_key_hash.Index.
  constructor;
    try (apply Path_encoding.Make_hex_is_valid; constructor);
    apply H_is_valid.
Qed.

Module Index.
  Lemma compare_is_valid :
    Compare.Valid.t
      (fun _ : Blinded_public_key_hash.t ⇒ True) id
      Blinded_public_key_hash.Index.compare.
  Proof.
    apply H_is_valid.
  Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Blinded_public_key_hash.Index.encoding.
  Proof.
    apply H_is_valid.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Index.

Module Activation_code.
  Module Valid.
    Definition t (activation_code : Blinded_public_key_hash.activation_code)
      : Prop :=
      Bytes.length activation_code =
      Blinded_public_key_hash.activation_code_size.
  End Valid.
End Activation_code.

Lemma activation_code_encoding_is_valid :
  Data_encoding.Valid.t Activation_code.Valid.t
    Blinded_public_key_hash.activation_code_encoding.
  apply Data_encoding.Valid.Fixed.bytes_value.
Qed.
#[global] Hint Resolve activation_code_encoding_is_valid : Data_encoding_db.