• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
        • Base64-impl
          • B64-bytes-from-vals
          • B64-vals-from-bytes
          • B64-dec3
          • B64-decode-str-impl
          • B64-dec2
          • B64-encode-last-group
          • B64-value-from-code
          • B64-enc3
          • B64-enc2
          • B64-decode-last-group
          • B64-dec1
          • B64-decode-list-impl
          • B64-encode-str-impl
          • B64-encode-last-group-str
          • B64-enc1
          • B64-char-from-value
          • B64-encode-list-impl
        • Base64-decode-list
        • Base64-decode
        • Base64-encode-list
        • Base64-revappend-decode
        • Base64-revappend-encode
        • Base64-encode
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)))