From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Wed, 5 Apr 2017 19:50:44 +0000 (+0200)
Subject: First revision of discrete-log, added Prime check
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=3a7f90b124563f2af49c96b4846c2f8919561034;p=cfuerst%2Fformal-numbers.git

First revision of discrete-log, added Prime check
---

diff --git a/discrete_log.txt b/discrete_log.txt
new file mode 100644
index 0000000..6c9a49e
--- /dev/null
+++ b/discrete_log.txt
@@ -0,0 +1,21 @@
+
+val M: ℕ;
+val K: ℕ;
+
+type nat = ℕ[M];
+type prime = ℕ[K];
+
+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
+   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
+            0 ≤ a ∧ a < p; // a is in ℤ/pℤ
+   ensures g^result = a;
+{
+   var loca:nat := a;
+   
+   return loca;
+}