def MR

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

import Base
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/ed25519/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR

37# decoding results: both None, or both Some of related points
38def MR(+pp: Nat, +m: Maybe<&2, PT.Pt>, +sm: Maybe<&2, SE.EPt>) -> Data:
39  match m sm:
40    case None{} None{}:
41      {True{} == True{} : Bool}
42    case Some{p} Some{sp}:
43      PR.Rp(pp, p, sp)
44    case None{} Some{sp}:
45      {True{} == False{} : Bool}
46    case Some{p} None{}:
47      {True{} == False{} : Bool}