Construct a bit-mask that captures the non-wild bits from a casex
pattern or the right-hand side of a
(vl-msb-bits-to-care-mask msb-bits care-bits value) → care-mask
Function:
(defun vl-msb-bits-to-care-mask (msb-bits care-bits value) (declare (xargs :guard (and (vl-bitlist-p msb-bits) (vl-bitlist-p care-bits) (natp value)))) (declare (xargs :guard (true-listp care-bits))) (let ((__function__ 'vl-msb-bits-to-care-mask)) (declare (ignorable __function__)) (b* ((value (lnfix value)) ((when (atom msb-bits)) value) (bit1 (vl-bit-fix (car msb-bits))) (value (if (member-eq bit1 (vl-bitlist-fix care-bits)) (logior 1 (ash value 1)) (ash value 1)))) (vl-msb-bits-to-care-mask (cdr msb-bits) care-bits value))))
Theorem:
(defthm natp-of-vl-msb-bits-to-care-mask (b* ((care-mask (vl-msb-bits-to-care-mask msb-bits care-bits value))) (natp care-mask)) :rule-classes :type-prescription)
Theorem:
(defthm unsigned-byte-p-of-vl-msb-bits-to-care-mask-general (implies (unsigned-byte-p n value) (unsigned-byte-p (+ n (len msb-bits)) (vl-msb-bits-to-care-mask msb-bits cares value))))
Theorem:
(defthm unsigned-byte-p-of-vl-msb-bits-to-care-mask-zero (unsigned-byte-p (len msb-bits) (vl-msb-bits-to-care-mask msb-bits cares 0)))
Theorem:
(defthm upper-bound-of-vl-msb-bits-to-care-mask-zero (< (vl-msb-bits-to-care-mask msb-bits cares 0) (expt 2 (len msb-bits))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-msb-bits-to-care-mask-of-vl-bitlist-fix-msb-bits (equal (vl-msb-bits-to-care-mask (vl-bitlist-fix msb-bits) care-bits value) (vl-msb-bits-to-care-mask msb-bits care-bits value)))
Theorem:
(defthm vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-msb-bits (implies (vl-bitlist-equiv msb-bits msb-bits-equiv) (equal (vl-msb-bits-to-care-mask msb-bits care-bits value) (vl-msb-bits-to-care-mask msb-bits-equiv care-bits value))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bits-to-care-mask-of-vl-bitlist-fix-care-bits (equal (vl-msb-bits-to-care-mask msb-bits (vl-bitlist-fix care-bits) value) (vl-msb-bits-to-care-mask msb-bits care-bits value)))
Theorem:
(defthm vl-msb-bits-to-care-mask-vl-bitlist-equiv-congruence-on-care-bits (implies (vl-bitlist-equiv care-bits care-bits-equiv) (equal (vl-msb-bits-to-care-mask msb-bits care-bits value) (vl-msb-bits-to-care-mask msb-bits care-bits-equiv value))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bits-to-care-mask-of-nfix-value (equal (vl-msb-bits-to-care-mask msb-bits care-bits (nfix value)) (vl-msb-bits-to-care-mask msb-bits care-bits value)))
Theorem:
(defthm vl-msb-bits-to-care-mask-nat-equiv-congruence-on-value (implies (acl2::nat-equiv value value-equiv) (equal (vl-msb-bits-to-care-mask msb-bits care-bits value) (vl-msb-bits-to-care-mask msb-bits care-bits value-equiv))) :rule-classes :congruence)