Added loop invariants

diff --git a/discrete_log.txt b/discrete_log.txt
index 3193ae5..32613be 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -12,13 +12,10 @@ pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n;
 pred isPrime(m:prime) ⇔ m > 1 ∧ ∀n:prime. n>1 ∧ divides(n,m) ⇒ (n = m);
 pred isComposite(m:prime) ⇔ ¬isPrime(m);
 
-theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒
-                          ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1;
-
 proc InvModP(a:ℕ[K^2],p:prime): prime
    requires isPrime(p) ∧
             0 < a ∧ a < p;
-   ensures 0 < result ∧ result < p ∧ 
+   ensures 0 < result ∧ result < p ∧
            (a*result) % p = 1;
 {
    var ainv:prime := 0;
@@ -42,7 +39,9 @@ proc IntegerRoot(a:nat): nat
    var z:ℕ[(K+1)^2] = 1;
 
    while y ≤ a do
-      invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
+      invariant 1 ≤ y ∧ y = x^2+z;
+      invariant 0 ≤ x ∧ x^2 ≤ a;
+      invariant 1 ≤ z ∧ z = 2*x+1;
       decreases a-x^2;
    {
       x=x+1;
@@ -52,6 +51,13 @@ proc IntegerRoot(a:nat): nat
    return x;
 }
 
+theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒
+                          ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1;
+theorem DiscreteLogExists(p:prime, g:nat,a:nat) ⇔ (isPrime(p) ∧  1 < g ∧ g < p ∧
+            ∀b:prime. (0 < b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧  g^(p-1)%p = 1 ∧ // g has order p-1
+            0 < a ∧ a < p) ⇒ (∃k:res with 0 < k ∧ k ≤ (IntegerRoot(p-1)+1)^2. g^k%p = a);
+
+
 proc DiscreteLog(p:prime,g:nat,a:nat): res
    requires isPrime(p) ∧
             1 < g ∧ g < p ∧ 
@@ -69,21 +75,33 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
   
    A[0] := 1;  b[0] := a;
  
-   for var i:nat=1;i<=m;i=i+1 do
+   for var i:nat=1;i≤m;i=i+1 do
+      invariant 1 ≤ i ∧ i ≤ m+1;
       invariant 0 ≤ A[i] ∧ A[i] < p;
       invariant 0 < gim ∧ gim < p;
+      invariant gim = gi^(i-1)%p;
+      invariant ∀j:nat with 1 ≤ j ∧ j < i. A[j] = A[j-1]*g % p;
       decreases m+1-i;
    {
       A[i] = A[i-1]*g%p; // Baby-Step
       gim = gim*gi % p;
    }
-   
+
+   assert(gim=gi^m%p);
+   assert(∀j:nat with 0 ≤ j ∧ j ≤ m. 0 ≤ A[j] ∧ A[j] < p);
+   assert(∀j:nat with 1 ≤ j ∧ j ≤ m. A[j] = A[j-1]*g % p);
+
    for var i:nat=0;i<m ∧ ¬solFound;i=i+1 do
+      invariant 0 ≤ i ∧ i < m;
       invariant 0 ≤ b[i] ∧ b[i] < p;
-      decreases m-i;   
+      invariant ∀k:nat with 1 < k ∧ k≤i. b[k] = b[k-1]*gim % p;
+      invariant (¬solFound) ⇔ ∀r:nat with r < m. ∀s:nat with s < i. A[r] ≠ b[s];
+      decreases m-i;
    {
       for var j:nat=0;j<m;j=j+1 do
-         invariant (¬solFound) ⇒ (∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]);
+         invariant 0 ≤ j ∧ j ≤ m;
+         invariant 0 ≤ ret ∧ ret ≤ m^2;
+         invariant (¬solFound) ⇔ (∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]);
          decreases m-j;      
       {
          if A[j] = b[i] then
@@ -93,10 +111,12 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
          }
       }
       b[i+1] = b[i]*gim % p; // Giant-Step
-   }   
-   return ret;
-}
-
+   }
 
+   assert(solFound = true  ⇔ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]);
+   // solFound = false should never be the case (see theorem DiscreteLogExists)
+   assert(solFound = false ⇔ ∀r:nat with r < m. ∀s:nat with s < m. A[r] ≠ b[s]);
 
+   return ret;
+}