Review optimization doc

[daira]

Questions for the review of this doc:

• Is it sufficiently clear?
• Is the definition of compilation correctness sufficient, i.e. it accurately preserves soundness and completeness?
• Does the model permit the optimizations we wanted to permit?
• Is the "Greedy algorithm for choosing $\mathbf{r}$" correct?

Re: compilation correctness, I wrote at #24 (comment) :

It is alright if one or more unconstrained abstract cells map to the same concrete cell as a constrained abstract cell, because that will not affect the meaning of the circuit.

I tend to think [this] needs either a proof or more detailed intuition as to why it is true. Specifically, it depends on the following:

• An unconstrained abstract cell is fully unconstrained (which is necessary for completeness of the translated circuit wrt the original). Note that this relies on some details of the definition of "constrained" — for example considering cells in fixed columns to be constrained, and $\equiv$ being transitive.
• An abstract cell with coordinates $(i, j)$ maps to only one concrete cell $(h_i, \mathbf{r}(j) + e_i)$.

Therefore the effect is that if both one constrained abstract cell and several unconstrained abstract cells map to the same concrete cell, you can think of it as assigning these unconstrained abstract cells the same value when you do the correctness proof. And the point is that this is harmless: it affects neither completeness nor knowledge soundness (and zero knowledge doesn't depend on the abstract-concrete mapping at all).