		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Funinfo-safep

Check the safety of function information.

Signature
(funinfo-safep funinfo funtab) → yes/no
Arguments: funinfo — Guard (funinfop funinfo).; funtab — Guard (funtablep funtab).
Returns: yes/no — Type (booleanp yes/no).

A key execution invariant needed for the static soundness proof is that, if the code being executed passes the static safety checks, then the functions in the function environments pass those checks. This predicate captures this notion of safety for function information: it performs the same checks as check-safe-fundef, except that it does so on function information instead of a function definition (so we could not use check-safe-fundef here, because we have no function definition). Safety is necessarily checked with respect to some function table. See funscope-safep and funenv-safep for more information.

Definitions and Theorems

Function: funinfo-safep

(defun funinfo-safep (funinfo funtab)
  (declare (xargs :guard (and (funinfop funinfo)
                              (funtablep funtab))))
  (let ((__function__ 'funinfo-safep))
    (declare (ignorable __function__))
    (b* (((funinfo funinfo) funinfo)
         (varset (add-vars funinfo.inputs nil))
         ((when (reserrp varset)) nil)
         (varset (add-vars funinfo.outputs varset))
         ((when (reserrp varset)) nil)
         (modes (check-safe-block funinfo.body varset funtab))
         ((when (reserrp modes)) nil)
         ((when (in (mode-break) modes)) nil)
         ((when (in (mode-continue) modes)) nil))
      t)))

Theorem: booleanp-of-funinfo-safep

(defthm booleanp-of-funinfo-safep
  (b* ((yes/no (funinfo-safep funinfo funtab)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: funinfo-safep-of-funinfo-fix-funinfo

(defthm funinfo-safep-of-funinfo-fix-funinfo
  (equal (funinfo-safep (funinfo-fix funinfo)
                        funtab)
         (funinfo-safep funinfo funtab)))

Theorem: funinfo-safep-funinfo-equiv-congruence-on-funinfo

(defthm funinfo-safep-funinfo-equiv-congruence-on-funinfo
  (implies (funinfo-equiv funinfo funinfo-equiv)
           (equal (funinfo-safep funinfo funtab)
                  (funinfo-safep funinfo-equiv funtab)))
  :rule-classes :congruence)

Theorem: funinfo-safep-of-funtable-fix-funtab

(defthm funinfo-safep-of-funtable-fix-funtab
  (equal (funinfo-safep funinfo (funtable-fix funtab))
         (funinfo-safep funinfo funtab)))

Theorem: funinfo-safep-funtable-equiv-congruence-on-funtab

(defthm funinfo-safep-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (funinfo-safep funinfo funtab)
                  (funinfo-safep funinfo funtab-equiv)))
  :rule-classes :congruence)