		Search-engine friendly clone of the ACL2 documentation.

Books

Uncertified-books

Invalid certificates and uncertified books

For relevant background see books, see books-tour, see certificate, and see portcullis.

You may have been led to this topic by a warning or error message such as the following.

There is no certificate on file for /u/smith/foo.lisp.  See :DOC
uncertified-books.

The remedy is to certify the indicated book; see certify-book. Such certification is typically a very good idea, as discussed further below. After certification succeeds, the book will have a valid certificate and the message will no longer be printed. The rest of this topic explains issues pertaining to books that are uncertified, that is, have not been certified.

Include-book has a special provision for dealing with an uncertified book, i.e., a file whose certificate is missing or invalid (e.g., one for a different ACL2 version or whose book-hash value describes a file other than the one actually read). In this case, a warning is printed (as above) and the book is usually processed much as though it were certified. If a book B.lisp was previously certified, it will probably have a corresponding file B.port representing the portcullis commands for that previous certification. (See keyword argument :write-port of certify-book.) Then if B.lisp is currently uncertified and B.port exists, evaluation of (include-book "B") will cause the forms in B.port to be evaluated before the forms in B.lisp. To avoid such evaluation for .port files, see compilation.

The ability to include uncertified books is handy but it can have disastrous consequences, ranging from hard lisp errors, to damaged memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the logic inconsistent. For example, one of its non-local events might be (defthm t-is-nil (equal t nil)). It is also possible for the inclusion of an uncertified book to cause hard errors or breaks into raw Common Lisp. For example, if the file has been edited since it was certified, it may contain too many open parentheses, causing Lisp to read past ``end of file.'' Similarly, it might contain non-ACL2 objects such as 3.1415 or ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a suitable extension of ACL2's initial world), its uncertified inclusion might cause Lisp errors or inconsistencies! For example, it might mention packages that do not exist in the host world, especially if the .port file (discussed above) does not exist from an earlier certification attempt. The portcullis of a certified book ensures that the correct defpkgs have been admitted, but if a book is read without actually raising its portcullis, symbols in the file, e.g., acl2-arithmetic::fn, could cause ``unknown package'' errors in Common Lisp. Perhaps the most subtle disaster occurs if the host world does have a defpkg for each package used in the book but the host defpkg imports different symbols than those required by the portcullis. In this case, it is possible that formulas which were theorems in the certified book are non-theorems in the host world, but those formulas can be read without error and will then be quietly assumed.

In short, if you include an uncertified book, all bets are off regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors don't occur, the chances are that deductions after the inclusion of an uncertified book are probably justified in the (possibly inconsistent) logical extension obtained by assuming the admissibility and validity of the definitions and conjectures in the book.