From: Christoph Fuerst Date: Fri, 14 Apr 2017 17:03:54 +0000 (+0200) Subject: Readability, no functional changes X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=4db5c1f52d6e8c94ec09af727257a1707fe62eb0;p=cfuerst%2Fformal-numbers.git Readability, no functional changes --- diff --git a/discrete_log.txt b/discrete_log.txt index e92aa12..2db452e 100644 --- a/discrete_log.txt +++ b/discrete_log.txt @@ -9,9 +9,7 @@ type prime = ℕ[K]; type res = ℕ[L]; pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n; - pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m); - pred isComposite(m:prime) ⇔ ¬isPrime(m); proc InvModP(a:ℕ[K^2],p:prime): prime @@ -26,7 +24,6 @@ proc InvModP(a:ℕ[K^2],p:prime): prime decreases p-i; if a*i % p = 1 then // straight search ainv = i; // algorithmic alternative: Euclidean algorithm - return ainv; } @@ -44,7 +41,6 @@ proc IntegerRoot(a:nat): nat z=z+2; y=y+z; } - return x; } @@ -63,8 +59,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res var gi:prime = InvModP(g,p); var solFound:Bool := false; - A[0] := 1; - b[0] := a; + A[0] := 1; b[0] := a; for var i:nat=1;i<=m;i=i+1 do decreases m+1-i; @@ -81,14 +76,12 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res { if A[j] = b[i] then { - // result found ret = i*m + j; solFound = true; } } b[i+1] = b[i]*gim % p; // Giant-Step } - return ret; } diff --git a/report/formal.pdf b/report/formal.pdf index 600a46b..a7d5b0a 100644 Binary files a/report/formal.pdf and b/report/formal.pdf differ diff --git a/report/formal.tex b/report/formal.tex index 4bea1c0..4c0cc8c 100644 --- a/report/formal.tex +++ b/report/formal.tex @@ -253,7 +253,7 @@ The algorithm proceeds by first compiling a table with entries $(i,t_i)$ where $ (computed by repeated multiplying modulo $p$). The table consists of $m := \lceil \sqrt{p-1}\,\rceil$ entries from 0 to $m-1$. In the next step, one computes $g^{-m}\pmod p$. Initialize an index $i$ with zero. -If $a_i$ happens to coincide with some $t_j$ where $0\leq j\leq m-1$, then the +If $a_i$ happens to coincide with some $t_j$ where $0\leq j\leq m-1$, then the algorithm terminates with $x=i\cdot m + j$, otherwise it computes $a_{i+1} = a_i g^{-m}\pmod p$. An implementation of this algorithm in \CC\, might be written as follows: {\tiny \lstinputlisting{../src/discrete_log.cpp}} @@ -440,7 +440,7 @@ Some comments on the formalization: \item The first argument is the characteristic of the finite field, which is a prime. Below 10, the primes are 2,3,5,7. Obviously, for $p=2$ we have no elements of order $p-1$; - \item The condition that $g$ has to be of order $p-1$ is a major restriction. + \item The condition that $g$ has to be of order $p-1$ is a major restriction. The only elements that satisfy this are given by \end{itemize} \begin{center} @@ -451,8 +451,8 @@ $p$ & Elements of order $p-1$\\ 3 & 2 \\ 5 & 2,3\\ 7 & 3,5\\ -\hline -\end{tabular} +\hline +\end{tabular} \end{center} \begin{itemize} \item The element $a$ has obviously to be non-zero in $\mathbb{Z}_p$. @@ -465,13 +465,33 @@ are in our scope might be explictly enumerated by $(p,g,a)$\\ \hline $(3,2,1)$, $(3,2,2)$\\ -$(5,2,1)$,$(5,2,2)$,$(5,2,3)$,$(5,2,4)$\\ +$(5,2,1)$,$(5,2,2)$,$(5,2,3)$,$(5,2,4)$\\ $(5,3,1)$, $(5,3,2)$, $(5,3,3)$, $(5,3,4)$\\ $(7,3,1)$, $(7,3,2)$, $(7,3,3)$, $(7,3,4)$, $(7,3,5)$, $(7,3,6)$ \\ -$(7,5,1)$, $(7,5,2)$, $(7,5,3)$, $(7,5,4)$, $(7,5,5)$, $(7,5,6)$ -\end{tabular} +$(7,5,1)$, $(7,5,2)$, $(7,5,3)$, $(7,5,4)$, $(7,5,5)$, $(7,5,6)$ +\end{tabular} \end{center} which gives a total of 22 elements to check. + +\subsection{Prime Number Generation} +A classic algorithm for generating prime-numbers less equal a given number, is the Sieve of Erathostenes. +Suppose, we want to produce a list of all primes less equal $m$, the algorithm proceeds by enumerating +all integers from 2 to $m$, we set $S^{(0)}:=\{2,\ldots,m\}$. The first prime, is obviously given by 2, i.e. +the minimal element of the set $S^{(0)}$. Of course, any number greater and divisible by 2 is not prime, +hence, we remove the \emph{even} elements from the set $S^{(0)}$ to obtain the set $S^{(1)}$. The next prime +number is the least number of the updated set $S^{(1)}$, i.e. 3. We remove all multiples of 3 to obtain +$S^{(2)}$. Proceedings likewise, up to $\sqrt{m}$, by selecting the minimal element $p$ (which is prime) +of $S^{(k)}$ and updating $S^{(k)}$ to $S^{(k+1)}$, that is, removing all multiples of $p$, we obtain a list +of primes less equal $m$.\\ + +We formalize this algorithm in two ways. While the first formalization treats the numbers 2..$m$ as boolean +array, we can for the second formalization the data structure of sets (that corresponds to sets in the +mathematical sense). Obviously, we should obtain the same results. + +\subsection*{The RISCAL Formalization} +{\scriptsize \verbatimboxed{../sieveEratosthenes.txt}} + + \appendix diff --git a/sieveEratosthenes.txt b/sieveEratosthenes.txt index 0ae53d4..11a16ce 100644 --- a/sieveEratosthenes.txt +++ b/sieveEratosthenes.txt @@ -6,7 +6,6 @@ pred divides(m:nat,n:nat) ⇔ ∃p:nat. m⋅p = n; pred isPrime(m:nat) ⇔ (m = 0) ∨ (m=1) ∨ (1 < m ∧ ∀n:nat. divides(n,m) ⇒ (n≤1 ∨ n=m)); - proc IntegerRoot(a:nat): nat ensures result^2 ≤ a ∧ a < (result+1)^2; { @@ -21,7 +20,6 @@ proc IntegerRoot(a:nat): nat z=z+2; y=y+z; } - return x; } @@ -38,14 +36,14 @@ proc SieveOfErathostenes(m:nat): Array[MAX,Bool] for i=2; i≤IntegerRoot(m); i=i+1 do decreases IntegerRoot(m)+1-i; { - if ret[i] = true then - { - for k=0;i^2+k*i