• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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-vals-from-codes-array*
          • 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/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • 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-impl

B64-value-from-code

Look up the value of a Base64 character code, e.g., (char-code #\A) → 0.

Signature

(b64-value-from-code code) → value

Returns

value — Type (or (not value) (natp value)).

This is our lowest level decoding function. It's just an array lookup. Codes for characters that aren't part of the Base64 alphabet are mapped to NIL.

Definitions and Theorems

Function: b64-value-from-code$inline

(defun b64-value-from-code$inline (code)
  (declare (type (unsigned-byte 8) code))
  (let ((acl2::__function__ 'b64-value-from-code))
    (declare (ignorable acl2::__function__))
    (aref1 '*b64-vals-from-codes-array*
           *b64-vals-from-codes-array*
           (lnfix code))))

Theorem: return-type-of-b64-value-from-code

(defthm return-type-of-b64-value-from-code
  (b* ((value (b64-value-from-code$inline code)))
    (or (not value) (natp value)))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-6-of-b64-value-from-code

(defthm unsigned-byte-p-6-of-b64-value-from-code
  (iff (unsigned-byte-p 6 (b64-value-from-code code))
       (b64-value-from-code code)))

Theorem: b64-value-from-code-of-b64-char-from-value

(defthm b64-value-from-code-of-b64-char-from-value
 (implies
  (unsigned-byte-p 6 value)
  (equal
       (b64-value-from-code (char-code (b64-char-from-value value)))
       value)))

Subtopics

*b64-vals-from-codes-array*

Array mapping each character code back to its associated value.