Tonelli-Shanks modular square root. Finds the even square root.
Function:
(defun tonelli-shanks-even-sqrt (n p z) (declare (xargs :guard (and (natp n) (natp p) (natp z)))) (declare (xargs :guard (and (> p 2) (< z p) (primep p) (< n p) (not (has-square-root? z p))))) (let ((acl2::__function__ 'tonelli-shanks-even-sqrt)) (declare (ignorable acl2::__function__)) (let ((sqrt (tonelli-shanks-sqrt-aux n p z))) (if (evenp sqrt) sqrt (mod (- sqrt) p)))))
Theorem:
(defthm natp-of-tonelli-shanks-even-sqrt (implies (and (natp n) (natp p) (natp z) (< '2 p) (< z p) (primep p) (< n p) (not (has-square-root? z p))) (b* ((sqrt (tonelli-shanks-even-sqrt n p z))) (natp sqrt))) :rule-classes :rewrite)
Theorem:
(defthm evenp-of-tonelli-shanks-even-sqrt (implies (and (natp n) (natp p) (natp z) (< '2 p) (< z p) (primep p) (< n p) (not (has-square-root? z p))) (b* ((sqrt (tonelli-shanks-even-sqrt n p z))) (evenp sqrt))) :rule-classes :rewrite)