From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Wed, 19 Apr 2017 19:24:41 +0000 (+0200)
Subject: Update after Review Wolfgang
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=d876a66b15b4cc82e51bc58fe808565c20428fd4;p=cfuerst%2Fformal-numbers.git

Update after Review Wolfgang
---

diff --git a/discrete_log.txt b/discrete_log.txt
index 2db452e..b66aa0c 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -9,11 +9,11 @@ type prime = ℕ[K];
 type res = ℕ[L];
 
 pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n;
-pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m);
+pred isPrime(m:prime) ⇔ m > 1 ∧ ∀n:prime. n>1 ∧ divides(n,m) ⇒ (n = m);
 pred isComposite(m:prime) ⇔ ¬isPrime(m);
 
 proc InvModP(a:ℕ[K^2],p:prime): prime
-   requires p>1 ∧ isPrime(p) ∧
+   requires isPrime(p) ∧
             0 < a ∧ a < p;
    ensures (a*result) % p = 1;
 {
@@ -21,6 +21,7 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
    var i:prime;
    
    for i=1;i<p;i=i+1 do
+     invariant (ainv = 0) ⇒ (∀j:prime. j < i ⇒ a*j % p ≠ 1);
      decreases p-i;
      if a*i % p = 1 then    // straight search
         ainv = i;           // algorithmic alternative: Euclidean algorithm   
@@ -45,7 +46,7 @@ proc IntegerRoot(a:nat): nat
 }
 
 proc DiscreteLog(p:prime,g:nat,a:nat): res
-   requires 1 < p ∧ isPrime(p) ∧ // p is a prime greater than 1
+   requires 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; // a is in ℤ/pℤ - {0}
@@ -62,6 +63,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;
       decreases m+1-i;
    {
       A[i] = A[i-1]*g%p; // Baby-Step
@@ -69,9 +72,11 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    }
    
    for var i:nat=0;i<m ∧ ¬solFound;i=i+1 do
+      invariant 0 ≤ b[i] ∧ b[i] < p;
       decreases m-i;   
    {
       for var j:nat=0;j<m;j=j+1 do
+         invariant (¬solFound) ⇒ (∀k:nat. 0 ≤ k ∧ k < j ⇒ A[k] ≠ b[i]);
          decreases m-j;      
       {
          if A[j] = b[i] then
@@ -85,3 +90,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
    return ret;
 }
 
+