🌱 Seed_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Seed_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.State_hash.

Module State_hash.
  Module Valid.
    Definition t (s : State_hash.t) : Prop :=
      Bytes.length (State_hash.to_bytes s) = Nonce_hash.size_value ∧
      State_hash.of_bytes_exn (State_hash.to_bytes s) = s.
  End Valid.
End State_hash.

Module Seed.
  Module Valid.
    Definition t (seed : Seed_repr.seed) : Prop :=
      let 'Seed_repr.B hash := seed in
      State_hash.Valid.t hash.
  End Valid.
End Seed.

Module Nonce.
  Module Valid.
    Definition t (nonce : Seed_repr.nonce) : Prop :=
      Bytes.length nonce = Constants_repr.nonce_length.
  End Valid.
End Nonce.

Lemma nonce_encoding_is_valid
  : Data_encoding.Valid.t Nonce.Valid.t Seed_repr.nonce_encoding.
  apply Data_encoding.Valid.Fixed.bytes_value.
Qed.
#[global] Hint Resolve nonce_encoding_is_valid : Data_encoding_db.

Lemma seed_state_hash_encoding_is_valid: Data_encoding.Valid.t State_hash.Valid.t Seed_repr.state_hash_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve seed_state_hash_encoding_is_valid : Data_encoding_db.

Lemma seed_encoding_is_valid :
  Data_encoding.Valid.t Seed.Valid.t Seed_repr.seed_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve seed_encoding_is_valid : Data_encoding_db.