		Search-engine friendly clone of the ACL2 documentation.

Bech32

Valid-bech32m

Check if address is valid Bech32m.

Signature
(valid-bech32m address) → y/n
Arguments: address — Guard (stringp address).
Returns: y/n — Type (booleanp y/n).

Verifies that address is a valid Bech32m string.

Disallows a mixed-case string; then downcases the string before converting the data characters to bytes and verifying the checksum.

Definitions and Theorems

Function: valid-bech32m

(defun valid-bech32m (address)
  (declare (xargs :guard (stringp address)))
  (let ((__function__ 'valid-bech32m))
    (declare (ignorable __function__))
    (b* (((when (mixed-case-stringp address))
          nil)
         (address (str::downcase-string address))
         ((mv erp hrp data)
          (bech32-split-address address))
         ((when erp) nil))
      (bech32m-verify-checksum hrp data))))

Theorem: booleanp-of-valid-bech32m

(defthm booleanp-of-valid-bech32m
  (b* ((y/n (valid-bech32m address)))
    (booleanp y/n))
  :rule-classes :rewrite)