		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Check-var-list

Check if the variables in a list are all in a variable table.

Signature
(check-var-list vars varset) → yes/no
Arguments: vars — Guard (identifier-listp vars).; varset — Guard (identifier-setp varset).
Returns: yes/no — Type (booleanp yes/no).

This lifts check-var to lists. It is not actually part of the formalization of the static safety checks, because that formalization uses check-var to define check-safe-path, and then lifts the latter to lists. For the static soundness proof, it is useful to have this check-var-list function. We may refactor the static safety checks to include this function, at some point, but for now we just define it here.

We prove a theorem that turns check-var-list into the inclusion of the list of variable in the variable table, which is a set.

Definitions and Theorems

Function: check-var-list

(defun check-var-list (vars varset)
  (declare (xargs :guard (and (identifier-listp vars)
                              (identifier-setp varset))))
  (let ((__function__ 'check-var-list))
    (declare (ignorable __function__))
    (or (endp vars)
        (and (check-var (car vars) varset)
             (check-var-list (cdr vars) varset)))))

Theorem: booleanp-of-check-var-list

(defthm booleanp-of-check-var-list
  (b* ((yes/no (check-var-list vars varset)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: check-var-list-to-set-list-in

(defthm check-var-list-to-set-list-in
  (implies (and (identifier-listp vars)
                (identifier-setp varset))
           (equal (check-var-list vars varset)
                  (set::list-in vars varset))))

Theorem: check-var-list-of-identifier-list-fix-vars

(defthm check-var-list-of-identifier-list-fix-vars
  (equal (check-var-list (identifier-list-fix vars)
                         varset)
         (check-var-list vars varset)))

Theorem: check-var-list-identifier-list-equiv-congruence-on-vars

(defthm check-var-list-identifier-list-equiv-congruence-on-vars
  (implies (identifier-list-equiv vars vars-equiv)
           (equal (check-var-list vars varset)
                  (check-var-list vars-equiv varset)))
  :rule-classes :congruence)

Theorem: check-var-list-of-identifier-set-fix-varset

(defthm check-var-list-of-identifier-set-fix-varset
  (equal (check-var-list vars (identifier-set-fix varset))
         (check-var-list vars varset)))

Theorem: check-var-list-identifier-set-equiv-congruence-on-varset

(defthm check-var-list-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-var-list vars varset)
                  (check-var-list vars varset-equiv)))
  :rule-classes :congruence)