• 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

Svar-lookup

Signature

(svar-lookup k x) → *

Arguments

k — Guard (svar-p k).

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

Definitions and Theorems

Function: svar-lookup

(defun svar-lookup (k x)
  (declare (xargs :guard (and (svar-p k) (svar-alist-p x))))
  (let ((__function__ 'svar-lookup))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (if (and (consp (car x))
                    (svar-p (caar x))
                    (equal (svar-fix k) (caar x)))
               (car x)
             (svar-lookup k (cdr x))))
         :exec (hons-get k x))))

Theorem: svar-lookup-of-cons

(defthm svar-lookup-of-cons
  (equal (svar-lookup k (cons a b))
         (if (and (consp a)
                  (svar-p (car a))
                  (svar-equiv (car a) k))
             a
           (svar-lookup k b))))

Theorem: svar-lookup-of-atom

(defthm svar-lookup-of-atom
  (implies (not (consp x))
           (equal (svar-lookup k x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svar-lookup-of-append

(defthm svar-lookup-of-append
  (equal (svar-lookup k (append a b))
         (or (svar-lookup k a)
             (svar-lookup k b))))

Theorem: svar-lookup-of-svex-alist-fix

(defthm svar-lookup-of-svex-alist-fix
  (iff (svar-lookup k (svex-alist-fix x))
       (svar-lookup k x)))

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

(defthm svar-lookup-of-svex-env-fix
  (iff (svar-lookup k (svex-env-fix x))
       (svar-lookup k x)))

Theorem: svar-lookup-of-true-list-fix

(defthm svar-lookup-of-true-list-fix
  (equal (svar-lookup k (true-list-fix x))
         (svar-lookup k x)))

Theorem: svar-lookup-of-svar-fix-k

(defthm svar-lookup-of-svar-fix-k
  (equal (svar-lookup (svar-fix k) x)
         (svar-lookup k x)))

Theorem: svar-lookup-svar-equiv-congruence-on-k

(defthm svar-lookup-svar-equiv-congruence-on-k
  (implies (svar-equiv k k-equiv)
           (equal (svar-lookup k x)
                  (svar-lookup k-equiv x)))
  :rule-classes :congruence)

Theorem: svar-lookup-of-svar-alist-fix-x

(defthm svar-lookup-of-svar-alist-fix-x
  (equal (svar-lookup k (svar-alist-fix x))
         (svar-lookup k x)))

Theorem: svar-lookup-svar-alist-equiv-congruence-on-x

(defthm svar-lookup-svar-alist-equiv-congruence-on-x
  (implies (svar-alist-equiv x x-equiv)
           (equal (svar-lookup k x)
                  (svar-lookup k x-equiv)))
  :rule-classes :congruence)