wip short-circuiting proof composition

[L-as]

Doesn't compile, unfinished.

The idea is to make an abstraction over "statements", such that they are either done by a recursive proof verification or by doing some minor logic in-circuit.

For the action state extension statement, it would be short-circuiting if source and target are only N actions from each other (for e.g. N = 8), but more than that could use a recursive proof (and reusing the portion of the circuit to verify the last N ones).

Then, we can define short-circuiting proof composition, currently called WrapTwo dumbly, such that if either of the two wrapped statements can be short-circuited, then we avoid an extra proof.

This is very useful for reducing proofs to deal with the 2 recursive proof verifications per circuit limit, since you can stack WrapTwos on top of WrapTwos, and only proving when necessary, short-circuiting the rest.

Closes #162

[L-as]

I've currently unprioritized this since it's non-trivial and hard to audit.