		Search-engine friendly clone of the ACL2 documentation.

Base64

Base64-decode

Base64 decode a string.

Signature
(base64-decode x) → (mv okp ans)
Arguments: x — String to be decoded.
Guard (stringp x).
Returns: okp — Was decoding successful? It can fail if we encounter non Base-64 alphabetic characters in the input, or if the input is not of the proper length (a multiple of 4), or if there is incorrect padding.
Type (booleanp okp).; ans — On success, the decoded version of x. On failure, it is some nonsensical string that should not be relied on.
Type (stringp ans).

Definitions and Theorems

Function: base64-decode

(defun base64-decode (x)
  (declare (xargs :guard (stringp x)))
  (declare (type string x))
  (let ((acl2::__function__ 'base64-decode))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* (((mv okp chars)
               (base64-decode-list (explode x))))
           (mv okp (implode chars)))
         :exec
         (b* (((mv okp rchars)
               (b64-decode-str-impl x 0 (length x)
                                    nil)))
           (mv okp (rchars-to-string rchars))))))

Theorem: booleanp-of-base64-decode.okp

(defthm booleanp-of-base64-decode.okp
  (b* (((mv ?okp ?ans) (base64-decode x)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: stringp-of-base64-decode.ans

(defthm stringp-of-base64-decode.ans
  (b* (((mv ?okp ?ans) (base64-decode x)))
    (stringp ans))
  :rule-classes :type-prescription)

Theorem: base64-decode-of-base64-encode

(defthm base64-decode-of-base64-encode
  (equal (base64-decode (base64-encode x))
         (mv t (if (stringp x) x ""))))