		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-theorems-about-add-funs

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.

Definitions and Theorems

Theorem: funinfo-to-funtype-of-funinfo-for-fundef

(defthm funinfo-to-funtype-of-funinfo-for-fundef
        (equal (funinfo-to-funtype (funinfo-for-fundef fundef))
               (funtype-for-fundef fundef)))

Theorem: in-funscope-for-fundefs-iff-in-funtable-for-fundefs

(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::in fun (funscope-for-fundefs fundefs)))
            (consp (omap::in fun (funtable-for-fundefs fundefs))))))

Theorem: error-funscope-for-fundefs-iff-error-funtable-for-fundefs

(defthm error-funscope-for-fundefs-iff-error-funtable-for-fundefs
        (equal (reserrp (funscope-for-fundefs fundefs))
               (reserrp (funtable-for-fundefs fundefs))))

Theorem: funscope-to-funtable-of-funscope-for-fundefs

(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: keys-of-funscope-for-fundefs-is-keys-of-funtable-for-fundefs

(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: funenv-to-funtable-of-add-funs

(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: error-add-funs-iff-error-add-funtypes

(defthm
 error-add-funs-iff-error-add-funtypes
 (equal
      (reserrp (add-funs fundefs funenv))
      (reserrp (add-funtypes fundefs (funenv-to-funtable funenv)))))

Theorem: funinfo-safep-of-funinfo-for-fundef

(defthm funinfo-safep-of-funinfo-for-fundef
        (implies (not (reserrp (check-safe-fundef fundef funtab)))
                 (funinfo-safep (funinfo-for-fundef fundef)
                                funtab)))

Theorem: funscope-safep-of-funscope-for-fundefs

(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: car-of-add-funs

(defthm car-of-add-funs
        (implies (not (reserrp (add-funs fundefs funenv)))
                 (equal (car (add-funs fundefs funenv))
                        (funscope-for-fundefs fundefs))))

Theorem: cdr-of-add-funs

(defthm cdr-of-add-funs
        (implies (not (reserrp (add-funs fundefs funenv)))
                 (equal (cdr (add-funs fundefs funenv))
                        (funenv-fix funenv))))

Theorem: not-error-funscope-for-fundefs-when-not-error-add-funs

(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: funenv-safep-of-add-funs

(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))))