• 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
        • Elf64_sym
        • Elf32_sym
          • !elf32_sym->value
          • !elf32_sym->shndx
          • !elf32_sym->other
          • !elf32_sym->size
          • !elf32_sym->name
          • !elf32_sym->info
          • Elf32_sym-p
          • Elf32_sym->value
          • Elf32_sym->size
          • Elf32_sym->shndx
          • Elf32_sym->other
          • Elf32_sym-fix
          • Elf32_sym->name
          • Elf32_sym->info
        • 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

Elf32_sym

An 128-bit unsigned bitstruct type.

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

Fields

name — elf_bits32

value — elf_bits32

size — elf_bits32

info — elf_bits8

other — elf_bits8

shndx — elf_bits16

Definitions and Theorems

Function: elf32_sym-p

(defun
 elf32_sym-p (x)
 (declare (xargs :guard t))
 (let
     ((__function__ 'elf32_sym-p))
     (declare (ignorable __function__))
     (mbe :logic (unsigned-byte-p 128 x)
          :exec (and (natp x)
                     (< x
                        340282366920938463463374607431768211456)))))

Theorem: elf32_sym-p-when-unsigned-byte-p

(defthm elf32_sym-p-when-unsigned-byte-p
        (implies (unsigned-byte-p 128 x)
                 (elf32_sym-p x)))

Theorem: unsigned-byte-p-when-elf32_sym-p

(defthm unsigned-byte-p-when-elf32_sym-p
        (implies (elf32_sym-p x)
                 (unsigned-byte-p 128 x)))

Theorem: elf32_sym-p-compound-recognizer

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

Function: elf32_sym-fix

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

Theorem: elf32_sym-p-of-elf32_sym-fix

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

Theorem: elf32_sym-fix-when-elf32_sym-p

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

Function: elf32_sym-equiv$inline

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

Theorem: elf32_sym-equiv-is-an-equivalence

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

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

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

Theorem: elf32_sym-fix-under-elf32_sym-equiv

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

Function: elf32_sym

(defun
 elf32_sym
 (name value size info other shndx)
 (declare (xargs :guard (and (elf_bits32-p name)
                             (elf_bits32-p value)
                             (elf_bits32-p size)
                             (elf_bits8-p info)
                             (elf_bits8-p other)
                             (elf_bits16-p shndx))))
 (let
  ((__function__ 'elf32_sym))
  (declare (ignorable __function__))
  (b*
   ((name (mbe :logic (elf_bits32-fix name)
               :exec name))
    (value (mbe :logic (elf_bits32-fix value)
                :exec value))
    (size (mbe :logic (elf_bits32-fix size)
               :exec size))
    (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)))
   (logapp
        32 name
        (logapp 32 value
                (logapp 32 size
                        (logapp 8 info (logapp 8 other shndx))))))))

Theorem: elf32_sym-p-of-elf32_sym

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

Theorem: elf32_sym-of-elf_bits32-fix-name

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

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

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

Theorem: elf32_sym-of-elf_bits32-fix-value

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

Theorem: elf32_sym-elf_bits32-equiv-congruence-on-value

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

Theorem: elf32_sym-of-elf_bits32-fix-size

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

Theorem: elf32_sym-elf_bits32-equiv-congruence-on-size

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

Theorem: elf32_sym-of-elf_bits8-fix-info

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

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

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

Theorem: elf32_sym-of-elf_bits8-fix-other

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

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

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

Theorem: elf32_sym-of-elf_bits16-fix-shndx

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

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

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

Function: elf32_sym-equiv-under-mask

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

Function: elf32_sym->name

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

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

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

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

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

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

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

Theorem: elf32_sym->name-of-elf32_sym

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

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

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

Function: elf32_sym->value

(defun elf32_sym->value (x)
       (declare (xargs :guard (elf32_sym-p x)))
       (mbe :logic (let ((x (elf32_sym-fix x)))
                        (part-select x :low 32 :width 32))
            :exec (the (unsigned-byte 32)
                       (logand (the (unsigned-byte 32) 4294967295)
                               (the (unsigned-byte 96)
                                    (ash (the (unsigned-byte 128) x)
                                         -32))))))

Theorem: elf_bits32-p-of-elf32_sym->value

(defthm elf_bits32-p-of-elf32_sym->value
        (b* ((value (elf32_sym->value x)))
            (elf_bits32-p value))
        :rule-classes :rewrite)

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

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

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

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

Theorem: elf32_sym->value-of-elf32_sym

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

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

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

Function: elf32_sym->size

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

Theorem: elf_bits32-p-of-elf32_sym->size

(defthm elf_bits32-p-of-elf32_sym->size
        (b* ((size (elf32_sym->size x)))
            (elf_bits32-p size))
        :rule-classes :rewrite)

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

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

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

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

Theorem: elf32_sym->size-of-elf32_sym

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

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

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

Function: elf32_sym->info

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

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

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

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

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

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

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

Theorem: elf32_sym->info-of-elf32_sym

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

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

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

Function: elf32_sym->other

(defun elf32_sym->other (x)
       (declare (xargs :guard (elf32_sym-p x)))
       (mbe :logic (let ((x (elf32_sym-fix x)))
                        (part-select x :low 104 :width 8))
            :exec (the (unsigned-byte 8)
                       (logand (the (unsigned-byte 8) 255)
                               (the (unsigned-byte 24)
                                    (ash (the (unsigned-byte 128) x)
                                         -104))))))

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

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

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

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

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

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

Theorem: elf32_sym->other-of-elf32_sym

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

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

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

Function: elf32_sym->shndx

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

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

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

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

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

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

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

Theorem: elf32_sym->shndx-of-elf32_sym

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

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

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

Theorem: elf32_sym-fix-in-terms-of-elf32_sym

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

Function: !elf32_sym->name

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

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

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

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

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

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

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

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

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

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

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

Theorem: !elf32_sym->name-is-elf32_sym

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

Theorem: elf32_sym->name-of-!elf32_sym->name

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

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

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

Function: !elf32_sym->value

(defun
  !elf32_sym->value (value x)
  (declare (xargs :guard (and (elf_bits32-p value)
                              (elf32_sym-p x))))
  (mbe :logic (b* ((value (mbe :logic (elf_bits32-fix value)
                               :exec value))
                   (x (elf32_sym-fix x)))
                  (part-install value x
                                :width 32
                                :low 32))
       :exec (the (unsigned-byte 128)
                  (logior (the (unsigned-byte 128)
                               (logand (the (unsigned-byte 128) x)
                                       (the (signed-byte 65)
                                            -18446744069414584321)))
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 32) value)
                                    32))))))

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

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

