With-guard-checking
Suppress or enable guard-checking for a form
Example:
; Turn off all guard-checking for the indicated calls of append and car:
(with-guard-checking :none
(append 3 4))
General Form:
(with-guard-checking val form)
where val evaluates to a legal guard-checking value (see set-guard-checking, or evaluate *guard-checking-values* to see the list
of such values), and form is a form that does not mention state
(unless there is an active trust tag, in which case mention of state can
be unsound; see below). See with-guard-checking-error-triple and with-guard-checking-event for analogous utilities to be used with forms that
return error-triples. Form is to be evaluated in a scope such
that, in essence, (set-guard-checking val) is first executed locally in
that scope. However, this guard-checking setting is ignored once evaluation
passes into raw Lisp functions (see guards-and-evaluation).
Note that the addition of with-guard-checking does not change the
proof obligations generated for guard verification. However, ec-call
can be used in order to eliminate those proof obligations. Consider the
following example.
(defun f1 (x)
(declare (xargs :guard t))
(with-guard-checking nil (ec-call (nth t x))))
Then guard verification succeeds, and evaluation of the form (f1 '(1 2
3)) will return 1, without causing a guard violation. However, if
ec-call is instead removed from this definition, then guard verification
will fail, and for good reason, as illustrated by the following example.
(defun f2 (x)
(declare (xargs :guard t))
(with-guard-checking nil (nth t x)))
(defun f3 (x)
(declare (xargs :guard t))
(f2 x))
Suppose guard verification were to succeed for f2. Then of course it
would also succeed for f3. But the call (f3 nil) would then cause a
raw Lisp error (at least in many host Lisps), because it would lead to a
raw-Lisp call of nth whose first argument is not a number.
The remainder of this topic provides a remark for advanced users.
With-guard-checking is implemented using return-last, which you
can in principle call directly; use :trans or :trans1 to see how a call of with-guard-checking expands to a
corresponding call of return-last. However, ACL2 enforces a couple of
checks that can only be circumvented if there is an active trust tag. The
following example from Jared Davis shows why those checks are required
(in particular, it shows how circumventing them with a trust tag can be
unsound). We start by defining our own version of the utility, which omits
the check that the form has no occurrences of state.
(defmacro my-with-guard-checking (val form)
`(with-guard-checking1 (chk-with-guard-checking-arg ,val)
,form))
Submitting the following event results in the error shown just below
it.
(defun foo (state)
(declare (xargs :stobjs state
:guard (f-boundp-global 'guard-checking-on state)))
(my-with-guard-checking :all (f-get-global 'guard-checking-on state)))
ACL2 Error in ( DEFUN FOO ...): The form
(RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
(CHK-WITH-GUARD-CHECKING-ARG :ALL)
(F-GET-GLOBAL 'GUARD-CHECKING-ON STATE))
is essentially a call of WITH-GUARD-CHECKING, but without certain checks
performed. This is illegal unless there is an active trust tag; see
:DOC defttag. To avoid this error without use of a trust tag, call
WITH-GUARD-CHECKING directly. Note: this error occurred in the context
(WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :ALL)
(F-GET-GLOBAL 'GUARD-CHECKING-ON
STATE)).
But if we first evaluate (defttag t), then the defun event
above is admitted, and we can subsequently prove something that is not
true.
(thm (equal (foo state)
(f-get-global 'guard-checking-on state)))
(assert-event (not (equal (foo state)
(f-get-global 'guard-checking-on state))))
