def add_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/prel.bend:80

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

80def 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)):
81  match p q sp sq:
82    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}:
83      +P = {1n+pp : Nat}
84      +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
85      +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
86      +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
87      +rt1 = rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
88      +rx2 = rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
89      +ry2 = rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
90      +rz2 = rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
91      +rt2 = rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
92      +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))
93      +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))
94      +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)
95      +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)
96      +ea = F.mul(F.sub(y1, x1), F.sub(y2, x2))
97      +EA = FS.fmul(P, FS.fsub(P, b1, a1), FS.fsub(P, b2, a2))
98      +eb = F.mul(F.add(y1, x1), F.add(y2, x2))
99      +EB = FS.fmul(P, FS.fadd(P, b1, a1), FS.fadd(P, b2, a2))
100      +ec = F.mul(F.mul(t1, PT.cs_d2(cs)), t2)
101      +EC = FS.fmul(P, FS.fmul(P, d1, FS.fadd(P, D, D)), d2)
102      +ed = F.mul(F.add(z1, z1), z2)
103      +ED = FS.fmul(P, FS.fadd(P, c1, c1), c2)
104      +re = rsub(one, h1, pp, hP, eb, ea, EB, EA, rb, ra)
105      +rf = rsub(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc)
106      +rg = radd(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc)
107      +rh = radd(one, h1, pp, hP, eb, ea, EB, EA, rb, ra)
108      +e = F.sub(eb, ea)
109      +f = F.sub(ed, ec)
110      +g = F.add(ed, ec)
111      +h = F.add(eb, ea)
112      +EE = FS.fsub(P, EB, EA)
113      +FF = FS.fsub(P, ED, EC)
114      +GG = FS.fadd(P, ED, EC)
115      +HH = FS.fadd(P, EB, EA)
116      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))