Implements svex-argmasks for
(svmask-for-==?? mask args) → argmasks
We are considering
We of course care about any bits
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 a b) args) (mask (4vmask-fix mask))) (b* (((s4vec aval) (svex-s4xeval a)) ((s4vec bval) (svex-s4xeval b)) (a-is-not-z (sparseint-bitorc2 aval.upper aval.lower)) (b-is-not-z (sparseint-bitorc2 bval.upper bval.lower)) (both-are-z (sparseint-bitnor a-is-not-z b-is-not-z)) ((when (sparseint-equal both-are-z 0)) (list b-is-not-z a-is-not-z)) (not-b-x (sparseint-test-bitandc2 bval.upper bval.lower)) ((when (not not-b-x)) (list b-is-not-z (sparseint-bitnand a-is-not-z both-are-z)))) (list (sparseint-bitnand b-is-not-z both-are-z) a-is-not-z)))))
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))))))