• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
          • Vl-reorder-portdecls
            • Vl-slow-reorder-portdecl
            • Vl-fast-reorder-portdecl
          • Vl-reorder-vardecls
          • Vl-reorder-fundecls
          • Vl-reorder-modules
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-portdecllist-p
• Reordering-by-name

Vl-reorder-portdecls

Collect a subset of a vl-portdecllist-p by their names, according to a given name ordering.

Signature

(vl-reorder-portdecls names x) → sublist

Arguments

names — Guard (string-listp names).

x — Guard (vl-portdecllist-p x).

Returns

sublist — Type (vl-portdecllist-p sublist).

This is a basic reordering function; see reordering-by-name.

Definitions and Theorems

Function: vl-reorder-portdecls

(defun vl-reorder-portdecls (names x)
  (declare (xargs :guard (and (string-listp names)
                              (vl-portdecllist-p x))))
  (let ((__function__ 'vl-reorder-portdecls))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (atom names)) nil)
              (decl (vl-find-portdecl (car names) x))
              ((when decl)
               (cons decl
                     (vl-reorder-portdecls (cdr names) x))))
           (vl-reorder-portdecls (cdr names) x))
         :exec
         (b* (((unless (and (longer-than-p 6 names)
                            (acl2::worth-hashing x)))
               (vl-slow-reorder-portdecl names x))
              (fal (make-fast-alist (vl-portdecllist-alist x nil)))
              (ans (vl-fast-reorder-portdecl names x fal)))
           (fast-alist-free fal)
           ans))))

Theorem: vl-portdecllist-p-of-vl-reorder-portdecls

(defthm vl-portdecllist-p-of-vl-reorder-portdecls
  (b* ((sublist (vl-reorder-portdecls names x)))
    (vl-portdecllist-p sublist))
  :rule-classes :rewrite)

Theorem: vl-slow-reorder-portdecl-removal

(defthm vl-slow-reorder-portdecl-removal
  (equal (vl-slow-reorder-portdecl names x)
         (vl-reorder-portdecls names x)))

Theorem: vl-fast-reorder-portdecl-removal

(defthm vl-fast-reorder-portdecl-removal
  (implies (and (string-listp names)
                (vl-portdecllist-p x)
                (equal fal (vl-portdecllist-alist x nil)))
           (equal (vl-fast-reorder-portdecl names x fal)
                  (vl-reorder-portdecls names x))))

Theorem: vl-reorder-portdecls-of-string-list-fix-names

(defthm vl-reorder-portdecls-of-string-list-fix-names
  (equal (vl-reorder-portdecls (string-list-fix names)
                               x)
         (vl-reorder-portdecls names x)))

Theorem: vl-reorder-portdecls-string-list-equiv-congruence-on-names

(defthm vl-reorder-portdecls-string-list-equiv-congruence-on-names
  (implies (str::string-list-equiv names names-equiv)
           (equal (vl-reorder-portdecls names x)
                  (vl-reorder-portdecls names-equiv x)))
  :rule-classes :congruence)

Theorem: vl-reorder-portdecls-of-vl-portdecllist-fix-x

(defthm vl-reorder-portdecls-of-vl-portdecllist-fix-x
  (equal (vl-reorder-portdecls names (vl-portdecllist-fix x))
         (vl-reorder-portdecls names x)))

Theorem: vl-reorder-portdecls-vl-portdecllist-equiv-congruence-on-x

(defthm vl-reorder-portdecls-vl-portdecllist-equiv-congruence-on-x
  (implies (vl-portdecllist-equiv x x-equiv)
           (equal (vl-reorder-portdecls names x)
                  (vl-reorder-portdecls names x-equiv)))
  :rule-classes :congruence)

We prove some basic correctness properties. To start, the list we get back is always a subset of the original list (modulo fixing).

Theorem: subsetp-of-vl-reorder-portdecls

(defthm subsetp-of-vl-reorder-portdecls
  (subsetp (vl-reorder-portdecls names x)
           (vl-portdecllist-fix x)))

Furthermore, the names we get back for are the names we asked for.

Theorem: vl-portdecllist->names-of-vl-reorder-portdecls

(defthm vl-portdecllist->names-of-vl-reorder-portdecls
 (implies
      (subsetp (double-rewrite names)
               (vl-portdecllist->names x))
      (equal (vl-portdecllist->names (vl-reorder-portdecls names x))
             (list-fix names))))

Theorem: vl-portdecllist->names-of-vl-reorder-portdecls-bounded

(defthm vl-portdecllist->names-of-vl-reorder-portdecls-bounded
  (subsetp (vl-portdecllist->names (vl-reorder-portdecls names x))
           (string-list-fix names)))

For stronger correctness properties, we need to know that the names in x are unique. After all, our finding functions rely on this, and won't return any "shadowed" objects in the list.

Theorem: member-of-vl-reorder-portdecls

(defthm member-of-vl-reorder-portdecls
  (implies (and (no-duplicatesp-equal (vl-portdecllist->names x))
                (force (vl-portdecllist-p x)))
           (iff (member a (vl-reorder-portdecls names x))
                (and (member a x)
                     (member (vl-portdecl->name a)
                             (string-list-fix names))))))

Theorem: vl-reorder-portdecls-under-set-equiv

(defthm vl-reorder-portdecls-under-set-equiv
  (implies (and (no-duplicatesp-equal (vl-portdecllist->names x))
                (set-equiv (double-rewrite (string-list-fix names))
                           (vl-portdecllist->names x)))
           (set-equiv (vl-reorder-portdecls names x)
                      (vl-portdecllist-fix x))))

Subtopics

Vl-slow-reorder-portdecl

Non fast-alist version of vl-reorder-portdecls, used when the lists are really short.

Vl-fast-reorder-portdecl

Fast-alist enhanced version of vl-reorder-portdecls.