		Search-engine friendly clone of the ACL2 documentation.

Base58

Base58-encode

Turn a list of bytes into the corresponding list of Base58 characters.

Signature
(base58-encode bytes) → chars
Arguments: bytes — Guard (byte-listp bytes).
Returns: chars — Type (base58-character-listp chars).

This is described in bullets 4, 5, and 6 in Section `Creating a Base58Check string' of Page `Base58Check encoding' of [Wiki].

The bytes are treated as big bendian digits in base 256 and converted into the natural number that they denote. This natural number is converted into a minimal-length list of big endian digits in base 58, which has no leading zeros. These digits are converted into the corresponding characters. The number of zeros in the input bytes is the difference between the number of all those bytes and the result of removing all their leading zero bytes. As many 1 characters (which correspond to value 0 in base 58) as this number of zero bytes are added before the other character. The resulting characters are returned as a string.

The addition of the ``zero'' (i.e. 1) characters does not affect the denoted natural number, which is the same denoted by the input bytes.

Note that trim-bendian* fixes its argument to a true list of natural numbers, not to a true list of bytes. Thus, we use an mbe there, so that the encoding function fixes its input to a true list of bytes.

Definitions and Theorems

Function: base58-encode

(defun base58-encode (bytes)
 (declare (xargs :guard (byte-listp bytes)))
 (let ((__function__ 'base58-encode))
  (declare (ignorable __function__))
  (b* ((nat (bebytes=>nat bytes))
       (vals (nat=>bendian* 58 nat))
       (number-of-zeros
            (- (len bytes)
               (len (trim-bendian* (mbe :logic (byte-list-fix bytes)
                                        :exec bytes)))))
       (chars (append (repeat number-of-zeros *base58-zero*)
                      (base58-vals=>chars vals))))
    chars)))

Theorem: base58-character-listp-of-base58-encode

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

Theorem: base58-encode-same-natural-number

(defthm base58-encode-same-natural-number
  (equal (bendian=>nat 58
                       (base58-chars=>vals (base58-encode bytes)))
         (bebytes=>nat bytes)))

Theorem: base58-encode-of-byte-list-fix-bytes

(defthm base58-encode-of-byte-list-fix-bytes
  (equal (base58-encode (byte-list-fix bytes))
         (base58-encode bytes)))

Theorem: base58-encode-byte-list-equiv-congruence-on-bytes

(defthm base58-encode-byte-list-equiv-congruence-on-bytes
  (implies (byte-list-equiv bytes bytes-equiv)
           (equal (base58-encode bytes)
                  (base58-encode bytes-equiv)))
  :rule-classes :congruence)

Subtopics

Base58-encode/decode-inverses-theorems: base58-encode and base58-decode are mutual inverses.