• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
    • Execloader
      • Elf-reader
        • Elf64_sym
          • !elf64_sym->value
          • !elf64_sym->shndx
          • !elf64_sym->other
          • !elf64_sym->size
          • !elf64_sym->name
          • !elf64_sym->info
          • Elf64_sym-p
          • Elf64_sym->value
          • Elf64_sym->size
          • Elf64_sym->shndx
          • Elf64_sym->other
          • Elf64_sym->info
          • Elf64_sym-fix
          • Elf64_sym->name
        • Elf32_sym
        • Elf-header
        • Elf-section-header
        • Elf64-segment-header
        • Elf32-segment-header
        • Elf_bits32
        • Elf_bits8
        • Elf_bits64
        • Elf_bits16
        • Section-info
        • Read-section-headers
        • Read-segment-headers-64
        • Read-segment-headers-32
        • Read-section-names
        • Elf64_sym-info
        • Elf32_sym-info
        • Read-elf-header
        • Parse-symtab-entries
        • Populate-elf-contents
        • Is-elf-content-p
        • Get-string-section-data
        • Get-section-info1
        • Set-elf-stobj-fields
        • Get-named-section-headers
        • Elf-read-mem-null-term
        • Get-section-info
        • Get-symtab-entries
        • Find-label-address-from-elf-symtab-info
        • Section-names
        • Populate-elf
        • Get-label-addresses
        • Elf-read-string-null-term
        • Get-label-address
        • Good-elf-p
        • Elf64_sym-equiv-under-mask
        • Elf64-segment-headers
        • Elf32_sym-equiv-under-mask
        • Elf32-segment-headers
        • Section-info-list
        • Elf64_sym-info-list
        • Elf32_sym-info-list
        • Elf-section-headers
        • Elf64_sym-debug
        • Elf32_sym-debug
      • 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

• Elf-reader

Elf64_sym

An 192-bit unsigned bitstruct type.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 192-bit integer.

Fields

name — elf_bits32

info — elf_bits8

other — elf_bits8

shndx — elf_bits16

value — elf_bits64

size — elf_bits64

Definitions and Theorems

Function: elf64_sym-p

(defun elf64_sym-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'elf64_sym-p))
  (declare (ignorable __function__))
  (mbe
   :logic (unsigned-byte-p 192 x)
   :exec
   (and
    (natp x)
    (<
     x
     6277101735386680763835789423207666416102355444464034512896)))))

Theorem: elf64_sym-p-when-unsigned-byte-p

(defthm elf64_sym-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 192 x)
           (elf64_sym-p x)))

Theorem: unsigned-byte-p-when-elf64_sym-p

(defthm unsigned-byte-p-when-elf64_sym-p
  (implies (elf64_sym-p x)
           (unsigned-byte-p 192 x)))

Theorem: elf64_sym-p-compound-recognizer

