The double_minimum example from #932 tests that the invariant infrastructure can handle an abstract subcircuit by assuming that it exists and matches a certain specification, then proving that if those assumptions hold the double_minimum circuit is correct. However, I think it's also important to test that the infrastructure can nicely handle actually instantiating those proofs with concrete subcircuits, which is what this PR adds.
The
double_minimumexample from #932 tests that the invariant infrastructure can handle an abstract subcircuit by assuming that it exists and matches a certain specification, then proving that if those assumptions hold thedouble_minimumcircuit is correct. However, I think it's also important to test that the infrastructure can nicely handle actually instantiating those proofs with concrete subcircuits, which is what this PR adds.