Secp256k1-has-square-root?
Test if a has a square root in secp256k1's prime field p.
(secp256k1-has-square-root? a) tests whether
a is
a quadratic residue of
p, i.e., whether there exists
an element
x of the prime field such that
x^2 = a\ (mod\ p).
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-has-square-root?
(defun secp256k1-has-square-root? (a)
(declare (xargs :guard (and (natp a)
(< a (secp256k1-field-prime)))))
(let ((p (secp256k1-field-prime)))
(equal (pow a (/ (- p 1) 2) p) 1)))