• 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-eval
            • Svex-eval-basics
          • 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

• Svex-eval

Svex-eval-basics

Very basic lemmas about svex-eval.

Definitions and Theorems

Congruence rules

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Svex-eval of constants/constructors

Theorem: svex-eval-of-quoted

(defthm svex-eval-of-quoted
 (implies
  (syntaxp (quotep x))
  (equal
   (svex-eval x env)
   ((lambda (__function__ env x)
     ((lambda (acl2::x.kind env x)
       (if (eql acl2::x.kind ':quote)
           ((lambda (x.val) x.val)
            (svex-quote->val$inline x))
        (if (eql acl2::x.kind ':var)
            ((lambda (x.name env)
               (svex-env-fastlookup x.name env))
             (svex-var->name$inline x)
             env)
         ((lambda (x.fn env x)
           ((lambda (x.args env x.fn)
             (return-last
              'acl2::mbe1-raw
              (if
               ((lambda (x acl2::l)
                 (return-last
                  'acl2::mbe1-raw
                  (acl2::member-eql-exec x acl2::l)
                  (return-last
                       'progn
                       (acl2::member-eql-exec$guard-check x acl2::l)
                       (member-equal x acl2::l))))
                x.fn '(? ?*))
               (if
                (eql (len x.args) '3)
                ((lambda (test x.fn env x.args)
                  ((lambda (test.upper x.args env x.fn test)
                    ((lambda
                       (test.lower test x.fn env x.args test.upper)
                      (if (eql test.upper '0)
                          (svex-eval (car (cdr (cdr x.args))) env)
                       (if (not (eql test.lower '0))
                           (svex-eval (car (cdr x.args)) env)
                        ((lambda (then x.fn test env x.args)
                           ((lambda (else then test x.fn)
                              (if (eql x.fn '?)
                                  (4vec-? test then else)
                                (if (eql x.fn '?*)
                                    (4vec-?* test then else)
                                  'nil)))
                            (svex-eval (car (cdr (cdr x.args))) env)
                            then test x.fn))
                         (svex-eval (car (cdr x.args)) env)
                         x.fn test env x.args))))
                     (4vec->lower$inline test)
                     test x.fn env x.args test.upper))
                   (4vec->upper$inline test)
                   x.args env x.fn test))
                 (3vec-fix (svex-eval (car x.args) env))
                 x.fn env x.args)
                (svex-apply x.fn (svexlist-eval x.args env)))
               (if
                (eql x.fn '?!)
                (if
                 (eql (len x.args) '3)
                 ((lambda (test x.args env)
                   ((lambda (test.upper env x.args test)
                     ((lambda (test.lower x.args env test.upper)
                       ((lambda (testvec env x.args)
                          (if
                            (eql testvec '0)
                            (svex-eval (car (cdr (cdr x.args))) env)
                            (svex-eval (car (cdr x.args)) env)))
                        (binary-logand test.upper test.lower)
                        env x.args))
                      (4vec->lower$inline test)
                      x.args env test.upper))
                    (4vec->upper$inline test)
                    env x.args test))
                  (svex-eval (car x.args) env)
                  x.args env)
                 (svex-apply x.fn (svexlist-eval x.args env)))
                (if
                 (eql x.fn 'bit?)
                 (if
                  (eql (len x.args) '3)
                  ((lambda (test env x.args)
                    (if (eql test '0)
                        (svex-eval (car (cdr (cdr x.args))) env)
                      (if (eql test '-1)
                          (svex-eval (car (cdr x.args)) env)
                        (4vec-bit?
                             test (svex-eval (car (cdr x.args)) env)
                             (svex-eval (car (cdr (cdr x.args)))
                                        env)))))
                   (svex-eval (car x.args) env)
                   env x.args)
                  (svex-apply x.fn (svexlist-eval x.args env)))
                 (if
                  (eql x.fn 'bit?!)
                  (if
                   (eql (len x.args) '3)
                   ((lambda (test env x.args)
                     (if (eql test '-1)
                         (svex-eval (car (cdr x.args)) env)
                      (if (eql test '0)
                          (svex-eval (car (cdr (cdr x.args))) env)
                        (4vec-bitmux
                             test (svex-eval (car (cdr x.args)) env)
                             (svex-eval (car (cdr (cdr x.args)))
                                        env)))))
                    (4vec-1mask (svex-eval (car x.args) env))
                    env x.args)
                   (svex-apply x.fn (svexlist-eval x.args env)))
                  (if
                   (eql x.fn 'bitand)
                   (if
                    (eql (len x.args) '2)
                    ((lambda (test env x.args)
                       (if (eql test '0)
                           '0
                         (4vec-bitand
                              test
                              (svex-eval (car (cdr x.args)) env))))
                     (svex-eval (car x.args) env)
                     env x.args)
                    (svex-apply x.fn (svexlist-eval x.args env)))
                   (if
                    (eql x.fn 'bitor)
                    (if
                     (eql (len x.args) '2)
                     ((lambda (test env x.args)
                        (if (eql test '-1)
                            '-1
                          (4vec-bitor
                               test
                               (svex-eval (car (cdr x.args)) env))))
                      (svex-eval (car x.args) env)
                      env x.args)
                     (svex-apply x.fn (svexlist-eval x.args env)))
                    (svex-apply
                         x.fn (svexlist-eval x.args env))))))))
              (svex-apply x.fn (svexlist-eval x.args env))))
            (svex-call->args$inline x)
            env x.fn))
          (svex-call->fn$inline x)
          env x))))
      (svex-kind$inline x)
      env x))
    'svex-eval
    env x))))

Theorem: svex-eval-of-svex-call

(defthm svex-eval-of-svex-call
  (equal (svex-eval (svex-call fn args) env)
         (svex-apply fn (svexlist-eval args env))))

Theorem: svex-eval-when-fncall

(defthm svex-eval-when-fncall
  (implies (equal (svex-kind x) :call)
           (equal (svex-eval x env)
                  (svex-apply (svex-call->fn x)
                              (svexlist-eval (svex-call->args x)
                                             env)))))

Theorem: svex-eval-when-quote

(defthm svex-eval-when-quote
  (implies (eq (svex-kind x) :quote)
           (equal (svex-eval x env)
                  (svex-quote->val x))))