Modular exponentiation

DefinitionModular exponentiation#✓fully proved

For natural numbers \(a\), \(b\) and \(n\), modular exponentiation with base \(a\), exponent \(b\) and modulus \(n\) is the recursive procedure that returns \(1\) if \(b = 0\). If \(b > 0\) is even, it computes the result \(d\) for exponent \(b/2\) (same base and modulus) and returns \(d \cdot d \bmod n\). If \(b\) is odd, it computes the result \(d\) for exponent \(b - 1\) and returns \(a \cdot d \bmod n\). Each even or odd step performs one multiplication, and the cost of the procedure is the total number of multiplications performed.

Cslib.Algorithms.Lean.ModularExponentiation.modularExponentiation · 17 lines 
def modularExponentiation (a b n : Nat) : TimeM Nat Nat :=
  if _hzero : b = 0 then
    pure 1
  else if _heven : b % 2 = 0 then
    do
      let d ← modularExponentiation a (b / 2) n
      TimeM.tick 1
      pure ((d * d) % n)
  else
    do
      let d ← modularExponentiation a (b - 1) n
      TimeM.tick 1
      pure ((a * d) % n)
termination_by b
decreasing_by
  · exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero _hzero) (by decide)
  · exact Nat.sub_lt (Nat.zero_lt_of_ne_zero _hzero) (by decide)
Sources
  • CLRS4 §31.6, printed page 934, MODULAR-EXPONENTIATION, with one tick per multiplication.
Used by 24
Used byMiller–Rabin witness test · What a non-witness satisfies · A prime has no Miller–Rabin witnesses in range · Fermat witnesses are Miller–Rabin witnesses · Cost of the Miller–Rabin witness test · Correctness of modular exponentiation · Even step of modular exponentiation · Modular exponentiation returns the least residue · Modular exponentiation returns a value below the modulus · Odd step of modular exponentiation · Value of the even step of modular exponentiation · Modular exponentiation returns a reduced value · Modular exponentiation is correct up to reduction · Modular exponentiation with a reduced base · Value of the odd step of modular exponentiation · Modular exponentiation returns 1 at exponent zero · Multiplication count of modular exponentiation · Multiplication count in the even case · The multiplication count depends only on the exponent · Multiplication count in the odd case · No multiplications at exponent zero · Base case of modular exponentiation · Least residue at exponent zero · Unreduced result at modulus one

TheoremBase case of modular exponentiation#✓fully proved

For all natural numbers \(a\) and \(n\), modular exponentiation with base \(a\), exponent \(0\) and modulus \(n\) returns \(1\) and performs no multiplications.

@[simp]
theorem modularExponentiation_zero (a n : Nat) :
    modularExponentiation a 0 n = ⟨1, 0⟩
Uses 1 · Used by 6
Statement usesModular exponentiation
Used byModular exponentiation is correct up to reduction · Modular exponentiation returns 1 at exponent zero · Multiplication count of modular exponentiation · The multiplication count depends only on the exponent · No multiplications at exponent zero · Unreduced result at modulus one

TheoremEven step of modular exponentiation#✓fully proved

Let \(a\), \(b\), \(n\) be natural numbers with \(b > 0\) and \(b\) even. If modular exponentiation on base \(a\), exponent \(b/2\) and modulus \(n\) returns the value \(d\) using \(t\) multiplications, then on base \(a\), exponent \(b\) and modulus \(n\) it returns the value \((d \cdot d) \bmod n\) using \(t + 1\) multiplications.

theorem modularExponentiation_even (a b n : Nat) (hb : 0 < b) (heven : b % 2 = 0) :
    modularExponentiation a b n =
      let d := modularExponentiation a (b / 2) n
      ⟨(d.ret * d.ret) % n, d.time + 1⟩
Uses 1 · Used by 2
Statement usesModular exponentiation
Used byValue of the even step of modular exponentiation · Multiplication count in the even case

TheoremOdd step of modular exponentiation#✓fully proved

Let \(a\), \(b\), \(n\) be natural numbers with \(b\) odd. If modular exponentiation on base \(a\), exponent \(b - 1\) and modulus \(n\) returns the value \(d\) using \(t\) multiplications, then on base \(a\), exponent \(b\) and modulus \(n\) it returns the value \((a \cdot d) \bmod n\) using \(t + 1\) multiplications.

theorem modularExponentiation_odd (a b n : Nat) (hodd : b % 2 ≠ 0) :
    modularExponentiation a b n =
      let d := modularExponentiation a (b - 1) n
      ⟨(a * d.ret) % n, d.time + 1⟩
Uses 1 · Used by 2
Statement usesModular exponentiation
Used byValue of the odd step of modular exponentiation · Multiplication count in the odd case

TheoremModular exponentiation returns 1 at exponent zero#✓fully proved

For all natural numbers \(a\) and \(n\), modular exponentiation with base \(a\), exponent \(0\) and modulus \(n\) returns \(1\).

In particular the returned value is \(1\) even when \(n = 1\), so it is not reduced modulo \(n\).

