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
certify-book and inspected by
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
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-
events of the book are independent of the
(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
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:
We say that a given execution of
The non-erroneous inclusion of a certified book is consistency preserving provided (a) the objects read by
include-bookfrom the certificate were the objects written there by a
certify-bookand (b) the forms read by
include-bookfrom the book itself are the forms read by the corresponding
include-bookis ``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-bookare the ones checked by
certify-book. When an uncertified
include-bookoccurs, 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 essentially contain two parts, a portcullis and a
keep. There is a third part, an
expansion-alist, in order
to record expansions if
make-event has been used, but the user
need not be concerned with that level of detail.
See portcullis to continue the guided tour through books.