Commit 67ac2bf0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Schorr-Waite algorithm: proof completed

parent 341e25cd
......@@ -7,14 +7,23 @@
Author: Mario Pereira (UBI, then Université Paris Sud)
The proof below closely follows that of Rustan Leino with dafny,
which is described in this paper:
The code, specification, and invariants below follow those of
the following two proofs:
- Thierry Hubert and Claude Marché, using Caduceus and Coq
A case study of C source code verification: the Schorr-Waite algorithm.
SEFM 2005. http://www.lri.fr/~marche/hubert05sefm.ps
- Rustan Leino, using Dafny
Dafny: An Automatic Program Verifier for Functional Correctness.
LPAR-16.
http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf
*)
module SchorrWaite
(*use import bool.Bool*)
use import seq.Seq
use import map.Map
use import ref.Ref
......@@ -24,55 +33,72 @@ module SchorrWaite
use import list.Append
use import set.Fset as S
(** a small component-as-array memory model *)
(** Why3 has no support for arbitrary pointers,
so we introduce a small component-as-array memory model *)
(** the type of pointers and the null pointer *)
type loc
constant null: loc
(** each (non-null) location holds four fields: two Boolean marks m and c
and two pointers left and right *)
val m: ref (map loc bool)
val c: ref (map loc bool)
val left: ref (map loc loc)
val right: ref (map loc loc)
(** record the path from the root to a node *)
val ghost path_from_root : ref (map loc (list loc))
val get_left (p: loc) : loc
requires { p <> null }
ensures { result = !left[p] }
val get_right (p: loc) : loc
requires { p <> null }
ensures { result = !right[p] }
val get_path_from_root (p : loc) : list loc
(*requires { p <> null } ---> maybe I don't need this pre-condition *)
ensures { result = !path_from_root[p] }
val set_left (p: loc) (v: loc) : unit
requires { p <> null }
writes { left }
ensures { !left = set (old !left) p v }
val get_right (p: loc) : loc
requires { p <> null }
ensures { result = !right[p] }
val set_right (p: loc) (v: loc) : unit
requires { p <> null }
writes { right }
ensures { !right = set (old !right) p v }
val get_m (p: loc) : bool
requires { p <> null }
ensures { result = !m[p] }
val set_m (p: loc) (v: bool) : unit
requires { p <> null }
writes { m }
ensures { !m = set (old !m) p v }
val get_c (p: loc) : bool
requires { p <> null }
ensures { result = !c[p] }
val set_c (p: loc) (v: bool) : unit
requires { p <> null }
writes { c }
ensures { !c = set (old !c) p v }
(** for the purpose of the proof, we add a fifth, ghost, field,
which records the path from the root (when relevant) *)
val ghost path_from_root : ref (map loc (list loc))
val get_path_from_root (p : loc) : list loc
ensures { result = !path_from_root[p] }
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 }
(** Stack of nodes, from the root to the current location, in
reverse order (i.e. the current location is the first element
in the stack) *)
type stacknodes = Seq.seq loc
predicate not_in_stack (n: loc) (s: stacknodes) =
......@@ -81,25 +107,25 @@ module SchorrWaite
let tl_stackNodes (stack: stacknodes) : stacknodes
requires { Seq.length stack > 0 }
ensures { result = stack[1 .. ] }
(*
* the following post-condition is usefull to prove the
* invariant that stackNodes' elements are also graph elements
* for the push case. An equivalent lemma would say:
* lemma mem_tl : forall x : 'a, l : list 'a. mem x l -> mem x (tl l)
*)
ensures { forall n. not_in_stack n stack -> not_in_stack n result }
=
stack[1 .. ]
(* usefull to prove that right field of every node out of the stack
remains the same after the push case *)
lemma cons_not_in: forall s: stacknodes, n t: loc. (*?????*)
Seq.length s > 0 ->
not_in_stack n (cons t s) -> not_in_stack n s
(** two lemmas about stacks *)
let lemma cons_not_in (s: stacknodes) (n t: loc)
requires { not_in_stack n (cons t s) }
ensures { not_in_stack n s }
=
assert { forall i: int. 0 <= i < Seq.length s ->
Seq.get s i = Seq.get (cons t s) (i+1) }
lemma tl_cons: forall s1 s2: stacknodes, p: loc.
Seq.length s2 > 0 ->
s1 = s2[1 ..] -> p = Seq.get s2 0 -> s2 = cons p s1
let lemma tl_cons (s1 s2: stacknodes) (p: loc)
requires { Seq.length s2 > 0 }
requires { s1 = s2[1 ..] }
requires { p = Seq.get s2 0 }
ensures { s2 = cons p s1 }
= assert { Seq.(==) s2 (cons p s1) }
function last (s: stacknodes) : loc =
Seq.get s (Seq.length s - 1)
......@@ -108,6 +134,8 @@ module SchorrWaite
forall i j. 0 <= i < Seq.length s -> 0 <= j < Seq.length s -> i <> j ->
Seq.get s i <> Seq.get s j
(** Paths *)
predicate edge (x y : loc) (left right : map loc loc) =
x <> null /\ (left[x] = y \/ right[x] = y)
......@@ -129,81 +157,48 @@ module SchorrWaite
| _ -> ()
end
(* the two following lemmas help proving the assertion in the push case *)
lemma path_edge : forall x y : loc, left right : map loc loc.
edge x y left right -> path left right x y (Cons x Nil)
(* TODO: choose between reachable_via and path *)
predicate reachable_via (x y : loc) (l r : map loc loc) (p : list loc) =
path l r x y p
lemma path_edge_cons:
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))
path left right n x pth -> edge x y left right ->
path left right n y (pth ++ (Cons x Nil))
predicate reachable (x y : loc) (l r : map loc loc) =
exists p : list loc. reachable_via x y l r p
predicate reachable (left right: map loc loc) (x y : loc) =
exists p : list loc. path left right x y p
(* auxiliary function the define the form of a stack *)
(*
function next (l r : map loc loc) (c : map loc bool) (p : loc) : loc =
if c[p] then r[p] else l[p]
*)
(*
inductive stack_form
(l r : map loc loc) (c : map loc bool) (p : loc) (stack : stacknodes) =
| stack_nil:
forall l r : map loc loc, c : map loc bool, p : loc.
stack_form l r c p Seq.empty
| stack_cons :
forall l r : map loc loc, c : map loc bool, p : loc, s : stacknodes.
stack_form l r c (next l r c p) s ->
stack_form l r c p (Seq.cons p s)
*)
(*
predicate pair_in_list (p1 p2 : loc) (l : list loc) =
match l with
| Cons b (Cons c _ as m) -> (b = p1 /\ c = p2) \/ pair_in_list p1 p2 m
| _ -> false
end
*)
(** Schorr-Waite algorithm *)
let schorr_waite (root: loc) (ghost graph : set loc) : unit
requires { root <> null /\ S.mem root graph }
(* what is set S --> closed under children of all vertices *)
(* graph is closed under left and right *)
requires { forall n : loc. S.mem n graph ->
n <> null /\ (* is this ok? won't this be a contradiction? *)
n <> null /\
S.mem !left[n] graph /\
S.mem !right[n] graph }
(* graph starts with nothing marked and no child currently visited *)
requires { forall x : loc. x <> null -> S.mem x graph ->
not !m[x] /\ not !c[x] }
(* the structure of the graph is not changed
TODO? actually, nothing is changed *)
ensures { forall n : loc. S.mem n graph -> n <> null ->
(* graph starts with nothing marked *)
requires { forall x : loc. S.mem x graph -> not !m[x] }
(* the structure of the graph is not changed *)
ensures { forall n : loc. S.mem n graph ->
(old !left)[n] = !left[n] /\
(old !right)[n] = !right[n] }
(* all the non-null vertices reachable from root
are marked at the end of the algorithm, and only these *)
(* update: following Leino's paper, I will specify that all reachable nodes
* are marked as a transitive property, rather than using reachability *)
ensures { forall n : loc. S.mem n graph -> n <> null -> !m[n] ->
reachable root n (old !left) (old !right) }
ensures { forall n : loc. S.mem n graph -> !m[n] ->
reachable (old !left) (old !right) root n }
ensures { !m[root] }
ensures { forall n : loc. S.mem n graph -> n <> null -> !m[n] ->
ensures { forall n : loc. S.mem n graph -> !m[n] ->
(forall ch : loc. edge n ch !left !right -> ch <> null -> !m[ch]) }
(* FIXME: remove unnecessary n<>null above *)
= 'Init:
let t = ref root in
let p = ref null in
let ghost stackNodes = ref Seq.empty in
let ghost pth = ref Nil in
set_path_from_root !t !pth;
ghost set_path_from_root !t !pth;
let ghost unmarked_nodes = ref graph in
let ghost c_false_nodes = ref graph in
while !p <> null || (!t <> null && not !m[!t]) do
while !p <> null || (!t <> null && not get_m !t) do
invariant { forall n. mem n graph -> not_in_stack n !stackNodes \/
exists i : int. Seq.get !stackNodes i = n }
invariant { not_in_stack null !stackNodes }
......@@ -211,21 +206,24 @@ module SchorrWaite
invariant { S.mem !t graph }
invariant { !p <> null -> S.mem !p graph }
invariant { Seq.length !stackNodes <> 0 -> Seq.get !stackNodes 0 = !p }
invariant { forall n : loc. S.mem n graph /\ n <> null /\ not !m[n] -> S.mem n !unmarked_nodes }
invariant { forall n : loc. S.mem n graph /\ n <> null /\ not !c[n] -> S.mem n !c_false_nodes }
invariant { forall i. 0 <= i < Seq.length !stackNodes -> S.mem (Seq.get !stackNodes i) graph }
invariant { forall n : loc. S.mem n graph -> not !m[n] ->
S.mem n !unmarked_nodes }
invariant { forall n : loc. S.mem n graph -> not !c[n] ->
S.mem n !c_false_nodes }
invariant { forall i. 0 <= i < Seq.length !stackNodes ->
S.mem (Seq.get !stackNodes i) graph }
invariant { forall i. 0 <= i < Seq.length !stackNodes - 1 ->
let p1 = Seq.get !stackNodes i in let p2 = Seq.get !stackNodes (i+1) in
(!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]) }
let p1 = Seq.get !stackNodes i in
let p2 = Seq.get !stackNodes (i+1) in
(!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 { !path_from_root[root] = Nil }
(*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 -> *)
invariant { forall n : loc. S.mem n graph ->
not_in_stack n !stackNodes ->
!left[n] = (at !left 'Init)[n] /\ !right[n] = (at !right 'Init)[n] }
(* I4a from Hubert and Marché's paper; useful to prove that !stackNodes = !p::... *)
(* invariant { stack_form !left !right !c !p !stackNodes } *)
!left[n] = (at !left 'Init)[n] /\
!right[n] = (at !right 'Init)[n] }
(* something like Leino's line 74; this is useful to prove that
* the stack is empty iff p = null *)
invariant { Seq.length !stackNodes <> 0 ->
......@@ -233,109 +231,91 @@ module SchorrWaite
if !c[first] then !right[first] = null
else !left[first] = null }
invariant { Seq.length !stackNodes <> 0 -> last !stackNodes = root }
(* something like lines 75-76 from Leino's paper --> with this invariant I believe there
* is no need to use 'stack_form' *)
(* something like lines 75-76 from Leino's paper *)
invariant { forall k : int. 0 <= k < Seq.length !stackNodes - 1 ->
if !c[Seq.get !stackNodes k]
then !right[Seq.get !stackNodes k] = Seq.get !stackNodes (k+1)
else !left [Seq.get !stackNodes k] = Seq.get !stackNodes (k+1) }
(* all nodes in the stack are marked ---> I4a from Hubert and Marché's paper
* and something alike line 57 from Leino's paper *)
invariant { forall i. 0 <= i < Seq.length !stackNodes -> !m[Seq.get !stackNodes i] }
(* all nodes in the stack are marked
* (I4a in Hubert and Marché and something alike line 57 in Leino) *)
invariant { forall i. 0 <= i < Seq.length !stackNodes ->
!m[Seq.get !stackNodes i] }
(* stack has no duplicates ---> line 55 from Leino's paper *)
invariant { distinct !stackNodes }
(* something like Leino's line 68; I believe this is useful to prove
* that in the pop case the left child of p is the initial one *)
(* something like Leino's line 68 *)
invariant { forall i. 0 <= i < Seq.length !stackNodes ->
let n = Seq.get !stackNodes i in
if !c[n] then !left[n] = (at !left 'Init)[n]
else !right[n] = (at !right 'Init)[n] }
(* lines 80-81 from Leino's paper *)
invariant { Seq.length !stackNodes <> 0 -> if !c[!p] then (at !right 'Init)[!p] = !t
invariant { Seq.length !stackNodes <> 0 ->
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 < Seq.length !stackNodes ->
let n = Seq.get !stackNodes k in
if !c[n] then Seq.get !stackNodes (k - 1) = (at !right 'Init)[n]
if !c[n]
then Seq.get !stackNodes (k - 1) = (at !right 'Init)[n]
else Seq.get !stackNodes (k - 1) = (at !left 'Init)[n] }
(* help establishing the next 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 }
(* 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 when p = null, ie
* for the firts push of the loop *)
(* line 70 from Leino's paper *)
invariant { !p <> null ->
path (at !left 'Init) (at !right 'Init) root !p !pth }
(* line 72 from Leino's paper *)
invariant { forall n : loc. S.mem n graph -> !m[n] ->
reachable (at !left 'Init) (at !right 'Init) root n }
invariant { !p = null -> !t = root }
(* help establishing the previous invariant for the pop case -->
* line 70 from Leino's paper *)
(* 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 }
(* lines 61-62 from Leinos' paper --> help establish the post that
* all nodes reachable from root are marked *)
S.mem n graph -> !m[n] ->
pth = !path_from_root[n] ->
path (at !left 'Init) (at !right 'Init) root n pth }
(* lines 61-62 from Leinos' paper *)
invariant { forall n : loc. S.mem n graph -> n <> null -> !m[n] ->
not_in_stack n !stackNodes ->
(*n <> !t*) (*---> do I really need this 'n <> !t'? *)
(*(forall ch : loc. edge n ch !left !right /\ ch <> null -> !m[ch]) }*)
(!left[n] <> null -> !m[!left[n]]) /\
(!right[n] <> null -> !m[!right[n]]) }
(* help establishing the previous invariant for the pop case --->
* something like Leino's lines 57-59 *)
(* something like Leino's lines 57-59 *)
invariant { forall i. 0 <= i < Seq.length !stackNodes ->
let n = Seq.get !stackNodes i in
!c[n] ->
(!left[n] <> null -> !m[!left[n]]) /\
(!right[n] <> null -> !m[!right[n]]) }
(* (forall ch : loc. edge n ch !left !right /\ ch <> null -> !m[ch]) } *)
(* termination proved using lexicographic order over a triple *)
variant { S.cardinal !unmarked_nodes,
S.cardinal !c_false_nodes,
Seq.length !stackNodes }
if !t = null || !m[!t] then begin
if !c[!p] then begin (* pop *)
if !t = null || get_m !t then begin
if get_c !p then begin (* pop *)
let q = !t in
t := !p;
assert { !p = Seq.get !stackNodes 0 };
assert { Seq.length !stackNodes > 0 };
stackNodes := tl_stackNodes !stackNodes;
ghost stackNodes := tl_stackNodes !stackNodes;
assert { not_in_stack !p !stackNodes };
p := !right[!p];
assert { !p = Seq.get !stackNodes 0 \/ !p = null };
set_right !t q;
pth := get_path_from_root !p;
ghost 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 *)
(* assert { pair_in_list !t !p (Seq.cons !t !stackNodes) }; *)
let q = !t in
t := get_right !p;
set_right !p (get_left !p);
set_left !p q;
c_false_nodes := S.remove !p !c_false_nodes;
ghost c_false_nodes := S.remove !p !c_false_nodes;
set_c !p true;
end
end else begin (* push *)
let q = !p in
(*if !p <> null then pth := !pth ++ (Cons q Nil);*)
p := !t;
stackNodes := Seq.cons !p !stackNodes;
ghost stackNodes := Seq.cons !p !stackNodes;
t := get_left !t;
set_left !p q;
set_m !p true;
if !p <> root then pth := !pth ++ (Cons q Nil) else pth := Nil;
set_path_from_root !p !pth;
(* this is assertion is automatically discharged and it helps
* proving that all marked nodes are reachable from root *)
ghost if !p <> root then pth := !pth ++ (Cons q Nil) else pth := Nil;
ghost set_path_from_root !p !pth;
assert { !p = Seq.get !stackNodes 0 };
assert { path (at !left 'Init) (at !right 'Init) root !p !pth };
set_c !p false; (* update: explicitly changing !c[p] to false and adding it to the
* set of false nodes (even if it is already there) helps in proving
* the invariant that all nodes in the stack with !c=1 have their
* children marked *)
c_false_nodes := S.add !p !c_false_nodes;
unmarked_nodes := S.remove !p !unmarked_nodes
set_c !p false;
ghost c_false_nodes := S.add !p !c_false_nodes;
ghost unmarked_nodes := S.remove !p !unmarked_nodes
end
done
......
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