		Search-engine friendly clone of the ACL2 documentation.

Books

Book-hash

Assigning ``often unique'' fingerprints to books

ACL2 provides a certification process for recording into a certificate file that a book is valid. That process records certain ``fingerprint'' values for the book and the books that it includes, in order to give some confidence in the book's validity. We call that value the ``book-hash'' for the book. By default, a book-hash is an alist that records, for a given book (.lisp file), its file size (in bytes) and its write-date.

You can arrange for a book-hash to be a checksum instead of an alist, which gives a bit greater security, as illustrated in an example provided below. See checksum. Nevertheless, the (default) use of book-hash alists may be worthwhile, in spite of the decreased security, because of faster times for certify-book and include-book when using book-hash alists instead of checksums. If you want to use checksums, however, there are these two ways to do so.

Before starting ACL2, set environment variable ACL2_BOOK_HASH_ALISTP to NIL (or nil; actually it suffices that string-upcase applied to the indicated string is "NIL"). A common way to get this effect is to supply the argument ACL2_BOOK_HASH_ALISTP=NIL with your "make" command.
After starting ACL2, set state global variable book-hash-alistp to nil, e.g.: (assign book-hash-alistp nil). (Set this variable to t to revert to the default behavior: (assign book-hash-alistp t).)

The simple example below illustrates the potential weakness of book-hash alists (as compared to checksums), by exploiting the fact that these alists do not hash information in the certificate itself. (Book-hash alists also ignore portcullis commands and the corresponding .acl2x file, if any (see set-write-ACL2x); but we don't exploit these facts in this example.) We start with the following book, "foo.lisp".

(in-package "ACL2")
(make-event '(defun foo (x) (cons x x)))

Now start ACL2 and run these commands.

(assign book-hash-alistp t) ; a no-op, by default
(certify-book "foo")
(read-file "foo.cert" state)
(quit)

Next, replace the contents of "foo.cert" by the values in the list printed by the read-file form above (hence, without the outer parentheses). Further edit that file by twice changing (cons x x) to x. Also, update the write-date on the compiled file, e.g. with touch foo.dx64fsl, if you want to avoid a warning. Then submit (include-book "foo"). We get the following contradictory behavior, without any warnings.

ACL2 !>(foo 3)
(3 . 3)
ACL2 !>(thm (equal (foo x) x))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION FOO))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  5

Proof succeeded.
ACL2 !>

For more information about connections between book-hash values and certification status, see book-hash-mismatch.

Subtopics

Book-hash-mismatch: Deeming a book uncertified because of a book-hash mismatch