		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

Leos2bsp

The function \mathsf{LEOS2BSP} in [ZPS:5.1].

Signature
(leos2bsp bytes) → bits
Arguments: bytes — Guard (byte-listp bytes).
Returns: bits — Type (bit-listp bits).

The \ell argumnent can be determined from the other argument: it is the length of the other argument times 8. Thus, in our formalization we just have one argument.

Definitions and Theorems

Function: leos2bsp

(defun leos2bsp (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (let ((__function__ 'leos2bsp))
    (declare (ignorable __function__))
    (acl2::lebytes=>bits bytes)))

Theorem: bit-listp-of-leos2bsp

(defthm bit-listp-of-leos2bsp
  (b* ((bits (leos2bsp bytes)))
    (bit-listp bits))
  :rule-classes :rewrite)

Theorem: len-of-leos2bsp

(defthm len-of-leos2bsp
  (b* ((?bits (leos2bsp bytes)))
    (equal (len bits) (* 8 (len bytes)))))