		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-dec1

Decode two base-64 characters to recover 1 arbitrary character.

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

This is only used to decode the last group of base-64 characters, when there are two pads.

Definitions and Theorems

Function: b64-dec1

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

Theorem: booleanp-of-b64-dec1.okp

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

Theorem: characterp-of-b64-dec1.d1

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

Theorem: b64-dec1-of-b64-enc1

(defthm b64-dec1-of-b64-enc1
  (implies (characterp c1)
           (b* (((mv e1 e2) (b64-enc1 c1))
                ((mv okp x1) (b64-dec1 e1 e2)))
             (and okp (equal x1 c1)))))