StackDFS_proof.v 10.1 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 21 22 23 24 25 26 27 28 29 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 71 72 73 74 75 76
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 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? *)

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) := {
77
  inv_nodes_index : nodes_index G n;
charguer's avatar
charguer committed
78
  inv_length_C : length C = n;
79
  inv_source_node : a \in nodes G;
charguer's avatar
charguer committed
80 81 82 83 84 85 86 87
  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 }.

88 89 90 91 92 93 94 95
Lemma inv_index : forall G n a C L E i,
  i \in nodes G ->
  inv G n a C L E ->
  index C i.
Proof. introv Hi I. destruct* I. Qed.

Hint Resolve inv_index.

charguer's avatar
charguer committed
96
Lemma inv_init : forall G n a C,
97
  nodes_index G n ->
charguer's avatar
charguer committed
98 99 100 101 102 103 104
  C = LibListZ.make n false ->
  a \in nodes G ->
  inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
  (* Ici il faudrait pousser une version spécialisée du lemme [mem_one_eq] (?),
     qui dit [mem i (a::nil) = (i = a)], à utiliser dans les branches.
     Ou alors, s'appuyer sur [rew_listx] qui devrait faire cette réécriture. *)
105 106 107
  introv Gn EC Ga. constructors~.
  { subst C. rew_array*. destruct* Gn. (* should be auto *) }
  { rew_array*. case_if~. }
charguer's avatar
charguer committed
108
  { introv H. inverts H as H.
109
    { splits~. rew_array*. case_if~.
charguer's avatar
charguer committed
110 111 112 113 114 115 116 117 118 119
      (* il faudrait introduire une tactique qui fait
         [rew_array; repeat case_if], mais avec la subtilité
         que ça ne fait [case_if] que sur le [if] introduit
         par les [read_update] sur les tableaux. On peut coder
         ça en utilisant une base de hint différentes que rew_array,
         et une marque identité qu'une variante de [case_if] pourrait
         reconnaitre spécifiquement. On peut, en option, avoir une
         variante qui effectue des [subst] sur les égalités générées
         par [case_if] *) }
    { inverts H. } }
120 121
  { introv Gi H.
    assert (i = a) as ->.
122
    { subst C. rew_array* in H. case_if~.
charguer's avatar
charguer committed
123
      (* idem, c'est un [rew_array;case_if] *) }
124
    applys~ reachable_self. }
charguer's avatar
charguer committed
125
  { introv Ci E. assert (i = a) as ->.
126
    { subst C. rew_array* in Ci. case_if~. }
127
    autos. }
charguer's avatar
charguer committed
128 129 130 131 132 133 134 135
Qed.

Lemma inv_step_push : forall G n a C L i j js,
  inv G n a C L (js \u \{j}) ->
  C[i] = true ->
  has_edge G i j ->
  inv G n a (C[j:=true]) (j :: L) js.
Proof.
136
  introv I Ci M. lets I': I. inverts I. constructors~.
charguer's avatar
charguer committed
137
  { rew_array~. }
138
  { rew_array*. case_if~. }
charguer's avatar
charguer committed
139
  { intros i' M'. rew_listx in M'. destruct M' as [-> | M'].
140
    - splits*. rew_array*. case_if~.
141 142
    - forwards~ (?&?): inv_stack0 i'. rew_array*. case_if~. }
  { intros k Hk Ck. rew_array* in Ck. case_if~. subst k.
143
    applys* reachable_trans_edge i. }
144
  { intros i' j' Ci' E. rew_array*. case_if~. tests~: (i' = j).
charguer's avatar
charguer committed
145
    forwards~ [H|[H|H]]: inv_true_edges0 i' j'.
146
    - rew_array* in Ci'. case_if~.
147
    - rew_set in H. branches; autos. }
charguer's avatar
charguer committed
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
Qed.

Lemma inv_step_skip : forall G n a C L j js,
  inv G n a C L (js \u \{j}) ->
  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*. (* set_in M devrait faire ça *) }
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. }
170
     { introv Cx. lets [M|[M|M]]: inv_true_edges I Cx H; rew_listx~ in M. } }
charguer's avatar
charguer committed
171 172 173 174 175 176 177 178
  { applys* inv_true_reachable. }
Qed.

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~.
179
  { intros i' j Ci' E.
charguer's avatar
charguer committed
180 181 182 183
    forwards~ [M|[M|M]]: inv_true_edges0 i' j.
    (* il faudrait peut être que je définisse une tactic
       [forwards_branches M: inv_true_edges0 i' j] qui évite
      de se taper le intro_pattern tout moche *)
184
    rew_listx in M. branches; autos*. }
charguer's avatar
charguer committed
185 186
Qed.

187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
Definition measure C (L: list int) :=
  count (= false) C + length L.

(* FIXME: lemmas about read and update are inconsistent.
   For example:
   - there is LibListZ.read_succ, but not LibListZ.update_succ
     (only LibList.update_succ)
   - there is read_cons_case, but not update_cons_case,
     only update_cons_pos *)
Lemma count_update_remove : forall A `{Inhab A} (P: A -> Prop) L i x,
  index L i ->
  P L[i] ->
  ~ P x ->
  count P L[i:=x] = count P L - 1.
Proof.
  induction L; introv Ii PLi Px.
  - destruct Ii. rew_list* in *.
  - tests: (i = 0).
    { rewrite read_zero in PLi. rewrite update_zero.
      rewrite !count_cons. repeat case_if*. }
    { rewrite read_cons_case in PLi. case_if~.
      rewrite index_eq_inbound, length_cons in Ii.
      rewrite* update_cons_pos. rewrite !count_cons. case_if~.
      { rewrite* IHL. rewrite* index_eq_inbound. }
211
      { rewrite* IHL. rewrite* index_eq_inbound. } }
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
Qed.

Lemma measure_step : forall C L i,
  index C i ->
  C[i] = false ->
  measure C[i:=true] (i :: L) = measure C L.
Proof.
  introv Ii Ci. unfold measure. rew_listx.
  erewrite~ count_update_remove. math.
Qed.

Lemma measure_nonneg : forall C L,
  0 <= measure C L.
Proof.
  intros. unfold measure.
  forwards: count_nonneg (= false) C.
  forwards*: length_nonneg L.
Qed.

charguer's avatar
charguer committed
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
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. { unfold nodes_index in Gn. math. }
  intros C0 HC0.
  xapp. xapp*. xseq. xapp.
  set (hinv := fun E C L =>
       g ~> RGraph G
    \* c ~> Array C
    \* s ~> Stack L
    \* \[inv G n a C L E]).
  set (K := (fun (C: array bool) (L: list int) => bool_of (L <> nil))).
  xseq (# Hexists C, hinv \{} C nil).
249 250 251 252 253
  xwhile_inv (fun (b:bool) (m:int) =>
    Hexists C L, hinv \{} C L \*
    \[b = isTrue (L<>nil)] \*
    \[m = measure C L]
  ) (downto 0).
charguer's avatar
charguer committed
254
  { unfold hinv. hsimpl~. apply* inv_init. }
255
  { intros S LS r m HS. unfold hinv at 1. xpull ;=> C L I Er Em.
charguer's avatar
charguer committed
256 257 258 259 260
    (* while condition *)
    xlet. xapps. xret. xpull ;=> E.
    (* todo: simplify E *)
    xif.
    { (* case loop step *)
261
       xseq (Hexists C' L', hinv \{} C' L' \* \[ measure C' L' < measure C L ]).
charguer's avatar
charguer committed
262 263
       xapp*. intros L' HL'. subst L.
       xfun as f. forwards~ [Gi Ci]: inv_stack I i.
264 265 266 267 268 269
       xapp_spec~ iter_edges_remaining_spec
         (>> (fun E =>
                Hexists C2 L2, hinv E C2 L2 \*
                \[ C2[i] = true ] \*
                \[ measure C2 L2 = measure C L'])
             G).
charguer's avatar
charguer committed
270 271
       { intros L. unfold hinv. applys heap_contains_intro (Hexists C2 L2,
           c ~> Array C2 \* s ~> Stack L2 \*
272 273 274
           \[ inv G n a C2 L2 L] \* \[ C2[i] = true]
           \* \[ measure C2 L2 = measure C L' ]
           ); hsimpl*.
charguer's avatar
charguer committed
275
         (* ça on automatisera plus tard avec une tactique *) }
276
       { introv N Hij. xpull. intros C2 L2 C2i Hm.
charguer's avatar
charguer committed
277 278
         xapp_spec Sf.
         unfold hinv at 1. xpull. intros I'.
279 280
         xapps*. xif.
         { xapps*. xapp. intros _. unfold hinv. hsimpl.
281
           { rewrite* measure_step. rew_bool_eq~. }
282
           { rew_array*. case_if~. }
charguer's avatar
charguer committed
283
           applys~ inv_step_push i. }
284
         { unfold hinv. xrets~. applys~ inv_step_skip j. } }
charguer's avatar
charguer committed
285
       { unfold hinv. hsimpl. apply~ inv_step_pop. }
286 287 288
       { intros ?. xpull;=> C2 L2 C2i Hm. hsimpl. rewrite Hm.
         unfold measure. rew_listx. math. }
       { intros C2 L2 Hm. xapplys~ HS. lets*: measure_nonneg C2 L2. } }
charguer's avatar
charguer committed
289 290
    { (* case loop end *)
      xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
291
  { intros r. hpull ;=> m C L E Em. rew_bool_eq in *. subst L.
charguer's avatar
charguer committed
292 293 294 295 296 297 298
    (* on pourra peut être essayer de patcher des x-tactiques
     pour que le [rew_bool_eq] soit fait automatiquement? *)
    hsimpl C. }
  { unfolds hinv. clear hinv K.
    intro C. xpull. intros I. (* dans cfm2, c'est pratique on peut faire [xpull ;=> C I]
     directement. il faudrait voir pour patcher [xpull] de cfml1 pour qu'il laisse
     les quantificateurs en tête de la même manière *)
299 300
    (* Armael: je ne sais pas comment implémenter ça. faire un pose mark /
       gen_until_mark ne marche pas parce que xpull shuffle le contexte *)
charguer's avatar
charguer committed
301 302 303
    lets: inv_length_C I.
    xapp*. hsimpl. apply affine_Stack. (* à mettre en hint *)
    forwards R: inv_end I Gb. subst r. extens. rew_bool_eq*. }
304
Qed.