		Search-engine friendly clone of the ACL2 documentation.

Execloader

Split-bytes

Split bytes into two lists, where first part has n elements

Signature
(split-bytes n bytes) → (mv one two)
Arguments: n — Guard (natp n).; bytes — Guard (byte-listp bytes).
Returns: one — Type (byte-listp one), given (byte-listp bytes).; two — Type (byte-listp two), given (byte-listp bytes).

Definitions and Theorems

Function: split-bytes

(defun split-bytes (n bytes)
 (declare (xargs :guard (and (natp n) (byte-listp bytes))))
 (let ((__function__ 'split-bytes))
  (declare (ignorable __function__))
  (b*
   ((rest (nthcdr n bytes))
    ((unless (<= n (len bytes)))
     (prog2$
      (raise
       "Not enough bytes to split into two by ~x0! (len bytes): ~x1"
       n (len bytes))
      (mv (make-list n :initial-element 0)
          rest)))
    (first (take n bytes)))
   (mv first rest))))

Theorem: byte-listp-of-split-bytes.one

(defthm byte-listp-of-split-bytes.one
  (implies (byte-listp bytes)
           (b* (((mv ?one ?two) (split-bytes n bytes)))
             (byte-listp one)))
  :rule-classes :rewrite)

Theorem: byte-listp-of-split-bytes.two

(defthm byte-listp-of-split-bytes.two
  (implies (byte-listp bytes)
           (b* (((mv ?one ?two) (split-bytes n bytes)))
             (byte-listp two)))
  :rule-classes :rewrite)

Theorem: len-of-mv-nth-0-split-bytes

(defthm len-of-mv-nth-0-split-bytes
  (b* (((mv ?one ?two) (split-bytes n bytes)))
    (equal (len one) (nfix n))))

Theorem: len-of-mv-nth-1-split-bytes

(defthm len-of-mv-nth-1-split-bytes
  (b* (((mv ?one ?two) (split-bytes n bytes)))
    (equal (len two)
           (nfix (- (len bytes) (nfix n))))))