|
|
|---|
|
|
|
|---|
A file specifying validity of a given book
A book, say
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. Book-hash values are used to help detect such problems, but provide imperfect security: two different files can have the same book-hash.
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 book-hash 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.
Certificates contain a portcullis and a keep, each documented
later in this guided tour through books. We mention here two other
parts, which we do not document elsewhere because we view them as
implementation details: an
See portcullis to continue the guided tour through books.