Major Section: BOOKS
The certificate (see certificate for general information) of a
certified file is divided into two parts, a portcullis and a
keep. These names come from castle lore. The portcullis of a
castle is an iron grate that slides up through the ceiling of the
tunnel-like entrance. The portcullis of a book ensures that
include-book does not start to read the book until the
appropriate context has been created.
Technically, the portcullis consists of the version number of
the certifying ACL2, a list of commands used to create the
``certification world'' and an alist specifying the check sums
of all the books included in that world. The portcullis
is constructed automatically by certify-book from the world
in which certify-book is called, but that world must have
certain properties described below. After listing the properties we
discuss the issues in a more leisurely manner.
Each command in the portcullis must be either a defpkg form or an
embedded event form (see embedded-event-form).
Consider a book to be certified. The book is a file containing
event forms. Suppose the file contains references to such symbols
as my-pkg::fn and acl2-arith::cancel, but that the book itself
does not create the packages. Then a hard Lisp error would be
caused merely by the attempt to read the expressions in the book.
The corresponding defpkgs cannot be written into the book itself
because the book must be compilable and Common Lisp compilers differ
on the rules concerning the inline definition of new packages. The
only safe course is to make all defpkgs occur outside of compiled
files.
More generally, when a book is certified it is certified within some
logical world. That ``certification world'' contains not only
the necessary defpkgs but also, perhaps, function and constant
definitions and maybe even references to other books. When
certify-book creates the certificate for a file it recovers
from the certification world the commands used to create that
world from the initial ACL2 world. Those commands become
part of the portcullis for the certified book. In addition,
certify-book records in the portcullis the check sums
(see check-sum) of all the books included in the certification
world.
Include-book presumes that it is impossible even to read the
contents of a certified book unless the portcullis can be
``raised.'' To raise the portcullis we must be able to execute
(possibly redundantly, but certainly without error), all of the
commands in the portcullis and then verify that the books thus
included were identical to those used to build the certification
world (up to check sum). This raising of the portcullis must
be done delicately since defpkgs are present: we cannot even read
a command in the portcullis until we have successfully executed the
previous ones, since packages are being defined.
Clearly, a book is most useful if it is certified in the most
elementary extension possible of the initial logic. If, for
example, your certification world happens to contain a
defpkg for "MY-PKG" and the function foo, then those
definitions become part of the portcullis for the book. Every time
the book is included, those names will be defined and will have to
be either new or redundant (see redundant-events). But if
those names were not necessary to the certification of the book,
their presence would unnecessarily restrict the utility of the book.