		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-enc1

Encode 1 final character into base-64 characters.

Signature
(b64-enc1 c1) → (mv e1 e2)
Returns: e1 — Type (characterp e1).; e2 — Type (characterp e2).

This is only used if we have almost reached the end of the string and there is exactly one character left to encode; note that in this case we need to insert two explicit pad characters (=).

Definitions and Theorems

Function: b64-enc1

(defun b64-enc1 (c1)
  (declare (type character c1))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'b64-enc1))
    (declare (ignorable acl2::__function__))
    (b* ((byte1 (char-code c1))
         ((mv val1 val2 & &)
          (b64-vals-from-bytes byte1 0 0))
         (char1 (b64-char-from-value val1))
         (char2 (b64-char-from-value val2)))
      (mv char1 char2))))

Theorem: characterp-of-b64-enc1.e1

(defthm characterp-of-b64-enc1.e1
  (b* (((mv ?e1 ?e2) (b64-enc1 c1)))
    (characterp e1))
  :rule-classes :type-prescription)

Theorem: characterp-of-b64-enc1.e2

(defthm characterp-of-b64-enc1.e2
  (b* (((mv ?e1 ?e2) (b64-enc1 c1)))
    (characterp e2))
  :rule-classes :type-prescription)