		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-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-odd-sqrt: Tonelli-Shanks modular square root. Finds the odd 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