		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-hrp-expand

The stretching of the human-readable portion.

Signature
(bech32-hrp-expand s) → expanded-hrp
Arguments: s — Guard (stringp s).
Returns: expanded-hrp — Type (unsigned-byte-listp 8 expanded-hrp), given (and (warrant bvshr) (warrant bvand)).

The hrp is converted to a list of ascii codes (octets) and then copied to make two lists. The first list shifts out all 5 low bits, leaving the 3 high bits of each code. The second list masks out the 3 high bits, leaving the low five bits of each code. Then the two lists are appended with a zero byte in between.

Definitions and Theorems

Function: bech32-hrp-expand

(defun bech32-hrp-expand (s)
  (declare (xargs :guard (stringp s)))
  (let ((__function__ 'bech32-hrp-expand))
    (declare (ignorable __function__))
    (b* ((char-codes (string=>nats s))
         (high-bit-codes (bech32-collect-high-3-bits char-codes))
         (low-bit-codes (bech32-collect-low-5-bits char-codes)))
      (append high-bit-codes '(0)
              low-bit-codes))))

Theorem: return-type-of-bech32-hrp-expand

(defthm return-type-of-bech32-hrp-expand
  (implies (and (warrant bvshr) (warrant bvand))
           (b* ((expanded-hrp (bech32-hrp-expand s)))
             (unsigned-byte-listp 8 expanded-hrp)))
  :rule-classes :rewrite)