## USING-COMPUTED-HINTS-2

One Hint to Every Top-Level Goal in a Forcing Round
```Major Section:  MISCELLANEOUS
```

Suppose the main proof completes with a forcing round on three subgoals, "[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1". Suppose you wish to `:use lemma42` in all top-level goals of the first forcing round. This can be done supplying the hint

```(if test '(:use lemma42) nil),
```
where `test` is an expression that returns `t` when `ID` is one of the clause ids in question.
```    goal-spec     (parse-clause-id goal-spec)

"[1]Subgoal 3"        ((1) (3) . 0)
"[1]Subgoal 2"        ((1) (2) . 0)
"[1]Subgoal 1"        ((1) (1) . 0)
```
Recall (see clause-identifier) that `parse-clause-id` maps from a goal spec to a clause id, so you can use that function on the goal specs printed in the failed proof attempt to determine the clause ids in question.

So one acceptable `test` is

```(member-equal id '(((1) (3) . 0)
((1) (2) . 0)
((1) (1) . 0)))
```
or you could use `parse-clause-id` in your computed hint if you don't want to see clause ids in your script:
```(or (equal id (parse-clause-id "[1]Subgoal 3"))
(equal id (parse-clause-id "[1]Subgoal 2"))
(equal id (parse-clause-id "[1]Subgoal 1")))
```
or you could use the inverse function (see clause-identifier):
```(member-equal (string-for-tilde-@-clause-id-phrase id)
'("[1]Subgoal 3"
"[1]Subgoal 2"
"[1]Subgoal 1"))
```

Recall that what we've shown above are the tests to use in the computed hint. The hint itself is `(if test '(:use lemma42) nil)` or something equivalent like `(and test '(:use lemma42))`.

The three tests above are all equivalent. They suffer from the problem of requiring the explicit enumeration of all the goal specs in the first forcing round. A change in the script might cause more forced subgoals and the ones other than those enumerated would not be given the hint.

You could write a test that recognizes all first round top-level subgoals no matter how many there are. Just think of the programming problem: how do I recognize all the clause id's of the form `((1) (n) . 0)`? Often you can come to this formulation of the problem by using `parse-clause-id` on a few of the candidate goal-specs to see the common structure. A suitable test in this case is:

```(and (equal (car id) '(1))     ; forcing round 1, top-level (pre-induction)
(equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
(equal (cddr id) 0))      ; no primes
```

The test above is ``overkill'' because it recognizes precisely the clause ids in question. But recall that once a computed hint is used, it is removed from the hints available to the children of the clause. Thus, we can widen the set of clause ids recognized to include all the children without worrying that the hint will be applied to those children.

In particular, the following test supplies the hint to every top-level goal of the first forcing round:

```(equal (car id) '(1))
```
You might worry that it would also supply the hint to the subgoal produced by the hint -- the cases we ruled out by the ``overkill'' above. But that doesn't happen since the hint is unavailable to the children. You could even write:
```(equal (car (car id)) 1)
```
which would supply the hint to every goal of the form "[1]Subgoal ..." and again, because we see and fire on the top-level goals first, we will not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2) . 0) even though the test recognizes that id.

Finally, the following test supplies the hint to every top-level goal of every forcing round (except the 0th, which is the ``gist'' of the proof, not ``really'' a forcing round):

```(not (equal (car (car id)) 0))
```

Recall again that in all the examples above we have exhibited the `test` in a computed hint of the form `(if test '(:key1 val1 ...) nil)`.

## USING-COMPUTED-HINTS-3

Hints as a Function of the Goal (not its Name)
```Major Section:  MISCELLANEOUS
```

Sometimes it is desirable to supply a hint whenever a certain term arises in a conjecture. For example, suppose we have proved

```(defthm all-swaps-have-the-property
(the-property (swap x))
:rule-classes nil)
```
and suppose that whenever `(SWAP A)` occurs in a goal, we wish to add the additional hypothesis that `(THE-PROPERTY (SWAP A))`. Note that this is equivalent supplying the hint
```(if test
'(:use (:instance all-swaps-have-the-property (x A)))
nil)
```
where test answers the question ``does the clause contain `(SWAP A)`?'' That question can be asked with `(occur-lst '(SWAP A) clause)`. Briefly, `occur-lst` takes the representation of a translated term, x, and a list of translated terms, y, and determines whether x occurs as a subterm of any term in y. (By ``subterm'' here we mean proper or improper, e.g., the subterms of `(CAR X)` are `X` and `(CAR X)`.)

Thus, the computed hint:

