		Search-engine friendly clone of the ACL2 documentation.

Elf64_sym

!elf64_sym->size

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

Signature
(!elf64_sym->size size x) → new-x
Arguments: size — Guard (elf_bits64-p size).; x — Guard (elf64_sym-p x).
Returns: new-x — Type (elf64_sym-p new-x).

Definitions and Theorems

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