From: Christoph Fuerst Date: Sun, 2 Apr 2017 18:37:32 +0000 (+0200) Subject: Divided into seperate files X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=80c3bb9e9695ef6fae0d95a474bbf1fbe2bc3329;p=cfuerst%2Fformal-numbers.git Divided into seperate files --- diff --git a/integerroot.txt b/integerroot.txt new file mode 100644 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 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 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 --- 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}