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

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

Update the |EXLD|::|SIZE| 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-p

Recognizer for elf32_sym bit structures.

!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->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->info

Access the |EXLD|::|INFO| 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.