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

Currently the most thorough example of such a proof can be found in the
book

- 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

An alternative to GL that uses rewriting has been developed. It involves
using 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 arenatp s. 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.