From 8adc253ac75658f9ed233337a91f4631f6ae1b57 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 14 May 2017 10:14:43 +0200
Subject: [PATCH] Added specifications of loop result

---
 discrete_log.txt | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/discrete_log.txt b/discrete_log.txt
index 410da66..5658ca6 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -125,12 +125,14 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
             ret = i*m + j;
             solFound = true;
          }
+         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 = true ∧ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]);
-//// overflow in result...   assert(∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s] ∧ (g^(s*m)%p * (g^r%p) = a));
+   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)
 
    return ret;
-- 
2.1.4