; JVM Problem Set 5
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;=============================================================
; In this problem set you will be expected to fill in the blanks
; to prove the correctness of several simple m0 programs.

; To proceed, first copy this file to a writeable directory.  Then
; execute each form in it, replacing the blanks (``***'') with
; appropriate expressions.

; To execute this file you will need to have access to two 
; certified books that have been posted on the class website:
; http://www.cs.uwyo.edu/~cowles/jvm-acl2/m0.lisp
; http://www.cs.uwyo.edu/~cowles/jvm-acl2/m0-utilities.lisp

; you should copy those two books to your file system and 
; recertify them, following the instructions in the two books.
; Then change the absolute path name below to point to your copy
; of m0-utilities.lisp.

(include-book "m0-utilities")

; (The form above will also include m0.lisp.)

(in-package "M0")

; To test whether your system is appropriately configured, try
; reproducing the following proof of the correctness of the
; *exp-program* which was described in class.

;; Define *exp-program* to be an m0 program that computes  b^n
;; for the local variables, b and n, provided the value of n is a
;; natural number and the value of b is a number, and leaves the
;; result on the stack.  The program should have only two local 
;; variables.

(defconst *exp-program*
                 ;; pc
  '((PUSH 1)     ;;  0  top := 1
   ;--------
    (GOTO 7)     ;;  1  while ( n > 0 )
   ;--------
    (LOAD b)     ;;  2      top := top * b  
    (MUL)        ;;  3
   ;--------
    (LOAD n)     ;;  4      n := n - 1
    (PUSH 1)     ;;  5
    (SUB)        ;;  6
    (STORE n)    ;;  7
   ;---------
    (LOAD n)     ;;  8  -------------- top of loop
    (IFGT -7)    ;;  9  end while
   ;---------
    (HALT)))     ;; 10

; Here is the tail recursive function that describes how the 
; loop in *exp-program* behaves.

(defun iexp-loop (b n top)
  (if (zp n)
      top
      (iexp-loop b (- n 1)(* b top))))

; Here is the function that describes how the entire 
; *exp-program* behaves.

(defun iexp (b n)
  (iexp-loop b n 1))

; Assuming that we have a state that is poised at the top of the
; exp loop, this function returns the number of steps that will
; drive  *exp-program* to the (HALT) statement.

(defun exp-prog-loop-steps (n)
  (if (zp n)
      2       ; Note: 2 steps take us to the HALT when n = 0.
      (+ 8 (exp-prog-loop-steps (- n 1)))))

; Assuming we have a state that is poised at the beginning of
; *exp-program*, this function returns the number of steps that
; will drive the machine to the (HALT) statement.

(defun exp-prog-steps(n)
  (+ 2 (exp-prog-loop-steps n)))

; Here is the theorem that establishes that the program loop
; computes the same thing as the iexp-loop function.  It says 
; that after (exp-prog-loop-steps n) clock ticks, we have pushed 
; (iexp-loop b n a) on the stack, where a is what's initially on
; the top of the stack.

