		Search-engine friendly clone of the ACL2 documentation.

Vl-constint->msb-bits

Vl-constint-lsb-bits-aux

Signature
(vl-constint-lsb-bits-aux len value) → lsb-bits
Arguments: len — Guard (natp len).; value — Guard (natp value).
Returns: lsb-bits — Type (vl-bitlist-p lsb-bits).

Definitions and Theorems

Function: vl-constint-lsb-bits-aux

(defun vl-constint-lsb-bits-aux (len value)
  (declare (xargs :guard (and (natp len) (natp value))))
  (let ((__function__ 'vl-constint-lsb-bits-aux))
    (declare (ignorable __function__))
    (b* (((when (zp len)) nil)
         (bit (if (logbitp 0 (lnfix value))
                  :vl-1val
                :vl-0val)))
      (cons bit
            (vl-constint-lsb-bits-aux (1- len)
                                      (ash (lnfix value) -1))))))

Theorem: vl-bitlist-p-of-vl-constint-lsb-bits-aux

(defthm vl-bitlist-p-of-vl-constint-lsb-bits-aux
  (b* ((lsb-bits (vl-constint-lsb-bits-aux len value)))
    (vl-bitlist-p lsb-bits))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-constint-lsb-bits-aux

(defthm true-listp-of-vl-constint-lsb-bits-aux
  (true-listp (vl-constint-lsb-bits-aux len value))
  :rule-classes :type-prescription)

Theorem: len-of-vl-constint-lsb-bits-aux

(defthm len-of-vl-constint-lsb-bits-aux
  (equal (len (vl-constint-lsb-bits-aux len value))
         (nfix len)))

Theorem: vl-constint-lsb-bits-aux-of-nfix-len

(defthm vl-constint-lsb-bits-aux-of-nfix-len
  (equal (vl-constint-lsb-bits-aux (nfix len)
                                   value)
         (vl-constint-lsb-bits-aux len value)))

Theorem: vl-constint-lsb-bits-aux-nat-equiv-congruence-on-len

(defthm vl-constint-lsb-bits-aux-nat-equiv-congruence-on-len
  (implies (acl2::nat-equiv len len-equiv)
           (equal (vl-constint-lsb-bits-aux len value)
                  (vl-constint-lsb-bits-aux len-equiv value)))
  :rule-classes :congruence)

Theorem: vl-constint-lsb-bits-aux-of-nfix-value

(defthm vl-constint-lsb-bits-aux-of-nfix-value
  (equal (vl-constint-lsb-bits-aux len (nfix value))
         (vl-constint-lsb-bits-aux len value)))

Theorem: vl-constint-lsb-bits-aux-nat-equiv-congruence-on-value

(defthm vl-constint-lsb-bits-aux-nat-equiv-congruence-on-value
  (implies (acl2::nat-equiv value value-equiv)
           (equal (vl-constint-lsb-bits-aux len value)
                  (vl-constint-lsb-bits-aux len value-equiv)))
  :rule-classes :congruence)