From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Mon, 15 May 2017 18:46:32 +0000 (+0200)
Subject: Added assertions for discrete_log
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=b9b6fc3ed16a951e2622e0763086187e40de74fa;p=cfuerst%2Fformal-numbers.git

Added assertions for discrete_log
---

diff --git a/discrete_log.txt b/discrete_log.txt
index 5658ca6..1fe4944 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -111,13 +111,18 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       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 (¬solFound) ⇔ ∀r:nat with r < m. ∀s:nat with s < i. A[r] ≠ b[s];
+      invariant (¬solFound) ⇒  ∀r:nat with r < m. ∀s:nat with s < i. A[r] ≠ b[s];
+      invariant   solFound  ⇒ (∃r:nat with r < m. ∃s:nat with s < i. A[r] = b[s] ∧
+                               PowerMod(g,s*m+r,p) = a ∧ ret = s*m+r);
       decreases m-i;
    {
       for var j:nat=0;j<m;j=j+1 do
          invariant 0 ≤ j ∧ j ≤ m;
          invariant 0 ≤ ret ∧ ret ≤ m^2;
-         invariant (¬solFound) ⇔ (∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]);
+         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 with 0 ≤ k ∧ k < j. A[k] = b[i] ∧ 
+                                  PowerMod(g,i*m+k,p) = a ∧ ret = i*m+k);
          decreases m-j;      
       {
          if A[j] = b[i] then
@@ -131,13 +136,11 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       assert( (¬solFound) ⇒ (∀i2:nat with i2 < i. ∀j:nat with j < m. A[i2] ≠ b[j]));
    }
 
-   assert(solFound = true ⇒ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]);
-   assert(∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s] ∧ PowerMod(g,s*m+r,p)=a);
-   // solFound = false should never be the case (see theorem DiscreteLogExists)
+   assert(solFound = true);
+   
+   assert(∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s] ∧ 
+          PowerMod(g,s*m+r,p)=a ∧ ret = s*m + r);
 
    return ret;
 }
 
-
-
-