Working version of Discrete Logarithm

diff --git a/discrete_log.txt b/discrete_log.txt
index 8241d31..047ffb9 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -1,9 +1,11 @@
 
 val M: ℕ;
 val K: ℕ;
+val L: ℕ;
 
 type nat = ℕ[M];
 type prime = ℕ[K];
+type res = ℕ[L];
 
 pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n;
 
@@ -30,19 +32,19 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
    return ainv;
 }
 
-proc discrete_log(p:prime,g:nat,a:nat,m:nat): nat
+proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
    requires p>1 ∧ isPrime(p) ∧ // p is a prime greater than 1
             ∀b:nat. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧  g^(p-1)%p = 1 ∧ // g has order p-1
             0 ≤ a ∧ a < p; // a is in ℤ/pℤ
    ensures (g^result)%p = a;
 {
-   var ret:Nat[K^2] := 0;
-   var A:Array[20,nat];
-   var b:Array[20,nat];
+   var ret:res := 0;
+   var A:Array[20,nat]; // Q: Is it possible to dynamically allocate??
+   var b:Array[20,nat]; // Q: Is it possible to dynamically allocate??
    var gim:prime := g;
    
-   A = Array[20,nat](0);
-   b = Array[20,nat](0);   
+   A = Array[20,nat](0); // Q: Is it possible to dynamically allocate??
+   b = Array[20,nat](0); // Q: Is it possible to dynamically allocate??  
    
    A[0] := 1;
    b[0] := a;
@@ -53,9 +55,7 @@ proc discrete_log(p:prime,g:nat,a:nat,m:nat): nat
    {
       A[i] = A[i-1]*g%p;
       gim = gim*gi % p;
-      print A[i];
    }
-   print gim;
    
    for var i:nat=0;i<m;i=i+1 do
    {
@@ -63,12 +63,16 @@ proc discrete_log(p:prime,g:nat,a:nat,m:nat): nat
       {
          if A[j] = b[i] then
          {
+            // result found
             ret = i*m + j;
+            // abort loop
+            i = m-1;
+            j = m-1;
          }
       }
       b[i+1] = b[i]*gim % p;
    }   
-   print ret;
+
    return ret;
 }
 
@@ -76,3 +80,5 @@ proc main(): ()
 {
    print discrete_log(11,2,10,10);
 }
+
+