		Search-engine friendly clone of the ACL2 documentation.

Tlbp

Recongizer for the tlb field of the x86 state.

Signature
(tlbp tlb) → *

tlbp recongizes a list where all the entries are tlb-entryp and the final cdr is :tlb, which serves as the name when the tlbp is a ACL2::fast-alist. This is the type of the tlb field on the x86 stobj.

Definitions and Theorems

Function: tlbp

(defun tlbp (tlb)
  (declare (xargs :guard t))
  (let ((__function__ 'tlbp))
    (declare (ignorable __function__))
    (b* (((unless (consp tlb)) (equal tlb :tlb))
         ((list* el tail) tlb)
         ((unless (tlb-entryp el)) nil))
      (tlbp tail))))

Theorem: :tlb-is-tlbp

(defthm |:tlb-is-tlbp| (tlbp :tlb))

Theorem: consing-tlb-entry-onto-tlbp-is-tlbp

(defthm consing-tlb-entry-onto-tlbp-is-tlbp
  (implies (and (tlb-entryp entry) (tlbp tlb))
           (tlbp (cons entry tlb))))

Theorem: integerp-cdr-hons-assoc-equal-tlb

(defthm integerp-cdr-hons-assoc-equal-tlb
  (implies (tlbp tlb)
           (b* ((result (hons-assoc-equal key tlb)))
             (implies result (integerp (cdr result))))))

Theorem: unsigned-byte-p-40-cdr-hons-assoc-equal-tlb

(defthm unsigned-byte-p-40-cdr-hons-assoc-equal-tlb
  (implies (tlbp tlb)
           (b* ((result (hons-assoc-equal key tlb)))
             (implies result
                      (unsigned-byte-p (- 52 12)
                                       (cdr result))))))