(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:
(b* ( ;; Run the first part of the circuit to get the partial products
(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-out-alist (sv::svtv-run (boothmul-direct) orig-in-alist)))
;; 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)
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
This re-composition is usually best done at the top level, so the meta rules
trigger on any of the following:
The env terms in the above may take the following forms, where
env1, env2 are recursively matched:
- (Deprecated) Hint used for svex hardware model recomposition proofs -- see svex-decomp.