		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-enc2

Encode 2 final characters into base-64 characters.

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

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

Definitions and Theorems

Function: b64-enc2

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

Theorem: characterp-of-b64-enc2.e1

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

Theorem: characterp-of-b64-enc2.e2

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

Theorem: characterp-of-b64-enc2.e3

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