|
|
|---|
|
|
|
|---|
Proof of correctness of the Tonelli-Shanks Modular Square Root Algorithm.
Below are the key lemmas and proof of correctness of the Tonelli-Shanks modular square root algorithm.
Key lemmas:
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)))))