CERTIFICATE

how a book is known to be admissible and where its defpkgs reside 
Major Section:  BOOKS

A book, say "arith", is said to have a ``certificate'' if there is a file named "arith.cert". Certificates are created by the function certify-book and inspected by include-book. Check sums are used to help ensure that certificates are legitimate and that the corresponding book has not been modified since certification. But because the file system is insecure and check sums are not perfect it is possible for the inclusion of a book to cause inconsistency even though the book carries an impeccable certificate.

The certificate includes the version number of the certifying ACL2. A book is considered uncertified if it is included in an ACL2 with a different version number.

The presence of a ``valid'' certificate file for a book attests to two things: all of the events of the book are admissible in a certain extension of the initial ACL2 logic, and the non-local events of the book are independent of the local ones (see local-incompatibility). In addition, the certificate contains the commands used to construct the world in which certification occurred. Among those commands, of course, are the defpkgs defining the packages used in the book. When a book is included into a host world, that world is first extended by the commands listed in the certificate for the book. Unless that causes an error due to name conflicts, the extension ensures that all the packages used by the book are identically defined in the host world.

Security:

Because the host file system is insecure, there is no way ACL2 can guarantee that the contents of a book remain the same as when its certificate was written. That is, between the time a book is certified and the time it is used, it may be modified. Furthermore, certificates can be counterfeited. Check sums (see check-sum) are used to help detect such problems. But check sums provide imperfect security: two different files can have the same check sum.

Therefore, from the strictly logical point of view, one must consider even the inclusion of certified books as placing a burden on the user:

The non-erroneous inclusion of a certified book is consistency preserving provided (a) the objects read by include-book from the certificate were the objects written there by a certify-book and (b) the forms read by include-book from the book itself are the forms read by the corresponding certify-book.

We say that a given execution of include-book is ``certified'' if a certificate file for the book is present and well-formed and the check sum information contained within it supports the conclusion that the events read by the include-book are the ones checked by certify-book. When an uncertified include-book occurs, warnings are printed or errors are caused. But even if no warning is printed, you must accept burdens (a) and (b) if you use books. These burdens are easier to live with if you protect your books so that other users cannot write to them, you abstain from running concurrent ACL2 jobs, and you abstain from counterfeiting certificates. But even on a single user uniprocessor, you can shoot yourself in the foot by using the ACL2 io primitives to fabricate an inconsistent book and the corresponding certificate.

Note that part (a) of the burden described above implies, in particular, that there are no guarantees when a certificate is copied. When books are renamed (as by copying them), it is recommended that their certificates be removed and the books be recertified. The expectation is that recertification will go through without a hitch if relative pathnames are used. See pathname, which is not on the guided tour.

Certificate essentially contain two parts, a portcullis and a keep. See portcullis to continue the guided tour through books.