Verifies a Bech32 checksum.
(bech32-or-bech32m-verify-checksum hrp data) → y/n
Verifies that the last 6 bytes of
Does not tell you whether a Bech32 or Bech32m checksum was found.
Function:
(defun bech32-or-bech32m-verify-checksum (hrp data) (declare (xargs :guard (and (stringp hrp) (unsigned-byte-listp 8 data)))) (let ((__function__ 'bech32-or-bech32m-verify-checksum)) (declare (ignorable __function__)) (and (hrp-valid-p hrp) (<= 6 (len data)) (warrant bvshr) (warrant bvand) (let ((cksum (bech32-polymod (append (bech32-hrp-expand hrp) data)))) (or (= cksum 1) (= cksum *bech32m-const*))))))
Theorem:
(defthm booleanp-of-bech32-or-bech32m-verify-checksum (b* ((y/n (bech32-or-bech32m-verify-checksum hrp data))) (booleanp y/n)) :rule-classes :rewrite)