		Search-engine friendly clone of the ACL2 documentation.

Elf64_sym

!elf64_sym->value

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

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

Definitions and Theorems

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