Verify-guards+
Verify the guards of a function
We assume familiarity with guard verification; see verify-guards. Unlike verify-guards, the macro call (verify-guards+
mac ...) will verify guards for a function, fn, such that the macro
mac is associated with the function symbol fn in macro-aliases-table
(also see add-macro-alias). For example, if you define a macro
app and list append function binary-app, and you associate macro
app with function symbol binary-app in macro-aliases-table,
then evaluation of the form (verify-guards+ app) will have the effect of
evaluating (verify-guards fn). Note that in this setting, evaluation of
(verify-guards app) would cause an error, because app is a macro and
verify-guards, unlike verify-guards+, cannot handle macros.
The rest of this documentation topic discusses why we do not simply
arrange that verify-guards be permitted to take a macro alias. The
following example shows a soundness issue in doing so.
(encapsulate
()
(defun f1 (x)
(declare (xargs :guard (consp x)
:verify-guards nil))
(car x))
(defun f2 (x)
(declare (xargs :guard t
:verify-guards nil))
(cdr x))
(defmacro mac (x)
x)
(add-macro-alias mac f2) ; silly macro alias ;
(local (add-macro-alias mac f1)) ; alternate silly macro alias ;
(verify-guards mac))
If we were to allow macro aliases in verify-guards, this event
would be admitted, because on the first pass we are verifying guards of
f1. But after the encapsulate form completes evaluation, it
would appear that f2 is guard-verified. That could of course cause a raw
Lisp error.
The enhanced functionality provided by verify-guards+ does not have
the above problem, because it takes advantage of make-event to avoid
taking advantage of the contradictory results produced by the two calls of
add-macro-alias. See make-event. If the specific example above
is modified by replacing verify-guards with verify-guards+, then the
first pass through the encapsulate form will expand the form
(verify-guards+ mac) to (verify-guards f1). That same expansion
will be used for the verify-guards+ call during the second pass through
the encapsulate form, which is evaluated successfully and leaves us in a
world where f1 is guard-verified and f2 is not.
