Major Section: MISCELLANEOUS
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
Tat the top-level (see defttag) and the declaration of trust tag
FOOin 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
set-raw-mode to replace
system functions with corrupt definitions or to introduce inconsistent axioms
ground-zero world; and finally, execute
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