		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-modular-sqrt-algorithm

Tonelli-shanks-either-sqrt

Tonelli-Shanks modular square root. Finds a square root if a square root exists.

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

Finds a square root of n modulo p if it exists, else returns 0. p must be an odd prime. z is a quadratic nonresidue in p.

Definitions and Theorems

Function: tonelli-shanks-either-sqrt

(defun tonelli-shanks-either-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-either-sqrt))
            (declare (ignorable acl2::__function__))
            (tonelli-shanks-sqrt-aux n p z)))

Theorem: natp-of-tonelli-shanks-either-sqrt

(defthm natp-of-tonelli-shanks-either-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-either-sqrt n p z)))
                     (natp sqrt)))
        :rule-classes :rewrite)