Theorems about the variable table being extended by the ACL2 safety checking functions.
The safety checking functions that return updated variables tables, namely check-safe-statement and check-safe-statement-list, extend the variable table in general. That is, the resulting variable table is always a superset of the initial variable table; this is not strict superset, i.e. they may be equal. We prove that first for add-var and add-vars, which are the functions that actually extend the variable table in the safety checking functions, and then we prove it on the safety checking functions by induction.
Theorem:
(defthm add-var-extends-varset (implies (identifier-setp varset) (b* ((varset1 (add-var var varset))) (implies (not (reserrp varset1)) (subset varset varset1)))))
Theorem:
(defthm add-vars-extends-varset (implies (identifier-setp varset) (b* ((varset1 (add-vars vars varset))) (implies (not (reserrp varset1)) (subset varset varset1)))))
Theorem:
(defthm check-safe-variable-single-extends-varset (implies (identifier-setp varset) (b* ((varset1 (check-safe-variable-single name init varset funtab))) (implies (not (reserrp varset1)) (subset varset varset1)))))
Theorem:
(defthm check-safe-variable-multi-extends-varset (implies (identifier-setp varset) (b* ((varset1 (check-safe-variable-multi name init varset funtab))) (implies (not (reserrp varset1)) (subset varset varset1)))))
Theorem:
(defthm check-safe-statement-extends-varset (implies (identifier-setp varset) (b* ((varsmodes (check-safe-statement stmt varset funtab))) (implies (not (reserrp varsmodes)) (subset varset (vars+modes->vars varsmodes))))))
Theorem:
(defthm check-safe-statement-list-extends-varset (implies (identifier-setp varset) (b* ((varsmodes (check-safe-statement-list stmts varset funtab))) (implies (not (reserrp varsmodes)) (subset varset (vars+modes->vars varsmodes))))))
Theorem:
(defthm check-safe-block-extends-varset t :rule-classes nil)
Theorem:
(defthm check-safe-block-option-extends-varset t :rule-classes nil)
Theorem:
(defthm check-safe-swcase-extends-varset t :rule-classes nil)
Theorem:
(defthm check-safe-swcase-list-extends-varset t :rule-classes nil)
Theorem:
(defthm check-safe-fundef-extends-varset t :rule-classes nil)