proofs/crypto/curve25519/pow.bend source
proofs/crypto/curve25519/pow.bend on the hub · documented module
import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/curve25519/field.bend as FSimport ../../../src/crypto/curve25519/field.bend as Fimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/word.bend as WDimport ../../lib/arith.bend as ARimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NRimport ./num.bend as Mimport ./limbs.bend as LMimport ./consts.bend as Kimport ./mulw.bend as MWimport ./cong.bend as G# The public-exponent powers of src/crypto/curve25519/field.bend:# pow_ones(n, x, acc) = acc^(2^n) x^(2^n - 1) and pow_bits (square, multiply# on a one bit), hence inv(x) = x^(p - 2) (250 one bits, then 0 1 0 1 1)# and pow_p58(x) = x^((p - 5) / 8) (250 one bits, then 0 1), mod p. The# exponents stay open in the symbolic one (Fo(one, n) + one == 2^n).def v(+x: U32) -> Nat: U32.to_nat(x)# 2^n - 1def Fo(+one: Nat, +n: Nat) -> Nat: Nat.sub(WD.sc(n, one), one)def one_le_sc(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat) -> {Nat.is_le(one, WD.sc(n, one)) == True{} : Bool}: +a = N.lt_succ_le_succ(0n, WD.sc(n, one), LM.sc_pos1(n, one, h1)) L.subst(Nat, o => {Nat.is_le(o, WD.sc(n, one)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), a)def fo_sum(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat) -> {Nat.add(Fo(one, n), one) == WD.sc(n, one) : Nat}: Equal.trans(Nat, Nat.add(Fo(one, n), one), Nat.add(one, Fo(one, n)), WD.sc(n, one), NA.add_comm(Fo(one, n), one), N.sub_add(WD.sc(n, one), one, one_le_sc(one, h1, n)))# (a + c) - b == a + (c - b) for b <= cdef sub_add_r(+a: Nat, +c: Nat, +b: Nat, +h: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.sub(Nat.add(a, c), b) == Nat.add(a, Nat.sub(c, b)) : Nat}: +d = Nat.sub(c, b) +e1 = Equal.cong(Nat, Nat, t => Nat.sub(Nat.add(a, t), b), c, Nat.add(b, d), Equal.sym(Nat, Nat.add(b, d), c, N.sub_add(c, b, h))) +e2 = Equal.cong(Nat, Nat, t => Nat.sub(t, b), Nat.add(a, Nat.add(b, d)), Nat.add(b, Nat.add(a, d)), NA.add_swap(a, b, d)) Equal.trans(Nat, Nat.sub(Nat.add(a, c), b), Nat.sub(Nat.add(a, Nat.add(b, d)), b), Nat.add(a, d), e1, Equal.trans(Nat, Nat.sub(Nat.add(a, Nat.add(b, d)), b), Nat.sub(Nat.add(b, Nat.add(a, d)), b), Nat.add(a, d), e2, N.add_sub_cancel(b, Nat.add(a, d))))# 2^m + (2^m - 1) == 2^(m+1) - 1def fo_step(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat) -> {Nat.add(WD.sc(m, one), Fo(one, m)) == Fo(one, 1n+m) : Nat}: +S = WD.sc(m, one) +e1 = Equal.cong(Nat, Nat, t => Nat.sub(t, one), Nat.double(S), Nat.add(S, S), NA.double_self(S)) Equal.sym(Nat, Nat.sub(Nat.double(S), one), Nat.add(S, Nat.sub(S, one)), Equal.trans(Nat, Nat.sub(Nat.double(S), one), Nat.sub(Nat.add(S, S), one), Nat.add(S, Nat.sub(S, one)), e1, sub_add_r(S, S, one, one_le_sc(one, h1, m))))def bexp(b: Bool) -> Nat: match b: case True{}: 1n case False{}: 0ndef blen(bs: List<&2, Bool>) -> Nat: match bs: case Nil{}: 0n case Con{b, bt}: 1n+blen(bt)# the exponent of x contributed by the bitsdef eb(+one: Nat, bs: List<&2, Bool>) -> Nat: match bs: case Nil{}: 0n case Con{b, +bt}: Nat.add(Nat.mul(bexp(b), WD.sc(blen(bt), one)), eb(one, bt))# ---- unfolding (the loops inspect x first) ----def po_zero(+x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {F.pow_ones(x, 0n, acc) == acc : List<&2, U32>}: match x: case Nil{}: {==} case Con{h, t}: {==}def po_step(+x: List<&2, U32>, +m: Nat, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {F.pow_ones(x, 1n+m, acc) == F.pow_ones(x, m, F.mul(F.sq(acc), x)) : List<&2, U32>}: match x: case Nil{}: Empty.absurd({acc == F.pow_ones(Nil{}, m, F.mul(F.sq(acc), Nil{})) : List<&2, U32>}, L.false_true(hx)) case Con{h, t}: {==}def pbs_nil(+x: List<&2, U32>, +acc: List<&2, U32>) -> {F.pow_bits(x, Nil{}, acc) == acc : List<&2, U32>}: match x: case Nil{}: {==} case Con{h, t}: {==}def pbs_con(+x: List<&2, U32>, +b: Bool, +bt: List<&2, Bool>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {F.pow_bits(x, Con{b, bt}, acc) == F.pow_bits(x, bt, F.pow_bit(b, x, acc)) : List<&2, U32>}: match x: case Nil{}: Empty.absurd({acc == F.pow_bits(Nil{}, bt, F.pow_bit(b, Nil{}, acc)) : List<&2, U32>}, L.false_true(hx)) case Con{h, t}: {==}# ---- shapes ----def po_okb(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> {LM.okb(32n, F.pow_ones(x, n, acc), 255n) == True{} : Bool}: match n: case 0n: %Equal.sym(List<&2, U32>, F.pow_ones(x, 0n, acc), acc, po_zero(x, acc, hx)) : {LM.okb(32n, _, 255n) == True{} : Bool} ha case 1n+ +m: %Equal.sym(List<&2, U32>, F.pow_ones(x, 1n+m, acc), F.pow_ones(x, m, F.mul(F.sq(acc), x)), po_step(x, m, acc, hx)) : {LM.okb(32n, _, 255n) == True{} : Bool} po_okb(one, h1, m, x, F.mul(F.sq(acc), x), hx, MW.mul_okb(one, h1, F.sq(acc), x, MW.sq_okb(one, h1, acc, ha), hx))def pb_okb(+one: Nat, +h1: {one == 1n : Nat}, +b: Bool, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> {LM.okb(32n, F.pow_bit(b, x, acc), 255n) == True{} : Bool}: match b: case True{}: MW.mul_okb(one, h1, F.sq(acc), x, MW.sq_okb(one, h1, acc, ha), hx) case False{}: MW.sq_okb(one, h1, acc, ha)def pbs_okb(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, Bool>, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> {LM.okb(32n, F.pow_bits(x, bs, acc), 255n) == True{} : Bool}: match bs: case Nil{}: %Equal.sym(List<&2, U32>, F.pow_bits(x, Nil{}, acc), acc, pbs_nil(x, acc)) : {LM.okb(32n, _, 255n) == True{} : Bool} ha case Con{+b, +bt}: %Equal.sym(List<&2, U32>, F.pow_bits(x, Con{b, bt}, acc), F.pow_bits(x, bt, F.pow_bit(b, x, acc)), pbs_con(x, b, bt, acc, hx)) : {LM.okb(32n, _, 255n) == True{} : Bool} pbs_okb(one, h1, bt, x, F.pow_bit(b, x, acc), hx, pb_okb(one, h1, b, x, acc, hx, ha))# ---- values ----# acc^2 xdef step_c(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +acc: List<&2, U32>, +x: List<&2, U32>, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.mul(F.sq(acc), x)), Nat.mul(Nat.mul(FS.value(acc), FS.value(acc)), FS.value(x))): +A = FS.value(acc) +X = FS.value(x) +e1 = MW.mul_mod(one, h1, pp, hP, F.sq(acc), x, MW.sq_okb(one, h1, acc, ha), hx) +e2 = G.c_mul(pp, FS.value(F.sq(acc)), Nat.mul(A, A), X, X, MW.sq_mod(one, h1, pp, hP, acc, ha), G.c_refl(pp, X)) G.c_trans(pp, FS.value(F.mul(F.sq(acc), x)), Nat.mul(FS.value(F.sq(acc)), X), Nat.mul(Nat.mul(A, A), X), e1, e2)# a^one * 1 == adef pow_one_one(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat) -> {Nat.mul(Nat.pow(a, one), 1n) == a : Nat}: +e = L.subst(Nat, o => {Nat.pow(a, o) == a : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), NA.mul_one(a)) Equal.trans(Nat, Nat.mul(Nat.pow(a, one), 1n), Nat.pow(a, one), a, NA.mul_one(Nat.pow(a, one)), e)# (a^2 y)^(2^m) z == a^(2^(m+1)) (y^(2^m) z)def sq_pow(+a: Nat, +y: Nat, +s: Nat, +z: Nat, +s2: Nat, +hs: {Nat.add(s, s) == s2 : Nat}) -> {Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), y), s), z) == Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)) : Nat}: +e1 = Equal.cong(Nat, Nat, t => Nat.mul(t, z), Nat.pow(Nat.mul(Nat.mul(a, a), y), s), Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), NR.mul_pow(Nat.mul(a, a), y, s)) +e2a = Equal.trans(Nat, Nat.pow(Nat.mul(a, a), s), Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), Nat.pow(a, s2), NR.mul_pow(a, a, s), Equal.trans(Nat, Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), Nat.pow(a, Nat.add(s, s)), Nat.pow(a, s2), Equal.sym(Nat, Nat.pow(a, Nat.add(s, s)), Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), NR.pow_add(a, s, s)), Equal.cong(Nat, Nat, t => Nat.pow(a, t), Nat.add(s, s), s2, hs))) +e2 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.mul(t, Nat.pow(y, s)), z), Nat.pow(Nat.mul(a, a), s), Nat.pow(a, s2), e2a) +e3 = NA.mul_assoc(Nat.pow(a, s2), Nat.pow(y, s), z) Equal.trans(Nat, Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), y), s), z), Nat.mul(Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), z), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)), e1, Equal.trans(Nat, Nat.mul(Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), z), Nat.mul(Nat.mul(Nat.pow(a, s2), Nat.pow(y, s)), z), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)), e2, e3))def po_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +n: Nat, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.pow_ones(x, n, acc)), Nat.mul(Nat.pow(FS.value(acc), WD.sc(n, one)), Nat.pow(FS.value(x), Fo(one, n)))): match n: case 0n: +A = FS.value(acc) +R = Nat.mul(Nat.pow(A, one), Nat.pow(FS.value(x), Fo(one, 0n))) %Equal.sym(List<&2, U32>, F.pow_ones(x, 0n, acc), acc, po_zero(x, acc, hx)) : G.ceq(pp, FS.value(_), R) +e0 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.pow(A, one), Nat.pow(FS.value(x), t)), Fo(one, 0n), 0n, N.sub_self(one)) G.c_eq(pp, A, R, Equal.sym(Nat, R, A, Equal.trans(Nat, R, Nat.mul(Nat.pow(A, one), 1n), A, e0, pow_one_one(one, h1, A)))) case 1n+ +m: +A = FS.value(acc) +X = FS.value(x) +acc2 = F.mul(F.sq(acc), x) +S = WD.sc(m, one) +Fm = Fo(one, m) +ha2 = MW.mul_okb(one, h1, F.sq(acc), x, MW.sq_okb(one, h1, acc, ha), hx) +ih = po_val(one, h1, pp, hP, m, x, acc2, hx, ha2) %Equal.sym(List<&2, U32>, F.pow_ones(x, 1n+m, acc), F.pow_ones(x, m, acc2), po_step(x, m, acc, hx)) : G.ceq(pp, FS.value(_), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Fo(one, 1n+m)))) +e1 = G.c_mul(pp, Nat.pow(FS.value(acc2), S), Nat.pow(Nat.mul(Nat.mul(A, A), X), S), Nat.pow(X, Fm), Nat.pow(X, Fm), G.c_pow(pp, FS.value(acc2), Nat.mul(Nat.mul(A, A), X), S, step_c(one, h1, pp, hP, acc, x, ha, hx)), G.c_refl(pp, Nat.pow(X, Fm))) +e2 = sq_pow(A, X, S, Nat.pow(X, Fm), WD.sc(1n+m, one), M.sc_dbl(m, one)) +e3 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), t), Nat.mul(Nat.pow(X, S), Nat.pow(X, Fm)), Nat.pow(X, Nat.add(S, Fm)), Equal.sym(Nat, Nat.pow(X, Nat.add(S, Fm)), Nat.mul(Nat.pow(X, S), Nat.pow(X, Fm)), NR.pow_add(X, S, Fm))) +fin = G.c_trans(pp, FS.value(F.pow_ones(x, m, acc2)), Nat.mul(Nat.pow(FS.value(acc2), S), Nat.pow(X, Fm)), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), ih, G.c_trans(pp, Nat.mul(Nat.pow(FS.value(acc2), S), Nat.pow(X, Fm)), Nat.mul(Nat.pow(Nat.mul(Nat.mul(A, A), X), S), Nat.pow(X, Fm)), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), e1, G.c_eq(pp, Nat.mul(Nat.pow(Nat.mul(Nat.mul(A, A), X), S), Nat.pow(X, Fm)), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), Equal.trans(Nat, Nat.mul(Nat.pow(Nat.mul(Nat.mul(A, A), X), S), Nat.pow(X, Fm)), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.mul(Nat.pow(X, S), Nat.pow(X, Fm))), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), e2, e3)))) G.c_trans(pp, FS.value(F.pow_ones(x, m, acc2)), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Fo(one, 1n+m))), fin, G.c_eq(pp, Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Nat.add(S, Fm))), Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, Fo(one, 1n+m))), Equal.cong(Nat, Nat, t => Nat.mul(Nat.pow(A, WD.sc(1n+m, one)), Nat.pow(X, t)), Nat.add(S, Fm), Fo(one, 1n+m), fo_step(one, h1, m))))def pb_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +b: Bool, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.pow_bit(b, x, acc)), Nat.mul(Nat.mul(FS.value(acc), FS.value(acc)), Nat.pow(FS.value(x), bexp(b)))): match b: case True{}: +A = FS.value(acc) +X = FS.value(x) G.c_trans(pp, FS.value(F.mul(F.sq(acc), x)), Nat.mul(Nat.mul(A, A), X), Nat.mul(Nat.mul(A, A), Nat.pow(X, 1n)), step_c(one, h1, pp, hP, acc, x, ha, hx), G.c_eq(pp, Nat.mul(Nat.mul(A, A), X), Nat.mul(Nat.mul(A, A), Nat.pow(X, 1n)), Equal.cong(Nat, Nat, t => Nat.mul(Nat.mul(A, A), t), X, Nat.pow(X, 1n), Equal.sym(Nat, Nat.mul(X, 1n), X, NA.mul_one(X))))) case False{}: +A = FS.value(acc) G.c_trans(pp, FS.value(F.sq(acc)), Nat.mul(A, A), Nat.mul(Nat.mul(A, A), 1n), MW.sq_mod(one, h1, pp, hP, acc, ha), G.c_eq(pp, Nat.mul(A, A), Nat.mul(Nat.mul(A, A), 1n), Equal.sym(Nat, Nat.mul(Nat.mul(A, A), 1n), Nat.mul(A, A), NA.mul_one(Nat.mul(A, A)))))# (a^2 x^e)^s y == a^(2 s) x^(e s) ydef bit_pow(+a: Nat, +x: Nat, +e: Nat, +s: Nat, +z: Nat, +s2: Nat, +hs: {Nat.add(s, s) == s2 : Nat}) -> {Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), Nat.pow(x, e)), s), Nat.pow(x, z)) == Nat.mul(Nat.pow(a, s2), Nat.pow(x, Nat.add(Nat.mul(e, s), z))) : Nat}: +e1 = sq_pow(a, Nat.pow(x, e), s, Nat.pow(x, z), s2, hs) +e2 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.pow(a, s2), Nat.mul(t, Nat.pow(x, z))), Nat.pow(Nat.pow(x, e), s), Nat.pow(x, Nat.mul(e, s)), G.pow_pow(x, e, s)) +e3 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.pow(a, s2), t), Nat.mul(Nat.pow(x, Nat.mul(e, s)), Nat.pow(x, z)), Nat.pow(x, Nat.add(Nat.mul(e, s), z)), Equal.sym(Nat, Nat.pow(x, Nat.add(Nat.mul(e, s), z)), Nat.mul(Nat.pow(x, Nat.mul(e, s)), Nat.pow(x, z)), NR.pow_add(x, Nat.mul(e, s), z))) Equal.trans(Nat, Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), Nat.pow(x, e)), s), Nat.pow(x, z)), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(Nat.pow(x, e), s), Nat.pow(x, z))), Nat.mul(Nat.pow(a, s2), Nat.pow(x, Nat.add(Nat.mul(e, s), z))), e1, Equal.trans(Nat, Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(Nat.pow(x, e), s), Nat.pow(x, z))), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(x, Nat.mul(e, s)), Nat.pow(x, z))), Nat.mul(Nat.pow(a, s2), Nat.pow(x, Nat.add(Nat.mul(e, s), z))), e2, e3))def pbs_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +bs: List<&2, Bool>, +x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +ha: {LM.okb(32n, acc, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.pow_bits(x, bs, acc)), Nat.mul(Nat.pow(FS.value(acc), WD.sc(blen(bs), one)), Nat.pow(FS.value(x), eb(one, bs)))): match bs: case Nil{}: %Equal.sym(List<&2, U32>, F.pow_bits(x, Nil{}, acc), acc, pbs_nil(x, acc)) : G.ceq(pp, FS.value(_), Nat.mul(Nat.pow(FS.value(acc), one), 1n)) G.c_eq(pp, FS.value(acc), Nat.mul(Nat.pow(FS.value(acc), one), 1n), Equal.sym(Nat, Nat.mul(Nat.pow(FS.value(acc), one), 1n), FS.value(acc), pow_one_one(one, h1, FS.value(acc)))) case Con{+b, +bt}: +A = FS.value(acc) +X = FS.value(x) +acc2 = F.pow_bit(b, x, acc) +S = WD.sc(blen(bt), one) +Z = eb(one, bt) +E = bexp(b) +ha2 = pb_okb(one, h1, b, x, acc, hx, ha) +ih = pbs_val(one, h1, pp, hP, bt, x, acc2, hx, ha2) %Equal.sym(List<&2, U32>, F.pow_bits(x, Con{b, bt}, acc), F.pow_bits(x, bt, acc2), pbs_con(x, b, bt, acc, hx)) : G.ceq(pp, FS.value(_), Nat.mul(Nat.pow(A, WD.sc(1n+blen(bt), one)), Nat.pow(X, Nat.add(Nat.mul(E, S), Z)))) +e1 = G.c_mul(pp, Nat.pow(FS.value(acc2), S), Nat.pow(Nat.mul(Nat.mul(A, A), Nat.pow(X, E)), S), Nat.pow(X, Z), Nat.pow(X, Z), G.c_pow(pp, FS.value(acc2), Nat.mul(Nat.mul(A, A), Nat.pow(X, E)), S, pb_val(one, h1, pp, hP, b, x, acc, hx, ha)), G.c_refl(pp, Nat.pow(X, Z))) +e2 = bit_pow(A, X, E, S, Z, WD.sc(1n+blen(bt), one), M.sc_dbl(blen(bt), one)) G.c_trans(pp, FS.value(F.pow_bits(x, bt, acc2)), Nat.mul(Nat.pow(FS.value(acc2), S), Nat.pow(X, Z)), Nat.mul(Nat.pow(A, WD.sc(1n+blen(bt), one)), Nat.pow(X, Nat.add(Nat.mul(E, S), Z))), ih, G.c_trans(pp, Nat.mul(Nat.pow(FS.value(acc2), S), Nat.pow(X, Z)), Nat.mul(Nat.pow(Nat.mul(Nat.mul(A, A), Nat.pow(X, E)), S), Nat.pow(X, Z)), Nat.mul(Nat.pow(A, WD.sc(1n+blen(bt), one)), Nat.pow(X, Nat.add(Nat.mul(E, S), Z))), e1, G.c_eq(pp, Nat.mul(Nat.pow(Nat.mul(Nat.mul(A, A), Nat.pow(X, E)), S), Nat.pow(X, Z)), Nat.mul(Nat.pow(A, WD.sc(1n+blen(bt), one)), Nat.pow(X, Nat.add(Nat.mul(E, S), Z))), e2)))# ---- x^(Fo(250) 2^k + e) ----# pow_bits(x, bs, pow_ones(x, n, x)) == x^(Fo(n + 1) 2^len + eb)def chain_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +n: Nat, +bs: List<&2, Bool>, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.pow_bits(x, bs, F.pow_ones(x, n, x))), Nat.pow(FS.value(x), Nat.add(Nat.mul(Fo(one, 1n+n), WD.sc(blen(bs), one)), eb(one, bs)))): +X = FS.value(x) +a1 = F.pow_ones(x, n, x) +F2 = Fo(one, 1n+n) +S = WD.sc(blen(bs), one) +ha1 = po_okb(one, h1, n, x, x, hx, hx) +e1 = po_val(one, h1, pp, hP, n, x, x, hx, hx) +e1b = Equal.trans(Nat, Nat.mul(Nat.pow(X, WD.sc(n, one)), Nat.pow(X, Fo(one, n))), Nat.pow(X, Nat.add(WD.sc(n, one), Fo(one, n))), Nat.pow(X, F2), Equal.sym(Nat, Nat.pow(X, Nat.add(WD.sc(n, one), Fo(one, n))), Nat.mul(Nat.pow(X, WD.sc(n, one)), Nat.pow(X, Fo(one, n))), NR.pow_add(X, WD.sc(n, one), Fo(one, n))), Equal.cong(Nat, Nat, t => Nat.pow(X, t), Nat.add(WD.sc(n, one), Fo(one, n)), F2, fo_step(one, h1, n))) +v1 = G.c_trans(pp, FS.value(a1), Nat.mul(Nat.pow(X, WD.sc(n, one)), Nat.pow(X, Fo(one, n))), Nat.pow(X, F2), e1, G.c_eq(pp, Nat.mul(Nat.pow(X, WD.sc(n, one)), Nat.pow(X, Fo(one, n))), Nat.pow(X, F2), e1b)) +e2 = pbs_val(one, h1, pp, hP, bs, x, a1, hx, ha1) +e3 = G.c_mul(pp, Nat.pow(FS.value(a1), S), Nat.pow(Nat.pow(X, F2), S), Nat.pow(X, eb(one, bs)), Nat.pow(X, eb(one, bs)), G.c_pow(pp, FS.value(a1), Nat.pow(X, F2), S, v1), G.c_refl(pp, Nat.pow(X, eb(one, bs)))) +e4 = Equal.trans(Nat, Nat.mul(Nat.pow(Nat.pow(X, F2), S), Nat.pow(X, eb(one, bs))), Nat.mul(Nat.pow(X, Nat.mul(F2, S)), Nat.pow(X, eb(one, bs))), Nat.pow(X, Nat.add(Nat.mul(F2, S), eb(one, bs))), Equal.cong(Nat, Nat, t => Nat.mul(t, Nat.pow(X, eb(one, bs))), Nat.pow(Nat.pow(X, F2), S), Nat.pow(X, Nat.mul(F2, S)), G.pow_pow(X, F2, S)), Equal.sym(Nat, Nat.pow(X, Nat.add(Nat.mul(F2, S), eb(one, bs))), Nat.mul(Nat.pow(X, Nat.mul(F2, S)), Nat.pow(X, eb(one, bs))), NR.pow_add(X, Nat.mul(F2, S), eb(one, bs)))) G.c_trans(pp, FS.value(F.pow_bits(x, bs, a1)), Nat.mul(Nat.pow(FS.value(a1), S), Nat.pow(X, eb(one, bs))), Nat.pow(X, Nat.add(Nat.mul(F2, S), eb(one, bs))), e2, G.c_trans(pp, Nat.mul(Nat.pow(FS.value(a1), S), Nat.pow(X, eb(one, bs))), Nat.mul(Nat.pow(Nat.pow(X, F2), S), Nat.pow(X, eb(one, bs))), Nat.pow(X, Nat.add(Nat.mul(F2, S), eb(one, bs))), e3, G.c_eq(pp, Nat.mul(Nat.pow(Nat.pow(X, F2), S), Nat.pow(X, eb(one, bs))), Nat.pow(X, Nat.add(Nat.mul(F2, S), eb(one, bs))), e4)))# ---- the exponents ----def cancel_r(+a: Nat, +b: Nat, +c: Nat, +e: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}: NR.add_cancel(c, a, b, Equal.trans(Nat, Nat.add(c, a), Nat.add(a, c), Nat.add(c, b), NA.add_comm(c, a), Equal.trans(Nat, Nat.add(a, c), Nat.add(b, c), Nat.add(c, b), e, NA.add_comm(b, c))))# 32 Fo(250) + 32 == p + 19def f32(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(Nat.mul(Fo(one, 250n), 32n), 32n) == Nat.add(1n+pp, 19n) : Nat}: +F2 = Fo(one, 250n) +e1 = Equal.trans(Nat, Nat.add(Nat.mul(F2, 32n), 32n), Nat.add(Nat.mul(F2, 32n), Nat.mul(one, 32n)), Nat.mul(Nat.add(F2, one), 32n), M.cong_r(Nat.mul(F2, 32n), 32n, Nat.mul(one, 32n), Equal.sym(Nat, Nat.mul(one, 32n), 32n, K.one_k(one, h1, 32n))), Equal.sym(Nat, Nat.mul(Nat.add(F2, one), 32n), Nat.add(Nat.mul(F2, 32n), Nat.mul(one, 32n)), NA.mul_add_right(F2, one, 32n))) +e2 = Equal.cong(Nat, Nat, t => Nat.mul(t, 32n), Nat.add(F2, one), WD.sc(250n, one), fo_sum(one, h1, 250n)) +e3 = AR.mul_sc(5n, WD.sc(250n, one)) Equal.trans(Nat, Nat.add(Nat.mul(F2, 32n), 32n), Nat.mul(Nat.add(F2, one), 32n), Nat.add(1n+pp, 19n), e1, Equal.trans(Nat, Nat.mul(Nat.add(F2, one), 32n), Nat.mul(WD.sc(250n, one), 32n), Nat.add(1n+pp, 19n), e2, Equal.trans(Nat, Nat.mul(WD.sc(250n, one), 32n), WD.sc(255n, one), Nat.add(1n+pp, 19n), e3, Equal.sym(Nat, Nat.add(1n+pp, 19n), WD.sc(255n, one), hP))))def small_one(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +a: Nat, +ha: {WD.sc(k, 1n) == a : Nat}) -> {WD.sc(k, one) == a : Nat}: L.subst(Nat, o => {WD.sc(k, o) == a : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), ha)def inv_bits() -> List<&2, Bool>: [False{}, True{}, False{}, True{}, True{}]def p58_bits() -> List<&2, Bool>: [False{}, True{}]def eb_inv(+one: Nat, +h1: {one == 1n : Nat}) -> {eb(one, inv_bits()) == 11n : Nat}: L.subst(Nat, o => {eb(o, inv_bits()) == 11n : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})def eb_p58(+one: Nat, +h1: {one == 1n : Nat}) -> {eb(one, p58_bits()) == 1n : Nat}: L.subst(Nat, o => {eb(o, p58_bits()) == 1n : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})# 32 Fo(250) + 11 == p - 2def inv_exp(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(Nat.mul(Fo(one, 250n), WD.sc(blen(inv_bits()), one)), eb(one, inv_bits())) == Nat.sub(1n+pp, 2n) : Nat}: +F2 = Fo(one, 250n) +P = {1n+pp : Nat} %Equal.sym(Nat, WD.sc(5n, one), 32n, small_one(one, h1, 5n, 32n, {==})) : {Nat.add(Nat.mul(F2, _), eb(one, inv_bits())) == Nat.sub(P, 2n) : Nat} %Equal.sym(Nat, eb(one, inv_bits()), 11n, eb_inv(one, h1)) : {Nat.add(Nat.mul(F2, 32n), _) == Nat.sub(P, 2n) : Nat} +x = Nat.add(Nat.mul(F2, 32n), 11n) +e1 = Equal.trans(Nat, Nat.add(Nat.add(x, 2n), 19n), Nat.add(Nat.mul(F2, 32n), 32n), Nat.add(P, 19n), Equal.trans(Nat, Nat.add(Nat.add(x, 2n), 19n), Nat.add(x, Nat.add(2n, 19n)), Nat.add(Nat.mul(F2, 32n), 32n), NA.add_assoc(x, 2n, 19n), NA.add_assoc(Nat.mul(F2, 32n), 11n, 21n)), f32(one, h1, pp, hP)) +e2 = cancel_r(Nat.add(x, 2n), P, 19n, e1) +e3 = Equal.trans(Nat, P, Nat.add(x, 2n), Nat.add(2n, x), Equal.sym(Nat, Nat.add(x, 2n), P, e2), NA.add_comm(x, 2n)) %Equal.sym(Nat, P, Nat.add(2n, x), e3) : {x == Nat.sub(_, 2n) : Nat} Equal.sym(Nat, Nat.sub(Nat.add(2n, x), 2n), x, N.add_sub_cancel(2n, x))# 4 Fo(250) + 1 == (p - 5) / 8def p58_exp(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(Nat.mul(Fo(one, 250n), WD.sc(blen(p58_bits()), one)), eb(one, p58_bits())) == Nat.div(Nat.sub(1n+pp, 5n), 8n) : Nat}: +F2 = Fo(one, 250n) +P = {1n+pp : Nat} %Equal.sym(Nat, WD.sc(2n, one), 4n, small_one(one, h1, 2n, 4n, {==})) : {Nat.add(Nat.mul(F2, _), eb(one, p58_bits())) == Nat.div(Nat.sub(P, 5n), 8n) : Nat} %Equal.sym(Nat, eb(one, p58_bits()), 1n, eb_p58(one, h1)) : {Nat.add(Nat.mul(F2, 4n), _) == Nat.div(Nat.sub(P, 5n), 8n) : Nat} +e = Nat.add(Nat.mul(F2, 4n), 1n) +m8 = Equal.trans(Nat, Nat.mul(e, 8n), Nat.add(Nat.mul(Nat.mul(F2, 4n), 8n), Nat.mul(1n, 8n)), Nat.add(Nat.mul(F2, 32n), 8n), NA.mul_add_right(Nat.mul(F2, 4n), 1n, 8n), M.cong_l(Nat.mul(Nat.mul(F2, 4n), 8n), Nat.mul(F2, 32n), Nat.mul(1n, 8n), NA.mul_assoc(F2, 4n, 8n))) +e1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(e, 8n), 5n), 19n), Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 8n), 5n), 19n), Nat.add(P, 19n), M.cong_l(Nat.add(Nat.mul(e, 8n), 5n), Nat.add(Nat.add(Nat.mul(F2, 32n), 8n), 5n), 19n, M.cong_l(Nat.mul(e, 8n), Nat.add(Nat.mul(F2, 32n), 8n), 5n, m8)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(F2, 32n), 8n), 5n), 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), 8n), 5n), 19n), Nat.add(Nat.add(Nat.mul(F2, 32n), 8n), Nat.add(5n, 19n)), Nat.add(Nat.mul(F2, 32n), 32n), NA.add_assoc(Nat.add(Nat.mul(F2, 32n), 8n), 5n, 19n), NA.add_assoc(Nat.mul(F2, 32n), 8n, 24n)), f32(one, h1, pp, hP))) +e2 = cancel_r(Nat.add(Nat.mul(e, 8n), 5n), P, 19n, e1) +e3 = Equal.trans(Nat, P, Nat.add(Nat.mul(e, 8n), 5n), Nat.add(5n, Nat.mul(e, 8n)), Equal.sym(Nat, Nat.add(Nat.mul(e, 8n), 5n), P, e2), NA.add_comm(Nat.mul(e, 8n), 5n)) %Equal.sym(Nat, P, Nat.add(5n, Nat.mul(e, 8n)), e3) : {e == Nat.div(Nat.sub(_, 5n), 8n) : Nat} %Equal.sym(Nat, Nat.sub(Nat.add(5n, Nat.mul(e, 8n)), 5n), Nat.mul(e, 8n), N.add_sub_cancel(5n, Nat.mul(e, 8n))) : {e == Nat.div(_, 8n) : Nat} %N.add_zero(Nat.mul(e, 8n)) : {e == Nat.div(_, 8n) : Nat} Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(e, 8n), 0n), 8n), e, NR.div_of(e, 7n, 0n, {==}))# ---- inv and pow_p58 ----def inv_okb(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {LM.okb(32n, F.inv(x), 255n) == True{} : Bool}: pbs_okb(one, h1, inv_bits(), x, F.pow_ones(x, 249n, x), hx, po_okb(one, h1, 249n, x, x, hx, hx))def p58_okb(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {LM.okb(32n, F.pow_p58(x), 255n) == True{} : Bool}: pbs_okb(one, h1, p58_bits(), x, F.pow_ones(x, 249n, x), hx, po_okb(one, h1, 249n, x, x, hx, hx))def inv_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.inv(x)), Nat.pow(FS.value(x), Nat.sub(1n+pp, 2n))): +ex = Nat.add(Nat.mul(Fo(one, 250n), WD.sc(blen(inv_bits()), one)), eb(one, inv_bits())) G.c_trans(pp, FS.value(F.inv(x)), Nat.pow(FS.value(x), ex), Nat.pow(FS.value(x), Nat.sub(1n+pp, 2n)), chain_val(one, h1, pp, hP, 249n, inv_bits(), x, hx), G.c_eq(pp, Nat.pow(FS.value(x), ex), Nat.pow(FS.value(x), Nat.sub(1n+pp, 2n)), Equal.cong(Nat, Nat, t => Nat.pow(FS.value(x), t), ex, Nat.sub(1n+pp, 2n), inv_exp(one, h1, pp, hP))))def p58_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.pow_p58(x)), Nat.pow(FS.value(x), Nat.div(Nat.sub(1n+pp, 5n), 8n))): +ex = Nat.add(Nat.mul(Fo(one, 250n), WD.sc(blen(p58_bits()), one)), eb(one, p58_bits())) G.c_trans(pp, FS.value(F.pow_p58(x)), Nat.pow(FS.value(x), ex), Nat.pow(FS.value(x), Nat.div(Nat.sub(1n+pp, 5n), 8n)), chain_val(one, h1, pp, hP, 249n, p58_bits(), x, hx), G.c_eq(pp, Nat.pow(FS.value(x), ex), Nat.pow(FS.value(x), Nat.div(Nat.sub(1n+pp, 5n), 8n)), Equal.cong(Nat, Nat, t => Nat.pow(FS.value(x), t), ex, Nat.div(Nat.sub(1n+pp, 5n), 8n), p58_exp(one, h1, pp, hP))))