• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-mono-eval-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-<<=

4vec-monotonicity

Monotonicity properties for the basic svex functions.

Definitions and Theorems

Theorem: 4vec-fix-monotonic

(defthm 4vec-fix-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-fix x) (4vec-fix x1))))

Theorem: 3vec-fix-monotonic

(defthm 3vec-fix-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (3vec-fix x) (3vec-fix x1))))

Theorem: 4vec-bitnot-monotonic

(defthm 4vec-bitnot-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-bitnot x)
                     (4vec-bitnot x1))))

Theorem: 4vec-onset-monotonic

(defthm 4vec-onset-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-onset x)
                     (4vec-onset x1))))

Theorem: 4vec-offset-monotonic

(defthm 4vec-offset-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-offset x)
                     (4vec-offset x1))))

Theorem: 4vec-bitand-monotonic

(defthm 4vec-bitand-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-bitand x y)
                     (4vec-bitand x1 y1))))

Theorem: 4vec-bitor-monotonic

(defthm 4vec-bitor-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-bitor x y)
                     (4vec-bitor x1 y1))))

Theorem: 4vec-bitxor-monotonic

(defthm 4vec-bitxor-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-bitxor x y)
                     (4vec-bitxor x1 y1))))

Theorem: 4vec-res-monotonic

(defthm 4vec-res-monotonic
  (implies (and (4vec-<<= a a1) (4vec-<<= b b1))
           (4vec-<<= (4vec-res a b)
                     (4vec-res a1 b1))))

Theorem: 4vec-resand-monotonic

(defthm 4vec-resand-monotonic
  (implies (and (4vec-<<= a a1) (4vec-<<= b b1))
           (4vec-<<= (4vec-resand a b)
                     (4vec-resand a1 b1))))

Theorem: 4vec-resor-monotonic

(defthm 4vec-resor-monotonic
  (implies (and (4vec-<<= a a1) (4vec-<<= b b1))
           (4vec-<<= (4vec-resor a b)
                     (4vec-resor a1 b1))))

Theorem: 4vec-override-monotonic

(defthm 4vec-override-monotonic
  (implies (and (4vec-<<= stronger stronger1)
                (4vec-<<= weaker weaker1))
           (4vec-<<= (4vec-override stronger weaker)
                     (4vec-override stronger1 weaker1))))

Theorem: 4vec-reduction-and-monotonic

(defthm 4vec-reduction-and-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-reduction-and x)
                     (4vec-reduction-and x1))))

Theorem: 4vec-reduction-or-monotonic

(defthm 4vec-reduction-or-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-reduction-or x)
                     (4vec-reduction-or x1))))

Theorem: 4vec-zero-ext-monotonic

(defthm 4vec-zero-ext-monotonic
  (implies (and (4vec-<<= n n1) (4vec-<<= x x1))
           (4vec-<<= (4vec-zero-ext n x)
                     (4vec-zero-ext n1 x1))))

Theorem: 4vec-sign-ext-monotonic

(defthm 4vec-sign-ext-monotonic
  (implies (and (4vec-<<= n n1) (4vec-<<= x x1))
           (4vec-<<= (4vec-sign-ext n x)
                     (4vec-sign-ext n1 x1))))

Theorem: 2vecx-fix-monotonic

(defthm 2vecx-fix-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (2vecx-fix x)
                     (2vecx-fix x1))))

Theorem: 2vecnatx-fix-monotonic

(defthm 2vecnatx-fix-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (2vecnatx-fix x)
                     (2vecnatx-fix x1))))

Theorem: 4vec-concat-monotonic

(defthm 4vec-concat-monotonic
  (implies (and (4vec-<<= width width1)
                (4vec-<<= low low1)
                (4vec-<<= high high1))
           (4vec-<<= (4vec-concat width low high)
                     (4vec-concat width1 low1 high1))))

Theorem: 4vec-rsh-monotonic

(defthm 4vec-rsh-monotonic
  (implies (and (4vec-<<= amt amt1)
                (4vec-<<= src src1))
           (4vec-<<= (4vec-rsh amt src)
                     (4vec-rsh amt1 src1))))

Theorem: 4vec-lsh-monotonic

(defthm 4vec-lsh-monotonic
  (implies (and (4vec-<<= amt amt1)
                (4vec-<<= src src1))
           (4vec-<<= (4vec-lsh amt src)
                     (4vec-lsh amt1 src1))))

Theorem: 4vec-parity-monotonic

(defthm 4vec-parity-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-parity x)
                     (4vec-parity x1))))

Theorem: 4vec-plus-monotonic

(defthm 4vec-plus-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-plus x y)
                     (4vec-plus x1 y1))))

Theorem: 4vec-minus-monotonic

