• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
        • Decomp.lisp
          • Svex-env-compat-union
          • Svdecomp-symenv-compat-union
          • Svexlists-rewrite-until-same
          • Svdecomp-normalize-svexlist-eval
          • Svex-decomp-process-env-term
          • Map-alist-term-keys-to-val-terms
          • Envmap-extract-union-env
          • Alist-collect-compositions
          • Envmap-entry-extract-env
          • Svdecomp-env-extract
          • Svex-alist-evaluation-to-symenv
          • Envmap-entry-to-term-alist
          • Svar-lookup
          • Svar-alist-keys
          • Map-alist-const-keys-to-val-terms
          • Svdecomp-svex?-eval-compare-term
          • Svdecomp-equal-svex-evals-metafun
          • Svdecomp-equal-svex-alist-evals-metafun
          • Envmap->svex-alist
          • Envmap-to-term-alist
          • Svdecomp-equal-svexlist-evals-metafun
          • Pseudo-term-fix
          • Svdecomp-symenv->term
          • Svdecomp-svex-alist-eval-metafun
          • Svdecomp-ev-symenv
          • Svdecomp-svexlist-eval-metafun
          • Svdecomp-svex-eval-metafun
          • Svdecomp-ev-envmap
          • Envmap
          • Svex-alist-alist
          • Svdecomp-symenv
          • Svdecomp-get-rewrite-limit
        • Svdecomp-hints
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Decomp.lisp

Svdecomp-symenv-compat-union

Signature

(svdecomp-symenv-compat-union x y) → (mv err union)

Arguments

x — Guard (svdecomp-symenv-p x).

y — Guard (svdecomp-symenv-p y).

Returns

union — Type (svdecomp-symenv-p union), given the guard.

Definitions and Theorems

Function: svdecomp-symenv-compat-union

(defun svdecomp-symenv-compat-union (x y)
  (declare (xargs :guard (and (svdecomp-symenv-p x)
                              (svdecomp-symenv-p y))))
  (let ((__function__ 'svdecomp-symenv-compat-union))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv nil (svar-alist-fix y)))
         ((unless (mbt (and (consp (car x))
                            (svar-p (caar x)))))
          (svdecomp-symenv-compat-union (cdr x)
                                        y))
         ((cons var val) (car x))
         (look (svar-lookup var (svar-alist-fix y)))
         ((unless (or (not look) (equal (cdr look) val)))
          (mv (msg "Mismatch: key ~x0, val ~x1 versus ~x2~%"
                   var val (cdr look))
              nil)))
      (svdecomp-symenv-compat-union
           (cdr x)
           (if look y (hons-acons var val y))))))

Theorem: svdecomp-symenv-p-of-svdecomp-symenv-compat-union.union

(defthm svdecomp-symenv-p-of-svdecomp-symenv-compat-union.union
  (implies (and (svdecomp-symenv-p x)
                (svdecomp-symenv-p y))
           (b* (((mv ?err set::?union)
                 (svdecomp-symenv-compat-union x y)))
             (svdecomp-symenv-p union)))
  :rule-classes :rewrite)

Theorem: svdecomp-symenv-compat-union-error-cond

(defthm svdecomp-symenv-compat-union-error-cond
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y))
       ((mv err ?union)
        (svex-env-compat-union (svdecomp-ev-symenv x a)
                               (svdecomp-ev-symenv y a))))
    (implies (not symerr) (not err))))

Theorem: eval-svdecomp-symenv-compat-union

(defthm eval-svdecomp-symenv-compat-union
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y))
       ((mv ?err ?union)
        (svex-env-compat-union (svdecomp-ev-symenv x a)
                               (svdecomp-ev-symenv y a))))
    (implies (not symerr)
             (svex-env-equiv (svdecomp-ev-symenv symunion a)
                             union))))

Theorem: lookup-in-svdecomp-symenv-compat-union-when-in-y

(defthm lookup-in-svdecomp-symenv-compat-union-when-in-y
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y)))
    (implies (and (not symerr) (svar-lookup k y))
             (equal (svar-lookup k symunion)
                    (svar-lookup k y)))))

Theorem: lookup-in-svdecomp-symenv-compat-union-when-not-in-y

(defthm lookup-in-svdecomp-symenv-compat-union-when-not-in-y
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y)))
    (implies (and (not symerr)
                  (case-split (not (svar-lookup k y))))
             (equal (svar-lookup k symunion)
                    (svar-lookup k x)))))

Theorem: lookup-in-svdecomp-symenv-compat-union-when-in-x

(defthm lookup-in-svdecomp-symenv-compat-union-when-in-x
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y)))
    (implies (and (not symerr) (svar-lookup k x))
             (equal (svar-lookup k symunion)
                    (svar-lookup k x)))))

Theorem: lookup-in-svdecomp-symenv-compat-union-when-not-in-x

(defthm lookup-in-svdecomp-symenv-compat-union-when-not-in-x
  (b* (((mv symerr ?symunion)
        (svdecomp-symenv-compat-union x y)))
    (implies (and (not symerr)
                  (case-split (not (svar-lookup k x))))
             (equal (svar-lookup k symunion)
                    (svar-lookup k y)))))

Theorem: alist-keys-of-svdecomp-symenv-compat-union

(defthm alist-keys-of-svdecomp-symenv-compat-union
  (b* (((mv err union)
        (svdecomp-symenv-compat-union env env2)))
    (implies (not err)
             (set-equiv (svar-alist-keys union)
                        (append (svar-alist-keys env)
                                (svar-alist-keys env2))))))

Theorem: svdecomp-symenv-compat-union-of-svar-alist-fix-x

(defthm svdecomp-symenv-compat-union-of-svar-alist-fix-x
  (equal (svdecomp-symenv-compat-union (svar-alist-fix x)
                                       y)
         (svdecomp-symenv-compat-union x y)))

Theorem: svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-x

(defthm
      svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-x
  (implies (svar-alist-equiv x x-equiv)
           (equal (svdecomp-symenv-compat-union x y)
                  (svdecomp-symenv-compat-union x-equiv y)))
  :rule-classes :congruence)

Theorem: svdecomp-symenv-compat-union-of-svar-alist-fix-y

(defthm svdecomp-symenv-compat-union-of-svar-alist-fix-y
  (equal (svdecomp-symenv-compat-union x (svar-alist-fix y))
         (svdecomp-symenv-compat-union x y)))

Theorem: svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-y

(defthm
      svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-y
  (implies (svar-alist-equiv y y-equiv)
           (equal (svdecomp-symenv-compat-union x y)
                  (svdecomp-symenv-compat-union x y-equiv)))
  :rule-classes :congruence)