def po_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/pow.bend:152

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
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/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as MW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G

152def 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)))):
153  match n:
154    case 0n:
155      +A = FS.value(acc)
156      +R = Nat.mul(Nat.pow(A, one), Nat.pow(FS.value(x), Fo(one, 0n)))
157      %Equal.sym(List<&2, U32>, F.pow_ones(x, 0n, acc), acc, po_zero(x, acc, hx)) : G.ceq(pp, FS.value(_), R)
158      +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))
159      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))))
160    case 1n+ +m:
161      +A = FS.value(acc)
162      +X = FS.value(x)
163      +acc2 = F.mul(F.sq(acc), x)
164      +S = WD.sc(m, one)
165      +Fm = Fo(one, m)
166      +ha2 = MW.mul_okb(one, h1, F.sq(acc), x, MW.sq_okb(one, h1, acc, ha), hx)
167      +ih = po_val(one, h1, pp, hP, m, x, acc2, hx, ha2)
168      %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))))
169      +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)))
170      +e2 = sq_pow(A, X, S, Nat.pow(X, Fm), WD.sc(1n+m, one), M.sc_dbl(m, one))
171      +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)))
172      +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,
173        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))))
174      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))))