		Search-engine friendly clone of the ACL2 documentation.

Elf-header

Elf-header-fix

Fixing function for elf-header structures.

Signature
(elf-header-fix x) → new-x
Arguments: x — Guard (elf-header-p x).
Returns: new-x — Type (elf-header-p new-x).

Definitions and Theorems

Function: elf-header-fix$inline

(defun elf-header-fix$inline (x)
 (declare (xargs :guard (elf-header-p x)))
 (let ((__function__ 'elf-header-fix))
   (declare (ignorable __function__))
   (mbe :logic
        (b* ((magic (acl2::byte-list-fix (cdr (std::da-nth 0 x))))
             (class (nfix (cdr (std::da-nth 1 x))))
             (dataenc (nfix (cdr (std::da-nth 2 x))))
             (identver (nfix (cdr (std::da-nth 3 x))))
             (osabi (nfix (cdr (std::da-nth 4 x))))
             (abiver (nfix (cdr (std::da-nth 5 x))))
             (padding (acl2::byte-list-fix (cdr (std::da-nth 6 x))))
             (type (nfix (cdr (std::da-nth 7 x))))
             (machine (nfix (cdr (std::da-nth 8 x))))
             (version (nfix (cdr (std::da-nth 9 x))))
             (entry (nfix (cdr (std::da-nth 10 x))))
             (phoff (nfix (cdr (std::da-nth 11 x))))
             (shoff (nfix (cdr (std::da-nth 12 x))))
             (flags (nfix (cdr (std::da-nth 13 x))))
             (ehsize (nfix (cdr (std::da-nth 14 x))))
             (phentsize (nfix (cdr (std::da-nth 15 x))))
             (phnum (nfix (cdr (std::da-nth 16 x))))
             (shentsize (nfix (cdr (std::da-nth 17 x))))
             (shnum (nfix (cdr (std::da-nth 18 x))))
             (shstrndx (nfix (cdr (std::da-nth 19 x)))))
          (list (cons 'magic magic)
                (cons 'class class)
                (cons 'dataenc dataenc)
                (cons 'identver identver)
                (cons 'osabi osabi)
                (cons 'abiver abiver)
                (cons 'padding padding)
                (cons 'type type)
                (cons 'machine machine)
                (cons 'version version)
                (cons 'entry entry)
                (cons 'phoff phoff)
                (cons 'shoff shoff)
                (cons 'flags flags)
                (cons 'ehsize ehsize)
                (cons 'phentsize phentsize)
                (cons 'phnum phnum)
                (cons 'shentsize shentsize)
                (cons 'shnum shnum)
                (cons 'shstrndx shstrndx)))
        :exec x)))

Theorem: elf-header-p-of-elf-header-fix

(defthm elf-header-p-of-elf-header-fix
  (b* ((new-x (elf-header-fix$inline x)))
    (elf-header-p new-x))
  :rule-classes :rewrite)

Theorem: elf-header-fix-when-elf-header-p

(defthm elf-header-fix-when-elf-header-p
  (implies (elf-header-p x)
           (equal (elf-header-fix x) x)))

Function: elf-header-equiv$inline

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

Theorem: elf-header-equiv-is-an-equivalence

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

Theorem: elf-header-equiv-implies-equal-elf-header-fix-1

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

Theorem: elf-header-fix-under-elf-header-equiv

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

Theorem: equal-of-elf-header-fix-1-forward-to-elf-header-equiv

(defthm equal-of-elf-header-fix-1-forward-to-elf-header-equiv
  (implies (equal (elf-header-fix x) y)
           (elf-header-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-elf-header-fix-2-forward-to-elf-header-equiv

(defthm equal-of-elf-header-fix-2-forward-to-elf-header-equiv
  (implies (equal x (elf-header-fix y))
           (elf-header-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elf-header-equiv-of-elf-header-fix-1-forward

(defthm elf-header-equiv-of-elf-header-fix-1-forward
  (implies (elf-header-equiv (elf-header-fix x) y)
           (elf-header-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elf-header-equiv-of-elf-header-fix-2-forward

(defthm elf-header-equiv-of-elf-header-fix-2-forward
  (implies (elf-header-equiv x (elf-header-fix y))
           (elf-header-equiv x y))
  :rule-classes :forward-chaining)