		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Defwellformed

Defwellformed is a macro for introducing well-formedness checking functions.

Motivation

Throughout VL, there are many functions that check to see whether some module element is well-formed. When we introduce these well-formedness checks, we often want to have two versions of the check:

A vanilla Boolean-valued predicate, foo-okp, that causes no side effects and is easy to reason about, and
A debugging function, foo-okp-warn that generates useful warnings that explain precisely why the object is malformed. In particular, foo-okp-warn takes a warnings accumulator as an extra argument, and returns (mv okp warnings').

The value of the debugging function is probably obvious: it allows us to provide a better explanation for why some module is not being translated. But the debugging function is not well-suited for reasoning. In particular, in theorems we generally do not care about which warnings have been accumulated; we only want to know whether some structure is well-formed. If we try to use the debugging function directly for this purpose, we might write theorems such as:

(implies (and (foo-p x)
              (car (foo-okp-warn x warnings)))
         (consequence x))

The problem with such a theorem is that warnings is a free variable, which can cause problems for ACL2 when it tries to apply the rule.

So, our approach is to introduce both versions of the well-formedness check, and then add a theorem that shows the first value returned by foo-okp-warn is exactly the value returned by foo-okp. Accordingly, we can run foo-okp-warn in our code and get useful warning messages, but we can always reason about the simpler function foo-okp.

Unfortunately, writing two versions of a function comes at its own cost; we have to duplicate the code, keep both versions in sync, and write these boilerplate theorems. The macro defwellformed allows us to automate this process.

Using defwellformed

The defwellformed macro is similar to defun. The general form is:

(defwellformed foo-okp (x other-args ...)
  :guard (and (foop x) ...)
  :body [...]
  :extra-decls ((xargs ...))
  :parents ...
  :short ...
  :long ...)

Here, foo-okp is the name of the new vanilla function, and (x other-args ...) are the formals. The :guard and :body are used in the defun form we generate, as are any :extra-decls that you need. Finally, the parents, short, and long fields are as in defxdoc.

The debugging function is always named by appending -warn to the name of the vanilla function. Having such a convention is necessary for our implementation of (@wf-call ...).

Meta-macros

The tricky part to using defwellformed is to write a :body that serves both as the vanilla definition and as the debugging definition. To accomplish this, we make use of certain "meta-macros", which can be identifier with the prefix @wf-.

In particular, the bodies of our well-formedness checks generally look something like this:

(let ((bar ...)
      (baz ...))
  (@wf-progn
   (@wf-assert condition1 [type msg args])
   (@wf-assert condition2 [type msg args])
   (@wf-note condition type msg args)
   (@wf-call other-wf-check ...)
   ...))

These @wf- expressions are only valid in the body of the defwellformed command, and are given different expansions depending upon whether we are in the vanilla or debugging version of the function.

In the vanilla function,

(@wf-progn ...) becomes (and ...)
(@wf-and ...) becomes (and ...)
(@wf-assert condition ...) becomes (if condition t nil)
(@wf-note condition ...) becomes t
(@wf-call other-wf-check ...) becomes (other-wf-check ...)

But in the debugging function, a more complex expansion is used.

(@wf-progn ...): This becomes an appropriate mv-let strucutre to handle the return values from @wf-assert and @ commands. Note that in the debugging version execution continues after a violation is discovered so that we uncover as many problems as possible. This behavior can cause problems for guard verification: you cannot rely upon the earlier assertions having "passed" in the guards of your later assertions. Hence the introduction of @wf-and.
(@wf-and ...): This becomes an mv-let structure as in @wf-progn, but execution stops when any assertion is violated.
(@wf-assert condition type msg args): If the condition is violated, okp becomes nil and we add a (non-fatal) warning of the indicated type, message, and arguments.
(@wf-note condition type msg args): We add a warning of the indicated type, message, and args, to the list of warnings, but we do not set okp to nil. That is, this is just a way to note suspicious things that aren't necessarily outright problems.
(@wf-call other-wf-check ...): Becomes (other-wf-check-warn ...). In other words, this allows you to call the vanilla version of some subsidiary well-formedness check from the vanilla version of your function, and the debugging version from your debugging function.

Note also that defwellformed-list allows you to call a well-formedness predicate on every element in a list, and that mutual-defwellformed is a replacement for mutual-recursion that allows for the mutually-recursive use of defwellformed.