Updates from the June 14 meeting.

* State that we intend to use terminology consistent with the Community
  Reference.
* Fix some inconsistencies that were introduced by Daira-Emma in the
  June 7 changes.
* Rename $\mathsf{instance}$ to $x$.
* Define "abstract cell" and "concrete cell" in the optimizations doc, and
  make sure its use of terminology is consistent with the relation doc.
* Other minor wording tweaks.

Co-authored-by: Mary Maller <[email protected]>
Co-authored-by: Jack Grigg <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>

src/optimizations.md

@@ -2,19 +2,21 @@
 
 ## Background
 
-The relation described in [Specification of the Plonkish Relation](relation.md) gives an abstract model of a Plonkish constraint system that is sufficiently expressive, but does not take into account some of the optimizations that are commonly used in Plonkish implementations, such as the use of offsets/rotations in Plonkish custom gates. The tradeoff here is that the abstract model allows rows to be arbitrarily reordered.
+The relation described in [Specification of the Plonkish Relation](relation.md) gives an abstract model of a Plonkish constraint system that is sufficiently expressive, but does not take into account some of the optimizations that are commonly used in Plonkish implementations, such as the use of offsets/rotations in Plonkish custom gates. The trade-off here is that the abstract model allows rows to be arbitrarily reordered.
 
 > It would have been possible to directly include offsets in the constraint system model, but the most obvious ways of doing this would require the circuit programmer to think about copy constraints that don't naturally arise from the intended circuit definition.
 >
