• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
        • Typo-detection
        • Vl-wireinfo-alistp
        • Vl-annotate-vardecllist-with-wireinfo
        • Vl-useset-report-entry-p
        • Vl-print-useset-report-entry
        • Vl-mark-wires-for-module
        • Vl-split-useset-report
        • Vl-annotate-vardecl-with-wireinfo
        • Vl-mark-wires-for-modinstlist
        • Vl-mark-wires-for-modinst
        • Vl-mark-wires-for-gateinstlist
        • Vl-mark-wires-for-gateinst
        • Vl-mark-wires-for-plainarg
        • Vl-wireinfo-p
        • Vl-mark-wires-for-modulelist
        • Vl-vardecllist-impexp-names
        • Vl-report-totals
        • Vl-mark-wires-for-plainarglist
        • Vl-collect-unused-or-unset-wires
        • Vl-clean-up-warning-wires
        • Vl-print-useset-report-top
        • Vl-mark-wires-for-arguments
        • Vl-useset-report-p
        • Vl-star-names-of-warning-wires
        • Vl-design-use-set-report
        • Vl-module-impexp-names
        • Vl-make-initial-wireinfo-alist
        • Vl-mark-wire-used
        • Vl-mark-wire-set
        • Vl-mark-wires-used
        • Vl-mark-wires-for-assignment
        • Vl-mark-wires-for-assignlist
        • Vl-mark-wires-set
        • Vl-print-useset-report-full-aux
        • Vl-print-typo-alist
        • Vl-print-typo-possibilities
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Use-set

Vl-annotate-vardecllist-with-wireinfo

(vl-annotate-vardecllist-with-wireinfo x alist wwires) maps vl-annotate-vardecl-with-wireinfo across a list.

Signature

(vl-annotate-vardecllist-with-wireinfo x alist wwires) → *

This is an ordinary defprojection.

Definitions and Theorems

Function: vl-annotate-vardecllist-with-wireinfo-exec

