From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Mon, 3 Apr 2017 18:46:28 +0000 (+0200)
Subject: Corrected wrong invariant of LeftToRight, Updated Report, Implemented Algorithm for... 
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=27f6b3d7dd540826eb977494fd291fa790d62b46;p=cfuerst%2Fformal-numbers.git

Corrected wrong invariant of LeftToRight, Updated Report, Implemented Algorithm for Discrete Log
---

diff --git a/lefttoright.txt b/lefttoright.txt
index 285ec7b..73fce20 100644
--- a/lefttoright.txt
+++ b/lefttoright.txt
@@ -20,11 +20,7 @@ proc LeftToRightExponentation(x:Base,n:Exp): Result
    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))); 
+                  (x^n = res*(locx^locn)); 
         decreases locn;
         {
           if locn%2 = 1 then
@@ -38,3 +34,4 @@ proc LeftToRightExponentation(x:Base,n:Exp): Result
 }
 
 
+
diff --git a/report/formal.pdf b/report/formal.pdf
index 8974510..7a15370 100644
Binary files a/report/formal.pdf and b/report/formal.pdf differ
diff --git a/report/formal.tex b/report/formal.tex
index ab315e5..23ee95d 100644
--- a/report/formal.tex
+++ b/report/formal.tex
@@ -335,7 +335,7 @@ $$
 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}
+\subsection*{The RISCAL Formalization}
 {\scriptsize \verbatimboxed{../lefttoright.txt}}
 
 \subsection{Computing Integer Roots}
@@ -396,7 +396,7 @@ y > a \Leftrightarrow (x^2+z) > a \Leftrightarrow x^2+2x+1 > a \Leftrightarrow (
 $$
 hence we have shown $x^2\leq a < (x+1)^2$, and taking square roots shows the claim.
 \newpage
-\subsection{The RISCAL Formalization}
+\subsection*{The RISCAL Formalization}
 %{\scriptsize \verbatiminput{../integerroot.txt}}
 {\scriptsize \verbatimboxed{../integerroot.txt}}
 \appendix
diff --git a/src/primefactors.cpp b/src/primefactors.cpp
index d4ad778..b1a3306 100644
--- a/src/primefactors.cpp
+++ b/src/primefactors.cpp
@@ -127,31 +127,81 @@ void tonelli(long a, long g, long p)
 	}
 	t = locpm1;
 
-	cout << "Express p-1 = " << p-1 << " as 2^" << s << "*" << t << endl;
+//	cout << "Express p-1 = " << p-1 << " as 2^" << s << "*" << t << endl;
 	unsigned long* e = new unsigned long[s];
 
 	e[0] = 0;
     xGCD(g,p,u,v);
     gi = fmod(u,p)+p;
-    cout << "So far we got: t=" << t << " and s=" << 2 << " and gi=" << gi << endl;
+//  cout << "So far we got: t=" << t << " and s=" << 2 << " and gi=" << gi << endl;
     for(long i=1;i<s;i++)
     {
        tmp = a*pow(gi,e[i-1]);
-       cout << "tmp: " << tmp << endl;
+//     cout << "tmp: " << tmp << endl;
        tmp = pow(tmp,(p-1)/pow(2,i+1));
-       cout << "tmp: " << tmp << endl;
+//     cout << "tmp: " << tmp << endl;
        if(fmod(tmp,p) != 1)
     	   e[i] = pow(2,i)+e[i-1];
        else
     	   e[i] = e[i-1];
     }
-    cout << "we got e:" << e[0] << " and " << e[1] << endl;
+//  cout << "we got e:" << e[0] << " and " << e[1] << endl;
     tmp = fmod(a*pow(gi,e[s-1]), p);
-    cout << "tmp: " << tmp << endl;
+//    cout << "tmp: " << tmp << endl;
     tmp = fmod(g*pow(tmp,(t+1)/2),p);
-    cout << "tmp: " << tmp << endl;
+    cout << "Computed Solution: " << tmp << endl;
 }
 
+void discrete_log(long p, long g, long a)
+{
+   long m = -floor(-sqrt(p-1));
+   cout << "So far we got: m=" << m << endl;
+   long *A = new long[m];
+   long *b = new long[m];
+
+   A[0] = 1;
+   b[0] = a;
+
+   for(int i=1;i<m;i++)
+   {
+       A[i] = fmod(g*A[i-1],p);
+   }
+
+   cout << "So far we got: " << endl;
+   for(int i=0;i<m;i++)
+   {
+	  cout << "A[" << i << "] = " << A[i] << "; ";
+   }
+   cout << endl;
+
+   long gi, s;
+   xGCD(g,p,gi,s);
+   gi = gi%p;
+   cout << "We got: gi=" << gi << endl;
+
+   long gim = 1;
+
+   for(int i=0;i<m;i++)
+	   gim = ((gim * gi) %p);
+   cout << "We got: gim=" << gim << endl;
+
+   for(int i=0;i<m;i++)
+   {
+	   for(int j=0;j<m;j++)
+	   {
+		  if(A[j] == b[i])
+		  {
+              cout << "We got: i=" << i << " and j=" << j << endl;
+              cout << "This gives the discrete logarithm: " << i*m + j << endl;
+		  }
+	   }
+	   b[i+1] = b[i]*gim % p;
+   }
+
+
+}
+
+
 int main(int argc, char** argv)
 {
    if(argc == 1)
@@ -164,9 +214,10 @@ int main(int argc, char** argv)
 		   cout << "Algorithm A: Trial division" << endl;
 		   cout << "Algorithm C: Fermat like factorization" << endl;
 		   cout << "Algorithm D: Tonelli's Algorithm" << endl;
+		   cout << "Algorithm E: Discrete Logarithm" << endl;
            cin >> input;
            cout << endl;
-	   }while((input != 'A') && (input != 'C') && (input != 'D') );
+	   }while((input != 'A') && (input != 'C') && (input != 'D') && (input != 'E') );
 
 	   switch(input)
 	   {
@@ -222,10 +273,16 @@ int main(int argc, char** argv)
 	   	   }
 	   	   case 'D':
 	   	   {
-	   		   cout << "Algorithm of Tonelli" << endl;
+//	   		   cout << "Algorithm of Tonelli" << endl;
 	   		   tonelli(10,2,13);
 	   		   break;
 	   	   }
+	   	   case 'E':
+	   		   	   {
+	   	//	   		   cout << "Algorithm of Tonelli" << endl;
+	   		   		   discrete_log(113, 3, 57);
+	   		   		   break;
+	   		   	   }
 	   	   default:
 	   		   break;
 	   }