		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstacks-compatible

Predicate that describes two svstacks that are in the same scope, but may have different values for the bound variables.

Signature
(svstacks-compatible then-st else-st) → *
Arguments: then-st — Guard (svstack-p then-st).; else-st — Guard (svstack-p else-st).

When we arrive at an IF, we create two versions of the state, one for the THEN and one for the ELSE. When we are done symbolically simulating both, we merge the two states. These two resulting states are back in the outer scope (the scopes for the then and else branches have been popped off) and they may have different values assigned to variables at some scopes, but the only place they may differ in which variables are bound is at the outermost (global) scope. This is because inside the inner block, there is no way to declare a variable for an outer scope other than the global one.

Symbolically simulating an assignment statement preserves svstack compatibility because it will only create a variable at the global scope; a local scope can get a modified value of the variable, but only if it already exists there.

Definitions and Theorems

Function: svstacks-compatible

(defun svstacks-compatible (then-st else-st)
  (declare (xargs :guard (and (svstack-p then-st)
                              (svstack-p else-st))))
  (let ((__function__ 'svstacks-compatible))
    (declare (ignorable __function__))
    (if (atom then-st)
        (atom else-st)
      (and (consp else-st)
           (if (atom (cdr then-st))
               (atom (cdr else-st))
             (and (consp (cdr else-st))
                  (set-equiv (svex-alist-keys (car then-st))
                             (svex-alist-keys (car else-st)))
                  (svstacks-compatible (cdr then-st)
                                       (cdr else-st))))))))

Theorem: svstacks-compatible-of-svstack-fix-then-st

(defthm svstacks-compatible-of-svstack-fix-then-st
  (equal (svstacks-compatible (svstack-fix then-st)
                              else-st)
         (svstacks-compatible then-st else-st)))

Theorem: svstacks-compatible-svstack-equiv-congruence-on-then-st

(defthm svstacks-compatible-svstack-equiv-congruence-on-then-st
  (implies (svstack-equiv then-st then-st-equiv)
           (equal (svstacks-compatible then-st else-st)
                  (svstacks-compatible then-st-equiv else-st)))
  :rule-classes :congruence)

Theorem: svstacks-compatible-of-svstack-fix-else-st

(defthm svstacks-compatible-of-svstack-fix-else-st
  (equal (svstacks-compatible then-st (svstack-fix else-st))
         (svstacks-compatible then-st else-st)))

Theorem: svstacks-compatible-svstack-equiv-congruence-on-else-st

(defthm svstacks-compatible-svstack-equiv-congruence-on-else-st
  (implies (svstack-equiv else-st else-st-equiv)
           (equal (svstacks-compatible then-st else-st)
                  (svstacks-compatible then-st else-st-equiv)))
  :rule-classes :congruence)

Theorem: svstacks-compatible-is-an-equivalence

(defthm svstacks-compatible-is-an-equivalence
  (and (booleanp (svstacks-compatible x y))
       (svstacks-compatible x x)
       (implies (svstacks-compatible x y)
                (svstacks-compatible y x))
       (implies (and (svstacks-compatible x y)
                     (svstacks-compatible y z))
                (svstacks-compatible x z)))
  :rule-classes (:equivalence))

Theorem: svstacks-compatible-of-svstack-assign

(defthm svstacks-compatible-of-svstack-assign
  (implies (consp x)
           (svstacks-compatible (svstack-assign k v x)
                                x)))

Theorem: svstacks-compatible-of-cdr

(defthm svstacks-compatible-of-cdr
  (implies (svstacks-compatible x y)
           (equal (svstacks-compatible (cdr x) (cdr y))
                  t)))

Theorem: equal-implies-svstacks-compatible-svstacks-compatible-1

(defthm equal-implies-svstacks-compatible-svstacks-compatible-1
  (implies (equal a a-equiv)
           (svstacks-compatible (svstacks-compatible a b)
                                (svstacks-compatible a-equiv b)))
  :rule-classes (:congruence))

Theorem: equal-implies-svstacks-compatible-svstacks-compatible-2

(defthm equal-implies-svstacks-compatible-svstacks-compatible-2
  (implies (equal b b-equiv)
           (svstacks-compatible (svstacks-compatible a b)
                                (svstacks-compatible a b-equiv)))
  :rule-classes (:congruence))

Theorem: svstacks-compatible-of-svstack-fork

(defthm svstacks-compatible-of-svstack-fork
  (svstacks-compatible (svstack-fork x)
                       x))

Theorem: svstacks-compatible-blkst-of-svstate-fork

(defthm svstacks-compatible-blkst-of-svstate-fork
  (svstacks-compatible (svstate->blkst (svstate-fork x))
                       (svstate->blkst x)))