DEFTTAG

introduce a trust tag (ttag) 
Major Section:  EVENTS


General Forms:
(defttag tag-name)
(defttag tag-name :doc doc-string)
where tag-name is a symbol. The :doc doc-string argument is optional; if supplied, then it must be a valid documentation string (see doc-string), and the defttag call will generate a corresponding defdoc event. For the rest of this discussion we ignore the :doc argument.

WARNING! This event is intended for advanced users who, in essence, want to build extensions of ACL2. Anyone who uses this event, even by way of including books, is placing trust in the correctness of all forms executed in the scope of that defttag event. (Thus, it may be a good idea if the scope of a defttag event, which is the enclosing book or encapsulate event, is kept small.) The documentation below explains this issue in detail.

This event introduces or removes a so-called active trust tag (or ``ttag'', pronounced ``tee tag''). An active ttag is a non-nil symbol (tag) that is associated with potentially unsafe acts. For example, sys-call can be used in an unsafe way, for example to overwrite files, or worse (see sys-call for a frightening example from Bob Boyer). Therefore, calls of sys-call are illegal unless a defttag event has been executed. If one introduces an active ttag and then writes definitions that calls sys-call, presumably in a defensibly ``safe'' way, then responsibility for those calls is attributed to that ttag. This attribution (or blame!) is at the level of books; a book's certificate contains a list of ttags that are active in that book, or in a book that is included (possibly locally), or in a book included in a book that is included (either inclusion being potentially local), and so on. We explain all this in more detail below.

(Defttag tag-name) is essentially equivalent to 

(table acl2-defaults-table :ttag tag-name)
and hence is local to any books and encapsulate events in which it occurs; see acl2-defaults-table. We say more about the scope of defttag forms below.

Note: This is an event! It does not print the usual event summary but nevertheless executes the above table event and hence changes the ACL2 logical world, and is so recorded. Although no event summary is printed, it is important to note that the ``TTAG NOTE'', discussed below, is always printed for a non-nil tag-name.

Active ttags. Suppose tag-name is a non-nil symbol. Then (defttag tag-name) sets tag-name to be the ``active ttag.'' There must be an active ttag in order for there to be any mention of certain function and macro symbols, including sys-call; evaluate the form (strip-cars *ttag-fns-and-macros*) to see the full list of such symbols. On the other hand, (defttag nil) removes the active ttag, if any; there is then no active ttag. The scope of a defttag form in a book being certified or included is limited to subsequent forms in the same book before the next defttag (if any) in that book. Similarly, if a defttag form is evaluated in the top-level loop, then its effect is limited to subsequent forms in the top-level loop before the next defttag in the top-level loop (if any). Moreoever, certify-book is illegal when a ttag is active; of course, in such a circumstance one can execute (defttag nil) in order to allow book certification.

Ttag notes and the ``certifier.'' When a defttag is executed with an argument other than nil, output is printed, starting on a fresh line with: TTAG NOTE. For example: 

ACL2 !>(defttag foo)


TTAG NOTE: Adding ttag FOO from the top level loop.
 FOO
ACL2 !>
If the defttag occurs in an included book, the message looks like this. 
TTAG NOTE (for included book): Adding ttag FOO from file /u/smith/acl2/my-book.lisp.
The ``TTAG NOTE'' message is always printed on a single line. The intention is that one can search the standard output for all such notes in order to find all defttag events. In a sense, defttag events can allow you to define your own system on top of ACL2 (for example, see progn!). So in order for someone else (who we might call the ``certifier'') to be confident that your collection of books is meaningful, that certifier should certify all the user-supplied books from scratch and check either that no :ttags were supplied to certify-book, or else look for every TTAG NOTE in the standard output in order to locate all defttag events with non-nil tag-name. In this way, the certifier can in principle decide whether to be satisfied that those defttag events did not allow inappropriate forms in the user-supplied books.

Allowed ttags when certifying and including books. A defttag form may not be evaluated unless its argument is a so-called ``allowed'' ttag. All ttags are allowed in the interactive top-level loop. However, during certify-book and include-book, the set of allowed ttags is restricted according to the :ttags keyword argument. If this argument is omitted then no ttag is allowed, so a defttag call will fail during book certification or inclusion in this case. This restriction applies even to defttag forms already evaluated in the so-called certification world at the time certify-book is called. But note that (defttag nil) is always legal.

A :ttags argument of certify-book and include-book can have value :all, indicating that every ttag is allowed, i.e., no restriction is being placed on the arguments, just as in the interactive top-level loop. Otherwise, the value is a true list of ttag specifications, each having one of the following forms, where sym is a non-nil symbol.

(1) sym

(2) (sym)

(3) (sym x1 x2 ... xk), where k > 0 and each xi is a string, except that one xi may be nil.

In Case (1), (defttag sym) is allowed to occur in at most one book or else in the top-level loop (i.e., the certification world for a book under certification or a book being included). Case (2) allows (defttag sym) to occur in an unlimited number of books. For case (3) the xi specify where (defttag sym) may occur, as follows. The case that xi is nil refers to the top-level loop, while all other xi are filenames, where the ".lisp" extension is optional and relative pathnames are considered to be relative to the connected book directory (see cbd).

An error message, as shown below, illustrates how ACL2 enforcess the notion of allowed ttags. Suppose that you call certify-book with argument :ttags (foo), where you have already executed (defttag foo) in the certification world (i.e., before calling certify-book). Then ACL2 immediately associates the ttag foo with nil, where again, nil refers to the top-level loop. If ACL2 then encounters (defttag foo) inside that book, you will get the following error (using the full book name for the book, as shown): 

ACL2 Error in ( TABLE ACL2-DEFAULTS-TABLE ...):  The ttag FOO associated
with file /u/smith/work/my-book.lisp is not among the set of ttags permitted
in the current context, namely:
  ((FOO NIL)).
See :DOC defttag.
In general the structure displayed by the error message, which is ((FOO NIL)) in this case, represents the currently allowed ttags with elements as discussed in (1) through (3) above. In this case, that list's unique element is (FOO NIL), meaning that ttag FOO is only allowed at the top level (as represented by NIL).

Associating ttags with books and with the top-level loop. When a book is certified, each form (defttag tag) that is encountered for non-nil tag in that book or an included book is recorded in the generated certificate, which associates tag with the full-book-name of the book containing that deftag. If such a defttag form is encountered outside a book, hence in the portcullis of the book being certified or one of its included books, then tag is associated with nil in the generated certificate. Note that the notion of ``included book'' here applies to the recursive notion of a book either included directly in the book being certified or else included in such a book, where we account even for locally included books.

For examples of ways to take advantage of ttags, see books/misc/hacker.lisp and see ttags-seen, see progn!, see remove-untouchable, see set-raw-mode, and see sys-call.