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
Inclusion of uncertified books can be handy, but it can have disastrous consequences.
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
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
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.