🔗 Skip_list_repr.v
Proofs
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.
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.
{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.
(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
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 ptr ⇒ deref 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;
{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 ptr ⇒ deref 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;
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.
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.
(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 item ⇒ item ≠ None)
value.(cell.back_pointers).(FallbackArray.t.items);
v_default_none : value.(cell.back_pointers).(FallbackArray.t.default)
= None }.
End Valid.
End Cell.
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 item ⇒ item ≠ 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_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_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.
(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 x2 ⇒ equal_ptr x1 x2
| None ⇒ false
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.
(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 x2 ⇒ equal_ptr x1 x2
| None ⇒ false
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_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.
(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_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.
(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.
(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 item ⇒ item :: l
| None ⇒ assert (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.
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 item ⇒ item :: l
| None ⇒ assert (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 ptr0 ⇒ ptr0 :: l_value
| None ⇒ assert (list ptr) false
end) array rev_prefix));
t.default := None
|}.
(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 ptr0 ⇒ ptr0 :: l_value
| None ⇒ assert (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 item ⇒ item ≠ 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.
(rev_prefix : list ptr) (array : FallbackArray.t (option ptr)):
array.(FallbackArray.t.default) = None →
Forall (fun item ⇒ item ≠ 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 item ⇒ item ≠ 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.
( bp : FallbackArray.t (M× ptr)) :
bp.(FallbackArray.t.default) = None →
Forall (fun item ⇒ item ≠ 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 ptr ⇒ deref 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 ptr ⇒ deref 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.
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 ptr ⇒ deref 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 ptr ⇒ deref 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.
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.
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.