• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
        • Printtree
        • Base64
          • Base64-impl
            • B64-bytes-from-vals
            • B64-vals-from-bytes
            • B64-dec3
            • B64-decode-str-impl
            • B64-dec2
            • B64-encode-last-group
            • B64-value-from-code
            • B64-enc3
            • B64-enc2
            • B64-decode-last-group
            • B64-dec1
            • B64-decode-list-impl
            • B64-encode-str-impl
            • B64-encode-last-group-str
            • B64-enc1
            • B64-char-from-value
            • B64-encode-list-impl
          • Base64-decode-list
          • Base64-decode
          • Base64-encode-list
          • Base64-revappend-decode
          • Base64-revappend-encode
          • Base64-encode
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Explode-implode-equalities
        • 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
    • Math
    • Testing-utilities
  • Base64

Base64-impl

Implementation details of base64 encoding/decoding.

These routines should generally not be used directly, and may be changed in future versions of the library.

Here are some naming conventions used throughout these functions:

  • chars refer to actual ACL2::characters, which typically will be in the Base64 alphabet, i.e., A-Z, a-z, 0-9, +, and /. Of course, when decoding, data might be coming from some external source; it might contain pad characters = or even arbitrary, invalid characters from beyond the Base64 alphabet.
  • codes refer to actual char-codes, with the usual correspondence to chars.
  • values refer to the interpretation of each Base64 character as a numeric value. For instance, the value of #\A is 0; the value of #\B is 1, and so on. In our representation, the values are exactly the 64 natural numbers from 0-63, and can be recognized with, e.g., (unsigned-byte-p 6 val).
  • bytes refer to ordinary 8-bit bytes, which typically will be part of the original, un-encoded data.

Subtopics

B64-bytes-from-vals
Decode 4 base-64 values into 3 bytes.
B64-vals-from-bytes
Encode 3 bytes into 4 base-64 characters.
B64-dec3
Decode 3 arbitrary characters from 4 base-64 characters.
B64-decode-str-impl
Efficient, string-based version of b64-decode-list-impl.
B64-dec2
Decode three base-64 characters to recover 2 arbitrary characters.
B64-encode-last-group
Encode the last group of (up to three) characters.
B64-value-from-code
Look up the value of a Base64 character code, e.g., (char-code #\A) → 0.
B64-enc3
Encode 3 arbitrary characters into 4 base-64 characters.
B64-enc2
Encode 2 final characters into base-64 characters.
B64-decode-last-group
Decode the final group of base-64 encoded characters into 1-3 characters.
B64-dec1
Decode two base-64 characters to recover 1 arbitrary character.
B64-decode-list-impl
Tail-recursive version of base64-decode-list.
B64-encode-str-impl
Efficient, string-based version of b64-encode-list-impl.
B64-encode-last-group-str
String-based version of b64-encode-last-group.
B64-enc1
Encode 1 final character into base-64 characters.
B64-char-from-value
Look up the Base64 character for a value, e.g., 0 → #\A.
B64-encode-list-impl
Tail-recursive version of base64-encode-list.