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

; Certification instructions:

(include-book "utilities")

(certify-book "isort" 1)

JSM June, 2000
|#

(in-package "M5")

#|
Here is Isort.java:

class Cons {
    int car;
    Object cdr;
    public static Cons cons(int x, Object y){
	Cons c = new Cons();
        c.car = x;
	c.cdr = y;
	return c;
    }
}
    
class ListProc extends Cons {
    public static Cons insert(int e,Object x){
	if (x==null)
	    {return cons(e,x);}
	else if (e <= ((Cons)x).car)
	    {return cons(e,x);}
	else return cons(((Cons)x).car,insert(e,((Cons)x).cdr));
    }

    public static Object isort(Object x){
	if (x==null)
	    {return x;}
	else return insert(((Cons)x).car,isort(((Cons)x).cdr));
    }
}
---------------------------------------------------------------------------
And here is the bytecode generated by javac and displayed by javap:

javap -c Cons
Compiled from Isort.java
synchronized class Cons extends java.lang.Object 
    /* ACC_SUPER bit set */
{
    int car;
    java.lang.Object cdr;
    public static Cons cons(int, java.lang.Object);
    Cons();
}

Method Cons cons(int, java.lang.Object)
   0 new #1 <Class Cons>
   3 dup
   4 invokespecial #4 <Method Cons()>
   7 astore_2
   8 aload_2
   9 iload_0
  10 putfield #6 <Field int car>
  13 aload_2
  14 aload_1
  15 putfield #7 <Field java.lang.Object cdr>
  18 aload_2
  19 areturn

Method Cons()
   0 aload_0
   1 invokespecial #5 <Method java.lang.Object()>
   4 return
---------------------------------------------------------------------------
javap -c ListProc
Compiled from Isort.java
synchronized class ListProc extends Cons 
    /* ACC_SUPER bit set */
{
    public static Cons insert(int, java.lang.Object);
    public static java.lang.Object isort(java.lang.Object);
    ListProc();
}

Method Cons insert(int, java.lang.Object)
   0 aload_1
   1 ifnonnull 10
   4 iload_0
   5 aload_1
   6 invokestatic #6 <Method Cons cons(int, java.lang.Object)>
   9 areturn
  10 iload_0
  11 aload_1
  12 checkcast #1 <Class Cons>
  15 getfield #4 <Field int car>
  18 if_icmpgt 27
  21 iload_0
  22 aload_1
  23 invokestatic #6 <Method Cons cons(int, java.lang.Object)>
  26 areturn
  27 aload_1
  28 checkcast #1 <Class Cons>
  31 getfield #4 <Field int car>
  34 iload_0
  35 aload_1
  36 checkcast #1 <Class Cons>
  39 getfield #5 <Field java.lang.Object cdr>
  42 invokestatic #7 <Method Cons insert(int, java.lang.Object)>
  45 invokestatic #6 <Method Cons cons(int, java.lang.Object)>
  48 areturn

Method java.lang.Object isort(java.lang.Object)
   0 aload_0
   1 ifnonnull 6
   4 aload_0
   5 areturn
   6 aload_0
   7 checkcast #1 <Class Cons>
  10 getfield #4 <Field int car>
  13 aload_0
  14 checkcast #1 <Class Cons>
  17 getfield #5 <Field java.lang.Object cdr>
  20 invokestatic #8 <Method java.lang.Object isort(java.lang.Object)>
  23 invokestatic #7 <Method Cons insert(int, java.lang.Object)>
  26 areturn

Method ListProc()
   0 aload_0
   1 invokespecial #3 <Method Cons()>
   4 return
---------------------------------------------------------------------------
|#

; Here is the state.  This state was hand created by reading the javap
; output.  (I don't have access to jvm2acl2 from this particular
; machine.)  I have had to omit several CHECKCAST instructions because
; they are not supported by M5.

