def add

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/ed25519.bend:54

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS

54# 5.1.4: A = (Y1-X1)(Y2-X2), B = (Y1+X1)(Y2+X2), C = T1 2d T2, D = Z1 2 Z2,
55# E = B-A, F = D-C, G = D+C, H = B+A, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
56def add(+p: Nat, +d: Nat, a: EPt, b: EPt) -> EPt:
57  match a b:
58    case EPt{+x1, +y1, +z1, +t1} EPt{+x2, +y2, +z2, +t2}:
59      +ea = FS.fmul(p, FS.fsub(p, y1, x1), FS.fsub(p, y2, x2))
60      +eb = FS.fmul(p, FS.fadd(p, y1, x1), FS.fadd(p, y2, x2))
61      +ec = FS.fmul(p, FS.fmul(p, t1, FS.fadd(p, d, d)), t2)
62      +ed = FS.fmul(p, FS.fadd(p, z1, z1), z2)
63      +ee = FS.fsub(p, eb, ea)
64      +ef = FS.fsub(p, ed, ec)
65      +eg = FS.fadd(p, ed, ec)
66      +eh = FS.fadd(p, eb, ea)
67      EPt{FS.fmul(p, ee, ef), FS.fmul(p, eg, eh), FS.fmul(p, ef, eg), FS.fmul(p, ee, eh)}