From 1c583171052b937252aa94c592908b5de7ff2135 Mon Sep 17 00:00:00 2001 From: Christoph Fuerst Date: Thu, 20 Apr 2017 16:39:39 +0200 Subject: [PATCH] Update after second review Wolfgang --- discrete_log.txt | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/discrete_log.txt b/discrete_log.txt index b66aa0c..13ad706 100644 --- a/discrete_log.txt +++ b/discrete_log.txt @@ -12,16 +12,22 @@ pred divides(m:prime,n:prime) ⇔ ∃p:prime. m⋅p = n; pred isPrime(m:prime) ⇔ m > 1 ∧ ∀n:prime. n>1 ∧ divides(n,m) ⇒ (n = m); pred isComposite(m:prime) ⇔ ¬isPrime(m); +theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒ + ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1; + proc InvModP(a:ℕ[K^2],p:prime): prime requires isPrime(p) ∧ 0 < a ∧ a < p; - ensures (a*result) % p = 1; + ensures 0 < result ∧ result < p ∧ + (a*result) % p = 1; { var ainv:prime := 0; var i:prime; for i=1;i