		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-extends-varset

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.

Definitions and Theorems

Theorem: add-var-extends-varset

(defthm add-var-extends-varset
  (implies (identifier-setp varset)
           (b* ((varset1 (add-var var varset)))
             (implies (not (reserrp varset1))
                      (subset varset varset1)))))

Theorem: add-vars-extends-varset

(defthm add-vars-extends-varset
  (implies (identifier-setp varset)
           (b* ((varset1 (add-vars vars varset)))
             (implies (not (reserrp varset1))
                      (subset varset varset1)))))

Theorem: check-safe-variable-single-extends-varset

(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: check-safe-variable-multi-extends-varset

(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: check-safe-statement-extends-varset

(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: check-safe-statement-list-extends-varset

(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: check-safe-block-extends-varset

(defthm check-safe-block-extends-varset
  t
  :rule-classes nil)

Theorem: check-safe-block-option-extends-varset

(defthm check-safe-block-option-extends-varset
  t
  :rule-classes nil)

Theorem: check-safe-swcase-extends-varset

(defthm check-safe-swcase-extends-varset
  t
  :rule-classes nil)

Theorem: check-safe-swcase-list-extends-varset

(defthm check-safe-swcase-list-extends-varset
  t
  :rule-classes nil)

Theorem: check-safe-fundef-extends-varset

(defthm check-safe-fundef-extends-varset
  t
  :rule-classes nil)