Proof in progress (Schorr-Waite)

examples/in_progress/schorr_waite.mlw

@@ -17,11 +17,11 @@ module SchorrWaite
   use import list.Length
   use import list.Mem as L
   use import list.HdTlNoOpt
+  use import list.NthNoOpt
   use import list.Append
   use import list.Reverse
   use import list.Distinct
   use import set.Fset as S
-  use import option.Option
 
   (** a small component-as-array memory model *)
 
@@ -43,6 +43,10 @@ module SchorrWaite
     requires { p <> null }
     ensures  { result = !right[p] }
 
+  val get_path_from_root (p : loc) : list loc
+    requires { p <> null }
+    ensures  { result = !path_from_root[p] }
+
   val set_left (p: loc) (v: loc) : unit
     requires { p <> null }
     writes   { left }
@@ -63,6 +67,11 @@ module SchorrWaite
     writes   { c }
     ensures  { !c = set (old !c) p v }
 
+  val set_path_from_root (p: loc) (l : list loc) : unit
+    requires { p <> null }
+    writes   { path_from_root }
+    ensures  { !path_from_root = set (old !path_from_root) p l }
+
   val tl_stackNodes (stack : list loc) : list loc 
     requires { stack <> Nil }
     ensures  { result = tl stack }
@@ -124,11 +133,12 @@ module SchorrWaite
 
   inductive stack_form (l r : map loc loc) (c : map loc bool) (p : loc) (stack : list loc) =
   | stack_nil  : forall l r : map loc loc, c : map loc bool, p : loc. stack_form l r c p Nil
-  | stack_cons : forall l r : map loc loc,
-    	       	 c : map loc bool,
-		 p : loc, 
-		 s : list loc. stack_form l r c (next l r c p) s -> 
-		 stack_form l r c p (Cons p s)
+  | stack_cons :
+    forall l r : map loc loc,
+    c : map loc bool,
+    p : loc,
+    s : list loc. stack_form l r c (next l r c p) s ->
+    stack_form l r c p (Cons p s)
 
   predicate pair_in_list (p1 p2 : loc) (l : list loc)  =
     match l with
@@ -140,6 +150,11 @@ module SchorrWaite
        end) \/ pair_in_list p1 p2 m
     end
 
+  lemma t : forall n x y: loc, left right : map loc loc, pth : list loc.
+   
+    reachable_via n x left right pth -> edge x y left right ->
+    reachable_via n y left right (pth ++ (Cons x Nil))
+
   let schorr_waite (root: loc) (graph : set loc) : unit
     requires { root <> null /\ S.mem root graph }
     (* what is set S --> closed under children of all vertices *)
@@ -156,22 +171,23 @@ module SchorrWaite
 	       (old !right)[n] = !right[n] }
     (* all the non-null vertices reachable from root
        are marked at the end of the algorithm *)
-    ensures  { forall n : loc.
-    	       n <> null /\ reachable root n (old !left) (old !right) ->
-	       !m[n] }
+    ensures  { forall n : loc. S.mem n graph /\  n <> null /\
+    	       reachable root n (old !left) (old !right) -> !m[n] }
     (* every marked node was reachable from 'root' in the pre-state *)	       
-    ensures  { forall n : loc. n <> null /\ 
-    	       !m[n] -> reachable root n (old !left) (old !right) }
+    ensures  { forall n : loc. S.mem n graph /\ n <> null /\ !m[n] ->
+    	       reachable root n (old !left) (old !right) }
     (* forall non-reachable vertices the mark remains 
        the same as in the pre-state *)
