def cbn_pow

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/mulw.bend:36

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/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL

36def cbn_pow(+j: Nat, +k: Nat) -> {PL.cbn(WD.sc(j, 1n), k) == WD.sc(j, k) : Nat}:
37  match j:
38    case 0n:
39      N.add_zero(k)
40    case 1n+ +q:
41      +n = WD.sc(q, 1n)
42      +e1 = Equal.cong(Nat, Nat, t => PL.cbn(t, k), Nat.double(n), Nat.add(n, n), NA.double_self(n))
43      +e2 = cbn_add(n, n, k)
44      +e3 = M.cong_add(PL.cbn(n, k), WD.sc(q, k), PL.cbn(n, k), WD.sc(q, k), cbn_pow(q, k), cbn_pow(q, k))
45      Equal.trans(Nat, PL.cbn(Nat.double(n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), WD.sc(1n+q, k), Equal.trans(Nat, PL.cbn(Nat.double(n), k), PL.cbn(Nat.add(n, n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), e1, e2), Equal.trans(Nat, Nat.add(PL.cbn(n, k), PL.cbn(n, k)), Nat.add(WD.sc(q, k), WD.sc(q, k)), WD.sc(1n+q, k), e3, M.sc_dbl(q, k)))