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

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

;          Proof of the Correctness of the MEMSET Function
#|
This is part of our effort to verify the Berkeley string library.  The
Berkeley string library is widely used as part of the Berkeley Unix OS.
This is the source code of memset function in the Berkeley string library.
void *
memset(dst, c, n)
       void *dst;
       register int c;
       register size_t n;
{
       if (n != 0) {
               register char *d = dst;

                do
                        *d++ = c;
                while (--n != 0);
        }
        return (dst);
}
The MC68020 assembly code of the C function memset on SUN-3 is given as
follows.  This binary is generated by "gcc -O".
0x29d0 <memset>:        linkw fp,#0
0x29d4 <memset+4>:      movel d2,sp@-
0x29d6 <memset+6>:      movel fp@(8),d2
0x29da <memset+10>:     movel fp@(16),d0
0x29de <memset+14>:     beq 0x29ec <memset+28>
0x29e0 <memset+16>:     moveal d2,a0
0x29e2 <memset+18>:     moveb fp@(15),d1
0x29e6 <memset+22>:     moveb d1,a0@+
0x29e8 <memset+24>:     subl #1,d0
0x29ea <memset+26>:     bne 0x29e6 <memset+22>
0x29ec <memset+28>:     movel d2,d0
0x29ee <memset+30>:     movel fp@(-4),d2
0x29f2 <memset+34>:     unlk fp
0x29f4 <memset+36>:     rts
The machine code of the above program is:
<memset>:     0x4e56  0x0000  0x2f02  0x242e  0x0008  0x202e  0x0010  0x670c
<memset+16>:  0x2042  0x122e  0x000f  0x10c1  0x5380  0x66fa  0x2002  0x242e
<memset+32>:  0xfffc  0x4e5e  0x4e75
'(78    86      0       0       47      2       36      46
  0     8       32      46      0       16      103     12
  32    66      18      46      0       15      16      193
  83    128     102     250     32      2       36      46
  255   252     78      94      78      117)
|#
; in the logic, the above program is defined by (memset-code).

Definition: memset-code

= '(78 86 0 0 47 2 36 46 0 8 32 46 0 16 103 12 32 66 18
      46 0 15 16 193 83 128 102 250 32 2 36 46 255 252 78

      94 78 117)
; the computation time of the program.

Definition: memset-t1 (n) = if (n − 1) = 0 then 7

else splus (3, memset-t1 (n − 1)) endif

Definition: memset-t (n) = if n = 0 then 9

else splus (7, memset-t1 (n)) endif

; an induction hint.

Definition: memset-induct (s, i* , i, n, lst, ch) = if (n − 1) = 0 then t

else memset-induct (stepn (s, 3), add (32, i* , 1), 1 + i, n − 1, put-nth (ch, i, lst), ch) endif

; the preconditions of the initial state.

Definition: memset-statep (s, str, n, lst, ch) = ((mc-status (s) = 'running)

∧ evenp (mc-pc (s))

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

∧ mcode-addrp (mc-pc (s), mc-mem (s), memset-code) ∧ ram-addrp (sub (32, 8, read-sp (s)), mc-mem (s), 24) ∧ ram-addrp (str, mc-mem (s), n) ∧ mem-lst (1, str, mc-mem (s), n, lst) ∧ disjoint (sub (32, 8, read-sp (s)), 24, str, n) ∧ (str = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (ch = uread-mem (add (32, read-sp (s), 11), mc-mem (s), 1)) ∧ (n = uread-mem (add (32, read-sp (s), 12), mc-mem (s), 4)))

; an intermediate state.

Definition: memset-s0p (s, i* , i, str, n, lst, ch, n )

= ((mc-status (s) = 'running)

∧ evenp (mc-pc (s)) ∧ rom-addrp (sub (32, 22, mc-pc (s)), mc-mem (s), 38) ∧ mcode-addrp (sub (32, 22, mc-pc (s)), mc-mem (s), memset-code) ∧ ram-addrp (sub (32, 4, read-an (32, 6, s)), mc-mem (s), 24) ∧ ram-addrp (str, mc-mem (s), n ) ∧ mem-lst (1, str, mc-mem (s), n , lst) ∧ disjoint (sub (32, 4, read-an (32, 6, s)), 24, str, n ) ∧ equal* (read-an (32, 0, s), add (32, str, i* )) ∧ (str = read-dn (32, 2, s)) ∧ (ch = nat-to-uint (read-dn (8, 1, s))) ∧ (i = nat-to-uint (i* )) ∧ (n = nat-to-uint (read-dn (32, 0, s))) ∧ ((i + n) ≤ n ) ∧ (n ≠ 0) ∧ (i* ∈ N) ∧ (n ∈ N) ∧ nat-rangep (i* , 32) ∧ uint-rangep (n , 32))

; from the intial state s to exit: s --> sn.

Theorem: memset-s-sn (memset-statep (s, str, n, lst, ch) ∧ (n = 0)) → ((mc-status (stepn (s, 9)) = 'running)

∧ (mc-pc (stepn (s, 9)) = rts-addr (s)) ∧ (read-dn (32, 0, stepn (s, 9)) = str) ∧ mem-lst (1, str, mc-mem (stepn (s, 9)), n, lst) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 9)))

= add (32, read-an (32, 7, s), 4)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 9))) = read-an (32, 6, s)))

