(in-package "ACL2")
; We now include the records book (definitions and theorems about records
; represented using list structures). As a result of loading that book, we can
; write (g :field b) to extract from record b the contents of field :field, and
; we can write (s :field val b) to set the contents of field :field of record b
; to val, obtaining a new record object.
(include-book "misc/records" :dir :system)
; Include definition of handy macro, b*:
(include-book "tools/bstar" :dir :system)
(defun ring-buffer-p (b)
(declare (xargs :guard t))
(let ((data (g :data b))
(size (g :size b))
(first (g :first b))
(len (g :len b)))
(and (true-listp data) ; no restrictions on data (generic)
(natp size)
(natp first)
(natp len)
(< first size)
(<= len size) ; implicit in problem statement ("capacity")
(<= size (len data)))))
; Note: In ACL2, when a :guard is provided, the defun principle proves that
; the :guard of the newly defined function guarantees the guards of all functions
; used in the body of the definition. For example, note that full-p below is
; given a guard of (ring-buffer-p b). When full-p is defined, ACL2 will prove
; that the guards of its body are implied by (ring-buffer-p b). Furthermore,
; when full-p is called in some other guarded function, ACL2 will prove that
; it is applied to a ring-buffer-p.
(defun full-p (b)
(declare (xargs :guard (ring-buffer-p b)))
(equal (g :len b) (g :size b)))
(defun empty-p (b)
(declare (xargs :guard (ring-buffer-p b)))
(equal (g :len b) 0))
(defun zeros (n) ; list of n zeros
(declare (xargs :guard (natp n)))
(cond ((zp n) nil)
(t (cons 0 (zeros (- n 1))))))
(defun create (n)
(declare (xargs :guard (posp n)))
(s :data (zeros n) ; use of 0 is arbitrary; any value would be OK
(s :size n
(s :first 0
(s :len 0
nil ; empty record
)))))
(defun clear (b)
(declare (xargs :guard (ring-buffer-p b)))
(s :len 0 b))
; Note: By specifying the :guards below for get-val and set-val we insure that
; any use of those functions in other guarded defuns will cause ACL2 to prove
; that array indices are in bounds.
(defun get-val (a i)
(declare (xargs :guard (and (true-listp a)
(natp i)
(< i (len a)))))
(nth i a))
(defun set-val (a i v)
(declare (xargs :guard (and (true-listp a)
(natp i)
(< i (len a)))))
(update-nth i v a))
(defun head (b)
(declare (xargs :guard (and (ring-buffer-p b)
(not (empty-p b)))))
(get-val (g :data b)
(g :first b)))
; For rules about mod etc.:
(include-book "arithmetic-5/top" :dir :system)
(defun pushb (b x)
(declare (xargs :guard (and (ring-buffer-p b)
(not (full-p b)))))
(let* ((len (g :len b))
(b (s :data
(set-val (g :data b)
(mod (+ (g :first b) len)
(g :size b))
x)
b))
(b (s :len (+ len 1) b)))
b))
(defun popb (b)
; We return both the value popped and the new ring buffer, since we are
; programming in a functional language without global variables (and hence b
; cannot be modified in place or as a global).
; We use ACL2's multiple-value construct to define (popb b) so that it returns
; a vector of two results, written (mv r b), where r is the value popped
; and b is the new ring buffer.
(declare (xargs :guard (and (ring-buffer-p b)
(not (empty-p b)))))
(let* ((first (g :first b))
(data (g :data b))
(size (g :size b))
(len (g :len b))
(r (get-val data first))
(b (s :first
(mod (+ first 1) size)
b))
(b (s :len (- len 1) b)))
(mv r b)))
;;; 1. Safety. Verify that every array access is made within bounds.
; For safety (every array access is made within bounds), we rely on ACL2's
; guard mechanism. The guards of get-val and set-val guarantee that every
; access is in bounds, because the index is a natural number less than the
; length of the array.
;;; 2. Behavior. Verify the correctness of your implementation w.r.t. the
;;; first-in first-out semantics of a queue.
; We define a simple semantics based on lists.
(defun firstn (n x) ; first n elements of the list x
(declare (xargs :guard (and (natp n)
(true-listp x)
(<= n (len x)))))
(cond ((zp n) nil)
(t (cons (car x)
(firstn (- n 1) (cdr x))))))
(defun dropn (n x) ; delete first n elements of the list x
(declare (xargs :guard (and (natp n)
(true-listp x)
(<= n (len x)))))
(cond ((zp n) x)
(t (dropn (- n 1) (cdr x)))))
(defthm true-listp-dropn
(implies (<= n (len x))
(equal (true-listp (dropn n x))
(true-listp x))))
(defthm len-dropn
(implies (and (natp n)
(<= n (len x)))
(equal (len (dropn n x))
(- (len x) n))))
(defun contents (b)
; This function specifies the contents of a ring-buffer as an ordinary list,
; where the oldest elements are towards the front and the newest are towards
; the back.
(declare (xargs :guard (ring-buffer-p b)))
(let ((first (g :first b))
(data (g :data b))
(size (g :size b))
(len (g :len b)))
(cond ((<= (+ first len) size)
(firstn len (dropn first data)))
(t (let ((final (- size first)))
(append (firstn final (dropn first data))
(firstn (- len final) data)))))))
; Now, the theorems....
; Start proof of empty-p-correct.
(defthm firstn-iff-reduction
(iff (firstn i a)
(posp i))
:hints (("Goal" :expand ((firstn i a)))))
(defthm append-iff-reduction
(iff (append x y)
(or (consp x)
y)))
(defthm empty-p-correct
(implies (ring-buffer-p b)
(iff (empty-p b)
(equal (contents b)
nil))))
; Start proof of full-p-correct.
(defthm len-append
(equal (len (append a b))
(+ (len a) (len b))))
(defthm len-firstn
(equal (len (firstn n x))
(nfix n)))
(defthm full-p-correct
(implies (ring-buffer-p b)
(iff (full-p b)
(equal (len (contents b))
(g :size b)))))
(defthm create-correct
(implies (natp n)
(equal (contents (create n))
nil)))
(defthm clear-correct
(implies (ring-buffer-p b)
(equal (contents (clear b))
nil)))
; Start proof of head-correct.
(defthm car-firstn
(equal (car (firstn n x))
(if (zp n)
nil
(car x))))
(defthm car-append
(equal (car (append x y))
(if (consp x)
(car x)
(car y))))
(defthm consp-firstn
(equal (consp (firstn n x))
(not (zp n))))
(defthm car-dropn
(implies (and (natp n)
(< n (len x)))
(equal (car (dropn n x))
(nth n x))))
(defthm head-correct
(implies (and (ring-buffer-p b)
(not (empty-p b)))
(equal (head b)
(car (contents b)))))
; Start proof of pushb-correct.
(defthm append-assoc
(equal (append (append x y) z)
(append x (append y z))))
(defthm dropn-update-nth
(implies (and (natp key)
(natp n)
(<= n (len a))
(< key (len a)))
(equal (dropn n (update-nth key val a))
(if (< key n)
(dropn n a)
(update-nth (- key n) val (dropn n a))))))
(defthm firstn-cdr-update-nth-as-append
(implies (posp n)
(equal (firstn n
(cdr (update-nth n x a)))
(append (firstn (1- n) (cdr a))
(list x)))))
(defthm pushb-correct
(implies (and (ring-buffer-p b)
(not (full-p b)))
(equal (contents (pushb b x))
(append (contents b) (list x))))
; After proving full-p-correct, our original proof no longer went through;
; hence, the following hint.
:hints (("Goal" :in-theory (disable full-p-correct))))
; Start proof of popb-correct.
(defthm dropn-cdr
(equal (dropn n (cdr a))
(cdr (dropn n a))))
(defthm mod-1-k
(implies (natp k)
(equal (mod 1 k)
(if (equal k 1) 0 1))))
(defthm firstn-1
(equal (firstn 1 x)
(list (car x))))
; Note: The mv-let construct below binds the variables r and b2 to the two
; values returned by (popb b) and then evaluates the subsequent equality in
; that scope.
(defthm popb-correct
(implies (and (ring-buffer-p b)
(not (empty-p b)))
(mv-let (r b2)
(popb b)
(equal (cons r (contents b2))
(contents b)))))
; Finally, we really should show that the data type is preserved by the
; operations.
(defthm ring-buffer-p-preserved
(and (implies (posp n)
(ring-buffer-p (create n)))
(implies (ring-buffer-p b)
(ring-buffer-p (clear b)))
(implies (and (ring-buffer-p b)
(not (full-p b)))
(ring-buffer-p (pushb b x)))
(implies (and (ring-buffer-p b)
(not (empty-p b)))
(b* (((mv - b2) (popb b)))
(ring-buffer-p b2))))
:otf-flg t)
;;; 3. Harness. The following test harness should be verified.
;;; test (x: int, y: int, z: int) :=
;;; b <- create(2);
;;; push(b, x);
;;; push(b, y);
;;; h <- pop(b); assert h = x;
;;; push(b, z);
;;; h <- pop(b); assert h = y;
;;; h <- pop(b); assert h = z;
(defthm test-harness
; Think of the following lines as a sequence of assignment statements. ACL2's
; b*, a user-defined macro introduced in the bstar book loaded earlier, is an
; extension of Lisp's let* macro for sequential variable binding, except it
; also permits one to bind a vector of variables to the corresponding values
; returned by a multi-valued function like popb. (B* extends let* in other
; ways not relevant here.) The three variables check1, check2, and check3, are
; just bound to Booleans at the spots in the sequence where the problem
; statement had asserts. At the bottom of the b* we confirm that all three
; checks are true. This is proved automatically of course, by symbolic
; expansion of the definitions.
(b* ((b (create 2))
(b (pushb b x))
(b (pushb b y))
((mv h b) (popb b)) ; h is the value popped; b is the new ring-buffer
(check1 (equal h x)) ; check1 should be true
(b (pushb b z))
((mv h b) (popb b))
(check2 (equal h y)) ; check2 should be true
((mv h -) (popb b))
(check3 (equal h z)) ; check3 should be true
)
(and check1 check2 check3)))
; We conclude with a ground instance of the test-harness above, where x, y, and
; z are bound to specific integers. We then evaluate the b* expression,
; carrying out the sequence of creates, pushes, and pops, just to demonstrate
; that our model is executable.
(assert-event
(let ((x 123)(y 456) (z 789))
(b* ((b (create 2))
(b (pushb b x))
(b (pushb b y))
((mv h b) (popb b))
(check1 (equal h x))
(b (pushb b z))
((mv h b) (popb b))
(check2 (equal h y))
((mv h -) (popb b))
(check3 (equal h z))
)
(and check1 check2 check3))))