		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-polymod

The polymod checksum for both Bech32 and Bech32m.

Signature
(bech32-polymod values) → checksum
Arguments: values — Guard (unsigned-byte-listp 8 values).
Returns: checksum — Type (unsigned-byte-p 48 checksum).

Definitions and Theorems

Function: bech32-polymod

(defun bech32-polymod (values)
  (declare (xargs :guard (unsigned-byte-listp 8 values)))
  (let ((__function__ 'bech32-polymod))
    (declare (ignorable __function__))
    (bech32-polymod-aux values 1)))

Theorem: return-type-of-bech32-polymod

(defthm return-type-of-bech32-polymod
  (b* ((checksum (bech32-polymod values)))
    (unsigned-byte-p 48 checksum))
  :rule-classes :rewrite)