(defthm 4vec-minus-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-minus x y)
                     (4vec-minus x1 y1))))

Theorem: 4vec-uminus-monotonic

(defthm 4vec-uminus-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-uminus x)
                     (4vec-uminus x1))))

Theorem: 4vec-xdet-monotonic

(defthm 4vec-xdet-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-xdet x)
                     (4vec-xdet x1))))

Theorem: 4vec-countones-monotonic

(defthm 4vec-countones-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-countones x)
                     (4vec-countones x1))))

Theorem: 4vec-onehot-monotonic

(defthm 4vec-onehot-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-onehot x)
                     (4vec-onehot x1))))

Theorem: 4vec-onehot0-monotonic

(defthm 4vec-onehot0-monotonic
  (implies (and (4vec-<<= x x1))
           (4vec-<<= (4vec-onehot0 x)
                     (4vec-onehot0 x1))))

Theorem: 4vec-times-monotonic

(defthm 4vec-times-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-times x y)
                     (4vec-times x1 y1))))

Theorem: 4vec-quotient-monotonic

(defthm 4vec-quotient-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-quotient x y)
                     (4vec-quotient x1 y1))))

Theorem: 4vec-remainder-monotonic

(defthm 4vec-remainder-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-remainder x y)
                     (4vec-remainder x1 y1))))

Theorem: 4vec-<-monotonic

(defthm 4vec-<-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-< x y) (4vec-< x1 y1))))

Theorem: 4vec-==-monotonic

(defthm 4vec-==-monotonic
  (implies (and (4vec-<<= x x1) (4vec-<<= y y1))
           (4vec-<<= (4vec-== x y)
                     (4vec-== x1 y1))))

Theorem: 4vec-?-monotonic

(defthm 4vec-?-monotonic
  (implies (and (4vec-<<= test test1)
                (4vec-<<= then then1)
                (4vec-<<= else else1))
           (4vec-<<= (4vec-? test then else)
                     (4vec-? test1 then1 else1))))

Theorem: 4vec-bit?-monotonic

(defthm 4vec-bit?-monotonic
  (implies (and (4vec-<<= tests tests1)
                (4vec-<<= thens thens1)
                (4vec-<<= elses elses1))
           (4vec-<<= (4vec-bit? tests thens elses)
                     (4vec-bit? tests1 thens1 elses1))))

Theorem: 4vec-?*-monotonic

(defthm 4vec-?*-monotonic
  (implies (and (4vec-<<= test test1)
                (4vec-<<= then then1)
                (4vec-<<= else else1))
           (4vec-<<= (4vec-?* test then else)
                     (4vec-?* test1 then1 else1))))

Theorem: 4vec-bit-extract-monotonic

(defthm 4vec-bit-extract-monotonic
  (implies (and (4vec-<<= n n1) (4vec-<<= x x1))
           (4vec-<<= (4vec-bit-extract n x)
                     (4vec-bit-extract n1 x1))))

Theorem: 4vec-rev-blocks-monotonic

(defthm 4vec-rev-blocks-monotonic
  (implies (and (4vec-<<= nbits nbits1)
                (4vec-<<= blocksz blocksz1)
                (4vec-<<= x x1))
           (4vec-<<= (4vec-rev-blocks nbits blocksz x)
                     (4vec-rev-blocks nbits1 blocksz1 x1))))

Theorem: 4vec-wildeq-safe-monotonic

(defthm 4vec-wildeq-safe-monotonic
  (implies (and (4vec-<<= a a1) (4vec-<<= b b1))
           (4vec-<<= (4vec-wildeq-safe a b)
                     (4vec-wildeq-safe a1 b1))))

Theorem: 4vec-symwildeq-monotonic

(defthm 4vec-symwildeq-monotonic
  (implies (and (4vec-<<= a a1) (4vec-<<= b b1))
           (4vec-<<= (4vec-symwildeq a b)
                     (4vec-symwildeq a1 b1))))

Theorem: 4vec-clog2-monotonic

(defthm 4vec-clog2-monotonic
  (implies (and (4vec-<<= a a1))
           (4vec-<<= (4vec-clog2 a)
                     (4vec-clog2 a1))))

Theorem: 4vec-pow-monotonic

(defthm 4vec-pow-monotonic
  (implies (and (4vec-<<= base base1)
                (4vec-<<= exp exp1))
           (4vec-<<= (4vec-pow base exp)
                     (4vec-pow base1 exp1))))

Theorem: 4vec-part-select-monotonic

(defthm 4vec-part-select-monotonic
  (implies (and (4vec-<<= lsb lsb1)
                (4vec-<<= width width1)
                (4vec-<<= in in1))
           (4vec-<<= (4vec-part-select lsb width in)
                     (4vec-part-select lsb1 width1 in1))))

