		Search-engine friendly clone of the ACL2 documentation.

Svex-decomp

(Deprecated) Proving that a decomposition is equivalent to some whole.

Here is an example, from "svex/tutorial/boothpipe.lisp", showing how to use svdecomp-hints to prove a decomposition theorem:

(defthm boothmul-decomp-is-boothmul
  (implies (boothmul-direct-autohyps)
           (b* ( ;; Run the first part of the circuit to get the partial products
                (in-alist1  (boothmul-step1-autoins))
                (out-alist1 (sv::svtv-run (boothmul-step1) in-alist1))

                ;; Get the results from the output and stick them into an
                ;; input alist for step2.  Some control signals from the
                ;; original input alist also are needed.
                (in-alist2 (boothmul-step2-alist-autoins (append out-alist1 in-alist1)))

                ;; Run the second part of the circuit on the results from the
                ;; first part, summing the partial products.
                (out-alist2 (sv::svtv-run (boothmul-step2) in-alist2))

                ;; Separately, run the original circuit.
                (orig-in-alist  (boothmul-direct-autoins))
                (orig-out-alist (sv::svtv-run (boothmul-direct) orig-in-alist)))

             (equal
              ;; The final answer from running the decomposed circuit the second
              ;; time, after feeding its partial products back into itself.
              (cdr (assoc 'o out-alist2))

              ;; The answer from running the original circuit.
              (cdr (assoc 'o orig-out-alist)))))
  :hints((sv::svdecomp-hints :hyp (boothmul-direct-autohyps)
                               :g-bindings (boothmul-direct-autobinds))))

The svdecomp-hints first gives a theory hint that allows ACL2 to efficiently open the svtv-run calls and process the goal into a form on which some special-purpose meta rules can operate. When this is done it enters a theory containing only those meta rules. The meta rules find svex decompositions and re-compose them together so that, if all goes well, you're left with the equivalence of two evaluations of svex expressions. In the best case, those svex expressions are equal, in which case the proof finishes there. However, often there are syntactic differences between the expressions. Then, we call GL to prove the two evaluations equivalent. To do this, we need a type hypothesis and symbolic bindings for the variables. These are provided by the :hyp and :g-bindings argument to svdecomp-hints.

Additional optional arguments:

:enable simply adds a list of rules to the theory used in the first step, before the meta rules are used. This is useful because the conclusion of the theorem must be in a particular form, described below, for the meta rules to work. If the statement of the theorem uses special-purpose functions to (say) construct alists or compare outputs, the theory may need to be augmented with rules to rewrite these functions away so that the meta rule can work.
:rewrite-limit sets the limit on the number of passes of rewriting to do on the resulting svex expressions. In some cases it might be useful to set this to 0, to disable rewriting. Using this keyword argument actually sets the state global variable sv::svdecomp-rewrite-limit, which sets the limit for future calls as well.

What can the meta rules handle?

The core algorithm of the meta rule operates on a call of svex-eval, svexlist-eval, or svex-alist-eval in which some of the values bound to variables in the environment are also calls of svex-eval. If its operation is successful, it results in an evaluation with an environment that does not bind any calls of svex-eval. It does this by basically applying the following rule, svex-eval-of-svex-compose, in reverse:

(equal (svex-eval (svex-compose x a) env)
       (svex-eval x (append (svex-alist-eval a env) env)))

The meta rule supposes that the top-level evaluation is equivalent to the RHS of the above rule for some term env and quoted value a, and tries to determine env and a for which this is the case. This would be relatively easy if the RHS was in a form that matched the above, but in practice the svex-alist-eval term is represented instead as several explicit cons pairs with svex-eval cdrs, the ordering among the keys is inconsistent, and in some places a subset of env is used in place of the whole thing.

This re-composition is usually best done at the top level, so the meta rules trigger on any of the following:

(equal (svex-eval (quote sv1) env1) (svex-eval (quote sv2) env2))

(equal (svexlist-eval (quote sv1) env1) (svexlist-eval (quote sv2) env2))

(equal (svex-alist-eval (quote sv1) env1) (svex-alist-eval (quote sv2) env2))

The env terms in the above may take the following forms, where env1, env2 are recursively matched:

```
(quote val)
```
```
(cons (cons (quote var) val) env1)
```
```
(cons (quote (var . val)) env1)
```
```
(binary-append env1 env2)
```
```
(svex-alist-eval (quote svalist) e)
```

Subtopics

Decomp.lisp
Svdecomp-hints: (Deprecated) Hint used for svex hardware model recomposition proofs -- see svex-decomp.