1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
<html>
<head><title>KEEP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>KEEP</h2>how we know if <code><a href="INCLUDE-BOOK.html">include-book</a></code> read the correct files
<pre>Major Section: <a href="BOOKS.html">BOOKS</a>
</pre><p>
The certificate (see <a href="CERTIFICATE.html">certificate</a> for general information) of a
certified file is divided into two parts, a <a href="PORTCULLIS.html">portcullis</a> 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 check sums used after the book has been
included, to determine if the files read were (up to check sum)
those certified.
<p>
Once the <a href="PORTCULLIS.html">portcullis</a> is open, <code><a href="INCLUDE-BOOK.html">include-book</a></code> can enter the book
and read the event forms therein. The non-<code><a href="LOCAL.html">local</a></code> event forms are
in fact executed, extending the host theory. That may read in other
<a href="BOOKS.html">books</a>. When that has been finished, the keep of the
<a href="CERTIFICATE.html">certificate</a> is inspected. The keep is a list of the book names
which are included (hereditarily through all subbooks) in the
certified book (including the certified book itself) together with
the check sums of the objects in those <a href="BOOKS.html">books</a> at the time of
certification. We compare the check sums of the <a href="BOOKS.html">books</a> just included
to the check sums of the <a href="BOOKS.html">books</a> stored in the keep. If differences
are found then we know that the book or one of its subbooks has been
changed since certification.<p>
See <a href="INCLUDE-BOOK.html">include-book</a> to continue the guided tour through <a href="BOOKS.html">books</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