```(if (occur-lst '(swap a) clause)
'(:use (:instance all-swaps-have-the-property (x A)))
nil)
```
will add the hypothesis `(THE-PROPERTY (SWAP A))` to every goal containing `(SWAP A)` -- except the children of goals to which the hypothesis was added.

A COMMON MISTAKE users are likely to make is to forget that they are dealing with translated terms. For example, suppose we wished to look for `(SWAP (LIST 1 A))` with `occur-lst`. We would never find it with

```(occur-lst '(SWAP (LIST 1 A)) clause)
```
because that presentation of the term contains macros and other abbreviations. By using :trans (see trans) we can obtain the translation of the target term. Then we can look for it with:
```(occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)
```
Note in particular that you must
```* eliminate all macros and
* explicitly quote all constants.
```
We recommend using `:trans` to obtain the translated form of the terms in which you are interested, before programming your hints.

An alternative is to use the expression `(prettyify-clause clause)` in your hint to convert the current goal clause into the s-expression that is actually printed. For example, the clause

```((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))
```
``prettyifies'' to
```(IMPLIES (AND (CONSP X)
(NOT (SYMBOLP Y)))
(EQUAL (CONS 1 (CAR X)) Y))
```
which is what you would see printed by ACL2 when the goal clause is that shown.

However, if you choose to convert your clauses to prettyified form, you will have to write your own explorers (like our `occur-lst`), because all of the ACL2 term processing utilities work on translated and/or clausal forms. This should not be taken as a terrible burden. You will, at least, gain the benefit of knowing what you are really looking for, because your explorers will be looking at exactly the s-expressions you see at your terminal. And you won't have to wade through our still undocumented term/clause utilities. The approach will slow things down a little, since you will be paying the price of independently consing up the prettyified term.

We make one more note on this example. We said above that the computed hint:

```(if (occur-lst '(swap a) clause)
'(:use (:instance all-swaps-have-the-property (x A)))
nil)
```
will add the hypothesis `(THE-PROPERTY (SWAP A))` to every goal containing `(SWAP A)` -- except the children of goals to which the hypothesis was added.

It bears noting that the subgoals produced by induction and top-level forcing round goals are not children. For example, suppose the hint above fires on "Subgoal 3" and produces, say, "Subgoal 3'". Then the hint will not fire on "Subgoal 3'" even though it (still) contains `(SWAP A)` because "Subgoal 3'" is a child of a goal on which the hint fired.

But now suppose that "Subgoal 3'" is pushed for induction. Then the goals created by that induction, i.e., the base case and induction step, are not considered children of "Subgoal 3'". All of the original hints are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1. That top-level forced subgoal is not a child. All the original hints are available to it. Thus, if it contains `(SWAP A)`, the hint will fire and supply the hypothesis, producing "[1]Subgoal 1'". This may be unnecessary, as the hypothesis might already be present in "[1]Subgoal 1". In this case, no harm is done. The hint won't fire on "[1]Subgoal 1" because it is a child of "[1]Subgoal 1" and the hint fired on that.

## USING-COMPUTED-HINTS-4

Computing the Hints
```Major Section:  MISCELLANEOUS
```

So far we have used computed hints only to compute when a fixed set of keys and values are to be used as a hint. But computed hints can, of course, compute the set of keys and values. You might, for example, write a hint that recognizes when a clause ``ought'' to be provable by a `:BDD` hint and generate the appropriate hint. You might build in a set of useful lemmas and check to see if the clause is proveable `:BY` one of them. You can keep all function symbols disabled and use computed hints to compute which ones you want to `:EXPAND`. In general, you can write a theorem prover for use in your hints, provided you can get it do its job by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of `(SWAP x)` and provide the corresponding instance of `ALL-SWAPS-HAVE-THE-PROPERTY`. Obviously, we must explore the clause looking for instances of `(SWAP x)` and build the appropriate instances of the lemma. We could do this in many different ways, but below we show a general purpose set of utilities for doing it. The functions are not defined in ACL2 but could be defined as shown.

Our plan is: (1) Find all instances of a given pattern (term) in a clause, obtaining a set of substitutions. (2) Build a set of `:instance` expressions for a given lemma name and set of substitutions. (3) Generate a `:use` hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term in either a term or a list of terms. The functions each return a list of substitutions, each substitution accounting for one of the matches of pat to a subterm. At this level in ACL2 substitutions are lists of pairs of the form `(var . term)`. All terms mentioned here are presumed to be in translated form.

