#|
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 ISQRT Program
;

Event: Start with the library "mc20-2" using the compiled version.

#|
The following C function ISQRT computes the integer square root of a given
nonnegative integer i.
/* computes the integer square root of a given nonnegative integer */
isqrt(int i)
{
 int j;
 j = (i / 2);
 while ((i / j) < j)
   j = (j + (i / j)) / 2;
 return (j);
}

Here is the MC68020 assembly code of the above ISQRT program.  The code is
generated by "gcc -O".
The program expects an nonnegative integer input which is on the sp
stack at address (sp)+4.  The local variable j is assigned to d2.  The
program exits with the answer in register d0 and the program counter
equals the return address saved on the sp stack at address (sp).
0x2318 <isqrt>:  linkw a6,#0
0x231c <isqrt+4>: movel d2,sp@-
0x231e <isqrt+6>: movel a6@(8),d1
0x2322 <isqrt+10>: movel d1,d2
0x2324 <isqrt+12>: bra 0x232e <isqrt+22>
0x2326 <isqrt+14>: movel d2,d0
0x2328 <isqrt+16>: divsll d1,d0,d0
0x232c <isqrt+20>: addl d0,d1
0x232e <isqrt+22>: tstl d1
0x2330 <isqrt+24>: bge 0x2334 <isqrt+28>
0x2332 <isqrt+26>: addql #1,d1
0x2334 <isqrt+28>: asrl #1,d1
0x2336 <isqrt+30>: movel d2,d0
0x2338 <isqrt+32>: divsll d1,d0,d0
0x233c <isqrt+36>: cmpl d0,d1
0x233e <isqrt+38>: bgt 0x2326 <isqrt+14>
0x2340 <isqrt+40>: movel d1,d0
0x2342 <isqrt+42>: movel a6@(-4),d2
0x2346 <isqrt+46>: unlk a6
0x2348 <isqrt+48>: rts
The machine code of the above program is:
<isqrt>: 0x4e56 0x0000 0x2f02 0x222e 0x0008 0x2401 0x6008 0x2002
<isqrt+16>: 0x4c41 0x0800 0xd280 0x4a81 0x6c02 0x5281 0xe281 0x2002
<isqrt+32>: 0x4c41 0x0800 0xb280 0x6ee6 0x2001 0x242e 0xfffc 0x4e5e
<isqrt+48>: 0x4e75
In the logic, it is going to be a list like:
'(78      86      0       0       47      2       34      46
  0       8       36      1       96      8       32      2
  76      65      8       0       210     128     74      129
  108     2       82      129     226     129     32      2
  76      65      8       0       178     128     110     230

  32      1       36      46      255     252     78      94
  78      117)
|#
; in the logic, the program is defined by (isqrt-code).

Definition: isqrt-code

= '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0
      210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0
      178 128 110 230 32 1 36 46 255 252 78 94 78 117)

Theorem: mean-lessp-1 (((b + a) ÷ 2) < b) = (a < b)

; isqrt1 is a function in the Logic simulating the loop of the above code.

Definition: isqrt1 (i, j ) = if j ≃ 0 then fix (i)

elseif (i ÷ j ) < j then isqrt1 (i, (j + (i ÷ j )) ÷ 2)

else fix (j ) endif

; isqrt is a function in the Logic simulating the above code.

Definition: isqrt (i) = isqrt1 (i, i ÷ 2)

; the computation time of the loop.

Definition: isqrt1-t (i, j ) = if j ≃ 0 then 0

elseif (i ÷ j ) < j

then splus (10, isqrt1-t (i, (j + (i ÷ j )) ÷ 2))

else 8 endif

Definition: isqrt-t (i) = splus (8, isqrt1-t (i, i ÷ 2))

Event: Enable iplus.

Event: Enable integerp.

Event: Enable iquotient.

Event: Enable ilessp.

Event: Disable remainder.

Event: Disable quotient.

Theorem: isqrt-no-overflow (int-rangep (2 ∗ j , n) ∧ ((i ÷ j ) < j )) → int-rangep (j + (i ÷ j ), n)

Theorem: j-nonzerop ((1 < i) ∧ (0 < j )) → (((j + (i ÷ j )) ÷ 2) ≠ 0)

Theorem: j-int-rangep (int-rangep (2 ∗ j , n) ∧ ((i ÷ j ) < j )) → int-rangep (2 ∗ ((j + (i ÷ j )) ÷ 2), n)

; an induction hint.

Definition: isqrt-induct (s, i, j ) = if j ≃ 0 then t

elseif (i ÷ j ) < j

then isqrt-induct (stepn (s, 10), i, (j + (i ÷ j )) ÷ 2)

else t endif

Definition: isqrt-statep (s, i) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (mc-pc (s), mc-mem (s), 50)

∧ mcode-addrp (mc-pc (s), mc-mem (s), isqrt-code) ∧ ram-addrp (sub (32, 8, read-sp (s)), mc-mem (s), 16) ∧ (i = iread-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ ilessp (1, i))

Definition: isqrt-s0p (s, i, j ) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (sub (32, 30, mc-pc (s)), mc-mem (s), 50)

∧ mcode-addrp (sub (32, 30, mc-pc (s)), mc-mem (s), isqrt-code) ∧ ram-addrp (sub (32, 4, read-an (32, 6, s)), mc-mem (s), 16) ∧ (i = iread-dn (32, 2, s)) ∧ (j = iread-dn (32, 1, s)) ∧ int-rangep (2 ∗ j , 32) ∧ ilessp (1, i) ∧ ilessp (0, j ))

; from the initial state to s0.

Theorem: initial-j-int-rangep int-rangep (i, n) → int-rangep (2 ∗ (i ÷ 2), n)

Theorem: isqrt-s-s0 isqrt-statep (s, i) → (isqrt-s0p (stepn (s, 8), i, i ÷ 2)

∧ (linked-rts-addr (stepn (s, 8)) = rts-addr (s)) ∧ (linked-a6 (stepn (s, 8)) = read-an (32, 6, s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 8))) = sub (32, 4, read-sp (s)))

∧ (rn-saved (stepn (s, 8)) = read-dn (32, 2, s)))

Theorem: isqrt-s-s0-rfile (isqrt-statep (s, i) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 8)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: isqrt-s-s0-mem (isqrt-statep (s, i) ∧ disjoint (x, k, sub (32, 8, read-sp (s)), 16)) → (read-mem (x, mc-mem (stepn (s, 8)), k) = read-mem (x, mc-mem (s), k))

; from s0 to s0 (induction csae), or from s0 to exit (base case).
; base case:
; the basics we need to prove:
;   0. the machine is still running.
;   1. the pc is at the right position.
;   2. d0 contains the local variable j, the computing square root.
;   3. a6 should have the right value.
;   4. sp(a7) should have the right value.

Theorem: isqrt-s0-sn (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) ≮ j )) → ((mc-status (stepn (s, 8)) = 'running)

∧ (mc-pc (stepn (s, 8)) = linked-rts-addr (s))

∧ (iread-dn (32, 0, stepn (s, 8)) = j )

∧ (read-rn (32, 14, mc-rfile (stepn (s, 8))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 8))) = add (32, read-an (32, 6, s), 8)))

; 5. d2, which is used by this program, should be restored.

Theorem: isqrt-s0-sn-d2 (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) ≮ j ) ∧ (oplen ≤ 32)) → (read-rn (oplen, 2, mc-rfile (stepn (s, 8))) = head (rn-saved (s), oplen))

; and 6. those registers untouched by this program should still
; have their original contents.

Theorem: isqrt-s0-sn-rfile (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) ≮ j ) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 8)))

= read-rn (oplen, rn, mc-rfile (s)))

; and 7. the memory is correctly changed.

Theorem: isqrt1-s0-sn-mem (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) ≮ j )) → (read-mem (x, mc-mem (stepn (s, 8)), k) = read-mem (x, mc-mem (s), k))

Theorem: isqrt-s0p-j nonzerop isqrt-s0p (s, i, j ) → ((j ≠ 0) ∧ (j ∈ N))

; induction case: s0 --> s0.
; we need to prove:
;  0. the state predicate at s0 is still satisfied.
;  1. a6 is unchanged.
;  2. the content of original a6 on the sp stack is not changed.
;  3. the return address on the sp atack is not changed.
;  4. the content of original d2 on the sp stack is not changed.

Theorem: isqrt-s0-s0 (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) < j )) → (isqrt-s0p (stepn (s, 10), i, (j + (i ÷ j )) ÷ 2)

∧ (read-rn (oplen, 14, mc-rfile (stepn (s, 10))) = read-rn (oplen, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 10)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 10)) = linked-rts-addr (s)) ∧ (rn-saved (stepn (s, 10)) = rn-saved (s)))

; and 5. the registers that are not modified by this program still have
; their previous values.

Theorem: isqrt-s0-s0-rfile (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) < j ) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 10)))

= read-rn (oplen, rn, mc-rfile (s)))

; and 6. the memory is correctly changed.

Theorem: isqrt-s0-s0-mem (isqrt-s0p (s, i, j ) ∧ ((i ÷ j ) < j )) → (read-mem (x, mc-mem (stepn (s, 10)), k) = read-mem (x, mc-mem (s), k))

