Check if a list of function definitions is safe.
(check-safe-fundef-list fundefs funtab) → _
This does not really add anything compared to check-safe-statement-list, in the sense that checking the safety of a list of function definitions is the same as checking the safety of them as a list of statements. However, it is convenient to define a dedicated ACL2 function to check the safety of lists of function definitions directly, and that does not return any information if the safety checks succeed. (This ACL2 function is used in the static soundness proof.)
We prove that if a list of statements passes the safety checks, the list of function definitions extracted from the statements passes the safety checks according to this ACL2 function. Given that the statement checking functions take variable tables as inputs while the function definition checking function do not, and given that the statement checking functions modify variable tables and thread them through the list of statements, we carry out the induction proof on a predicate that is universally quantified over variable tables.
Function:
(defun check-safe-fundef-list (fundefs funtab) (declare (xargs :guard (and (fundef-listp fundefs) (funtablep funtab)))) (let ((__function__ 'check-safe-fundef-list)) (declare (ignorable __function__)) (b* (((when (endp fundefs)) nil) ((okf &) (check-safe-fundef (car fundefs) funtab)) ((okf &) (check-safe-fundef-list (cdr fundefs) funtab))) nil)))
Theorem:
(defthm reserr-optionp-of-check-safe-fundef-list (b* ((_ (check-safe-fundef-list fundefs funtab))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-fundef-list-of-statements-to-fundefs (implies (not (reserrp (check-safe-statement-list stmts varset funtab))) (not (reserrp (check-safe-fundef-list (statements-to-fundefs stmts) funtab)))))
Theorem:
(defthm check-safe-fundef-list-of-fundef-list-fix-fundefs (equal (check-safe-fundef-list (fundef-list-fix fundefs) funtab) (check-safe-fundef-list fundefs funtab)))
Theorem:
(defthm check-safe-fundef-list-fundef-list-equiv-congruence-on-fundefs (implies (fundef-list-equiv fundefs fundefs-equiv) (equal (check-safe-fundef-list fundefs funtab) (check-safe-fundef-list fundefs-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-fundef-list-of-funtable-fix-funtab (equal (check-safe-fundef-list fundefs (funtable-fix funtab)) (check-safe-fundef-list fundefs funtab)))
Theorem:
(defthm check-safe-fundef-list-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-fundef-list fundefs funtab) (check-safe-fundef-list fundefs funtab-equiv))) :rule-classes :congruence)