From 79ba73940aa9c7fd5f9a13a7c72250280f8df904 Mon Sep 17 00:00:00 2001 From: charguer Date: Mon, 18 Jun 2018 18:55:08 +0200 Subject: [PATCH] stack_temp --- examples/DFS/DFS.ml | 65 +++++-- examples/DFS/DFS_proof.v | 27 +-- examples/DFS/OtherAlgo.ml | 338 ++++++++++------------------------ examples/DFS/StackDFS_proof.v | 192 +++++++++++++++++++ 4 files changed, 345 insertions(+), 277 deletions(-) create mode 100644 examples/DFS/StackDFS_proof.v diff --git a/examples/DFS/DFS.ml b/examples/DFS/DFS.ml index e248885..f8cd4d0 100644 --- a/examples/DFS/DFS.ml +++ b/examples/DFS/DFS.ml @@ -1,21 +1,16 @@ - - - - - (*************************************************************************) (** Graph representation by adjacency lists *) module Graph = struct -type t = (int list) array +type t = (int list) array -let nb_nodes (g:t) = +let nb_nodes (g:t) = Array.length g -let iter_edges (f:int->unit) (g:t) (i:int) = +let iter_edges (g:t) (i:int) (f:int->unit) = List.iter (fun j -> f j) g.(i) end @@ -28,15 +23,61 @@ type color = White | Gray | Black let rec dfs_from g c i = c.(i) <- Gray; - Graph.iter_edges (fun j -> - if c.(j) = White - then dfs_from g c j) g i; + Graph.iter_edges g i (fun j -> + if c.(j) = White + then dfs_from g c j); c.(i) <- Black let dfs_main g rs = let n = Graph.nb_nodes g in let c = Array.make n White in - List.iter (fun i -> + List.iter (fun i -> if c.(i) = White then dfs_from g c i) rs; c + + + +(*************************************************************************) +(** Minimal stack structure *) + +module Stack = struct + +type 'a t = ('a list) ref + +let create () : 'a t = + ref [] + +let is_empty (s : 'a t) = + !s = [] + +let pop (s : 'a t) = + match !s with + | [] -> assert false + | x::n -> s := n; x + +let push (x : 'a) (s : 'a t) = + s := x::!s + +end + + +(*************************************************************************) +(** DFS Algorithm, using two colors and a stack *) + +let reachable_imperative g a b = + let n = Graph.nb_nodes g in + let c = Array.make n false in + let s = Stack.create() in + c.(a) <- true; + Stack.push a s; + while not (Stack.is_empty s) do + let i = Stack.pop s in + Graph.iter_edges g i (fun j -> + if not c.(j) then begin + c.(i) <- true; + Stack.push i s; + end); + done; + c.(b) + diff --git a/examples/DFS/DFS_proof.v b/examples/DFS/DFS_proof.v index c7d9675..9dec577 100644 --- a/examples/DFS/DFS_proof.v +++ b/examples/DFS/DFS_proof.v @@ -333,7 +333,7 @@ Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i, (forall L, (g ~> RGraph G) \c (I L)) -> (forall j E, j \notin E -> has_edge G i j -> (app f [j] (I E) (# I (\{j} \u E)))) -> - app Graph_ml.iter_edges [f g i] + app Graph_ml.iter_edges [g i f] PRE (I \{}) POST (# I (out_edges G i)). Proof. @@ -630,28 +630,3 @@ Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec. - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/examples/DFS/OtherAlgo.ml b/examples/DFS/OtherAlgo.ml index fa1afbd..c79b336 100644 --- a/examples/DFS/OtherAlgo.ml +++ b/examples/DFS/OtherAlgo.ml @@ -11,7 +11,7 @@ Inv No black to white false -(* 2 <-> grays C = \{} +(* 2 <-> grays C = \{} 5 <-> i \in blacks C 6 <-> j \notin white C <-> j \in (blacks C \u grays C) *) @@ -34,8 +34,8 @@ Proof using. (* trivial *) Qed. *) -Lemma evolution_trans' : forall C2 X C1 C3, - evolution' X C1 C2 -> +Lemma evolution_trans' : forall C2 X C1 C3, + evolution' X C1 C2 -> evolution C2 C3 -> evolution' X C1 C3. Proof using. (* trivial *) @@ -50,7 +50,7 @@ Lemma no_white_in_evolution' : forall C C' X E, evolution' X C C' -> no_white_in E C'. Proof using. (* trivial *) - =>> N (H1&H2) i Hi. cases (C[i]) as Ci. + =>> N (H1&H2) i Hi. cases (C[i]) as Ci. { false* N. } { forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. } rewrite~ H1. auto_false. @@ -75,7 +75,7 @@ Lemma reachables_monotone : forall G E1 E2 F1 F2, Proof using. introv R HE HF. rewrite incl_in_eq in HE,HF. skip. Qed. - + Lemma reachables_trans : forall G E1 E2 E3, reachables G E1 E2 -> reachables G E2 E3 -> @@ -96,13 +96,13 @@ Definition grays C := Lemma iter_nodes_spec : forall (I:set int->hprop) (G:graph) g f, (forall i N, i \in nodes G -> i \notin N -> - (app f [i] (I N) (# I (\{i}\u N)))) -> + (app f [i] (I N) (# I (\{i}\u N)))) -> app iter_nodes [f g] - PRE (g ~> GraphAdj G \* I \{}) + PRE (g ~> GraphAdj G \* I \{}) POST (# g ~> GraphAdj G \* I (nodes G)). Proof. (* -- TODO -- *) -Admitted. +Admitted. Hint Extern 1 (RegisterSpec iter_nodes) => Provide iter_nodes_spec. @@ -130,9 +130,9 @@ let dfs_main g r = module GraphAdj = struct -type 'a t = ((int*'a) list) array +type 'a t = ((int*'a) list) array -let nb_nodes (g:'a t) = +let nb_nodes (g:'a t) = Array.length g let iter_edges_of (g:'a t) (i:int) (f:int->'a->unit) = @@ -171,9 +171,9 @@ end module GraphMat = struct -type 'a t = ('a array) array +type 'a t = ('a array) array -let nb_nodes (g:'a t) = +let nb_nodes (g:'a t) = Array.length g let get_edge (g:'a t) i j = @@ -201,8 +201,8 @@ let reachable_recursive g a b = let c = Array.make n White in let rec visit i = c.(i) <- Gray; - GraphAdj.iter_edges_target_of g i (fun j -> - if c.(j) = White + GraphAdj.iter_edges_target_of g i (fun j -> + if c.(j) = White then visit j); c.(i) <- Black; in @@ -213,17 +213,17 @@ let reachable_recursive g a b = (*************************************************************************) (** Reachability by imperative DFS, two-colored *) -let reachable_imperative g a b = +let reachable_imperative g a b = let n = GraphAdj.nb_nodes g in let c = Array.make n false in let s = Stack.create() in - c.(a) <- true; + c.(a) <- true; Stack.push a s; while not (Stack.is_empty s) do let i = Stack.pop s in - GraphAdj.iter_edges_target_of g i (fun j -> - if not c.(j) then begin - c.(i) <- true; + GraphAdj.iter_edges_target_of g i (fun j -> + if not c.(j) then begin + c.(i) <- true; Stack.push i s; end); done; @@ -233,7 +233,7 @@ let reachable_imperative g a b = (*************************************************************************) (** Cycle detection by recursive DFS, three-colored *) -(** Note: for simlicity, the current implementation does not exit +(** Note: for simlicity, the current implementation does not exit abruptly when detecting a cycle. *) let cycle_detection g s e = @@ -242,8 +242,8 @@ let cycle_detection g s e = let r = ref false in let rec visit i = c.(i) <- Gray; - GraphAdj.iter_edges_target_of g i (fun j -> - if c.(j) = White + GraphAdj.iter_edges_target_of g i (fun j -> + if c.(j) = White then visit j else if c.(j) = Gray then r := true); @@ -267,8 +267,8 @@ let topological_sort g s e = let k = ref (n-1) in let rec visit i = c.(i) <- processed; - GraphAdj.iter_edges_target_of g i (fun j -> - if c.(j) = neverseen + GraphAdj.iter_edges_target_of g i (fun j -> + if c.(j) = neverseen then visit j); c.(i) <- !k; decr k; @@ -281,18 +281,18 @@ let topological_sort g s e = (*************************************************************************) (** Connected components by recursive DFS, two-colored *) -let connected_recursive g = +let connected_recursive g = let n = GraphAdj.nb_nodes g in let neverseen = -1 in let c = Array.make n neverseen in let k = ref 0 in let rec visit i = c.(i) <- !k; - GraphAdj.iter_edges_target_of g i (fun j -> + GraphAdj.iter_edges_target_of g i (fun j -> if c.(j) = neverseen then visit j) in - GraphAdj.iter_nodes g (fun i -> + GraphAdj.iter_nodes g (fun i -> if c.(i) = neverseen then begin visit i; incr k @@ -307,15 +307,15 @@ let connected_recursive g = type tree = Tree of int * tree list type forest = tree list -let spanning_forest g = +let spanning_forest g = let n = GraphAdj.nb_nodes g in let c = Array.make n false in let rec build_tree i = c.(i) <- true; let ts = GraphAdj.fold_edges_target_of g i [] harvest in - Tree (i,ts) - and harvest acc i = - if c.(i) then acc else (build_tree i)::acc + Tree (i,ts) + and harvest acc i = + if c.(i) then acc else (build_tree i)::acc in GraphAdj.fold_nodes g [] harvest @@ -330,7 +330,7 @@ let connected_imperative g = let k = ref 0 in let s = Stack.create() in let find i = - c.(i) <- !k; + c.(i) <- !k; Stack.push i s in GraphAdj.iter_nodes g (fun i -> @@ -338,8 +338,8 @@ let connected_imperative g = find i; while not (Stack.is_empty s) do let i = Stack.pop s in - GraphAdj.iter_edges_target_of g i (fun j -> - if c.(j) = neverseen + GraphAdj.iter_edges_target_of g i (fun j -> + if c.(j) = neverseen then find j) done; incr k; @@ -350,7 +350,7 @@ let connected_imperative g = (*************************************************************************) (** Connected components by warshall-floyd *) -(** Note: implemented by side-effects on the adjacency matrix *) +(** Note: implemented by side-effects on the adjacency matrix *) let connected_warshall_floyd g = let n = GraphMat.nb_nodes g in @@ -370,7 +370,7 @@ let connected_warshall_floyd g = nbcompo++ foreach neighbor mark it - + *) @@ -457,7 +457,7 @@ Parameter array_to_map : forall A, array A -> map int A. (* ** TLC Graph *) Inductive is_path A (g:graph A) : int -> int -> path A -> Prop := - | is_path_nil : forall x, + | is_path_nil : forall x, x \in nodes g -> is_path g x x nil | is_path_cons : forall x y z w p, @@ -469,32 +469,32 @@ Inductive is_path A (g:graph A) : int -> int -> path A -> Prop := (********************************************************************) (* ** Stdlib Stack *) -Parameter StackOf : forall a A (T:htype A a) (L:list A) (l:loc), hprop. +Parameter StackOf : forall a A (T:htype A a) (L:list A) (l:loc), hprop. Notation "'Stack'" := (StackOf Id). Parameter ml_stack_create_spec : forall a, - Spec ml_stack_create (i:unit) |R>> + Spec ml_stack_create (i:unit) |R>> R \[] (~> Stack (@nil a)). Hint Extern 1 (RegisterSpec ml_stack_create) => Provide ml_stack_create_spec. Parameter ml_stack_is_empty_spec : forall a, - Spec ml_stack_is_empty (l:loc) |R>> + Spec ml_stack_is_empty (l:loc) |R>> forall (L:list a), keep R (l ~> Stack L) (fun b => \[b = bool_of (L = nil)]). Hint Extern 1 (RegisterSpec ml_stack_is_empty) => Provide ml_stack_is_empty_spec. Parameter ml_stack_push_spec : forall a, - Spec ml_stack_push (X:a) (l:loc) |R>> + Spec ml_stack_push (X:a) (l:loc) |R>> forall (L:list a), R (l ~> Stack L) (# l ~> Stack (X::L)). Hint Extern 1 (RegisterSpec ml_stack_push_spec) => Provide ml_stack_push_spec. Parameter ml_stack_pop_spec : forall a, - Spec ml_stack_pop (l:loc) |R>> + Spec ml_stack_pop (l:loc) |R>> forall (L:list a), L <> nil -> R (l ~> Stack L) (fun X => Hexists L', \[L = X::L'] \* l ~> Stack L'). @@ -503,7 +503,7 @@ Hint Extern 1 (RegisterSpec ml_stack_pop) => Provide ml_stack_pop_spec. (********************************************************************) (********************************************************************) (********************************************************************) -(* ** Representation predicate for unweighted graphs +(* ** Representation predicate for unweighted graphs by adjacency lists *) (** [nodes_index G n] holds if the nodes in [G] are indexed from @@ -517,8 +517,8 @@ Definition nodes_index A (G:graph A) (n:int) := Definition GraphAdjList A (G:graph A) (g:loc) := Hexists N, g ~> Array N - \* \[nodes_index G (LibArray.length N) - /\ forall i j w, i \in nodes G -> + \* \[nodes_index G (LibArray.length N) + /\ forall i j w, i \in nodes G -> Mem (j,w) (N[i]) = has_edge G i j w]. @@ -541,8 +541,8 @@ Hint Resolve @index_array_length_eq @index_make @index_update. Hint Immediate has_edge_in_nodes_l has_edge_in_nodes_r. Hint Extern 1 (nodes_index _ _) => congruence. Hint Extern 1 (index ?n ?x) => - eapply graph_adj_index; - [ try eassumption + eapply graph_adj_index; + [ try eassumption | instantiate; try eassumption | instantiate; try congruence ]. @@ -554,22 +554,22 @@ Hint Extern 1 (index ?n ?x) => Import MLGraphAdj. Ltac hdata_simpl_step ::= - match goal with |- context C [ ?l ~> ?S ] => + match goal with |- context C [ ?l ~> ?S ] => match S with (fun _ => _) => rewrite (hdata_fun' l) end end. - + Lemma nb_nodes_spec : forall A, - Spec nb_nodes g |R>> + Spec nb_nodes g |R>> forall (G:graph A), keep R (g ~> GraphAdjList G) (fun n => \[nodes_index G n]). Proof. xcf. instantiate (1:=A). (* todo: fix instantiation *) intros. unfold GraphAdjList. hdata_simpl. - xextract as N [GI GN]. xapp. hsimpl~. + xextract as N [GI GN]. xapp. hsimpl~. Admitted. (*faster*) Hint Extern 1 (RegisterSpec nb_nodes) => Provide nb_nodes_spec. @@ -587,38 +587,38 @@ Parameter out_edges_target_has_edge : forall (G:graph unit) i j, Parameter ml_list_iter_spec' : forall a, Spec ml_list_iter f l |R>> forall (I:list a->hprop), - (forall x t, (App f x;) (I t) (# I (t&x))) -> + (forall x t, (App f x;) (I t) (# I (t&x))) -> R (I nil) (# I l). -Lemma iter_edges_target_of_spec : - Spec iter_edges_target_of g i f |R>> +Lemma iter_edges_target_of_spec : + Spec iter_edges_target_of g i f |R>> forall (G:graph unit) (I:set int->hprop), i \in nodes G -> (forall j js, has_edge G i j tt -> j \notin js -> - (App f j;) (I js) (# I (\{j} \u js))) -> - R (g ~> GraphAdjList G \* I \{}) + (App f j;) (I js) (# I (\{j} \u js))) -> + R (g ~> GraphAdjList G \* I \{}) (# g ~> GraphAdjList G \* I (out_edges_target G i)). Proof. (*---TODO--- xcf. introv Gi Sf. (* todo: fix instantiation *) - unfold GraphAdjList. hdata_simpl. xextract as N [GI GN]. + unfold GraphAdjList. hdata_simpl. xextract as N [GI GN]. xfun_mg. xapps*. xapp_spec ml_list_iter_spec' (fun l:list(int*unit) => I (List.map fst l)). - intros [j w] t. simpls. eapply S_f0. + intros [j w] t. simpls. eapply S_f0. intros_all. applys H0. applys H. (* todo: xbody/xisspec *) - clear j w. intros [j w]. xcase. + clear j w. intros [j w]. xcase. --- TODO ---*) -Admitted. +Admitted. Hint Extern 1 (RegisterSpec iter_edges_target_of) => Provide iter_edges_target_of_spec. (* Another similar one talking about remaining edges *) -Lemma iter_edges_target_of_spec' : - Spec iter_edges_target_of g i f |R>> +Lemma iter_edges_target_of_spec' : + Spec iter_edges_target_of g i f |R>> forall (G:graph unit) (I:set int->hprop), i \in nodes G -> (forall j js, has_edge G i j tt -> j \notin js -> - (App f j;) (I (\{j} \u js)) (# I js)) -> - R (g ~> GraphAdjList G \* I (out_edges_target G i)) + (App f j;) (I (\{j} \u js)) (# I js)) -> + R (g ~> GraphAdjList G \* I (out_edges_target G i)) (# g ~> GraphAdjList G \* I \{}). Admitted. @@ -626,16 +626,16 @@ Admitted. -Lemma iter_nodes_spec : - Spec iter_nodes g f |R>> - forall (G:graph unit) (I:set int->hprop), +Lemma iter_nodes_spec : + Spec iter_nodes g f |R>> + forall (G:graph unit) (I:set int->hprop), (forall i N, i \in nodes G -> i \notin N -> - (App f i;) (I N) (# I (\{i}\u N))) -> - R (g ~> GraphAdjList G \* I \{}) + (App f i;) (I N) (# I (\{i}\u N))) -> + R (g ~> GraphAdjList G \* I \{}) (# g ~> GraphAdjList G \* I (nodes G)). Proof. (* -- TODO -- *) -Admitted. +Admitted. Hint Extern 1 (RegisterSpec iter_nodes) => Provide iter_nodes_spec. @@ -649,31 +649,31 @@ Implicit Types G : graph unit. Definition undirected G := forall i j, has_edge G i j tt -> has_edge G j i tt. -Definition reachable G i j := +Definition reachable G i j := exists p, is_path G i j p. Definition cyclic G := exists p i, is_path G i i p. Definition topological_order G L := - dom L = nodes G - /\ img L = range 0 (card (nodes G)) + dom L = nodes G + /\ img L = range 0 (card (nodes G)) /\ forall i j, reachable G i j -> L[i] < L[j]. Definition topological_order_one_step G L := - dom L = nodes G - /\ img L = range 0 (card (nodes G)) + dom L = nodes G + /\ img L = range 0 (card (nodes G)) /\ forall i j, has_edge G i j tt -> L[i] < L[j]. Definition connected_components G L := - exists k, - dom L = nodes G + exists k, + dom L = nodes G /\ img L = range 0 k /\ forall i j, reachable G i j <-> L[i] = L[j]. Definition strongly_connected_components G L := - exists k, - dom L = nodes G + exists k, + dom L = nodes G /\ img L = range 0 k /\ forall i j, (reachable G i j /\ reachable G j i) <-> L[i] = L[j]. @@ -683,7 +683,7 @@ Definition strongly_connected_components G L := (********************************************************************) -(** * Reachability by recursive DFS, three-colored +(** * Reachability by recursive DFS, three-colored -- DEPRECATED Definition reachable_iff_black G s C := @@ -693,13 +693,13 @@ Definition not_white_reachable G s C := forall i, i \in nodes G -> C[i] <> White -> reachable G s i. Definition black_no_white_neighbour G C := - forall i j, i \in nodes G -> C[i] = Black -> + forall i j, i \in nodes G -> C[i] = Black -> has_edge G i j tt -> C[j] <> White. -Record inv G n s C := { +Record inv G n s C := { inv_length_C : length C = n; - inv_not_white_reachable : not_white_reachable G s C; + inv_not_white_reachable : not_white_reachable G s C; inv_black_no_white_neighbour : black_no_white_neighbour G C }. Definition hinv g c (N:array (list int)) G n s C := @@ -718,32 +718,32 @@ Definition fewer_white := Lemma reachable_rec_spec : Spec reachable_rec g s |R>> forall G, s \in nodes G -> R (g ~> GraphAdjList G) - (fun (c:loc) => Hexists (C:array color), + (fun (c:loc) => Hexists (C:array color), g ~> GraphAdjList G \* c ~> Array C \* [reachable_iff_black G s C]). Proof. xcf. introv Gs. unfold GraphAdjList at 1. hdata_simpl. xextract as N Neg Adj. - xapp. intros Gn. xapps. + xapp. intros Gn. xapps. xfun_induction_heap_nointro (fun f => Spec f i |R>> forall C, - i \in nodes G -> C[i] = White -> + i \in nodes G -> C[i] = White -> R (hinv g c N G n s C) - (# Hexists C', hinv g c N G n s C' \* + (# Hexists C', hinv g c N G n s C' \* [same_gray G C C' /\ no_more_white G C' C /\ C'[i] = Black])) fewer_white. unfold hinv. intros i C0 IH Gi Ci. hide IH. xextract as I0. lets Cn0: inv_length_C I0. xapp*. xfun f. simpls. xapps*. - xapp_spec ml_list_iter_spec' (fun L => - Hexists C, hinv g c N G n s C + xapp_spec ml_list_iter_spec' (fun L => + Hexists C, hinv g c N G n s C \* [Forall (fun j => j \in nodes G /\ C[j] <> White) L /\ no_more_white G C C0]). - Focus 1. + Focus 1. intros j L' Lx. unfold hinv. xextract as C I [HL' F]. lets [Cn I1 I2]: I. xapp_body. intro. intro_subst. rewrite* Adj in Lx. xapps*. xif. - xapp*. + xapp*. skip. (* decrease *) hextract as C'. intros I' (SG&SW&C'j). lets [Cn' I1' I2']: I'. - hsimpl~. splits*. + hsimpl~. splits*. applys* Forall_last. applys* Forall_weaken HL'. intros k (Gk&Ck). split~. applys* SW. split*. congruence. @@ -758,7 +758,7 @@ Proof. xapp* (make n White). skip. (* ok *) unfold hinv. hsimpl. skip. (* inv init *) - introv (SW&?&?). xret. unfold hinv. + introv (SW&?&?). xret. unfold hinv. unfold GraphAdjList at 1. hdata_simpl. hextract as [_ SW' SG']. hsimpl*. unfolds. unfolds in SW'. @@ -780,7 +780,7 @@ Admitted. Definition GraphMatrix (G:graph unit) (g:loc) := Hexists (N:array (array bool)), g ~> Array N - \* \[exists n, n = LibArray.length N + \* \[exists n, n = LibArray.length N /\ (forall (x:int), x \in nodes G -> n = LibArray.length (N[x])) /\ (forall (x y:int), x \in nodes G -> y \in nodes G -> N[x][y] = isTrue (has_edge G x y tt))]. @@ -789,17 +789,17 @@ Definition GraphMatrix (G:graph unit) (g:loc) := -let reachable_imperative g a b = +let reachable_imperative g a b = let n = GraphAdj.nb_nodes g in let c = Array.make n false in let s = Stack.create() in - c.(a) <- true; + c.(a) <- true; Stack.push a s; while not (Stack.is_empty s) do let i = Stack.pop s in - GraphAdj.iter_edges_target_of g i (fun j -> - if not c.(j) then begin - c.(i) <- true; + GraphAdj.iter_edges_target_of g i (fun j -> + if not c.(j) then begin + c.(i) <- true; Stack.push i s; end); done; @@ -809,143 +809,3 @@ let reachable_imperative g a b = (********************************************************************) (** * Reachability by imperative DFS, two-colored *) - - -(* Note: [E] describes set of edges left to process in the loop *) - -Record inv (G:graph unit) n a (C:array bool) L (E:set int) := { - inv_length_C : length C = n; - inv_source : C[a] = true; - inv_stack : forall i, Mem i L -> i \in nodes G /\ C[i] = true; - inv_true_reachable : forall i, i \in nodes G -> - C[i] = true -> reachable G a i; - inv_true_edges : forall i j, - C[i] = true -> has_edge G i j tt -> - Mem i L \/ C[j] = true \/ j \in E }. - -Lemma inv_init : forall G n a C, - C = LibArray.make n false -> a \in nodes G -> - inv G n a (C[a:=true]) (a :: nil) \{}. -Proof. - introv EC Ga. constructors. - skip. - skip. - introv H. inverts H as H. skip. inverts H. - introv Gi H. skip_rewrite (i = a). - exists (nil:path unit). constructors*. - introv Ci E. skip_rewrite (i = a). left*. -Qed. - - -Lemma inv_step_push : forall G n a C L i j js, - inv G n a C L ('{j} \u js) -> - C[i] = true -> has_edge G i j tt -> - inv G n a (C[i:=true]) (i :: L) js. -Proof. - introv I Ci M. inverts I. constructors; auto. - skip. - intros i' M'. skip. - skip. (* extend path with edge at end *) - intros i' j' Ci' E. - (* two cases: i is i' or not. If so, wrote true *) - skip. -Qed. - - -Lemma inv_step_skip : forall G n a C L j js, - inv G n a C L ('{j} \u js) -> C[j] = true -> - inv G n a C L js. -Proof. - introv I Cj. inverts I. constructors; auto. - intros i' j' Ci' E. - lets [M|[M|M]]: inv_true_edges0 Ci' E; [ eauto | eauto | ]. - set_in M; eauto. -Qed. - -Lemma inv_end : forall G n a C, - inv G n a C nil \{} -> - forall j, j \in nodes G -> - (reachable G a j <-> C[j] = true). -Proof. - introv I Gj. iff H. - destruct H as [p P]. lets PC: inv_source I. gen P PC. - generalize a as i. intros i P. induction P. - auto. - introv Cx. destruct w. lets [M|[M|M]]: inv_true_edges I Cx H. - inverts M. - auto. - inverts M. - applys* inv_true_reachable. -Qed. - - -Parameter ml_stack_is_empty_spec : forall a, - Spec ml_stack_is_empty (l:loc) |R>> - forall (L:list a), - keep R (l ~> Stack L) (fun b => \[b = isTrue (L = nil)]). - -Hint Extern 1 (RegisterSpec ml_stack_is_empty) => Provide ml_stack_is_empty_spec. - - -Ltac fix_boolof := fix_bool_of_known tt. - -Lemma reachable_imperative_spec : - Spec reachable_imperative g a b |R>> - forall G, a \in nodes G -> b \in nodes G -> - keep R (g ~> GraphAdjList G) (fun r => \[r = isTrue (reachable G a b)]). -Proof. - xcf. instantiate (1:=unit). introv Ga Gb. - xapp. intros Gn. xapp. intros C0 HC0. - xapp. xapp*. xseq. xapp. - set (hinv := fun E CL => - let '(C,L) := CL in - g ~> GraphAdjList G - \* c ~> Array C - \* s ~> Stack L - \* \[inv G n a C L E]). - set (W := lexico2 (binary_map (count (= true)) (upto n)) - (binary_map (fun L:list int => LibList.length L) (downto 0))). - set (K := (fun CL => bool_of (let '(C,L) := CL : array bool * list int in - L <> nil))). - xseq (# Hexists C, hinv \{} (C,nil)). - xwhile_inv W (hinv \{}) K. - skip. (* well_founded W *) - unfold hinv. - evar (X:array bool); evar (Y:list int); exists (X,Y); subst X Y. - hsimpl. apply* inv_init. - intros [C L]. splits. - unfold hinv. xextract as I. xlet. xapps. simpl. - (* todo: cleanup*) xextract. intro_subst. xret. - hsimpl*. unfold K. fix_boolof. rew_reflect*. - xextract as HK I. unfolds in HK. fix_boolof. - xapp*. intros L' HL'. subst L. clear HK. - xfun f. forwards~ [Gi Ci]: inv_stack I i. - xapp_spec* iter_edges_target_of_spec' (fun E => Hexists CL, hinv E CL). - introv E N. xapp_body. clear Sf. intros ?. intro_subst. - clears W K C. clears L'. unfold hinv at 1. xextract. intros [C L]. xextract as I. - xapps. skip. xif. - xapp*. skip. xapp. unfold hinv. hsimpl (C[i:=true],i::L). - applys inv_step_push. eauto. skip. (* come from pop of L' *) eauto. - xret. unfold hinv. hsimpl (C,L). apply* inv_step_skip. - skip. (* ?? - unfold hinv. hsimpl (C,L'). hsimpl. *) - hextract as CL HCL. hsimpl CL. - skip. (* termination. *) - unfold K. xextracts. hsimpl*. - clear hinv K W. intros C I. lets: inv_length_C I. - xapp*. hsimpl. - forwards R: inv_end I Gb. subst r. extens. rew_reflect*. -Admitted. (* faster *) - -End ReachableImp. - -(* Another similar one talking about remaining edges *) - -Lemma iter_edges_target_of_spec' : - Spec iter_edges_target_of g i f |R>> - forall (G:graph unit) (I:set int->hprop), i \in nodes G -> - (forall j js, has_edge G i j tt -> j \notin js -> - (App f j;) (I (\{j} \u js)) (# I js)) -> - R (g ~> GraphAdjList G \* I (out_edges_target G i)) - (# g ~> GraphAdjList G \* I \{}). -Admitted. diff --git a/examples/DFS/StackDFS_proof.v b/examples/DFS/StackDFS_proof.v new file mode 100644 index 0000000..6277d67 --- /dev/null +++ b/examples/DFS/StackDFS_proof.v @@ -0,0 +1,192 @@ +Set Implicit Arguments. +Require Import CFML.CFLib. +Require Import DFS_ml. +Require Import Stdlib. +Require Import TLC.LibListZ. +Require Import Array_proof. +Require Import List_proof. +Require Import DFS_proof. +Open Scope tag_scope. + + +(*************************************************************************) +(** Verification of a minimal stack *) + +Module Import Stack_proof. +Import Stack_ml. + +Definition Stack A (L:list A) (p:loc) := + p ~~> L. + +Lemma create_spec : forall A, + app create [tt] + PRE \[] + POST (fun p => p ~> Stack (@nil A)). +Proof using. xcf_go. Qed. + +Hint Extern 1 (RegisterSpec create) => Provide create_spec. + +Lemma is_empty_spec : forall A (L:list A) (p:loc), + app is_empty [p] + INV (p ~> Stack L) + POST (fun b => \[b = isTrue (L = nil)]). +Proof using. xcf_go*. xpolymorphic_eq. (* todo: automate *) Qed. + +Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec. + +Lemma pop_spec : forall A (L:list A) (p:loc), + L <> nil -> + app pop [p] + PRE (p ~> Stack L) + POST (fun x => Hexists L', \[L = x::L'] \* p ~> Stack L'). +Proof using. xcf_go*. Qed. + +Hint Extern 1 (RegisterSpec pop) => Provide pop_spec. + +Lemma push_spec : forall A (L:list A) x p, + app push [x p] + PRE (p ~> Stack L) + POST (# p ~> Stack (x::L)). +Proof using. xcf_go*. Qed. + +Hint Extern 1 (RegisterSpec push) => Provide push_spec. + +End Stack_proof. + + +(*************************************************************************) +(** Proof of DFS with a stack *) + +(* Note: [E] describes set of edges left to process in the loop *) + +(* - [L] describes the contents of the stack + - [a] describes the source + - [n] describes the number of nodes in [G] + - [E] describes a set of vertices: the neighbors of the currently processed vertex *) + +Record inv (G:graph) (n:int) (a:int) (C:list bool) (L:list int) (E:set int) := { + inv_length_C : length C = n; + inv_source : C[a] = true; + inv_stack : forall i, mem i L -> i \in nodes G /\ C[i] = true; + inv_true_reachable : forall i, i \in nodes G -> + C[i] = true -> reachable G a i; + inv_true_edges : forall i j, + C[i] = true -> has_edge G i j -> + mem i L \/ C[j] = true \/ j \in E }. + +Lemma inv_init : forall G n a C, + C = LibListZ.make n false -> + a \in nodes G -> + inv G n a (C[a:=true]) (a :: nil) \{}. +Proof. + introv EC Ga. constructors. + { skip. } + { skip. } + { introv H. inverts H as H. skip. inverts H. } + { introv Gi H. skip_rewrite (i = a). + exists (nil:path). constructors*. } + { introv Ci E. skip_rewrite (i = a). left*. } +Qed. + +Lemma inv_step_push : forall G n a C L i j js, + inv G n a C L ('{j} \u js) -> + C[i] = true -> + has_edge G i j -> + inv G n a (C[i:=true]) (i :: L) js. +Proof. + introv I Ci M. inverts I. constructors. + { skip. } + { skip. } + { intros i' M'. skip. } + { skip. (* extend path with edge at end *) } + { intros i' j' Ci' E. + (* two cases: i is i' or not. If so, wrote true *) + skip. } +Qed. + +Lemma inv_step_skip : forall G n a C L j js, + inv G n a C L ('{j} \u js) -> + C[j] = true -> + inv G n a C L js. +Proof. + introv I Cj. inverts I. constructors; auto. + { intros i' j' Ci' E. + lets [M|[M|M]]: inv_true_edges0 Ci' E; [ eauto | eauto | ]. + rew_set in M. destruct~ M. subst*. } +Qed. + +Lemma inv_end : forall G n a C, + inv G n a C nil \{} -> + forall j, j \in nodes G -> + (reachable G a j <-> C[j] = true). +Proof. + introv I Gj. iff H. + { destruct H as [p P]. lets PC: inv_source I. gen P PC. + generalize a as i. intros i P. induction P. + { auto. } + { introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H. + { inverts M. } + { auto. } + { inverts M. } } } + { applys* inv_true_reachable. } +Qed. + +Lemma reachable_imperative_spec : forall g G a b, + a \in nodes G -> + b \in nodes G -> + app reachable_imperative [g a b] + INV (g ~> RGraph G) + POST (fun (r:bool) => \[r = isTrue (reachable G a b)]). +Proof. + introv Ga Gb. xcf. + xapp. intros Gn. xapp. { skip. (* index *) } + intros C0 HC0. + xapp. xapp*. xseq. xapp. + set (hinv := fun E CL => + let '(C,L) := CL in + g ~> RGraph G + \* c ~> Array C + \* s ~> Stack L + \* \[inv G n a C L E]). + (* TODO: fix termination + set (W := lexico2 (binary_map (count (= true)) (upto n)) + (binary_map (fun L:list int => LibList.length L) (downto 0))). *) + set (K := (fun CL => bool_of (let '(C,L) := CL : array bool * list int in + L <> nil))). + xseq (# Hexists C, hinv \{} (C,nil)). + xwhile_inv_skip (fun (b:bool) => Hexists C L, hinv \{} (C,L) \* \[b = isTrue (L<>nil)]). + (* TODO: xwhile_inv_basic (hinv \{}) W *) + { unfold hinv. + evar (X:list bool); evar (Y:list int); hsimpl (X,Y); subst X Y; eauto. + apply* inv_init. } + { intros S LS r HS. xpull ;=> C L I Er. (* TODO: why is hinv unfolded ?*) + (* while condition *) + xlet. xapps. xret. xpull ;=> E. + (* todo: simplify E *) + xif. + { (* case loop step *) + xseq. xapp*. intros L' HL'. subst L. + xfun as f. forwards~ [Gi Ci]: inv_stack I i. + xapp (fun E => Hexists CL, hinv E CL) G. + { auto. } + { unfold hinv. intros. skip. (* applys heap_contains_intro. *) } + { introv N Hij. xpull. intros (C2&L2). xapp_spec Sf. + skip. (* loop *) } + { skip. (* unfold hinv. hsimpl (C,L'). *) } + { skip. } + { skip. (* xapplys HS. *) } + (* Notes... + { intros E. xapp_body. clear Sf. intros ?. intro_subst. + clears W K C. clears L'. unfold hinv at 1. xextract. intros [C L]. xextract as I. + xapps. skip. xif. + xapp*. skip. xapp. unfold hinv. hsimpl (C[i:=true],i::L). + applys inv_step_push. eauto. skip. (* come from pop of L' *) eauto. + xret. unfold hinv. hsimpl (C,L). apply* inv_step_skip. *) + } + { (* case loop end *) + xret. subst L. hsimpl*. { rew_bool_eq*. } } } + { intros r. hpull ;=> C L E. rew_bool_eq in *. subst L. hsimpl C. } + { clear hinv K. intros C I. lets: inv_length_C I. + xapp*. hsimpl. skip. (* TODO affine *) + forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. } +Admitted. -- GitLab