Commit 79ba7394 authored by charguer's avatar charguer

stack_temp

parent 9474d364
(*************************************************************************)
(** Graph representation by adjacency lists *)
......@@ -15,7 +10,7 @@ type t = (int list) array
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,9 +23,9 @@ type color = White | Gray | Black
let rec dfs_from g c i =
c.(i) <- Gray;
Graph.iter_edges (fun j ->
Graph.iter_edges g i (fun j ->
if c.(j) = White
then dfs_from g c j) g i;
then dfs_from g c j);
c.(i) <- Black
let dfs_main g rs =
......@@ -40,3 +35,49 @@ let dfs_main g rs =
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)
......@@ -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.
......@@ -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.
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment