#|
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 a GCD Program

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

#|
The following C program computes the greatest common divisor of two
integers a and b. We, here, investigate the machine code of this
program generated by a widely used C compiler, and verify the
correctness of the code.
/* computes the greatest common divisor by Euclid's algorithm */
gcd(int a, int b)
{
 while (a != 0){
   if (b == 0) return (a);
   if (a > b)
     a = a % b;
   else b = b % a;

  };
  return (b);
}
Here is the MC68020 assembly code of the above GCD program.  The code is
generated by "gcc -O".
0x22c6 <gcd>:           linkw a6,#0
0x22ca <gcd+4>:         moveml d2-d3,sp@-
0x22ce <gcd+8>:         movel a6@(8),d2
0x22d2 <gcd+12>:        movel a6@(12),d3
0x22d6 <gcd+16>:        tstl d2
0x22d8 <gcd+18>:        beq 0x22f6 <gcd+48>
0x22da <gcd+20>:        tstl d3
0x22dc <gcd+22>:        bne 0x22e2 <gcd+28>
0x22de <gcd+24>:        movel d2,d0
0x22e0 <gcd+26>:        bra 0x22f8 <gcd+50>
0x22e2 <gcd+28>:        cmpl d2,d3
0x22e4 <gcd+30>:        bge 0x22ee <gcd+40>
0x22e6 <gcd+32>:        divsll d3,d0,d2
0x22ea <gcd+36>:        movel d0,d2
0x22ec <gcd+38>:        bra 0x22d6 <gcd+16>
0x22ee <gcd+40>:        divsll d2,d0,d3
0x22f2 <gcd+44>:        movel d0,d3
0x22f4 <gcd+46>:        bra 0x22d6 <gcd+16>
0x22f6 <gcd+48>:        movel d3,d0
0x22f8 <gcd+50>:        moveml a6@(-8),d2-d3
0x22fe <gcd+56>:        unlk a6
0x2300 <gcd+58>:        rts
The machine code of the above program is:
<gcd>:       0x4e56  0x0000  0x48e7  0x3000  0x242e  0x0008  0x262e  0x000c
<gcd+16>:    0x4a82  0x671c  0x4a83  0x6604  0x2002  0x6016  0xb682  0x6c08
<gcd+32>:    0x4c43  0x2800  0x2400  0x60e8  0x4c42  0x3800  0x2600  0x60e0
<gcd+48>:    0x2003  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75
'(78      86      0       0       72      231     48      0
  36      46      0       8       38      46      0       12
  74      130     103     28      74      131     102     4
  32      2       96      22      182     130     108     8
  76      67      40      0       36      0       96      232
  76      66      56      0       38      0       96      224
  32      3       76      238     0       12      255     248

  78      94      78      117)
|#
; now we start the correctness proof of this GCD program, defined by
; (gcd-code).

Definition: gcd-code

= '(78 86 0 0 72 231 48 0 36 46 0 8 38 46 0 12 74 130
      103 28 74 131 102 4 32 2 96 22 182 130 108 8 76 67
      40 0 36 0 96 232 76 66 56 0 38 0 96 224 32 3 76 238
      0 12 255 248 78 94 78 117)

Conservative Axiom: gcd-load gcd-loadp (s) = (evenp (gcd-addr)

∧ (gcd-addr ∈ N)

∧ nat-rangep (gcd-addr, 32)

∧ rom-addrp (gcd-addr, mc-mem (s), 60)

∧ mcode-addrp (gcd-addr, mc-mem (s), gcd-code))

Simultaneously, we introduce the new function symbols gcd-loadp and gcd-addr.

Theorem: stepn-gcd-loadp gcd-loadp (stepn (s, n)) = gcd-loadp (s)

; the functional description of the program (gcd-code).

Definition: gcd (a, b) = if a ≃ 0 then fix (b)

elseif b ≃ 0 then a

elseif b < a then gcd (a mod b, b)

else gcd (a, b mod a) endif

; the clock function.

Definition: gcd-t1 (a, b) = if a ≃ 0 then 6

elseif b ≃ 0 then 9

elseif b < a then splus (9, gcd-t1 (a mod b, b))

else splus (9, gcd-t1 (a, b mod a)) endif

Definition: gcd-t (a, b) = splus (4, gcd-t1 (a, b))

; an induction hint.

Definition: gcd-induct (s, a, b) = if (a ≃ 0) ∨ (b ≃ 0) then t

elseif b < a then gcd-induct (stepn (s, 9), a mod b, b) else gcd-induct (stepn (s, 9), a, b mod a) endif

; the initial state.

Definition: gcd-statep (s, a, b) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (mc-pc (s), mc-mem (s), 60) ∧ mcode-addrp (mc-pc (s), mc-mem (s), gcd-code) ∧ ram-addrp (sub (32, 12, read-sp (s)), mc-mem (s), 24) ∧ (a = iread-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (b = iread-mem (add (32, read-sp (s), 8), mc-mem (s), 4)) ∧ (a ∈ N) ∧ (b ∈ N))

