Given a packeddimensionlist like [5:0][3:1][0:8], multiplies the dimensions together to get the total number of bits, or returns nil on failure.
(vl-packeddimensionlist-total-size x) → size
Function:
(defun vl-packeddimensionlist-total-size (x) (declare (xargs :guard (vl-packeddimensionlist-p x))) (let ((__function__ 'vl-packeddimensionlist-total-size)) (declare (ignorable __function__)) (b* (((when (atom x)) 1) (rest (vl-packeddimensionlist-total-size (cdr x))) ((unless rest) nil) (first (vl-packeddimension-fix (car x))) ((when (eq first :vl-unsized-dimension)) nil) ((unless (vl-range-resolved-p first)) nil)) (* (vl-range-size first) rest))))
Theorem:
(defthm maybe-posp-of-vl-packeddimensionlist-total-size (b* ((size (vl-packeddimensionlist-total-size x))) (maybe-posp size)) :rule-classes :type-prescription)
Theorem:
(defthm vl-packeddimensionlist-total-size-of-vl-packeddimensionlist-fix-x (equal (vl-packeddimensionlist-total-size (vl-packeddimensionlist-fix x)) (vl-packeddimensionlist-total-size x)))
Theorem:
(defthm vl-packeddimensionlist-total-size-vl-packeddimensionlist-equiv-congruence-on-x (implies (vl-packeddimensionlist-equiv x x-equiv) (equal (vl-packeddimensionlist-total-size x) (vl-packeddimensionlist-total-size x-equiv))) :rule-classes :congruence)