Ed25519.double: 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 69-83 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=69&end_line=83

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

# 5.1.4: A = X1^2, B = Y1^2, C = 2 Z1^2, H = A+B, E = H-(X1+Y1)^2, G = A-B,
# F = C+G, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
def double(+p: Nat, a: EPt) -> EPt:
  match a:
    case EPt{+x1, +y1, +z1, t1}:
      +ea = FS.fmul(p, x1, x1)
      +eb = FS.fmul(p, y1, y1)
      +zz = FS.fmul(p, z1, z1)
      +ec = FS.fadd(p, zz, zz)
      +eh = FS.fadd(p, ea, eb)
      +xy = FS.fadd(p, x1, y1)
      +ee = FS.fsub(p, eh, FS.fmul(p, xy, xy))
      +eg = FS.fsub(p, ea, eb)
      +ef = FS.fadd(p, ec, eg)
      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