SRT Division and Quotient Digit Selection
Function:
(defun quot$ (j) (if (zp j) 0 (+ (quot$ (1- j)) (* (q$ j) (expt (r$) (- 1 j))))))
Function:
(defun rem$ (j) (* (expt (r$) (1- j)) (- (x$) (* (d$) (quot$ j)))))
Theorem:
(defthm rem0-div-rewrite (equal (rem$ 0) (/ (x$) (r$))))
Theorem:
(defthm rem-div-recurrence (implies (natp j) (equal (rem$ (+ 1 j)) (- (* (r$) (rem$ j)) (* (q$ (1+ j)) (d$))))))
Theorem:
(defthm rem0-div-bound (< (abs (rem$ 0)) (* (rho$) (d$))))
Function:
(defun sel-upper-div (k d) (* (+ k (rho$)) d))
Function:
(defun sel-lower-div (k d) (* (- k (rho$)) d))
Theorem:
(defthm rem-div-bnd-next (implies (and (natp j) (<= (sel-lower-div (q$ (1+ j)) (d$)) (* (r$) (rem$ j))) (>= (sel-upper-div (q$ (1+ j)) (d$)) (* (r$) (rem$ j)))) (<= (abs (rem$ (1+ j))) (* (rho$) (d$)))))
Theorem:
(defthm select-overlap (implies (integerp k) (and (< (sel-lower-div k (d$)) (sel-lower-div (1+ k) (d$))) (< (sel-lower-div (1+ k) (d$)) (sel-upper-div k (d$))) (< (sel-upper-div k (d$)) (sel-upper-div (1+ k) (d$))) (<= (sel-upper-div k (d$)) (sel-lower-div (+ k 2) (d$))))))
Theorem:
(defthm div-containment (and (equal (sel-upper-div (a$) (d$)) (* (r$) (rho$) (d$))) (equal (sel-lower-div (- (a$)) (d$)) (- (* (r$) (rho$) (d$))))))
Function:
(defun md4 (k) (case k (2 13/8) (1 1/2) (0 -3/8) (-1 -3/2)))
Function:
(defun select-digit-d4 (a) (cond ((<= (md4 2) a) 2) ((<= (md4 1) a) 1) ((<= (md4 0) a) 0) ((<= (md4 -1) a) -1) (t -2)))
Theorem:
(defthm sel-limits-4 (implies (and (<= 63/64 (d$)) (<= (d$) 9/8) (= (r$) 4) (= (a$) 2) (member k '(-2 -1 0 1 2))) (and (<= (sel-lower-div k (d$)) (max (sel-lower-div k 63/64) (sel-lower-div k 9/8))) (>= (sel-upper-div k (d$)) (min (sel-upper-div k 63/64) (sel-upper-div k 9/8))))))
Theorem:
(defthm sel-limits-check-4 (implies (and (<= 63/64 (d$)) (<= (d$) 9/8) (= (r$) 4) (= (a$) 2) (member k '(-1 0 1 2))) (and (<= (+ (max (sel-lower-div k 63/64) (sel-lower-div k 9/8)) 1/8) (md4 k)) (>= (min (sel-upper-div k 63/64) (sel-upper-div k 9/8)) (md4 k)))))
Theorem:
(defthm md4-k-bounds (implies (and (<= 63/64 (d$)) (<= (d$) 9/8) (= (r$) 4) (= (a$) 2)) (and (implies (member k '(-1 0 1 2)) (<= (+ (sel-lower-div k (d$)) 1/8) (md4 k))) (implies (member k '(-2 -1 0 1)) (>= (sel-upper-div k (d$)) (md4 (1+ k)))))))
Theorem:
(defthm srt-div-rad-4 (implies (and (= (r$) 4) (= (a$) 2) (<= 63/64 (d$)) (<= (d$) 9/8) (natp j) (<= (abs (rem$ j)) (* 2/3 (d$))) (rationalp approx) (integerp (* 8 approx)) (< (abs (- approx (* 4 (rem$ j)))) 1/8) (= (q$ (1+ j)) (select-digit-d4 approx))) (<= (abs (rem$ (1+ j))) (* 2/3 (d$)))))
Function:
(defun md8*64 (k i) (case (fl (/ i 2)) (0 (case k (4 (if (= i 0) 113 115)) (3 82) (2 50) (1 16) (0 -16) (-1 -48) (-2 -81) (-3 (if (= i 0) -112 -114)))) (1 (case k (4 (if (= i 2) 117 118)) (3 84) (2 50) (1 16) (0 -16) (-1 -50) (-2 -83) (-3 (if (= i 2) -116 -117)))) (2 (case k (4 121) (3 86) (2 52) (1 16) (0 -16) (-1 -52) (-2 -86) (-3 -120))) (3 (case k (4 125) (3 90) (2 54) (1 18) (0 -18) (-1 -54) (-2 -88) (-3 -124))) (4 (case k (4 128) (3 92) (2 54) (1 18) (0 -18) (-1 -54) (-2 -90) (-3 -127))) (5 (case k (4 132) (3 94) (2 56) (1 18) (0 -18) (-1 -56) (-2 -94) (-3 -131))) (6 (case k (4 135) (3 96) (2 58) (1 18) (0 -18) (-1 -58) (-2 -96) (-3 -134))) (7 (case k (4 139) (3 100) (2 60) (1 20) (0 -20) (-1 -60) (-2 -98) (-3 -138))) (8 (case k (4 142) (3 102) (2 60) (1 20) (0 -20) (-1 -60) (-2 -100) (-3 -141))) (9 (case k (4 146) (3 104) (2 62) (1 20) (0 -20) (-1 -62) (-2 -104) (-3 -144))) (10 (case k (4 150) (3 106) (2 64) (1 20) (0 -20) (-1 -64) (-2 -106) (-3 -148))) (11 (case k (4 152) (3 108) (2 64) (1 20) (0 -20) (-1 -64) (-2 -108) (-3 -152))) (12 (case k (4 156) (3 112) (2 66) (1 22) (0 -22) (-1 -66) (-2 -112) (-3 -156))) (13 (case k (4 160) (3 114) (2 68) (1 22) (0 -22) (-1 -68) (-2 -114) (-3 -158))) (14 (case k (4 164) (3 116) (2 70) (1 24) (0 -24) (-1 -70) (-2 -116) (-3 -162))) (15 (case k (4 166) (3 118) (2 70) (1 24) (0 -24) (-1 -70) (-2 -118) (-3 -166))) (16 (case k (4 170) (3 120) (2 72) (1 24) (0 -24) (-1 -72) (-2 -120) (-3 -170))) (17 (case k (4 173) (3 124) (2 73) (1 24) (0 -24) (-1 -72) (-2 -124) (-3 -172))) (18 (case k (4 176) (3 126) (2 76) (1 24) (0 -24) (-1 -76) (-2 -124) (-3 -176))) (19 (case k (4 180) (3 128) (2 76) (1 24) (0 -24) (-1 -76) (-2 -128) (-3 -180))) (20 (case k (4 184) (3 132) (2 78) (1 24) (0 -24) (-1 -78) (-2 -132) (-3 -184))) (21 (case k (4 188) (3 134) (2 80) (1 28) (0 -28) (-1 -80) (-2 -134) (-3 -188))) (22 (case k (4 190) (3 136) (2 82) (1 28) (0 -28) (-1 -82) (-2 -136) (-3 -190))) (23 (case k (4 194) (3 138) (2 82) (1 28) (0 -28) (-1 -82) (-2 -138) (-3 -194))) (24 (case k (4 198) (3 140) (2 84) (1 28) (0 -28) (-1 -84) (-2 -140) (-3 -198))) (25 (case k (4 200) (3 142) (2 84) (1 28) (0 -28) (-1 -84) (-2 -142) (-3 -200))) (26 (case k (4 204) (3 146) (2 86) (1 28) (0 -28) (-1 -86) (-2 -146) (-3 -204))) (27 (case k (4 208) (3 148) (2 88) (1 28) (0 -28) (-1 -88) (-2 -148) (-3 -208))) (28 (case k (4 212) (3 152) (2 90) (1 28) (0 -28) (-1 -90) (-2 -152) (-3 -212))) (29 (case k (4 214) (3 152) (2 90) (1 28) (0 -28) (-1 -90) (-2 -152) (-3 -214))) (30 (case k (4 218) (3 154) (2 94) (1 28) (0 -28) (-1 -94) (-2 -154) (-3 -218))) (31 (case k (4 222) (3 158) (2 94) (1 32) (0 -32) (-1 -94) (-2 -158) (-3 -222)))))
Function:
(defun md8 (k i) (/ (md8*64 k i) 64))
Function:
(defun max-lower (i k) (max (sel-lower-div k (+ 1/2 (/ i 128))) (sel-lower-div k (+ 1/2 (/ (1+ i) 128)))))
Function:
(defun min-upper (i k) (min (sel-upper-div k (+ 1/2 (/ i 128))) (sel-upper-div k (+ 1/2 (/ (1+ i) 128)))))
Theorem:
(defthm sel-limits-check-8 (implies (and (= (r$) 8) (= (a$) 4) (bvecp i 6) (member k '(-3 -2 -1 0 1 2 3 4))) (and (<= (+ (max-lower i k) 1/64) (md8 k i)) (>= (min-upper i (1- k)) (md8 k i)))))
Function:
(defun i64 (d) (fl (* 128 (- d 1/2))))
Theorem:
(defthm sel-limits-8 (implies (and (= (r$) 8) (= (a$) 4) (<= 1/2 (d$)) (< (d$) 1) (member k '(-4 -3 -2 -1 0 1 2 3 4))) (and (<= (sel-lower-div k (d$)) (max-lower (i64 (d$)) k)) (>= (sel-upper-div k (d$)) (min-upper (i64 (d$)) k)))))
Theorem:
(defthm md8-k-bounds (implies (and (= (r$) 8) (= (a$) 4) (<= 1/2 (d$)) (< (d$) 1)) (and (implies (member k '(-3 -2 -1 0 1 2 3 4)) (<= (+ (sel-lower-div k (d$)) 1/64) (md8 k (i64 (d$))))) (implies (member k '(-4 -3 -2 -1 0 1 2 3)) (>= (sel-upper-div k (d$)) (md8 (1+ k) (i64 (d$))))))))
Function:
(defun select-digit-d8 (a i) (cond ((<= (md8 4 i) a) 4) ((<= (md8 3 i) a) 3) ((<= (md8 2 i) a) 2) ((<= (md8 1 i) a) 1) ((<= (md8 0 i) a) 0) ((<= (md8 -1 i) a) -1) ((<= (md8 -2 i) a) -2) ((<= (md8 -3 i) a) -3) (t -4)))
Theorem:
(defthm srt-div-rad-8 (implies (and (= (r$) 8) (= (a$) 4) (<= 1/2 (d$)) (< (d$) 1) (natp j) (<= (abs (rem$ j)) (* 4/7 (d$))) (rationalp approx) (integerp (* 64 approx)) (< (abs (- approx (* 8 (rem$ j)))) 1/64) (= (q$ (1+ j)) (select-digit-d8 approx (i64 (d$))))) (<= (abs (rem$ (1+ j))) (* 4/7 (d$)))))