StackDFS_proof.v 6.14 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 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 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 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 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.