• 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
      • Svex-compose-dfs
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
          • Svex-compose-assigns-keys
          • Svex-compose*
          • Svex-compose
          • Svex-compose-svstack
            • Svexlist-compose-svstack
          • Svex-assigns-compose1
          • Svex-assigns-compose
          • Svex-compose-bit-sccs
          • Svex-compose-assigns
          • Svex-replace-var
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-composition

Svex-compose-svstack

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

Signature

(svex-compose-svstack x a) → xa

Arguments

x — Guard (svex-p x).

a — Guard (svstack-p a).

Returns

xa — Type (equal xa (svex-compose-rw x (make-svex-substconfig :alist (svstack-to-svex-alist a) :simp 5))) .

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

(defthm return-type-of-svex-compose-svstack.xa
 (b* ((?xa (svex-compose-svstack x a)))
   (equal
        xa
        (svex-compose-rw
             x
             (make-svex-substconfig :alist (svstack-to-svex-alist a)
                                    :simp 5))))
 :rule-classes :rewrite)

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

(defthm return-type-of-svexlist-compose-svstack.xa
 (b* ((?xa (svexlist-compose-svstack x a)))
   (equal
        xa
        (svexlist-compose-rw
             x
             (make-svex-substconfig :alist (svstack-to-svex-alist a)
                                    :simp 5))))
 :rule-classes :rewrite)

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

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

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

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

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

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

Theorem: svexlist-compose-svstack-of-svstack-fix-a

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

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

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

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

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

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

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

Theorem: svexlist-compose-svstack-svstack-equiv-congruence-on-a

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

Function: svex-compose-svstack-memoize-condition

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

Subtopics

Svexlist-compose-svstack