Defwarrant
Issue a warrant for a function so apply$ can use it in proofs
It is best to be somewhat familiar with the documentation of apply$ before reading this topic.
Before using defwarrant or a utility like defun$ that relies
on it:
(include-book "projects/apply/top" :dir :system)
Several lemmas in that book are necessary for defwarrant to prove
the theorems it must prove.
Badges versus Warrants
It is easy to confuse badges, which are issued by defbadge,
with warrants, which are issued by defwarrant. See the first
section of defbadge for an extended discussion.
Requirements of Defwarrant
General Form:
(defwarrant fn)
where fn is a defined function name. This command analyzes the body
of fn to determine whether it satisfies certain stringent syntactic and
semantic conditions that allow the ACL2 proof theory to be extended so that
the prover can simplify forms like (apply$ 'fn ...). The syntactic
conditions include those of defbadge, which defwarrant
essentially invokes if fn is a :logic mode function that is
not already badged. But below we describe all the conditions checked by
defwarrant since many users use defwarrant to issue both a badge
and a warrant.
Basic conditions include that fn is in :logic-mode and
that its justification (i.e., the measure, well-founded relation, and domain
predicate used to admit fn) be expressible without any reference to
apply$, ev$, or apply$-userfn.
Defwarrant imposes some additional conditions on fn, but exactly
what those conditions are depends on a certain ``reachability'' test detailed
in the section titled The ``Reachability'' Test in defbadge.
Roughly speaking the test is whether apply$ is ancestral in fn,
meaning apply$ is somehow involved in the definition of fn or the
functions it calls.
If the reachability test succeeds — colloquially, if fn depends
on apply$ — then defwarrant imposes the following additional
conditions in order to issue a warrant.
(a) If fn is recursive it must not be part of a mutually
recursive clique and its measure must be of type natp or be a
lexicographic combination of natural numbers as defined by the llist
function in the Community Books at books/ordinals/.
(b) Every function called in the body of fn, except fn
itself, must already have a badge and a warrant. If some subfunction
doesn't already have a badge, defwarrant will call defbadge and
signal an error if that fails. If some subfunction doesn't already have a
warrant, defwarrant will signal an error and suggest that you call
defwarrant on the offending subfunction first. Defwarrant will
continue to fail until all subfunctions have badges and warrants.
(c) It must be possible for each formal of fn to be assigned
one of three ilks, :FN, :EXPR, or NIL, as described
below. The basic idea is that a formal can be assigned ilk :FN (or ilk
:EXPR) iff it is sometimes passed into a :FN (or :EXPR) slot
in the body of fn and is never passed into any other kind of slot. A
formal can be be assigned ilk NIL iff it is never passed into a slot of
ilk :FN or :EXPR, i.e., if it is used as an ``ordinary'' object.
We are more precise below.
(d) Every :FN and :EXPR slot of every function called in
the body of fn is occupied either by a formal of fn of the same ilk
or, in the case of calls of functions other than fn, a quoted tame function symbol or quoted tame (preferably well-formed) LAMBDA
object.
This completes the list of additional restrictions imposed by
defwarrant on fn, when apply$ is reachable from fn.
If the reachability test fails — colloquially, if fn does not
depend on apply$ — then defwarrant just checks that fn
does not call any of a few functions that apply$ is prohibited from
running. Among those blacklisted functions are sys-call and other
functions requiring a trust tag. For a list of the blacklisted functions see
the value of *blacklisted-apply$-fns*.
Note that the restrictions imposed on functions from which apply$
cannot be reached are comparatively generous. If fn does not depend on
apply$ then fn can be warranted despite (a) being defined mutually
recursively or with an arbitrary ordinal measure, or (b) calling unbadged or
unbadgeable functions. Defwarrant can be relaxed in this case because
the warrant constrains (apply$ 'fn ...) to be (fn ...) and fn
is a well-defined :logic mode function that is independent of
apply$. Thus, in the model of apply$ that justifies the whole
apply$ story, the handling of fn is just a base case. The
situation would be more restrictive if the warrant constrained (apply$ 'fn
...) to evaluate the body of fn with ev$ which would possibly
raise termination issues.
Regardless of whether apply$ is reachable, if the requisite
conditions are not met, defwarrant causes an error.
If the requisite conditions are met, defwarrant obtains or constructs
the badge for fn, setting the arity and out arity appropriately
and setting the ilks field to the list of computed ilks (or to T if
every formal has ilk NIL). The generated badge is stored for the future
use of defwarrant. See defbadge for a brief discussion of how
ilks are computed.
Furthermore, defwarrant generates the warrant for fn.
The name of that 0-ary function will be APPLY$-WARRANT-fn. Calls of
apply$ on 'fn in proof attempts can only be simplified if the
warrant hypothesis, (APPLY$-WARRANT-fn), aka ``the warrant,'' is
among the hypotheses of the conjecture being proved. The warrant specifies
the values of both (badge 'fn) and (apply$ 'fn ...), including the
tameness requirements imposed on apply$. (The warrant explicitly
specifies the values of badge-userfn and apply$-userfn and
then defwarrant proves rewrite rules to make calls of badge and
apply$ simplify accordingly.)
If a warrant is issued for fn, then defwarrant also extends
ACL2's evaluation theory (but not its proof theory) so that the warrant
hypothesis is assumed true in that theory, allowing calls of badge and
apply$ to be evaluated in the evaluation theory (but not in the proof
theory). See warrant for details.
You might worry that theorems burdened by warrants are vacuously valid
because it might be impossible to satisfy all the warrant hypotheses. You
needn't worry about this. There is a model of apply$ and all of its
scions that makes every warrant issued by defwarrant valid.
The proof of this is sketched in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore and fully fleshed out in the comment titled Essay on
Admitting a Model for Apply$ and the Functions that Use It in the ACL2
source file apply-raw.lisp.
Defwarrant also proves that fn-equal is a congruence
relation for each :FN position of fn.
Subtopics
- Fn-equal
- Equivalence relation on tame functions