Event: Disable isqrt-statep.

Event: Disable isqrt-s0p.

Theorem: isqrt1-correctness isqrt-s0p (s, i, j ) → ((mc-status (stepn (s, isqrt1-t (i, j ))) = 'running)

∧ (mc-pc (stepn (s, isqrt1-t (i, j ))) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, isqrt1-t (i, j ))) = isqrt1 (i, j )) ∧ (read-rn (32, 14, mc-rfile (stepn (s, isqrt1-t (i, j ))))

= linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, isqrt1-t (i, j ))))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, isqrt1-t (i, j ))), k)

= read-mem (x, mc-mem (s), k)))

Theorem: isqrt1-d2 (isqrt-s0p (s, i, j ) ∧ (oplen ≤ 32)) → (read-rn (oplen, 2, mc-rfile (stepn (s, isqrt1-t (i, j ))))

= head (rn-saved (s), oplen))

Theorem: isqrt1-rfile (isqrt-s0p (s, i, j ) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, isqrt1-t (i, j ))))

= read-rn (oplen, rn, mc-rfile (s)))

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

Theorem: isqrt-correctness isqrt-statep (s, i) → ((mc-status (stepn (s, isqrt-t (i))) = 'running)

∧ (mc-pc (stepn (s, isqrt-t (i))) = rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, isqrt-t (i))) = isqrt (i)) ∧ (read-an (32, 6, stepn (s, isqrt-t (i))) = read-an (32, 6, s)) ∧ (read-an (32, 7, stepn (s, isqrt-t (i))) = add (32, read-an (32, 7, s), 4)))

;  5. d2, used for local variable j, is restored to its original value.

Theorem: isqrt-d2 (isqrt-statep (s, i) ∧ (oplen ≤ 32)) → (read-rn (oplen, 2, mc-rfile (stepn (s, isqrt-t (i))))

= read-dn (oplen, 2, s))

; and 6. the registers that are not modified by this program still have
; their original values.

Theorem: isqrt-rfile (isqrt-statep (s, i) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, isqrt-t (i))))

= read-rn (oplen, rn, mc-rfile (s)))

; and 7. the memory is correctly changed.  i.e. specify clearly the portions
; of the memory were changed and prove that is a truth.

Theorem: isqrt-read-mem (isqrt-statep (s, i) ∧ disjoint (x, k, sub (32, 8, read-sp (s)), 16)) → (read-mem (x, mc-mem (stepn (s, isqrt-t (i))), k)

= read-mem (x, mc-mem (s), k))

Event: Disable isqrt-t.

#|
; we next need to prove that isqrt does compute the integer square root.
; the following is the same as the proof in the file isqrt-ada.events.
(defn sq (j)
  (times j j))
(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)))
|#

Index

add, 4, 5, 7

d3-7a2-5p, 5–8 disjoint, 5, 8

evenp, 4

head, 5, 7

ilessp, 4 initial-j-int-rangep, 5 int-rangep, 4, 5 iread-dn, 4, 5, 7 iread-mem, 4 isqrt, 3, 7 isqrt-code, 3, 4 isqrt-correctness, 7 isqrt-d2, 8 isqrt-induct, 4 isqrt-no-overflow, 4 isqrt-read-mem, 8 isqrt-rfile, 8 isqrt-s-s0, 5 isqrt-s-s0-mem, 5 isqrt-s-s0-rfile, 5 isqrt-s0-s0, 6 isqrt-s0-s0-mem, 6 isqrt-s0-s0-rfile, 6 isqrt-s0-sn, 5 isqrt-s0-sn-d2, 5 isqrt-s0-sn-rfile, 6 isqrt-s0p, 4–7 isqrt-s0p-j nonzerop, 6 isqrt-statep, 4, 5, 7, 8 isqrt-t, 3, 7, 8 isqrt1, 3, 7 isqrt1-correctness, 7 isqrt1-d2, 7 isqrt1-rfile, 7 isqrt1-s0-sn-mem, 6 isqrt1-t, 3, 7 j-int-rangep, 4 j-nonzerop, 4

linked-a6, 5–7

linked-rts-addr, 5–7

mc-mem, 4–8 mc-pc, 4, 5, 7 mc-rfile, 5–8 mc-status, 4, 5, 7 mcode-addrp, 4 mean-lessp-1, 3

ram-addrp, 4 read-an, 4, 5, 7 read-dn, 5, 8 read-mem, 5–8 read-rn, 5–8 read-sp, 4, 5, 8 rn-saved, 5–7 rom-addrp, 4 rts-addr, 5, 7

splus, 3 stepn, 4–8 sub, 4, 5, 8