-    ensures  { forall n : loc. n <> null /\
-    	       not reachable root n !left !right ->
-	       !m[n] = (old !m)[n] }
+    (* update: no need for this post-condition (taken from Hubert and Marché's work) 
+     * since the previous one guarantees that only reachable nodes from root have their 
+     * marks changed *)
+    (* ensures  { forall n : loc. n <> null /\ not reachable root n !left !right ->
+	       !m[n] = (old !m)[n] } *)
   = 'Init:
     let t = ref root in
     let p = ref null in
     let ghost stackNodes = ref Nil in
-    let ghost path = ref Nil in
+    let ghost pth = ref Nil in
     let ghost unmarked_nodes = ref graph in
     let ghost c_false_nodes = ref graph in
     while !p <> null || (!t <> null && not !m[!t]) do
@@ -186,7 +202,7 @@ module SchorrWaite
       invariant { forall p1 p2 : loc. pair_in_list p1 p2 (Cons !t !stackNodes) ->
       		  (!c[p2] -> (at !left 'Init)[p2] = !left[p2] /\ (at !right 'Init)[p2] = p1) /\
 		  (not !c[p2] -> (at !left 'Init)[p2] = p1 /\ (at !right 'Init)[p2] = !right[p2]) }
-      invariant { not L.mem !t !stackNodes } (* this will be usefull to prove that !t is in graph *)
+      (*invariant { not L.mem !t !stackNodes }*) (* this will be usefull to prove that !t is in graph after the push ---> but this is false! think of the case when the graph is cyclic *)
       (* I4d from Hubert and Marché's paper and something related to line 63-65 from Leino's *)
       invariant { forall n : loc. S.mem n graph /\ n <> null /\ not L.mem n !stackNodes ->
       		  !left[n] = (at !left 'Init)[n] /\ !right[n] = (at !right 'Init)[n] }
@@ -210,6 +226,27 @@ module SchorrWaite
       (* lines 80-81 from Leino's paper *)
       invariant { !stackNodes <> Nil -> if !c[!p] then (at !right 'Init)[!p] = !t
       		  else (at !left 'Init)[!p] = !t }
+      (* lines 78-79 from Leino's paper *)
+      invariant { forall k : int. 0 < k < length !stackNodes ->
+      		  if !c[nth k !stackNodes] then
+		    nth (k - 1) !stackNodes = (at !right 'Init)[nth k !stackNodes]
+		  else nth (k - 1) !stackNodes = (at !left 'Init)[nth k !stackNodes] }
+      (* line 72 from Leino's paper --> used to prove the post that very marked node was 
+       * reachable from 'root' in the pre-state *)
+      invariant { forall n : loc. S.mem n graph /\ !m[n] /\ n <> null ->
+      		  reachable root n (at !left 'Init) (at !right 'Init) }
+      (* help establishing the previous invariant for the push case -->
+       * line 70 from Leino's paper *)
+      invariant { !p <> null -> reachable_via root !p (at !left 'Init) (at !right 'Init) !pth }
+      (* help establishing the previous invariant when p = null, ie 
+       * for the firts push of the loop *)
+      invariant { !p = null <-> !t = root }
+      invariant { (!p = null \/ !p = root) -> !pth = Nil }
+      (* help establishing the previous invariant for the pop case -->
+       * line 70 from Leino's paper *)
+      invariant { forall n : loc, pth : list loc.
+      		  S.mem n graph /\ n <> null /\ !m[n] /\ pth = !path_from_root[n] ->
+		  reachable_via root n (at !left 'Init) (at !right 'Init) pth }
       (* termination proved using lexicographic order over a triple *)
       variant   { S.cardinal !unmarked_nodes, S.cardinal !c_false_nodes, length !stackNodes }
       if !t = null || !m[!t] then begin
@@ -219,7 +256,7 @@ module SchorrWaite
           p := !right[!p];
 	  stackNodes := tl_stackNodes !stackNodes;
           set_right !t q;
-	  path := !path_from_root[!p];
+	  pth := get_path_from_root !p;
         end else begin (* swing *)
 	  (* the following assertion is automatically discharged 
 	   * and it is useful to prove that t is in the set graph *)
@@ -233,13 +270,16 @@ module SchorrWaite
         end
       end else begin (* push *)
         let q = !p in
+	if !p <> null then pth := !pth ++ (Cons q Nil);
         p := !t;
 	stackNodes := Cons !p !stackNodes;
-	(*if !p <> root then path := !path ++ (Cons !p Nil);*)
         t := get_left !t;
         set_left !p q;
         set_m !p true;
-	!path_from_root[!p] = !path;
+	set_path_from_root !p !pth;
+	(* this is assertion is automatically discharged and it helps 
+ 	 * proving that all marked nodes are reachable from root *)
+	assert { path (at !left 'Init) (at !right 'Init) root !p !pth }; 
         (*set_c !p false;*) (* if we assume at the pre-condition that all nodes start with c = 0,
 		   	       then this redundant *)
 	unmarked_nodes := S.remove !p !unmarked_nodes