• 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
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
          • Svex-xeval
          • Svex-mono-eval
            • Svex-alist-mono-eval
            • Svex-mono-eval-monotonicity
            • Svexlist-mono-eval
            • Svex-fn/args-mono-eval
            • Svex-call-mono-eval
          • Svex-eval
          • Svex-apply
          • Svex-env
          • Svex-alist-eval
          • Svar-boolmasks-lookup
          • Svex-s4eval
          • Svexlist-unquote
          • Svex-alist-eval-for-symbolic
          • Svexlist-eval
          • Svexlist-quotesp
          • Svar-boolmasks
          • Svexlist-s4eval
          • Svexlist-eval-for-symbolic
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Evaluation

Svex-mono-eval

Evaluate an X-monotonic approximation of an svex

Signature

(svex-mono-eval x env) → val

Arguments

x — Expression to evaluate.
    Guard (svex-p x).

env — Guard (svex-env-p env).

Returns

val — Type (4vec-p val).

Theorem: return-type-of-svex-mono-eval.val

(defthm return-type-of-svex-mono-eval.val
  (b* ((?val (svex-mono-eval x env)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-call-mono-eval.val

(defthm return-type-of-svex-call-mono-eval.val
  (b* ((?val (svex-call-mono-eval x env)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-fn/args-mono-eval.val

(defthm return-type-of-svex-fn/args-mono-eval.val
  (b* ((?val (svex-fn/args-mono-eval fn args env)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-mono-eval.val

(defthm return-type-of-svexlist-mono-eval.val
  (b* ((?val (svexlist-mono-eval x env)))
    (4veclist-p val))
  :rule-classes :rewrite)

Theorem: svex-mono-eval-of-quote

(defthm svex-mono-eval-of-quote
  (implies (svex-case x :quote)
           (equal (svex-mono-eval x env)
                  (svex-quote->val x))))

Theorem: svex-mono-eval-of-svex-fix-x

(defthm svex-mono-eval-of-svex-fix-x
  (equal (svex-mono-eval (svex-fix x) env)
         (svex-mono-eval x env)))

Theorem: svex-mono-eval-of-svex-env-fix-env

(defthm svex-mono-eval-of-svex-env-fix-env
  (equal (svex-mono-eval x (svex-env-fix env))
         (svex-mono-eval x env)))

Theorem: svex-call-mono-eval-of-svex-fix-x

(defthm svex-call-mono-eval-of-svex-fix-x
  (equal (svex-call-mono-eval (svex-fix x) env)
         (svex-call-mono-eval x env)))

Theorem: svex-call-mono-eval-of-svex-env-fix-env

(defthm svex-call-mono-eval-of-svex-env-fix-env
  (equal (svex-call-mono-eval x (svex-env-fix env))
         (svex-call-mono-eval x env)))

Theorem: svex-fn/args-mono-eval-of-fnsym-fix-fn

(defthm svex-fn/args-mono-eval-of-fnsym-fix-fn
  (equal (svex-fn/args-mono-eval (fnsym-fix fn)
                                 args env)
         (svex-fn/args-mono-eval fn args env)))

Theorem: svex-fn/args-mono-eval-of-svexlist-fix-args

(defthm svex-fn/args-mono-eval-of-svexlist-fix-args
  (equal (svex-fn/args-mono-eval fn (svexlist-fix args)
                                 env)
         (svex-fn/args-mono-eval fn args env)))

Theorem: svex-fn/args-mono-eval-of-svex-env-fix-env

(defthm svex-fn/args-mono-eval-of-svex-env-fix-env
  (equal (svex-fn/args-mono-eval fn args (svex-env-fix env))
         (svex-fn/args-mono-eval fn args env)))

Theorem: svexlist-mono-eval-of-svexlist-fix-x

(defthm svexlist-mono-eval-of-svexlist-fix-x
  (equal (svexlist-mono-eval (svexlist-fix x)
                             env)
         (svexlist-mono-eval x env)))

Theorem: svexlist-mono-eval-of-svex-env-fix-env

(defthm svexlist-mono-eval-of-svex-env-fix-env
  (equal (svexlist-mono-eval x (svex-env-fix env))
         (svexlist-mono-eval x env)))

Theorem: svex-mono-eval-svex-equiv-congruence-on-x

(defthm svex-mono-eval-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-mono-eval x env)
                  (svex-mono-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svex-mono-eval-svex-env-equiv-congruence-on-env

(defthm svex-mono-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-mono-eval x env)
                  (svex-mono-eval x env-equiv)))
  :rule-classes :congruence)

Theorem: svex-call-mono-eval-svex-equiv-congruence-on-x

(defthm svex-call-mono-eval-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-call-mono-eval x env)
                  (svex-call-mono-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svex-call-mono-eval-svex-env-equiv-congruence-on-env

(defthm svex-call-mono-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-call-mono-eval x env)
                  (svex-call-mono-eval x env-equiv)))
  :rule-classes :congruence)

Theorem: svex-fn/args-mono-eval-fnsym-equiv-congruence-on-fn

(defthm svex-fn/args-mono-eval-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-fn/args-mono-eval fn args env)
                  (svex-fn/args-mono-eval fn-equiv args env)))
  :rule-classes :congruence)

Theorem: svex-fn/args-mono-eval-svexlist-equiv-congruence-on-args

(defthm svex-fn/args-mono-eval-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-fn/args-mono-eval fn args env)
                  (svex-fn/args-mono-eval fn args-equiv env)))
  :rule-classes :congruence)

Theorem: svex-fn/args-mono-eval-svex-env-equiv-congruence-on-env

(defthm svex-fn/args-mono-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svex-fn/args-mono-eval fn args env)
                  (svex-fn/args-mono-eval fn args env-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-mono-eval-svexlist-equiv-congruence-on-x

(defthm svexlist-mono-eval-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-mono-eval x env)
                  (svexlist-mono-eval x-equiv env)))
  :rule-classes :congruence)

Theorem: svexlist-mono-eval-svex-env-equiv-congruence-on-env

(defthm svexlist-mono-eval-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svexlist-mono-eval x env)
                  (svexlist-mono-eval x env-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-mono-eval-nil

(defthm svexlist-mono-eval-nil
  (equal (svexlist-mono-eval nil env)
         nil))

Theorem: car-of-svexlist-mono-eval

(defthm car-of-svexlist-mono-eval
  (4vec-equiv (car (svexlist-mono-eval x env))
              (svex-mono-eval (car x) env)))

Theorem: cdr-of-svexlist-mono-eval

(defthm cdr-of-svexlist-mono-eval
  (4veclist-equiv (cdr (svexlist-mono-eval x env))
                  (svexlist-mono-eval (cdr x) env)))

Theorem: len-of-svexlist-mono-eval

(defthm len-of-svexlist-mono-eval
  (equal (len (svexlist-mono-eval x env))
         (len x)))

Theorem: svexlist-mono-eval-of-append

(defthm svexlist-mono-eval-of-append
  (equal (svexlist-mono-eval (append a b) env)
         (append (svexlist-mono-eval a env)
                 (svexlist-mono-eval b env))))

Subtopics

Svex-alist-mono-eval

Maps svex-mono-eval over an svex alist.

Svex-mono-eval-monotonicity

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

Svexlist-mono-eval

Maps svex-mono-eval over an svex list.

Svex-fn/args-mono-eval

Svex-call-mono-eval