(vl-lucid-valid-bits-for-datatype x ss) → (mv simple-p bits)
Function:
(defun vl-lucid-valid-bits-for-datatype (x ss) (declare (xargs :guard (and (vl-datatype-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-lucid-valid-bits-for-datatype)) (declare (ignorable __function__)) (b* (((mv warning x) (vl-datatype-usertype-elim x ss 1000)) ((when warning) (mv nil nil))) (vl-datatype-case x (:vl-coretype (case x.name ((:vl-logic :vl-reg :vl-bit) (b* (((when (consp x.udims)) (mv nil nil)) ((when (atom x.pdims)) (mv t '(0))) ((unless (and (atom (cdr x.pdims)) (vl-fast-range-p (first x.pdims)) (vl-range-resolved-p (first x.pdims)))) (mv nil nil))) (mv t (vl-lucid-range->bits (first x.pdims))))) ((:vl-byte :vl-shortint :vl-int :vl-longint :vl-integer :vl-time) (if (or (consp x.pdims) (consp x.udims)) (mv nil nil) (case x.name (:vl-byte (mv t (nats-from 0 8))) (:vl-shortint (mv t (nats-from 0 16))) (:vl-int (mv t (nats-from 0 32))) (:vl-longint (mv t (nats-from 0 64))) (:vl-integer (mv t (nats-from 0 32))) (:vl-time (mv t (nats-from 0 64))) (otherwise (mv (impossible) nil))))) (otherwise (mv nil nil)))) (:vl-struct (mv nil nil)) (:vl-union (mv nil nil)) (:vl-enum (mv nil nil)) (:vl-usertype (mv nil nil))))))
Theorem:
(defthm booleanp-of-vl-lucid-valid-bits-for-datatype.simple-p (b* (((mv ?simple-p ?bits) (vl-lucid-valid-bits-for-datatype x ss))) (booleanp simple-p)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-lucid-valid-bits-for-datatype.bits (b* (((mv ?simple-p ?bits) (vl-lucid-valid-bits-for-datatype x ss))) (and (nat-listp bits) (setp bits))) :rule-classes :rewrite)
Theorem:
(defthm vl-lucid-valid-bits-for-datatype-of-vl-datatype-fix-x (equal (vl-lucid-valid-bits-for-datatype (vl-datatype-fix x) ss) (vl-lucid-valid-bits-for-datatype x ss)))
Theorem:
(defthm vl-lucid-valid-bits-for-datatype-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-lucid-valid-bits-for-datatype x ss) (vl-lucid-valid-bits-for-datatype x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-lucid-valid-bits-for-datatype-of-vl-scopestack-fix-ss (equal (vl-lucid-valid-bits-for-datatype x (vl-scopestack-fix ss)) (vl-lucid-valid-bits-for-datatype x ss)))
Theorem:
(defthm vl-lucid-valid-bits-for-datatype-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-lucid-valid-bits-for-datatype x ss) (vl-lucid-valid-bits-for-datatype x ss-equiv))) :rule-classes :congruence)