🔗 Skip_list_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.FallbackArray.
Module Cell.
Module Valid.
Import Proto_alpha.Skip_list_repr.S.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.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_ptr equal_content).
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, index, back_pointers)
)
(Compare.Equal.couple
(Compare.Equal.couple
equal_content
Compare.Int.equal)
(equal_back_pointers equal_ptr)
)
).
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_ptr equal_content).
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, index, back_pointers)
)
(Compare.Equal.couple
(Compare.Equal.couple
equal_content
Compare.Int.equal)
(equal_back_pointers equal_ptr)
)
).
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.
intros [] []; simpl in ×.
rewrite back_pointers_of_list_to_list by easy.
hauto l: on.
Qed.
#[global] Hint Resolve encoding_pt_cell : Data_encoding_db.
Lemma back_pointer_lst_nth `{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.
intros [] []; simpl in ×.
rewrite back_pointers_of_list_to_list by easy.
hauto l: on.
Qed.
#[global] Hint Resolve encoding_pt_cell : Data_encoding_db.
Lemma back_pointer_lst_nth `{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.
Here starts the proof of the [Lemma back_path_is_valid].
We decompose all the functions to the smaller ones, getting
rid of nested definitions. This will make it easier to do
formal reasoning in proofs. To be able to run reduction we
equip functions, marked in source code by [bypass ] with [fuel].
We retrieve inner function aux out of back_path and equip it with fuel
Fixpoint aux' `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A)
(cell_value : option (cell B A)) (fuel : nat) {struct fuel} :
option (list A) :=
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
let path := cons ptr path in
Option.bind cell_value
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if Compare.Int.(Compare.S.op_eq) target_index index_value then
Some (List.rev path)
else
if Compare.Int.(Compare.S.op_gt) target_index index_value then
None
else
Option.bind (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒
aux' deref powers target_index path ptr
(deref ptr) fuel)))
end.
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A)
(cell_value : option (cell B A)) (fuel : nat) {struct fuel} :
option (list A) :=
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
let path := cons ptr path in
Option.bind cell_value
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if Compare.Int.(Compare.S.op_eq) target_index index_value then
Some (List.rev path)
else
if Compare.Int.(Compare.S.op_gt) target_index index_value then
None
else
Option.bind (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒
aux' deref powers target_index path ptr
(deref ptr) fuel)))
end.
Generalization of fuel
Parameter bp_compute_fuel : ∀ `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(cell_ptr : A) (target_index : int),
Datatypes.nat.
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(cell_ptr : A) (target_index : int),
Datatypes.nat.
We define [back_path'] - the simulation of [back_path]
Definition back_path' `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
Option.bind (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
let powers := list_powers cell_value in
aux' deref powers target_index nil cell_ptr
(deref cell_ptr)
(bp_compute_fuel deref powers cell_ptr target_index)).
(deref : A → option (cell B A)) (cell_ptr : A) (target_index : int)
: option (list A) :=
Option.bind (deref cell_ptr)
(fun (cell_value : cell B A) ⇒
let powers := list_powers cell_value in
aux' deref powers target_index nil cell_ptr
(deref cell_ptr)
(bp_compute_fuel deref powers cell_ptr target_index)).
We axiomatize equality of our simulation and initial [back_path]
Axiom back_path_eq : ∀ `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (cell_ptr : A)
(target_index : int),
back_path deref cell_ptr target_index =
back_path' deref cell_ptr target_index.
(deref : A → option (cell B A)) (cell_ptr : A)
(target_index : int),
back_path deref cell_ptr target_index =
back_path' deref cell_ptr target_index.
Another way of defining the inner function -
for some lemmas it is more useful to use that definition,
but it is not exactly the same as the [back_path] inner [aux],
so instead of axiomatizing we prove its equivalence
Fixpoint aux'' `{H : FArgs} {A B : Set} (fuel : Datatypes.nat)
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A) : option (list A) :=
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
let path := cons ptr path in
Option.bind (deref ptr)
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if Compare.Int.(Compare.S.op_eq) target_index index_value then
Some (List.rev path)
else
if Compare.Int.(Compare.S.op_gt) target_index index_value then
None
else
Option.bind (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒
aux'' fuel deref powers target_index path ptr)))
end.
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A) : option (list A) :=
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
let path := cons ptr path in
Option.bind (deref ptr)
(fun (cell_value : cell B A) ⇒
let index_value := cell_value.(cell.index) in
if Compare.Int.(Compare.S.op_eq) target_index index_value then
Some (List.rev path)
else
if Compare.Int.(Compare.S.op_gt) target_index index_value then
None
else
Option.bind (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
Option.bind (back_pointer cell_value best_idx)
(fun (ptr : A) ⇒
aux'' fuel deref powers target_index path ptr)))
end.
Lemma states that we have enough fuel (will be used in one-step-reduction
proofs)
Lemma aux'_sufficient_fuel `{FArgs} {A B : Set} (deref : A → M× cell B A)
(powers : FallbackArray.t int) (target_index : int) (path : list A)
(ptr : A) (cell : M× cell B A) (fuel fuel' : Datatypes.nat)
(res : list A) :
aux' deref powers target_index path ptr cell fuel = Some res →
(fuel ≤ fuel')%nat →
aux' deref powers target_index path ptr cell fuel' = Some res.
Proof.
intros. revert path ptr cell fuel H0 H1.
induction fuel'; [ sauto lq: on rew: off |].
intros. destruct fuel; try discriminate. simpl in ×.
destruct cell0; try discriminate. simpl in ×.
destruct (target_index =? c.(cell.index)); trivial.
destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate. simpl in ×.
destruct (back_pointer c i); try discriminate. simpl in ×.
apply IHfuel' with fuel; intuition.
Qed.
(powers : FallbackArray.t int) (target_index : int) (path : list A)
(ptr : A) (cell : M× cell B A) (fuel fuel' : Datatypes.nat)
(res : list A) :
aux' deref powers target_index path ptr cell fuel = Some res →
(fuel ≤ fuel')%nat →
aux' deref powers target_index path ptr cell fuel' = Some res.
Proof.
intros. revert path ptr cell fuel H0 H1.
induction fuel'; [ sauto lq: on rew: off |].
intros. destruct fuel; try discriminate. simpl in ×.
destruct cell0; try discriminate. simpl in ×.
destruct (target_index =? c.(cell.index)); trivial.
destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate. simpl in ×.
destruct (back_pointer c i); try discriminate. simpl in ×.
apply IHfuel' with fuel; intuition.
Qed.
Equality of simulations
Lemma aux''_eq_aux' `{FArgs} {A B : Set}
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A) (fuel : nat) :
aux'' fuel deref powers target_index path ptr =
aux' deref powers target_index path ptr (deref ptr) fuel.
Proof.
revert path ptr. induction fuel; trivial. intros. simpl.
destruct (deref ptr); trivial. simpl in ×.
destruct (target_index =? c.(cell.index)); trivial.
destruct (target_index >? c.(cell.index)); trivial.
destruct (best_skip c target_index); trivial. simpl in ×.
destruct (back_pointer c i); trivial. now simpl in ×.
Qed.
(deref : A → option (cell B A)) (powers : FallbackArray.t int)
(target_index : int) (path : list A) (ptr : A) (fuel : nat) :
aux'' fuel deref powers target_index path ptr =
aux' deref powers target_index path ptr (deref ptr) fuel.
Proof.
revert path ptr. induction fuel; trivial. intros. simpl.
destruct (deref ptr); trivial. simpl in ×.
destruct (target_index =? c.(cell.index)); trivial.
destruct (target_index >? c.(cell.index)); trivial.
destruct (best_skip c target_index); trivial. simpl in ×.
destruct (back_pointer c i); trivial. now simpl in ×.
Qed.
Simulation aux'' has enough fuel for inner one-step-reductions
Lemma aux''_sufficient_fuel `{FArgs} {A B : Set} (deref : A → M× cell B A)
(powers : FallbackArray.t int) (target_index : int) (path : list A)
(ptr : A) (fuel fuel' : Datatypes.nat) (res : list A) :
aux'' fuel deref powers target_index path ptr = Some res →
(fuel ≤ fuel')%nat →
aux'' fuel' deref powers target_index path ptr = Some res.
Proof.
rewrite aux''_eq_aux', aux''_eq_aux'. apply aux'_sufficient_fuel.
Qed.
(powers : FallbackArray.t int) (target_index : int) (path : list A)
(ptr : A) (fuel fuel' : Datatypes.nat) (res : list A) :
aux'' fuel deref powers target_index path ptr = Some res →
(fuel ≤ fuel')%nat →
aux'' fuel' deref powers target_index path ptr = Some res.
Proof.
rewrite aux''_eq_aux', aux''_eq_aux'. apply aux'_sufficient_fuel.
Qed.
Initial cell of successfully generated path can not be [None]
Lemma back_path'_cell_not_none `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr : ptr_type) target_index (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some path →
∃ c_cell, deref cell_ptr = Some c_cell.
Proof.
intros. destruct (deref cell_ptr) eqn:DC.
{ ∃ c; reflexivity. }
{ unfold back_path' in H0. rewrite DC in ×. discriminate. }
Qed.
(* @TODO move to lists library*)
Lemma list_rev_not_nil {A : Set} : ∀ (acc : list A) p,
rev (p :: acc) = [] → False.
Proof.
intros. replace (rev (p :: acc))%list with
((rev (p :: acc) ++ []))%list in H by hauto lq: on.
rewrite List.rev_head_app_eq in H.
symmetry in H.
apply app_cons_not_nil in H. inversion H.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr : ptr_type) target_index (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some path →
∃ c_cell, deref cell_ptr = Some c_cell.
Proof.
intros. destruct (deref cell_ptr) eqn:DC.
{ ∃ c; reflexivity. }
{ unfold back_path' in H0. rewrite DC in ×. discriminate. }
Qed.
(* @TODO move to lists library*)
Lemma list_rev_not_nil {A : Set} : ∀ (acc : list A) p,
rev (p :: acc) = [] → False.
Proof.
intros. replace (rev (p :: acc))%list with
((rev (p :: acc) ++ []))%list in H by hauto lq: on.
rewrite List.rev_head_app_eq in H.
symmetry in H.
apply app_cons_not_nil in H. inversion H.
Qed.
Result path can not be empty, proved for auxiliary function
Fixpoint aux'_not_nil `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) target_index (acc_path : list ptr_type)
cell_ptr (cell : option (cell content_type ptr_type)) fuel {struct fuel} :
aux' deref powers target_index acc_path cell_ptr cell fuel = Some [] →
False.
Proof.
unfold aux'.
destruct fuel. scongruence.
destruct cell; try scongruence.
simpl. destruct (target_index =? c.(cell.index)) eqn:TI.
intro H0. injection H0 as H0.
apply list_rev_not_nil in H0. inversion H0.
destruct (target_index >? c.(cell.index)); try scongruence.
destruct (best_skip c target_index); try scongruence.
simpl. destruct (back_pointer c i); try scongruence.
simpl. hauto l: on.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) target_index (acc_path : list ptr_type)
cell_ptr (cell : option (cell content_type ptr_type)) fuel {struct fuel} :
aux' deref powers target_index acc_path cell_ptr cell fuel = Some [] →
False.
Proof.
unfold aux'.
destruct fuel. scongruence.
destruct cell; try scongruence.
simpl. destruct (target_index =? c.(cell.index)) eqn:TI.
intro H0. injection H0 as H0.
apply list_rev_not_nil in H0. inversion H0.
destruct (target_index >? c.(cell.index)); try scongruence.
destruct (best_skip c target_index); try scongruence.
simpl. destruct (back_pointer c i); try scongruence.
simpl. hauto l: on.
Qed.
Result path can not be empty, proved for main function
Fixpoint back_path'_not_nil `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr : ptr_type) target_index (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some [] → False.
Proof.
unfold back_path'.
destruct deref; simpl; [| discriminate ].
apply (aux'_not_nil
deref (list_powers c) target_index nil cell_ptr (Some c)).
Qed.
(* @TODO move to lists library*)
Fact list_rev_cons {A : Set} (a : A) (l : list A) :
List.rev (a::l) = (List.rev l ++ [a])%list.
Proof.
sauto lq: on use: app_nil_r, List.rev_head_app_eq.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr : ptr_type) target_index (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some [] → False.
Proof.
unfold back_path'.
destruct deref; simpl; [| discriminate ].
apply (aux'_not_nil
deref (list_powers c) target_index nil cell_ptr (Some c)).
Qed.
(* @TODO move to lists library*)
Fact list_rev_cons {A : Set} (a : A) (l : list A) :
List.rev (a::l) = (List.rev l ++ [a])%list.
Proof.
sauto lq: on use: app_nil_r, List.rev_head_app_eq.
Qed.
Result of sucessfull work of second simulation [aux'']
Lemma aux''_nonempty_success `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (cell_ptr : ptr_type)
(path' : list ptr_type) (target_index : int) (fuel : Datatypes.nat) :
(∃ l, aux'' fuel deref powers target_index path' cell_ptr = Some l) →
∃ l,
aux'' fuel deref powers target_index path' cell_ptr
= Some (rev path' ++ cell_ptr :: l)%list.
Proof.
revert cell_ptr path'.
induction fuel; intros cell_ptr path' []; try discriminate.
simpl in ×.
destruct (deref cell_ptr); try discriminate.
simpl in ×.
destruct (target_index =? c.(cell.index)).
{ hauto lq: on use: list_rev_cons. }
{ destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate.
simpl in ×.
destruct (back_pointer c i); try discriminate.
simpl in ×.
specialize IHfuel with p (cell_ptr :: path').
hauto q: on use: List.app_assoc, list_rev_cons.
}
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (cell_ptr : ptr_type)
(path' : list ptr_type) (target_index : int) (fuel : Datatypes.nat) :
(∃ l, aux'' fuel deref powers target_index path' cell_ptr = Some l) →
∃ l,
aux'' fuel deref powers target_index path' cell_ptr
= Some (rev path' ++ cell_ptr :: l)%list.
Proof.
revert cell_ptr path'.
induction fuel; intros cell_ptr path' []; try discriminate.
simpl in ×.
destruct (deref cell_ptr); try discriminate.
simpl in ×.
destruct (target_index =? c.(cell.index)).
{ hauto lq: on use: list_rev_cons. }
{ destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate.
simpl in ×.
destruct (back_pointer c i); try discriminate.
simpl in ×.
specialize IHfuel with p (cell_ptr :: path').
hauto q: on use: List.app_assoc, list_rev_cons.
}
Qed.
Head pointers are equal - one of conditions of valid_path
Lemma aux''_equal_head `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(fuel : Datatypes.nat) (equal_ptr : ptr_type → ptr_type → bool) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux'' fuel deref powers target_index acc_path cell_ptr =
Some (rev acc_path ++ (ptr::rest_path))%list →
equal_ptr ptr cell_ptr = true.
Proof.
intros.
destruct (aux''_nonempty_success
deref powers cell_ptr acc_path target_index fuel);
eauto.
rewrite H1 in H2.
unfold Compare.Equal.Valid.t in H0.
hauto lq: on use: List.app_inv_head.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(fuel : Datatypes.nat) (equal_ptr : ptr_type → ptr_type → bool) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux'' fuel deref powers target_index acc_path cell_ptr =
Some (rev acc_path ++ (ptr::rest_path))%list →
equal_ptr ptr cell_ptr = true.
Proof.
intros.
destruct (aux''_nonempty_success
deref powers cell_ptr acc_path target_index fuel);
eauto.
rewrite H1 in H2.
unfold Compare.Equal.Valid.t in H0.
hauto lq: on use: List.app_inv_head.
Qed.
First auxiliary simulation. Proof of it's successfull result
Lemma aux'_nonempty_success `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (cell_ptr : ptr_type)
(path' : list ptr_type) (target_index : int)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
(∃ l,
aux' deref powers target_index path' cell_ptr cell fuel = Some l) →
∃ l,
aux' deref powers target_index path' cell_ptr cell fuel
= Some (rev path' ++ cell_ptr :: l)%list.
Proof.
revert cell_ptr cell path'.
induction fuel; intros cell_ptr cell path' []; try discriminate.
simpl in ×.
destruct cell; try discriminate.
simpl in ×.
destruct (target_index =? c.(cell.index)).
{ hauto lq: on use: list_rev_cons. }
{ destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate.
simpl in ×.
destruct (back_pointer c i); try discriminate.
simpl in ×.
specialize IHfuel with p (deref p) (cell_ptr :: path').
hauto q: on use: List.app_assoc, list_rev_cons.
}
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (cell_ptr : ptr_type)
(path' : list ptr_type) (target_index : int)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
(∃ l,
aux' deref powers target_index path' cell_ptr cell fuel = Some l) →
∃ l,
aux' deref powers target_index path' cell_ptr cell fuel
= Some (rev path' ++ cell_ptr :: l)%list.
Proof.
revert cell_ptr cell path'.
induction fuel; intros cell_ptr cell path' []; try discriminate.
simpl in ×.
destruct cell; try discriminate.
simpl in ×.
destruct (target_index =? c.(cell.index)).
{ hauto lq: on use: list_rev_cons. }
{ destruct (target_index >? c.(cell.index)); try discriminate.
destruct (best_skip c target_index); try discriminate.
simpl in ×.
destruct (back_pointer c i); try discriminate.
simpl in ×.
specialize IHfuel with p (deref p) (cell_ptr :: path').
hauto q: on use: List.app_assoc, list_rev_cons.
}
Qed.
[cell_ptr] argument is the head of the successful result of
(the first simulation of) [aux] (discarding the accumulator [acc])
Lemma aux'_equal_Prop_head `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
aux' deref powers target_index acc_path cell_ptr cell fuel =
Some (rev acc_path ++ (ptr::rest_path))%list →
ptr = cell_ptr.
Proof.
intros.
destruct (aux'_nonempty_success
deref powers cell_ptr acc_path target_index cell fuel);
eauto.
rewrite H0 in H1.
unfold Compare.Equal.Valid.t in H0.
hauto lq: on use: List.app_inv_head.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
aux' deref powers target_index acc_path cell_ptr cell fuel =
Some (rev acc_path ++ (ptr::rest_path))%list →
ptr = cell_ptr.
Proof.
intros.
destruct (aux'_nonempty_success
deref powers cell_ptr acc_path target_index cell fuel);
eauto.
rewrite H0 in H1.
unfold Compare.Equal.Valid.t in H0.
hauto lq: on use: List.app_inv_head.
Qed.
[cell_ptr] is the head of the successful result of [back_path]
Lemma back_path'_equal_Prop_head `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some (ptr :: path) →
ptr = cell_ptr.
Proof.
unfold back_path'. destruct deref; simpl; [| discriminate ].
hauto l: on use: aux'_equal_Prop_head.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
back_path' deref cell_ptr target_index = Some (ptr :: path) →
ptr = cell_ptr.
Proof.
unfold back_path'. destruct deref; simpl; [| discriminate ].
hauto l: on use: aux'_equal_Prop_head.
Qed.
Auxiliary function for equality of headers
Lemma aux'_equal_head `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat)
(equal_ptr : ptr_type → ptr_type → bool) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux' deref powers target_index acc_path cell_ptr cell fuel =
Some (rev acc_path ++ (ptr::rest_path))%list →
equal_ptr ptr cell_ptr = true.
Proof.
unfold Compare.Equal.Valid.t. intros. apply H0; trivial.
hauto lq: on use: aux'_equal_Prop_head.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (target_index : int)
(acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
(cell : M× cell content_type ptr_type) (fuel : Datatypes.nat)
(equal_ptr : ptr_type → ptr_type → bool) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux' deref powers target_index acc_path cell_ptr cell fuel =
Some (rev acc_path ++ (ptr::rest_path))%list →
equal_ptr ptr cell_ptr = true.
Proof.
unfold Compare.Equal.Valid.t. intros. apply H0; trivial.
hauto lq: on use: aux'_equal_Prop_head.
Qed.
Auxiliary function for equality of head and a parameter
Lemma back_path'_equal_head `{FArgs} {content_type ptr_type : Set} equal_ptr
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
back_path' deref cell_ptr target_index = Some (ptr :: path) →
equal_ptr ptr cell_ptr = true.
Proof.
unfold back_path'. destruct deref; simpl; [| discriminate ].
hauto l: on use: aux'_equal_head.
Qed.
(deref : ptr_type → option (cell content_type ptr_type))
(cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
back_path' deref cell_ptr target_index = Some (ptr :: path) →
equal_ptr ptr cell_ptr = true.
Proof.
unfold back_path'. destruct deref; simpl; [| discriminate ].
hauto l: on use: aux'_equal_head.
Qed.
Step of decomposition. We retrieve all nested definitions in
order to be able to do different kind of manipulations with them.
Fixpoint valid_path' `{FArgs} {content_type ptr_type : Set}
equal_ptr target_ptr (target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
(path : list ptr_type) {struct path} : bool :=
let target_index := Skip_list_repr.Make.index_value target_cell in
match path with
| [] ⇒
(equal_ptr target_ptr cell_ptr) &&
(Compare.Int.(Compare.S.op_eq) index_value target_index)
| cell_ptr' :: path ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell content_type ptr_type) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell content_type ptr_type) ⇒
mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : ptr_type) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal &&
(valid_path' equal_ptr target_ptr target_cell deref
powers index' cell_ptr' path)))))
end.
equal_ptr target_ptr (target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
(path : list ptr_type) {struct path} : bool :=
let target_index := Skip_list_repr.Make.index_value target_cell in
match path with
| [] ⇒
(equal_ptr target_ptr cell_ptr) &&
(Compare.Int.(Compare.S.op_eq) index_value target_index)
| cell_ptr' :: path ⇒
assume_some (deref cell_ptr)
(fun (cell_value : cell content_type ptr_type) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell content_type ptr_type) ⇒
mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : ptr_type) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal &&
(valid_path' equal_ptr target_ptr target_cell deref
powers index' cell_ptr' path)))))
end.
We prove equality of retrieved function and piece of original code,
we will use this equality in [rewrite] tactic this in the main proof.
Fixpoint valid_path_eq
`{FArgs} {content_type ptr_type : Set}
(equal_ptr : ptr_type → ptr_type → bool) (target_ptr : ptr_type)
(target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
(path : list ptr_type) :
(fix valid_path
(index_value : int) (cell_ptr0 : ptr_type) (path0 : list ptr_type)
{struct path0} : bool :=
let target_index := Skip_list_repr.Make.index_value target_cell in
match path0 with
| [] ⇒
equal_ptr target_ptr cell_ptr0 &&
(Compare.Int.(Compare.S.op_eq) index_value target_index)
| cell_ptr' :: path1 ⇒
assume_some (deref cell_ptr0)
(fun (cell_value : cell content_type ptr_type) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell content_type ptr_type) ⇒
mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : ptr_type) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal &&
(valid_path index' cell_ptr' path1)))))
end) index_value cell_ptr path =
valid_path' equal_ptr target_ptr
(target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int)
(cell_ptr : ptr_type) (path : list ptr_type).
Proof.
destruct path; simpl; [reflexivity|].
repeat (f_equal; (try apply
FunctionalExtensionality.functional_extensionality; intro);
f_equal);
hauto lq: on.
Qed.
(* In this module we have all the auxiliary functions
for proving back_path'_valid_path'
which is used in main lemma back_path_is_valid. *)
Module Helper_valid.
(* @TODO move to lists library*)
Fact list_rev_In (A : Set) (a : A) (l : list A) :
In a l ↔ In a (rev l).
Proof.
induction l; intuition.
{ hauto q: on use: List.in_app_iff, list_rev_cons. }
{ rewrite list_rev_cons in H1.
hauto q: on use: List.in_app_iff.
}
Qed.
Lemma rev_one {A : Set} : ∀ (a : A), [a] = rev [a].
Proof.
sfirstorder.
Qed.
(* @TODO move to lists library *)
Lemma rev_injective {A : Set} :
∀ (xs ys : list A), rev xs = rev ys → xs = ys.
Proof.
induction xs; destruct ys; try sfirstorder;
intro H; unfold rev in H; unfold rev' in H;
repeat rewrite <- rev_alt in H;
simpl in H; try (symmetry in H; apply app_cons_not_nil in H);
try apply app_cons_not_nil in H; try sfirstorder.
(* inductive case *)
apply app_inj_tail_iff in H;
destruct H; unfold rev in IHxs;
unfold rev' in IHxs;
repeat rewrite rev_alt in H;
apply IHxs in H; sfirstorder.
Qed.
(* @TODO: move to list library *)
Fact nth_valid_result {A : Set}
(l : list A) (idx : int) (res : A) :
nth l idx = Some res →
In res l.
Proof.
revert idx. induction l; hauto lq: on.
Qed.
(* TODO: move to list library *)
Fact nth_success {A : Set}
(l : list A) (idx : int) :
0 ≤ idx < Z.of_nat (Datatypes.length l) →
∃ res : A, nth l idx = Some res.
Proof.
revert idx. induction l; simpl; intuition.
destruct idx; intuition. eauto.
Qed.
(* TODO: move to list library *)
Fact get_valid_result {A : Set}
(a : FallbackArray.t A) (idx : int) :
0 ≤ idx < Z.of_nat (Datatypes.length a.(t.items)) →
In (FallbackArray.get a idx) a.(t.items).
Proof.
destruct a. unfold FallbackArray.get.
hauto q: on use: nth_success, nth_valid_result.
Qed.
Fact normalize_positive_le (i : int) :
0 ≤ i →
normalize_int i ≤ i.
Proof.
intuition.
Qed.
(* TODO: move to list library *)
Fact le_length {A : Set} (l : list A) :
List.length l ≤ Z.of_nat (Datatypes.length l).
Proof.
rewrite List.length_eq. apply normalize_positive_le. intuition.
Qed.
Fact option_cases {A : Type} (oa : M× A) :
oa = None ∨ (∃ a : A, oa = Some a).
Proof.
destruct oa; eauto.
Qed.
Fact to_nat_eq_0_int_le_0 (i : int) :
Z.to_nat i = 0%nat → i ≤ 0.
Proof.
intuition.
Qed.
Fact int_cyclic (i : int) :
normalize_int (i + two_pow_63) = normalize_int i.
Proof.
unfold normalize_int. f_equal. rewrite <- Z.add_assoc.
rewrite Z.add_comm with two_pow_63 two_pow_62. rewrite Z.add_assoc.
rewrite <- Z.mul_1_l with two_pow_63. apply Z_mod_plus_full.
Qed.
Lemma neg_lt_ind:
∀ A : BinNums.Z → Prop,
Proper (Logic.eq ==> iff) A →
∀ n : BinNums.Z,
A (BinInt.Z.pred n) →
(∀ m : BinNums.Z, m < n → A m → A (BinInt.Z.pred m)) →
∀ m : BinNums.Z, m < n → A m.
Proof.
intros.
pose (A' := (fun k' ⇒ A (- k'))).
assert (∀ k, A k ↔ A' (- k))
by (unfold A'; intros; now rewrite Z.opp_involutive).
apply H3.
apply Z.lt_ind with (A := A') (n := - n); intuition; unfold A'.
{ now rewrite <- Z.opp_pred, Z.opp_involutive. }
{ rewrite Z.opp_succ. intuition. }
Qed.
Lemma neg_le_ind:
∀ A : BinNums.Z → Prop,
Proper (Logic.eq ==> iff) A →
∀ n : BinNums.Z,
A n →
(∀ m : BinNums.Z, m ≤ n → A m → A (BinInt.Z.pred m)) →
∀ m : BinNums.Z, m ≤ n → A m.
Proof.
intros.
apply neg_lt_ind with (n := BinInt.Z.succ n); intuition.
now rewrite Z.pred_succ.
Qed.
`{FArgs} {content_type ptr_type : Set}
(equal_ptr : ptr_type → ptr_type → bool) (target_ptr : ptr_type)
(target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
(path : list ptr_type) :
(fix valid_path
(index_value : int) (cell_ptr0 : ptr_type) (path0 : list ptr_type)
{struct path0} : bool :=
let target_index := Skip_list_repr.Make.index_value target_cell in
match path0 with
| [] ⇒
equal_ptr target_ptr cell_ptr0 &&
(Compare.Int.(Compare.S.op_eq) index_value target_index)
| cell_ptr' :: path1 ⇒
assume_some (deref cell_ptr0)
(fun (cell_value : cell content_type ptr_type) ⇒
assume_some (deref cell_ptr')
(fun (cell' : cell content_type ptr_type) ⇒
mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
assume_some (best_skip cell_value target_index powers)
(fun (best_idx : int) ⇒
assume_some (back_pointer cell_value best_idx)
(fun (best_ptr : ptr_type) ⇒
let minimal := equal_ptr best_ptr cell_ptr' in
let index' := cell'.(cell.index) in
minimal &&
(valid_path index' cell_ptr' path1)))))
end) index_value cell_ptr path =
valid_path' equal_ptr target_ptr
(target_cell : cell content_type ptr_type)
(deref : ptr_type → option (cell content_type ptr_type))
(powers : FallbackArray.t int) (index_value : int)
(cell_ptr : ptr_type) (path : list ptr_type).
Proof.
destruct path; simpl; [reflexivity|].
repeat (f_equal; (try apply
FunctionalExtensionality.functional_extensionality; intro);
f_equal);
hauto lq: on.
Qed.
(* In this module we have all the auxiliary functions
for proving back_path'_valid_path'
which is used in main lemma back_path_is_valid. *)
Module Helper_valid.
(* @TODO move to lists library*)
Fact list_rev_In (A : Set) (a : A) (l : list A) :
In a l ↔ In a (rev l).
Proof.
induction l; intuition.
{ hauto q: on use: List.in_app_iff, list_rev_cons. }
{ rewrite list_rev_cons in H1.
hauto q: on use: List.in_app_iff.
}
Qed.
Lemma rev_one {A : Set} : ∀ (a : A), [a] = rev [a].
Proof.
sfirstorder.
Qed.
(* @TODO move to lists library *)
Lemma rev_injective {A : Set} :
∀ (xs ys : list A), rev xs = rev ys → xs = ys.
Proof.
induction xs; destruct ys; try sfirstorder;
intro H; unfold rev in H; unfold rev' in H;
repeat rewrite <- rev_alt in H;
simpl in H; try (symmetry in H; apply app_cons_not_nil in H);
try apply app_cons_not_nil in H; try sfirstorder.
(* inductive case *)
apply app_inj_tail_iff in H;
destruct H; unfold rev in IHxs;
unfold rev' in IHxs;
repeat rewrite rev_alt in H;
apply IHxs in H; sfirstorder.
Qed.
(* @TODO: move to list library *)
Fact nth_valid_result {A : Set}
(l : list A) (idx : int) (res : A) :
nth l idx = Some res →
In res l.
Proof.
revert idx. induction l; hauto lq: on.
Qed.
(* TODO: move to list library *)
Fact nth_success {A : Set}
(l : list A) (idx : int) :
0 ≤ idx < Z.of_nat (Datatypes.length l) →
∃ res : A, nth l idx = Some res.
Proof.
revert idx. induction l; simpl; intuition.
destruct idx; intuition. eauto.
Qed.
(* TODO: move to list library *)
Fact get_valid_result {A : Set}
(a : FallbackArray.t A) (idx : int) :
0 ≤ idx < Z.of_nat (Datatypes.length a.(t.items)) →
In (FallbackArray.get a idx) a.(t.items).
Proof.
destruct a. unfold FallbackArray.get.
hauto q: on use: nth_success, nth_valid_result.
Qed.
Fact normalize_positive_le (i : int) :
0 ≤ i →
normalize_int i ≤ i.
Proof.
intuition.
Qed.
(* TODO: move to list library *)
Fact le_length {A : Set} (l : list A) :
List.length l ≤ Z.of_nat (Datatypes.length l).
Proof.
rewrite List.length_eq. apply normalize_positive_le. intuition.
Qed.
Fact option_cases {A : Type} (oa : M× A) :
oa = None ∨ (∃ a : A, oa = Some a).
Proof.
destruct oa; eauto.
Qed.
Fact to_nat_eq_0_int_le_0 (i : int) :
Z.to_nat i = 0%nat → i ≤ 0.
Proof.
intuition.
Qed.
Fact int_cyclic (i : int) :
normalize_int (i + two_pow_63) = normalize_int i.
Proof.
unfold normalize_int. f_equal. rewrite <- Z.add_assoc.
rewrite Z.add_comm with two_pow_63 two_pow_62. rewrite Z.add_assoc.
rewrite <- Z.mul_1_l with two_pow_63. apply Z_mod_plus_full.
Qed.
Lemma neg_lt_ind:
∀ A : BinNums.Z → Prop,
Proper (Logic.eq ==> iff) A →
∀ n : BinNums.Z,
A (BinInt.Z.pred n) →
(∀ m : BinNums.Z, m < n → A m → A (BinInt.Z.pred m)) →
∀ m : BinNums.Z, m < n → A m.
Proof.
intros.
pose (A' := (fun k' ⇒ A (- k'))).
assert (∀ k, A k ↔ A' (- k))
by (unfold A'; intros; now rewrite Z.opp_involutive).
apply H3.
apply Z.lt_ind with (A := A') (n := - n); intuition; unfold A'.
{ now rewrite <- Z.opp_pred, Z.opp_involutive. }
{ rewrite Z.opp_succ. intuition. }
Qed.
Lemma neg_le_ind:
∀ A : BinNums.Z → Prop,
Proper (Logic.eq ==> iff) A →
∀ n : BinNums.Z,
A n →
(∀ m : BinNums.Z, m ≤ n → A m → A (BinInt.Z.pred m)) →
∀ m : BinNums.Z, m ≤ n → A m.
Proof.
intros.
apply neg_lt_ind with (n := BinInt.Z.succ n); intuition.
now rewrite Z.pred_succ.
Qed.
Inner [mem] equipped with fuel and decomposed
Fixpoint mem'_aux `{FArgs} {A B : Set} (idx : int)
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat) {struct fuel}:
bool :=
let n_value := FallbackArray.length l_value in
match fuel with
| Datatypes.O ⇒ false
| Datatypes.S fuel ⇒
if Compare.Int.(Compare.S.op_gteq) idx n_value then
false
else
match FallbackArray.get l_value idx with
| None ⇒ mem'_aux (idx +i 1) equal x_value l_value fuel
| Some y_value ⇒
if equal x_value y_value then
true
else
mem'_aux (idx +i 1) equal x_value l_value fuel
end
end.
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat) {struct fuel}:
bool :=
let n_value := FallbackArray.length l_value in
match fuel with
| Datatypes.O ⇒ false
| Datatypes.S fuel ⇒
if Compare.Int.(Compare.S.op_gteq) idx n_value then
false
else
match FallbackArray.get l_value idx with
| None ⇒ mem'_aux (idx +i 1) equal x_value l_value fuel
| Some y_value ⇒
if equal x_value y_value then
true
else
mem'_aux (idx +i 1) equal x_value l_value fuel
end
end.
Simulation of [mem] function
Definition mem' `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat) : bool :=
mem'_aux 0 equal x_value l_value fuel.
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat) : bool :=
mem'_aux 0 equal x_value l_value fuel.
We axiomatize equality of mem function and it's simulation
Axiom mem_eq : ∀ `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat),
let n_value := FallbackArray.length l_value in
((Z.to_nat n_value) ≤ fuel)%nat →
mem equal x_value l_value =
mem' equal x_value l_value fuel.
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(fuel : Datatypes.nat),
let n_value := FallbackArray.length l_value in
((Z.to_nat n_value) ≤ fuel)%nat →
mem equal x_value l_value =
mem' equal x_value l_value fuel.
Inductive predicate for easier case-analysis reasoning
Inductive mem_aux_Prop `{FArgs} {A B : Set} (idx : int)
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) : Prop :=
| maP_None :
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = None →
mem_aux_Prop (idx +i 1) equal x_value l_value →
mem_aux_Prop idx equal x_value l_value
| maP_Some_eq :
∀ (y_value : B),
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = Some y_value →
equal x_value y_value = true →
mem_aux_Prop idx equal x_value l_value
| maP_Some_neq :
∀ (y_value : B),
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = Some y_value →
equal x_value y_value = false →
mem_aux_Prop (idx +i 1) equal x_value l_value →
mem_aux_Prop idx equal x_value l_value.
(* if the length of an array does not exceed the upper bound of int,
then FallbackArray.length gives the real length in result *)
(* this fact is important for the following lemmas *)
Fact length_of_list_length (A : Set) (l : FallbackArray.t A) :
Z.of_nat (Datatypes.length l.(t.items)) ≤ Pervasives.max_int →
FallbackArray.length l = Z.of_nat (Datatypes.length l.(t.items)).
Proof.
destruct l. cbn. destruct items; trivial. simpl.
induction items; trivial. simpl. rewrite Pos2Z.inj_succ. intros.
rewrite IHitems; intuition.
unfold "+i". rewrite Z.add_1_r. apply Pervasives.normalize_identity.
intuition.
Qed.
(* if the length of an array is less then the upper bound of int,
then the result of FallbackArray.length is also less then that *)
(* this fact is obvious but also important for the following lemmas *)
Fact stronger_length_limit (A : Set) (l : FallbackArray.t A) :
Z.of_nat (Datatypes.length l.(t.items)) < Pervasives.max_int →
FallbackArray.length l < Pervasives.max_int.
Proof.
intros. rewrite length_of_list_length; intuition.
Qed.
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) : Prop :=
| maP_None :
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = None →
mem_aux_Prop (idx +i 1) equal x_value l_value →
mem_aux_Prop idx equal x_value l_value
| maP_Some_eq :
∀ (y_value : B),
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = Some y_value →
equal x_value y_value = true →
mem_aux_Prop idx equal x_value l_value
| maP_Some_neq :
∀ (y_value : B),
idx >=? FallbackArray.length l_value = false →
FallbackArray.get l_value idx = Some y_value →
equal x_value y_value = false →
mem_aux_Prop (idx +i 1) equal x_value l_value →
mem_aux_Prop idx equal x_value l_value.
(* if the length of an array does not exceed the upper bound of int,
then FallbackArray.length gives the real length in result *)
(* this fact is important for the following lemmas *)
Fact length_of_list_length (A : Set) (l : FallbackArray.t A) :
Z.of_nat (Datatypes.length l.(t.items)) ≤ Pervasives.max_int →
FallbackArray.length l = Z.of_nat (Datatypes.length l.(t.items)).
Proof.
destruct l. cbn. destruct items; trivial. simpl.
induction items; trivial. simpl. rewrite Pos2Z.inj_succ. intros.
rewrite IHitems; intuition.
unfold "+i". rewrite Z.add_1_r. apply Pervasives.normalize_identity.
intuition.
Qed.
(* if the length of an array is less then the upper bound of int,
then the result of FallbackArray.length is also less then that *)
(* this fact is obvious but also important for the following lemmas *)
Fact stronger_length_limit (A : Set) (l : FallbackArray.t A) :
Z.of_nat (Datatypes.length l.(t.items)) < Pervasives.max_int →
FallbackArray.length l < Pervasives.max_int.
Proof.
intros. rewrite length_of_list_length; intuition.
Qed.
If inductive predicate exists then result of work of function
[mem] can not be equal to false
Lemma mem_aux_of_Prop `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(idx : int) (fuel : Datatypes.nat) :
Pervasives.Int.Valid.t idx →
let n_value := FallbackArray.length l_value in
(Z.to_nat (n_value - idx) ≤ fuel)%nat →
mem_aux_Prop idx equal x_value l_value →
mem'_aux idx equal x_value l_value fuel = true.
Proof.
intros idx_valid ? le_fuel HmaP.
revert le_fuel. revert fuel.
induction HmaP; (destruct fuel; simpl; intro le_fuel; [intuition |]);
[ rewrite H0, H1 | now rewrite H0, H1, H2 | rewrite H0, H1, H2 ].
all: apply IHHmaP; [ intuition |]; unfold "+i";
rewrite Pervasives.normalize_identity;
[ fold n_value;
rewrite Z.sub_add_distr, Z2Nat.inj_sub; [| intuition ];
destruct Z.to_nat; intuition
| rewrite Z.geb_leb in H0; apply Z.leb_gt in H0;
unfold FallbackArray.length in *;
pose (Compare.length_is_valid l_value.(t.items)); intuition
].
Qed.
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B))
(idx : int) (fuel : Datatypes.nat) :
Pervasives.Int.Valid.t idx →
let n_value := FallbackArray.length l_value in
(Z.to_nat (n_value - idx) ≤ fuel)%nat →
mem_aux_Prop idx equal x_value l_value →
mem'_aux idx equal x_value l_value fuel = true.
Proof.
intros idx_valid ? le_fuel HmaP.
revert le_fuel. revert fuel.
induction HmaP; (destruct fuel; simpl; intro le_fuel; [intuition |]);
[ rewrite H0, H1 | now rewrite H0, H1, H2 | rewrite H0, H1, H2 ].
all: apply IHHmaP; [ intuition |]; unfold "+i";
rewrite Pervasives.normalize_identity;
[ fold n_value;
rewrite Z.sub_add_distr, Z2Nat.inj_sub; [| intuition ];
destruct Z.to_nat; intuition
| rewrite Z.geb_leb in H0; apply Z.leb_gt in H0;
unfold FallbackArray.length in *;
pose (Compare.length_is_valid l_value.(t.items)); intuition
].
Qed.
Opposite statement : if auxiliary function returned true
then predicate holds and exists (inhabited)
Lemma mem_aux_Prop_of_mem'_aux `{FArgs} {A B : Set}
(idx : int) (equal : A → B → bool) (x : A) (l : FallbackArray.t (M× B))
(fuel : Datatypes.nat) :
mem'_aux idx equal x l fuel = true →
mem_aux_Prop idx equal x l.
Proof.
revert idx. induction fuel; try discriminate.
simpl. intro.
destruct (idx >=? FallbackArray.length l) eqn:idxGT; try discriminate.
destruct FallbackArray.get eqn:GET; intros;
[ destruct equal eqn:EQUAL | ].
{ apply maP_Some_eq with b; trivial. }
{ apply maP_Some_neq with b; intuition. }
{ apply maP_None; intuition. }
Qed.
Lemma mem_aux_Prop_exists `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) (idx : int) (ptr : B) :
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
equal x_value ptr = true →
0 ≤ idx < FallbackArray.length l_value →
mem_aux_Prop idx equal x_value l_value.
Proof.
intros. apply maP_Some_eq with ptr; intuition. cbn. rewrite Z.geb_leb.
now apply Z.leb_gt.
Qed.
Lemma get_for_valid_idx {A : Set}
(idx : int) (l_value : FallbackArray.t (option A)) (ptr : A) :
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
0 ≤ idx < Z.of_nat (Datatypes.length l_value.(t.items)).
Proof.
destruct l_value. cbn. unfold FallbackArray.get. simpl. intros.
assert (nth items idx = Some (Some ptr)) by hauto lq: on.
rewrite H1 in H0. intuition; revert idx H1; induction items;
try discriminate; [ hfcrush |].
cbn in ×. rewrite Zpos_P_of_succ_nat. destruct idx; intuition.
apply IHitems in H1. intuition.
Qed.
(idx : int) (equal : A → B → bool) (x : A) (l : FallbackArray.t (M× B))
(fuel : Datatypes.nat) :
mem'_aux idx equal x l fuel = true →
mem_aux_Prop idx equal x l.
Proof.
revert idx. induction fuel; try discriminate.
simpl. intro.
destruct (idx >=? FallbackArray.length l) eqn:idxGT; try discriminate.
destruct FallbackArray.get eqn:GET; intros;
[ destruct equal eqn:EQUAL | ].
{ apply maP_Some_eq with b; trivial. }
{ apply maP_Some_neq with b; intuition. }
{ apply maP_None; intuition. }
Qed.
Lemma mem_aux_Prop_exists `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A)
(l_value : FallbackArray.t (option B)) (idx : int) (ptr : B) :
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
equal x_value ptr = true →
0 ≤ idx < FallbackArray.length l_value →
mem_aux_Prop idx equal x_value l_value.
Proof.
intros. apply maP_Some_eq with ptr; intuition. cbn. rewrite Z.geb_leb.
now apply Z.leb_gt.
Qed.
Lemma get_for_valid_idx {A : Set}
(idx : int) (l_value : FallbackArray.t (option A)) (ptr : A) :
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
0 ≤ idx < Z.of_nat (Datatypes.length l_value.(t.items)).
Proof.
destruct l_value. cbn. unfold FallbackArray.get. simpl. intros.
assert (nth items idx = Some (Some ptr)) by hauto lq: on.
rewrite H1 in H0. intuition; revert idx H1; induction items;
try discriminate; [ hfcrush |].
cbn in ×. rewrite Zpos_P_of_succ_nat. destruct idx; intuition.
apply IHitems in H1. intuition.
Qed.
We need appropriate level of generalization in order to be able
to use our predicate in the proofs
Lemma mem_aux_Prop_exists_general `{FArgs} {A B : Set}
(equal : A → B → bool) (x_value : A) (ptr : B)
(l_value : FallbackArray.t (option B)) (idx : int) (idx' : int) :
idx < FallbackArray.length l_value →
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
equal x_value ptr = true →
0 ≤ idx' ≤ idx →
mem_aux_Prop idx' equal x_value l_value.
Proof.
intros. pose (Compare.length_is_valid l_value.(t.items)).
apply mem_aux_Prop_exists with equal x_value l_value idx ptr in H1;
trivial; try lia.
destruct H4. revert H4.
apply neg_le_ind with (m := idx') (n := idx); intuition.
rewrite <- Z.sub_1_r.
destruct (FallbackArray.get l_value (m - 1)) eqn:getValue;
[ destruct (equal x_value b) eqn:equalValue;
[ apply maP_Some_eq with b | apply maP_Some_neq with b ]
| apply maP_None ]; trivial; try lia.
all: unfold FallbackArray.length, "+i" in *;
rewrite Pervasives.normalize_identity; rewrite Z.sub_add;
intuition.
Qed.
(equal : A → B → bool) (x_value : A) (ptr : B)
(l_value : FallbackArray.t (option B)) (idx : int) (idx' : int) :
idx < FallbackArray.length l_value →
l_value.(t.default) = None →
FallbackArray.get l_value idx = Some ptr →
equal x_value ptr = true →
0 ≤ idx' ≤ idx →
mem_aux_Prop idx' equal x_value l_value.
Proof.
intros. pose (Compare.length_is_valid l_value.(t.items)).
apply mem_aux_Prop_exists with equal x_value l_value idx ptr in H1;
trivial; try lia.
destruct H4. revert H4.
apply neg_le_ind with (m := idx') (n := idx); intuition.
rewrite <- Z.sub_1_r.
destruct (FallbackArray.get l_value (m - 1)) eqn:getValue;
[ destruct (equal x_value b) eqn:equalValue;
[ apply maP_Some_eq with b | apply maP_Some_neq with b ]
| apply maP_None ]; trivial; try lia.
all: unfold FallbackArray.length, "+i" in *;
rewrite Pervasives.normalize_identity; rewrite Z.sub_add;
intuition.
Qed.
[binary_search] function for [best_skip] retrieved
Fixpoint binary_search `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (start_idx : int) (end_idx : int)
(fuel : Datatypes.nat) {struct fuel} : option int :=
let pointed_cell_index (i_value : int) : int :=
(cell_value.(cell.index) -i
(Pervasives._mod cell_value.(cell.index)
(FallbackArray.get powers i_value))) -i 1 in
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
if Compare.Int.(Compare.S.op_gteq) start_idx end_idx then
Some start_idx
else
let mid_idx := start_idx +i ((end_idx -i start_idx) /i 2) in
let mid_cell_index := pointed_cell_index mid_idx in
if Compare.Int.(Compare.S.op_eq) mid_cell_index target_index then
Some mid_idx
else
if Compare.Int.(Compare.S.op_lt) mid_cell_index target_index then
binary_search
cell_value target_index powers start_idx (mid_idx -i 1) fuel
else
let prev_mid_cell_index := pointed_cell_index (mid_idx +i 1) in
if Compare.Int.(Compare.S.op_eq)
prev_mid_cell_index target_index
then
Some (mid_idx +i 1)
else
if Compare.Int.(Compare.S.op_lt)
prev_mid_cell_index target_index
then
Some mid_idx
else
binary_search
cell_value target_index powers (mid_idx +i 1) end_idx fuel
end.
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (start_idx : int) (end_idx : int)
(fuel : Datatypes.nat) {struct fuel} : option int :=
let pointed_cell_index (i_value : int) : int :=
(cell_value.(cell.index) -i
(Pervasives._mod cell_value.(cell.index)
(FallbackArray.get powers i_value))) -i 1 in
match fuel with
| Datatypes.O ⇒ None
| Datatypes.S fuel ⇒
if Compare.Int.(Compare.S.op_gteq) start_idx end_idx then
Some start_idx
else
let mid_idx := start_idx +i ((end_idx -i start_idx) /i 2) in
let mid_cell_index := pointed_cell_index mid_idx in
if Compare.Int.(Compare.S.op_eq) mid_cell_index target_index then
Some mid_idx
else
if Compare.Int.(Compare.S.op_lt) mid_cell_index target_index then
binary_search
cell_value target_index powers start_idx (mid_idx -i 1) fuel
else
let prev_mid_cell_index := pointed_cell_index (mid_idx +i 1) in
if Compare.Int.(Compare.S.op_eq)
prev_mid_cell_index target_index
then
Some (mid_idx +i 1)
else
if Compare.Int.(Compare.S.op_lt)
prev_mid_cell_index target_index
then
Some mid_idx
else
binary_search
cell_value target_index powers (mid_idx +i 1) end_idx fuel
end.
Simulation of [best_skip]
Definition best_skip' `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) :
option int :=
binary_search cell_value target_index powers 0
((FallbackArray.length cell_value.(cell.back_pointers)) -i 1) fuel.
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) :
option int :=
binary_search cell_value target_index powers 0
((FallbackArray.length cell_value.(cell.back_pointers)) -i 1) fuel.
Equality of initial function and simulation
Axiom best_skip'_eq : ∀ `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat),
(Z.to_nat (FallbackArray.length cell_value.(cell.back_pointers))
≤ fuel)%nat →
best_skip cell_value target_index powers =
best_skip' cell_value target_index powers fuel.
(* here the real lower bound for fuel
is the logarithm of FallbackArray.length,
but it makes no harm
since it would always be less then the current limit *)
(cell_value : cell A B) (target_index : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat),
(Z.to_nat (FallbackArray.length cell_value.(cell.back_pointers))
≤ fuel)%nat →
best_skip cell_value target_index powers =
best_skip' cell_value target_index powers fuel.
(* here the real lower bound for fuel
is the logarithm of FallbackArray.length,
but it makes no harm
since it would always be less then the current limit *)
Values between valid integers are also valid
Fact between_valid (i j k : int) :
i ≤ k ≤ j →
Pervasives.Int.Valid.t i →
Pervasives.Int.Valid.t j →
Pervasives.Int.Valid.t k.
Proof.
intuition.
Qed.
i ≤ k ≤ j →
Pervasives.Int.Valid.t i →
Pervasives.Int.Valid.t j →
Pervasives.Int.Valid.t k.
Proof.
intuition.
Qed.
Validity of result of work of [best_skip'_aux] function
Lemma binary_search_result_valid `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index start_idx end_idx res : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) :
Pervasives.Int.Valid.t start_idx →
Pervasives.Int.Valid.t end_idx →
binary_search cell_value target_index powers start_idx end_idx fuel
= Some res →
Pervasives.Int.Valid.t res.
Proof.
revert cell_value target_index powers start_idx end_idx res.
induction fuel; try discriminate. cbn. intros ? ? ? ? ? ? Hstart Hend.
step; [ congruence |].
step.
{ intro eq_res. inversion eq_res. clear. intuition. }
{ step; [ apply IHfuel; hauto l: on use: Pervasives.int_add_valid |].
step; [| step ].
1-2: (intro eq_res; inversion eq_res; clear; intuition).
apply IHfuel; hauto l: on use: Pervasives.int_add_valid.
}
Qed.
(cell_value : cell A B) (target_index start_idx end_idx res : int)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) :
Pervasives.Int.Valid.t start_idx →
Pervasives.Int.Valid.t end_idx →
binary_search cell_value target_index powers start_idx end_idx fuel
= Some res →
Pervasives.Int.Valid.t res.
Proof.
revert cell_value target_index powers start_idx end_idx res.
induction fuel; try discriminate. cbn. intros ? ? ? ? ? ? Hstart Hend.
step; [ congruence |].
step.
{ intro eq_res. inversion eq_res. clear. intuition. }
{ step; [ apply IHfuel; hauto l: on use: Pervasives.int_add_valid |].
step; [| step ].
1-2: (intro eq_res; inversion eq_res; clear; intuition).
apply IHfuel; hauto l: on use: Pervasives.int_add_valid.
}
Qed.
Validity of result of work of [best_skip'_aux] function
Lemma best_skip_result_valid `{FArgs} {A B : Set}
(cell_value : cell A B) (target_index res : int)
(powers : FallbackArray.t int) :
best_skip cell_value target_index powers = Some res →
Pervasives.Int.Valid.t res.
Proof.
erewrite best_skip'_eq; trivial. unfold best_skip'.
apply binary_search_result_valid; intuition.
Qed.
(cell_value : cell A B) (target_index res : int)
(powers : FallbackArray.t int) :
best_skip cell_value target_index powers = Some res →
Pervasives.Int.Valid.t res.
Proof.
erewrite best_skip'_eq; trivial. unfold best_skip'.
apply binary_search_result_valid; intuition.
Qed.
Validity of the index of a cell - our interpretation of how
dereferencing operator should work
Module Cell_Index.
Module Valid.
Definition t `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
: Prop :=
∀ (cell_1_ptr cell_2_ptr : ptr_type)
(cell1 cell2 : cell content_type ptr_type),
deref cell_1_ptr = Some cell1 →
deref cell_2_ptr = Some cell2 →
cell1.(cell.index) =i cell2.(cell.index) = true →
cell_1_ptr = cell_2_ptr.
End Valid.
End Cell_Index.
Section Helper_section.
Context `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type)).
Module Valid.
Definition t `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type))
: Prop :=
∀ (cell_1_ptr cell_2_ptr : ptr_type)
(cell1 cell2 : cell content_type ptr_type),
deref cell_1_ptr = Some cell1 →
deref cell_2_ptr = Some cell2 →
cell1.(cell.index) =i cell2.(cell.index) = true →
cell_1_ptr = cell_2_ptr.
End Valid.
End Cell_Index.
Section Helper_section.
Context `{FArgs} {content_type ptr_type : Set}
(deref : ptr_type → option (cell content_type ptr_type)).
If indexes of two cells are equal, then pointers to the cells equal too,
so this is one and the same cell,
because index of each cell in the structure is unique.
Hypothesis index_ptr_eq : Cell_Index.Valid.t deref.
Lemma ptr_index_eq
(cell_1_ptr cell_2_ptr : ptr_type)
(cell1 cell2 : cell content_type ptr_type) :
deref cell_1_ptr = Some cell1 →
deref cell_2_ptr = Some cell2 →
cell_1_ptr = cell_2_ptr →
cell1.(cell.index) =i cell2.(cell.index) = true.
Proof.
intros deref1 deref2 cell_eq.
rewrite cell_eq in deref1.
rewrite deref1 in deref2.
hauto lq: on use: Z.eqb_refl.
Qed.
Lemma ptr_index_eq
(cell_1_ptr cell_2_ptr : ptr_type)
(cell1 cell2 : cell content_type ptr_type) :
deref cell_1_ptr = Some cell1 →
deref cell_2_ptr = Some cell2 →
cell_1_ptr = cell_2_ptr →
cell1.(cell.index) =i cell2.(cell.index) = true.
Proof.
intros deref1 deref2 cell_eq.
rewrite cell_eq in deref1.
rewrite deref1 in deref2.
hauto lq: on use: Z.eqb_refl.
Qed.
Path can not consist out of just one pointer.
it should have more elements, so assumption is False
Fixpoint aux'_contra
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) target_index
(powers : FallbackArray.t int) (acc : list ptr_type) fuel p
{struct fuel} :
acc ≠ nil →
aux' deref powers target_index acc p
(deref p) fuel = Some [cell_ptr] → False.
Proof. intro not_nil_acc.
destruct fuel; try scongruence.
unfold aux'. destruct (deref p); try scongruence; simpl.
step.
{ intro H0. injection H0 as H0. rewrite rev_one in H0.
apply rev_injective in H0. hauto l: on. }
{ step; try scongruence.
destruct best_skip eqn:G; try scongruence; simpl.
destruct back_pointer eqn:BP; try scongruence; simpl.
apply aux'_contra.
{ hauto l: on. }
{ scongruence. }
{ scongruence. }
{ pose proof (nil_cons). hauto l: on. } }
Qed.
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) target_index
(powers : FallbackArray.t int) (acc : list ptr_type) fuel p
{struct fuel} :
acc ≠ nil →
aux' deref powers target_index acc p
(deref p) fuel = Some [cell_ptr] → False.
Proof. intro not_nil_acc.
destruct fuel; try scongruence.
unfold aux'. destruct (deref p); try scongruence; simpl.
step.
{ intro H0. injection H0 as H0. rewrite rev_one in H0.
apply rev_injective in H0. hauto l: on. }
{ step; try scongruence.
destruct best_skip eqn:G; try scongruence; simpl.
destruct back_pointer eqn:BP; try scongruence; simpl.
apply aux'_contra.
{ hauto l: on. }
{ scongruence. }
{ scongruence. }
{ pose proof (nil_cons). hauto l: on. } }
Qed.
If we have just one pointer in the path,
this pointer points to the target_ cell
Lemma one_cell_valid (equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type) target_cell p x :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
equal_ptr p cell_ptr = true →
let target_index := index_value target_cell in
back_path' deref cell_ptr target_index = Some [p] →
(equal_ptr target_ptr cell_ptr
&& (index_value x =i index_value target_cell))%bool = true.
Proof. intros.
unfold Compare.Equal.Valid.t in H0.
apply H0 in H3. 2, 3 : apply I. subst.
match goal with
| |- (?x && _)%bool = true ⇒ assert (G : x = true)
end.
{ revert H4. unfold back_path'. rewrite H2. simpl.
destruct bp_compute_fuel; [sfirstorder|].
simpl. step.
{ intros. clear H4. apply H0; try apply I.
apply (index_ptr_eq
target_ptr cell_ptr target_cell x H1 H2 Heqb). }
{ intros. apply H0; try apply I.
revert H4.
step; try scongruence.
destruct best_skip eqn:Best; try scongruence; simpl.
destruct back_pointer eqn:N; try scongruence; simpl.
match goal with
| |- aux' _ _ _ ?acc _ _ _ = _ → _ ⇒
intros; assert (G : acc ≠ nil) by hfcrush
end.
revert H4. unfold target_index.
match goal with
| |- context[aux' _ ?pow (?iv ?tc) ?acc ?p' _ ?n'] ⇒
match goal with
| |- _ → ?tp = ?cp ⇒
pose proof (aux'_contra equal_ptr cp tp tc (iv tc)
pow acc n' p') G
end
end.
hauto q: on.
}
}
match goal with
| |- (_ && ?x)%bool = true ⇒ assert (G2 : x = true)
end.
{ revert H4. unfold back_path'. apply H0 in G; trivial.
intro aux. eapply ptr_index_eq.
{ apply H2. }
{ apply H1. }
{ scongruence. }
}
hauto lq: on.
Qed.
(cell_ptr target_ptr : ptr_type) target_cell p x :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
equal_ptr p cell_ptr = true →
let target_index := index_value target_cell in
back_path' deref cell_ptr target_index = Some [p] →
(equal_ptr target_ptr cell_ptr
&& (index_value x =i index_value target_cell))%bool = true.
Proof. intros.
unfold Compare.Equal.Valid.t in H0.
apply H0 in H3. 2, 3 : apply I. subst.
match goal with
| |- (?x && _)%bool = true ⇒ assert (G : x = true)
end.
{ revert H4. unfold back_path'. rewrite H2. simpl.
destruct bp_compute_fuel; [sfirstorder|].
simpl. step.
{ intros. clear H4. apply H0; try apply I.
apply (index_ptr_eq
target_ptr cell_ptr target_cell x H1 H2 Heqb). }
{ intros. apply H0; try apply I.
revert H4.
step; try scongruence.
destruct best_skip eqn:Best; try scongruence; simpl.
destruct back_pointer eqn:N; try scongruence; simpl.
match goal with
| |- aux' _ _ _ ?acc _ _ _ = _ → _ ⇒
intros; assert (G : acc ≠ nil) by hfcrush
end.
revert H4. unfold target_index.
match goal with
| |- context[aux' _ ?pow (?iv ?tc) ?acc ?p' _ ?n'] ⇒
match goal with
| |- _ → ?tp = ?cp ⇒
pose proof (aux'_contra equal_ptr cp tp tc (iv tc)
pow acc n' p') G
end
end.
hauto q: on.
}
}
match goal with
| |- (_ && ?x)%bool = true ⇒ assert (G2 : x = true)
end.
{ revert H4. unfold back_path'. apply H0 in G; trivial.
intro aux. eapply ptr_index_eq.
{ apply H2. }
{ apply H1. }
{ scongruence. }
}
hauto lq: on.
Qed.
If path was generated by [back_path'] - all elements are (Some ..)
generalized version
Lemma all_elements_not_none_general
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
path init_path :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr = Some path →
(∀ p, In p init_path → deref p = None → False) →
In p_any path →
deref p_any = None → False.
Proof.
intros.
revert H0 H1.
revert init_path cell_ptr.
induction fuel; [ discriminate |].
intros ? ?.
simpl in ×.
destruct (deref cell_ptr) eqn:DC; [| discriminate ].
simpl in ×. step.
{ qauto l: on use: list_rev_cons, list_rev_In, List.in_app_iff. }
{ step; try discriminate.
destruct best_skip; [| discriminate ]. simpl in ×.
destruct back_pointer; [| discriminate ].
hauto q: on.
}
Qed.
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
path init_path :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr = Some path →
(∀ p, In p init_path → deref p = None → False) →
In p_any path →
deref p_any = None → False.
Proof.
intros.
revert H0 H1.
revert init_path cell_ptr.
induction fuel; [ discriminate |].
intros ? ?.
simpl in ×.
destruct (deref cell_ptr) eqn:DC; [| discriminate ].
simpl in ×. step.
{ qauto l: on use: list_rev_cons, list_rev_In, List.in_app_iff. }
{ step; try discriminate.
destruct best_skip; [| discriminate ]. simpl in ×.
destruct back_pointer; [| discriminate ].
hauto q: on.
}
Qed.
If path was generated by [back_path'] - all elements are (Some ..)
Lemma all_elements_not_none
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
(path : list ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index nil cell_ptr = Some path →
In p_any path →
deref p_any = None → False.
Proof.
hauto l: on use: all_elements_not_none_general.
Qed.
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
(path : list ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index nil cell_ptr = Some path →
In p_any path →
deref p_any = None → False.
Proof.
hauto l: on use: all_elements_not_none_general.
Qed.
Generalized version of headers equality
Lemma aux'_head_equal_general
(cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
(target_index : int) (powers : FallbackArray.t int)
(equal_ptr : ptr_type → ptr_type → bool) (p : ptr_type)
(l acc : list ptr_type) (fuel : nat) :
Compare.Equal.Valid.t (fun _ : ptr_type ⇒ True) equal_ptr →
aux' deref powers target_index acc cell_ptr cell fuel =
Some (rev acc ++ p :: l)%list →
p = cell_ptr.
Proof.
intro Hequal.
match goal with
| |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ → _ ⇒
pose proof (Ha'ns := aux'_nonempty_success der pow cp acc ti cell fuel)
end.
intro Haux.
destruct Ha'ns; eauto. rewrite Haux in H0.
hauto lq: on use: List.app_inv_head.
Qed.
(cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
(target_index : int) (powers : FallbackArray.t int)
(equal_ptr : ptr_type → ptr_type → bool) (p : ptr_type)
(l acc : list ptr_type) (fuel : nat) :
Compare.Equal.Valid.t (fun _ : ptr_type ⇒ True) equal_ptr →
aux' deref powers target_index acc cell_ptr cell fuel =
Some (rev acc ++ p :: l)%list →
p = cell_ptr.
Proof.
intro Hequal.
match goal with
| |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ → _ ⇒
pose proof (Ha'ns := aux'_nonempty_success der pow cp acc ti cell fuel)
end.
intro Haux.
destruct Ha'ns; eauto. rewrite Haux in H0.
hauto lq: on use: List.app_inv_head.
Qed.
Generalized version of headers equality. Boolean
Lemma aux'_head_true_general
(cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
(target_index : int) (powers : FallbackArray.t int)
(equal_ptr : ptr_type → ptr_type → bool) (p : ptr_type)
(l acc : list ptr_type) (fuel : Datatypes.nat) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux' deref powers target_index acc cell_ptr cell fuel =
Some (rev acc ++ p :: l)%list →
equal_ptr p cell_ptr = true.
Proof.
intro Hequal.
match goal with
| |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ → _ ⇒
intro Haux;
destruct (aux'_nonempty_success der pow cp acc ti cell fuel); eauto
end.
rewrite Haux in H0.
unfold Compare.Equal.Valid.t in Hequal.
hauto lq: on use: List.app_inv_head.
Qed.
(cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
(target_index : int) (powers : FallbackArray.t int)
(equal_ptr : ptr_type → ptr_type → bool) (p : ptr_type)
(l acc : list ptr_type) (fuel : Datatypes.nat) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
aux' deref powers target_index acc cell_ptr cell fuel =
Some (rev acc ++ p :: l)%list →
equal_ptr p cell_ptr = true.
Proof.
intro Hequal.
match goal with
| |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ → _ ⇒
intro Haux;
destruct (aux'_nonempty_success der pow cp acc ti cell fuel); eauto
end.
rewrite Haux in H0.
unfold Compare.Equal.Valid.t in Hequal.
hauto lq: on use: List.app_inv_head.
Qed.
Result of work of [mem] function equals true
Lemma member_true'
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (path init_path : list ptr_type)
(fuel : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr =
Some (rev init_path ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
∃ (idx : int) (ptr : ptr_type),
FallbackArray.get x.(cell.back_pointers) idx = Some ptr ∧
equal_ptr p0 ptr = true ∧
Pervasives.Int.Valid.t idx.
Proof.
intro. rewrite aux''_eq_aux'. intros.
assert (cell_ptr = p)
by now apply aux'_head_equal_general
with (equal_ptr := equal_ptr) in H0.
revert H0. revert init_path.
induction fuel; try discriminate.
intros. simpl in ×.
destruct deref; try discriminate.
simpl in ×. inversion H2. rewrite H5 in ×. revert H0. step.
{ rewrite list_rev_cons. hauto q: on use: List.app_inv_head. }
{ step; try discriminate.
destruct best_skip eqn:BSkip; try discriminate.
simpl in ×. apply best_skip_result_valid in BSkip.
destruct back_pointer eqn:BP; try discriminate.
hecrush use: aux'_head_true_general,
(List.rev_head_app_eq init_path (p0 :: path) p).
}
Qed.
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (path init_path : list ptr_type)
(fuel : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr =
Some (rev init_path ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
∃ (idx : int) (ptr : ptr_type),
FallbackArray.get x.(cell.back_pointers) idx = Some ptr ∧
equal_ptr p0 ptr = true ∧
Pervasives.Int.Valid.t idx.
Proof.
intro. rewrite aux''_eq_aux'. intros.
assert (cell_ptr = p)
by now apply aux'_head_equal_general
with (equal_ptr := equal_ptr) in H0.
revert H0. revert init_path.
induction fuel; try discriminate.
intros. simpl in ×.
destruct deref; try discriminate.
simpl in ×. inversion H2. rewrite H5 in ×. revert H0. step.
{ rewrite list_rev_cons. hauto q: on use: List.app_inv_head. }
{ step; try discriminate.
destruct best_skip eqn:BSkip; try discriminate.
simpl in ×. apply best_skip_result_valid in BSkip.
destruct back_pointer eqn:BP; try discriminate.
hecrush use: aux'_head_true_general,
(List.rev_head_app_eq init_path (p0 :: path) p).
}
Qed.
Result of work of [mem] function equals true, auxiliary statement
Lemma member_true'' (equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type)
(path init_path : list ptr_type) (fuel : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr =
Some (rev init_path ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
x.(cell.back_pointers).(t.default) = None →
∃ (idx : int) (ptr : ptr_type),
FallbackArray.get x.(cell.back_pointers) idx = Some ptr ∧
equal_ptr p0 ptr = true ∧ 0 ≤ idx.
Proof.
intros.
destruct (
member_true'
equal_ptr cell_ptr target_cell powers path init_path fuel p p0 x
); trivial.
destruct H4, H4.
apply get_for_valid_idx in H4 as H4'; hauto lq: on rew: off.
Qed.
(cell_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type)
(path init_path : list ptr_type) (fuel : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index init_path cell_ptr =
Some (rev init_path ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
x.(cell.back_pointers).(t.default) = None →
∃ (idx : int) (ptr : ptr_type),
FallbackArray.get x.(cell.back_pointers) idx = Some ptr ∧
equal_ptr p0 ptr = true ∧ 0 ≤ idx.
Proof.
intros.
destruct (
member_true'
equal_ptr cell_ptr target_cell powers path init_path fuel p p0 x
); trivial.
destruct H4, H4.
apply get_for_valid_idx in H4 as H4'; hauto lq: on rew: off.
Qed.
This lemma requires that an array it uses
was shorter than [max_int], due to the integer overflows in [mem]
Lemma member_true_general (equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path acc : list ptr_type)
(fuel fuel' : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
= Some (rev acc ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
Cell.Valid.t x →
Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
< Pervasives.max_int →
let n_value := FallbackArray.length x.(cell.back_pointers) in
((Z.to_nat n_value) ≤ fuel')%nat →
mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
Proof.
unfold mem'. rewrite <- aux''_eq_aux'. intros. destruct H3.
apply mem_aux_of_Prop; try hfcrush use: stronger_length_limit. revert H0.
match goal with
| |- context[aux'' ?fuel ?der ?pow (?iv ?tc) ?acc ?cp =
Some (_ ++ ?p' :: ?p'' :: ?path)%list] ⇒
pose (member_true'' equal_ptr cp pow tc path acc fuel p' p'' x)
end.
pose stronger_length_limit. intro. destruct e; intuition. destruct H3.
apply mem_aux_Prop_exists_general with x1 x0; try hfcrush.
destruct H3. apply get_for_valid_idx in H3; intuition.
rewrite length_of_list_length; intuition.
Qed.
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path acc : list ptr_type)
(fuel fuel' : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
= Some (rev acc ++ p :: p0 :: path)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
Cell.Valid.t x →
Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
< Pervasives.max_int →
let n_value := FallbackArray.length x.(cell.back_pointers) in
((Z.to_nat n_value) ≤ fuel')%nat →
mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
Proof.
unfold mem'. rewrite <- aux''_eq_aux'. intros. destruct H3.
apply mem_aux_of_Prop; try hfcrush use: stronger_length_limit. revert H0.
match goal with
| |- context[aux'' ?fuel ?der ?pow (?iv ?tc) ?acc ?cp =
Some (_ ++ ?p' :: ?p'' :: ?path)%list] ⇒
pose (member_true'' equal_ptr cp pow tc path acc fuel p' p'' x)
end.
pose stronger_length_limit. intro. destruct e; intuition. destruct H3.
apply mem_aux_Prop_exists_general with x1 x0; try hfcrush.
destruct H3. apply get_for_valid_idx in H3; intuition.
rewrite length_of_list_length; intuition.
Qed.
This lemma requires that an array it uses
was shorter than [max_int], due to the integer overflows in [mem]
Lemma member_true (equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) (path : list ptr_type)
(fuel' : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
back_path' deref cell_ptr target_index = Some (p :: p0 :: path) →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
Cell.Valid.t x →
Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
< Pervasives.max_int →
let n_value := FallbackArray.length x.(cell.back_pointers) in
((Z.to_nat n_value) ≤ fuel')%nat →
mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
Proof.
unfold back_path'. destruct deref eqn:D; simpl; [| discriminate ].
hauto l: on use: member_true_general.
Qed.
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) (path : list ptr_type)
(fuel' : Datatypes.nat) (p p0 : ptr_type)
(x : cell content_type ptr_type) :
let target_index := index_value target_cell in
back_path' deref cell_ptr target_index = Some (p :: p0 :: path) →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref cell_ptr = Some x →
Cell.Valid.t x →
Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
< Pervasives.max_int →
let n_value := FallbackArray.length x.(cell.back_pointers) in
((Z.to_nat n_value) ≤ fuel')%nat →
mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
Proof.
unfold back_path'. destruct deref eqn:D; simpl; [| discriminate ].
hauto l: on use: member_true_general.
Qed.
Lemma states that auxiliary function [best_skip'] could not
return [None] result
Lemma best_skip'_always_some
(cell_ptr p p0 : ptr_type) (target_cell x : cell content_type ptr_type)
(powers : FallbackArray.t int) (l acc : list ptr_type)
(fuel fuel' : Datatypes.nat) :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
deref cell_ptr = Some x →
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)) ≤ fuel')%nat →
best_skip' x (index_value target_cell) powers fuel' = None → False.
Proof.
destruct fuel; try discriminate.
intros. simpl in ×. rewrite H1 in H0. simpl in H0. revert H0. step.
{ intro. inversion H0.
rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H5.
rewrite List.rev_head_app_eq in H5. apply app_inv_head in H5.
inversion H5.
}
{ step; try discriminate. intro.
rewrite best_skip'_eq with (fuel0 := fuel') in H0; trivial.
unfold target_index in H0. rewrite H3 in H0. discriminate.
}
Qed.
(cell_ptr p p0 : ptr_type) (target_cell x : cell content_type ptr_type)
(powers : FallbackArray.t int) (l acc : list ptr_type)
(fuel fuel' : Datatypes.nat) :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
deref cell_ptr = Some x →
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)) ≤ fuel')%nat →
best_skip' x (index_value target_cell) powers fuel' = None → False.
Proof.
destruct fuel; try discriminate.
intros. simpl in ×. rewrite H1 in H0. simpl in H0. revert H0. step.
{ intro. inversion H0.
rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H5.
rewrite List.rev_head_app_eq in H5. apply app_inv_head in H5.
inversion H5.
}
{ step; try discriminate. intro.
rewrite best_skip'_eq with (fuel0 := fuel') in H0; trivial.
unfold target_index in H0. rewrite H3 in H0. discriminate.
}
Qed.
Lemma states that auxiliary function [FallbackArray.get] could not
return [None] result : generalized version
Lemma get_always_some_general
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type)
(fuel : Datatypes.nat) (i start_idx end_idx : int) :
let target_index := index_value target_cell in
0 ≤ start_idx →
start_idx ≤ end_idx →
end_idx < FallbackArray.length x.(cell.back_pointers) →
deref cell_ptr = Some x →
Cell.Valid.t x →
binary_search x target_index powers start_idx end_idx fuel = Some i →
∃ best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
Some best_ptr.
Proof.
(* @TODO *)
Admitted.
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type)
(fuel : Datatypes.nat) (i start_idx end_idx : int) :
let target_index := index_value target_cell in
0 ≤ start_idx →
start_idx ≤ end_idx →
end_idx < FallbackArray.length x.(cell.back_pointers) →
deref cell_ptr = Some x →
Cell.Valid.t x →
binary_search x target_index powers start_idx end_idx fuel = Some i →
∃ best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
Some best_ptr.
Proof.
(* @TODO *)
Admitted.
Lemma states that auxiliary function [get] could not
return [None] result
Lemma get_always_some
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type) (fuel : Datatypes.nat)
(i : int) :
let target_index := index_value target_cell in
deref cell_ptr = Some x →
Cell.Valid.t x →
binary_search x target_index powers 0
((FallbackArray.length x.(cell.back_pointers)) -i 1) fuel =
Some i →
∃ best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
Some best_ptr.
Proof.
(* @TODO *)
Admitted.
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type) (fuel : Datatypes.nat)
(i : int) :
let target_index := index_value target_cell in
deref cell_ptr = Some x →
Cell.Valid.t x →
binary_search x target_index powers 0
((FallbackArray.length x.(cell.back_pointers)) -i 1) fuel =
Some i →
∃ best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
Some best_ptr.
Proof.
(* @TODO *)
Admitted.
Lemma states that auxiliary function [back_pointer] could not
return [None] result
Lemma back_pointer_always_some
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type)
(fuel : Datatypes.nat) (i : int) :
let target_index := index_value target_cell in
deref cell_ptr = Some x →
Cell.Valid.t x →
best_skip' x (index_value target_cell) powers fuel = Some i →
∃ best_ptr, (back_pointer x i) = Some best_ptr.
Proof.
unfold best_skip', back_pointer. now apply get_always_some.
Qed.
(cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type)
(fuel : Datatypes.nat) (i : int) :
let target_index := index_value target_cell in
deref cell_ptr = Some x →
Cell.Valid.t x →
best_skip' x (index_value target_cell) powers fuel = Some i →
∃ best_ptr, (back_pointer x i) = Some best_ptr.
Proof.
unfold best_skip', back_pointer. now apply get_always_some.
Qed.
Lemma shows equality of pointers in certain conditions
Fixpoint best_ptr_eq
(equal_ptr : ptr_type → ptr_type → bool) (powers : FallbackArray.t int)
(cell_ptr target_ptr p p0 best_ptr : ptr_type)
(target_cell x c : cell content_type ptr_type) (l acc : list ptr_type)
(fuel fuel' : Datatypes.nat) (i : int) {struct fuel} :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
equal_ptr p cell_ptr = true →
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)) ≤ fuel')%nat →
best_skip' x target_index powers fuel' = Some i →
deref p0 = Some c →
back_pointer x i = Some best_ptr →
equal_ptr best_ptr p0 = true.
Proof.
destruct fuel, fuel'; try discriminate.
intros; simpl in ×. revert H0. rewrite H3. simpl. step.
{ intro. inversion H0.
rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H10.
rewrite List.rev_head_app_eq in H10. apply app_inv_head in H10.
inversion H10.
}
{ step; try discriminate.
rewrite best_skip'_eq with (fuel0 := Datatypes.S fuel'); trivial.
rewrite H6. simpl.
rewrite H8. simpl.
apply H1 in H4. 2, 3 : apply I.
rewrite H4.
assert (T
: (rev acc ++ cell_ptr :: p0 :: l
= rev (cell_ptr :: acc) ++ p0 :: l)%list) by
(symmetry; apply List.rev_head_app_eq). rewrite T.
clear T. intro.
pose proof (aux'_head_true_general best_ptr (deref best_ptr)
target_index powers equal_ptr p0 l (cell_ptr :: acc) fuel H1
H0).
apply H1 in H9; trivial. now apply H1. }
Qed.
(* We do one step reduction inside path-building.
We will need this statement in the main proof *)
Lemma one_step
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr p p0 : ptr_type) (powers : FallbackArray.t int)
(target_cell x c : cell content_type ptr_type)
(l acc : list ptr_type) (fuel : Datatypes.nat) (i : int) :
let target_index := index_value target_cell in
deref p = Some x →
best_skip x (index_value target_cell) powers = Some i →
mem equal_ptr p0 x.(cell.back_pointers) = true →
deref p0 = Some c →
back_pointer x i = Some p0 →
aux' deref powers target_index acc p (deref p) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
aux' deref powers (index_value target_cell) (p :: acc) p0 (deref p0)
(Datatypes.S fuel) = Some (rev (p :: acc) ++ p0 :: l)%list.
Proof.
intros.
unfold aux' in H5. destruct fuel. inversion H5. revert H5.
rewrite H0. simpl. step.
{ intro. injection H5 as H5.
assert (B1 : rev (p :: acc)%list = (rev (p :: acc) ++ [])%list)
by scongruence use: app_nil_r. rewrite B1 in H5.
rewrite List.rev_head_app_eq in H5. apply List.app_inv_head_iff in H5.
scongruence.
}
{ step.
{ intro. inversion H5. }
{ assert (H6 : target_index = index_value target_cell) by scongruence.
rewrite <- H6 in H1. rewrite H1. simpl. rewrite H4. simpl.
assert (T : (rev acc ++ p :: p0 :: l = rev (p :: acc) ++ p0 :: l)%list)
by (symmetry; apply List.rev_head_app_eq).
rewrite T. intro. apply (aux'_sufficient_fuel _ _ _ _ _ _ fuel
(Datatypes.S (Datatypes.S fuel))).
apply H5. hauto l: on.
}
}
Qed.
(equal_ptr : ptr_type → ptr_type → bool) (powers : FallbackArray.t int)
(cell_ptr target_ptr p p0 best_ptr : ptr_type)
(target_cell x c : cell content_type ptr_type) (l acc : list ptr_type)
(fuel fuel' : Datatypes.nat) (i : int) {struct fuel} :
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
equal_ptr p cell_ptr = true →
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)) ≤ fuel')%nat →
best_skip' x target_index powers fuel' = Some i →
deref p0 = Some c →
back_pointer x i = Some best_ptr →
equal_ptr best_ptr p0 = true.
Proof.
destruct fuel, fuel'; try discriminate.
intros; simpl in ×. revert H0. rewrite H3. simpl. step.
{ intro. inversion H0.
rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H10.
rewrite List.rev_head_app_eq in H10. apply app_inv_head in H10.
inversion H10.
}
{ step; try discriminate.
rewrite best_skip'_eq with (fuel0 := Datatypes.S fuel'); trivial.
rewrite H6. simpl.
rewrite H8. simpl.
apply H1 in H4. 2, 3 : apply I.
rewrite H4.
assert (T
: (rev acc ++ cell_ptr :: p0 :: l
= rev (cell_ptr :: acc) ++ p0 :: l)%list) by
(symmetry; apply List.rev_head_app_eq). rewrite T.
clear T. intro.
pose proof (aux'_head_true_general best_ptr (deref best_ptr)
target_index powers equal_ptr p0 l (cell_ptr :: acc) fuel H1
H0).
apply H1 in H9; trivial. now apply H1. }
Qed.
(* We do one step reduction inside path-building.
We will need this statement in the main proof *)
Lemma one_step
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr p p0 : ptr_type) (powers : FallbackArray.t int)
(target_cell x c : cell content_type ptr_type)
(l acc : list ptr_type) (fuel : Datatypes.nat) (i : int) :
let target_index := index_value target_cell in
deref p = Some x →
best_skip x (index_value target_cell) powers = Some i →
mem equal_ptr p0 x.(cell.back_pointers) = true →
deref p0 = Some c →
back_pointer x i = Some p0 →
aux' deref powers target_index acc p (deref p) fuel =
Some (rev acc ++ p :: p0 :: l)%list →
aux' deref powers (index_value target_cell) (p :: acc) p0 (deref p0)
(Datatypes.S fuel) = Some (rev (p :: acc) ++ p0 :: l)%list.
Proof.
intros.
unfold aux' in H5. destruct fuel. inversion H5. revert H5.
rewrite H0. simpl. step.
{ intro. injection H5 as H5.
assert (B1 : rev (p :: acc)%list = (rev (p :: acc) ++ [])%list)
by scongruence use: app_nil_r. rewrite B1 in H5.
rewrite List.rev_head_app_eq in H5. apply List.app_inv_head_iff in H5.
scongruence.
}
{ step.
{ intro. inversion H5. }
{ assert (H6 : target_index = index_value target_cell) by scongruence.
rewrite <- H6 in H1. rewrite H1. simpl. rewrite H4. simpl.
assert (T : (rev acc ++ p :: p0 :: l = rev (p :: acc) ++ p0 :: l)%list)
by (symmetry; apply List.rev_head_app_eq).
rewrite T. intro. apply (aux'_sufficient_fuel _ _ _ _ _ _ fuel
(Datatypes.S (Datatypes.S fuel))).
apply H5. hauto l: on.
}
}
Qed.
Lemma states that last index of the path equals to [target_index]
Lemma aux''_last_index_is_target
(cell_ptr ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
∃ c, deref ptr = Some c ∧
target_index =i index_value c = true.
Proof.
intros.
revert path' cell_ptr H0.
induction fuel; try discriminate.
intros ? ?. simpl. destruct (deref cell_ptr) eqn:H'; try discriminate.
simpl. step.
{ qauto l: on use: app_inj_tail, list_rev_cons, index_ptr_eq. }
{ step; try discriminate.
destruct best_skip; try discriminate. simpl.
destruct back_pointer; try discriminate. simpl.
intro. now apply IHfuel in H0.
}
Qed.
(cell_ptr ptr : ptr_type) (target_cell : cell content_type ptr_type)
(powers : FallbackArray.t int) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
∃ c, deref ptr = Some c ∧
target_index =i index_value c = true.
Proof.
intros.
revert path' cell_ptr H0.
induction fuel; try discriminate.
intros ? ?. simpl. destruct (deref cell_ptr) eqn:H'; try discriminate.
simpl. step.
{ qauto l: on use: app_inj_tail, list_rev_cons, index_ptr_eq. }
{ step; try discriminate.
destruct best_skip; try discriminate. simpl.
destruct back_pointer; try discriminate. simpl.
intro. now apply IHfuel in H0.
}
Qed.
Lemma states that last index of the path equals to [target_index]
Lemma aux''_last_is_target
(cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
deref target_ptr = Some target_cell →
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
target_ptr = ptr.
Proof.
hauto l: on use: aux''_last_index_is_target.
Qed.
(cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
deref target_ptr = Some target_cell →
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
target_ptr = ptr.
Proof.
hauto l: on use: aux''_last_index_is_target.
Qed.
Lemma states that last index of the path equals to [target_index]
boolean version
Lemma aux''_last_is_target_bool
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
equal_ptr target_ptr ptr = true.
Proof.
unfold Compare.Equal.Valid.t. hauto l: on use: aux''_last_is_target.
Qed.
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
(target_cell : cell content_type ptr_type) (path path' : list ptr_type)
(fuel : Datatypes.nat) :
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
deref target_ptr = Some target_cell →
let target_index := index_value target_cell in
aux'' fuel deref powers target_index path' cell_ptr
= Some (path ++ [ptr])%list →
equal_ptr target_ptr ptr = true.
Proof.
unfold Compare.Equal.Valid.t. hauto l: on use: aux''_last_is_target.
Qed.
Heart of the proof - we prove by induction that function [valid_path']
will return true if path was byilt by [back_path].
Lemma back_path'_valid_path'
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr p : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type) (path acc : list ptr_type)
(fuel : Datatypes.nat)
(path_valid : ∀ p x,
In p path → deref p = Some x → Cell.Valid.t x) :
(∀ cptr cval,
In cptr (rev acc ++ p :: path)%list →
deref cptr = Some cval →
Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
< Pervasives.max_int) →
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
= Some (rev acc ++ p :: path)%list →
(∀ p1 : ptr_type, In p1 acc → deref p1 = None → False) →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
Cell.Valid.t x →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
p = cell_ptr→
valid_path' equal_ptr target_ptr target_cell deref powers (index_value x)
cell_ptr path = true.
Proof.
revert equal_ptr cell_ptr target_ptr target_cell acc fuel p x path_valid.
induction path as [|p0 l]; intros; unfold valid_path'.
{ rewrite <- aux''_eq_aux' in H1. rewrite H7 in ×.
apply aux''_last_is_target_bool
with (equal_ptr := equal_ptr) (target_ptr := target_ptr)
in H1 as H1';
trivial.
apply aux''_last_index_is_target in H1. destruct H1. rewrite H6 in ×.
destruct H1. inversion H1. rewrite H10 in ×. rewrite H1'. cbn in ×.
now rewrite Z.eqb_sym.
}
{ rewrite H6; simpl. destruct (deref p0) eqn:DP0; simpl;
[| rewrite <- aux''_eq_aux' in H1;
apply all_elements_not_none_general with (p_any := p0) in H1;
intuition ].
assert ((mem equal_ptr p0 x.(cell.back_pointers)) = true).
{ rewrite mem_eq
with (fuel0 :=
Z.to_nat (FallbackArray.length x.(cell.back_pointers)));
[| intuition ].
apply member_true_general
with cell_ptr powers target_cell l acc fuel p;
trivial.
apply H0 with cell_ptr; trivial.
rewrite <- aux''_eq_aux' in H1.
destruct (aux''_nonempty_success
deref powers cell_ptr acc target_index fuel).
{ hauto l: on. }
{ rewrite H8 in H1. inversion H1. apply List.app_inv_head in H10.
intuition.
}
}
{ rewrite H8. rewrite Bool.andb_true_l.
rewrite best_skip'_eq
with (fuel0 :=
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))));
[| intuition ].
pose proof (
best_skip'_always_some
cell_ptr p p0 target_cell x powers l acc fuel
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))) H1 H6).
destruct (best_skip' x (index_value target_cell)) eqn:Best_skip;
[simpl|hauto lq: on rew: off].
destruct (back_pointer x i) eqn:Back_P;
[ simpl
| pose proof (
back_pointer_always_some cell_ptr target_ptr powers target_cell
x (Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
i H6 H4 Best_skip); destruct H10; scongruence].
assert (equal_ptr p1 p0 = true).
{ assert (EP : equal_ptr p cell_ptr = true)
by (apply H3; hauto l: on).
apply (best_ptr_eq equal_ptr powers cell_ptr target_ptr p p0 p1
target_cell x c l acc fuel
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
i H1 H3 H5 H6 EP
(Nat.le_refl
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))))
Best_skip DP0 Back_P).
}
{ rewrite H10. rewrite Bool.andb_true_l.
assert (T : (deref p = Some x)) by scongruence.
assert (p0 = p1) by (apply H3 in H10; hauto l: on).
assert (T1 : (back_pointer x i = Some p0)) by scongruence.
assert (equal_ptr p0 p0 = true) by scongruence.
assert (PR : aux' deref powers (index_value target_cell) (p :: acc)
p0 (deref p0) (Datatypes.S (Datatypes.S fuel)) =
Some (rev (p :: acc) ++ p0 :: l)%list).
{ (* Proving PR with one_step *)
assert (U2: back_pointer x i = Some p0) by scongruence.
pose Best_skip as B_skip.
rewrite <- best_skip'_eq in B_skip; [| intuition ].
apply (one_step equal_ptr cell_ptr target_ptr p p0 powers
target_cell x c l acc (Datatypes.S fuel) i T
B_skip H8 DP0 U2).
assert (Y : (index_value target_cell) = target_index)
by scongruence.
rewrite Y. rewrite H7 in ×. rewrite <- H11 in ×.
apply (aux'_sufficient_fuel _ _ _ _ _ _ _ (Datatypes.S fuel))
in H1;
[ apply H1 | hauto l: on ].
}
{ fold (valid_path'
equal_ptr target_ptr target_cell
deref powers c.(cell.index) p0 l). fold (index_value c).
assert (∀ (p : ptr_type) (x : cell content_type ptr_type),
In p l → deref p = Some x → Cell.Valid.t x) by
(intros; apply path_valid with p2; intuition).
rewrite <- List.rev_head_app_eq in H0.
apply (IHl equal_ptr p0 target_ptr target_cell (p :: acc)%list _
p0 c H13 H0 PR); trivial.
{ cbn. intros. destruct H14.
{ rewrite <- H14 in H15. rewrite H15 in T. discriminate. }
{ intuition. }
}
{ apply path_valid with p0; intuition. }
}
}
}
}
Qed.
End Helper_section.
End Helper_valid.
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr p : ptr_type) (powers : FallbackArray.t int)
(target_cell x : cell content_type ptr_type) (path acc : list ptr_type)
(fuel : Datatypes.nat)
(path_valid : ∀ p x,
In p path → deref p = Some x → Cell.Valid.t x) :
(∀ cptr cval,
In cptr (rev acc ++ p :: path)%list →
deref cptr = Some cval →
Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
< Pervasives.max_int) →
let target_index := index_value target_cell in
aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
= Some (rev acc ++ p :: path)%list →
(∀ p1 : ptr_type, In p1 acc → deref p1 = None → False) →
Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
Cell.Valid.t x →
deref target_ptr = Some target_cell →
deref cell_ptr = Some x →
p = cell_ptr→
valid_path' equal_ptr target_ptr target_cell deref powers (index_value x)
cell_ptr path = true.
Proof.
revert equal_ptr cell_ptr target_ptr target_cell acc fuel p x path_valid.
induction path as [|p0 l]; intros; unfold valid_path'.
{ rewrite <- aux''_eq_aux' in H1. rewrite H7 in ×.
apply aux''_last_is_target_bool
with (equal_ptr := equal_ptr) (target_ptr := target_ptr)
in H1 as H1';
trivial.
apply aux''_last_index_is_target in H1. destruct H1. rewrite H6 in ×.
destruct H1. inversion H1. rewrite H10 in ×. rewrite H1'. cbn in ×.
now rewrite Z.eqb_sym.
}
{ rewrite H6; simpl. destruct (deref p0) eqn:DP0; simpl;
[| rewrite <- aux''_eq_aux' in H1;
apply all_elements_not_none_general with (p_any := p0) in H1;
intuition ].
assert ((mem equal_ptr p0 x.(cell.back_pointers)) = true).
{ rewrite mem_eq
with (fuel0 :=
Z.to_nat (FallbackArray.length x.(cell.back_pointers)));
[| intuition ].
apply member_true_general
with cell_ptr powers target_cell l acc fuel p;
trivial.
apply H0 with cell_ptr; trivial.
rewrite <- aux''_eq_aux' in H1.
destruct (aux''_nonempty_success
deref powers cell_ptr acc target_index fuel).
{ hauto l: on. }
{ rewrite H8 in H1. inversion H1. apply List.app_inv_head in H10.
intuition.
}
}
{ rewrite H8. rewrite Bool.andb_true_l.
rewrite best_skip'_eq
with (fuel0 :=
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))));
[| intuition ].
pose proof (
best_skip'_always_some
cell_ptr p p0 target_cell x powers l acc fuel
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))) H1 H6).
destruct (best_skip' x (index_value target_cell)) eqn:Best_skip;
[simpl|hauto lq: on rew: off].
destruct (back_pointer x i) eqn:Back_P;
[ simpl
| pose proof (
back_pointer_always_some cell_ptr target_ptr powers target_cell
x (Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
i H6 H4 Best_skip); destruct H10; scongruence].
assert (equal_ptr p1 p0 = true).
{ assert (EP : equal_ptr p cell_ptr = true)
by (apply H3; hauto l: on).
apply (best_ptr_eq equal_ptr powers cell_ptr target_ptr p p0 p1
target_cell x c l acc fuel
(Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
i H1 H3 H5 H6 EP
(Nat.le_refl
(Z.to_nat (FallbackArray.length x.(cell.back_pointers))))
Best_skip DP0 Back_P).
}
{ rewrite H10. rewrite Bool.andb_true_l.
assert (T : (deref p = Some x)) by scongruence.
assert (p0 = p1) by (apply H3 in H10; hauto l: on).
assert (T1 : (back_pointer x i = Some p0)) by scongruence.
assert (equal_ptr p0 p0 = true) by scongruence.
assert (PR : aux' deref powers (index_value target_cell) (p :: acc)
p0 (deref p0) (Datatypes.S (Datatypes.S fuel)) =
Some (rev (p :: acc) ++ p0 :: l)%list).
{ (* Proving PR with one_step *)
assert (U2: back_pointer x i = Some p0) by scongruence.
pose Best_skip as B_skip.
rewrite <- best_skip'_eq in B_skip; [| intuition ].
apply (one_step equal_ptr cell_ptr target_ptr p p0 powers
target_cell x c l acc (Datatypes.S fuel) i T
B_skip H8 DP0 U2).
assert (Y : (index_value target_cell) = target_index)
by scongruence.
rewrite Y. rewrite H7 in ×. rewrite <- H11 in ×.
apply (aux'_sufficient_fuel _ _ _ _ _ _ _ (Datatypes.S fuel))
in H1;
[ apply H1 | hauto l: on ].
}
{ fold (valid_path'
equal_ptr target_ptr target_cell
deref powers c.(cell.index) p0 l). fold (index_value c).
assert (∀ (p : ptr_type) (x : cell content_type ptr_type),
In p l → deref p = Some x → Cell.Valid.t x) by
(intros; apply path_valid with p2; intuition).
rewrite <- List.rev_head_app_eq in H0.
apply (IHl equal_ptr p0 target_ptr target_cell (p :: acc)%list _
p0 c H13 H0 PR); trivial.
{ cbn. intros. destruct H14.
{ rewrite <- H14 in H15. rewrite H15 in T. discriminate. }
{ intuition. }
}
{ apply path_valid with p0; intuition. }
}
}
}
}
Qed.
End Helper_section.
End Helper_valid.
Main lemma [back_path_is_valid]
Lemma back_path_is_valid `{FArgs} {content_type ptr_type : Set}
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) (path : list ptr_type)
(deref : ptr_type → option (cell content_type ptr_type)) (fuel : nat)
(cell_index_spec : Helper_valid.Cell_Index.Valid.t deref)
(path_valid : ∀ p x,
In p path → deref p = Some x → Cell.Valid.t x)
(array_len_valid :
∀ cptr cval,
In cptr path →
deref cptr = Some cval →
Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
< Pervasives.max_int) :
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.
intros. rewrite (back_path_eq deref cell_ptr target_index) in H2.
unfold valid_back_path. rewrite H1. simpl.
remember H2 as H3; clear HeqH3. apply back_path'_cell_not_none in H2.
destruct H2; rewrite H2; simpl. remember H3 as H4; clear HeqH4.
pose proof (back_path'_not_nil deref cell_ptr target_index path).
assert (G : path ≠ []) by scongruence. destruct path; try scongruence.
remember H3 as H6; clear HeqH6. apply back_path'_equal_Prop_head
in H6. rewrite H6. apply Bool.andb_true_iff.
split; try apply H0; trivial.
rewrite valid_path_eq. unfold back_path' in H3.
assert (W : aux' deref (list_powers x) target_index nil cell_ptr
(deref cell_ptr)
(bp_compute_fuel deref (list_powers x) cell_ptr
target_index) =
Some (rev nil ++ p :: path)%list)
by (revert H4; hauto lq: on).
apply Helper_valid.back_path'_valid_path'
with p nil (bp_compute_fuel deref (list_powers x) cell_ptr target_index);
hauto lq: on.
Qed.
(equal_ptr : ptr_type → ptr_type → bool)
(cell_ptr target_ptr : ptr_type)
(target_cell : cell content_type ptr_type) (path : list ptr_type)
(deref : ptr_type → option (cell content_type ptr_type)) (fuel : nat)
(cell_index_spec : Helper_valid.Cell_Index.Valid.t deref)
(path_valid : ∀ p x,
In p path → deref p = Some x → Cell.Valid.t x)
(array_len_valid :
∀ cptr cval,
In cptr path →
deref cptr = Some cval →
Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
< Pervasives.max_int) :
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.
intros. rewrite (back_path_eq deref cell_ptr target_index) in H2.
unfold valid_back_path. rewrite H1. simpl.
remember H2 as H3; clear HeqH3. apply back_path'_cell_not_none in H2.
destruct H2; rewrite H2; simpl. remember H3 as H4; clear HeqH4.
pose proof (back_path'_not_nil deref cell_ptr target_index path).
assert (G : path ≠ []) by scongruence. destruct path; try scongruence.
remember H3 as H6; clear HeqH6. apply back_path'_equal_Prop_head
in H6. rewrite H6. apply Bool.andb_true_iff.
split; try apply H0; trivial.
rewrite valid_path_eq. unfold back_path' in H3.
assert (W : aux' deref (list_powers x) target_index nil cell_ptr
(deref cell_ptr)
(bp_compute_fuel deref (list_powers x) cell_ptr
target_index) =
Some (rev nil ++ p :: path)%list)
by (revert H4; hauto lq: on).
apply Helper_valid.back_path'_valid_path'
with p nil (bp_compute_fuel deref (list_powers x) cell_ptr target_index);
hauto lq: on.
Qed.
Proof of [back_path_is_uniq] starts here
Fixpoint 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)) {struct path}:
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.
(* @TODO: prove in Proto_J first *)
Admitted.
End Make.