Cs.uwyo.edu

Hacking and Extending ACL2∗
ABSTRACT
smaller, ACL2 authors were more able to adapt and ex- The ACL2 theorem prover provides the user a wide range tend the system itself to suit user needs. A new reality has of mechanisms for customization and extension while pre- set in, in which a growing number of sophisticated users are serving soundness. ACL2 researchers and power users, how- seeking to adapt ACL2 to new environments [1], modify or ever, sometimes work outside this realm in order to add new extend core functionality [5], or combine it with other rea- core functionality, to attach new user interfaces, or to con- soning engines [8, 7]. The ACL2 authors cannot possibly nect ACL2 with other reasoning engines. We first describe satisfy all these requests for new functionality from ACL2, new features of ACL2 that enable users to add to the set of nor, arguably, should they/we. The needs and desires of “trusted code” in a trackable way. The advantage is that such “power users” can extend far beyond what the current users can dynamically install system extensions they choose ACL2 can be practically made to accommodate soundly by to trust in reaching their verification results, and ACL2 will the ACL2 authors. It may seem ironic that as ACL2 has track what was trusted in the process. We then describe fea- grown more powerful, the demand for more functionality tures, idioms, and abstractions that leverage the freedoms has grown; but it is certainly being applied to a larger vari- given to trusted code and the dynamic, reflective nature of Common Lisp to modify ACL2 in deep ways at runtime.
Our abstractions are designed to make it easier for system To address this problem, ACL2 Version 3.1 introduced a fea- hackers to preserve sound reasoning when writing metathe- ture, trust tags (“ttags” for short), which has “opened the flood gates” to potentially unsound extensions of ACL2 byend-users. The basic idea behind trust tags is not particu- INTRODUCTION
larly novel (see for example [2]), though ACL2’s approachmay be unique in that it allows for rather arbitrary system “ACL2” stands for “A Computational Logic for Applica- extensions written in the system itself. But trust tags pre- tive Common Lisp.” ACL2 consists of a first-order func- sented unique challenges for implementation in ACL2. The tional programming language, a logic for that language, and basic idea is that constructs that can render ACL2 unsound an “industrial-strength” automatic theorem prover [6, 4, 3].
are now legal in the command loop and in books, provided ACL2 has been used to prove some of the most complex they are used in a context with an active trust tag. Defining theorems ever proved about commercial systems.
(activating) a trust tag is subject to authorization and afterdoing so, an ACL2 session is thence forth “tainted,” at least As ACL2 has become more widely used, the need and/or de- in the sense that sound reasoning depends on code that is sire to extend ACL2 in unsupported ways has risen. Within not a part of ACL2 proper. Trust tags enable authors to the bounds of a command-line automatic theorem prover make such code small and concise and enable other users to based largely on term rewriting, ACL2 is quite extensible, track down easily which code must be trusted.
not only with user-defined theorems and theories, but alsowith computed hints, meta rules, powerful metaprogram- This paper introduces, documents, and demonstrates some applications of trust tags. Section 2 gives some background information and terminology on ACL2’s inner workings. Sec- This research was funded in part by National Science Foun- dation grants CCF-0429924, IIS-0417413, CCF-0438871, tion 3 introduces trust tags in some detail, giving some rules and EIA-0303609, and also based upon work supported by and conventions on their use. Section 4 enumerates the po- DARPA and NSF under Grant No. CNS-0429591 tentially unsafe constructs ttags make available. We alsodiscuss some of our own low-level tools that can be addedto provide more powerful and robust extensions of ACL2.
Section 5 describes some higher-level idioms for modifyingand extending ACL2 behavior, which have proved quite use-ful. Section 6 concludes.
Keep in mind that this paper does not offer any insight intoproving theorems with ACL2, but a basic knowledge of theideas in Section 3 is important for users who might use non- standard extensions. Later sections are intended for ACL2 certain invariants on the logical state to maintain sound rea- system hackers, who seek to alter or extend ACL2 in funda- mental ways. Beware that such nonstandard extensions areerror-prone and can run into compatibility issues with the The ACL2-DEFAULTS-TABLE is a special part of the world that various implementations of Common Lisp. To the contrary, keeps track of settings that govern how the theorem prover standard use of ACL2 is designed to be quite robust and behaves and how some events are interpreted. The ACL2- DEFAULTS-TABLE is the only ACL2 table that is reset at thebeginning of every book.
Throughout this paper, we will “offer,” “introduce,” or “de-fine” some functionality that is not in ACL2—at least at Intricacies (for Section 4+)
the time of writing. This code is available in the supporting ACL2 function definitions are stored as elements (proper- ties) of a list (the world). Installing a world makes the func-tions executable by defining them in the underlying Com- The examples we present will be drawn from the develop- mon Lisp. In fact, to support ACL2 functions being fully ment of ACL2s, the “ACL2 Sedan.” ACL2s is an Eclipse- defined (unlike Common Lisp functions) all functions actu- based development environment for ACL2 that is designed ally have two raw definitions: a Common Lisp definition and to make formal reasoning in ACL2 easier to learn [1]. Key an executable counterpart. ACL2 uses one or both of the features of ACL2s are based on extending ACL2 to enhance raw definitions whenever it executes the function on a par- invisible communication with the development environment, ticular input; the executable counterpart often defers to the and on limiting or extending the theorem prover in non- Common Lisp definition. In this paper, we will only con- standard but visible ways. While previously ACL2s required sider cases that use the Common Lisp definition, so we will a specially-built ACL2 image to implement these extensions, not need to investigate manipulation of executable counter- trust tags enable them to be installed into a standard ACL2 parts. Outside of this paragraph, the “raw” definition is the image at runtime, in an “approved,” trackable manner.
BACKGROUND INFORMATION
Macros have raw definitions also, but only one per macro, a Terminology and Basics
“Common Lisp” definition. When we use a macro in ACL2, The standard, safe ways of extending ACL2 involve extend- including those as simple and common as DEFUN, it is ex- ing the world. The ACL2 world is a property list consisting panded by looking up its definition in the world, binding of everything about the current interpretation of the ACL2 its lambda variables, and evaluating the body in that envi- logic, all the theorem prover rules and settings, and def- ronment. Thus, the raw macro definition is not involved in initions that are not part of the logic. When, for exam- macro expansion of input to the ACL2 loop. To the contrary, ple, a new function is defined, an extension of the current executing a function (on a particular input) from the ACL2 world is computed and then installed to make it the cur- loop always uses one or both of the raw function definitions.
rent world. Undoing that definition reinstalls a retractionof the current world, one that was previously the current The raw definitions of macros are only relevant for code in- world. Even though the world is an applicative object, “be- terpreted by Common Lisp. Most importantly, this includes hind the scenes” optimizations make extension, retraction, raw function bodies, because these are interpreted (and/or and look-ups fast for the current world.
compiled) by Common Lisp. But this also includes the bod-ies of books. Books bundle together definitions of functions, Roughly speaking, events are inputs to ACL2 that extend macros, and theorems to be used by ACL2, but they can the world, and books are files of events. Certifying a book also be compiled by raw Lisp. In fact, this is the default means verifying all of its events in some certification world case. For example, a DEFUN in a book when processed by and writing out a certificate that enables fast inclusion of the ACL2 loop is macro-expanded to a function that installs a world updated with the new definition. When processedby raw Lisp, either during compilation or inclusion of the The ACL2 state is a single-threaded object, which means it is compiled file, the Common Lisp meaning of DEFUN is used, modifiable by virtue of there being only one “live” instance, which installs the compiled version of the raw functions and enforced through static checks at definition time. The state macros. As another example, DEFTHM proves theorems and includes the current world, assignments to global variables, potentially adds them as rules in the world, but when in- and many other things that do not show up in this paper.
terpreted by raw Lisp, DEFTHM is a no-op. This differentbehavior is due to the difference between the Common Lisp “The loop” is the ACL2 read-eval-print loop. Unlike books, and ACL2 definitions of the DEFTHM macro.
the loop accepts types of input other than events. Some ofthese inputs can modify the ACL2 state, including the world, TRUST TAGS IN ACL2
and some even interact with the external environment, such Here we introduce the ACL2 notion of trust tags. For more as reading from or writing to files.
details, start with ACL2 documentation topic DEFTTAG.
We will refer to a critical subset of the full ACL2 state asthe “logical state”. We can formally define the logical state as that which is protected by MAKE-EVENT (discussed be- MAKE-EVENT, introduced in ACL2 Version 3.0, made it pos- low), but it basically consists of the world and many global sible to embed arbitrary ACL2 code to be executed on the variables that ACL2 uses internally. ACL2 must maintain certification or inclusion of a book. By contrast, books were previously restricted primarily to contain definitions, theo- there is an active trust tag. Intuitively, defining a trust tag rems, and evaluation of stateless functions. Since all that is for a block of code declares that the author (or at least that needed from the code in a MAKE-EVENT is the return value, block of code) must be trusted to preserve soundness. The MAKE-EVENT is able to protect the logical state from corrup- trust tag indicates who or what is to blame if unsoundness tion by saving it, executing the code, and then restoring the Each time a trust tag is declared, the ACL2 session should However, some ACL2 functions interact with the external be considered “tainted” by another extension. There is no environment or can have other dangerous effects that aren’t tracking of which subsequent lemmas depend on the poten- tracked as part of the logical state. Bob Boyer demonstrated tially unsound extension, not only because ACL2 has trou- the incompleteness of the protection offered by MAKE-EVENT, ble determining which theorems were required for a proof, by creating a book that derives a contradiction in ACL2 but also because the extensions are often metatheoretic, in- by embedding in a MAKE-EVENT a SYS-CALL that invokes an capable of being described succinctly by a set of rules or external debugger to overwrite memory in the ACL2 process.
postulates. In a sense, ACL2 takes a conservative approach, (See the ACL2 documentation for SYS-CALL for details.) in which every subsequent lemma is considered to dependon all ttags seen. Along these lines, a book is tagged with An approach to patching this problem that was rejected af- any ttags seen in the logical world that certified the book, in ter some consideration was to add a parameter to CERTIFY- addition to any ttags seen in the resulting logical world af- BOOK and INCLUDE-BOOK to allow or disallow use of SYS-CALL ter certification. This tracking includes ttags used in a local inside the corresponding book. This was analogous to ex- context, but does not include ttags used in worlds that have isting :DEFAXIOMS-OKP and :SKIP-PROOFS-OKP parameters, been undone or ttags that try to hide their existence. This but there was an important difference. DEFAXIOM and, in a is a limitation to the conservativity: “taintedness” tracking sense, SKIP-PROOFS do not affect the soundness of ACL2’s is subject to cooperation of the ttagged code. Thus, printed reasoning. If the formulae introduce inconsistencies, we can ttag notes and manual inspection must be considered the prove NIL (derive an apparent contradiction), but if we inter- pret the constructs as simply adding new formulas to the setof axioms/postulates, the reasoning is still sound 1. Also,any Authorizing Trust Tags
DEFAXIOM events, and any events under SKIP-PROOFS, can be readily undone with no lingering impact.
An important aspect of trust tags is that an included bookcan generally only define trust tags that have been autho- Constructs such as SYS-CALL and SET-RAW-MODE, on the other rized by the user (but see the discussion of “ttag notes” in hand, can irreversibly render an ACL2 session unsound.
Section 3.4). The ACL2 authors intend for this to provide That is, these constructs can break ACL2’s implementation a degree of protection for the user’s session and entire sys- of its underlying logic. Since each of these constructs has tem; that is, ACL2 is designed so that an included book the potential to affect ACL2 in the worst possible way, it cannot “taint” the user’s session (or system!) without spe- makes little sense to distinguish between them for the pur- cific authorization to use ttags. Thus, it should be safe to poses of allowing or disallowing use. More important than certify and include books that do not require ttags without which construct is used is where, by whom, and for what inspecting them first. Attempting to define a ttag without purpose. This is what we intend to capture with trust tags, in a concise, understandable, and usable way.
In the current implementation, defining a trust tag inside Defining Trust Tags
the command loop is always authorized. Recall that justbecause a ttag is active in the command loop doesn’t mean A trust tag (or ttag ) instance has a name and a location.
an included book can use dangerous functions without defin- The name is any (non-NIL) ACL2 symbol, and the location ing its own ttag; the :TTAG setting does not propagate to is either the top-level command loop (indicated by NIL) or a book location (indicated by a path string). A trust tagis activated by passing the name to DEFTTAG. The location Defining a ttag in book certification or inclusion requires au- associated with the trust tag is always the current location.
thorization, and the user specifies what is authorized by the The name of the current active trust tag is stored in the :TTAGS keyword parameter to CERTIFY-BOOK or INCLUDE- :TTAG entry of the ACL2-DEFAULTS-TABLE, alongside settings BOOK. This parameter defaults to NIL, indicating no ttags are such as :DEFUN-MODE and :WELL-FOUNDED-RELATION. There authorized. Specifying :ALL allows all ttags. One can also can be only one active ttag at a time, or a NIL setting indi- be more precise by specifying names and/or locations, and cates there is no active ttag, as produced by (defttag nil).
we refer the reader to the ACL2 documentation on DEFTTAG Like other ACL2-DEFAULTS-TABLE settings, the current ttag for that syntax. The reason we would want to be able to setting is local to the book in which it occurs.
specify locations other than the one we are including is thatthe specification for authorized ttags also restricts what that The :TTAG setting becomes relevant when command loop book can authorize to books it includes, and so on recur- code or book code attempts to use a dangerous function, a sively. Thus, books can only reduce the set of authorized function such as SYS-CALL that is known to enable unsound ttags when including books themselves (unless they use an reasoning. Use of such functions is permitted if and only if active ttag to get around the restriction, as in Section 3.6).
1If the postulates are inconsistent, no models satisfy the pos- tulates; thus any formula is trivially satisfied by all modelssatisfying the postulates.
The Certifier
We now explore what is involved in the job of the certifier, Smith’s ACL2 interface to UCLID Version 0.73a|, though a person who takes the role of being skeptical that ACL2 has reached its conclusions through sound reasoning. If thecertifier trusts an “untainted” ACL2, then he must at least Regarding version numbers in ttag names, on the one hand, confirm that the result was reached without tainting ACL2.
updating version numbers in what one authorizes can bea hassle, but on the other hand, that hassle reminds users The main caveat is that although we can ask ACL2 which that changes have been made and they should proceed with ttags have tainted it (see the ACL2 documentation for TTAGS- caution. When or whether such reminders are needed is a SEEN), that answer is only trustworthy if the session has not been tainted. Thus, as a skeptic, the certifier learns nothingfrom that query. This observation demonstrates the need for Since ttag names are symbols, they have a package. With ttag notes. Whenever DEFTTAG is called with a non-nil value, the exception of T, we have assumed use of keyword symbols ACL2 prints out the following (but for the appropriate name (package "KEYWORD") for ttag names so far. This is great for avoiding package import issues, and, as mentioned, nameclashes are not a big problem. It’s hard to foresee a casethat strongly motivates using symbols other than keywords.
TTAG NOTE: Adding ttag T from the top level loop.
Extent. Let us now consider the issue of how much func-tionality should be encompassed by one ttag, or by the same The first DEFTTAG is guaranteed to print out such a note, and ttag name in different locations, etc. First, observe that it the certifier should determine the effects of that ttagged code is possible to use DEFTTAG more than once within a single first because it could modify ACL2 behavior in arbitrary book. One case of this is using (defttag nil) to mark the ways, including modifications to the printing of later ttag end of a block of code that uses dangerous constructs; this notes. Once convinced the code “behaves nicely”, including is highly encouraged, except when it would make sense to preserving the printing of later ttag notes, the certifier can relegate that block of code to a separate book. (It’s not move on to the next ttag note and repeat until all potentially necessary to put (defttag nil) at the end of a book, but can serve as documentation.) In fact, the certifier’s job iseasiest when ttagged code is restricted to small, stand-alone Unfortunately, we can’t really define “behaves nicely” much more precisely than “extends ACL2 only as intended, andthe intended extensions, as used, preserve soundness.” The It is also possible to activate and deactivate the same ttag job of certifying an extension against possible uses is much multiple times in the same book. Using the same name in harder than against actual uses, but in either case, the certi- the same file refers to the same ttag.
fier’s job will require some knowledge of ttags, the extension to leaving a ttag active where not needed, but when it’s mechanisms enabled by them, and ACL2 internals.
convenient, we suggest grouping together related dangerouscode.
Etiquette
Finally, although it is possible to declare ttags of different To ease certification and interoperability, a developer who names in the same book, we recommend instead the splitting uses trust tags should try to follow some rules that we pro- of more than one capability into separate books.
Naming Conventions. The canonical ttag name for “I Subsumption
just want to use some dangerous functions, and this is not There is no built-in notion of inheritance or subsumption going to affect anyone else” is T, as in (defttag t). Oth- with trust tags, so under that scheme, if a capability ttagged erwise, the name should be something short that describes as A depends on or includes a stand-alone capability B, both the capability that is added to ACL2 under that trust tag.
A and B would have to be authorized and both would show It could, for example, correspond to the name of an external up as having “tainted” the session.
tool, as in :MINISAT or :UCLID. We use the ttag :ACL2S toadd the capability for a session to talk to the ACL2s develop- One can easily imagine, however, wanting a mechanism for ment environment. An informative name helps to document one ttag to subsume others. A common idiom here is want- which potentially unsound extensions were used in reaching ing to encapsulate a piece of functionality into a book that requires authorization of one ttag, even if that book usesother reusable books that have their own ttags associated Uniqueness of names is not critically important, since use of with them. A trusting user of that book is concerned with a ttag always traces back to its location, but use of a docu- the function interface to that book, not which other books mentation string with DEFTTAG makes unique naming more We encourage use of a documentation string with a ttag so that a user can find out the capability pro- Recall that ttags enable us to do virtually anything, includ- vided by and authorship of a ttag with the :DOC command.
ing the modification of some settings and recorded history So to improve our likelihood of unique naming without being that allow ttag subsumption. We first save the state global too verbose, one might use the ttag :UCLID-GT rather than variable TTAGS-ALLOWED, governing which ttags are autho- :UCLID for code written by Georgia Tech students to inter- rized, and add to it which ttags we want to subsume. We face with an external tool called UCLID. A name like |Bob next save the world global value TTAGS-SEEN, which records which ttags have affected the current world. Then we exe- is interpreted by both the ACL2 loop and the Common cute the events that use the ttags we want to subsume, and Lisp compiler. Problems arise if compiled code attempts after we restore TTAGS-ALLOWED and TTAGS-SEEN to the old to change the world. Embedded event forms like DEFUN and values, ACL2 will not complain that we have used trust tags DEFTHM (see the ACL2 documentation for EMBEDDED-EVENT- FORM) are fine inside PROGN! because they have raw Lispdefinitions that do not affect the world, but directly calling This could be considered subversive behavior, but we con- INSTALL-EVENT, for example, is discouraged (if not illegal) sider it okay as long as it is done in a way that would be clear in a PROGN!, because it always modifies the world. Observe to a certifier. We provide a macro PROGN+SUBSUME-TTAGS that DEFUN calls INSTALL-EVENT, but only when executed in that handles the mechanics of such subsumption. See its the ACL2 loop. Outside the loop, DEFUN corresponds to the underlying Lisp’s DEFUN, which knows nothing of the ACL2world, and, thus, DEFUN is fine inside PROGN!.
BASIC EXTENSION MECHANISMS
Here we describe the ACL2 constructs that can only be used Third, PROGN! allows us to specify changes to ACL2 that when a trust tag is in effect. When appropriate, we also de- are not captured by the logical world, but does not support scribe more elegant abstractions that we have implemented “undoing” those changes in any way. For example, if we and make available in the supporting materials.
include a book that uses PROGN! to change the raw Lispdefinition of a function, that change is not reverted if we Arbitrary Code
undo the inclusion of the book! And if that raw Lisp codecalls user-defined ACL2 functions, the system breaks if those PROGN! is a basic building block for potentially dangerous ACL2 functions are undone. The only built-in, robust work- ACL2 extensions because it allows unprotected embedding around to this problem is to ensure the book is never undone of arbitrary code into certifiable books. Just as PROGN col- by executing (reset-prehistory t) within it or following lects many inputs into a single event, PROGN! does so with- its inclusion. As its documentation describes, this use of out the restriction that the inputs be embedded event forms.
RESET-PREHISTORY sets a new starting point for the world, And PROGN! does not protect logical state as MAKE-EVENT In response to these issues with PROGN!, we have developed SET-RAW-MODE also requires an active ttag and can be used a complementary construct that we call DEFCODE. DEFCODE in PROGN! to embed raw Lisp code in a book. For example, is able to “embed” code at some point in a book in four we could embed some code that turns off garbage collection different ways; thus, a call to DEFCODE is optionally given, for each of those different ways, a code block to embed inthat way: (set (intern "*NOTIFY-GBC*" "SI") :LOOP code is executed each time the DEFCODE form is exe- cuted by the ACL2 loop, such as in an INCLUDE-BOOKor each ACL2 pass of CERTIFY-BOOK or ENCAPSULATE.
Any code that modifies the world or checks that the Note that changing the raw mode setting inside a PROGN! current world is compatible with what we want to do does not propagate beyond its body, so a matching (set- should go under :LOOP. Like PROGN!, a soft error re- raw-mode nil) is not necessary. For some raw inputs, ACL2 turned by :LOOP code aborts further processing.
will complain about not knowing how many values are re-turned; this can be avoided by wrapping forms in (progn :LOOP code is typically used for checking that the cur- . nil). Considering these things, we define a convenient rent world is compatible with how we intend to extend abstraction (in-raw-mode .) to be (progn! (set-raw- it. It can also be used for embedded event forms and As a small limitation, we were not allowed to write (setq :COMPILE code is compiled and loaded by the underlying si::*notify-gbc* nil) because the code must be an ACL2 CERTIFY-BOOK and INCLUDE-BOOK (if book com- object, and ACL2 does not recognize GCL’s “SI” package.
pilation is chosen). This is the only code in a DEFCODE As shown, we can usually work around this problem by gen- seen by the Lisp compiler, so authors need not worry erating symbols from their constituent strings with about how other code (in particular, code specified by :LOOP) would be compiled. Further, this code is only seen by the Lisp compiler, so authors need not worry PROGN! in general has bigger caveats. First, the code can be executed several times, because of the dual passes of about how the ACL2 loop would execute it (though certify-book and/or encapsulate, because the code is part of the code itself must be constructed of ACL2 objects).
what is compiled and executed in raw Lisp if the containing :COMPILE code will typically only contain DEFUN and book is compiled, and because the containing book could DEFMACRO forms to be compiled in the underlying Lisp.
be “undone” and reloaded. Thus, code in PROGN! should beidempotent, though ACL2 provides no check for that.
:EXTEND code is executed each time the DEFCODE event is installed into the current ACL2 world. Except in error Second, we are limited in how we can safely modify the world cases, this happens after the ACL2 loop successfully inside a PROGN!. The reason is that code inside a PROGN! processes the :LOOP code. The :EXTEND code is also executed when a world is “resurrected”, as with the though it seems to recover, it is probably best to assume :EXTEND code will typically use IN-RAW-MODE to makesome modifications in raw Lisp or modify ACL2 state Note that using (in-raw-mode .) in the :COMPILE block is unnecessary, since that part is only used by the raw Lisp modify the world; ACL2 seems to catch the error and compiler. Eliminating the :COMPILE block would prevent the recover, but more importantly, it doesn’t make sense definition from being compiled during book compilation, but to extend the world in the middle of extending the it would still be possible to compile the function later with (in-raw-mode (compile ’x)) or similar.
:RETRACT code is executed each time the DEFCODE event is MAKE-EVENT is not supported inside DEFCODE, which is, per- retracted from the current ACL2 world, such as with haps, the only reason DEFCODE does not make PROGN! ob- :UBT or the multiple passes of CERTIFY-BOOK or EN- solete. In fact, PROGN! has recently been endowed with a CAPSULATE. :RETRACT code should undo the effect of capability that makes it well-suited for setting up modified the corresponding :EXTEND code, and it is an error for environments in which to process embedded event forms, including MAKE-EVENT. Specifically, PROGN! can optionallytake a list of state global variable bindings to pass to aSTATE-GLOBAL-LET* surrounding the body of the PROGN! To clarify the relationship between DEFCODE, PROGN!, and or- when it is processed in the ACL2 loop.
dinary book events, consider these inputs, which are equiv- bindings <bindings> <forms>), and writing the STATE-GLO-BAL-LET* in the body oneself, (progn! can be used in <forms> in the former but not in the lat- ter. See documentation for PROGN! and our implementation of PROGN+TOUCHABLE and PROGN+REDEF (described below) for It is very easy to make an ACL2 session inconsistent or As illustrated, DEFCODE separates the two interpretations ap- unsound by using DEFCODE, PROGN!, or SET-RAW-MODE. But plied to PROGN! code and ordinary book code, allowing more in later sections, we describe abstractions that make it easier customization. We do not need :EXTEND and :RETRACT in this case because the DEFUN in the :LOOP code extends theworld in a way that already causes ACL2 to update the Untouchables
raw definition of X on world extension/retraction. :EXTEND ACL2 untouchables, which include untouchable functions/ and :RETRACT cause the DEFCODE itself to update the world macros2 and untouchable state-global variables3, enable much with custom code that is executed on world extension and of ACL2 to be written in its own language while maintaining metatheoretic invariants on the logical state in the presenceof user code. As part of the ACL2 build process, the ACL2 Here is an example that defines a function only in raw Lisp, world is populated with a preset list of functions/macros using :EXTEND and :RETRACT code to associate the definition and variables that should be inaccessible to direct call or assignment by the user. If the user attempts to call an un-touchable function or macro or assign an untouchable state- global variable, either in code for immediate evaluation, in the body of a function definition, or in the macro expansion of either of those, an error results.
For example, INSTALL-EVENT is an untouchable function be- cause the user could use that function to install an arbitrary extension of the current world, including those that are logi- :extend ((in-raw-mode (defun x (y) (z y)))) cally inconsistent. ACL2-RAW-MODE-P is an untouchable vari- :retract ((in-raw-mode (fmakunbound ’x)))) able because assigning T to that variable would enter rawmode without authorization.
In that example, the :EXTEND block defines a function X But untouchable functions and variables are used on behalf in raw Lisp and the :RETRACT block removes that defini- of the user all the time. DEFTHM and DEFUN, for example, tion. We use the :LOOP block to check that X does not yet use INSTALL-EVENT to extend the world with the new for- have a raw function or macro definition. We choose this mulas, but only if they are found to be admissible. Thus, place for such checks rather than :EXTEND because (1) if the key for “touchable” functions that use untouchables is all raw definitions are managed properly with DEFCODE, we that they guarantee the untouchables are only used in ways can safely assume the check is satisfied in the case of world“resurrection”, and (2) throwing an error within :EXTEND 2(global-val ’untouchable-fns (w state)) or :RETRACT is typically difficult for ACL2 to recover from; 3(global-val ’untouchable-vars (w state)) that maintain the required invariants.
use redefinition to reach a contradiction. With a trust tag,however, it is possible to redefine any function, even in a cer- PUSH-UNTOUCHABLE allows the user to add to the list of un- tifiable book. Our PROGN+REDEF implements this capability, touchable functions or variables. Though no trust tag is enabling redefinition for the scope of its constituent events.
required for this operation, it will typically only be neededby hackers who create functions or use variables that need Because most of the ACL2 system is written in the ACL2 language, we can override its behavior with redefinition in PUT-GLOBALS that is able to assign values to any state-global the ACL2 loop. For example, the ACL2s “Recursion & In- variables, regardless of whether they are untouchable. Obvi- duction” mode, designed by J Moore, disables automatic, ously, this function needs to be untouchable to the untrusted heuristically-chosen induction by the theorem prover, and this is implemented by redefining a few system functions.
Also important is the ability for a trusted user to use un- The main caveat of redefining these functions is that we touchables in building potentially unsound extensions to should avoid changes that could lead to a logical contradic- ACL2. REMOVE-UNTOUCHABLE, which is the inverse of PUSH- tion. This first means we should not redefine a function in UNTOUCHABLE and requires an active ttag, was the first way the logic (:LOGIC mode) unless the new version computes the of getting access to untouchables from user ACL2 code, but same function (presumably in a different way). Fortunately, we decided to discourage its use in favor of a new construct most of the functions that we would want to behave differ- that better captured the notion of making some functions ently are not defined in the logic but are in :PROGRAM mode.
or variables touchable with the intention of making them But even :PROGRAM mode functions can affect the logic in two ways: macro expansion and promotion to :LOGIC mode.
Thus, we introduced a notion of temporary touchability, :PROGRAM mode functions, including those that take single- captured in two (untouchable) state-global variables: TEMP- threaded objects (stobjs) such as STATE4 can be used to TOUCHABLE-FNS and TEMP-TOUCHABLE-VARS. These have touch- define macros, and logical consistency of ACL2 depends on able “updater” functions SET-TEMP-TOUCHABLE-FNS and SET- macros expanding in the same way in any extension of a TEMP-TOUCHABLE-VARS respectively, which require an active world. :PROGRAM mode functions can also be promoted to trust tag to access. Each of these variables is bound to either :LOGIC mode with VERIFY-TERMINATION if they meet defini- a (potentially empty) list of symbols that are temporarily touchable or T, indicating all fns or vars are touchable.
As of Version 3.2, ACL2 has a way of disabling these loop- One might ask why we did not choose a simpler solution of holes on a function-by-function basis. Specifically, if a :PROGRAM disabling untouchable checking when a ttag is active. The mode function is (re)defined after its name has been added answer is to make the job of the certifier easier. Rather than to the state global variable BUILT-IN-PROGRAM-MODE-FNS, it needing to check through all ttagged code for use of untouch- can no longer be used in macro expansion or promoted to ables, the certifier can check just those places in which there :LOGIC mode. These are insignificant concessions that take are temporary touchables. We make it easy for the author to care of the loopholes. Note that BUILT-IN-PROGRAM-MODE-FNS identify to the certifier those places where untouchables are is untouchable, so a ttag is required to manipulate it.
made temporarily touchable, by way of abstractions basedon the ACL2 event aggregator PROGN. Our PROGN+TOUCHABLE We offer an event ENSURE-PROGRAM-ONLY that first asserts and PROGN=TOUCHABLE add to and override (respectively) the that a function is defined only in :PROGRAM mode, and then set of temporarily touchable fns and vars for a sequence of adds it to BUILT-IN-PROGRAM-MODE-FNS if not already there.
Note that this change is not tied to the world and so isnot undoable in the traditional sense, but one could fix this An example application of using an untouchable function in developing a system-level extension is in the “super his-tory” code for ACL2s, whose script management interface Another subtle caveat of redefinition is that if a function has calls for a more powerful notion of undoing and redoing a raw Lisp definition that does not match its ACL2 defini- commands than standard ACL2 has. Among other things, tion, redefining it based on modifying its ACL2 definition our code saves “the world” after each command is executed, can cause problems. In fact, ACL2 utilizes many such func- and to revert to a previous logical state, we must reinstall tions, because they bridge the gap between the functionality an old world with SET-W!, which is untouchable.
available in the ACL2 programming world and that available wrap the definition of the appropriate function with (progn+ in raw Lisp. Unfortunately, ACL2 does not currently keep touchable :fns set-w! .). To maintain soundness, the track of which built-in functions are in this category, so we ACL2s code (if correct) only installs legitimate old worlds.
introduce a state global variable HAS-SPECIAL-RAW-DEFINITION, This is part of the trust involved in using the ACL2s script which should contain a list of all function names with a raw definition that is not observationally equivalent to its ACL2definition.
Redefinition
GOOD-BYE-FN, for example, has a function body of NIL in The ACL2 user can turn on a setting that allows redefini- ACL2, but it has a raw Lisp definition that exits the un- tion of user functions from the command loop without us-ing a ttag, but the user cannot certify a book in a world in 4Stobjs are not available in the macro language, but logical which functions have been redefined, because one can easily counterparts can be used in their place.
derlying Lisp process. Redefining this function in the ACL2 Raw-only Definitions
loop would cause the function to lose its special behavior, We define functions that safely add raw Lisp definitions from so it should be in HAS-SPECIAL-RAW-DEFINITION and should within the ACL2 loop. They are safe because definitions are only have its behavior changed by modifying its raw defini- made only if the names to be defined are not in use by ACL2 or raw Lisp. These use DEFCODE to associate the definitionswith the ACL2 world, enabling them to be undone and even We define ENSURE-SPECIAL-RAW-DEFINITION-FLAG to add to the list HAS-SPECIAL-RAW-DEFINITION, for example whenchanging the raw definition of an ACL2 function, and ASSERT- The names are DEFUN-RAW, DEFMACRO-RAW, DEFSTRUCT-RAW, NO-SPECIAL-RAW-DEFINITION to assert something is not on DEFPARAMETER-RAW, DEFVAR-RAW, and DEFCONSTANT-RAW, which the list, for example when redefining a function in the ACL2 of course correspond to their Common Lisp counterparts loop. In the future, the list might automatically be initial- without “-RAW” in the name. (See the summary below for ized with all the appropriate entries, but presently, we only include some such built-in functions that have been manu-ally listed.
DEFSTRUCT-RAW is the most complex because it figures outwhat functions would be defined by the underlying raw Lisp External Interaction
DEFSTRUCT. This one is special also because there is no portableway to undo a DEFSTRUCT in Common Lisp. We can, how- Trust tags also enable connecting the proof engine with arbi- ever, unbind all the functions defined by the event.
trary ACL2 code, via clause processors [7], and allow ACL2code to write to arbitrary files, via OPEN-OUTPUT-CHANNEL!, These functions also “stub out” the ACL2 names (with DEF- and run arbitrary programs, via SYS-CALL. Each of these LABEL) for which they give a definition in raw Lisp. This can alone render ACL2 unsound, as described in their re- ensures that later ACL2 definitions will not interfere with spective documentation, which is why they require a trust tag. These are important to the overall picture of hackingand extending ACL2, but are not the focus of this paper.
Also, these functions respect a non-nil LD-REDEFINITION- ACTION by removing the requirement that the names notbe in use. If in use in ACL2, though, they must only be ACL2 labels to proceed, as would be the case if the names Here are the abstractions we recommend for basic extension.
were introduced using one of our “-RAW” functions. This Some are built-in and the rest are defined in the accompa- should not be viewed as a shortcoming, though, since the next section describes a meaningful way of changing the rawdefinition of ACL2 functions.
• (defcode [:loop <loop-code>] [:compile <raw-compile-code>] [:extend <extend-code>] Bridging Raw Lisp and ACL2
The ACL2 loop rightly prohibits the definition of functionsthat depend on functions or constants defined only in raw • (progn! [:state-global-bindings <bindings>] Lisp. The way to bridge this gap is to let an ACL2 function have a special raw definition, as we described with HAS-SPECIAL-RAW-DEFINITION. Our DEFUN-BRIDGE creates new ACL2 functions that are implemented as special raw defi-nitions, and our MODIFY-RAW-DEFUN adds to or replaces the • (progn+touchable [:fns <fns-or-:all>] [:vars functionality of an existing raw function definition.
<vars-or-:all>] <event-form>*) DEFUN-BRIDGE appears much like DEFUN except that it takes • (progn=touchable [:fns <fns-or-:all>] [:vars declarations and a body for ACL2 and declarations and a <vars-or-:all>] <event-form>*) body for raw Lisp. It first asserts no previous raw or ACL2definitions (unless calls ENSURE-PROGRAM-ONLY and ENSURE-SPECIAL-RAW-DEF- INITION-FLAG to avoid caveats described above. Then the :PROGRAM-mode ACL2 definition is made, and the custom raw Lisp definition is installed. We do not support ensure-special-raw-definition-flag <fn>*) mode for DEFUN-BRIDGE because it is intended for new metathe- assert-no-special-raw-definition <fn>*) MODIFY-RAW-DEFUN, on the other hand, can be applied to any HIGH-LEVEL EXTENSION IDIOMS
raw function definition, whether it has a :LOGIC-mode ACL2 Whereas the previous section focused on low-level constructs definition, a :PROGRAM-mode ACL2 definition, or no function and how they support hacking, we now focus on coherent, definition at all in ACL2. MODIFY-RAW-DEFUN allows building high-level idioms for hacking ACL2, abstractions we provide a new raw definition of a function using the old definition that take care of low-level details, and how these idioms can as a “black box” function in the new definition. This code be used and combined to customize ACL2 in deep ways.
from ACL2s, for example, disables GOOD-BYE for the user: one call of REVERT-WORLD-ON-ERROR with ACL2s’s REVERT- SUPERHIST-ON-ERROR if we are in the top-most command loop. (The purpose of this change is to revert other impor- tant ACL2 settings on error, in addition to the world. For example, in pure ACL2 (er-progn (set-guard-checking nil) (defun foo (x) (foo y))) would have a side effect of disabling guard checking even though the (defun foo .) failed, but ACL2s’s “super history” reverts the setting.) ld-read-eval-print(:pat (revert-world-on-error %form%) The definition that was attached to GOOD-BYE-FN is now globally attached to ORIGINAL-GOOD-BYE-FN, and GOOD-BYE- FN now throws an error in some cases rather than invoking (revert-superhist-on-error %form%)(revert-world-on-error %form%)))) Redefining System Functions
The :PAT specifies a pattern to match in the body of the If a :PROGRAM-mode system function does not have a special function; everything matches only itself, except for sym- raw definition, however, we can change its behavior with bols among the :VARS and :RECVARS (both optional), each of more control by using the ACL2 loop to redefine the func- which match any one thing. By convention, we put percent tion. In this case, we can look up the old body in the world, signs around our variables to make them stand out. :MULT modify it according to our changes, and then use redefinition asserts that the rule is applied a certain number of times, or within some range; an error is returned if there are too manyor too few matches. :REPL is what the pattern is replaced Our REDEFUN looks just like a DEFUN but it takes care of all by after substituting the values of the variables.
the details that promote soundness-preservation: checkingthat the existing definition is one we can overwrite, check- In the above example, the pattern and replacement are rather ing that the new definition has the same input and output simple, matching any call to REVERT-WORLD-ON-ERROR, since signature, and calling ENSURE-PROGRAM-ONLY to keep it out variables such as %FORM% can match anything.
of the logic. No LD-REDEFINITION-ACTION setting is required teresting is that we used :RECVARS instead of :VARS and to use REDEFUN, but it does, of course, require an active trust added :MULT 1. Specifying :MULT 1 causes the translation to fail if we rewrite more than one instance of REVERT-WORLD-ON-ERROR. Using :RECVARS instead of :VARS in this A more flexible version of REDEFUN is our REDEFUN+REWRITE, case means that we also search for uses of REVERT-WORLD- which computes the new function body based on applying ON-ERROR nested within other uses, because if a variable is specified transformations to the old body. Here we take full in :RECVARS, then the current “simultaneous” set of rules is advantage of the fact that, like Lisp, ACL2 code is composed applied to the binding of that variable before using it in the REDEFUN+REWRITE’s first parameter is the name of the func- We have used our code rewrite specification language to tion to modify, and any subsequent parameters comprise a specify how to change the call to REVERT-WORLD-ON-ERROR in code rewrite specification for transforming the body. Note LD-READ-EVAL-PRINT, and to force reexamination of the sit- that these “rewrite specs” have no connection with ACL2 uation if and only if there is not exactly one REVERT-WORLD- rewrite rules, which solve a significantly different problem.
ON-ERROR in that function. There are more features to the Specifically, ACL2 rewrite rules are for simplifying new ex- code rewriting, and the above description is far from a speci- pressions we might encounter; our code rewrite specs are fication. See the supporting materials for more information.
for changing the meaning of known code, modulo any non-interfering changes. Each uses “rules” for specifying piecesof translation, but ACL2 rewrite rules are “semantic” in the Copying Definitions
sense that they refer to properties of functions applied to On many occasions we have wanted to create a new function values, while our code rewrite rules are “syntactic” in that based on the definition of an existing function. For exam- they refer to code independent of its meaning or interpre- ple, before redefining a function whose behavior we want to tation and can universally quantify over raw syntax. Our change, we might define another function in the same way to code rewrite rules can be recursive, but in a way that is preserve the old functionality under a different name. We well-founded, so that we never get stuck looping in transla- provide some constructs to accommodate this and similar tion. Finally, the order of rule application is easily defined, giving our translations only one interpretation.
From the ACL2 loop, our COPY-RAW-DEFUN is a safe way Let us consider an example from ACL2s, in which we mod- of defining a raw Lisp function to be exactly the same as ify some functionality of the top-level ACL2 read-eval-print 5To make the recursion well-founded, we prohibit the case loop. Specifically, in LD-READ-EVAL-PRINT, we replace the in which the pattern is a stand-alone RECVAR.
another. The copy is direct, in the sense that if the func- We have used these dynamic extension mechanisms quite tion associated with the source symbol changes, the function successfully for the ACL2s development environment. Whereas associated with the destination is unchanged, except as it we used to require building a custom ACL2 image with our refers back to the source function. Using COPY-RAW-DEFUN on communication hooks, we can now load them into a stan- recursive functions, therefore, can give undesirable results.
dard ACL2 image as we would a book of theorems. In ad- MODIFY-RAW-DEFUN actually uses COPY-RAW-DEFUN in its im- dition, it is easier to adapt our changes to new versions of plementation. COPY-RAW-DEFMACRO is analogous for raw Lisp ACL2, because our method of specifying changes is based on structured syntax, and can be made as sensitive to otherchanges as is appropriate for each of our changes. Dynamic COPY-DEFUN uses a MAKE-EVENT to generate a DEFUN event extension has also enabled us to package an automatic termi- that defines a destination function from a source ACL2 func- nation analysis based on calling context graphs (CCGs) [5] Later redefinition of the source does not as a book that can be used orthogonally from the rest of modify the destination, but COPY-DEFUN, like REDEFUN+RE- WRITE, asserts that the source definition at inclusion timebe the same as it was at certification time. COPY-DEFUN+RE- We hope these features encourage the development of new, WRITE is like COPY-DEFUN except it uses a REDEFUN+REWRITE- innovative extensions of ACL2. That said, we recommend like specification to transform the copied function body.
the use of ACL2’s built-in mechanisms for customizationand extension (from rewrite rules to MAKE-EVENT) before re- sorting to the types of extension we have described.
• (defun-raw <name> <ll> <decl>* <body>) ACKNOWLEDGEMENTS
• (defmacro-raw <name> <ll> <decl>* <body>) We thank Sandip Ray, Erik Reeber, and J Moore for useful contributions to conversations on topics of this paper. We (defstruct-raw <name-and-opts> <slot desc>+) also thank Daron Vroon for being a gracious customer and • (defvar-raw <name> [<initial-value>]) • (defparameter-raw <name> <initial-value>) REFERENCES
• (defconstant-raw <name> <initial-value>) [1] P. C. Dillinger, P. Manolios, D. Vroon, and J. S. Moore.
ACL2s: The ACL2 Sedan. In Proceedings of the User • (defun-bridge <name> <ll> [:doc <doc-string>] Interfaces for Theorem Provers workshop (UITP), [:loop-declare <decl-lst>] :loop <acl2-body> 2006. ENTCS, 2006. Part of FLOC ’06.
[:raw-declare <decl-lst>] :raw <raw-body>) [2] E. L. Gunter. Adding External Decision Procedures to HOL90 Securely. In Proceedings of the 11th • (modify-raw-defun <name> <name-for-old> <ll> International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1998), volume 1479 of • (redefun <name> <ll> <decl>* <body>) LNCS, pages 143–152. Springer-Verlag, 1998.
[3] M. Kaufmann, P. Manolios, and J. S. Moore, editors.
• (redefun+rewrite <name> <rewrite-spec>*) Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer Academic Publishers, June 2000. See URL • (copy-defun <src-name> <dst-name>) • (copy-defun+rewrite <src-name> <dst-name> [4] M. Kaufmann, P. Manolios, and J. S. Moore.
Computer-Aided Reasoning: An Approach. Kluwer CONCLUSION
Academic Publishers, July 2000. See URLhttp://www.cs.utexas.edu/users/moore/- The first contribution of this paper is a discussion of trust tags in ACL2. We describe their motivation, when a trust [5] M. Kaufmann, P. Manolios, J. S. Moore, and D. Vroon.
tag is appropriate, and how to use them when appropriate.
Integrating CCG analysis into ACL2. In Eighth Trust tags open up ACL2 constructs that are dangerous in International Workshop on Termination, August 2006.
the sense that they can render ACL2 unsound or even ef- fect malice on a user’s computer, but they also facilitate [6] M. Kaufmann and J. S. Moore. ACL2 homepage. See unprecedented runtime customization of ACL2.
URL http://www.cs.utexas.edu/users/moore/acl2.
The other contribution of this paper is a set of ACL2 ex- [7] M. Kaufmann, J. S. Moore, S. Ray, and E. Reeber.
tensions for modifying and extending ACL2. In the pro- Integrating External Deduction Tools with ACL2. In cess of hacking ACL2 in various ways, we have produced a Proc. of the 6th International Workshop on nice set of dynamic extension idioms that promote sound- Implementation of Logics (IWIL 2006), volume 212 of ness preservation, safe mixing of extensions, and checking CEUR Workshop Proceedings, pages 7–26, 2006.
of incompatibilities. These idioms bear some resemblance Expanded version to appear, Journal of Applied Logic.
to aspect-oriented programming; we can specify where and [8] P. Manolios and S. Srinivasan. Verification of how to insert or change code. We also attach changes to executable pipelined machines with bit-level interfaces.
the ACL2 world, so that, if we so choose, the normal undo In ICCAD-2005, International Conference on mechanisms can revert our code changes.

Source: http://www.cs.uwyo.edu/~ruben/acl2-07/uploads/Main/001.pdf