#| 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 an Integer Square Root Program ; (note-lib "mc20-2" t) #| This is a revisit to our ISQRT proof. Dr. Don Good talked with Dr. Steve Zeigler, vice president for Ada products at Verdix, and they agreed to let me publicize the machine codes generated by their present Ada compiler. The following Ada function ISQRT computes the integer square root of a given nonnegative integer i. This is our third proof about ISQRT. function isqrt (i:integer) return integer is j : integer := (i / 2); begin while ((i / j) < j) loop j := (j + (i / j)) / 2; end loop; return j; end isqrt; Here is the MC68020 assembly code of the above ISQRT program. The code is from Dr. Steve Zeigler and generated by their present Ada compiler. 1 function isqrt (i:integer) return integer is 00000: link.w a6, #-04 2 j : integer := (i / 2); 00004: move.l d2, d1 00006: bge.b 06 -> 0e 00008: addi.l #01, d1 0000e: asr.l #01, d1 3 begin 4 while not ((i / j) >= j) loop 00010: move.l d2, d0 00012: divsl.l d1, d0:d0 00016: trapv 00018: cmp.l d0, d1 0001a: ble.b 01c -> 038 5 j := (j + (i / j)) / 2; 0001c: add.l d1, d0 0001e: trapv 00020: move.l d0, d1 00022: bge.b 06 -> 02a 00024: addi.l #01, d1 0002a: asr.l #01, d1 4 while not ((i / j) >= j) loop 0002c: move.l d2, d0 0002e: divsl.l d1, d0:d0 00032: trapv 6 end loop; 00034: cmp.l d0, d1 00036: bgt.b -01c -> 01c 7 return j; 00038: move.l d1, d0 0003a: unlk a6 0003c: rts 8 end isqrt; 0x4e56 0xfffc 0x2202 0x6c06 0x0681 0x0000 0x0001 0xe281 0x2002 0x4c41 0x0800 0x4e76 0xb280 0x6f1c 0xd081 0x4e76 0x2200 0x6c06 0x0681 0x0000 0x0001 0xe281 0x2002 0x4c41 0x0800 0x4e76 0xb280 0x6ee4 0x2001 0x4e5e 0x4e75 '(78 86 255 252 34 2 108 6 6 129 0 0 0 1 226 129 32 2 76 65 8 0 78 118 178 128 111 28 208 129 78 118 34 0 108 6 6 129 0 0 0 1 226 129 32 2 76 65 8 0 78 118 178 128 110 228 32 1 78 94 78 117) |# ; in the logic, the above program is defined by (isqrt-code). (defn isqrt-code () '(78 86 255 252 34 2 108 6 6 129 0 0 0 1 226 129 32 2 76 65 8 0 78 118 178 128 111 28 208 129 78 118 34 0 108 6 6 129 0 0 0 1 226 129 32 2 76 65 8 0 78 118 178 128 110 228 32 1 78 94 78 117)) (defn sq (x) (times x x)) ; isqrt1 is a function in the Logic simulating the loop of the above code. (defn isqrt1 (i j) (if (zerop j) (fix i) (if (lessp (quotient i j) j) (isqrt1 i (quotient (plus j (quotient i j)) 2)) (fix j)))) ; isqrt specifies the semantics of ISQRT in the Logic. To see why ; the function isqrt computes the square root for any nonnegative ; integer input, please refer to the proof in file isqrt.events. (defn isqrt (i) (let ((j1 (quotient (plus (quotient i 2) (quotient i (quotient i 2))) 2))) (if (lessp i (sq (quotient i 2))) (isqrt1 i j1) (quotient i 2)))) ; the computation time of this program. (defn isqrt1-t (i j) (if (zerop j) 0 (if (lessp (quotient i j) j) (splus 10 (isqrt1-t i (quotient (plus j (quotient i j)) 2))) 8))) (defn isqrt-t (i) (let ((j1 (quotient (plus (quotient i 2) (quotient i (quotient i 2))) 2))) (if (lessp i (sq (quotient i 2))) (splus 14 (isqrt1-t i j1)) 12))) ; enable a few functions. (enable iplus) (enable integerp) (enable iquotient) (enable ilessp) ; disable a few functions. (disable remainder) (disable quotient) (prove-lemma isqrt-no-overflow (rewrite) (implies (and (int-rangep (times 2 j) n) (lessp (quotient i j) j)) (int-rangep (plus j (quotient i j)) n))) (prove-lemma j-nonzerop (rewrite) (implies (and (lessp 1 i) (lessp 0 j)) (not (equal (quotient (plus j (quotient i j)) 2) 0)))) (prove-lemma j-int-rangep (rewrite) (implies (and (int-rangep (times 2 j) n) (lessp (quotient i j) j)) (int-rangep (times 2 (quotient (plus j (quotient i j)) 2)) n))) ; an induction hint. (defn isqrt-induct (s i j) (if (zerop j) t (if (lessp (quotient i j) j) (isqrt-induct (stepn s 10) i (quotient (plus j (quotient i j)) 2)) t))) ; the properties of the initial state. (defn isqrt-statep (s i) (and (equal (mc-status s) 'running) (evenp (mc-pc s)) (rom-addrp (mc-pc s) (mc-mem s) 70) (mcode-addrp (mc-pc s) (mc-mem s) (isqrt-code)) (ram-addrp (sub 32 8 (read-sp s)) (mc-mem s) 12) (equal i (iread-dn 32 2 s)) (ilessp 1 i))) ; an intermediate state s0. (defn isqrt-s0p (s i j) (and (equal (mc-status s) 'running) (evenp (mc-pc s)) (rom-addrp (sub 32 44 (mc-pc s)) (mc-mem s) 70) (mcode-addrp (sub 32 44 (mc-pc s)) (mc-mem s) (isqrt-code)) (ram-addrp (sub 32 4 (read-an 32 6 s)) (mc-mem s) 12) (equal i (iread-dn 32 2 s)) (equal j (iread-dn 32 1 s)) (int-rangep (times 2 j) 32) (ilessp 1 i) (ilessp 0 j))) (prove-lemma initial-j-int-rangep (rewrite) (implies (int-rangep i n) (int-rangep (times 2 (quotient i 2)) n)) ((enable int-rangep))) ; from the initial state to exit. (prove-lemma isqrt-s-exit (rewrite) (implies (and (isqrt-statep s i) (not (lessp i (times (quotient i 2) (quotient i 2))))) (and (equal (mc-status (stepn s 12)) 'running) (equal (mc-pc (stepn s 12)) (rts-addr s)) (equal (iread-dn 32 0 (stepn s 12)) (quotient i 2)) (equal (read-rn 32 14 (mc-rfile (stepn s 12))) (read-rn 32 14 (mc-rfile s))) (equal (read-rn 32 15 (mc-rfile (stepn s 12))) (add 32 (read-sp s) 4))))) (prove-lemma isqrt-s-exit-rfile (rewrite) (implies (and (isqrt-statep s i) (not (lessp i (times (quotient i 2) (quotient i 2)))) (d2-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 12))) (read-rn oplen rn (mc-rfile s))))) (prove-lemma isqrt-s-exit-mem (rewrite) (implies (and (isqrt-statep s i) (not (lessp i (times (quotient i 2) (quotient i 2)))) (disjoint x k (sub 32 8 (read-sp s)) 12)) (equal (read-mem x (mc-mem (stepn s 12)) k) (read-mem x (mc-mem s) k)))) ; from the initial state to s0. (prove-lemma isqrt-s-s0 (rewrite) (let ((j1 (quotient (plus (quotient i 2) (quotient i (quotient i 2))) 2))) (implies (and (isqrt-statep s i) (lessp i (times (quotient i 2) (quotient i 2)))) (and (isqrt-s0p (stepn s 14) i j1) (equal (linked-rts-addr (stepn s 14)) (rts-addr s)) (equal (linked-a6 (stepn s 14)) (read-an 32 6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 14))) (sub 32 4 (read-sp s)))))) ((disable quotient-equal-0))) (prove-lemma isqrt-s-s0-rfile (rewrite) (implies (and (isqrt-statep s i) (lessp i (times (quotient i 2) (quotient i 2))) (d2-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 14))) (read-rn oplen rn (mc-rfile s)))) ((disable quotient-equal-0))) (prove-lemma isqrt-s-s0-mem (rewrite) (implies (and (isqrt-statep s i) (lessp i (times (quotient i 2) (quotient i 2))) (disjoint x k (sub 32 8 (read-sp s)) 12)) (equal (read-mem x (mc-mem (stepn s 14)) k) (read-mem x (mc-mem s) k))) ((disable quotient-equal-0))) ; from s0 to exit (base case), or from s0 to s0 (induction case). ; base case: s0 --> exit. (prove-lemma isqrt-s0-exit-base (rewrite) (implies (and (isqrt-s0p s i j) (not (lessp (quotient i j) j))) (and (equal (mc-status (stepn s 8)) 'running) (equal (mc-pc (stepn s 8)) (linked-rts-addr s)) (equal (iread-dn 32 0 (stepn s 8)) j) (equal (read-rn 32 14 (mc-rfile (stepn s 8))) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile (stepn s 8))) (add 32 (read-an 32 6 s) 8))))) (prove-lemma isqrt1-s0-exit-rfile-base (rewrite) (implies (and (isqrt-s0p s i j) (not (lessp (quotient i j) j)) (d2-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 8))) (read-rn oplen rn (mc-rfile s))))) (prove-lemma isqrt1-s0-exit-mem-base (rewrite) (implies (and (isqrt-s0p s i j) (not (lessp (quotient i j) j))) (equal (read-mem x (mc-mem (stepn s 8)) k) (read-mem x (mc-mem s) k)))) ; induction case: s0 --> s0. (prove-lemma isqrt-s0-s0 (rewrite) (implies (and (isqrt-s0p s i j) (lessp (quotient i j) j)) (and (isqrt-s0p (stepn s 10) i (quotient (plus j (quotient i j)) 2)) (equal (read-rn oplen 14 (mc-rfile (stepn s 10))) (read-rn oplen 14 (mc-rfile s))) (equal (linked-a6 (stepn s 10)) (linked-a6 s)) (equal (linked-rts-addr (stepn s 10)) (linked-rts-addr s)))) ((disable quotient-equal-0 quotient-times-lessp))) (prove-lemma isqrt-s0-s0-rfile (rewrite) (implies (and (isqrt-s0p s i j) (lessp (quotient i j) j) (d2-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 10))) (read-rn oplen rn (mc-rfile s))))) (prove-lemma isqrt-s0-s0-mem (rewrite) (implies (and (isqrt-s0p s i j) (lessp (quotient i j) j) (disjoint x k (sub 32 8 (read-an 32 6 s)) 20)) (equal (read-mem x (mc-mem (stepn s 10)) k) (read-mem x (mc-mem s) k)))) (prove-lemma isqrt-s0p-j_nonzerop (rewrite) (implies (isqrt-s0p s i j) (and (not (equal j 0)) (numberp j)))) (disable isqrt-statep) (disable isqrt-s0p) ; put together: s0 --> exit. (prove-lemma isqrt-s0-exit (rewrite) (let ((sn (stepn s (isqrt1-t i j)))) (implies (isqrt-s0p s i j) (and (equal (mc-status sn) 'running) (equal (mc-pc sn) (linked-rts-addr s)) (equal (iread-dn 32 0 sn) (isqrt1 i j)) (equal (read-rn 32 14 (mc-rfile sn)) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile sn)) (add 32 (read-an 32 6 s) 8))))) ((induct (isqrt-induct s i j)) (disable quotient-times-lessp linked-rts-addr linked-a6 iread-dn))) (prove-lemma isqrt-s0-exit-rfile (rewrite) (implies (and (isqrt-s0p s i j) (d2-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s (isqrt1-t i j)))) (read-rn oplen rn (mc-rfile s)))) ((induct (isqrt-induct s i j)))) (prove-lemma isqrt-s0-exit-mem (rewrite) (implies (and (isqrt-s0p s i j) (disjoint x k (sub 32 8 (read-an 32 6 s)) 20)) (equal (read-mem x (mc-mem (stepn s (isqrt1-t i j))) k) (read-mem x (mc-mem s) k))) ((induct (isqrt-induct s i j)))) (disable isqrt-s0p-j_nonzerop) ; ISQRT program is correct. ; after an execution of this program, the machine state satisfies: ; 0. normal exit. ; 1. the pc is returned to the next instruction of the caller. ; 2. the result -- ISQRT(i), is stored in D0. ; 3. a6, used by LINK, is restored to its original content. ; 4. the stack pointer sp(a7) is updated correctly to pop off one frame. ; the registers not touched by this program still have their original values. ; the memory is correctly changed -- the local effect on memory. (prove-lemma isqrt-correctness (rewrite) (let ((sn (stepn s (isqrt-t i)))) (implies (isqrt-statep s i) (and (equal (mc-status sn) 'running) (equal (mc-pc sn) (rts-addr s)) (equal (read-rn 32 14 (mc-rfile sn)) (read-an 32 6 s)) (equal (read-rn 32 15 (mc-rfile sn)) (add 32 (read-an 32 7 s) 4)) (implies (d2-7a2-5p rn) (equal (read-rn oplen rn (mc-rfile sn)) (read-rn oplen rn (mc-rfile s)))) (implies (disjoint x k (sub 32 12 (read-sp s)) 20) (equal (read-mem x (mc-mem sn) k) (read-mem x (mc-mem s) k))) (equal (iread-dn 32 0 sn) (isqrt i))))) ((disable rts-addr linked-rts-addr linked-a6 iread-dn quotient-times-lessp))) (disable isqrt-t) ; start to prove isqrt correct. (prove-lemma isqrt1-lower-bound (rewrite) (implies (not (zerop j)) (not (lessp i (sq (isqrt1 i j)))))) (prove-lemma quotient-by-2 (rewrite) (not (lessp (plus (quotient x 2) (quotient x 2)) (sub1 x)))) (prove-lemma main-trick (rewrite) (not (lessp (sq (add1 (quotient (plus j k) 2))) (plus (times j k) j))) ((induct (difference j k)))) (prove-lemma sq-add1-non-zero (rewrite) (not (equal (sq (add1 x)) 0))) (prove-lemma main (rewrite) (implies (not (zerop j)) (lessp i (sq (add1 (quotient (plus j (quotient i j)) 2))))) ((disable sq))) (prove-lemma isqrt1-upper-bound (rewrite) (implies (lessp i (sq (add1 j))) (lessp i (sq (add1 (isqrt1 i j))))) ((disable sq))) (prove-lemma isqrt->isqrt1 (rewrite) (implies (lessp 1 i) (lessp i (sq (add1 (quotient i 2)))))) ; (isqrt i) is the square root of i: (isqrt i)^2 <= i < [(isqrt i)+1]^2. (prove-lemma isqrt-logic-correctness () (implies (lessp 1 i) (and (lessp i (sq (add1 (isqrt i)))) (not (lessp i (sq (isqrt i)))))) ((disable sq isqrt1))) ; a simple time analysis. (prove-lemma quotient-mono-1 (rewrite) (implies (and (leq y z) (not (zerop y)) (not (zerop z))) (not (lessp (quotient x y) (quotient x z))))) (prove-lemma mean-lessp-1 (rewrite) (implies (not (lessp x y)) (not (lessp x (quotient (plus x y) 2)))) ((induct (difference x y)))) (prove-lemma isqrt1-t-la-0 () (let ((j1 (quotient (plus j (quotient i j)) 2))) (implies (and (leq (quotient i j) j) (lessp 1 i) (lessp 0 j)) (not (lessp (difference x (quotient i j)) (difference x (quotient i j1)))))) ((use (quotient-mono-1 (x i) (y (quotient (plus j (quotient i j)) 2)) (z j))) (disable quotient-times-lessp))) (prove-lemma mean-difference-1-1 (rewrite) (implies (leq i j) (equal (difference (quotient (plus j i) 2) i) (quotient (difference j i) 2)))) (prove-lemma isqrt1-t-la-1 (rewrite) (let ((j1 (quotient (plus j (quotient i j)) 2))) (implies (and (lessp (quotient i j) j) (lessp 1 i) (lessp 0 j)) (not (lessp (quotient (difference j (quotient i j)) 2) (difference j1 (quotient i j1)))))) ((use (isqrt1-t-la-0 (x (quotient (plus j (quotient i j)) 2)))) (disable quotient-times-lessp))) (prove-lemma isqrt1-t-la-2 (rewrite) (let ((j1 (quotient (plus j (quotient i j)) 2))) (implies (and (lessp (quotient i j) j) (lessp 1 i) (lessp 0 j)) (not (lessp (log 2 (quotient (difference j (quotient i j)) 2)) (log 2 (difference j1 (quotient i j1))))))) ((use (isqrt1-t-la-1)) (disable quotient-times-lessp log))) (prove-lemma isqrt-t1-ubound () (implies (and (lessp 1 i) (lessp 0 j)) (not (lessp (plus 18 (times 10 (log 2 (difference j (quotient i j))))) (isqrt1-t i j)))) ((enable splus) (disable quotient-times-lessp log) (expand (log 2 (difference j (quotient i j)))))) (prove-lemma isqrt-t->isqrt1-t () (implies (lessp 1 i) (not (lessp (plus 4 (isqrt1-t i (quotient i 2))) (isqrt-t i)))) ((enable splus isqrt-t))) (prove-lemma log-mono (rewrite) (not (lessp (log b y) (log b (difference y x)))) ((use (log-leq (x (difference y x)))))) (prove-lemma isqrt-t-ubound-la (rewrite) (implies (lessp 1 i) (not (lessp (plus 12 (times 10 (log 2 i))) (isqrt-t i)))) ((use (isqrt-t->isqrt1-t) (isqrt-t1-ubound (j (quotient i 2)))))) (prove-lemma isqrt-t-ubound () (implies (and (lessp i (exp 2 31)) (lessp 1 i)) (leq (isqrt-t i) 322)) ((use (ta-lemma-1 (a i) (a1 (exp 2 31)) (x 12) (y 10)))))