How we know if include-book read the correct files
The certificate (see certificate for general information) of a certified file contains a portcullis and a keep. These names come from castle lore. The keep is the strongest and usually tallest tower of a castle from which the entire courtyard can be surveyed by the defenders. The keep of a book is a list of file names and book-hash values used after the book has been included, to determine if the files read were (up to book-hash) those certified.
Once the portcullis is open, include-book can enter the book and read the event forms therein. The non-local event forms are in fact executed, extending the host theory. That may read in other books. When that has been finished, the keep of the certificate is inspected. The keep is a list of the book names which are included (hereditarily through all sub-books) in the certified book (including the certified book itself) together with the book-hash values for those books at the time of certification. We compare the book-hash values of the books just included to those of the books stored in the keep. If differences are found then we know that the book or one of its sub-books has been changed since certification.