Invalid certificates and uncertified books
For relevant background see books, see certificate,
and see portcullis.
Include-book has a special provision for dealing with an
uncertified book, i.e., a file with no certificate or an invalid certificate (i.e., one whose book-hash values describe files other
than the ones actually read). In this case, a warning is printed and the book
is otherwise processed much as though it were certified and had an open portcullis.
If a book B.lisp is uncertified and a file B.port exists, then
the forms in B.port are evaluated before the forms in B.lisp. Such
a file B.port is typically created calling certify-book on book
"B" with argument :write-port t, so that B.port contains the
portcullis commands for B (the commands present in the
world when that certification was attempted). To avoid loading
.port files, see compilation.
Inclusion of uncertified books can be handy, but it can have disastrous
The provision allowing uncertified books to be included 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.