• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
      • Open-channel-lemmas
      • Std/io/read-char$
      • Std/io/read-object
      • Std/io/open-output-channel
      • Unsound-read
      • Read-string
      • Read-bytes$
        • Read-64ule
        • Read-64ube
        • Read-64sle
        • Read-64sbe
        • Read-32ule
        • Read-32sle
        • Read-32sbe
        • Read-32ube
        • Read-16sle
        • Read-16sbe
        • Read-16ule
        • Read-16ube
        • Read-8s
        • Combine-functions
          • Combine64u
          • Combine64s
          • Combine32u
          • Combine32s
          • Combine16u
          • Combine16s
      • File-measure
      • Read-bytes$-n
      • Std/io/read-byte$
      • Std/io/open-input-channel
      • Read-file-lines-no-newlines
      • Print-compressed
      • Nthcdr-bytes
      • Read-file-lines
      • Std/io/close-output-channel
      • Read-file-characters
      • Read-file-bytes
      • Print-legibly
      • Std/io/close-input-channel
      • Read-file-objects
      • Logical-story-of-io
      • Take-bytes
      • Std/io/peek-char$
      • Read-file-characters-rev
      • Read-file-as-string
      • Std/io/write-byte$
      • Std/io/set-serialize-character
      • Std/io/print-object$
      • Std/io/princ$
      • Std/io/read-file-into-string
      • *file-types*
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Combine-functions

Combine64u

(combine64u a7 a6 a5 a4 a3 a2 a1 a0) merges unsigned bytes, producing the 64-bit unsigned interpretation of {a7, a6, a5, a4, a3, a2, a1, a0}.

Definitions and Theorems

Function: combine64u$inline

(defun combine64u$inline (a7 a6 a5 a4 a3 a2 a1 a0)
  (declare (type (unsigned-byte 8)
                 a7 a6 a5 a4 a3 a2 a1 a0))
  (mbe :logic
       (logior (ash (nfix a7) 56)
               (ash (nfix a6) 48)
               (ash (nfix a5) 40)
               (ash (nfix a4) 32)
               (ash (nfix a3) 24)
               (ash (nfix a2) 16)
               (ash (nfix a1) 8)
               (nfix a0))
       :exec
       (b* ((a1 (the (unsigned-byte 16) (ash a1 8)))
            (ans (the (unsigned-byte 16)
                      (logior (the (unsigned-byte 16) a1)
                              (the (unsigned-byte 16) a0))))
            (a2 (the (unsigned-byte 24) (ash a2 16)))
            (ans (the (unsigned-byte 24)
                      (logior (the (unsigned-byte 24) a2)
                              (the (unsigned-byte 24) ans))))
            (a3 (the (unsigned-byte 32) (ash a3 24)))
            (ans (the (unsigned-byte 32)
                      (logior (the (unsigned-byte 32) a3)
                              (the (unsigned-byte 32) ans))))
            (a4 (the (unsigned-byte 40) (ash a4 32)))
            (ans (the (unsigned-byte 40)
                      (logior (the (unsigned-byte 40) a4)
                              (the (unsigned-byte 40) ans))))
            (a5 (the (unsigned-byte 48) (ash a5 40)))
            (ans (the (unsigned-byte 48)
                      (logior (the (unsigned-byte 48) a5)
                              (the (unsigned-byte 48) ans))))
            (a6 (the (unsigned-byte 56) (ash a6 48)))
            (ans (the (unsigned-byte 56)
                      (logior (the (unsigned-byte 56) a6)
                              (the (unsigned-byte 56) ans))))
            (a7 (the (unsigned-byte 64) (ash a7 56))))
         (the (unsigned-byte 64)
              (logior (the (unsigned-byte 64) a7)
                      (the (unsigned-byte 56) ans))))))

Theorem: combine64u-unsigned-byte

(defthm combine64u-unsigned-byte
  (implies (and (force (unsigned-byte-p 8 a7))
                (force (unsigned-byte-p 8 a6))
                (force (unsigned-byte-p 8 a5))
                (force (unsigned-byte-p 8 a4))
                (force (unsigned-byte-p 8 a3))
                (force (unsigned-byte-p 8 a2))
                (force (unsigned-byte-p 8 a1))
                (force (unsigned-byte-p 8 a0)))
           (unsigned-byte-p 64
                            (combine64u a7 a6 a5 a4 a3 a2 a1 a0))))