\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 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
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|

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:
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2-code} \\  
\=\+{\sc{log2-code}}\index{log2-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{128}} \\ 
{\tt{108}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{116}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{109}}{\tt{ }}{\tt{240}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{36}} \\ 
{\tt{46}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{252}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{verbatim}; we define the Nqthm counterpart of log2.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2} \\  
\=\+{\rm{log2}}\,({\it{n\/}}, {\it{log2\/}})\index{log2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{1}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{log2}}\,({\it{n\/}} $\div$ {\tt{2}}, $1\;+$ {\it{log2\/}})\index{log2} \\ 
{\bf else }{\it{log2\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the clock.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2-t0} \\  
\=\+{\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{1}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{splus}}\,({\tt{7}}, {\rm{log2-t0}}\,({\it{n\/}} $\div$ {\tt{2}})\index{log2-t0})\index{splus} \\ 
{\bf else }{\tt{7}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{log2-t}$\;\;$
{\rm{log2-t}}\,({\it{n\/}})\index{log2-t} $=$ {\rm{splus}}\,({\tt{5}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{splus}
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2-induct} \\  
\=\+{\rm{log2-induct}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{1}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{log2-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn}, {\it{n\/}} $\div$ {\tt{2}}, $1\;+$ {\it{log2\/}})\index{log2-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the preconditions on the initail state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2-statep} \\  
\=\+{\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{40}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{log2-code}}\index{log2-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{log2-s0p} \\  
\=\+{\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{40}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{log2-code}}\index{log2-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{log2\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\it{log2\/}} $+$ {\it{n\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{log2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; from the initial state to s0:  s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-s-s0 \\ \index{log2-s-s0}
{\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} $\rightarrow$ {\rm{log2-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\it{n\/}}, {\tt{0}})\index{log2-s0p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s-s0-else \\ \index{log2-s-s0-else}
\=\+{\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{rn-saved} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s-s0-rfile \\ \index{log2-s-s0-rfile}
\=\+({\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} $\wedge$ {\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s-s0-mem \\ \index{log2-s-s0-mem}
\=\+({\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; s0 --> exit.
; base case: s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-s0-sn-base \\ \index{log2-s0-sn-base}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ ({\tt{1}} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{iread-dn} $=$ {\it{log2\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s0-sn-base-rfile \\ \index{log2-s0-sn-base-rfile}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ ({\tt{1}} $\not<$ {\it{n\/}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s0s-n-base-mem \\ \index{log2-s0s-n-base-mem}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ ({\tt{1}} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; induction case: s0 --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-rangep-la \\ \index{log2-rangep-la}
\=\+({\rm{int-rangep}}\,({\it{m\/}} $+$ {\it{n\/}}, {\tt{32}})\index{int-rangep} $\wedge$ ({\tt{1}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{int-rangep}}\,($1\;+$ ({\it{m\/}} $+$ ({\it{n\/}} $\div$ {\tt{2}})), {\tt{32}})\index{int-rangep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s0-s0 \\ \index{log2-s0-s0}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ ({\tt{1}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{log2-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn}, {\it{n\/}} $\div$ {\tt{2}}, $1\;+$ {\it{log2\/}})\index{log2-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s0-s0-rfile \\ \index{log2-s0-s0-rfile}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ ({\tt{1}} $<$ {\it{n\/}}) $\wedge$ {\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; put together.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-s0-sn \\ \index{log2-s0-sn}
\=\+{\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{iread-dn} $=$ {\rm{log2}}\,({\it{n\/}}, {\it{log2\/}})\index{log2}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-s0-sn-rfile \\ \index{log2-s0-sn-rfile}
\=\+({\rm{log2-s0p}}\,({\it{s\/}}, {\it{n\/}}, {\it{log2\/}})\index{log2-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t0}}\,({\it{n\/}})\index{log2-t0})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d3-7a2-5p}}\,({\it{rn\/}})\index{d3-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; correctness.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-correct \\ \index{log2-correct}
\=\+{\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{iread-dn} $=$ {\rm{log2}}\,({\it{n\/}}, {\tt{0}})\index{log2}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{read-an} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-rfile \\ \index{log2-rfile}
\=\+({\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log2-mem \\ \index{log2-mem}
\=\+({\rm{log2-statep}}\,({\it{s\/}}, {\it{n\/}})\index{log2-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{log2-t}}\,({\it{n\/}})\index{log2-t})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; the correctness of the Nqthm function log2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-log \\ \index{log2-log}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{log2}}\,({\it{n\/}}, {\it{i\/}})\index{log2} $=$ ({\it{i\/}} $+$ {\rm{log}}\,({\tt{2}}, {\it{n\/}})\index{log}))
\end{tabbing}

\begin{verbatim}; 2^log2(n) <= n.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-thm1 \\ \index{log2-thm1}
({\tt{1}} $<$ {\it{n\/}}) $\rightarrow$ ({\it{n\/}} $\not<$ {\rm{exp}}\,({\tt{2}}, {\rm{log2}}\,({\it{n\/}}, {\tt{0}})\index{log2})\index{exp})
\end{tabbing}

\begin{verbatim}; n < 2^(log2(n)+1).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  log2-thm2 \\ \index{log2-thm2}
{\it{n\/}} $<$ {\rm{exp}}\,({\tt{2}}, $1\;+$ {\rm{log2}}\,({\it{n\/}}, {\tt{0}})\index{log2})\index{exp}
\end{tabbing}

%\end{list}
\printindex
\end{document}
