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* (((s4vec tval) (svex-s4xeval tests)) (tests-non0 (sparseint-bitor tval.upper tval.lower)) (tests-non1 (sparseint-bitnand tval.upper tval.lower))) (list mask (sparseint-bitand mask tests-non0) (sparseint-bitand mask tests-non1))))))
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))))))