		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Funenv-safep

Check the safey of a function environment.

Signature
(funenv-safep funenv) → yes/no
Arguments: funenv — Guard (funenvp funenv).
Returns: yes/no — Type (booleanp yes/no).

The invariant alluded to in funinfo-safep is here defined. Recall that a function enviroment is a stack of function scope. The invariant is that each function scope is safe (i.e. all the functions in the scope are safe) with respect to the function table consisting of that scope and all the preceding scopes in the stack. In fact, as a new function scope is pushed onto the stack, the functions are safe with respect to not only the functions already in scope, but also the functions of the new scope: a function is always in its own scope, making recursive calls possible.

Definitions and Theorems

Function: funenv-safep

(defun funenv-safep (funenv)
  (declare (xargs :guard (funenvp funenv)))
  (let ((__function__ 'funenv-safep))
    (declare (ignorable __function__))
    (or (endp funenv)
        (and (funscope-safep (car funenv)
                             (funenv-to-funtable funenv))
             (funenv-safep (cdr funenv))))))

Theorem: booleanp-of-funenv-safep

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

Theorem: funenv-safep-of-funenv-fix-funenv

(defthm funenv-safep-of-funenv-fix-funenv
  (equal (funenv-safep (funenv-fix funenv))
         (funenv-safep funenv)))

Theorem: funenv-safep-funenv-equiv-congruence-on-funenv

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