Theorem: !elf32_sym->value-of-elf_bits32-fix-value

(defthm !elf32_sym->value-of-elf_bits32-fix-value
        (equal (!elf32_sym->value (elf_bits32-fix value)
                                  x)
               (!elf32_sym->value value x)))

Theorem: !elf32_sym->value-elf_bits32-equiv-congruence-on-value

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

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

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

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

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

Theorem: !elf32_sym->value-is-elf32_sym

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

Theorem: elf32_sym->value-of-!elf32_sym->value

(defthm elf32_sym->value-of-!elf32_sym->value
        (b* ((?new-x (!elf32_sym->value value x)))
            (equal (elf32_sym->value new-x)
                   (elf_bits32-fix value))))

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

(defthm
    !elf32_sym->value-equiv-under-mask
    (b* ((?new-x (!elf32_sym->value value x)))
        (elf32_sym-equiv-under-mask new-x x -18446744069414584321)))

Function: !elf32_sym->size

(defun
 !elf32_sym->size (size x)
 (declare (xargs :guard (and (elf_bits32-p size)
                             (elf32_sym-p x))))
 (mbe
    :logic (b* ((size (mbe :logic (elf_bits32-fix size)
                           :exec size))
                (x (elf32_sym-fix x)))
               (part-install size x :width 32 :low 64))
    :exec
    (the (unsigned-byte 128)
         (logior (the (unsigned-byte 128)
                      (logand (the (unsigned-byte 128) x)
                              (the (signed-byte 97)
                                   -79228162495817593519834398721)))
                 (the (unsigned-byte 96)
                      (ash (the (unsigned-byte 32) size)
                           64))))))

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

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

Theorem: !elf32_sym->size-of-elf_bits32-fix-size

(defthm !elf32_sym->size-of-elf_bits32-fix-size
        (equal (!elf32_sym->size (elf_bits32-fix size)
                                 x)
               (!elf32_sym->size size x)))

Theorem: !elf32_sym->size-elf_bits32-equiv-congruence-on-size

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

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

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

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

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

Theorem: !elf32_sym->size-is-elf32_sym

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

Theorem: elf32_sym->size-of-!elf32_sym->size

