#|
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.
|#
;           Function Pointer Constrains with a Witness GT

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

#|
/* greater than relation */
gt(int a, int b)
{
 if (a == b)
   return 0;
 else if (a > b)
   return 1;
 else return -1;
}
The MC68020 assembly code of the above GCD program.  The code is generated
by "gcc -O".
0x22de <gt>:    linkw fp,#0

0x22e2 <gt+4>:  movel fp@(8),d1
0x22e6 <gt+8>:  movel fp@(12),d0
0x22ea <gt+12>: cmpl d1,d0
0x22ec <gt+14>: bne 0x22f2 <gt+20>
0x22ee <gt+16>: clrl d0
0x22f0 <gt+18>: bra 0x22fc <gt+30>
0x22f2 <gt+20>: cmpl d1,d0
0x22f4 <gt+22>: bge 0x22fa <gt+28>
0x22f6 <gt+24>: movel #1,d0
0x22f8 <gt+26>: bra 0x22fc <gt+30>
0x22fa <gt+28>: movel #-1,d0
0x22fc <gt+30>: unlk fp
0x22fe <gt+32>: rts
The machine code:
0x22de <gt>:    0x4e56  0x0000  0x222e  0x0008  0x202e  0x000c  0xb081  0x6604
0x22ee <gt+16>: 0x4280  0x600a  0xb081  0x6c04  0x7001  0x6002  0x70ff  0x4e5e
0x22fe <gt+32>: 0x4e75
'(78      86      0       0       34      46      0       8
  32      46      0       12      176     129     102     4
  66      128     96      10      176     129     108     4
  112     1       96      2       112     255     78      94
  78      117)
|#
; In Nqthm logic, gt-code defines the programs.

Definition: gt-code

= '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128
      96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)

Definition: gt (a, b) = if a = b then 0

elseif ilessp (b, a) then 1 else -1 endif

Definition: gt-t (a, b) = if a = b then 9

elseif ilessp (b, a) then 11 else 10 endif

; preconditions on the initial state.

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

∧ evenp (mc-pc (s))

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

∧ mcode-addrp (mc-pc (s), mc-mem (s), gt-code) ∧ ram-addrp (sub (32, 4, read-sp (s)), mc-mem (s), 16) ∧ (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)))

; correctness.

Event: Disable ilessp.

Theorem: gt-s-sn let sn be stepn (s, gt-t (a, b)) in gt-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-sp (s), 4))

