\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 the ISQRT 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 ISQRT computes the integer square root of a given 
nonnegative integer i.

/* computes the integer square root of a given nonnegative integer */
isqrt(int i)
{
  int j;

  j = (i / 2);
  while ((i / j) < j) 
    j = (j + (i / j)) / 2;
  return (j);
}

Here is the MC68020 assembly code of the above ISQRT program.  The code is
generated by "gcc -O".

The program expects an nonnegative integer input which is on the sp
stack at address (sp)+4.  The local variable j is assigned to d2.  The
program exits with the answer in register d0 and the program counter
equals the return address saved on the sp stack at address (sp).

0x2318 <isqrt>: 	linkw a6,#0
0x231c <isqrt+4>:	movel d2,sp@-
0x231e <isqrt+6>:	movel a6@(8),d1
0x2322 <isqrt+10>:	movel d1,d2
0x2324 <isqrt+12>:	bra 0x232e <isqrt+22>
0x2326 <isqrt+14>:	movel d2,d0
0x2328 <isqrt+16>:	divsll d1,d0,d0
0x232c <isqrt+20>:	addl d0,d1
0x232e <isqrt+22>:	tstl d1
0x2330 <isqrt+24>:	bge 0x2334 <isqrt+28>
0x2332 <isqrt+26>:	addql #1,d1
0x2334 <isqrt+28>:	asrl #1,d1
0x2336 <isqrt+30>:	movel d2,d0
0x2338 <isqrt+32>:	divsll d1,d0,d0
0x233c <isqrt+36>:	cmpl d0,d1
0x233e <isqrt+38>:	bgt 0x2326 <isqrt+14>
0x2340 <isqrt+40>:	movel d1,d0
0x2342 <isqrt+42>:	movel a6@(-4),d2
0x2346 <isqrt+46>:	unlk a6
0x2348 <isqrt+48>:	rts

The machine code of the above program is:

<isqrt>:	0x4e56	0x0000	0x2f02	0x222e	0x0008	0x2401	0x6008	0x2002
<isqrt+16>:	0x4c41	0x0800	0xd280	0x4a81	0x6c02	0x5281	0xe281	0x2002
<isqrt+32>:	0x4c41	0x0800	0xb280	0x6ee6	0x2001	0x242e	0xfffc	0x4e5e
<isqrt+48>:	0x4e75

In the logic, it is going to be a list like:

'(78      86      0       0       47      2       34      46
  0       8       36      1       96      8       32      2
  76      65      8       0       210     128     74      129
  108     2       82      129     226     129     32      2
  76      65      8       0       178     128     110     230
  32      1       36      46      255     252     78      94
  78      117)
|#

