Implements svex-argmasks for
(svmask-for-bit?! mask args) → argmasks
We are considering a
As a starting point, since 4vec-bit?! operates in a bit-by-bit
fashion, we certainly don't care about any bits that are don't cares in our
outer
For
For
For
Function:
(defun svmask-for-bit?! (mask args) (declare (xargs :guard (and (4vmask-p mask) (svexlist-p args)))) (let ((__function__ 'svmask-for-bit?!)) (declare (ignorable __function__)) (b* (((svex-nths tests) args) (mask (4vmask-fix mask))) (b* (((mv maybe-1 maybe-not1) (if (svex-case tests :quote) (b* (((4vec test) (svex-quote->val tests)) (known1 (logand test.upper test.lower))) (mv (int-to-sparseint known1) (int-to-sparseint (lognot known1)))) (b* (((s4vec tval) (svex-s4xeval tests))) (mv tval.upper (sparseint-bitnand tval.upper tval.lower)))))) (list mask (sparseint-bitand mask maybe-1) (sparseint-bitand mask maybe-not1))))))
Theorem:
(defthm 4vmasklist-p-of-svmask-for-bit?! (b* ((argmasks (svmask-for-bit?! mask args))) (4vmasklist-p argmasks)) :rule-classes :rewrite)
Theorem:
(defthm svmask-for-bit?!-of-4vmask-fix-mask (equal (svmask-for-bit?! (4vmask-fix mask) args) (svmask-for-bit?! mask args)))
Theorem:
(defthm svmask-for-bit?!-4vmask-equiv-congruence-on-mask (implies (4vmask-equiv mask mask-equiv) (equal (svmask-for-bit?! mask args) (svmask-for-bit?! mask-equiv args))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-bit?!-of-svexlist-fix-args (equal (svmask-for-bit?! mask (svexlist-fix args)) (svmask-for-bit?! mask args)))
Theorem:
(defthm svmask-for-bit?!-svexlist-equiv-congruence-on-args (implies (svexlist-equiv args args-equiv) (equal (svmask-for-bit?! mask args) (svmask-for-bit?! mask args-equiv))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-bit?!-correct (implies (and (equal (4veclist-mask (svmask-for-bit?! mask args) (svexlist-eval args env)) (4veclist-mask (svmask-for-bit?! mask args) args1)) (syntaxp (not (equal args1 (cons 'svexlist-eval (cons args (cons env 'nil))))))) (equal (4vec-mask mask (svex-apply 'bit?! args1)) (4vec-mask mask (svex-apply 'bit?! (svexlist-eval args env))))))