def equal_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:184

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

184def 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}:
185  match p q sp sq:
186    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}:
187      +P = {1n+pp : Nat}
188      +rx1 = PR.rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
189      +ry1 = PR.rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
190      +rz1 = PR.rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
191      +rx2 = PR.rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
192      +ry2 = PR.rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
193      +rz2 = PR.rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
194      +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)))
195      +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)))
196      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))