; (ld "isort.lisp" :ld-pre-eval-print t)
#|

; Certification instructions:

(DEFPKG "TJVM"
  (set-difference-equal
   (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP
                           QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))
   '(PC PROGRAM PUSH POP REVERSE STEP ++)))


(certify-book "isort" 1)

JSM June, 2000
|#

(in-package "TJVM")

(include-book "examples")

; We start by defining an important invariant on the heap.  We do it
; piecewise and then conjoin the pieces.  We could develop a more
; general treatment, but because I'm in a hurry I will focus on heaps
; constructed entirely by the cons method.

(defun cons-method ()
  '("cons" (x y)
    (new "Cons")
    (store temp)
    (load temp)
    (load x)
    (putfield "Cons" "car")
    (load temp)
    (load y)
    (putfield "Cons" "cdr")
    (load temp)
    (xreturn)))

(defun cons-clock () 11)

(defun heap-car (ref heap)
; Return the car field of a ref in the heap.
  (field-value "Cons" "car" (deref ref heap)))

(defun heap-cdr (ref heap)
; Return the cdr field of a ref in the heap.
  (field-value "Cons" "cdr" (deref ref heap)))

(defun heap-cons (x y heap)
; Construct the heap produced by consing x and y.
  (bind (len heap)
        (list (list "Cons" (cons "car" x) (cons "cdr" y))
              '("Object"))
        heap))

; It is trivial to prove that the cons method above implements
; heap-cons.  But we don't do that yet.  We're interested in our
; invariant.  The bulk of the invariant has nothing to do with the
; proof of cons and everything to do with chasing pointers.

(defthm heap-car-cons
  (equal (heap-car addr
                   (heap-cons x y heap))
         (if (equal (cadr addr) (len heap))
             x
           (heap-car addr heap))))

(defthm heap-cdr-cons
  (equal (heap-cdr addr
                   (heap-cons x y heap))
         (if (equal (cadr addr) (len heap))
             y
           (heap-cdr addr heap))))

(defthm len-bind
  (implies (case-split (alistp alist))
           (equal (len (bind key val alist))
                  (if (bound? key alist)
                      (len alist)
                    (+ 1 (len alist))))))

(defthm alistp-bind
  (implies (alistp alist)
           (alistp (bind key val alist))))

; Conjunct (1) Alistp is the first conjunct of our heap invariant.
; Here we show that it is preserved by heap-cons.

(defthm alistp-heap
  (implies (alistp heap)
           (alistp (heap-cons x y heap))))

; Conjunct (2): Every key bound in the heap is a natural number less
; than the length of the heap.

(defun all-smallp (heap max)
  (cond ((endp heap) t)
        (t (and (integerp (caar heap))
                (<= 0 (caar heap))
                (< (caar heap) max)
                (all-smallp (cdr heap) max)))))

(defthm len-heap-cons
  (implies (and (alistp heap)
                (all-smallp heap (len heap)))
           (equal (len (heap-cons x y heap))
                  (+ 1 (len heap)))))

(defthm all-smallp-bind
  (implies (and (all-smallp alist max1)
                (<= max1 max2))
           (equal (all-smallp (bind key val alist) max2)
                  (and (integerp key)
                       (<= 0 key)
                       (< key max2)))))

; So here is the lemma that shows that all-smallp is preserved by
; heap-cons.

(defthm all-smallp-heap
  (implies (and (alistp heap)
                (all-smallp heap (- max 1)))
           (equal (all-smallp (heap-cons x y heap) max)
                  (< (len heap) max))))

; Conjunct (3) Every address less than the heap length is bound.

(defun all-bound? (heap n)
  (cond ((zp n) t)
        (t (and (bound? (- n 1) heap)
                (all-bound? heap (- n 1))))))

(defthm all-bound?-bind
  (implies (and (integerp n)
                (<= 0 n)
                (integerp k)
                (<= n k)
                (alistp alist))
           (equal (all-bound? (bind k val alist) n)
                  (all-bound? alist n))))

; This too is preserved by heap-cons.

(defthm all-bound?-heap
  (implies (and (alistp heap)
                (all-bound? heap (len heap)))
           (all-bound? (heap-cons x y heap) (+ 1 (len heap)))))

; Conjunct (4) Every ref in a "cdr" field in the heap points to a
; legal address smaller than that for the cons holding it.

(defun all-refs-smallp (heap)
  (cond
   ((endp heap) t)
   (t (let ((d (field-value "Cons" "cdr" (cdar heap))))
        (and (or (equal d 0)
                 (and (refp d)
                      (<= 0 (cadr d))
                      (< (cadr d) (caar heap))))
             (all-refs-smallp (cdr heap)))))))

(defthm all-refs-smallp-bind
  (implies (and (alistp heap)
                (all-smallp heap max)
                (all-refs-smallp heap)
                (integerp key)
                (<= 0 key)
                (<= max key))
           (equal (all-refs-smallp (bind key val heap))
                  (let ((d (field-value "Cons" "cdr" val)))
                    (or (equal d 0)
                        (and (refp d)
                             (<= 0 (cadr d))
                             (< (cadr d) key)))))))

(defun ok-refp (y heap)
  (or (equal y 0)
      (and (refp y)
           (<= 0 (cadr y))
           (< (cadr y) (len heap)))))


(defthm all-refs-smallp-heap
  (implies (and (alistp heap)
                (all-smallp heap (len heap))
                (all-refs-smallp heap))
           (equal (all-refs-smallp (heap-cons x y heap))
                  (ok-refp y heap))))


(defun heap-invariantp (heap)
  (and (alistp heap)
       (all-smallp heap (len heap))
       (all-bound? heap (len heap))
       (all-refs-smallp heap)))

(defthm all-smallp-implies-unbound-len
  (implies (all-smallp heap max)
           (not (assoc-equal max heap))))

(defthm heap-invariantp-heap
  (implies (and (heap-invariantp heap)
                (ok-refp y heap))
           (heap-invariantp (heap-cons x y heap))))


(in-theory (disable heap-car heap-cdr heap-cons heap-invariantp ok-refp))

(defun ref-measure (x)
  (cond
   ((equal x 0) 0)
   (t (+ 1 (acl2-count (cadr x))))))

(defthm all-bound?-is-a-quantifier
  (implies (and (all-bound? heap max)
                (integerp max)
                (integerp k)
                (<= 0 k)
                (< k max))
           (assoc-equal k heap)))

(defthm ref-addresses-are-bound
  (implies (and (heap-invariantp heap)
                (ok-refp y heap)
                (case-split (not (equal y 0))))
           (assoc-equal (cadr y) heap))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))
                
