• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • 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->shndx
          • Elf64_sym->other
          • Elf64_sym-fix
          • Elf64_sym->size
          • Elf64_sym->name
          • Elf64_sym->info
        • Elf32_sym
        • Elf-header
        • Elf-section-header
        • Elf64-segment-header
        • Elf32-segment-header
        • Elf_bits32
        • Elf_bits8
        • Elf_bits64
        • Elf_bits16
        • Section-info
        • Read-elf-header
        • Read-section-headers
        • Read-segment-headers-64
        • Read-segment-headers-32
        • Read-section-names
        • Elf64_sym-info
        • Elf32_sym-info
        • Parse-symtab-entries
        • Is-elf-content-p
        • Populate-elf-contents
        • Get-string-section-data
        • Get-section-info1
        • Set-elf-stobj-fields
        • Get-named-section-headers
        • Elf-read-mem-null-term
        • Get-section-info
        • Find-label-address-from-elf-symtab-info
        • Section-names
        • Get-symtab-entries
        • Populate-elf
        • Get-label-addresses
        • Get-label-address
        • Elf-read-string-null-term
        • 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
      • Charlist->bytes
      • Take-till-zero
      • Merge-bytes
      • Bytes->charlist
      • Bytes->string
      • String->bytes
    • Axe
  • Testing-utilities
  • Math

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

Fixing function for elf64_sym bit structures.

Elf64_sym->size

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

Elf64_sym->name

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

Elf64_sym->info

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