(defthm exp-program-loop-is-iexp-loop
  (implies (and (integerp n)
                (>= n 0)
		(acl2-numberp b))
           (equal (run (modify nil
                               :pc      8
                               :program *exp-program*
                               :locals  (list (cons 'b b)
					      (cons 'n n))
                               :stack   (push a stk))
		       (exp-prog-loop-steps n))
                  (modify nil
                          :pc      10
                          :program *exp-program*
                          :locals  (list (cons 'b b)
					 (cons 'n 0))
                          :stack   (push (iexp-loop b n a) stk))
		  )))

; And here is the lemma that says *exp-program* computes
; (iexp b n) in (exp-prog-steps n) clock ticks.

(defthm exp-program-is-iexp
  (implies (and (integerp n)
                (>= n 0)
		(acl2-numberp b))
           (equal (run (modify nil
                               :pc      0
                               :program *exp-program*
                               :locals  (list (cons 'b b)
					      (cons 'n n))
                               :stack   stk)
		       (exp-prog-steps n))
                  (modify nil
                          :pc      10
                          :program *exp-program*
                          :locals   (list (cons 'b b)
					  (cons 'n 0))
                          :stack   (push (iexp b n) stk)))))

; By disabling exp-prog-steps now we make it possible for 
; subsequent programs to use the lemma exp-program-is-iexp.  
; (Think about it: if we have some target expression 
; (run ... (exp-prog-steps n)) that is being rewritten, then it
; will match with the left-hand side of the lemma above if the 
; state is appropriately formed.  But if the (exp-prog-steps n) 
; in the target is first rewritten, by expanding the definition of
; exp-prog-steps, then it won't match any more.  Thus, we disable
; exp-prog-steps.)

(in-theory (disable exp-prog-steps))

; Your ACL2 should process the above events without error if you
; have it properly configured.

; Problem 5.1
; We really don't want to know that *exp-program* computes 
; (iexp b n).  We want to know that it computes the following
; recursive version, (rexp b n), where

(defun rexp (b n)
  (if (zp n)
      1
      (* b (rexp b (- n 1)))))

; Prove the following theorem about the exp program.  Hint: Your
; proof should use the theorems above as lemmas.  Your proof 
; should not require further-analysis of *exp-program*!

; You will need to fill in this blank with one or more lemmas.

***

(defthm exp-program-is-correct
  (implies (and (integerp n)
                (>= n 0)
		(acl2-numberp b))
           (equal (run (modify nil
                               :pc      0
                               :program *exp-program*
                               :locals  (list (cons 'b b)
					      (cons 'n n))
                               :stack   stk)
		       (exp-prog-steps n))
                  (modify nil
                          :pc      10
                          :program *exp-program*
                          :locals   (list (cons 'b b)
					  (cons 'n 0))
                          :stack   (push (rexp b n) stk)))))

;;---------------------------------------------------------------
;; Here is an m0 program that computes n! for the local variable,
;; n, provided the value of n is a natural number, and leaves the
;; result on the stack.

(defconst *fact-program*
                  ;; pc
  '((PUSH 1)      ;;  0  top := 1  
    ;-------
    (GOTO 7)      ;;  1  while ( n > 0 )
    ;-------
    (LOAD n)      ;;  2      top := top * n
    (MUL)         ;;  3
    ;-------
    (LOAD n)      ;;  4      n := n - 1
    (PUSH 1)      ;;  5
    (SUB)         ;;  6
    (STORE n)     ;;  7
    ;--------
    (LOAD n)      ;;  8  -------------- top of loop
    (IFGT -7)     ;;  9  end while
    ;--------
    (HALT)))      ;; 10

; Problem 5.2
; Define the function that returns the number of steps that will
; drive the machine to the (HALT) statement for *fact-program*.
; Name the function fact-prog-steps.  It will take one argument,
; n.  (You will probably first define an auxilary function for
; computing the number of steps required for the loop in 
; *fact-program*.)

(defun fact-prog-steps(n)
  ***)

; Problem 5.3
; Our high level specification for *fact-program* is that it
; computes (! n), as defined below, and leaves that value on top
; of the stack.  Prove that *fact-program* is correct, as
; specified below.  You will have to prove several lemmas here:

(defun ! (n)
  (if (zp n)
      1
      (* n (! (- n 1)))))

***

(defthm fact-program-is-correct
  (implies (and (integerp n)
                (<= 0 n))
           (equal (run (modify nil
                               :pc      0
                               :program *fact-program*
                               :locals  (list (cons 'n n))
                               :stack   stk)
		       (fact-prog-steps n))
                  (modify nil
                          :pc      10
                          :program *fact-program*
                          :locals  (list (cons 'n 0))
                          :stack   (push (! n) stk)))))

;--------------------------------------------------------------
; Here is an m0 program that sums the natural numbers from 0 to n.
; Note that while fact accumulated its result on the stack, this
; one stores it in a local variable.  It also pushes the final 
; value of that variable on the stack.

(defconst *sum-nats-program*
  '((PUSH 0)               ;;;  0
    (STORE s)              ;;;  1
    (LOAD n)               ;;;  2
    (IFLE 10)              ;;;  3
    (LOAD n)               ;;;  4
    (LOAD s)               ;;;  5
    (ADD)                  ;;;  6
    (STORE s)              ;;;  7
    (LOAD n)               ;;;  8
    (PUSH -1)              ;;;  9
    (ADD)                  ;;; 10
    (STORE n)              ;;; 11
    (GOTO -10)             ;;; 12
    (LOAD s)               ;;; 13
    (HALT)))               ;;; 14

; Problem 5.4
; Define the ``number of steps'' function for *sum-nats-program*.
; Name the function sum-nats-prog-steps.  It will take one 
; argument, n.  (You will probably first define an auxilary
; function for computing the ``number of steps'' for the loop in
; *sum-nats-program*.)

(defun sum-nats-prog-steps (n)
  ***)

; Problem 5.5
; Our high level specification for *sum-nats-program* is that it
; computes (n*(n+1))/2 and leaves that value both in the local
; variable s and on top of the stack.  Prove that
; *sum-nats-program* is correct, as specified below.  You will 
; have to prove several lemmas here:

***

(defthm sum-nats-program-is-correct
  (implies (and (integerp n)
                (<= 0 n))
           (equal (run (modify nil
                               :pc      0
                               :program *sum-nats-program*
                               :locals  (list (cons 'n n)
					      (cons 's s))
                               :stack   stk)
		       (sum-nats-prog-steps n))
                  (modify nil
                          :pc      14
                          :program *sum-nats-program*
                          :locals  (list (cons 'n 0)
					 (cons 's (/ (* n (+ n 1))
						     2)))
                          :stack   (push (/ (* n (+ n 1)) 2)
					 stk)))))