MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit cbadeed3 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Split off several files examples_*.v.

parent 520f2727
......@@ -17,3 +17,7 @@ src/adequacy.v
src/proofmode.v
src/notation.v
src/test.v
src/examples_lists.v
src/examples_queues.v
src/examples_graphs.v
src/examples_sort.v
From Coq Require Program RelationClasses.
From spacelang Require Import stdpp proofmode notation.
From spacelang Require Import examples_lists examples_queues.
Section Functional_BFS.
Context `{EqDecision A}.
Fixpoint remove_first (x : A) (l : list A) : list A :=
match l with
| [] => []
| y :: l => if decide (x = y) then l else y :: remove_first x l
end.
Lemma remove_first_not_in x (l : list A) : x l -> remove_first x l = l.
Proof.
induction l; auto. simpl.
destruct decide.
- subst x. intros Ha; destruct Ha. left.
- intros Ha. rewrite IHl; auto. intros Hl. apply Ha. now right.
Qed.
Lemma remove_first_in x (l : list A) :
x l -> l1 l2, l = l1 ++ [x] ++ l2 /\ x l1 /\ remove_first x l = l1 ++ l2.
Proof.
induction l as [| a l IHl]; intros i.
- inversion i.
- simpl. destruct decide as [<- | n].
+ exists [], l. repeat split; auto. inversion 1.
+ destruct IHl as (l1 & l2 & -> & ni & E).
{ inversion i; subst; auto; tauto. }
exists (a :: l1), l2. repeat split.
* inversion 1; subst; tauto.
* rewrite E //.
Qed.
Lemma remove_first_length x (l : list A) :
x l -> (1 + length (remove_first x l) = length l)%nat.
Proof.
induction l; inversion 1; subst; simpl; destruct decide; auto. tauto.
Qed.
(** keep? a bit closer to the spacelang program *)
Fixpoint mark_neigh (neigh : list A) (unvisited queue : list A) :=
match neigh with
| [] => (unvisited, queue)
| v :: l =>
if decide (v unvisited) then
mark_neigh l (remove_first v unvisited) (queue ++ [v])
else
mark_neigh l unvisited queue
end.
Lemma mark_neigh_length l :
forall r q r' q',
mark_neigh l r q = (r', q') -> length r + length q = length r' + length q'.
Proof.
induction l as [ | v l IHl]; intros r q r' q'.
- intros [= <- <-]. auto.
- simpl. destruct decide; intros E; apply IHl in E; auto.
pose proof remove_first_length v r ltac:(auto).
rewrite app_length in E. simpl in E. lia.
Qed.
Program Fixpoint fbfs_1 (E : A -> list A) (unvisited queue : list A)
{ measure (length (queue ++ unvisited)) } :=
match queue with
| [] => []
| v :: queue =>
let uq := mark_neigh (E v) unvisited queue in
v :: fbfs_1 E (fst uq) (snd uq)
end.
Next Obligation.
intros E u ? _ v q <- uq.
destruct uq as (u', q') eqn:Euq; subst uq. simpl.
apply mark_neigh_length in Euq.
rewrite !app_length. lia.
Defined.
Next Obligation.
apply Wf.measure_wf, lt_wf.
Defined.
(** [uniques l] returns the list of unique elements of [l], in order
of first appearance *)
Definition uniques (l : list A) := rev (remove_dups (rev l)).
(* Keep if this is a better spec for BFS? It is harder to prove
terminating, also it is not really the same algorithm. *)
Program Fixpoint bfs_filters (E : A -> list A) (unvisited queue : list A)
{ measure (length (queue ++ unvisited)) } :=
match queue with
| [] => []
| v :: queue =>
v :: bfs_filters E
(filter (fun x => x E v) unvisited)
(queue ++ uniques (filter (fun x => x unvisited) (E v)))
end.
Next Obligation.
intros E ? u _ v q <-.
rewrite !app_length /=.
match goal with |- (?q + ?a + ?u' < S (?q + ?u))%nat => cut (a + u' = u)%nat end. lia.
generalize (E v) as l; intros l. clear v q E. revert unvisited.
induction l as [ | a l IHl]; intros u.
- simpl. f_equal. induction u; auto.
rewrite filter_cons_True. congruence. inversion 1.
- rewrite filter_cons. destruct decide as [e | n].
+ (** hmmm for now I should work on the other, implementation,
both closer to the program and easier to prove terminating. *)
shelve.
+ rewrite <-(IHl u). do 2 f_equal. clear IHl.
apply list_filter_iff_dom.
intros x xu; split; intros i j.
* apply i. now right.
* apply elem_of_cons in j. intuition; subst; tauto.
Admitted.
Next Obligation.
apply Wf.measure_wf, lt_wf.
Defined.
(** [select unvisited [] l] returns the pair [(s, u)] where [s] is
the list of unique elements of [l] that are not in [unvisited],
in order of first appearance in [l], and [u] is [unvisited]
where the elements [l] are removed. ---> not used in the spec! *)
Fixpoint select_visit (acc unvisited l : list A) :=
match l with
| [] => (rev acc, unvisited)
| v :: l => if decide (v unvisited) then
select_visit (v :: acc) (remove_first v unvisited) l
else
select_visit acc unvisited l
end.
Lemma select_visit_length l :
forall a u a' u',
select_visit a u l = (a', u') ->
length a + length u = length a' + length u'.
Proof.
induction l as [ | v l IHl]; intros u q u' q'.
- intros [= <- <-]. now rewrite rev_length.
- simpl.
destruct decide; intros E; apply IHl in E; try lia.
simpl in E.
pose proof remove_first_length v q ltac:(auto). lia.
Qed.
Program Fixpoint fbfs_ (E : A -> list A) (unvisited queue : list A)
{ measure (length (queue ++ unvisited)) } :=
match queue with
| [] => []
| v :: queue => let su := select_visit [] unvisited (E v) in
v :: fbfs_ E (snd su) (queue ++ fst su)
end.
Next Obligation.
intros E u ? _ v q <- uq.
destruct uq as (u', q') eqn:Euq; subst uq. simpl.
apply select_visit_length in Euq. simpl in Euq.
rewrite !app_length. lia.
Defined.
Next Obligation.
apply Wf.measure_wf, lt_wf.
Defined.
Definition fbfs V E root : list A :=
fbfs_ E (remove EqDecision0 root V) [root].
Inductive reachable (E : A -> list A) : relation A :=
| reachable_refl root : reachable E root root
| reachable_step root x y : reachable E root x -> y E x -> reachable E root y.
Definition valid_graph (V : list A) (E : A -> list A) :=
forall v w, v V -> w E v -> w E w.
Lemma bfs_reaches V E root :
valid_graph V E ->
forall x, reachable E root x <-> x fbfs V E root.
Abort.
End Functional_BFS.
(* example graph: square 0 -> 1,2 -> 3 with diagonal back arrow 3->0
and antidiagonals 1<->2 *)
Section Example.
Definition E (v : Z) :=
if v =? 0 then [1;2] else
if v =? 1 then [2;3] else
if v =? 2 then [2;3] else
if v =? 3 then [0] else
[].
Example example : fbfs_ E [1;2;3;4] [0] = [0;1;2;3].
Proof.
Fail Fail reflexivity.
Ltac step :=
match goal with
|- context [fbfs_ ?E ?u (?v :: ?q)] =>
let su := fresh "su" in
pose (su := select_visit [] u (E v));
replace (fbfs_ E u (v :: q))
with (v :: fbfs_ E (snd su) (q ++ fst su)) by (compute; reflexivity)
end.
step. compute in su. subst su; simpl snd; simpl app.
step. compute in su. subst su; simpl snd; simpl app.
step. compute in su. subst su; simpl snd; simpl app.
step. compute in su. subst su; simpl snd; simpl app.
reflexivity.
Qed.
End Example.
Section proof.
Context `{!heapG Σ}.
(** We represent directed graphs on locations, with a list of
location vertices [V], and for each vertex [v] in [V], [E v] is
its adjacency list. Note that [V] must contain all neighbours of
any [v V]: *)
(* Our representation in memory also contains marks (for the
algorithm to mark vertices as visited). Each node [v] points to a
tuple [[mark, l]] where [l] points to the list of locations [E v]
and [mark] is a finite size integer. Isomorphically, [v] points
to the list [mark :: E v] *)
Definition Node (v : loc) (mark : bool) (successors : list loc) :=
List ((^(Z.b2z mark))%V :: List.map VLoc successors) v.
Definition Graph (V : list loc) (E : loc -> list loc) (mark : gmap loc bool) :=
([ list] v V, Node v (mark !!! v) (E v))%I.
Lemma NoDup_lookup_neq {A} (l : list A) i j x y :
NoDup l -> i j -> l !! i = Some x -> l !! j = Some y -> x y.
Proof.
intros nd n ix jy <-.
eapply n, NoDup_lookup; eauto.
Qed.
(* Reasoning rule for marking an element as visited *)
Lemma visit_spec V E x visited :
NoDup V ->
x V ->
{{{ Graph V E visited }}}
#x ! 0 <- ^1
{{{ RET (); Graph V E (<[x := true]> visited) }}}.
Proof.
iIntros (nv hx phi) "g post".
set visited' := <[x:=true]> _.
unfold Graph.
(* pose g := fun (_ : nat) y => Node y (visited' !!! y) (E y). *)
apply elem_of_list_split in hx.
destruct hx as (V1 & V2 & EV). rewrite EV.
change (V1 ++ x :: V2) with (V1 ++ [x] ++ V2).
rewrite ->2big_sepL_app.
iDestruct "g" as "(g1 & gx & g2)".
rewrite big_sepL_singleton. iSimpl in "gx".
iDestruct "gx" as (l) "[hx hl]".
wp_store.
iAssert ([ list] y [x], Node y (visited' !!! y) (E y))%I with "[hx hl]" as "gx".
{ rewrite big_sepL_singleton. simpl. iExists l. iFrame.
unfold visited'. rewrite lookup_total_insert. auto. }
iApply "post". rewrite ->2big_sepL_app.
iFrame.
iSplitL "g1".
+ erewrite <-big_opL_ext.
iFrame. intros k y H. simpl. f_equal.
apply lookup_total_insert_ne.
subst V.
eapply (NoDup_lookup_neq _ (length V1) k); eauto.
* apply lookup_lt_Some in H. lia.
* now apply list_lookup_middle.
* now apply lookup_app_l_Some.
+ erewrite <-big_opL_ext.
iFrame. intros k y H. simpl. f_equal.
apply lookup_total_insert_ne.
subst V.
eapply (NoDup_lookup_neq _ (length V1) (length V1 + 1 + k)); eauto.
* lia.
* now apply list_lookup_middle.
* rewrite lookup_app_r. 2:lia.
cut (length V1 + 1 + k - length V1 = 1 + k)%nat. 2:lia.
now intros ->.
Qed.
Definition enqueue_and_visit_children : val :=
μ: "iter", [["q", "v"]],
let: "visited" := "v" ? 0 in
(if: "visited" then
return: ()
else
"v" ! 0 <- ^1;;
push_back [["q", "v"]]
);;
let: "nextchild" := "v" ? 1 in
"iter" [["q", "nextchild"]].
Definition bfs_loop : val :=
μ: "loop", [["q", "out"]],
let: "b" := is_empty [["q"]] in
(if: "b" then
(* end of while loop *)
return: ()
else
let: "v" := pop_front [["q"]] in
(* do something with v, for example: *)
push_back [["out", "v"]];;
let: "children" := "v" ? 1 in
enqueue_and_visit_children [["q", "children"]]
);;
"loop" [["q", "out"]].
Definition bfs : val :=
λ: [["root"]],
let: "out" := new_queue [[]] in
let: "q" := new_queue [[]] in
push_back [["q", "root"]];;
"root" ! 0 <- ^1;;
bfs_loop [["q", "out"]];;
"out" ? 0.
Lemma bfs_loop_spec (V : list loc) (E : loc -> list loc) (visited : gmap loc bool) (q o : loc) (queue out : list loc) :
let unvisited := List.filter (fun x => negb (visited !!! x)) V in
{{{ Graph V E visited Queue (map VLoc queue) q Queue (map VLoc out) o }}}
bfs_loop [[#q, #o]]
{{{ RET (); Graph V E visited Queue (map VLoc queue) q Queue (map VLoc (out ++ fbfs_ E unvisited queue)) o }}}.
Abort.
Axiom const_gmap : forall {A} (l : list Z) (x : A), gmap Z A.
Axiom infspace : iProp Σ.
Axiom infspace_spec : forall n, infspace - infspace n.
Lemma bfs_spec V E v :
{{{ Graph V E (const_gmap V false) v V valid_graph V E infspace }}}
(* (6 + 6 * length (fbfs V E v)) *)
(* vraie complexité ~= 2 * "largeur" de l'arbre bfs? (+ length fbfs pour la sortie) *)
bfs [[#v]]
{{{ l, RET #l; List (map VLoc (fbfs V E v)) l visited, Graph V E visited }}}.
Proof.
iIntros (phi) "(g & iv & vg & dia) post".
wp_code.
iDestruct (infspace_spec 3 with "dia") as "(dia & d3)".
(* iDestruct (diamond_split 3 _ with "dia") as "(d3 & d3' & dia)"; auto. *)
wp_bind (new_queue _). iApply (new_queue_spec with "d3"). iNext. iIntros (out) "ho". wp_pures.
iDestruct (infspace_spec 3 with "dia") as "(dia & d3)".
wp_bind (new_queue _). iApply (new_queue_spec with "d3"). iNext. iIntros (q) "hq". wp_pures.
iDestruct (infspace_spec 3 with "dia") as "(dia & d3)".
(* iDestruct (diamond_split 3 12 with "dia") as "(d3 & dia)". admit. *)
wp_bind (push_back _). iApply (push_back_spec with "[d3 hq]"). iFrame. iNext. iIntros "hq". wp_pures.
Abort.
End proof.
From spacelang Require Import proofmode notation.
Lemma if_neq {l l'} : l l' -> (l =? l') = false.
Proof.
apply Z.eqb_neq.
Qed.
Ltac ifeq :=
(erewrite Z.eqb_refl; eauto)
|| erewrite (if_neq ltac:(solve[eauto]))
|| match goal with
|- context [ if ?a =? ?b then _ else _ ] =>
rewrite (@if_neq a b ltac:(solve[eauto]))
|| (let H := fresh "eq" in
destruct (Z.eq_dec a b) as [H | H];
[rewrite ->H, Z.eqb_refl; eauto | erewrite if_neq; eauto ])
end.
Section proof.
Context `{!heapG Σ}.
Axiom null : loc.
Axiom mapsto_non_null : forall l v, (l v) - l null.
Fixpoint List (L : list val) (l : loc) : iProp Σ :=
match L with
| [] => l = null
| x :: L => (l' : loc), l BTuple [x; #l'] List L l'
end%I.
Lemma List_null (L : list val) : List L null - L = [].
Proof.
iIntros "h". destruct L; auto. simpl. iDestruct "h" as (l) "(hn & _)".
iDestruct (mapsto_non_null with "hn") as %f. tauto.
Qed.
Lemma fold_List x L l l' : l BTuple [x; #l'] - List L l' - List (x :: L) l.
Proof.
simpl; iIntros "? ?". iExists l'; iFrame.
Qed.
Definition realloclist : val := (* ~= List.map (fun x -> x) i.e. non tail-rec *)
μ: "realloclist" , [["p"]] ,
let: "b" := "p" == #null in
if: "b" then
return: #null
else
let: "x" := "p" ? 0 in
let: "q" := "p" ? 1 in
let: "r" := "realloclist" [["q"]] in (** no stack cost? *)
free "p";;
init [[ "x", "r" ]].
Lemma realloclist_spec (l : loc) (L : list val) :
{{{ 0 List L l }}}
realloclist [[#l]]
{{{ l', RET #l'; List L l' }}}.
Proof.
iIntros (phi) "[dia hl] post".
iInduction L as [ | x L ] "IH" forall (phi l).
- wp_code.
iDestruct "hl" as %->.
wp_pures.
ifeq.
wp_pures.
iApply "post". auto.
- simpl.
iDestruct "hl" as (l') "(Hl & Hl')".
iDestruct (mapsto_non_null with "Hl") as %nn.
wp_code.
wp_pures.
ifeq.
wp_load.
wp_load.
wp_bind (realloclist _).
iApply ("IH" with "dia Hl'").
iNext.
iIntros (l1) "Hl1".
wp_pures.
wp_free as "[dl dia]".
wp_init l2 as "[Hl2 dia]".
iApply "post".
iExists l1. iFrame; auto.
Qed.
Definition list_map : val :=
μ: "list_map" , [["f", "p"]] ,
let: "b" := "p" == #null in
if: "b" then
return: #null
else
let: "x" := "p" ? 0 in
let: "q" := "p" ? 1 in
free "p";;
let: "y" := "f" [["x"]] in
let: "r" := "list_map" [["f", "q"]] in (** no stack cost? *)
init [[ "y", "r" ]].
Lemma list_map_spec_aux (l : loc) (L A A': list val) (f : val) :
forall (step : list val -> list val -> iProp Σ),
(forall li lo i,
{{{ step li lo }}}
f [[i]]
{{{ o, RET o; step (li ++ [i]) (lo ++ [o]) }}}) ->
{{{ 0 List L l step A A' }}}
list_map [[f, #l]]
{{{ l', RET #l'; L', step (A ++ L) (A' ++ L') List L' l' }}}.
Proof.
iIntros (step hf phi) "(_ & hl & ha) post".
iInduction L as [ | i L ] "IH" forall (phi l A A').
- wp_code.
iDestruct "hl" as %->.
wp_pures.
ifeq.
wp_pures.
iApply "post". iModIntro.
iExists []. rewrite !app_nil_r.
auto.
- simpl.
iDestruct "hl" as (l') "(Hl & Hl')".
iDestruct (mapsto_non_null with "Hl") as %nn.
wp_code.
wp_pures.
ifeq.
wp_load.
wp_load.
wp_free as "[dl ?]".
wp_bind (f _).
iApply (hf with "ha"). iNext. iIntros (o) "ha".
wp_pures.
wp_bind (list_map _).
iApply ("IH" with "Hl' ha"). clear l'. iNext.
iIntros (l') "Hl'". iDestruct "Hl'" as (L') "[ha hl']".
wp_pures.
wp_init l2 as "[Hl2 ?]".
iApply "post".
iExists (o :: L').
rewrite <-!app_assoc. iFrame.
iExists l'; iFrame; auto.
Qed.
Lemma list_map_spec (l : loc) (L : list val) (f : val) :
forall (step : list val -> list val -> iProp Σ),
(forall li lo i,
{{{ step li lo }}}
f [[i]]
{{{ o, RET o; step (li ++ [i]) (lo ++ [o]) }}}) ->
{{{ 0 List L l step [] [] }}}
list_map [[f, #l]]
{{{ l', RET #l'; L', step L L' List L' l' }}}.
Proof.
apply list_map_spec_aux.
Qed.
Definition rev_append : val :=
μ: "rev_append" , [["p", "acc"]] ,
let: "b" := "p" == #null in
if: "b" then
return: "acc"
else
let: "x" := "p" ? 0 in
let: "q" := "p" ? 1 in
free "p";;
let: "acc" := init [[ "x", "acc" ]] in
"rev_append" [["q", "acc"]].
Lemma rev_append_spec (a l : loc) (A L : list val) :
{{{ List A a List L l }}}
rev_append [[#l, #a]]
{{{ la, RET #la; List (List.rev_append L A) la }}}.
Proof.
iIntros (phi) "(ha & hl) post".
iInduction L as [ | x L ] "IH" forall (phi a l A).
- wp_code.
iDestruct "hl" as %->.
wp_pures.
ifeq.
wp_pures.
iApply "post". auto.
- simpl.
iDestruct "hl" as (l') "(hl & hl')".
iDestruct (mapsto_non_null with "hl") as %nn.
wp_code.
wp_pures.
ifeq.
wp_load.
wp_load.
wp_free as "[dl ?]".
wp_init a' as "[ha' ?]".
iAssert (List (x :: A) a')%I with "[ha ha']" as "ha'".
now iExists _; iFrame.
iApply ("IH" with "ha' hl'").
iNext.
iIntros (q) "Hq".
now iApply "post".
Qed.
Inductive tree A := leaf | node (x : A) (l r : tree A).
Arguments leaf {A}.
Arguments node {A}.
Fixpoint size_tree {A} (t : tree A) :=
(match t with
| leaf => 0
| node _ l r => 1 + size_tree l + size_tree r
end)%nat.
Fixpoint Tree (t : tree val) (l : loc) : iProp Σ :=
match t with
| leaf => l = null
| node x t1 t2 =>
(l1 l2 : loc),
l BTuple [x; #l1; #l2]
Tree t1 l1
Tree t2 l2