Skip to main content

🔗 Skip_list_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.FallbackArray.

Module Cell.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

A cell is valid when it is produced either using the [genesis] or the [next] operator.
    Inductive t {cell : Set Set Set} {content ptr : Set}
      {L : Skip_list_repr.S (cell := cell)}
      {deref : ptr option (cell content ptr)}
      : cell content ptr Prop :=
    | Is_genesis content : t (L.(genesis) content)
    | Is_next prev_cell prev_ptr content :
      t prev_cell
      deref prev_ptr = Some prev_cell
      t (L.(next) prev_cell prev_ptr content).
  End Valid.
End Cell.

Module Deref.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

The dereferencing operator is valid when all its target cells are valid.
    Definition t {cell : Set Set Set} {content ptr : Set}
      (L : Skip_list_repr.S (cell := cell))
      (deref : ptr option (cell content ptr)) : Prop :=
       ptr cell, deref ptr = Some cell
      Cell.Valid.t (L := L) (deref := deref) cell.
  End Valid.
End Deref.

We split properties described in this module into individual lemmas, Using `{FArgs} to represent the current functor parameters without having to repeat it
Module S.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

The validity of a skip list implementation.
    Record t {cell : Set Set Set} {content ptr : Set}
      {L : Skip_list_repr.S (cell := cell)}
      {deref : ptr option (cell content ptr)} : Prop := {
      equal equal_content equal_ptr :
        Compare.Equal.Valid.t (a := content) (fun _True) equal_content
        Compare.Equal.Valid.t (a := ptr) (fun _True) equal_ptr
        Compare.Equal.Valid.t (fun _True)
          (L.(equal) equal_content equal_ptr);
      encoding encoding_ptr encoding_cell :
        Data_encoding.Valid.t (a := ptr) (fun _True) encoding_ptr
        Data_encoding.Valid.t (a := content) (fun _True) encoding_cell
        Data_encoding.Valid.t (fun _True)
          (L.(encoding) encoding_ptr encoding_cell);
      back_pointer (cell : cell content ptr) index :
        L.(back_pointer) cell index = List.nth (L.(back_pointers) cell) index;
      back_pointers (cell : cell content ptr) :
        List.Forall (fun ptrderef ptr None)
          (L.(back_pointers) cell);
      genesis_content (content : content) :
        L.(Skip_list_repr.S.content) (L.(genesis) (ptr := ptr) content) =
        content;
      genesis_index (content : content) :
        L.(index_value) (L.(genesis) (ptr := ptr) content) =
        0;
      next_content prev_cell (prev_ptr : ptr) (content : content) :
        L.(Skip_list_repr.S.content) (L.(next) prev_cell prev_ptr content) =
        content;
      next_index prev_cell (prev_ptr : ptr) (content : content) :
        L.(index_value) (L.(next) prev_cell prev_ptr content) =
        L.(index_value) prev_cell +i 1;
      
The primitive [back_path] produces a valid path according to [valid_back_path].
      back_path_is_valid equal_ptr cell_ptr target_ptr target_cell path :
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref target_ptr = Some target_cell
        let target_index := L.(index_value) target_cell in
        L.(back_path) deref cell_ptr target_index = Some path
        L.(valid_back_path) equal_ptr deref cell_ptr target_ptr path = true;
      
The path produced by [back_path] is the only acceptable one for [valid_back_path].
      back_path_is_uniq equal_ptr cell_ptr target_ptr target_cell path :
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref target_ptr = Some target_cell
        let target_index := L.(index_value) target_cell in
        L.(valid_back_path) equal_ptr deref cell_ptr target_ptr path = true
        L.(back_path) deref cell_ptr target_index = Some path;
    }.
    Arguments t {_ _ _}.
  End Valid.
End S.

Module Make.
  Import Proto_alpha.Skip_list_repr.Make.

  Module Back_pointers.
    Module Valid.
Validity of the back-pointers array, given its list of items.
      Record t {ptr : Set} (items : list ptr)
        (x : FallbackArray.t (option ptr)) : Prop := {
        of_list : x = FallbackArray.of_list None Some items;
        int_length : List.Int_length.t items;
      }.
    End Valid.
  End Back_pointers.

  Module Cell.
    Import Proto_alpha.Skip_list_repr.Make.cell.

    Module Valid.
Validity of a cell.
      Record t `{FArgs} {content ptr : Set} (value : cell content ptr) : Prop := {
          v_items : items, Back_pointers.Valid.t items value.(back_pointers)
                               value.(cell.index) = List.length items;
          v_index_int : Pervasives.Int31.Valid.t value.(cell.index);
          v_all_not_none : Forall (fun itemitem None)
                             value.(cell.back_pointers).(FallbackArray.t.items);
          v_default_none : value.(cell.back_pointers).(FallbackArray.t.default)
                           = None }.
    End Valid.
  End Cell.

