• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Execloader
      • Elf-reader
      • Mach-o-reader
      • Merge-first-split-bytes
      • Split-bytes
      • Charlist->bytes
      • Take-till-zero
      • Merge-bytes
      • Bytes->charlist
      • Bytes->string
      • String->bytes
    • Axe
  • Testing-utilities
  • Math

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