(defthm elf64_sym-p-compound-recognizer
  (implies (elf64_sym-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: elf64_sym-fix

(defun elf64_sym-fix (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (let ((__function__ 'elf64_sym-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 192 x) :exec x)))

Theorem: elf64_sym-p-of-elf64_sym-fix

(defthm elf64_sym-p-of-elf64_sym-fix
  (b* ((fty::fixed (elf64_sym-fix x)))
    (elf64_sym-p fty::fixed))
  :rule-classes :rewrite)

Theorem: elf64_sym-fix-when-elf64_sym-p

(defthm elf64_sym-fix-when-elf64_sym-p
  (implies (elf64_sym-p x)
           (equal (elf64_sym-fix x) x)))

Function: elf64_sym-equiv$inline

(defun elf64_sym-equiv$inline (x y)
  (declare (xargs :guard (and (elf64_sym-p x) (elf64_sym-p y))))
  (equal (elf64_sym-fix x)
         (elf64_sym-fix y)))

Theorem: elf64_sym-equiv-is-an-equivalence

(defthm elf64_sym-equiv-is-an-equivalence
  (and (booleanp (elf64_sym-equiv x y))
       (elf64_sym-equiv x x)
       (implies (elf64_sym-equiv x y)
                (elf64_sym-equiv y x))
       (implies (and (elf64_sym-equiv x y)
                     (elf64_sym-equiv y z))
                (elf64_sym-equiv x z)))
  :rule-classes (:equivalence))

Theorem: elf64_sym-equiv-implies-equal-elf64_sym-fix-1

(defthm elf64_sym-equiv-implies-equal-elf64_sym-fix-1
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym-fix x)
                  (elf64_sym-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: elf64_sym-fix-under-elf64_sym-equiv

(defthm elf64_sym-fix-under-elf64_sym-equiv
  (elf64_sym-equiv (elf64_sym-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: elf64_sym

(defun elf64_sym (name info other shndx value size)
 (declare (xargs :guard (and (elf_bits32-p name)
                             (elf_bits8-p info)
                             (elf_bits8-p other)
                             (elf_bits16-p shndx)
                             (elf_bits64-p value)
                             (elf_bits64-p size))))
 (let ((__function__ 'elf64_sym))
  (declare (ignorable __function__))
  (b* ((name (mbe :logic (elf_bits32-fix name)
                  :exec name))
       (info (mbe :logic (elf_bits8-fix info)
                  :exec info))
       (other (mbe :logic (elf_bits8-fix other)
                   :exec other))
       (shndx (mbe :logic (elf_bits16-fix shndx)
                   :exec shndx))
       (value (mbe :logic (elf_bits64-fix value)
                   :exec value))
       (size (mbe :logic (elf_bits64-fix size)
                  :exec size)))
   (logapp
      32 name
      (logapp 8 info
              (logapp 8 other
                      (logapp 16 shndx (logapp 64 value size))))))))

Theorem: elf64_sym-p-of-elf64_sym

(defthm elf64_sym-p-of-elf64_sym
  (b* ((elf64_sym (elf64_sym name info other shndx value size)))
    (elf64_sym-p elf64_sym))
  :rule-classes :rewrite)

Theorem: elf64_sym-of-elf_bits32-fix-name

(defthm elf64_sym-of-elf_bits32-fix-name
  (equal (elf64_sym (elf_bits32-fix name)
                    info other shndx value size)
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits32-equiv-congruence-on-name

(defthm elf64_sym-elf_bits32-equiv-congruence-on-name
  (implies (elf_bits32-equiv name name-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name-equiv
                             info other shndx value size)))
  :rule-classes :congruence)

Theorem: elf64_sym-of-elf_bits8-fix-info

(defthm elf64_sym-of-elf_bits8-fix-info
  (equal (elf64_sym name (elf_bits8-fix info)
                    other shndx value size)
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits8-equiv-congruence-on-info

(defthm elf64_sym-elf_bits8-equiv-congruence-on-info
  (implies (elf_bits8-equiv info info-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name
                             info-equiv other shndx value size)))
  :rule-classes :congruence)

Theorem: elf64_sym-of-elf_bits8-fix-other

(defthm elf64_sym-of-elf_bits8-fix-other
  (equal (elf64_sym name info (elf_bits8-fix other)
                    shndx value size)
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits8-equiv-congruence-on-other

(defthm elf64_sym-elf_bits8-equiv-congruence-on-other
  (implies (elf_bits8-equiv other other-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name
                             info other-equiv shndx value size)))
  :rule-classes :congruence)

Theorem: elf64_sym-of-elf_bits16-fix-shndx

(defthm elf64_sym-of-elf_bits16-fix-shndx
  (equal (elf64_sym name info other (elf_bits16-fix shndx)
                    value size)
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits16-equiv-congruence-on-shndx

(defthm elf64_sym-elf_bits16-equiv-congruence-on-shndx
  (implies (elf_bits16-equiv shndx shndx-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name
                             info other shndx-equiv value size)))
  :rule-classes :congruence)

Theorem: elf64_sym-of-elf_bits64-fix-value

(defthm elf64_sym-of-elf_bits64-fix-value
  (equal (elf64_sym name
                    info other shndx (elf_bits64-fix value)
                    size)
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits64-equiv-congruence-on-value

(defthm elf64_sym-elf_bits64-equiv-congruence-on-value
  (implies (elf_bits64-equiv value value-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name
                             info other shndx value-equiv size)))
  :rule-classes :congruence)

Theorem: elf64_sym-of-elf_bits64-fix-size

(defthm elf64_sym-of-elf_bits64-fix-size
  (equal (elf64_sym name info
                    other shndx value (elf_bits64-fix size))
         (elf64_sym name info other shndx value size)))

Theorem: elf64_sym-elf_bits64-equiv-congruence-on-size

(defthm elf64_sym-elf_bits64-equiv-congruence-on-size
  (implies (elf_bits64-equiv size size-equiv)
           (equal (elf64_sym name info other shndx value size)
                  (elf64_sym name
                             info other shndx value size-equiv)))
  :rule-classes :congruence)

Function: elf64_sym-equiv-under-mask

(defun elf64_sym-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (elf64_sym-p x)
                              (elf64_sym-p x1)
                              (integerp mask))))
  (let ((__function__ 'elf64_sym-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (elf64_sym-fix x)
                               (elf64_sym-fix x1)
                               mask)))

Function: elf64_sym->name

(defun elf64_sym->name (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 0 :width 32))
       :exec (the (unsigned-byte 32)
                  (logand (the (unsigned-byte 32) 4294967295)
                          (the (unsigned-byte 192) x)))))

Theorem: elf_bits32-p-of-elf64_sym->name

(defthm elf_bits32-p-of-elf64_sym->name
  (b* ((name (elf64_sym->name x)))
    (elf_bits32-p name))
  :rule-classes :rewrite)

Theorem: elf64_sym->name-of-elf64_sym-fix-x

(defthm elf64_sym->name-of-elf64_sym-fix-x
  (equal (elf64_sym->name (elf64_sym-fix x))
         (elf64_sym->name x)))

Theorem: elf64_sym->name-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->name-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->name x)
                  (elf64_sym->name x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->name-of-elf64_sym

(defthm elf64_sym->name-of-elf64_sym
 (equal
      (elf64_sym->name (elf64_sym name info other shndx value size))
      (elf_bits32-fix name)))

Theorem: elf64_sym->name-of-write-with-mask

(defthm elf64_sym->name-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x elf64_sym-equiv-under-mask)
                (elf64_sym-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4294967295)
                       0))
           (equal (elf64_sym->name x)
                  (elf64_sym->name y))))

Function: elf64_sym->info

(defun elf64_sym->info (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 32 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 160)
                               (ash (the (unsigned-byte 192) x)
                                    -32))))))

Theorem: elf_bits8-p-of-elf64_sym->info

(defthm elf_bits8-p-of-elf64_sym->info
  (b* ((info (elf64_sym->info x)))
    (elf_bits8-p info))
  :rule-classes :rewrite)

Theorem: elf64_sym->info-of-elf64_sym-fix-x

(defthm elf64_sym->info-of-elf64_sym-fix-x
  (equal (elf64_sym->info (elf64_sym-fix x))
         (elf64_sym->info x)))

Theorem: elf64_sym->info-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->info-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->info x)
                  (elf64_sym->info x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->info-of-elf64_sym

(defthm elf64_sym->info-of-elf64_sym
 (equal
      (elf64_sym->info (elf64_sym name info other shndx value size))
      (elf_bits8-fix info)))

Theorem: elf64_sym->info-of-write-with-mask

(defthm elf64_sym->info-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x elf64_sym-equiv-under-mask)
                (elf64_sym-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask)
                               1095216660480)
                       0))
           (equal (elf64_sym->info x)
                  (elf64_sym->info y))))

Function: elf64_sym->other

(defun elf64_sym->other (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 40 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 152)
                               (ash (the (unsigned-byte 192) x)
                                    -40))))))

