; JVM Problem Set 6
; Copyright (C) 2004  J Strother Moore and John R. Cowles,
;               University of Texas at Austin and
                University of Wyoming

; 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: John R. Cowles
; email:      cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.

; Based on earlier work and ideas of
;            J Strother Moore
; email:     Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.
;=============================================================
; In this problem set you will be expected to fill in the blanks
; to prove the partial 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.
;==============================================================
;; Partial Correctness of M0 Programs

;;                 Part 1.

;; Use Hoare Semantics for m0 programs to show the following is
;; parially correct.

;; {STK = empty}
;;                  ;; pc
;;  (PUSH 10)       ;;  0
;;  (PUSH 5)        ;;  1
;;  (ADD)           ;;  2
;;  (HALT)          ;;  3
;; {STK.top = 15 and STK.bot = empty} 

;; ------------------------------------------
;; Hand generated proof using Hoare Sematics:

;; {STK = empty}
;; {10 + 5 = 15 and STK = empty}
;;  (PUSH 10)                                   ;; 0
;; {STK.top + 5 = 15 and STK.bot = empty}
;;  (PUSH 5)                                    ;; 1
;; {STK.bot.top + STK.top = 15 and STK.bot.bot = empty}
;;  (ADD)                                       ;; 2
;; {STK.top = 15 and STK.bot = empty} 
;;  (HALT)                                      ;; 3
;; {STK.top = 15 and STK.bot = empty} 

;; VERIFY: STK = empty ==> (10 + 5 = 15 and STK = empty)

;; -----------------------------------------------
;; Using ACL2 to help verify the Hoare Sematntics.

;; Use hand proof above to supply an explicit assertion for each
;; value of the pc.

(include-book "m0-utilities")

(in-package "M0")

(defconst *eg1-program*
                    ;; pc
  '((PUSH 10)       ;;  0
    (PUSH 5)        ;;  1
    (ADD)           ;;  2
    (HALT)))        ;;  3

; Here are the explicit assertions, translated directly from the
; hand generated proof.

(defun eg1-prog-assertion-1 (s)
  (let* ((STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK))
	 (STK.bot.top (top STK.bot))
	 (STK.bot.bot (pop STK.bot)))
    (and (equal (program s) *eg1-program*)
	 (case (pc s)
	       (0 ;; {STK = empty}
       		     (equal STK nil))

	       (1 ;; {STK.top + 5 = 15 and STK.bot = empty}
		     (and (equal (+ STK.top 5) 15)
			  (equal STK.bot nil)))

	       (2 ;; {STK.bot.top + STK.top = 15
                  ;;  and STK.bot.bot = empty}
		     (and (equal (+ STK.bot.top STK.top) 15)
			  (equal STK.bot.bot nil)))

	       (3 ;; {STK.top = 15 and STK.bot = empty} 
		     (and (equal STK.top 15)
			  (equal STK.bot nil)))

	       (otherwise nil)))))

; Here is the key theorem of the Hoare Semantics approach, showing
; that eg1-prog-assertion-1 remains true as m0 steps through the
; program.

(defthm eg1-prog-assertion-1-step
  (implies (eg1-prog-assertion-1 s)
	   (eg1-prog-assertion-1 (step s))))

; We immediately conclude that eg1-prog-assertion-1 remains true 
; as m0 runs for an arbitrary number of steps.

(defthm eg1-prog-assertion-1-run
  (implies (eg1-prog-assertion-1 s)
	   (eg1-prog-assertion-1 (run s n)))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory (e/d (run)(eg1-prog-assertion-1)))))

; If we plug in an initial state satisfying eg1-prog-assertion-1
; then we get a final state satisfying it.  If the final state is
; supposed to have pc 3, then we can read out what
; eg1-prog-assertion-1 tells us about that state.