∧ (d2-7a2-5p (rn)

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

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

∧ (disjoint (x, k, sub (32, 4, read-sp (s)), 4) → (read-mem (x, mc-mem (sn), k)

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

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

Event: Disable gt-t.

Event: Disable gt.

; function constrain with gt as witness.

Conservative Axiom: p-disjointness (p-disjoint (x, n, s) ∧ ((j + index-n (y, x)) ≤ n)) → p-disjoint (y, j , s)

Simultaneously, we introduce the new function symbol p-disjoint.

Conservative Axiom: fn*-correctness fn*-statep (s, a, b) → let sn be stepn (s, fn*-t (a, b))

in

(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-sp (s), 4)) ∧ (((oplen ≤ 32) ∧ d2-7a2-5p (rn))

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

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

∧ (p-disjoint (x, k, s)

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

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

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

Simultaneously, we introduce the new function symbols fn*-statep, fn*-t, and fn* .

;          Proof of the Correctness of a MAX Function
#|
The following C function max computes the maximum of integers a and b,
according to the comparison function comp.  Here, we study the problem
of function pointer.
max(int a, int b, int (*comp)(int, int))
{
  if ((*comp)(a, b) < 0)
    return b;
  else return a;
}
The MC68020 assembly code of the C function max on SUN-3 is given as
follows.  This binary is generated by "gcc -O".
0x2320 <max>:           linkw fp,#0
0x2324 <max+4>:         moveml d2-d3,sp@-
0x2328 <max+8>:         movel fp@(8),d3
0x232c <max+12>:        movel fp@(12),d2
0x2330 <max+16>:        movel d2,sp@-
0x2332 <max+18>:        movel d3,sp@-
0x2334 <max+20>:        moveal fp@(16),a0

0x2338 <max+24>:        jsr a0@
0x233a <max+26>:        tstl d0
0x233c <max+28>:        bge 0x2342 <max+34>
0x233e <max+30>:        movel d2,d0
0x2340 <max+32>:        bra 0x2344 <max+36>
0x2342 <max+34>:        movel d3,d0
0x2344 <max+36>:        moveml fp@(-8),d2-d3
0x234a <max+42>:        unlk fp
0x234c <max+44>:        rts
The machine code of the above program is:
<max>:      0x4e56  0x0000  0x48e7  0x3000  0x262e  0x0008  0x242e  0x000c
<max+16>:   0x2f02  0x2f03  0x206e  0x0010  0x4e90  0x4a80  0x6c04  0x2002
<max+32>:   0x6002  0x2003  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75
'(78      86      0       0       72      231     48      0
  38      46      0       8       36      46      0       12
  47      2       47      3       32      110     0       16
  78      144     74      128     108     4       32      2
  96      2       32      3       76      238     0       12
  255     248     78      94      78      117)
|#

Definition: max-code

= '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3
      32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76
      238 0 12 255 248 78 94 78 117)
; imax is the Nqthm counterpart of the program (max-code).

Definition: max-fn* (a, b) = if negativep (fn* (a, b)) then b

else a endif

; the computation time of the program.

Definition: max-t0 (a, b) = 8

Definition: max-t (a, b) = splus (max-t0 (a, b), splus (fn*-t (a, b),

if negativep (fn* (a, b)) then 7 else 6 endif))

; the assumptions of the initial state.

Definition: max-sp (s, a, b) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (mc-pc (s), mc-mem (s), 46) ∧ mcode-addrp (mc-pc (s), mc-mem (s), max-code) ∧ (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)) ∧ ram-addrp (sub (32, 24, read-sp (s)), mc-mem (s), 40))

Conservative Axiom: max-state (max-statep (s, a, b) → fn*-statep (stepn (s, max-t0 (a, b)), a, b)) ∧ (max-statep (s, a, b)

→ p-disjoint (add (32, read-rn (32, 15, mc-rfile (s)), 4294967272),

             40,

stepn (s, max-t0 (a, b))))

∧ (max-statep (s, a, b) = (max-sp (s, a, b) ∧ comp-loadp (s, a, b)))

Simultaneously, we introduce the new function symbols max-statep and comploadp.

; an intermediate state.

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

∧ (mc-pc (s)

= read-mem (add (32, read-an (32, 6, s), 16), mc-mem (s), 4)) ∧ evenp (rts-addr (s)) ∧ rom-addrp (sub (32, 26, rts-addr (s)), mc-mem (s), 46) ∧ mcode-addrp (sub (32, 26, rts-addr (s)), mc-mem (s), max-code) ∧ ram-addrp (read-sp (s), mc-mem (s), 40) ∧ equal* (read-sp (s), sub (32, 20, read-an (32, 6, s))) ∧ (a = iread-dn (32, 3, s)) ∧ (b = iread-dn (32, 2, s)) ∧ (iread-mem (add (32, read-sp (s), 4), mc-mem (s), 4) = a) ∧ (iread-mem (add (32, read-sp (s), 8), mc-mem (s), 4) = b))

; an intermediate state.

Definition: max-s1p (s, a, b) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

∧ rom-addrp (sub (32, 26, mc-pc (s)), mc-mem (s), 46)

∧ mcode-addrp (sub (32, 26, mc-pc (s)), mc-mem (s), max-code) ∧ ram-addrp (sub (32, 20, read-an (32, 6, s)), mc-mem (s), 40) ∧ (a = iread-dn (32, 3, s)) ∧ (b = iread-dn (32, 2, s)) ∧ (iread-dn (32, 0, s) = fn* (a, b)))

Conservative Axiom: max-disjointness (max-statep (s, a, b) ∧ max-disjoint (x, k, s)) → p-disjoint (x, k, stepn (s, max-t0 (a, b)))

Simultaneously, we introduce the new function symbol max-disjoint.

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

