Quoting the instructions:
"The README file should contain the following information:"
============================================================
"team members and contact information (email);"
Jared Davis (jared@centtech.com)
Matt Kaufmann (kaufmann@cs.utexas.edu)
J Strother Moore (moore@cs.utexas.edu)
Sol Swords (sswords@centtech.com)
============================================================
"detailed description of the submitted solutions: properties that
have been specified and/or proved, restrictions and/or
generalizations, anything that may facilitate the review":
Our solutions, which are input files for ACL2 Version 4.3, solve all
parts of all of the problems. We put each problem into its own
directory, as instructed.
Each problem's directory has two files ("books"):
1. foo.lisp the "top book"
2. foo-proof.lisp the "proof book"
The top book contains all the definitions and theorems that constitute
a solution; comments clearly mark the association of problem
statements with their solutions.
The proof book is subsidiary to the top-level book, and contains all
input necessary to lead ACL2 to prove the necessary theorems.
This separation is intended to facilitate your review: you can look at
the top book to evaluate our definitions and the theorems we have
proven, without the distracting details of the lemmas and hints we
have provided. Then, once you are convinced that the problems have
been formulated correctly, you can inspect the proof file to see how
the proof was carried out.
At the end of this README is some introductory information about ACL2
that may further help to facilitate the review.
============================================================
"detailed instructions to replay the solutions, including the
software to use, URLs to get it from, compilation commands, etc."
Our proofs are for ACL2 version 4.3. You will need to build ACL2 and
certify its books ("make regression"). Below we give an abbreviated
but sufficient set of instructions, followed by a detailed
self-contained sequence of instructions. Take your pick!
..... Short version of instructions: .....
For a detailed installation guide, please see the following web page:
http://www.cs.utexas.edu/users/moore/acl2/v4-3/installation/installation.html
Once ACL2 is installed and its books are certified, please edit
Makefile.include (in the same directory as this README) to set up the
ACL2_DIR variable.
Finally, please run "make" in the same directory as this README. This
should certify the books for our solutions.
..... Complete step-by-step instructions: .....
The following instructions are for Linux. We will refer to the full
pathname of the directory of our contribution, without the trailing
slash (/), as "$DIR"; that is, $DIR is the directory of this README.
We refer below to a process of book certification, which runs ACL2 on
a specified file ("book") that contains definitions and theorems and,
if all proofs and other checks are successful, writes out a
"certificate", which is a file with extension ".cert" that is checked
when we later "include" that book.
Step 1: Fetch ACL2 Version 4.3 and extract.
wget http://www.cs.utexas.edu/users/moore/acl2/v4-3/distrib/acl2.tar.gz
tar xfz acl2.tar.gz
Step 2: Fetch a current Lisp implementation, CCL. (Note: ACL2 runs on
Allegro CL, CCL, CLISP, CMUCL, GCL (non-ANSI), Lispworks, and SBCL.
If you already have such a Lisp implementation installed, then you can
skip this step and make the obvious corresponding modifications to
subsequent instructions.)
mkdir ccl
cd ccl
svn co -r 15050 http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx86/ccl
Step 3: Build CCL. The "? " shown below is the CCL prompt. NOTE: if
you are on a 32-bit machine, replace "lx86cl64" by "lx86cl".
pushd ccl
./lx86cl64
? (rebuild-ccl :full t)
? (quit)
./lx86cl64
? (rebuild-ccl :full t)
? (quit)
popd
Step 4: Complete the installation of CCL, simply by editing the file
$DIR/ccl, as indicated in that file. (Recall that by "$DIR" we mean
the directory full pathname for our contribution, i.e., the directory
of this README.)
Step 5: Build ACL2. This takes a minute or two, and creates an
executable file saved_acl2.
cd ../acl2-sources
make LISP=$DIR/ccl >& make.log
Step 6: Certify the ACL2 distributed books. Below, we use "-j 8"
under the assumption that you have 8 cores available (or 4 cores with
hyper-threading, etc.). Our run using this command took just under 25
minutes on a fast machine, but it could take significantly longer on a
slower machine or with a lower -j setting.
(time nice make -j 8 certify-books) >& make-certify-books.log&
Step 7: Certify our contributed solutions. First, edit the file
$DIR/Makefile.include as indicated at the top of that file. Then:
cd $DIR
make
============================================================
Finally, here is some introductory information about ACL2 that will
help to facilitate the review.
The language of ACL2 is an applicative subset of the ANSI standard
programming language Common Lisp, extended with a few additional
primitives. There are at least seven industrial-strength versions of
Common Lisp: Allegro Common Lisp, CCL (OpenMCL), CLisp, CMU Common
Lisp, GCL, LispWorks, and SBCL. ACL2 can be built and run on any of
them.
While Lisp has been around for 40 years and ACL2 for more than 20
years, we realize that not all members of the PL community are
familiar with Lisp. We are happy to provide additional explanations
upon request. Here we describe some key aspects of ACL2 that are
useful for understanding our solutions:
A. Preliminaries, foundations, etc.
B. Termination
C. "Type checks" like array bounds checking
---------- A. Foundations etc. ----------
The ACL2 home page is http://www.cs.utexas.edu/users/moore/acl2/.
Among the information accessible from that page is a User's Manual
containing extensive hypertext documentation.
ACL2 is a functional programming language. But it is also a
mathematical framework. For example, the ``axioms of (applicative)
Common Lisp'' are made explicit by the ACL2 system.
To make ACL2 more useful as a mathematical language, it provides some
features not supported by Common Lisp. Among those features are the
ability to to introduce uninterpreted function symbols or, more
generally, undefined function symbols constrained to satisfy certain
formulas, and the ability to define functions using top-level
universal or existential quantification. In both cases, the logical
extensions introduced by these non-Common Lisp facilities are
conservative. For example, a constrained function may only be
introduced after showing that there exists some function satisfying
the constraint.
Unlike Common Lisp functions, these ``specification'' functions are
not executable, i.e., one cannot run them on constants to compute
constants. Unless a call-by-value execution trace of an ACL2
expression requires the evaluation of a constrained or quantified
function, all ACL2 expressions are executable.
No proof obligations have been skipped in carrying out any of the
solutions to these challenges, and no axioms have been used except
those that provide conservative extensions (in particular,
definitions, which are proved to terminate if they are recursive).
Collections of ACL2 definitions, theorems and other ``events'' are
arranged into files called ``books.'' Books can be ``certified'' to
check that theorem follows from the base axioms of ACL2 and the
definitions.
ACL2 disallows certification of a book that depends on any skipped
proofs or non-conservative axioms unless specific extra arguments are
given to the certify-book command. NO SUCH ARGUMENTS ARE SUPPLIED BY
OUR `MAKE' PROCESS.
---------- B. Termination ----------
The logic of ACL2 requires termination proofs for recursive
definitions, which guarantee that those definitions are conservative.
See for example ``Structured Theory Development for a Mechanized
Logic'', Journal of Automated Reasoning 26, no. 2 (2001) pp. 161-203.
Thus, in our solutions, the termination for our function definitions
is implicitly guaranteed by the fact that the books containing them
can be certified.
When a function is defined with defun it has two important effects: it
adds a conservative definitional axiom to the logical theory and it
defines a Common Lisp program that will compute on constants in a way
that is consistent with the axioms of the theory.
---------- C. "Type checks" like array bounds checking ----------
The kernel logic of ACL2 is a type-free, first-order logic with
induction. However, a notion of "guard" ties these logical
definitions to underlying host Common Lisp programs. If guards have
been "verified", then ACL2 makes the following guarantee for every
call of a function on arguments that satisfy its guard, which we will
call a "well-guarded call": every call of any function during the
ensuing evaluation is also well-guarded. So for example, if we
program with a list accessor function whose guard specifies that the
index is in bounds, then for evaluation of any well-guarded call, all
accesses of that function will be on an index that is in bounds. This
guarantee is established by proof of the so-called ``guard
conjectures.''
Thus, in our solutions, such checks are implicitly guaranteed by the
guard verification performed on our definitions.