Leading One Prediction
Function:
(defun u0 (x y n) (bits (logior x (lognot y)) (- n 2) 0))
Theorem:
(defthm lza-thm-0-a (implies (and (natp n) (> n 1) (natp x) (natp y) (= (expo x) (1- n)) (= (expo y) (- n 2))) (iff (equal (- x y) 1) (equal (u0 x y n) 0))))
Theorem:
(defthm lza-thm-0-b (implies (and (natp n) (> n 1) (natp x) (natp y) (= (expo x) (1- n)) (= (expo y) (- n 2)) (not (= (u0 x y n) 0))) (and (<= (expo (u0 x y n)) (expo (- x y))) (<= (expo (- x y)) (1+ (expo (u0 x y n)))))))
Function:
(defun p0 (a b) (declare (xargs :guard (and (integerp a) (integerp b)))) (logxor a b))
Function:
(defun g0 (a b) (declare (xargs :guard (and (integerp a) (integerp b)))) (logand a b))
Function:
(defun k0 (a b n) (declare (xargs :guard (and (integerp a) (integerp b) (integerp n)))) (logand (bits (lognot a) (1- n) 0) (bits (lognot b) (1- n) 0)))
Function:
(defun w0 (a b n) (declare (xargs :guard (and (integerp a) (integerp b) (integerp n)))) (bits (lognot (logxor (p0 a b) (* 2 (k0 a b n)))) (1- n) 0))
Theorem:
(defthm p0-rewrite (implies (and (integerp a) (integerp b) (integerp j)) (equal (bitn (p0 a b) j) (if (= (bitn a j) (bitn b j)) 0 1))))
Theorem:
(defthm g0-rewrite (implies (and (integerp a) (integerp b) (integerp j)) (equal (bitn (g0 a b) j) (if (and (= (bitn a j) 1) (= (bitn b j) 1)) 1 0))))
Theorem:
(defthm k0-rewrite (implies (and (integerp a) (integerp b) (natp j) (natp n) (< j n)) (equal (bitn (k0 a b n) j) (if (and (= (bitn a j) 0) (= (bitn b j) 0)) 1 0))))
Theorem:
(defthm w0-rewrite (implies (and (integerp a) (integerp b) (not (zp n)) (not (zp j)) (< j n)) (equal (bitn (w0 a b n) j) (if (= (bitn (p0 a b) j) (bitn (k0 a b n) (1- j))) 1 0))))
Theorem:
(defthm lza-thm-1-case-1 (implies (and (not (zp n)) (bvecp a n) (bvecp b n) (= (+ a b) (expt 2 n))) (equal (w0 a b n) 1)))
Theorem:
(defthm lza-thm-1-case-2 (implies (and (not (zp n)) (bvecp a n) (bvecp b n) (> (+ a b) (expt 2 n))) (and (>= (w0 a b n) 2) (or (= (expo (bits (+ a b) (1- n) 0)) (expo (w0 a b n))) (= (expo (bits (+ a b) (1- n) 0)) (1- (expo (w0 a b n))))) (or (= (expo (bits (+ a b 1) (1- n) 0)) (expo (w0 a b n))) (= (expo (bits (+ a b 1) (1- n) 0)) (1- (expo (w0 a b n))))))) :rule-classes nil)
Function:
(defun z1 (a b n) (declare (xargs :guard (and (integerp a) (integerp b) (integerp n)))) (logior (logand (logxor (bits (p0 a b) n 1) (k0 a b n)) (logxor (p0 a b) (* 2 (k0 a b n)))) (logand (logxor (bits (p0 a b) n 1) (g0 a b)) (logxor (p0 a b) (* 2 (g0 a b))))))
Function:
(defun w1 (a b n) (declare (xargs :guard (and (integerp a) (integerp b) (integerp n)))) (bits (lognot (z1 a b n)) (- n 2) 0))
Theorem:
(defthm w1-rewrite (implies (and (integerp a) (integerp b) (not (zp n)) (not (zp j)) (< j (1- n))) (equal (bitn (w1 a b n) j) (if (and (or (= (bitn (p0 a b) (1+ j)) (bitn (k0 a b n) j)) (= (bitn (p0 a b) j) (bitn (k0 a b n) (1- j)))) (or (= (bitn (p0 a b) (1+ j)) (bitn (g0 a b) j)) (= (bitn (p0 a b) j) (bitn (g0 a b) (1- j))))) 1 0))))
Theorem:
(defthm lza-thm-2-case-1 (implies (and (not (zp n)) (bvecp a n) (bvecp b n) (= (+ a b) (1- (expt 2 n))) (natp i)) (equal (w1 a b n) 0)))
Theorem:
(defthm lza-thm-2-case-2 (implies (and (natp n) (> n 1) (bvecp a n) (bvecp b n) (or (= (+ a b) (expt 2 n)) (= (+ a b) (- (expt 2 n) 2)))) (equal (w1 a b n) 1)))
Theorem:
(defthm lza-thm-2-case-3 (implies (and (not (zp n)) (bvecp a n) (bvecp b n) (= (bitn (p0 a b) (1- n)) 1) (> (+ a b) (expt 2 n))) (and (>= (w1 a b n) 2) (or (= (expo (bits (+ a b) (1- n) 0)) (expo (w1 a b n))) (= (expo (bits (+ a b) (1- n) 0)) (1- (expo (w1 a b n))))) (or (= (expo (bits (+ a b 1) (1- n) 0)) (expo (w1 a b n))) (= (expo (bits (+ a b 1) (1- n) 0)) (1- (expo (w1 a b n))))))) :rule-classes nil)
Theorem:
(defthm lza-thm-2-case-4 (implies (and (not (zp n)) (bvecp a n) (bvecp b n) (= (bitn (p0 a b) (1- n)) 1) (< (+ a b) (- (expt 2 n) 2))) (and (>= (w1 a b n) 2) (or (= (expo (bits (lognot (+ a b)) (1- n) 0)) (expo (w1 a b n))) (= (expo (bits (lognot (+ a b)) (1- n) 0)) (1- (expo (w1 a b n))))) (or (= (expo (bits (lognot (+ a b 1)) (1- n) 0)) (expo (w1 a b n))) (= (expo (bits (lognot (+ a b 1)) (1- n) 0)) (1- (expo (w1 a b n))))))) :rule-classes nil)
Function:
(defun zseg (x k i) (if (zp k) (if (= (bitn x i) 0) 1 0) (if (and (= (zseg x (1- k) (1+ (* 2 i))) 1) (= (zseg x (1- k) (* 2 i)) 1)) 1 0)))
Function:
(defun zcount (x k i) (if (zp k) 0 (if (= (zseg x (1- k) (1+ (* 2 i))) 1) (logior (expt 2 (1- k)) (zcount x (1- k) (* 2 i))) (zcount x (1- k) (1+ (* 2 i))))))
Function:
(defun clz (x n) (zcount x n 0))
Theorem:
(defthm clz-thm (implies (and (natp n) (bvecp x (expt 2 n)) (> x 0)) (equal (clz x n) (- (1- (expt 2 n)) (expo x)))))