		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-char-from-value

Look up the Base64 character for a value, e.g., 0 → #\A.

Signature
(b64-char-from-value value) → char
Returns: char — Type (characterp char).

This is our lowest level encoding function. It's just an array lookup.

Definitions and Theorems

Function: b64-char-from-value$inline

(defun b64-char-from-value$inline (value)
  (declare (type (unsigned-byte 6) value))
  (let ((acl2::__function__ 'b64-char-from-value))
    (declare (ignorable acl2::__function__))
    (the character
         (aref1 '*b64-chars-from-vals-array*
                *b64-chars-from-vals-array* value))))

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

(defthm characterp-of-b64-char-from-value
  (b* ((char (b64-char-from-value$inline value)))
    (characterp char))
  :rule-classes :type-prescription)

Theorem: b64-char-from-value-never-produces-a-pad

(defthm b64-char-from-value-never-produces-a-pad
  (not (equal (b64-char-from-value value)
              #\=)))

Subtopics

*b64-chars-from-vals-array*: Array mapping each value to its associated character.