#|

 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
 WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
 LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.

|#

;          Proof of the correctness of the AMAX program
;
(note-lib "mc20-2" t)
#|

This program finds the maximum value of an integer array.  The way I 
wrote this program is to test the ability to handle the while statement.

/* find the maximum in an integer array  */
amax(a, n)
int a[], n;
{ 
  int max;

  max = a[--n];
  while (n > 0)
    if (a[--n] > max)
      max = a[n];
  return (max);
}

Here is the MC68020 assembly code of the above AMAX program.  The code is
generated by "gcc -O".

0x2342 <amax>:          linkw a6,#0
0x2346 <amax+4>:        moveal a6@(8),a0
0x234a <amax+8>:        movel a6@(12),d0
0x234e <amax+12>:       subl #1,d0
0x2350 <amax+14>:       bra 0x235a <amax+24>
0x2352 <amax+16>:       subl #1,d0
0x2354 <amax+18>:       cmpl 0(a0)[d0.l*4],d1
0x2358 <amax+22>:       bge 0x235e <amax+28>
0x235a <amax+24>:       movel 0(a0)[d0.l*4],d1
0x235e <amax+28>:       tstl d0
0x2360 <amax+30>:       bgt 0x2352 <amax+16>
0x2362 <amax+32>:       movel d1,d0
0x2364 <amax+34>:       unlk a6
0x2366 <amax+36>:       rts

The machine code of the above program is:

<amax>:       0x4e56  0x0000  0x206e  0x0008  0x202e  0x000c  0x5380  0x6008
<amax+16>:    0x5380  0xb2b0  0x0c00  0x6c04  0x2230  0x0c00  0x4a80  0x6ef0
<amax+32>:    0x2001  0x4e5e  0x4e75

'(78      86      0       0       32      110     0       8
  32      46      0       12      83      128     96      8
  83      128     178     176     12      0       108     4
  34      48      12      0       74      128     110     240
  32      1       78      94      78      117)
|#

; now we start to prove the correctness of this AMAX program, defined by
; (amax-code).
(defn amax-code ()
  '(78      86      0       0       32      110     0       8
    32      46      0       12      83      128     96      8
    83      128     178     176     12      0       108     4
    34      48      12      0       74      128     110     240
    32      1       78      94      78      117))

; the maximum value in a list.
(defn amax1 (imax n lst)
  (if (zerop n)
      imax
    (if (ilessp imax (get-nth (sub1 n) lst))
	(amax1 (get-nth (sub1 n) lst) (sub1 n) lst)
      (amax1 imax (sub1 n) lst))))

(defn amax (n lst)
  (amax1 (get-nth (sub1 n) lst) (sub1 n) lst))

; the clock of AMAX program.
(defn amax1-t (imax i lst)
  (if (zerop i)
      5
    (if (ilessp imax (get-nth (sub1 i) lst))
	(splus 6 (amax1-t (get-nth (sub1 i) lst) (sub1 i) lst))
      (splus 5 (amax1-t imax (sub1 i) lst)))))
      
(defn amax-t (n lst)
  (splus 6 (amax1-t (get-nth (sub1 n) lst) (sub1 n) lst)))

; the induction hint for the loop.
(defn amax-induct (imax n lst s)
  (if (zerop n)
      t
    (if (ilessp imax (get-nth (sub1 n) lst))
	(amax-induct (get-nth (sub1 n) lst) (sub1 n) lst (stepn s 6))
      (amax-induct imax (sub1 n) lst (stepn s 5)))))

