From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 7 May 2017 08:27:55 +0000 (+0200)
Subject: Assertion of result
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=b333fe3f394e6b98e0aa49cfc97cd3f2dee79d80;p=cfuerst%2Fformal-numbers.git

Assertion of result
---

diff --git a/discrete_log.txt b/discrete_log.txt
index 32613be..b2e6535 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -53,6 +53,7 @@ proc IntegerRoot(a:nat): nat
 
 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);
@@ -113,10 +114,12 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
       b[i+1] = b[i]*gim % p; // Giant-Step
    }
 
-   assert(solFound = true  ⇔ ∃r:nat with r < m. ∃s:nat with s < m. A[r] = b[s]);
+   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));
    // 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;
 }
 
+
+