An 32-bit unsigned bitstruct type.
This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 32-bit integer.
Function:
(defun cutinfo-p (x) (declare (xargs :guard t)) (let ((__function__ 'cutinfo-p)) (declare (ignorable __function__)) (and (mbe :logic (unsigned-byte-p 32 x) :exec (and (natp x) (< x 4294967296))) (cutsize-p (part-select x :low 16 :width 3)))))
Theorem:
(defthm unsigned-byte-p-when-cutinfo-p (implies (cutinfo-p x) (unsigned-byte-p 32 x)))
Theorem:
(defthm cutinfo-p-compound-recognizer (implies (cutinfo-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun cutinfo-fix (x) (declare (xargs :guard (cutinfo-p x))) (let ((__function__ 'cutinfo-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 32 (logapp 16 (part-select x :width 16 :low 0) (logapp 3 (cutsize-fix (part-select x :width 3 :low 16)) (logapp 1 (part-select x :width 1 :low 19) (part-select x :width 12 :low 20))))) :exec x)))
Theorem:
(defthm cutinfo-p-of-cutinfo-fix (b* ((fty::fixed (cutinfo-fix x))) (cutinfo-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo-fix-when-cutinfo-p (implies (cutinfo-p x) (equal (cutinfo-fix x) x)))
Function:
(defun cutinfo-equiv$inline (x acl2::y) (declare (xargs :guard (and (cutinfo-p x) (cutinfo-p acl2::y)))) (equal (cutinfo-fix x) (cutinfo-fix acl2::y)))
Theorem:
(defthm cutinfo-equiv-is-an-equivalence (and (booleanp (cutinfo-equiv x y)) (cutinfo-equiv x x) (implies (cutinfo-equiv x y) (cutinfo-equiv y x)) (implies (and (cutinfo-equiv x y) (cutinfo-equiv y z)) (cutinfo-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm cutinfo-equiv-implies-equal-cutinfo-fix-1 (implies (cutinfo-equiv x x-equiv) (equal (cutinfo-fix x) (cutinfo-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm cutinfo-fix-under-cutinfo-equiv (cutinfo-equiv (cutinfo-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm cutinfo-fix-of-cutinfo-fix-x (equal (cutinfo-fix (cutinfo-fix x)) (cutinfo-fix x)))
Theorem:
(defthm cutinfo-fix-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo-fix x) (cutinfo-fix x-equiv))) :rule-classes :congruence)
Function:
(defun cutinfo (truth size valid score) (declare (xargs :guard (and (truth::truth4-p truth) (cutsize-p size) (booleanp valid) (cutscore-p score)))) (let ((__function__ 'cutinfo)) (declare (ignorable __function__)) (b* ((truth (mbe :logic (truth::truth4-fix$ truth) :exec truth)) (size (mbe :logic (cutsize-fix size) :exec size)) (valid (bool->bit valid)) (score (mbe :logic (cutscore-fix score) :exec score))) (logapp 16 truth (logapp 3 size (logapp 1 valid score))))))
Theorem:
(defthm cutinfo-p-of-cutinfo (b* ((cutinfo (cutinfo truth size valid score))) (cutinfo-p cutinfo)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo-of-truth4-fix$-truth (equal (cutinfo (truth::truth4-fix$ truth) size valid score) (cutinfo truth size valid score)))
Theorem:
(defthm cutinfo-truth4-equiv-congruence-on-truth (implies (truth::truth4-equiv truth truth-equiv) (equal (cutinfo truth size valid score) (cutinfo truth-equiv size valid score))) :rule-classes :congruence)
Theorem:
(defthm cutinfo-of-cutsize-fix-size (equal (cutinfo truth (cutsize-fix size) valid score) (cutinfo truth size valid score)))
Theorem:
(defthm cutinfo-cutsize-equiv-congruence-on-size (implies (cutsize-equiv size size-equiv) (equal (cutinfo truth size valid score) (cutinfo truth size-equiv valid score))) :rule-classes :congruence)
Theorem:
(defthm cutinfo-of-bool-fix-valid (equal (cutinfo truth size (acl2::bool-fix valid) score) (cutinfo truth size valid score)))
Theorem:
(defthm cutinfo-iff-congruence-on-valid (implies (iff valid valid-equiv) (equal (cutinfo truth size valid score) (cutinfo truth size valid-equiv score))) :rule-classes :congruence)
Theorem:
(defthm cutinfo-of-cutscore-fix-score (equal (cutinfo truth size valid (cutscore-fix score)) (cutinfo truth size valid score)))
Theorem:
(defthm cutinfo-cutscore-equiv-congruence-on-score (implies (cutscore-equiv score score-equiv) (equal (cutinfo truth size valid score) (cutinfo truth size valid score-equiv))) :rule-classes :congruence)
Function:
(defun cutinfo-equiv-under-mask (x x1 mask) (declare (xargs :guard (and (cutinfo-p x) (cutinfo-p x1) (integerp mask)))) (let ((__function__ 'cutinfo-equiv-under-mask)) (declare (ignorable __function__)) (fty::int-equiv-under-mask (cutinfo-fix x) (cutinfo-fix x1) mask)))
Theorem:
(defthm cutinfo-equiv-under-mask-of-cutinfo-fix-x (equal (cutinfo-equiv-under-mask (cutinfo-fix x) x1 mask) (cutinfo-equiv-under-mask x x1 mask)))
Theorem:
(defthm cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo-equiv-under-mask x x1 mask) (cutinfo-equiv-under-mask x-equiv x1 mask))) :rule-classes :congruence)
Theorem:
(defthm cutinfo-equiv-under-mask-of-cutinfo-fix-x1 (equal (cutinfo-equiv-under-mask x (cutinfo-fix x1) mask) (cutinfo-equiv-under-mask x x1 mask)))
Theorem:
(defthm cutinfo-equiv-under-mask-cutinfo-equiv-congruence-on-x1 (implies (cutinfo-equiv x1 x1-equiv) (equal (cutinfo-equiv-under-mask x x1 mask) (cutinfo-equiv-under-mask x x1-equiv mask))) :rule-classes :congruence)
Theorem:
(defthm cutinfo-equiv-under-mask-of-ifix-mask (equal (cutinfo-equiv-under-mask x x1 (ifix mask)) (cutinfo-equiv-under-mask x x1 mask)))
Theorem:
(defthm cutinfo-equiv-under-mask-int-equiv-congruence-on-mask (implies (int-equiv mask mask-equiv) (equal (cutinfo-equiv-under-mask x x1 mask) (cutinfo-equiv-under-mask x x1 mask-equiv))) :rule-classes :congruence)
Function:
(defun cutinfo->truth (x) (declare (xargs :guard (cutinfo-p x))) (mbe :logic (let ((x (cutinfo-fix x))) (part-select x :low 0 :width 16)) :exec (the (unsigned-byte 16) (logand (the (unsigned-byte 16) 65535) (the (unsigned-byte 32) x)))))
Theorem:
(defthm truth4-p-of-cutinfo->truth (b* ((truth (cutinfo->truth x))) (truth::truth4-p truth)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo->truth-of-cutinfo-fix-x (equal (cutinfo->truth (cutinfo-fix x)) (cutinfo->truth x)))
Theorem:
(defthm cutinfo->truth-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo->truth x) (cutinfo->truth x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cutinfo->truth-of-cutinfo (equal (cutinfo->truth (cutinfo truth size valid score)) (truth::truth4-fix$ truth)))
Theorem:
(defthm cutinfo->truth-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cutinfo-equiv-under-mask) (cutinfo-equiv-under-mask x acl2::y fty::mask) (equal (logand (lognot fty::mask) 65535) 0)) (equal (cutinfo->truth x) (cutinfo->truth acl2::y))))
Function:
(defun cutinfo->size (x) (declare (xargs :guard (cutinfo-p x))) (mbe :logic (let ((x (cutinfo-fix x))) (part-select x :low 16 :width 3)) :exec (the (unsigned-byte 3) (logand (the (unsigned-byte 3) 7) (the (unsigned-byte 16) (ash (the (unsigned-byte 32) x) -16))))))
Theorem:
(defthm cutsize-p-of-cutinfo->size (b* ((size (cutinfo->size x))) (cutsize-p size)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo->size-of-cutinfo-fix-x (equal (cutinfo->size (cutinfo-fix x)) (cutinfo->size x)))
Theorem:
(defthm cutinfo->size-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo->size x) (cutinfo->size x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cutinfo->size-of-cutinfo (equal (cutinfo->size (cutinfo truth size valid score)) (cutsize-fix size)))
Theorem:
(defthm cutinfo->size-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cutinfo-equiv-under-mask) (cutinfo-equiv-under-mask x acl2::y fty::mask) (equal (logand (lognot fty::mask) 458752) 0)) (equal (cutinfo->size x) (cutinfo->size acl2::y))))
Function:
(defun cutinfo->valid (x) (declare (xargs :guard (cutinfo-p x))) (mbe :logic (let ((x (cutinfo-fix x))) (bit->bool (part-select x :low 19 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 13) (ash (the (unsigned-byte 32) x) -19)))))))
Theorem:
(defthm booleanp-of-cutinfo->valid (b* ((valid (cutinfo->valid x))) (booleanp valid)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo->valid-of-cutinfo-fix-x (equal (cutinfo->valid (cutinfo-fix x)) (cutinfo->valid x)))
Theorem:
(defthm cutinfo->valid-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo->valid x) (cutinfo->valid x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cutinfo->valid-of-cutinfo (equal (cutinfo->valid (cutinfo truth size valid score)) (acl2::bool-fix valid)))
Theorem:
(defthm cutinfo->valid-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cutinfo-equiv-under-mask) (cutinfo-equiv-under-mask x acl2::y fty::mask) (equal (logand (lognot fty::mask) 524288) 0)) (equal (cutinfo->valid x) (cutinfo->valid acl2::y))))
Function:
(defun cutinfo->score (x) (declare (xargs :guard (cutinfo-p x))) (mbe :logic (let ((x (cutinfo-fix x))) (part-select x :low 20 :width 12)) :exec (the (unsigned-byte 12) (logand (the (unsigned-byte 12) 4095) (the (unsigned-byte 12) (ash (the (unsigned-byte 32) x) -20))))))
Theorem:
(defthm cutscore-p-of-cutinfo->score (b* ((score (cutinfo->score x))) (cutscore-p score)) :rule-classes :rewrite)
Theorem:
(defthm cutinfo->score-of-cutinfo-fix-x (equal (cutinfo->score (cutinfo-fix x)) (cutinfo->score x)))
Theorem:
(defthm cutinfo->score-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo->score x) (cutinfo->score x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cutinfo->score-of-cutinfo (equal (cutinfo->score (cutinfo truth size valid score)) (cutscore-fix score)))
Theorem:
(defthm cutinfo->score-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x cutinfo-equiv-under-mask) (cutinfo-equiv-under-mask x acl2::y fty::mask) (equal (logand (lognot fty::mask) 4293918720) 0)) (equal (cutinfo->score x) (cutinfo->score acl2::y))))
Theorem:
(defthm cutinfo-fix-in-terms-of-cutinfo (equal (cutinfo-fix x) (change-cutinfo x)))
Function:
(defun !cutinfo->truth (truth x) (declare (xargs :guard (and (truth::truth4-p truth) (cutinfo-p x)))) (mbe :logic (b* ((truth (mbe :logic (truth::truth4-fix$ truth) :exec truth)) (x (cutinfo-fix x))) (part-install truth x :width 16 :low 0)) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 32) (logand (the (unsigned-byte 32) x) (the (signed-byte 17) -65536))) (the (unsigned-byte 16) truth)))))
Theorem:
(defthm cutinfo-p-of-!cutinfo->truth (b* ((new-x (!cutinfo->truth truth x))) (cutinfo-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cutinfo->truth-of-truth4-fix$-truth (equal (!cutinfo->truth (truth::truth4-fix$ truth) x) (!cutinfo->truth truth x)))
Theorem:
(defthm !cutinfo->truth-truth4-equiv-congruence-on-truth (implies (truth::truth4-equiv truth truth-equiv) (equal (!cutinfo->truth truth x) (!cutinfo->truth truth-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->truth-of-cutinfo-fix-x (equal (!cutinfo->truth truth (cutinfo-fix x)) (!cutinfo->truth truth x)))
Theorem:
(defthm !cutinfo->truth-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (!cutinfo->truth truth x) (!cutinfo->truth truth x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->truth-is-cutinfo (equal (!cutinfo->truth truth x) (change-cutinfo x :truth truth)))
Theorem:
(defthm cutinfo->truth-of-!cutinfo->truth (b* ((?new-x (!cutinfo->truth truth x))) (equal (cutinfo->truth new-x) (truth::truth4-fix$ truth))))
Theorem:
(defthm !cutinfo->truth-equiv-under-mask (b* ((?new-x (!cutinfo->truth truth x))) (cutinfo-equiv-under-mask new-x x -65536)))
Function:
(defun !cutinfo->size (size x) (declare (xargs :guard (and (cutsize-p size) (cutinfo-p x)))) (mbe :logic (b* ((size (mbe :logic (cutsize-fix size) :exec size)) (x (cutinfo-fix x))) (part-install size x :width 3 :low 16)) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 32) (logand (the (unsigned-byte 32) x) (the (signed-byte 20) -458753))) (the (unsigned-byte 19) (ash (the (unsigned-byte 3) size) 16))))))
Theorem:
(defthm cutinfo-p-of-!cutinfo->size (b* ((new-x (!cutinfo->size size x))) (cutinfo-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cutinfo->size-of-cutsize-fix-size (equal (!cutinfo->size (cutsize-fix size) x) (!cutinfo->size size x)))
Theorem:
(defthm !cutinfo->size-cutsize-equiv-congruence-on-size (implies (cutsize-equiv size size-equiv) (equal (!cutinfo->size size x) (!cutinfo->size size-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->size-of-cutinfo-fix-x (equal (!cutinfo->size size (cutinfo-fix x)) (!cutinfo->size size x)))
Theorem:
(defthm !cutinfo->size-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (!cutinfo->size size x) (!cutinfo->size size x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->size-is-cutinfo (equal (!cutinfo->size size x) (change-cutinfo x :size size)))
Theorem:
(defthm cutinfo->size-of-!cutinfo->size (b* ((?new-x (!cutinfo->size size x))) (equal (cutinfo->size new-x) (cutsize-fix size))))
Theorem:
(defthm !cutinfo->size-equiv-under-mask (b* ((?new-x (!cutinfo->size size x))) (cutinfo-equiv-under-mask new-x x -458753)))
Function:
(defun !cutinfo->valid (valid x) (declare (xargs :guard (and (booleanp valid) (cutinfo-p x)))) (mbe :logic (b* ((valid (bool->bit valid)) (x (cutinfo-fix x))) (part-install valid x :width 1 :low 19)) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 32) (logand (the (unsigned-byte 32) x) (the (signed-byte 21) -524289))) (the (unsigned-byte 20) (ash (the (unsigned-byte 1) (bool->bit valid)) 19))))))
Theorem:
(defthm cutinfo-p-of-!cutinfo->valid (b* ((new-x (!cutinfo->valid valid x))) (cutinfo-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cutinfo->valid-of-bool-fix-valid (equal (!cutinfo->valid (acl2::bool-fix valid) x) (!cutinfo->valid valid x)))
Theorem:
(defthm !cutinfo->valid-iff-congruence-on-valid (implies (iff valid valid-equiv) (equal (!cutinfo->valid valid x) (!cutinfo->valid valid-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->valid-of-cutinfo-fix-x (equal (!cutinfo->valid valid (cutinfo-fix x)) (!cutinfo->valid valid x)))
Theorem:
(defthm !cutinfo->valid-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (!cutinfo->valid valid x) (!cutinfo->valid valid x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->valid-is-cutinfo (equal (!cutinfo->valid valid x) (change-cutinfo x :valid valid)))
Theorem:
(defthm cutinfo->valid-of-!cutinfo->valid (b* ((?new-x (!cutinfo->valid valid x))) (equal (cutinfo->valid new-x) (acl2::bool-fix valid))))
Theorem:
(defthm !cutinfo->valid-equiv-under-mask (b* ((?new-x (!cutinfo->valid valid x))) (cutinfo-equiv-under-mask new-x x -524289)))
Function:
(defun !cutinfo->score (score x) (declare (xargs :guard (and (cutscore-p score) (cutinfo-p x)))) (mbe :logic (b* ((score (mbe :logic (cutscore-fix score) :exec score)) (x (cutinfo-fix x))) (part-install score x :width 12 :low 20)) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 32) (logand (the (unsigned-byte 32) x) (the (signed-byte 33) -4293918721))) (the (unsigned-byte 32) (ash (the (unsigned-byte 12) score) 20))))))
Theorem:
(defthm cutinfo-p-of-!cutinfo->score (b* ((new-x (!cutinfo->score score x))) (cutinfo-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !cutinfo->score-of-cutscore-fix-score (equal (!cutinfo->score (cutscore-fix score) x) (!cutinfo->score score x)))
Theorem:
(defthm !cutinfo->score-cutscore-equiv-congruence-on-score (implies (cutscore-equiv score score-equiv) (equal (!cutinfo->score score x) (!cutinfo->score score-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->score-of-cutinfo-fix-x (equal (!cutinfo->score score (cutinfo-fix x)) (!cutinfo->score score x)))
Theorem:
(defthm !cutinfo->score-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (!cutinfo->score score x) (!cutinfo->score score x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !cutinfo->score-is-cutinfo (equal (!cutinfo->score score x) (change-cutinfo x :score score)))
Theorem:
(defthm cutinfo->score-of-!cutinfo->score (b* ((?new-x (!cutinfo->score score x))) (equal (cutinfo->score new-x) (cutscore-fix score))))
Theorem:
(defthm !cutinfo->score-equiv-under-mask (b* ((?new-x (!cutinfo->score score x))) (cutinfo-equiv-under-mask new-x x 1048575)))
Function:
(defun cutinfo-debug (x) (declare (xargs :guard (cutinfo-p x))) (let ((__function__ 'cutinfo-debug)) (declare (ignorable __function__)) (b* (((cutinfo x))) (cons (cons 'truth x.truth) (cons (cons 'size x.size) (cons (cons 'valid x.valid) (cons (cons 'score x.score) nil)))))))
Theorem:
(defthm cutinfo-debug-of-cutinfo-fix-x (equal (cutinfo-debug (cutinfo-fix x)) (cutinfo-debug x)))
Theorem:
(defthm cutinfo-debug-cutinfo-equiv-congruence-on-x (implies (cutinfo-equiv x x-equiv) (equal (cutinfo-debug x) (cutinfo-debug x-equiv))) :rule-classes :congruence)