APT solving transformation: directly determine a solution to a specification.

Program synthesis, i.e. deriving a program from a specification, can be viewed as a form of constraint solving: the specification expresses the constraints, and the synthesized program is a solution to the constraints. In some cases, this kind of constraint satisfaction problem can be solved directly, e.g. via inference techniques. This transformation attempts to solve a specification directly, producing a satisfying program if successful.

A specification is a predicate over target programs,
so that a solution to a specification is indeed a program.
The programs may be deeply or shallowly embedded in the ACL2 logic,
according to the pop-refinement and shallow pop-refinement approaches, respectively.
Currently, this solving transformation operates on
specifications over shallowly embedded programs,
i.e. second-order predicates in ACL2.
Currently, this solving transformation expects
these predicates to be expressed using SOFT, but the transformation may be extended, in the future,
to operate on second-order predicates expressed via
the built-in `apply$`.

A range of direct solving methods may be employed: rewriting, narrowing (i.e. computing sufficient conditions), witness finding via resolution, SMT solving, SAT solving, etc. Currently this solving transformation only supports (two forms of) rewriting, but there are plans to extend it to additional methods. Note that some of the methods listed above correspond to the sketching approach to program synthesis, which can therefore be a valuable tool in APT's arsenal.

This transformation also supports a manual solving method, in which the user provides the solution, possibly with hints to prove its correctness. While this is not an automatic method like the ones described above, it may be useful when the automatic methods fail, or when the solution happens to be simple to find and to prove. Using this transformation with the manual solving method is generally more convenient than writing out the full refinement step: in particular, this transformation automates the generation and proof of the refinement theorem (i.e. that the new specification implies the old one) from the proof that the manually provided solution satisfies the (old) specification.

Solving methods that require tools that are not part of ACL2 can be modularly and selectively used by including the files in which the callers of such tools reside. This solving transformation, as part of input validation, checks that (the file of) the specified solving method has been loaded (more precisely, it checks that the function symbol of the caller is present in the ACL2 world). The caller is called via reflection by the solving transformation.

The

