• 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-rewrite
            • Svexlist-rewrite
          • Svexlist-rewrite-nrev
          • Svex-args-apply-masks
          • 4veclist-quote
          • Svex-simpconfig-p
          • Svex-rewrite-memo-correct
          • Svex-alist-maybe-rewrite-fixpoint
          • Svexlist-compute-masks
          • Svexlist-rewrite-under-masks
          • Svex-alist-rewrite-fixpoint
          • Svexlist-maybe-rewrite-fixpoint
          • Svexlist-rewrite-fixpoint
          • Svexlist-mask-acons
          • Svexlist-mask-alist/toposort
          • Svex-call-simp
          • Svex-alist-compose
          • Svexlist-rewrite-top
          • Svex-alist-subst
          • Svex-alist-compose-rw
          • Svex-argmasks-lookup
          • Svex-alist-subst-rw
          • Svexlist-mask-acons-rev
          • Svex-mask-lookup
          • Svex-mask-acons
          • Svexlist-mask-alist
          • Svex-alist-rewrite-top
          • Constraintlist-compose
          • Svex-substconfig
          • Svex-simpconfig-fix
          • Svex-subst
          • Svex-rewrite-memo-vars-ok
          • Svex-norm-call
          • Svex-3value-mask
          • Svexlist-count-calls-aux
          • Svex-mask-alist-keys
          • Rewriter-tracing
          • Svex-rewrite-top
          • Svexlist-maskfree-rewrite-nrev
          • Svexlist-multirefs-top
          • Svexlist-count-calls
          • Svex-unify
          • Svexlist-toposort-p
          • Svexlist-maskfree-rewrite-top
          • Svex-alist-compose-nrev
          • Rewriting-concatenations
          • Svex-svex-memo
          • Svex-mask-alist
          • Svex-alist-subst-nrev
          • Svex-simpconfig-fix!
          • Svex-rewrite-rules
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Rewriting

Svex-rewrite

Recursively rewrite an svex expression.

Signature

(svex-rewrite x masks multirefs out-multirefs memo) 
  → 
(mv xx out-multirefs memo)

Arguments

x — Guard (svex-p x).

masks — Guard (svex-mask-alist-p masks).

multirefs — Guard (svex-key-alist-p multirefs).

out-multirefs — Guard (svex-key-alist-p out-multirefs).

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

Returns

xx — Type (svex-p xx).

out-multirefs — Type (svex-key-alist-p out-multirefs).

memo — Type (svex-svex-memo-p memo).

Theorem: return-type-of-svex-rewrite.xx

(defthm return-type-of-svex-rewrite.xx
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svex-rewrite x masks multirefs out-multirefs memo)))
    (svex-p xx))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-rewrite.out-multirefs

(defthm return-type-of-svex-rewrite.out-multirefs
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svex-rewrite x masks multirefs out-multirefs memo)))
    (svex-key-alist-p out-multirefs))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-rewrite.memo

(defthm return-type-of-svex-rewrite.memo
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svex-rewrite x masks multirefs out-multirefs memo)))
    (svex-svex-memo-p memo))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-rewrite.xx

(defthm return-type-of-svexlist-rewrite.xx
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svexlist-rewrite x masks multirefs out-multirefs memo)))
    (svexlist-p xx))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-rewrite.out-multirefs

(defthm return-type-of-svexlist-rewrite.out-multirefs
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svexlist-rewrite x masks multirefs out-multirefs memo)))
    (svex-key-alist-p out-multirefs))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-rewrite.memo

(defthm return-type-of-svexlist-rewrite.memo
  (b* (((mv ?xx ?out-multirefs ?memo)
        (svexlist-rewrite x masks multirefs out-multirefs memo)))
    (svex-svex-memo-p memo))
  :rule-classes :rewrite)

Theorem: svex-rewrite-of-svex-fix-x

(defthm svex-rewrite-of-svex-fix-x
  (equal (svex-rewrite (svex-fix x)
                       masks multirefs out-multirefs memo)
         (svex-rewrite x masks multirefs out-multirefs memo)))

Theorem: svex-rewrite-of-svex-mask-alist-fix-masks

(defthm svex-rewrite-of-svex-mask-alist-fix-masks
  (equal (svex-rewrite x (svex-mask-alist-fix masks)
                       multirefs out-multirefs memo)
         (svex-rewrite x masks multirefs out-multirefs memo)))

Theorem: svex-rewrite-of-svex-key-alist-fix-multirefs

(defthm svex-rewrite-of-svex-key-alist-fix-multirefs
  (equal (svex-rewrite x masks (svex-key-alist-fix multirefs)
                       out-multirefs memo)
         (svex-rewrite x masks multirefs out-multirefs memo)))

