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 (
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.
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
(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
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.