		Search-engine friendly clone of the ACL2 documentation.

Vl-constint->msb-bits

Vl-constint-msb-bits-aux

Accumulate lsb's into acc, which produces an MSB-ordered list.

Signature
(vl-constint-msb-bits-aux len value acc) → *
Arguments: len — Guard (natp len).; value — Guard (natp value).

Definitions and Theorems

Function: vl-constint-msb-bits-aux

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

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

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

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

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

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

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

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

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