|
|
|---|
|
|
|
|---|
The gate guarding the entrance to a certified book
The certificate (see certificate for general information) of a certified book contains 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 book-hash values for 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
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 contribute to the portcullis for the certified book. In addition, certify-book records in the portcullis certain book-hash values (see book-hash) for 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 book-hash). 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. Note that when
Clearly, a book is most useful if its certification takes place with as few
non-local events as possible that extend the initial logical world. If, for example, your certification world happens to contain a
defpkg for