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