Constructor for the Code Segment attribute field
(make-code-segment-attr-field descriptor) → *
Function:
(defun make-code-segment-attr-field (descriptor) (declare (type (unsigned-byte 64) descriptor)) (let ((__function__ 'make-code-segment-attr-field)) (declare (ignorable __function__)) (b* ((a (code-segment-descriptorbits->a descriptor)) (r (code-segment-descriptorbits->r descriptor)) (c (code-segment-descriptorbits->c descriptor)) (msb-of-type (code-segment-descriptorbits->msb-of-type descriptor)) (s (code-segment-descriptorbits->s descriptor)) (dpl (code-segment-descriptorbits->dpl descriptor)) (p (code-segment-descriptorbits->p descriptor)) (avl (code-segment-descriptorbits->avl descriptor)) (l (code-segment-descriptorbits->l descriptor)) (d (code-segment-descriptorbits->d descriptor)) (g (code-segment-descriptorbits->g descriptor))) (change-code-segment-descriptor-attributesbits 0 :a a :r r :c c :msb-of-type msb-of-type :s s :dpl dpl :p p :avl avl :l l :d d :g g))))
Theorem:
(defthm n16p-make-code-segment-attr (implies (unsigned-byte-p 64 descriptor) (unsigned-byte-p 16 (make-code-segment-attr-field descriptor))) :rule-classes (:rewrite (:type-prescription :corollary (implies (unsigned-byte-p 64 descriptor) (natp (make-code-segment-attr-field descriptor))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (implies (unsigned-byte-p 64 descriptor) (and (<= 0 (make-code-segment-attr-field descriptor)) (< (make-code-segment-attr-field descriptor) 65536))) :hints (("Goal" :in-theory (e/d* nil (make-code-segment-attr-field)))))))