Theorem: max-s-s0 max-sp (s, a, b) → max-s0p (stepn (s, max-t0 (a, b)), a, b)

Theorem: max-s-s0-else let s0 be stepn (s, max-t0 (a, b)) in max-sp (s, a, b) → ((linked-rts-addr (s0 ) = rts-addr (s))

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

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

∧ (movem-saved (s0 , 4, 8, 2)

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

Theorem: max-s-s0-rfile (max-sp (s, a, b) ∧ d4-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, max-t0 (a, b))))

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

Theorem: max-s-s0-mem (max-sp (s, a, b) ∧ disjoint (x, k, sub (32, 24, read-sp (s)), 24)) → (read-mem (x, mc-mem (stepn (s, max-t0 (a, b))), k)

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

; from s0 to s1.  s0 --> s1.  This is basically a fact about the
; subroutine comp.

Theorem: max-s0-s1 (max-s0p (s, a, b) ∧ fn*-statep (s, a, b)) → max-s1p (stepn (s, fn*-t (a, b)), a, b)

Theorem: max-s0-s1-else (max-s0p (s, a, b) ∧ fn*-statep (s, a, b) ∧ p-disjoint (sub (32, 20, read-an (32, 6, s)), 40, s)) → ((linked-rts-addr (stepn (s, fn*-t (a, b))) = linked-rts-addr (s))

∧ (read-rn (32, 14, mc-rfile (stepn (s, fn*-t (a, b))))

= read-rn (32, 14, mc-rfile (s))) ∧ (linked-a6 (stepn (s, fn*-t (a, b))) = linked-a6 (s)) ∧ (movem-saved (stepn (s, fn*-t (a, b)), 4, 8, 2)

= movem-saved (s, 4, 8, 2)))

Theorem: max-s0-s1-rfile (max-s0p (s, a, b) ∧ fn*-statep (s, a, b) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, fn*-t (a, b))))

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

Theorem: max-s0-s1-mem (max-s0p (s, a, b) ∧ fn*-statep (s, a, b) ∧ p-disjoint (x, k, s)) → (read-mem (x, mc-mem (stepn (s, fn*-t (a, b))), k)

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

; from s1 to exit.  s1 --> exit.

Theorem: max-s1-sn-1 (max-s1p (s, a, b) ∧ negativep (fn* (a, b))) → ((mc-status (stepn (s, 7)) = 'running)

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

∧ (iread-dn (32, 0, stepn (s, 7)) = b)

∧ (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)) ∧ (read-mem (x, mc-mem (stepn (s, 7)), k) = read-mem (x, mc-mem (s), k)))

Theorem: max-s1-sn-rfile-1 (max-s1p (s, a, b) ∧ negativep (fn* (a, b)) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

= 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: max-s1-sn-2 (max-s1p (s, a, b) ∧ (¬ negativep (fn* (a, b)))) → ((mc-status (stepn (s, 6)) = 'running)

∧ (mc-pc (stepn (s, 6)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 6)) = a) ∧ (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)), k)

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

Theorem: max-s1-sn-rfile-2 (max-s1p (s, a, b) ∧ (¬ negativep (fn* (a, b))) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (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)

; the correctness of max.

Event: Disable max-t0.

Theorem: max-correctness let sn be stepn (s, max-t (a, b)) in max-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-sp (s), 4)) ∧ (((oplen ≤ 32) ∧ d2-7a2-5p (rn))

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

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

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

∧ max-disjoint (x, k, s))

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

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

∧ (iread-dn (32, 0, sn) = max-fn* (a, b))) endlet

Theorem: disjoint-la4 (disjoint (a, m, b, n) ∧ ((j + index-n (a1 , a)) ≤ m) ∧ ((l + index-n (b1 , b)) ≤ n)) → disjoint (a1 , j , b1 , l)

; instantiation.

Definition: max-gt-statep (s, a, b) = let comp be read-mem (add (32, read-sp (s), 12), mc-mem (s), 4)

