		Search-engine friendly clone of the ACL2 documentation.

Ia32e-paging

Same-page-offset

Signature
(same-page-offset lin-addr lin-addr-2) → *
Arguments: lin-addr — Guard (integerp lin-addr).; lin-addr-2 — Guard (integerp lin-addr-2).

Definitions and Theorems

Function: same-page-offset

(defun same-page-offset (lin-addr lin-addr-2)
  (declare (xargs :guard (and (integerp lin-addr)
                              (integerp lin-addr-2))))
  (let ((__function__ 'same-page-offset))
    (declare (ignorable __function__))
    (equal (loghead 12 lin-addr)
           (loghead 12 lin-addr-2))))

Theorem: same-page-offset-is-an-equivalence

(defthm same-page-offset-is-an-equivalence
  (and (booleanp (same-page-offset x y))
       (same-page-offset x x)
       (implies (same-page-offset x y)
                (same-page-offset y x))
       (implies (and (same-page-offset x y)
                     (same-page-offset y z))
                (same-page-offset x z)))
  :rule-classes (:equivalence))

Theorem: same-page-offset-addr-construction

(defthm same-page-offset-addr-construction
  (implies (and (natp n) (>= n 12))
           (same-page-offset (logior (loghead n x) (ash y n))
                             x)))

Theorem: logexted-is-same-page

(defthm logexted-is-same-page
  (implies (and (natp n) (>= n 12))
           (same-page-offset (logext n x) x)))

Theorem: same-page-offset-implies-same-logheads

(defthm same-page-offset-implies-same-logheads
  (implies (and (natp n)
                (<= n 12)
                (same-page-offset y (double-rewrite x))
                (syntaxp (not (equal x y))))
           (equal (loghead n x) (loghead n y))))