• 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
          • Svex-focused-equivalence-checking
            • Svexlist-evals-equal-with-transforms
            • Svexlist-eval-integer-listp-with-transforms
            • Svexlist-evals-equal-and-integerp-with-transforms
            • Eval-collection-of-a4vecs-and-aigs
            • Svexlist->a4vecs-for-varlist-with-subexprs
            • Svex-mask-env-common-constants
            • Svex-envs-common-constants-aux
            • 4veclist-separate-upper-lower-rec-log
            • Svex-envs-common-constants
            • A4veclist-separate-upper-lower-aux
            • 4veclist-separate-upper-lower
            • Svexlists->a4vec-top
            • A4veclist-separate-upper-lower
            • A4veclist->upper-a4vecs
            • 4veclist->upper-4vecs
            • Hons-aig-accumulate-nodes
            • A4veclist-accumulate-upper-nodes
            • Fgl::fgl-list-object-bfrcounts
            • Hons-aiglist-accumulate-nodes
            • Svexlist-evals-equal
            • A4veclist->upper-a4vecs-acc
            • My-replace-assoc
            • Svexlist-mask-alist/toposort-memo
            • My-binary-append
            • A4veclist-upper-subnodes
            • A4veclist-subnodes
            • A4veclist-accumulate-nodes
            • A4vec-accumulate-nodes
          • A4vec-operations
          • Svexlist-eval-gl
          • Aig-symbolic-arithmetic
          • Svex-varmasks/env->aig-env-rec
          • Svex-varmasks->a4env-rec
          • Svexlist/env-list-eval-gl
          • 4vmask-to-a4vec-rec-env
          • 4vmask-to-a4vec-rec
          • Svexlist->a4vecs-for-varlist
          • Svex-varmasks/env->aig-env-stats-rec
          • Svexlist->a4vec-nrev
          • A4veclist/svex-env-list-eval
          • A4vec
          • Svexlist-x-out-unused-vars
          • Svex->a4vec-memotable-correctp
          • A4vec/svex-env-eval
          • Svex-varmasks->a4env
          • Svex-varmasks/env->aig-env-rec-log
          • 4vmask-to-a4vec-env
          • 4veclist-from-bitlist-log-rec
          • Svex-apply-aig
          • Svexlist-vars-for-symbolic-eval
          • Nat-bool-a4env-upper-boundp
          • 4vmask-to-a4vec
          • Svexlist/env-list-vars-for-symbolic-eval
          • Svex-maskbits-for-vars
          • Svexlist->a4vec-aig-env-for-varlist
          • 4vec-from-bitlist
          • Svexlist-full-masks-p
          • Svex-varmasks/env->aig-env-stats
          • Svex-varmasks/env->aig-env
          • Svexlistlist->a4vec
          • Svex-const-concat-args
          • Svex-mask-alist-extract-vars
          • Svexlist->a4vec-top
          • Nat-bool-a4vec-upper-boundp
          • Nat-bool-a4env-lower-boundp
          • Maybe-a3vec-fix
          • Svex-maskbits-ok
          • Svex-envlist-check-boolmasks
          • Svex-env-check-boolmasks
          • Nat-bool-list-upper-boundp
          • Nat-bool-a4vec-lower-boundp
          • Maybe-svexlist-rewrite-fixpoint
          • 4vmask-to-a4vec-varcount
          • A4vec-eval
          • Svexlist-nth
          • A4veclist-nth
          • Nat-bool-list-lower-boundp
          • 4veclist-from-bitlist
          • V2i-first-n
          • A4veclist-eval-gl
          • Svex-envlist-keyset
          • Svex-a4vec-env-eval
          • A4veclist/env-list-eval
          • Svexlist-variable-mask-alist
          • Sparseint-nfix
          • A4veclist-length
          • A4veclist-eval
          • 4vec-boolmaskp
          • Nat-bool-list-nats
          • Nat-bool-a4env-p
          • Nat-bool-listp
          • A4veclist->aiglist
          • Svexlist-rewrite-fixpoint-memo
          • Nat-bool-a4vec-p
          • A4vec->aiglist
          • Svex-is-const-concat
          • Nat-bool-a4env-vars
          • Svexlist-mask-alist-memo
          • Nat-bool-a4vec-vars
          • Svexlist-vars-memo
          • A4vec-constantp
          • Svex-aig-memotable
          • Svex-a4vec-env
          • A4veclistlist
          • A4veclist
          • Symbolic-params-x-out-cond
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-focused-equivalence-checking

