		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-split-address

Split Bech32 address into hrp and data.

Signature
(bech32-split-address address) → (mv erp ret-hrp data-octets)
Arguments: address — Guard (stringp address).
Returns: erp — Type (booleanp erp).; ret-hrp — Type (stringp ret-hrp), given (stringp address).; data-octets — Type (unsigned-byte-listp 5 data-octets).

Splits the Bech32 or Bech32m address into the human-readable portion (hrp) as a string and the data portion as a list of 5-bit bytes.

Also performs some validity checks.

The overall string must not exceed 90 characters. Since none of the characters is allowed to be encoded using multiple bytes, this means the string does not exceed 90 bytes.
There must be a #\1' character) in the string. The last @('#\1 in the string separates the hrp from the data.
hrp-valid-p makes sure the hrp has at least one character and no more than 83 characters, and the ASCII codes of the characters must be in the range [33,126] inclusive.
The data part must have at least 6 characters.
The characters in the data part must be drawn from qpzry9x8gf2tvdw0s3jn54khce6mua7l.

There are three values returned: an error flag, the hrp as a string or the empty string in the case of an error, and the data as a list of 5-bit bytes or the empty list in the case of an error.

Definitions and Theorems

Function: bech32-split-address

(defun bech32-split-address (address)
  (declare (xargs :guard (stringp address)))
  (let ((__function__ 'bech32-split-address))
    (declare (ignorable __function__))
    (b* (((unless (<= (length address) 90))
          (mv t "" nil))
         (separator-1 (bech32-index-of-last-1 address))
         ((unless (natp separator-1))
          (mv t "" nil))
         ((unless (< separator-1 (- (length address) 1)))
          (mv t "" nil))
         (hrp (subseq address 0 separator-1))
         ((unless (hrp-valid-p hrp))
          (mv t "" nil))
         (data-string (subseq address (+ separator-1 1)
                              (length address)))
         ((unless (<= 6 (length data-string)))
          (mv t "" nil))
         (data-chars (explode data-string))
         (data-octets-or-nils (bech32-chars-to-octets data-chars))
         ((unless (unsigned-byte-listp 5 data-octets-or-nils))
          (mv t "" nil)))
      (mv nil hrp data-octets-or-nils))))

Theorem: booleanp-of-bech32-split-address.erp

(defthm booleanp-of-bech32-split-address.erp
  (b* (((mv ?erp ?ret-hrp ?data-octets)
        (bech32-split-address address)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: stringp-of-bech32-split-address.ret-hrp

(defthm stringp-of-bech32-split-address.ret-hrp
  (implies (stringp address)
           (b* (((mv ?erp ?ret-hrp ?data-octets)
                 (bech32-split-address address)))
             (stringp ret-hrp)))
  :rule-classes :rewrite)

Theorem: return-type-of-bech32-split-address.data-octets

(defthm return-type-of-bech32-split-address.data-octets
  (b* (((mv ?erp ?ret-hrp ?data-octets)
        (bech32-split-address address)))
    (unsigned-byte-listp 5 data-octets))
  :rule-classes :rewrite)