🍃 Dal.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Module parameters.
  Module Valid.
    Import V8.Dal.parameters.

Validity predicate for [parameters]

    Record t (x : Dal.parameters) : Prop := {
      redundancy_factor :
        Pervasives.UInt8.Valid.t x.(redundancy_factor);
      page_size : Pervasives.UInt16.Valid.t x.(page_size);
      slot_size : Pervasives.Int31.Valid.t x.(slot_size);
      number_of_shards : Pervasives.UInt16.Valid.t x.(number_of_shards);
    }.
  End Valid.
End parameters.

The encoding [parameters_encoding] is valid

Axiom parameters_encoding_is_valid :
  Data_encoding.Valid.t parameters.Valid.t Dal.parameters_encoding.
#[global] Hint Resolve parameters_encoding_is_valid : Data_encoding_db.

Module commitment.
  Module Valid.

Validity predicate for [commitment]

    Axiom t : Dal.commitment → Prop.
  End Valid.
End commitment.

Module Commitment.

The encoding [encoding] is valid

  Axiom encoding_is_valid :
    Data_encoding.Valid.t commitment.Valid.t Dal.Commitment.encoding.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Commitment.