(defthm all-refs-smallp-is-a-quantifier
  (implies (and (all-refs-smallp heap)
                (assoc-equal k heap))
           (let ((d (CDR
                     (ASSOC-EQUAL "cdr"
                                  (CDR (ASSOC-EQUAL
                                        "Cons"
                                        (cdr (assoc-equal k heap))))))))
             (or (equal d 0)
                 (and (refp d)
                      (<= 0 (cadr d))
                      (< (cadr d) k)))))
  :rule-classes nil)

; This is the measure theorem for our heap exploration functions.

(defthm ref-measure-decreases
  (implies (and (not (equal xref 0))
                (heap-invariantp heap)
                (ok-refp xref heap))
           (< (ref-measure (heap-cdr xref heap))
              (ref-measure xref)))
  :rule-classes :linear
  :hints (("Goal"
           :in-theory (enable heap-invariantp ok-refp heap-cdr)
           :use
           ((:instance all-refs-smallp-is-a-quantifier
                       (heap heap)
                       (k (cadr xref)))))))

(in-theory (disable ref-measure))

(defun insert-method ()
  '("insert" (e x)
    (load x)
    (ifeq 18)
    (load x)
    (getfield "Cons" "car")
    (load e)
    (sub)
    (ifle 5)   ; if (car x) <= e, then skip 5
    (load e)
    (load x)
    (invokestatic "Cons" "cons" 2)
    (xreturn)
    (load x)
    (getfield "Cons" "car")
    (load e)
    (load x)
    (getfield "Cons" "cdr")
    (invokestatic "Cons" "insert" 2)
    (invokestatic "Cons" "cons" 2)
    (xreturn)
    (load e)
    (load x)
    (invokestatic "Cons" "cons" 2)
    (xreturn)))

