		Search-engine friendly clone of the ACL2 documentation.

Restrict

APT domain restriction transformation: restrict the effective domain of a function.

Introduction

Even though functions are total in ACL2 (i.e. their domain is always the whole ACL2 universe of values), the guard of a function can be regarded as its effective domain (i.e. where it is well-defined). This transformation adds restrictions to the guard, and wraps the body with a test for the restrictions, which may enable further optimizations by taking advantage of the added restrictions. As a special case, this transformation can leave the guard unchanged but wrap the body with a test for the guard, thus treating the guard as the restriction: this may enable further optimizations by effectively removing from consideration, in the body of the function, conditions under which the guard does not hold.

The restrict design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to them in some places.

General Form

(restrict old
          restriction
          :undefined          ; default :undefined
          :new-name           ; default :auto
          :new-enable         ; default :auto
          :old-to-new-name    ; default from table
          :old-to-new-enable  ; default from table
          :new-to-old-name    ; default from table
          :new-to-old-enable  ; default from table
          :verify-guards      ; default :auto
          :hints              ; default nil
          :print              ; default :result
          :show-only          ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be in logic mode, be defined, have at least one formal argument, return a non-multiple value, and have no input or output stobjs.If old is recursive, it must be singly (not mutually) recursive and not have a :? measure (see :measure in xargs). If the :verify-guards input is t, old must be guard-verified.
In the rest of this documentation page:
Let x1, ..., xn be the formal arguments of old, where n > 0.
Let old-guard<x1,...,xn> be the guard term of old.
If old is not recursive, let
old-body<x1,...,xn>
be the body of old.
If old is recursive, let
old-body<x1,...,xn,
         (old update1-x1<x1,...,xn,old>
              ...
              update1-xn<x1,...,xn,old>)
         ...
         (old updatem-x1<x1,...,xn,old>
              ...
              updatem-xn<x1,...,xn,old>)>
be the body of old, where m > 0 is the number of recursive calls in the body of old and each updatej-xi<x1,...,xn,old> is the i-th actual argument passed to the j-th recursive call. Furthermore, let contextj<x1,...,xn,old> be the context (i.e. controlling tests) in which the j-th recursive call occurs. The dependency of updatej-xi<...,old> and contextj<...,old> on old only applies to so-called `reflexive functions', i.e. functions that occur in their own termination theorem.
In the restrict design notes, old is denoted by f. When old is not recursive, old-body<x1,...,xn> is denoted by e(\overline{x}). When old is recursive, the design notes use a single non-recursive branch b(\overline{x}) controlled by a(\overline{x}) and a single recursive branch c(\overline{x},f(\overline{d}(\overline{x}))) controlled by the negation of a(\overline{x}): this is a representative recursive structure, but the transformation handles multiple non-recursive and recursive branches, and also recursive functions that occur in their termination theorem; in this representative recursive structure, update-xi<x1,...,xn> is denoted by d_i(\overline{x}) and context<x1,...,xn> is denoted by the negation of a(\overline{x}).

restriction

Denotes the restricting predicate for the domain of old, i.e. the predicate that will be added to the guard (unless this input is :guard, see below), and as the test that wraps the body.
It must be one of the following:
A term that only references logic-mode functions and that includes no free variables other than x1, ..., xn. This term must have no output stobjs. This term must return a single (i.e. non-mv value. If the generated function is guard-verified (which is determined by the :verify-guards input; see below), then this term must only call guard-verified functions, except possibly in the :logic subterms of mbes or via ec-call. This term must not reference old.This term must not be the keyword :guard, i.e. if the restriction input is :guard, it is treated as denoting the guard (see below), and not as denoting the term :guard, which may be denoted by using the quoted ':guard as the restriction input instead (even though there is no use case for doing so).
They keyword :guard.
The restriction input denotes the predicate (lambda (x1 ... xn) old-guard<x1,...,xn>) if restriction is :guard, otherwise it denotes the predicate (lambda (x1 ... xn) restriction). In the rest of this documentation page, we refer to this predicate as (lambda (x1 ... xn) pred<x1,...,xn>).
Using :guard as the restriction input is essentially equivalent to using the guard term of old as the restriction input. However, using :guard is simpler and more robust (in the face of changes to the guard), and leads to a simpler guard in the new function (see `Generated Events' below).
In the restrict design notes, (lambda (x1 ... xn) pred<x1,...,xn>) is denoted by R.

:undefined — default :undefined

Denotes the value that the generated new function must return outside of the domain restriction.
A term that only references logic-mode functions and that includes no free variables other than x1, ..., xn. This term must have no output stobjs. This term must return a single (i.e. non-mv value. This term must not reference old.
Even if the generated function is guard-verified (which is determined by the :verify-guards input; see below), the term needs not be guard-verified. Since the term is governed by the negation of the guard (see the generated new function, below), the verification of its guards always succeeds trivially.
In the rest of this documentation page, let undefined be this term.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

:old-to-new-name — default from table

Determines the name of the theorem that rewrites the old function in terms of the new function.
It must be one of the following:
A keyword, to use as separator between the names of old and new. A keyword :kwd specifies the theorem name oldkwdnew, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-to-new-name.
In the rest of this documentation page, let old-to-new be the name of this theorem.

:old-to-new-enable — default from table

Determines whether the old-to-new theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-to-new-enable.
If this input is t, the :new-to-old-enable input must be nil. At most one of these two inputs may be t at any time.

:new-to-old-name — default from table

Determines the name of the theorem that rewrites the new function in terms of the old function.
It must be one of the following:
A keyword, to use as separator between the names of new and old. A keyword :kwd specifies the theorem name newkwdold, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-new-to-old-name.
In the rest of this documentation page, let new-to-old be the name of this theorem.

:new-to-old-enable — default from table

Determines whether the new-to-old theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-new-to-old-enable.
If this input is t, the :old-to-new-enable input must be nil. At most one of these two inputs may be t at any time.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:hints — default nil

Hints to prove the applicability conditions.
It must be one of the following:
A keyword-value list (appcond1 hints1 appcond2 hints2 ...), where each appcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and each hintsk is a list of hints of the kind that may appear just after :hints in a defthm. The hints hintsk are used to prove applicability condition appcondk. The appcond1, appcond2, ... keywords must be all distinct. An appcondk keyword is allowed only if the corresponding applicability condition is present, as specified in the `Applicability Conditions' section.
A list of hints of the kind that may appear just after :hints in a defthm. In this case, these same hints are used to prove every applicability condition,.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of restrict. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of restrict.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of restrict is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of restrict is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of restrict is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Applicability Conditions

In order for restrict to apply, in addition to the requirements on the inputs stated in the `Inputs' section, the following applicability conditions must be proved. The proofs are attempted when restrict is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

:restriction-of-rec-calls

(lambda (x1 ... xn) pred<x1,...,xn>) is preserved across the recursive calls of old:
(implies pred<x1,...,xn>
         (and (implies context1<x1,...,xn,?f>
                       pred<update1-x1<x1,...,xn,?f>,
                            ...,
                            update1-xn<x1,...,xn,?f>>)
              ...
              (implies contextm<x1,...,xn,?f>
                       pred<updatem-x1<x1,...,xn,?f>,
                            ...,
                            updatem-xn<x1,...,xn,?f>>)))
where ?f is an n-ary stub that replaces old (this only applies to reflexive functions; see above).
This corresponds to \mathit{Rd} in the restrict design notes.
This applicability condition is present if and only if old is recursive.

:restriction-guard

The restricting predicate is well-defined (according to its guard) on every value in the guard of old:
(implies old-guard<x1,...,xn>
         pred-guard<x1,...,xn>)
where pred-guard<x1,...,xn> is the guard obligation of pred<x1,...,xn>.
This corresponds to \mathit{GR} in the restrict design notes.
This applicability condition is present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above).

Generated Events

new

Domain-restricted version of old:
;; when old is not recursive:
(defun new (x1 ... xn)
  (if (mbt$ pred<x1,...,xn>)
      old-body<x1,...,xn>
    undefined))

;; when old is recursive:
(defun new (x1 ... xn)
  (if (mbt$ pred<x1,...,xn>)
      old-body<x1,...,xn,
               (new update1-x1<x1,...,xn,new>
                    ...
                    update1-xn<x1,...,xn,new>)
               ...
               (new updatem-x1<x1,...,xn,new>
                    ...
                    updatem-xn<x1,...,xn,new>)>
    undefined))
If old is recursive, the measure term and well-founded relation of new are the same as old.
The guard is (and old-guard<x1,...,xn> pred<x1,...,xn>) if the restriction input is not :guard. Otherwise, the guard is just old-guard<x1,...,xn>.
Since the restriction test follows from the guard, the test is wrapped by mbt$. The use of mbt$, as opposed to mbt, avoids requiring pred<x1,...,xn> to be boolean-valued.
In the restrict design notes, new is denoted by f'.

old-to-new

Theorem that relates old to new:
(defthm old-to-new
  (implies pred<x1,...,xn>
           (equal (old x1 ... xn)
                  (new x1 ... xn))))
In the restrict design notes, old-to-new is denoted by \mathit{ff}'.

new-to-old

Theorem that relates new to old:
(defthm new-to-old
  (implies pred<x1,...,xn>
           (equal (new x1 ... xn)
                  (old x1 ... xn))))
In the restrict design notes, new-to-old is denoted by f'f.

A theory invariant is also generated to prevent both new-to-old and old-to-new from being enabled at the same time.

Redundancy

A call of restrict is redundant if and only if it is identical to a previous successful call of restrict whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of restrict whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Restrict-implementation: Implementation of restrict.