Prel.add_rel: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as Prel Lines 80-116 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&start_line=80&end_line=116 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/rel.bend as RL def add_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> Rp(pp, PT.add(cs, p, q), SE.add(1n+pp, D, sp, sq)): match p q sp sq: case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}: +P = {1n+pp : Nat} +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) +rt1 = rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp) +rx2 = rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) +ry2 = rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) +rz2 = rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) +rt2 = rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq) +ra = rmul(one, h1, pp, hP, F.sub(y1, x1), F.sub(y2, x2), FS.fsub(P, b1, a1), FS.fsub(P, b2, a2), rsub(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), rsub(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2)) +rb = rmul(one, h1, pp, hP, F.add(y1, x1), F.add(y2, x2), FS.fadd(P, b1, a1), FS.fadd(P, b2, a2), radd(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), radd(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2)) +rc = rmul(one, h1, pp, hP, F.mul(t1, PT.cs_d2(cs)), t2, FS.fmul(P, d1, FS.fadd(P, D, D)), d2, rmul(one, h1, pp, hP, t1, PT.cs_d2(cs), d1, FS.fadd(P, D, D), rt1, rd2), rt2) +rdd = rmul(one, h1, pp, hP, F.add(z1, z1), z2, FS.fadd(P, c1, c1), c2, radd(one, h1, pp, hP, z1, z1, c1, c1, rz1, rz1), rz2) +ea = F.mul(F.sub(y1, x1), F.sub(y2, x2)) +EA = FS.fmul(P, FS.fsub(P, b1, a1), FS.fsub(P, b2, a2)) +eb = F.mul(F.add(y1, x1), F.add(y2, x2)) +EB = FS.fmul(P, FS.fadd(P, b1, a1), FS.fadd(P, b2, a2)) +ec = F.mul(F.mul(t1, PT.cs_d2(cs)), t2) +EC = FS.fmul(P, FS.fmul(P, d1, FS.fadd(P, D, D)), d2) +ed = F.mul(F.add(z1, z1), z2) +ED = FS.fmul(P, FS.fadd(P, c1, c1), c2) +re = rsub(one, h1, pp, hP, eb, ea, EB, EA, rb, ra) +rf = rsub(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc) +rg = radd(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc) +rh = radd(one, h1, pp, hP, eb, ea, EB, EA, rb, ra) +e = F.sub(eb, ea) +f = F.sub(ed, ec) +g = F.add(ed, ec) +h = F.add(eb, ea) +EE = FS.fsub(P, EB, EA) +FF = FS.fsub(P, ED, EC) +GG = FS.fadd(P, ED, EC) +HH = FS.fadd(P, EB, EA) mk(pp, F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h), FS.fmul(P, EE, FF), FS.fmul(P, GG, HH), FS.fmul(P, FF, GG), FS.fmul(P, EE, HH), rmul(one, h1, pp, hP, e, f, EE, FF, re, rf), rmul(one, h1, pp, hP, g, h, GG, HH, rg, rh), rmul(one, h1, pp, hP, f, g, FF, GG, rf, rg), rmul(one, h1, pp, hP, e, h, EE, HH, re, rh)) Uses (25): 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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=R 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=mk https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rT 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=radd 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/crypto/ed25519/prel.bend&name=rsub 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=fadd 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/field.bend&name=fsub 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=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=add 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=sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=Cs 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=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=cs_d2