(vl-arith-range-from-size/type ctxsize type) → (mv ok min max)
Function:
(defun vl-arith-range-from-size/type (ctxsize type) (declare (xargs :guard (and (natp ctxsize) (vl-exprsign-p type)))) (let ((__function__ 'vl-arith-range-from-size/type)) (declare (ignorable __function__)) (case (vl-exprsign-fix type) (:vl-unsigned (mv t 0 (1- (ash 1 (lnfix ctxsize))))) (t (mv t (- (ash 1 (max 0 (1- (lnfix ctxsize))))) (1- (ash 1 (max 0 (1- (lnfix ctxsize))))))))))
Theorem:
(defthm integerp-of-vl-arith-range-from-size/type.min (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-arith-range-from-size/type ctxsize type))) (integerp min)) :rule-classes :type-prescription)
Theorem:
(defthm integerp-of-vl-arith-range-from-size/type.max (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-arith-range-from-size/type ctxsize type))) (integerp max)) :rule-classes :type-prescription)