(vl-msb-bitslice-hidexpr-base x ss warnings) → (mv successp warnings bit-exprs)
Function:
(defun vl-msb-bitslice-hidexpr-base (x ss warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-warninglist-p warnings)))) (declare (xargs :guard (vl-hidexpr-p x))) (let ((__function__ 'vl-msb-bitslice-hidexpr-base)) (declare (ignorable __function__)) (b* (((mv warning range) (vl-ss-find-hidexpr-range x ss)) (x (vl-expr-fix x)) ((when warning) (mv nil (fatal :type :vl-slicing-fail :msg "Expected to find a declaration for ~a0." :args (list x)) nil)) ((unless (vl-maybe-range-resolved-p range)) (mv nil (fatal :type :vl-slicing-fail :msg "Expected the range of ~a0 to be resolved, but it is ~ ~a1." :args (list x range)) nil)) (msb-index (if range (vl-resolved->val (vl-range->msb range)) 0)) (lsb-index (if range (vl-resolved->val (vl-range->lsb range)) 0)) (size (vl-maybe-range-size range)) (baseexpr (if (vl-fast-atom-p x) (change-vl-atom x :finalwidth size :finaltype :vl-unsigned) (change-vl-nonatom x :finalwidth size :finaltype :vl-unsigned))) (main-bits (if range (vl-make-msb-to-lsb-bitselects baseexpr msb-index lsb-index) (list baseexpr)))) (mv t (ok) main-bits))))
Theorem:
(defthm booleanp-of-vl-msb-bitslice-hidexpr-base.successp (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr-base x ss warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-bitslice-hidexpr-base.warnings (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr-base x ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-msb-bitslice-hidexpr-base.bit-exprs (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr-base x ss warnings))) (vl-exprlist-p bit-exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-mvtypes-0 (booleanp (mv-nth 0 (vl-msb-bitslice-hidexpr-base x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-mvtypes-2 (true-listp (mv-nth 2 (vl-msb-bitslice-hidexpr-base x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm nonempty-of-vl-msb-bitslice-hidexpr-base (let ((ret (vl-msb-bitslice-hidexpr-base x ss warnings))) (implies (mv-nth 0 ret) (mv-nth 2 ret))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-hidexpr-base (let ((ret (vl-msb-bitslice-hidexpr-base x ss warnings))) (equal (vl-exprlist->finalwidths (mv-nth 2 ret)) (replicate (len (mv-nth 2 ret)) 1))))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-hidexpr-base (let ((ret (vl-msb-bitslice-hidexpr-base x ss warnings))) (equal (vl-exprlist->finaltypes (mv-nth 2 ret)) (replicate (len (mv-nth 2 ret)) :vl-unsigned))))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-hidexpr-base (let ((ret (vl-msb-bitslice-hidexpr-base x ss warnings))) (implies (and (mv-nth 0 ret) (vl-hidexpr-p x) (or (vl-atom-p x) (eq (vl-nonatom->op x) :vl-hid-dot))) (vl-exprlist-welltyped-p (mv-nth 2 ret)))))
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-of-vl-expr-fix-x (equal (vl-msb-bitslice-hidexpr-base (vl-expr-fix x) ss warnings) (vl-msb-bitslice-hidexpr-base x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-msb-bitslice-hidexpr-base x ss warnings) (vl-msb-bitslice-hidexpr-base x-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-of-vl-scopestack-fix-ss (equal (vl-msb-bitslice-hidexpr-base x (vl-scopestack-fix ss) warnings) (vl-msb-bitslice-hidexpr-base x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-msb-bitslice-hidexpr-base x ss warnings) (vl-msb-bitslice-hidexpr-base x ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-of-vl-warninglist-fix-warnings (equal (vl-msb-bitslice-hidexpr-base x ss (vl-warninglist-fix warnings)) (vl-msb-bitslice-hidexpr-base x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-base-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-msb-bitslice-hidexpr-base x ss warnings) (vl-msb-bitslice-hidexpr-base x ss warnings-equiv))) :rule-classes :congruence)