Update after second review Wolfgang

diff --git a/discrete_log.txt b/discrete_log.txt
index b66aa0c..13ad706 100644 (file)
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -12,16 +12,22 @@ 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 (a*result) % p = 1;
+   ensures 0 < result ∧ result < p ∧ 
+           (a*result) % p = 1;
 {
    var ainv:prime := 0;
    var i:prime;
    
    for i=1;i<p;i=i+1 do
+     invariant 0 < i ∧ i ≤ p;
      invariant (ainv = 0) ⇒ (∀j:prime. j < i ⇒ a*j % p ≠ 1);
+     invariant (ainv ≠ 0) ⇒ (0 < ainv ∧ ainv < i ∧ (a*ainv)%p = 1);     
      decreases p-i;
      if a*i % p = 1 then    // straight search
         ainv = i;           // algorithmic alternative: Euclidean algorithm   
@@ -63,8 +69,8 @@ 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
-      invariant 0 ≤ A[i] ∧ A[i] < p ∧
-                0 < gim ∧ gim < p;
+      invariant 0 ≤ A[i] ∧ A[i] < p;
+      invariant 0 < gim ∧ gim < p;
       decreases m+1-i;
    {
       A[i] = A[i-1]*g%p; // Baby-Step
@@ -91,3 +97,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
 }
 
 
+