The functions take as their third argument a list of substitutions accumulated to date and add to it the substitutions produced by matching pat to the subterms of the term. We intend this accumulator to be nil initially. If the returned value is nil, then no instances of pat occurred.

```(mutual-recursion

(defun find-all-instances (pat term alists)
(declare (xargs :mode :program))
(mv-let
(instancep alist)
(one-way-unify pat term)
(let ((alists (if instancep (add-to-set-equal alist alists) alists)))
(cond
((variablep term) alists)
((fquotep term) alists)
((flambdap (ffn-symb term))
(find-all-instances pat
(lambda-body (ffn-symb term))
(find-all-instances-list pat (fargs term) alists)))
(t (find-all-instances-list pat (fargs term) alists))))))

(defun find-all-instances-list (pat list-of-terms alists)
(declare (xargs :mode :program))
(cond
((null list-of-terms) alists)
(t (find-all-instances pat
(car list-of-terms)
(find-all-instances-list pat
(cdr list-of-terms)
alists))))))
```

We now turn our attention to converting a list of substitutions into a list of lemma instances, each of the form

```(:INSTANCE name (var1 term1) ... (vark termk))
```
as written in `:use` hints. In the code shown above, substitutions are lists of pairs of the form `(var . term)`, but in lemma instances we must write ``doublets.'' So here we show how to convert from one to the other:
```(defun pairs-to-doublets (alist)
(declare (xargs :mode :program))
(cond ((null alist) nil)
(t (cons (list (caar alist) (cdar alist))
(pairs-to-doublets (cdr alist))))))
```

Now we can make a list of lemma instances:

```(defun make-lemma-instances (name alists)
(declare (xargs :mode :program))
(cond
((null alists) nil)
(t (cons (list* :instance name (pairs-to-doublets (car alists)))
(make-lemma-instances name (cdr alists))))))
```

Finally, we can package it all together into a hint function. The function takes a pattern, `pat`, which must be a translated term, the name of a lemma, `name`, and a clause. If some instances of `pat` occur in `clause`, then the corresponding instances of `name` are `:USE`d in the computed hint. Otherwise, the hint does not apply.

```(defun add-corresponding-instances (pat name clause)
(declare (xargs :mode :program))
(let ((alists (find-all-instances-list pat clause nil)))
(cond
((null alists) nil)
(t (list :use (make-lemma-instances name alists))))))
```
The design of this particular hint function makes it important that the variables of the pattern be the variables of the named lemma and that all of the variables we wish to instantiate occur in the pattern. We could, of course, redesign it to allow ``free variables'' or some sort of renaming.

We could now use this hint as shown below:

```(defthm ... ...
'(SWAP x)
'ALL-SWAPS-HAVE-THE-PROPERTY
clause)))
```
The effect of the hint above is that any time a clause arises in which any instance of `(SWAP x)` appears, we add the corresponding instance of `ALL-SWAPS-HAVE-THE-PROPERTY`. So for example, if Subgoal *1/3.5 contains the subterm `(SWAP (SWAP A))` then this hint fires and makes the system behave as though the hint:
```("Subgoal *1/3.5"
:USE ((:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X A))
(:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X (SWAP A)))))
```

## USING-COMPUTED-HINTS-5

Debugging Computed Hints
```Major Section:  MISCELLANEOUS
```

We have found that it is sometimes helpful to define hints so that they print out messages to the terminal when they fire, so you can see what hint was generated and which of your computed hints did it.

To that end we have defined a macro we sometimes use. Suppose you have a `:hints` specification such as:

```:hints (computed-hint-fn (hint-expr id))
```
If you defmacro the macro below you could then write instead:
```:hints ((show-hint computed-hint-fn 1)
(show-hint (hint-expr id) 2))
```
with the effect that whenever either hint is fired (i.e., returns non-`nil`), a message identifying the hint by the marker (1 or 2, above) and the non-`nil` value is printed.

