~/bend-docscommunity

proofs/math/typed/u64mont.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as U64mont

26 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64m128.bend as M128
import ./w64dm.bend as DM
import ./natlight.bend as AQ
import ./montnat.bend as MN
import ./w64dmrem.bend as DR
import ../../lib/u32.bend as U
import ../u64/u64div.bend as PD
import ./w64mm.bend as MM
import ../../../src/math/natural.bend as M
import ../natural/sqrtn.bend as SQ2

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def b32v source · line 34 · raw

@c:Bool -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(c) : Nat}

def true_ne_false source · line 41 · raw

@+h:{True{} == False{} : Bool} -> Empty

def shl_inv_c source · line 45 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {c == True{} : Bool}

shift(k, a) < shift(k, b) gives a < b

def shl_inv source · line 53 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def ones_v source · line 57 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:U32 -> @+pw:{w == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{w, w}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat}

the all-ones word is 2^64 - 1

def m128v source · line 72 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(p, q))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(p, q))))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q)) : Nat}

the full product's two words

def sif_c source · line 79 · raw

@+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hr:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool} -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(m, r) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub_if(r, m, c)) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 1n+bp) : Nat}

sub_if: r < 2 m gives r mod m

def sif source · line 95 · raw

@+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hr:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_r(m, r)) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r), 1n+bp) : Nat}

def swap4 source · line 98 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}

def rp_low source · line 103 · raw

@+one:Nat -> @+bp:Nat -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl))) : Nat}

the low words of t + u m cancel: tl + pl == 2^64 carry

def rp_eq source · line 110 · raw

@+one:Nat -> @+bp:Nat -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl)))) == Nat.add(T, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp)) : Nat}

2^64 r' == t + u m for r' = th + ph + carry

def rp_lt_g source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+hb:{Nat.is_lt(0n, b) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+hT:{Nat.is_lt(T, Nat.mul(b, b)) == True{} : Bool} -> @+h63:{Nat.is_lt(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+er:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl)))) == Nat.add(T, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), b)) : Nat} -> {Nat.is_lt(Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl))), Nat.add(b, b)) == True{} : Bool}

r' < 2 m, for t < m^2 and m < 2^63 rp_lt over b = 1 + bp: with the literal successor, 2^64 * (1 + bp) would unfold into 2^64 successors in the checker

def rp_lt source · line 132 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl))), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}

def lt_mul source · line 137 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> @+hc:{Nat.is_lt(0n, c) == True{} : Bool} -> {Nat.is_lt(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}

a < b and c > 0 give a c < b c

def mm64 source · line 143 · raw

@+one:Nat -> @+bp:Nat -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> {Nat.is_lt(Nat.add(1n+bp, 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one)) == True{} : Bool}

m + m < 2^64

def fit_lt source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, x) == True{} : Bool}

def rp_val source · line 151 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(th, ph), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl)), 0})) == Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl))) : Nat}

the word r' of redc_p

def rp_mod source · line 162 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_p(m, tl, th, (pl, ph))) == Nat.mod(Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(tl, pl))), 1n+bp) : Nat}

redc_p is r' mod m

def rp_lt_m source · line 168 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_p(m, tl, th, (pl, ph))), 1n+bp) == True{} : Bool}

redc_p is below m and is t / 2^64 (mod m)

def rp_cong source · line 171 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+pl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ph:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(pl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ph))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_p(m, tl, th, (pl, ph)))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}

def rpp_lt source · line 175 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(p)))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_p(m, tl, th, p)), 1n+bp) == True{} : Bool}

def rpp_cong source · line 180 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+tl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+th:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(tl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(th))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> @+eP:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(p)))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(tl, mp)), 1n+bp) : Nat} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc_p(m, tl, th, p))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}

def ep_m source · line 185 · raw

@+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+u:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(u, m))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(u, m))))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(u), 1n+bp) : Nat}

def rd_lt source · line 188 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @t:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(t)))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc(m, mp, t)), 1n+bp) == True{} : Bool}

def rd_cong source · line 193 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @t:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+T:Nat -> @+eT:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(t)))) == T : Nat} -> @+hT:{Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.redc(m, mp, t))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}

def ab_lt source · line 198 · raw

@+bp:Nat -> @+a:Nat -> @+b:Nat -> @+ha:{Nat.is_lt(a, 1n+bp) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 1n+bp) == True{} : Bool} -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}

def mont_lt source · line 202 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 1n+bp) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 1n+bp) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont(m, mp, a, b)), 1n+bp) == True{} : Bool}

Montgomery multiplication: mont(a, b) < m and mont(a, b) 2^64 == a b (mod m)

def mont_cong source · line 205 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 1n+bp) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 1n+bp) == True{} : Bool} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont(m, mp, a, b))), 1n+bp) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)), 1n+bp) : Nat}

def mlt source · line 209 · raw

@+bp:Nat -> @+x:Nat -> {Nat.is_lt(Nat.mod(x, 1n+bp), 1n+bp) == True{} : Bool}

def smul source · line 212 · raw

@+x:Nat -> @+y:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.mul(x, y))) : Nat}

def mform source · line 216 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+hh:Nat -> @+hH:{2n+bp == Nat.add(hh, hh) : Nat} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+an:Nat -> @+bn:Nat -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, an), 1n+bp) : Nat} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, bn), 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont(m, mp, a, b)) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp) : Nat}

