Theorems about find-fun for the static soundness proof.
We prove that if a function environment is safe, and if find-fun succeeds in that environment, then the resulting function is safe. We prove this for function scopes first, then for function environments. The latter is an important theorem to use in the static soundness proof: it serves to establish the safety of a function's body, when executing the function, so that the static soundness inductive hypothesis about the function applies, i.e. tells us that the execution of the body will not return an error result.
We also prove certain properties that relate get-funtype and find-fun, which are static/dynamic counterparts.
Theorem:
(defthm check-safe-block-when-funscope-safep (implies (and (identifierp fun) (funscopep funscope) (funscope-safep funscope funtab) (consp (omap::assoc fun funscope))) (b* ((funinfo (cdr (omap::assoc fun funscope))) (varset0 (add-vars (funinfo->inputs funinfo) nil)) (varset (add-vars (funinfo->outputs funinfo) varset0)) (modes (check-safe-block (funinfo->body funinfo) varset funtab))) (and (not (reserrp varset0)) (not (reserrp varset)) (not (reserrp modes)) (not (in (mode-break) modes)) (not (in (mode-continue) modes))))))
Theorem:
(defthm check-safe-block-when-funenv-safep (b* ((funinfoenv (find-fun fun funenv))) (implies (and (funenv-safep funenv) (not (reserrp funinfoenv))) (b* ((funinfo (funinfo+funenv->info funinfoenv)) (funenv1 (funinfo+funenv->env funinfoenv)) (varset0 (add-vars (funinfo->inputs funinfo) nil)) (varset (add-vars (funinfo->outputs funinfo) varset0)) (modes (check-safe-block (funinfo->body funinfo) varset (funenv-to-funtable funenv1)))) (and (not (reserrp varset0)) (not (reserrp varset)) (not (reserrp modes)) (not (in (mode-break) modes)) (not (in (mode-continue) modes)) (funenv-safep funenv1))))))
Theorem:
(defthm funinfo-to-funtype-of-cdr-of-in (implies (and (funscopep funscope) (consp (omap::assoc fun funscope))) (equal (funinfo-to-funtype (cdr (omap::assoc fun funscope))) (cdr (omap::assoc fun (funscope-to-funtable funscope))))))
Theorem:
(defthm funinfo-to-funtype-of-find-fun-info (b* ((funinfoenv (find-fun fun funenv)) (funtype (get-funtype fun (funenv-to-funtable funenv)))) (implies (not (reserrp funinfoenv)) (b* ((funinfo (funinfo+funenv->info funinfoenv))) (and (not (reserrp funtype)) (equal (funinfo-to-funtype funinfo) funtype))))))
Theorem:
(defthm reserrp-of-find-fun (equal (reserrp (find-fun fun funenv)) (reserrp (get-funtype fun (funenv-to-funtable funenv)))))