		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-collect-high-3-bits

Signature
(bech32-collect-high-3-bits codes) → high-bits-codes
Arguments: codes — Guard (unsigned-byte-listp 8 codes).
Returns: high-bits-codes — Type (unsigned-byte-listp 8 high-bits-codes), given (warrant bvshr).

Definitions and Theorems

Function: bech32-collect-high-3-bits

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

Theorem: return-type-of-bech32-collect-high-3-bits

(defthm return-type-of-bech32-collect-high-3-bits
 (implies (warrant bvshr)
          (b* ((high-bits-codes (bech32-collect-high-3-bits codes)))
            (unsigned-byte-listp 8 high-bits-codes)))
 :rule-classes :rewrite)