; the preconditions of the initial state.
(defn amax-statep (s a n lst)
  (and (equal (mc-status s) 'running)
       (evenp (mc-pc s))
       (rom-addrp (mc-pc s) (mc-mem s) 38)
       (mcode-addrp (mc-pc s) (mc-mem s) (amax-code))
       (ram-addrp (sub 32 4 (read-sp s)) (mc-mem s) 16)
       (mem-ilst 4 a (mc-mem s) n lst)
       (ram-addrp a (mc-mem s) (times 4 n))
       (disjoint a (times 4 n) (sub 32 4 (read-sp s)) 16)
       (equal a (read-mem (add 32 (read-sp s) 4) (mc-mem s) 4))
       (equal n (iread-mem (add 32 (read-sp s) 8) (mc-mem s) 4))
       (lessp 0 n)))

; the conditions of the intermediate state.
(defn amax1-statep (s imax i n lst)
  (and (equal (mc-status s) 'running)
       (evenp (mc-pc s))
       (rom-addrp (sub 32 28 (mc-pc s)) (mc-mem s) 38)
       (mcode-addrp (sub 32 28 (mc-pc s)) (mc-mem s) (amax-code))
       (ram-addrp (read-an 32 6 s) (mc-mem s) 16)
       (mem-ilst 4 (read-an 32 0 s) (mc-mem s) n lst)
       (ram-addrp (read-an 32 0 s) (mc-mem s) (times 4 n))
       (disjoint (read-an 32 0 s) (times 4 n) (read-an 32 6 s) 16)
       (equal i (nat-to-int (read-dn 32 0 s) 32))
       (equal imax (nat-to-int (read-dn 32 1 s) 32))
       (lessp 0 n)
       (numberp i)
       (lessp i n)))

(enable iplus)
(disable ilessp)

; the initial segment of the program.
(prove-lemma amax->amax1-statep ()
     (implies (amax-statep s a n lst)
	      (amax1-statep (stepn s 6) 
			    (get-nth (sub1 n) lst) 
			    (sub1 n)
			    n
			    lst)))

(prove-lemma amax-initial (rewrite)
     (implies (amax-statep s a n lst)
	      (and (equal (linked-rts-addr (stepn s 6)) (rts-addr s))
		   (equal (linked-a6 (stepn s 6)) (read-an 32 6 s))
		   (equal (read-rn 32 14 (mc-rfile (stepn s 6)))
			  (sub 32 4 (read-sp s))))))

(prove-lemma amax-initial-rfile (rewrite)
     (implies (and (amax-statep s a n lst)
		   (d2-7a2-5p rn))
	      (equal (read-rn oplen rn (mc-rfile (stepn s 6)))
		     (read-rn oplen rn (mc-rfile s)))))
		      
(prove-lemma amax-initial-mem (rewrite)
     (implies (and (amax-statep s a n lst)
		   (disjoint x k (sub 32 4 (read-sp s)) 16))
	      (equal (read-mem x (mc-mem (stepn s 6)) k)
		     (read-mem x (mc-mem s) k))))

; base case.
(prove-lemma amax-base-case (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (zerop i))
	      (and (equal (mc-status (stepn s 5)) 'running)
		   (equal (mc-pc (stepn s 5)) (linked-rts-addr s))
		   (equal (iread-dn 32 0 (stepn s 5)) imax)
		   (equal (read-rn 32 14 (mc-rfile (stepn s 5)))
			  (linked-a6 s))
		   (equal (read-rn 32 15 (mc-rfile (stepn s 5)))
			  (add 32 (read-an 32 6 s) 8))
		   (equal (read-mem x (mc-mem (stepn s 5)) k)
			  (read-mem x (mc-mem s) k)))))

(prove-lemma amax-base-rfile (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (d2-7a2-5p rn)
		   (zerop i))
	      (equal (read-rn oplen rn (mc-rfile (stepn s 5)))
		     (read-rn oplen rn (mc-rfile s)))))

; induction case.
(prove-lemma amax-induct-case1 (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (not (equal i 0))
		   (ilessp imax (get-nth (sub1 i) lst)))
	      (and (amax1-statep (stepn s 6)
				 (get-nth (sub1 i) lst)
				 (sub1 i)
				 n
				 lst)
		   (equal (read-rn oplen 14 (mc-rfile (stepn s 6)))
			  (read-rn oplen 14 (mc-rfile s)))
		   (equal (linked-a6 (stepn s 6)) (linked-a6 s))
		   (equal (linked-rts-addr (stepn s 6)) (linked-rts-addr s))
		   (equal (read-mem x (mc-mem (stepn s 6)) k)
			  (read-mem x (mc-mem s) k)))))

(prove-lemma amax-induct-case2 (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (not (equal i 0))
		   (not (ilessp imax (get-nth (sub1 i) lst))))
	      (and (amax1-statep (stepn s 5) imax (sub1 i) n lst)
		   (equal (read-rn oplen 14 (mc-rfile (stepn s 5)))
			  (read-rn oplen 14 (mc-rfile s)))
		   (equal (linked-a6 (stepn s 5)) (linked-a6 s))
		   (equal (linked-rts-addr (stepn s 5)) (linked-rts-addr s))
		   (equal (read-mem x (mc-mem (stepn s 5)) k)
			  (read-mem x (mc-mem s) k)))))

(prove-lemma amax-induct-rfile1 (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (not (equal i 0))
		   (ilessp imax (get-nth (sub1 i) lst))
		   (d2-7a2-5p rn))
	      (equal (read-rn oplen rn (mc-rfile (stepn s 6)))
		     (read-rn oplen rn (mc-rfile s)))))

(prove-lemma amax-induct-rfile2 (rewrite)
     (implies (and (amax1-statep s imax i n lst)
		   (not (equal i 0))
		   (not (ilessp imax (get-nth (sub1 i) lst)))
		   (d2-7a2-5p rn))
	      (equal (read-rn oplen rn (mc-rfile (stepn s 5)))
		     (read-rn oplen rn (mc-rfile s)))))

