base58-encode and base58-decode are mutual inverses.
Theorem:
(defthm base58-decode-of-base58-encode (equal (base58-decode (base58-encode bytes)) (byte-list-fix bytes)))
Theorem:
(defthm base58-encode-of-base58-decode (equal (base58-encode (base58-decode chars)) (base58-character-list-fix chars)))