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.
(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:
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.