(page-table-entry-addr lin-addr base-addr) → *
Function:
(defun page-table-entry-addr$inline (lin-addr base-addr) (declare (type (signed-byte 48) lin-addr) (type (unsigned-byte 52) base-addr)) (declare (xargs :guard (equal (loghead 12 base-addr) 0))) (if (mbt (and (unsigned-byte-p *physical-address-size* base-addr) (equal (loghead 12 base-addr) 0))) (mbe :logic (part-install (part-select lin-addr :low 12 :high 20) base-addr :low 3 :high 11) :exec (the (unsigned-byte 52) (logior (logand base-addr (lognot (ash 511 3))) (ash (the (unsigned-byte 9) (logand 511 (the (signed-byte 36) (ash lin-addr -12)))) 3)))) 0))
Theorem:
(defthm natp-page-table-entry-addr (natp (page-table-entry-addr lin-addr base-addr)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm *physical-address-size*p-page-table-entry-addr (unsigned-byte-p *physical-address-size* (page-table-entry-addr lin-addr base-addr)) :rule-classes (:rewrite (:linear :corollary (and (<= 0 (page-table-entry-addr lin-addr base-addr)) (< (page-table-entry-addr lin-addr base-addr) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d nil (page-table-entry-addr)))))))
Theorem:
(defthm page-table-entry-addr-is-a-multiple-of-8 (equal (loghead 3 (page-table-entry-addr lin-addr base-addr)) 0))
Theorem:
(defthm adding-7-to-page-table-entry-addr (unsigned-byte-p *physical-address-size* (+ 7 (page-table-entry-addr lin-addr base-addr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (+ 7 (page-table-entry-addr lin-addr base-addr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (+ 7 (page-table-entry-addr lin-addr base-addr))) (< (+ 7 (page-table-entry-addr lin-addr base-addr)) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d nil (page-table-entry-addr)))))))
Theorem:
(defthm page-table-entry-addr-equal-if-same-page (implies (same-page lin-addr lin-addr-2) (equal (page-table-entry-addr lin-addr base-addr) (page-table-entry-addr lin-addr-2 base-addr))) :rule-classes :congruence)