		Search-engine friendly clone of the ACL2 documentation.

Break-rewrite

Why-brr

An explanation of why ACL2 has an explicit brr mode

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 unaware 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.