maintaining the ACL2 theorem proving system [KMM00b, KM04a℄. Although ACL2 ground on ACL2. Then while we’re waiting for a table, we’ll see a small example that We will use footnotes for material that we will make a point of skipping during the they make their theorem proving system easier to use. They denitely want you to fkaufmann,mooreg s.utexas.edu talk, due to time onstraints.1 Imagine you’re at lun h, where two guys are blabbing to you about their work. system so that when they get going, at least they might make some sense. By the time But even before we eat, they insist on providing some general ba kground on their of features that we’ll ome a ross while we eat.
This talk will provide a view into the task of improving the ACL2 theorem prover to meet users’ needs.
ACL2 release notes (minimally edited in a few ases). These sele ted items should give gives a sense of how ACL2 is used. After we’re seated, we’ll take a qui k look at a list reason than that they an eat! ask questions and share your own related experien es, though you may nd it hard to reasoning system. related talk in 1991 [Kau91℄ gives a large list of aspe ts of me hanized reasoning systems and 1A a sense of what an be involved in maintaining an empiri ally su essful automated orem proving system useful in pra ti e. Spe i ally , we will draw from our experien es 1 Introdu tion The goal of this talk is to provide a sense of some possible hallenges to making a theinterrupt them after they get started.
Thus, this talk onsists of three parts.
Matt Kaufmann and J Strother Moore in orporates years of ongoing resear h in automated reasoning, the fo us of this talk is Next, for the Main Course, we will fo us on some sele ted items taken from re ent questions and omments will be stimulating and informative for all of us.
Fortunately, this blabbing might be of some interest, sin e they are talking about how dessert arrives, these two guys will be eager for questions and omments, if for no other University of Texas on the engineering required to make the system useful.
Abstra t Maintaining the ACL2 Theorem Proving System First, Before We Eat : While we’re walking to lun h you’ll get some general ba kFinally, we will have a give-and-take during Dessert. With any lu k, the ensuing but to fo us on maintenan e. software, and hardware designs.
Computer-Aided Reasoning: An Approa h [KMM00b℄, and edit pro eedings of the rst ACL2 workshop, { 1973: The Boyer/Moore \Edinburgh Pure Lisp Theorem Prover" { 1988: Boyer and Moore, A Computational Logi Handbook (1997, 2nd ed. (some) people want to use. That is, the point here is not to give an overview of what ACL2 provides, Moore system," is the produ t of Kaufmann and Moore, with many early workshops, and installation instru tions).
Some milestones: { 1992: Final release of Boyer-Moore \Nqthm" prover Here is some relevant data. addressed dire tly here: fundamental reasoning algorithms, exe ution eÆ ien y, logi al foundations, { 1979: Boyer and Moore, A Computational Logi [BM79℄ from that paper: appli ations, as well other useful links (mailing lists, tours, demos, do umentation, trodu tion to ACL2, in luding relevant ba kground and how to use the system. Quoting { 2000: Kaufmann, Manolios, and Moore write a book on ACL2, Computer-Aided Reasoning: ACL2 Case Studies [KMM00a℄ mann and J Moore, with substantial early ontributions from Bob Boyer and ongoing omments on them. The fo us here is narrower: What sorts of things must be done to make su h a system is the latest in the Boyer-Moore family of provers, and is joint work of Matt Kaufmon Lisp), a rst-order mathemati al logi , and a me hani al theorem prover. { 1993: Kaufmann formally added as a o-author of ACL2 \ACL2" is the name of a fun tional programming language (based on Comthe ACL2 home page [KM04a℄, whi h also has links to many papers that des ribe ACL2 ACL2, whi h is sometimes alled an \industrial strength version of the Boyer{ 1989: Boyer and Moore begin ACL2 2 Before We Eat | Some general ba kground on ACL2 A long but in omplete list of appli ations is then given, in luding various algorithms, { 1986: Kaufmann joins Boyer/Moore proje t ontributions from many. The paper [KM04b℄ provides a reasonably self- ontained inof the maintenan e required on a parti ular mature system, ACL2, in order to make it a system that formal methods proje ts of industrial and ommer ial interest, in luding.... design ontributions by Boyer. It has been used for a variety of important ACL2 is freely available, distributed under the GPL [gpl℄. It an be obtained from [BM97℄) system ar hite ture, and trust. Rather, we present here sele tions from release notes that give a a vor system useful? Our fo us is a tually still narrower, as for example the following are riti al but not \ACL2" stands for \A Computational Logi for Appli ative Common Lisp." The ACL2 ACL2 makes useful generalizations on the y . seems amenable to indu tion. In this talk we do not onsider resear h in performing su h generalizations original term, (revappend x nil). We have generalized by hand to produ e a lemma whose proof automati ally; in ACL2 as it is today, the user is responsible for su h generalization, though o asionally reader may noti e that the lemma len-revappend is about (revappend x y) rather than the 3The
sponding instan e of (+ (len x) (len y)). Thus, our original theorem, len-reverse, order to save time, during the talk we’ll run through these very qui kly, just to give a sense of 4In system without having to understand automated reasoning stru tures and on epts, as Error messages and warnings provide riti al feedba k, often pointing to do usupport provided for one empiri ally su essful automated reasoning system.4 2.2 Summary of some useful ACL2 features megabytes. Do umentation for a new release is intended to be omplete and a is now proved automati ally and immediately. mentation topi s. We put a lot of are into these! Do umentation onsists of over 1000 topi s organized hierar hi ally. The do uby the new user. the do umentation (below) and are not intended to be self- ontained or to be read dieren es between one release and the next. They make frequent itations into Theorems are stored by default as ( onditional) rewrite rules; so now, any instan e sprinkled with hyperlink annotations, whi h is pro essed to reate HTML, Ema s unexpe ted ways, leading to maintenan e tasks. Many improvements in these and other output from the prover. Our intention is that users an make good progress with the features are the dire t result of user requests, whi h are very important to the evolution for example, the HTML version of the Version 3.0 do umentation is about 3.3 There is no intention here to be omplete. ACL2 is a large system not to be explored urate for that release; for example, the HTML has grown about 300 kilobytes That is, they prove olle tions of rewrite rules, dis overing missing rules by looking at (+ (len x) (len y)))) thoroughly over the ourse of a meal! Our goal is just to give a sense of the kind of To a rst approximation, it’s fair to say that ACL2 users work as illustrated above. that we’ll see while devouring the Main Course. O asionally these features intera t in (defthm len-revappend in resolution-based provers. what is oming. might be ne essary in order to program ta ti s in ta ti -based provers or set parameters As we wait for our food, we’ll take a very brief look at a smattering of ACL2 features of (len (revappend x y)) en ountered during a proof will be repla ed by the orreInfo, and (generally not used) printed views. The do umentation is extensive; but our impression from users is that it’s worth the eort. mentation sour e onsists of strings in the ACL2 sour e ode that are liberally (equal (len (revappend x y)) takes about as mu h time to write as the ode to implement a feature or hange, sin e Version 2.9, released less than two years ago. The do umentation sometimes of the system. signi an t automation. [. . . and so on, as before℄ We now augment .... provided exhibited the problem.
But simplifi ation redu es this to T, using the :definitions ATOM and (IF (ATOM X) Sometimes we nd improvements to ACL2’s prover heuristi s. All three items below hypotheses were being evaluated even if the exe utable- ounterparts of the :USE hint. This produ es a propositional tautology. The hypothesis we an establish the six onstraints generated. By the simple :rewrite We now augment the goal above by adding the hypothesis indi ated by 3.3 Prover heuristi tweaks Subgoal 5 Fixed a long-standing bug in forward- haining, where variable-free Subgoal 4 bringing this bug to our attention by sending a simple example that their fun tion symbols had been disabled. Thanks to Eri Smith for an be derived from AC-FN-LIST-REV via fun tional instantiation, provided rules are disabled, thus severely impa ting eÆ ien y in at least one user’s experien e.
Here is the orresponding output (suitably elided) from ACL2 3.0.
We fixed an infinite loop that ould o ur during destru tor elimination evaluation of alls of a fun tion f by disabling the so- alled exe utable- ounterpart rule our regression suite to gain onden e that our heuristi hanges would not severely for f. For a parti ular type of onditional rule, a forward- haining rule, evaluation ............................................................................
TIMES-LIST and primitive type reasoning. impa t users. These hanges are only ne essary be ause ACL2 attempts to provide ............................................................................ of ground hypotheses had taken pla e without regard to whi h exe utable- ounterpart we an establish the six onstraints generated.
ACL2 uses evaluation as part of its proof strategy, but it allows the user to disable ............................................................................ to five subgoals. (EQUAL (TIMES-LIST X) 1 (* (CAR X) (TIMES-LIST (CDR X))))). 3.2 A rough edge in theory ontrol .... des ribe hanges that were arefully made in response to user feedba k, and tested with rules ASSOCIATIVITY-OF-* and UNICITY-OF-1 we redu e the six onstraints read the sour e ode. Sin e ACL2 is written in ACL2, this is straightforward and sort The simplifier has been hanged slightly in order to avoid using users. rtl library developed at AMD, and in orporated into books/rtl/rel4/lib/. way they are. This is important in a software proje t of 35 years duration. Sometimes of represents a se ond, more detailed, level of do umentation.
Fares Fraij for sending us an example that led us to make this hange. to take pla e on a term that an be rewritten for any reason (generally attention and sending a ni e example, and to Doug Harper for sending a We modified the rewriter to avoid ertain infinite loops aused by an (see *Note ELIM::). Thanks to Sol Swords for bringing this to our intera tion of the opening of re ursive fun tions with equality But buried in this item is a hange that we nd parti ularly interesting. omments also sometimes ontain interesting examples and ounterexamples illustrating The following release note item illustrates one maintenan e aspe t: we update the disments are largely intended to be a re ord, for the implementors, of why things are the as a way to atta h exe utable ounterparts eÆ iently. fun tion expansion or appli ation of rewrite rules). Formerly, the Other book hanges in lude a hange to lemma trun ate-rem-elim in ............................................................................ ould be used as long as the hypothesis was not rewritten to t. Thanks Several interesting new definitions and lemmas have been added to the 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 omthe omments show how we used to do something and why and when we hanged it. The We mentioned guards earlier as a exible analogue of types, and we mentioned mbe tributed books (libraries of denitions and proved theorems), often in onsultation with reasoning. (This hange is do umented in detail in the sour e ode, in forward- haining fa ts derived from a literal (essentially, a top-level restri tion was less severe: forward- haining fa ts from a hypothesis ............................................................................ matter, this may mean that the user should not expe t forward- haining hypothesis or on lusion) that has been rewritten. As a pra ti al to Art Flatau for providing an example that led us to make this hange; se ond example that we also found useful. parti ular fun tions rewrite-fn all and fnsta k-term-member.) Thanks to ............................................................................ see the omments in sour e fun tion rewrite- lause for details. 3.4 A library improvement using MBE ............................................................................ books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis. 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 The following three items all make life easier for the user, as we explain below ea h one. 3.5 Some onvenien e features :exe that o urs, ACL2 aborts leanly (a major advan e starting with Version 2.8 | previSuppose we have a le top.lisp that we want to ertify as a book. ............................................................................ ............................................................................ the rewrite sta k. Unfortunately, the entire rewrite sta k is large, so there was interest Here, imagine that result-1 is proved in le work/book-1.lisp. The lo al anno............................................................................ (set-enfor e-redundan y t).
Improved w-gsta k to allow a :frames argument to spe ify a range of one tation guarantees that additional theorems proved in work/book-1.lisp will ultimately work/book-1.lisp. ACL2 would then try to prove result-1, but we may prefer that SET-ENFORCE-REDUNDANCY::. or more frames to be printed. See *Note CW-GSTACK::. inappropriate argument. ...
The item above provides a solution. We simply start top.lisp with the form has already been proved. in being able to limit the number of frames printed. are ertifying the present book, we expe t that result-1 will be redundant be ause it kinds of events alled deflabel events are not allowed to be redundant. So even with the rewriter. This freedom, however, makes it possible to introdu e innite loops. When disabledp now has a guard of t but auses a hard error on an ACL2 makes very few restri tions on how users introdu e rewrite rules to program disappear, ex ept for result-1, whi h (as seen above) we have made expli it. When we set-enfor e-redundan y, we need to allow non-redundant deflabel events.
One thing we’ve found is that nothing is ever simple! So for example, ertain ............................................................................ defthms, defuns, and most other events are redundant. See *Note work was restri ted to books in an auxiliary dire tory. It seemed desirable to enfor e AMD’s rtl library (mentioned above) employed a methodology in whi h the proof (lo al (in lude-book "work/book-1")) this methodology, so that the main dire tory was kept lean and the auxiliary dire tory ACL2 instead fail immediately with a lear omplaint that it didn’t nd that result-1 already appears in work/book-1.lisp. But suppose we a identally delete result-1 in orresponding fun tion; see *Note MACRO-ALIASES-TABLE::. Also, ............................................................................ ously it sometimes seg faulted!) and suggests use of the tool w-gsta k, whi h shows The fun tion disabledp an now be given a ma ro name that has a A new event, set-enfor e-redundan y, enfor es a restri tion that all (defthm result-1 ...) ould be modied as desired. Here is how that works. ............................................................................ #<"foo" pa kage> >(make-pa kage "foo") in the underlying lisp; we have done so when feature :sb-thread is ACL2 has a break-rewrite utility that allows the user to put a breakpoint upon the apthat led us to this dis overy. exploited to prove nil, and hen e is a soundness bug. Thanks to Dave >(pa kage-name (symbol-pa kage ’|FOO|::A)) most, but not all, Lisps. The other is that we want users to be able to build on whatever ............................................................................
Added SBCL support. Thanks to Juho Snellman for signifi ant assistan e (implies (and (p2 x y) ............................................................................ 3.7 Portability, and help from others be omes ompli ated when there are so- alled free variables in hypotheses. For example, GCL, OpenMCL, Allegro CL, SBCL, CMUCL, CLISP, and Lispworks. The most re ent pli ation of a spe ied rewrite rule, optionally under spe ied onditions. The situation 3.8 User-level debug support Greve for sending us an example of a problem with def ong (see below) (p3 y)) (GCL only) A bug in symbol-pa kage-name has been fixed that ould be Lisp platform they happen to have. Perhaps a third reason is to support ea h Lisp’s handle lower ase pa kage names orre tly. Consider for example the addition is SBCL. There are at least two reasons for porting to all of these Lisps, in (equal (p1 x) t)) present. "foo" ............................................................................ is that we have seen at least one lisp implementation that does not onsider the onditional rewrite rule saying that if predi ate p2 holds of x and y, and spite of a ertain amount of low-level Lisp-spe i ode we need to write and maintain. development by providing a non-trivial test suite. >(pa kage-name (symbol-pa kage ’FOO::A)) :a l2-mv-as-values with SBCL, whi h an allow thread-level parallelism predi ate p3 holds of y, then predi ate p1 holds of x: ACL2 an be built on most (all?) stable Common Lisp implementations, in luding ............................................................................ following raw lisp log (some newlines omitted). with the port. Thanks to Bob Boyer for suggesting the use of feature "foo" > One is that we sometimes nd bugs in our ode that are in some sense \forgiven" by
eÆ ien y. There are o asions when the a hed result is from an equality rewrite, Users an spe ify a limit on ba k haining through rewrite rules, and they an a notion of default hints without noti ing that we needed to allow them with environment (e.g., the ACL2 state obje t). The main idea is that expansions of ma ros on the state. the undo" apability with the re lamation of spa e. begun). re ently [KM06℄, we have provided the user a means to handle this situation for :hints to dire t the automati prover, and :instru tions to dire t the replay Users an undo events and they an even undo the undo. But some heavy users are equivalent but not ne essarily equal. ACL2 also a hes rewrite results, for to anti ipate all intera tions of other aspe ts of the system and logi with lo al. meta-rules. dire ted proof management tool. We quite sensibly aused an error if both :hints other equivalen e relations, together with warnings that bring this situation to the after re eiving a user request, we instituted a ompromise where we give spe ial 3.9 Some other release note items of interest but we need to rewrite with an equivalen e, whi h ould produ e a stronger result. urrent state. But it’s not hard to imagine that otherwise, a ma ro might expand to give one denition instru tion that alls the full prover. (This has been xed.) of ommands saved during a session with the proof- he ker, an intera tive goalTwo very dieren t kinds of hints for defthm events are generally in ompatible: in luded. Besides, ACL2 ompiles its books, and the Common Lisp spe i ation disallows dependen e and :instru tions were present for the same defthm event. But we added Several bugs have been xed that are related to lo al. It seems somewhat diÆ ult :instru tions, in whi h ase the default hints should apply to any individual ACL2 supports rewriting with ongruen es, where the original and rewritten term that might otherwise depend on the environment, whi h is illegal for ma are ros,5 example, what if the make-event is submitted intera tively before erti ation is handling in some ases when the equivalen e relation is Boolean equivalen e. More would take us too far aeld to explain in detail why it is illegal for ma ros to depend on the 5It saved in the book’s erti ate. But there were lots of ompli ations to solve (for A feature new to Version 3.0, of ex itement to some experien ed ACL2 users, is are hitting memory limitations, so we now provide the option of trading the \undo of a fun tion as a book is ertied, but a dieren t denition of the same fun tion when the book is later user’s attention. spe ify synta ti he ks to ontrol the appli ation of a rewrite rule [HKK+05℄. a apability, make-event, that is similar to ma ros but whi h is sensitive to the If we always ignore the a he in su h ases, eÆ ien y be omes a problem. But