Svexlist-evals-equal-with-transforms

Signature

(svexlist-evals-equal-with-transforms x env1 env2 symbolic-params 
                                      transforms &key tracked-alist) 
 
  → 
*

Arguments

x — Guard (svexlist-p x).

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

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

symbolic-params — Guard (alistp symbolic-params).

Definitions and Theorems

Function: svexlist-evals-equal-with-transforms-fn

(defun svexlist-evals-equal-with-transforms-fn
       (x env1 env2 symbolic-params
          transforms tracked-alist)
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-env-p env1)
                              (svex-env-p env2)
                              (alistp symbolic-params))))
  (declare (ignorable symbolic-params
                      transforms tracked-alist))
  (let ((__function__ 'svexlist-evals-equal-with-transforms))
    (declare (ignorable __function__))
    (svexlist-evals-equal x env1 env2)))

Theorem: unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-4

(defthm
    unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-4
  (implies (fgl::unequiv symbolic-params symbolic-params-equiv)
           (equal (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params
                       transforms tracked-alist)
                  (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params-equiv
                       transforms tracked-alist)))
  :rule-classes (:congruence))

Theorem: unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-5

(defthm
    unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-5
  (implies (fgl::unequiv transforms transforms-equiv)
           (equal (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params
                       transforms tracked-alist)
                  (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params
                       transforms-equiv tracked-alist)))
  :rule-classes (:congruence))

Theorem: unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-6

(defthm
    unequiv-implies-equal-svexlist-evals-equal-with-transforms-fn-6
  (implies (fgl::unequiv tracked-alist tracked-alist-equiv)
           (equal (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params
                       transforms tracked-alist)
                  (svexlist-evals-equal-with-transforms-fn
                       x env1 env2 symbolic-params
                       transforms tracked-alist-equiv)))
  :rule-classes (:congruence))

Theorem: svexlist-evals-equal-with-transforms-fgl

(defthm svexlist-evals-equal-with-transforms-fgl
 (equal
  (svexlist-evals-equal-with-transforms
       x env1 env2 symbolic-params transforms
       :tracked-alist tracked-alist)
  (b*
   ((orig-x x)
    (env1 (make-fast-alist (svex-env-fix env1)))
    (env2 (make-fast-alist (svex-env-fix env2)))
    (svars
     (union
          (svexlist-vars-for-symbolic-eval x env1 symbolic-params)
          (svexlist-vars-for-symbolic-eval x env2 symbolic-params)))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (and (svex-env-check-boolmasks boolmasks env1)
                  (svex-env-check-boolmasks boolmasks env2)))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?foo (break$)))
      (fgl::abort-rewrite (svexlist-evals-equal orig-x env1 env2))))
    ((mv err x-a4vecs hint-a4vecs)
     (time$
      (svexlist->a4vecs-for-varlist-with-subexprs x svars boolmasks)
      :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err)))
      (fgl::abort-rewrite (svexlist-evals-equal orig-x env1 env2))))
    ((mv ?err aig-env1)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env1)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env1 (make-fast-alist aig-env1))
    ((mv ?err aig-env2)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env2)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env2 (make-fast-alist aig-env2))
    (?ign (fast-alist-free env1))
    (?ign (fast-alist-free env2))
    (x-eval1
     (time$
          (a4veclist-eval x-a4vecs aig-env1)
          :msg "; a4veclist-eval (x, env1): ~st sec, ~sa bytes.~%"))
    (hint-eval1
     (time$
        (a4veclist-eval hint-a4vecs aig-env1)
        :msg "; a4veclist-eval (sub, env1): ~st sec, ~sa bytes.~%"))
    (x-eval2
     (time$
          (a4veclist-eval x-a4vecs aig-env2)
          :msg "; a4veclist-eval (x, env2): ~st sec, ~sa bytes.~%"))
    (hint-eval2
     (time$
        (a4veclist-eval hint-a4vecs aig-env2)
        :msg "; a4veclist-eval (sub, env2): ~st sec, ~sa bytes.~%"))
    (evals-equal (equal x-eval1 x-eval2))
    ((mv iso-ok hint-eval1 hint-eval2)
     (fgl::fgl-make-isomorphic iso-ok hint-eval1 hint-eval2))
    ((unless iso-ok)
     (b*
      ((?ign
        (cw
         "ERROR: the equivalence hint objects couldn't be made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite (svexlist-evals-equal orig-x env1 env2))))
    (len1
     (fgl::syntax-bind
      len1
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-eval1)))))
    (len2
     (fgl::syntax-bind
      len2
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-eval2)))))
    ((unless (fgl::syntax-bind lens-equal (equal len1 len2)))
     (b*
      ((?ign
        (cw
         "ERROR: the number of BFR objects in the ~
                                 equivalence hint objects wasn't equal after ~
                                 they were made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (svexlist-evals-equal orig-x env1 env2)))))
   (fgl::fgl-simplify-ordered
    evals-equal transforms
    :tracked-obj
    (cons
     (cons
       :evals-equivalent-equiv-classes (cons hint-eval1 hint-eval2))
     tracked-alist)))))