(defthm elf32_sym->size-of-!elf32_sym->size
        (b* ((?new-x (!elf32_sym->size size x)))
            (equal (elf32_sym->size new-x)
                   (elf_bits32-fix size))))

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

(defthm
 !elf32_sym->size-equiv-under-mask
 (b* ((?new-x (!elf32_sym->size size x)))
     (elf32_sym-equiv-under-mask new-x
                                 x -79228162495817593519834398721)))

Function: !elf32_sym->info

(defun
 !elf32_sym->info (info x)
 (declare (xargs :guard (and (elf_bits8-p info)
                             (elf32_sym-p x))))
 (mbe
  :logic (b* ((info (mbe :logic (elf_bits8-fix info)
                         :exec info))
              (x (elf32_sym-fix x)))
             (part-install info x :width 8 :low 96))
  :exec
  (the
      (unsigned-byte 128)
      (logior (the (unsigned-byte 128)
                   (logand (the (unsigned-byte 128) x)
                           (the (signed-byte 105)
                                -20203181441137406086353707335681)))
              (the (unsigned-byte 104)
                   (ash (the (unsigned-byte 8) info)
                        96))))))

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

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

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

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

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

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

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

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

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

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

Theorem: !elf32_sym->info-is-elf32_sym

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

Theorem: elf32_sym->info-of-!elf32_sym->info

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

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

(defthm
 !elf32_sym->info-equiv-under-mask
 (b*
  ((?new-x (!elf32_sym->info info x)))
  (elf32_sym-equiv-under-mask new-x
                              x -20203181441137406086353707335681)))

Function: !elf32_sym->other

(defun
 !elf32_sym->other (other x)
 (declare (xargs :guard (and (elf_bits8-p other)
                             (elf32_sym-p x))))
 (mbe
  :logic (b* ((other (mbe :logic (elf_bits8-fix other)
                          :exec other))
              (x (elf32_sym-fix x)))
             (part-install other x
                           :width 8
                           :low 104))
  :exec
  (the
    (unsigned-byte 128)
    (logior (the (unsigned-byte 128)
                 (logand (the (unsigned-byte 128) x)
                         (the (signed-byte 113)
                              -5172014448931175958106549077934081)))
            (the (unsigned-byte 112)
                 (ash (the (unsigned-byte 8) other)
                      104))))))

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

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

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

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

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

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

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

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

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

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

Theorem: !elf32_sym->other-is-elf32_sym

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

Theorem: elf32_sym->other-of-!elf32_sym->other

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

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

(defthm !elf32_sym->other-equiv-under-mask
        (b* ((?new-x (!elf32_sym->other other x)))
            (elf32_sym-equiv-under-mask
                 new-x
                 x -5172014448931175958106549077934081)))

Function: !elf32_sym->shndx

(defun
 !elf32_sym->shndx (shndx x)
 (declare (xargs :guard (and (elf_bits16-p shndx)
                             (elf32_sym-p x))))
 (mbe
  :logic (b* ((shndx (mbe :logic (elf_bits16-fix shndx)
                          :exec shndx))
              (x (elf32_sym-fix x)))
             (part-install shndx x
                           :width 16
                           :low 112))
  :exec
  (the
   (unsigned-byte 128)
   (logior
       (the (unsigned-byte 128)
            (logand (the (unsigned-byte 128) x)
                    (the (signed-byte 129)
                         -340277174624079928635746076935438991361)))
       (the (unsigned-byte 128)
            (ash (the (unsigned-byte 16) shndx)
                 112))))))

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

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

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

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

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

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

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

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

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

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

Theorem: !elf32_sym->shndx-is-elf32_sym

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

Theorem: elf32_sym->shndx-of-!elf32_sym->shndx

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

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

(defthm !elf32_sym->shndx-equiv-under-mask
        (b* ((?new-x (!elf32_sym->shndx shndx x)))
            (elf32_sym-equiv-under-mask
                 new-x
                 x 5192296858534827628530496329220095)))

Function: elf32_sym-debug

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

Subtopics

!elf32_sym->value

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

!elf32_sym->shndx

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

!elf32_sym->other

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

!elf32_sym->size

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

!elf32_sym->name

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

!elf32_sym->info

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

Elf32_sym-p

Recognizer for elf32_sym bit structures.

Elf32_sym->value

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

Elf32_sym->size

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

Elf32_sym->shndx

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

Elf32_sym->other

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

Elf32_sym-fix

Fixing function for elf32_sym bit structures.

Elf32_sym->name

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

Elf32_sym->info

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