Incorporated last review of Wolfgang

diff --git a/discrete_log.txt b/discrete_log.txt
index 21193ac..b2f86ad 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -118,10 +118,14 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       decreases m-i;
    {
       for var j:nat=0;j<m;j=j+1 do
+         invariant 0 ≤ i ∧ i < m;
+         invariant 0 ≤ b[i] ∧ b[i] < p;
+                invariant ∀k:nat with 1 < k ∧ k≤i. b[k] = b[k-1]*gim % p;
          invariant 0 ≤ j ∧ j ≤ m;
          invariant 0 ≤ ret ∧ ret ≤ m^2;
          invariant ∀r:nat with r < m. ∀s:nat with s < i. A[r] ≠ b[s];
-         invariant (¬solFound) ⇒ (∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]);
+         invariant (¬solFound) ⇒ ((∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]) ∧ 
+                                  (∀r:nat with r < m. ∀s:nat with s < i. A[r] ≠ b[s]));
          invariant   solFound  ⇒ (∃k:nat with 0 ≤ k ∧ k < j. A[k] = b[i] ∧ 
                                   PowerMod(g,i*m+k,p) = a ∧ ret = i*m+k);
          decreases m-j;      
@@ -134,7 +138,7 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
          assert(solFound ⇒ ∃i:nat with i < m. ∃j:nat with j < m. ret = i*m +j);
       }
       b[i+1] = b[i]*gim % p; // Giant-Step
-      assert( (¬solFound) ⇒ (∀i2:nat with i2 < i. ∀j:nat with j < m. A[i2] ≠ b[j]));
+      assert( (¬solFound) ⇒ (∀r:nat with r < i. ∀s:nat with s < m. A[r] ≠ b[s]));
    }
 
    assert(solFound = true);
@@ -145,3 +149,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    return ret;
 }
 
+