-> By separating the abstract constraint system from the concrete circuit, the programmer can instead locally add only the copy constraints that they know are needed. They are not forced to add artificial copy constraints corresponding to offsets. Although we still use numbered rows for convenience in the model, it would be sufficient to use any set with $n$ unique, not necessarily ordered elements. The abstract $\rightarrow$ concrete compilation can then reorder the rows as needed without changing the meaning of the circuit. This allows layout optimizations that would be impractical or error-prone to do manually, because they rely on global rather than local knowledge (such as which neighbouring cells are used or free, which can depend on gates that are logically unrelated).
+> By separating the abstract constraint system from the concrete circuit, the programmer can instead locally add only the copy constraints that they know are needed. They are not forced to add artificial copy constraints corresponding to offsets. Although we still number the rows of the abstract witness matrix for convenience in the model, it would be sufficient to use any set with $n$ unique, not necessarily ordered elements. The abstract $\rightarrow$ concrete compilation can then reorder the rows as needed without changing the meaning of the circuit. This allows layout optimizations that would be impractical or error-prone to do manually, because they rely on global rather than local knowledge (such as which neighbouring cells are used or free, which can depend on gates that are logically unrelated).
 
 ## Compiling to a concrete circuit
 
 TODO: define variables consistent with [the relation description](relation.md).
 
 Below we will use the convention that variables marked with a prime ($'$) refer to *concrete* column or row indices.
 
-We say that a cell with coordinates $(i, j)$ is ``constrained'' if it is in a fixed column or if it appears in some copy, custom, or lookup constraint. More precisely, $\mathsf{constrained}(i, j)$ is true iff any of the following hold:
+An "abstract cell" or "concrete cell" specifies an entry in the witness matrix of the abstract circuit or concrete circuit, respectively.
+
+We say that an abstract cell with coordinates $(i, j)$ is ``constrained'' if it is in a fixed column or if it appears in some copy, custom, or lookup constraint. More precisely, $\mathsf{constrained}(i, j)$ is true iff any of the following hold:
 $$
 \begin{array}{rcl}
 && i < m_f \\
@@ -38,7 +40,7 @@ $w$ represents $m$ _abstract_ columns, that do not directly correspond 1:1 to ac
 
 Offsets are represented by hints $\{ (h_i, e_i) \mathrel{⦂} [0,m') \times \mathbb{Z} \}_i$ where $m'$ is the number of concrete columns. To simplify the programming model, the hints are not supposed to affect the meaning of a circuit (i.e. the set of public inputs for which it is satisfiable, and the knowledge required to find a witness).
 
-Tesselation between custom constraints is just represented by equivalence under $\equiv$. When the offset hints indicate that two cells in the same concrete column are equivalent, the backend can optimise overall circuit area by reordering the rows so that the equivalent cells overlap.
+Tesselation between custom constraints is just represented by equivalence under $\equiv$. When the offset hints indicate that two concrete cells in the same column are equivalent, the backend can optimise overall circuit area by reordering the rows so that the equivalent cells overlap.
 
 More specifically, to compile the abstract circuit to a concrete circuit using the hints $\{ (h_i, e_i) \}_i$, we construct an injective mapping of abstract row numbers to concrete row numbers before applying offsets, $\mathbf{r} : [0, n) \mapsto [0, n')$ with $n' \geq n$, such that the abstract cell with coordinates $(i, j)$ maps to the concrete cell with coordinates $(h_i, \mathbf{r}(j) + e_i)$, and all *constrained* abstract cells map to concrete cell coordinates that are in range.
 
@@ -52,19 +54,19 @@ $$
 
 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.
 
-The constrained abstract advice cells $w : \mathbb{F}^{m \times n}$ are translated to concrete advice cells $w' : \mathbb{F}^{m' \times n'}$:
+The constrained abstract cells $w : \mathbb{F}^{m \times n}$ are translated to concrete cells $w' : \mathbb{F}^{m' \times n'}$:
 $$
 \mathsf{constrained}(i, j) \Rightarrow w'[h_i, \mathbf{r}(j) + e_i] = w[i, j]
 $$
 
 The values of concrete cells not corresponding to any constrained abstract cell are arbitrary.
 
-The abstract fixed cells $f : \mathbb{F}^{m_f \times n}$ are similarly translated to concrete fixed cells $f' : \mathbb{F}^{m_f \times n'}$:
+The fixed abstract cells $f : \mathbb{F}^{m_f \times n}$ are similarly translated to fixed concrete cells $f' : \mathbb{F}^{m_f \times n'}$:
 $$
 f'[h_i, \mathbf{r}(j) + e_i] = f[i, j]
 $$
 
-Concrete fixed cells not assigned values by this mapping are filled with zeros.
+Fixed concrete cells not assigned values by this mapping are filled with zeros.
 
 The abstract coordinates appearing in $\equiv$ and $S$ are similarly mapped to their concrete coordinates.
 
@@ -106,4 +108,4 @@ This algorithm can be proven correct by induction on $n$. It is complete because
 $$
 \mathsf{constrained}(i, j) \;\wedge\; \mathsf{constrained}(k, \ell) \;\wedge\; (i, j) \not\equiv (k, \ell) \Rightarrow (h_i, \mathbf{r}(j) + e_i) \neq (h_k, \mathbf{r}(\ell) + e_k)
 $$
-for $j = g$ or $\ell = g$ are met, because $\mathbf{r}(g) = u$ and both $(h_i, \mathbf{r}(j) + e_i)$ and $(h_k, \mathbf{r}(\ell) + e_k)$ can be made not to overlap with any previously constrained cell.
+for $j = g$ or $\ell = g$ are met, because $\mathbf{r}(g) = u$ and both $(h_i, \mathbf{r}(j) + e_i)$ and $(h_k, \mathbf{r}(\ell) + e_k)$ can be made not to overlap with any concrete cell that became constrained in a previous iteration.

src/relation.md

@@ -10,16 +10,21 @@ This is intended to be read in conjunction with the [Plonkish Backend Optimizati
 
 Plonkish arithmetisation depends on a scalar field over a prime modulus $p$. We represent this field as the object $\mathbb{F}$. We denote the additive identity by $0$ and the multiplicative identity by $1$. Integers, taken modulo the field modulus $p$, are called scalars; arithmetic operations on scalars are implicitly performed modulo $p$. We denote the sum, difference, and product of two scalars using the $+$, $-$, and $*$ operators, respectively.
 
-The notation $a \text{..} b$ means the sequence of integers from $a$ (inclusive) to $b$ (exclusive) in ascending order. $[a, b)$ means the corresponding set of integers. $[f(x) : x \leftarrow a \text{..} b]$ means the sequence of evaluations of $f$ on $a \text{..} b$.
+The notation $a \text{..} b$ means the sequence of integers from $a$ (inclusive) to $b$ (exclusive) in ascending order. $[a, b)$ means the corresponding set of integers. $[f(e) : e \leftarrow a \text{..} b]$ means the sequence of evaluations of $f$ on $a \text{..} b$.
+
+The terminology used here is intended to be consistent with the [ZKProof Community Reference](https://docs.zkproof.org/reference). We diverge from this terminology as follows:
+* We refer to the public inputs to the circuit as an "instance vector". The entries of this vector are called "instance variables" in the Community Reference.
 
 ## The Plonkish Relation $\mathcal{R}_{\mathsf{plonkish}}$
 
-The relation $\mathcal{R}_{\mathsf{plonkish}}$ contains pairs of instances $\mathsf{instance}$, and witnesses $w$.
+The relation $\mathcal{R}_{\mathsf{plonkish}}$ contains pairs of $(x, w)$ where:
+* the instance $x$ consists of the parameters of the proof system, the circuit, and the public inputs to the circuit (i.e. the instance vector).
+* the witness $w$ consists of the matrix of values provided by the prover. In this model it consists of the (potentially private) prover inputs to the circuit, and any intermediate values (including fixed values) that are not inputs to the circuit but are required in order to satisfy it.
 
-We say that $\mathsf{instance}$ is a valid instance whenever there exists some advice $w$ such that $(\mathsf{instance}, w) \in \mathcal{R}_{\mathsf{plonkish}}.$
+We say that a $x$ is a *valid* instance whenever there exists some witness $w$ such that $(x, w) \in \mathcal{R}_{\mathsf{plonkish}}$ holds.
 The Plonkish language $\mathcal{L}_{\mathsf{plonkish}}$ contains all valid instances.
 
-If the proof system is knowledge sound, then the prover must have knowledge of the witness in order to construct a valid proof. In the setting of a zero-knowledge proof system, the witness is private and the proof leaks no additional information about it.
+If the proof system is knowledge sound, then the prover must have knowledge of the witness in order to construct a valid proof. If it is also zero knowledge, then witness entries can be private, and an honestly generated proof leaks no information about the private inputs to the circuit beyond the fact that it was obtained with knowledge of some satisfying witness.
 
 ### Instances
 
@@ -28,12 +33,12 @@ The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes instances of the following
 | Instance element  | Description |
 | ----------------- | -------- |
 | $\mathbb{F}$      | A prime field. |
-| $t$               | Number of instance entries. |
-| $\phi$            | Instance entries $\phi \mathrel{⦂} \mathbb{F}^t$. |
+| $t$               | Length of the instance vector. |
+| $\phi$            | The instance vector $\phi \mathrel{⦂} \mathbb{F}^t$. |
 | $n > 0$           | Number of rows. |
 | $m$               | Number of columns. |
-| $\equiv$          | An equivalence relation on $[0,m) \times [0,n)$ indicating which advice entries are equal. |
-| $S$               | A set $S \subseteq ([0,m) \times [0,n)) \times [0,t)$ indicating which instance entries must be used in the advice. |
+| $\equiv$          | An equivalence relation on $[0,m) \times [0,n)$ indicating which witness entries are equal to each other. |
+| $S$               | A set $S \subseteq ([0,m) \times [0,n)) \times [0,t)$ indicating which witness entries are equal to instance vector entries. |
 | $m_f \leq m$      | Number of columns that are fixed. |
 | $f$               | The fixed content of the first $m_f$ columns, $f \mathrel{⦂} \mathbb{F}^{m_f \times n}$. |
 | $\mathsf{CUS}_u$  | Sets $\mathsf{CUS}_u \subseteq [0,n)$ indicating which rows the custom functions $p_u \mathrel{⦂} \mathbb{F}^{m} \mapsto \mathbb{F}$ are applied to. |
@@ -43,15 +48,13 @@ The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes instances of the following
 | $q_{v,s}$         | Custom scaling functions $q_{v,s} \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$ for $s \leftarrow 0 \text{..} L_v$. |
 | $\mathsf{TAB}_v$  | Lookup tables $\mathsf{TAB}_v \subseteq \mathbb{F}^{L_v}$, each with a number of tuples in $\mathbb{F}^{L_v}$. |
 
-> TODO: do we need to generalise lookup tables to support dynamic tables (in advice columns)? Probably too early, but we could think about it.
-
 ### Witnesses
 
-The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes a witness of the following form:
+The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes witnesses of the following form:
 
-| Witness           | Description |
+| Witness element   | Description |
 | ----------------- | -------- |
-| $w$               | Columns $w \mathrel{⦂} \mathbb{F}^{m \times n}$. |
+| $w$               | The witness matrix $w \mathrel{⦂} \mathbb{F}^{m \times n}$. |
 
 Define $\vec{w}_j$ as the row vector $[w[i, j] : i \leftarrow 0 \text{..} m]$.
 
@@ -62,7 +65,7 @@ Given the above definitions, the relation $\mathcal{R}_{\mathsf{plonkish}}$ is g
 $$
 \left\{ \begin{array}{cc | c}
    (\mathbb{F}, t, \phi, n, m, \equiv, S, m_f, f, \{\mathsf{CUS}_{u}, p_u\}_u, \{ L_v, \mathsf{LOOK}_v, \{ q_{v,s} \}_s, \mathsf{TAB}_v \}), & & - \\
-   f \mathrel{⦂} \mathbb{F}^{m_f \times n}, \ w \mathrel{⦂} \mathbb{F}^{m \times n} & & i \in [0,m_f), \ j \in [0,n) \Rightarrow w[i, j] = f[i, j] \\
+   w \mathrel{⦂} \mathbb{F}^{m \times n}, \ f \mathrel{⦂} \mathbb{F}^{m_f \times n} & & i \in [0,m_f), \ j \in [0,n) \Rightarrow w[i, j] = f[i, j] \\
    S \subseteq ([0,m) \times [0,n)) \times [0,t), \ \phi \mathrel{⦂} \mathbb{F}^t & & ((i,j),k) \in S \Rightarrow w[i, j] = \phi[k] \\
    \equiv\; \subseteq ([0,m) \times [0,n)) \times ([0,m) \times [0,n)) & & (i,j) \equiv (k,\ell) \Rightarrow w[i, j] = w[k, \ell] \\
    \mathsf{CUS}_u \subseteq [0,n), \ p_u \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F} & & j \in \mathsf{CUS}_u \Rightarrow p_u(\vec{w}_j) = 0 \\
@@ -72,7 +75,7 @@ $$
 
 ### Conditions satisfied by statements in $\mathcal{R}_{\mathsf{plonkish}}$
 
-There are four types of constraints that a Plonkish statement $(\mathsf{instance}, w) \in \mathcal{R}_{\mathsf{Plonkish}}$ must satisfy:
+There are four types of constraints that a Plonkish statement $(x, w) \in \mathcal{R}_{\mathsf{Plonkish}}$ must satisfy:
 
 * Fixed constraints
 * Copy constraints
@@ -85,16 +88,18 @@ The first $m_f$ columns of $w$ are fixed to the columns of $f$.
 
 #### Copy constraints
 
-Copy constraints that enforce that advice entries must be equal to other inputs.  Plonkish allows custom constraints between the instance, fixed, and advice constraint entries.
+Copy constraints enforce that entries in the witness matrix are equal to each other, or that an instance entry is equal to a witness entry.
 
 | Copy Constraints  | Description |
 | ----------------- | -------- |
 | $((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 advice entries are constrained to be equal. |
+| $(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. |
 
 #### Custom constraints
 
-Custom constraints that enforce that fixed entries and advice entries satisfy some multivariate polynomial. Here $p_u$ could indicate a multiplication gate, an addition gate, or any other custom case that can be generated using a combination of multiplication gates and addition gates.
+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.
+
+Custom constraints enforce that witness entries within a row satisfy some multivariate polynomial. Here $p_u$ could indicate any case that can be generated using a combination of multiplication gates and addition gates.
 
 | Custom Constraints | Description |
 | -------- | -------- | 
@@ -107,14 +112,16 @@ Here $p_u \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$ is an arbitrary [multiv
 
 #### Lookup constraints
 
-Lookup constraints enforce that advice entries are contained in some table.
+Lookup constraints enforce that some polynomial function of the witness entries on a row are contained in some table.
 
 The sizes of tables are not limited at this layer. A realization of a proving system using Plonkish arithmetization may limit the supported size of tables, possibly depending on $n$, or it may have some way to compile larger tables.
 
-Fixed lookup tables are determined in advance. Dynamic lookup tables would be determined by the advice, but are not supported in this version.
+In this specification, we only support fixed lookup tables determined in advance. This could be generalized to support dynamic tables determined by part of the witness matrix.
+
+Fixed lookup tables are determined in advance. Dynamic lookup tables would be determined by part of the witness matrix, but are not supported in this version.
 
 | Lookup Constraints | Description |
 | -------- | -------- |
 | $j \in \mathsf{LOOK}_v \Rightarrow [q_{v,s}(\vec{w}_j) : s \leftarrow 0 \text{..} L_v] \in \mathsf{TAB}_v$ | $v$ is the index of a lookup table. $j$ ranges over the set of rows $\mathsf{LOOK}_v$ for which the lookup constraint is switched on. |
 
-Here $q_{v,s} \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$ for $s \leftarrow 0 \text{..} L_v$ are multivariate polynomials that collectively map the fixed and advice cells $\vec{w}_j$ on the lookup row $j \in \mathsf{LOOK}_v$ to a tuple of field elements. This tuple will be constrained to match some row of the table $\mathsf{TAB}_v$.
+Here $q_{v,s} \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$ for $s \leftarrow 0 \text{..} L_v$ are multivariate polynomials that collectively map the witness entries $\vec{w}_j$ on the lookup row $j \in \mathsf{LOOK}_v$ to a tuple of field elements. This tuple will be constrained to match some row of the table $\mathsf{TAB}_v$.