• 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

    Charlist->bytes

    Convert a list of characters to a list of bytes.

    Signature
    (charlist->bytes charlist) → bl
    Arguments
    charlist — Guard (character-listp charlist).
    Returns
    bl — Type (byte-listp bl), given the guard.

    Definitions and Theorems

    Function: charlist->bytes

    (defun charlist->bytes (charlist)
      (declare (xargs :guard (character-listp charlist)))
      (let ((__function__ 'charlist->bytes))
        (declare (ignorable __function__))
        (if (endp charlist)
            nil
          (cons (char-code (car charlist))
                (charlist->bytes (cdr charlist))))))

    Theorem: byte-listp-of-charlist->bytes

    (defthm byte-listp-of-charlist->bytes
      (implies (and (character-listp charlist))
               (b* ((bl (charlist->bytes charlist)))
                 (byte-listp bl)))
      :rule-classes :rewrite)

    Theorem: same-length-of-byte-and-character-lists

    (defthm same-length-of-byte-and-character-lists
      (b* ((?bl (charlist->bytes charlist)))
        (implies (character-listp charlist)
                 (equal (len bl) (len charlist)))))