Pcodec.encode_rel: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec Lines 223-239 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&start_line=223&end_line=239 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 def 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>}: match p sp: case PT.Pt{+x, +y, +z, +t} SE.EPt{+a, +b, +c, +d}: +P = {1n+pp : Nat} +rx = PR.rX(pp, x, y, z, t, a, b, c, d, hp) +ry = PR.rY(pp, x, y, z, t, a, b, c, d, hp) +rz = PR.rZ(pp, x, y, z, t, a, b, c, d, hp) +zi = F.inv(z) +ZI = FS.finv(P, c) +rzi = RL.r_inv(one, h1, pp, hP, z, c, RL.r_o(pp, z, c, rz), RL.r_c(pp, z, c, rz)) +my = PR.rmul(one, h1, pp, hP, y, zi, b, ZI, ry, rzi) +mx = PR.rmul(one, h1, pp, hP, x, zi, a, ZI, rx, rzi) +eb = bytes_rel(one, h1, pp, hP, F.mul(y, zi), FS.fmul(P, b, ZI), my, red(pp, Nat.mul(b, ZI))) +ep = par_u32(one, h1, pp, hP, F.mul(x, zi), FS.fmul(P, a, ZI), mx, red(pp, Nat.mul(a, ZI))) +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) +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) 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)))) Uses (35): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=r_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=r_inv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=r_o https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=bytes_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=par_u32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=red https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=set_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=Rp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rX https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rY https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rZ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rmul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=finv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=fmul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=le_bytes https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=EPt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=encode_n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=set_msb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=inv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=parity https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=to_bytes https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=Pt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=encode https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=set_top