		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Atc-write-var-rules

Rules about write-var.

The theorem about write-var turns it into update-var, similarly to create-var being turned into add-var. The condition for the replacemenet is captured by write-var-okp, for which we supply rules to go through the computation state layers. When the computation state (meta) variable is reached, it must be the case that there are hypotheses available saying that reading the variable yields a value: this happens for loop proofs, for variables created outside the loop, which are therefore not visible as add-vars. The rule is used as last resort, only if the computation state is an ACL2 variable (as enforced by the syntaxp hypothesis).

We also include the executable counterpart of typep in the list of rules related to write-var. This is needed to discharge some typep hypotheses that arise during symbolic execution and are applied to quoted constants. We may arrange things in the future so that these quoted constants do not arise and thus there is no need for the executable counterpart of typep to be included in the list of rules here.

Also see atc-write-static-var-rules for a rule that relates write-var-okp and add-frame.

Definitions and Theorems

Function: write-var-aux-okp

(defun write-var-aux-okp (var val scopes)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (scope-listp scopes))))
  (let ((__function__ 'write-var-aux-okp))
    (declare (ignorable __function__))
    (b* (((when (endp scopes)) nil)
         (scope (scope-fix (car scopes)))
         (pair (omap::assoc (ident-fix var) scope))
         ((when (consp pair))
          (equal (type-of-value (cdr pair))
                 (type-of-value val))))
      (write-var-aux-okp var val (cdr scopes)))))

Theorem: booleanp-of-write-var-aux-okp

(defthm booleanp-of-write-var-aux-okp
  (b* ((yes/no (write-var-aux-okp var val scopes)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: write-var-aux-okp-of-ident-fix-var

(defthm write-var-aux-okp-of-ident-fix-var
  (equal (write-var-aux-okp (ident-fix var)
                            val scopes)
         (write-var-aux-okp var val scopes)))

Theorem: write-var-aux-okp-ident-equiv-congruence-on-var

(defthm write-var-aux-okp-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (write-var-aux-okp var val scopes)
                  (write-var-aux-okp var-equiv val scopes)))
  :rule-classes :congruence)

Theorem: write-var-aux-okp-of-value-fix-val

(defthm write-var-aux-okp-of-value-fix-val
  (equal (write-var-aux-okp var (value-fix val)
                            scopes)
         (write-var-aux-okp var val scopes)))

Theorem: write-var-aux-okp-value-equiv-congruence-on-val

(defthm write-var-aux-okp-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-var-aux-okp var val scopes)
                  (write-var-aux-okp var val-equiv scopes)))
  :rule-classes :congruence)

Theorem: write-var-aux-okp-of-scope-list-fix-scopes

(defthm write-var-aux-okp-of-scope-list-fix-scopes
  (equal (write-var-aux-okp var val (scope-list-fix scopes))
         (write-var-aux-okp var val scopes)))

Theorem: write-var-aux-okp-scope-list-equiv-congruence-on-scopes

(defthm write-var-aux-okp-scope-list-equiv-congruence-on-scopes
  (implies (scope-list-equiv scopes scopes-equiv)
           (equal (write-var-aux-okp var val scopes)
                  (write-var-aux-okp var val scopes-equiv)))
  :rule-classes :congruence)

Function: write-var-okp

(defun write-var-okp (var val compst)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (compustatep compst))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'write-var-okp))
    (declare (ignorable __function__))
    (b* ((scopes (frame->scopes (top-frame compst)))
         (autop (var-in-scopes-p var scopes))
         ((when autop)
          (write-var-aux-okp var val scopes))
         (static (compustate->static compst))
         (pair (omap::assoc (ident-fix var) static)))
      (and (consp pair)
           (equal (type-of-value (cdr pair))
                  (type-of-value val))))))

Theorem: booleanp-of-write-var-okp

(defthm booleanp-of-write-var-okp
  (b* ((yes/no (write-var-okp var val compst)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: write-var-okp-of-ident-fix-var

(defthm write-var-okp-of-ident-fix-var
  (equal (write-var-okp (ident-fix var)
                        val compst)
         (write-var-okp var val compst)))

Theorem: write-var-okp-ident-equiv-congruence-on-var

(defthm write-var-okp-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (write-var-okp var val compst)
                  (write-var-okp var-equiv val compst)))
  :rule-classes :congruence)

Theorem: write-var-okp-of-value-fix-val

(defthm write-var-okp-of-value-fix-val
  (equal (write-var-okp var (value-fix val)
                        compst)
         (write-var-okp var val compst)))

Theorem: write-var-okp-value-equiv-congruence-on-val

(defthm write-var-okp-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-var-okp var val compst)
                  (write-var-okp var val-equiv compst)))
  :rule-classes :congruence)

Theorem: write-var-okp-of-compustate-fix-compst

(defthm write-var-okp-of-compustate-fix-compst
  (equal (write-var-okp var val (compustate-fix compst))
         (write-var-okp var val compst)))

Theorem: write-var-okp-compustate-equiv-congruence-on-compst

(defthm write-var-okp-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (write-var-okp var val compst)
                  (write-var-okp var val compst-equiv)))
  :rule-classes :congruence)

Theorem: write-var-okp-of-enter-scope

(defthm write-var-okp-of-enter-scope
  (equal (write-var-okp var val (enter-scope compst))
         (write-var-okp var val compst)))

Theorem: write-var-okp-of-add-var

(defthm write-var-okp-of-add-var
  (equal (write-var-okp var val (add-var var2 val2 compst))
         (if (equal (ident-fix var) (ident-fix var2))
             (equal (type-of-value val2)
                    (type-of-value val))
           (write-var-okp var val compst))))

Theorem: write-var-okp-of-update-var

(defthm write-var-okp-of-update-var
  (equal (write-var-okp var val (update-var var2 val2 compst))
         (if (equal (ident-fix var) (ident-fix var2))
             (equal (type-of-value val2)
                    (type-of-value val))
           (write-var-okp var val compst))))

Theorem: write-var-okp-of-update-static-var

(defthm write-var-okp-of-update-static-var
  (implies
       (not (equal (ident-fix var)
                   (ident-fix var2)))
       (equal (write-var-okp var val
                             (update-static-var var2 val2 compst))
              (write-var-okp var val compst))))

Theorem: write-var-okp-of-update-object

(defthm write-var-okp-of-update-object
  (equal (write-var-okp var
                        val (update-object objdes obj compst))
         (write-var-okp var val compst)))

Theorem: write-var-okp-when-valuep-of-read-var

(defthm write-var-okp-when-valuep-of-read-var
  (implies (and (syntaxp (symbolp compst))
                (> (compustate-frames-number compst) 0)
                (equal old-val (read-var var compst))
                (valuep old-val))
           (equal (write-var-okp var val compst)
                  (equal (type-of-value val)
                         (type-of-value old-val)))))

Theorem: write-var-to-update-var

(defthm write-var-to-update-var
  (implies (and (> (compustate-frames-number compst) 0)
                (write-var-okp var val compst))
           (equal (write-var var val compst)
                  (update-var var val compst))))

Theorem: write-var-to-write-static-var

(defthm write-var-to-write-static-var
  (implies (not (var-autop var compst))
           (equal (write-var var val compst)
                  (write-static-var var val compst))))