		Search-engine friendly clone of the ACL2 documentation.

Base58

Base58-decode

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

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

This is not explicitly described in [Wiki] or [MB], but is, implicitly, the inverse of encoding.

From a formal specification perspective, we could define this function as the inverse of base58-encode. But since decoding is quite analogous to encoding, and not more complicated than encoding, instead we define it in an executable way, and prove that it is indeed the inverse of encoding. This way, the formal specification of decoding is executable.

This executable formal specification of decoding essentially runs the encoding steps ``in reverse''. Instead of counting the number of leading ``zero'' (i.e. 1) characters in the input characters, we count the number of leading zeros in their corresponding values, via trim-bendian*. Unlike in base58-encode, there is no need here for an mbe to fix the argument of trim-bendian*.

The addition of the zero bytes does not affect the denoted natural number, which is the same denoted by (the corresponding values of) the input characters.

Definitions and Theorems

Function: base58-decode

(defun base58-decode (chars)
  (declare (xargs :guard (base58-character-listp chars)))
  (let ((__function__ 'base58-decode))
    (declare (ignorable __function__))
    (b* ((vals (base58-chars=>vals chars))
         (nat (bendian=>nat 58 vals))
         (number-of-zeros (- (len vals)
                             (len (trim-bendian* vals))))
         (bytes (append (repeat number-of-zeros 0)
                        (nat=>bebytes* nat))))
      bytes)))

Theorem: byte-listp-of-base58-decode

(defthm byte-listp-of-base58-decode
  (b* ((bytes (base58-decode chars)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: base58-decode-same-natural-number

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

Theorem: base58-decode-of-base58-character-list-fix-chars

(defthm base58-decode-of-base58-character-list-fix-chars
  (equal (base58-decode (base58-character-list-fix chars))
         (base58-decode chars)))

Theorem: base58-decode-base58-character-list-equiv-congruence-on-chars

(defthm
      base58-decode-base58-character-list-equiv-congruence-on-chars
  (implies (base58-character-list-equiv chars chars-equiv)
           (equal (base58-decode chars)
                  (base58-decode chars-equiv)))
  :rule-classes :congruence)

Subtopics

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