Theorem: elf_bits8-p-of-elf64_sym->other

(defthm elf_bits8-p-of-elf64_sym->other
  (b* ((other (elf64_sym->other x)))
    (elf_bits8-p other))
  :rule-classes :rewrite)

Theorem: elf64_sym->other-of-elf64_sym-fix-x

(defthm elf64_sym->other-of-elf64_sym-fix-x
  (equal (elf64_sym->other (elf64_sym-fix x))
         (elf64_sym->other x)))

Theorem: elf64_sym->other-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->other-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->other x)
                  (elf64_sym->other x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->other-of-elf64_sym

(defthm elf64_sym->other-of-elf64_sym
 (equal
     (elf64_sym->other (elf64_sym name info other shndx value size))
     (elf_bits8-fix other)))

Theorem: elf64_sym->other-of-write-with-mask

(defthm elf64_sym->other-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x elf64_sym-equiv-under-mask)
                (elf64_sym-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask)
                               280375465082880)
                       0))
           (equal (elf64_sym->other x)
                  (elf64_sym->other y))))

Function: elf64_sym->shndx

(defun elf64_sym->shndx (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 48 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 144)
                               (ash (the (unsigned-byte 192) x)
                                    -48))))))

Theorem: elf_bits16-p-of-elf64_sym->shndx

