def r_sqm1

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

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/spec/crypto/ed25519.bend as SE
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/src/crypto/ed25519/point.bend as PT
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/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/rel.bend as RL

145def r_sqm1(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>) -> RL.R(pp, PT.cs_s(PT.consts(xs)), SE.sqm1(1n+pp)):
146  +P = {1n+pp : Nat}
147  +two = PT.lit(xs, F.small(2))
148  +ex = Nat.add(Nat.mul(PW.Fo(one, 250n), WD.sc(PW.blen(p14_bits()), one)), PW.eb(one, p14_bits()))
149  +k = Nat.div(Nat.sub(P, 1n), 4n)
150  +o2 = RL.r_o(pp, two, 2n, r_lit_small(pp, xs, 2, {==}))
151  +r2 = r_lit_small(pp, xs, 2, {==})
152  +c1 = PW.chain_val(one, h1, pp, hP, 249n, p14_bits(), two, o2)
153  +c1b = G.c_trans(pp, FS.value(PT.pow_p14(two)), Nat.pow(FS.value(two), ex), Nat.pow(2n, ex), c1, G.c_pow(pp, FS.value(two), 2n, ex, RL.r_c(pp, two, 2n, r2)))
154  +c2 = G.c_eq(pp, Nat.pow(2n, ex), Nat.pow(2n, k), Equal.cong(Nat, Nat, t => Nat.pow(2n, t), ex, k, p14_exp(one, h1, pp, hP)))
155  +c3 = G.c_sym(pp, FS.fpow(P, 2n, k), Nat.pow(2n, k), G.c_mod(pp, Nat.pow(2n, k)))
156  (PW.pbs_okb(one, h1, p14_bits(), two, F.pow_ones(two, 249n, two), o2, PW.po_okb(one, h1, 249n, two, two, o2, o2)), G.c_trans(pp, FS.value(PT.pow_p14(two)), Nat.pow(2n, ex), FS.fpow(P, 2n, k), c1b, G.c_trans(pp, Nat.pow(2n, ex), Nat.pow(2n, k), FS.fpow(P, 2n, k), c2, c3)))