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