• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
        • Base64-impl
        • Base64-decode-list
        • Base64-decode
        • Base64-encode-list
        • Base64-revappend-decode
        • Base64-encode
        • Base64-revappend-encode
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings-extensions
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/strings

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-encode

Base64 encode a string.

Base64-revappend-encode

Efficient (revappend-chars (base64-encode x) acc).