(defthm elf_bits16-p-of-elf64_sym->shndx
  (b* ((shndx (elf64_sym->shndx x)))
    (elf_bits16-p shndx))
  :rule-classes :rewrite)

Theorem: elf64_sym->shndx-of-elf64_sym-fix-x

(defthm elf64_sym->shndx-of-elf64_sym-fix-x
  (equal (elf64_sym->shndx (elf64_sym-fix x))
         (elf64_sym->shndx x)))

Theorem: elf64_sym->shndx-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->shndx-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->shndx x)
                  (elf64_sym->shndx x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->shndx-of-elf64_sym

(defthm elf64_sym->shndx-of-elf64_sym
 (equal
     (elf64_sym->shndx (elf64_sym name info other shndx value size))
     (elf_bits16-fix shndx)))

Theorem: elf64_sym->shndx-of-write-with-mask

(defthm elf64_sym->shndx-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x elf64_sym-equiv-under-mask)
                (elf64_sym-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask)
                               18446462598732840960)
                       0))
           (equal (elf64_sym->shndx x)
                  (elf64_sym->shndx y))))

Function: elf64_sym->value

(defun elf64_sym->value (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 64 :width 64))
       :exec (the (unsigned-byte 64)
                  (logand (the (unsigned-byte 64)
                               18446744073709551615)
                          (the (unsigned-byte 128)
                               (ash (the (unsigned-byte 192) x)
                                    -64))))))

Theorem: elf_bits64-p-of-elf64_sym->value

(defthm elf_bits64-p-of-elf64_sym->value
  (b* ((value (elf64_sym->value x)))
    (elf_bits64-p value))
  :rule-classes :rewrite)

Theorem: elf64_sym->value-of-elf64_sym-fix-x

(defthm elf64_sym->value-of-elf64_sym-fix-x
  (equal (elf64_sym->value (elf64_sym-fix x))
         (elf64_sym->value x)))

Theorem: elf64_sym->value-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->value-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->value x)
                  (elf64_sym->value x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->value-of-elf64_sym

(defthm elf64_sym->value-of-elf64_sym
 (equal
     (elf64_sym->value (elf64_sym name info other shndx value size))
     (elf_bits64-fix value)))

Theorem: elf64_sym->value-of-write-with-mask

(defthm elf64_sym->value-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x elf64_sym-equiv-under-mask)
            (elf64_sym-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask)
                           340282366920938463444927863358058659840)
                   0))
       (equal (elf64_sym->value x)
              (elf64_sym->value y))))

Function: elf64_sym->size

(defun elf64_sym->size (x)
  (declare (xargs :guard (elf64_sym-p x)))
  (mbe :logic
       (let ((x (elf64_sym-fix x)))
         (part-select x :low 128 :width 64))
       :exec (the (unsigned-byte 64)
                  (logand (the (unsigned-byte 64)
                               18446744073709551615)
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 192) x)
                                    -128))))))

Theorem: elf_bits64-p-of-elf64_sym->size

(defthm elf_bits64-p-of-elf64_sym->size
  (b* ((size (elf64_sym->size x)))
    (elf_bits64-p size))
  :rule-classes :rewrite)

Theorem: elf64_sym->size-of-elf64_sym-fix-x

(defthm elf64_sym->size-of-elf64_sym-fix-x
  (equal (elf64_sym->size (elf64_sym-fix x))
         (elf64_sym->size x)))

Theorem: elf64_sym->size-elf64_sym-equiv-congruence-on-x

(defthm elf64_sym->size-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (elf64_sym->size x)
                  (elf64_sym->size x-equiv)))
  :rule-classes :congruence)

Theorem: elf64_sym->size-of-elf64_sym

(defthm elf64_sym->size-of-elf64_sym
 (equal
      (elf64_sym->size (elf64_sym name info other shndx value size))
      (elf_bits64-fix size)))

Theorem: elf64_sym->size-of-write-with-mask

(defthm elf64_sym->size-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps
        x elf64_sym-equiv-under-mask)
   (elf64_sym-equiv-under-mask x y fty::mask)
   (equal
    (logand
         (lognot fty::mask)
         6277101735386680763495507056286727952638980837032266301440)
    0))
  (equal (elf64_sym->size x)
         (elf64_sym->size y))))

Theorem: elf64_sym-fix-in-terms-of-elf64_sym

