• 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

Alist-collect-compositions

Signature

(alist-collect-compositions x) → (mv err base-env envmap)

Arguments

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

Returns

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

envmap — Type (envmap-p envmap), given the guard.

Definitions and Theorems

Function: alist-collect-compositions

(defun alist-collect-compositions (x)
  (declare (xargs :guard (svdecomp-symenv-p x)))
  (let ((__function__ 'alist-collect-compositions))
    (declare (ignorable __function__))
    (b* ((x (fast-alist-free (fast-alist-clean (svar-alist-fix x))))
         ((mv err base-env envmap)
          (alist-collect-compositions-aux x nil nil)))
      (mv err
          base-env (fast-alist-clean envmap)))))

Theorem: svdecomp-symenv-p-of-alist-collect-compositions.base-env

(defthm svdecomp-symenv-p-of-alist-collect-compositions.base-env
  (implies (and (svdecomp-symenv-p x))
           (b* (((mv ?err ?base-env ?envmap)
                 (alist-collect-compositions x)))
             (svdecomp-symenv-p base-env)))
  :rule-classes :rewrite)

Theorem: envmap-p-of-alist-collect-compositions.envmap

(defthm envmap-p-of-alist-collect-compositions.envmap
  (implies (and (svdecomp-symenv-p x))
           (b* (((mv ?err ?base-env ?envmap)
                 (alist-collect-compositions x)))
             (envmap-p envmap)))
  :rule-classes :rewrite)

Theorem: alist-collect-compositions-envmap-lookup-eval

(defthm alist-collect-compositions-envmap-lookup-eval
 (b* (((mv ?err ?base-env ?envmap)
       (alist-collect-compositions x)))
  (implies
   (and (svar-lookup k (envmap->svex-alist envmap))
        (not err))
   (equal
    (svdecomp-ev (cdr (svar-lookup k (envmap-to-term-alist envmap)))
                 a)
    (svdecomp-ev (cdr (svar-lookup k x))
                 a)))))

Theorem: eval-lookup-in-envmap-entry-to-term-alist

(defthm eval-lookup-in-envmap-entry-to-term-alist
 (implies
  (svar-lookup k (svex-alist-fix svalist))
  (equal
   (svdecomp-ev
        (cdr (svar-lookup k
                          (envmap-entry-to-term-alist svalist env)))
        a)
   (svex-eval (cdr (svar-lookup k svalist))
              (svdecomp-ev env a)))))

Theorem: 4vec-p-lookup-in-envmap-to-term-alist

(defthm 4vec-p-lookup-in-envmap-to-term-alist
 (implies
  (svar-lookup k (envmap->svex-alist envmap))
  (4vec-p
    (svdecomp-ev (cdr (svar-lookup k (envmap-to-term-alist envmap)))
                 a))))

Theorem: alist-collect-compositions-envmap-implies-4vec-term

(defthm alist-collect-compositions-envmap-implies-4vec-term
  (b* (((mv ?err ?base-env ?envmap)
        (alist-collect-compositions x)))
    (implies (and (svar-lookup k (envmap->svex-alist envmap))
                  (not err))
             (svdecomp-4vec-termp (cdr (svar-lookup k x)))))
  :rule-classes :forward-chaining)

Theorem: alist-collect-compositions-base-env-lookup

(defthm alist-collect-compositions-base-env-lookup
 (b* (((mv ?err ?base-env ?envmap)
       (alist-collect-compositions x)))
  (implies
   (and
      (case-split (not (svar-lookup k (envmap->svex-alist envmap))))
      (not err))
   (equal (svar-lookup k base-env)
          (svar-lookup k x)))))

Theorem: alist-collect-compositions-of-svar-alist-fix-x

(defthm alist-collect-compositions-of-svar-alist-fix-x
  (equal (alist-collect-compositions (svar-alist-fix x))
         (alist-collect-compositions x)))

Theorem: alist-collect-compositions-svar-alist-equiv-congruence-on-x

(defthm alist-collect-compositions-svar-alist-equiv-congruence-on-x
  (implies (svar-alist-equiv x x-equiv)
           (equal (alist-collect-compositions x)
                  (alist-collect-compositions x-equiv)))
  :rule-classes :congruence)