#|
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 "strcmp" using the compiled version.

;          Proof of the Correctness of the STRCOLL 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 strcoll function in the Berkeley string library.
/*
* Compare strings according to LC_COLLATE category of current locale.
*/
strcoll(s1, s2)
       const char *s1, *s2;
{
       /* LC_COLLATE is unimplemented, hence always "C" */
       return (strcmp(s1, s2));
}

The MC68020 assembly code of the C function strcoll on SUN-3 is given as
follows.  This binary is generated by "gcc -O".
0x2388 <strcoll>:       linkw fp,#0
0x238c <strcoll+4>:     movel fp@(12),sp@-
0x2390 <strcoll+8>:     movel fp@(8),sp@-
0x2394 <strcoll+12>:    jsr @#0x2358 <strcmp>
0x239a <strcoll+18>:    unlk fp
0x239c <strcoll+20>:    rts
The machine code of the above program is:
<strcoll>:    0x4e56  0x0000  0x2f2e  0x000c  0x2f2e  0x0008  0x4eb9  0x0000
<strcoll+16>: 0x2358  0x4e5e  0x4e75
'(78     86      0       0       47      46      0       12
  47     46      0       8       78      185     0       0
  35     88      78      94      78      117)
|#
; in the logic, the above program is defined by (strcoll-code).

Definition: strcoll-code

= '(78 86 0 0 47 46 0 12 47 46 0 8 78 185 -1 -1 -1 -1 78
      94 78 117)

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

∧ (strcoll-addr ∈ N)

∧ nat-rangep (strcoll-addr, 32)

∧ rom-addrp (strcoll-addr, mc-mem (s), 22)

∧ mcode-addrp (strcoll-addr, mc-mem (s), strcoll-code) ∧ strcmp-loadp (s) ∧ (pc-read-mem (add (32, strcoll-addr, 14), mc-mem (s), 4)

= strcmp-addr))

Simultaneously, we introduce the new function symbols strcoll-loadp and strcolladdr.

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

; the computation time of the program.

Definition: strcoll-t (n1 , lst1 , lst2 ) = splus (4, splus (strcmp-t (n1 , lst1 , lst2 ), 2))

; the preconditions of the initial state.

Definition: strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) = ((mc-status (s) = 'running)

∧ strcoll-loadp (s) ∧ (mc-pc (s) = strcoll-addr) ∧ ram-addrp (sub (32, 24, read-sp (s)), mc-mem (s), 36) ∧ ram-addrp (str1 , mc-mem (s), n1 ) ∧ mem-lst (1, str1 , mc-mem (s), n1 , lst1 ) ∧ ram-addrp (str2 , mc-mem (s), n2 ) ∧ mem-lst (1, str2 , mc-mem (s), n2 , lst2 ) ∧ disjoint (sub (32, 24, read-sp (s)), 36, str1 , n1 ) ∧ disjoint (sub (32, 24, read-sp (s)), 36, str2 , n2 ) ∧ (str1 = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (str2 = read-mem (add (32, read-sp (s), 8), mc-mem (s), 4)) ∧ stringp (0, n1 , lst1 ) ∧ (n1 ≤ n2 ) ∧ (n1 ∈ N) ∧ (n2 ∈ N) ∧ uint-rangep (n2 , 32))

; the intermediate state right before the execution of the subroutine strcmp.

Definition: strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) = ((mc-status (s) = 'running)

∧ strcoll-loadp (s) ∧ (mc-pc (s) = strcmp-addr) ∧ (rts-addr (s) = add (32, strcoll-addr, 18)) ∧ ram-addrp (sub (32, 20, read-an (32, 6, s)), mc-mem (s), 36) ∧ ram-addrp (str1 , mc-mem (s), n1 ) ∧ mem-lst (1, str1 , mc-mem (s), n1 , lst1 ) ∧ ram-addrp (str2 , mc-mem (s), n2 ) ∧ mem-lst (1, str2 , mc-mem (s), n2 , lst2 ) ∧ disjoint (sub (32, 20, read-an (32, 6, s)), 36, str1 , n1 ) ∧ disjoint (sub (32, 20, read-an (32, 6, s)), 36, str2 , n2 ) ∧ (str1 = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (str2 = read-mem (add (32, read-sp (s), 8), mc-mem (s), 4)) ∧ equal* (read-sp (s), sub (32, 12, read-an (32, 6, s)))

∧ stringp (0, n1 , lst1 )

∧ (n1 ≤ n2 ) ∧ (n1 ∈ N) ∧ (n2 ∈ N) ∧ uint-rangep (n2 , 32))

; the intermediate state right after the execution of the subroutine strcmp.

Definition: strcoll-s1p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) = ((mc-status (s) = 'running)

∧ strcoll-loadp (s)

∧ (mc-pc (s) = add (32, strcoll-addr, 18))

∧ ram-addrp (sub (32, 20, read-an (32, 6, s)), mc-mem (s), 36)

∧ (iread-dn (32, 0, s) = strcmp (0, n1 , lst1 , lst2 )))

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

Theorem: strcoll-s-s0 strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → strcoll-s0p (stepn (s, 4), str1 , n1 , lst1 , str2 , n2 , lst2 )

Theorem: strcoll-s-s0-else strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → ((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))))

Theorem: strcoll-s-s0-rfile (strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 4)))

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

