		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Symbolic-test-vector-composition

Strategy for performing compositional proofs involving stv's

It is common to use gl to perform proofs about small and moderately-sized circuits. However, performing proofs about large circuits typically involves first breaking the circuit into smaller parts, and then showing that the sum of the parts is equivalent to the original whole circuit. We call this proof a compositional equivalence proof.

Currently the most thorough example of such a proof can be found in the book centaur/esim/tutorial/boothmul.lisp. This example highlights two ways of performing a compositional equivalence proof:

By using gl
By using rewriting

The advantage of using gl is that it is automatic. The disadvantage is that once one is working on very large circuits, the underlying BDDs or SAT solvers are unlikely to complete. This is because the compositional proof relies upon the fact that every relevant intermediate value should be a natp (as opposed to X. This turns out to be a very time-consuming proof obligation!

An alternative to GL that uses rewriting has been developed. It involves using book centaur/esim/stv/stv-decomp-proofs. We recommend looking at the boothmul example mentioned above but offer additional points of clarification for anyone striving to use this book:

You will need to enable the stv-decomp-theory. Thus, the user's hints for the composition proof will look something like:
```
:use ((:instance phase-1-types)
      (:instance phase-2-types))
:in-theory (stv-decomp-theory)
```
At one point the book only worked when the stv's used their autoins macro (see defstv) for finding the inputs. We think this is no longer the case, but it is something to keep in mind when debugging the failures of your proofs.

The user absolutely must prove and :use a lemma that says the relevant intermediate values are natps. If the user fails to do this, they will likely get an error message that looks like the following. Note that the user can still obtain a "not equivalent" error for other reasons, which must be debugged by the user.

HARD ACL2 ERROR in STV-DECOMP-4V-ENV-EQUIV-META:  Not equivalent

A-alist:
((WIRENAME[0] CAR (IF (EQUAL (4V-TO-NAT #) 'X) '(X X X X X ...) (IF (IF # #
#) (BOOL-TO-4V-LST #) '#))) (WIRENAME[10] CAR (CDR (CDR (CDR
#)))) (WIRENAME[11] CAR (CDR (CDR (CDR #)))) (WIRENAME[12] CAR (CDR (CDR (CDR
#)))) (WIRENAME[13] CAR (CDR (CDR (CDR #)))) ...)
B-alist:
((WIRENAME[0] BOOL-TO-4V (LOGBITP '0 WIRENAME)) (WIRENAME[10] BOOL-TO-4V
(LOGBITP '10 WIRENAME)) (WIRENAME[11] BOOL-TO-4V (LOGBITP '11 WIRENAME))
(WIRENAME[12] BOOL-TO-4V (LOGBITP '12 WIRENAME)) (WIRENAME[13] BOOL-TO-4V
(LOGBITP '13 WIRENAME)) ...)

The stv-decomp-proofs book is experimental and not as robust as many of the other features provided in the ACL2 books. Please send inquiries to the acl2-books project.