Pcodec.equal_rel: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
Lines 184-196 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&start_line=184&end_line=196

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/ed25519/prel.bend as PR

def equal_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: PR.Rp(pp, p, sp), +hq: PR.Rp(pp, q, sq)) -> {PT.equal(p, q) == SE.equal(1n+pp, sp, sq) : Bool}:
  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 = PR.rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
      +ry1 = PR.rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
      +rz1 = PR.rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
      +rx2 = PR.rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
      +ry2 = PR.rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
      +rz2 = PR.rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
      +e1 = eq_rel(one, h1, pp, hP, F.mul(x1, z2), F.mul(x2, z1), FS.fmul(P, a1, c2), FS.fmul(P, a2, c1), PR.rmul(one, h1, pp, hP, x1, z2, a1, c2, rx1, rz2), PR.rmul(one, h1, pp, hP, x2, z1, a2, c1, rx2, rz1), red(pp, Nat.mul(a1, c2)), red(pp, Nat.mul(a2, c1)))
      +e2 = eq_rel(one, h1, pp, hP, F.mul(y1, z2), F.mul(y2, z1), FS.fmul(P, b1, c2), FS.fmul(P, b2, c1), PR.rmul(one, h1, pp, hP, y1, z2, b1, c2, ry1, rz2), PR.rmul(one, h1, pp, hP, y2, z1, b2, c1, ry2, rz1), red(pp, Nat.mul(b1, c2)), red(pp, Nat.mul(b2, c1)))
      Equal.trans(Bool, Bool.and(F.eq(F.mul(x1, z2), F.mul(x2, z1)), F.eq(F.mul(y1, z2), F.mul(y2, z1))), Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), F.eq(F.mul(y1, z2), F.mul(y2, z1))), Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), Nat.is_eq(FS.fmul(P, b1, c2), FS.fmul(P, b2, c1))), Equal.cong(Bool, Bool, z => Bool.and(z, F.eq(F.mul(y1, z2), F.mul(y2, z1))), F.eq(F.mul(x1, z2), F.mul(x2, z1)), Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), e1), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(FS.fmul(P, a1, c2), FS.fmul(P, a2, c1)), z), F.eq(F.mul(y1, z2), F.mul(y2, z1)), Nat.is_eq(FS.fmul(P, b1, c2), FS.fmul(P, b2, c1)), e2))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=eq_rel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=red
  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=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=rmul
  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=fmul
  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=equal
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=eq
  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/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=equal