(defun insert-clock (e xref heap)
  (declare
   (xargs :measure (ref-measure xref)))
  (cond
   ((equal xref 0)
    (++ 5 (cons-clock) 1))
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    0)
   ((<= (heap-car xref heap) e)
    (++ 13
        (insert-clock e
                      (heap-cdr xref heap)
                      heap)
        (cons-clock)
        1))
   (t (++ 10 (cons-clock) 1))))

(defun isort-method ()
  '("isort" (x)
    (load x)
    (ifeq 8)
    (load x)
    (getfield "Cons" "car")
    (load x)
    (getfield "Cons" "cdr")
    (invokestatic "Cons" "isort" 1)
    (invokestatic "Cons" "insert" 2)
    (xreturn)
    (load x)
    (xreturn)))

(defun heap-insert (e xref heap)
  (declare (xargs :measure (ref-measure xref)))
  (cond ((equal xref 0)
         (heap-cons e 0 heap))
        ((not (and (heap-invariantp heap)
                   (ok-refp xref heap)))
         heap)
        ((<= (heap-car xref heap) e)
         (let ((new-heap (heap-insert e
                                      (heap-cdr xref heap)
                                      heap)))
           (heap-cons (heap-car xref heap)
                      (list 'ref (- (len new-heap) 1))
                      new-heap)))
        (t (heap-cons e xref heap))))



(defun heap-isort (xref heap)
  (declare
   (xargs :measure (ref-measure xref)))
  (cond
   ((equal xref 0)
    heap)
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    heap)
   (t
    (heap-insert (heap-car xref heap)
                 (if (equal (heap-cdr xref heap) 0)
                     0
                   (list 'ref
                         (- (len (heap-isort (heap-cdr xref heap)
                                            heap))
                            1)))
                 (heap-isort (heap-cdr xref heap)
                            heap)))))
                 

(defun isort-clock (xref heap)
  (declare
   (xargs :measure (ref-measure xref)))
  (cond
   ((equal xref 0)
    5)
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    0)
   (t
    (++ 7
        (isort-clock (heap-cdr xref heap) heap)
        (insert-clock (heap-car xref heap)
                      (if (equal (heap-cdr xref heap) 0)
                          0
                        (list 'ref
                            (- (len (heap-isort (heap-cdr xref heap) heap))
                               1)))
                      (heap-isort (heap-cdr xref heap) heap))
        1))))
    
    


(defun Cons-class ()
  (make-class-decl "Cons"
                   '("Object")
                   '("car" "cdr")
                   (list (cons-method)
                         (insert-method)
                         (isort-method)
                         )))