; in the logic, the program is defined by (isqrt-code).	     
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-code} \\  
\=\+{\sc{isqrt-code}}\index{isqrt-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{65}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{0}} \\ 
{\tt{210}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{65}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{0}} \\ 
{\tt{178}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{230}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{252}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mean-lessp-1 \\ \index{mean-lessp-1}
((({\it{b\/}} $+$ {\it{a\/}}) $\div$ {\tt{2}}) $<$ {\it{b\/}}) $=$ ({\it{a\/}} $<$ {\it{b\/}})
\end{tabbing}

\begin{verbatim}; isqrt1 is a function in the Logic simulating the loop of the above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt1} \\  
\=\+{\rm{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{i\/}}) \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}$\;\;${\bf then }{\rm{isqrt1}}\,({\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt1} \\ 
{\bf else }{\rm{fix}}\,({\it{j\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; isqrt is a function in the Logic simulating the above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt}$\;\;$
{\rm{isqrt}}\,({\it{i\/}})\index{isqrt} $=$ {\rm{isqrt1}}\,({\it{i\/}}, {\it{i\/}} $\div$ {\tt{2}})\index{isqrt1}
\end{tabbing}

\begin{verbatim}; the computation time of the loop.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt1-t} \\  
\=\+{\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}} \\ 
{\bf then }{\rm{splus}}\,({\tt{10}}, {\rm{isqrt1-t}}\,({\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt1-t})\index{splus} \\ 
{\bf else }{\tt{8}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{isqrt-t}$\;\;$
{\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t} $=$ {\rm{splus}}\,({\tt{8}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{i\/}} $\div$ {\tt{2}})\index{isqrt1-t})\index{splus}
\end{tabbing}


\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Enable integerp.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iquotient.

\addvspace{18pt}

\noindent{\sc Event}:   Enable ilessp.

\addvspace{18pt}


\noindent{\sc Event}:   Disable remainder.

\addvspace{18pt}

\noindent{\sc Event}:   Disable quotient.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  isqrt-no-overflow \\ \index{isqrt-no-overflow}
\=\+({\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\it{n\/}})\index{int-rangep} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{int-rangep}}\,({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}}), {\it{n\/}})\index{int-rangep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  j-nonzerop \\ \index{j-nonzerop}
(({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ({\tt{0}} $<$ {\it{j\/}})) $\rightarrow$ ((({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}) $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  j-int-rangep \\ \index{j-int-rangep}
\=\+({\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\it{n\/}})\index{int-rangep} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ (({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}}), {\it{n\/}})\index{int-rangep}\-
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isqrt-induct} \\  
\=\+{\rm{isqrt-induct}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}} \\ 
{\bf then }{\rm{isqrt-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{isqrt-statep} \\  
\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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{50}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{isqrt-code}}\index{isqrt-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{i\/}} $=$ {\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$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{isqrt-s0p} \\  
\=\+{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-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{30}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{50}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{30}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{isqrt-code}}\index{isqrt-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{i\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;${\rm{int-rangep}}\,({\tt{2}} $*$ {\it{j\/}}, {\tt{32}})\index{int-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp})\-\-
\end{tabbing}

\begin{verbatim}; from the initial state to s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  initial-j-int-rangep \\ \index{initial-j-int-rangep}
{\rm{int-rangep}}\,({\it{i\/}}, {\it{n\/}})\index{int-rangep} $\rightarrow$ {\rm{int-rangep}}\,({\tt{2}} $*$ ({\it{i\/}} $\div$ {\tt{2}}), {\it{n\/}})\index{int-rangep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s-s0 \\ \index{isqrt-s-s0}
\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{isqrt-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{i\/}}, {\it{i\/}} $\div$ {\tt{2}})\index{isqrt-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{8}})\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{8}})\index{stepn})\index{rn-saved} $=$ {\rm{read-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-dn}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt-s-s0-rfile \\ \index{isqrt-s-s0-rfile}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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{8}})\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}:  isqrt-s-s0-mem \\ \index{isqrt-s-s0-mem}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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{8}})\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}; from s0 to s0 (induction csae), or from s0 to exit (base case).
; base case:
; the basics we need to prove: 
;   0. the machine is still running.
;   1. the pc is at the right position.
;   2. d0 contains the local variable j, the computing square root.
;   3. a6 should have the right value.
;   4. sp(a7) should have the right value.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-sn \\ \index{isqrt-s0-sn}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{8}})\index{stepn})\index{iread-dn} $=$ {\it{j\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{8}})\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{verbatim}; 5. d2, which is used by this program, should be restored.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-sn-d2 \\ \index{isqrt-s0-sn-d2}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}}) $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-rn}}\,({\it{oplen\/}}, {\tt{2}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head})\-
\end{tabbing}

\begin{verbatim}; and 6. those registers untouched by this program should still
; have their original contents.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-sn-rfile \\ \index{isqrt-s0-sn-rfile}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}}) $\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{8}})\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}; and 7. the memory is correctly changed.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt1-s0-sn-mem \\ \index{isqrt1-s0-sn-mem}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $\not<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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}:  isqrt-s0p-j\_nonzerop \\ \index{isqrt-s0p-j\_nonzerop}
{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\rightarrow$ (({\it{j\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{j\/}} $\in\;${\bf{N}}${}$))
\end{tabbing}

\begin{verbatim}; induction case: s0 --> s0.
; we need to prove:
;  0. the state predicate at s0 is still satisfied.
;  1. a6 is unchanged.
;  2. the content of original a6 on the sp stack is not changed.
;  3. the return address on the sp atack is not changed.
;  4. the content of original d2 on the sp stack is not changed.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0 \\ \index{isqrt-s0-s0}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{isqrt-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn}, {\it{i\/}}, ({\it{j\/}} $+$ ({\it{i\/}} $\div$ {\it{j\/}})) $\div$ {\tt{2}})\index{isqrt-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\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{10}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\index{stepn})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-
\end{tabbing}

\begin{verbatim}; and 5. the registers that are not modified by this program still have
; their previous values.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0-rfile \\ \index{isqrt-s0-s0-rfile}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}}) $\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{10}})\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}; and 6. the memory is correctly changed.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-s0-s0-mem \\ \index{isqrt-s0-s0-mem}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ (({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{10}})\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}


