; This is the script for the flying demo.  It is divided into two
; parts by a line of hyphens.

; This is the first part.  It should be carried out before the demo
; starts.  It consists of commands to configure emacs and load a few
; things into ACL2.

; (1) Fire up an emacs on this directory.  Put this file in one
; buffer, named script.lisp.  Set up a shell buffer named *shell*.
; Run acl2 in that shell.

; (2) Execute the following Emacs Lisp code.  You can do this by
; grabbing the s-expression below and typing meta-: ctrl-y Return,
; i.e., yank the s-expression into the Emacs Eval command.

(progn
  (fset 'scroll-acl2-prompt-to-top
   "\C-r!>\M-0\C-l\C-x\C-x")
  (fset 'back-to-acl2-prompt
   "\C-r!>\C-r\C-f\C-f\M-0\C-l\C-a")
  (fset 'back-to-end-of-buffer
        "\M->")
  (defun yank-sexp-into-shell ()
    "Yanks current sexp into the buffer named *shell*"
    (interactive)
    (forward-char)
    (beginning-of-defun)
    (let ((pos (point))) 
      (forward-sexp)
      (kill-ring-save pos (point)))
    (forward-sexp)
    (backward-sexp)
    (switch-to-buffer "*shell*")
    (goto-char (point-max))
    (yank))
  
  (fset 'yank-sexpr-into-shell-from-last-buffer-visited
        "\C-xb\C-m\M-xyank-sexp-into-shell")

  (global-set-key "[" 'scroll-acl2-prompt-to-top)
  (global-set-key "{" 'back-to-acl2-prompt)
  (global-set-key "\M-[" 'back-to-acl2-prompt)
  (global-set-key "\M-]" 'back-to-end-of-buffer)
  (global-set-key "]" 'yank-sexpr-from-last-buffer-visited))

; This s-expression above sets up the following emacs commands.
;  [   to move the current acl2 prompt line to the top and
;  ]   to yank the next event from this file into the shell.
;  M-[ to return to last prompt

; (3) Search below for the include-book that mentions
; books/arithmetic/top and change the absolute directory to wherever
; the books directory is located on your local host.
; 
; (4) Position the Emacs cursor just before the (value :q) below,
; change to buffer *shell* (which has ACL2 running in it), hit \M-] to
; go to the bottom of the buffer, and then repeatedly hit the ] key
; until you see ACL2 type "Almost ready...".  That message will tell
; you to type one more ].

(value :q)
(setq si:*notify-gbc* nil)
(lp)

(progn

(defthm append-right-id
         (implies (true-listp a)
                  (equal (append a nil) a)))

(defthm equal-len-0
         (equal (equal (len x) 0) (atom x)))

(include-book "/projects/acl2/v2-5/books/arithmetic/top")

; Here we define functions for treating lists as stacks.

(defun empty-stackp (stk) (endp stk))
(defun pop-stack (stk) (cdr stk))
(defun top-stack (stk) (if (consp stk) (car stk) 0))
(defun push-stack (val stk) (cons val stk))

(defun lookup (x alist)
  (cond
   ((endp alist) 0)
   ((equal x (caar alist)) (cdar alist))
   (t (lookup x (cdr alist)))))

(defun bind (name val alist)
  (cons (cons name val) alist))

(defun lookup-all (names alist)
        (cond ((endp names) nil)
              (t (cons (lookup (car names) alist)
                       (lookup-all (cdr names) alist)))))

(defun xor (p q) (if p (if q nil t) (if q t nil)))

(defun maj (p q c)
        (or (and p q)
            (or (and p c)
                (and q c))))

(defun evaluate-gate (gate alist)
        (cond
         ((atom gate) (lookup gate alist))
         (t
          (case (car gate)
            (xor (xor (lookup (cadr gate) alist)
                      (lookup (caddr gate) alist)))
            (maj (maj (lookup (cadr gate) alist)
                      (lookup (caddr gate) alist)
                      (lookup (cadddr gate) alist)))
            (t nil)))))

(defun net-val-hint (a b c i alist)
        (cond ((endp a) (list b c i alist))
              (t (net-val-hint (cdr a)
                               (cdr b)
                               (+ i 2)
                               (+ i 3)
                               (list* (cons (+ 2 i)
                                            (maj (lookup (car a) alist)
                                                 (lookup (car b) alist)
                                                 (lookup c alist)))
                                      (cons (+ 1 i)
                                            (xor (lookup (car a) alist)
                                                 (xor (lookup (car b) alist)
                                                      (lookup c alist))))
                                      (cons i
                                            (xor (lookup (car b) alist)
                                                 (lookup c alist)))
                                      alist)))))

(defthm input-lookup-all-not-changed
         (implies (and (integerp i)
                       (symbol-listp a))
                  (equal (lookup-all a (cons (cons i x) alist))
                         (lookup-all a alist))))

)

(include-book "isort")

(defun tjvm::object-class nil
 '("Object" NIL NIL NIL))

(in-theory (disable TJVM::COMMUTATIVITY2-OF-+
                    TJVM::PLUS-RIGHT-ID
                    TJVM::CONSTANT-FOLD-+
                    TJVM::*-0
                    TJVM::COMMUTATIVITY2-OF-*))

(value :q)
(quote "Almost ready...

I generally put the next line of output, ACL2's banner, at the top of the
buffer with \M-0 \C-l before starting the demo.  Type one more ], position
the buffer appropriately, and begin the demo by continuing to type ]'s.")

(lp)


; ---------------------------------------------------------------------------
; Demo Starts Here

; Things I will demonstrate:
; evaluation of ACL2 expressions
; correctness of Lisp insertion sort
; correctness of bit-vector adder and multiplier
; correctness of netlist generator
; correctness of simple expression compiler for stack machine
; correctness of Java byte code implementation of insertion sort

(+ 3 4)

(equal (car (cons 1 '(2 3 4))) 1)

(thm (equal (car (cons x y)) x))

(endp nil)
(endp '(1 2 3 4))



(thm (implies (and (not (endp x))
                          (endp (cdr x))
                          (integerp n)
                          (<= 0 n)
                          (rationalp u))
                     (< (* (len x) u) (+ u n 3))))

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

(insert 3 '(1 2 4 5))

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

(isort '(5 4 6 7 2 1 0 3))

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

(ordered '(1 2 3 4))
(ordered '(1 2 3 3 4))
(ordered '(1 3 2 4))

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

(pe 'perm)

(perm '(1 2 3 3 4) '(4 3 1 2 3))
(perm '(1 2 3 3 4) '(4 3 1 2 2))

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

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

(buggy-insert 3 '(1 2 4 5))
(buggy-insert 3 '(1 2))

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

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

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

(defthm buggy-isort-is-nil
  (equal (buggy-isort x) nil))
  

; Binary Addition and Multiplication with Bit Vectors

(defun full-adder (p q c)
        (mv (xor p (xor q c))
            (maj p q c)))

(full-adder t t nil)
(full-adder nil nil t)

(defun serial-adder (a b c)
        (declare (xargs :measure (+ (acl2-count a) (acl2-count b))))
        (if (and (endp a) (endp b))
            (list c)
          (mv-let (sum cout)
                  (full-adder (car a) (car b) c)
                  (cons sum (serial-adder (cdr a) (cdr b) cout)))))

(serial-adder '(t t nil)
                     '(t nil t)
                      nil)
(serial-adder '(t t nil)
                     '(t nil t)
                     t)
(serial-adder '(t t nil)
                     '()
                     t)

(defconst *a*
        '(t nil nil t t t t t nil t t t nil t nil t
          nil t nil t t t t t t t t t t t nil nil
          nil nil nil t t t t t nil t t t nil t nil t
          t t nil t t t t t nil t nil t t nil nil t
          t nil nil t t t t t nil t nil t nil t t t
          nil t nil t t t t t nil t nil t nil t nil nil
          t nil nil t t t t t t t t t t t nil nil
          nil nil nil t t t t t t t t t nil t nil t
          nil nil nil nil t t t t t t nil t nil nil t t))

(defconst *b*
        '(t t t t t t t t t t nil t nil t nil t
          t nil t t t t t t t t t t nil nil nil nil
          nil nil nil t t t t t nil t nil t t t t t
          t nil nil t t t t t t t t t t nil t nil
          t nil t nil t t t t t t t t t nil nil nil
          nil t t t t t t t nil t nil t t t t nil
          t nil t nil t t t t nil t nil t t nil nil t
          nil nil nil t t t t t nil t nil t nil t nil nil
          nil t t t t t t t t t t t nil t nil t))

(serial-adder *a* *b* nil)

(defun n (v)
        (cond ((endp v) 0)
              ((car v) (+ 1 (* 2 (n (cdr v)))))
              (t (* 2 (n (cdr v))))))

(n '(t t nil))

(n *a*)
(n *b*)
(+ (n *a*) (n *b*))
(n (serial-adder *a* *b* nil))

(defthm serial-adder-correct
  (equal (n (serial-adder x y c))
         (+ (n x) (n y) (if c 1 0))))

(defthm serial-adder-special-case
  (and (equal (n (serial-adder x nil t)) (+ 1 (n x)))
       (equal (n (serial-adder x nil nil)) (n x))))

(defthm serial-adder-correct
  (equal (n (serial-adder x y c))
         (+ (n x) (n y) (if c 1 0))))


; Here is a shift-and-add multiplier.  

(defun multiplier (x y p)
  (if (endp x)
      p
    (multiplier (cdr x)
		(cons nil y)
		(if (car x)
		    (serial-adder y p nil)
		  p))))

(n '(nil nil nil t nil t t t t t))

(n (multiplier '(nil nil nil t nil t t t t t) 
                      '(nil nil nil t nil t t t t t)
                      nil))

(defthm multiplier-correct
  (equal (n (multiplier x y p))
         (+ (* (n x) (n y)) (n p))))

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

; This function generates a netlist for a ripple-carry adder.

(defun adder-net (a b c i)
        (cond
         ((endp a)
          `((,i ,c *)))
         (t `((,i (xor ,(car b) ,c))
              (,(+ i 1) (xor ,(car a) ,i) *)
              (,(+ i 2) (maj ,(car a) ,(car b) ,c))
              ,@(adder-net (cdr a)
                           (cdr b)
                           (+ i 2)
                           (+ i 3))))))

; For example:

(adder-net '(a0 a1 a2) '(b0 b1 b2) 'c 0)

; Here is the semantics of this simple netlist description language.

(defun net-val (netlist alist)
        (cond
         ((endp netlist) nil)
         (t (let* ((wire-name (car (car netlist)))
                   (gate-expr (cadr (car netlist)))
                   (output-flag (caddr (car netlist)))
                   (val (evaluate-gate gate-expr alist))
                   (ans (net-val (cdr netlist)
                                 (bind wire-name val alist))))
              (cond
               ((eq output-flag '*)
                (cons val ans))
               (t ans))))))

; For example,

(net-val '((0 (xor a1 b1))
                  (1 (xor c 0) *))
                '((a1 . t) (b1 . nil) (c . nil)))

; Here are a few lemmas I will need.

(defthm true-listp-adder-net
         (true-listp (adder-net a b c i)))

; This theorem establishes that the adder-net is correct, in the
; sense that its value is that of the serial adder.

(defthm adder-net-is-serial-adder
         (implies (and (symbol-listp a)
                       (symbol-listp b)
                       (equal (len a) (len b))
                       (integerp i)
                       (or (symbolp c)
                           (and (integerp c)
                                (< c i))))
                  (equal (net-val (adder-net a b c i) alist)
                         (serial-adder (lookup-all a alist)
                                       (lookup-all b alist)
                                       (lookup c alist))))
  :hints (("Goal" :induct (net-val-hint a b c i alist)
                  :in-theory (disable xor maj))))

; Consequently:

(defthm adder-net-is-correct
  (implies (and (symbol-listp a)
                (symbol-listp b)
                (equal (len a) (len b))
                (integerp i)
                (or (symbolp c)
                    (and (integerp c)
                         (< c i))))
           (equal (n (net-val (adder-net a b c i) alist))
                  (+ (n (lookup-all a alist))
                     (n (lookup-all b alist))
                     (if (lookup c alist) 1 0)))))


; So here is a ``big'' adder

(adder-net 
         '(a00 a01 a02 a03 a04 a05 a06 a07 a08 a09
           a10 a11 a12 a13 a14 a15 a16 a17 a18 a19
           a20 a21 a22 a23 a24 a25 a26 a27 a28 a29
           a30 a31 a32 a33 a34 a35 a36 a37 a38 a39
           a40 a41 a42 a43 a44 a45 a46 a47 a48 a49
           a50 a51 a52 a53 a54 a55 a56 a57 a58 a59
           a60 a61 a62 a63 a64 a65 a66 a67 a68 a69
           a70 a71 a72 a73 a74 a75 a76 a77 a78 a79
           a80 a81 a82 a83 a84 a85 a86 a87 a88 a89
           a90 a91 a92 a93 a94 a95 a96 a97 a98 a99)
         '(b00 b01 b02 b03 b04 b05 b06 b07 b08 b09
           b10 b11 b12 b13 b14 b15 b16 b17 b18 b19
           b20 b21 b22 b23 b24 b25 b26 b27 b28 b29
           b30 b31 b32 b33 b34 b35 b36 b37 b38 b39
           b40 b41 b42 b43 b44 b45 b46 b47 b48 b49
           b50 b51 b52 b53 b54 b55 b56 b57 b58 b59
           b60 b61 b62 b63 b64 b65 b66 b67 b68 b69
           b70 b71 b72 b73 b74 b75 b76 b77 b78 b79
           b80 b81 b82 b83 b84 b85 b86 b87 b88 b89
           b90 b91 b92 b93 b94 b95 b96 b97 b98 b99)
         'c
         0)

               
           
(defun execute (instr alist stk)
        (let ((op (car instr)))
          (cond
           ((equal op 'load)
            (push-stack (lookup (cadr instr) alist) stk))
           ((equal op 'push)
            (push-stack (cadr instr) stk))
           ((equal op 'dup)
            (push-stack (top-stack stk) stk))
           ((equal op 'add)
            (push-stack (+ (top-stack (pop-stack stk)) (top-stack stk))
                        (pop-stack (pop-stack stk))))
           ((equal op 'mul)
            (push-stack (* (top-stack (pop-stack stk)) (top-stack stk))
                        (pop-stack (pop-stack stk))))
           (t stk))))

(execute '(LOAD A)  '((A . 7) (B . 4))   '(3 2 1))
(execute '(PUSH A)  '((A . 7) (B . 4))   '(3 2 1))
(execute '(DUP)     '((A . 7) (B . 4))   '(3 2 1))
(execute '(ADD)     '((A . 7) (B . 4))   '(3 2 1))
(execute '(MUL)     '((A . 7) (B . 4))   '(3 2 1))

; A program is a list of instructions.

(defun m (program alist stk)
         (cond ((endp program) stk)
               ((m (cdr program)
                   alist
                   (execute (car program) alist stk)))))

(m '((LOAD A) (DUP) (ADD)) '((A . 7) (B . 4))  '(0 0 0))

(defun evaluate (x alist)
         (cond
          ((atom x)
           (cond ((symbolp x) (lookup x alist))
                 (t x)))
          ((equal (len x) 2)
           (cond
            ((equal (car x) 'inc)
             (+ 1 (evaluate (cadr x) alist)))
            ((equal (car x) 'sq)
             (* (evaluate (cadr x) alist)
                (evaluate (cadr x) alist)))
            (t 0)))
          ((equal (cadr x) '+)
           (+ (evaluate (car x) alist)
              (evaluate (caddr x) alist)))
          ((equal (cadr x) '*)
           (* (evaluate (car x) alist)
              (evaluate (caddr x) alist)))
          (t 0)))

(evaluate '((3 * b) + a)   '((a . 7) (b . 4)))

(m '((PUSH 3) (LOAD B) (MUL) (LOAD A) (ADD)) '((a . 7) (b . 4)) nil)

(defun compile-expression (x)
         (cond
          ((atom x)
           (cond
            ((symbolp x) (list (list 'load x)))
            (t (list (list 'push x)))))
          ((equal (len x) 2)
           (cond
            ((eq (car x) 'inc)
             (append (compile-expression (cadr x))
                     '((push 1)
                       (add))))
            ((eq (car x) 'sq)
             (append (compile-expression (cadr x))
                     '((dup)
                       (mul))))
            (t (list (list 'push 0)))))
          ((eq (cadr x) '+)
           (append (compile-expression (car x))
                   (compile-expression (caddr x))
                   '((add))))
          ((eq (cadr x) '*)
           (append (compile-expression (car x))
                   (compile-expression (caddr x))
                   '((mul))))
          (t (list (list 'push 0)))))

(compile-expression '(SQ (INC (A + (3 * B)))))

(defthm sequential-execution
         (equal (m (append x y) a s)
                (m y a (m x a s))))

(defun hintfn (x a s)
        (cond
         ((atom x) (list x a s))
         ((equal (len x) 2)
          (cond
           ((eq (car x) 'inc)
            (hintfn (cadr x) a s))
           ((eq (car x) 'sq)
            (hintfn (cadr x) a s))
           (t (list x a s))))
         ((eq (cadr x) '+)
          (cons (hintfn (car x) a s)
                (hintfn (caddr x) a (push-stack (evaluate (car x) a) s))))
         ((eq (cadr x) '*)
          (cons (hintfn (car x) a s)
                (hintfn (caddr x) a (push-stack (evaluate (car x) a) s))))
         (t (list x a s))))
   
(defthm key-compiler-lemma
         (equal (m (compile-expression x) a s)
                (push-stack (evaluate x a) s))
         :hints (("Goal" :induct (hintfn x a s))))

(defthm main-compiler-thm
        (equal (top-stack (m (compile-expression x) a s))
               (evaluate x a))
        :rule-classes nil)



(in-package "TJVM")

(pe 'step)
(pe 'next-inst)
(pe 'do-inst)
(pe 'execute-load)
(pe 'execute-invokevirtual)
(pe 'tjvm)

(cons-class)

(defconst *s0*
         (make-state
          (push                                         ; activation stack
           (make-frame 1                                ;  pc
                       '((x . (REF 4)))                 ;  local vars
                       '((REF 4))                       ;  stack
                       '((load x)                       ;  byte code
                         (invokestatic "Cons" "isort" 1);   for most
                         (halt)))                       ;   recent method
           nil)
          '((0 ("Cons" ("car" . 5) ("cdr" . 0))         ; heap
               ("Object"))
            (1 ("Cons" ("car" . 1) ("cdr" REF 0))
               ("Object"))
            (2 ("Cons" ("car" . 4) ("cdr" REF 1))
               ("Object"))
            (3 ("Cons" ("car" . 2) ("cdr" REF 2))
               ("Object"))
            (4 ("Cons" ("car" . 3) ("cdr" REF 3))
               ("Object")))
          (list (cons-class)                            ; class table
                (object-class))))

(deref* (top (stack (top-frame *s0*))) (heap *s0*))

(defconst *s1* (tjvm *s0* 250))

(deref* (top (stack (top-frame *s1*))) (heap *s1*))

(pe 'isort-spec)

(pe 'tjvm-isort-lemma)

(quote "The End")

; Note: In some versions of this demo I have introduced the partial
; function step* which steps a tjvm state until it halts.  Then I've
; defined (== a b) to be the induced equivalence relation and shown
; theorems about fact and isort that do not involve clocks.  These
; theorems have indeed been proved by methods that suggest I can
; operate entirely without clocks if I am content to consider a form
; of partial correctness.  But I have not yet stabilized my lemma
; library about step* and == and so don't want to release these demos
; just yet.  (JSM June 26, 2000).