(xlate-equiv-entries e-1 e-2) → *
Two paging structure entries are
Function:
(defun xlate-equiv-entries (e-1 e-2) (declare (type (unsigned-byte 64) e-1) (type (unsigned-byte 64) e-2)) (let ((__function__ 'xlate-equiv-entries)) (declare (ignorable __function__)) (and (equal (ia32e-page-tablesbits->p e-1) (ia32e-page-tablesbits->p e-2)) (equal (ia32e-page-tablesbits->r/w e-1) (ia32e-page-tablesbits->r/w e-2)) (equal (ia32e-page-tablesbits->u/s e-1) (ia32e-page-tablesbits->u/s e-2)) (equal (ia32e-page-tablesbits->pwt e-1) (ia32e-page-tablesbits->pwt e-2)) (equal (ia32e-page-tablesbits->pcd e-1) (ia32e-page-tablesbits->pcd e-2)) (equal (ia32e-page-tablesbits->ps e-1) (ia32e-page-tablesbits->ps e-2)) (equal (ia32e-page-tablesbits->res1 e-1) (ia32e-page-tablesbits->res1 e-2)) (equal (ia32e-page-tablesbits->reference-addr e-1) (ia32e-page-tablesbits->reference-addr e-2)) (equal (ia32e-page-tablesbits->res2 e-1) (ia32e-page-tablesbits->res2 e-2)) (equal (ia32e-page-tablesbits->xd e-1) (ia32e-page-tablesbits->xd e-2)))))
Theorem:
(defthm xlate-equiv-entries-is-an-equivalence (and (booleanp (xlate-equiv-entries x y)) (xlate-equiv-entries x x) (implies (xlate-equiv-entries x y) (xlate-equiv-entries y x)) (implies (and (xlate-equiv-entries x y) (xlate-equiv-entries y z)) (xlate-equiv-entries x z))) :rule-classes (:equivalence))
Theorem:
(defthm xlate-equiv-entries-self-set-accessed-bit (and (xlate-equiv-entries e (set-accessed-bit (double-rewrite e))) (xlate-equiv-entries (set-accessed-bit e) (double-rewrite e))))
Theorem:
(defthm xlate-equiv-entries-self-set-dirty-bit (and (xlate-equiv-entries e (set-dirty-bit (double-rewrite e))) (xlate-equiv-entries (set-dirty-bit e) (double-rewrite e))))
Function:
(defun find-xlate-equiv-entries (e-1-equiv e-2-equiv) (cond ((equal e-1-equiv e-2-equiv) (cons (cons 'e-1 e-1-equiv) (cons (cons 'e-2 e-2-equiv) 'nil))) ((equal (first e-1-equiv) 'rm-low-64) (cond ((equal (first e-2-equiv) 'rm-low-64) (cons (cons 'e-1 e-1-equiv) (cons (cons 'e-2 e-2-equiv) 'nil))) ((equal (first e-2-equiv) 'set-accessed-bit) (b* ((e-2 (if (equal (car (second e-2-equiv)) 'set-dirty-bit) (second (second e-2-equiv)) (second e-2-equiv)))) (cons (cons 'e-1 e-1-equiv) (cons (cons 'e-2 e-2) 'nil)))) ((equal (first e-2-equiv) 'set-dirty-bit) (b* ((e-2 (if (equal (car (second e-2-equiv)) 'set-accessed-bit) (second (second e-2-equiv)) (second (second e-2-equiv))))) (cons (cons 'e-1 e-1-equiv) (cons (cons 'e-2 e-2) 'nil)))) (t (cons (cons 'e-1 e-1-equiv) (cons (cons 'e-2 e-2-equiv) 'nil))))) ((equal (first e-2-equiv) 'rm-low-64) (cond ((equal (first e-1-equiv) 'rm-low-64) (cons (cons 'e-2 e-2-equiv) (cons (cons 'e-1 e-1-equiv) 'nil))) ((equal (first e-1-equiv) 'set-accessed-bit) (b* ((e-1 (if (equal (car (second e-1-equiv)) 'set-dirty-bit) (second (second e-1-equiv)) (second e-1-equiv)))) (cons (cons 'e-2 e-2-equiv) (cons (cons 'e-1 e-1) 'nil)))) ((equal (first e-1-equiv) 'set-dirty-bit) (b* ((e-1 (if (equal (car (second e-1-equiv)) 'set-accessed-bit) (second (second e-1-equiv)) (second e-1-equiv)))) (cons (cons 'e-2 e-2-equiv) (cons (cons 'e-1 e-1) 'nil)))) (t (cons (cons 'e-2 e-2-equiv) (cons (cons 'e-1 e-1-equiv) 'nil)))))))
Theorem:
(defthm xlate-equiv-entries-and-set-accessed-and/or-dirty-bit (implies (and (bind-free (find-xlate-equiv-entries e-1-equiv e-2-equiv) (e-1 e-2)) (xlate-equiv-entries e-1 e-2) (or (equal e-1-equiv e-1) (equal e-1-equiv (set-accessed-bit e-1)) (equal e-1-equiv (set-dirty-bit e-1)) (equal e-1-equiv (set-dirty-bit (set-accessed-bit e-1)))) (or (equal e-2-equiv e-2) (equal e-2-equiv (set-accessed-bit e-2)) (equal e-2-equiv (set-dirty-bit e-2)) (equal e-2-equiv (set-dirty-bit (set-accessed-bit e-2))))) (xlate-equiv-entries e-1-equiv e-2-equiv)))
Theorem:
(defthm xlate-equiv-entries-and-page-present-cong (implies (xlate-equiv-entries e-1 e-2) (equal (page-present e-1) (page-present e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-page-read-write-cong (implies (xlate-equiv-entries e-1 e-2) (equal (page-read-write e-1) (page-read-write e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-page-user-supervisor-cong (implies (xlate-equiv-entries e-1 e-2) (equal (page-user-supervisor e-1) (page-user-supervisor e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-reference-addr (implies (xlate-equiv-entries e-1 e-2) (equal (ia32e-page-tablesbits->reference-addr e-1) (ia32e-page-tablesbits->reference-addr e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-page-size (implies (xlate-equiv-entries e-1 e-2) (equal (page-size e-1) (page-size e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-page-execute-disable (implies (xlate-equiv-entries e-1 e-2) (equal (page-execute-disable e-1) (page-execute-disable e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-with-loghead-64-1 (equal (xlate-equiv-entries (loghead 64 e-1) e-2) (xlate-equiv-entries e-1 e-2)))
Theorem:
(defthm xlate-equiv-entries-with-loghead-64-2 (equal (xlate-equiv-entries e-1 (loghead 64 e-2)) (xlate-equiv-entries e-1 e-2)))
Theorem:
(defthm xlate-equiv-entries-with-loghead-64-cong (implies (xlate-equiv-entries e-1 e-2) (xlate-equiv-entries (loghead 64 e-1) (loghead 64 e-2))) :rule-classes :congruence)
Theorem:
(defthm xlate-equiv-entries-and-loghead (implies (and (xlate-equiv-entries e-1 e-2) (syntaxp (quotep n)) (natp n) (<= n 5)) (equal (loghead n e-1) (loghead n e-2))))
Theorem:
(defthm xlate-equiv-entries-and-logtail (implies (and (xlate-equiv-entries e-1 e-2) (syntaxp (quotep n)) (natp n) (<= 7 n) (<= n 64)) (equal (logtail n (loghead 64 e-1)) (logtail n (loghead 64 e-2)))))