Automating type inference from circuit simulations

_From [rage...@gmail.com](https://code.google.com/u/102895947197065323718/) on April 04, 2014 10:36:18_

In the following, it is necessary to know that sum/carry are both natp's of a certain limit when trying to use the lemmas that describe the phase-3-outs. But in a dream world, the type information could be inferred since they are outputs of phase-2.

(b\* (
(phase-2-outs (stv-run (an-stv) phase-2-ins))
(sum (cdr (assoc 'sum phase-2-outs)))
(carry (cdr (assoc 'carry phase-2-outs)))
(phase-3-ins `((sum . ,sum)
(carry . ,carry)))
(phase-3-outs (stv-run (an-stv) phase-3-ins))
)
...)

Sol's comments:
The main problem is that you have to show (for each output) that all of its bits are Boolean-valued, as opposed to X or Z. You probably need to do a GL proof for this, and if you're going to do that anyway, you might as well prove the bounds at the same time -- it shouldn't be any harder.

In an ideal world you might be able to prove by the syntax of the 4v-sexprs of the STV that they're all Boolean-valued, and then show that since there are a certain number of bits for each output, the 4v-list-to-int (or I forget the exact function name) is a bounded natp. But that's probably harder than the GL

Anna's comment:
The easiest way is to include types in the theorems that use phase-2.
For instance, from your code it is not clear whether sum and carry are not nils.

Rager's responses:
I've got a workaround for the set of typing lemmas I'll need to repeat many times over, but this seems like it could be a nice feature to have in the long-term.

It looks like the functions Sol was referring to are 4v-to-nat and 4v-alist-to-param. I've got some hair-brained idea that involves having a version of defthm that looked for calls of stv-run, opened them up selectively, added some :forward-chaining facts that it can derive from reasoning about stv-run, 4v-to-nat, 4v-alist-to-param and other relevant functions, then proceeding with the original proof. This would probably always be on, so it might slow things down too much. Maybe Sol's thoughts were simpler.

If I end up with 100+ brittle typing GL thms that are a pain to maintain, I might look into this further. Fun fact: one of the typing thm's takes 70 seconds to prove, but when I use a hint that rewrites the complicated STV to the simpler one (about which I have a typing lemma that proves in a couple seconds), proving the obligation is trivial (in time).

_Original issue: http://code.google.com/p/acl2-books/issues/detail?id=170_