def dec_root

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

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

142def dec_root(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, is_u: Bool, is_nu: Bool) -> Maybe<&2, EPt>:
143  match is_u:
144    case True{}:
145      dec_fin(p, x, y, x0, Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(x0, 1n)))
146    case False{}:
147      match is_nu:
148        case True{}:
149          +x1 = FS.fmul(p, x, sqm1(p))
150          dec_fin(p, x1, y, x0, Bool.and(Nat.is_eq(x1, 0n), Nat.is_eq(x0, 1n)))
151        case False{}:
152          None{}