• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Decomp.lisp

Svdecomp-env-extract

Signature

(svdecomp-env-extract keys env) → res

Arguments

keys — Guard (svarlist-p keys).

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

Returns

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

Definitions and Theorems

Function: svdecomp-env-extract

(defun svdecomp-env-extract (keys env)
  (declare (xargs :guard (and (svarlist-p keys)
                              (svdecomp-symenv-p env))))
  (let ((__function__ 'svdecomp-env-extract))
    (declare (ignorable __function__))
    (if (atom keys)
        nil
      (cons (cons (svar-fix (car keys))
                  (let ((look (svar-lookup (car keys) env)))
                    (if look (cdr look) (quote-4vec-x))))
            (svdecomp-env-extract (cdr keys)
                                  env)))))

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

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

Theorem: svar-lookup-in-svdecomp-env-extract

(defthm svar-lookup-in-svdecomp-env-extract
  (equal (svar-lookup k (svdecomp-env-extract keys env))
         (and (member (svar-fix k)
                      (svarlist-fix keys))
              (or (svar-lookup k env)
                  (cons (svar-fix k) (quote-4vec-x))))))

Theorem: svex-env-lookup-in-svdecomp-ev-symenv

(defthm svex-env-lookup-in-svdecomp-ev-symenv
  (equal (svex-env-lookup k (svdecomp-ev-symenv env a))
         (let ((pair (svar-lookup k env)))
           (if pair (4vec-fix (svdecomp-ev (cdr pair) a))
             (4vec-x)))))

Theorem: eval-of-svdecomp-env-extract

(defthm eval-of-svdecomp-env-extract
  (svex-env-equiv
       (svdecomp-ev-symenv (svdecomp-env-extract keys env)
                           a)
       (svex-env-extract keys (svdecomp-ev-symenv env a))))

Theorem: keys-of-svdecomp-env-extract

(defthm keys-of-svdecomp-env-extract
  (equal (svar-alist-keys (svdecomp-env-extract keys env))
         (svarlist-fix keys)))

Theorem: svdecomp-env-extract-of-svarlist-fix-keys

(defthm svdecomp-env-extract-of-svarlist-fix-keys
  (equal (svdecomp-env-extract (svarlist-fix keys)
                               env)
         (svdecomp-env-extract keys env)))

Theorem: svdecomp-env-extract-svarlist-equiv-congruence-on-keys

(defthm svdecomp-env-extract-svarlist-equiv-congruence-on-keys
  (implies (svarlist-equiv keys keys-equiv)
           (equal (svdecomp-env-extract keys env)
                  (svdecomp-env-extract keys-equiv env)))
  :rule-classes :congruence)

Theorem: svdecomp-env-extract-of-svar-alist-fix-env

(defthm svdecomp-env-extract-of-svar-alist-fix-env
  (equal (svdecomp-env-extract keys (svar-alist-fix env))
         (svdecomp-env-extract keys env)))

Theorem: svdecomp-env-extract-svar-alist-equiv-congruence-on-env

(defthm svdecomp-env-extract-svar-alist-equiv-congruence-on-env
  (implies (svar-alist-equiv env env-equiv)
           (equal (svdecomp-env-extract keys env)
                  (svdecomp-env-extract keys env-equiv)))
  :rule-classes :congruence)