Let's let the OP try to write up the logic formula for SHA256's first 32 bits of input and 1 bit of output.
Thanks for the links.
I rewrote the code so that it performs the double SHA256 first, constructing an in-memory tree of all the operations and variables (without actually evaluating them, arithmetically or symbolically.) So basically for each bit in the final hash, I have a tree representing all the operations that have to occur (using an in-order walk) to compute that bit.
...
If everything looks good, the longer term plan is to assign branch simplification to different datacenter machines, so that I can have a few thousand of them simplifying in parallel instead of 8 on my desktop.
Fun! This work could be published in crypto journals, you know. Even if you find that a (SHA-256)^2 function can be implemented with depth=2 and width=1,000,000,000 - it would be useful work that could be built upon. And you code to do this could be modified to examine SHA-3, whirlpool, and other hash functions.
For the record - (SHA-256)^2 has 64+64=128 rounds with 6 32-bit additions per round.