(disable amax-statep)
(disable amax1-statep)

; the correctness of the loop.
(prove-lemma amax1-correctness (rewrite)
     (implies 
      (amax1-statep s imax i n lst)
      (and (equal (mc-status (stepn s (amax1-t imax i lst)))
		  'running)
	   (equal (mc-pc (stepn s (amax1-t imax i lst)))
		  (linked-rts-addr s))
	   (equal (iread-dn 32 0 (stepn s (amax1-t imax i lst)))
		  (amax1 imax i lst))
	   (equal (read-rn 32 14 (mc-rfile (stepn s (amax1-t imax i lst))))
		  (linked-a6 s))
	   (equal (read-rn 32 15 (mc-rfile (stepn s (amax1-t imax i lst))))
		  (add 32 (read-an 32 6 s) 8))
	   (equal (read-mem x (mc-mem (stepn s (amax1-t imax i lst))) k)
		  (read-mem x (mc-mem s) k))))
     ((induct (amax-induct imax i lst s))
      (disable linked-rts-addr linked-a6)))

(prove-lemma amax1-rfile-correctness (rewrite)
     (implies 
      (and (amax1-statep s imax i n lst)
	   (d2-7a2-5p rn))
      (equal (read-rn oplen rn (mc-rfile (stepn s (amax1-t imax i lst))))
	     (read-rn oplen rn (mc-rfile s))))
     ((induct (amax-induct imax i lst s))))

; the correctness of the AMAX program.
(prove-lemma amax-correctness (rewrite)
     (implies (amax-statep s a n lst)
	      (and (equal (mc-status (stepn s (amax-t n lst)))
			  'running)
		   (equal (mc-pc (stepn s (amax-t n lst)))
			  (rts-addr s))
		   (equal (iread-dn 32 0 (stepn s (amax-t n lst)))
			  (amax n lst))
		   (equal (read-rn 32 14 (mc-rfile (stepn s (amax-t n lst))))
			  (read-rn 32 14 (mc-rfile s)))
		   (equal (read-rn 32 15 (mc-rfile (stepn s (amax-t n lst))))
			  (add 32 (read-rn 32 15 (mc-rfile s)) 4))))
     ((use (amax->amax1-statep))
      (disable rts-addr linked-rts-addr linked-a6)))

(prove-lemma amax-rfile-correctness (rewrite)
     (implies (and (amax-statep s a n lst)
		   (d2-7a2-5p rn))
	      (equal (read-rn oplen rn (mc-rfile (stepn s (amax-t n lst))))
		     (read-rn oplen rn (mc-rfile s))))
     ((use (amax->amax1-statep))))
	      
(prove-lemma amax-mem-correctness (rewrite)
	     (implies (and (amax-statep s a n lst)
			   (disjoint x k (sub 32 4 (read-sp s)) 16))
		      (equal (read-mem x (mc-mem (stepn s (amax-t n lst))) k)
			     (read-mem x (mc-mem s) k)))
	     ((use (amax->amax1-statep))))

(disable amax-t)

; amax does find the maximum of an integer list.  We need to prove two 
; things:  
;      1. the output is no less than any element of the list.  
;      2. the output is in the list.
(prove-lemma ilessp-transitivity (rewrite)
     (implies (and (ilessp x y)
		   (ileq y z))
	      (ilessp x z))
     ((enable ilessp)))

(prove-lemma amax1-mono (rewrite)
     (implies (not (ilessp imax imax1))
	      (not (ilessp (amax1 imax n lst) imax1))))

(prove-lemma amax1-max (rewrite)
     (implies (lessp i n)
	      (not (ilessp (amax1 imax n lst) (get-nth i lst))))
     ((induct (amax1 imax n lst))
      (enable get-nth-0)))

(prove-lemma amax-max (rewrite)
     (implies (lessp i n)
	      (not (ilessp (amax n lst) (get-nth i lst))))
     ((use (amax1-max (imax (get-nth (sub1 n) lst)) (n (sub1 n))))
      (enable get-nth-0)))

(prove-lemma get-nth-memberp (rewrite)
     (implies (lessp n (len lst))
	      (member (get-nth n lst) lst))
     ((enable get-nth)))

(prove-lemma amax1-closed (rewrite)
     (implies (and (leq n (len lst))
		   (member imax lst))
	      (member (amax1 imax n lst) lst)))

(prove-lemma amax-closed (rewrite)
     (implies (and (leq n (len lst))
		   (not (zerop n)))
	      (member (amax n lst) lst))
     ((use (amax1-closed (imax (get-nth (sub1 n) lst)) (n (sub1 n))))))