; an intermediate state.

Definition: gcd-s0p (s, a, b) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (sub (32, 16, mc-pc (s)), mc-mem (s), 60) ∧ mcode-addrp (sub (32, 16, mc-pc (s)), mc-mem (s), gcd-code) ∧ ram-addrp (sub (32, 8, read-an (32, 6, s)), mc-mem (s), 24) ∧ (a = iread-dn (32, 2, s)) ∧ (b = iread-dn (32, 3, s)) ∧ (a ∈ N) ∧ (b ∈ N))

; s --> s0.

Theorem: gcd-s-s0 gcd-statep (s, a, b) → (gcd-s0p (stepn (s, 4), a, b)

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

= sub (32, 4, read-sp (s))) ∧ (movem-saved (stepn (s, 4), 4, 8, 2)

= readm-rn (32, '(2 3), mc-rfile (s))))

Theorem: gcd-s-s0-rfile (gcd-statep (s, a, b) ∧ d4-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 4)))

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

Theorem: gcd-s-s0-mem (gcd-statep (s, a, b) ∧ disjoint (x, l, sub (32, 12, read-sp (s)), 24)) → (read-mem (x, mc-mem (stepn (s, 4)), l) = read-mem (x, mc-mem (s), l))

; s0 --> exit.
; base case: s0 --> exit.

Theorem: gcd-s0-sn-base-1 (gcd-s0p (s, a, b) ∧ (a ≃ 0)) → ((mc-status (stepn (s, 6)) = 'running)

∧ (mc-pc (stepn (s, 6)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 6)) = fix (b)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 6))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 6)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 6)), l)

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

Theorem: gcd-s0-sn-base-rfile-1 (gcd-s0p (s, a, b) ∧ (a ≃ 0) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= if d4-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s)) else get-vlst (oplen, 0, rn, '(2 3), movem-saved (s, 4, 8, 2)) endif)

Theorem: gcd-s0-sn-base-2 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≃ 0)) → ((mc-status (stepn (s, 9)) = 'running)

∧ (mc-pc (stepn (s, 9)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 9)) = fix (a)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 9))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 9)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 9)), l)

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

Theorem: gcd-s0-sn-base-rfile-2 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≃ 0) ∧ d2-7a2-5p (rn)

∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

= if d4-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s)) else get-vlst (oplen, 0, rn, '(2 3), movem-saved (s, 4, 8, 2)) endif)

; induction case:  s0 --> s0.

Event: Enable integerp.

Event: Enable iremainder.

Theorem: gcd-s0-s0-1 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≄ 0) ∧ (b < a)) → (gcd-s0p (stepn (s, 9), a mod b, b)

∧ (read-rn (oplen, 14, mc-rfile (stepn (s, 9)))

= read-rn (oplen, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 9)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 9)) = linked-rts-addr (s)) ∧ (movem-saved (stepn (s, 9), 4, 8, 2) = movem-saved (s, 4, 8, 2)) ∧ (read-mem (x, mc-mem (stepn (s, 9)), l)

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

Theorem: gcd-s0-s0-2 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≄ 0) ∧ (b ≮ a)) → (gcd-s0p (stepn (s, 9), a, b mod a)

∧ (read-rn (oplen, 14, mc-rfile (stepn (s, 9)))

= read-rn (oplen, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 9)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 9)) = linked-rts-addr (s)) ∧ (movem-saved (stepn (s, 9), 4, 8, 2) = movem-saved (s, 4, 8, 2)) ∧ (read-mem (x, mc-mem (stepn (s, 9)), l)

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

Theorem: gcd-s0-s0-rfile-1 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≄ 0) ∧ (b < a) ∧ d4-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

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

Theorem: gcd-s0-s0-rfile-2 (gcd-s0p (s, a, b) ∧ (a ≄ 0) ∧ (b ≄ 0) ∧ (b ≮ a) ∧ d4-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

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

; put together.

Theorem: gcd-s0-sn let sn be stepn (s, gcd-t1 (a, b)) in gcd-s0p (s, a, b) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, sn) = gcd (a, b)) ∧ (read-rn (32, 14, mc-rfile (sn)) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (sn), k) = read-mem (x, mc-mem (s), k))) endlet

Theorem: gcd-s0-sn-rfile (gcd-s0p (s, a, b) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, gcd-t1 (a, b))))

= if d4-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen, 0, rn, '(2 3), movem-saved (s, 4, 8, 2)) endif)

; the correctness of gcd.

