Arranging that source functions come up as guard-verified
ACL2 is maintained solely by Matt Kaufmann and J Moore. However,
we anticipate that a few others will eventually contribute as well. Here we
discuss how to put built-in functions into :logic mode. Since
ACL2 insists that its built-in :logic mode functions are guard-verified, we actually explain how to arrange that built-in :program mode functions become built-in guard-verified :logic mode
To put a system function into guard-verified :logic mode, you might
first need or want to modify your local copy of the ACL2 sources, for example
replacing (null lst) by (endp lst) in a function's definition in
support of the termination proof and then specifying (true-listp lst) in
its guard. You don't need to become a system developer to do this, but see
developers-guide if you are an experienced ACL2 user and system
development interests you. IMPORTANT: Eventually you will probably want to
undo your changes; this will be explained further below.
After making such changes, build an ACL2 executable image containing your
modified code, to test that the modified code builds. The next step is
typically to create a new file, perhaps named after the main function(s) whose
guards you want to verify, in directory books/system. Community book
books/system/too-many-ifs.lisp is a good example. Ultimately, this file
should be a certifiable book that verifies the desired termination and guards.
Include this book in books/system/top.lisp. Of course, you can instead
add to some existing file in the same directory that is already included in
books/system/top.lisp, rather than creating a new book and including it
In general, in this new file or new file addition, it is necessary to use
both verify-termination and verify-guards on the system
functions in question, in order to both put them in logic mode and verify their
guards. However, as explained in the documentation of verify-termination, sometimes verify-termination also verifies the
guards (see also set-verify-guards-eagerness). In this case, it is
good practice to add a comment `; and guards' just after the verify-termination form, on the same line, as can be seen in some of the files
under community-books directory system/.
Now it is time to add entries to the value of constant
*system-verify-guards-alist* in your local copy of the ACL2 sources,
which specifies functions whose guard-verification is completed by including
community-book books/system/devel-check.lisp (which includes
books/system/top.lisp. Each entry is of the form (function-symbol
. measure). For example, the entry (ARITY-ALISTP ACL2-COUNT ALIST)
signifies that the function symbol arity-alistp is to have measure
(acl2-count alist), while the entry (ARGLISTP) signifies that
function symbol arglistp has no measure (i.e., we use nil for the
measure), presumably because its definition is not recursive. After you make
those additions, then follow the steps below.
- Build a so-called ``devel'' copy in which the functions in
*system-verify-guards-alist* remain in :program mode. For example,
the following command will create ``devel'' executable saved_acl2d.
(time nice make ACL2_DEVEL=d) >& make-devel.log
- Check that the build seems to have worked, for example by finding the
string "Successfully built" near the end of your log file.
- Run a ``devel'' regression, for example as follows if starting in the ACL2
sources directory. Note that including ``ACL2_USELESS_RUNES= '' as shown
below may be necessary because of how proofs differ between normal and
``devel'' versions of ACL2.
make clean-books ACL2=`pwd`/saved_acl2d
(time nice make -j 8 \
The last of these commands should run much more quickly than a normal
regression. You can of course check on it as follows.
- Check that there are no errors, by checking that the following produces no
fgrep -a '**' make-devel-regression.log
- Run the following check from your ACL2 sources directory.
make devel-check ACL2=`pwd`/saved_acl2d
You should see output like the following.
SUCCESS for chk-new-verified-guards
SUCCESS for check-system-events
SUCCESS for devel-check
- Now clean the books (see make clean-books above) and then do a normal
build and regression.
- Finally, send your changes to Matt Kaufmann, with a request that they be
incorporated into the ACL2 sources and books.
We now return to the remark labeled ``IMPORTANT'' above: undoing your
changes. This isn't necessary if you will not be using that local copy of
ACL2 in the future. But otherwise you may run into problems when you try to
use git to merge changes into that local ACL2+books copy. One option is to
throw your changes away by standing in your local ACL2 directory and using the
shell command: git checkout -f. But be careful — this will throw
away all your work! So you might want to wait until your changes make it into
the main (master) git branch.