• 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
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
          • 4vec
          • 4vec-<<=
            • 4vec-monotonicity
            • Svex-monotonify
            • Svex-alist-partial-monotonic
            • Svex-alist-monotonic-on-vars
            • 4veclist-<<=
            • Svexlist-partial-monotonic
            • Svex-partial-monotonic
            • Svex-alist-<<=
            • Svex-alist-ovmonotonic
            • Svexlist-<<=
            • Svex-env-<<=
            • Svex-alist-ovcongruent
            • Svex-alist-monotonic-p
            • Svexlist-monotonic-on-vars
            • Svex-monotonic-on-vars
            • Svex-<<=
            • Svexlist-monotonic-p
            • 4vec-xfree-p
            • Svex-apply-monotonocity
            • Svexlist-ovmonotonic
            • Svexlist-ovcongruent
            • Svex-ovmonotonic
            • Svex-monotonic-p
          • 3vec
          • 2vec
          • 2vecx
          • 2vecnatx
          • 4vec-x
          • 4vec-1x
          • 4vec-1z
          • 4vec-z
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 4vec-<<=

Svexlist-partial-monotonic

Definitions and Theorems

Theorem: svexlist-partial-monotonic-necc

(defthm svexlist-partial-monotonic-necc
 (implies
     (svexlist-partial-monotonic param-keys x)
     (implies (and (svex-alist-constantp setting)
                   (subsetp (svarlist-fix param-keys)
                            (svex-alist-keys setting)))
              (svexlist-monotonic-p (svexlist-compose x setting)))))

Theorem: eval-when-svexlist-partial-monotonic

(defthm eval-when-svexlist-partial-monotonic
  (implies (and (svexlist-partial-monotonic param-keys x)
                (equal (svex-env-extract param-keys env1)
                       (svex-env-extract param-keys env2))
                (svex-env-<<= env1 env2))
           (4veclist-<<= (svexlist-eval x env1)
                         (svexlist-eval x env2))))

Function: svexlist-partial-monotonic-eval-witness

(defun svexlist-partial-monotonic-eval-witness (param-keys x)
  (b* ((setting (svexlist-partial-monotonic-witness param-keys x))
       (compose (svexlist-compose x setting))
       ((mv env1 env2)
        (svexlist-monotonic-p-witness compose))
       (setting-ev (svex-alist-eval setting nil)))
    (mv (append setting-ev env1)
        (append setting-ev env2))))

Theorem: svexlist-partial-monotonic-by-eval

(defthm svexlist-partial-monotonic-by-eval
 (equal
      (svexlist-partial-monotonic param-keys x)
      (b* (((mv env1 env2)
            (svexlist-partial-monotonic-eval-witness param-keys x)))
        (or (not (equal (svex-env-extract param-keys env1)
                        (svex-env-extract param-keys env2)))
            (not (svex-env-<<= env1 env2))
            (4veclist-<<= (svexlist-eval x env1)
                          (svexlist-eval x env2)))))
 :rule-classes ((:definition :install-body nil)))

Theorem: svexlist-partial-monotonic-of-svarlist-fix-param-keys

(defthm svexlist-partial-monotonic-of-svarlist-fix-param-keys
  (equal (svexlist-partial-monotonic (svarlist-fix param-keys)
                                     x)
         (svexlist-partial-monotonic param-keys x)))

Theorem: svexlist-partial-monotonic-svarlist-equiv-congruence-on-param-keys

(defthm
 svexlist-partial-monotonic-svarlist-equiv-congruence-on-param-keys
 (implies (svarlist-equiv param-keys param-keys-equiv)
          (equal (svexlist-partial-monotonic param-keys x)
                 (svexlist-partial-monotonic param-keys-equiv x)))
 :rule-classes :congruence)

Theorem: set-equiv-implies-equal-svexlist-partial-monotonic-1

(defthm set-equiv-implies-equal-svexlist-partial-monotonic-1
  (implies (set-equiv param-keys param-keys-equiv)
           (equal (svexlist-partial-monotonic param-keys x)
                  (svexlist-partial-monotonic param-keys-equiv x)))
  :rule-classes (:congruence))

Theorem: svexlist-eval-equiv-implies-svexlist-eval-equiv-svexlist-compose-1

(defthm
 svexlist-eval-equiv-implies-svexlist-eval-equiv-svexlist-compose-1
 (implies (svexlist-eval-equiv x x-equiv)
          (svexlist-eval-equiv (svexlist-compose x a)
                               (svexlist-compose x-equiv a)))
 :rule-classes (:congruence))

Theorem: svexlist-eval-equiv-implies-equal-svexlist-partial-monotonic-2

(defthm
     svexlist-eval-equiv-implies-equal-svexlist-partial-monotonic-2
  (implies (svexlist-eval-equiv x x-equiv)
           (equal (svexlist-partial-monotonic param-keys x)
                  (svexlist-partial-monotonic param-keys x-equiv)))
  :rule-classes (:congruence))