		Search-engine friendly clone of the ACL2 documentation.

Wormhole-programming-tips

some tips for how to use wormholes

Wormholes allow one to collect data and print without having access to ACL2's state. Many ACL2 utilities are implemented in terms of wormholes. Examples include break-rewrite, accumulated-persistence, and forward-chaining-reports. So an ACL2 developer wishing to add features or fixing misbehaviors in these system utilities must be familiar with programming wormholes. But users might also employ wormholes to implement utilities in their own models. Thus, this documentation topic is as much for future ACL2 developers and maintainers as for ACL2 users (but items meant primarily for developers often include references to functions in the ACL2 source code which other users may just ignore). This is simply a list of tips for a person programming with wormholes. This list doesn't replace the topics wormhole and wormhole-eval, and their subtopics including the particularly relevant wormhole-status. But this list of tips might serve as a useful reminder when you're programming with wormholes.

The “function” wormhole is really a macro that expands in raw Lisp into a call of wormhole-eval to set the entry code and then a call of wormhole1 to do the interactive work. But in addition, the source code functions ev-rec, translate11-wormhole-eval, translate11-call-1, and translate11-call all contain special provisions for wormholes. Do not think you can add features to wormholes by just changing the definition of wormhole or wormhole1! These functions are in what we call the wormhole implementation nexus and there is entitled ``; Essay on the Wormhole Implementation Nexus” in the source file axioms.lisp.
The built-in ACL2 system wormholes are protected by mechanisms in translate11-call-1 and translate11-call so that code executed during ACL2's boot-strapping process is allowed to manipulate system wormholes but code executed after boot-strap cannot. Search the source code for occurrences of *protected-system-wormhole-names*.
System implementors and maintainers may be hampered by being unable to invoke wormhole functions on system wormholes like brr or accumulated-persistence. One way around that, e.g., to test changes to existing code, is to execute (defconst *protected-system-wormhole-names* nil) after doing (redef+).
Users may wish to employ wormholes so they can build tools allowing the state-less exploration of their models. But we confess that to make wormholes as useful to other tool developers as they are to the ACL2 developers we will need to add some protection features (similar to those in the item above) to user-defined wormholes. Ideas we have toyed with but not implemented include pairing a wormhole's name with various attributes such as a flag to prevent its use except through named interfaces, a wrapper form or filter that applies to every form read, translated, and evaluated by the ld inside that wormhole, and what should happen when the wormhole is exited. But these ideas are not implemented. If you really need them, let us know.
Each wormhole has a name, which is typically but not necessarily a symbol.
Each wormhole has a current status. The status is a cons whose car is either :ENTER or :SKIP, and whose cdr is an arbitrary ACL2 object managed by the creator of the wormhole. The car of the status is called the “entry code”. The cdr is called the “data”. See wormhole-entry-code, wormhole-data, and make-wormhole-status.
The status object of a wormhole named nm is stored in raw Lisp in a part of memory inaccessible to ACL2 terms other than the ACL2 oracle (see read-ACL2-oracle). We call this the persistent wormhole status or persistent-whs. If you're in raw Lisp — which you can reach by exiting the ACL2 loop with :q or by invoking break$ — you can recover the persistent-whs of the nm wormhole with (cdr (assoc nm *wormhole-status-alist*)). However, the logic-mode function get-persistent-whs takes a name and state returns an error triple containing the persistent status. Get-persistent-whs reads the ACL2 oracle (see read-ACL2-oracle) to get the otherwise hidden status of the wormhole. In doing so it changes the state. So if you're not in a context in which you have state and can return a modified state, you can't use get-persistent-whs.
Wormhole-eval gives you a way, without access to state, to set the persistent-whs of a named wormhole as a function of its current persistent-whs. Wormhole-eval takes a wormhole name, a lambda expression, and a term (which is functionally irrelevant), applies the lambda expression to the persistent-whs, stores as the new persistent-whs, and returns nil.
Wormhole is a function that allows you to set and test the status of a named wormhole and if the resulting status has an entry code of :enter you will enter a read-eval-print loop. Wormhole has two other arguments, the so-called ``input'' object and the ``first form'' to execute if and when the loop is entered.
The read-eval-print loop is managed by ld, the same function that manages ACL2's top-level read-eval-print loop. The wormhole function allows you to specify the standard ld variables (e.g., ld-error-action, etc.). One of those variables is ld-keyword-aliases which specifies the behaviors of keyword commands issued in the wormhole's loop.

Before wormhole (actually wormhole1) calls ld it sets the three important state global variables mentioned below. Then while in the interactive loop:

(@ wormhole-name) = nm

(@ wormhole-input) = the ``input'' object supplied to wormhole

(@ wormhole-status) = the wormhole's persistent-whs at the time of entry

