• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
          • Vl-reorder-portdecls
          • Vl-reorder-vardecls
          • Vl-reorder-fundecls
            • Vl-slow-reorder-fundecl
            • Vl-fast-reorder-fundecl
          • Vl-reorder-modules
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-fundecllist-p
• Reordering-by-name

Vl-reorder-fundecls

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

Signature

(vl-reorder-fundecls names x) → sublist

Arguments

names — Guard (string-listp names).

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

Returns

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

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

Definitions and Theorems

Function: vl-reorder-fundecls

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

Theorem: vl-fundecllist-p-of-vl-reorder-fundecls

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

Theorem: vl-slow-reorder-fundecl-removal

(defthm vl-slow-reorder-fundecl-removal
  (equal (vl-slow-reorder-fundecl names x)
         (vl-reorder-fundecls names x)))

Theorem: vl-fast-reorder-fundecl-removal

(defthm vl-fast-reorder-fundecl-removal
  (implies (and (string-listp names)
                (vl-fundecllist-p x)
                (equal fal (vl-fundecllist-alist x nil)))
           (equal (vl-fast-reorder-fundecl names x fal)
                  (vl-reorder-fundecls names x))))

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

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

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

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

Theorem: vl-reorder-fundecls-of-vl-fundecllist-fix-x

(defthm vl-reorder-fundecls-of-vl-fundecllist-fix-x
  (equal (vl-reorder-fundecls names (vl-fundecllist-fix x))
         (vl-reorder-fundecls names x)))

Theorem: vl-reorder-fundecls-vl-fundecllist-equiv-congruence-on-x

(defthm vl-reorder-fundecls-vl-fundecllist-equiv-congruence-on-x
  (implies (vl-fundecllist-equiv x x-equiv)
           (equal (vl-reorder-fundecls names x)
                  (vl-reorder-fundecls 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-fundecls

(defthm subsetp-of-vl-reorder-fundecls
  (subsetp (vl-reorder-fundecls names x)
           (vl-fundecllist-fix x)))

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

Theorem: vl-fundecllist->names-of-vl-reorder-fundecls

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

Theorem: vl-fundecllist->names-of-vl-reorder-fundecls-bounded

(defthm vl-fundecllist->names-of-vl-reorder-fundecls-bounded
  (subsetp (vl-fundecllist->names (vl-reorder-fundecls 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-fundecls

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

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

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

Subtopics

Vl-slow-reorder-fundecl

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

Vl-fast-reorder-fundecl

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