(defconst *Isort-state*
  (make-state
   (list
    (cons 0
          (make-thread
           (push
            (make-frame
             0
             nil
             nil
             '()
             'UNLOCKED
             "ListProc")
            nil)
           'SCHEDULED
           nil)))
   '((0 . (("java.lang.Class"
           ("<name>" . "java.lang.Object"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (1 . (("java.lang.Class"
           ("<name>" . "ARRAY"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (2 . (("java.lang.Class"
           ("<name>" . "java.lang.Thread"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (3 . (("java.lang.Class"
           ("<name>" . "java.lang.String"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (4 . (("java.lang.Class"
           ("<name>" . "java.lang.Class"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (5 . (("java.lang.Class"
           ("<name>" . "Cons"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0))))
    (6 . (("java.lang.Class"
           ("<name>" . "ListProc"))
          ("java.lang.Object"
           ("monitor" . 0)
           ("mcount" . 0)
           ("wait-set" . 0)))))
   '(("java.lang.Object"
     NIL
     ("monitor" "mcount" "wait-set")
     NIL
     NIL
     (("<init>" NIL NIL (RETURN)))
     (REF 0))
    ("ARRAY"
     ("java.lang.Object")
     (("<array>" . *ARRAY*))
     NIL
     NIL
     NIL
     (REF 1))
    ("java.lang.Thread"
     ("java.lang.Object")
     NIL
     NIL
     NIL
     (("run" NIL NIL (RETURN))
      ("start" NIL NIL NIL)
      ("stop" NIL NIL NIL)
      ("<init>" NIL NIL (ALOAD\_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 2))
    ("java.lang.String"
     ("java.lang.Object")
     ("strcontents")
     NIL
     NIL
     (("<init>" NIL NIL
       (ALOAD\_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 3))
    ("java.lang.Class"
     ("java.lang.Object")
     NIL
     NIL
     NIL
     (("<init>" NIL NIL
       (ALOAD\_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN)))
     (REF 4))
    ("Cons"
     ("java.lang.Object")
     ("car" "cdr")
     nil
     nil
     (("<init>" NIL NIL
       (ALOAD\_0)
       (INVOKESPECIAL "java.lang.Object" "<init>" 0)
       (RETURN))
      ("cons" (int java.lang.Object) nil
       (NEW "Cons")
       (DUP)
       (INVOKESPECIAL "Cons" "<init>" 0)
       (ASTORE_2)
       (ALOAD_2)
       (ILOAD_0)
       (PUTFIELD "Cons" "car")
       (ALOAD_2)
       (ALOAD_1)
       (PUTFIELD "Cons" "cdr")
       (ALOAD_2)
       (ARETURN))))
    ("ListProc"
     ("Cons" "java.lang.Object")
     nil
     nil
     nil
     (("<init>" nil nil
       (ALOAD\_0)
       (INVOKESPECIAL "Cons" "<init>" 0)
       (RETURN))
      ("insert" (int java.lang.Object) nil
        (aload_1)
        (ifnonnull 9)
        (iload_0)
        (aload_1)
        (invokestatic "Cons" "cons" 2)
        (areturn)
        (iload_0)
        (aload_1)
                                  ;;; checkcast "Cons" ommitted
        (getfield "Cons" "car")
        (if_icmpgt 9)
        (iload_0)
        (aload_1)
        (invokestatic "Cons" "cons" 2)
        (areturn)
        (aload_1)
                                  ;;; checkcast "Cons" ommitted
        (getfield "Cons" "car")
        (iload_0)
        (aload_1)
                                  ;;; checkcast "Cons" ommitted
        (getfield "Cons" "cdr")
        (invokestatic "ListProc" "insert" 2)
        (invokestatic "Cons" "cons" 2)
        (areturn))
      ("isort" (java.lang.Object) nil
       (aload_0)
       (ifnonnull 5)
       (aload_0)
       (areturn)
       (aload_0)
                                  ;;; checkcast "Cons" ommitted
       (getfield "Cons" "car")
       (aload_0)
                                  ;;; checkcast "Cons" ommitted
       (getfield "Cons" "cdr")
       (invokestatic "ListProc" "isort" 1)
       (invokestatic "ListProc" "insert" 2)
       (areturn)))))))

; Now we will name some parts of the state for future use.

(defconst *Object-class*
  (bound? "java.lang.Object" (class-table *Isort-state*)))

(defconst *Cons-class*
  (bound? "Cons" (class-table *Isort-state*)))

(defconst *ListProc-class*
  (bound? "ListProc" (class-table *Isort-state*)))

(defconst *cons-def*
  (lookup-method "cons" "Cons" (class-table *Isort-state*)))

(defconst *insert-def*
  (lookup-method "insert" "ListProc" (class-table *Isort-state*)))

(defconst *isort-def*
  (lookup-method "isort" "ListProc" (class-table *Isort-state*)))

(defconst *Isort-heap0*
  (heap *Isort-state*))

(defconst *Isort-class-table*
  (class-table *Isort-state*))

(defun cons-sched (th)
  (repeat th 17))

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

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

(defun cons-heap (x y heap)
; Construct the heap produced by consing x and y.
  (bind (len heap)
        (list (list "Cons" (cons "car" x) (cons "cdr" y))
              '("java.lang.Object"
                ("monitor" . 0)
                ("mcount" . 0)
                ("wait-set" . 0)))
        heap))

; It is trivial to prove that the cons method above implements
; cons-heap.  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 car-heap-cons-heap
  (equal (car-heap addr
                   (cons-heap x y heap))
         (if (equal (cadr addr) (len heap))
             x
           (car-heap addr heap))))

(defthm cdr-heap-cons-heap
  (equal (cdr-heap addr
                   (cons-heap x y heap))
         (if (equal (cadr addr) (len heap))
             y
           (cdr-heap 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 cons-heap.

(defthm alistp-cons-heap
  (implies (alistp heap)
           (alistp (cons-heap 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-cons-heap
  (implies (and (alistp heap)
                (all-smallp heap (len heap)))
           (equal (len (cons-heap 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
; cons-heap.

(defthm all-smallp-cons-heap
  (implies (and (alistp heap)
                (all-smallp heap (- max 1)))
           (equal (all-smallp (cons-heap 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 cons-heap.

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

; Conjunct (4) Every ref in a "cdr" field of a "cons" in the heap is
; either the null pointer or a ref to a lower address.

(defun refp (x)
  (and (consp x)
       (equal (car x) 'ref)
       (consp (cdr x))
       (integerp (cadr x))
       (equal (cddr x) nil)))

(defun all-refs-smallp (heap)
  (cond
   ((endp heap) t)
   ((not (bound? "Cons" (cdar heap)))
    (all-refs-smallp (cdr heap)))
   (t (let ((d (field-value "Cons" "cdr" (cdar heap))))
        (and (or (nullrefp d)
                 (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))
                  (or (not (bound? "Cons" val))
                      (let ((d (field-value "Cons" "cdr" val)))
                        (or (nullrefp d)
                            (and (refp d)
                                 (<= 0 (cadr d))
                                 (< (cadr d) key))))))))

(defun ok-refp (x heap)

; We check that x is a legal ref to occupy the cdr of some cons:
; it is either the null reference or a reference to a "Cons".

  (or (nullrefp x)
      (and (refp x)
           (<= 0 (cadr x))
           (< (cadr x) (len heap))
           (bound? "Cons" (deref x heap)))))

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

; Conjunct (5) Every "cdr" field of every "cons" is occupied by a nullref or
; a "cons" ref.

(defun cdr-type-correctnessp (alist heap)
  (cond ((endp alist) t)
        ((bound? "Cons" (cdar alist))
         (and (ok-refp (field-value "Cons" "cdr" (cdar alist)) heap)
              (cdr-type-correctnessp (cdr alist) heap)))
        (t (cdr-type-correctnessp (cdr alist) heap))))

(defthm cdr-type-correctnessp-bind
  (implies (cdr-type-correctnessp alist heap)
           (iff (cdr-type-correctnessp (bind key val alist) heap)
                (if (bound? "Cons" val)
                    (ok-refp (field-value "Cons" "cdr" val) heap)
                  t))))

(defun heap-extensionp (heap1 heap2)
  (cond ((endp heap1) t)
        ((endp heap2) nil)
        (t (and (equal (car heap1) (car heap2))
                (heap-extensionp (cdr heap1) (cdr heap2))))))

(defthm len-heap-extensionp
  (implies (heap-extensionp heap1 heap2)
           (<= (len heap1) (len heap2)))
  :rule-classes :linear)

(defthm cdr-type-correctnessp-heap-extensionp
  (implies (and (cdr-type-correctnessp alist heap1)
                (heap-extensionp heap1 heap2))
           (cdr-type-correctnessp alist heap2)))

(defthm assoc-equal-heap-extensionp
  (implies (and (assoc-equal key heap1)
                (heap-extensionp heap1 heap2))
           (equal (assoc-equal key heap1)
                  (assoc-equal key heap2))))

(defthm assoc-equal-implies-assoc-equal
  (implies (assoc-equal key1 (cdr (assoc-equal key2 alist)))
           (assoc-equal key2 alist)))

(defthm cdr-type-correctness-cons-heap-lemma
  (implies (and (cdr-type-correctnessp alist heap1)
                (ok-refp y heap1)
                (heap-extensionp heap1 heap2))
           (cdr-type-correctnessp (cons-heap x y alist)
                                  heap2))
  :rule-classes nil)

(in-theory (disable assoc-equal-heap-extensionp))

(defthm heap-extensionp-bind
  (implies (and (alistp heap)
                (not (assoc-equal key heap)))
           (heap-extensionp heap (bind key val heap))))

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

(defthm cdr-type-correctness-heap
  (implies (and (alistp heap)
                (all-smallp heap (len heap))
                (cdr-type-correctnessp heap heap)
                (ok-refp y heap))
           (cdr-type-correctnessp (cons-heap x y heap)
                                  (cons-heap x y heap)))
  :hints (("Goal" :use (:instance
                        cdr-type-correctness-cons-heap-lemma
                        (alist heap)
                        (heap1 heap)
                        (heap2 (cons-heap x y heap))))))

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


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


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

(defun ref-measure (x)
  (cond
   ((nullrefp x) 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 (nullrefp y))))
           (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))
           (or (not (bound? "Cons" (cdr (assoc-equal k heap))))
               (let ((d (CDR
                         (ASSOC-EQUAL "cdr"
                                      (CDR (ASSOC-EQUAL
                                            "Cons"
                                            (cdr (assoc-equal k heap))))))))
                 (or (nullrefp d)
                     (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 (force (not (nullrefp xref)))
                (heap-invariantp heap)
                (ok-refp xref heap))
           (< (ref-measure (cdr-heap xref heap))
              (ref-measure xref)))
  :rule-classes :linear
  :hints (("Goal"
           :in-theory (enable heap-invariantp ok-refp cdr-heap)
           :use
           ((:instance all-refs-smallp-is-a-quantifier
                       (heap heap)
                       (k (cadr xref)))))))

(in-theory (disable ref-measure))

(defun insert-sched (th e xref heap)
  (declare
   (xargs :measure (ref-measure xref)))
  (cond
   ((nullrefp xref)
    (append (repeat th 5)
            (cons-sched th)
            (repeat th 1)))
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    nil)
   ((< (car-heap xref heap) e)
    (append (repeat th 12)
            (insert-sched th
                          e
                          (cdr-heap xref heap)
                          heap)
            (cons-sched th)
            (repeat th 1)))
   (t (append (repeat th 9)
              (cons-sched th)
              (repeat th 1)))))

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


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

(defun isort-sched (th xref heap)
  (declare
   (xargs :measure (ref-measure xref)))
  (cond
   ((nullrefp xref)
    (repeat th 5))
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    nil)
   (t
    (append (repeat th 7)
            (isort-sched th (cdr-heap xref heap) heap)
            (insert-sched th
                          (car-heap xref heap)
                          (if (nullrefp (cdr-heap xref heap))
                              '(ref -1)
                            (list 'ref
                                  (- (len (isort-heap
                                           (cdr-heap xref heap)
                                           heap))
                                     1)))
                          (isort-heap (cdr-heap xref heap) heap))
            (repeat th 1)))))
    
    
(defun deref* (xref heap)
  (declare (xargs :measure (ref-measure xref)))
  (cond
   ((nullrefp xref) nil)
   ((not (and (heap-invariantp heap)
              (ok-refp xref heap)))
    nil)
   (t (cons (car-heap xref heap)
            (deref* (cdr-heap xref heap) heap)))))

; Here is an example execution of isort on the list (3 2 1) producing
; the list (1 2 3).  The isort call takes 188 steps.

(defthm isort-3-2-1
  (let* ((s0
          (make-state
           (list
            (cons 0
                  (make-thread
                   (push
                    (make-frame
                     0
                     '((REF -1))
                     nil
                     '((bipush 3)
                       (bipush 2)
                       (bipush 1)
                       (aload_0)
                       (invokestatic "Cons" "cons" 2)
                       (invokestatic "Cons" "cons" 2)
                       (invokestatic "Cons" "cons" 2)
                       (invokestatic "ListProc" "isort" 1)
                       (halt))
                     'UNLOCKED
                     "ListProc")
                    nil)
                   'SCHEDULED
                   nil)))
           *isort-heap0*
           *isort-class-table*))
         (s1
          (run (append (repeat 0 4)
                       (cons-sched 0)
                       (cons-sched 0)
                       (cons-sched 0))
               s0))
         (sched (isort-sched 0
                             (top (stack (top-frame 0 s1)))
                             (heap s1)))
         (s2 (run sched s1)))
    (and (equal (deref* (top (stack (top-frame 0 s1)))
                        (heap s1))
                '(3 2 1))
         (equal (len sched) 188)
         (heap-invariantp (heap s2))
         (equal (deref* (top (stack (top-frame 0 s2)))
                        (heap s2))
                '(1 2 3))
         (equal (next-inst 0 s2) '(HALT))))
  :rule-classes nil)


(defun standard-hyps (th s)
  (and (equal (status th s) 'SCHEDULED)
       (equal (assoc-equal "java.lang.Object" (class-table s))
              *Object-class*)
       (equal (assoc-equal "Cons" (class-table s))
              *Cons-class*)
       (equal (assoc-equal "ListProc" (class-table s))
              *ListProc-class*)
       (heap-invariantp (heap s))))



#|Test -- (i-am-here) get rid of this.  it is very confusing.
(thm
  (implies (and (standard-hyps 0 s0)
                (ok-refp y (heap s0)))
           (standard-hyps
            0
            (make-state
             (list (cons 0
                         (make-thread
                          (push (make-frame (+ 1 (pc (top-frame 0 s0)))
                                            (locals (top-frame 0 s0))
                                            (push (list 'ref (len (heap s0)))
                                                  (pop (pop (stack (top-frame 0 s0)))))
                                            (program (top-frame 0 s0))
                                            'unlocked
                                            class)
                                (pop (call-stack 0 s0)))
                          'SCHEDULED
                          nil)))
             (cons-heap x y (heap s0))
             (class-table s0)))))|#


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

(defthm cdr-type-correctness-is-a-quantifier
  (implies (and (alistp alist)
                (cdr-type-correctnessp alist heap)
                (assoc-equal k alist))
           (or (not (bound? "Cons" (cdr (assoc-equal k alist))))
               (nullrefp (field-value "Cons" "cdr" (cdr (assoc-equal k alist))))
               (bound? "Cons" (deref (field-value "Cons" "cdr" (cdr (assoc-equal k alist))) heap))))
  :hints (("Goal" :in-theory (enable ok-refp)))
  :rule-classes nil)
                                     
(defthm ok-ref-cdr-heap
  (implies (and (heap-invariantp heap)
                (not (nullrefp xref))
                (ok-refp xref heap))
           (ok-refp (cdr-heap xref heap) heap))
  :hints
  (("Goal" :in-theory (enable heap-invariantp
                              ok-refp
                              cdr-heap)
    :use ((:instance all-refs-smallp-is-a-quantifier
                     (heap heap)
                     (k (cadr xref)))
          (:instance cdr-type-correctness-is-a-quantifier
                     (alist heap)
                     (k (cadr xref)))))))

; I am not really sure if I need the type conditions on the two
; stack items or not.

(defun poised-to-invoke-cons (th s)
  (and (standard-hyps th s)
       (equal (next-inst th s) '(INVOKESTATIC "Cons" "cons" 2))
;      (intp (top (pop (stack (top-frame th s)))))
;      (ok-refp (top (stack (top-frame th s))) (heap s))
       ))

(defthm cons-is-correct
  (implies (poised-to-invoke-cons th s)
           (equal
            (run (cons-sched th) s)
            (modify th s
                    :pc (+ 3 (pc (top-frame th s)))
                    :stack (push (list 'REF (len (heap s)))
                                 (pop (pop (stack (top-frame th s)))))
                    :heap (cons-heap
                           (top (pop (stack (top-frame th s))))
                           (top (stack (top-frame th s)))
                           (heap s)))))
  :hints
  (("Goal" :in-theory (enable cons-heap))))

(in-theory (disable cons-sched))

(defun insert-heap-hint (th s e x)
  (declare (xargs :measure (ref-measure x)))
  (cond
   ((nullrefp x)
    (list th s e x))
   ((not (and (heap-invariantp (heap s))
              (ok-refp x (heap s))))
    (list th s e x))
   ((< (car-heap x (heap s)) e)
    (insert-heap-hint
     th
     (make-state
      (bind
       th
       (make-thread
        (push
         (make-frame 33
                     (list e x)
                     (push (cdr-heap x (heap s))
                           (push e
                                 (push (car-heap x (heap s))
                                       nil)))
                     (method-program *insert-def*)
                     'UNLOCKED
                     "ListProc")
         (push
          (make-frame (+ 3 (pc (top-frame th s)))
                      (locals (top-frame th s))
                      (pop (pop (stack (top-frame th s))))
                      (program (top-frame th s))
                      (sync-flg (top (call-stack th s)))
                      (cur-class (top (call-stack th s))))
          (pop (call-stack th s))))
        'SCHEDULED
        (rref th s))
       (thread-table s))
      (heap s)
      (class-table s))
     e
     (cdr-heap x (heap s))))
   (t (list th s e x))))

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

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

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

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


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

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

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

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

; Note that heap is an additional argument to this predicate.  The
; reason is that we use heap, instead of (heap s) in the insert-sched
; function.

(defun poised-to-invoke-insert (th s e x heap)
  (and (standard-hyps th s)
       (equal heap (heap s))
       (equal (next-inst th s) '(INVOKESTATIC "ListProc" "insert" 2))
       (equal e (top (pop (stack (top-frame th s)))))
       (equal x (top (stack (top-frame th s))))
;      (intp e)
       (ok-refp x (heap s))
       ))

(defthm insert-is-correct
  (implies (poised-to-invoke-insert th s e x heap)
           (equal
            (run (insert-sched th e x heap) s)
            (modify th s
                    :pc (+ 3 (pc (top-frame th s)))
                    :stack (push (list 'ref
                                       (- (len (insert-heap e x (heap s)))
                                          1))
                                 (pop (pop (stack (top-frame th s)))))
                    :heap (insert-heap e x (heap s)))))
  :hints (("Goal" :induct (insert-heap-hint th s e x)
           :do-not '(acl2::generalize acl2::eliminate-destructors))))

(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-cons-heap
  (implies (and (HEAP-INVARIANTP HEAP)
                (ok-refp xref heap))
           (ok-refp xref (cons-heap e xref1 heap)))
  :hints
  (("Goal" :in-theory (enable heap-invariantp ok-refp cons-heap))))

(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
                          (cons-heap E XREF HEAP))
                  (DEREF* xref1 HEAP))))

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

(defun isort-heap-hint (th s x)
  (declare (xargs :measure (ref-measure x)))
  (cond
   ((nullrefp x)
    (list th s x))
   ((not (and (heap-invariantp (heap s))
              (ok-refp x (heap s))))
    (list th s x))
   (t
    (isort-heap-hint
     th
     (make-state
      (bind
       th
       (make-thread
        (push
         (make-frame 14
                     (list x)
                     (push (cdr-heap x (heap s))
                           (push (car-heap x (heap s))
                                 nil))
                     (method-program *isort-def*)
                     'UNLOCKED
                     "ListProc")
         (push
          (make-frame (+ 3 (pc (top-frame th s)))
                      (locals (top-frame th s))
                      (pop (stack (top-frame th s)))
                      (program (top-frame th s))
                      (sync-flg (top (call-stack th s)))
                      (cur-class (top (call-stack th s))))
          (pop (call-stack th s))))
        'SCHEDULED
        (rref th s))
       (thread-table s))
      (heap s)
      (class-table s))
     (cdr-heap x (heap s))))))

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

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

(defthm ok-refp-nullrefp
  (ok-refp '(ref -1) heap)
  :hints (("Goal" :in-theory (enable ok-refp))))

(defthm ok-refp-heap-invariantp
  (implies (and (heap-invariantp heap)
                (force
                 (bound? "Cons"
                         (deref (list 'ref (+ -1 (len heap)))
                                heap))))
           (ok-refp (list 'ref (+ -1 (len heap))) heap))
  :hints (("Goal" :in-theory (enable heap-invariantp
                                     ok-refp))))

; The lemma above will force the bound? question for
; cons-heap and insert-heap on nonnull refs.  Let's do it.
; The bound? question is really an assoc-equal.

(defthm consp-cons-heap
  (assoc-equal "Cons"
               (cdr (assoc-equal (len heap)
                                 (cons-heap x y heap))))
  :hints (("Goal" :in-theory (enable heap-invariantp cons-heap))))

; The general form of the assoc-equal heap address in the lemma above
; is shown below, (+ -1 (len <heap-function>)).  But in the special
; case of cons-heap, that simplifies to (len heap) as used above.

(defthm consp-insert-heap
  (implies (and (heap-invariantp heap)
                (ok-refp x heap))
           (assoc-equal "Cons"
                        (cdr (assoc-equal (+ -1 (len (insert-heap e x heap)))
                                          (insert-heap e x heap))))))
(encapsulate
 nil
 (local
  (defthm strong-lemma
    (implies (and (heap-invariantp heap)
                  (not (nullrefp x))
                  (ok-refp x heap))
             (and (assoc-equal "Cons"
                               (cdr (assoc-equal
                                     (+ -1 (len (isort-heap x heap)))
                                     (isort-heap x heap))))
                  (heap-invariantp (isort-heap x heap))))))
 (defthm consp-isort-heap
   (implies (and (heap-invariantp heap)
                 (not (nullrefp x))
                 (ok-refp x heap))
            (assoc-equal "Cons"
                         (cdr (assoc-equal
                               (+ -1 (len (isort-heap x heap)))
                               (isort-heap x heap))))))
 (defthm heap-invariantp-isort-heap
   (implies (and (heap-invariantp heap)
                 (not (nullrefp x))
                 (ok-refp x heap))
            (heap-invariantp (isort-heap x heap)))))
 
(defun poised-to-invoke-isort (th s x heap)
  (and (standard-hyps th s)
       (equal heap (heap s))
       (equal (next-inst th s) '(INVOKESTATIC "ListProc" "isort" 1))
       (equal x (top (stack (top-frame th s))))
       (ok-refp x (heap s))))

(defthm isort-is-correct
  (implies (poised-to-invoke-isort th s x heap)
           (equal
            (run (isort-sched th x heap) s)
            (modify th s
                    :pc (+ 3 (pc (top-frame th s)))
                    :stack (push (if (nullrefp x)
                                     x
                                   (list 'ref
                                         (- (len (isort-heap x (heap s)))
                                            1)))
                                 (pop (stack (top-frame th s))))
                    :heap (isort-heap x (heap s)))))
  :hints (("Goal" :induct (isort-heap-hint th s x)
           :do-not '(acl2::generalize acl2::eliminate-destructors))))

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

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

(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 perm))

(defthm main-isort-theorem
  (let ((x0 (top (stack (top-frame th s))))
        (heap0 (heap s)))
    (implies (poised-to-invoke-isort th s x0 heap0)
             (let* ((sched (isort-sched th x0 heap0))
                    (s1 (run sched s))
                    (x1 (top (stack (top-frame th s1))))
                    (heap1 (heap s1)))
               (let ((list0 (deref* x0 heap0))
                     (list1 (deref* x1 heap1)))
                 (and (ordered list1)
                      (perm list1 list0))))))
  :rule-classes nil)