TRACE!

trace the indicated functions after creating an active trust tag
Major Section:  TRACE

Example:
(trace! (fact :native t :entry *foo*))

General Form: (trace! spec1 ... specn)

where the fni are suitable arguments to trace$.

Trace! is a version of trace$ that avoids the need for an already-active trust tag (or ``ttag''; see defttag), as explained below. See trace$ for when a trust tag can be necessary.

See untrace$ for how to undo the effect of trace!.

The evaluation of a trace! form causes temporary creation of an active trust tag, :trace!, followed by the corresponding trace$ form. The trust tag will disappear when the call to trace! completes. Even though trace! will remove its temporary ttag, it will still print a ``TTAG NOTE'', which indicates that the session is suspect. See defttag and see ttags-seen for further remarks on this issue.

Because of the active trust tag, it is possible to do things with trace! that are useful but without logical justification. Below is an example of how to use trace! to cause a function call to change state, even though the function does not take state as a parameter.

ACL2 !>(defun fact (n)
         (declare (xargs :guard (natp n) :verify-guards nil))
         (if (zp n)
             1
           (* n (fact (1- n)))))

The admission of FACT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of FACT is described by the theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))). We used the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning.

Summary Form: ( DEFUN FACT ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 !>(defun update-foo (n value state) (declare (xargs :stobjs state :verify-guards nil)) (assign foo (cons (cons n value) (@ foo))))

Since UPDATE-FOO is non-recursive, its admission is trivial. We observe that the type of UPDATE-FOO is described by the theorem (AND (CONSP (UPDATE-FOO N VALUE STATE)) (TRUE-LISTP (UPDATE-FOO N VALUE STATE))). We used primitive type reasoning.

(UPDATE-FOO * * STATE) => (MV * * STATE).

Summary Form: ( DEFUN UPDATE-FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) UPDATE-FOO ACL2 !>(trace! (fact :exit (update-foo n value state)))

TTAG NOTE: Adding ttag :TRACE! from the top level loop. ((FACT :EXIT (UPDATE-FOO N VALUE STATE))) ACL2 !>(assign foo nil) NIL ACL2 !>(fact 7) 1> (ACL2_*1*_ACL2::FACT 7) 2> (ACL2_*1*_ACL2::FACT 6) 3> (ACL2_*1*_ACL2::FACT 5) 4> (ACL2_*1*_ACL2::FACT 4) 5> (ACL2_*1*_ACL2::FACT 3) 6> (ACL2_*1*_ACL2::FACT 2) 7> (ACL2_*1*_ACL2::FACT 1) 8> (ACL2_*1*_ACL2::FACT 0) <8 NIL <7 NIL <6 NIL <5 NIL <4 NIL <3 NIL <2 NIL <1 NIL 5040 ACL2 !>(@ foo) ((7 . 5040) (6 . 720) (5 . 120) (4 . 24) (3 . 6) (2 . 2) (1 . 1) (0 . 1)) ACL2 !>(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FACT. FACT is compliant with Common Lisp.

Summary Form: ( VERIFY-GUARDS FACT) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 !>(assign foo nil) NIL ACL2 !>(fact 7) 1> (ACL2_*1*_ACL2::FACT 7) 2> (FACT 7) 3> (FACT 6) 4> (FACT 5) 5> (FACT 4) 6> (FACT 3) 7> (FACT 2) 8> (FACT 1) 9> (FACT 0) <9 NIL <8 NIL <7 NIL <6 NIL <5 NIL <4 NIL <3 NIL <2 NIL <1 NIL 5040 ACL2 !>(@ foo) ((7 . 5040) (7 . 5040) (6 . 720) (5 . 120) (4 . 24) (3 . 6) (2 . 2) (1 . 1) (0 . 1)) ACL2 !>(trace! (fact :exit (progn (update-foo n value state) (cons traced-fn values))))

TTAG NOTE: Adding ttag :TRACE! from the top level loop. ((FACT :EXIT (PROGN (UPDATE-FOO N VALUE STATE) (CONS TRACED-FN VALUES)))) ACL2 !>(assign foo nil) NIL ACL2 !>(fact 7) 1> (ACL2_*1*_ACL2::FACT 7) 2> (FACT 7) 3> (FACT 6) 4> (FACT 5) 5> (FACT 4) 6> (FACT 3) 7> (FACT 2) 8> (FACT 1) 9> (FACT 0) <9 (FACT 1) <8 (FACT 1) <7 (FACT 2) <6 (FACT 6) <5 (FACT 24) <4 (FACT 120) <3 (FACT 720) <2 (FACT 5040) <1 (ACL2_*1*_ACL2::FACT 5040) 5040 ACL2 !>(@ foo) ((7 . 5040) (7 . 5040) (6 . 720) (5 . 120) (4 . 24) (3 . 6) (2 . 2) (1 . 1) (0 . 1)) ACL2 !>