Certify-book
How to produce a certificate for a book
Also see certificate for information about the
".cert" file produced by certify-book, in particular for
information about the use of book-hash values to help ensure that the
corresponding book has not been modified since certification. See certify-book-debug for some potential remedies for failures of
certify-book.
Examples:
(certify-book "my-arith") ; certify in a world with 0 commands
(certify-book "my-arith" 3) ; ... in a world with 3 commands
(certify-book "my-arith" ?) ; ... in a world without checking the
; number of commands
(certify-book "my-arith" 0 nil) ; ... without compilation
(certify-book "my-arith" 0 t) ; ... with compilation (default)
(certify-book "my-arith" 0 t :ttags (foo))
; ... allowing trust tag (ttag) foo
(certify-book "my-arith" 0 t :ttags :all)
; ... allowing all trust tags (ttags)
(certify-book "my-arith" 0 nil :acl2x t)
; ... writing or reading a .acl2x file
(certify-book "my-arith" 0 t :useless-runes :write)
; ... write file to speed up future proofs
(certify-book "my-arith" 0 t :useless-runes :read)
; ... read file to speed up future proofs
General Form:
(certify-book book-name
k ; [default 0]
compile-flg ; [default t]
:defaxioms-okp t/nil ; [default nil]
:skip-proofs-okp t/nil ; [default nil]
:ttags ttags ; [default nil]
:acl2x t/nil ; [default nil]
:ttagsx ttags ; [default nil]
:pcert pcert ; [default nil]
:write-port t/nil ; [default t unless pcert is non-nil]
:useless-runes ; :write/:read/:read?/n/-n/nil
; (-100 < n < 0 or 0 < n <= 100)
; [default nil or from environment]
:write-event-data ; [default nil or from environment]
)
where book-name is a book filename, k is used to indicate your
approval of the ``certification world,'' and compile-flg can
control whether the book is to be compiled. The defaults for
compile-flg, skip-proofs-okp, acl2x, write-port,
pcert, :useless-runes, and :write-event-data can be affected by
environment variables. All of these arguments are described in detail below,
except for :pcert, :useless-runes, and :write-event-data: see
provisional-certification, useless-runes, and saving-event-data, respectively, for the effects of these three arguments and
related environment variables, as we ignore those effects in the present
topic.
NOTE: If a given book includes some books (see include-book), then
those included books need to be certified before the given book is certified.
See build::cert.pl for a tool that certifies not only a given book but
also all of the books that it includes, as well as all the books that those
books include, and so on — all in the proper order, and with parallelism
by using the -j option.
Certification occurs in some logical world, called the
``certification world.'' That world must contain the defpkgs needed to read and execute the forms in the book. The commands necessary to recreate that world from the ACL2 initial world are called the ``portcullis commands,'' and will be copied into
the certificate created for the book. Those commands will be
re-executed whenever the book is included, to ensure that the appropriate
packages (and all other names used in the certification world) are
correctly defined. Note that Step 1 of certify-book will fail if a
package mentioned in the book is not defined before attempting the
certification, i.e., defined by a portcullis command in the certification
world. For example, suppose that your book contains the symbol FOO::X,
but the package "FOO" is not currently defined. Then an error message will
likely complain either about a missing package "FOO", or about a symbol
FOO::X that is ``not in any of the packages known to ACL2.'' A solution
is to define the package "FOO", perhaps directly using defpkg or by
including a book that defines this package, before attempting the
certification.
The certified book will be more often usable if the certification world is kept to a minimal extension of the ACL2 initial world (for
example, to prevent name clashes with functions defined in other books, or to
avoid including undesired rules). Alternatively, use local events to build your certification world, as these will be skipped when
including the certified book. But perhaps it's simplest just to get into the
initial ACL2 world (e.g., with :ubt 1 or by just starting a new
ACL2 run), then define the desired packages (directly with defpkg or
by including books that define the packages), and finally invoke
certify-book.
The k argument to certify-book has default value 0, and it
must be either a nonnegative integer or else the symbol ? in any package.
If k is an integer, then it must be the number of commands that
have been executed after the initial ACL2 world to create the world in which certify-book was called. One way to obtain this number
is by doing :pbt :start to see all the commands back to the first
one.
Otherwise, k is ? (or any symbol whose symbol-name is
"?"). In that case there is no check made on the certification world.
This can be a nice convenience but at the cost of eliminating a potentially
valuable check that the certification world may be as expected.
We next describe the meaning of compile-flg and how it defaults. If
explicit compilation has been suppressed by (set-compiler-enabled nil
state), then compile-flg is coerced to nil; see compilation. Otherwise compile-flg may be given the value of t (or
:all, which is equivalent to t except during provisional
certification; see provisional-certification), indicating that the book
is to be compiled, or else nil. (Note that compilation initially creates
a compiled file with a temporary file name, and then moves that temporary file
to the final compiled file name obtained by adding a suitable extension to the
book's filename. Thus, a compiled file will appear atomically in its intended
location.) Finally, if compile-flg is not supplied (or is :default)
then it is treated as t. Note that the value :all is equivalent to
t except for during the Convert procedure of provisional certification;
see provisional-certification.
Two keyword arguments, :defaxioms-okp and :skip-proofs-okp,
determine how the system handles the inclusion of defaxiom events and
skip-proofs events, respectively, in the book. The value t
allows such events, but prints a warning message. The value nil causes
an error if such an event is found. Nil is the default unless keyword
argument :acl2x t is provided and state global 'write-acl2x is a
cons (see set-write-ACL2x), in which case the default is t.
The keyword argument :ttags may normally be omitted. A few
constructs, used for example if you are building your own system based on
ACL2, may require it. See defttag for an explanation of this
argument.
When book B is certified with value t (the default, unless the
value used for pcert is non-nil) for keyword argument
:write-port, a file B.port is written by certification process.
This file contains all of the portcullis commands for B,
i.e., all user commands present in the ACL2 logical world at the time
certify-book is called. If B.lisp later becomes uncertified, say
because events from that file or an included book have been edited,
then (include-book "B") will consult B.port to evaluate forms in
that file before evaluating the events in B.lisp. On the other hand,
B.port is ignored when including B if B is certified.
If you use guards, please note certify-book is executed as
though (set-guard-checking t) has been evaluated; see set-guard-checking. If you want to run with different guard-checking,
consider using ld instead, or in addition; see ld.
For a general discussion of books, see books. Certify-book is
akin to what we have historically called a ``proveall'': all the forms in the
book are ``proved'' to guarantee their admissibility. More precisely,
certify-book (1) reads the forms in the book, confirming that the
appropriate packages are defined in the certification world; (2) does
the full admissibility checks on each form (proving termination of recursive
functions, proving theorems, etc.), checking as it goes that each form is an
embedded event form (see embedded-event-form); (3) may roll back the
logical world (how far? — see below) and perform an include-book to check for local incompatibilities (see local-incompatibility); (4) writes a certificate recording not only
that the book was certified but also recording the commands necessary
to recreate the certification world (so the appropriate packages can be
defined when the book is included in other worlds) and a book-hash for each of the books involved (see certificate); and
(5) compiles the book if so directed (and then loads the object file in that
case).
Certify-book is a macro that returns an error-triple, where
success is indicated by an error component of nil and has the effect of
extending the world with a corresponding include-book event.
If you don't want the included book's events in your present world, simply execute :u.
Remark. Step (3) above mentions rolling back the logical world to
check for local incompatibilities. This process is skipped if no local
event is encountered. Otherwise, the world is rolled back through the first
local event past the boot-strap world — see local-incompatibility
— before the book is included. Note that if that first local event is
in the certification world, then all commands from that event onward will be
rolled back. See fast-cert for a way to skip entirely this process of
roll-back and check, regardless of local events, but with a risk to soundness.
End of Remark.
A utility is provided to assist in debugging failures of certify-book;
see redo-flat.)
Certify-book requires that the default defun-mode (see default-defun-mode) be :logic when certification is attempted.
If the mode is not :logic, an error is signaled.
An error will occur if certify-book has to deal with any uncertified
book other than the one on which it was called. For example, if the book
being certified includes another book, that sub-book must already have been
certified; that is, that sub-book must have a valid certificate
file.
If you have a certified book that has remained unchanged for some time you
might well not remember the appropriate defpkgs for it, though they
are stored in the certificate file and (by default) also in the
.port file. If you begin to change the book, don't throw away its certificate file just because it has become invalid! It is an important
historical document until the book is re-certified. More important, don't
throw away the .port file, as it will provide the portcullis
commands when including the book as an uncertified book; see include-book.
When certify-book is directed to produce a compiled file, it calls the
Common Lisp function compile-file on the original source file. This
creates a compiled file with an extension known to ACL2, e.g., if the book is
named "my-book" then the source file is "my-book.lisp" and the
compiled file under GCL will be "my-book.o" while under SBCL it will be
"my-book.fasl". The compiled file is then loaded. When include-book is used later on "my-book" it will automatically load the
compiled file, provided the compiled file has a later write date than the
source file. The only effect of such compilation and loading is that
the functions defined in the book execute faster. See guard for a
discussion of the issues, and if you want more details about books and
compilation, see book-compiled-file.
When certify-book is directed not to produce a compiled file, it will
delete any existing compiled file for the book, so as not to mislead include-book into loading the now outdated compiled file. Otherwise,
certify-book will create a temporary ``expansion file'' to compile,
obtained by appending the string "@expansion.lsp" to the end of the book's
filename. Remark: Users may ignore that file, which is automatically deleted
unless state global variable 'save-expansion-file has been set,
presumably by a system developer, to a non-nil value; see book-compiled-file for more information about this issue, including the role
of environment variable ACL2_SAVE_EXPANSION.
After execution of a certify-book form, the value of ACL2-defaults-table is restored to what it was immediately before that
certify-book form was executed. See ACL2-defaults-table.
Those who use the relatively advanced features of trust tags (see defttag) and make-event may wish to know how to create a certificate file that avoids dependence on trust tags that are used only
during make-event expansion. For this, including documentation of the
:acl2x and :ttagsx keyword arguments for certify-book, see
set-write-ACL2x.
This completes the tour through the documentation of books.
Subtopics
- Useless-runes
- Speed up proofs by disabling useless runes
- Fast-cert
- A mode for faster, but possibly unsound, book certification
- Certify-book-debug
- Some possible ways to work around certify-book failures
- Certify-book!
- A variant of certify-book
