		Search-engine friendly clone of the ACL2 documentation.

Bits/bytes-digit-grouping

Bits=>bebytes

Group bits into bytes, big-endian.

Signature
(bits=>bebytes digits) → new-digits
Arguments: digits — Guard (bit-listp digits).
Returns: new-digits — Type (byte-listp new-digits).

Definitions and Theorems

Function: bits=>bebytes

(defun bits=>bebytes (digits)
  (declare (xargs :guard (bit-listp digits)))
  (declare (xargs :guard (integerp (/ (len digits) 8))))
  (let ((__function__ 'bits=>bebytes))
    (declare (ignorable __function__))
    (group-bendian 2 8 digits)))

Theorem: byte-listp-of-bits=>bebytes

(defthm byte-listp-of-bits=>bebytes
  (b* ((new-digits (bits=>bebytes digits)))
    (byte-listp new-digits))
  :rule-classes :rewrite)

Theorem: bits=>bebytes-of-bit-list-fix-digits

(defthm bits=>bebytes-of-bit-list-fix-digits
  (equal (bits=>bebytes (bit-list-fix digits))
         (bits=>bebytes digits)))

Theorem: bits=>bebytes-bit-list-equiv-congruence-on-digits

(defthm bits=>bebytes-bit-list-equiv-congruence-on-digits
  (implies (bit-list-equiv digits digits-equiv)
           (equal (bits=>bebytes digits)
                  (bits=>bebytes digits-equiv)))
  :rule-classes :congruence)