		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-encode-str-impl

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

Signature
(b64-encode-str-impl x n xl acc) → *
Arguments: x — Guard (stringp x).; n — Guard (natp n).; xl — Guard (eql xl (length x)).

Definitions and Theorems

Function: b64-encode-str-impl

(defun b64-encode-str-impl (x n xl acc)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (eql xl (length x)))))
  (declare (type (integer 0 *) n xl)
           (type string x))
  (declare (xargs :guard (<= n xl)))
  (let ((acl2::__function__ 'b64-encode-str-impl))
    (declare (ignorable acl2::__function__))
    (b* (((the (integer 0 *) left)
          (mbe :logic (nfix (- (nfix xl) (nfix n)))
               :exec (- xl n)))
         ((when (zp left)) acc)
         ((when (<= left 3))
          (b* (((mv c1 c2 c3 c4)
                (b64-encode-last-group-str x n xl)))
            (list* c4 c3 c2 c1 acc)))
         ((mv c1 c2 c3 c4)
          (b64-enc3 (char x n)
                    (char x (+ 1 n))
                    (char x (+ 2 n))))
         (acc (list* c4 c3 c2 c1 acc)))
      (b64-encode-str-impl x (+ 3 (lnfix n))
                           xl acc))))

Theorem: b64-encode-str-impl-removal

(defthm b64-encode-str-impl-removal
  (implies
       (and (stringp x)
            (natp n)
            (equal xl (length x))
            (<= n xl))
       (equal (b64-encode-str-impl x n xl acc)
              (revappend (base64-encode-list (nthcdr n (explode x)))
                         acc))))