Theorem: svex-rewrite-of-svex-key-alist-fix-out-multirefs

(defthm svex-rewrite-of-svex-key-alist-fix-out-multirefs
  (equal (svex-rewrite x masks multirefs
                       (svex-key-alist-fix out-multirefs)
                       memo)
         (svex-rewrite x masks multirefs out-multirefs memo)))

Theorem: svex-rewrite-of-svex-svex-memo-fix-memo

(defthm svex-rewrite-of-svex-svex-memo-fix-memo
  (equal (svex-rewrite x masks multirefs
                       out-multirefs (svex-svex-memo-fix memo))
         (svex-rewrite x masks multirefs out-multirefs memo)))

Theorem: svexlist-rewrite-of-svexlist-fix-x

(defthm svexlist-rewrite-of-svexlist-fix-x
  (equal (svexlist-rewrite (svexlist-fix x)
                           masks multirefs out-multirefs memo)
         (svexlist-rewrite x masks multirefs out-multirefs memo)))

Theorem: svexlist-rewrite-of-svex-mask-alist-fix-masks

(defthm svexlist-rewrite-of-svex-mask-alist-fix-masks
  (equal (svexlist-rewrite x (svex-mask-alist-fix masks)
                           multirefs out-multirefs memo)
         (svexlist-rewrite x masks multirefs out-multirefs memo)))

Theorem: svexlist-rewrite-of-svex-key-alist-fix-multirefs

(defthm svexlist-rewrite-of-svex-key-alist-fix-multirefs
  (equal (svexlist-rewrite x masks (svex-key-alist-fix multirefs)
                           out-multirefs memo)
         (svexlist-rewrite x masks multirefs out-multirefs memo)))

Theorem: svexlist-rewrite-of-svex-key-alist-fix-out-multirefs

(defthm svexlist-rewrite-of-svex-key-alist-fix-out-multirefs
  (equal (svexlist-rewrite x masks multirefs
                           (svex-key-alist-fix out-multirefs)
                           memo)
         (svexlist-rewrite x masks multirefs out-multirefs memo)))

Theorem: svexlist-rewrite-of-svex-svex-memo-fix-memo

(defthm svexlist-rewrite-of-svex-svex-memo-fix-memo
  (equal (svexlist-rewrite x masks multirefs
                           out-multirefs (svex-svex-memo-fix memo))
         (svexlist-rewrite x masks multirefs out-multirefs memo)))

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

