		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-decode-list-impl

Tail-recursive version of base64-decode-list.

Signature
(b64-decode-list-impl x acc) → (mv okp acc)
Arguments: x — Guard (character-listp x).
Returns: okp — Type (booleanp okp).; acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: b64-decode-list-impl

(defun b64-decode-list-impl (x acc)
  (declare (xargs :guard (character-listp x)))
  (let ((acl2::__function__ 'b64-decode-list-impl))
    (declare (ignorable acl2::__function__))
    (b* (((when (atom x)) (mv t acc))
         ((when (atom (cdddr x))) (mv nil acc))
         (c1 (first x))
         (c2 (second x))
         (c3 (third x))
         (c4 (fourth x))
         (rest (cddddr x))
         ((when (atom rest))
          (b* (((mv okp last)
                (b64-decode-last-group c1 c2 c3 c4)))
            (mv okp (revappend last acc))))
         ((mv okp x1 x2 x3)
          (b64-dec3 c1 c2 c3 c4))
         ((unless okp) (mv nil acc))
         (acc (list* x3 x2 x1 acc)))
      (b64-decode-list-impl (cddddr x) acc))))

Theorem: booleanp-of-b64-decode-list-impl.okp

(defthm booleanp-of-b64-decode-list-impl.okp
  (b* (((mv ?okp ?acc)
        (b64-decode-list-impl x acc)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: character-listp-of-b64-decode-list-impl.acc

(defthm character-listp-of-b64-decode-list-impl.acc
  (implies (character-listp acc)
           (b* (((mv ?okp ?acc)
                 (b64-decode-list-impl x acc)))
             (character-listp acc)))
  :rule-classes :rewrite)