Finally corrected DiscreteLog-Algorithm

diff --git a/discrete_log.txt b/discrete_log.txt
index c5c11a5..e92aa12 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -2,6 +2,7 @@
 val M: ℕ;
 val K: ℕ;
 val L: ℕ;
+val MAX: ℕ;
 
 type nat = ℕ[M];
 type prime = ℕ[K];
@@ -20,13 +21,11 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
 {
    var ainv:prime := 0;
    var i:prime;
-
-   // straight search
-   // algorithmic alternative: Euclidean algorithm   
+   
    for i=1;i<p;i=i+1 do
      decreases p-i;
-     if a*i % p = 1 then
-        ainv = i;
+     if a*i % p = 1 then    // straight search
+        ainv = i;           // algorithmic alternative: Euclidean algorithm   
 
    return ainv;
 }
@@ -58,19 +57,15 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
 {
    var ret:res := 0;
    var m:nat := IntegerRoot(p-1)+1; 
-   var A:Array[20,nat]; // Q: Is it possible to dynamically allocate?? m would suffice
-   var b:Array[20,nat]; // Q: Is it possible to dynamically allocate?? m would suffice
+   var A:Array[MAX,nat] := Array[MAX,nat](0);
+   var b:Array[MAX,nat] := Array[MAX,nat](0);
    var gim:prime := 1;
-
-   
-   A = Array[20,nat](0); // Q: Is it possible to dynamically allocate?? m would suffice
-   b = Array[20,nat](0); // Q: Is it possible to dynamically allocate??   m would suffice
-   
-   A[0] := 1;
-   b[0] := a;
-
    var gi:prime = InvModP(g,p);
+   var solFound:Bool := false;
   
+   A[0] := 1;
+   b[0] := a;
+ 
    for var i:nat=1;i<=m;i=i+1 do
       decreases m+1-i;
    {
@@ -78,7 +73,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       gim = gim*gi % p;
    }
    
-   for var i:nat=0;i<m;i=i+1 do
+   for var i:nat=0;i<m ∧ ¬solFound;i=i+1 do
       decreases m-i;   
    {
       for var j:nat=0;j<m;j=j+1 do
@@ -88,11 +83,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
          {
             // result found
             ret = i*m + j;
-            print ret;
-            // abort loop
-            // Q: Is there a more comfortable way (e.g. break??)
-            i = m-1; 
-            j = m-1;
+            solFound = true;
          }
       }
       b[i+1] = b[i]*gim % p; // Giant-Step
@@ -101,4 +92,3 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    return ret;
 }
 
-