Corrected and finalized verification of Baby-Step Giant Step

diff --git a/discrete_log.txt b/discrete_log.txt
index b4ce377..08e5964 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -11,6 +11,8 @@ 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
    requires p>1 ∧ isPrime(p) ∧
             0 < a ∧ a < p;
@@ -29,7 +31,7 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
    return ainv;
 }
 
-proc integerroot(a:nat): nat
+proc IntegerRoot(a:nat): nat
    ensures result^2 ≤ a ∧ a < (result+1)^2;
 {
    var x:nat = 0;
@@ -50,27 +52,27 @@ proc integerroot(a:nat): nat
 proc DiscreteLog(p:prime,g:nat,a:nat): res
    requires 1 < p ∧ isPrime(p) ∧ // p is a prime greater than 1
             1 < g ∧ g < p ∧ 
-            1 < a ∧ ¬divides(p,a) ∧
             ∀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ℤ
+            0 < a ∧ a < p; // a is in ℤ/pℤ - {0}
    ensures (g^result)%p = a;
 {
    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;
-   var m:nat := integerroot(p-1)+2; // actually \lceil sqrt(p-1) \rceil // TODO
+   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 gim:prime := 1;
+
    
-   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 = 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);
   
-   for var i:nat=1;i<m;i=i+1 do
-      decreases m-i;
+   for var i:nat=1;i<=m;i=i+1 do
+      decreases m+1-i;
    {
       A[i] = A[i-1]*g%p; // Baby-Step
       gim = gim*gi % p;
@@ -98,10 +100,3 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    return ret;
 }
 
-proc main(): ()
-{
-   print DiscreteLog(11,2,10);
-}
-
-
-