verify the guards of a function
Major Section:  EVENTS

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-guard+ app) will have the effect of evaluating (verify-guards fn). Note that in this setting, evaluation of (verify-guard 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.

 (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)
 (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.