Clever implementation.  Lends itself well to complete regression testing / provability.

On first inspection, I'm not convinced that the reduced form is correct.  By definition, doesn't c31 depend on a30 if b30 = 1?

Looking at it another way, the third term of c31 will be zero in all but 2 out of 2^32 cases for all possible values of b and in all cases if a0 = 0.