		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-decode-last-group

Decode the final group of base-64 encoded characters into 1-3 characters.

Signature
(b64-decode-last-group c1 c2 c3 c4) → (mv okp ans)
Returns: okp — Type (booleanp okp).; ans — Type (character-listp ans).

Definitions and Theorems

Function: b64-decode-last-group

(defun b64-decode-last-group (c1 c2 c3 c4)
  (declare (type character c1 c2 c3 c4))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'b64-decode-last-group))
    (declare (ignorable acl2::__function__))
    (cond ((not (eql c4 #\=))
           (b* (((mv okp char1 char2 char3)
                 (b64-dec3 c1 c2 c3 c4)))
             (mv okp (list char1 char2 char3))))
          ((not (eql c3 #\=))
           (b* (((mv okp char1 char2)
                 (b64-dec2 c1 c2 c3)))
             (mv okp (list char1 char2))))
          (t (b* (((mv okp char1) (b64-dec1 c1 c2)))
               (mv okp (list char1)))))))

Theorem: booleanp-of-b64-decode-last-group.okp

(defthm booleanp-of-b64-decode-last-group.okp
  (b* (((mv ?okp ?ans)
        (b64-decode-last-group c1 c2 c3 c4)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: character-listp-of-b64-decode-last-group.ans

(defthm character-listp-of-b64-decode-last-group.ans
  (b* (((mv ?okp ?ans)
        (b64-decode-last-group c1 c2 c3 c4)))
    (character-listp ans))
  :rule-classes :rewrite)

Theorem: b64-decode-last-group-of-b64-encode-last-group

(defthm b64-decode-last-group-of-b64-encode-last-group
  (implies (and (character-listp x)
                (consp x)
                (atom (cdddr x)))
           (b* (((mv c1 c2 c3 c4)
                 (b64-encode-last-group x))
                ((mv okp result)
                 (b64-decode-last-group c1 c2 c3 c4)))
             (and okp (equal result x)))))