# Base64

Routines for Base 64 string encoding/decoding.

We implement ACL2 functions for Base 64 encoding and decoding as
described in RFC 4648.

Our functions are quite efficient, given the constraints of ACL2 string
processing. We prove the following inversion theorem, which shows that if
encode some text and then try to decode it, then (1) decoding succeeds and (2)
we get the original text back.

**Theorem: **base64-decode-of-base64-encode

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

Of course, this theorem does not say anything about whether we have encoded
or decoded the text "correctly" as described in RFC 4648. After all, if we
simply used the identity function as our encoder and decoder, the above theorem
would still hold.

However, to the degree possible, our encoder/decoder are intended to
implement Base64 encoding as described by RFC 4648. We do not implement
variants of base64 encoding such as "base64 URL encoding" and "base64 MIME
encoding." Some particular details of our implementation:

- Per Section 3.1, our encoder does not add line breaks.
- Per Section 3.2, our encoder adds appropriate padding characters.
- Per Section 3.3, our decoder rejects data with non-alphabet
characters.
- Per Section 3.5, our encoder sets the pad bits to zero.
- We use the Base64 alphabet described in Table 1. We do not use the "URL
and Filename safe" Base64 alphabet.

We have not attempted to prove the "other" inversion property, i.e., if we
start with some encoded text, decode it, and re-encode the result, then we
should get back our initial, encoded text. This is probably not currently
true. To prove it, we would need to change the decoder to reject inputs where
the pad bits are nonzero. Implementations "may" choose to implement this
check according to Section 3.5, and in principle it would be a nice
enhancement.

### Subtopics

- Base64-impl
- Implementation details of base64 encoding/decoding.
- Base64-decode-list
- Base64 decode a character list.
- Base64-decode
- Base64 decode a string.
- Base64-encode-list
- Base64 encode a character list.
- Base64-revappend-decode
- Efficiently revappend the characters from base64-decode onto
an accumulator.
- Base64-revappend-encode
- Efficient (revappend-chars (base64-encode x) acc).
- Base64-encode
- Base64 encode a string.