Theorem: 4vec-part-install-monotonic

(defthm 4vec-part-install-monotonic
  (implies (and (4vec-<<= lsb lsb1)
                (4vec-<<= width width1)
                (4vec-<<= in in1)
                (4vec-<<= val val1))
           (4vec-<<= (4vec-part-install lsb width in val)
                     (4vec-part-install lsb1 width1 in1 val1))))

Theorem: 4vec-==-<<=-===

(defthm 4vec-==-<<=-===
  (4vec-<<= (4vec-== a b) (4vec-=== a b)))

Theorem: 4vec-==-<<=-===-ext2

(defthm 4vec-==-<<=-===-ext2
  (implies (4vec-<<= x (4vec-== a b))
           (4vec-<<= x (4vec-=== a b))))

Theorem: 4vec-==-<<=-===-ext1

(defthm 4vec-==-<<=-===-ext1
  (implies (4vec-<<= (4vec-=== a b) x)
           (4vec-<<= (4vec-== a b) x)))

Theorem: 4vec-===*-<<=-===

(defthm 4vec-===*-<<=-===
  (4vec-<<= (4vec-===* a b)
            (4vec-=== a b)))

Theorem: 4vec-===*-<<=-===-ext2

(defthm 4vec-===*-<<=-===-ext2
  (implies (4vec-<<= x (4vec-===* a b))
           (4vec-<<= x (4vec-=== a b))))

Theorem: 4vec-===*-<<=-===-ext1

(defthm 4vec-===*-<<=-===-ext1
  (implies (4vec-<<= (4vec-=== a b) x)
           (4vec-<<= (4vec-===* a b) x)))

Theorem: 4vec-===*-<<=-===-rev

(defthm 4vec-===*-<<=-===-rev
  (4vec-<<= (4vec-===* a b)
            (4vec-=== b a)))

Theorem: 4vec-==-<<=-===*

(defthm 4vec-==-<<=-===*
  (4vec-<<= (4vec-== a b)
            (4vec-===* a b)))

Theorem: 4vec-===*-monotonic-when-second-const

(defthm 4vec-===*-monotonic-when-second-const
  (implies (4vec-<<= a b)
           (4vec-<<= (4vec-===* a c)
                     (4vec-===* b c))))

Theorem: 4vec-wildeq-safe-<<=-wildeq

(defthm 4vec-wildeq-safe-<<=-wildeq
  (4vec-<<= (4vec-wildeq-safe a b)
            (4vec-wildeq a b)))

Theorem: 4vec-wildeq-safe-<<=-wildeq-ext2

(defthm 4vec-wildeq-safe-<<=-wildeq-ext2
  (implies (4vec-<<= x (4vec-wildeq-safe a b))
           (4vec-<<= x (4vec-wildeq a b))))

Theorem: 4vec-wildeq-monotonic-when-second-const

(defthm 4vec-wildeq-monotonic-when-second-const
  (implies (4vec-<<= a b)
           (4vec-<<= (4vec-wildeq a c)
                     (4vec-wildeq b c))))

Theorem: 4vec-bit?!-monotonic-on-nontest-args

(defthm 4vec-bit?!-monotonic-on-nontest-args
  (implies (and (4vec-<<= then1 then2)
                (4vec-<<= else1 else2))
           (4vec-<<= (4vec-bit?! test then1 else1)
                     (4vec-bit?! test then2 else2))))

Theorem: 4vec-bit?-<<=-bit?!

(defthm 4vec-bit?-<<=-bit?!
  (4vec-<<= (4vec-bit? test then else)
            (4vec-bit?! test then else)))

Theorem: 4vec-bit?-<<=-bit?!-ext2

(defthm 4vec-bit?-<<=-bit?!-ext2
  (implies (4vec-<<= x (4vec-bit? test then else))
           (4vec-<<= x (4vec-bit?! test then else))))

Theorem: 4vec-?!-monotonic-on-nontest-args

(defthm 4vec-?!-monotonic-on-nontest-args
  (implies (and (4vec-<<= then1 then2)
                (4vec-<<= else1 else2))
           (4vec-<<= (4vec-?! test then1 else1)
                     (4vec-?! test then2 else2))))

Theorem: 4vec-?*-<<=-?!

(defthm 4vec-?*-<<=-?!
  (4vec-<<= (4vec-?* test then else)
            (4vec-?! test then else)))

Theorem: 4vec-?*-<<=-?!-ext2

(defthm 4vec-?*-<<=-?!-ext2
  (implies (4vec-<<= x (4vec-?* test then else))
           (4vec-<<= x (4vec-?! test then else))))

Subtopics

Svex-mono-eval-monotonicity

(svex-mono-eval x) always approximates (svex-eval x env), for any environment.