		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

Lebs2osp

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

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

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

Definitions and Theorems

Function: lebs2osp

(defun lebs2osp (bits)
  (declare (xargs :guard (bit-listp bits)))
  (let ((__function__ 'lebs2osp))
    (declare (ignorable __function__))
    (b* ((l (len bits))
         (padlen (- (* 8 (ceiling l 8)) l))
         (padded (append bits (repeat padlen 0))))
      (acl2::bits=>lebytes padded))))

Theorem: byte-listp-of-lebs2osp

(defthm byte-listp-of-lebs2osp
  (b* ((bytes (lebs2osp bits)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: len-of-lebs2osp

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