🧱 Block_header_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.

Require Import TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Blake2B.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Block_header.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.

Module Contents.
  Module Valid.
    Import Block_header_repr.contents.

    Record t (x : Block_header_repr.contents) : Prop := {
      payload_round : Round_repr.Valid.t x.(payload_round);
      proof_of_work_nonce :
        Bytes.length x.(proof_of_work_nonce) =
        Constants_repr.proof_of_work_nonce_size;
    }.
  End Valid.
End Contents.

Module Protocol_data.
  Module Valid.
    Definition t (data : Block_header_repr.protocol_data) : Prop :=
      Contents.Valid.t data.(Block_header_repr.protocol_data.contents).
  End Valid.
End Protocol_data.

Lemma raw_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Block_header_repr.raw_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve raw_encoding_is_valid : Data_encoding_db.

Lemma shell_header_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Block_header_repr.shell_header_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve shell_header_encoding_is_valid : Data_encoding_db.

Lemma contents_encoding_is_valid :
    Data_encoding.Valid.t Contents.Valid.t Block_header_repr.contents_encoding.
  Data_encoding.Valid.data_encoding_auto.
  sauto lq: on.
Qed.
#[global] Hint Resolve contents_encoding_is_valid : Data_encoding_db.

Lemma protocol_data_encoding_is_valid :
    Data_encoding.Valid.t Protocol_data.Valid.t Block_header_repr.protocol_data_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve protocol_data_encoding_is_valid : Data_encoding_db.

Lemma unsigned_encoding_is_valid :
    Data_encoding.Valid.t (fun p ⇒ Contents.Valid.t (snd p)) Block_header_repr.unsigned_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve unsigned_encoding_is_valid : Data_encoding_db.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun x ⇒ Protocol_data.Valid.t x.(Block_header_repr.t.protocol_data)) Block_header_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.