Bit Vector Addition
Theorem:
(defthm half-adder (implies (and (bvecp u 1) (bvecp v 1)) (equal (+ u v) (cat (logand u v) 1 (logxor u v) 1))) :rule-classes nil)
Theorem:
(defthm add-2 (implies (and (integerp x) (integerp y)) (equal (+ x y) (+ (logxor x y) (* 2 (logand x y))))) :rule-classes nil)
Theorem:
(defthm full-adder (implies (and (bvecp u 1) (bvecp v 1) (bvecp w 1)) (equal (+ u v w) (cat (logior (logand u v) (logior (logand u w) (logand v w))) 1 (logxor u (logxor v w)) 1))) :rule-classes nil)
Theorem:
(defthm add-3 (implies (and (integerp x) (integerp y) (integerp z)) (= (+ x y z) (+ (logxor x (logxor y z)) (* 2 (logior (logand x y) (logior (logand x z) (logand y z))))))) :rule-classes nil)
Theorem:
(defthm plus-logior-logand (implies (and (integerp x) (integerp y)) (equal (+ x y) (- (* 2 (logior x y)) (logxor x y)))))
Theorem:
(defthm lutz-lemma (implies (and (integerp x) (integerp y) (natp n)) (and (iff (= (bits (+ x y) (1- n) 0) (1- (expt 2 n))) (= (bits (logxor x y) (1- n) 0) (1- (expt 2 n)))) (iff (= (bits (+ x y) (1- n) 0) (1- (expt 2 n))) (= (+ (bits x (1- n) 0) (bits y (1- n) 0)) (1- (expt 2 n)))))))
Function:
(defun cbit (x y cin k) (if (zp k) cin (logior (logand (bitn x (1- k)) (bitn y (1- k))) (logior (logand (bitn x (1- k)) (cbit x y cin (1- k))) (logand (bitn y (1- k)) (cbit x y cin (1- k)))))))
Theorem:
(defthm ripple-carry-lemma (implies (and (integerp x) (integerp y) (bitp cin) (natp i)) (equal (bitn (+ x y cin) i) (logxor (logxor (bitn x i) (bitn y i)) (cbit x y cin i)))))
Function:
(defun gen (x y i j) (declare (xargs :guard (and (integerp x) (integerp y)))) (if (and (natp i) (natp j) (>= i j)) (if (= (bitn x i) (bitn y i)) (bitn x i) (gen x y (1- i) j)) 0))
Function:
(defun prop (x y i j) (declare (xargs :guard (and (integerp x) (integerp y)))) (if (and (natp i) (natp j) (>= i j)) (if (= (bitn x i) (bitn y i)) 0 (prop x y (1- i) j)) 1))
Theorem:
(defthm bvecp-1-gen (bvecp (gen x y i j) 1) :rule-classes (:rewrite (:forward-chaining :trigger-terms ((gen x y i j)))))
Theorem:
(defthm bvecp-1-prop (bvecp (prop x y i j) 1) :rule-classes (:rewrite (:forward-chaining :trigger-terms ((prop x y i j)))))
Theorem:
(defthm gen-i-i (implies (and (integerp x) (integerp y) (natp i)) (equal (gen x y i i) (logand (bitn x i) (bitn y i)))))
Theorem:
(defthm prop-i-i (implies (and (integerp x) (integerp y) (natp i)) (equal (prop x y i i) (logxor (bitn x i) (bitn y i)))))
Theorem:
(defthm gen-val (implies (natp j) (equal (gen x y i j) (if (>= (+ (bits x i j) (bits y i j)) (expt 2 (1+ (- i j)))) 1 0))))
Theorem:
(defthm bits-sum (implies (and (integerp x) (integerp y)) (equal (bits (+ x y) i j) (bits (+ (bits x i j) (bits y i j) (gen x y (1- j) 0)) (- i j) 0))) :rule-classes nil)
Theorem:
(defthm prop-val (implies (and (integerp i) (natp j) (>= i j)) (equal (prop x y i j) (if (= (+ (bits x i j) (bits y i j)) (1- (expt 2 (1+ (- i j))))) 1 0))))
Function:
(defun gp (x y i j) (cons (gen x y i j) (prop x y i j)))
Function:
(defun gp0 (x y i) (gp x y i i))
Function:
(defun fco (gp1 gp2) (cons (logior (car gp1) (logand (cdr gp1) (car gp2))) (logand (cdr gp1) (cdr gp2))))
Theorem:
(defthm fco-assoc (implies (and (bitp g1) (bitp p1) (bitp g2) (bitp p2) (bitp g3) (bitp p3)) (equal (fco (fco (cons g1 p1) (cons g2 p2)) (cons g3 p3)) (fco (cons g1 p1) (fco (cons g2 p2) (cons g3 p3))))))
Theorem:
(defthm gp-decomp (implies (and (integerp x) (integerp y) (natp j) (natp i) (natp k) (<= j k) (< k i)) (equal (fco (gp x y i (1+ k)) (gp x y k j)) (gp x y i j))))
Theorem:
(defthm cbit-rewrite (implies (and (integerp x) (integerp y) (bitp cin) (natp i)) (equal (cbit x y cin (1+ i)) (logior (gen x y i 0) (logand (prop x y i 0) cin)))))
Function:
(defun rc (x y i) (if (zp i) (gp0 x y 0) (fco (gp0 x y i) (rc x y (1- i)))))
Theorem:
(defthm rc-correct (implies (and (integerp x) (integerp y) (natp i)) (equal (rc x y i) (gp x y i 0))))
Function:
(defun lf (x y i d) (if (zp d) (gp0 x y i) (if (< (mod i (expt 2 d)) (expt 2 (1- d))) (lf x y i (1- d)) (fco (lf x y i (1- d)) (lf x y (+ (chop i (- d)) (expt 2 (1- d)) -1) (1- d))))))
Theorem:
(defthm lf-correct-gen (implies (and (integerp x) (integerp y) (natp i) (natp d)) (equal (lf x y i d) (gp x y i (chop i (- d))))))
Theorem:
(defthm lf-correct (implies (and (integerp x) (integerp y) (natp n) (bvecp i n)) (equal (lf x y i n) (gp x y i 0))))
Function:
(defun ks (x y i d) (if (zp d) (gp0 x y i) (if (< i (expt 2 (1- d))) (ks x y i (1- d)) (fco (ks x y i (1- d)) (ks x y (- i (expt 2 (1- d))) (1- d))))))
Theorem:
(defthm ks-correct-gen (implies (and (integerp x) (integerp y) (natp i) (natp d)) (equal (ks x y i d) (gp x y i (max 0 (1+ (- i (expt 2 d))))))))
Theorem:
(defthm ks-correct (implies (and (integerp x) (integerp y) (natp n) (bvecp i n)) (equal (ks x y i n) (gp x y i 0))))
Function:
(defun pi2 (k) (if (zp k) 0 (if (integerp (/ k 2)) (1+ (pi2 (/ k 2))) 0)))
Theorem:
(defthm pi2-upper (implies (not (zp k)) (<= (expt 2 (pi2 k)) k)))
Theorem:
(defthm pi2-lemma (implies (and (not (zp k)) (integerp p)) (iff (integerp (/ k (expt 2 p))) (<= p (pi2 k)))))
Function:
(defun bk0 (x y i d) (if (zp d) (gp0 x y i) (if (< (pi2 (1+ i)) d) (bk0 x y i (1- d)) (fco (bk0 x y i (1- d)) (bk0 x y (- i (expt 2 (1- d))) (1- d))))))
Function:
(defun bk (x y i n) (let ((p (pi2 (1+ i)))) (if (or (zp n) (not (bvecp i n)) (= i (1- (expt 2 p)))) (bk0 x y i n) (fco (bk0 x y i n) (bk x y (- i (expt 2 p)) n)))))
Theorem:
(defthm bk0-correct-gen (implies (and (integerp x) (integerp y) (natp i) (natp d)) (equal (bk0 x y i d) (gp x y i (1+ (- i (expt 2 (min (pi2 (1+ i)) d))))))))
Theorem:
(defthm bk0-correct (implies (and (integerp x) (integerp y) (natp n) (bvecp i n)) (equal (bk0 x y i n) (gp x y i (1+ (- i (expt 2 (pi2 (1+ i)))))))))
Theorem:
(defthm bk-correct (implies (and (integerp x) (integerp y) (natp n) (bvecp i n)) (equal (bk x y i n) (gp x y i 0))))
Function:
(defun hc0 (x y i k d) (let ((p (pi2 (1+ i)))) (if (or (zp d) (< p k)) (bk0 x y i k) (if (< i (expt 2 (+ k d -1))) (hc0 x y i k (1- d)) (fco (hc0 x y i k (1- d)) (hc0 x y (- i (expt 2 (+ k d -1))) k (1- d)))))))
Function:
(defun hc (x y i k n) (let ((p (pi2 (1+ i)))) (if (or (zp n) (not (bvecp i n)) (>= (pi2 (1+ i)) k) (= i (1- (expt 2 p)))) (hc0 x y i k (- n k)) (fco (hc0 x y i k (- n k)) (hc x y (- i (expt 2 p)) k n)))))
Theorem:
(defthm hc0-correct-gen (implies (and (integerp x) (integerp y) (natp i) (natp k) (natp d) (>= (pi2 (1+ i)) k)) (let ((m (max 0 (- (1+ i) (expt 2 (+ k d)))))) (equal (hc0 x y i k d) (gp x y i m)))))
Theorem:
(defthm hc0-correct (implies (and (integerp x) (integerp y) (natp n) (natp k) (<= k n) (bvecp i n) (integerp (/ (1+ i) (expt 2 k)))) (equal (hc0 x y i k (- n k)) (gp x y i 0))))
Theorem:
(defthm hc-correct (implies (and (integerp x) (integerp y) (natp n) (natp k) (<= k n) (bvecp i n)) (equal (hc x y i k n) (gp x y i 0))))