Maintaining the ACL2 Theorem Proving System Matt Kaufmann and J Strother Moore University of Texas fkaufmann,mooreg s.utexas.edu Abstra t This talk will provide a view into the task of improving the ACL2 theorem prover to meet users' needs. 1 Introdu tion The goal of this talk is to provide a sense of some possible hallenges to making a the- orem proving system useful in pra ti e. Spe i ally, we will draw from our experien es maintaining the ACL2 theorem proving system [KMM00b, KM04a℄. Although ACL2 in orporates years of ongoing resear h in automated reasoning, the fo us of this talk is on the engineering required to make the system useful. Imagine you're at lun h, where two guys are blabbing to you about their work. Fortunately, this blabbing might be of some interest, sin e they are talking about how they make their theorem proving system easier to use. They de nitely want you to ask questions and share your own related experien es, though you may nd it hard to interrupt them after they get started. But even before we eat, they insist on providing some general ba kground on their system so that when they get going, at least they might make some sense. By the time dessert arrives, these two guys will be eager for questions and omments, if for no other reason than that they an eat! Thus, this talk onsists of three parts. First, Before We Eat : While we're walking to lun h you'll get some general ba k- ground on ACL2. Then while we're waiting for a table, we'll see a small example that gives a sense of how ACL2 is used. After we're seated, we'll take a qui k look at a list of features that we'll ome a ross while we eat. Next, for the Main Course, we will fo us on some sele ted items taken from re ent ACL2 release notes (minimally edited in a few ases). These sele ted items should give a sense of what an be involved in maintaining an empiri ally su essful automated reasoning system. Finally, we will have a give-and-take during Dessert. With any lu k, the ensuing questions and omments will be stimulating and informative for all of us. We will use footnotes for material that we will make a point of skipping during the talk, due to time onstraints.1 1 A related talk in 1991 [Kau91℄ gives a large list of aspe ts of me hanized reasoning systems and Empirically Successful Computerized Reasoning 1 2 Before We Eat | Some general ba kground on ACL2 \ACL2" stands for \A Computational Logi for Appli ative Common Lisp." The ACL2 system is the latest in the Boyer-Moore family of provers, and is joint work of Matt Kauf- mann and J Moore, with substantial early ontributions from Bob Boyer and ongoing ontributions from many. The paper [KM04b℄ provides a reasonably self- ontained in- trodu tion to ACL2, in luding relevant ba kground and how to use the system. Quoting from that paper: \ACL2" is the name of a fun tional programming language (based on Com- mon Lisp), a rst-order mathemati al logi , and a me hani al theorem prover. ACL2, whi h is sometimes alled an \industrial strength version of the Boyer- Moore system," is the produ t of Kaufmann and Moore, with many early design ontributions by Boyer. It has been used for a variety of important formal methods proje ts of industrial and ommer ial interest, in luding.... A long but in omplete list of appli ations is then given, in luding various algorithms, software, and hardware designs. ACL2 is freely available, distributed under the GPL [gpl℄. It an be obtained from the ACL2 home page [KM04a℄, whi h also has links to many papers that des ribe ACL2 appli ations, as well other useful links (mailing lists, tours, demos, do umentation, workshops, and installation instru tions). Here is some relevant data.  Some milestones: { 1973: The Boyer/Moore \Edinburgh Pure Lisp Theorem Prover" { 1979: Boyer and Moore, A Computational Logi [BM79℄ { 1986: Kaufmann joins Boyer/Moore proje t { 1988: Boyer and Moore, A Computational Logi Handbook (1997, 2nd ed. [BM97℄) { 1989: Boyer and Moore begin ACL2 { 1992: Final release of Boyer-Moore \Nqthm" prover { 1993: Kaufmann formally added as a o-author of ACL2 { 2000: Kaufmann, Manolios, and Moore write a book on ACL2, Computer-Aided Reasoning: An Approa h [KMM00b℄, and edit pro eedings of the rst ACL2 workshop, Computer-Aided Reasoning: ACL2 Case Studies [KMM00a℄ omments on them. The fo us here is narrower: What sorts of things must be done to make su h a system useful? Our fo us is a tually still narrower, as for example the following are riti al but not addressed dire tly here: fundamental reasoning algorithms, exe ution eÆ ien y, logi al foundations, system ar hite ture, and trust. Rather, we present here sele tions from release notes that give a avor of the maintenan e required on a parti ular mature system, ACL2, in order to make it a system that (some) people want to use. That is, the point here is not to give an overview of what ACL2 provides, but to fo us on maintenan e. 2 Empirically Successful Computerized Reasoning { 2006: Boyer, Kaufmann, and Moore win ACM Software System Award for Boyer-Moore family of provers  Version 3.0 sour e les size: 8.3M of Common Lisp (in luding sour e ode, do u- mentation strings, and omments)  There are 229 release note items stri tly after Version 2.8 (Mar h, 2004) as follows (but we'll look at just a few of these): { 63 in Version 2.9, O tober, 2004 { 19 in Version 2.9.1, De ember, 2004 { 30 in Version 2.9.2, April, 2005 { 31 in Version 2.9.3, August, 2005 { 53 in Version 2.9.4, February, 2006 { 33 in Version 3.0, June, 2006 An interesting aspe t of ACL2 is that it is written in its own formal language (with the ex eption of a small amount of Common Lisp ode mainly of a bootstrapping na- ture). This has for ed us to make ACL2's formal programming language, whi h is a arefully- rafted extension of an appli ative subset of Common Lisp, a language that is both eÆ ient and onvenient to use. As a result, ACL2 users often employ ACL2's programming environment to write tools. 2.1 The user's view of ACL2: A small example The following example will provide a sense of ACL2. The rst thing to noti e is that the syntax is Lisp's pre x syntax, so for example we write (+ 3 4) and (len x) rather than more traditional notation su h as 3+4 and len(x), respe tively. The syntax is ase-insensitive. Suppose that we want to prove that the length does not hange when we reverse a list. Lists and some list-pro essing fun tions, in luding reverse and len for reverse and length of a list, are built into ACL2. So let us submit a theorem named len-reverse, stating that for any list x, the length of the reverse of x is equal to the length of x:2 ACL2 !>(defthm len-reverse (implies (true-listp x) (equal (len (reverse x)) (len x)))) ACL2 Warning [Non-re ℄ in ( DEFTHM LEN-REVERSE ...): A :REWRITE rule generated from LEN-REVERSE will be triggered only by terms ontaining the non-re ursive fun tion symbol REVERSE. Unless this fun tion is disabled, this rule is unlikely ever to be used. 2 The warning below is not too important here. Think of it as a reminder that after the proof is omplete, we should disable the de nition of reverse so that the equality an be used as a left-to-right rewrite rule by ACL2's inside-out rewriter. If reverse were left enabled, the rewriter would rst repla e a term of the form (len (reverse x)) by expanding the de nition of reverse, after whi h that term would no longer mat h (len (reverse x)). Empirically Successful Computerized Reasoning 3 This simplifies, using the :definition REVERSE, to Goal' (IMPLIES (TRUE-LISTP X) (EQUAL (LEN (REVAPPEND X NIL)) (LEN X))). Name the formula above *1. Perhaps we an prove *1 by indu tion. Three indu tion s hemes are suggested by this onje ture. Subsumption redu es that number to two. These merge into one derived indu tion s heme. The proof ultimately fails. But sin e Goal' above did not simplify, we will take a look at it in a moment. As an aside, noti e that \using the :definition REVERSE" the prover has repla ed the original all of reverse with a all of revappend, whi h makes sense if we use a \print event" utility: ACL2 !>:pe reverse V -477 (DEFUN REVERSE (X) "Do umentation available via :do " (DECLARE (XARGS :GUARD (OR (TRUE-LISTP X) (STRINGP X)))) (COND ((STRINGP X) (COERCE (REVAPPEND (COERCE X 'LIST) NIL) 'STRING)) (T (REVAPPEND X NIL)))) Of ourse, if reverse hadn't been built in, we ould have de ned it exa tly as shown above, using the defun ommand. Looking again at Goal', we realize that a suitable rewrite rule ould simplify the term (LEN (REVAPPEND X NIL)). First let us look at the de nition of revappend, this time using a \print formula" query. ACL2 !>:pf revappend (EQUAL (REVAPPEND X Y) (IF (CONSP X) (REVAPPEND (CDR X) (CONS (CAR X) Y)) Y)) ACL2 !> Thus, if we don't know it already, we now see that (revappend x y) pushes su - essive elements of x onto y. The following lemma, aptly named len-revappend, says that the length of a revappend all is the sum of the lengths of the arguments. ACL2 proves this by indu tion automati ally (in less than 1/100 se ond).3 3 The reader may noti e that the lemma len-revappend is about (revappend x y) rather than the original term, (revappend x nil). We have generalized by hand to produ e a lemma whose proof seems amenable to indu tion. In this talk we do not onsider resear h in performing su h generalizations automati ally; in ACL2 as it is today, the user is responsible for su h generalization, though o asionally ACL2 makes useful generalizations on the y. 4 Empirically Successful Computerized Reasoning (defthm len-revappend (equal (len (revappend x y)) (+ (len x) (len y)))) Theorems are stored by default as ( onditional) rewrite rules; so now, any instan e of (len (revappend x y)) en ountered during a proof will be repla ed by the orre- sponding instan e of (+ (len x) (len y)). Thus, our original theorem, len-reverse, is now proved automati ally and immediately. To a rst approximation, it's fair to say that ACL2 users work as illustrated above. That is, they prove olle tions of rewrite rules, dis overing missing rules by looking at output from the prover. Our intention is that users an make good progress with the system without having to understand automated reasoning stru tures and on epts, as might be ne essary in order to program ta ti s in ta ti -based provers or set parameters in resolution-based provers. 2.2 Summary of some useful ACL2 features As we wait for our food, we'll take a very brief look at a smattering of ACL2 features that we'll see while devouring the Main Course. O asionally these features intera t in unexpe ted ways, leading to maintenan e tasks. Many improvements in these and other features are the dire t result of user requests, whi h are very important to the evolution of the system. There is no intention here to be omplete. ACL2 is a large system not to be explored thoroughly over the ourse of a meal! Our goal is just to give a sense of the kind of support provided for one empiri ally su essful automated reasoning system.4  Release Notes onsist of brief notes alerting the experien ed user to important di eren es between one release and the next. They make frequent itations into the do umentation (below) and are not intended to be self- ontained or to be read by the new user.  Do umentation onsists of over 1000 topi s organized hierar hi ally. The do u- mentation sour e onsists of strings in the ACL2 sour e ode that are liberally sprinkled with hyperlink annotations, whi h is pro essed to reate HTML, Ema s Info, and (generally not used) printed views. The do umentation is extensive; for example, the HTML version of the Version 3.0 do umentation is about 3.3 megabytes. Do umentation for a new release is intended to be omplete and a - urate for that release; for example, the HTML has grown about 300 kilobytes sin e Version 2.9, released less than two years ago. The do umentation sometimes takes about as mu h time to write as the ode to implement a feature or hange, but our impression from users is that it's worth the e ort.  Error messages and warnings provide riti al feedba k, often pointing to do u- mentation topi s. We put a lot of are into these! 4 In order to save time, during the talk we'll run through these very qui kly, just to give a sense of what is oming. Empirically Successful Computerized Reasoning 5  Ma ros make it easy to extend the syntax, but they have limitations (addressed by a new feature, make-event).  A book is a olle tion of legal embedded event forms (events ), in parti ular def- initions (defun events) and theorems (defthm events), that have been admitted : syntax has been he ked, theorems have been proved, and termination has been proved for re ursive de nitions. { Certi ation of a book reates a erti ate witnessing the su essful pro ess- ing of the book. { The ommand (in lude-book "foo") will load events from foo.lisp into the urrent session. { However, lo al events, e.g., (lo al (defun foo ...)), are not exported by in lude-book. A logi al story [KM01℄ involving onservativity justi es the dropping of lo al events. { About 850 books in about 70 dire tories, mostly ontributed by users rather than the developers, are distributed with ACL2, with over 700 more in over 200 dire tories available from supporting materials for the rst ve ACL2 workshops (not in luding the one this year, 2006). Thus there are over 1500 books in our regression suite. We rely heavily on that test suite to test purported improvements to the prover's heuristi s.  Like books, en apsulate provides a modular stru turing me hanism. En apsulate events an be used to provide partial de nitions for fun tions: that is, fun tions are total but may have in omplete axiomatizations.  The defevaluator ma ro generates events that de ne an evaluator, against whi h one an prove meta-rules [BM81, HKK+05℄ that, in essen e, augment the simpli er with formally veri ed user-de ned fun tions.  Proof ontrol in ludes in-theory events and hints, whi h disable (turn o ) or enable (turn on) spe i ed rules. Supported are not only in-theory hints but oth- ers, for example dire ting indu tion, fun tion expansion, or the use of previously- proved theorems. These an be atta hed to spe i named goals or an be gener- ated by ode (\ omputed hints"), whi h an be spe i ed globally (\default hints").  Database ontrol in ludes undo and undo-the-undo (oops) ommands.  An intera tive proof- he ker loop is a goal manager that has the feel of ta ti - based prover interfa es, allowing a range of ommands, from individual rewrites to alls of the full prover.  Proof debug is supported by the above-mentioned proof- he ker and also by a utility for inspe ting apparent rewriter loops, a break-rewrite debugger for the rewriter, and proof-tree displays for navigating proof output.  A top-level read-eval-print loop allows for intera tive testing of one's fun tions. Su h testing is typi ally relatively slow unless one issues a ompilation ommand. 6 Empirically Successful Computerized Reasoning  EÆ ient exe ution is supported for ground terms not only in the top-level loop, but also during proofs. EÆ ient exe ution also relies on single-threaded obje ts [BM02℄, or stobjs, in luding the ACL2 state obje ts.  Guards provide a powerful, exible analogue of types, and help support eÆ ient exe ution by way of a onne tion to the underlying Common Lisp. The mbe (\must be equal") feature allows one to atta h eÆ ient ode to logi ally elegant fun tions [GKM+ ℄.  Lisp pa kages provide namespa es.  While the main proof te hnique is onditional rewriting, there are ertainly others (for example, integrated de ision pro edures for ground equality and linear arith- meti ). And, rewriting is a tually ongruen e-based, i.e., an be used to repla e a term with one that is suitably equivalent even if not a tually equal.  A fun tional instantiation utility [BGKM91, KM01℄ allows deriving a theorem '(g) from a orresponding theorem '(f ) provided the fun tion g satis es all on- straints on the fun tion f . 3 Main Course | A sele tion of re ent enhan ements to ACL2 We now present a sele tion of items from re ent ACL2 release notes, annotated with explanations and dis ussion about impli ations for system maintenan e. We introdu e ea h item very brie y, then display the Ema s Info version of the relevant release note, and nally explain the issues if ne essary. 3.1 Subgoal ounting This item illustrates the e ort we put into prover output. Here, \:fun tional-instan e" refers to ACL2's fun tional instantiation utility, mentioned above; but the main point here is about output format, not fun tional instantiation. ............................................................................ Fixed a bug that was ausing proof output on behalf of :fun tional-instan e to be onfusing, be ause it failed to mention that the number of onstraints may be different from the number of subgoals generated. Thanks to Robert Krug for pointing out this onfusing output. The fix also auses the reporting of rules used when silently simplifying the onstraints to reate the subgoals. ............................................................................ Here is output from a proof attempt using ACL2 Version 2.9.3 that illustrates the problem. Noti e that \six onstraints" doesn't mat h up with the subgoal numbering, whi h ounts down from 5 to 1. (We ount down to give the user a real-time sense of how mu h work remains as the output s rolls by.) The old output was onfusing, and thus potentially undermined the user's on den e in his understanding of what ACL2 is doing and in his belief in ACL2's orre tness. Empirically Successful Computerized Reasoning 7 We now augment the goal above by adding the hypothesis indi ated by the :USE hint. This produ es a propositional tautology. The hypothesis an be derived from AC-FN-LIST-REV via fun tional instantiation, provided we an establish the six onstraints generated. Subgoal 5 (EQUAL (TIMES-LIST X) (IF (ATOM X) 1 (* (CAR X) (TIMES-LIST (CDR X))))). But simplifi ation redu es this to T, using the :definitions ATOM and TIMES-LIST and primitive type reasoning. Subgoal 4 .... Here is the orresponding output (suitably elided) from ACL2 3.0. We now augment .... provided we an establish the six onstraints generated. By the simple :rewrite rules ASSOCIATIVITY-OF-* and UNICITY-OF-1 we redu e the six onstraints to five subgoals. [. . . and so on, as before℄ 3.2 A rough edge in theory ontrol ACL2 uses evaluation as part of its proof strategy, but it allows the user to disable evaluation of alls of a fun tion f by disabling the so- alled exe utable- ounterpart rule for f. For a parti ular type of onditional rule, a forward- haining rule, evaluation of ground hypotheses had taken pla e without regard to whi h exe utable- ounterpart rules are disabled, thus severely impa ting eÆ ien y in at least one user's experien e. ............................................................................ Fixed a long-standing bug in forward- haining, where variable-free hypotheses were being evaluated even if the exe utable- ounterparts of their fun tion symbols had been disabled. Thanks to Eri Smith for bringing this bug to our attention by sending a simple example that exhibited the problem. ............................................................................ 3.3 Prover heuristi tweaks Sometimes we nd improvements to ACL2's prover heuristi s. All three items below des ribe hanges that were arefully made in response to user feedba k, and tested with our regression suite to gain on den e that our heuristi hanges would not severely impa t users. These hanges are only ne essary be ause ACL2 attempts to provide signi ant automation. ............................................................................ We fixed an infinite loop that ould o ur during destru tor elimination 8 Empirically Successful Computerized Reasoning (see *Note ELIM::). Thanks to Sol Swords for bringing this to our attention and sending a ni e example, and to Doug Harper for sending a se ond example that we also found useful. ............................................................................ The simplifier has been hanged slightly in order to avoid using forward- haining fa ts derived from a literal (essentially, a top-level hypothesis or on lusion) that has been rewritten. As a pra ti al matter, this may mean that the user should not expe t forward- haining to take pla e on a term that an be rewritten for any reason (generally fun tion expansion or appli ation of rewrite rules). Formerly, the restri tion was less severe: forward- haining fa ts from a hypothesis ould be used as long as the hypothesis was not rewritten to t. Thanks to Art Flatau for providing an example that led us to make this hange; see the omments in sour e fun tion rewrite- lause for details. ............................................................................ We modified the rewriter to avoid ertain infinite loops aused by an intera tion of the opening of re ursive fun tions with equality reasoning. (This hange is do umented in detail in the sour e ode, in parti ular fun tions rewrite-fn all and fnsta k-term-member.) Thanks to Fares Fraij for sending us an example that led us to make this hange. ............................................................................ There are over 36,000 lines of omments in the sour e ode, some of whi h survived multiple translations from the earliest version of the Boyer-Moore system. The om- ments are largely intended to be a re ord, for the implementors, of why things are the way they are. This is important in a software proje t of 35 years duration. Sometimes the omments show how we used to do something and why and when we hanged it. The omments also sometimes ontain interesting examples and ounterexamples illustrating supposed properties of the ode. Despite the original intention of the implementors to use omments as a way of re ording the design de isions and history, many ACL2 users read the sour e ode. Sin e ACL2 is written in ACL2, this is straightforward and sort of represents a se ond, more detailed, level of do umentation. 3.4 A library improvement using MBE The following release note item illustrates one maintenan e aspe t: we update the dis- tributed books (libraries of de nitions and proved theorems), often in onsultation with users. ............................................................................ Several interesting new definitions and lemmas have been added to the rtl library developed at AMD, and in orporated into books/rtl/rel4/lib/. Other book hanges in lude a hange to lemma trun ate-rem-elim in books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis. ............................................................................ But buried in this item is a hange that we nd parti ularly interesting. We mentioned guards earlier as a exible analogue of types, and we mentioned mbe as a way to atta h exe utable ounterparts eÆ iently. Empirically Successful Computerized Reasoning 9 At AMD, we found a need for more eÆ ient exe ution of bit-ve tor operations. Through Version 2.9.1, the rtl library, books/rtl/rel4/lib/, ontained the following de nition of the bit-sli e operation that returns bits i down to j of a natural number x. (Here, defund is a de ne-then-disable ommand, implemented in response to a user's request.) (defund bits (x i j) (de lare (xargs :guard (rationalp x))) (if (or (not (integerp i)) (not (integerp j))) 0 (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))) However, we found this de nition in terms of oor, modulo, and exponentiation operations painfully slow to exe ute. We really wanted a de nition that uses bitwise- and and shift operations instead: (defund bits (x i j) (if (< i j) 0 (logand (ash x (- j)) (1- (ash 1 (1+ (- i j))))))) Fortunately, we were able to hange the de nition of bits for purposes of exe ution without hanging its logi al de nition, whi h saved us from having to rework our proofs of any lemmas! The mbe (\must be equal") all below says to use the form after :logi as the body, with a proof obligation that the :guard (that x, i, and j are natural numbers) implies the equality of the :logi and :exe forms. The :guard must also imply ertain formulas generated for the alls in the :exe form; for example the all (ash x (- j)) arries a guard-related obligation that x and (- j) be integers, whi h is trivial from the guard assumptions that x and j are natural numbers. Then alls of bits on natural numbers will be exe uted dire tly in Common Lisp using the :exe form as the de nition. (defund bits (x i j) (de lare (xargs :guard (and (natp x) (natp i) (natp j)))) (mbe :logi (if (or (not (integerp i)) (not (integerp j))) 0 (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j)))) :exe (if (< i j) 0 (logand (ash x (- j)) (1- (ash 1 (1+ (- i j)))))))) 3.5 Some onvenien e features The following three items all make life easier for the user, as we explain below ea h one. 10 Empirically Successful Computerized Reasoning ............................................................................ Improved w-gsta k to allow a :frames argument to spe ify a range of one or more frames to be printed. See *Note CW-GSTACK::. ............................................................................ ACL2 makes very few restri tions on how users introdu e rewrite rules to program the rewriter. This freedom, however, makes it possible to introdu e in nite loops. When that o urs, ACL2 aborts leanly (a major advan e starting with Version 2.8 | previ- ously it sometimes seg faulted!) and suggests use of the tool w-gsta k, whi h shows the rewrite sta k. Unfortunately, the entire rewrite sta k is large, so there was interest in being able to limit the number of frames printed. ............................................................................ A new event, set-enfor e-redundan y, enfor es a restri tion that all defthms, defuns, and most other events are redundant. See *Note SET-ENFORCE-REDUNDANCY::. ............................................................................ AMD's rtl library (mentioned above) employed a methodology in whi h the proof work was restri ted to books in an auxiliary dire tory. It seemed desirable to enfor e this methodology, so that the main dire tory was kept lean and the auxiliary dire tory ould be modi ed as desired. Here is how that works. Suppose we have a le top.lisp that we want to ertify as a book. (lo al (in lude-book "work/book-1")) (defthm result-1 ...) ... Here, imagine that result-1 is proved in le work/book-1.lisp. The lo al anno- tation guarantees that additional theorems proved in work/book-1.lisp will ultimately disappear, ex ept for result-1, whi h (as seen above) we have made expli it. When we are ertifying the present book, we expe t that result-1 will be redundant be ause it already appears in work/book-1.lisp. But suppose we a identally delete result-1 in work/book-1.lisp. ACL2 would then try to prove result-1, but we may prefer that ACL2 instead fail immediately with a lear omplaint that it didn't nd that result-1 has already been proved. The item above provides a solution. We simply start top.lisp with the form (set-enfor e-redundan y t). One thing we've found is that nothing is ever simple! So for example, ertain kinds of events alled deflabel events are not allowed to be redundant. So even with set-enfor e-redundan y, we need to allow non-redundant deflabel events. ............................................................................ The fun tion disabledp an now be given a ma ro name that has a orresponding fun tion; see *Note MACRO-ALIASES-TABLE::. Also, disabledp now has a guard of t but auses a hard error on an inappropriate argument. ............................................................................ Empirically Successful Computerized Reasoning 11 For example, in ACL2 append is a ma ro, be ause fun tions must take a xed number of arguments but we want to be able to apply append to an arbitrary number of arguments. We an see how this works by using ACL2's :trans1 ommand to perform a single-step ma roexpansion. ACL2 !>:trans1 (append x y z) (BINARY-APPEND X (BINARY-APPEND Y Z)) ACL2 !> ACL2, however, is kind enough to print terms using append rather than using the orresponding fun tion, binary-append. Thus, novi e users might not even realize that append is not a fun tion. ACL2 has a notion of table events that allows maintenan e of information of interest, and on e su h table asso iates append with binary-append. The user then may refer to append in ontexts where a fun tion symbol is expe ted, for example when disabling a de nition, for example: (in-theory (disable append)) ............................................................................ The ma ro omp is now an event, so it may be pla ed in books. ............................................................................ The above item simply allows a ompilation dire tive to be pla ed in books. It's a simple thing to provide and we wish we had done it sooner in order to save users some annoyan e! 3.6 Common Lisp ompatibility: Pa kages Namespa e ontrol is provided by Common Lisp pa kages. Ea h symbol is in essen e a pair of strings: a pa kage name and a symbol name. But getting this exa tly right is quite tri ky. A rather elaborate x was made in Version 2.8, not shown here, to deal with an unsoundness that ould result from a subtle use, arefully employing lo al, of two di erent pa kages with the same name. (See ACL2's do umentation topi \hidden- death-pa kage" if you want to learn more about this issue. And it points to a very elaborate omment in the sour e ode that gives even more of an idea of how nasty this issue really is.) Below are three pa kage issues solved more re ently than that one, and not nearly as omplex. They show how we sometimes need to work hard to ensure ompatibility with the host Common Lisp. ............................................................................ We fixed a soundness hole due to the fa t that the "LISP" pa kage does not exist in OpenMCL. We now expli itly disallow this pa kage name as an argument to defpkg. Thanks to Bob Boyer and Warren Hunt for bringing an issue to our attention that led to this fix. ............................................................................ ACL2 now requires all pa kage names to onsist of standard hara ters (see *Note STANDARD-CHAR-P::, none of whi h is lower ase. The reason 12 Empirically Successful Computerized Reasoning is that we have seen at least one lisp implementation that does not handle lower ase pa kage names orre tly. Consider for example the following raw lisp log (some newlines omitted). >(make-pa kage "foo") #<"foo" pa kage> >(pa kage-name (symbol-pa kage 'FOO::A)) "foo" >(pa kage-name (symbol-pa kage '|FOO|::A)) "foo" > ............................................................................ (GCL only) A bug in symbol-pa kage-name has been fixed that ould be exploited to prove nil, and hen e is a soundness bug. Thanks to Dave Greve for sending us an example of a problem with def ong (see below) that led us to this dis overy. ............................................................................ 3.7 Portability, and help from others ACL2 an be built on most (all?) stable Common Lisp implementations, in luding GCL, OpenMCL, Allegro CL, SBCL, CMUCL, CLISP, and Lispworks. The most re ent addition is SBCL. There are at least two reasons for porting to all of these Lisps, in spite of a ertain amount of low-level Lisp-spe i ode we need to write and maintain. One is that we sometimes nd bugs in our ode that are in some sense \forgiven" by most, but not all, Lisps. The other is that we want users to be able to build on whatever Lisp platform they happen to have. Perhaps a third reason is to support ea h Lisp's development by providing a non-trivial test suite. ............................................................................ Added SBCL support. Thanks to Juho Snellman for signifi ant assistan e with the port. Thanks to Bob Boyer for suggesting the use of feature :a l2-mv-as-values with SBCL, whi h an allow thread-level parallelism in the underlying lisp; we have done so when feature :sb-thread is present. ............................................................................ 3.8 User-level debug support ACL2 has a break-rewrite utility that allows the user to put a breakpoint upon the ap- pli ation of a spe i ed rewrite rule, optionally under spe i ed onditions. The situation be omes ompli ated when there are so- alled free variables in hypotheses. For example, onsider the onditional rewrite rule saying that if predi ate p2 holds of x and y, and predi ate p3 holds of y, then predi ate p1 holds of x: (implies (and (p2 x y) (p3 y)) (equal (p1 x) t)) Empirically Successful Computerized Reasoning 13 Now suppose the rewriter en ounters the term (p1 (foo a)). So, x is bound to (foo a) when we apply the above rule. But how an we rewrite the rst hypothesis (to true ) if we do not have a binding for the free variable y? In this ase, ACL2 simply looks in its urrent ontext for some term for whi h (p1 (foo a) ) is known to be true. When it nds su h an then it binds y to and goes on to the next hypothesis. So it will now be \thinking about" (p3 ). If the rewriter annot prove this is true, it will ba ktra k and look for another value of y in pla e of for the rst hypothesis. The above information an be riti al to a user who is trying to understand why a rule is failing to be applied, espe ially when there is a omplex set of available rules operating on the hypotheses. The following item des ribes an improvement that provides onvenient display of su h information. ............................................................................ Improved reporting by the break-rewrite utility upon failure to relieve hypotheses in the presen e of free variables, so that information is shown about the attempting bindings. See *Note FREE-VARIABLES-EXAMPLES-REWRITE::. Thanks to Eri Smith for requesting this improvement. Also improved the break-rewrite loop so that terms, in parti ular from unifying substitutions, are printed without hiding subterms by default. The user an ontrol su h hiding ("evis eration"); see *Note SET-BRR-TERM-EVISC-TUPLE::. ............................................................................ The ACL2 do umentation topi \free-variables-examples-rewrite" des ribes how all this works. We'll just show a pie e of that do umentation here in order to give a visual ue of what we provide. (1 Breaking (:REWRITE LEMMA-1) on (PROP U0): 1 ACL2 >:eval 1x (:REWRITE LEMMA-1) failed be ause :HYP 1 ontains free variables. The following display summarizes the attempts to relieve hypotheses by binding free variables; see :DOC free-variables and see :DOC set- brr-term-evis -tuple. [1℄ X : X1 Failed be ause :HYP 3 ontains free variables Y and Z, for whi h no suitable bindings were found. [1℄ X : X2 Failed be ause :HYP 2 rewrote to (BAD X2). [1℄ X : X3 [3℄ Z : Z1 Y : Y1 Failed be ause :HYP 6 rewrote to (FOO X3 Y1). [3℄ Z : Z1 Y : Y3 Failed be ause :HYP 6 rewrote to (POO X3 Y3). 1 ACL2 > 14 Empirically Successful Computerized Reasoning 3.9 Some other release note items of interest  Several bugs have been xed that are related to lo al. It seems somewhat diÆ ult to anti ipate all intera tions of other aspe ts of the system and logi with lo al.  Two very di erent kinds of hints for defthm events are generally in ompatible: :hints to dire t the automati prover, and :instru tions to dire t the replay of ommands saved during a session with the proof- he ker, an intera tive goal- dire ted proof management tool. We quite sensibly aused an error if both :hints and :instru tions were present for the same defthm event. But we added a notion of default hints without noti ing that we needed to allow them with :instru tions, in whi h ase the default hints should apply to any individual instru tion that alls the full prover. (This has been xed.)  Users an undo events and they an even undo the undo. But some heavy users are hitting memory limitations, so we now provide the option of trading the \undo the undo" apability with the re lamation of spa e.  A feature new to Version 3.0, of ex itement to some experien ed ACL2 users, is a apability, make-event, that is similar to ma ros but whi h is sensitive to the environment (e.g., the ACL2 state obje t). The main idea is that expansions that might otherwise depend on the environment, whi h is illegal for ma ros,5 are saved in the book's erti ate. But there were lots of ompli ations to solve (for example, what if the make-event is submitted intera tively before erti ation is begun).  Users an spe ify a limit on ba k haining through rewrite rules, and they an spe ify synta ti he ks to ontrol the appli ation of a rewrite rule [HKK+ 05℄. But until a user requested it, these features were not available with onditional meta-rules.  ACL2 supports rewriting with ongruen es, where the original and rewritten term are equivalent but not ne essarily equal. ACL2 also a hes rewrite results, for eÆ ien y. There are o asions when the a hed result is from an equality rewrite, but we need to rewrite with an equivalen e, whi h ould produ e a stronger result. If we always ignore the a he in su h ases, eÆ ien y be omes a problem. But after re eiving a user request, we instituted a ompromise where we give spe ial handling in some ases when the equivalen e relation is Boolean equivalen e. More re ently [KM06℄, we have provided the user a means to handle this situation for other equivalen e relations, together with warnings that bring this situation to the user's attention. 5 It would take us too far a eld to explain in detail why it is illegal for ma ros to depend on the urrent state. But it's not hard to imagine that otherwise, a ma ro might expand to give one de nition of a fun tion as a book is erti ed, but a di erent de nition of the same fun tion when the book is later in luded. Besides, ACL2 ompiles its books, and the Common Lisp spe i ation disallows dependen e of ma ros on the state. Empirically Successful Computerized Reasoning 15 4 Dessert I intend to leave time for audien e members to share related observations from their own experien es, and to ask further questions. A knowledgments We thank Robert Krug and Sandip Ray for useful omments on a draft of this pa- per. This material is based upon work supported by DARPA and the National S ien e Foundation under Grant No. CNS-0429591. Referen es [BGKM91℄ R.S. Boyer, D.M. Golds hlag, M. Kaufmann, and J S. Moore. Fun tional instantiation in rst-order logi . In V. Lifs hitz, editor, Arti ial Intelli- gen e and Mathemati al Theory of Computation: Papers in Honor of John M Carthy, pages 7{26. A ademi Press, 1991. [BM79℄ R. S. Boyer and J S. Moore. A Computational Logi . A ademi Press, New York, 1979. [BM81℄ R. S. Boyer and J S. Moore. Metafun tions: Proving them orre t and using them eÆ iently as new proof pro edures. In The Corre tness Problem in Computer S ien e. A ademi Press, London, 1981. [BM97℄ R. S. Boyer and J S. Moore. A Computational Logi Handbook, Se ond Edition. A ademi Press, New York, 1997. [BM02℄ R. S. Boyer and J S. Moore. Single-threaded obje ts in ACL2. In S. Krish- namurthi and C. R. Ramakrishnan, editors, PADL 2002, LNCS 2257, pages 9{27, 2002. [GKM+ ℄ D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J. L. Ruiz- Reina, R. Sumners, D. Vroon, and M. Wilding. EÆ ient exe ution in an automated reasoning environment. Submitted. [gpl℄ http://www.gnu.org/ opyleft/gpl.html. [HKK+05℄ W. A. Hunt, Jr, M. Kaufmann, R. B. Krug, J S. Moore, and E. W. Smith. Meta reasoning in ACL2. In Joe Hurd and Tom Melham, editors, 18th Inter- national Conferen e on Theorem Proving in Higher Order Logi s: TPHOLs 2005, volume 3603 of Le ture Notes in Computer S ien e. Springer, August 2005. [Kau91℄ M. Kaufmann. An informal dis ussion of issues in me hani ally-assisted reasoning. In M. Ar her, J. J. Joy e, K. N. Levitt, and P. H. Windley, editors, Pro eedings of the 1991 International Workshop on the HOL The- orem Proving System and its Appli ations, pages 318{337, Los Alamitos, CA, 1991. IEEE Computer So iety Press. 16 Empirically Successful Computerized Reasoning [KM01℄ M. Kaufmann and J S. Moore. Stru tured theory development for a me h- anized logi . Journal of Automated Reasoning, 26(2):161{203, 2001. [KM04a℄ M. Kaufmann and J S. Moore. The ACL2 home page. In http: // www. s. utexas. edu/ users/ moore/ a l2/ . Dept. of Computer S ien es, Uni- versity of Texas at Austin, 2004. [KM04b℄ M. Kaufmann and J S. Moore. How to prove theorems for- mally. In http: // www. s. utexas. edu/ users/ moore/ publi ations/ how-to-prove-thms/ . Department of Computer S ien es, University of Texas at Austin, 2004. [KM06℄ M. Kaufmann and J S. Moore. Double rewriting for equivalential reasoning in ACL2. In Pro eedings of ACL2 Workshop 2006, August 2006. [KMM00a℄ M. Kaufmann, P. Manolios, and J S. Moore, editors. Computer-Aided Rea- soning: ACL2 Case Studies. Kluwer A ademi Press, Boston, MA., 2000. [KMM00b℄ M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approa h. Kluwer A ademi Press, Boston, MA., 2000. Empirically Successful Computerized Reasoning 17