def encode_rel

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

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/curve25519/x25519.bend as SX
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/rel.bend as RL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR

223def encode_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +sp: SE.EPt, +hp: PR.Rp(pp, p, sp)) -> {PT.encode(p) == SE.encode_n(32n, 1n+pp, sp) : List<&2, U32>}:
224  match p sp:
225    case PT.Pt{+x, +y, +z, +t} SE.EPt{+a, +b, +c, +d}:
226      +P = {1n+pp : Nat}
227      +rx = PR.rX(pp, x, y, z, t, a, b, c, d, hp)
228      +ry = PR.rY(pp, x, y, z, t, a, b, c, d, hp)
229      +rz = PR.rZ(pp, x, y, z, t, a, b, c, d, hp)
230      +zi = F.inv(z)
231      +ZI = FS.finv(P, c)
232      +rzi = RL.r_inv(one, h1, pp, hP, z, c, RL.r_o(pp, z, c, rz), RL.r_c(pp, z, c, rz))
233      +my = PR.rmul(one, h1, pp, hP, y, zi, b, ZI, ry, rzi)
234      +mx = PR.rmul(one, h1, pp, hP, x, zi, a, ZI, rx, rzi)
235      +eb = bytes_rel(one, h1, pp, hP, F.mul(y, zi), FS.fmul(P, b, ZI), my, red(pp, Nat.mul(b, ZI)))
236      +ep = par_u32(one, h1, pp, hP, F.mul(x, zi), FS.fmul(P, a, ZI), mx, red(pp, Nat.mul(a, ZI)))
237      +e1 = Equal.cong(List<&2, U32>, List<&2, U32>, w => PT.set_top(w, F.parity(F.mul(x, zi))), F.to_bytes(F.mul(y, zi)), SX.le_bytes(32n, FS.fmul(P, b, ZI)), eb)
238      +e2 = Equal.cong(U32, List<&2, U32>, w => PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), w), F.parity(F.mul(x, zi)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n)), ep)
239      Equal.trans(List<&2, U32>, PT.set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), SE.set_msb(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), Equal.trans(List<&2, U32>, PT.set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), F.parity(F.mul(x, zi))), PT.set_top(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))), e1, e2), set_eq(SX.le_bytes(32n, FS.fmul(P, b, ZI)), U32.from_nat(Nat.mod(FS.fmul(P, a, ZI), 2n))))