StackDFS_proof.v 7.39 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
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.

21 22 23 24 25 26 27 28 29
Lemma affine_Stack : forall A p (L: list A),
  affine (p ~> Stack L).
Proof.
  intros. unfold Stack, hdata. affine.
Qed.

(* Hint Resolve affine_Stack : affine. *)
(* Transparency issues... FIXME? *)

charguer's avatar
charguer committed
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
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 *)

71
(* - [L] describes the contents of the stack
charguer's avatar
charguer committed
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
   - [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,
87 88
  index a n ->
  C = LibListZ.make n false ->
charguer's avatar
charguer committed
89 90 91
  a \in nodes G ->
  inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
92 93 94 95 96 97 98 99 100 101 102 103
  introv Ha EC Ga. constructors.
  { subst C. rew_array~. destruct~ Ha. }
  { rew_array. case_if~. subst C. apply~ index_make. }
  { introv H. inverts H as H.
    { splits~. rew_array~. case_if~. }
    { inverts H. } }
  { introv Gi H. assert (i = a) as ->.
    { subst C. rew_array~ in H. case_if~. }
    exists (nil:path). constructors*. }
  { introv Ci E. assert (i = a) as ->.
    { subst C. rew_array~ in Ci. case_if~. }
    left*. }
charguer's avatar
charguer committed
104 105 106
Qed.

Lemma inv_step_push : forall G n a C L i j js,
107
  inv G n a C L (js \u \{j}) ->
108
  C[i] = true ->
charguer's avatar
charguer committed
109
  has_edge G i j ->
110
  inv G n a (C[j:=true]) (j :: L) js.
charguer's avatar
charguer committed
111 112
Proof.
  introv I Ci M. inverts I. constructors.
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
  { rew_array~. }
  { rew_array~. case_if~. }
  { intros i' M'. rew_listx in M'. destruct M' as [-> | M'].
    - splits. now applys~ (>> has_edge_nodes i j). rew_array~. case_if~.
    - rew_array~. case_if~. splits~. subst i'. applys~ has_edge_nodes i j. }
  { intros k Hk Ck. rew_array~ in Ck. case_if~. subst k.
    forwards~ Ri: inv_true_reachable0 i. { applys~ has_edge_nodes i j. }
    skip. (* use rtclosure from LibRelation *) }
  { intros i' j' Ci' E.
    rewrite read_update_case in Ci' by skip.
    case_if~. { subst i'. rew_listx~. }
    forwards~ [H|[H|H]]: inv_true_edges0 i' j'.
    - rew_array~. case_if~.
    - rew_set in H. branches; auto_tilde. subst j'.
      rewrite~ read_update_same. }
charguer's avatar
charguer committed
128 129 130
Qed.

Lemma inv_step_skip : forall G n a C L j js,
131
  inv G n a C L (js \u \{j}) ->
charguer's avatar
charguer committed
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
  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.

157 158 159 160 161 162 163 164
Lemma inv_step_pop : forall G n a C i L,
  inv G n a C (i :: L) \{} ->
  inv G n a C L (out_edges G i).
Proof.
  introv I. destruct I. constructors~.
  intros i' j ? ?.
  forwards~ [M|[M|M]]: inv_true_edges0 i' j.
  rew_listx in M. branches; try tauto. subst i'.
charguer's avatar
charguer committed
165
  right. right. rewrite~ out_edges_has_edge.
166 167
Qed.

168

charguer's avatar
charguer committed
169
Lemma reachable_imperative_spec : forall g G a b,
170
  a \in nodes G ->
charguer's avatar
charguer committed
171 172
  b \in nodes G ->
  app reachable_imperative [g a b]
173
    INV (g ~> RGraph G)
charguer's avatar
charguer committed
174 175 176
    POST (fun (r:bool) => \[r = isTrue (reachable G a b)]).
Proof.
  introv Ga Gb. xcf.
177
  xapp. intros Gn. xapp. { unfold nodes_index in Gn. math. }
charguer's avatar
charguer committed
178 179
  intros C0 HC0.
  xapp. xapp*. xseq. xapp.
180
  set (hinv := fun E C L =>
charguer's avatar
charguer committed
181 182 183 184 185 186 187
       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))). *)
188 189 190 191 192 193
  set (K := (fun (C: array bool) (L: list int) => bool_of (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. hsimpl~. apply* inv_init. }
  { intros S LS r HS. unfold hinv at 1. xpull ;=> C L I Er.
charguer's avatar
charguer committed
194
    (* while condition *)
195
    xlet. xapps. xret. xpull ;=> E.
charguer's avatar
charguer committed
196 197 198
    (* todo: simplify E *)
    xif.
    { (* case loop step *)
199 200 201
       xseq (Hexists C L, hinv \{} C L).
       xapp*. intros L' HL'. subst L.
       xfun as f. forwards~ [Gi Ci]: inv_stack I i.
202 203
       xapp_spec iter_edges_remaining_spec
         (>> (fun E => Hexists C2 L2, hinv E C2 L2 \* \[ C2[i] = true ]) G).
charguer's avatar
charguer committed
204
       { auto. }
charguer's avatar
charguer committed
205 206 207
       { intros L. unfold hinv. applys heap_contains_intro (Hexists C2 L2,
           c ~> Array C2 \* s ~> Stack L2 \*
           \[ inv G n a C2 L2 L] \* \[ C2[i] = true]); hsimpl*. }
208 209 210 211 212 213
       { introv N Hij. xpull. intros C2 L2 ?. xapp_spec Sf.
         unfold hinv at 1. xpull. intros I'.
         xapps. skip.
         xif.
         { xapps. skip. xapp. intros _. unfold hinv. hsimpl.
           { rewrite read_update_case. case_if~. skip. }
214 215 216
           applys~ inv_step_push i. }
         { xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } }
       { unfold hinv. hsimpl. apply~ inv_step_pop. }
217
       { rew_bool_eq~. }
218
       { hsimpl. }
219
       { intros C2 L2. xapplys~ HS. } }
charguer's avatar
charguer committed
220
    { (* case loop end *)
221
      xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
charguer's avatar
charguer committed
222
  { intros r. hpull ;=> C L E. rew_bool_eq in *. subst L. hsimpl C. }
223 224
  { unfolds hinv. clear hinv K. intro C. xpull. intros I. lets: inv_length_C I.
    xapp*. hsimpl. apply affine_Stack.
charguer's avatar
charguer committed
225
    forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. }
226
Admitted.