Theorem: svexlist-evals-equal-with-transforms-fgl-less-extreme

(defthm svexlist-evals-equal-with-transforms-fgl-less-extreme
 (equal
  (svexlist-evals-equal-with-transforms
       x env1 env2 symbolic-params transforms
       :tracked-alist tracked-alist)
  (b*
   ((orig-x x)
    (env1 (make-fast-alist (svex-env-fix env1)))
    (env2 (make-fast-alist (svex-env-fix env2)))
    ((mv masks ?toposort)
     (svexlist-mask-alist/toposort-memo x))
    (const-env
     (time$
        (svex-mask-env-common-constants const-env masks env1 env2)))
    (x
     (time$
      (svexlist-compose-rw
         x
         (make-svex-substconfig
              :alist (make-fast-alist (svex-env-to-subst const-env))
              :simp 10))))
    (svars
     (union
          (svexlist-vars-for-symbolic-eval x env1 symbolic-params)
          (svexlist-vars-for-symbolic-eval x env2 symbolic-params)))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (and (svex-env-check-boolmasks boolmasks env1)
                  (svex-env-check-boolmasks boolmasks env2)))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2)))))
    ((mv err x-a4vecs subexp-a4vecs)
     (time$
      (svexlist->a4vecs-for-varlist-with-subexprs x svars boolmasks)
      :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err)))
       (fgl::abort-rewrite
            (and (svexlist-evals-equal orig-x env1 env2)))))
    ((mv ?err aig-env1)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env1)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env1 (make-fast-alist aig-env1))
    ((mv ?err aig-env2)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env2)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env2 (make-fast-alist aig-env2))
    (?ign (fast-alist-free env1))
    (?ign (fast-alist-free env2))
    ((mv x-eval1 sub-eval1 & & &)
     (eval-collection-of-a4vecs-and-aigs
          x-a4vecs
          subexp-a4vecs nil nil nil aig-env1))
    ((mv x-eval2 sub-eval2 & & &)
     (eval-collection-of-a4vecs-and-aigs
          x-a4vecs
          subexp-a4vecs nil nil nil aig-env2))
    (evals-equal (equal x-eval1 x-eval2))
    (sub-eval1 (acl2::list-to-tree sub-eval1))
    (sub-eval2 (acl2::list-to-tree sub-eval2))
    ((mv iso-ok hint-iso1 hint-iso2)
     (time$ (fgl::fgl-make-isomorphic iso-ok sub-eval1 sub-eval2)))
    ((unless iso-ok)
     (b*
      ((?ign
        (cw
         "ERROR: the equivalence hint objects couldn't be made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2)))))
    (len1
     (fgl::syntax-bind
       len1
       (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-iso1)))))
    (len2
     (fgl::syntax-bind
       len2
       (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-iso2)))))
    ((unless (fgl::syntax-bind lens-equal (equal len1 len2)))
     (b*
      ((?ign
        (cw
         "ERROR: the number of BFR objects in the ~
                                 equivalence hint objects wasn't equal after ~
                                 they were made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2))))))
   (fgl::fgl-simplify-ordered
    evals-equal transforms
    :tracked-obj
    (cons
     (cons
         :evals-equivalent-equiv-classes (cons hint-iso1 hint-iso2))
     tracked-alist)))))