Theorem: gcd-correctness let sn be stepn (s, gcd-t (a, b)) in gcd-statep (s, a, b) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = rts-addr (s)) ∧ (read-rn (32, 14, mc-rfile (sn))

= read-rn (32, 14, mc-rfile (s))) ∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 7, s), 4)) ∧ ((d2-7a2-5p (rn) ∧ (oplen ≤ 32))

→ (read-rn (oplen, rn, mc-rfile (sn))

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

∧ (disjoint (x, k, sub (32, 12, read-sp (s)), 24)

→ (read-mem (x, mc-mem (sn), k)

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

∧ (iread-dn (32, 0, sn) = gcd (a, b))) endlet

Event: Disable gcd-t.

; to prove that (gcd a b) does compute the greatest common divisor, we need
; to prove the following two theorems:
;     1. (gcd a b) divides a and (gcd a b) divides b.
;        i.e. (gcd a b) is a common divisor of a and b.
;     2. any divisor of a and b is no greater than (gcd a b).

Theorem: remainder-remainder ((b mod c) = 0) → (((a mod b) mod c) = (a mod c))

Theorem: gcd-is-cd ((a mod gcd (a, b)) = 0) ∧ ((b mod gcd (a, b)) = 0)

Theorem: gcd-the-greatest ((a ≄ 0) ∧ (b ≄ 0) ∧ ((a mod x) = 0) ∧ ((b mod x) = 0)) → (gcd (a, b) ≮ x)

; a simple timing analysis.

Theorem: lessp-times-lessp ((a < b) ∧ (c ≄ 0)) → (a < (b ∗ c))

Theorem: remainder-shrink-half ((b ≤ a) ∧ (b ≄ 0)) → ((a ÷ 2) ≮ (a mod b))

Theorem: gcd-t-shrink-1 ((b ≤ a) ∧ (b ≄ 0)) → ((log (2, a) − 1) ≮ log (2, a mod b))

Theorem: gcd-t-shrink-2 ((b ≤ a) ∧ (b ≄ 0) ∧ (a ≠ 1)) → ((9 ∗ (x + log (2, a)))

≮ (9 + (9 ∗ (x + log (2, a mod b)))))

Definition: gcd-t2 (a, b) = if a ≃ 0 then 6

elseif b ≃ 0 then 9

elseif b < a then 9 + gcd-t2 (a mod b, b) elseif a < b then 9 + gcd-t2 (a, b mod a) else 18 endif

Theorem: gcd-t2-ub gcd-t2 (a, b) ≤ (18 + (9 ∗ (log (2, a) + log (2, b))))

Theorem: gcd-t1-t2 gcd-t1 (a, b) = gcd-t2 (a, b)

Theorem: gcd-t-ub gcd-t (a, b) ≤ (22 + (9 ∗ (log (2, a) + log (2, b))))

Theorem: gcd-t-ubound ((a < exp (2, 31)) ∧ (b < exp (2, 31))) → (gcd-t (a, b) ≤ 580)

Event: Make the library "gcd" and compile it.

Index

add, 4, 5, 7

d2-7a2-5p, 5, 7 d4-7a2-5p, 5–7 disjoint, 5, 7

evenp, 3, 4 exp, 8

gcd, 3, 7, 8 gcd-addr, 3 gcd-code, 3, 4 gcd-correctness, 7 gcd-induct, 4 gcd-is-cd, 8 gcd-load, 3 gcd-loadp, 3 gcd-s-s0, 4 gcd-s-s0-mem, 5 gcd-s-s0-rfile, 5 gcd-s0-s0-1, 6 gcd-s0-s0-2, 6 gcd-s0-s0-rfile-1, 6 gcd-s0-s0-rfile-2, 6 gcd-s0-sn, 7 gcd-s0-sn-base-1, 5 gcd-s0-sn-base-2, 5 gcd-s0-sn-base-rfile-1, 5 gcd-s0-sn-base-rfile-2, 5 gcd-s0-sn-rfile, 7 gcd-s0p, 4–7 gcd-statep, 4, 5, 7 gcd-t, 3, 7, 8 gcd-t-shrink-1, 8 gcd-t-shrink-2, 8 gcd-t-ub, 8 gcd-t-ubound, 8 gcd-t1, 3, 7, 8 gcd-t1-t2, 8 gcd-t2, 8 gcd-t2-ub, 8 gcd-the-greatest, 8 get-vlst, 5–7

iread-dn, 4, 5, 7 iread-mem, 4

lessp-times-lessp, 8 linked-a6, 4–7 linked-rts-addr, 4–7 log, 8

mc-mem, 3–7 mc-pc, 4, 5, 7 mc-rfile, 4–7 mc-status, 4, 5, 7 mcode-addrp, 3, 4 movem-saved, 4–7

nat-rangep, 3

ram-addrp, 4 read-an, 4, 5, 7 read-mem, 5–7 read-rn, 4–7 read-sp, 4, 5, 7 readm-rn, 4 remainder-remainder, 8 remainder-shrink-half, 8 rom-addrp, 3, 4 rts-addr, 4, 7

splus, 3 stepn, 3–7 stepn-gcd-loadp, 3 sub, 4, 5, 7