Encode a payload, with a version prefix, in Base58Check.

- Signature
(base58check-encode version payload) → chars

- Arguments
`version`—Guard (byte-listp version) .`payload`—Guard (byte-listp payload) .- Returns
`chars`—Type (base58-character-listp chars) .

This is described in Section `Creating a Base58Check string' of Page `Base58Check encoding' of [Wiki]. It is also described in Section `Base58 and Base58Check Encoding' of Chapter 4 of [MB], with an illustration in Figure 6.

Version prefix and payload (which are both lists of bytes) are concatenated and hashed twice with SHA-256. The first four bytes of the hash are used as a checksum, which is appended to the concatenated version prefix and payload. The resulting bytes are Base58-encoded.

Bullet 1 of the description in [Wiki] talks about a single version byte. However, both Table 1 of Chapter 4 of [MB] and Page `List of address prefixes' of [Wiki] include multi-byte prefixes. Thus, this function takes a list of bytes as the version prefix.

The combined length of version prefix and payload
must not exceed the (large) limit for SHA-256.
See the guard of

We require the version to be non-empty. A version that is the empty list of bytes does not seem to make sense. We allow the payload to be empty, even though this may never happen in Bitcoin.

**Function: **

(defun base58check-encode (version payload) (declare (xargs :guard (and (byte-listp version) (byte-listp payload)))) (declare (xargs :guard (and (consp version) (< (+ (len version) (len payload)) (expt 2 61))))) (let ((__function__ 'base58check-encode)) (declare (ignorable __function__)) (b* ((version (mbe :logic (if (consp version) version (list 0)) :exec version)) (version+payload (append version payload)) (hash (sha-256-bytes (sha-256-bytes version+payload))) (checksum (take 4 hash)) (version+payload+checksum (append version+payload checksum))) (base58-encode version+payload+checksum))))

**Theorem: **

(defthm base58-character-listp-of-base58check-encode (b* ((chars (base58check-encode version payload))) (base58-character-listp chars)) :rule-classes :rewrite)

**Theorem: **

(defthm base58check-encode-fixes-version-nonempty (equal (base58check-encode nil payload) (base58check-encode (list 0) payload)))

**Theorem: **

(defthm base58check-encode-of-byte-list-fix-version (equal (base58check-encode (byte-list-fix version) payload) (base58check-encode version payload)))

**Theorem: **

(defthm base58check-encode-byte-list-equiv-congruence-on-version (implies (byte-list-equiv version version-equiv) (equal (base58check-encode version payload) (base58check-encode version-equiv payload))) :rule-classes :congruence)

**Theorem: **

(defthm base58check-encode-of-byte-list-fix-payload (equal (base58check-encode version (byte-list-fix payload)) (base58check-encode version payload)))

**Theorem: **

(defthm base58check-encode-byte-list-equiv-congruence-on-payload (implies (byte-list-equiv payload payload-equiv) (equal (base58check-encode version payload) (base58check-encode version payload-equiv))) :rule-classes :congruence)