Subset of call-gate-descriptorBits.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 16-bit integer.
Function:
(defun call-gate-descriptor-attributesbits-p (x) (declare (xargs :guard t)) (let ((__function__ 'call-gate-descriptor-attributesbits-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 16 x) :exec (and (natp x) (< x 65536)))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-when-unsigned-byte-p (implies (unsigned-byte-p 16 x) (call-gate-descriptor-attributesbits-p x)))
Theorem:
(defthm unsigned-byte-p-when-call-gate-descriptor-attributesbits-p (implies (call-gate-descriptor-attributesbits-p x) (unsigned-byte-p 16 x)))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-compound-recognizer (implies (call-gate-descriptor-attributesbits-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun call-gate-descriptor-attributesbits-fix (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (let ((__function__ 'call-gate-descriptor-attributesbits-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 16 x) :exec x)))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-call-gate-descriptor-attributesbits-fix (b* ((fty::fixed (call-gate-descriptor-attributesbits-fix x))) (call-gate-descriptor-attributesbits-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits-fix-when-call-gate-descriptor-attributesbits-p (implies (call-gate-descriptor-attributesbits-p x) (equal (call-gate-descriptor-attributesbits-fix x) x)))
Function:
(defun call-gate-descriptor-attributesbits-equiv$inline (x y) (declare (xargs :guard (and (call-gate-descriptor-attributesbits-p x) (call-gate-descriptor-attributesbits-p y)))) (equal (call-gate-descriptor-attributesbits-fix x) (call-gate-descriptor-attributesbits-fix y)))
Theorem:
(defthm call-gate-descriptor-attributesbits-equiv-is-an-equivalence (and (booleanp (call-gate-descriptor-attributesbits-equiv x y)) (call-gate-descriptor-attributesbits-equiv x x) (implies (call-gate-descriptor-attributesbits-equiv x y) (call-gate-descriptor-attributesbits-equiv y x)) (implies (and (call-gate-descriptor-attributesbits-equiv x y) (call-gate-descriptor-attributesbits-equiv y z)) (call-gate-descriptor-attributesbits-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm call-gate-descriptor-attributesbits-equiv-implies-equal-call-gate-descriptor-attributesbits-fix-1 (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits-fix x) (call-gate-descriptor-attributesbits-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm call-gate-descriptor-attributesbits-fix-under-call-gate-descriptor-attributesbits-equiv (call-gate-descriptor-attributesbits-equiv (call-gate-descriptor-attributesbits-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun call-gate-descriptor-attributesbits (type s dpl p unknownbits) (declare (xargs :guard (and (4bits-p type) (bitp s) (2bits-p dpl) (bitp p) (8bits-p unknownbits)))) (let ((__function__ 'call-gate-descriptor-attributesbits)) (declare (ignorable __function__)) (b* ((type (mbe :logic (4bits-fix type) :exec type)) (s (mbe :logic (bfix s) :exec s)) (dpl (mbe :logic (2bits-fix dpl) :exec dpl)) (p (mbe :logic (bfix p) :exec p)) (unknownbits (mbe :logic (8bits-fix unknownbits) :exec unknownbits))) (logapp 4 type (logapp 1 s (logapp 2 dpl (logapp 1 p unknownbits)))))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-call-gate-descriptor-attributesbits (b* ((call-gate-descriptor-attributesbits (call-gate-descriptor-attributesbits type s dpl p unknownbits))) (call-gate-descriptor-attributesbits-p call-gate-descriptor-attributesbits)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits-of-4bits-fix-type (equal (call-gate-descriptor-attributesbits (4bits-fix type) s dpl p unknownbits) (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits-4bits-equiv-congruence-on-type (implies (4bits-equiv type type-equiv) (equal (call-gate-descriptor-attributesbits type s dpl p unknownbits) (call-gate-descriptor-attributesbits type-equiv s dpl p unknownbits))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits-of-bfix-s (equal (call-gate-descriptor-attributesbits type (bfix s) dpl p unknownbits) (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits-bit-equiv-congruence-on-s (implies (bit-equiv s s-equiv) (equal (call-gate-descriptor-attributesbits type s dpl p unknownbits) (call-gate-descriptor-attributesbits type s-equiv dpl p unknownbits))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits-of-2bits-fix-dpl (equal (call-gate-descriptor-attributesbits type s (2bits-fix dpl) p unknownbits) (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits-2bits-equiv-congruence-on-dpl (implies (2bits-equiv dpl dpl-equiv) (equal (call-gate-descriptor-attributesbits type s dpl p unknownbits) (call-gate-descriptor-attributesbits type s dpl-equiv p unknownbits))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits-of-bfix-p (equal (call-gate-descriptor-attributesbits type s dpl (bfix p) unknownbits) (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (call-gate-descriptor-attributesbits type s dpl p unknownbits) (call-gate-descriptor-attributesbits type s dpl p-equiv unknownbits))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits-of-8bits-fix-unknownbits (equal (call-gate-descriptor-attributesbits type s dpl p (8bits-fix unknownbits)) (call-gate-descriptor-attributesbits type s dpl p unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits-8bits-equiv-congruence-on-unknownbits (implies (8bits-equiv unknownbits unknownbits-equiv) (equal (call-gate-descriptor-attributesbits type s dpl p unknownbits) (call-gate-descriptor-attributesbits type s dpl p unknownbits-equiv))) :rule-classes :congruence)
Function:
(defun call-gate-descriptor-attributesbits-equiv-under-mask (x x1 mask) (declare (xargs :guard (and (call-gate-descriptor-attributesbits-p x) (call-gate-descriptor-attributesbits-p x1) (integerp mask)))) (let ((__function__ 'call-gate-descriptor-attributesbits-equiv-under-mask)) (declare (ignorable __function__)) (fty::int-equiv-under-mask (call-gate-descriptor-attributesbits-fix x) (call-gate-descriptor-attributesbits-fix x1) mask)))
Function:
(defun call-gate-descriptor-attributesbits->type$inline (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (mbe :logic (let ((x (call-gate-descriptor-attributesbits-fix x))) (part-select x :low 0 :width 4)) :exec (the (unsigned-byte 4) (logand (the (unsigned-byte 4) 15) (the (unsigned-byte 16) x)))))
Theorem:
(defthm 4bits-p-of-call-gate-descriptor-attributesbits->type (b* ((type (call-gate-descriptor-attributesbits->type$inline x))) (4bits-p type)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits->type$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (call-gate-descriptor-attributesbits->type$inline (call-gate-descriptor-attributesbits-fix x)) (call-gate-descriptor-attributesbits->type$inline x)))
Theorem:
(defthm call-gate-descriptor-attributesbits->type$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits->type$inline x) (call-gate-descriptor-attributesbits->type$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits->type-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits->type (call-gate-descriptor-attributesbits type s dpl p unknownbits)) (4bits-fix type)))
Theorem:
(defthm call-gate-descriptor-attributesbits->type-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x call-gate-descriptor-attributesbits-equiv-under-mask) (call-gate-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 15) 0)) (equal (call-gate-descriptor-attributesbits->type x) (call-gate-descriptor-attributesbits->type y))))
Function:
(defun call-gate-descriptor-attributesbits->s$inline (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (mbe :logic (let ((x (call-gate-descriptor-attributesbits-fix x))) (part-select x :low 4 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 12) (ash (the (unsigned-byte 16) x) -4))))))
Theorem:
(defthm bitp-of-call-gate-descriptor-attributesbits->s (b* ((s (call-gate-descriptor-attributesbits->s$inline x))) (bitp s)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits->s$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (call-gate-descriptor-attributesbits->s$inline (call-gate-descriptor-attributesbits-fix x)) (call-gate-descriptor-attributesbits->s$inline x)))
Theorem:
(defthm call-gate-descriptor-attributesbits->s$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits->s$inline x) (call-gate-descriptor-attributesbits->s$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits->s-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits->s (call-gate-descriptor-attributesbits type s dpl p unknownbits)) (bfix s)))
Theorem:
(defthm call-gate-descriptor-attributesbits->s-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x call-gate-descriptor-attributesbits-equiv-under-mask) (call-gate-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 16) 0)) (equal (call-gate-descriptor-attributesbits->s x) (call-gate-descriptor-attributesbits->s y))))
Function:
(defun call-gate-descriptor-attributesbits->dpl$inline (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (mbe :logic (let ((x (call-gate-descriptor-attributesbits-fix x))) (part-select x :low 5 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 11) (ash (the (unsigned-byte 16) x) -5))))))
Theorem:
(defthm 2bits-p-of-call-gate-descriptor-attributesbits->dpl (b* ((dpl (call-gate-descriptor-attributesbits->dpl$inline x))) (2bits-p dpl)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits->dpl$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (call-gate-descriptor-attributesbits->dpl$inline (call-gate-descriptor-attributesbits-fix x)) (call-gate-descriptor-attributesbits->dpl$inline x)))
Theorem:
(defthm call-gate-descriptor-attributesbits->dpl$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits->dpl$inline x) (call-gate-descriptor-attributesbits->dpl$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits->dpl-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits->dpl (call-gate-descriptor-attributesbits type s dpl p unknownbits)) (2bits-fix dpl)))
Theorem:
(defthm call-gate-descriptor-attributesbits->dpl-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x call-gate-descriptor-attributesbits-equiv-under-mask) (call-gate-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 96) 0)) (equal (call-gate-descriptor-attributesbits->dpl x) (call-gate-descriptor-attributesbits->dpl y))))
Function:
(defun call-gate-descriptor-attributesbits->p$inline (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (mbe :logic (let ((x (call-gate-descriptor-attributesbits-fix x))) (part-select x :low 7 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 9) (ash (the (unsigned-byte 16) x) -7))))))
Theorem:
(defthm bitp-of-call-gate-descriptor-attributesbits->p (b* ((p (call-gate-descriptor-attributesbits->p$inline x))) (bitp p)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits->p$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (call-gate-descriptor-attributesbits->p$inline (call-gate-descriptor-attributesbits-fix x)) (call-gate-descriptor-attributesbits->p$inline x)))
Theorem:
(defthm call-gate-descriptor-attributesbits->p$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits->p$inline x) (call-gate-descriptor-attributesbits->p$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits->p-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits->p (call-gate-descriptor-attributesbits type s dpl p unknownbits)) (bfix p)))
Theorem:
(defthm call-gate-descriptor-attributesbits->p-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x call-gate-descriptor-attributesbits-equiv-under-mask) (call-gate-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 128) 0)) (equal (call-gate-descriptor-attributesbits->p x) (call-gate-descriptor-attributesbits->p y))))
Function:
(defun call-gate-descriptor-attributesbits->unknownbits$inline (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (mbe :logic (let ((x (call-gate-descriptor-attributesbits-fix x))) (part-select x :low 8 :width 8)) :exec (the (unsigned-byte 8) (logand (the (unsigned-byte 8) 255) (the (unsigned-byte 8) (ash (the (unsigned-byte 16) x) -8))))))
Theorem:
(defthm 8bits-p-of-call-gate-descriptor-attributesbits->unknownbits (b* ((unknownbits (call-gate-descriptor-attributesbits->unknownbits$inline x))) (8bits-p unknownbits)) :rule-classes :rewrite)
Theorem:
(defthm call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (call-gate-descriptor-attributesbits->unknownbits$inline (call-gate-descriptor-attributesbits-fix x)) (call-gate-descriptor-attributesbits->unknownbits$inline x)))
Theorem:
(defthm call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (call-gate-descriptor-attributesbits->unknownbits$inline x) (call-gate-descriptor-attributesbits->unknownbits$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm call-gate-descriptor-attributesbits->unknownbits-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits->unknownbits (call-gate-descriptor-attributesbits type s dpl p unknownbits)) (8bits-fix unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits->unknownbits-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x call-gate-descriptor-attributesbits-equiv-under-mask) (call-gate-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 65280) 0)) (equal (call-gate-descriptor-attributesbits->unknownbits x) (call-gate-descriptor-attributesbits->unknownbits y))))
Theorem:
(defthm call-gate-descriptor-attributesbits-fix-in-terms-of-call-gate-descriptor-attributesbits (equal (call-gate-descriptor-attributesbits-fix x) (change-call-gate-descriptor-attributesbits x)))
Function:
(defun !call-gate-descriptor-attributesbits->type$inline (type x) (declare (xargs :guard (and (4bits-p type) (call-gate-descriptor-attributesbits-p x)))) (mbe :logic (b* ((type (mbe :logic (4bits-fix type) :exec type)) (x (call-gate-descriptor-attributesbits-fix x))) (part-install type x :width 4 :low 0)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 5) -16))) (the (unsigned-byte 4) type)))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->type (b* ((new-x (!call-gate-descriptor-attributesbits->type$inline type x))) (call-gate-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptor-attributesbits->type$inline-of-4bits-fix-type (equal (!call-gate-descriptor-attributesbits->type$inline (4bits-fix type) x) (!call-gate-descriptor-attributesbits->type$inline type x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->type$inline-4bits-equiv-congruence-on-type (implies (4bits-equiv type type-equiv) (equal (!call-gate-descriptor-attributesbits->type$inline type x) (!call-gate-descriptor-attributesbits->type$inline type-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->type$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (!call-gate-descriptor-attributesbits->type$inline type (call-gate-descriptor-attributesbits-fix x)) (!call-gate-descriptor-attributesbits->type$inline type x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->type$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (!call-gate-descriptor-attributesbits->type$inline type x) (!call-gate-descriptor-attributesbits->type$inline type x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->type-is-call-gate-descriptor-attributesbits (equal (!call-gate-descriptor-attributesbits->type type x) (change-call-gate-descriptor-attributesbits x :type type)))
Theorem:
(defthm call-gate-descriptor-attributesbits->type-of-!call-gate-descriptor-attributesbits->type (b* ((?new-x (!call-gate-descriptor-attributesbits->type$inline type x))) (equal (call-gate-descriptor-attributesbits->type new-x) (4bits-fix type))))
Theorem:
(defthm !call-gate-descriptor-attributesbits->type-equiv-under-mask (b* ((?new-x (!call-gate-descriptor-attributesbits->type$inline type x))) (call-gate-descriptor-attributesbits-equiv-under-mask new-x x -16)))
Function:
(defun !call-gate-descriptor-attributesbits->s$inline (s x) (declare (xargs :guard (and (bitp s) (call-gate-descriptor-attributesbits-p x)))) (mbe :logic (b* ((s (mbe :logic (bfix s) :exec s)) (x (call-gate-descriptor-attributesbits-fix x))) (part-install s x :width 1 :low 4)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) s) 4))))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->s (b* ((new-x (!call-gate-descriptor-attributesbits->s$inline s x))) (call-gate-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptor-attributesbits->s$inline-of-bfix-s (equal (!call-gate-descriptor-attributesbits->s$inline (bfix s) x) (!call-gate-descriptor-attributesbits->s$inline s x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->s$inline-bit-equiv-congruence-on-s (implies (bit-equiv s s-equiv) (equal (!call-gate-descriptor-attributesbits->s$inline s x) (!call-gate-descriptor-attributesbits->s$inline s-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->s$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (!call-gate-descriptor-attributesbits->s$inline s (call-gate-descriptor-attributesbits-fix x)) (!call-gate-descriptor-attributesbits->s$inline s x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->s$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (!call-gate-descriptor-attributesbits->s$inline s x) (!call-gate-descriptor-attributesbits->s$inline s x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->s-is-call-gate-descriptor-attributesbits (equal (!call-gate-descriptor-attributesbits->s s x) (change-call-gate-descriptor-attributesbits x :s s)))
Theorem:
(defthm call-gate-descriptor-attributesbits->s-of-!call-gate-descriptor-attributesbits->s (b* ((?new-x (!call-gate-descriptor-attributesbits->s$inline s x))) (equal (call-gate-descriptor-attributesbits->s new-x) (bfix s))))
Theorem:
(defthm !call-gate-descriptor-attributesbits->s-equiv-under-mask (b* ((?new-x (!call-gate-descriptor-attributesbits->s$inline s x))) (call-gate-descriptor-attributesbits-equiv-under-mask new-x x -17)))
Function:
(defun !call-gate-descriptor-attributesbits->dpl$inline (dpl x) (declare (xargs :guard (and (2bits-p dpl) (call-gate-descriptor-attributesbits-p x)))) (mbe :logic (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl)) (x (call-gate-descriptor-attributesbits-fix x))) (part-install dpl x :width 2 :low 5)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 8) -97))) (the (unsigned-byte 7) (ash (the (unsigned-byte 2) dpl) 5))))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->dpl (b* ((new-x (!call-gate-descriptor-attributesbits->dpl$inline dpl x))) (call-gate-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl (equal (!call-gate-descriptor-attributesbits->dpl$inline (2bits-fix dpl) x) (!call-gate-descriptor-attributesbits->dpl$inline dpl x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl$inline-2bits-equiv-congruence-on-dpl (implies (2bits-equiv dpl dpl-equiv) (equal (!call-gate-descriptor-attributesbits->dpl$inline dpl x) (!call-gate-descriptor-attributesbits->dpl$inline dpl-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (!call-gate-descriptor-attributesbits->dpl$inline dpl (call-gate-descriptor-attributesbits-fix x)) (!call-gate-descriptor-attributesbits->dpl$inline dpl x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (!call-gate-descriptor-attributesbits->dpl$inline dpl x) (!call-gate-descriptor-attributesbits->dpl$inline dpl x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl-is-call-gate-descriptor-attributesbits (equal (!call-gate-descriptor-attributesbits->dpl dpl x) (change-call-gate-descriptor-attributesbits x :dpl dpl)))
Theorem:
(defthm call-gate-descriptor-attributesbits->dpl-of-!call-gate-descriptor-attributesbits->dpl (b* ((?new-x (!call-gate-descriptor-attributesbits->dpl$inline dpl x))) (equal (call-gate-descriptor-attributesbits->dpl new-x) (2bits-fix dpl))))
Theorem:
(defthm !call-gate-descriptor-attributesbits->dpl-equiv-under-mask (b* ((?new-x (!call-gate-descriptor-attributesbits->dpl$inline dpl x))) (call-gate-descriptor-attributesbits-equiv-under-mask new-x x -97)))
Function:
(defun !call-gate-descriptor-attributesbits->p$inline (p x) (declare (xargs :guard (and (bitp p) (call-gate-descriptor-attributesbits-p x)))) (mbe :logic (b* ((p (mbe :logic (bfix p) :exec p)) (x (call-gate-descriptor-attributesbits-fix x))) (part-install p x :width 1 :low 7)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) p) 7))))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->p (b* ((new-x (!call-gate-descriptor-attributesbits->p$inline p x))) (call-gate-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptor-attributesbits->p$inline-of-bfix-p (equal (!call-gate-descriptor-attributesbits->p$inline (bfix p) x) (!call-gate-descriptor-attributesbits->p$inline p x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->p$inline-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (!call-gate-descriptor-attributesbits->p$inline p x) (!call-gate-descriptor-attributesbits->p$inline p-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->p$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (!call-gate-descriptor-attributesbits->p$inline p (call-gate-descriptor-attributesbits-fix x)) (!call-gate-descriptor-attributesbits->p$inline p x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->p$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (!call-gate-descriptor-attributesbits->p$inline p x) (!call-gate-descriptor-attributesbits->p$inline p x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->p-is-call-gate-descriptor-attributesbits (equal (!call-gate-descriptor-attributesbits->p p x) (change-call-gate-descriptor-attributesbits x :p p)))
Theorem:
(defthm call-gate-descriptor-attributesbits->p-of-!call-gate-descriptor-attributesbits->p (b* ((?new-x (!call-gate-descriptor-attributesbits->p$inline p x))) (equal (call-gate-descriptor-attributesbits->p new-x) (bfix p))))
Theorem:
(defthm !call-gate-descriptor-attributesbits->p-equiv-under-mask (b* ((?new-x (!call-gate-descriptor-attributesbits->p$inline p x))) (call-gate-descriptor-attributesbits-equiv-under-mask new-x x -129)))
Function:
(defun !call-gate-descriptor-attributesbits->unknownbits$inline (unknownbits x) (declare (xargs :guard (and (8bits-p unknownbits) (call-gate-descriptor-attributesbits-p x)))) (mbe :logic (b* ((unknownbits (mbe :logic (8bits-fix unknownbits) :exec unknownbits)) (x (call-gate-descriptor-attributesbits-fix x))) (part-install unknownbits x :width 8 :low 8)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 17) -65281))) (the (unsigned-byte 16) (ash (the (unsigned-byte 8) unknownbits) 8))))))
Theorem:
(defthm call-gate-descriptor-attributesbits-p-of-!call-gate-descriptor-attributesbits->unknownbits (b* ((new-x (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x))) (call-gate-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits$inline-of-8bits-fix-unknownbits (equal (!call-gate-descriptor-attributesbits->unknownbits$inline (8bits-fix unknownbits) x) (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits$inline-8bits-equiv-congruence-on-unknownbits (implies (8bits-equiv unknownbits unknownbits-equiv) (equal (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x) (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits$inline-of-call-gate-descriptor-attributesbits-fix-x (equal (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits (call-gate-descriptor-attributesbits-fix x)) (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x)))
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits$inline-call-gate-descriptor-attributesbits-equiv-congruence-on-x (implies (call-gate-descriptor-attributesbits-equiv x x-equiv) (equal (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x) (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits-is-call-gate-descriptor-attributesbits (equal (!call-gate-descriptor-attributesbits->unknownbits unknownbits x) (change-call-gate-descriptor-attributesbits x :unknownbits unknownbits)))
Theorem:
(defthm call-gate-descriptor-attributesbits->unknownbits-of-!call-gate-descriptor-attributesbits->unknownbits (b* ((?new-x (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x))) (equal (call-gate-descriptor-attributesbits->unknownbits new-x) (8bits-fix unknownbits))))
Theorem:
(defthm !call-gate-descriptor-attributesbits->unknownbits-equiv-under-mask (b* ((?new-x (!call-gate-descriptor-attributesbits->unknownbits$inline unknownbits x))) (call-gate-descriptor-attributesbits-equiv-under-mask new-x x 255)))
Function:
(defun call-gate-descriptor-attributesbits-debug (x) (declare (xargs :guard (call-gate-descriptor-attributesbits-p x))) (let ((__function__ 'call-gate-descriptor-attributesbits-debug)) (declare (ignorable __function__)) (b* (((call-gate-descriptor-attributesbits x))) (cons (cons 'type x.type) (cons (cons 's x.s) (cons (cons 'dpl x.dpl) (cons (cons 'p x.p) (cons (cons 'unknownbits x.unknownbits) nil))))))))