Theorem: memset-s-sn-rfile (memset-statep (s, str, n, lst, ch) ∧ (n = 0) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

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

Theorem: memset-s-sn-mem (memset-statep (s, str, n, lst, ch) ∧ (n = 0) ∧ disjoint (x, k, sub (32, 8, read-sp (s)), 24)) → (read-mem (x, mc-mem (stepn (s, 9)), k) = read-mem (x, mc-mem (s), k))

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

Theorem: memset-s-s0 (memset-statep (s, str, n, lst, ch) ∧ (n ≠ 0)) → memset-s0p (stepn (s, 7), 0, 0, str, n, lst, ch, n)

Theorem: memset-s-s0-else (memset-statep (s, str, n, lst, ch) ∧ (n ≠ 0)) → ((linked-rts-addr (stepn (s, 7)) = rts-addr (s))

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

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

∧ (rn-saved (stepn (s, 7)) = read-rn (32, 2, mc-rfile (s))))

Theorem: memset-s-s0-rfile (memset-statep (s, str, n, lst, ch) ∧ (n ≠ 0) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 7)))

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

Theorem: memset-s-s0-mem (memset-statep (s, str, n, lst, ch) ∧ (n ≠ 0) ∧ disjoint (x, k, sub (32, 8, read-sp (s)), 24)) → (read-mem (x, mc-mem (stepn (s, 7)), k) = read-mem (x, mc-mem (s), k))

; from s0 to exit (base case), from s0 to s0 (induction case).
; base case: s0 --> exit.

Theorem: memset-s0-sn-base (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) = 0)) → ((mc-status (stepn (s, 7)) = 'running)

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

∧ (read-dn (32, 0, stepn (s, 7)) = str)

∧ mem-lst (1, str, mc-mem (stepn (s, 7)), n , put-nth (ch, i, lst)) ∧ (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: memset-s0-sn-rfile-base (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) = 0) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (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: memset-s0-sn-mem-base (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) = 0) ∧ disjoint (x, k, str, n )) → (read-mem (x, mc-mem (stepn (s, 7)), k) = read-mem (x, mc-mem (s), k))

; induction case: s0 --> s0.

Theorem: memset-s0-s0 (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) ≠ 0)) → (memset-s0p (stepn (s, 3),

add (32, i* , 1),

1 + i, str, n − 1, put-nth (ch, i, lst), ch, n )

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

Theorem: memset-s0-s0-rfile (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) ≠ 0) ∧ d3-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 3)))

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

Theorem: memset-s0-s0-mem (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ ((n − 1) ≠ 0) ∧ disjoint (x, k, str, n )) → (read-mem (x, mc-mem (stepn (s, 3)), k) = read-mem (x, mc-mem (s), k))

; put together (s0 --> exit).

Theorem: memset-s0-sn let sn be stepn (s, memset-t1 (n)) in memset-s0p (s, i* , i, str, n, lst, ch, n ) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s))

∧ (read-dn (32, 0, sn) = str)

∧ mem-lst (1, str, mc-mem (sn), n , memset1 (i, n, lst, ch))

∧ (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))) endlet

Theorem: memset-s0-sn-rfile (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ (oplen ≤ 32) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, memset-t1 (n))))

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

Theorem: memset-s0-sn-mem (memset-s0p (s, i* , i, str, n, lst, ch, n ) ∧ disjoint (x, k, str, n )) → (read-mem (x, mc-mem (stepn (s, memset-t1 (n))), k)

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

; the correctness of the MEMSET program.

Theorem: memset-correctness let sn be stepn (s, memset-t (n)) in memset-statep (s, str, n, lst, ch) → ((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, 8, read-sp (s)), 24)

∧ disjoint (x, k, str, n))

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

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

∧ (read-dn (32, 0, sn) = str) ∧ mem-lst (1, str, mc-mem (sn), n, memset (n, lst, ch))) endlet

Event: Disable memset-t.

; some properties of memset.
; see file cstring.events.

Index

add, 3–7

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

equal*, 4 evenp, 3, 4

head, 5, 7

linked-a6, 5–7 linked-rts-addr, 5, 6

mc-mem, 3–7 mc-pc, 3–7 mc-rfile, 4–7 mc-status, 3–7 mcode-addrp, 3, 4 mem-lst, 3–7 memset, 7 memset-code, 2–4 memset-correctness, 7 memset-induct, 3 memset-s-s0, 5 memset-s-s0-else, 5 memset-s-s0-mem, 5 memset-s-s0-rfile, 5 memset-s-sn, 4 memset-s-sn-mem, 4 memset-s-sn-rfile, 4 memset-s0-s0, 6 memset-s0-s0-mem, 6 memset-s0-s0-rfile, 6 memset-s0-sn, 6 memset-s0-sn-base, 5 memset-s0-sn-mem, 7 memset-s0-sn-mem-base, 6 memset-s0-sn-rfile, 7 memset-s0-sn-rfile-base, 5 memset-s0p, 3, 5–7 memset-statep, 3–5, 7 memset-t, 3, 7 memset-t1, 3, 6, 7 memset1, 6

nat-rangep, 4 nat-to-uint, 4

put-nth, 3, 5, 6

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

splus, 3 stepn, 3–7 sub, 3–5, 7

uint-rangep, 4 uread-mem, 3