Tonelli-Shanks modular square root. Finds the odd square root.
Function:
(defun tonelli-shanks-odd-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-odd-sqrt)) (declare (ignorable acl2::__function__)) (let ((sqrt (tonelli-shanks-sqrt-aux n p z))) (if (oddp sqrt) sqrt (mod (- sqrt) p)))))
Theorem:
(defthm natp-zero-or-oddp-of-tonelli-shanks-odd-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-odd-sqrt n p z))) (natp-zero-or-oddp sqrt))) :rule-classes :rewrite)