When inside the interactive loop of the wormhole we call the value of wormhole-status the ephemeral wormhole status or ephemeral-whs. It ``disappears'' when the wormhole is exited but it is easy to read without changing state while inside the wormhole.
The ``first form'' is very often the only form executed! We typically use that form to grab the input and the status and print stuff. Then the first form returns (value :q). Recall that typing (value :q) to the ACL2 loop (i.e., to ld) exits the loop, which exits the wormhole. See the example in the documentation topic wormhole, starting with "(wormhole 'demo". If the first form returns any other non-erroneous value triple, user input is read and evaluated. So if your first form always returns (value :q) you're in complete control of your wormhole — and if it doesn't, you're not because the next thing that happens is the wormhole reads and evaluates whatever the user types!
The use of ld to manage the read-eval-print loop means that the user can execute virtually any ACL2 term. If you use wormhole and allow input from the user, you have no control over the operations performed.
If, while in the nm wormhole, you execute (wormhole-eval nm ...) it will set the persistent-whs but not set the ephemeral-whs. (Recall, wormhole-eval does not have access to state.) This means that you can't trust (@ wormhole-status) after a call of wormhole-eval — or of any function that calls wormhole-eval — from within the wormhole.
This brings us to the Wormhole Coherence Convention. The problem described in the bullet above is akin to the cache coherence problem. Think of the persistent-whs stored in *wormhole-status-alist* as being stored in a distant memory location and the ephemeral-whs stored in (@ wormhole-status) as a nearby, easily accessible cache when you're in the wormhole. Wormhole-eval reads and writes the persistent-whs and does not update the cache. The Wormhole Coherence Convention is to keep persistent-whs and the ephemeral-whs equal. Of course, the convention is meant to hold except in the region of code between updating the two locations.
The wormhole programmer is responsible for maintaining the wormhole coherence — or not. It's up to you. But remember: if your wormhole permits user interaction, you can't prevent the execution of certain forms.
The state global variable wormhole-status is untouchable, so the user cannot just execute (assign wormhole-status new-status) to change it. But wormhole-status can be changed by certain special functions available to the user, namely sync-ephemeral-whs-with-persistent-whs and set-persistent-whs-and-ephemeral-whs, though these will only have effect after executing wormhole-eval or wormhole.
We have already mentioned wormhole-eval, which writes to the persistent-whs not to the ephemeral-whs. But the other two utilities mentioned above are helpful in establishing and maintaining coherence.
(sync-ephemeral-whs-with-persistent-whs nm state) moves the ``distant'' memory status into the cached status. It returns the modified state.
(set-persistent-whs-and-ephemeral-whs nm new-status state) writes new-status to the persistent-whs of nm and, if you're in the wormhole nm, it also updates the ephemeral-whs status. It returns a new state.
Using sync-ephemeral-whs-with-persistent-whs and set-persistent-whs-and-ephemeral-whs you can program your wormhole operations to establish and maintain coherence. But you can't prevent the user from breaking it if you allow user interaction.
While it may seem that set-persistent-whs-and-ephemeral-whs is the preferred way to update the status of a wormhole, that function suffers from the requirement that you have to have the new status in hand when you call set-persistent-whs-and-ephemeral-whs. So from a practical perspective set-persistent-whs-and-ephemeral-whs is either used outside the wormhole to initialize the status to some standard value or is used inside the wormhole after having obtained the current status from the cache and modifying it to create the new status.
Both sync-ephemeral-whs-with-persistent-whs and set-persistent-whs-and-ephemeral-whs take and return state and so can only be used in contexts allowing that.
In contrast, wormhole-eval allows you to compute the new status as a function of the old status, WITHOUT HAVING PRIOR ACCESS to the old status and without access to state. But then remember to call sync-ephemeral-whs-with-persistent-whs, which will restore coherence.
The most direct way to establish and maintain the wormhole coherence is to avoid use of fully interactive calls of wormhole (i.e., make sure the first form executed always returns (value :q)), and do all modifications to the wormhole status with wormhole-eval, which reads and writes the persistent-whs. For example, search the ACL2 sources for occurrences of 'accumulated-persistence. You'll see wormhole-eval is used to collect all the data. Then in show-accumulated-persistence-fn, wormhole is used to display the data and exit with (value :q).
But the break-rewrite wormhole, named brr, is necessarily different because the whole intention is to allow interaction with the user! So there is special code here and there throughout ACL2 to maintain coherence. We're sorry we don't provide suitable provisions for other users!
If you're in a wormhole, all modifications to state globals during the execution of the commands in the read-eval-print loop will be undone when the loop is exited. This cleanup is done in the raw Lisp code for wormhole1, by evaluating the raw Lisp form held in *wormhole-cleanup-form*. That form is destructively modified every time an f-put-global is executed from within some wormhole. The modification introduces code to undo each f-put-global and restore the previous values.
The cleanup form just mentioned contains special code for the break-rewrite wormhole! Look for 'brr in wormhole1 and read the comments.