@[simp]
theorem modularExponentiation_ret_zero (a n : Nat) :
    (modularExponentiation a 0 n).ret = 1
Uses 2 · Used by 1
Statement usesModular exponentiation
Proof usesBase case of modular exponentiation
Used byLeast residue at exponent zero

TheoremNo multiplications at exponent zero#✓fully proved

For all natural numbers \(a\) and \(n\), modular exponentiation with base \(a\), exponent \(0\) and modulus \(n\) performs no multiplications.

@[simp]
theorem modularExponentiation_time_zero (a n : Nat) :
    (modularExponentiation a 0 n).time = 0
Uses 2
Statement usesModular exponentiation
Proof usesBase case of modular exponentiation

TheoremValue of the even step of modular exponentiation#✓fully proved

Let \(a\), \(b\), \(n\) be natural numbers with \(b > 0\) and \(b\) even, and let \(d\) be the value returned by modular exponentiation on base \(a\), exponent \(b/2\) and modulus \(n\). Then the value returned on base \(a\), exponent \(b\) and modulus \(n\) is \((d \cdot d) \bmod n\).

theorem modularExponentiation_ret_even (a b n : Nat) (hb : 0 < b)
    (heven : b % 2 = 0) :
    (modularExponentiation a b n).ret =
      let d := (modularExponentiation a (b / 2) n).ret
      (d * d) % n
Uses 2 · Used by 2
Statement usesModular exponentiation
Proof usesEven step of modular exponentiation
Used byModular exponentiation returns a reduced value · Modular exponentiation is correct up to reduction

TheoremMultiplication count in the even case#✓fully proved

Let \(a\), \(b\) and \(n\) be natural numbers with \(b\) positive and even. Modular exponentiation with base \(a\), exponent \(b\) and modulus \(n\) performs exactly one more multiplication than it does with base \(a\), exponent \(b/2\) and modulus \(n\).

theorem modularExponentiation_time_even (a b n : Nat) (hb : 0 < b)
    (heven : b % 2 = 0) :
    (modularExponentiation a b n).time =
      (modularExponentiation a (b / 2) n).time + 1
Uses 2 · Used by 2
Statement usesModular exponentiation
Proof usesEven step of modular exponentiation
Used byMultiplication count of modular exponentiation · The multiplication count depends only on the exponent

TheoremValue of the odd step of modular exponentiation#✓fully proved

Let \(a\), \(b\), \(n\) be natural numbers with \(b\) odd, and let \(d\) be the value returned by modular exponentiation on base \(a\), exponent \(b - 1\) and modulus \(n\). Then the value returned on base \(a\), exponent \(b\) and modulus \(n\) is \((a \cdot d) \bmod n\).

theorem modularExponentiation_ret_odd (a b n : Nat) (hodd : b % 2 ≠ 0) :
    (modularExponentiation a b n).ret =
      (a * (modularExponentiation a (b - 1) n).ret) % n
Uses 2 · Used by 2
Statement usesModular exponentiation
Proof usesOdd step of modular exponentiation
Used byModular exponentiation returns a reduced value · Modular exponentiation is correct up to reduction

TheoremMultiplication count in the odd case#✓fully proved

Let \(a\), \(b\) and \(n\) be natural numbers with \(b\) odd. Modular exponentiation with base \(a\), exponent \(b\) and modulus \(n\) performs exactly one more multiplication than it does with base \(a\), exponent \(b - 1\) and modulus \(n\).

theorem modularExponentiation_time_odd (a b n : Nat) (hodd : b % 2 ≠ 0) :
    (modularExponentiation a b n).time =
      (modularExponentiation a (b - 1) n).time + 1
Uses 2 · Used by 2
Statement usesModular exponentiation
Proof usesOdd step of modular exponentiation
Used byMultiplication count of modular exponentiation · The multiplication count depends only on the exponent

TheoremModular exponentiation is correct up to reduction#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(n > 0\), including \(b = 0\), the value \(r\) returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) satisfies \(r \bmod n = a^b \bmod n\).

theorem modularExponentiation_ret_mod (a b n : Nat) (_hn : 0 < n) :
    (modularExponentiation a b n).ret % n = a ^ b % n
Uses 4 · Used by 2
Statement usesModular exponentiation
Proof usesValue of the even step of modular exponentiation · Value of the odd step of modular exponentiation · Base case of modular exponentiation
Used byCorrectness of modular exponentiation · Modular exponentiation with a reduced base

TheoremModular exponentiation with a reduced base#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(n > 0\), the value \(r\) returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) satisfies \(r \bmod n = (a \bmod n)^b \bmod n\).

theorem modularExponentiation_ret_mod_base (a b n : Nat) (hn : 0 < n) :
    (modularExponentiation a b n).ret % n = (a % n) ^ b % n
Uses 2
Statement usesModular exponentiation
Proof usesModular exponentiation is correct up to reduction

TheoremModular exponentiation returns a reduced value#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(b > 0\), the value \(r\) returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) satisfies \(r \bmod n = r\) (with the convention \(r \bmod 0 = r\)).

