DEFTTAG
introduce a trust tag (ttag)Major Section: EVENTSIntroduction. This event is intended for advanced users who, inessence, want to build extensions of ACL2. The typical intended use is tocreate books that extend the functionality of ACL2 in ways not allowedwithout a so-called ``active trust tag''. A trust tag thus represents acontract: The writer of such a book is guaranteeing that the book extendsACL2 in a ``correct'' way as defined by the writer of the book. The writerof the book will often have a small section of the book in the scope of anactive 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 canintroduce bugs and even unsoundness, but can be useful in restricted waysthat avoid such issues. For example, sys-call can be used in an unsafeway, for example to overwrite files, or worse; see sys-call for afrightening example from Bob Boyer. The following example shows that thefunction sys-call is restricted by default, but can be called afterinstalling an active trust tag.
ACL2 !>(sys-call "pwd" nil)ACL2 Error in TOP-LEVEL: The SYS-CALL function cannot be called unlessa 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. TACL2 !>(sys-call "pwd" nil) ; print the current directory and return NIL/u/kaufmannNILACL2 !>(defttag nil) ; Remove the active trust tag (using value NIL). NILACL2 !>(sys-call "pwd" nil) ; Now we get the error again:ACL2 Error in TOP-LEVEL: The SYS-CALL function cannot be called unlessa trust tag is in effect. See :DOC defttag.ACL2 !>
Of course, using sys-call with the Linux command pwd is not likelyto cause any soundness problems! So suppose we want to create a functionthat prints the working directory. We might put the following eventsinto 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 legaltrust tag:(certify-book "pwd" 0 t :ttags (:pwd-ttag))One can now use this book by executing
include-book with keywordparameter :ttags (:pwd-ttag) and then calling functionprint-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 isoptional; if supplied, then it must be a valid documentation string(see doc-string), and the defttag call will generate a correspondingdefdoc event for tag-name. (For the rest of this discussion weignore the :doc argument.)Note however that (other than the :doc argument), if tag-name is notnil then it is converted to a ``corresponding keyword'': a symbol inthe "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" isillegal 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 isassociated with potentially unsafe evaluation. For example, calls ofsys-call are illegal unless there is an active trust tag. An activetrust tag can be installed using a defttag event. If one introduces anactive ttag and then writes definitions that calls sys-call, presumablyin a defensibly ``safe'' way, then responsibility for those calls isattributed to that ttag. This attribution (or blame!) is at the level ofbooks; a book's certificate contains a list of ttags that areactive 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 beingpotentially local), and so on. We explain all this in more detailbelow.
(Defttag :tag-name) is essentially equivalent to
(table acl2-defaults-table :ttag :tag-name)and hence is
local to any books and encapsulate eventsin which it occurs; see acl2-defaults-table. We say more about the scope ofdefttag forms below.Note: This is an event! It does not print the usual event summary butnevertheless executes the above table event and hence changes the ACL2logical world, and is so recorded. Although no event summary isprinted, it is important to note that the ``TTAG NOTE'', discussed below, isalways 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) ``activettag.'' There must be an active ttag in order for there to be any mention ofcertain function and macro symbols, including sys-call; evaluate theform (strip-cars *ttag-fns-and-macros*) to see the full list of suchsymbols. On the other hand, (defttag nil) removes the active ttag, ifany; there is then no active ttag. The scope of a defttag form in a bookbeing certified or included is limited to subsequent forms in the same bookbefore the next defttag (if any) in that book. Similarly, if adefttag form is evaluated in the top-level loop, then its effect islimited to subsequent forms in the top-level loop before the next defttagin the top-level loop (if any). Moreoever, certify-book is illegalwhen a ttag is active; of course, in such a circ*mstance one can execute(defttag nil) in order to allow book certification.
Ttag notes and the ``certifier.'' When a defttag is executed withan argument other than nil, output is printed, starting on a fresh linewith: TTAG NOTE. For example:
ACL2 !>(defttag :foo)TTAG NOTE: Adding ttag :FOO from the top level loop. :FOOACL2 !>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. Theintention is that one can search the standard output for all such notes inorder to find all defttag events. In a sense, defttag events canallow 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 ismeaningful, that certifier should certify all the user-supplied books fromscratch and check either that no :ttags were supplied tocertify-book, or else look for every TTAG NOTE in the standardoutput in order to locate all defttag events with non-niltag name. In this way, the certifier can in principle decide whether to besatisfied that those defttag events did not allow inappropriate forms inthe 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 issomewhat less; therefore, a TTAG NOTE is printed when invokingset-deferred-ttag-notes to defer printing of ttag notes.
Allowed ttags when certifying and including books. A defttag formmay not be evaluated unless its argument is a so-called ``allowed'' ttag.All ttags are allowed in the interactive top-level loop. However, duringcertify-book and include-book, the set of allowed ttags isrestricted according to the :ttags keyword argument. If this argument isomitted then no ttag is allowed, so a defttag call will fail during bookcertification or inclusion in this case. This restriction applies even todefttag forms already evaluated in the so-called certification worldat the time certify-book is called. But note that (defttag nil) isalways legal.
A :ttags argument of certify-book and include-book can havevalue :all, indicating that every ttag is allowed, i.e., no restrictionis being placed on the arguments, just as in the interactive top-level loop.In the case of include-book, an omitted :ttags argument or anargument of :default is treated as :all, except that warnings willoccur when the book's certificate includes ttags; but forcertify-book, an omitted ttags argument is treated as nil.Otherwise, if the :ttags argument is supplied but not :all, then itsvalue is a true list of ttag specifications, each having one of the followingforms, where sym is a non-nil symbol which is treated as thecorresponding keyword.
(1)
:sym(2)
(:sym)(3)
(:sym x1 x2 ... xk), where k > 0 and eachxiis a string, exceptthat oneximay benil.
In Case (1), (defttag :sym) is allowed to occur in at most one book orelse in the top-level loop (i.e., the certification world for a book undercertification or a book being included). Case (2) allows (defttag :sym)to occur in an unlimited number of books. For case (3) the xi specifywhere (defttag :sym) may occur, as follows. The case that xi isnil refers to the top-level loop, while all other xi are filenames,where the ".lisp" extension is optional and relative pathnames areconsidered to be relative to the connected book directory (see cbd). Notethat the restrictions on (defttag :sym) apply equally to any equivalentfor 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 notionof allowed ttags. Suppose that you call certify-book with argument:ttags (:foo), where you have already executed (defttag :foo) in thecertification world (i.e., before calling certify-book). Then ACL2immediately associates the ttag :foo with nil, where again, nilrefers to the top-level loop. If ACL2 then encounters (defttag foo)inside that book, you will get the following error (using the full book namefor the book, as shown):
ACL2 Error in ( TABLE ACL2-DEFAULTS-TABLE ...): The ttag :FOO associatedwith file /u/smith/work/my-book.lisp is not among the set of ttags permittedin 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 withelements as discussed in (1) through (3) above. In this case, that list'sunique element is (:FOO NIL), meaning that ttag :FOO is only allowed atthe top level (as represented by NIL).Associating ttags with books and with the top-level loop. When a bookis certified, each form (defttag tag) that is encountered for non-niltag in that book or an included book is recorded in the generatedcertificate, which associates the keyword corresponding to tag withthe full-book-name of the book containing that deftag. If such adefttag form is encountered outside a book, hence in the portcullisof the book being certified or one of its included books, then that keywordis associated with nil in the generated certificate. Note that thenotion of ``included book'' here applies to the recursive notion of a bookeither included directly in the book being certified or else included in sucha book, where we account even for locally included books.
For examples of ways to take advantage of ttags, see community bookbooks/hacking/hacker.lisp and see ttags-seen, see progn!,see remove-untouchable, see set-raw-mode, and see sys-call.
