; Best Practices Documentation ; Copyright (C) 2013-2014 Centaur Technology ; ; Contact: ; Centaur Technology Formal Verification Group ; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA. ; http://www.centtech.com/ ; ; License: (An MIT/X11-style license) ; ; Permission is hereby granted, free of charge, to any person obtaining a ; copy of this software and associated documentation files (the "Software"), ; to deal in the Software without restriction, including without limitation ; the rights to use, copy, modify, merge, publish, distribute, sublicense, ; and/or sell copies of the Software, and to permit persons to whom the ; Software is furnished to do so, subject to the following conditions: ; ; The above copyright notice and this permission notice shall be included in ; all copies or substantial portions of the Software. ; ; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING ; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER ; DEALINGS IN THE SOFTWARE. ; ; Original author: Jared Davis (in-package "ACL2") (include-book "xdoc/top" :dir :system) (defxdoc best-practices :parents (books) :short "Recommended best practices for ACL2 books." :long "

DRAFT

This is a preliminary document. Feedback is very much welcome and appreciated. Please direct feedback to the acl2-books list or to Jared Davis.

We recommend the use of the Standard Libraries (@(see std)) to ease your burden of modeling and reasoning in a formal sytem. See other subtopics below for other best practices.

If you expect your library to be used at all by other people, put your code in a package. Jared, Rager, and Kaufmann spend a large amount of time just dealing with name clashes, and it leaves them grumpy. See @(see working-with-packages).

") (local (xdoc::set-default-parents best-practices)) (defxdoc finite-reasoning :short "Use @(see gl) to reason about finitely bounded values." :long "It is often convenient to use as much automation as possible when performing proofs. @(csee gl) provides the ability to automatically reason about finite values, such as 32-bit integers. As examples, this can be quite useful when reasoning about cryptography algorithms or verifying hardware.") (defxdoc file-extensions :short "Conventions to follow for choosing file extensions like @('.lisp'), @('.lsp'), and @('.acl2') files." :long "

