• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
          • Svex-compose-assigns-keys
          • Svex-compose
            • Svexlist-compose
          • Svex-compose*
          • Svex-compose-svstack
          • Svex-assigns-compose1
          • Svex-assigns-compose
          • Svex-compose-bit-sccs
          • Svex-compose-assigns
          • Svex-replace-var
        • Compile.lisp
        • Assign->netassigns
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svex-composition

Svex-compose

Compose an svex with a substitution alist. Variables not in the substitution are left in place.

Signature

(svex-compose x a) → xa

Arguments

x — Guard (svex-p x).

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

Returns

xa — x composed with a, unbound variables preserved.
    Type (svex-p xa).

Theorem: return-type-of-svex-compose.xa

(defthm return-type-of-svex-compose.xa
        (b* ((?xa (svex-compose x a)))
            (svex-p xa))
        :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose.xa

(defthm return-type-of-svexlist-compose.xa
        (b* ((?xa (svexlist-compose x a)))
            (svexlist-p xa))
        :rule-classes :rewrite)

Theorem: svex-compose-of-svex-fix-x

(defthm svex-compose-of-svex-fix-x
        (equal (svex-compose (svex-fix x) a)
               (svex-compose x a)))

Theorem: svex-compose-of-svex-alist-fix-a

(defthm svex-compose-of-svex-alist-fix-a
        (equal (svex-compose x (svex-alist-fix a))
               (svex-compose x a)))

Theorem: svexlist-compose-of-svexlist-fix-x

(defthm svexlist-compose-of-svexlist-fix-x
        (equal (svexlist-compose (svexlist-fix x) a)
               (svexlist-compose x a)))

Theorem: svexlist-compose-of-svex-alist-fix-a

(defthm svexlist-compose-of-svex-alist-fix-a
        (equal (svexlist-compose x (svex-alist-fix a))
               (svexlist-compose x a)))

Theorem: svex-compose-svex-equiv-congruence-on-x

(defthm svex-compose-svex-equiv-congruence-on-x
        (implies (svex-equiv x x-equiv)
                 (equal (svex-compose x a)
                        (svex-compose x-equiv a)))
        :rule-classes :congruence)

Theorem: svex-compose-svex-alist-equiv-congruence-on-a

(defthm svex-compose-svex-alist-equiv-congruence-on-a
        (implies (svex-alist-equiv a a-equiv)
                 (equal (svex-compose x a)
                        (svex-compose x a-equiv)))
        :rule-classes :congruence)

Theorem: svexlist-compose-svexlist-equiv-congruence-on-x

(defthm svexlist-compose-svexlist-equiv-congruence-on-x
        (implies (svexlist-equiv x x-equiv)
                 (equal (svexlist-compose x a)
                        (svexlist-compose x-equiv a)))
        :rule-classes :congruence)

Theorem: svexlist-compose-svex-alist-equiv-congruence-on-a

(defthm svexlist-compose-svex-alist-equiv-congruence-on-a
        (implies (svex-alist-equiv a a-equiv)
                 (equal (svexlist-compose x a)
                        (svexlist-compose x a-equiv)))
        :rule-classes :congruence)

Theorem: len-of-svexlist-compose

(defthm len-of-svexlist-compose
        (equal (len (svexlist-compose x a))
               (len x)))

Theorem: svex-eval-of-svex-compose

(defthm svex-eval-of-svex-compose
        (equal (svex-eval (svex-compose x a) env)
               (svex-eval x
                          (append (svex-alist-eval a env) env))))

Theorem: svexlist-eval-of-svexlist-compose

(defthm
     svexlist-eval-of-svexlist-compose
     (equal (svexlist-eval (svexlist-compose x a)
                           env)
            (svexlist-eval x
                           (append (svex-alist-eval a env) env))))

Theorem: vars-of-svex-compose

(defthm vars-of-svex-compose
        (implies (and (not (member v (svex-vars x)))
                      (not (member v (svex-alist-vars a))))
                 (not (member v (svex-vars (svex-compose x a))))))

Theorem: vars-of-svexlist-compose

(defthm
    vars-of-svexlist-compose
    (implies (and (not (member v (svexlist-vars x)))
                  (not (member v (svex-alist-vars a))))
             (not (member v
                          (svexlist-vars (svexlist-compose x a))))))

Theorem: vars-of-svex-compose-strong

(defthm vars-of-svex-compose-strong
        (implies (and (not (member v (svex-alist-vars a)))
                      (or (member v (svex-alist-keys a))
                          (not (member v (svex-vars x)))))
                 (not (member v (svex-vars (svex-compose x a))))))

Theorem: vars-of-svexlist-compose-strong

(defthm
    vars-of-svexlist-compose-strong
    (implies (and (not (member v (svex-alist-vars a)))
                  (or (member v (svex-alist-keys a))
                      (not (member v (svexlist-vars x)))))
             (not (member v
                          (svexlist-vars (svexlist-compose x a))))))

Function: svex-compose-memoize-condition

(defun
     svex-compose-memoize-condition (x a)
     (declare (ignorable x a)
              (xargs :guard (if (svex-p x) (svex-alist-p a) 'nil)))
     (eq (svex-kind x) :call))

Subtopics

Svexlist-compose