		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Combine-bytes

Combine a list of bytes, LSB-first, into a single unsigned number

Signature
(combine-bytes bytes) → *

Definitions and Theorems

Function: combine-bytes

(defun combine-bytes (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (let ((__function__ 'combine-bytes))
    (declare (ignorable __function__))
    (if (endp bytes)
        0
      (logapp 8
              (if (mbt (unsigned-byte-p 8 (car bytes)))
                  (car bytes)
                0)
              (combine-bytes (cdr bytes))))))

Theorem: natp-combine-bytes

(defthm natp-combine-bytes
  (implies (force (byte-listp bytes))
           (natp (combine-bytes bytes)))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-of-combine-bytes

(defthm unsigned-byte-p-of-combine-bytes
  (implies (and (equal n (ash (len bytes) 3))
                (byte-listp bytes))
           (unsigned-byte-p n (combine-bytes bytes)))
  :rule-classes
  ((:rewrite)
   (:linear :corollary (implies (and (equal n (ash (len bytes) 3))
                                     (byte-listp bytes))
                                (<= 0 (combine-bytes bytes))))))

Theorem: size-of-combine-bytes

(defthm size-of-combine-bytes
  (implies (and (equal l (len bytes))
                (byte-listp bytes))
           (< (combine-bytes bytes)
              (expt 2 (ash l 3))))
  :rule-classes :linear)