First revision of discrete-log, added Prime check

diff --git a/discrete_log.txt b/discrete_log.txt
new file mode 100644 (file)
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;
+}