LEMMA in the ttrees, then the set for
ttree' is the extension of that for ttree obtained by unioning into
it all the runes used by the rewrite. The set associated with
LEMMA can be obtained by (tagged-objects 'LEMMA ttree nil).
Major Section: MISCELLANEOUS
Many low-level ACL2 functions take and return ``tag trees'' or ``ttrees'' (pronounced ``tee-trees'') which contain various useful bits of information such as the lemmas used, the linearize assumptions made, etc.
Let a ``tagged pair'' be a list whose car is a symbol, called the ``tag,'' and whose cdr is an arbitrary object, called the ``tagged object.'' A ``tag tree'' is either nil, a tagged pair consed onto a tag tree, or a non-nil tag tree consed onto a tag tree.
Abstractly a tag tree represents a list of sets, each member set
having a name given by one of the tags occurring in the ttree. The
elements of the set named tag are all of the objects tagged
tag in the tree. To cons a tagged pair (tag . obj) onto a
tree is to add-to-set-equal obj to the set corresponding to
tag. To cons two tag trees together is to union-equal the
corresponding sets. The concrete representation of the union so
produced has duplicates in it, but we feel free to ignore or delete
duplicates.
The beauty of this definition is that to combine two non-nil tag
trees you need do only one cons.
The following function accumulates onto ans the set associated with a given tag in a ttree:
(defun tagged-objects (tag ttree ans)
(cond
((null ttree) ans)
((symbolp (caar ttree)) ; ttree = ((tag . obj) . ttree)
(tagged-objects tag (cdr ttree)
(cond ((eq (caar ttree) tag)
(add-to-set-equal (cdar ttree) ans))
(t ans))))
(t ; ttree = (ttree . ttree)
(tagged-objects tag (cdr ttree)
(tagged-objects tag (car ttree) ans)))))
This function is defined as a :PROGRAM mode function in ACL2.
The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.
Term' is equivalent to term (under the current assumptions) and the
ttree' is an extension of ttree. If we focus just on the set
associated with the tag LEMMA in the ttrees, then the set for
ttree' is the extension of that for ttree obtained by unioning into
it all the runes used by the rewrite. The set associated with
LEMMA can be obtained by (tagged-objects 'LEMMA ttree nil).
Major Section: MISCELLANEOUS
To help you experiment with type-sets we briefly note the following utility functions.
(type-set-quote x) will return the type-set of the object x. For
example, (type-set-quote "test") is 2048 and
(type-set-quote '(a b c)) is 512.
(type-set 'term nil nil nil nil (ens state) (w state) nil) will
return the type-set of term. For example,
(type-set '(integerp x) nil nil nil nil (ens state) (w state) nil)will return (mv 192 nil). 192, otherwise known as
*ts-boolean*,
is the type-set containing t and nil. The second result may
be ignored in these experiments. Term must be in the
translated, internal form shown by :trans. See trans
and see term.
(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil)
will return the type-set deduced for the variable symbol x assuming
the translated term, term, true. The second result may be ignored
in these experiments. For example,
(type-set-implied-by-term 'v nil '(integerp v)
(ens state) (w state) nil)
returns 11.
(convert-type-set-to-term 'x ts (ens state) (w state) nil) will
return a term whose truth is equivalent to the assertion that the
term x has type-set ts. The second result may be ignored in these
experiments. For example
(convert-type-set-to-term 'v 523 (ens state) (w state) nil)returns a term expressing the claim that
v is either an integer
or a non-nil true-list. 523 is the logical-or of 11 (which
denotes the integers) with 512 (which denotes the non-nil
true-lists).
The ``actual primitive types'' of ACL2 are listed in
*actual-primitive-types*. These primitive types include such types
as *ts-zero*, *ts-positive-integer*, *ts-nil* and *ts-proper-consp*.
Each actual primitive type denotes a set -- sometimes finite and
sometimes not -- of ACL2 objects and these sets are pairwise
disjoint. For example, *ts-zero* denotes the set containing 0 while
*ts-positive-integer* denotes the set containing all of the positive
integers.
The actual primitive types were chosen by us to make theorem proving
convenient. Thus, for example, the actual primitive type *ts-nil*
contains just nil so that we can encode the hypothesis ``x is nil''
by saying ``x has type *ts-nil*'' and the hypothesis ``x is
non-nil'' by saying ``x has type complement of *ts-nil*.'' We
similarly devote a primitive type to t, *ts-t*, and to a third type,
*ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.
Let *ts-other* denote the set of all Common Lisp objects other than
those in the actual primitive types. Thus, *ts-other* includes such
things as floating point numbers and CLTL array objects. The actual
primitive types together with *ts-other* constitute what we call
*universe*. Note that *universe* is a finite set containing one
more object than there are actual primitive types; that is, here we
are using *universe* to mean the finite set of primitive types, not
the infinite set of all objects in all of those primitive types.
*Universe* is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in *universe*.
Abstractly, a ``type-set'' is a subset of *universe*. To say that a
term, x, ``has type-set ts'' means that under all possible
assignments to the variables in x, the value of x is a member of
some member of ts. Thus, (cons x y) has type-set
{*ts-proper-cons* *ts-improper-cons*}. A term can have more than
one type-set. For example, (cons x y) also has the type-set
{*ts-proper-cons* *ts-improper-cons* *ts-nil*}. Extraneous types
can be added to a type-set without invalidating the claim that a
term ``has'' that type-set. Generally we are interested in the
smallest type-set a term has, but because the entire theorem-proving
problem for ACL2 can be encoded as a type-set question, namely,
``Does p have type-set complement of *ts-nil*?,'' finding the
smallest type-set for a term is an undecidable problem. When we
speak informally of ``the'' type-set we generally mean ``the
type-set found by our heuristics'' or ``the type-set assumed in the
current context.''
Note that if a type-set, ts, does not contain *ts-other* as an
element then it is just a subset of the actual primitive types. If
it does contain *ts-other* it can be obtained by subtracting from
*universe* the complement of ts. Thus, every type-set can be
written as a (possibly complemented) subset of the actual primitive
types.
By assigning a unique bit position to each actual primitive type we
can encode every subset, s, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if s contains the
ith actual primitive type. The type-sets written as the complement
of s are encoded as the twos-complement of the encoding of s. Those
type-sets are thus negative integers. The bit positions assigned to
the actual primitive types are enumerated from 0 in the same order
as the types are listed in *actual-primitive-types*. At the
concrete level, a type-set is an integer between *min-type-set* and
*max-type-set*, inclusive.
For example, *ts-nil* has bit position 6. The type-set containing
just *ts-nil* is thus represented by 64. If a term has type-set 64
then the term is always equal to nil. The type-set containing
everything but *ts-nil* is the twos-complement of 64, which is -65.
If a term has type-set -65, it is never equal to nil. By ``always''
and ``never'' we mean under all, or under no, assignments to the
variables, respectively.
Here is a more complicated example. Let s be the type-set
containing all of the symbols and the natural numbers. The relevant
actual primitive types, their bit positions and their encodings are:
actual primitive type bit valueThus, the type-set*ts-zero* 0 1 *ts-positive-integer* 1 2 *ts-nil* 6 64 *ts-t* 7 128 *ts-non-t-non-nil-symbol* 8 256
s is represented by (+ 1 2 64 128 256) = 451.
The complement of s, i.e., the set of all objects other than the
natural numbers and the symbols, is -452.
Major Section: MISCELLANEOUS
Computed hints are extraordinarily powerful. We show a few examples here to illustrate their use. We recommend that these be read in the following sequence:
Major Section: MISCELLANEOUS
The common hint
("Subgoal 3.2.1''" :use lemma42)
has the same effect as the computed hint
(if (equal id '((0) (3 2 1) . 2))
'(:use lemma42)
nil)
which, of course, is equivalent to
(and (equal id '((0) (3 2 1) . 2))
'(:use lemma42))
which is also equivalent to the computed hint
my-special-hintprovided the following
defun has first been executed
(defun my-special-hint (id clause world)
(declare (xargs :mode :program)
(ignore clause world))
(if (equal id '((0) (3 2 1) . 2))
'(:use lemma42)
nil))
It is permitted for the defun to be in :LOGIC mode
(see defun-mode) also.
Just to be concrete, the following three events all behave the same
way (if my-special-hint is as above):
(defthm main (big-thm a b c)
:hints (("Subgoal 3.2.1''" :use lemma42)))
(defthm main (big-thm a b c)
:hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))))
(defthm main (big-thm a b c)
:hints (my-special-hint))
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).
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.
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 :USEd 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 ... ...
:hints ((add-corresponding-instances
'(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)))))
had been present.
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.
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.
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.
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.