		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Ttags-seen

List some declared trust tags (ttags)

General Forms:
:ttags-seen
(ttags-seen)

Suppose the output is as follows.

(T NIL)
(FOO "/home/bob/bar.lisp"
     "/home/cindy/bar.lisp")
Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).

This output indicates that the current logical world has seen the declaration of trust tag T at the top-level (see defttag) and the declaration of trust tag FOO in the two books included from the listed locations. The warning emphasizes that this command cannot be used to validate the ``purity'' of an ACL2 session, because using a ttag renders enough power to hide from this or any other command the fact that the ttag was ever declared.

As discussed elsewhere (see defttag), the only reliable way to validate the ``purity'' of a session is to watch for ``TTAG NOTE'' output.

Another shortcoming of this command is that it only checks the current logical world for ttag declarations. For example, one could execute a defttag event; then use progn! and set-raw-mode to replace system functions with corrupt definitions or to introduce inconsistent axioms in the ground-zero world; and finally, execute :ubt! 1 to remove all evidence of the ttag in the world while leaving in place the corrupt definitions or axioms. The base world is now tainted, meaning we could prove nil or certify a book that proves nil, but the resulting session or book would contain no trace of the ttag that tainted it!

Despite shortcomings, this command might be useful to system hackers. It also serves to illustrate the inherent flaw in asking a session whether or how it is ``tainted'', justifying the ``TTAG NOTE'' approach (see defttag).