		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-enc3

Encode 3 arbitrary characters into 4 base-64 characters.

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

This is the main function for encoding, which is used for all but perhaps the last one or two characters.

Definitions and Theorems

Function: b64-enc3

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

Theorem: characterp-of-b64-enc3.e1

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

Theorem: characterp-of-b64-enc3.e2

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

Theorem: characterp-of-b64-enc3.e3

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

Theorem: characterp-of-b64-enc3.e4

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