Bit Slices
Function:
(defun bits (x i j) (declare (xargs :guard (and (integerp x) (integerp i) (integerp j)))) (mbe :logic (if (or (not (integerp i)) (not (integerp j))) 0 (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j)))) :exec (if (< i j) 0 (logand (ash x (- j)) (1- (ash 1 (1+ (- i j))))))))
Theorem:
(defthm bits-nonnegative-integerp-type (and (<= 0 (bits x i j)) (integerp (bits x i j))) :rule-classes (:type-prescription))
Theorem:
(defthm bits-bvecp (implies (and (<= (+ 1 i (- j)) k) (case-split (integerp k))) (bvecp (bits x i j) k)))
Theorem:
(defthm bits-bvecp-simple (implies (equal k (+ 1 i (* -1 j))) (bvecp (bits x i j) k)))
Theorem:
(defthm bits-bounds (implies (and (integerp i) (integerp j)) (and (natp (bits x i j)) (< (bits x i j) (expt 2 (1+ (- i j)))))) :rule-classes nil)
Theorem:
(defthm bits-upper-bound (implies (and (integerp i) (integerp j)) (< (bits x i j) (expt 2 (1+ (- i j))))) :rule-classes :linear)
Theorem:
(defthm mod-bits-equal (implies (= (mod x (expt 2 (1+ i))) (mod y (expt 2 (1+ i)))) (= (bits x i j) (bits y i j))) :rule-classes nil)
Theorem:
(defthm mod-bits-equal-cor (implies (and (integerp x) (integerp n) (integerp i) (integerp j) (< i n)) (equal (bits (mod x (expt 2 n)) i j) (bits x i j))))
Theorem:
(defthm bits-mod (implies (and (case-split (integerp x)) (case-split (integerp i))) (equal (bits x i 0) (mod x (expt 2 (1+ i))))))
Theorem:
(defthm bits-diff-equal (implies (and (natp n) (integerp x) (integerp y) (< (abs (- x y)) (expt 2 n))) (iff (= x y) (= (bits (- x y) (1- n) 0) 0))) :rule-classes nil)
Theorem:
(defthm bits-tail (implies (and (bvecp x (1+ i)) (case-split (acl2-numberp i))) (equal (bits x i 0) x)))
Theorem:
(defthm bits-tail-gen (implies (and (integerp x) (natp i) (< x (expt 2 i)) (>= x (- (expt 2 (+ 1 i))))) (equal (bits x i 0) (if (>= x 0) x (+ x (expt 2 (+ 1 i)))))))
Theorem:
(defthm neg-bits-1 (implies (and (integerp x) (natp i) (natp j) (< x 0) (>= x (- (expt 2 j))) (>= i j)) (equal (bits x i j) (1- (expt 2 (1+ (- i j)))))))
Theorem:
(defthm bits-top-ones (implies (and (natp i) (natp j) (>= i j) (natp x) (< x (expt 2 (1+ i))) (>= x (- (expt 2 (1+ i)) (expt 2 j)))) (equal (bits x i j) (1- (expt 2 (- (1+ i) j))))))
Theorem:
(defthm bits-bits-sum (implies (and (integerp x) (integerp y) (integerp i) (integerp j) (integerp k) (>= j 0) (>= k i)) (equal (bits (+ (bits x k 0) y) i j) (bits (+ x y) i j))))
Theorem:
(defthm bits-bits-sum-alt (implies (and (integerp x) (integerp y) (integerp i) (integerp j) (integerp k) (>= j 0) (>= k i)) (equal (bits (+ x (bits y k 0)) i j) (bits (+ x y) i j))))
Theorem:
(defthm bits-bits-diff (implies (and (integerp x) (integerp y) (integerp i) (integerp j) (integerp k) (>= j 0) (>= k i)) (equal (bits (+ x (- (bits y k 0))) i j) (bits (- x y) i j))))
Theorem:
(defthm bits-bits-prod (implies (and (integerp x) (integerp y) (integerp i) (integerp j) (integerp k) (>= j 0) (>= k i)) (equal (bits (* x (bits y k 0)) i j) (bits (* x y) i j))))
Theorem:
(defthm bits-fl-diff (implies (and (integerp x) (integerp i) (integerp j) (>= i j)) (equal (bits x (1- i) j) (- (fl (/ x (expt 2 j))) (* (expt 2 (- i j)) (fl (/ x (expt 2 i))))))) :rule-classes nil)
Theorem:
(defthm bits-fl-diff-alt (implies (and (integerp x) (integerp i) (integerp j) (>= i (1- j))) (equal (bits x i j) (- (fl (/ x (expt 2 j))) (* (expt 2 (- (1+ i) j)) (fl (/ x (expt 2 (1+ i)))))))))
Theorem:
(defthm bits-mod-fl (implies (and (integerp i) (integerp j)) (equal (bits x (1- i) j) (mod (fl (/ x (expt 2 j))) (expt 2 (- i j))))) :rule-classes nil)
Theorem:
(defthm bits-neg-indices (implies (and (< i 0) (integerp x)) (equal (bits x i j) 0)))
Theorem:
(defthm bits-reverse-indices (implies (< i j) (equal (bits x i j) 0)))
Theorem:
(defthm bvecp-bits-0 (implies (bvecp x j) (equal (bits x i j) 0)))
Theorem:
(defthm bits-0 (equal (bits 0 i j) 0))
Theorem:
(defthm bits-shift-down-1 (implies (and (<= 0 j) (integerp i) (integerp j) (integerp k)) (equal (bits (fl (/ x (expt 2 k))) i j) (bits x (+ i k) (+ j k)))))
Theorem:
(defthm bits-shift-down-2 (implies (and (integerp x) (natp i) (natp k)) (equal (fl (/ (bits x (+ i k) 0) (expt 2 k))) (bits (fl (/ x (expt 2 k))) i 0))))
Theorem:
(defthm bits-shift-up-1 (implies (and (integerp k) (integerp i) (integerp j)) (equal (bits (* (expt 2 k) x) i j) (bits x (- i k) (- j k)))))
Theorem:
(defthm bits-shift-up-2 (implies (and (integerp x) (natp k) (integerp i)) (equal (* (expt 2 k) (bits x i 0)) (bits (* (expt 2 k) x) (+ i k) 0))))
Theorem:
(defthm bits-plus-mult-1 (implies (and (bvecp x k) (<= k m) (integerp y) (case-split (integerp m)) (case-split (integerp n)) (case-split (integerp k))) (equal (bits (+ x (* y (expt 2 k))) n m) (bits y (- n k) (- m k)))))
Theorem:
(defthm bits-plus-mult-2 (implies (and (< n k) (integerp y) (integerp k)) (equal (bits (+ x (* y (expt 2 k))) n m) (bits x n m))))
Theorem:
(defthm bits-plus-mult-2-rewrite (implies (and (syntaxp (quotep c)) (equal (mod c (expt 2 (1+ n))) 0)) (equal (bits (+ c x) n m) (bits x n m))))
Theorem:
(defthm bits-plus-bits (implies (and (integerp m) (integerp p) (integerp n) (<= m p) (<= p n)) (= (bits x n m) (+ (bits x (1- p) m) (* (expt 2 (- p m)) (bits x n p))))) :rule-classes nil)
Theorem:
(defthm bits-bits (implies (and (case-split (<= 0 l)) (case-split (integerp i)) (case-split (integerp j)) (case-split (integerp k)) (case-split (integerp l))) (equal (bits (bits x i j) k l) (if (<= k (- i j)) (bits x (+ k j) (+ l j)) (bits x i (+ l j))))))
Theorem:
(defthm bits-match (implies (and (syntaxp (and (quotep i) (quotep j) (quotep k))) (equal (bits x i2 j2) k2) (syntaxp (and (quotep i2) (quotep j2) (quotep k2))) (<= j2 j) (<= j i) (<= i i2) (equal k (bits k2 (+ i (- j2)) (+ (- j2) j))) (<= 0 i) (<= 0 j) (<= 0 k) (<= 0 i2) (<= 0 j2) (<= 0 k2) (integerp i) (integerp j) (integerp k) (integerp i2) (integerp j2) (integerp k2)) (equal (equal k (bits x i j)) t)))
Theorem:
(defthm bits-dont-match (implies (and (syntaxp (and (quotep i) (quotep j) (quotep k))) (equal (bits x i2 j2) k2) (syntaxp (and (quotep i2) (quotep j2) (quotep k2))) (<= j2 j) (<= j i) (<= i i2) (not (equal k (bits k2 (+ i (- j2)) (+ (- j2) j)))) (<= 0 i) (<= 0 j) (<= 0 k) (<= 0 i2) (<= 0 j2) (<= 0 k2) (integerp i) (integerp j) (integerp k) (integerp i2) (integerp j2) (integerp k2)) (equal (equal k (bits x i j)) nil)))