← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to doc/HTML/TTAGS-SEEN.html

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HTML/TTAGS-SEEN.html
 
1
<html>
 
2
<head><title>TTAGS-SEEN.html  --  ACL2 Version 3.1</title></head>
 
3
<body text=#000000 bgcolor="#FFFFFF">
 
4
<h2>TTAGS-SEEN</h2>list some declared trust tags (ttags)
 
5
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
 
6
</pre><p>
 
7
 
 
8
 
 
9
<pre>
 
10
General Forms:
 
11
:ttags-seen
 
12
(ttags-seen)
 
13
</pre>
 
14
 
 
15
Suppose the output is as follows.
 
16
 
 
17
<pre>
 
18
(T NIL)
 
19
(FOO "/home/bob/bar.lisp"
 
20
     "/home/cindy/bar.lisp")
 
21
Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).
 
22
</pre>
 
23
 
 
24
This output indicates that the current logical <a href="WORLD.html">world</a> has seen the
 
25
declaration of trust tag <code>T</code> at the top-level (see <a href="DEFTTAG.html">defttag</a>) and the
 
26
declaration of trust tag <code>FOO</code> in the two books included from the listed
 
27
locations.  The warning emphasizes that this command cannot be used to
 
28
validate the ``purity'' of an ACL2 session, because using a ttag renders
 
29
enough power to hide from this or any other command the fact that the ttag
 
30
was ever declared.
 
31
<p>
 
32
As discussed elsewhere (see <a href="DEFTTAG.html">defttag</a>), the only reliable way to validate
 
33
the ``purity'' of a session is to watch for ``<code>TTAG NOTE</code>'' output.<p>
 
34
 
 
35
Another shortcoming of this command is that it only checks the current
 
36
logical <a href="WORLD.html">world</a> for ttag declarations.  For example, one could execute a
 
37
<code><a href="DEFTTAG.html">defttag</a></code> event; then use <code><a href="PROGN_bang_.html">progn!</a></code> and <code><a href="SET-RAW-MODE.html">set-raw-mode</a></code> to replace
 
38
system functions with corrupt definitions or to introduce inconsistent axioms
 
39
in the <code><a href="GROUND-ZERO.html">ground-zero</a></code> <a href="WORLD.html">world</a>; and finally, execute <code>:</code><code><a href="UBT_bang_.html">1</a></code>
 
40
to remove all evidence of the ttag in the <a href="WORLD.html">world</a> while leaving in place
 
41
the corrupt definitions or axioms.  The base world is now tainted, meaning we
 
42
could prove <code>nil</code> or certify a book that proves <code>nil</code>, but the resulting
 
43
session or book would contain no trace of the ttag that tainted it!<p>
 
44
 
 
45
Despite shortcomings, this command might be useful to system hackers.  It
 
46
also serves to illustrate the inherent flaw in asking a session whether or
 
47
how it is ``tainted'', justifying the ``<code>TTAG NOTE</code>'' approach
 
48
(see <a href="DEFTTAG.html">defttag</a>).
 
49
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
 
50
</body>
 
51
</html>