• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-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-svex-memo-p
              • Svex-svex-memo-fix
                • Svex-svex-memo-equiv
              • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svex-svex-memo

    Svex-svex-memo-fix

    (svex-svex-memo-fix x) is an fty alist fixing function that follows the fix-keys strategy.

    Signature
    (svex-svex-memo-fix x) → fty::newx
    Arguments
    x — Guard (svex-svex-memo-p x).
    Returns
    fty::newx — Type (svex-svex-memo-p fty::newx).

    Note that in the execution this is just an inline identity function.

    Definitions and Theorems

    Function: svex-svex-memo-fix$inline

    (defun svex-svex-memo-fix$inline (x)
      (declare (xargs :guard (svex-svex-memo-p x)))
      (let ((__function__ 'svex-svex-memo-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 x
               (if (consp (car x))
                   (cons (cons (svex-fix (caar x))
                               (svex-fix (cdar x)))
                         (svex-svex-memo-fix (cdr x)))
                 (svex-svex-memo-fix (cdr x))))
             :exec x)))

    Theorem: svex-svex-memo-p-of-svex-svex-memo-fix

    (defthm svex-svex-memo-p-of-svex-svex-memo-fix
      (b* ((fty::newx (svex-svex-memo-fix$inline x)))
        (svex-svex-memo-p fty::newx))
      :rule-classes :rewrite)

    Theorem: svex-svex-memo-fix-when-svex-svex-memo-p

    (defthm svex-svex-memo-fix-when-svex-svex-memo-p
      (implies (svex-svex-memo-p x)
               (equal (svex-svex-memo-fix x) x)))

    Function: svex-svex-memo-equiv$inline

    (defun svex-svex-memo-equiv$inline (x y)
      (declare (xargs :guard (and (svex-svex-memo-p x)
                                  (svex-svex-memo-p y))))
      (equal (svex-svex-memo-fix x)
             (svex-svex-memo-fix y)))

    Theorem: svex-svex-memo-equiv-is-an-equivalence

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

    Theorem: svex-svex-memo-equiv-implies-equal-svex-svex-memo-fix-1

    (defthm svex-svex-memo-equiv-implies-equal-svex-svex-memo-fix-1
      (implies (svex-svex-memo-equiv x x-equiv)
               (equal (svex-svex-memo-fix x)
                      (svex-svex-memo-fix x-equiv)))
      :rule-classes (:congruence))

    Theorem: svex-svex-memo-fix-under-svex-svex-memo-equiv

    (defthm svex-svex-memo-fix-under-svex-svex-memo-equiv
      (svex-svex-memo-equiv (svex-svex-memo-fix x)
                            x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-svex-svex-memo-fix-1-forward-to-svex-svex-memo-equiv

    (defthm
          equal-of-svex-svex-memo-fix-1-forward-to-svex-svex-memo-equiv
      (implies (equal (svex-svex-memo-fix x) y)
               (svex-svex-memo-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: equal-of-svex-svex-memo-fix-2-forward-to-svex-svex-memo-equiv

    (defthm
          equal-of-svex-svex-memo-fix-2-forward-to-svex-svex-memo-equiv
      (implies (equal x (svex-svex-memo-fix y))
               (svex-svex-memo-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: svex-svex-memo-equiv-of-svex-svex-memo-fix-1-forward

    (defthm svex-svex-memo-equiv-of-svex-svex-memo-fix-1-forward
      (implies (svex-svex-memo-equiv (svex-svex-memo-fix x)
                                     y)
               (svex-svex-memo-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: svex-svex-memo-equiv-of-svex-svex-memo-fix-2-forward

    (defthm svex-svex-memo-equiv-of-svex-svex-memo-fix-2-forward
      (implies (svex-svex-memo-equiv x (svex-svex-memo-fix y))
               (svex-svex-memo-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: cons-of-svex-fix-k-under-svex-svex-memo-equiv

    (defthm cons-of-svex-fix-k-under-svex-svex-memo-equiv
      (svex-svex-memo-equiv (cons (cons (svex-fix acl2::k) acl2::v)
                                  x)
                            (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-svex-equiv-congruence-on-k-under-svex-svex-memo-equiv

    (defthm cons-svex-equiv-congruence-on-k-under-svex-svex-memo-equiv
      (implies (svex-equiv acl2::k k-equiv)
               (svex-svex-memo-equiv (cons (cons acl2::k acl2::v) x)
                                     (cons (cons k-equiv acl2::v) x)))
      :rule-classes :congruence)

    Theorem: cons-of-svex-fix-v-under-svex-svex-memo-equiv

    (defthm cons-of-svex-fix-v-under-svex-svex-memo-equiv
      (svex-svex-memo-equiv (cons (cons acl2::k (svex-fix acl2::v))
                                  x)
                            (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-svex-equiv-congruence-on-v-under-svex-svex-memo-equiv

    (defthm cons-svex-equiv-congruence-on-v-under-svex-svex-memo-equiv
      (implies (svex-equiv acl2::v v-equiv)
               (svex-svex-memo-equiv (cons (cons acl2::k acl2::v) x)
                                     (cons (cons acl2::k v-equiv) x)))
      :rule-classes :congruence)

    Theorem: cons-of-svex-svex-memo-fix-y-under-svex-svex-memo-equiv

    (defthm cons-of-svex-svex-memo-fix-y-under-svex-svex-memo-equiv
      (svex-svex-memo-equiv (cons x (svex-svex-memo-fix y))
                            (cons x y)))

    Theorem: cons-svex-svex-memo-equiv-congruence-on-y-under-svex-svex-memo-equiv

    (defthm
     cons-svex-svex-memo-equiv-congruence-on-y-under-svex-svex-memo-equiv
     (implies (svex-svex-memo-equiv y y-equiv)
              (svex-svex-memo-equiv (cons x y)
                                    (cons x y-equiv)))
     :rule-classes :congruence)

    Theorem: svex-svex-memo-fix-of-acons

    (defthm svex-svex-memo-fix-of-acons
      (equal (svex-svex-memo-fix (cons (cons acl2::a acl2::b) x))
             (cons (cons (svex-fix acl2::a)
                         (svex-fix acl2::b))
                   (svex-svex-memo-fix x))))

    Theorem: svex-svex-memo-fix-of-append

    (defthm svex-svex-memo-fix-of-append
      (equal (svex-svex-memo-fix (append std::a std::b))
             (append (svex-svex-memo-fix std::a)
                     (svex-svex-memo-fix std::b))))

    Theorem: consp-car-of-svex-svex-memo-fix

    (defthm consp-car-of-svex-svex-memo-fix
      (equal (consp (car (svex-svex-memo-fix x)))
             (consp (svex-svex-memo-fix x))))