• 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
          • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-composition

Svex-compose-assigns-keys

Compose together svex assignments (using svex-compose-dfs) for the listed keys.

Signature

(svex-compose-assigns-keys keys assigns updates memo) 
  → 
(mv updates1 memo1)

Arguments

keys — List of remaining target variables.
    Guard (svarlist-p keys).

assigns — Original list of assignments.
    Guard (svex-alist-p assigns).

updates — Accumulator of composed update functions.
    Guard (svex-alist-p updates).

memo — accumulated memo table.
    Guard (svex-svex-memo-p memo).

Returns

updates1 — Type (svex-alist-p updates1).

memo1 — Type (svex-svex-memo-p memo1).

Definitions and Theorems

Function: svex-compose-assigns-keys

(defun svex-compose-assigns-keys (keys assigns updates memo)
  (declare (xargs :guard (and (svarlist-p keys)
                              (svex-alist-p assigns)
                              (svex-alist-p updates)
                              (svex-svex-memo-p memo))))
  (let ((__function__ 'svex-compose-assigns-keys))
    (declare (ignorable __function__))
    (b* (((when (atom keys))
          (mv (mbe :logic (svex-alist-fix updates)
                   :exec updates)
              (svex-svex-memo-fix memo)))
         ((mv & updates memo)
          (svex-compose-dfs (svex-var (car keys))
                            assigns updates memo nil)))
      (svex-compose-assigns-keys (cdr keys)
                                 assigns updates memo))))

Theorem: svex-alist-p-of-svex-compose-assigns-keys.updates1

(defthm svex-alist-p-of-svex-compose-assigns-keys.updates1
  (b* (((mv ?updates1 ?memo1)
        (svex-compose-assigns-keys keys assigns updates memo)))
    (svex-alist-p updates1))
  :rule-classes :rewrite)

Theorem: svex-svex-memo-p-of-svex-compose-assigns-keys.memo1

(defthm svex-svex-memo-p-of-svex-compose-assigns-keys.memo1
  (b* (((mv ?updates1 ?memo1)
        (svex-compose-assigns-keys keys assigns updates memo)))
    (svex-svex-memo-p memo1))
  :rule-classes :rewrite)

Theorem: svex-compose-assigns-keys-of-svarlist-fix-keys

(defthm svex-compose-assigns-keys-of-svarlist-fix-keys
  (equal (svex-compose-assigns-keys (svarlist-fix keys)
                                    assigns updates memo)
         (svex-compose-assigns-keys keys assigns updates memo)))

Theorem: svex-compose-assigns-keys-svarlist-equiv-congruence-on-keys

(defthm svex-compose-assigns-keys-svarlist-equiv-congruence-on-keys
 (implies
  (svarlist-equiv keys keys-equiv)
  (equal
       (svex-compose-assigns-keys keys assigns updates memo)
       (svex-compose-assigns-keys keys-equiv assigns updates memo)))
 :rule-classes :congruence)

Theorem: svex-compose-assigns-keys-of-svex-alist-fix-assigns

(defthm svex-compose-assigns-keys-of-svex-alist-fix-assigns
  (equal (svex-compose-assigns-keys keys (svex-alist-fix assigns)
                                    updates memo)
         (svex-compose-assigns-keys keys assigns updates memo)))

Theorem: svex-compose-assigns-keys-svex-alist-equiv-congruence-on-assigns

(defthm
   svex-compose-assigns-keys-svex-alist-equiv-congruence-on-assigns
 (implies
  (svex-alist-equiv assigns assigns-equiv)
  (equal
       (svex-compose-assigns-keys keys assigns updates memo)
       (svex-compose-assigns-keys keys assigns-equiv updates memo)))
 :rule-classes :congruence)

Theorem: svex-compose-assigns-keys-of-svex-alist-fix-updates

(defthm svex-compose-assigns-keys-of-svex-alist-fix-updates
 (equal
    (svex-compose-assigns-keys keys assigns (svex-alist-fix updates)
                               memo)
    (svex-compose-assigns-keys keys assigns updates memo)))

Theorem: svex-compose-assigns-keys-svex-alist-equiv-congruence-on-updates

(defthm
   svex-compose-assigns-keys-svex-alist-equiv-congruence-on-updates
 (implies
  (svex-alist-equiv updates updates-equiv)
  (equal
       (svex-compose-assigns-keys keys assigns updates memo)
       (svex-compose-assigns-keys keys assigns updates-equiv memo)))
 :rule-classes :congruence)

Theorem: svex-compose-assigns-keys-of-svex-svex-memo-fix-memo

(defthm svex-compose-assigns-keys-of-svex-svex-memo-fix-memo
  (equal
       (svex-compose-assigns-keys keys assigns
                                  updates (svex-svex-memo-fix memo))
       (svex-compose-assigns-keys keys assigns updates memo)))

Theorem: svex-compose-assigns-keys-svex-svex-memo-equiv-congruence-on-memo

(defthm
  svex-compose-assigns-keys-svex-svex-memo-equiv-congruence-on-memo
 (implies
  (svex-svex-memo-equiv memo memo-equiv)
  (equal
       (svex-compose-assigns-keys keys assigns updates memo)
       (svex-compose-assigns-keys keys assigns updates memo-equiv)))
 :rule-classes :congruence)