Implements svex-argmasks for
(svmask-for-?* mask args) → argmasks
We are considering a
We will almost always need to care about the entire
More obvious and probably more useful mask improvements:
Function:
(defun svmask-for-?* (mask args) (declare (xargs :guard (and (4vmask-p mask) (svexlist-p args)))) (let ((__function__ 'svmask-for-?*)) (declare (ignorable __function__)) (b* (((svex-nths test then else) args) (mask (4vmask-fix mask))) (b* (((when (4vmask-empty mask)) (list 0 0 0)) ((s4vec testval) (svex-s4xeval test)) (test-1s (sparseint-bitand testval.upper testval.lower)) ((unless (sparseint-equal test-1s 0)) (list test-1s mask 0)) ((when (and (sparseint-equal testval.upper 0) (sparseint-equal testval.lower 0))) (list -1 0 mask))) (if (or (equal then else) (branches-same-under-mask-p mask then else)) (list 0 mask mask) (list -1 mask mask))))))
Theorem:
(defthm 4vmasklist-p-of-svmask-for-?* (b* ((argmasks (svmask-for-?* mask args))) (4vmasklist-p argmasks)) :rule-classes :rewrite)
Theorem:
(defthm svmask-for-?*-of-4vmask-fix-mask (equal (svmask-for-?* (4vmask-fix mask) args) (svmask-for-?* mask args)))
Theorem:
(defthm svmask-for-?*-4vmask-equiv-congruence-on-mask (implies (4vmask-equiv mask mask-equiv) (equal (svmask-for-?* mask args) (svmask-for-?* mask-equiv args))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-?*-of-svexlist-fix-args (equal (svmask-for-?* mask (svexlist-fix args)) (svmask-for-?* mask args)))
Theorem:
(defthm svmask-for-?*-svexlist-equiv-congruence-on-args (implies (svexlist-equiv args args-equiv) (equal (svmask-for-?* mask args) (svmask-for-?* mask args-equiv))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-?*-correct (implies (and (equal (4veclist-mask (svmask-for-?* mask args) (svexlist-eval args env)) (4veclist-mask (svmask-for-?* mask args) args1)) (syntaxp (not (equal args1 (cons 'svexlist-eval (cons args (cons env 'nil))))))) (equal (4vec-mask mask (svex-apply '?* args1)) (4vec-mask mask (svex-apply '?* (svexlist-eval args env))))))