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.