		Search-engine friendly clone of the ACL2 documentation.

Tonelli-shanks-modular-sqrt-algorithm

Tonelli-shanks-algorithm-is-correct

Proof of correctness of the Tonelli-Shanks Modular Square Root Algorithm.

Overview

Below are the key lemmas and proof of correctness of the Tonelli-Shanks modular square root algorithm.

Theorems

Key lemmas:

Theorem: y^2=1modp

(defthm y^2=1modp
  (implies (and (primep p) (integerp y) (< 2 p))
           (iff (equal (mod (* y y) p) 1)
                (or (equal (mod y p) 1)
                    (equal (mod y p) (mod -1 p))))))

Theorem: least-repeated-square-equiv

(defthm least-repeated-square-equiv
  (implies (and (natp tt)
                (natp m)
                (natp p)
                (< 2 p)
                (equal (least-repeated-square tt m p)
                       lrs)
                (not (= lrs 0)))
           (= (mod (expt tt (expt 2 lrs)) p) 1)))

Theorem: least-repeated-square-tt^2^lrs=1

(defthm least-repeated-square-tt^2^lrs=1
  (implies (and (natp tt)
                (natp m)
                (natp p)
                (natp i)
                (< i m)
                (< 2 p)
                (= (mod (expt tt (expt 2 i)) p) 1))
           (= (mod (expt tt
                         (expt 2 (least-repeated-square tt m p)))
                   p)
              1)))

Theorem: least-repeated-square-is-least

(defthm least-repeated-square-is-least
  (implies (and (natp tt)
                (natp m)
                (natp p)
                (< 2 p)
                (equal (least-repeated-square tt m p) d)
                (not (= d 0)))
           (not (= (mod (expt tt (expt 2 (- d 1))) p)
                   1))))

Theorem about loop invariants of the algorithm:

Theorem: t-s-aux-loop-invariants

(defthm t-s-aux-loop-invariants
 (implies
  (and
     (posp n)
     (has-square-root? n p)
     (posp m)
     (natp c)
     (natp tt)
     (natp r)
     (natp p)
     (< n p)
     (primep p)
     (< 2 p)
     (equal (mod (expt c (expt 2 (- m 1))) p)
            (mod -1 p))
     (= (acl2::mod-expt-fast tt
                             (expt 2 (least-repeated-square tt m p))
                             p)
        1)
     (equal (mod (* r r) p) (mod (* tt n) p))
     (< 0 (least-repeated-square tt m p)))
  (let ((b (repeated-square c
                            (- (- m (least-repeated-square tt m p))
                               1)
                            p)))
   (let ((c2 (mod (* b b) p))
         (tt2 (mod (* tt b b) p))
         (r2 (mod (* r b) p)))
    (and
     (equal (mod (* r2 r2) p)
            (mod (* tt2 n) p))
     (=
      (acl2::mod-expt-fast
       tt2
       (expt
           2
           (least-repeated-square tt2 (least-repeated-square tt m p)
                                  p))
       p)
      1)
     (equal
          (mod (expt c2
                     (expt 2 (- (least-repeated-square tt m p) 1)))
               p)
          (mod -1 p)))))))

Base case theorem:

Theorem: t-s-aux-base-case

(defthm t-s-aux-base-case
  (implies (and (equal (least-repeated-square tt m p) 0)
                (integerp n)
                (< 0 n)
                (primep p)
                (equal (acl2::mod-expt-fast n (+ -1/2 (* 1/2 p))
                                            p)
                       1)
                (integerp m)
                (< 0 m)
                (integerp c)
                (<= 0 c)
                (integerp tt)
                (<= 0 tt)
                (integerp r)
                (<= 0 r)
                (< n p)
                (< 2 p)
                (equal (mod (expt c (expt 2 (+ -1 m))) p)
                       (+ -1 p))
                (equal (acl2::mod-expt-fast tt 1 p) 1)
                (equal (mod (* r r) p)
                       (mod (* n tt) p)))
           (equal (mod (* n tt) p) n)))

Assuming some properties about the loop invariants and using the theorems t-s-aux-loop-invariants, t-s-aux-base-case, we can prove the following theorem about t-s-aux function of the Tonelli-Shanks algorithm.

Theorem: t-s-aux-equiv

(defthm t-s-aux-equiv
 (implies
  (and
     (posp n)
     (has-square-root? n p)
     (posp m)
     (natp c)
     (natp tt)
     (natp r)
     (< n p)
     (primep p)
     (< 2 p)
     (equal (mod (expt c (expt 2 (- m 1))) p)
            (mod -1 p))
     (= (acl2::mod-expt-fast tt
                             (expt 2 (least-repeated-square tt m p))
                             p)
        1)
     (equal (mod (* r r) p)
            (mod (* tt n) p)))
  (= (mod (* (t-s-aux m c tt r p)
             (t-s-aux m c tt r p))
          p)
     n)))

Proof that the algorithm returns the square root of n modulo p if a square root exists for n modulo p:

Theorem: tonelli-shanks-sqrt-aux-is-sqrt-modp

(defthm tonelli-shanks-sqrt-aux-is-sqrt-modp
  (implies (and (natp n)
                (natp z)
                (> p 2)
                (< n p)
                (< z p)
                (primep p)
                (not (has-square-root? z p))
                (equal (tonelli-shanks-sqrt-aux n p z)
                       y))
           (if (has-square-root? n p)
               (equal (mod (* y y) p) n)
             (equal y 0))))

Key lemma required to prove that the algorithm is correct:

Theorem: modx^2-y^2

(defthm modx^2-y^2
  (implies (and (natp x)
                (natp y)
                (primep p)
                (< 2 p)
                (< x p)
                (< y p)
                (equal (mod (* x x) p) (mod (* y y) p)))
           (or (equal x y)
               (equal x (mod (- y) p)))))

Proof that the Tonelli-Shanks modular square root algorithm is correct:

Theorem: tonelli-shanks-sqrt-aux-is-correct

(defthm tonelli-shanks-sqrt-aux-is-correct
  (implies (and (natp z)
                (> p 2)
                (< z p)
                (primep p)
                (not (has-square-root? z p))
                (natp y)
                (< y p)
                (= (mod (* y y) p) n))
           (or (= (tonelli-shanks-sqrt-aux n p z) y)
               (= (tonelli-shanks-sqrt-aux n p z)
                  (- p y)))))