Signed Integer Formats
Function:
(defun ui (r) (declare (xargs :guard t)) r)
Function:
(defun si (r n) (declare (xargs :guard (and (integerp r) (natp n)))) (if (= (bitn r (1- n)) 1) (- r (expt 2 n)) r))
Theorem:
(defthm int-si (implies (and (integerp r) (natp n)) (integerp (si r n))) :rule-classes (:type-prescription :rewrite))
Theorem:
(defthm si-bits (implies (and (integerp x) (natp n) (< x (expt 2 (1- n))) (>= x (- (expt 2 (1- n))))) (= (si (bits x (1- n) 0) n) x)) :rule-classes nil)
Theorem:
(defthm bits-si (implies (and (integerp n) (< i n)) (equal (bits (si r n) i j) (bits r i j))))
Theorem:
(defthm si-shift (implies (and (natp n) (natp k) (bvecp r n)) (equal (si (* (expt 2 k) r) (+ k n)) (* (expt 2 k) (si r n)))))
Function:
(defun sextend (m n r) (declare (xargs :guard (and (natp m) (natp n) (integerp r)))) (bits (si r n) (1- m) 0))
Theorem:
(defthm si-sextend (implies (and (natp n) (natp m) (<= n m) (bvecp r n)) (equal (si (sextend m n r) m) (si r n))))
Theorem:
(defthm si-approx (implies (and (not (zp n)) (integerp x) (integerp y) (< (abs (si (mod x (expt 2 n)) n)) (- (expt 2 (1- n)) (abs (- x y))))) (equal (- (si (mod x (expt 2 n)) n) (si (mod y (expt 2 n)) n)) (- x y))))
Theorem:
(defthm si-to-fl-mod (implies (and (rationalp x) (integerp m) (integerp n) (< m n)) (equal (si x n) (+ (* (expt 2 m) (si (fl (/ x (expt 2 m))) (- n m))) (mod x (expt 2 m))))))
Function:
(defun uf (r n m) (declare (xargs :guard (and (natp r) (natp n) (natp m)))) (* (expt 2 (- m n)) (ui r)))
Function:
(defun sf (r n m) (declare (xargs :guard (and (integerp r) (natp n) (natp m)))) (* (expt 2 (- m n)) (si r n)))
Theorem:
(defthm bits-uf (let ((x (uf r n m)) (f (- n m))) (implies (and (natp n) (natp m) (<= m n) (bvecp r n) (natp i) (natp j) (<= j i)) (equal (bits r i j) (* (expt 2 (- f j)) (- (chop x (- f j)) (chop x (- f (1+ i)))))))))
Theorem:
(defthm bits-sf (let ((x (sf r n m)) (f (- n m))) (implies (and (natp n) (natp m) (<= m n) (bvecp r n) (natp i) (natp j) (<= j i) (< i n)) (equal (bits r i j) (* (expt 2 (- f j)) (- (chop x (- f j)) (chop x (- f (1+ i)))))))))
Theorem:
(defthm chop-uf (let ((x (uf r n m)) (f (- n m))) (implies (and (natp n) (natp m) (<= m n) (bvecp r n) (integerp k) (<= (- f n) k) (< k f)) (iff (= (chop x k) x) (= (bits r (1- (- f k)) 0) 0)))) :rule-classes nil)
Theorem:
(defthm chop-sf (let ((x (sf r n m)) (f (- n m))) (implies (and (natp n) (natp m) (<= m n) (bvecp r n) (integerp k) (<= (- f n) k) (< k f)) (iff (= (chop x k) x) (= (bits r (1- (- f k)) 0) 0)))) :rule-classes nil)
Theorem:
(defthm sf-val (implies (and (natp n) (natp m) (<= m n) (bvecp r n) (integerp y) (= (mod y (expt 2 n)) r) (<= (- (expt 2 (1- n))) y) (< y (expt 2 (1- n)))) (equal (sf r n m) (* (expt 2 (- m n)) y))))