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