(defthm elf64_sym-fix-in-terms-of-elf64_sym
  (equal (elf64_sym-fix x)
         (change-elf64_sym x)))

Function: !elf64_sym->name

(defun !elf64_sym->name (name x)
 (declare (xargs :guard (and (elf_bits32-p name)
                             (elf64_sym-p x))))
 (mbe :logic
      (b* ((name (mbe :logic (elf_bits32-fix name)
                      :exec name))
           (x (elf64_sym-fix x)))
        (part-install name x :width 32 :low 0))
      :exec
      (the (unsigned-byte 192)
           (logior (the (unsigned-byte 192)
                        (logand (the (unsigned-byte 192) x)
                                (the (signed-byte 33) -4294967296)))
                   (the (unsigned-byte 32) name)))))

Theorem: elf64_sym-p-of-!elf64_sym->name

(defthm elf64_sym-p-of-!elf64_sym->name
  (b* ((new-x (!elf64_sym->name name x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->name-of-elf_bits32-fix-name

(defthm !elf64_sym->name-of-elf_bits32-fix-name
  (equal (!elf64_sym->name (elf_bits32-fix name)
                           x)
         (!elf64_sym->name name x)))

Theorem: !elf64_sym->name-elf_bits32-equiv-congruence-on-name

(defthm !elf64_sym->name-elf_bits32-equiv-congruence-on-name
  (implies (elf_bits32-equiv name name-equiv)
           (equal (!elf64_sym->name name x)
                  (!elf64_sym->name name-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->name-of-elf64_sym-fix-x

(defthm !elf64_sym->name-of-elf64_sym-fix-x
  (equal (!elf64_sym->name name (elf64_sym-fix x))
         (!elf64_sym->name name x)))

Theorem: !elf64_sym->name-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->name-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->name name x)
                  (!elf64_sym->name name x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->name-is-elf64_sym

(defthm !elf64_sym->name-is-elf64_sym
  (equal (!elf64_sym->name name x)
         (change-elf64_sym x :name name)))

Theorem: elf64_sym->name-of-!elf64_sym->name

(defthm elf64_sym->name-of-!elf64_sym->name
  (b* ((?new-x (!elf64_sym->name name x)))
    (equal (elf64_sym->name new-x)
           (elf_bits32-fix name))))

Theorem: !elf64_sym->name-equiv-under-mask

(defthm !elf64_sym->name-equiv-under-mask
  (b* ((?new-x (!elf64_sym->name name x)))
    (elf64_sym-equiv-under-mask new-x x -4294967296)))

Function: !elf64_sym->info

(defun !elf64_sym->info (info x)
 (declare (xargs :guard (and (elf_bits8-p info)
                             (elf64_sym-p x))))
 (mbe
   :logic
   (b* ((info (mbe :logic (elf_bits8-fix info)
                   :exec info))
        (x (elf64_sym-fix x)))
     (part-install info x :width 8 :low 32))
   :exec
   (the (unsigned-byte 192)
        (logior (the (unsigned-byte 192)
                     (logand (the (unsigned-byte 192) x)
                             (the (signed-byte 41) -1095216660481)))
                (the (unsigned-byte 40)
                     (ash (the (unsigned-byte 8) info)
                          32))))))

Theorem: elf64_sym-p-of-!elf64_sym->info

(defthm elf64_sym-p-of-!elf64_sym->info
  (b* ((new-x (!elf64_sym->info info x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->info-of-elf_bits8-fix-info

(defthm !elf64_sym->info-of-elf_bits8-fix-info
  (equal (!elf64_sym->info (elf_bits8-fix info)
                           x)
         (!elf64_sym->info info x)))

Theorem: !elf64_sym->info-elf_bits8-equiv-congruence-on-info

(defthm !elf64_sym->info-elf_bits8-equiv-congruence-on-info
  (implies (elf_bits8-equiv info info-equiv)
           (equal (!elf64_sym->info info x)
                  (!elf64_sym->info info-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->info-of-elf64_sym-fix-x

(defthm !elf64_sym->info-of-elf64_sym-fix-x
  (equal (!elf64_sym->info info (elf64_sym-fix x))
         (!elf64_sym->info info x)))

Theorem: !elf64_sym->info-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->info-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->info info x)
                  (!elf64_sym->info info x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->info-is-elf64_sym

(defthm !elf64_sym->info-is-elf64_sym
  (equal (!elf64_sym->info info x)
         (change-elf64_sym x :info info)))

Theorem: elf64_sym->info-of-!elf64_sym->info

(defthm elf64_sym->info-of-!elf64_sym->info
  (b* ((?new-x (!elf64_sym->info info x)))
    (equal (elf64_sym->info new-x)
           (elf_bits8-fix info))))

Theorem: !elf64_sym->info-equiv-under-mask

(defthm !elf64_sym->info-equiv-under-mask
  (b* ((?new-x (!elf64_sym->info info x)))
    (elf64_sym-equiv-under-mask new-x x -1095216660481)))

Function: !elf64_sym->other

(defun !elf64_sym->other (other x)
  (declare (xargs :guard (and (elf_bits8-p other)
                              (elf64_sym-p x))))
  (mbe :logic
       (b* ((other (mbe :logic (elf_bits8-fix other)
                        :exec other))
            (x (elf64_sym-fix x)))
         (part-install other x :width 8 :low 40))
       :exec (the (unsigned-byte 192)
                  (logior (the (unsigned-byte 192)
                               (logand (the (unsigned-byte 192) x)
                                       (the (signed-byte 49)
                                            -280375465082881)))
                          (the (unsigned-byte 48)
                               (ash (the (unsigned-byte 8) other)
                                    40))))))

Theorem: elf64_sym-p-of-!elf64_sym->other

(defthm elf64_sym-p-of-!elf64_sym->other
  (b* ((new-x (!elf64_sym->other other x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->other-of-elf_bits8-fix-other

(defthm !elf64_sym->other-of-elf_bits8-fix-other
  (equal (!elf64_sym->other (elf_bits8-fix other)
                            x)
         (!elf64_sym->other other x)))

Theorem: !elf64_sym->other-elf_bits8-equiv-congruence-on-other

(defthm !elf64_sym->other-elf_bits8-equiv-congruence-on-other
  (implies (elf_bits8-equiv other other-equiv)
           (equal (!elf64_sym->other other x)
                  (!elf64_sym->other other-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->other-of-elf64_sym-fix-x

(defthm !elf64_sym->other-of-elf64_sym-fix-x
  (equal (!elf64_sym->other other (elf64_sym-fix x))
         (!elf64_sym->other other x)))

Theorem: !elf64_sym->other-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->other-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->other other x)
                  (!elf64_sym->other other x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->other-is-elf64_sym

(defthm !elf64_sym->other-is-elf64_sym
  (equal (!elf64_sym->other other x)
         (change-elf64_sym x :other other)))

Theorem: elf64_sym->other-of-!elf64_sym->other

(defthm elf64_sym->other-of-!elf64_sym->other
  (b* ((?new-x (!elf64_sym->other other x)))
    (equal (elf64_sym->other new-x)
           (elf_bits8-fix other))))

Theorem: !elf64_sym->other-equiv-under-mask

(defthm !elf64_sym->other-equiv-under-mask
  (b* ((?new-x (!elf64_sym->other other x)))
    (elf64_sym-equiv-under-mask new-x x -280375465082881)))

Function: !elf64_sym->shndx

(defun !elf64_sym->shndx (shndx x)
  (declare (xargs :guard (and (elf_bits16-p shndx)
                              (elf64_sym-p x))))
  (mbe :logic
       (b* ((shndx (mbe :logic (elf_bits16-fix shndx)
                        :exec shndx))
            (x (elf64_sym-fix x)))
         (part-install shndx x
                       :width 16
                       :low 48))
       :exec (the (unsigned-byte 192)
                  (logior (the (unsigned-byte 192)
                               (logand (the (unsigned-byte 192) x)
                                       (the (signed-byte 65)
                                            -18446462598732840961)))
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 16) shndx)
                                    48))))))

Theorem: elf64_sym-p-of-!elf64_sym->shndx

(defthm elf64_sym-p-of-!elf64_sym->shndx
  (b* ((new-x (!elf64_sym->shndx shndx x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->shndx-of-elf_bits16-fix-shndx

(defthm !elf64_sym->shndx-of-elf_bits16-fix-shndx
  (equal (!elf64_sym->shndx (elf_bits16-fix shndx)
                            x)
         (!elf64_sym->shndx shndx x)))

Theorem: !elf64_sym->shndx-elf_bits16-equiv-congruence-on-shndx

(defthm !elf64_sym->shndx-elf_bits16-equiv-congruence-on-shndx
  (implies (elf_bits16-equiv shndx shndx-equiv)
           (equal (!elf64_sym->shndx shndx x)
                  (!elf64_sym->shndx shndx-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->shndx-of-elf64_sym-fix-x

(defthm !elf64_sym->shndx-of-elf64_sym-fix-x
  (equal (!elf64_sym->shndx shndx (elf64_sym-fix x))
         (!elf64_sym->shndx shndx x)))

Theorem: !elf64_sym->shndx-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->shndx-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->shndx shndx x)
                  (!elf64_sym->shndx shndx x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->shndx-is-elf64_sym

(defthm !elf64_sym->shndx-is-elf64_sym
  (equal (!elf64_sym->shndx shndx x)
         (change-elf64_sym x :shndx shndx)))

Theorem: elf64_sym->shndx-of-!elf64_sym->shndx

(defthm elf64_sym->shndx-of-!elf64_sym->shndx
  (b* ((?new-x (!elf64_sym->shndx shndx x)))
    (equal (elf64_sym->shndx new-x)
           (elf_bits16-fix shndx))))

Theorem: !elf64_sym->shndx-equiv-under-mask

(defthm !elf64_sym->shndx-equiv-under-mask
  (b* ((?new-x (!elf64_sym->shndx shndx x)))
    (elf64_sym-equiv-under-mask new-x x -18446462598732840961)))

Function: !elf64_sym->value

(defun !elf64_sym->value (value x)
 (declare (xargs :guard (and (elf_bits64-p value)
                             (elf64_sym-p x))))
 (mbe
  :logic
  (b* ((value (mbe :logic (elf_bits64-fix value)
                   :exec value))
       (x (elf64_sym-fix x)))
    (part-install value x
                  :width 64
                  :low 64))
  :exec
  (the
   (unsigned-byte 192)
   (logior
       (the (unsigned-byte 192)
            (logand (the (unsigned-byte 192) x)
                    (the (signed-byte 129)
                         -340282366920938463444927863358058659841)))
       (the (unsigned-byte 128)
            (ash (the (unsigned-byte 64) value)
                 64))))))

Theorem: elf64_sym-p-of-!elf64_sym->value

(defthm elf64_sym-p-of-!elf64_sym->value
  (b* ((new-x (!elf64_sym->value value x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->value-of-elf_bits64-fix-value

(defthm !elf64_sym->value-of-elf_bits64-fix-value
  (equal (!elf64_sym->value (elf_bits64-fix value)
                            x)
         (!elf64_sym->value value x)))

Theorem: !elf64_sym->value-elf_bits64-equiv-congruence-on-value

(defthm !elf64_sym->value-elf_bits64-equiv-congruence-on-value
  (implies (elf_bits64-equiv value value-equiv)
           (equal (!elf64_sym->value value x)
                  (!elf64_sym->value value-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->value-of-elf64_sym-fix-x

(defthm !elf64_sym->value-of-elf64_sym-fix-x
  (equal (!elf64_sym->value value (elf64_sym-fix x))
         (!elf64_sym->value value x)))

Theorem: !elf64_sym->value-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->value-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->value value x)
                  (!elf64_sym->value value x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->value-is-elf64_sym

(defthm !elf64_sym->value-is-elf64_sym
  (equal (!elf64_sym->value value x)
         (change-elf64_sym x :value value)))

Theorem: elf64_sym->value-of-!elf64_sym->value

(defthm elf64_sym->value-of-!elf64_sym->value
  (b* ((?new-x (!elf64_sym->value value x)))
    (equal (elf64_sym->value new-x)
           (elf_bits64-fix value))))

Theorem: !elf64_sym->value-equiv-under-mask

(defthm !elf64_sym->value-equiv-under-mask
  (b* ((?new-x (!elf64_sym->value value x)))
    (elf64_sym-equiv-under-mask
         new-x x
         -340282366920938463444927863358058659841)))

Function: !elf64_sym->size

(defun !elf64_sym->size (size x)
 (declare (xargs :guard (and (elf_bits64-p size)
                             (elf64_sym-p x))))
 (mbe
  :logic
  (b* ((size (mbe :logic (elf_bits64-fix size)
                  :exec size))
       (x (elf64_sym-fix x)))
    (part-install size x
                  :width 64
                  :low 128))
  :exec
  (the
   (unsigned-byte 192)
   (logior
    (the
     (unsigned-byte 192)
     (logand
      (the (unsigned-byte 192) x)
      (the
       (signed-byte 193)
       -6277101735386680763495507056286727952638980837032266301441)))
    (the (unsigned-byte 192)
         (ash (the (unsigned-byte 64) size)
              128))))))

Theorem: elf64_sym-p-of-!elf64_sym->size

(defthm elf64_sym-p-of-!elf64_sym->size
  (b* ((new-x (!elf64_sym->size size x)))
    (elf64_sym-p new-x))
  :rule-classes :rewrite)

Theorem: !elf64_sym->size-of-elf_bits64-fix-size

(defthm !elf64_sym->size-of-elf_bits64-fix-size
  (equal (!elf64_sym->size (elf_bits64-fix size)
                           x)
         (!elf64_sym->size size x)))

Theorem: !elf64_sym->size-elf_bits64-equiv-congruence-on-size

(defthm !elf64_sym->size-elf_bits64-equiv-congruence-on-size
  (implies (elf_bits64-equiv size size-equiv)
           (equal (!elf64_sym->size size x)
                  (!elf64_sym->size size-equiv x)))
  :rule-classes :congruence)

Theorem: !elf64_sym->size-of-elf64_sym-fix-x

(defthm !elf64_sym->size-of-elf64_sym-fix-x
  (equal (!elf64_sym->size size (elf64_sym-fix x))
         (!elf64_sym->size size x)))

Theorem: !elf64_sym->size-elf64_sym-equiv-congruence-on-x

(defthm !elf64_sym->size-elf64_sym-equiv-congruence-on-x
  (implies (elf64_sym-equiv x x-equiv)
           (equal (!elf64_sym->size size x)
                  (!elf64_sym->size size x-equiv)))
  :rule-classes :congruence)

Theorem: !elf64_sym->size-is-elf64_sym

(defthm !elf64_sym->size-is-elf64_sym
  (equal (!elf64_sym->size size x)
         (change-elf64_sym x :size size)))

Theorem: elf64_sym->size-of-!elf64_sym->size

(defthm elf64_sym->size-of-!elf64_sym->size
  (b* ((?new-x (!elf64_sym->size size x)))
    (equal (elf64_sym->size new-x)
           (elf_bits64-fix size))))

Theorem: !elf64_sym->size-equiv-under-mask

(defthm !elf64_sym->size-equiv-under-mask
  (b* ((?new-x (!elf64_sym->size size x)))
    (elf64_sym-equiv-under-mask
         new-x x
         340282366920938463463374607431768211455)))

Function: elf64_sym-debug

(defun elf64_sym-debug (x)
 (declare (xargs :guard (elf64_sym-p x)))
 (let ((__function__ 'elf64_sym-debug))
  (declare (ignorable __function__))
  (b* (((elf64_sym x)))
   (cons
      (cons 'name x.name)
      (cons (cons 'info x.info)
            (cons (cons 'other x.other)
                  (cons (cons 'shndx x.shndx)
                        (cons (cons 'value x.value)
                              (cons (cons 'size x.size) nil)))))))))

Subtopics

!elf64_sym->value

Update the |ACL2|::|VALUE| field of a elf64_sym bit structure.

!elf64_sym->shndx

Update the |EXLD|::|SHNDX| field of a elf64_sym bit structure.

!elf64_sym->other

Update the |EXLD|::|OTHER| field of a elf64_sym bit structure.

!elf64_sym->size

Update the |EXLD|::|SIZE| field of a elf64_sym bit structure.

!elf64_sym->name

Update the |EXLD|::|NAME| field of a elf64_sym bit structure.

!elf64_sym->info

Update the |EXLD|::|INFO| field of a elf64_sym bit structure.

Elf64_sym-p

Recognizer for elf64_sym bit structures.

Elf64_sym->value

Access the |ACL2|::|VALUE| field of a elf64_sym bit structure.

Elf64_sym->size

Access the |EXLD|::|SIZE| field of a elf64_sym bit structure.

Elf64_sym->shndx

Access the |EXLD|::|SHNDX| field of a elf64_sym bit structure.

Elf64_sym->other

Access the |EXLD|::|OTHER| field of a elf64_sym bit structure.

Elf64_sym->info

Access the |EXLD|::|INFO| field of a elf64_sym bit structure.

Elf64_sym-fix

Fixing function for elf64_sym bit structures.

Elf64_sym->name

Access the |EXLD|::|NAME| field of a elf64_sym bit structure.