theorem modularExponentiation_ret_is_reduced (a b n : Nat) (hb : 0 < b) :
    (modularExponentiation a b n).ret % n =
      (modularExponentiation a b n).ret
Uses 3 · Used by 1
Statement usesModular exponentiation
Proof usesValue of the even step of modular exponentiation · Value of the odd step of modular exponentiation
Used byCorrectness of modular exponentiation

TheoremCorrectness of modular exponentiation#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(b > 0\) and \(n > 0\), the value returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) equals \(a^b \bmod n\).

theorem modularExponentiation_correct (a b n : Nat) (hb : 0 < b) (hn : 0 < n) :
    (modularExponentiation a b n).ret = a ^ b % n
Uses 3 · Used by 5
Statement usesModular exponentiation
Proof usesModular exponentiation returns a reduced value · Modular exponentiation is correct up to reduction
Used byWhat a non-witness satisfies · A prime has no Miller–Rabin witnesses in range · Fermat witnesses are Miller–Rabin witnesses · Modular exponentiation returns the least residue · Modular exponentiation returns a value below the modulus

TheoremModular exponentiation returns a value below the modulus#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(b > 0\) and \(n > 0\), the value returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) is less than \(n\).

theorem modularExponentiation_lt (a b n : Nat) (hb : 0 < b) (hn : 0 < n) :
    (modularExponentiation a b n).ret < n
Uses 2 · Used by 1
Statement usesModular exponentiation
Proof usesCorrectness of modular exponentiation
Used byModular exponentiation returns the least residue

TheoremModular exponentiation returns the least residue#✓fully proved

For natural numbers \(a\), \(b\), \(n\) with \(b > 0\) and \(n > 0\), the value \(r\) returned by modular exponentiation on base \(a\), exponent \(b\) and modulus \(n\) satisfies \(r = a^b \bmod n\) and \(r < n\).

theorem modularExponentiation_is_leastResidue (a b n : Nat) (hb : 0 < b) (hn : 0 < n) :
    (modularExponentiation a b n).ret = a ^ b % n ∧
      (modularExponentiation a b n).ret < n
Uses 3
Statement usesModular exponentiation
Proof usesCorrectness of modular exponentiation · Modular exponentiation returns a value below the modulus

TheoremLeast residue at exponent zero#✓fully proved

For all natural numbers \(a\) and \(n\) with \(n > 1\), the value returned by modular exponentiation with base \(a\), exponent \(0\) and modulus \(n\) equals \(a^0 \bmod n\) and is less than \(n\).

theorem modularExponentiation_zero_is_leastResidue (a n : Nat) (hn : 1 < n) :
    (modularExponentiation a 0 n).ret = a ^ 0 % n ∧
      (modularExponentiation a 0 n).ret < n
Uses 2
Statement usesModular exponentiation
Proof usesModular exponentiation returns 1 at exponent zero

TheoremUnreduced result at modulus one#✓fully proved

For every natural number \(a\), modular exponentiation with base \(a\), exponent \(0\) and modulus \(1\) returns \(1\), whereas \(a^0 \bmod 1 = 0\).

The base case of the CLRS procedure returns \(1\) without reducing it modulo the modulus; this boundary case keeps that visible.

theorem modularExponentiation_zero_modulus_one (a : Nat) :
    (modularExponentiation a 0 1).ret = 1 ∧ a ^ 0 % 1 = 0
Uses 2
Statement usesModular exponentiation
Proof usesBase case of modular exponentiation

TheoremThe multiplication count depends only on the exponent#✓fully proved

For all natural numbers \(a\), \(a'\), \(b\), \(n\) and \(n'\), modular exponentiation performs the same number of multiplications with base \(a\), exponent \(b\) and modulus \(n\) as with base \(a'\), exponent \(b\) and modulus \(n'\).

theorem modularExponentiation_time_independent (a a' b n n' : Nat) :
    (modularExponentiation a b n).time =
      (modularExponentiation a' b n').time
Uses 4
Statement usesModular exponentiation
Proof usesMultiplication count in the even case · Multiplication count in the odd case · Base case of modular exponentiation

TheoremMultiplication count of modular exponentiation#✓fully proved

Let \(a\), \(b\) and \(n\) be natural numbers with \(b > 0\), and let \(\beta = \lfloor \log_2 b \rfloor + 1\) be the number of binary digits of \(b\). The number of multiplications performed by modular exponentiation with base \(a\), exponent \(b\) and modulus \(n\) is at least \(\beta\) and at most \(2\beta - 1\).

theorem modularExponentiation_time_bounds (a b n : Nat) (hb : 0 < b) :
    let β := Nat.log2 b + 1
    β ≤ (modularExponentiation a b n).time ∧
      (modularExponentiation a b n).time ≤ 2 * β - 1
Uses 4
Statement usesModular exponentiation
Proof usesMultiplication count in the even case · Multiplication count in the odd case · Base case of modular exponentiation
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.