Updates to the relation from 2024-04-19 meeting.

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

src/relation.md

@@ -8,29 +8,17 @@ This is intended to be read in conjunction with the [Plonkish Backend Optimizati
 
 ## Dependencies
 
-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.
+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 Plonkish Relation
-The relation $\mathcal{R}_{\mathsf{plonkish}}$ contains pairs of public instances $\mathsf{instance}$ and private advice $w$.  We say that $\mathsf{instance}$ is a valid instance whenever their exists some advice $w$ such that $(\mathsf{instance}, w) \in \mathcal{R}_{\mathsf{plonkish}}$.  The Plonkish language $\mathcal{L}_{\mathsf{plonkish}}$ contains all valid instances.
+The relation $\mathcal{R}_{\mathsf{plonkish}}$ contains pairs of public instances $\mathsf{instance}$ and private advice $w$.
+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}}.$
+The Plonkish language $\mathcal{L}_{\mathsf{plonkish}}$ contains all valid instances.
 
-$$
-\mathcal{R}_{\mathsf{plonkish}} =
-\left\{ \begin{array}{cc | c}
-   (\mathbb{F}, (f, \phi), \equiv_A, S_I, \{\mathsf{CUS}_{u}, p_u\}_u, \{ \mathsf{LOOK}_v, \mathsf{TAB}_v, q_v \}), & & - \\
-   f \in \mathbb{F}^{m_F \times n}, w \in \mathbb{F}^{m_A \times n}, \phi \in \mathbb{F}^{t_I} & & - \\
-   S_I \subset ([0,m_A) \times [0,n)) \times [0,t_I) & & ((i,j),k) \in S_I \Rightarrow w[i, j] = \phi[k] \\
-   S_F \subset ([0,m_A) \times [0,n)) \times ([0,m_F) \times [0,n)) & & ((i,j),(k,\ell)) \in S_F \Rightarrow w[i, j] = f[k, \ell] \\
-   \equiv_A \subset ([0,m_A) \times [0,n)) \times ([0,m_A) \times [0,n)) & & (i,j) \equiv_A (k,\ell) \Rightarrow w[i, j] = w[k, \ell] \\
-   \forall u, \ \mathsf{CUS}_u \subset [0,n), \ p_u: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F} & & j \in \mathsf{CUS}_u \Rightarrow p_u( f[0, j], \ldots, f[m_F-1, j], w[0, j], \ldots, w[m_A-1,j] ) = 0\hspace{1.15em} \\
-   \mathsf{LOOK}_v \subset [0,n), \mathsf{TAB}_v \subset \mathbb{F}^{m_{Q,v}} & & j \in \mathsf{LOOK}_v \Rightarrow q_v(f[0, j], \ldots, f[m_F-1, j], w[0, j], \ldots, w[m_A-1, j] ) \in \mathsf{TAB}_k \\
-\end{array} \right\}
-$$
-
-The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes as public inputs the instances
+The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes, as public inputs, instances of the form
 $$
 \mathsf{instance} = (\mathbb{F}, \phi, f, \equiv_A, S_I, \{ \mathsf{CUS}_{u}, p_u \}_u, \{ \mathsf{LOOK}_v, \mathsf{TAB}_v \}_v)
 $$
-of the following form.
 
 ### Inputs into $\mathcal{R}_{\mathsf{plonkish}}$
 
@@ -48,17 +36,33 @@ of the following form.
 | $\equiv_A$        | An equivalence relation on $[0,m_A) \times [0,n)$ indicating which advice entries are equal. |
 | $\mathsf{CUS}_u$  | Sets $\mathsf{CUS}_u \subseteq [0,n)$ indicating which rows the custom functions $p_u: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}$ are applied to. |
 | $p_u$             | Custom multivariate polynomials $p_u: \mathbb{F}^{m_F + m_A}  \mapsto \mathbb{F}$. |
-| $m_{Q,v}$         | The width of lookup table $\mathsf{TAB}_v$. |
+| $L_v$             | Number of table columns in each lookup table $\mathsf{TAB}_v$. |
 | $\mathsf{LOOK}_v$ | Sets $\mathsf{LOOK}_v \subseteq [0,n)$ indicating which rows the scaled lookups $q_v(\text{fixed and advice entries on row } j) \in \mathsf{TAB}_v$ are applied to. |