(defthm eg1-prog-is-partially-correct-1
  (let* ((s (run (modify nil
			 :pc 0
			 :program *eg1-program*
                         :locals local-vars
                         :stack nil)
		 n))
	 (STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK)))
    (implies (equal (pc s) 3)
             (and (equal STK.top 15)
		  (equal STK.bot nil))))
  :rule-classes nil
  :hints (("Goal" 
	   :use (:instance 
		 eg1-prog-assertion-1-run
		 (s (modify nil
			    :pc 0
			    :program *eg1-program*
			    :locals local-vars
			    :stack nil))))))
;;===========================================================
;;                 Part 2.

;; In Part 1, the hand generated proof, using the Hoare 
;; Semantics, was used to supply an explicit assertion 
;; for each value of the pc. Then ACL2 helped complete the 
;; partial correctness proof.

;; Here we show how to supply only the precondition and 
;; postcondition and still have ACL2 help complete the 
;; partial correctness proof. 
;; --------------------------------------

;; Show the following is parially correct.

;; {STK = empty}- - - - - - - - - - - - precondition
;;                  ;; pc
;;  (PUSH 10)       ;;  0
;;  (PUSH 5)        ;;  1
;;  (ADD)           ;;  2
;;  (HALT)          ;;  3
;; {STK.top = 15 and STK.bot = empty} - postcondition

;; -------------------------------------------------------------
; This is the Defpun book by Manolios and Moore.  It may be found
; on the class website.

; You should copy the Defpun book to your file system and 
; recertify it.
; Then change the absolute path name below to point to your copy
; of defpun.lisp.

(include-book "defpun")

; Defpun is not part of the m0-utilities, so it is added by macro.

