From dbcfdfa96be8b52664b394b4d946b83ee3d84d5a Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 6 Apr 2017 21:46:06 +0200
Subject: [PATCH] Added calculation for m

---
 discrete_log.txt | 52 ++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 36 insertions(+), 16 deletions(-)

diff --git a/discrete_log.txt b/discrete_log.txt
index c64a129..5ea4687 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -18,25 +18,39 @@ proc InvModP(a:ℕ[K^2],p:prime): prime
 {
    var ainv:prime := 0;
    var i:ℕ[K^2];
-   
-   if a = 1 then
-   {
-      ainv = 1;
-   }
-   else
+
+   // straight search
+   // algorithmic alternative: Euclidean algorithm   
+   for i=1;i<p;i=i+1 do
+     decreases p-i;
+     if a*i % p = 1 then
+        ainv = i;
+
+   return ainv;
+}
+
+proc integerroot(a:nat): nat
+   ensures result^2 ≤ a ∧ a < (result+1)^2;
+{
+   var x:nat = 0;
+   var y:ℕ[(K+1)^2] = 1;
+   var z:ℕ[(K+1)^2] = 1;
+
+   while y ≤ a do
+      invariant x^2 ≤ a ∧ y = x^2+z ∧ z = 2*x+1;
    {
-      for i=1;i<p;i=i+1 do
-         if a*i % p = 1 then
-            ainv = i;
+      x=x+1;
+      z=z+2;
+      y=y+z;
    }
-   return ainv;
+
+   return x;
 }
 
-proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
+proc DiscreteLog(p:prime,g:nat,a:nat): res
    requires 1 < p ∧ isPrime(p) ∧ // p is a prime greater than 1
             1 < g ∧ g < p ∧ 
             1 < a ∧ ¬divides(p,a) ∧
-            8 < m ∧ 
             ∀b:nat. (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ℤ
    ensures (g^result)%p = a;
@@ -45,6 +59,7 @@ proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
    var A:Array[20,nat]; // Q: Is it possible to dynamically allocate??
    var b:Array[20,nat]; // Q: Is it possible to dynamically allocate??
    var gim:prime := g;
+   var m:nat := integerroot(p-1)+2; // actually \lceil sqrt(p-1) \rceil // TODO
    
    A = Array[20,nat](0); // Q: Is it possible to dynamically allocate??
    b = Array[20,nat](0); // Q: Is it possible to dynamically allocate??  
@@ -55,25 +70,29 @@ proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
    var gi:prime = InvModP(g,p);
   
    for var i:nat=1;i<m;i=i+1 do
+      decreases m-i;
    {
-      A[i] = A[i-1]*g%p;
+      A[i] = A[i-1]*g%p; // Baby-Step
       gim = gim*gi % p;
    }
    
    for var i:nat=0;i<m;i=i+1 do
+      decreases m-i;   
    {
       for var j:nat=0;j<m;j=j+1 do
+         decreases m-j;      
       {
          if A[j] = b[i] then
          {
             // result found
             ret = i*m + j;
             // abort loop
-            i = m-1;
+            // Q: Is there a more comfortable way (e.g. break??)
+            i = m-1; 
             j = m-1;
          }
       }
-      b[i+1] = b[i]*gim % p;
+      b[i+1] = b[i]*gim % p; // Giant-Step
    }   
 
    return ret;
@@ -81,7 +100,8 @@ proc discrete_log(p:prime,g:nat,a:nat,m:nat): res
 
 proc main(): ()
 {
-   print discrete_log(11,2,10,10);
+   print DiscreteLog(11,2,10);
 }
 
 
+
-- 
2.1.4