proofs/math/natural/modpow.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/modpow.bend as Modpow

8 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R
import ./lcm.bend as LC
import ./bits.bend as B

Definitions

def mod_pow source · line 18 · raw

@+mp:Nat -> @+x:Nat -> @+k:Nat -> {Nat.mod(Nat.pow(Nat.mod(x, 1n+mp), k), 1n+mp) == Nat.mod(Nat.pow(x, k), 1n+mp) : Nat}

(x mod m)^k == x^k (mod m) (Mathlib Nat.pow_mod)

def pow_double source · line 30 · raw

@+x:Nat -> @+y:Nat -> {Nat.pow(x, Nat.double(y)) == Nat.pow(Nat.mul(x, x), y) : Nat}

x^(2 y) == (x x)^y

def same_sq source · line 40 · raw

@+mp:Nat -> @+c:Nat -> @+base:Nat -> @+e2:Nat -> {Nat.mod(Nat.mul(c, Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(c, Nat.pow(base, Nat.double(e2))), 1n+mp) : Nat}

the squared base, reduced, is x^(2 e2) under any factor c

def pm_bit source · line 49 · raw

@+mp:Nat -> @+e2:Nat -> @+bit:Nat -> @+hbit:{Nat.is_lt(bit, 2n) == True{} : Bool} -> @+base:Nat -> @+acc:Nat -> {Nat.mod(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.pow_mod_odd(1n+mp, bit, base, acc), Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(acc, Nat.pow(base, Nat.add(Nat.double(e2), bit))), 1n+mp) : Nat}

one step: the odd bit multiplies acc by base

def odd_lt source · line 65 · raw

@+mp:Nat -> @+bit:Nat -> @+base:Nat -> @+acc:Nat -> @+hacc:{Nat.is_lt(acc, 1n+mp) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.pow_mod_odd(1n+mp, bit, base, acc), 1n+mp) == True{} : Bool}

def pm_go source · line 73 · raw

@fuel:Nat -> @+mp:Nat -> @+e:Nat -> @+base:Nat -> @+acc:Nat -> @+he:{Nat.is_le(e, fuel) == True{} : Bool} -> @+hacc:{Nat.is_lt(acc, 1n+mp) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.pow_mod_go(fuel, 1n+mp, e, base, acc) == Nat.mod(Nat.mul(acc, Nat.pow(base, e)), 1n+mp) : Nat}

the loop: acc < m, e <= fuel give pow_mod_go == acc base^e mod m

def pow_mod_ok source · line 94 · raw

@+b:Nat -> @+e:Nat -> @+mp:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.pow_mod(b, e, 1n+mp) == Done{Nat.mod(Nat.pow(b, e), 1n+mp)} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.MathError, Nat>}

pow_mod(b, e, m) == Done{b^e mod m} (Mathlib Nat.pow_mod; Python pow(b, e, m))

def pow_mod_zero source · line 101 · raw

@+b:Nat -> @+e:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.pow_mod(b, e, 0n) == Fail{0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.ZeroDivision{}} : Result<&2, &2, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.MathError, Nat>}