		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-dec2

Decode three base-64 characters to recover 2 arbitrary characters.

Signature
(b64-dec2 c1 c2 c3) → (mv okp d1 d2)
Returns: okp — Decoding can fail if we encounter non Base-64 alphabetic characters in the input.
Type (booleanp okp).; d1 — Type (characterp d1).; d2 — Type (characterp d2).

This is only used to decode the last group of base-64 characters, when there is exactly one pad.

Definitions and Theorems

Function: b64-dec2

(defun b64-dec2 (c1 c2 c3)
  (declare (type character c1 c2 c3))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'b64-dec2))
    (declare (ignorable acl2::__function__))
    (b* ((code1 (char-code c1))
         (code2 (char-code c2))
         (code3 (char-code c3))
         (val1 (b64-value-from-code code1))
         (val2 (b64-value-from-code code2))
         (val3 (b64-value-from-code code3))
         ((unless (and val1 val2 val3))
          (mv nil #\0 #\0))
         ((mv (the (unsigned-byte 8) b1)
              (the (unsigned-byte 8) b2)
              &)
          (b64-bytes-from-vals val1 val2 val3 0))
         (char1 (code-char b1))
         (char2 (code-char b2)))
      (mv t char1 char2))))

Theorem: booleanp-of-b64-dec2.okp

(defthm booleanp-of-b64-dec2.okp
  (b* (((mv ?okp ?d1 ?d2) (b64-dec2 c1 c2 c3)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: characterp-of-b64-dec2.d1

(defthm characterp-of-b64-dec2.d1
  (b* (((mv ?okp ?d1 ?d2) (b64-dec2 c1 c2 c3)))
    (characterp d1))
  :rule-classes :type-prescription)

Theorem: characterp-of-b64-dec2.d2

(defthm characterp-of-b64-dec2.d2
  (b* (((mv ?okp ?d1 ?d2) (b64-dec2 c1 c2 c3)))
    (characterp d2))
  :rule-classes :type-prescription)

Theorem: b64-dec2-of-b64-enc2

(defthm b64-dec2-of-b64-enc2
  (implies (and (characterp c1) (characterp c2))
           (b* (((mv e1 e2 e3) (b64-enc2 c1 c2))
                ((mv okp x1 x2) (b64-dec2 e1 e2 e3)))
             (and okp (equal x1 c1) (equal x2 c2)))))