Fix the issue mentioned at #24 (comment)

about allowing fixed abstract cells with the same value to be mapped to
the same concrete cell.

Signed-off-by: Daira-Emma Hopwood <[email protected]>

src/optimizations.md

@@ -51,6 +51,8 @@ $$
 $$
 
 > 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. Notice that specifying $\equiv$ as an equivalence relation helps to simplify this definition (as compared to specifying it as a set of copy constraints), because an equivalence relation is by definition symmetric, reflexive, and transitive.
+>
+> Recall from the [relation definition](relation.md#copy-constraints) that fixed abstract cells with the same value are considered to be equivalent under $\equiv$. This allows a fixed column to be specified as a rotation of another fixed column, which can be useful to reduce the number of fixed concrete columns used by the concrete circuit.
 
 Since correctness does not depend on the specific hints provided by the circuit programmer, it is also valid to use any subset of the provided hints, or to infer hints that were not provided.
 

src/relation.md

@@ -95,6 +95,8 @@ Copy constraints enforce that entries in the witness matrix are equal to each ot
 | $((i,j),k) \in S \Rightarrow w[i, j] = \phi[k]$ | The $(i,j)$ th advice entry is equal to the $k$ th instance entry for all $((i,j),k) \in S$. |
 | $(i,j) \equiv (k,\ell) \Rightarrow w[i, j] = w[k, \ell]$ | $\equiv$ is an equivalence relation indicating which witness entries are constrained to be equal. |
 
+By convention, when fixed abstract cells have the same value, we consider them to be equivalent under $\equiv$. That is, $i < m_f \;\wedge\; k < m_f \;\wedge\; f[i, j] = f[k, \ell] \Rightarrow (i, j) \equiv (k, \ell)$. This has no direct effect on the relation, but it will simplify expressing an [optimization](optimizations.md).
+
 #### Custom constraints
 
 Plonkish also allows custom constraints between the witness matrix entries. In the abstract model we are defining, a custom constraint applies only within a single row of the witness matrix, for the rows that are selected for that constraint.