• 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

Envmap-entry-extract-env

Signature

(envmap-entry-extract-env x env) → res

Arguments

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

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

Returns

res — Type (svdecomp-symenv-p res), given (svdecomp-symenv-p env).

Definitions and Theorems

Function: envmap-entry-extract-env

(defun envmap-entry-extract-env (x env)
 (declare (xargs :guard (and (svex-alist-p x)
                             (svdecomp-symenv-p env))))
 (let ((__function__ 'envmap-entry-extract-env))
  (declare (ignorable __function__))
  (b*
   ((keys
        (mergesort
             (cwtime (svexlist-collect-vars (svex-alist-vals x))))))
   (with-fast-alist env (svdecomp-env-extract keys env)))))

Theorem: svdecomp-symenv-p-of-envmap-entry-extract-env

(defthm svdecomp-symenv-p-of-envmap-entry-extract-env
  (implies (svdecomp-symenv-p env)
           (b* ((res (envmap-entry-extract-env x env)))
             (svdecomp-symenv-p res)))
  :rule-classes :rewrite)

Theorem: svex-alist-eval-under-envmap-entry-extract-env

(defthm svex-alist-eval-under-envmap-entry-extract-env
  (equal (svex-alist-eval
              x
              (svdecomp-ev-symenv (envmap-entry-extract-env x env)
                                  a))
         (svex-alist-eval x (svdecomp-ev-symenv env a))))

Theorem: lookup-vars-subset-of-alist-vars

(defthm lookup-vars-subset-of-alist-vars
  (subsetp (svex-vars (cdr (svar-lookup k x)))
           (svex-alist-vars x)))

Theorem: eval-lookup-in-svdecomp-ev-symenv

(defthm eval-lookup-in-svdecomp-ev-symenv
 (equal
     (svex-eval (cdr (svar-lookup k x))
                (svdecomp-ev-symenv (envmap-entry-extract-env x env)
                                    a))
     (svex-eval (cdr (svar-lookup k x))
                (svdecomp-ev-symenv env a))))

Theorem: keys-of-envmap-entry-extract-env

(defthm keys-of-envmap-entry-extract-env
  (set-equiv (svar-alist-keys (envmap-entry-extract-env x env))
             (svex-alist-vars x)))

Theorem: ev-lookup-of-envmap-entry-extract-env

(defthm ev-lookup-of-envmap-entry-extract-env
 (implies
    (member (svar-fix k)
            (svex-alist-vars x))
    (4vec-equiv
         (svdecomp-ev
              (cdr (svar-lookup k (envmap-entry-extract-env x env)))
              a)
         (svex-env-lookup k (svdecomp-ev-symenv env a)))))

Theorem: envmap-entry-extract-env-of-svex-alist-fix-x

(defthm envmap-entry-extract-env-of-svex-alist-fix-x
  (equal (envmap-entry-extract-env (svex-alist-fix x)
                                   env)
         (envmap-entry-extract-env x env)))

Theorem: envmap-entry-extract-env-svex-alist-equiv-congruence-on-x

(defthm envmap-entry-extract-env-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (envmap-entry-extract-env x env)
                  (envmap-entry-extract-env x-equiv env)))
  :rule-classes :congruence)

Theorem: envmap-entry-extract-env-of-svar-alist-fix-env

(defthm envmap-entry-extract-env-of-svar-alist-fix-env
  (equal (envmap-entry-extract-env x (svar-alist-fix env))
         (envmap-entry-extract-env x env)))

Theorem: envmap-entry-extract-env-svar-alist-equiv-congruence-on-env

(defthm envmap-entry-extract-env-svar-alist-equiv-congruence-on-env
  (implies (svar-alist-equiv env env-equiv)
           (equal (envmap-entry-extract-env x env)
                  (envmap-entry-extract-env x env-equiv)))
  :rule-classes :congruence)