From: Christoph Fuerst <ch.fuerst@gmx.at>
Date: Sun, 14 May 2017 08:01:27 +0000 (+0200)
Subject: Added PowerMod
X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=67a107c34b5e5c24714a46aa5b572f2c08d84ddf;p=cfuerst%2Fformal-numbers.git

Added PowerMod
---

diff --git a/discrete_log.txt b/discrete_log.txt
index b2e6535..410da66 100644
--- a/discrete_log.txt
+++ b/discrete_log.txt
@@ -51,6 +51,21 @@ proc IntegerRoot(a:nat): nat
    return x;
 }
 
+proc PowerMod(a:nat, b:nat, p:nat): nat
+{
+   var x:nat;
+
+   if b=0 then
+     x = 1;
+   else
+     x = a%p;
+     for var i:nat=1;i<b;i = i+1 do
+       x = a*x%p;
+   return x;
+}
+
+theorem PowerModWorks() ⇔ ∀a:nat. ∀b:nat. ∀p:nat. p>1 ⇒ PowerMod(a,b,p) = (a^b)%p;
+
 theorem InverseExists() ⇔ ∀a:nat. ∀p:prime. isPrime(p) ∧ 0 < a ∧ a < p ⇒
                           ∃r:nat. 0 < r ∧ r < p ∧ (a*r)%p = 1;
 
@@ -123,3 +138,4 @@ proc DiscreteLog(p:prime,g:nat,a:nat): res
 
 
 
+