(defmacro defpun (g args &rest tail)
  `(acl2::defpun ,g ,args ,@tail))

;; We'll need this lemma later

(defthm binding-bind
  (equal (binding x (bind var val alist))
	 (if (equal x var)
	     val
	     (binding x alist))))
;----------------------------------------------

; Here are the explicit pre- and post-conditions translated 
; directly from above.

(defun eg1-prog-pre-post (s)
  (let* ((STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK)))
    (and (equal (program s) *eg1-program*)
	 (case (pc s)
	       (0 ;; {STK = empty}
       		     (equal STK nil))

	       (3 ;; {STK.top = 15 and STK.bot = empty} 
		     (and (equal STK.top 15)
			  (equal STK.bot nil)))

	       (otherwise nil)))))

; The assertion for the entire program is defined using tail
; recursion.  The pre- and post-conditions are attached at the
; proper values of the pc and tail recursion by step is used to
; propagate assertions from these conditions to all the pcs.

; Defpun is used to introduce the tail recursion without the
; need to explicitly keep track of the number of steps.

(defpun eg1-prog-assertion (s)
  (if (or (equal (pc s) 0)
	  (equal (pc s) 3))
      (eg1-prog-pre-post s)
      (eg1-prog-assertion (step s))))

; The next lemma is a technical lemma to force eg1-prog-assertion
; to keep opening if it hasn't reached a pre- or post-condition
; yet.

(defthm eg1-prog-assert-make-state-opener
  (implies (and (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 3)))
           (equal (eg1-prog-assertion
		   (make-state pc locs stk prog))
                  (eg1-prog-assertion
		   (step (make-state pc locs stk prog))))))

; Once more, here is the key theorem of the Hoare Semantics 
; approach, showing that eg1-prog-assertion remains true as m0 
; steps through the program.

(defthm eg1-prog-assertion-step
  (implies (eg1-prog-assertion s)
	   (eg1-prog-assertion (step s))))

; As before, we immediately conclude that eg1-prog-assertion 
; remains true as m0 runs for an arbitrary number of steps.

(defthm eg1-prog-assertion-run
  (implies (eg1-prog-assertion s)
	   (eg1-prog-assertion (run s n)))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory (e/d (run)(eg1-prog-assertion-def)))))

; As before, if we plug in an initial state satisfying 
; eg1-prog-assertion then we get a final state satisfying it.  If
; the final state is supposed to have pc 3, then we can read out
; what eg1-prog-assertion tells us about that state.

(defthm eg1-prog-is-partially-correct
  (let* ((s (run (modify nil
			 :pc 0
			 :program *eg1-program*
                         :locals local-vars
                         :stack nil)
		 n))
	 (STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK)))
    (implies (equal (pc s) 3)
             (and (equal STK.top 15)
		  (equal STK.bot nil))))
  :rule-classes nil
  :hints (("Goal" 
	   :use (:instance 
		 eg1-prog-assertion-run
		 (s (modify nil
			    :pc 0
			    :program *eg1-program*
			    :locals local-vars
			    :stack nil))))))
;;===========================================================
;;                 Part 3.

;; In the examples above, there are no loops.  The classic 
;; application of Hoare Semantics to partial program correctness 
;; supplies an assertion at selected locations, one for each loop,
;; plus the pre- and post-conditions.  
;; -------------------------------------------------------------
;; Here is an m0 program with a loop.

;; 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.

;; Show the following is parially correct.
;; Here we assume that all variables have integer type, i is the 
;; initial value of the variable n, and s0 is the initial stack.

;;  {n = i and n >= 0 and STK = s0} - precondition
;;                  ;; 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
;;  {STK.top = b^i and STK.bot = s0} - postcondition

;; Dealing with a loop requires a LOOP INVARIANT. That is,
;; construct and place an assertion, somewhere in the body of the
;; loop, that is true every time execution gets to the assertion. 

;; Here is my choice for the loop invariant and its placement.

(defconst *exp-program*
;{n = i and n >= 0 and STK = s0} - precondition
                 ;; 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
   ;---------
;{STK.top * b^n = b^i and n >= 0 and STK.bot = s0} - invariant
    (LOAD n)     ;;  8  -------------- top of loop
    (IFGT -7)    ;;  9  end while
   ;---------
    (HALT))     ;; 10
;{STK.top = b^i and STK.bot = s0} - postcondition
  )

;; Use the following functions to tell ACL2 about the loop
;; invariant and the pre- and post-conditions.

; Even to do partial correctness you have to have some 
; understanding of what's going on in the loops.

; 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))

; Here are the explicit loop invariant and pre- and 
; post-conditions translated directly from above.
; Notice that the initial values of n and the stack are
; input arguments to the function.

(defun exp-prog-pre-post-inv (s i s0)
  (let* ((STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK))
	 (n (binding 'n (locals s)))
	 (b (binding 'b (locals s))))
    (and (integerp n) ;; Here we enforce that n has integer type.
	 (equal (program s) *exp-program*)
	 (case (pc s)
	       (0 ;; {n = i and n >= 0 and STK = s0}
		     (and (equal n i)
			  (>= n 0)
			  (equal STK s0)))

	       (8 ;; {STK.top * b^n = b^i and n >= 0
                  ;;  and STK.bot = s0}
		     (and (equal (iexp-loop b n STK.top)
				 (iexp b i))
			  (>= n 0)
			  (equal STK.bot s0)))

	       (10 ;;{STK.top = b^i and STK.bot = s0}
		     (and (equal STK.top (iexp b i))
			  (equal STK.bot s0)))

	       (otherwise nil)))))

; The assertion for the entire program is defined using tail
; recursion.  The loop invarant and the pre- and post-conditions 
; are attached at the proper values of the pc and tail recursion
; by step is used to propagate assertions from these conditions 
; to all the pcs.

; Defpun is used to introduce the tail recursion without the
; need to explicitly keep track of the number of steps.

(defpun exp-prog-assertion (s i s0)
  (if (or (equal (pc s) 0)
          (equal (pc s) 8)
          (equal (pc s) 10))
      (exp-prog-pre-post-inv s i s0)
      (exp-prog-assertion (step s) i s0)))

; The next lemma is a technical lemma to force exp-prog-assertion
; to keep opening if it hasn't reached the loop invariant or a 
; pre-  or post-condition yet.

; This lemma also highlights a nice feature of this approach.  
; Suppose that in our function exp-prog-pre-post-inv we had failed
; to supply an invariant for some loop.  Then we'll get a stack 
; overflow from the repeated indefinite application of this
; rewrite rule. This mimics the classical Hoare Semantics
; approach: You cannot complete the proof that the program is
; partially correct without supplying a loop invariant for every
; loop.

(defthm exp-prog-assert-make-state-opener
  (implies (and (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 8))
                (not (equal pc 10)))
           (equal (exp-prog-assertion 
		   (make-state pc locs stk prog) i s0)
                  (exp-prog-assertion
		   (step (make-state pc locs stk prog)) i s0))))

; Here is the key theorem of the Hoare Semantics approach, showing
; that exp-prog-assertion remains true as m0 steps through the
; program.

(defthm exp-prog-assertion-step
  (implies (exp-prog-assertion s i s0)
	   (exp-prog-assertion (step s) i s0)))

; We immediately conclude that exp-prog-assertion remains true 
; as m0 runs for an arbitrary number of steps.

(defthm exp-prog-assertion-run
  (implies (exp-prog-assertion s i s0)
	   (exp-prog-assertion (run s k) i s0))
  :rule-classes nil
  :hints (("Goal"
	   :in-theory (e/d (run)(exp-prog-assertion-def)))))

; If we plug in an initial state satisfying exp-prog-assertion
; then we get a final state satisfying it.  If the final state is
; supposed to have pc 10, then we can read out what
; exp-prog-assertion tells us about that state.

(defthm exp-prog-is-partially-correct-1
  (let* ((s (run (modify nil
			 :pc 0
			 :program *exp-program*
                         :locals (list* (cons 'n i)
					local-vars)
                         :stack s0)
		 k))
	 (STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK))
	 (b (binding 'b (locals s))))
    (implies (and (equal (pc s) 10)
		  (integerp i)
		  (>= i 0))
	     (and (equal STK.top (iexp b i))
		  (equal STK.bot s0))))
  :rule-classes nil
  :hints (("Goal"
	   :use (:instance 
		 exp-prog-assertion-run
		 (s (modify nil
			    :pc 0
			    :program *exp-program*
			    :locals (list* (cons 'n i)
					   local-vars)
			    :stack s0))))))

;;---------------------------------------------------------
; Problem 6.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 partial correctness theorem about the exp
; program.  Hint: 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-prog-is-partially-correct
  (let* ((s (run (modify nil
			 :pc 0
			 :program *exp-program*
                         :locals (list* (cons 'n i)
					local-vars)
                         :stack s0)
		 k))
	 (STK (stack s))
	 (STK.top (top STK))
	 (STK.bot (pop STK))
	 (b (binding 'b (locals s))))
    (implies (and (equal (pc s) 10)
		  (integerp i)
		  (>= i 0))
	     (and (equal STK.top (rexp b i))
		  (equal STK.bot s0))))
  :rule-classes nil
  :hints (("Goal"
	   :use exp-prog-is-partially-correct-1)))
;;====================================================
;; Use ACL2 to show the following is partially correct.

;; {x = a and y = b and STK = s0} - precondition
;;                  ;; pc
;;  (LOAD x)        ;;  0
;;  (LOAD y)        ;;  1
;;  (STORE x)       ;;  2
;;  (STORE y)       ;;  3
;;  (HALT)          ;;  4
;; {x = b and y = a and STK = s0} - postcondition
;; -----------------------------------------------

(defconst *swap-program*
;;{x = a and y = b and STK = s0} - precondition
                    ;; pc
  '((LOAD x)        ;;  0
    (LOAD y)        ;;  1
    (STORE x)       ;;  2
    (STORE y)       ;;  3
    (HALT))         ;;  4
;; {x = b and y = a and STK = s0} - postcondition
  )

;----------------------------------------------------------
; Problem 6.2
; Here are the explicit pre- and post-conditions translated 
; directly from above.

(defun swap-prog-pre-post (s s0 a b)
  (let ((STK (stack s))
	(x (binding 'x (locals s)))
	(y (binding 'y (locals s))))
    (and (equal (program s) *swap-program*)
	 (case (pc s)
	       (0 ;; {x = a and y = b and STK = s0}
		     ***
	       (4 ;; {x = b and y = a and STK = s0} 
		     ***
	       (otherwise nil)))))
;--------------------------------------------------------------
; Problem 6.3
; The assertion for the entire program is defined using tail
; recursion.  The pre- and post-conditions are attached at the
; proper values of the pc and tail recursion by step is used to
; propagate assertions from these conditions to all the pcs.

; Defpun is used to introduce the tail recursion without the
; need to explicitly keep track of the number of steps.

(defpun swap-prog-assertion (s s0 a b)
  ***)
;-----------------------------------------------------------------
; The next lemma is a technical lemma to force swap-prog-assertion
; to keep opening if it hasn't reached a pre- or post-condition
; yet.

(defthm swap-prog-assert-make-state-opener
  (implies (and (syntaxp (quotep pc))
                (not (equal pc 0))
                (not (equal pc 4)))
           (equal (swap-prog-assertion
		   (make-state pc locs stk prog) s0 a b)
                  (swap-prog-assertion
		   (step (make-state pc locs stk prog)) s0 a b))))

;-----------------------------------------------------------------
; Problem 6.4
; The next theorem is the key theorem of the Hoare Semantics approach,
; showing that swap-prog-assertion remains true as m0 steps through
; the program.  We can then immediately conclude that 
; swap-prog-assertion remains true as m0 runs for an arbitrary number
; of steps.

(defthm swap-prog-assertion-step
  ***)

(defthm swap-prog-assertion-run
  ***)
  :rule-classes nil
  :hints (("Goal"
	   :in-theory (e/d (run)(swap-prog-assertion-def)))))

;---------------------------------------------------------------
; If we plug in an initial state satisfying swap-prog-assertion
; then we get a final state satisfying it.  If the final state is
; supposed to have pc 4, then we can read out what
; swap-prog-assertion tells us about that state.

(defthm swap-prog-is-partially-correct
  (let* ((s (run (modify nil
			 :pc 0
			 :program *swap-program*
                         :locals (list* (cons 'x a)
					(cons 'y b)
					local-vars)
                         :stack s0)
		 n))
	 (STK (stack s))
	 (x (binding 'x (locals s)))
	 (y (binding 'y (locals s))))
    (implies (equal (pc s) 4)
	     (and (equal x b)
		  (equal y a)
		  (equal STK s0))))
  :rule-classes nil
  :hints (("Goal"
	   :use (:instance 
		 swap-prog-assertion-run
		 (s (modify nil
			    :pc 0
			    :program *swap-program*
			    :locals (list* (cons 'x a)
					   (cons 'y b)
					   local-vars)
			    :stack s0))))))
;;====================================================
;; Problem 6.5
;; Use ACL2 to show the following is partially correct.

;; {STK = s0} - - - - - - - - - - - - - - - precondition
;;                  ;; pc
;;  (LOAD x)        ;;  0
;;  (LOAD y)        ;;  1
;;  (SUB)           ;;  2
;;  (IFLE 3)        ;;  3
;;  (LOAD x)        ;;  4
;;  (GOTO 2)        ;;  5
;;  (LOAD y)        ;;  6
;;  (HALT)          ;;  7
;; {STK.top = (max x y) and STK.bot = s0} - postcondition
;; -----------------------------------------------

;; A defconst, a defun, a defpun, and several defthms
;; will be required.

***
;;---------------------------------------------------------------
;; Below 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.

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

;; Problem 6.6
;; Use ACL2 to show the following is partially correct.
;; Here we assume that all variables have integer type, i is the 
;; initial value of the variable n, and s0 is the initial stack.

(defconst *fact-program*
;;{n = i and n >= 0 and STK = s0} - precondition
                  ;; 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
;;{STK.top = (! i) and STK.bot = s0} - postcondition
  )

;; A loop invariant, several defuns, a defpun, and several 
;; defthms will be required. Hint: Consider using, temporarily,
;; an iterative version factorial in place of the recursive !.

***