(pml4-table-entry-addr lin-addr base-addr) → *
Function:
(defun pml4-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 39 :high 47) base-addr :low 3 :high 11) :exec (the (unsigned-byte 52) (logior (the (unsigned-byte 52) (logand base-addr (lognot (ash 511 3)))) (the (unsigned-byte 12) (ash (the (unsigned-byte 9) (logand 511 (ash lin-addr -39))) 3))))) 0))
Theorem:
(defthm natp-pml4-table-entry-addr (natp (pml4-table-entry-addr lin-addr base-addr)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm *physical-address-size*p-pml4-table-entry-addr (unsigned-byte-p *physical-address-size* (pml4-table-entry-addr lin-addr base-addr)) :rule-classes (:rewrite (:linear :corollary (and (<= 0 (pml4-table-entry-addr lin-addr base-addr)) (< (pml4-table-entry-addr lin-addr base-addr) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d nil (pml4-table-entry-addr)))))))
Theorem:
(defthm pml4-table-entry-addr-is-a-multiple-of-8 (equal (loghead 3 (pml4-table-entry-addr lin-addr base-addr)) 0))
Theorem:
(defthm adding-7-to-pml4-table-entry-addr (unsigned-byte-p *physical-address-size* (+ 7 (pml4-table-entry-addr lin-addr base-addr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (+ 7 (pml4-table-entry-addr lin-addr base-addr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (+ 7 (pml4-table-entry-addr lin-addr base-addr))) (< (+ 7 (pml4-table-entry-addr lin-addr base-addr)) (expt 2 *physical-address-size*))) :hints (("Goal" :in-theory (e/d nil (pml4-table-entry-addr)))))))