Good-tlb-key-p
Recongnizer for a valid TLB key.
- Signature
(good-tlb-key-p key) → *
The defbitstruct book generates a tlb-key-p
recongnizer, but that allows a tlb-key to have r-w-x to be set to
3, since it is a 2 bit field, but we only want to allow it to be 0-2 because
we only have three kinds of accesses, read/write/execute. good-tlb-key-p
recongizes a tlb-key-p which has the r-w-x field less than or equal to
2. All keys in the TLB are good-tlb-key-p.
Definitions and Theorems
Function: good-tlb-key-p
(defun good-tlb-key-p (key)
(declare (xargs :guard t))
(let ((__function__ 'good-tlb-key-p))
(declare (ignorable __function__))
(and (tlb-key-p key)
(<= (tlb-key->r-w-x key) 2))))
