		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-vals-from-bytes

Encode 3 bytes into 4 base-64 characters.

Signature
(b64-vals-from-bytes b1 b2 b3) → (mv v1 v2 v3 v4)
Returns: v1 — Type (natp v1).; v2 — Type (natp v2).; v3 — Type (natp v3).; v4 — Type (natp v4).

Convert three bytes into four values, basically as follows:

Byte   Bit Pattern  --->  Values
b1      aaaaaabb           aaaaaa  v1
b2      bbbbcccc           bbbbbb  v2
b3      ccdddddd           cccccc  v3
                           dddddd  v4

Definitions and Theorems

Function: b64-vals-from-bytes$inline

(defun b64-vals-from-bytes$inline (b1 b2 b3)
  (declare (type (unsigned-byte 8) b1 b2 b3))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'b64-vals-from-bytes))
    (declare (ignorable acl2::__function__))
    (b* ((v1 (the (unsigned-byte 6)
                  (ash (lnfix b1) -2)))
         (v2h (the (unsigned-byte 2)
                   (logand (lnfix b1) 3)))
         (v2l (the (unsigned-byte 4)
                   (ash (lnfix b2) -4)))
         (v2 (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 2) v2h) 4))
                          (the (unsigned-byte 4) v2l))))
         (v3h (the (unsigned-byte 4)
                   (logand (lnfix b2) 15)))
         (v3l (the (unsigned-byte 2)
                   (ash (lnfix b3) -6)))
         (v3 (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 4) v3h) 2))
                          (the (unsigned-byte 2) v3l))))
         (v4 (the (unsigned-byte 6)
                  (logand (lnfix b3) 63))))
      (mv v1 v2 v3 v4))))

Theorem: natp-of-b64-vals-from-bytes.v1

(defthm natp-of-b64-vals-from-bytes.v1
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes$inline b1 b2 b3)))
    (natp v1))
  :rule-classes :type-prescription)

Theorem: natp-of-b64-vals-from-bytes.v2

(defthm natp-of-b64-vals-from-bytes.v2
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes$inline b1 b2 b3)))
    (natp v2))
  :rule-classes :type-prescription)

Theorem: natp-of-b64-vals-from-bytes.v3

(defthm natp-of-b64-vals-from-bytes.v3
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes$inline b1 b2 b3)))
    (natp v3))
  :rule-classes :type-prescription)

Theorem: natp-of-b64-vals-from-bytes.v4

(defthm natp-of-b64-vals-from-bytes.v4
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes$inline b1 b2 b3)))
    (natp v4))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-6-of-b64-vals-from-bytes

(defthm unsigned-byte-p-6-of-b64-vals-from-bytes
  (implies (and (force (unsigned-byte-p 8 b1))
                (force (unsigned-byte-p 8 b2))
                (force (unsigned-byte-p 8 b3)))
           (b* (((mv v1 v2 v3 v4)
                 (b64-vals-from-bytes b1 b2 b3)))
             (and (unsigned-byte-p 6 v1)
                  (unsigned-byte-p 6 v2)
                  (unsigned-byte-p 6 v3)
                  (unsigned-byte-p 6 v4)))))

Theorem: b64-vals-from-bytes-padding-1

(defthm b64-vals-from-bytes-padding-1
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes b1 b2 0)))
    (equal v4 0)))

Theorem: b64-vals-from-bytes-padding-2

(defthm b64-vals-from-bytes-padding-2
  (b* (((mv ?v1 ?v2 ?v3 ?v4)
        (b64-vals-from-bytes b1 0 0)))
    (equal v3 0)))