(defun standard-hyps (s)
  (and (equal (assoc-equal "Cons" (class-table s))
              (Cons-class))
       (equal (assoc-equal "Object" (class-table s))
              '("Object" nil nil nil))
       (heap-invariantp (heap s))))



#|Test
(thm
  (implies (and (standard-hyps s0)
                (ok-refp y (heap s0)))
           (standard-hyps
            (make-state
             (push (make-frame (+ 1 (pc (top-frame s0)))
                               (locals (top-frame s0))
                               (push (list 'ref (len (heap s0)))
                                     (pop (pop (stack (top-frame s0)))))
                               (program (top-frame s0)))
                   (pop (call-stack s0)))
             (heap-cons x y (heap s0))
             (class-table s0)))))|#


; We will need this to maintain the ok-refp hyp through inductions.

(defthm ok-ref-heap-cdr
  (implies (and (heap-invariantp heap)
                (not (equal xref 0))
                (ok-refp xref heap))
           (ok-refp (heap-cdr xref heap) heap))
  :hints
  (("Goal" :in-theory (enable heap-invariantp
                              ok-refp
                              heap-cdr)
    :use ((:instance all-refs-smallp-is-a-quantifier
                     (heap heap)
                     (k (cadr xref)))))))

(defthm bind-bind
  (equal (bind n v1 (bind n v2 h)) (bind n v1 h)))


(defthm cons-spec
  (implies (and (equal (next-inst s0) '(invokestatic "Cons" "cons" 2))
                (standard-hyps s0)
                (equal x (top (pop (stack (top-frame s0)))))
                (equal y (top (stack (top-frame s0)))))
           (equal
            (tjvm s0 (cons-clock))
            (make-state
             (push (make-frame (+ 1 (pc (top-frame s0)))
                               (locals (top-frame s0))
                               (push (list 'ref (len (heap s0)))
                                     (pop (pop (stack (top-frame s0)))))
                               (program (top-frame s0)))
                   (pop (call-stack s0)))
             (heap-cons x y (heap s0))
             (class-table s0))))
  :hints
  (("Goal''" :in-theory (enable heap-cons))))

(in-theory (disable cons-clock (cons-clock)))


(defun heap-insert-hint (s0 e x)
  (declare (xargs :measure (ref-measure x)))
  (cond
   ((equal x 0)
    (list s0 e x))
   ((not (and (heap-invariantp (heap s0))
              (ok-refp x (heap s0))))
    (list s0 e x))
   ((<= (heap-car x (heap s0)) e)
    (heap-insert-hint
     (make-state
      (push
       (make-frame 16
                   (list (cons 'e e)
                         (cons 'x (top (stack (top-frame s0)))))
                   (push (heap-cdr x (heap s0))
                         (push e
                               (push (heap-car x (heap s0))
                                     nil)))
                   (method-program (insert-method)))
       (push
        (make-frame (+ 1 (pc (top-frame s0)))
                    (locals (top-frame s0))
                    (pop (pop (stack (top-frame s0))))
                    (program (top-frame s0)))
        (pop (call-stack s0))))
      (heap s0)
      (class-table s0))
     e
     (heap-cdr x (heap s0))))
   (t (list s0 e x))))

; I have arranged to keep heap-car and heap-cdr disabled.  I have
; lemmas about them.  But tjvm introduces them in their expanded
; forms.  So I close them up.  If you enable heap-car, be sure to
; disable this; likewise for heap-cdr!

(defthm heap-car-folder
  (equal
   (CDR
    (ASSOC-EQUAL
     "car"
     (CDR (ASSOC-EQUAL
           "Cons"
           (CDR (ASSOC-EQUAL (CADR xref)
                             heap))))))
   (heap-car xref heap))
  :hints (("Goal" :in-theory (enable heap-car))))

(defthm heap-cdr-folder
  (equal
   (CDR
    (ASSOC-EQUAL
     "cdr"
     (CDR (ASSOC-EQUAL
           "Cons"
           (CDR (ASSOC-EQUAL (CADR xref)
                             heap))))))
   (heap-cdr xref heap))
  :hints (("Goal" :in-theory (enable heap-cdr))))


  
  


(defthm weak-len-heap-cons
  (implies (alistp heap)
           (<= (len heap) (len (heap-cons x y heap))))
  :rule-classes :linear
  :hints (("Goal" :in-theory (enable heap-cons))))


(defthm alistp-heap-insert
  (implies (alistp heap)
           (alistp (heap-insert e xref heap))))


(defthm ok-refp-list-ref
  (implies (and (heap-invariantp heap)
                (ok-refp xref heap))
          (ok-refp (list 'ref (- (len (heap-insert e xref heap)) 1))
                   (heap-insert e xref heap)))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))



(defthm heap-invariantp-heap-insert
  (implies (and (heap-invariantp heap)
                (ok-refp xref heap))
           (heap-invariantp (heap-insert e xref heap))))

(defthm len-heap-cons-lifted
  (implies (heap-invariantp heap)
           (equal (len (heap-cons x y heap))
                  (+ 1 (len heap))))
  :hints (("Goal" :in-theory (enable heap-invariantp))))

(defthm insert-spec-generalized
  (implies (and (equal (next-inst s0) '(invokestatic "Cons" "insert" 2))
                (standard-hyps s0)
                (ok-refp x (heap s0))
                (equal e (top (pop (stack (top-frame s0)))))
                (equal x (top (stack (top-frame s0))))
                (equal heap (heap s0)))
           (equal
            (tjvm s0 (insert-clock e x heap))
            (make-state
             (push (make-frame (+ 1 (pc (top-frame s0)))
                               (locals (top-frame s0))
                               (push (list 'ref
                                           (- (len (heap-insert e x (heap s0)))
                                              1))
                                     (pop (pop (stack (top-frame s0)))))
                               (program (top-frame s0)))
                   (pop (call-stack s0)))
             (heap-insert e x (heap s0))
             (class-table s0))))
  :hints (("Goal" :induct (heap-insert-hint s0 e x)
           :do-not '(acl2::generalize acl2::eliminate-destructors))))


(defun deref* (xref heap)
  (declare (xargs :measure (ref-measure xref)))
  (cond
   ((equal xref 0) nil)
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    nil)
   (t (cons (heap-car xref heap)
            (deref* (heap-cdr xref heap) heap)))))


(defun insert (e x)
  (cond ((endp x) (cons e x))
        ((< e (car x)) (cons e x))
        (t (cons (car x) (insert e (cdr x))))))

(defthm ok-refp-heap-cons
  (implies (and (HEAP-INVARIANTP HEAP)
                (ok-refp xref heap))
           (ok-refp xref (heap-cons e xref1 heap)))
  :hints
  (("Goal" :in-theory (enable heap-invariantp ok-refp heap-cons))))

(defthm foo1
  (IMPLIES (AND (HEAP-INVARIANTP HEAP)
                (OK-REFP XREF HEAP))
           (equal (EQUAL (CADR XREF) (LEN HEAP))
                  nil))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))


(defthm foo2
  (IMPLIES (AND (HEAP-INVARIANTP HEAP)
                (OK-REFP XREF1 HEAP)
                (OK-REFP XREF HEAP))
           (EQUAL (DEREF* xref1
                          (HEAP-CONS E XREF HEAP))
                  (DEREF* xref1 HEAP))))

(defthm foo3
  (IMPLIES (HEAP-INVARIANTP HEAP)
           (OK-REFP (LIST 'REF (LEN HEAP))
                    (HEAP-CONS E XREF HEAP)))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))
  
(defthm deref*-heap-insert
  (implies (and (heap-invariantp heap)
                (ok-refp xref heap))
           (equal (deref* (list 'ref (- (len (heap-insert e xref heap)) 1))
                          (heap-insert e xref heap))
                  (insert e (deref* xref heap)))))



(defun heap-isort-hint (s0 x)
  (declare (xargs :measure (ref-measure x)))
  (cond
   ((equal x 0)
    (list s0 x))
   ((not (and (heap-invariantp (heap s0))
              (ok-refp x (heap s0))))
    (list s0 x))
   (t
    (heap-isort-hint
     (make-state
      (push
       (make-frame 6
                   (list (cons 'x (top (stack (top-frame s0)))))
                   (push (heap-cdr x (heap s0))
                         (push (heap-car x (heap s0))
                               nil))
                   (method-program (isort-method)))
       (push
        (make-frame (+ 1 (pc (top-frame s0)))
                    (locals (top-frame s0))
                    (pop (stack (top-frame s0)))
                    (program (top-frame s0)))
        (pop (call-stack s0))))
      (heap s0)
      (class-table s0))
     (heap-cdr x (heap s0))))))




(defthm alistp-heap-isort
  (implies (alistp heap)
           (alistp (heap-isort xref heap))))


(defthm weak-len-heap-insert
  (implies (alistp heap)
           (<= (len heap) (len (heap-insert x y heap))))
  :rule-classes :linear
  :hints (("Goal" :in-theory (enable heap-cons))))


(defthm ok-refp-list-ref-heap-isort
  (implies (and (heap-invariantp heap)
                (case-split (not (equal xref 0)))
                (ok-refp xref heap))
          (ok-refp (list 'ref (- (len (heap-isort xref heap)) 1))
                   (heap-isort xref heap)))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))

(defthm ok-refp-list-ref-len-heap
  (implies (and (heap-invariantp heap)
                (case-split (consp heap)))
           (ok-refp (list 'ref (- (len heap) 1))
                    heap))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))

(defthm foo4
  (IMPLIES (and (heap-invariantp heap)
                (ok-refp xref heap)
                (not (equal xref 0)))
           (consp (heap-isort xref2 heap)))
  :hints (("Goal" :in-theory (enable heap-invariantp ok-refp))))

(defthm ok-refp-0
  (ok-refp 0 heap)
  :hints (("Goal" :in-theory (enable ok-refp))))

(defthm heap-invariantp-heap-isort
  (implies (and (heap-invariantp heap)
                (ok-refp xref heap))
           (heap-invariantp (heap-isort xref heap))))

(defthm isort-spec-generalized
  (implies (and (equal (next-inst s0) '(invokestatic "Cons" "isort" 1))
                (standard-hyps s0)
                (ok-refp x (heap s0))
                (equal x (top (stack (top-frame s0))))
                (equal heap (heap s0)))
           (equal
            (tjvm s0 (isort-clock x heap))
            (make-state
             (push (make-frame (+ 1 (pc (top-frame s0)))
                               (locals (top-frame s0))
                               (push (if (equal x 0)
                                         0
                                       (list 'ref
                                             (- (len (heap-isort x (heap s0)))
                                                1)))
                                     (pop (stack (top-frame s0))))
                               (program (top-frame s0)))
                   (pop (call-stack s0)))
             (heap-isort x (heap s0))
             (class-table s0))))
  :hints (("Goal" :induct (heap-isort-hint s0 x)
           :do-not '(acl2::generalize acl2::eliminate-destructors))))

(defun isort (x)
        (if (endp x)
            nil
          (insert (car x)
                  (isort (cdr x)))))

(defthm deref*-heap-isort
  (implies (and (heap-invariantp heap)
                (ok-refp xref heap)
                (not (equal xref 0)))
           (equal (deref* (list 'ref (- (len (heap-isort xref heap)) 1))
                          (heap-isort xref heap))
                  (isort (deref* xref heap)))))

(defthm tjvm-isort-lemma
  (implies (and (standard-hyps s0)
                (equal (next-inst s0)
                       '(invokestatic "Cons" "isort" 1)))

           (let* ((x0 (top (stack (top-frame s0))))
                  (heap0 (heap s0))
                  (n0 (isort-clock x0 heap0))
                  (s1 (tjvm s0 n0))
                  (x1 (top (stack (top-frame s1))))
                  (heap1 (heap s1)))

             (implies (ok-refp x0 heap0)
                      (equal (deref* x1 heap1)
                             (isort (deref* x0 heap0)))))))



(defun ordered (x)
  (cond ((endp x) t)
        ((endp (cdr x)) t)
        (t (and (<= (car x) (car (cdr x)))
                (ordered (cdr x))))))

(include-book "perm")

(defun perm (x y) (acl2::perm x y))                           

(defthm ordered-isort
  (ordered (isort x)))

(defthm perm-isort
  (perm (isort x) x))

(in-theory (disable isort-spec-generalized
                    top-frame
                    perm))

(defthm isort-spec
  (implies (and (standard-hyps s0)
                (equal (next-inst s0)
                       '(invokestatic "Cons" "isort" 1)))

           (let* ((x0 (top (stack (top-frame s0))))
                  (heap0 (heap s0))
                  (n0 (isort-clock x0 heap0))
                  (s1 (tjvm s0 n0))
                  (x1 (top (stack (top-frame s1))))
                  (heap1 (heap s1)))

             (implies (ok-refp x0 heap0)

                      (let ((list0 (deref* x0 heap0))
                            (list1 (deref* x1 heap1)))
                        (and (ordered list1)
                             (perm list1 list0)))))))