Recommendations

  1. Certifiable books should use the extension @('.lisp')
  2. Certification commands (\"portcullis\" stuff) should use the extension @('.acl2')
  3. Other Lisp files (package definitions, raw lisp code) should that are not certifiable books should use @('.lsp')

Rationale

These conventions allow build systems like @(see build::cert.pl) to automatically distinguish between what should be certified and what should not.

Once a user is familiar with these conventions, they act as a signal about what files are likely to be of interest.

") (defxdoc file-names :short "Restrictions to follow for naming books, directories, and other files." :long "

Recommendations

  1. All file names and directory should use strictly lower-case, printable ASCII letters.
  2. Spaces and odd punctuation characters (e.g., beyond dash, underscore, and period) should not be used.
  3. Dashes should generally be preferred over underscores.

Rationale

These name restrictions encourage portability across different operating systems, file systems, etc. (Some file systems restrict certain characters, or differ from one another with respect to case sensitivity.)

Avoiding file names with spaces and special characters helps to makes it easier to write scripts or to write quick, one-off shell commands to process the books without worrying overly much about escaping.

") (defxdoc working-with-packages :parents (best-practices packages) :short "How to set up new package and portcullis files." :long "

Recommendations

Here is a basic recipe to follow for creating new directories that make use of packages:

@('foo/package.lsp') — main package definitions
@({ ;; load other packages needed to define our new packages... ;; note that we only include portcullis files, that define ;; the packages, not the libraries which those files support (include-book \"lib1/portcullis\" :dir :system) (include-book \"lib2/portcullis\" :dir :system) ;; define our new packages (defpkg \"PKG1\" ...) (defpkg \"PKG2\" ...) ;; optionally set up useful exports lists (defconst PKG1::*pkg1-exports* ...) (defconst PKG2::*pkg2-exports* ...) })
@('foo/portcullis.lisp') — a nearly empty book
@({ ;; We need an \"in-package\" line to make this a valid book, but ;; which package doesn't matter since the rest of the book is empty. (in-package \"FOO\") })
@('foo/portcullis.acl2') — certification instructions for the portcullis book
@({ (ld \"package.lsp\") })
@('foo/cert.acl2') — certification instructions for the other books
@({ (include-book \"portcullis\") ;; cert-flags: ? t [:ttags :all ...] })
@('foo/acl2-customization.lsp') — merely for convenience
@({ (ld \"~/acl2-customization.lsp\" :ld-missing-input-ok t) (ld \"package.lsp\") (in-package \"FOO\") })

Rationale

Using the same names for @('package.lsp') and @('portcullis.lisp') is a nice convention that improves consistency and discoverability.

The empty portcullis book is a useful trick. Including this book, rather than directly @(see ld)'ing the package from @('cert.acl2'), means that when several books from the same directory are loaded into the same session, each of their individual @('.cert') files contain commands like:

@({ (include-book \"portcullis\") })

instead of:

@({ (defpkg \"FOO\" (union-eq ...)) })

This is good because ACL2 can quickly realize that the @(see include-book) form is redundant and not do any work, instead of having to re-evaluate the package commands to see if it is indeed the same.

Having a customization file that starts ACL2 up in \"the right package\" is often very convenient while developing. Loading the user's customization file first, if one exists, is nice for users who have their own macros.

It can also be good to pre-load packages like @('std') when your session starts. See @('books/std/std-customization.lsp') for an @(see acl2-customization) file that does this.

") (defxdoc theory-management :short "Recommendations related to enabling and disabling functions and theorems." :long "

The best practices depend somewhat on the kind of book you are writing. We distinguish between Widget Libraries and Core Libraries.

Widget Libraries

Scenario: your library describes a particular kind of \"Widget:\" it defines what Widgets are, provides some useful algorithms for operating on Widgets, and proves some theorems about the properties of Widgets and these algorithms.

Recommendations

  1. Avoid any non-local inclusion of arithmetic libraries
  2. Avoid any non-local @('(in-theory ...)') events that involve built-in ACL2 functions. For instance, do not do: @('(in-theory (enable append))').
  3. Try to respect the ACL2 namespace, e.g., do not define new functions in the ACL2 package, especially with short or generic names, etc.

Rationale

Core Libraries

Scenario: your library is meant to assist with reasoning about built-in ACL2 functions, for instance:

Since your library is inherently about existing ACL2 functions rather than new definitions, the Widget-library recommendations do not necessarily apply.

") (defxdoc conventional-normal-forms :short "Recommendations for respecting global conventions that the ACL2 books authors have agreed to." :long "

In many cases there are alternate normal forms that you can use for the same concept. For greater compatibility between libraries, we prefer to use various forms as described below.

Disable @(see mv-nth)

Recommendations:

  1. Write lemmas in terms of @('(mv-nth n ...)') instead of @('(caddr ...)')
  2. Include the @('tools/mv-nth') book

Rationale

BOZO Other important normal forms we should all agree on?

Member versus Memberp?

") (defsection naming-rewrite-rules :short "Recommendations for writing understandable rule names." :long "

Strong Recommendations

Do not non-locally use common names for local lemmas, such as:

@({ lemma* crock* crux* a0 b0 c0 ... temp* goal* main-goal* a1 b1 c1 stupid* wtf* corollary* ... })

Rationale

Using the above names may make your book hard to include for people who (perhaps via macros) are already using these names or who may want to use them.

Weak Recommendations

  1. For unconditional, equality-based rules, we base the rule name on a reading of the left-hand side, using @('of') as a separator. This is meant to boost readability when the function names involved have their own hyphens. Examples: @({ (defthm append-of-cons (equal (append (cons a x) y) (cons a (append x y)))) (defthm true-listp-of-append (equal (true-listp (append x y)) (true-listp y))) })
  2. For rules describing the return-type of a function, we use a similar naming convention, using @('of') as a separator. Example: @({ (defthm consp-of-cons (consp (cons x y))) })
  3. For rules with one simple hypothesis, we add @('-when-hyp') to the name. Examples: @({ (defthm member-when-atom ;; lhs is (member a x) (implies (atom x) (not (member a x)))) (defthm logbitp-of-0-when-bitp (implies (bitp b) (equal (logbitp 0 b) (equal b 1)))) })
  4. For rules about other equivalence relations, we add @('-under-equiv') to the name. Examples: @({ (defthm append-under-iff ;; lhs is (append x y) (iff (append x y) (or (consp x) y))) (defthm union-equal-under-set-equiv ;; lhs is (union-equal a b) (set-equiv (union-equal a b) (append a b))) })
  5. For rules that specify the upper limit of a function's numerical return value, we often add @('-limit').
  6. For rules that specify both the lower and upper limit of a function's numerical return value, we often add @('-bounds').

Obviously you can take this too far. For complex theorems, these recommendations would lead to names that are far too long. Think of them as a starting point, not a mandate.

Rationale

Following these conventions can help lead to more consistently named rules whose effect may be more easy to guess.

") (defxdoc where-do-i-place-my-book :parents (best-practices projects books) :short "How to decide where in the books directory structure to place your book" :long "

Here is our loose view of the books organization:

  1. project-specific stuff
  2. useful libraries not yet vetted by the 'std' maintainers
  3. libraries 'approved' for the standard approach

Books in category (1) easily belong in @('books/projects').

Books in category (2) can go in the top-level @('books') directory or in projects. There's so much stuff in the top-level directory, that we suggest @('books/projects') -- especially for people that are new to the ACL2 community.

Once general-use books are vetted by the ACL2 book Czars, they go in the @('std') directory. Some of the criteria the book czars use to decide whether a book should be in @('std') follow below:

") (defxdoc remove-whitespace :short "How to find and remove whitespace from .lisp files" :long "

Some of us are of the opinion that it's good hygiene to not allow trailing whitespaces. To see trailing-whitespaces in Emacs enable:

@({(setq-default show-trailing-whitespace t)})

To remove trailing-whitespaces from a file you have open in emacs do:

@({M-x delete-trailing-whitespace})

To find trailing whitespaces in @('.lisp') files within your current directory, in your shell do:

@({find . -name '*.lisp' -exec egrep -l \" +$\" {} \;})")