def p14_exp

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:128

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend as PW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M2

128# 8 Fo(250) + 3 == (p - 1) / 4
129def p14_exp(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(Nat.mul(PW.Fo(one, 250n), WD.sc(PW.blen(p14_bits()), one)), PW.eb(one, p14_bits())) == Nat.div(Nat.sub(1n+pp, 1n), 4n) : Nat}:
130  +F2 = PW.Fo(one, 250n)
131  +P = {1n+pp : Nat}
132  %Equal.sym(Nat, WD.sc(3n, one), 8n, PW.small_one(one, h1, 3n, 8n, {==})) : {Nat.add(Nat.mul(F2, _), PW.eb(one, p14_bits())) == Nat.div(Nat.sub(P, 1n), 4n) : Nat}
133  %Equal.sym(Nat, PW.eb(one, p14_bits()), 3n, eb_p14(one, h1)) : {Nat.add(Nat.mul(F2, 8n), _) == Nat.div(Nat.sub(P, 1n), 4n) : Nat}
134  +e = Nat.add(Nat.mul(F2, 8n), 3n)
135  +m4 = Equal.trans(Nat, Nat.mul(e, 4n), Nat.add(Nat.mul(Nat.mul(F2, 8n), 4n), Nat.mul(3n, 4n)), Nat.add(Nat.mul(F2, 32n), 12n), NA.mul_add_right(Nat.mul(F2, 8n), 3n, 4n), M2.cong_l(Nat.mul(Nat.mul(F2, 8n), 4n), Nat.mul(F2, 32n), Nat.mul(3n, 4n), NA.mul_assoc(F2, 8n, 4n)))
136  +e1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(e, 4n), 1n), 19n), Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(P, 19n), M2.cong_l(Nat.add(Nat.mul(e, 4n), 1n), Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n, M2.cong_l(Nat.mul(e, 4n), Nat.add(Nat.mul(F2, 32n), 12n), 1n, m4)),
137    Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(Nat.mul(F2, 32n), 32n), Nat.add(P, 19n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), 1n), 19n), Nat.add(Nat.add(Nat.mul(F2, 32n), 12n), Nat.add(1n, 19n)), Nat.add(Nat.mul(F2, 32n), 32n), NA.add_assoc(Nat.add(Nat.mul(F2, 32n), 12n), 1n, 19n), NA.add_assoc(Nat.mul(F2, 32n), 12n, 20n)), PW.f32(one, h1, pp, hP)))
138  +e2 = G.cancel_r(Nat.add(Nat.mul(e, 4n), 1n), P, 19n, e1)
139  +e3 = Equal.trans(Nat, P, Nat.add(Nat.mul(e, 4n), 1n), Nat.add(1n, Nat.mul(e, 4n)), Equal.sym(Nat, Nat.add(Nat.mul(e, 4n), 1n), P, e2), NA.add_comm(Nat.mul(e, 4n), 1n))
140  %Equal.sym(Nat, P, Nat.add(1n, Nat.mul(e, 4n)), e3) : {e == Nat.div(Nat.sub(_, 1n), 4n) : Nat}
141  %Equal.sym(Nat, Nat.sub(Nat.add(1n, Nat.mul(e, 4n)), 1n), Nat.mul(e, 4n), N.add_sub_cancel(1n, Nat.mul(e, 4n))) : {e == Nat.div(_, 4n) : Nat}
142  %N.add_zero(Nat.mul(e, 4n)) : {e == Nat.div(_, 4n) : Nat}
143  Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(e, 4n), 0n), 4n), e, NR.div_of(e, 3n, 0n, {==}))