; VSSTE 2012 Problem 5
(in-package "ACL2")
; This book has the actual proof.
(local (include-book "breadth-first-proof"))
(set-enforce-redundancy t)
; Set theory library (defines SETS:: functions like setp, in, union, etc.)
(include-book "finite-set-theory/osets/sets" :dir :system)
; Note on Sets: The book above defines FINITE sets. We will use finite sets to
; represent the successor sets of a vertex. However, our formalization of the
; search algorithm does NOT assume that the set of vertices is finite, only
; that that the set of successors of each vertex is finite. This is consistent
; with the problem statement.
; Note on the Syntax of Symbols: Recall that function and variable symbols in
; Lisp (and ACL2) language are actually symbol objects. (Lisp expressions are
; Lisp objects.) Thus the name of the function mentioned above, union, is a
; symbol object. Symbols are essentially case insensitive. Union, union, and
; UNION all denote the same symbol object. Symbol objects in Common Lisp (and
; ACL2) are associated with packages. The symbol UNION in the "SETS" package
; is different from the symbol UNION in the "ACL2" package. By default (as
; specified by the IN-PACKAGE expression at the top of this file) all the
; symbols mentioned in this file are in the "ACL2" package. So how do we refer
; to the UNION in the "SETS" package? Answer: we write SETS::UNION.
; The b* macro, defined in the next book loaded, is like Common Lisp's (and
; ACL2's) let*, but lets you handle multiple value vectors and mix control with
; binding, and is generally convenient. This macro is used throughout our
; solutions and we'll comment on its use below as necessary. But roughly
; speaking,
; (b* ((v (foo x))
; ((mv a b) (bar v)))
; )
; means ``bind v to the value returned by (foo x), then bind a and b to the two
; values returned by the multiple-valued expression (bar v), and then evaluate
; .'' However, b* also permits us to test certain conditions before we
; do the bindings, so that
; (b* ((when (p x)) )
; (v (foo x))
; ((mv a b) (bar v)))
; )
; is like the b*-expression above except if (p x) is true, it skips the rest of
; the expression and evaluates and return .
(include-book "tools/bstar" :dir :system)
; This book defines a convenient two-place measure that we use to admit the
; main BFS loop.
(include-book "unicode/two-nats-measure" :dir :system)
; -----------------------------------------------------------------------------
;
; MODEL OF THE BFS ALGORITHM
;
; -----------------------------------------------------------------------------
; We allow any object to be a vertex.
; We use ordinary sets of objects to represent vertex sets.
; The following encapsulate introduces (SUCC V) as an abstract function that we
; assume returns the set of successors for a particular vertex.
(encapsulate
(((succ *) => *))
(local (defun succ (v)
(declare (ignore v))
nil))
(defthm setp-of-succ
(sets::setp (succ v))))
; For the algorithm, we keep everything mostly the same as in the pseudocode.
;
; However, we've changed the names of V, N, and C to Vs, Ns, and Cs. This
; helps us remember that they are sets, and also avoids a name clash between v
; and V, since ACL2 is case insensitive.
(defun bfs-inner-loop (succs Vs Ns)
; This corresponds to the inner loop, whose pseudocode is:
;
; for each w in succ(v) do
; if w is not in Vs then
; add w to Vs
; add w to Ns
; endif
; endfor
;
; The idea is that succs should initially be set to succ(v), and we will
; recur down succs, doing the set-insertions into Vs and Ns as needed.
;
; We return the updated sets of Vs and Ns, as a multiple-value vector (mv Vs Ns).
;
; A subtle tweak is that, in the base case, we set-fix Vs and Ns. This
; ``fixing'' is the identity on sets, but coerces non-set arguments to the
; empty set. This gives us unconditional setp theorems.
(declare (xargs :guard (and (sets::setp succs)
(sets::setp Vs)
(sets::setp Ns))))
(b* (((when (sets::empty succs))
(mv (sets::sfix Vs) (sets::sfix Ns)))
(w (sets::head succs))
((unless (sets::in w Vs))
(bfs-inner-loop (sets::tail succs)
(sets::insert w Vs)
(sets::insert w Ns))))
(bfs-inner-loop (sets::tail succs) Vs Ns)))
(defun bfs-main-step (dest Vs Cs Ns d)
; This is one step of through the "while" statement of the BFS algorithm.
; It returns multiple values (mv Vs' Cs' Ns' d' flg), where:
; - Vs', Cs', Ns', and d' are the next values of Vs, Cs, Ns, and d;
; - flg is true if we are to go through the loop again, else nil.
(declare (xargs :guard (and (sets::setp Vs)
(sets::setp Cs)
(sets::setp Ns)
(natp d))))
(b* (((when (sets::empty Cs))
;; Cs has become empty, so we fail "no path."
(mv Vs Cs Ns :NO-PATH nil))
;; Remove one vertex, v, from Cs. I'll just choose to take its head.
(v (sets::head Cs))
(Cs (sets::tail Cs))
;; if v = dest then return d.
((when (equal v dest)) ; return
(mv Vs Cs Ns d nil))
;; for each w in succ(v) do ... endfor
((mv Vs Ns) (bfs-inner-loop (succ v) Vs Ns))
;; the if statement... ; if Cs is empty then
((mv Cs Ns d) ; Cs <- Ns
(if (sets::empty Cs) ; Ns <- {}
(mv Ns nil (+ d 1)) ; d <- d + 1
(mv Cs Ns d)))) ; endif
(mv Vs Cs Ns d t)))
(defun bfs-main-loop (dest Vs Cs Ns d clk)
; This is basically the BFS algorithm from the ``while'' statement onwards,
; that is, it's just missing the preliminary setup.
;
; - Dest is the dest vertex we've been given
; - Vs, Cs, Ns are the sets we're manipulating
; - d is the depth we've explored to, so far.
;
; What is clk?
;
; The BFS algorithm doesn't necessarily terminate, so we add a ``clock''
; argument to let us model when it diverges. Basically, clk says how many more
; times we are willing to continue increasing D.
;
; To show ACL2 that this function terminates, we have to use a two-part measure
; with the CLK as the major component and the size of Cs as the minor
; component. (Perhaps the ACL2 Sedan's Calling Context Graph (CCG) analysis
; could get this automatically, but we have not tried.)
(declare (xargs :measure (two-nats-measure clk
(sets::cardinality Cs))))
(b* (((when (zp clk))
;; Ran out of clock, there is no path within our artificial time bound.
;; (Later we'll consider the existence of a sufficiently large clk).
;; We return the keyword constant :DIVERGE to signal divergence.
:DIVERGE)
((mv Vs Cs Ns d1 flg)
(bfs-main-step dest Vs Cs Ns d)))
(if flg
;; Continue the while loop.
(bfs-main-loop dest Vs Cs Ns d1
(if (equal d d1) clk (- clk 1)))
d1)))
; Note: Defun-sk allows us to introduce a function containing a top-level
; quantifier in its body. (bfs-finishes source dest Vs Cs Ns d) means ``there
; exists clk such that (bfs-main-loop source dest Vs Cs Ns d clk) is not
; :DIVERGE.''
(defun-sk bfs-finishes (dest Vs Cs Ns d)
; We will say that BFS-FINISHES if there exists some clock for which the main
; loop does not diverge. Quantifiers are formalized with (not necessarily
; uncomputable) Skolem-like witness functions. This defun-sk introduces
; BFS-FINISHES-WITNESS, which is such a clock, if one exists.
(exists (clk)
(not (equal (bfs-main-loop dest Vs Cs Ns d clk)
:DIVERGE))))
(defun bfs-main-loop-exec (dest Vs Cs Ns d)
; This variant of bfs-main-loop eliminates the clock. The mbe form below
; specifies a logical definition in its :logic component. That logical
; definition uses a skolem function, bfs-finishes-witness, produced by the
; defun-sk form above, to provide a sufficiently large clock (if such exists)
; to avoid returning :DIVERGE. The :exec part avoids the clock and may not
; terminate, but is provably equal to the :logic part, as is guaranteed by the
; guard verification. Our guard verification also guarantees that
; bfs-main-loop-exec is truly an executable program (except for the use of the
; abstract function, succ), not appealing to an existential quantifier (from
; bfs-finishes) during evaluation of its calls. See the final section of this
; file for a demonstration.
(declare (xargs :guard (and (sets::setp Vs)
(sets::setp Cs)
(sets::setp Ns)
(natp d))
;; The following is the default, but we add it to emphasize
;; that we have indeed verified the guards (in
;; breadth-first-proof.lisp).
:verify-guards t))
(mbe :logic
(if (bfs-finishes dest Vs Cs Ns d)
;; The main loop is going to finish if we give it enough clock, so
;; just go ahead and run it for enough steps.
(let ((long-enough (bfs-finishes-witness dest Vs Cs Ns d)))
(bfs-main-loop dest Vs Cs Ns d long-enough))
:DIVERGE)
:exec
(b* (((mv Vs Cs Ns d1 flg)
(bfs-main-step dest Vs Cs Ns d)))
(if flg
;; Continue the while loop.
(bfs-main-loop-exec dest Vs Cs Ns d1)
d1))))
(defun bfs (source dest)
; Finally, here is the whole BFS algorithm. We do the setup stuff, and then
; (via quantification) check whether there exists any depth that will cause the
; main loop to terminate.
;
; You might object to this use of quantification. After all, this is supposed
; to be a program, and it hardly seems fair to use universal quantification in
; its definition. In a way this seems fair enough, but really the algorithm
; that has been proposed is only a partial function anyway, and what we're doing
; with this quantification is making explicit whether or not it indeed
; terminates.
(declare (xargs :guard t))
(b* ( ;; Preliminary setup stuff.
(Vs (sets::insert source nil)) ;; Vs <- {source}
(Cs (sets::insert source nil)) ;; Cs <- {source}
(Ns nil) ;; Ns <- {}
(d 0)) ;; d <- 0
(bfs-main-loop-exec dest Vs Cs Ns d)))
; -----------------------------------------------------------------------------
;
; DEFINITIONS OF PATHS AND REACHABILITY
;
; -----------------------------------------------------------------------------
; For our verification tasks, we need to talk about paths, shortest paths, the
; existence of paths, etc. We now introduce some basic definitions related to
; paths and reachability.
(defun path-p (x)
(cond ((atom x) nil) ;; the empty list is NOT a valid path
((atom (cdr x)) t) ;; a singleton list IS a valid path (length 0)
(t
(let ((v1 (first x))
(v2 (second x)))
(and (sets::in v2 (succ v1)) ;; v2 must be a successor of v1, and
(path-p (cdr x))))))) ;; (v2 ...) must be a path
(defun path-length (x)
;; The length of a path is one less than the actual length of the list.
(- (len x) 1))
(defun path-from (x)
;; The vertex where a path starts.
(car x))
(defun path-to (x)
;; The vertex where a path ends.
(car (last x)))
;; Just a few examples to show that our definitions of paths seem to be
;; basically reasonable.
(assert-event (equal (path-length '(a b c)) 2))
(assert-event (equal (path-from '(a b c)) 'a))
(assert-event (equal (path-to '(a b c)) 'c))
; The verification tasks deal with notions like the existence of paths of
; certain lengths. Here are some definitions to capture these ideas.
(defun-sk reachable (from to)
;; Does there exist a path from FROM to TO?
(exists (path)
(and (path-p path)
(equal (path-from path) from)
(equal (path-to path) to))))
(defun-sk reachable-at-n (from to n)
;; Does there exist a path from FROM to TO of length N?
(exists (path)
(and (path-p path)
(equal (path-from path) from)
(equal (path-to path) to)
(equal (path-length path) n))))
(defun-sk reachable-before-n (from to n)
;; Does there exist a path from FROM to TO with length less than N?
(exists (path)
(and (path-p path)
(equal (path-from path) from)
(equal (path-to path) to)
(< (path-length path) n))))
; -----------------------------------------------------------------------------
;
; VERIFICATION TASKS
;
; -----------------------------------------------------------------------------
; Note: See breadth-first-proof.lisp for the supporting definitions and lemmas
; used to get ACL2 to prove these theorems.
; Verification Task 1. (Soundness).
;
; Goal: Verify that whenever function bfs returns an integer n, this is indeed
; the length of the shortest path from source to dest.
(defthm soundness
(let ((n (bfs source dest)))
(implies (integerp n)
(and (reachable-at-n source dest n)
(not (reachable-before-n source dest n))))))
; Verification Task 2. (Completeness).
;
; Goal: Verify that whenever BFS reports failure, there is no path from source
; to dest.
;
; NOTE: We interpret ``reporting failure'' as either
;
; (1) BFS diverges, or
; (2) BFS returns NO-PATH.
;
; In either case we prove that there is no path from source to dest.
(defthm completeness
(implies (not (integerp (bfs source dest)))
(not (reachable source dest))))
; -----------------------------------------------------------------------------
;
; EXECUTABILITY
;
; -----------------------------------------------------------------------------
; As promised in a comment in bfs-main-loop-exec, we now demonstrate that our
; use of mbe in that function did indeed support executability. We define a
; very simple concrete version of succ, succ-exec. The defattach form below
; generates proof obligations (see
; http://www.cs.utexas.edu/users/moore/acl2/v4-3/DEFATTACH.html for
; documentation) to guarantee that succ-exec satisfies the constraints on the
; abstract function, succ. Upon successful execution of the defattach form, a
; call of succ is evaluated by making the corresponding call to succ-exec, as
; checked in one instance by the assert-event form below. (However, this
; attachment of succ-exec to succ is disabled during proofs, as explained in
; the documentation mentioned above.)
; Consider the following graph, where, for example, there are edges from
; node 0 to nodes 1 and 2. Note that node 6 is isolated.
; 5 6
; ^
; |
; 2 ----
; ^ |
; | v
; 0 --> 1 --> 3
; |
; v
; 4
; Concretely, we could represent this graph with the successor function
; defined below, as the executable function succ-exec.
(defun succ-exec (v)
(declare (xargs :guard t))
(case v
(0 (sets::insert 1 (sets::insert 2 nil)))
(1 (sets::insert 3 (sets::insert 4 nil)))
(2 (sets::insert 5 (sets::insert 1 nil)))
(otherwise nil)))
; We can then tell ACL2 to ``attach'' succ-exec to succ in the sense that
; when asked to evaluate succ, ACL2 will evaluate succ-exec instead.
; This attachment is only possible because we have proved that succ-exec
; is guard verified and satisfies the constraints on succ. Furthermore,
; ACL2 will use succ-exec for succ only in the ``evaluation theory,''
; and, in particular, will NOT use it when it is proving theorems about
; succ.
(defattach succ succ-exec)
; Finally, we exhibit the answers computed by bfs for all the source and
; destination node combinations in {0,1,2,3,4,5,6}. This demonstrates
; that our bfs is an executable program when succ is executable.
(assert-event
(equal (list (list 0 (list (bfs 0 0) (bfs 0 1) (bfs 0 2)
(bfs 0 3) (bfs 0 4) (bfs 0 5) (bfs 0 6)))
(list 1 (list (bfs 1 0) (bfs 1 1) (bfs 1 2) (bfs 1 3)
(bfs 1 4) (bfs 1 5) (bfs 1 6)))
(list 2 (list (bfs 2 0) (bfs 2 1) (bfs 2 2)
(bfs 2 3) (bfs 2 4) (bfs 2 5) (bfs 2 6)))
(list 3 (list (bfs 3 0) (bfs 3 1) (bfs 3 2)
(bfs 3 3) (bfs 3 4) (bfs 3 5) (bfs 3 6)))
(list 4 (list (bfs 4 0) (bfs 4 1) (bfs 4 2)
(bfs 4 3) (bfs 4 4) (bfs 4 5) (bfs 4 6)))
(list 5 (list (bfs 5 0) (bfs 5 1) (bfs 5 2)
(bfs 5 3) (bfs 5 4) (bfs 5 5) (bfs 5 6)))
(list 6 (list (bfs 6 0) (bfs 6 1) (bfs 6 2)
(bfs 6 3) (bfs 6 4) (bfs 6 5) (bfs 6 6))))
; 0 1 2 3 4 5 6
'((0 (0 1 1 2 2 2 :NO-PATH))
(1 (:NO-PATH 0 :NO-PATH 1 1 :NO-PATH :NO-PATH))
(2 (:NO-PATH 1 0 2 2 1 :NO-PATH))
(3 (:NO-PATH :NO-PATH :NO-PATH 0 :NO-PATH :NO-PATH :NO-PATH))
(4 (:NO-PATH :NO-PATH :NO-PATH :NO-PATH 0 :NO-PATH :NO-PATH))
(5 (:NO-PATH :NO-PATH :NO-PATH :NO-PATH :NO-PATH 0 :NO-PATH))
(6 (:NO-PATH :NO-PATH :NO-PATH :NO-PATH :NO-PATH :NO-PATH 0)))))