Check the safety of a function scope.
See funinfo-safep for motivation (i.e. the invariant). This predicate checks the safety of all the values of the omap.
Function:
(defun funscope-safep (funscope funtab) (declare (xargs :guard (and (funscopep funscope) (funtablep funtab)))) (let ((__function__ 'funscope-safep)) (declare (ignorable __function__)) (b* (((when (or (not (mbt (funscopep funscope))) (omap::emptyp funscope))) t) ((mv & info) (omap::head funscope))) (and (funinfo-safep info funtab) (funscope-safep (omap::tail funscope) funtab)))))
Theorem:
(defthm booleanp-of-funscope-safep (b* ((yes/no (funscope-safep funscope funtab))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm funscope-safep-of-update (implies (and (identifierp fun) (funinfop funinfo) (funscopep funscope) (funinfo-safep funinfo funtab) (funscope-safep funscope funtab)) (funscope-safep (omap::update fun funinfo funscope) funtab)))
Theorem:
(defthm funscope-safep-of-funscope-fix-funscope (equal (funscope-safep (funscope-fix funscope) funtab) (funscope-safep funscope funtab)))
Theorem:
(defthm funscope-safep-funscope-equiv-congruence-on-funscope (implies (funscope-equiv funscope funscope-equiv) (equal (funscope-safep funscope funtab) (funscope-safep funscope-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm funscope-safep-of-funtable-fix-funtab (equal (funscope-safep funscope (funtable-fix funtab)) (funscope-safep funscope funtab)))
Theorem:
(defthm funscope-safep-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (funscope-safep funscope funtab) (funscope-safep funscope funtab-equiv))) :rule-classes :congruence)