Theorem: svexlist-evals-equal-with-transforms-fgl-extreme

(defthm svexlist-evals-equal-with-transforms-fgl-extreme
 (equal
  (svexlist-evals-equal-with-transforms
       x env1 env2 symbolic-params transforms
       :tracked-alist tracked-alist)
  (b*
   ((orig-x x)
    (env1 (make-fast-alist (svex-env-fix env1)))
    (env2 (make-fast-alist (svex-env-fix env2)))
    ((mv masks ?toposort)
     (svexlist-mask-alist/toposort-memo x))
    (const-env
     (time$
        (svex-mask-env-common-constants const-env masks env1 env2)))
    (x
     (time$
      (svexlist-compose-rw
         x
         (make-svex-substconfig
              :alist (make-fast-alist (svex-env-to-subst const-env))
              :simp 10))))
    (svars
     (union
          (svexlist-vars-for-symbolic-eval x env1 symbolic-params)
          (svexlist-vars-for-symbolic-eval x env2 symbolic-params)))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (and (svex-env-check-boolmasks boolmasks env1)
                  (svex-env-check-boolmasks boolmasks env2)))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2)))))
    ((mv err x-a4vecs)
     (time$ (svexlist->a4vecs-for-varlist x svars boolmasks)
            :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err)))
       (fgl::abort-rewrite
            (and (svexlist-evals-equal orig-x env1 env2)))))
    ((mv ?err aig-env1)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env1)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env1 (make-fast-alist aig-env1))
    ((mv ?err aig-env2)
     (time$
        (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env2)
        :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env2 (make-fast-alist aig-env2))
    (?ign (fast-alist-free env1))
    (?ign (fast-alist-free env2))
    (aigs (a4veclist-subnodes x-a4vecs))
    ((mv x-eval1 & & & aigs-eval1)
     (eval-collection-of-a4vecs-and-aigs
          x-a4vecs nil nil nil aigs aig-env1))
    ((mv x-eval2 & & & aigs-eval2)
     (eval-collection-of-a4vecs-and-aigs
          x-a4vecs nil nil nil aigs aig-env2))
    (evals-equal (equal x-eval1 x-eval2))
    (aigs-eval1 (acl2::list-to-tree aigs-eval1))
    (aigs-eval2 (acl2::list-to-tree aigs-eval2))
    ((mv iso-ok hint-iso1 hint-iso2)
     (time$
          (fgl::fgl-make-isomorphic iso-ok aigs-eval1 aigs-eval2)))
    ((unless iso-ok)
     (b*
      ((?ign
        (cw
         "ERROR: the equivalence hint objects couldn't be made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2)))))
    (len1
     (fgl::syntax-bind
       len1
       (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-iso1)))))
    (len2
     (fgl::syntax-bind
       len2
       (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-iso2)))))
    ((unless (fgl::syntax-bind lens-equal (equal len1 len2)))
     (b*
      ((?ign
        (cw
         "ERROR: the number of BFR objects in the ~
                                 equivalence hint objects wasn't equal after ~
                                 they were made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (svexlist-evals-equal orig-x env1 env2))))))
   (fgl::fgl-simplify-ordered
    evals-equal transforms
    :tracked-obj
    (cons
     (cons
         :evals-equivalent-equiv-classes (cons hint-iso1 hint-iso2))
     tracked-alist)))))