Theorems about add-funs for the static soundness proof.
Similarly to how get-funtype and find-fun are static/dynamic counterparts, so add-funtypes and add-funs are static/dynamic counterparts. Here we prove theorems that relate the latter two, or that relate functions that the latter two are built on.
We also prove theorems about the preservation of the safety invariant of function environments. Essentially, given a safe function environments, if we extend with a new scope whose functions are safe in the function table that also includes those functions, we push a scope into the stack that satisfies the invariant; and furthermore, the existing scopes still satisfy the invariant, because the invariant only refers to the current and earlier scopes, not to later ones that are pushed.
Theorem:
(defthm funinfo-to-funtype-of-funinfo-for-fundef (equal (funinfo-to-funtype (funinfo-for-fundef fundef)) (funtype-for-fundef fundef)))
Theorem:
(defthm in-funscope-for-fundefs-iff-in-funtable-for-fundefs (implies (and (not (reserrp (funscope-for-fundefs fundefs))) (not (reserrp (funtable-for-fundefs fundefs)))) (equal (consp (omap::assoc fun (funscope-for-fundefs fundefs))) (consp (omap::assoc fun (funtable-for-fundefs fundefs))))))
Theorem:
(defthm error-funscope-for-fundefs-iff-error-funtable-for-fundefs (equal (reserrp (funscope-for-fundefs fundefs)) (reserrp (funtable-for-fundefs fundefs))))
Theorem:
(defthm funscope-to-funtable-of-funscope-for-fundefs (implies (not (reserrp (funscope-for-fundefs fundefs))) (equal (funscope-to-funtable (funscope-for-fundefs fundefs)) (funtable-for-fundefs fundefs))))
Theorem:
(defthm keys-of-funscope-for-fundefs-is-keys-of-funtable-for-fundefs (implies (and (not (reserrp (funscope-for-fundefs fundefs))) (not (reserrp (funtable-for-fundefs fundefs)))) (equal (omap::keys (funscope-for-fundefs fundefs)) (omap::keys (funtable-for-fundefs fundefs)))))
Theorem:
(defthm funenv-to-funtable-of-add-funs (implies (not (reserrp (add-funs fundefs funenv))) (equal (funenv-to-funtable (add-funs fundefs funenv)) (add-funtypes fundefs (funenv-to-funtable funenv)))))
Theorem:
(defthm error-add-funs-iff-error-add-funtypes (equal (reserrp (add-funs fundefs funenv)) (reserrp (add-funtypes fundefs (funenv-to-funtable funenv)))))
Theorem:
(defthm funinfo-safep-of-funinfo-for-fundef (implies (not (reserrp (check-safe-fundef fundef funtab))) (funinfo-safep (funinfo-for-fundef fundef) funtab)))
Theorem:
(defthm funscope-safep-of-funscope-for-fundefs (implies (and (not (reserrp (check-safe-fundef-list fundefs funtab))) (not (reserrp (funscope-for-fundefs fundefs)))) (funscope-safep (funscope-for-fundefs fundefs) funtab)))
Theorem:
(defthm car-of-add-funs (implies (not (reserrp (add-funs fundefs funenv))) (equal (car (add-funs fundefs funenv)) (funscope-for-fundefs fundefs))))
Theorem:
(defthm cdr-of-add-funs (implies (not (reserrp (add-funs fundefs funenv))) (equal (cdr (add-funs fundefs funenv)) (funenv-fix funenv))))
Theorem:
(defthm not-error-funscope-for-fundefs-when-not-error-add-funs (implies (not (reserrp (add-funs fundefs funenv))) (not (reserrp (funscope-for-fundefs fundefs)))))
Theorem:
(defthm funenv-safep-of-add-funs (implies (and (funenv-safep funenv) (not (reserrp (add-funs fundefs funenv))) (not (reserrp (check-safe-fundef-list fundefs (add-funtypes fundefs (funenv-to-funtable funenv)))))) (funenv-safep (add-funs fundefs funenv))))