(solve old :method ; no default :method-rules ; default nil :solution-name ; default :auto :solution-enable ; default nil :solution-guard ; default t :solution-guard-hints ; default nil :solution-body ; no default :solution-hints ; default nil :new-name ; default :auto :new-enable ; default :auto :old-if-new-name ; default from table :old-if-new-enable ; default from table :verify-guards ; default :auto :print ; default :result :show-only ; default nil )

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 a SOFT quantifier function (see `Classification' section insoft::defsoft) that depends on one function variable (let it be?f ), that has no parameters, and whose body has the form(forall (x1 ... xn) matrix<(?f x1 ... xn)>)where

x1 , ...,xn are 0 or more variables andmatrix<(?f x1 ... xn)> is a term that contains a single call of?f onx1 , ...,xn (after translation andletexpansion).The transformation attempts to solve for

?f , i.e. to determine ann -ary function that satisfies the constraints thatold puts on?f .In the

solve design notes,old is denoted byS ,?f is denoted byf ,x0 , ...,xn are denoted by the single variablex (the generalization to multiple variables is straighforward in the design notes), andmatrix<(?f x1 ... xn)> is denoted byR(x,f(x)) .

Specifies the solving method to use.

It must be one of the following:

:acl2-rewriter , to use the ACL2 rewriter. This method is made available by including community bookkestrel/apt/solve-method-acl2-rewriter.lisp .:axe-rewriter , to use the Axe rewriter. This method is available by including community bookkestrel/apt/solve-method-axe-rewriter.lisp .:manual , to manually supply a solution.Support for more methods is planned.

Specifies the ACL2 or Axe rewrite rules to use when

:method is:acl2-rewriter or:axe-rewriter .It must be a list of symbols that are names of ACL2 theorems usable as ACL2 or Axe rewrite rules.

For the ACL2 rewriter, these rules are added to the current theory, and the rewriter operates in the so-augmented theory. For the Axe rewriter, these rules define the theory that the rewriter operates on.

This input may be present only if

:method is:acl2-rewriter or:axe-rewriter .

Determines the name of the solution function for

?f , and whether the function is generated or not.It must be one of the following:

:auto , which may only be used when the name of?f starts with a? . In this case, the function is generated, and its name is the symbol obtained by removing the initial? from the name of?f .- A symbol that names an existing function. In this case, the function is not generated: the existing function is used instead. This is allowed only if
:method is:manual .- Any other symbol, to use as the name of the solution function, which is generated in this case.
If this input is the name of an existing function, then the inputs

:solution-enable ,:solution-guard ,:solution-guard-hints , and:solution-body must be all absent. If any of these inputs are present, then the:solution-name input must not be the name of an existing function.If this input is the name of an existing function, it must be in logic mode and it must be defined. Its arity must be the same as

?f . It must return a single result. If guards must be verified (as determined by the:verify-guards input), then the function must be guard-verified.In the rest of the documentation page, let

f be the name of this function, whether it already exists or is generated.

Determines whether

f is enabled, when this function is generated.It must be one of the following:

t , to enable it.nil , to disable it.This input must be absent if

f already exists.

Determines the guard of

f , when this function is generated.It must be an untranslated term whose free variables are among

x1 , ...,xn . The term must return a single (i.e. non-mv) result.See Section `Solution Determination' below for a discussion about this input.

This input must be absent if

f already exists.

Determines the hints to verify the guards of

f , when this function is generated.See Section `Solution Determination' below for a discussion about this input.

This input may be present only if guards are to be verified, as determined by the

:verify-guards input.This input must be absent if

f already exists.

Specifies the body of the solution function, when

:method is:manual andf is generated.It must be an untranslated term whose free variables are among

x1 , ...,xn . The term must return a single (i.e. non-mv) result.See Section `Solution Determination' below for a discussion about this input.

This input must be present if

:method is:manual andf is generated; otherwise, this input must be absent.

Specifies the hints to prove the correctness of the solution, when

:method is:manual .This input may be present only if

:method is:manual .

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.

Determines whether

new is enabled.It must be one of the following:

t , to enable it.nil , to disable it.:auto , to enable it iffold is enabled.

Determines the name of the theorem asserting that the old function is implied by the old function.

It must be one of the following:

- A keyword, to use as separator between the names of
old andnew . A keyword:kwd specifies the theorem nameoldkwdnew , in the same package asnew .- 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-if-new-name.In the rest of this documentation page, let

old-if-new be the name of this theorem.

Determines whether the

old-if-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-if-new-enable.If this input is

t , the:new-to-old-enable input must benil . At most one of these two inputs may bet at any time.

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 functionold are verified.

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 ofsolve . This is the default value of the:info , to print, besides any error output and the results, also some additional information about the internal operations ofsolve .: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

solve is redundant, an indication to that effect is printed on the screen, unlessnil .

Determines whether the event expansion of

solve 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 ifnil (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:result or:info or:all ; no ACL2 output is printed for the event expansion even if:all (because the event expansion is not submitted). If the call ofsolve is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

The transformation attempts to find a solution for

When the

Consider the outer `if` tree structure of

- If
result is not a call of`if`, thenresult is the only leaf. - If
result has the form(if a b c) , recursively collect the leaves ofb ofc , and join them into a list.

For instance, if

There are three cases to consider.

The first case is the one where all the collected leaves are

(defun f (x1 ... xn) nil)

The fact that `if` tree)
means that any

The second case is the one where one collected leaf has the form

(equal (?f x1 ... xn) term<x1,...,xn>)

where

(defun f (x1 ... xn) term<x1,...,xn>)

The conditions under which the rewritten term is

The third case is the one where the two cases above do not apply. In this case, the transformation fails. No solution has been determined.

Support for determining solutions in more cases may be added in the future.

Note that, in the second case above,
there is no general guarantee that

When the transformation is successful,
the ACL2 or Axe rewriting provides
an ACL2 or Axe proof of correctness of the solution.
This should suffice to generate an ACL2 proof
of the

In any case, the transformation attempts to prove a theorem to confirm the correctness of ACL2's or Axe's rewriting in ACL2. If that theorem is successful, the transformation internally generates a theorem of the form

(implies (equal (?f x1 ... xn) term<x1,...,xn>) matrix<(?f x1 ... xn)>)

which essentially says that the matrix of

When the

If

(implies (equal (?f x1 ... xn) (f x1 ... xn)) matrix<(?f x1 ... xn)>)

This proof is attempted via the

If

(defun f (x1 ... xn) term<x1,...,xn>)

where

It must be the case that

(implies (equal (?f x1 ... xn) term<x1,...,xn>) matrix<(?f x1 ... xn)>)

This proof is attempted via the

The guard of

The solution for

?f .(defun f (x1 ... xn) (declare (xargs :guard ...)) ; from :solution-guard input ...) ; see section 'Solution Determination' aboveThis is not generated if

:method is:manual and:solution-name names an existing function.In the

solve design notes,f is denoted byf_0 .

Specification strengthened by choosing the solution, i.e. equality between

?f andf :(soft::defun-sk2 new () (forall (x1 ... xn) (equal (?f x1 ... xn) (f x1 ... xn))))In the

solve design notes,new is denoted byS' .

Theorem asserting that

new impliesold (i.e. a refinement relation):(defthm old-if-new (implies (new) (old))In the

solve design notes,old-if-new is denoted bySS' .

- Solve-implementation
- Implementation of
`solve`.