		Search-engine friendly clone of the ACL2 documentation.

Verify-guards-for-system-functions

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

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

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
cd books
(time nice make -j 8 \
           ACL2=`pwd`/../saved_acl2d \
           ACL2_USELESS_RUNES= \
           system/devel-check.cert) \
  >& make-devel-regression.log&
```
The last of these commands should run much more quickly than a normal regression. You can of course check on it as follows.
```
tail make-devel-regression.log
```
Check that there are no errors, by checking that the following produces no output.
```
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.