Defttag
Introduce a trust tag (ttag)
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
<final 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 Form:
(defttag tag-name)
where tag-name is a symbol.
Note however that 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 contain calls of 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 names 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 functions, including sys-call; evaluate the form
(strip-cars *ttag-fns*) to see the full list of such symbols. The macro
progn! similarly requires an active ttag. 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). Moreover, 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 may be
restricted according to the :ttags keyword argument. If this argument is
nil 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 enforces 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 book's absolute
pathname, 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
defttag. 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 hacker, include-raw, quicklisp, and more generally interfacing-tools.
See also ttags-seen, progn!, remove-untouchable, set-raw-mode, and sys-call.
Subtopics
- Set-raw-mode
- Enter or exit ``raw mode,'' a raw Lisp environment
- Include-raw
- A better way to load raw Lisp code than directly using progn!
or set-raw-mode.
- Remove-untouchable
- Remove names from lists of untouchable symbols
- Push-untouchable
- Add name or list of names to the list of untouchable symbols
- Set-deferred-ttag-notes
- Modify the verbosity of TTAG NOTE printing
- Untouchable
- Function symbols and state globals that cannot be referenced
- Set-raw-mode-on!
- Enter ``raw mode,'' a raw Lisp environment (adds trust tag)
- Set-raw-mode-on
- Enter ``raw mode,'' a raw Lisp environment (requires trust tag)
