(paging-entry-no-page-fault-p-did-fault? u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl) → fault?
Function:
(defun paging-entry-no-page-fault-p-did-fault? (u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl) (declare (type (unsigned-byte 1) u/s-all) (type (unsigned-byte 1) r/w-all) (type (unsigned-byte 1) x/d-all) (type (unsigned-byte 1) wp) (type (unsigned-byte 1) smep) (type (unsigned-byte 1) smap) (type (unsigned-byte 1) ac) (type (unsigned-byte 1) nxe) (type (unsigned-byte 1) implicit-supervisor-access) (type (member :r :w :x) r-w-x) (type (unsigned-byte 2) cpl)) (declare (xargs :guard (or (not (equal implicit-supervisor-access 1)) (< cpl 3)))) (let ((__function__ 'paging-entry-no-page-fault-p-did-fault?)) (declare (ignorable __function__)) (or (and (equal r-w-x :r) (if (< cpl 3) (if (equal u/s-all 0) nil (if (equal smap 0) nil (or (equal implicit-supervisor-access 1) (equal ac 0)))) (equal u/s-all 0))) (and (equal r-w-x :w) (if (< cpl 3) (if (equal u/s-all 0) (and (equal wp 1) (equal r/w-all 0)) (if (equal wp 0) (if (equal smap 0) nil (or (equal implicit-supervisor-access 1) (equal ac 0))) (if (equal smap 0) (equal r/w-all 0) (if (and (equal implicit-supervisor-access 0) (equal ac 1)) (equal r/w-all 0) t)))) (or (equal u/s-all 0) (equal r/w-all 0)))) (and (equal r-w-x :x) (if (< cpl 3) (if (equal u/s-all 0) (if (equal nxe 0) nil (equal x/d-all 1)) (if (equal smep 0) (if (equal nxe 0) nil (equal x/d-all 1)) t)) (or (equal u/s-all 0) (and (equal nxe 1) (equal x/d-all 1))))))))
Theorem:
(defthm booleanp-of-paging-entry-no-page-fault-p-did-fault? (b* ((fault? (paging-entry-no-page-fault-p-did-fault? u/s-all r/w-all x/d-all wp smep smap ac nxe implicit-supervisor-access r-w-x cpl))) (booleanp fault?)) :rule-classes :rewrite)