		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32m-verify-checksum

Verifies a Bech32 checksum.

Signature
(bech32m-verify-checksum hrp data) → y/n
Arguments: hrp — Guard (stringp hrp).; data — Guard (unsigned-byte-listp 8 data).
Returns: y/n — Type (booleanp y/n).

Verifies that the last 6 bytes of data are a correct Bech32m checksum of a string that is split into hrp and data.

Definitions and Theorems

Function: bech32m-verify-checksum

(defun bech32m-verify-checksum (hrp data)
 (declare (xargs :guard (and (stringp hrp)
                             (unsigned-byte-listp 8 data))))
 (let ((__function__ 'bech32m-verify-checksum))
  (declare (ignorable __function__))
  (and (hrp-valid-p hrp)
       (<= 6 (len data))
       (warrant bvshr)
       (warrant bvand)
       (equal (bech32-polymod (append (bech32-hrp-expand hrp) data))
              *bech32m-const*))))

Theorem: booleanp-of-bech32m-verify-checksum

(defthm booleanp-of-bech32m-verify-checksum
  (b* ((y/n (bech32m-verify-checksum hrp data)))
    (booleanp y/n))
  :rule-classes :rewrite)