		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)