From df9708d995b671c33a5561a84096de0471645e54 Mon Sep 17 00:00:00 2001
From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Thu, 6 Apr 2017 18:22:22 +0200
Subject: [PATCH] Formalization of DiscreteLog

---
 discrete_log.txt | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 62 insertions(+), 5 deletions(-)

diff --git a/discrete_log.txt b/discrete_log.txt
index 6c9a49e..8241d31 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -9,13 +9,70 @@ pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n;
 
 pred isPrime(m:prime) ⇔ ∀n:prime. divides(n,m) ⇒ (n ≤ 1 ∨ n = m);
 
-proc discrete_log(p:prime,g:nat,a:nat): nat
+proc InvModP(a:ℕ[K^2],p:prime): prime
+   requires p>1 ∧ isPrime(p) ∧
+            0 < a ∧ a < p;
+   ensures (a*result) % p = 1;
+{
+   var ainv:prime := 0;
+   var i:ℕ[K^2];
+   
+   if a = 1 then
+   {
+      ainv = 1;
+   }
+   else
+   {
+      for i=1;i<p;i=i+1 do
+         if a*i % p = 1 then
+            ainv = i;
+   }
+   return ainv;
+}
+
+proc discrete_log(p:prime,g:nat,a:nat,m:nat): nat
    requires p>1 ∧ isPrime(p) ∧ // p is a prime greater than 1
-            ∀b:nat. (0 ≤ b ∧ b < p-1) ⇒ (g^b % p ≠ 1) ∧ g^(p-1)%p = 1 ∧ // g has order p-1
+            ∀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 = a;
+   ensures (g^result)%p = a;
 {
-   var loca:nat := a;
+   var ret:Nat[K^2] := 0;
+   var A:Array[20,nat];
+   var b:Array[20,nat];
+   var gim:prime := g;
+   
+   A = Array[20,nat](0);
+   b = Array[20,nat](0);   
    
-   return loca;
+   A[0] := 1;
+   b[0] := a;
+
+   var gi:prime = InvModP(g,p);
+  
+   for var i:nat=1;i<m;i=i+1 do
+   {
+      A[i] = A[i-1]*g%p;
+      gim = gim*gi % p;
+      print A[i];
+   }
+   print gim;
+   
+   for var i:nat=0;i<m;i=i+1 do
+   {
+      for var j:nat=0;j<m;j=j+1 do
+      {
+         if A[j] = b[i] then
+         {
+            ret = i*m + j;
+         }
+      }
+      b[i+1] = b[i]*gim % p;
+   }   
+   print ret;
+   return ret;
+}
+
+proc main(): ()
+{
+   print discrete_log(11,2,10,10);
 }
-- 
2.1.4