Simplified definition of the equality check between two list of items. Note that we actually check that [items1] is a prefix of [items2].
  Fixpoint equal_back_pointers_simple {ptr : Set}
    (equal_ptr : ptr ptr bool) (items1 items2 : list ptr) :=
    match items1, items2 with
    | [], _true
    | item1 :: items1, item2 :: items2
      equal_ptr item1 item2 &&
      equal_back_pointers_simple equal_ptr items1 items2
    | _ :: _, []false
    end.

[equal_back_pointers_simple] is reflexive.
  Lemma equal_back_pointers_simple_refl {ptr : Set}
    (equal_ptr : ptr ptr bool) items :
    ( item, equal_ptr item item = true)
    equal_back_pointers_simple equal_ptr items items = true.
  Proof.
    intros; induction items; hauto lq: on.
  Qed.

[equal_back_pointers_simple] is anti-symmetric for two lists of the same length.
  Lemma equal_back_pointers_simple_anti_sym {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 items2 :
    ( item1 item2, equal_ptr item1 item2 = true item1 = item2)
    Lists.List.length items1 = Lists.List.length items2
    equal_back_pointers_simple equal_ptr items1 items2 = true
    items1 = items2.
  Proof.
    intros H_equal_ptr; generalize items2; clear items2.
    induction items1 as [|item1 items1]; simpl; intros items2 H_length H_eq.
    { sauto lq: on. }
    { destruct items2 as [|item2 items2].
      { sfirstorder. }
      { destruct (andb_prop _ _ H_eq) as [H_eq_item H_eq_items].
        hauto q: on.
      }
    }
  Qed.

A reduction step for [equal_back_pointers_simple] to use later in a proof by induction.
  Lemma equal_back_pointers_simple_step {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 x1 items2 :
    List.Int_length.t items1
    equal_back_pointers_simple equal_ptr (items1 ++ [x1]) items2 =
    (equal_back_pointers_simple equal_ptr items1 items2 &&
    match List.nth items2 (List.length items1) with
    | Some x2equal_ptr x1 x2
    | Nonefalse
    end).
  Proof.
    generalize items2; clear items2.
    induction items1 as [|item1 items1]; simpl; intros.
    { destruct items2; simpl; [reflexivity|].
      now rewrite Bool.andb_true_r.
    }
    { destruct items2 as [|item2 items2]; simpl; [reflexivity|].
      rewrite <- Bool.andb_assoc; f_equal; [hauto lq: on|].
      unfold List.Int_length.t in H; simpl in H.
      rewrite IHitems1 by lia.
      f_equal; [hauto lq: on|].
      replace (List.length items1 +i 1 - 1) with (List.length items1).
      2: {
        rewrite List.length_eq.
        lia.
      }
      destruct (List.length items1 +i 1) eqn:?;
        rewrite List.length_eq in *; lia.
    }
  Qed.

A generalized version of the equality check of two arrays of pointers.
  Definition equal_back_pointers_generalized {ptr : Set}
    (equal_ptr : ptr ptr bool) (rev_prefix1 suffix1 items2 : list ptr) :=
    List.fold_left
      (fun acc item1
        (let '(equal, i) := acc in
        fun opt_item1
          (
            equal && Option.equal equal_ptr opt_item1 (List.nth items2 i),
            i +i 1
          )
        ) (Some item1)
      )
      (
        equal_back_pointers_simple equal_ptr (List.rev rev_prefix1) items2,
        List.length rev_prefix1
      )
      suffix1.

[equal_back_pointers_generalized] expressed with [equal_back_pointers_simple].
  Lemma equal_back_pointers_generalized_eq {ptr : Set}
    (equal_ptr : ptr ptr bool) rev_prefix1 suffix1 items2 :
    List.Int_length.t (rev_prefix1 ++ suffix1)
    let items1 := (List.rev rev_prefix1 ++ suffix1)%list in
    equal_back_pointers_generalized equal_ptr rev_prefix1 suffix1 items2 =
    (
      equal_back_pointers_simple equal_ptr items1 items2,
      List.length items1
    ).
  Proof.
    generalize rev_prefix1; clear rev_prefix1.
    induction suffix1 as [|item1 suffix1]; simpl; intros; cbn.
    { now rewrite List.app_nil_r, List.length_rev_eq. }
    { pose proof (IHsuffix1 (item1 :: rev_prefix1)) as H_ind.
      unfold equal_back_pointers_generalized in H_ind.
      rewrite <- List.length_rev_eq.
      rewrite <- equal_back_pointers_simple_step.
      2: {
        unfold List.Int_length.t in ×.
        rewrite List.app_length in ×.
        unfold List.rev, Lists.List.rev'.
        rewrite <- List.rev_alt.
        rewrite List.rev_length.
        lia.
      }
      repeat rewrite <- List.rev_head_app_eq.
      simpl in H_ind.
      rewrite <- H_ind.
      2: {
        unfold List.Int_length.t in ×.
        simpl.
        rewrite List.app_length in ×.
        simpl in ×.
        lia.
      }
      f_equal.
      now rewrite List.app_nil_r, List.length_rev_eq.
    }
  Qed.

Definition extracted from the generated Coq code of [equal].
  Definition equal_back_pointers {ptr : Set}
    (equal_ptr : ptr ptr bool)
    (b1 : FallbackArray.t (option ptr)) (b2 : FallbackArray.t (option ptr))
    : bool :=
    ((FallbackArray.length b1) =i (FallbackArray.length b2)) &&
    (Pervasives.fst
      (FallbackArray.fold
        (fun (function_parameter : bool × int) ⇒
          let '(equal, i_value) := function_parameter in
          fun (h1 : option ptr) ⇒
            ((equal &&
            (Option.equal equal_ptr h1 (FallbackArray.get b2 i_value))),
              (i_value +i 1))) b1 (true, 0))).

[equal_back_pointers] expressed with [equal_back_pointers_simple].
  Lemma equal_back_pointers_eq {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 items2 :
    let b1 := FallbackArray.of_list None Some items1 in
    let b2 := FallbackArray.of_list None Some items2 in
    List.Int_length.t items1
    equal_back_pointers equal_ptr b1 b2 =
      (List.length items1 =? List.length items2) &&
      equal_back_pointers_simple equal_ptr items1 items2.
  Proof.
    unfold equal_back_pointers; simpl; intros.
    repeat rewrite FallbackArray.Of_list.length_eq.
    f_equal; [hauto lq: on|].
    rewrite FallbackArray.Of_list.fold_eq.
    replace (FallbackArray.get _) with (List.nth items2).
    2: {
      apply FunctionalExtensionality.functional_extensionality; intro.
      now rewrite FallbackArray.Of_list.get_eq.
    }
    pose proof (equal_back_pointers_generalized_eq equal_ptr [] items1 items2)
      as H_eq.
    unfold equal_back_pointers_generalized in H_eq; simpl in H_eq.
    sauto lq: on.
  Qed.

The equality function [equal_back_pointers] is valid.
  Lemma equal_back_pointers_is_valid {ptr : Set}
    (equal_ptr : ptr ptr bool) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    Compare.Equal.Valid.t
      (fun b items, Back_pointers.Valid.t items b)
      (equal_back_pointers equal_ptr).
  Proof.
    intros H_equal_ptr b1 b2
      [items1 [H_b1_eq H_b1_length]]
[items2 [H_b2_eq H_b2_length]].
    rewrite H_b1_eq, H_b2_eq.
    rewrite equal_back_pointers_eq by trivial.
    split; intro H.
    { pose proof (FallbackArray.Of_list.of_list_inj _ _ H) as H_eq.
      rewrite <- H_eq.
      apply andb_true_intro; split; [lia|].
      apply equal_back_pointers_simple_refl.
      intro item.
      destruct (H_equal_ptr item item); hauto l: on.
    }
    { assert (items1 = items2); [|congruence].
      destruct (andb_prop _ _ H) as [H_length H_simple].
      apply (equal_back_pointers_simple_anti_sym equal_ptr).
      { intros item1 item2; destruct (H_equal_ptr item1 item2); hauto l: on. }
      { assert (H_length_eq : List.length items1 = List.length items2) by lia.
        repeat rewrite List.length_eq in H_length_eq.
        lia.
      }
      { trivial. }
    }
  Qed.

The equality function [equal] is valid.
  Lemma equal_is_valid `{FArgs} {content ptr : Set} equal_content equal_ptr :
    Compare.Equal.Valid.t (a := content) (fun _True) equal_content
    Compare.Equal.Valid.t (a := ptr) (fun _True) equal_ptr
    Compare.Equal.Valid.t Cell.Valid.t (equal equal_content equal_ptr).
  Proof.
    intros H_content H_ptr.
    replace (equal _ _) with (
      Compare.Equal.projection (fun cell
        let '{|
          cell.content := content;
          cell.back_pointers := back_pointers;
          cell.index := index
        |} := cell in
        (content, back_pointers, index)
      )
      (Compare.Equal.couple
        (Compare.Equal.couple
          equal_content
          (equal_back_pointers equal_ptr))
        Compare.Int.equal
      )
    ).
    2: {
      do 2 (apply FunctionalExtensionality.functional_extensionality; intro).
      unfold equal; cbn.
      now destruct equal_content.
    }
    eapply Compare.Equal.Valid.implies.
    2: {
      apply Compare.Equal.projection_is_valid; [|sauto lq: on].
      repeat apply Compare.Equal.couple_is_valid;
        try apply H_content;
        try (apply equal_back_pointers_is_valid; apply H_ptr);
        try apply Compare.Equal.int_is_valid.
    }
    sauto l: on.
  Qed.

  Definition back_pointers_to_list_generalized `{FArgs} {A : Set}
    (rev_prefix : list A) (array : FallbackArray.t (option A)) : list A :=
    List.rev
      (FallbackArray.fold
         (fun l item
            match item with
            | Some itemitem :: l
            | Noneassert (list A) false
            end)
         array rev_prefix).

  Lemma back_pointers_to_list_generalized_eq `{FArgs} {A : Set}
    (rev_prefix l : list A) :
    let array := FallbackArray.of_list None Some l in
    back_pointers_to_list_generalized rev_prefix array =
      (List.rev rev_prefix ++ l)%list.
  Proof.
    unfold back_pointers_to_list_generalized.
    generalize rev_prefix; clear rev_prefix.
    induction l as [|x l]; intros; rewrite FallbackArray.Of_list.fold_eq; simpl.
    { now rewrite List.app_nil_r. }
    { pose proof (IHl (x :: rev_prefix)) as H_ind.
      rewrite FallbackArray.Of_list.fold_eq in H_ind.
      rewrite H_ind.
      unfold List.rev, Lists.List.rev'.
      repeat rewrite List.rev_append_rev; simpl.
      repeat rewrite List.app_nil_r.
      now rewrite <- List.app_assoc.
    }
  Qed.

  Lemma back_pointers_to_list_eq `{FArgs} {A : Set} (l : list A) :
    let array := FallbackArray.of_list None Some l in
    back_pointers_to_list array = l.
  Proof.
    apply back_pointers_to_list_generalized_eq.
  Qed.

Below we prove that encoding function [encoding] is valid, in order to do so, we need some auxillary definitions and lemmas
Generalized version of [back_pointers_of_list] function, we need it to generalize accumulator [rev_prefix : list ptr]
  Definition back_pointers_of_list_generalized `{FArgs} {ptr : Set}
    (rev_prefix : list ptr) (array : FallbackArray.t (option ptr)) :
    FallbackArray.t (option ptr) :=
    {|
      t.items :=
        Lists.List.map Some
          (rev
             (FallbackArray.fold
                (fun (l_value : list ptr) (function_parameter : M× ptr) ⇒
                   match function_parameter with
                   | Some ptr0ptr0 :: l_value
                   | Noneassert (list ptr) false
                   end) array rev_prefix));
      t.default := None
    |}.

We show equality of result of work of [back_pointers_of_list_generalized] in combination with any initial array [rev_prefix]. We will use this definition for [rewrite] tactic in the proof of Lemma [back_pointers_of_list_to_list], which, in turn, will be used to prove the main lemma: [encoding_pt_cell].
  Lemma back_pointers_of_list_generalized_eq `{FArgs} {ptr : Set}
    (rev_prefix : list ptr) (array : FallbackArray.t (option ptr)):
    array.(FallbackArray.t.default) = None
    Forall (fun itemitem None) (array.(FallbackArray.t.items))
    back_pointers_of_list_generalized rev_prefix array =
      {| t.items :=
          List.rev (Lists.List.map Some rev_prefix) ++
            array.(FallbackArray.t.items) ;
        t.default := array.(FallbackArray.t.default) |}.
  Proof.
    intros.
    unfold back_pointers_of_list_generalized.
    generalize rev_prefix. clear rev_prefix.
    destruct array. induction items as [| x items].
    intros. simpl. rewrite List.app_nil_r. cbn.
    simpl in H0. rewrite H0. f_equal.
    unfold rev, rev'. induction rev_prefix; try reflexivity; simpl.
    rewrite rev_append_rev.
    replace [a] with ([] ++ [a])%list by reflexivity.
    rewrite app_assoc, <- rev_append_rev, map_app, IHrev_prefix,
      rev_append_rev, app_nil_r, rev_append_rev; reflexivity.
    { (* inductive case  *)
      intros. f_equal. simpl in H0. specialize (IHitems H0).
      simpl. destruct x eqn:Destruct_X. cbn. apply Forall_inv_tail in H1.
      specialize (IHitems H1 (p::rev_prefix)). cbn in IHitems.
      injection IHitems as IHitems. rewrite IHitems.
      unfold rev, rev'. rewrite rev_append_rev, <- app_assoc, rev_append_rev,
        app_nil_r; sfirstorder. apply Forall_inv in H1; sfirstorder.
      sfirstorder. }
  Qed.

We will need this property in the main [encoding_pt_cell] lemma
  Lemma back_pointers_of_list_to_list `{FArgs} {ptr : Set}
    ( bp : FallbackArray.t (M× ptr)) :
    bp.(FallbackArray.t.default) = None
    Forall (fun itemitem None) (bp.(FallbackArray.t.items))
    of_list None Some (back_pointers_to_list bp) = bp.
    intros.
    apply back_pointers_of_list_generalized_eq; trivial.
  Qed.

In the lemma [encoding_pt_cell] we prove validity of encoding function.
  Lemma encoding_pt_cell `{FArgs} {content ptr : Set}
    encoding_ptr encoding_cell :
    Data_encoding.Valid.t (a := ptr) (fun _True) encoding_ptr
    Data_encoding.Valid.t (a := content) (fun _True) encoding_cell
    Data_encoding.Valid.t Cell.Valid.t (encoding encoding_ptr encoding_cell).
  Proof.
    intros. split. intros value H2. destruct value.
    eapply Data_encoding.Valid.of_bytes_opt_to_bytes_opt.
    Data_encoding.Valid.data_encoding_auto.
    split. simpl. split. destruct H2. tauto.
    split; [apply I |]. apply List.Forall_True. trivial.
    simpl in ×. inversion H2.
    pose proof (back_pointers_of_list_to_list back_pointers0 v_default_none v_all_not_none).
    hauto lq: on.
    eapply Data_encoding.Valid.to_bytes_opt_of_bytes_opt.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_pt_cell : Data_encoding_db.

  Lemma back_pointer `{FArgs} {content ptr : Set}
    (cell : cell content ptr) index :
    Cell.Valid.t cell
    back_pointer cell index = List.nth (back_pointers cell) index.
  Proof.
    intros.
    unfold back_pointer.
    match goal with
    | H : Cell.Valid.t _ |- _
        inversion H
    end.
    destruct v_items. repeat destruct H1.
    rewrite of_list, FallbackArray.Of_list.get_eq.
    f_equal; unfold back_pointers; rewrite of_list.
    now rewrite back_pointers_to_list_eq.
  Qed.

  Module Back_pointers_valid.
    Module Valid.
      Definition t `{FArgs} {content_type ptr_type c : Set}
        (cell : cell content_type ptr_type)
        (deref : ptr_type option c) : Prop :=
        List.Forall (fun ptrderef ptr None) (back_pointers cell).
    End Valid.
  End Back_pointers_valid.

  Lemma back_pointers `{FArgs} {content_type ptr_type : Set}
    {deref : ptr_type option (cell content_type ptr_type)}
    (cell : cell content_type ptr_type) :
    Back_pointers_valid.Valid.t cell deref
    List.Forall (fun ptrderef ptr None)
      (back_pointers cell).
  Proof.
    intros. inversion H0.
    apply Forall_nil.
    apply Forall_cons; trivial.
  Qed.

  Lemma genesis_content `{FArgs} {content_type ptr_type : Set}
    (content_value : content_type) :
    content (genesis (B := ptr_type) content_value) = content_value.
  Proof.
    reflexivity.
  Qed.

  Lemma genesis_index `{FArgs} {content_type ptr_type : Set}
    (content : content_type)
    (ptr : ptr_type) :
    index_value (genesis (B := ptr_type) content) = 0.
  Proof.
    reflexivity.
  Qed.

  Lemma next_content `{FArgs} {content_type ptr_type : Set}
    (prev_ptr : ptr_type) (content_value : content_type) prev_cell :
    content (next (A := content_type) prev_cell prev_ptr content_value) =
      content_value.
  Proof.
    reflexivity.
  Qed.

  Lemma next_index `{FArgs} {content_type ptr_type : Set}
    prev_cell
    (prev_ptr : ptr_type) (content : content_type) :
    index_value (next (A := content_type) prev_cell prev_ptr content) =
      index_value prev_cell +i 1.
  Proof.
    reflexivity.
  Qed.

@TODO
  Lemma back_path_is_valid `{FArgs} {content_type ptr_type : Set} equal_ptr
    cell_ptr target_ptr target_cell path
    (deref : ptr_type option (cell content_type ptr_type)) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    deref target_ptr = Some target_cell
    let target_index := index_value target_cell in
    back_path deref cell_ptr target_index = Some path
    valid_back_path equal_ptr deref cell_ptr target_ptr path = true.
  Proof. Admitted.

@TODO
  Lemma back_path_is_uniq `{FArgs} {content_type ptr_type : Set} equal_ptr
    cell_ptr target_ptr target_cell path
    (deref : ptr_type option (cell content_type ptr_type)) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    deref target_ptr = Some target_cell
    let target_index := index_value target_cell in
    valid_back_path equal_ptr deref cell_ptr target_ptr path = true
    back_path deref cell_ptr target_index = Some path.
  Proof. Admitted.
End Make.