Hanbing Liu, May 5, 2004 [updated Mon May  3 17:39:39 2004]

SHORT ABSTRACT 
==============

This coming Wednesday, I will present my formalization of a ring data
structure in ACL2. I will describe a mechanically checked proof about
it briefly. We proved that "join" (add a new node to a ring) and "rm"
(remove a node from a ring) primitives maintain the unidirectional
ring topology. Because the ring concept is formulated in terms of
reachable sets from different nodes, the proof revolves around
reachability on a graph in a certain representation and how the
reachability changes when the graph is updated.

This work is motivated by Xiaozhou (Steve) Li's ACL2 Seminar
presentation of "Concurrent Maintenance of Rings" on March 03,
2004. It can be considered as a small initial step towards a
mechanically verified ring maintenance protocol in ACL2.


SUMMARY 
=======

The system of interest is comprised of a set of nodes. Each has a
neighbor pointer. Certain system configurations can be recognized as
representing a unidirectional ring. We need to show primitives that
adds new node and removes some node preserve the unidirectional
ring-ness.


Representation
--------------

The set of nodes and their neighborhood information can be modeled and
recorded in a list of pairs. The first component pair records the name
of a node, the second component records the reference to the neighbor
of the node.

For example:
      L =  
	        (( A . B )  
	         ( B . C )  
	         ( C . A )  
	         ( D . nil) 
	         ( E . X))    	
	 
represents a system configuration with 5 nodes. From A's neighbor is
B, B's neighbor is C and so on. D, E do not have any neighbor.


Ring Definition
---------------

In my formulation, a system configuration represents a ring, if and
only if, starting from any node that has a neighbor, all nodes with a
neighbor are reachable.

   -------------------------------------------------------------------

   (defun ring (l)
      (non-nil-neighbor-set1 (all-nodes l) l))

   (defun ringp-aux (l1 l ring)
     "Test whether any nodes in l1's reachable set is set-equal to ring"
     (declare (xargs :measure (len l1)))
     (if (endp l1) t
       (and  (set-equal (reachable-set1 (car l1) l nil) ring)
             (ringp-aux (cdr l1) l ring))))


   (defun ringp (l)
     "Assert all nodes on the ring can reach all other such nodes" 
      (ringp-aux (ring l) l (ring l)))
       
   -------------------------------------------------------------------

Thus, the system configuration L is a ring. A, B, C form a "ring". D,
E are not on the ring.


Update Primitives
-----------------

Join(n, s, e, l) is a primitive that updates a system configuration.

      (defun join (n s e l)
        "set node n's neighbor to s, set node e's neighbor to n"
        (bind e n (bind n s l)))


Join adjusts n's neighbor to s, and adjust e's neighbor to n in a
system configuration l.


Join(E, A, C, L) transforms L in to new system configuration:

     (( A . B )  	  (( A . B ) 
      ( B . C )   	   ( B . C ) 
      ( C . A )   ====>	   ( C . E ) 
      ( D . nil) 	   ( D . nil )
      ( E . X))  	   ( E . A))	

For "join", we show

      (defthm join-preserve-ringp
        (implies (and (not (mem n (ring l)))
                      (ringp l)
                      (alistp l)
                      (mem e (ring l))
                      (mem s (ring l))
                      (assoc-equal n l)
                      (equal (cdr (assoc-equal e l)) s))
                 (ringp (join n s e l)))

when if e's neighbor is s, if e, s are on ring, node n is not on the
ring, the resulting system configuration represents a ring with n as
an additional node.


Similarly "rm" is defined as 

 (defun rm (s a l)
  (bind a nil (bind s (cdr (assoc-equal a l)) l)))

which adjusts s to point to the neighbor of a, and update a's neighbor
to nil



Short Proof Sketch  
------------------

For JOIN: 

1. Prove that updating the neighbor field of a node, which is not on the
   original ring, does not change the ring. 

2. Prove that a reachable-set can be decomposed into two segments.

3. Show the segment before the node, which is being updated, does not
   change from what it was. Show the new second segment is extended
   with a new node -- when the new node's neighbor is the original
   neighbor of the node being updated.

4. Prove that after join, the set of nodes reachable from a node on
   the ring is equal to the set of nodes on the ring.

For RM: 

1. Prove that our reachable-set is in fact a path through a graph. The
   path is a simple path.

2. Prove that there is a unique simple path between two nodes.

3. Prove that the reachable-set is equal a concatenation of two
   segments. One segment ends with the node to be skipped.

4. Prove that the reachable-set after "rm" operation is a
   concatenation of two segments
   
5. Prove that DEL a node from the concatenation of two segments from 3
   gives us the concatenation of two segment that happens to equal to
   those from 4. 

6. Prove that one and only one node, which has a neigbor originally,
   become neighborless after "rm"


Comments and Discussion
-----------------------

* Other possible representation/definition/proof strategy


* Reachability and ACL2 definition principle


;----------------------------------------------------------------------