		Search-engine friendly clone of the ACL2 documentation.

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.