(defthm svex-rewrite-svex-equiv-congruence-on-x
 (implies (svex-equiv x x-equiv)
          (equal (svex-rewrite x masks multirefs out-multirefs memo)
                 (svex-rewrite x-equiv
                               masks multirefs out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svex-rewrite-svex-mask-alist-equiv-congruence-on-masks

(defthm svex-rewrite-svex-mask-alist-equiv-congruence-on-masks
 (implies (svex-mask-alist-equiv masks masks-equiv)
          (equal (svex-rewrite x masks multirefs out-multirefs memo)
                 (svex-rewrite x masks-equiv
                               multirefs out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svex-rewrite-svex-key-alist-equiv-congruence-on-multirefs

(defthm svex-rewrite-svex-key-alist-equiv-congruence-on-multirefs
 (implies (svex-key-alist-equiv multirefs multirefs-equiv)
          (equal (svex-rewrite x masks multirefs out-multirefs memo)
                 (svex-rewrite x masks
                               multirefs-equiv out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svex-rewrite-svex-key-alist-equiv-congruence-on-out-multirefs

(defthm
      svex-rewrite-svex-key-alist-equiv-congruence-on-out-multirefs
 (implies (svex-key-alist-equiv out-multirefs out-multirefs-equiv)
          (equal (svex-rewrite x masks multirefs out-multirefs memo)
                 (svex-rewrite x masks
                               multirefs out-multirefs-equiv memo)))
 :rule-classes :congruence)

Theorem: svex-rewrite-svex-svex-memo-equiv-congruence-on-memo

(defthm svex-rewrite-svex-svex-memo-equiv-congruence-on-memo
 (implies (svex-svex-memo-equiv memo memo-equiv)
          (equal (svex-rewrite x masks multirefs out-multirefs memo)
                 (svex-rewrite x masks
                               multirefs out-multirefs memo-equiv)))
 :rule-classes :congruence)

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

(defthm svexlist-rewrite-svexlist-equiv-congruence-on-x
 (implies
      (svexlist-equiv x x-equiv)
      (equal (svexlist-rewrite x masks multirefs out-multirefs memo)
             (svexlist-rewrite x-equiv
                               masks multirefs out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-svex-mask-alist-equiv-congruence-on-masks

(defthm svexlist-rewrite-svex-mask-alist-equiv-congruence-on-masks
 (implies
      (svex-mask-alist-equiv masks masks-equiv)
      (equal (svexlist-rewrite x masks multirefs out-multirefs memo)
             (svexlist-rewrite x masks-equiv
                               multirefs out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-svex-key-alist-equiv-congruence-on-multirefs

(defthm
      svexlist-rewrite-svex-key-alist-equiv-congruence-on-multirefs
 (implies
      (svex-key-alist-equiv multirefs multirefs-equiv)
      (equal (svexlist-rewrite x masks multirefs out-multirefs memo)
             (svexlist-rewrite x masks
                               multirefs-equiv out-multirefs memo)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-svex-key-alist-equiv-congruence-on-out-multirefs

(defthm
  svexlist-rewrite-svex-key-alist-equiv-congruence-on-out-multirefs
 (implies
      (svex-key-alist-equiv out-multirefs out-multirefs-equiv)
      (equal (svexlist-rewrite x masks multirefs out-multirefs memo)
             (svexlist-rewrite x masks
                               multirefs out-multirefs-equiv memo)))
 :rule-classes :congruence)

Theorem: svexlist-rewrite-svex-svex-memo-equiv-congruence-on-memo

(defthm svexlist-rewrite-svex-svex-memo-equiv-congruence-on-memo
 (implies
      (svex-svex-memo-equiv memo memo-equiv)
      (equal (svexlist-rewrite x masks multirefs out-multirefs memo)
             (svexlist-rewrite x masks
                               multirefs out-multirefs memo-equiv)))
 :rule-classes :congruence)

Theorem: len-of-svexlist-rewrite

(defthm len-of-svexlist-rewrite
 (equal
  (len
   (mv-nth 0
           (svexlist-rewrite x masks multirefs out-multirefs memo)))
  (len x)))

Theorem: svex-rewrite-correct

(defthm svex-rewrite-correct
  (b* (((mv res out-multirefs1 memo1)
        (svex-rewrite x masks multirefs out-multirefs memo))
       (mask (svex-mask-lookup x masks)))
    (implies (and (svex-rewrite-memo-correct memo masks env)
                  (svex-mask-alist-complete masks))
             (and (svex-rewrite-memo-correct memo1 masks env)
                  (equal (4vec-mask mask (svex-eval res env))
                         (4vec-mask mask (svex-eval x env)))))))

Theorem: svexlist-rewrite-correct

(defthm svexlist-rewrite-correct
 (b* (((mv res out-multirefs1 memo1)
       (svexlist-rewrite x masks multirefs out-multirefs memo))
      (argmasks (svex-argmasks-lookup x masks)))
  (implies
     (and (svex-rewrite-memo-correct memo masks env)
          (svex-mask-alist-complete masks))
     (and (svex-rewrite-memo-correct memo1 masks env)
          (equal (4veclist-mask argmasks (svexlist-eval res env))
                 (4veclist-mask argmasks (svexlist-eval x env)))))))

Theorem: svex-rewrite-vars

(defthm svex-rewrite-vars
  (b* (((mv res out-multirefs1 memo1)
        (svex-rewrite x masks multirefs out-multirefs memo)))
    (implies (svex-rewrite-memo-vars-ok memo v)
             (and (svex-rewrite-memo-vars-ok memo1 v)
                  (implies (not (member v (svex-vars x)))
                           (not (member v (svex-vars res))))))))

Theorem: svexlist-rewrite-vars

(defthm svexlist-rewrite-vars
  (b* (((mv res out-multirefs1 memo1)
        (svexlist-rewrite x masks multirefs out-multirefs memo)))
    (implies (svex-rewrite-memo-vars-ok memo v)
             (and (svex-rewrite-memo-vars-ok memo1 v)
                  (implies (not (member v (svexlist-vars x)))
                           (not (member v (svexlist-vars res))))))))

Theorem: true-listp-of-svexlist-rewrite

(defthm true-listp-of-svexlist-rewrite
 (true-listp
  (mv-nth 0
          (svexlist-rewrite x masks multirefs out-multirefs memo))))

Theorem: svexlist-rewrite-breakdown

(defthm svexlist-rewrite-breakdown
 (equal
  (list
   (mv-nth 0
           (svexlist-rewrite x masks multirefs out-multirefs memo))
   (mv-nth 1
           (svexlist-rewrite x masks multirefs out-multirefs memo))
   (mv-nth 2
           (svexlist-rewrite x masks multirefs out-multirefs memo)))
  (svexlist-rewrite x masks multirefs out-multirefs memo)))

Subtopics

Svexlist-rewrite

Recursively rewrite a list of svex expressions.