(vl-consteval-$bits x orig ss) → (mv successp ans)
Function:
(defun vl-consteval-$bits (x orig ss) (declare (xargs :guard (and (vl-expr-p x) (vl-expr-p orig) (vl-scopestack-p ss)))) (declare (xargs :guard (vl-unary-syscall-p "$bits" orig))) (let ((__function__ 'vl-consteval-$bits)) (declare (ignorable __function__)) (b* ((orig (vl-expr-fix orig)) (orig.finalwidth (vl-expr->finalwidth orig)) (orig.finaltype (vl-expr->finaltype orig)) ((unless (and (posp orig.finalwidth) orig.finaltype)) (mv nil orig)) ((unless (and (vl-atom-p x) (member (tag (vl-atom->guts x)) '(:vl-basictype :vl-typename)))) (b* (((mv & arg-width) (vl-expr-selfsize x ss *vl-fake-elem-for-vl-consteval* nil))) (if arg-width (mv t (vl-consteval-ans :value (acl2::loghead orig.finalwidth arg-width) :width orig.finalwidth :type orig.finaltype)) (mv nil orig)))) (typeguts (vl-atom->guts x)) ((mv ok res) (if (eq (tag typeguts) :vl-typename) (vl-consteval-usertype-bits (vl-typename->name typeguts) ss) (vl-consteval-basictype-bits typeguts)))) (if ok (mv ok (vl-consteval-ans :value (acl2::loghead orig.finalwidth res) :width orig.finalwidth :type orig.finaltype)) (mv nil orig)))))
Theorem:
(defthm booleanp-of-vl-consteval-$bits.successp (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-expr-p-of-vl-consteval-$bits.ans (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (vl-expr-p ans)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-welltyped-p-of-vl-consteval-$bits (implies (vl-expr-welltyped-p orig) (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (vl-expr-welltyped-p ans))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-consteval-$bits (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (equal (vl-expr->finalwidth ans) (vl-expr->finalwidth orig))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finaltype-of-vl-consteval-$bits (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (equal (vl-expr->finaltype ans) (vl-expr->finaltype orig))) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-resolved-p-of-vl-consteval-$bits (b* (((mv ?successp ?ans) (vl-consteval-$bits x orig ss))) (implies successp (vl-expr-resolved-p ans))) :rule-classes :rewrite)
Theorem:
(defthm vl-consteval-$bits-of-vl-expr-fix-x (equal (vl-consteval-$bits (vl-expr-fix x) orig ss) (vl-consteval-$bits x orig ss)))
Theorem:
(defthm vl-consteval-$bits-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-consteval-$bits x orig ss) (vl-consteval-$bits x-equiv orig ss))) :rule-classes :congruence)
Theorem:
(defthm vl-consteval-$bits-of-vl-expr-fix-orig (equal (vl-consteval-$bits x (vl-expr-fix orig) ss) (vl-consteval-$bits x orig ss)))
Theorem:
(defthm vl-consteval-$bits-vl-expr-equiv-congruence-on-orig (implies (vl-expr-equiv orig orig-equiv) (equal (vl-consteval-$bits x orig ss) (vl-consteval-$bits x orig-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-consteval-$bits-of-vl-scopestack-fix-ss (equal (vl-consteval-$bits x orig (vl-scopestack-fix ss)) (vl-consteval-$bits x orig ss)))
Theorem:
(defthm vl-consteval-$bits-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-consteval-$bits x orig ss) (vl-consteval-$bits x orig ss-equiv))) :rule-classes :congruence)