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

• Execloader

Merge-first-split-bytes

Merge first n bytes (least-significant byte first) from bytes; return remaining bytes

Signature

(merge-first-split-bytes n bytes) → (mv merged-num rest)

Arguments

n — Guard (natp n).

bytes — Guard (byte-listp bytes).

Returns

merged-num — Type (natp merged-num).

rest — Type (byte-listp rest), given (byte-listp bytes).

Definitions and Theorems

Function: merge-first-split-bytes

(defun merge-first-split-bytes (n bytes)
  (declare (xargs :guard (and (natp n) (byte-listp bytes))))
  (let ((__function__ 'merge-first-split-bytes))
    (declare (ignorable __function__))
    (b* (((mv first rest) (split-bytes n bytes)))
      (mv (merge-bytes first) rest))))

Theorem: natp-of-merge-first-split-bytes.merged-num

(defthm natp-of-merge-first-split-bytes.merged-num
  (b* (((mv ?merged-num common-lisp::?rest)
        (merge-first-split-bytes n bytes)))
    (natp merged-num))
  :rule-classes :type-prescription)

Theorem: byte-listp-of-merge-first-split-bytes.rest

(defthm byte-listp-of-merge-first-split-bytes.rest
  (implies (byte-listp bytes)
           (b* (((mv ?merged-num common-lisp::?rest)
                 (merge-first-split-bytes n bytes)))
             (byte-listp rest)))
  :rule-classes :rewrite)

Theorem: width-of-mv-nth-0-merge-first-split-bytes

(defthm width-of-mv-nth-0-merge-first-split-bytes
  (b* (((mv ?merged-num common-lisp::?rest)
        (merge-first-split-bytes n bytes)))
    (implies (and (equal m (* 8 n)) (natp n))
             (unsigned-byte-p m merged-num))))

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

(defthm len-of-mv-nth-1-merge-first-split-bytes
  (b* (((mv ?merged-num common-lisp::?rest)
        (merge-first-split-bytes n bytes)))
    (equal (len rest)
           (nfix (- (len bytes) (nfix n))))))