(defun vl-annotate-vardecllist-with-wireinfo-exec
       (x alist wwires acc)
  (declare (xargs :guard (and (vl-vardecllist-p x)
                              (vl-wireinfo-alistp alist)
                              (string-listp wwires))))
  (let ((__function__ 'vl-annotate-vardecllist-with-wireinfo-exec))
    (declare (ignorable __function__))
    (if (consp x)
        (vl-annotate-vardecllist-with-wireinfo-exec
             (cdr x)
             alist wwires
             (cons (vl-annotate-vardecl-with-wireinfo (car x)
                                                      alist wwires)
                   acc))
      acc)))

Function: vl-annotate-vardecllist-with-wireinfo-nrev

(defun vl-annotate-vardecllist-with-wireinfo-nrev
       (x alist wwires nrev)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (and (vl-vardecllist-p x)
                             (vl-wireinfo-alistp alist)
                             (string-listp wwires))))
 (let ((__function__ 'vl-annotate-vardecllist-with-wireinfo-nrev))
  (declare (ignorable __function__))
  (if (atom x)
      (nrev-fix nrev)
   (let
    ((nrev
         (nrev-push (vl-annotate-vardecl-with-wireinfo (car x)
                                                       alist wwires)
                    nrev)))
    (vl-annotate-vardecllist-with-wireinfo-nrev
         (cdr x)
         alist wwires nrev)))))

Function: vl-annotate-vardecllist-with-wireinfo

(defun vl-annotate-vardecllist-with-wireinfo (x alist wwires)
 (declare (xargs :guard (and (vl-vardecllist-p x)
                             (vl-wireinfo-alistp alist)
                             (string-listp wwires))))
 (let ((__function__ 'vl-annotate-vardecllist-with-wireinfo))
  (declare (ignorable __function__))
  (mbe
     :logic
     (if (consp x)
         (cons (vl-annotate-vardecl-with-wireinfo (car x)
                                                  alist wwires)
               (vl-annotate-vardecllist-with-wireinfo (cdr x)
                                                      alist wwires))
       nil)
     :exec
     (if (atom x)
         nil
       (with-local-nrev (vl-annotate-vardecllist-with-wireinfo-nrev
                             x alist wwires nrev))))))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-update-nth

(defthm vl-annotate-vardecllist-with-wireinfo-of-update-nth
 (implies
  (<= (nfix acl2::n) (len acl2::x))
  (equal
   (vl-annotate-vardecllist-with-wireinfo
        (update-nth acl2::n acl2::v acl2::x)
        alist wwires)
   (update-nth
     acl2::n
     (vl-annotate-vardecl-with-wireinfo acl2::v alist wwires)
     (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-revappend

(defthm vl-annotate-vardecllist-with-wireinfo-of-revappend
 (equal
  (vl-annotate-vardecllist-with-wireinfo (revappend acl2::x acl2::y)
                                         alist wwires)
  (revappend
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::y alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: nthcdr-of-vl-annotate-vardecllist-with-wireinfo

(defthm nthcdr-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (nthcdr
       acl2::n
       (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (vl-annotate-vardecllist-with-wireinfo (nthcdr acl2::n acl2::x)
                                         alist wwires))
 :rule-classes ((:rewrite)))

Theorem: nth-of-vl-annotate-vardecllist-with-wireinfo

(defthm nth-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (nth acl2::n
       (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (and (< (nfix acl2::n) (len acl2::x))
       (vl-annotate-vardecl-with-wireinfo (nth acl2::n acl2::x)
                                          alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-nrev-removal

(defthm vl-annotate-vardecllist-with-wireinfo-nrev-removal
 (equal
  (vl-annotate-vardecllist-with-wireinfo-nrev
       acl2::x alist wwires nrev)
  (append
      nrev
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-exec-removal

(defthm vl-annotate-vardecllist-with-wireinfo-exec-removal
 (equal
   (vl-annotate-vardecllist-with-wireinfo-exec
        acl2::x alist wwires acl2::acc)
   (revappend
        (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
        acl2::acc))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-take

(defthm vl-annotate-vardecllist-with-wireinfo-of-take
 (implies
  (<= (nfix acl2::n) (len acl2::x))
  (equal
   (vl-annotate-vardecllist-with-wireinfo (take acl2::n acl2::x)
                                          alist wwires)
   (take
     acl2::n
     (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))))
 :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-annotate-vardecllist-with-wireinfo

(defthm
    set-equiv-congruence-over-vl-annotate-vardecllist-with-wireinfo
 (implies
  (set-equiv acl2::x acl2::y)
  (set-equiv
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::y alist wwires)))
 :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-annotate-vardecllist-with-wireinfo-when-subsetp

(defthm
      subsetp-of-vl-annotate-vardecllist-with-wireinfo-when-subsetp
 (implies
  (subsetp acl2::x acl2::y)
  (subsetp
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::y alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: member-of-vl-annotate-vardecl-with-wireinfo-in-vl-annotate-vardecllist-with-wireinfo

(defthm
 member-of-vl-annotate-vardecl-with-wireinfo-in-vl-annotate-vardecllist-with-wireinfo
 (implies
  (member acl2::k acl2::x)
  (member
      (vl-annotate-vardecl-with-wireinfo acl2::k alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-rev

(defthm vl-annotate-vardecllist-with-wireinfo-of-rev
 (equal
  (vl-annotate-vardecllist-with-wireinfo (rev acl2::x)
                                         alist wwires)
  (rev
      (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-list-fix

(defthm vl-annotate-vardecllist-with-wireinfo-of-list-fix
  (equal
       (vl-annotate-vardecllist-with-wireinfo (list-fix acl2::x)
                                              alist wwires)
       (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-append

(defthm vl-annotate-vardecllist-with-wireinfo-of-append
 (equal
  (vl-annotate-vardecllist-with-wireinfo (append acl2::a acl2::b)
                                         alist wwires)
  (append
      (vl-annotate-vardecllist-with-wireinfo acl2::a alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::b alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: cdr-of-vl-annotate-vardecllist-with-wireinfo

(defthm cdr-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (cdr (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (vl-annotate-vardecllist-with-wireinfo (cdr acl2::x)
                                         alist wwires))
 :rule-classes ((:rewrite)))

Theorem: car-of-vl-annotate-vardecllist-with-wireinfo

(defthm car-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (car (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (and (consp acl2::x)
       (vl-annotate-vardecl-with-wireinfo (car acl2::x)
                                          alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-under-iff

(defthm vl-annotate-vardecllist-with-wireinfo-under-iff
  (iff (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
       (consp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-vl-annotate-vardecllist-with-wireinfo

(defthm consp-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (consp
       (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (consp acl2::x))
 :rule-classes ((:rewrite)))

Theorem: len-of-vl-annotate-vardecllist-with-wireinfo

(defthm len-of-vl-annotate-vardecllist-with-wireinfo
 (equal
  (len (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  (len acl2::x))
 :rule-classes ((:rewrite)))

Theorem: true-listp-of-vl-annotate-vardecllist-with-wireinfo

(defthm true-listp-of-vl-annotate-vardecllist-with-wireinfo
  (true-listp
       (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires))
  :rule-classes :type-prescription)

Theorem: vl-annotate-vardecllist-with-wireinfo-when-not-consp

(defthm vl-annotate-vardecllist-with-wireinfo-when-not-consp
 (implies
   (not (consp acl2::x))
   (equal
        (vl-annotate-vardecllist-with-wireinfo acl2::x alist wwires)
        nil))
 :rule-classes ((:rewrite)))

Theorem: vl-annotate-vardecllist-with-wireinfo-of-cons

(defthm vl-annotate-vardecllist-with-wireinfo-of-cons
 (equal
  (vl-annotate-vardecllist-with-wireinfo (cons acl2::a acl2::b)
                                         alist wwires)
  (cons
      (vl-annotate-vardecl-with-wireinfo acl2::a alist wwires)
      (vl-annotate-vardecllist-with-wireinfo acl2::b alist wwires)))
 :rule-classes ((:rewrite)))

Theorem: vl-vardecllist-p-of-vl-annotate-vardecllist-with-wireinfo

(defthm vl-vardecllist-p-of-vl-annotate-vardecllist-with-wireinfo
 (implies
      (force (vl-vardecllist-p x))
      (vl-vardecllist-p
           (vl-annotate-vardecllist-with-wireinfo x alist wwires))))