```(defmacro show-hint (hint &optional marker)
(cond
((and (consp hint)
(stringp (car hint)))
hint)
(t
`(let ((marker ,marker)
(ans ,(if (symbolp hint)
`(,hint id clause world)
hint)))
(if ans
(prog2\$
(cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%"
(if (null marker) 0 1)
marker
(cons (string-for-tilde-@-clause-id-phrase id)
ans))
ans)
nil)))))
```
Putting a `show-hint` around a common hint has no effect. If you find yourself using this utility let us know and we'll consider putting it into the system itself. But it does illustrate that you can use computed hints to do unusual things.

## USING-COMPUTED-HINTS-6

```Major Section:  MISCELLANEOUS
```

None of the examples show the use of the variable `WORLD`, which is allowed in computed hints. There are some (undocumented) ACL2 utilities that might be useful in programming hints, but these utilities need access to the ACL2 logical world (see world).

Using these utilities to look at the `WORLD` one can, for example, determine whether a symbol is defined recursively or not, get the body and formals of a defined function, or fetch the statement of a given lemma. Because these utilities are not yet documented, we do not expect users to employ `WORLD` in computed hints. But experts might and it might lead to the formulation of a more convenient language for computed hints.

If you start using computed hints extensively, please contact the developers of ACL2 and let us know what you are doing with them and how we can help.

## VERSION

ACL2 Version Number
```Major Section:  MISCELLANEOUS
```

To determine the version number of your copy of ACL2, evaluate the ACL2 constant `*acl2-version*`. The value will be a string. For example,

```ACL2 !>*acl2-version*
"ACL2 Version 1.9"
```

Books are considered certified only in the same version of ACL2 in which the certification was done. The certificate file records the version number of the certifying ACL2 and include-book considers the book uncertified if that does not match the current version number. Thus, each time we release a new version of ACL2, previously certified books must be recertified.

One reason for this is immediately obvious from the fact that the version number is a logical constant in the ACL2 theory: changing the version number changes the axioms! For example, in version 1.8 you can prove

```(defthm version-8
(equal *acl2-version* "ACL2 Version 1.8"))
```
while in version 1.9 you can prove
```(defthm version-9
(equal *acl2-version* "ACL2 Version 1.9"))
```
Thus, if a book containing the former were included into version 1.9, one could prove a contradiction.

We could eliminate this particular threat of unsoundness by not making the version number part of the axioms. But there are over 150 constants in the system, most having to do with the fact that ACL2 is coded in ACL2, and ``version number inconsistency'' is just the tip of the iceberg. Other likely-to-change constants include `*common-lisp-specials-and-constants*`, which may change when we port ACL2 to some new implementation of Common Lisp, and `*acl2-exports*`, which lists commonly used ACL2 command names users are likely to import into new packages. Furthermore, it is possible that from one version of the system to another we might change, say, the default values on some system function or otherwise make ``intentional'' changes to the axioms. It is even possible one version of the system is discovered to be unsound and we release a new version to correct our error.

Therefore we adopted the draconian policy that books are certified by a given version of ACL2 and must be recertified to be used in other versions. While there are less draconian solutions to the problems illustrated above, we thought this was the simplest.

## WHY-BRR

an explanation of why ACL2 has an explicit `brr` mode
```Major Section:  MISCELLANEOUS
```

Why isn't `brr` mode automatically disabled when there are no monitored runes? The reason is that the list of monitored runes is kept in a wormhole state.

See wormhole for more information on wormholes in general. But the fundamental property of the wormhole function is that it is a logical `no-op`, a constant function that does not take state as an argument. When entering a wormhole, arbitrary information can be passed in (including the external state). That information is used to construct a near copy of the external state and that ``wormhole state'' is the one with respect to which interactions occur during breaks. But no information is carried by ACL2 out of a wormhole -- if that were allowed wormholes would not be logical no-ops. The only information carried out of a wormhole is in the user's head.

`Break-rewrite` interacts with the user in a wormhole state because the signature of the ACL2 rewrite function does not permit it to modify `state`. Hence, only wormhole interaction is possible. (This has the additional desirable property that the correctness of the rewriter does not depend on what the user does during interactive breaks within it; indeed, it is logically impossible for the user to affect the course of `rewrite`.)

Now consider the list of monitored runes. Is that kept in the external state as a normal state global or is it kept in the wormhole state? If it is in the external state then it can be inspected within the wormhole but not changed. This is unacceptable; it is common to change the monitored rules as the proof attempt progresses, installing monitors when certain rules are about to be used in certain contexts. Thus, the list of monitored runes must be kept as a wormhole variable. Hence, its value cannot be determined outside the wormhole, where the proof attempt is ongoing.

This raises another question: If the list of monitored runes is unknown to the rewriter operating on the external state, how does the rewriter know when to break? The answer is simple: it breaks every time, for every rune, if `brr` mode is enabled. The wormhole is entered (silently), computations are done within the wormhole state to determine if the user wants to see the break, and if so, interactions begin. For unmonitored runes and runes with false break conditions, the silent wormhole entry is followed by a silent wormhole exit and the user perceives no break.

Thus, the penalty for running with `brr` mode enabled when there are no monitored runes is high: a wormhole is entered on every application of every rune and the user is simply unware of it. The user who has finally unmonitored all runes is therefore strongly advised to carry this information out of the wormhole and to do `:``brr` `nil` in the external state when the next opportunity arises.

## WORLD

ACL2 property lists and the ACL2 logical data base
```Major Section:  MISCELLANEOUS
```

A ``world'' is a list of triples, each of the form `(sym prop . val)`, implementing the ACL2 notion of property lists. ACL2 permits the simultaneous existence of many property list worlds. ``The world'' is often used as a shorthand for ``the ACL2 logical world'' which is the particular property list world used within the ACL2 system to maintain the data base of rules.

Common Lisp provides the notion of ``property lists'' by which one can attach ``properties'' and their corresponding ``values'' to symbols. For example, one can arrange for the `'color` property of the symbol `'box-14` to be `'purple` and the `'color` property of the symbol `'triangle-7` to be `'yellow`. Access to property lists is given via the Common Lisp function `get`. Thus, `(get 'box-14 'color)` might return `'purple`. Property lists can be changed via the special form `setf`. Thus, `(setf (get 'box-14 'color) 'blue)` changes the Common Lisp property list configuration so that `(get 'box-14 'color)` returns `'blue`. It should be obvious that ACL2 cannot provide this facility, because Common Lisp's `get` ``function'' is not a function of its argument, but instead a function of some implicit state object representing the property list settings for all symbols.

ACL2 provides the functions `getprop` and `putprop` which allow one to mimic the Common Lisp property list facility. However, ACL2's `getprop` takes as one of its arguments a list that is a direct encoding of what was above called the ``state object representing the property list settings for all symbols.'' Because ACL2 already has a notion of ``state'' that is quite distinct from that used here, we call this property list object a ``world.'' A world is just a true list of triples. Each triple is of the form `(sym prop . val)`. This world can be thought of as a slightly elaborated form of association list and `getprop` is a slightly elaborated form of `assoc` that takes two keys. When `getprop` is called on a symbol, `s`, property `p`, and world, `w`, it scans `w` for the first triple whose `sym` is `s` and `prop` is `p` and returns the corresponding `val`. `Getprop` has two additional arguments, one of which that controls what it returns if no such `sym` and `prop` exist in `w`, and other other of which allows an extremely efficient implementation. To set some property's value for some symbol, ACL2 provides `putprop`. `(putprop sym prop val w)` merely returns a new world, `w'`, in which `(sym prop . val)` has been `cons`ed onto the front of `w`, thus ``overwriting'' the `prop` value of `sym` in `w` to `val` and leaving all other properties in `w` unchanged.

One aspect of ACL2's property list arrangment is that it is possible to have many different property list worlds. For example, `'box-14` can have `'color` `'purple` in one world and can have `'color` `'yes` in another, and these two worlds can exist simultaneously because `getprop` is explicitly provided the world from which the property value is to be extracted.

The efficiency alluded to above stems from the fact that Common Lisp provides property lists. Using Common Lisp's provisions behind the scenes, ACL2 can ``install'' the properties of a given world into the Common Lisp property list state so as to make retrieval via `getprop` very fast in the special case that the world provided to `getprop` has been installed. To permit multiple installed worlds, each of which is permitted to be changed via `putprop`, ACL2 requires that worlds be named and these names are used to distinquish installed versions of the various worlds. At the moment we do not further document `getprop` and `putprop`.

However, the ACL2 system uses a property list world, named `'current-acl2-world`, in which to store the succession of user commands and their effects on the logic. This world is often referred to in our documentation as ``the world'' though it should be stressed that the user is permitted to have worlds and ACL2's is in no way distinguished except that the user is not permitted to modify it except via event commands. The ACL2 world is part of the ACL2 state and may be obtained via `(w state)`.

Warning: The ACL2 world is very large. Its length as of this writing (Version 1.5) is over `31,000` and it grows with each release. Furthermore, some of the values stored in it are pointers to old versions of itself. Printing `(w state)` is something you should avoid because you likely will not have the patience to await its completion. For these practical reasons, the only thing you should do with `(w state)` is provide it to `getprop`, as in the form

```  (getprop sym prop default 'current-acl2-world (w state))
```
to inspect properties within it, or to pass it to ACL2 primitives, such as theory functions, where it is expected.

Some ACL2 command forms, such as theory expressions (see theories) and the values to be stored in tables (see table), are permitted to use the variable symbol `world` freely with the understanding that when these forms are evaluated that variable is bound to `(w state)`. Theoretically, this gives those forms complete knowledge of the current logical configuration of ACL2. However, at the moment, few world scanning functions have been documented for the ACL2 user. Instead, supposedly convenient macro forms have been created and documented. For example, `(current-theory :here)`, which is the theory expression which returns the currently enabled theory, actually macroexpands to `(current-theory-fn :here world)`. When evaluated with `world` bound to `(w state)`, `current-theory-fn` scans the current ACL2 world and computes the set of runes currently enabled in it.

## WORMHOLE

`ld` without `state` -- a short-cut to a parallel universe
```Major Section:  MISCELLANEOUS
```

```Example Form:
(wormhole t 'interactive-break nil '(value 'hi!))
; Enters a recursive read-eval-print loop
; on a copy of the ``current `state`'' and
; returns nil!

General Form:
(wormhole pseudo-flg name input form
:current-package    ...  ; known package name
:ld-skip-proofsp    ...  ; t, nil or 'include-book
:ld-redefinition-action  ; nil or '(:a . :b)
:ld-prompt          ...  ; nil, t, or some prompt printer fn
:ld-keyword-aliases ...  ; an alist pairing keywords to parse info
:ld-pre-eval-filter ...  ; :all, :query, or some new name
:ld-pre-eval-print  ...  ; nil, t, or :never
:ld-post-eval-print ...  ; nil, t, or :command-conventions
:ld-evisc-tuple     ...  ; nil or '(alist nil nil level length)
:ld-error-triples   ...  ; nil or t
:ld-error-action    ...  ; :continue, :return, or :error
:ld-query-control-alist  ; alist supplying default responses
:ld-verbose         ...) ; nil or t
```
The keyword arguments above are exactly those of `ld` (see ld) except that three of `ld`'s keyword arguments are missing: the three that specify the channels `standard-oi`, `standard-co` and `proofs-co`. Essentially `wormhole` is just a call of `ld` on the current `state` with the given keyword arguments. `Wormhole` always returns `nil`. The amazing thing about `wormhole` is that it calls `ld` and interacts with the user even though `state` is not available as an argument!

`Wormhole` does this by manufacturing a ``wormhole state,'' a copy of the ``current state'' (whatever that is) modified so as to contain some of the wormhole arguments. `Ld` is called on that wormhole state with the three `ld` channels directed to ACL2's ``comment window.'' At the moment, the comment window is overlaid on the terminal and you cannot tell when output is going to `*standard-co*` and when it is going to the comment window. But we imagine that eventually a different window will pop up on your screen. In any case, the interaction provided by this call of `ld` does not modify the `state` ``from which'' wormhole was called, it modifies the copied `state`. When `ld` exits (e.g., in response to `:``q` being typed in the comment window) the wormhole state evaporates and `wormhole` returns `nil`. Logically and actually (from the perspective of the ongoing computation) nothing has happened except that a ``no-op'' function was called and returned `nil`.

The name `wormhole` is meant to suggest the idea that the function provides easy access to `state` in situations where it is apparently impossible to get `state`. Thus, for example, if you define the `factorial` function, say, except that you sprinkled into its body appropriate calls of `wormhole`, then the execution of `(factorial 6)` would cause interactive breaks in the comment window. During those breaks you would apparently be able to inspect the ``current state'' even though `factorial` does not take `state` as an argument. The whole notion of there being a ``current state'' during the evaluation of `(factorial 6)` is logically ill-defined. And yet, we know from practical experience with the sequential computing machines upon which ACL2 is implemented that there is a ``current state'' (to which the `factorial` function is entirely insensitive) and that is the state to which `wormhole` ``tunnels.'' A call of `wormhole` from within `factorial` can pass `factorial`-specific information that is embedded in the wormhole state and made available for inspection by the user in an interactive setting. But no information ever flows out of a wormhole state: `wormhole` always returns `nil`.

There are four arguments to `wormhole` that need further explanation: `pseudo-flg`, `name`, `input`, and `form`. Roughly speaking, the value of `pseudo-flg` should be `t` or `nil` and indicates whether we are actually to enter a wormhole or just return `nil` immediately. The actual handling of `pseudo-flg` is more sophisticated and is explained in detail at the end of this documentation.

`Name` and `input` are used as follows. Recall that `wormhole` copies the ``current state'' and then modifies it slightly to obtain the `state` upon which `ld` is called. We now describe the modifications. First, the `state` global variable `'wormhole-name` is set to `name`, which may be any non-`nil` ACL2 object but is usually a symbol. Then, `'wormhole-input` is set to `input`, which may be any ACL2 object. Finally, and inexplicably, `'wormhole-output` is set to the value of `'wormhole-output` the last time a wormhole named `name` was exited (or `nil` if this is the first time a wormhole named `name` was entered). `this` last aspect of wormholes, namely the preservation of `'wormhole-output`, allows all the wormholes of a given name to communicate with each other.

We can now explain how `form` is used. The modified `state` described above is the `state` on which `ld` is called. However, `standard-oi` -- the input channel from which `ld` reads commands -- is set so that the first command that `ld` reads and evaluates is `form`. If `form` returns an error triple with value `:``q`, i.e., `form` returns via `(value :q)`, then no further commands are read, `ld` exits, and the wormhole exits and returns `nil`. But if `form` returns any other value (or is not an error triple), then subsequent commands are read from the comment window.

As usual, the `ld`-specials affect whether a herald is printed upon entry, whether `form` is printed before evaluation, whether a prompt is printed, how errors are handled, etc. The `ld`-specials can be specified with the corresponding arguments to `wormhole`. It is standard practice to call `wormhole` so that the entry to `ld` and the evaluation of `form` are totally silent. Then, tests in `form` can inspect the `state` and decide whether user interaction is desired. If so, `form` can appropriately set `ld-prompt`, `ld-error-action`, etc., print a herald, and then return `(value :invisible)`. Recall (see ld) that `(value :invisible)` causes `ld` not to print a value for the just executed form. The result of this arrangement is that whether interaction occurs can be based on tests that are performed on the wormhole state after `(@ wormhole-input)` and the last `(@ wormhole-output)` are available for inspection. This is important because outside the wormhole you can access `wormhole-input` (you are passing it into the wormhole) but you may not be able to access the current `state` (because you might be in `factorial`) and you definitely cannot access the `wormhole-output` of the last wormhole because it is not part of the ACL2 `state`. Thus, if the condition under which you wish to interact depends upon the `state` or that part of it preserved from the last wormhole interaction, that condition can only be tested from within the wormhole, via `form`.

It is via this mechanism that `break-rewrite` (see break-rewrite) is implemented. To be more precise, the list of monitored runes is maintained as part of the preserved `wormhole-output` of the `break-rewrite` wormhole. Because it is not part of the normal `state`, it may be changed by the user during proofs. That is what allows you to install new monitors while debugging proofs. But that means that the list of monitored runes cannot be inspected from outside the wormhole. Therefore, to decide whether a break is to occur when a given rule is applied, the rewriter must enter the `break-rewrite` wormhole, supplying a form that causes interaction if the given rule's break condition is satisfied. The user perceives this as though the wormhole was conditionally entered -- a perception that is happily at odds with the informed user's knowledge that the list of monitored runes is not part of the `state`. In fact, the wormhole was unconditionally entered and the condition was checked from within the wormhole, that being the only state in which the condition is known.

Another illustrative example is available in the implemention of the `monitor` command. How can we add a new rune to the list of monitored runes while in the normal ACL2 `state` (i.e., while not in a wormhole)? The answer is: by getting into a wormhole. In particular, when you type `(monitor rune expr)` at the top-level of ACL2, `monitor` enters the `break-rewrite` wormhole with a cleverly designed first `form`. That form adds rune and `expr` to the list of monitored runes -- said list only being available in `break-rewrite` wormhole states. Then the first form returns `(value :q)`, which causes us to exit the wormhole. By using `ld`-specials that completely suppress all output during the process, it does not appear to the user that a wormhole was entered. The moral here is rather subtle: the first form supplied to `wormhole` may be the entire computation you want to perform in the wormhole; it need not just be a predicate that decides if interaction is to occur. Using wormholes of different names you can maintain a variety of ``hidden'' data structures that are always accessible (whether passed in or not). This appears to violate completely the applicative semantics of ACL2, but it does not: because these data structures are only accessible via `wormhole`s, it is impossible for them to affect any ACL2 computation (except in the comment window).

As one might imagine, there is some overhead associated with entering a wormhole because of the need to copy the current `state`. This brings us back to `pseudo-flg`. Ostensibly, `wormhole` is a function and hence all of its argument expressions are evaluated outside the function (and hence, outside the wormhole it creates) and then their values are passed into the function where an appropriate wormhole is created. In fact, `wormhole` is a macro that permits the `pseudo-flg` expression to peer dimly into the wormhole that will be created before it is created. In particular, `pseudo-flg` allows the user to access the `wormhole-output` that will be used to create the wormhole state.

This is done by allowing the user to mention the (apparently unbound) variable `wormhole-output` in the first argument to `wormhole`. Logically, `wormhole` is a macro that wraps

```(let ((wormhole-output nil)) ...)
```
around the expression supplied as its first argument. So logically, `wormhole-output` is always `nil` when the expression is evaluated. However, actually, `wormhole-output` is bound to the value of `(@ wormhole-output)` on the last exit from a wormhole of the given name (or `nil` if this is the first entrance). Thus, the `pseudo-flg` expression, while having to handle the possibility that `wormhole-output` is `nil`, will sometimes see non-`nil` values. The next question is, of course, ``But how can you get away with saying that logically `wormhole-output` is always `nil` but actually it is not? That doesn't appear to be sound.'' But it is sound because whether `pseudo-flg` evaluates to `nil` or non-`nil` doesn't matter, since in either case `wormhole` returns `nil`. To make that point slightly more formal, imagine that `wormhole` did not take `pseudo-flg` as an argument. Then it could be implemented by writing
```(if pseudo-flg (wormhole name input form ...) nil).
```
Now since wormhole always returns `nil`, this expression is equivalent to `(if pseudo-flg nil nil)` and we see that the value of `pseudo-flg` is irrelevant. So we could in fact allow the user to access arbitrary information to decide which branch of this if to take. We allow access to `wormhole-output` because it is often all that is needed. We don't allow access to `state` (unless `state` is available at the level of the wormhole call) for technical reasons having to do with the difficulty of overcoming `translate`'s prohibition of the sudden appearance of the variable `state`.

We conclude with an example of the use of `pseudo-flg`. This example is a simplification of our implementation of `break-rewrite`. To enter `break-rewrite` at the beginning of the attempted application of a rule, `rule`, we use

```(wormhole
(and (f-get-global 'brr-mode state)
(member-equal (access rewrite-rule rule :rune)
(cdr (assoc-eq 'monitored-runes wormhole-output))))
'break-rewrite
...)
```
The function in which this call of `wormhole` occurs has `state` as a formal. The `pseudo-flg` expression can therefore refer to `state` to determine whether `'brr-mode` is set. But the `pseudo-flg` expression above mentions the variable `wormhole-output`; this variable is not bound in the context of the call of `wormhole`; if `wormhole` were a simple function symbol, this expression would be illegal because it mentions a free variable.

However, it is useful to think of `wormhole` as a simple function that evaluates all of its arguments but to also imagine that somehow `wormhole-output` is magically bound around the first argument so that `wormhole-output` is the output of the last `break-rewrite` wormhole. If we so imagine, then the `pseudo-flg` expression above evaluates either to `nil` or non-`nil` and we will enter the wormhole named `break-rewrite` in the latter case.

Now what does the `pseudo-flg` expression above actually test? We know the format of our own `wormhole-output` because we are responsible for maintaining it. In particular, we know that the list of monitored runes can be obtained via

```(cdr (assoc-eq 'monitored-runes wormhole-output)).
```
Using that knowledge we can design a `pseudo-flg` expression which tests whether (a) we are in `brr-mode` and (b) the rune of the current rule is a member of the monitored runes. Question (a) is answered by looking into the current `state`. Question (b) is answered by looking into that part of the about-to-be-created wormhole state that will differ from the current `state`. To reiterate the reason we can make `wormhole-output` available here even though it is not in the current `state`: logically speaking the value of `wormhole-output` is irrelevant because it is only used to choose between two identical alternatives. This example also makes it clear that `pseudo-flg` provides no additional functionality. The test made in the `pseudo-flg` expression could be moved into the first form evaluated by the wormhole -- changing the free variable `wormhole-output` to `(@ wormhole-output)` and arranging for the first form to return `(value :q)` when the `pseudo-flg` expression returns `nil`. The only reason we provide the `pseudo-flg` feature is because it allows the test to be carried out without the overhead of entering the wormhole.

Wormholes can be used not only in :program mode definitions but also in :logic mode definitions. Thus, it is possible (though somewhat cumbersome without investing in macro support) to annotate logical functions with output facilities that do not require STATE. These facilities do not complicate proof obligations. Suppose then that one doctored a simple function, e.g., APP, so as to do some printing and then proved that APP is associative. The proof may generate extraneous output due to the doctoring. Furthermore, contrary to the theorem proved, execution of the function appears to affect *standard-co*. To see what the function ``really'' does when evaluated, enter raw lisp and set the global variable *inhibit-wormhole-activityp* to t.