🍃 Block_header.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Time.

Module shell_header.
  Module Valid.
    Import V8.Block_header.shell_header.

Validity predicate for the [Block_header.shell_header] type

    Record t (x : Block_header.shell_header) : Prop := {
      level : Int32.Valid.t x.(level);
      proto_level : Pervasives.Int.Valid.t x.(proto_level);
      timestamp : Time.Valid.t x.(timestamp);
      validation_passes : Pervasives.Int.Valid.t x.(validation_passes);
    }.
  End Valid.
End shell_header.

Module Valid.
  Import Block_header.t.

Validity predicate for the [Block_header.t] type

  Record t (x : Block_header.t) : Prop := {
    shell : shell_header.Valid.t x.(shell);
  }.
End Valid.

Axiom Block_header_Included_HASHABLE_HASHABLE_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Block_header.Included_HASHABLE.(HASHABLE.encoding).
#[global] Hint Resolve Block_header_Included_HASHABLE_HASHABLE_encoding_is_valid : Data_encoding_db.

Axiom Block_header_shell_header_encoding :
  Data_encoding.Valid.t (fun _ ⇒ True) Block_header.shell_header_encoding.
#[global] Hint Resolve Block_header_shell_header_encoding : Data_encoding_db.

Lemma block_header_encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Block_header.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve block_header_encoding_is_valid : Data_encoding_db.