-| $q_v$             | Custom scaling functions $q_v: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}^{m_{Q,v}}$. |
-| $\mathsf{TAB}_v$  | Lookup tables $\mathsf{TAB}_v \subseteq \mathbb{F}^{m_{Q,v}}$, each with a number of tuples in $\mathbb{F}^{m_{Q,v}}$. |
+| $q_v$             | Custom scaling functions $q_v: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}^{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.
 
 | Private Inputs    | Description |
 | ----------------- | -------- |
 | $w$               | Advice columns $w : \mathbb{F}^{m_A \times n}$. |
 
+Define $\mathsf{ROW}_j$ as the vector $[f[0, j], \ldots, f[m_F-1, j], w[0, j], \ldots, w[m_A-1,j]]$.
+
+Given the above definitions, the relation $\mathcal{R}_{\mathsf{plonkish}}$ is given by:
+
+$$
+\left\{ \begin{array}{cc | c}
+   (\mathbb{F}, (f, \phi), \equiv_A, S_I, \{\mathsf{CUS}_{u}, p_u\}_u, \{ \mathsf{LOOK}_v, \mathsf{TAB}_v, q_v \}), & & - \\
+   f \in \mathbb{F}^{m_F \times n}, w \in \mathbb{F}^{m_A \times n}, \phi \in \mathbb{F}^{t_I} & & - \\
+   S_I \subset ([0,m_A) \times [0,n)) \times [0,t_I) & & ((i,j),k) \in S_I \Rightarrow w[i, j] = \phi[k] \\
+   S_F \subset ([0,m_A) \times [0,n)) \times ([0,m_F) \times [0,n)) & & ((i,j),(k,\ell)) \in S_F \Rightarrow w[i, j] = f[k, \ell] \\
+   \equiv_A \subset ([0,m_A) \times [0,n)) \times ([0,m_A) \times [0,n)) & & (i,j) \equiv_A (k,\ell) \Rightarrow w[i, j] = w[k, \ell] \\
+   \forall u, \ \mathsf{CUS}_u \subset [0,n), \ p_u: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F} & & j \in \mathsf{CUS}_u \Rightarrow p_u(\mathsf{ROW}_j) = 0 \\
+   \mathsf{LOOK}_v \subset [0,n), \mathsf{TAB}_v \subset \mathbb{F}^{L_v} & & j \in \mathsf{LOOK}_v \Rightarrow q_v(\mathsf{ROW}_j) \in \mathsf{TAB}_k
+\end{array} \right\}
+$$
+
 ### Conditions satisfied by statements in $\mathcal{R}_{\mathsf{plonkish}}$
 
 There are three types of constraints that a Plonkish statement $(\mathsf{instance}, w) \in \mathcal{R}_{\mathsf{Plonkish}}$ must satisfy:
@@ -83,25 +87,27 @@ Custom constraints that enforce that fixed entries and advice entries satisfy so
 
 | Custom Constraints | Description |
 | -------- | -------- | 
-| $j \in \mathsf{CUS}_u \Rightarrow p_u( f[0, j], \ldots ,  f[m_F-1, j], w[0, j], \ldots, w[m_A - 1, j] ) = 0$ | $u$ is the index of a custom constraint. $j$ ranges over the set of rows $\mathsf{CUS}_u$ for which the custom constraint is switched on. |
+| $j \in \mathsf{CUS}_u \Rightarrow p_u(\mathsf{ROW}_j) = 0$ | $u$ is the index of a custom constraint. $j$ ranges over the set of rows $\mathsf{CUS}_u$ for which the custom constraint is switched on. |
 
 <!---
 Define the X notation earlier and use it throughout.
 -->
 
-Here $p_u: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}$ is a function such that $$ p_u( X_0, \ldots, X_{m_F + m_A - 1}) = p_{u,0} * X_0 \ \ * / + \ \ p_{u,1} * X_1 \ \ * / + \ \ \cdots \ \ * / + \ \ p_{u,m_F + m_A - 1} X_{m_F + m_A - 1}$$ where $p_{u,i} \in \mathbb{F}$ are scalars and where $p_u$ determines whether to use the multiplication $*$ or addition $+$ operation at each step.
+Here $p_u: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}$ is an arbitrary [multivariate polynomial](https://en.wikipedia.org/wiki/Polynomial_ring#Definition_(multivariate_case)):
+
+> Given $\eta$ symbols $X_1, \dots, X_\eta$ called indeterminates, a multivariate polynomial $p$ in these indeterminates, with coefficients in $\mathbb{F}$,
+> is a finite linear combination $$p(X_1, \dots, X_\eta) = \sum_{i=1}^\nu c_i X_1^{\alpha_{i,1}}\cdots X_\eta^{\alpha_{i,\eta}}$$ where $\nu \in \mathbb{N}$, $c_i$ in $\mathbb{F}$, and $\alpha_{i,j} \in \mathbb{N}$.
 
 #### Lookup constraints
 
 Lookup constraints enforce that advice entries are contained in some table.
 
-Fixed lookup tables are determined in advance, whereas dynamic lookup tables are determined by the advice.
+The sizes of tables are not constrained at this layer. A realization of a proving system using Plonkish arithmetization may limit the supported size of tables, for example limiting the number of entries in a given table 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.
 
 | Lookup Constraints | Description |
 | -------- | -------- |
-| $j \in \mathsf{LOOK}_v \Rightarrow q_v( f[0, j], \ldots, f[m_F-1, j], w[0, j], \ldots, w[m_A-1, j] ) \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. |
+| $j \in \mathsf{LOOK}_v \Rightarrow q_v(\mathsf{ROW}_j) \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,i}: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}^{m_{Q,v}}$ is an evaluation function that maps the fixed and advice cells on the lookup row to a tuple of field elements that must match a row of the table. Then
-$$
-q_{v,i}(X_0, \ldots, X_{m_F + m_A - 1}) = \text{polynomial as for custom constraints}
-$$
+Here $q_v: \mathbb{F}^{m_F + m_A} \mapsto \mathbb{F}^{L_v}$ is a multivariate polynomial that maps the fixed and advice cells $\mathsf{ROW}_j$ on the lookup row $j \in \mathsf{LOOK}_v$ to a tuple of field elements that must match a row of the table $\mathsf{TAB}_v$.