Divided into seperate files

diff --git a/integerroot.txt b/integerroot.txt
new file mode 100644 (file)
index 0000000..e372df0
--- /dev/null
+++ b/integerroot.txt
@@ -0,0 +1,29 @@
+//
+// Computing the Integer-Square-Root of a non-negative integer a
+// Author: Christoph Fuerst (2017)
+
+val K: ℕ;
+
+type nat     = ℕ[K];
+
+////////////////////////////////////////////////////////////////////
+// Algorithm: Integer-Square-Root
+////////////////////////////////////////////////////////////////////
+proc integerroot(a:nat): nat
+   ensures result^2 ≤ a ∧ a < (result+1)^2;
+{
+   var x:nat = 0;
+   var y:ℕ[(K+1)^2] = 1;
+   var z:ℕ[(K+1)^2] = 1;
+
+   while y ≤ a do
+      invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
+   {
+      x=x+1;
+      z=z+2;
+      y=y+z;
+   }
+
+   return x;
+}
+

diff --git a/lefttoright.txt b/lefttoright.txt
new file mode 100644 (file)
index 0000000..285ec7b
--- /dev/null
+++ b/lefttoright.txt
@@ -0,0 +1,40 @@
+//
+// Computing Powers by Left-To-Right Exponentation
+// Author: Christoph Fuerst (2017)
+
+val N: ℕ;
+val M: ℕ;
+
+type Base    = ℕ[N];
+type Exp     = ℕ[M];
+type Result  = ℕ[N^M];
+
+////////////////////////////////////////////////////////////////////
+// Algorithm: Calculate x^n by Left-To-Right Exponentation
+////////////////////////////////////////////////////////////////////
+proc LeftToRightExponentation(x:Base,n:Exp): Result
+   ensures result = x^n;
+{
+   var res:Result = 1; 
+   var locn:Exp = n;
+   var locx:ℕ[N^(2*M)] = x;
+     while locn > 0 do
+        invariant (n ≥ locn) ∧ (locn ≥ 0) ∧ 
+                  (x^n = res*(locx^locn)) ∧
+                  (old_locx ≤ locx) ∧
+                  (res = 0 ∨ old_res ≤ res) ∧
+                  (((locn%2 = 1) ⇒ (old_res < res)) ∨ 
+                   ((locn%2 = 0) ⇒ (old_res = res))); 
+        decreases locn;
+        {
+          if locn%2 = 1 then
+          {
+             res = locx*res;
+          }
+          locx = locx^2;
+          locn = locn/2;
+        }
+   return res;
+}
+
+

diff --git a/report/formal.pdf b/report/formal.pdf
index 8af4496..a3781aa 100644 (file)
Binary files a/report/formal.pdf and b/report/formal.pdf differ

diff --git a/report/formal.tex b/report/formal.tex
index ac8c8bf..de6e576 100644 (file)
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -28,6 +28,16 @@
 \renewcommand{\thesection}{\arabic{section}}
 \renewcommand{\thealgorithm}{\arabic{section}.\arabic{algorithm}}
 
