#|
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 LOG2 Program

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

#|
The following C function computes the integer logarithm (base 2) of a
nonnegative integer.  We proved the correctness of the binary of this
C function.  The binary is produced by Gnu C compiler.
The proof described here was worked out with Matt Kaufmann and Bill
Pierce.
/* computes the integer logarithm of a nonnegative integer. */
log2(int n)
{
 int log = 0;
 while (n > 1) {
   log++;

    n /= 2;}
  return(log);
}
Here is the MC68020 assembly code of the above LOG2 program.  The code is
generated by "gcc -O".
0x22ce <log2>:          linkw fp,#0
0x22d2 <log2+4>:        movel d2,sp@-
0x22d4 <log2+6>:        movel fp@(8),d0
0x22d8 <log2+10>:       clrl d1
0x22da <log2+12>:       bra 0x22e6 <log2+24>
0x22dc <log2+14>:       addql #1,d1
0x22de <log2+16>:       tstl d0
0x22e0 <log2+18>:       bge 0x22e4 <log2+22>
0x22e2 <log2+20>:       addql #1,d0
0x22e4 <log2+22>:       asrl #1,d0
0x22e6 <log2+24>:       movel #1,d2
0x22e8 <log2+26>:       cmpl d0,d2
0x22ea <log2+28>:       blt 0x22dc <log2+14>
0x22ec <log2+30>:       movel d1,d0
0x22ee <log2+32>:       movel fp@(-4),d2
0x22f2 <log2+36>:       unlk fp
0x22f4 <log2+38>:       rts
<log2>:      0x4e56  0x0000  0x2f02  0x202e  0x0008  0x4281  0x600a  0x5281
<log2+16>:   0x4a80  0x6c02  0x5280  0xe280  0x7401  0xb480  0x6df0  0x2001
<log2+32>:   0x242e  0xfffc  0x4e5e  0x4e75
'(78      86      0       0       47      2       32      46
  0       8       66      129     96      10      82      129
  74      128     108     2       82      128     226     128
  116     1       180     128     109     240     32      1
  36      46      255     252     78      94      78      117)
|#
; in Nqthm, log2 is defined as:

Definition: log2-code

= '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128
      108 2 82 128 226 128 116 1 180 128 109 240 32 1 36
      46 255 252 78 94 78 117)
; we define the Nqthm counterpart of log2.

Definition: log2 (n, log2 ) = if 1 < n then log2 (n ÷ 2, 1 + log2 )

else log2 endif

; the clock.

Definition: log2-t0 (n) = if 1 < n then splus (7, log2-t0 (n ÷ 2))

else 7 endif

Definition: log2-t (n) = splus (5, log2-t0 (n))

; an induction hint.

Definition: log2-induct (s, n, log2 ) = if 1 < n then log2-induct (stepn (s, 7), n ÷ 2, 1 + log2 )

else t endif

; the preconditions on the initail state.

Definition: log2-statep (s, n) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

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

∧ mcode-addrp (mc-pc (s), mc-mem (s), log2-code) ∧ ram-addrp (sub (32, 8, read-sp (s)), mc-mem (s), 16) ∧ (n = iread-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (n ∈ N))

; an intermediate state.

Definition: log2-s0p (s, n, log2 ) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (sub (32, 24, mc-pc (s)), mc-mem (s), 40)

∧ mcode-addrp (sub (32, 24, mc-pc (s)), mc-mem (s), log2-code) ∧ ram-addrp (sub (32, 4, read-an (32, 6, s)), mc-mem (s), 16) ∧ (n = iread-dn (32, 0, s)) ∧ (log2 = iread-dn (32, 1, s)) ∧ int-rangep (log2 + n, 32) ∧ (log2 ∈ N) ∧ (n ∈ N))

; from the initial state to s0:  s --> s0.

Theorem: log2-s-s0 log2-statep (s, n) → log2-s0p (stepn (s, 5), n, 0)

Theorem: log2-s-s0-else log2-statep (s, n) → ((linked-rts-addr (stepn (s, 5)) = rts-addr (s))

∧ (linked-a6 (stepn (s, 5)) = read-an (32, 6, s))

∧ (read-rn (32, 14, mc-rfile (stepn (s, 5))) = sub (32, 4, read-sp (s)))

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

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

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

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

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

Theorem: log2-s0-sn-base (log2-s0p (s, n, log2 ) ∧ (1 ≮ n)) → ((mc-status (stepn (s, 7)) = 'running)

∧ (mc-pc (stepn (s, 7)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 7)) = log2 ) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 7))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 7))) = add (32, read-an (32, 6, s), 8)))

