PUFF

Major Section:  HISTORY

Example Forms:
ACL2 !>:puff :max
ACL2 !>:puff :x
ACL2 !>:puff 15
ACL2 !>:puff "book"

General Form:
:puff cd

A command is ``puffable'' if it is an encapsulate command, an include-book command, or any command other than those consisting of a single primitive event. For example, since defun is a primitive event, a defun command is not puffable. But a macro form that expands into several defun events is puffable. The only primitive event commands that are puffable are encapsulate and include-book commands. A puffable command contains (interesting) subevents, namely, the events in the body of the encapsulate, in the file of the book included, or in the command block.

The puff command ``lifts'' the immediate subevents of the indicated command so that they become commands themselves. The command puff* recursively puffs the newly introduced commands. See puff*, which also gives an example illustrating both puff and puff*. Puff undoes the command at cd and replaces it by its immediate subevents. Thus, in general the length of the history grows when a puff command is executed. If puff causes an error (see below), the logical world remains unchanged from its initial configuration.

The intended use of puff is to allow the user access to the events ``hidden'' inside compound commands. For example, while trying to prove some theorem, p, about a constrained function, fn, one might find that the encapsulate, cd, that introduced fn failed to include an important constraint, q. Without puff, the only way to proceed is to undo back through cd, create a suitable encapsulate that proves and exports q as well as the old constraints, re-execute the new encapsulate, re-execute the events since cd, and then try p again. Unfortunately, it may be hard to prove q and additional events may have to be inserted into the encapsulate to prove it. It may also be hard to formulate the ``right'' q, i.e., one that is provable in the encapsulate and provides the appropriate facts for use in the proof of p.

Using puff, the user can erase the encapsulate at cd, replacing it by the events in its body. Now the formerly constrained function, fn, is defined as its witness. The user can experiment with formulations and proofs of q suitable for p. Of course, to get into the ultimately desired state -- where fn is constrained rather than defined and q is exported by an encapsulate at cd -- the user must ultimately undo back to cd and carry out the more tedious program described above. But by using puff it is easier to experiment.

Similar applications of puff allow the user of a book to expose the innards of the book as though they had all be typed as commands. The user might then ``partially undo'' the book, keeping only some of the events in it.

Puff operates as follows. First, it determines the list of immediate subevents of the command indicated by cd. It causes an error if there is only one subevent and that subevent is identical to the command -- i.e., if the command at cd is a primitive. Next, puff undoes back through the indicated command. This not only erases the command at cd but all the commands executed after it. Finally, puff re-executes the subevents of (the now erased) cd followed by all the commands that were executed afterwards.

Observe that the commands executed after cd will generally have higher command numbers than they did before the puff. For example, suppose 100 commands have been executed and that :puff 80 is then executed. Suppose command 80 contains 5 immediate subevents (i.e., is an encapsulation of five events). Then, after puffing, command 80 is the first event of the puffed command, command 81 is the second, and so on; 104 commands appear to have been executed.

When puffing an encapsulate or include-book, the local commands are executed. Note that this will replace constrained functions by their witnesses.

Finally, it is impossible to puff in the presence of include-book commands involving certified files that have been altered since they were included. To be specific, suppose "arith" is a certified book that has been included in a session. Suppose that after "arith" was included, the source file is modified. (This might happen if the user of "arith" is not its author and the author happens to be working on a new version of "arith" during the same time period.) Now suppose the user tries to puff the command that included "arith". The attempt to obtain the subevents in "arith" will discover that the check sum of "arith" has changed and an error will be caused. No change is made in the logical world. A similar error is caused if, in this same situation, the user tries to puff any command that occurred before the inclusion of "arith"! That is, puff may cause an error and leave the world unchanged even if the command puffed is not one involving the modified book. This happens because in order to reconstruct the world after the puffed command, puff must obtain the events in the book and if the book's source file has changed there is no assurance that the reconstructed world is the one the user intends.

Warning: We do not detect changes to uncertified books that have been included and are then puffed or re-included! The act of including an uncertified book leaves no trace of the check sum of the book. Furthermore, the act prints a warning message disclaiming soundness. In light of this, :puff quietly ``re-''executes the current contents of the book.