+\def\verbatimboxed#1{\begingroup
+\def\verbatim@processline{%
+{\setbox0=\hbox{\the\verbatim@line}%
+\hsize=\wd0
+\the\verbatim@line\par}}%
+\setbox0=\vbox{\parskip=0pt\topsep=0pt\partopsep=0pt
+\verbatiminput{#1}}%
+\begin{center}\fbox{\box0}\end{center}%
+\endgroup}
+
 %opening
 \title{Formal Verification of Algorithms arising in Cryptography}
 \author{Christoph F\"urst\qquad Wolfgang Schreiner\\ Research Institute for Symbolic Computation (RISC) Linz}
@@ -320,10 +330,13 @@ y \leq y' \text{ and }
         n \text{ is odd } &\Rightarrow y < y',\\
         n \text{ is even }&\Rightarrow y = y',
 \end{cases}
-\qquad \text{and further } x < x' = x^2.
+\qquad \text{and further } x \leq x' = x^2.
 $$
 The termination of the loop is a consequence of $\lfloor n/2^k\rfloor \rightarrow 0$ after
 finitely many steps, i.e. there exists $k\in\mathbb{N}$ such that $\lfloor n/2^k\rfloor = 0$.
+\newpage
+\subsection{The RISCAL Formalization}
+{\scriptsize \verbatimboxed{../lefttoright.txt}}
 
 \subsection{Computing Integer Roots}
 Given a number $x\in\mathbb{R}^+$, the \emph{square-root} $y := \sqrt{x}\in\mathbb{R}$ is implicit
@@ -376,35 +389,36 @@ $$
 y > a \Leftrightarrow (x^2+z) > a \Leftrightarrow x^2+2x+1 > a \Leftrightarrow (x+1)^2 > a,
 $$
 hence we have shown $x^2\leq a < (x+1)^2$, and taking square roots shows the claim.
+\newpage
+\subsection{The RISCAL Formalization}
+%{\scriptsize \verbatiminput{../integerroot.txt}}
+{\scriptsize \verbatimboxed{../integerroot.txt}}
 \appendix
-\section{Listing of the developed Theory}
-{\scriptsize \verbatiminput{../numbertheory.txt}}
-
-
-\section{Listing of Implementations}
-\lstset{language=C++,
-    backgroundcolor=\color{black!5}, % set backgroundcolor
-    basicstyle=\ttfamily\tiny,% basic font setting
- breakatwhitespace=false,         % sets if automatic breaks should only happen at whitespace
-  breaklines=true,                 % sets automatic line breaking
-   captionpos=b,                    % sets the caption-position to bottom
-   deletekeywords={...},            % if you want to delete keywords from the given language
-  escapeinside={\%*}{*)},          % if you want to add LaTeX within your code
-  extendedchars=true,              % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
-  frame=single,                           % adds a frame around the code
-  keepspaces=true,                 % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
-  language=Octave,                 % the language of the code
-  morekeywords={*,...},           % if you want to add more keywords to the set
-  numbers=left,                    % where to put the line-numbers; possible values are (none, left, right)
-  numbersep=5pt,                   % how far the line-numbers are from the code
-  showspaces=false,                % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
-  showstringspaces=false,          % underline spaces within strings only
-  showtabs=false,                  % show tabs within strings adding particular underscores
-  stepnumber=1,                  % the step between two line-numbers. If it's 1, each line will be numbered
-  tabsize=2,                      % sets default tabsize to 2 spaces
-}
-
-{\tiny \lstinputlisting{../src/primefactors.cpp}}
+
+% \section{Listing of Implementations}
+% \lstset{language=C++,
+%     backgroundcolor=\color{black!5}, % set backgroundcolor
+%     basicstyle=\ttfamily\tiny,% basic font setting
+%  breakatwhitespace=false,         % sets if automatic breaks should only happen at whitespace
+%   breaklines=true,                 % sets automatic line breaking
+%    captionpos=b,                    % sets the caption-position to bottom
+%    deletekeywords={...},            % if you want to delete keywords from the given language
+%   escapeinside={\%*}{*)},          % if you want to add LaTeX within your code
+%   extendedchars=true,              % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
+%   frame=single,                         % adds a frame around the code
+%   keepspaces=true,                 % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
+%   language=Octave,                 % the language of the code
+%   morekeywords={*,...},           % if you want to add more keywords to the set
+%   numbers=left,                    % where to put the line-numbers; possible values are (none, left, right)
+%   numbersep=5pt,                   % how far the line-numbers are from the code
+%   showspaces=false,                % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
+%   showstringspaces=false,          % underline spaces within strings only
+%   showtabs=false,                  % show tabs within strings adding particular underscores
+%   stepnumber=1,                  % the step between two line-numbers. If it's 1, each line will be numbered
+%   tabsize=2,                    % sets default tabsize to 2 spaces
+% }
+% 
+% {\tiny \lstinputlisting{../src/primefactors.cpp}}
 
 \begin{thebibliography}{9}
 \bibitem{hardylittlewood}