Theorem: log2-s0-sn-base-rfile (log2-s0p (s, n, log2 ) ∧ (1 ≮ n) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

= if d3-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s)) else head (rn-saved (s), oplen) endif)

Theorem: log2-s0s-n-base-mem (log2-s0p (s, n, log2 ) ∧ (1 ≮ n)) → (read-mem (x, mc-mem (stepn (s, 7)), k) = read-mem (x, mc-mem (s), k))

; induction case: s0 --> s0.

Theorem: log2-rangep-la (int-rangep (m + n, 32) ∧ (1 < n)) → int-rangep (1 + (m + (n ÷ 2)), 32)

Theorem: log2-s0-s0 (log2-s0p (s, n, log2 ) ∧ (1 < n)) → (log2-s0p (stepn (s, 7), n ÷ 2, 1 + log2 )

∧ (read-rn (oplen, 14, mc-rfile (stepn (s, 7))) = read-rn (oplen, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, 7)) = linked-a6 (s)) ∧ (linked-rts-addr (stepn (s, 7)) = linked-rts-addr (s)) ∧ (read-mem (x, mc-mem (stepn (s, 7)), k) = read-mem (x, mc-mem (s), k)) ∧ (rn-saved (stepn (s, 7)) = rn-saved (s)))

Theorem: log2-s0-s0-rfile (log2-s0p (s, n, log2 ) ∧ (1 < n) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

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

; put together.

Theorem: log2-s0-sn log2-s0p (s, n, log2 ) → ((mc-status (stepn (s, log2-t0 (n))) = 'running)

∧ (mc-pc (stepn (s, log2-t0 (n))) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, log2-t0 (n))) = log2 (n, log2 )) ∧ (read-rn (32, 14, mc-rfile (stepn (s, log2-t0 (n))))

= linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, log2-t0 (n))))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, log2-t0 (n))), k)

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

Theorem: log2-s0-sn-rfile (log2-s0p (s, n, log2 ) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, log2-t0 (n))))

= if d3-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s)) else head (rn-saved (s), oplen) endif)

; correctness.

Theorem: log2-correct log2-statep (s, n) → ((mc-status (stepn (s, log2-t (n))) = 'running)

∧ (mc-pc (stepn (s, log2-t (n))) = rts-addr (s))

∧ (iread-dn (32, 0, stepn (s, log2-t (n))) = log2 (n, 0))

∧ (read-an (32, 6, stepn (s, log2-t (n))) = read-an (32, 6, s)) ∧ (read-an (32, 7, stepn (s, log2-t (n))) = add (32, read-an (32, 7, s), 4)))

Theorem: log2-rfile (log2-statep (s, n) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, log2-t (n))))

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

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

; the correctness of the Nqthm function log2.

Theorem: log2-log (i ∈ N) → (log2 (n, i) = (i + log (2, n)))

; 2^log2(n) <= n.

Theorem: log2-thm1 (1 < n) → (n ≮ exp (2, log2 (n, 0)))

; n < 2^(log2(n)+1).

Theorem: log2-thm2 n < exp (2, 1 + log2 (n, 0))

Index

add, 3–6

d2-7a2-5p, 4–6 d3-7a2-5p, 4, 5 disjoint, 4, 6

evenp, 3 exp, 6

head, 4, 5

int-rangep, 3, 5 iread-dn, 3–6 iread-mem, 3

linked-a6, 4, 5 linked-rts-addr, 4, 5 log, 6 log2, 3, 5, 6 log2-code, 2, 3 log2-correct, 5 log2-induct, 3 log2-log, 6 log2-mem, 6 log2-rangep-la, 5 log2-rfile, 6 log2-s-s0, 4 log2-s-s0-else, 4 log2-s-s0-mem, 4 log2-s-s0-rfile, 4 log2-s0-s0, 5 log2-s0-s0-rfile, 5 log2-s0-sn, 5 log2-s0-sn-base, 4 log2-s0-sn-base-rfile, 4 log2-s0-sn-rfile, 5 log2-s0p, 3–5 log2-s0s-n-base-mem, 4 log2-statep, 3–6 log2-t, 3, 5, 6 log2-t0, 3, 5 log2-thm1, 6 log2-thm2, 6

mc-mem, 3–6 mc-pc, 3–6 mc-rfile, 4–6 mc-status, 3–5 mcode-addrp, 3

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

splus, 3 stepn, 3–6 sub, 3, 4, 6