		Search-engine friendly clone of the ACL2 documentation.

Base58check

Base58check-encode

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 sha-256.

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.

Definitions and Theorems

Function: base58check-encode

(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: base58-character-listp-of-base58check-encode

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

Theorem: base58check-encode-fixes-version-nonempty

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

Theorem: base58check-encode-of-byte-list-fix-version

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

Theorem: base58check-encode-byte-list-equiv-congruence-on-version

(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: base58check-encode-of-byte-list-fix-payload

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

Theorem: base58check-encode-byte-list-equiv-congruence-on-payload

(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)