Implements svex-argmasks for
(svmask-for-safer-==? mask args) → argmasks
We are considering
The outer mask doesn't much matter since there's nothing bitwise about this, except that if the whole outer mask is zero then we (of course) don't care about any bits at all.
We can't do anything smart for
Function:
(defun svmask-for-safer-==? (mask args) (declare (xargs :guard (and (4vmask-p mask) (svexlist-p args)))) (let ((__function__ 'svmask-for-safer-==?)) (declare (ignorable __function__)) (b* (((svex-nths a b) args) (mask (4vmask-fix mask))) (b* (((when (sparseint-equal mask 0)) (list 0 0)) ((s4vec bval) (svex-s4xeval b)) (b-nonz (sparseint-bitorc2 bval.upper bval.lower))) (list b-nonz -1)))))
Theorem:
(defthm 4vmasklist-p-of-svmask-for-safer-==? (b* ((argmasks (svmask-for-safer-==? mask args))) (4vmasklist-p argmasks)) :rule-classes :rewrite)
Theorem:
(defthm svmask-for-safer-==?-of-4vmask-fix-mask (equal (svmask-for-safer-==? (4vmask-fix mask) args) (svmask-for-safer-==? mask args)))
Theorem:
(defthm svmask-for-safer-==?-4vmask-equiv-congruence-on-mask (implies (4vmask-equiv mask mask-equiv) (equal (svmask-for-safer-==? mask args) (svmask-for-safer-==? mask-equiv args))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-safer-==?-of-svexlist-fix-args (equal (svmask-for-safer-==? mask (svexlist-fix args)) (svmask-for-safer-==? mask args)))
Theorem:
(defthm svmask-for-safer-==?-svexlist-equiv-congruence-on-args (implies (svexlist-equiv args args-equiv) (equal (svmask-for-safer-==? mask args) (svmask-for-safer-==? mask args-equiv))) :rule-classes :congruence)
Theorem:
(defthm svmask-for-safer-==?-correct (implies (and (equal (4veclist-mask (svmask-for-safer-==? mask args) (svexlist-eval args env)) (4veclist-mask (svmask-for-safer-==? mask args) args1)) (syntaxp (not (equal args1 (cons 'svexlist-eval (cons args (cons env 'nil))))))) (equal (4vec-mask mask (svex-apply 'safer-==? args1)) (4vec-mask mask (svex-apply 'safer-==? (svexlist-eval args env))))))