• 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

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