Skip to main content

🎲 Sampler.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Sampler.

Module Make.
  Import FallbackArray.
Validity predicate for [Make.array_encoding_is_valid].
  Module Valid.
    Record t {A : Set} (x : FallbackArray.t A) : Prop := {
      fallback_make : Forall (fun yy = x.(t.default)) x.(t.items);
      perv_int : Pervasives.Int31.Valid.non_negative
        (Z.of_nat (Datatypes.length x.(t.items))); }.
  End Valid.

Auxiliary lemma, we use it in [fallbackArray_make_default]
  Lemma mk_items_default {a : Set} : (default : a) items,
    Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items))
    Forall (fun y : ay = default) items
    mk_items (Z.to_nat (List.length items)) default = items.
  Proof.
    intros default items H H_Length.
    induction items; intros; [sfirstorder|].
    assert (H' : Forall (fun y : ay = default) (a0 :: items)) by scongruence.
    specialize (Forall_inv_tail H') as H''; apply Forall_inv in H'.
    rewrite List.length_eq, Pervasives.normalize_identity, Nat2Z.id; trivial;
      simpl in ×.
    assert (Y : Pervasives.Int.Valid.non_negative
      (Z.of_nat (Datatypes.length items))) by lia.
    apply IHitems in Y; [|trivial].
    rewrite List.length_eq, Pervasives.normalize_identity,
      Nat2Z.id in Y; [|lia]. rewrite H'. f_equal. scongruence.
  Qed.

Auxiliary lemma, we use it in [array_encoding_is_valid]
  Lemma fallbackArray_make_default {a : Set} : (default : a) items,
    Pervasives.Int.Valid.non_negative (Z.of_nat (Datatypes.length items))
    Forall (fun y : ay =
      {| t.items := items; t.default := default |}.(t.default))
      {| t.items := items; t.default := default |}.(t.items)
      make (length {| t.items := items; t.default := default |}) default =
      {| t.items := items; t.default := default |}.
  Proof.
    intros default items H.
    unfold make. pose proof mk_items_default default items H.
    assert
      (Y : {| t.items := items; t.default := default |}.(t.items) = items)
      by scongruence.
    assert
      (Y' : {| t.items := items; t.default := default |}.(t.default) = default)
      by scongruence.
    rewrite Y, Y'.
    hauto lq: on rew: off.
  Qed.

Encoding [array_encoding] is valid.
  Lemma array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
     (venc : Data_encoding.t A), Data_encoding.Valid.t (fun _True) venc
    Data_encoding.Valid.t Valid.t (Sampler.Make.array_encoding venc).
  Proof.
    intros; Data_encoding.Valid.data_encoding_auto.
    intros ? H1; repeat split; [destruct H1; unfold length;
      rewrite List.length_eq; lia..| |].
    { sauto lq: on use: fallbackArray_make_default. }
    { apply fallbackArray_make_default; destruct H1; lia; apply H1. }
  Qed.
  #[global] Hint Resolve array_encoding_is_valid : Data_encoding_db.

  Module MassArray.
    Module Valid.
Validity predicate for [mass_array_encoding_is_valid].
      Record t `{Sampler.Make.FArgs} {A : Set}
        (x : t Sampler.Make.Mass.(Sampler.SMass.t)) := {
        non_negative : Pervasives.Int31.Valid.non_negative
          (Z.of_nat (Datatypes.length x.(t.items)));
        forall_default : Forall (fun yy = x.(t.default)) x.(t.items); }.
    End Valid.

Encoding [mass_array_encoding] is valid.
    Lemma mass_array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
      Data_encoding.Valid.t (fun _True)
        Sampler.Make.Mass.(Sampler.SMass.encoding)
      Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.mass_array_encoding.
    Proof.
      intros; Data_encoding.Valid.data_encoding_auto. intros ? H1.
      repeat split; [destruct H1; unfold length;
        rewrite List.length_eq; lia..|hauto l: on|].
      apply fallbackArray_make_default; destruct H1; lia; apply H1.
    Qed.
    #[global] Hint Resolve mass_array_encoding_is_valid : Data_encoding_db.
  End MassArray.

  Module Int_Array_Encoding.
    Module Valid.
Validity predicate for [int_array_encoding_is_valid].
      Record t `{Sampler.Make.FArgs} {A : Set} (x : t int) := {
        non_negative : Pervasives.Int31.Valid.non_negative
          (Z.of_nat (Datatypes.length x.(t.items)));
        default : Pervasives.Int31.Valid.t x.(t.default);
        forall_default : Forall (fun yy = x.(t.default)) x.(t.items); }.
    End Valid.

Auxiliary function, which is used in [int_array_encoding_is_valid] and other encoding-related proofs in this file.
    Lemma fold_left_eq : xs, (Lists.List.fold_left (fun (acc_value : list int)
      (elt_value : int) ⇒ elt_value :: acc_value) xs nil = rev xs).
    Proof.
      intros. rewrite <- fold_left_rev_right. unfold rev, rev'.
      rewrite <- rev_alt. remember (Lists.List.rev xs) as ys.
      clear Heqys. induction ys; sfirstorder.
    Qed.

Encoding [int_array_encoding] is valid.
    Lemma int_array_encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
      Data_encoding.Valid.t (Valid.t (A:=A)) Sampler.Make.int_array_encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
      intros x H1; destruct H1; unfold length; rewrite List.length_eq;
        destruct x; simpl in ×.
      repeat split; [lia..| | ].
      { unfold fold; rewrite fold_left_eq; unfold rev, rev';
          repeat (rewrite <- rev_alt); rewrite rev_involutive; simpl;
          apply Forall_impl with (P:=(fun y : inty = default0)); lia. }
      { rewrite <- List.length_eq. apply fallbackArray_make_default; lia. }
    Qed.
    #[global] Hint Resolve int_array_encoding_is_valid : Data_encoding_db.
  End Int_Array_Encoding.

  Module Encoding_is_valid.
    Module Valid.
Validity predicate for [encoding_is_valid].
      Record t `{Sampler.Make.FArgs} {A : Set} (x : Sampler.Make.t A) := {
        non_neg_support : Pervasives.Int31.Valid.non_negative (Z.of_nat
          (Datatypes.length x.(Sampler.Make.t.support).(t.items)));
        forall_deflt_sup : Forall (fun yy =
          x.(Sampler.Make.t.support).(t.default))
          x.(Sampler.Make.t.support).(t.items);
        non_neg_p : Pervasives.Int31.Valid.non_negative (Z.of_nat
          (Datatypes.length x.(Sampler.Make.t.p).(t.items)));
        forall_deflt_p : Forall (fun yy = x.(Sampler.Make.t.p).(t.default))
          x.(Sampler.Make.t.p).(t.items);
        non_neg_al : Pervasives.Int31.Valid.non_negative (Z.of_nat
          (Datatypes.length x.(Sampler.Make.t.alias).(t.items)));
        default_alias : Pervasives.Int31.Valid.t x.(Sampler.Make.t.alias).(t.default);
        forall_df_al : Forall (fun yy = x.(Sampler.Make.t.alias).(t.default))
          x.(Sampler.Make.t.alias).(t.items) }.
    End Valid.

Validity of encoding [encoding].
    Lemma encoding_is_valid `{Sampler.Make.FArgs} {A : Set} :
       (enc : Data_encoding.t A), Data_encoding.Valid.t (fun _True) enc
        Data_encoding.Valid.t (fun _True)
          Sampler.Make.Mass.(Sampler.SMass.encoding)
        Data_encoding.Valid.t Valid.t (Sampler.Make.encoding enc).
    Proof.
      intros enc H0 H1.
      Data_encoding.Valid.data_encoding_auto. intros x H2; destruct H2;
        unfold length; destruct x; simpl in *; rewrite List.length_eq in ×.
      repeat split; try lia; try hauto l: on.
      rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
      all : try (rewrite List.length_eq); try lia.
      rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
      unfold fold. rewrite Int_Array_Encoding.fold_left_eq.
      unfold rev, rev'. repeat (rewrite <- rev_alt); rewrite rev_involutive.
      apply Forall_impl with (P:=(fun y : inty = alias.(t.default))); lia.
      rewrite <- List.length_eq; apply fallbackArray_make_default; lia.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Encoding_is_valid.
End Make.

Module Mass.
Validity predicate for [Mass.t].
  Module Valid.
    Definition t (x : int64) : Prop :=
      Int64.Valid.t x.
  End Valid.

The encoding [Mass.encoding] is valid.
  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t
      Sampler.Mass.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Mass.

[Sampler.sample] has no internal errors
Lemma sample_is_valid {A}
  (s : Sampler.Make.t A)
  (f :
    int
    Sampler.Mass.(Sampler.SMass.t)
    int × Sampler.Mass.(Sampler.SMass.t))
  : letP? _ := Sampler.sample s f in True.
Proof. Admitted.