Ed25519.add: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as Ed25519
Lines 54-67 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&start_line=54&end_line=67

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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