on Montgomery forms: mont(a R, b R) == (a b mod m) R (mod m)

def mbit_v source · line 226 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+hh:Nat -> @+hH:{2n+bp == Nat.add(hh, hh) : Nat} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+acc:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bn:Nat -> @+an:Nat -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, bn), 1n+bp) : Nat} -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(acc) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, an), 1n+bp) : Nat} -> @+d:Nat -> @+o:Bool -> @+hd:{Nat.is_lt(d, 2n) == True{} : Bool} -> @+ho:{o == Nat.is_eq(d, 1n) : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mbit(o, m, mp, b, acc)) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+bp, d, bn, an)), 1n+bp) : Nat}

def izv source · line 239 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a) == n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(a) == Nat.is_eq(n, 0n) : Bool}

def msim source · line 243 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+hh:Nat -> @+hH:{2n+bp == Nat.add(hh, hh) : Nat} -> @+f:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+acc:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bn:Nat -> @+an:Nat -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, bn), 1n+bp) : Nat} -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(acc) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, an), 1n+bp) : Nat} -> @+ez:Bool -> @+ne:Nat -> @+hez:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(e) == ez : Bool} -> @+hne:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(e) == ne : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mpow_go(f, m, mp, b, acc, (e, ez))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f, 1n+bp, ne, bn, an)), 1n+bp) : Nat}

the Montgomery loop computes pow_mod_go on the forms

def not_t source · line 266 · raw

@+x:Bool -> @+h:{Bool.not(x) == True{} : Bool} -> {x == False{} : Bool}

def to_mont_v source · line 274 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hx:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x), 1n+bp) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.to_mont(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x)), 1n+bp) : Nat}

x 2^64 mod m by two 2^32 reductions

def pmo_lt source · line 282 · raw

@+bp:Nat -> @+d:Nat -> @+base:Nat -> @+acc:Nat -> @+ha:{Nat.is_lt(acc, 1n+bp) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+bp, d, base, acc), 1n+bp) == True{} : Bool}

def pm_lt source · line 289 · raw

@+bp:Nat -> @+f:Nat -> @+e:Nat -> @+base:Nat -> @+acc:Nat -> @+ha:{Nat.is_lt(acc, 1n+bp) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(f, 1n+bp, e, base, acc), 1n+bp) == True{} : Bool}

def two_le_k source · line 301 · raw

@+k:Nat -> @+lo:Nat -> @+h:Nat -> @+hh:{Nat.is_eq(h, 0n) == False{} : Bool} -> {Nat.is_le(2n, Nat.add(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+k, h))) == True{} : Bool}

2 <= m for a nonzero high word 2 <= lo + 2^(1+k) h for h > 0, over an open width (k is 31 at the use): a closed 2^32 in a goal is expanded by the checker

def two_le source · line 309 · raw

@+ml:U32 -> @+mh:U32 -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> {Nat.is_le(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})) == True{} : Bool}

def mpow_v source · line 314 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+mp:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hodd:{Nat.mod(1n+bp, 2n) == 1n : Nat} -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mp))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat} -> @+h63:{Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool} -> @+hz:{U32.is_zero(mh) == False{} : Bool} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 1n+bp) == True{} : Bool} -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mpow_m(b, e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, mp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(140n, 1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), Nat.mod(1n, 1n+bp)) : Nat}

the Montgomery pow_mod is pow_mod_go on the values

def mok_ab source · line 342 · raw

@+ml:U32 -> @+mh:U32 -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.odd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.minv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{4294967295, 4294967295})) == True{} : Bool}

what mont_ok(m) gives

def mok_cd source · line 345 · raw

@+ml:U32 -> @+mh:U32 -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {Bool.and(Bool.not(U32.is_zero(mh)), U32.is_lt(mh, 2147483648)) == True{} : Bool}

def mok_odd source · line 348 · raw

@+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {Nat.mod(1n+bp, 2n) == 1n : Nat}

def mok_inv_o source · line 354 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+o:U32 -> @+po:{o == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> @+heq:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.minv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{o, o}) == True{} : Bool} -> {1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.minv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat}

over an open all-ones word o: a literal 2^64 - 1 under SW.value would be expanded in unary by any conversion that unfolds it

def mok_inv source · line 362 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.minv(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, one) : Nat}

def mok_hz source · line 365 · raw

@+ml:U32 -> @+mh:U32 -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {U32.is_zero(mh) == False{} : Bool}

def mok_63_c source · line 369 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> @+hlt:{U32.is_lt(mh, c) == True{} : Bool} -> {Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool}

over an open 2^31 word c: comparisons never meet the literal

def mok_63 source · line 381 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+ml:U32 -> @+mh:U32 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == 1n+bp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{ml, mh}) == True{} : Bool} -> {Nat.is_lt(1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool}

def mpow_top source · line 385 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hM:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(m) == 1n+bp : Nat} -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mont_ok(m) == True{} : Bool} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mpow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.rem(b, m), e, m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_go(140n, 1n+bp, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(e), Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 1n+bp), Nat.mod(1n, 1n+bp)) : Nat}

pow_mod through Montgomery multiplication when mont_ok(m)