in (mc-status (s) = 'running) ∧ evenp (mc-pc (s)) ∧ rom-addrp (mc-pc (s), mc-mem (s), 46) ∧ mcode-addrp (mc-pc (s), mc-mem (s), max-code) ∧ (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)) ∧ evenp (comp) ∧ rom-addrp (comp, mc-mem (s), len (gt-code)) ∧ mcode-addrp (comp, mc-mem (s), gt-code) ∧ ram-addrp (sub (32, 28, read-sp (s)), mc-mem (s), 44) endlet

Definition: max-gt-t (a, b) = splus (max-t0 (a, b),

splus (gt-t (a, b), if negativep (gt (a, b)) then 7 else 6 endif))

Definition: max-gt (a, b) = if negativep (gt (a, b)) then b

else a endif

Theorem: max-gt-statep-s0 let s0 be stepn (s, max-t0 (a, b)) in max-gt-statep (s, a, b) → ((mc-status (s0 ) = 'running)

∧ (mc-pc (s0 )

= read-mem (add (32, read-sp (s), 12), mc-mem (s), 4)) ∧ (read-rn (32, 15, mc-rfile (s0 ))

= sub (32, 24, read-sp (s))) ∧ (iread-mem (add (32, read-rn (32, 15, mc-rfile (s0 )), 4),

mc-mem (s0 ),

= a) ∧ (iread-mem (add (32, read-rn (32, 15, mc-rfile (s0 )), 8),

mc-mem (s0 ),

               4)

= b)) endlet

Theorem: max-gt-correctness max-gt-statep (s, a, b) → let sn be stepn (s, max-gt-t (a, b))

in (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-sp (s), 4)) ∧ (((oplen ≤ 32) ∧ d2-7a2-5p (rn))

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

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

∧ ((disjoint (x, k, sub (32, 24, read-sp (s)), 40) ∧ disjoint (x, k, sub (32, 28, read-sp (s)), 4)) → (read-mem (x, mc-mem (sn), k)

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

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

Index

add, 3, 4, 6, 8–11

comp-loadp, 6

d2-7a2-5p, 3, 4, 8, 9, 11 d4-7a2-5p, 7–9 disjoint, 3, 7, 9–11 disjoint-la4, 10

equal*, 6 evenp, 3, 6, 7, 10

fn*, 4–9 fn*-correctness, 4 fn*-statep, 4, 6, 8 fn*-t, 4, 6, 8

get-vlst, 8, 9 gt, 2, 3, 10 gt-code, 2, 3, 10 gt-s-sn, 3 gt-statep, 3 gt-t, 2, 3, 10

ilessp, 2 index-n, 3, 10 iread-dn, 3, 4, 6–9, 11 iread-mem, 3, 6, 10, 11

len, 10 linked-a6, 7–9 linked-rts-addr, 7–9

max-code, 5–7, 10 max-correctness, 9 max-disjoint, 7, 9 max-disjointness, 7 max-fn*, 5, 9 max-gt, 10, 11 max-gt-correctness, 11 max-gt-statep, 10, 11 max-gt-statep-s0, 10 max-gt-t, 10, 11 max-s-s0, 7 max-s-s0-else, 7 max-s-s0-mem, 7 max-s-s0-rfile, 7 max-s0-s1, 8 max-s0-s1-else, 8 max-s0-s1-mem, 8 max-s0-s1-rfile, 8 max-s0p, 6–8 max-s1-sn-1, 8 max-s1-sn-2, 9 max-s1-sn-rfile-1, 8 max-s1-sn-rfile-2, 9 max-s1p, 7–9 max-sp, 6, 7 max-state, 6 max-statep, 6, 7, 9 max-t, 5, 9 max-t0, 5–7, 10 mc-mem, 3, 4, 6–11 mc-pc, 3, 4, 6–11 mc-rfile, 3, 4, 6–11 mc-status, 3, 4, 6–11 mcode-addrp, 3, 6, 7, 10 movem-saved, 7–9

p-disjoint, 3, 4, 6–8 p-disjointness, 3

ram-addrp, 3, 6, 7, 10 read-an, 6–9 read-mem, 3, 4, 6–11 read-rn, 3, 4, 6–11 read-sp, 3, 4, 6, 7, 9–11 readm-rn, 7 rom-addrp, 3, 6, 7, 10 rts-addr, 3, 4, 6, 7, 9, 11

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