\noindent{\sc Event}:   Disable isqrt-statep.

\addvspace{18pt}

\noindent{\sc Event}:   Disable isqrt-s0p.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  isqrt1-correctness \\ \index{isqrt1-correctness}
\=\+{\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\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{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\index{stepn})\index{iread-dn} $=$ {\rm{isqrt1}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\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{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\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{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-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{tabbing}{\sc Theorem}:  isqrt1-d2 \\ \index{isqrt1-d2}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{2}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  isqrt1-rfile \\ \index{isqrt1-rfile}
\=\+({\rm{isqrt-s0p}}\,({\it{s\/}}, {\it{i\/}}, {\it{j\/}})\index{isqrt-s0p} $\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\/}}, {\rm{isqrt1-t}}\,({\it{i\/}}, {\it{j\/}})\index{isqrt1-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{verbatim}; after an execution of this program,  the machine state satisfies:
;  0. normal exit.
;  1. the pc is returned to the next instruction of the caller.
;  2. the result -- ISQRT(i), is stored in D0.
;  3. a6, used by LINK, is restored to its original content.
;  4. the stack pointer sp(a7) is updated correctly to pop off one frame.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-correctness \\ \index{isqrt-correctness}
\=\+{\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-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{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})\index{stepn})\index{iread-dn} $=$ {\rm{isqrt}}\,({\it{i\/}})\index{isqrt}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-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{isqrt-t}}\,({\it{i\/}})\index{isqrt-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{verbatim};  5. d2, used for local variable j, is restored to its original value.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-d2 \\ \index{isqrt-d2}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-statep} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{2}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-dn}}\,({\it{oplen\/}}, {\tt{2}}, {\it{s\/}})\index{read-dn})\-\-
\end{tabbing}
	      
\begin{verbatim}; and 6. the registers that are not modified by this program still have
; their original values.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-rfile \\ \index{isqrt-rfile}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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\/}}, {\rm{isqrt-t}}\,({\it{i\/}})\index{isqrt-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{verbatim}; and 7. the memory is correctly changed.  i.e. specify clearly the portions
; of the memory were changed and prove that is a truth.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  isqrt-read-mem \\ \index{isqrt-read-mem}
\=\+({\rm{isqrt-statep}}\,({\it{s\/}}, {\it{i\/}})\index{isqrt-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{isqrt-t}}\,({\it{i\/}})\index{isqrt-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}


\noindent{\sc Event}:   Disable isqrt-t.

\addvspace{18pt}

\begin{verbatim}#|
; we next need to prove that isqrt does compute the integer square root.
; the following is the same as the proof in the file isqrt-ada.events.
(defn sq (j)
  (times j j))

(prove-lemma isqrt1-lower-bound (rewrite)
     (implies (not (zerop j))
	      (not (lessp i (sq (isqrt1 i j))))))

(prove-lemma quotient-by-2 (rewrite)
     (not (lessp (plus (quotient x 2) (quotient x 2))
		 (sub1 x))))

(prove-lemma main-trick (rewrite)
     (not (lessp (sq (add1 (quotient (plus j k) 2)))
		 (plus (times j k) j)))
     ((induct (difference j k))))

(prove-lemma sq-add1-non-zero (rewrite)
     (not (equal (sq (add1 x)) 0)))

(prove-lemma main (rewrite)
     (implies (not (zerop j))
	      (lessp i 
		     (sq (add1 (quotient (plus j (quotient i j)) 2)))))
     ((disable sq)))

(prove-lemma isqrt1-upper-bound (rewrite)
     (implies (lessp i (sq (add1 j)))
	      (lessp i (sq (add1 (isqrt1 i j)))))
     ((disable sq)))

(prove-lemma isqrt->isqrt1 (rewrite)
   (implies (lessp 1 i)
	    (lessp i (sq (add1 (quotient i 2))))))

; (isqrt i) is the square root of i:  (isqrt i)^2 <= i < [(isqrt i)+1]^2.
(prove-lemma isqrt-logic-correctness ()
     (implies (lessp 1 i)
	      (and (lessp i (sq (add1 (isqrt i))))
		   (not (lessp i (sq (isqrt i))))))
     ((disable sq isqrt1)))

|#
\end{verbatim}
%\end{list}
\printindex
\end{document}
