Check if a single assignment is safe.
(check-safe-assign-single target value varset funtab) → _
Similarly to check-safe-expression, for now we require the path to be a singleton; see discussion there about non-singleton paths.
We check the expression, and and ensure that it returns one result.
Function:
(defun check-safe-assign-single (target value varset funtab) (declare (xargs :guard (and (pathp target) (expressionp value) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-assign-single)) (declare (ignorable __function__)) (b* (((okf &) (check-safe-path target varset)) ((okf results) (check-safe-expression value varset funtab)) ((unless (= results 1)) (reserrf (list :assign-single-var-mismatch (path-fix target) results)))) nil)))
Theorem:
(defthm reserr-optionp-of-check-safe-assign-single (b* ((_ (check-safe-assign-single target value varset funtab))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-assign-single-of-path-fix-target (equal (check-safe-assign-single (path-fix target) value varset funtab) (check-safe-assign-single target value varset funtab)))
Theorem:
(defthm check-safe-assign-single-path-equiv-congruence-on-target (implies (path-equiv target target-equiv) (equal (check-safe-assign-single target value varset funtab) (check-safe-assign-single target-equiv value varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-assign-single-of-expression-fix-value (equal (check-safe-assign-single target (expression-fix value) varset funtab) (check-safe-assign-single target value varset funtab)))
Theorem:
(defthm check-safe-assign-single-expression-equiv-congruence-on-value (implies (expression-equiv value value-equiv) (equal (check-safe-assign-single target value varset funtab) (check-safe-assign-single target value-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-assign-single-of-identifier-set-fix-varset (equal (check-safe-assign-single target value (identifier-set-fix varset) funtab) (check-safe-assign-single target value varset funtab)))
Theorem:
(defthm check-safe-assign-single-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-assign-single target value varset funtab) (check-safe-assign-single target value varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-assign-single-of-funtable-fix-funtab (equal (check-safe-assign-single target value varset (funtable-fix funtab)) (check-safe-assign-single target value varset funtab)))
Theorem:
(defthm check-safe-assign-single-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-assign-single target value varset funtab) (check-safe-assign-single target value varset funtab-equiv))) :rule-classes :congruence)