• 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

Svex-env-compat-union

Signature

(svex-env-compat-union x y) → (mv err union)

Arguments

x — Guard (svex-env-p x).

y — Guard (svex-env-p y).

Returns

union — Type (svex-env-p union).

Definitions and Theorems

Function: svex-env-compat-union

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

Theorem: svex-env-p-of-svex-env-compat-union.union

(defthm svex-env-p-of-svex-env-compat-union.union
  (b* (((mv ?err set::?union)
        (svex-env-compat-union x y)))
    (svex-env-p union))
  :rule-classes :rewrite)

Theorem: svar-lookup-in-svex-env-fix

(defthm svar-lookup-in-svex-env-fix
  (equal (svar-lookup k (svex-env-fix env))
         (and (svar-lookup k env)
              (cons (svar-fix k)
                    (4vec-fix (cdr (svar-lookup k env)))))))

Theorem: lookup-in-compat-union-2

(defthm lookup-in-compat-union-2
  (b* (((mv err union)
        (svex-env-compat-union x y)))
    (implies (and (svar-lookup k (svex-env-fix y))
                  (not err))
             (equal (svar-lookup k union)
                    (svar-lookup k (svex-env-fix y))))))

Theorem: lookup-in-compat-union-1

(defthm lookup-in-compat-union-1
  (b* (((mv err union)
        (svex-env-compat-union x y)))
    (implies (and (svar-lookup k (svex-env-fix x))
                  (not err))
             (equal (svar-lookup k union)
                    (svar-lookup k (svex-env-fix x))))))

Theorem: lookup-in-compat-union-neither

(defthm lookup-in-compat-union-neither
  (b* (((mv ?err union)
        (svex-env-compat-union x y)))
    (implies (and (not (svar-lookup k (svex-env-fix x)))
                  (not (svar-lookup k (svex-env-fix y))))
             (equal (svar-lookup k union) nil))))

Theorem: compat-union-reduce-to-append

(defthm compat-union-reduce-to-append
  (b* (((mv err union)
        (svex-env-compat-union x y)))
    (implies (not err)
             (svex-envs-similar union (append x y)))))

Theorem: svex-eval-compat-union-when-vars-in-first

(defthm svex-eval-compat-union-when-vars-in-first
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svex-vars x)
                           (svar-alist-keys (svex-env-fix env)))
                  (not err))
             (equal (svex-eval x union)
                    (svex-eval x env)))))

Theorem: svexlist-eval-compat-union-when-vars-in-first

(defthm svexlist-eval-compat-union-when-vars-in-first
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svexlist-vars x)
                           (svar-alist-keys (svex-env-fix env)))
                  (not err))
             (equal (svexlist-eval x union)
                    (svexlist-eval x env)))))

Theorem: svex-alist-eval-compat-union-when-vars-in-first

(defthm svex-alist-eval-compat-union-when-vars-in-first
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svex-alist-vars x)
                           (svar-alist-keys (svex-env-fix env)))
                  (not err))
             (equal (svex-alist-eval x union)
                    (svex-alist-eval x env)))))

Theorem: svex-eval-compat-union-when-vars-in-second

(defthm svex-eval-compat-union-when-vars-in-second
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svex-vars x)
                           (svar-alist-keys (svex-env-fix env2)))
                  (not err))
             (equal (svex-eval x union)
                    (svex-eval x env2)))))

Theorem: svexlist-eval-compat-union-when-vars-in-second

(defthm svexlist-eval-compat-union-when-vars-in-second
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svexlist-vars x)
                           (svar-alist-keys (svex-env-fix env2)))
                  (not err))
             (equal (svexlist-eval x union)
                    (svexlist-eval x env2)))))

Theorem: svex-alist-eval-compat-union-when-vars-in-second

(defthm svex-alist-eval-compat-union-when-vars-in-second
  (b* (((mv err union)
        (svex-env-compat-union env env2)))
    (implies (and (subsetp (svex-alist-vars x)
                           (svar-alist-keys (svex-env-fix env2)))
                  (not err))
             (equal (svex-alist-eval x union)
                    (svex-alist-eval x env2)))))

Theorem: alist-keys-of-svex-env-compat-union

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

Theorem: svex-env-compat-union-of-svex-env-fix-x

(defthm svex-env-compat-union-of-svex-env-fix-x
  (equal (svex-env-compat-union (svex-env-fix x)
                                y)
         (svex-env-compat-union x y)))

Theorem: svex-env-compat-union-svex-env-equiv-congruence-on-x

(defthm svex-env-compat-union-svex-env-equiv-congruence-on-x
  (implies (svex-env-equiv x x-equiv)
           (equal (svex-env-compat-union x y)
                  (svex-env-compat-union x-equiv y)))
  :rule-classes :congruence)

Theorem: svex-env-compat-union-of-svex-env-fix-y

(defthm svex-env-compat-union-of-svex-env-fix-y
  (equal (svex-env-compat-union x (svex-env-fix y))
         (svex-env-compat-union x y)))

Theorem: svex-env-compat-union-svex-env-equiv-congruence-on-y

(defthm svex-env-compat-union-svex-env-equiv-congruence-on-y
  (implies (svex-env-equiv y y-equiv)
           (equal (svex-env-compat-union x y)
                  (svex-env-compat-union x y-equiv)))
  :rule-classes :congruence)