def dec_fin

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/ed25519.bend:134

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/curve25519/x25519.bend as SX

134def dec_fin(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, fail: Bool) -> Maybe<&2, EPt>:
135  match fail:
136    case True{}:
137      None{}
138    case False{}:
139      +x2 = SX.cs_fst(SX.bxor(Nat.mod(x, 2n), x0), x, FS.fsub(p, 0n, x))
140      Some{EPt{x2, y, 1n, FS.fmul(p, x2, y)}}