Theorem: strcoll-s-s0-mem (strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) ∧ disjoint (x, k, sub (32, 24, read-sp (s)), 36)) → (read-mem (x, mc-mem (stepn (s, 4)), k) = read-mem (x, mc-mem (s), k))

; from s0 to s1: s0 --> s1. by strcmp.

Theorem: strcoll-s0p-strcmp-statep strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → strcmp-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 )

Theorem: strcoll-s0-s1 let s1 be stepn (s, strcmp-t (n1 , lst1 , lst2 )) in strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → strcoll-s1p (s1 , str1 , n1 , lst1 , str2 , n2 , lst2 ) endlet

Theorem: strcoll-s0-s1-else let s1 be stepn (s, strcmp-t (n1 , lst1 , lst2 )) in strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → ((read-rn (32, 14, mc-rfile (s1 ))

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

∧ (linked-rts-addr (s1 ) = linked-rts-addr (s)) ∧ (linked-a6 (s1 ) = linked-a6 (s))) endlet

Theorem: strcoll-s0-s1-rfile let s1 be stepn (s, strcmp-t (n1 , lst1 , lst2 )) in (strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (s1 ))

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

Theorem: strcoll-s0-s1-mem let s1 be stepn (s, strcmp-t (n1 , lst1 , lst2 )) in (strcoll-s0p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) ∧ disjoint (x, k, sub (32, 20, read-an (32, 6, s)), 36)) → (read-mem (x, mc-mem (s1 ), k) = read-mem (x, mc-mem (s), k)) endlet

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

Theorem: strcoll-s1-sn strcoll-s1p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → ((mc-status (stepn (s, 2)) = 'running)

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

∧ (iread-dn (32, 0, stepn (s, 2)) = strcmp (0, n1 , lst1 , lst2 )) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 2))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 2))) = add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 2)), k) = read-mem (x, mc-mem (s), k)))

Theorem: strcoll-s1-sn-rfile (strcoll-s1p (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) ∧ d2-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 2)))

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

; the correctness of strcoll.

Theorem: strcoll-correctness let sn be stepn (s, strcoll-t (n1 , lst1 , lst2 )) in strcoll-statep (s, str1 , n1 , lst1 , str2 , n2 , lst2 ) → ((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, 24, read-sp (s)), 36)

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

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

∧ (iread-dn (32, 0, sn) = strcoll (n1 , lst1 , lst2 ))) endlet

Event: Disable strcoll-t.

; some properties of strcoll.
; the same as strcmp.

Index

add, 2–6

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

equal*, 3 evenp, 2

iread-dn, 4–6

linked-a6, 4, 5 linked-rts-addr, 4, 5

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

nat-rangep, 2

pc-read-mem, 2

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

splus, 3 stepn, 2, 4–6 stepn-strcoll-loadp, 2 strcmp, 4, 5 strcmp-addr, 2, 3 strcmp-loadp, 2 strcmp-statep, 4 strcmp-t, 3, 5 strcoll, 6 strcoll-addr, 2–4 strcoll-code, 2 strcoll-correctness, 6 strcoll-load, 2 strcoll-loadp, 2–4 strcoll-s-s0, 4 strcoll-s-s0-else, 4 strcoll-s-s0-mem, 4 strcoll-s-s0-rfile, 4 strcoll-s0-s1, 5 strcoll-s0-s1-else, 5 strcoll-s0-s1-mem, 5 strcoll-s0-s1-rfile, 5 strcoll-s0p, 3–5 strcoll-s0p-strcmp-statep, 4 strcoll-s1-sn, 5 strcoll-s1-sn-rfile, 6 strcoll-s1p, 4–6 strcoll-statep, 3, 4, 6 strcoll-t, 3, 6 stringp, 3, 4 sub, 3–6

uint-rangep, 3, 4