Secp256k1-sqrt
Compute the modular square root of a in the field p.
(secp256k1-sqrt a) finds an
x such that
x^2 = a\ (mod\ p), if such exists, where
p is the prime
field used for secp256k1. If there is no square root, the symbol
:invalid is returned.
Note that this function is about the prime field
p used
to define secp256k1. It is independent of
the other secp256k1 domain parameters.
Definitions and Theorems
Function: secp256k1-sqrt
(defun secp256k1-sqrt (a)
(declare (xargs :guard (and (natp a)
(< a (secp256k1-field-prime)))))
(let ((p (secp256k1-field-prime)))
(let ((poss-root (pow a (/ (+ p 1) 4) p)))
(if (equal (mod (* poss-root poss-root) p)
a)
poss-root
':invalid))))
