		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-modular-sqrt-algorithm

Tonelli-shanks-odd-sqrt

Tonelli-Shanks modular square root. Finds the odd square root.

Signature
(tonelli-shanks-odd-sqrt n p z) → sqrt
Arguments: n — Guard (natp n).; p — Guard (natp p).; z — Guard (natp z).
Returns: sqrt — Type (natp-zero-or-oddp sqrt), given the guard.

Finds the odd square root of the two square roots of n modulo p if a square root exists. Otherwise returns 0. z is a quadratic nonresidue in p.

Definitions and Theorems

Function: tonelli-shanks-odd-sqrt

(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: natp-zero-or-oddp-of-tonelli-shanks-odd-sqrt

(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)