Tonelli-Shanks modular square root. Finds least square root if a square root exists.
Function:
(defun tonelli-shanks-lesser-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-lesser-sqrt)) (declare (ignorable acl2::__function__)) (let ((sqrt (tonelli-shanks-sqrt-aux n p z))) (if (> sqrt (/ p 2)) (mod (- sqrt) p) sqrt))))
Theorem:
(defthm natp-of-tonelli-shanks-lesser-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-lesser-sqrt n p z))) (natp sqrt))) :rule-classes :rewrite)