		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-collect-low-5-bits

Signature
(bech32-collect-low-5-bits codes) → low-bits-codes
Arguments: codes — Guard (unsigned-byte-listp 8 codes).
Returns: low-bits-codes — Type (unsigned-byte-listp 8 low-bits-codes), given (warrant bvand).

Definitions and Theorems

Function: bech32-collect-low-5-bits

(defun bech32-collect-low-5-bits (codes)
  (declare (xargs :guard (unsigned-byte-listp 8 codes)))
  (let ((__function__ 'bech32-collect-low-5-bits))
    (declare (ignorable __function__))
    (loop$ for code of-type (integer 0 255)
           in codes collect (bvand 8 code 31))))

Theorem: return-type-of-bech32-collect-low-5-bits

(defthm return-type-of-bech32-collect-low-5-bits
  (implies (warrant bvand)
           (b* ((low-bits-codes (bech32-collect-low-5-bits codes)))
             (unsigned-byte-listp 8 low-bits-codes)))
  :rule-classes :rewrite)