Speed up a function using verified input-output pairs

For examples, see the book

**Summary**. This utility provides a way to redefine a function so that
it can quickly look up a function call `show-io-pairs` for how to
print the current I/O pairs. The present utility,

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 (((rtl::primep (primes::secp256k1-field-prime)) t) ((rtl::primep (primes::bn-254-group-prime)) t) ((rtl::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) wherefn is a guard-verified function symbol, eachi_n is a term, andval 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. Alli_n andval are evaluated to produce values used as inputs and corresponding output; therefore, these terms should not contain any free variables.Hints (optional, defaultnil ), when non-nil , is used as the: `hints`argument for the theorem discussed below.Test (optional, defaultequal ) is the equality variant —`eq`,`eql`, or`equal`— used for testing equality of each input offn 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, defaultnil ), 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 forfn ).Verbose (optional, defaultnil ), 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 equatesfn to the corresponding new function (that looks up inputs from a table of all verified I/O pairs).

If

This event defines a new function, denoted

(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 `pcb!`

In the underlying Common Lisp, `cw` will not take place for such an input list.

A generated proof obligation has the following form, where

(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

Remark 2. Evaluation of input and output terms in an I/O pair is performed
with guard-checking set to

Remark 3. Although `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

Remark 4. A more general utility, which allows the substitution of one
function for another during execution, is available with the `memoize`. Indeed,

Remark 5. If you include a book with an `make-event` in the implementation of

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

(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

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

- 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