		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-decode-str-impl

Efficient, string-based version of b64-decode-list-impl.

Signature
(b64-decode-str-impl x n xl acc) → (mv okp acc)
Arguments: x — Guard (stringp x).; n — Guard (natp n).; xl — Guard (equal xl (length x)).
Returns: okp — Type (booleanp okp).; acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: b64-decode-str-impl

(defun b64-decode-str-impl (x n xl acc)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (equal xl (length x)))))
  (declare (type (integer 0 *) n xl)
           (type string x))
  (declare (xargs :guard (<= n xl)))
  (let ((acl2::__function__ 'b64-decode-str-impl))
    (declare (ignorable acl2::__function__))
    (b* (((the (integer 0 *) left)
          (mbe :logic (nfix (- (nfix xl) (nfix n)))
               :exec (- xl n)))
         ((when (zp left)) (mv t acc))
         ((when (< left 4)) (mv nil acc))
         (c1 (char x n))
         (c2 (char x (+ 1 n)))
         (c3 (char x (+ 2 n)))
         (c4 (char x (+ 3 n)))
         ((when (int= left 4))
          (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-str-impl x (+ 4 (lnfix n))
                           xl acc))))

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

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

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

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

Theorem: b64-decode-str-impl-removal

(defthm b64-decode-str-impl-removal
  (implies
       (and (stringp x)
            (natp n)
            (equal xl (length x))
            (<= n xl))
       (equal (b64-decode-str-impl x n xl acc)
              (let ((chars (nthcdr n (explode x))))
                (mv (mv-nth 0 (base64-decode-list chars))
                    (revappend (mv-nth 1 (base64-decode-list chars))
                               acc))))))