		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-dec3

Decode 3 arbitrary characters from 4 base-64 characters.

Signature
(b64-dec3 c1 c2 c3 c4) → (mv okp d1 d2 d3)
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).; d3 — Type (characterp d3).

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

Definitions and Theorems

Function: b64-dec3

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

Theorem: booleanp-of-b64-dec3.okp

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

Theorem: characterp-of-b64-dec3.d1

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

Theorem: characterp-of-b64-dec3.d2

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

Theorem: characterp-of-b64-dec3.d3

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

Theorem: b64-dec3-of-b64-enc3

(defthm b64-dec3-of-b64-enc3
  (implies (and (characterp c1)
                (characterp c2)
                (characterp c3))
           (b* (((mv e1 e2 e3 e4) (b64-enc3 c1 c2 c3))
                ((mv okp x1 x2 x3)
                 (b64-dec3 e1 e2 e3 e4)))
             (and okp (equal x1 c1)
                  (equal x2 c2)
                  (equal x3 c3)))))