DEFTTAG

introduce a trust tag (ttag) 
Major Section:  EVENTS

Introduction. This event is intended for advanced users who, in essence, want to build extensions of ACL2. The typical intended use is to create books that extend the functionality of ACL2 in ways not allowed without a so-called ``active trust tag''. A trust tag thus represents a contract: The writer of such a book is guaranteeing that the book extends ACL2 in a ``correct'' way as defined by the writer of the book. The writer of the book will often have a small section of the book in the scope of an active trust tag that can be inspected by potential users of that book: 

<initial part of book, which does not use trust tags>
(defttag :some-ttag) ; install :some-ttag as an active trust tag
<various code that requires an active trust tag>
(defttag nil)        ; remove active trust tag
<initial part of book, which does not use trust tags>

Why might trust tags be needed? The evaluation of certain functions can introduce bugs and even unsoundness, but can be useful in restricted ways that avoid such issues. 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. The following example shows that the function sys-call is restricted by default, but can be called after installing an active trust tag. 

ACL2 !>(sys-call "pwd" nil)


ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
a trust tag is in effect.  See :DOC defttag.

ACL2 !>(defttag t) ; Install :T as an active trust tag.

TTAG NOTE: Adding ttag :T from the top level loop.
 T
ACL2 !>(sys-call "pwd" nil) ; print the current directory and return NIL
/u/kaufmann
NIL
ACL2 !>(defttag nil) ; Remove the active trust tag (using value NIL).
 NIL
ACL2 !>(sys-call "pwd" nil) ; Now we get the error again:


ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
a trust tag is in effect.  See :DOC defttag.

ACL2 !>

Of course, using sys-call with the Linux command pwd is not likely to cause any soundness problems! So suppose we want to create a function that prints the working directory. We might put the following events into a book that is to be certified. 

(in-package "ACL2")
(defttag :pwd-ttag)
(defun print-working-dir ()
  (declare (xargs :mode :program))
  (sys-call "pwd" nil))
(defttag nil) ; optional (books end with this implicitly)
We can certify this book with a specification that :pwd-ttag is a legal trust tag: 
(certify-book "pwd" 0 t :ttags (:pwd-ttag))
One can now use this book by executing include-book with keyword parameter :ttags (:pwd-ttag) and then calling function print-working-dir: 
(include-book "pwd" :ttags (:pwd-ttag))
(print-working-dir) ; working directory is printed to terminal

Detailed documentation. 

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 tag-name. (For the rest of this discussion we ignore the :doc argument.)

Note however that (other than the :doc argument), if tag-name is not nil then it is converted to a ``corresponding keyword'': a symbol in the "KEYWORD" package with the same symbol-name as tag-name. Thus, for example, (defttag foo) is equivalent to (defttag :foo). Moreover, a non-nil symbol with a symbol-name of "NIL" is illegal for trust tags; thus, for example, (defttag :nil) is illegal.

This event introduces or removes a so-called active trust tag (or ``ttag'', pronounced ``tee tag''). An active ttag is a keyword symbol that is associated with potentially unsafe evaluation. For example, calls of sys-call are illegal unless there is an active trust tag. An active trust tag can be installed using a defttag event. 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 (unless deferred; see set-deferred-ttag-notes).

Active ttags. Suppose tag-name is a non-nil symbol. Then (defttag :tag-name) sets :tag-name to be the (unique) ``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.

In order to eliminate much of the output from TTAG NOTEs, see set-deferred-ttag-notes. Note however that the resulting security is somewhat less; therefore, a TTAG NOTE is printed when invoking set-deferred-ttag-notes to defer printing of ttag notes.

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. In the case of include-book, an omitted :ttags argument or an argument of :default is treated as :all, except that warnings will occur when the book's certificate includes ttags; but for certify-book, an omitted ttags argument is treated as nil. Otherwise, if the :ttags argument is supplied but not :all, then its value is a true list of ttag specifications, each having one of the following forms, where sym is a non-nil symbol which is treated as the corresponding keyword.

(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). Note that the restrictions on (defttag :sym) apply equally to any equivalent for based on the notion of ``corresponding keyword'' discussed above, e.g., (defttag acl2::sym).

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, specified as follows:
  ((: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 the keyword corresponding to 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 that keyword 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 community book books/hacking/hacker.lisp and see ttags-seen, see progn!, see remove-untouchable, see set-raw-mode, and see sys-call.