Merge protocol soundness

[ledwards2225]

In each GUH proof, we do a "zero check" on the op queue transcript polynomials T_i. In turns out that we also need to do a similar check on the aggregate op queue transcript A_i at each stage for the protocol to be sound. Basically the issue is that the verifier doesn't know that when constructing A_{i+1} = A_i || T_i, the A_i does not have non-zero entries in the region overlapping where T_i has non-zero entries.

I originally thought that this was handled inductively a la: since A_0 == T_0 and we do a zero check on T_0, A_0 is handled. Then we do a zero check on T_1 and A_1 = A_0 || T_0, so A_1 is handled and so on. This doesn't work though because the verifier only has access to A_n, T_n and thus can't argue inductively from T_0. I also thought that since the proper aggregation was proved by deciding the final instance + ECCVM etc, that this would be sufficient for the soundness of the merge. But this becomes circular because the merge has to have been sound for the rest of the protocol to be sound. (I'm speaking pretty imprecisely here but hopefully this summarizes the point sufficiently).

One option proposed by Zac is to simply add a zero check for A_i into the main protocol, similar to what we do for T_i. This has the disadvantage of forcing circuits in the IVC to be at least as large as A_i but in practice even the full op queue is fairly short so while icky, perhaps this isn't a problem.