		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Atc-create-var-rules

Rules about create-var.

The theorem about create-var turns that into add-var, provided that the variable can be created, which we check via the function create-var-okp introduced below, and also provided that there are frames. The latter condition is motivated by the fact that, during symbolic execution, we always have frames, because we are always executing code in some function; thus, we only need to replace create-var with add-var when there are frames. Additional theorems about create-var-okp go through the layers of the computation states to check this condition. No rule is needed for create-var-ok on update-var, because update-var is pushed past the first enter-scope.

Definitions and Theorems

Function: create-var-okp

(defun create-var-okp (var compst)
  (declare (xargs :guard (and (identp var)
                              (compustatep compst))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'create-var-okp))
    (declare (ignorable __function__))
    (b* ((frame (top-frame compst))
         (scopes (frame->scopes frame))
         (scope (car scopes)))
      (not (consp (omap::assoc (ident-fix var) scope))))))

Theorem: booleanp-of-create-var-okp

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

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

(defthm create-var-okp-of-ident-fix-var
  (equal (create-var-okp (ident-fix var) compst)
         (create-var-okp var compst)))

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

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

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

(defthm create-var-okp-of-compustate-fix-compst
  (equal (create-var-okp var (compustate-fix compst))
         (create-var-okp var compst)))

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

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

Theorem: create-var-okp-of-add-frame

(defthm create-var-okp-of-add-frame
  (create-var-okp var (add-frame fun compst)))

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

(defthm create-var-okp-of-enter-scope
  (create-var-okp var (enter-scope compst)))

Theorem: create-var-okp-of-add-var

(defthm create-var-okp-of-add-var
  (equal (create-var-okp var (add-var var2 val compst))
         (and (not (equal (ident-fix var)
                          (ident-fix var2)))
              (create-var-okp var compst))))

Theorem: create-var-okp-of-update-var

(defthm create-var-okp-of-update-var
  (equal (create-var-okp var (update-var var2 val compst))
         (create-var-okp var compst)))

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

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

Theorem: create-var-to-add-var

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