		Search-engine friendly clone of the ACL2 documentation.

Bitcoin

Bech32

A library for Bech32 encoding.

Bech32 and Bech32m are used to encode a sequence of bytes in a checksummed base32 format.

The following executable formal specifications follow the specifications in BIP 173andBIP 350.

Bech32 and Bech32m differ only in the value xored into the checksum at the end of the computation. When we describe Bech32, we are usually referring to both Bech32 and Bech32m.

Subtopics

Bech32-split-address: Split Bech32 address into hrp and data.
Bech32-hrp-expand: The stretching of the human-readable portion.
Valid-bech32-or-bech32m: Check if address is valid Bech32 or Bech32m.
Bech32-polymod-aux
Bech32-or-bech32m-verify-checksum: Verifies a Bech32 checksum.
Bech32m-verify-checksum: Verifies a Bech32 checksum.
Valid-bech32m: Check if address is valid Bech32m.
Valid-bech32: Check if address is valid Bech32.
Bech32-verify-checksum: Verifies a Bech32 checksum.
Bech32-collect-low-5-bits
Bech32-collect-high-3-bits
Bech32-polymod: The polymod checksum for both Bech32 and Bech32m.
Bech32-chars-to-octets
Hrp-valid-p: Check if a Bech32 human-readable portion is valid.
Mixed-case-stringp
Hrp-valid-string-length-p
Hrp-valid-char-code-p
*bech32-char-vals*: Map from 5-bit nonnegative integer to Bech32 character.
Bech32-index-of-last-1
*bech32m-const*: Bech32m constant.