🍃 Block_header.v
Proofs
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.
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.
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.
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.