		Search-engine friendly clone of the ACL2 documentation.

Number-theory

Tonelli-shanks-modular-sqrt-algorithm

Tonelli-Shanks Modular Square Root Algorithm.

Overview

Below is an implementation of the Tonelli-Shanks modular square root algorithm. The function tonelli-shanks-sqrt-aux returns a square root for a natural number n in the prime field p if a square root exists for n in the field. The function returns 0 if n is equal to 0 or if n does not have a square root.

See subtopics for interface functions and for the proof of correctness of the algorithm, and supportive functions to tonelli-shanks-sqrt-aux.

Definitions and Theorems

Function: q*2^s

(defun q*2^s (n)
  (declare (xargs :guard (natp n)))
  (let ((acl2::__function__ 'q*2^s))
    (declare (ignorable acl2::__function__))
    (if (or (not (natp n)) (= n 0))
        (mv 0 0)
      (if (oddp n)
          (mv n 0)
        (mv-let (inner-q inner-s)
                (q*2^s (/ n 2))
          (mv inner-q (+ inner-s 1)))))))

Theorem: q2s-is-correct

(defthm q2s-is-correct
  (implies (natp n)
           (equal (* (mv-nth 0 (q*2^s n))
                     (expt 2 (mv-nth 1 (q*2^s n))))
                  n)))

Theorem: posp-q*2^s-n-is-even

(defthm posp-q*2^s-n-is-even
  (implies (and (> n 1) (natp n) (evenp n))
           (posp (mv-nth 1 (q*2^s n)))))

Function: least-repeated-square-aux

(defun least-repeated-square-aux (i tt^2^i m p)
  (declare (xargs :guard (and (posp i)
                              (natp tt^2^i)
                              (natp m)
                              (natp p)
                              (< 2 p))))
  (if (not (and (posp i) (natp m) (< i m)))
      0
    (let ((next-square (mod (* tt^2^i tt^2^i) p)))
      (if (= next-square 1)
          i
        (least-repeated-square-aux (+ i 1)
                                   next-square m p)))))

Function: least-repeated-square

(defun least-repeated-square (tt m p)
  (declare (xargs :guard (and (natp tt)
                              (natp m)
                              (natp p)
                              (< 2 p))))
  (if (= (mod tt p) 1)
      0
    (least-repeated-square-aux 1 tt m p)))

Function: repeated-square

(defun repeated-square (base n p)
  (declare (xargs :guard (and (natp base) (natp n) (natp p))))
  (declare (xargs :guard (and (natp base)
                              (natp n)
                              (natp p)
                              (< 2 p))))
  (let ((acl2::__function__ 'repeated-square))
    (declare (ignorable acl2::__function__))
    (if (or (not (natp base))
            (not (natp n))
            (not (natp p))
            (< p 3))
        0
      (if (zp n)
          base
        (repeated-square (mod (* base base) p)
                         (- n 1)
                         p)))))

Theorem: repeated-square-equiv

(defthm repeated-square-equiv
  (implies (and (posp x) (natp c) (natp p) (< 2 p))
           (equal (repeated-square c x p)
                  (acl2::mod-expt-fast c (expt 2 x) p))))

Function: t-s-aux

(defun t-s-aux (m c tt r p)
  (declare (xargs :guard (and (posp m)
                              (natp c)
                              (natp tt)
                              (natp r)
                              (primep p)
                              (< 2 p))))
  (let ((m2 (least-repeated-square tt m p)))
    (if (zp m2)
        r
      (let ((b (repeated-square c (- (- m m2) 1) p)))
        (let ((c2 (mod (* b b) p))
              (tt2 (mod (* tt b b) p))
              (r2 (mod (* r b) p)))
          (t-s-aux m2 c2 tt2 r2 p))))))

Function: tonelli-shanks-sqrt-aux

(defun tonelli-shanks-sqrt-aux (n p z)
  (declare (xargs :guard (and (natp n)
                              (natp p)
                              (natp z)
                              (> p 2)
                              (< z p)
                              (primep p)
                              (< n p)
                              (not (has-square-root? z p)))))
  (if (has-square-root? n p)
      (if (= n 0)
          0
        (mv-let (q s)
                (q*2^s (- p 1))
          (let ((m s)
                (c (acl2::mod-expt-fast z q p))
                (tt (acl2::mod-expt-fast n q p))
                (r (acl2::mod-expt-fast n (/ (+ q 1) 2)
                                        p)))
            (t-s-aux m c tt r p))))
    0))

Subtopics

Tonelli-shanks-algorithm-is-correct: Proof of correctness of the Tonelli-Shanks Modular Square Root Algorithm.
Tonelli-shanks-even-sqrt: Tonelli-Shanks modular square root. Finds the even square root.
Tonelli-shanks-odd-sqrt: Tonelli-Shanks modular square root. Finds the odd square root.
Tonelli-shanks-lesser-sqrt: Tonelli-Shanks modular square root. Finds least square root if a square root exists.
Tonelli-shanks-greater-sqrt: Tonelli-Shanks modular square root. Finds the greater square root.
Tonelli-shanks-sqrt: Tonelli-Shanks modular square root. Finds the least square root.
Tonelli-shanks-either-sqrt: Tonelli-Shanks modular square root. Finds a square root if a square root exists.
Tonelli-shanks-supportive-functions: Supportive Functions