Add-io-pairs
Speed up a function using verified input-output pairs
For examples, see the book std/util/add-io-pairs-tests.lisp in
community-books. Also see add-io-pair for an equivalent utility
with slightly simpler syntax that can add a single input-output pair.
Summary. This utility provides a way to redefine a function so that
it can quickly look up a function call (fn i1 ... ik) to produce its
output, val, thus avoiding its usual computation. We call such a pair
((fn i1 ... ik) val) an ``I/O pair'' (for fn). Each I/O pair is
``verified'': a proof obligation has been met showing that the input list is
indeed mapped to the corresponding output. The (verified) I/O pairs are
stored efficiently in a table. See show-io-pairs for how to
print the current I/O pairs. The present utility, add-io-pairs, extends
the table by adding the specified I/O pairs and also redefines the specified
function to take advantage of the updated table.
Examples (see std/util/add-io-pairs-tests.lisp):
(add-io-pairs (((f 3) '(3 . 3))))
(add-io-pairs (((g 3 6) (mv (* 3 10) (* 6 10)))
((g (/ 40 10) (/ 50 10)) (mv 40 50))))
(add-io-pairs
(((primep (primes::secp256k1-field-prime)) t)
((primep (primes::bn-254-group-prime)) t)
((primep (primes::baby-jubjub-subgroup-prime)) t))
:debug t
:hints (("Goal"
:in-theory
(enable primes::primep-of-baby-jubjub-subgroup-prime-constant
primes::primep-of-bn-254-group-prime-constant
primes::primep-of-secp256k1-field-prime-constant))))
General Form:
(add-io-pairs tuples &key hints debug test verbose)
where the arguments, which are not evaluated, are described below and the
keyword arguments are optional.
- Tuples is a list of I/O pairs, each of the form ((fn i_1 ... i_k)
val) where fn is a guard-verified function symbol, each i_n
is a term, and val is a term. (The terms need not be translated.)
Fn must be the same in each of these I/O pairs, and must not take state or any user-defined stobj as an argument. All i_n and
val are evaluated to produce values used as inputs and corresponding
output; therefore, these terms should not contain any free variables.
- Hints (optional, default nil), when non-nil, is used as the
:hints argument for the theorem discussed below.
- Test (optional, default equal) is the equality variant —
eq, eql, or equal — used for testing equality of
each input of fn to a corresponding input of an I/O pair; or, test
can be a true-list of such equality variants, as described in the concluding
remarks below.
- Debug (optional, default nil), when non-nil, causes cw to print a message to the terminal when an I/O pair is being used during
evaluation (thus avoiding the usual computation for fn).
- Verbose (optional, default nil), when non-nil, avoids
suppressing output (other than what is currently globally suppressed; see
set-inhibit-output-lst). This argument may be particularly useful when
the proof fails for the theorem, described below, that equates fn to the
corresponding new function (that looks up inputs from a table of all verified
I/O pairs).
If tuples is nil then the call of add-io-pairs is a no-op.
Otherwise, as noted above, the function symbol (fn, above) must be the
same for each I/O pair.
This event defines a new function, denoted new-fn below (the actual
name is generated automatically), to compute as follows. First, the inputs
i_n and corresponding output val of an I/O pair ((fn i_1 ... i_k)
val) are evaluated to produce a corresponding ``evaluated I/O pair'' ((fn
j_1 ... j_k) v), where the values of i_n and val are j_n and
v, respectively. Then new-fn is defined so that (fn j_1
... j_k) is computed by finding that evaluated I/O pair and returning
v, thus avoiding the usual computation for fn. That is: a call of
new-fn considers every evaluated I/O pair ((fn j_1 ... j_k) val),
whether added by this call of add-io-pairs or a previous such call,
searching for one whose inputs (j_1 ... j_k) equal that call's actual
parameters, and returning the corresponding output v in that case; if no
such evaluated I/O pair is found, then new-fn just calls fn. This
description is accurate if fn returns a single value; otherwise, if
fn returns n values where n is greater than 1, val should
evaluate to multiple values (mv v_1 .... v_n), in which case the multiple
values returned by new-fn are v_1 through v_n. The definition
of new-fn thus has roughly the following form, where: IO-LOOKUP
denotes a lookup utility that searches for the given inputs among evaluated
I/O pairs, returning the one-element list containing the value associated with
those inputs, if found; TEST is the value for :test discussed
above (defaulting to equal); and IO-PAIRS is the extension of the
existing evaluated I/O pairs for fn by the current call of
add-io-pairs, as described above.
(defun new-fn (x1 ... xk) ; same formals as for fn
(declare (xargs :guard t)) ; ensure guard-verified
<declare_forms> ; same declare forms as for fn
(let ((pair <<IO-LOOKUP (x1 ... xk) in 'IO-PAIRS using 'TEST>>))
(if pair
(car pair)
(fn x))))
The event displayed above is approximate. One can see the precise
definition produced by evaluating a call of add-io-pairs and using
:pcb! :x to see what has been generated. Alternatively, run
add-io-pairs using option :verbose t and peruse the log.
In the underlying Common Lisp, fn is redefined to be new-fn, but
with a twist: once control passes from fn to new-fn, all recursive
calls of fn will be calls of the old version of fn, without
re-entering new-fn. Note that when new-fn is called on an input
list that has an associated I/O pair, the corresponding output is returned
immediately without calling fn (which of course is the point of this
tool); thus, in particular, side effects from fn such as printing with
cw will not take place for such an input list.
A generated proof obligation has the following form, where HINTS below
is the non-nil :hints keyword if supplied by add-io-pairs;
otherwise the :hints keyword below is omitted.
(defthm <generated_name>
(equal (fn x1 ... xk)
(new-fn x1 ... xk))
:hints HINTS ; omitted if the given :hints is nil or omitted
:rule-classes nil)
We conclude with a few remarks.
Remark 1. When the value :test is a non-nil list, its length
should be the number of inputs of fn and each member should be eq,
eql, or equal, indicating the test used when comparing an input at
that position to an input specified in an evaluated I/O pairs for fn.
Remark 2. Evaluation of input and output terms in an I/O pair is performed
with guard-checking set to nil (see set-guard-checking) and
attachments allowed (see defattach).
Remark 3. Although fn is required to be guard-verified, one
may be able to avoid most of the effort of guard verification by using ec-call. Here is a trivial example that illustrates the technique.
ACL2 !>(defun h (x)
(declare (xargs :guard t))
(ec-call (car x)))
Since H is non-recursive, its admission is trivial. We could deduce
no constraints on the type of H.
Computing the guard conjecture for H....
The guard conjecture for H is trivial to prove. H is compliant with
Common Lisp.
Summary
Form: ( DEFUN H ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
H
ACL2 !>(add-io-pairs (((h 3) nil) ((h '(a b c)) 'a)) :debug t)
H
ACL2 !>(h 3)
; DEBUG: Found io-pair for input list (3).
NIL
ACL2 !>(h '(a b c))
; DEBUG: Found io-pair for input list ((A B C)).
A
ACL2 !>(h '(e f))
E
ACL2 !>(h 7)
ACL2 Error in TOP-LEVEL: The guard for the function call (CAR X),
which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 7).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.
ACL2 !>(add-io-pair (h 7) nil)
H
ACL2 !>(h 7)
NIL
ACL2 !>(h '(a b c))
A
ACL2 !>
Note that there is no debug printing in the final two calls. This isn't
surprising for (h 7), since the call of add-io-pair for (h 7)
did not specify keyword argument :debug. It may be more surprising that
debug printing no longer occurs for (h '(a b c)). The reason is that
each invocation of add-io-pair or add-io-pairs defines a new
replacement function (denoted new-fn in the discussions above), which is
based on the updated table of evaluated I/O pairs and the :debug option
provided to the new invocation.
Remark 4. A more general utility, which allows the substitution of one
function for another during execution, is available with the :invoke
argument of memoize. Indeed, add-io-pairs actually works by
invoking (memoize 'fn :invoke 'new-fn), where new-fn is as above.
Note that this memoization does not perform memoize's usual function of
saving computational results.
Remark 5. If you include a book with an add-io-pairs form for a
function symbol, fn, to which you have already added I/O pairs in the
current session, then by default an error will occur. The key relevant
observation is that during book certification, when add-io-pairs defines
new-fn as discussed above, that definition is saved in the book's certificate. (Technical note: This is a consequence of the use of make-event in the implementation of add-io-pairs.) Without an error,
ACL2 would simply use that saved definition of new-fn, discarding the I/O
pairs previously added in the current session.
The error message explains how to allow the include-book to
complete without error, merging in all I/O pairs from the current session and
included books by wrapping it in a call of the macro, merge-io-pairs,
whose first argument is fn. So a sequence of events might look like
this.
(defun f (x)
(declare (xargs :guard t))
(cons x x))
(include-book "book1") ; has calls of add-io-pair(s) for f
(merge-io-pairs
f
(include-book "book2") ; has calls of add-io-pair(s) for f
)
An analogous problem occurs with encapsulate, when there are local calls of add-io-pairs followed by non-local calls. Much as
certify-book saves the definition of new-fn in the book's
certificate, ACL2 saves such a definition from the first pass of the
encapsulate and detects missing I/O pairs (the local ones) in the second
pass. We expect local calls of add-io-pairs inside encapsulate to
be rare, so we do not discuss them further.
Although the discussion above and the error message should suffice, you can
get more understanding by looking at examples in the section ``Including a
book'' in community-book std/util/add-io-pairs-tests.lisp. For
technical details (probably not necessary), you are also welcome to see add-io-pairs-details.
Subtopics
- Add-io-pairs-details
- Details about add-io-pairs
- Show-io-pairs
- Display verified input-output pairs
- Get-io-pairs
- Return a list of verified input-output pairs
- Merge-io-pairs
- Incorporate I/O pairs from different sources
- Remove-io-pairs
- Remove input-output pairs
- Add-io-pair
- Speed up a function using a verified input-output pair
- Deinstall-io-pairs
- Deinstall input-output pairs
- Install-io-pairs
- Install input-output pairs
