the gate guarding the entrance to a certified book
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.

See keep to continue the guided tour of books.