		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-modular-sqrt-algorithm

Tonelli-shanks-greater-sqrt

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

Signature
(tonelli-shanks-greater-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 the greater square root of the two square roots of n modulo p if a square root exists, otherwise returns 0. p must be an odd prime. z is a quadratic nonresidue in p.

Definitions and Theorems

Function: tonelli-shanks-greater-sqrt

(defun tonelli-shanks-greater-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-greater-sqrt))
    (declare (ignorable acl2::__function__))
    (let ((sqrt (tonelli-shanks-sqrt-aux n p z)))
      (if (> sqrt (/ p 2))
          sqrt
        (mod (- sqrt) p)))))

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

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