• 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
          • Moddb.lisp
            • Moddb-add-modinst-to-last
            • Moddb-add-module1
            • Moddb-norm
            • Elab-modlist-norm
            • Moddb-ok
            • Elab-modinsts-rem-dups
            • Moddb-add-modinst
            • Elab-mod-initialize-aliases
            • Modinstlist-add-modinsts
            • Moddb-mod-ok
            • Wirelist-rem-dups
            • Moddb-norm-p
            • Elab-mod$a-fix
            • Moddb-mod-order-ok
            • Moddb-mod-insts-ok
            • Elab-mod-wire-find-inst-aux
            • Svex-alist->absindexed
            • Modscope-push-frame
            • Moddb-modinst-ok
            • Lhspairs->absindexed
            • Moddb-mod-inst-wireoffset
            • Moddb-find-bad-modinst-order
            • Constraintlist->absindexed
            • Wirelist-remove-names
            • Moddb-mod-inst-instoffset
            • Lhspairs-named->indexed
            • Elab-modinst-fix
            • Moddb-mod-totalwires
            • Svar-map->absindexed
            • Moddb-modinst-order-ok
            • Moddb-mod-totalinsts
            • Moddb-find-bad-modinst
            • Modscope
            • Constraintlist-named->indexed
            • Assigns->absindexed
            • Moddb-indices-ok
            • Lhs->absindexed
            • Svar-map-named->indexed
            • Module-named->indexed
            • Moddb-find-bad-index
            • Assigns-named->indexed
            • Svar-named->indexed
            • Lhs-named->indexed
            • Elab-mod$c-add-wire
            • Moddb-modname-get-index
            • Moddb-maybe-grow
            • Lhspairs-named->indexed-aux-nrev
            • Elab-modinst-list-names
            • Elab-mod-wire-find-inst
            • Svar->absindexed
            • Moddb-path->wiredecl
            • Modalist-named->indexed
            • Lhspairs->absindexed-nrev
            • Elab-mod$ap
            • Elab-modinst-remove-names
            • Moddb-wireidx->paths
            • Moddb-mods-ok
            • Moddb-find-bad-mod
            • Elab-mod$c-add-inst
            • Elab-mod$c-modinsts-ok
            • Elab-modinst-remove-name
            • Modscope->nth
            • Moddb-basics-ok
            • Svex->absindexed-memo-ok
            • Svex-named->indexed-memo-ok
            • Svarlist-idxaddr-okp
            • Elab-modlist-normp
            • Wirelist-remove-name
            • Modscope->top
            • Moddb-fix
            • Elab-mod$a-add-inst
            • Elab-mod-wiresearch-smartpivot
            • Elab-mod$c-wires-ok
            • Update-elab-mod$a->totalwires
            • Update-elab-mod$a->totalinsts
            • Update-elab-mod$a->orig-mod
            • Update-elab-mod$a->name
            • Moddb-modinst-order-badguy
            • Elab-mod$a-add-wire
            • Elab-mod$a-wiretablei
            • Elab-mod-wiresearch-pivot
            • Elab-mod-wireoffset
            • Elab-mod-instoffset
            • Svar-idxaddr-okp
            • Paths-add-scope
            • Moddb-modinst-badguy
            • Moddb-mod-nwires
            • Moddb-mod-ninsts
            • Modalist-all-idxaddr-okp
            • Elab-mod$a->instname
            • Elab-mods->names
            • Elab-modinst$c-copy
            • Elab-mod$a->inst-wireoffset
            • Elab-mod$a->inst-instoffset
            • Moddb-elab-mod-stats
            • Moddb-contains-modnames
            • Elab-mod$c-inst-abstraction
            • Elab-mod$a->inst-modidx
            • Elab-mod$a-wirename->idx
            • Elab-mod$a-instname->idx
            • Elab-mod-add-wires
            • Modscope-top-bound
            • Modscope-local-bound
            • Constraintlist-add-scope
            • Moddb-modidx-get-name
            • Moddb-add-module
            • Elab-mod-wiresearch-dumbpivot
            • Update-moddb->nmods
            • Elab-mod$c->inst-wireoffset
            • Elab-mod$c->inst-modidx
            • Elab-mod$c->inst-instoffset
            • Elab-mod$c-wire-abstraction
            • Moddb-clear
            • Elab-mod$c->instname
            • Svex-mod->flatten
            • Names->paths
            • Modscope->wireoffset
            • Modscope->instoffset
            • Moddb-mod-badguy
            • Elab-modinsts-nodups-p
            • Wirelist-nodups-p
            • Nat-list-max
            • Modscope->modidx
            • Elab-mod-wiresearch-next-smartp
            • Elab-mod$a->totalwires
            • Elab-mod$a->totalinsts
            • Elab-mod$a->orig-mod
            • Elab-mod$a->name
            • Elab-mod$a-nwires
            • Elab-mod$a-ninsts
            • Elab-modinst$c-fix
            • Elab-mod-fix
            • Create-elab-mod$a
            • Pathlist
            • Module->db
            • Elab-modlist
              • Elab-modlist-fix
                • Elab-modlist-equiv
                • Elab-modlist-p
              • Elab-modinst-list
              • Nrec-list-mods
              • Moddb->nmods
              • Nrec-list
              • Nrec
            • Elab-mod
            • Moddb-path->wireidx/decl
            • Moddb-wireidx->path/decl
            • Moddb-path->wireidx
            • Moddb-address->wireidx
            • Moddb-address->wiredecl
            • Moddb-wireidx->path
            • Modscope-okp
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Elab-modlist

    Elab-modlist-fix

    (elab-modlist-fix x) is a usual fty list fixing function.

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

    In the logic, we apply elab-mod$a-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

    Definitions and Theorems

    Function: elab-modlist-fix$inline

    (defun elab-modlist-fix$inline (x)
      (declare (xargs :guard (elab-modlist-p x)))
      (let ((__function__ 'elab-modlist-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 nil
               (cons (elab-mod$a-fix (car x))
                     (elab-modlist-fix (cdr x))))
             :exec x)))

    Theorem: elab-modlist-p-of-elab-modlist-fix

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

    Theorem: elab-modlist-fix-when-elab-modlist-p

    (defthm elab-modlist-fix-when-elab-modlist-p
      (implies (elab-modlist-p x)
               (equal (elab-modlist-fix x) x)))

    Function: elab-modlist-equiv$inline

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

    Theorem: elab-modlist-equiv-is-an-equivalence

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

    Theorem: elab-modlist-equiv-implies-equal-elab-modlist-fix-1

    (defthm elab-modlist-equiv-implies-equal-elab-modlist-fix-1
      (implies (elab-modlist-equiv x x-equiv)
               (equal (elab-modlist-fix x)
                      (elab-modlist-fix x-equiv)))
      :rule-classes (:congruence))

    Theorem: elab-modlist-fix-under-elab-modlist-equiv

    (defthm elab-modlist-fix-under-elab-modlist-equiv
      (elab-modlist-equiv (elab-modlist-fix x)
                          x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-elab-modlist-fix-1-forward-to-elab-modlist-equiv

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

    Theorem: equal-of-elab-modlist-fix-2-forward-to-elab-modlist-equiv

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

    Theorem: elab-modlist-equiv-of-elab-modlist-fix-1-forward

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

    Theorem: elab-modlist-equiv-of-elab-modlist-fix-2-forward

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

    Theorem: car-of-elab-modlist-fix-x-under-elab-mod$a-equiv

    (defthm car-of-elab-modlist-fix-x-under-elab-mod$a-equiv
      (elab-mod$a-equiv (car (elab-modlist-fix x))
                        (car x)))

    Theorem: car-elab-modlist-equiv-congruence-on-x-under-elab-mod$a-equiv

    (defthm
          car-elab-modlist-equiv-congruence-on-x-under-elab-mod$a-equiv
      (implies (elab-modlist-equiv x x-equiv)
               (elab-mod$a-equiv (car x)
                                 (car x-equiv)))
      :rule-classes :congruence)

    Theorem: cdr-of-elab-modlist-fix-x-under-elab-modlist-equiv

    (defthm cdr-of-elab-modlist-fix-x-under-elab-modlist-equiv
      (elab-modlist-equiv (cdr (elab-modlist-fix x))
                          (cdr x)))

    Theorem: cdr-elab-modlist-equiv-congruence-on-x-under-elab-modlist-equiv

    (defthm
        cdr-elab-modlist-equiv-congruence-on-x-under-elab-modlist-equiv
      (implies (elab-modlist-equiv x x-equiv)
               (elab-modlist-equiv (cdr x)
                                   (cdr x-equiv)))
      :rule-classes :congruence)

    Theorem: cons-of-elab-mod$a-fix-x-under-elab-modlist-equiv

    (defthm cons-of-elab-mod$a-fix-x-under-elab-modlist-equiv
      (elab-modlist-equiv (cons (elab-mod$a-fix x) y)
                          (cons x y)))

    Theorem: cons-elab-mod$a-equiv-congruence-on-x-under-elab-modlist-equiv

    (defthm
         cons-elab-mod$a-equiv-congruence-on-x-under-elab-modlist-equiv
      (implies (elab-mod$a-equiv x x-equiv)
               (elab-modlist-equiv (cons x y)
                                   (cons x-equiv y)))
      :rule-classes :congruence)

    Theorem: cons-of-elab-modlist-fix-y-under-elab-modlist-equiv

    (defthm cons-of-elab-modlist-fix-y-under-elab-modlist-equiv
      (elab-modlist-equiv (cons x (elab-modlist-fix y))
                          (cons x y)))

    Theorem: cons-elab-modlist-equiv-congruence-on-y-under-elab-modlist-equiv

    (defthm
       cons-elab-modlist-equiv-congruence-on-y-under-elab-modlist-equiv
      (implies (elab-modlist-equiv y y-equiv)
               (elab-modlist-equiv (cons x y)
                                   (cons x y-equiv)))
      :rule-classes :congruence)

    Theorem: consp-of-elab-modlist-fix

    (defthm consp-of-elab-modlist-fix
      (equal (consp (elab-modlist-fix x))
             (consp x)))

    Theorem: elab-modlist-fix-under-iff

    (defthm elab-modlist-fix-under-iff
      (iff (elab-modlist-fix x) (consp x)))

    Theorem: elab-modlist-fix-of-cons

    (defthm elab-modlist-fix-of-cons
      (equal (elab-modlist-fix (cons a x))
             (cons (elab-mod$a-fix a)
                   (elab-modlist-fix x))))

    Theorem: len-of-elab-modlist-fix

    (defthm len-of-elab-modlist-fix
      (equal (len (elab-modlist-fix x))
             (len x)))

    Theorem: elab-modlist-fix-of-append

    (defthm elab-modlist-fix-of-append
      (equal (elab-modlist-fix (append std::a std::b))
             (append (elab-modlist-fix std::a)
                     (elab-modlist-fix std::b))))

    Theorem: elab-modlist-fix-of-repeat

    (defthm elab-modlist-fix-of-repeat
      (equal (elab-modlist-fix (repeat acl2::n x))
             (repeat acl2::n (elab-mod$a-fix x))))

    Theorem: list-equiv-refines-elab-modlist-equiv

    (defthm list-equiv-refines-elab-modlist-equiv
      (implies (list-equiv x y)
               (elab-modlist-equiv x y))
      :rule-classes :refinement)

    Theorem: nth-of-elab-modlist-fix

    (defthm nth-of-elab-modlist-fix
      (equal (nth acl2::n (elab-modlist-fix x))
             (if (< (nfix acl2::n) (len x))
                 (elab-mod$a-fix (nth acl2::n x))
               nil)))

    Theorem: elab-modlist-equiv-implies-elab-modlist-equiv-append-1

    (defthm elab-modlist-equiv-implies-elab-modlist-equiv-append-1
      (implies (elab-modlist-equiv x fty::x-equiv)
               (elab-modlist-equiv (append x y)
                                   (append fty::x-equiv y)))
      :rule-classes (:congruence))

    Theorem: elab-modlist-equiv-implies-elab-modlist-equiv-append-2

    (defthm elab-modlist-equiv-implies-elab-modlist-equiv-append-2
      (implies (elab-modlist-equiv y fty::y-equiv)
               (elab-modlist-equiv (append x y)
                                   (append x fty::y-equiv)))
      :rule-classes (:congruence))

    Theorem: elab-modlist-equiv-implies-elab-modlist-equiv-nthcdr-2

    (defthm elab-modlist-equiv-implies-elab-modlist-equiv-nthcdr-2
      (implies (elab-modlist-equiv acl2::l l-equiv)
               (elab-modlist-equiv (nthcdr acl2::n acl2::l)
                                   (nthcdr acl2::n l-equiv)))
      :rule-classes (:congruence))

    Theorem: elab-modlist-equiv-implies-elab-modlist-equiv-take-2

    (defthm elab-modlist-equiv-implies-elab-modlist-equiv-take-2
      (implies (elab-modlist-equiv acl2::l l-equiv)
               (elab-modlist-equiv (take acl2::n acl2::l)
                                   (take acl2::n l-equiv)))
      :rule-classes (:congruence))