🍲 Dal_slot_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.

Require TezosOfOCaml.Environment.V8.Proofs.Dal.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.

Import Error.Tactics_letP.

Module Commitment.
  Module Valid.

Validity predicate for [t]

    Definition t (x : Dal_slot_repr.Commitment.t) : Prop :=
      Dal.commitment.Valid.t x.
  End Valid.

The encoding [encoding] is valid

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Dal_slot_repr.Commitment.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Commitment.

Module Index.
  Module Valid.

Validity predicate for the type [t].

    Definition t (x : Dal_slot_repr.Index.t) : Prop :=
      0 ≤ x ≤ Dal_slot_repr.Index.max_value.
    #[global] Hint Unfold t : tezos_z.
  End Valid.

  #[global] Hint Unfold
    Dal_slot_repr.Index.zero
    Dal_slot_repr.Index.max_value :
    tezos_z.

The function [of_int] is valid.

  Lemma of_int_is_valid i :
    Option.Forall Valid.t (Dal_slot_repr.Index.of_int i).
  Proof.
    unfold Dal_slot_repr.Index.of_int.
    destruct (_ ≤i _) eqn:?; destruct (_ ≥i _) eqn:?; simpl; lia.
  Qed.

The equality function [equal] is valid.

  Lemma equal_is_valid :
    Compare.Equal.Valid.t (fun _ ⇒ True) Dal_slot_repr.Index.equal.
  Proof.
    unfold Compare.Equal.Valid.t.
    intros i1 i2 _ _ . unfold Dal_slot_repr.Index.equal.
    lia.
  Qed.
End Index.

Module Header.
  Module id.
    Module Valid.
      Import Proto_alpha.Dal_slot_repr.Header.id.

The validity predicate for the type [Dal_slot_repr.Header.id].

      Record t (x : Dal_slot_repr.Header.id) : Prop := {
        published_level : Raw_level_repr.Valid.t x.(published_level);
        index : Index.Valid.t x.(index);
      }.
    End Valid.
  End id.

  Module Valid.
    Import Dal_slot_repr.Header.t.

The validity predicate for the type [Dal_slot_repr.Header.t].

    Record t (x : Dal_slot_repr.Header.t) : Prop := {
      id : id.Valid.t x.(id);
      commitment : Commitment.Valid.t x.(commitment);
    }.
  End Valid.

The equality function [slot_id_equal]is valid, i.e. captures propositional equality.

  Lemma slot_id_equal_is_valid :
    Compare.Equal.Valid.t (fun _ ⇒ True) Dal_slot_repr.Header.slot_id_equal.
  Proof.
    unfold Compare.Equal.Valid.t.
    intros slot_id1 slot_id2 _ _.
    split ; intros H ;
    unfold Dal_slot_repr.Header.slot_id_equal in ×.
    { subst. apply Bool.andb_true_iff.
      split.
      { apply Raw_level_repr.equal_is_valid ; try constructor. }
      { apply Index.equal_is_valid ; try constructor. }
    }
    { destruct slot_id1, slot_id2.
      symmetry in H. apply Bool.andb_true_eq in H.
      destruct H as [Hpub_level Hindex ].
      symmetry in Hindex.
      apply Index.equal_is_valid in Hindex ; try constructor.
      symmetry in Hpub_level.
      apply Index.equal_is_valid in Hpub_level ; try constructor.
      simpl in ×. subst. reflexivity.
    }
  Qed.

The encoding [id_encoding] is valid

  Lemma id_encoding_is_valid :
    Data_encoding.Valid.t id.Valid.t Dal_slot_repr.Header.id_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve id_encoding_is_valid : Data_encoding_db.

The encoding [encoding] is valid

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Dal_slot_repr.Header.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Header.

Module Page.
  Module Valid.

Validity predicate for the type [Dal_slot_repr.Page.t].

    Record t (page : Dal_slot_repr.Page.t) : Prop := {
      slot_id : Header.id.Valid.t page.(Dal_slot_repr.Page.t.slot_id);
      index : Index.Valid.t page.(Dal_slot_repr.Page.t.page_index);
    }.
  End Valid.

The equality function [equal] on [Page.t] is valid, i.e. captures propositional equality.

  Lemma equal_is_valid :
    Compare.Equal.Valid.t (fun _ ⇒ True) Dal_slot_repr.Page.equal.
  Proof.
    unfold Compare.Equal.Valid.t.
    intros page1 page2 _ _.
    split ; intro H ; try inversion H.
    { unfold Dal_slot_repr.Page.equal.
      subst. apply Bool.andb_true_iff.
      split.
      { apply Header.slot_id_equal_is_valid ; try constructor ; reflexivity. }
      { apply Index.equal_is_valid ; try constructor ; reflexivity. }
    }
    { unfold Dal_slot_repr.Page.equal in H.
      apply Bool.andb_true_iff in H. destruct H as [Hslot_id Hpage_index].
      apply Header.slot_id_equal_is_valid in Hslot_id ; try constructor.
      apply Index.equal_is_valid in Hpage_index ; try constructor.
      destruct page1, page2. subst. reflexivity.
    }
  Qed.

The encoding [Page.encoding] is valid.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t Dal_slot_repr.Page.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros.
    destruct H as [Hslot_id Hindex].
    destruct Hslot_id.
    destruct Hindex.
    destruct x as [slot_id page_index].
    destruct published_level.
    destruct index.
    repeat split ; simpl in × ; try assumption ;lia.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Page.

Module parameters.
  Module Valid.

Validity predicate for [parameters]

    Definition t (x : Dal_slot_repr.parameters) : Prop :=
      Dal.parameters.Valid.t x.
  End Valid.
End parameters.

The encoding [parameters_encoding] is valid

Lemma parameters_encoding_is_valid :
  Data_encoding.Valid.t parameters.Valid.t Dal_slot_repr.parameters_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve parameters_encoding_is_valid : Data_encoding_db.

Module History.

[produce_proof] is valid.

  Lemma produce_proof_is_valid dal_params page_id page_info slots_hist
    hist_cache :
    letP? res := Dal_slot_repr.History.produce_proof dal_params
      page_id page_info slots_hist hist_cache in True.
  Proof.
    unfold Dal_slot_repr.History.produce_proof.
    esplit_letP.
  Admitted.
End History.