• 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-apply
          • Svex-env
            • Svex-env-p
            • Svex-env-reduce
            • Svex-envs-similar
            • Svex-envs-equivalent
            • Svex-env-fix
            • Svex-env-extract
            • Svex-env-lookup
            • Svex-env-acons
            • Svex-env-<<=
            • Svarlist-x-subst
            • Svex-env-equiv
            • Svex-env-boundp
            • Svarlist-x-env
            • Svex-env-fastlookup
          • 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-env

Svex-envs-equivalent

(svex-envs-equivalent x y) is a stronger form of alist equivalence for svex-envs than svex-envs-similar: environments are similar if they bind all variables to the same values, in the sense of svex-env-lookup, and they bind the same variables.

This is a universal equivalence, introduced using def-universal-equiv.

Function: svex-envs-equivalent

(defun svex-envs-equivalent (x y)
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'svex-envs-equivalent
                                     (list x y))
          (let ((k (svex-envs-equivalent-witness x y)))
            (and (equal (svex-env-lookup k x)
                        (svex-env-lookup k y))
                 (iff (svex-env-boundp k x)
                      (svex-env-boundp k y))))))

Definitions and Theorems

Theorem: svex-envs-equivalent-necc

(defthm svex-envs-equivalent-necc
  (implies (not (and (equal (svex-env-lookup k x)
                            (svex-env-lookup k y))
                     (iff (svex-env-boundp k x)
                          (svex-env-boundp k y))))
           (not (svex-envs-equivalent x y))))

Theorem: svex-envs-equivalent-witnessing-witness-rule-correct

(defthm svex-envs-equivalent-witnessing-witness-rule-correct
  (implies (not ((lambda (k y x)
                   (not (if (equal (svex-env-lookup k x)
                                   (svex-env-lookup k y))
                            (iff (svex-env-boundp k x)
                                 (svex-env-boundp k y))
                          'nil)))
                 (svex-envs-equivalent-witness x y)
                 y x))
           (svex-envs-equivalent x y))
  :rule-classes nil)

Theorem: svex-envs-equivalent-instancing-instance-rule-correct

(defthm svex-envs-equivalent-instancing-instance-rule-correct
  (implies (not (if (equal (svex-env-lookup k x)
                           (svex-env-lookup k y))
                    (iff (svex-env-boundp k x)
                         (svex-env-boundp k y))
                  'nil))
           (not (svex-envs-equivalent x y)))
  :rule-classes nil)

Theorem: svex-envs-equivalent-is-an-equivalence

(defthm svex-envs-equivalent-is-an-equivalence
  (and (booleanp (svex-envs-equivalent x y))
       (svex-envs-equivalent x x)
       (implies (svex-envs-equivalent x y)
                (svex-envs-equivalent y x))
       (implies (and (svex-envs-equivalent x y)
                     (svex-envs-equivalent y z))
                (svex-envs-equivalent x z)))
  :rule-classes (:equivalence))

Theorem: svex-envs-equivalent-refines-svex-envs-similar

(defthm svex-envs-equivalent-refines-svex-envs-similar
  (implies (svex-envs-equivalent x y)
           (svex-envs-similar x y))
  :rule-classes (:refinement))

Theorem: svex-envs-equivalent-implies-equal-svex-env-boundp-2

(defthm svex-envs-equivalent-implies-equal-svex-env-boundp-2
  (implies (svex-envs-equivalent x x-equiv)
           (equal (svex-env-boundp k x)
                  (svex-env-boundp k x-equiv)))
  :rule-classes (:congruence))

Theorem: set-equiv-implies-svex-envs-equivalent-svex-env-extract-1

(defthm set-equiv-implies-svex-envs-equivalent-svex-env-extract-1
  (implies (set-equiv keys keys-equiv)
           (svex-envs-equivalent (svex-env-extract keys env)
                                 (svex-env-extract keys-equiv env)))
  :rule-classes (:congruence))

Theorem: svex-envs-similar-implies-svex-envs-equivalent-svex-env-extract-2

(defthm
  svex-envs-similar-implies-svex-envs-equivalent-svex-env-extract-2
  (implies (svex-envs-similar env env-equiv)
           (svex-envs-equivalent (svex-env-extract keys env)
                                 (svex-env-extract keys env-equiv)))
  :rule-classes (:congruence))

Theorem: svex-env-boundp-of-append

(defthm svex-env-boundp-of-append
  (iff (svex-env-boundp k (append a b))
       (or (svex-env-boundp k a)
           (svex-env-boundp k b))))

Theorem: svex-env-lookup-of-append

(defthm svex-env-lookup-of-append
  (equal (svex-env-lookup k (append a b))
         (if (svex-env-boundp k a)
             (svex-env-lookup k a)
           (svex-env-lookup k b))))

Theorem: svex-envs-equivalent-implies-svex-envs-equivalent-append-1

(defthm svex-envs-equivalent-implies-svex-envs-equivalent-append-1
  (implies (svex-envs-equivalent a a-equiv)
           (svex-envs-equivalent (append a b)
                                 (append a-equiv b)))
  :rule-classes (:congruence))

Theorem: svex-envs-equivalent-implies-svex-envs-equivalent-append-2

(defthm svex-envs-equivalent-implies-svex-envs-equivalent-append-2
  (implies (svex-envs-equivalent b b-equiv)
           (svex-envs-equivalent (append a b)
                                 (append a b-equiv)))
  :rule-classes (:congruence))

Theorem: svex-envs-similar-implies-svex-envs-similar-append-2

(defthm svex-envs-similar-implies-svex-envs-similar-append-2
  (implies (svex-envs-similar b b-equiv)
           (svex-envs-similar (append a b)
                              (append a b-equiv)))
  :rule-classes (:congruence))

Theorem: svex-env-equiv-refines-svex-envs-equivalent

(defthm svex-env-equiv-refines-svex-envs-equivalent
  (implies (svex-env-equiv x y)
           (svex-envs-equivalent x y))
  :rule-classes (:refinement))