diff --git a/src/optimizations.md b/src/optimizations.md index e494d4e..04ba47f 100644 --- a/src/optimizations.md +++ b/src/optimizations.md @@ -2,113 +2,111 @@ ## 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 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 rotations 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. +> 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 rotations. 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 +## Preliminary definitions + +If not otherwise defined, variable names used here are consistent with [the relation description](relation.md). -TODO: define variables, and make this consistent with changes to [the relation](relation.md). +We will use the convention that variables marked with a prime ($'$) refer to *concrete* column or row indices. -Below we will use the convention that variables marked with a prime ($'$) refer to *concrete* column or row indices. +An "abstract cell" or "concrete cell" specifies an entry in the witness matrix $w$ of the abstract circuit, or the witness matrix $w'$ of the concrete circuit, respectively. -We say that an advice cell with coordinates $(i, j)$ "might be used" if it appears in some nontrivial copy constraint or custom constraint, i.e. $\mathsf{used}(i, j)$ is true iff any of the following hold: +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} -\exists (k, \ell) \neq (i, j) &:& (i, j) \equiv_A (k, \ell) \\ -\exists k &:& ((i, j), k) \in S_I \\ -\exists (k, \ell) &:& ((i, j), (k, \ell)) \in S_F \\ -\exists u &:& j \in \mathsf{CUS}_u \text{ and } w[i, j] \text{ ``might be used'' in } p_u(\mathsf{ROW}_j), +&& i < m_f \\ +\exists (k, \ell) \neq (i, j) &:& (i, j) \equiv (k, \ell) \\ +\exists k &:& ((i, j), k) \in S \\ +\exists u &:& j \in \mathsf{CUS}_u \text{ and } w[i, j] \text{ ``might be used'' in } p_u(\vec{w}_j) \\ +\exists v, s &:& j \in \mathsf{LOOK}_v \text{ and } w[i, j] \text{ ``might be used'' in } q_{v,s}(\vec{w}_j), \end{array} $$ -where -$$p_u(\mathsf{ROW}_j) = \sum_{z=0}^{\nu-1} \left( c_z \cdot \prod_{b=0}^{m_F-1} f[b, j]^{\alpha_{z,b}} \cdot \prod_{b'=0}^{m_A-1} w[b', j]^{\alpha_{z,m_F+b'}} \right).$$ - - +Here $p_u, \ q_{v,s} \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$ are each [multivariate polynomials](https://en.wikipedia.org/wiki/Polynomial_ring#Definition_(multivariate_case)) as defined in the relation description: -$w[i, j]$ "might be used" in $p_u(\mathsf{ROW}_j)$ iff $\exists z \in [0, \nu)$ s.t. $\alpha_{z,m_F+i} > 0$. +> Given $\eta$ symbols $X_0, \dots, X_{\eta-1}$ called indeterminates, a multivariate polynomial $P$ in these indeterminates, with coefficients in $\mathbb{F}$, +> is a finite linear combination $$P(X_0, \dots, X_{\eta-1}) = \sum_{z=0}^{\nu-1} \Big(c_z\, {\small\prod_{b=0}^{\eta-1}}\, X_b^{\alpha_{z,b}}\Big)$$ where $\nu \mathrel{⦂} \mathbb{N}$, $c_z \mathrel{⦂} \mathbb{F}$, and $\alpha_{z,b} \mathrel{⦂} \mathbb{N}$. ----- +Cell $w[i, j]$ "might be used" in $P(\vec{w}_j)$ iff $\exists z \in [0, \nu)$ s.t. $\alpha_{z,i} > 0$. -$w$ represents $m_A$ _abstract_ columns, that do not directly correspond 1:1 to actual columns in the compiled circuit (but may do so if the backend chooses). +## Compiling to a concrete circuit -Rotations are represented by hints $\mathbf{h} : [0,m_A) \mapsto [0,m_A') \times [0,n)$ where $m_A'$ 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). +$w$ represents $m$ _abstract_ columns, that do not directly correspond 1:1 to actual columns in the compiled circuit (but may do so if the backend chooses). -For convenience define: +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). -$$ -j \;\triangledown\; e = (j + e) \bmod n \\ -\mathbf{H}(i, j') = (i', j' \;\triangledown\; e_i) \text{ where }\mathbf{h}(i) = (i', e_i) -$$ +> TODO: should we only allow nonnegative $e_i$? That would simplify the correctness condition below. -Tesselation between custom constraints is just represented by equivalence under $\equiv_A$. When the rotation 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 $\mathbf{h}$, we construct an injective mapping of abstract row numbers to concrete row numbers (before rotation), $\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 $\mathbf{H}(i, \mathbf{r}(j)) = (i', \mathbf{r}(j) \;\triangledown\; e_i)$ where $\mathbf{h}(i) = (i', e_i)$. +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)$, where: +* all *constrained* abstract cells map to concrete cell coordinates that are in range; +* every *constrained* abstract cell is represented by a distinct concrete cell, except that abstract cells that are equivalent under $\equiv$ *may* be identified. -In order for this compilation to be correct, we must choose $\mathbf{r}$ so that every *used* abstract cell is represented by a distinct concrete cell, except that abstract cells that are equivalent under $\equiv_A$ *may* be identified. That is, $\mathbf{r}$ must be chosen such that: +That is: for $R \subseteq [0, n)$ define $$ -\forall (i, j, k, \ell) \in [0, m_A) \times [0, n) \times [0, m_A) \times [0, n) : \\ -\mathsf{used}(i, j) \;\wedge\; \mathsf{used}(k, \ell) \;\wedge\; (i, j) \not\equiv_A (k, \ell) \Rightarrow \mathbf{H}(i, \mathbf{r}(j)) \neq \mathbf{H}(k, \mathbf{r}(\ell)) +\begin{array}{rcl} +\mathsf{ok\_for}(R, \mathbf{r}) &=& \forall (i, j), (k, \ell) \in ([0, m) \times R) \times ([0, m) \times R) :\\[0.5ex] +&& \hspace{2em} (\mathsf{constrained}(i, j) \;\Rightarrow\; \mathbf{r}(j) + e_i \geq 0) \;\;\wedge\; \\[0.3ex] +&& \hspace{2em} (\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)) \\ +\end{array} $$ -> In other words, no two *used* advice cells map to the same concrete advice cell unless they are equivalent under $\equiv_A$. It is alright if one or more *unused* abstract cells map to the same concrete cell as a used abstract cell, because that will not affect the meaning of the circuit. Notice that specifying $\equiv_A$ 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. +Then, $\mathbf{r}$ must be chosen such that $\mathsf{ok\_for}([0, n), \mathbf{r})$. + +> 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. -The used abstract advice cells $w : \mathbb{F}^{m_A \times n}$ are translated to concrete advice cells $w' : \mathbb{F}^{m'_A \times n'}$: +The constrained abstract cells $w : \mathbb{F}^{m \times n}$ are translated to concrete cells $w' : \mathbb{F}^{m' \times n'}$: $$ -\mathsf{used}(i, j) \Rightarrow w'(\mathbf{H}(i, \mathbf{r}(j))) = w(i, j) +\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 used abstract cell are arbitrary. - -The instance columns are zero-extended to $n'$ rows. +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 translated to concrete fixed cells $f' : \mathbb{F}^{m_F \times n'}$ using just the row mapping, filling the fixed cells of added rows with zeros: +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'(i, \mathbf{r}(j)) = f(i, j) \\ -f'(i, j') = 0\text{ if } j' \not\in Im(\mathbf{r}) +f'[h_i, \mathbf{r}(j) + e_i] = f[i, j] $$ -The abstract coordinates appearing in $\equiv_A$, $S_I$, and $S_F$ are similarly mapped to their concrete coordinates. +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. The conditions for custom gates in the concrete circuit are then given by: $$ \mathsf{CUS}'_u = \{ \mathbf{r}(j) : j \in \mathsf{CUS}_u \} \\ -j' \in \mathsf{CUS}'_u \Rightarrow p_u\left( \begin{array}{rcl} -f'[0, j'], &\ldots,& f'[m_F-1, j'], \\ -w'[\mathbf{H}(0, j')], &\ldots,& w'[\mathbf{H}(m_A-1, j')] -\end{array} -\right) = 0 +j' \in \mathsf{CUS}'_u \Rightarrow p_u\left([w'[h_i, j' + e_i] : i \leftarrow 0 \text{..} m]\right) = 0 $$ -### Greedy algorithm for choosing $\mathbf{r}$ - -There is a greedy algorithm for deterministically choosing $\mathbf{r}$ that maintains ordering of rows (i.e. $\mathbf{r}$ is strictly increasing), and simply inserts a gap in the row mapping whenever the above constraint would not be met for all rows so far: - -For $t \in [0, n)$, define +and similarly for lookups: $$ -\begin{array}{rcl} -\mathsf{ok\_up\_to}(t, \mathbf{r}) &=& \forall (i, j, k, l) \in [0, m_A) \times [0, t] \times [0, m_A) \times [0, t] : \\ -&&\mathsf{used}(i, j) \;\wedge\; \mathsf{used}(k, \ell) \;\wedge\; (i, j) \not\equiv_A (k, \ell) \Rightarrow \mathbf{H}(i, \mathbf{r}(j)) \neq \mathbf{H}(k, \mathbf{r}(\ell)) -\end{array} +\mathsf{LOOK}'_v = \{ \mathbf{r}(j) : j \in \mathsf{LOOK}_v \} \\ +j' \in \mathsf{LOOK}'_v \Rightarrow [q_{v,s}\left([w'[h_i, j' + e_i] : i \leftarrow 0 \text{..} m]\right) : s \leftarrow 0 \text{..} L_v] \in \mathsf{TAB}_v $$ -That is, $\mathsf{ok\_up\_to}(t, \mathbf{r})$ means that the correctness criterion above holds for the subset $[0, t]$ of abstract rows. + +### Greedy algorithm for choosing $\mathbf{r}$ + +There is a greedy algorithm for deterministically choosing $\mathbf{r}$ that maintains ordering of rows (i.e. $\mathbf{r}$ is strictly increasing), and simply inserts a gap in the row mapping whenever the above constraint would not be met for all rows so far. | Algorithm for choosing $\mathbf{r}$ | |----| | set $\mathbf{r} := \{\}$ | -| set $v := 0$ | -| for $t$ from $0$ up to $n-1$: | -| $\hspace{2em}$ find the minimal $u \geq v$ such that $\mathsf{ok\_up\_to}(t, \mathbf{r} \cup \{t \mapsto u\})$ | -| $\hspace{2em}$ set $\mathbf{r} := \mathbf{r} \cup \{t \mapsto u\}$ and $v := u+1$ | -| let $n' = v$ be the number of concrete rows. | - -This algorithm can be proven correct by induction on $n$. It is complete because for each step it is always possible to find a suitable $u$. That is, we can always choose $u$ large enough that any additional conditions $$ -\mathsf{used}(i, j) \;\wedge\; \mathsf{used}(k, \ell) \;\wedge\; (i, j) \not\equiv_A (k, \ell) \Rightarrow \mathbf{H}(i, \mathbf{r}(j)) \neq \mathbf{H}(k, \mathbf{r}(\ell)) -$$ for $j = t$ or $\ell = t$ are met, because $\mathbf{r}(t) = u$ and both $\mathbf{H}(i, u)$ and $\mathbf{H}(k, u)$ can be made not to overlap with any previously used cell. +| set $a' := 0$ | +| for $g$ from $0$ up to $n-1$: | +| $\hspace{2em}$ find the minimal $g' \geq a'$ such that $\mathsf{ok\_for}([0, g], \mathbf{r} \cup \{g \mapsto g'\})$ | +| $\hspace{2em}$ set $\mathbf{r} := \mathbf{r} \cup \{g \mapsto g'\}$ and $a' := g'+1$ | + +The number of concrete rows is then given by $n' = \max \{ \mathbf{r}(j) + e_i : (i, j) \in ([0, m) \times [0, n)) \;\wedge\; \mathsf{constrained}(i, j) \} + 1$. + +This algorithm is correct because in the last step it finds $\mathbf{r}$ such that $\mathsf{ok\_for}([0, n), \mathbf{r})$, which is the correctness condition above. + +It is complete because for each step it is always possible to find a suitable $g'$: there is no upper bound on $g'$, and so we can always choose it large enough that any additional conditions of $\mathsf{ok\_for}([0, g], \mathbf{r} \cup \{g \mapsto g'\})$ relative to $\mathsf{ok\_for}([0, g-1], \mathbf{r})$ hold. Specifically: by symmetry it is sufficient to consider the additional conditions for which $j = g$ and $\ell < g$. There must be some $g' = \mathbf{r}(j)$ such that $(h_i, g' + e_i)$ does not overlap with $(h_k, \mathbf{r}(\ell) + e_k)$ for any $i, k \in [0, m)$ and $\ell \in [0, g-1]$. diff --git a/src/relation.md b/src/relation.md index 75730c8..d9c855a 100644 --- a/src/relation.md +++ b/src/relation.md @@ -6,108 +6,120 @@ This is intended to be read in conjunction with the [Plonkish Backend Optimizations](optimizations.md) document, which describes how to compile the abstract constraint system described here into a concrete circuit. -## Dependencies +## Dependencies and notation 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 there exists some advice $w$ such that $(\mathsf{instance}, w) \in \mathcal{R}_{\mathsf{plonkish}}.$ +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 $(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 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. -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) -$$ +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 -### Inputs into $\mathcal{R}_{\mathsf{plonkish}}$ +The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes instances of the following form: -| Public Inputs | Description | +| Instance element | Description | | ----------------- | -------- | | $\mathbb{F}$ | A prime field. | -| $t_I$ | Number of instance entries. | -| $\phi$ | Instance entries $\phi : \mathbb{F}^{t_I}$. | +| $t$ | Length of the instance vector. | +| $\phi$ | The instance vector $\phi \mathrel{⦂} \mathbb{F}^t$. | | $n > 0$ | Number of rows. | -| $S_I$ | A set $S_I \subseteq ([0,m_A) \times [0,n)) \times [0,t_I)$ indicating which instance entries must be used in the advice. | -| $m_F$ | Number of fixed columns. | -| $f$ | Fixed columns $f : \mathbb{F}^{m_F \times n}$. | -| $S_F$ | A set $S_F \subseteq ([0,m_A) \times [0,n)) \times ([0,m_F) \times [0,n))$ indicating which fixed entries must be used in the advice. | -| $m_A > 0$ | Number of advice columns. | -| $\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$ | Number of columns. | +| $\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. | +| $p_u$ | Custom multivariate polynomials $p_u \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}$. | | $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}^{L_v}$. | +| $\mathsf{LOOK}_v$ | Sets $\mathsf{LOOK}_v \subseteq [0,n)$ indicating which rows the scaled lookups into $\mathsf{TAB}_v$ are applied to. | +| $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 -| Private Inputs | Description | +The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes witnesses of the following form: + +| Witness element | Description | | ----------------- | -------- | -| $w$ | Advice columns $w : \mathbb{F}^{m_A \times n}$. | +| $w$ | The witness matrix $w \mathrel{⦂} \mathbb{F}^{m \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]]$. +Define $\vec{w}_j$ as the row vector $[w[i, j] : i \leftarrow 0 \text{..} m]$. -Given the above definitions, the relation $\mathcal{R}_{\mathsf{plonkish}}$ is given by: +### Definition of the relation +Given the above definitions, the relation $\mathcal{R}_{\mathsf{plonkish}}$ is given by $\{ (x = (\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 \}_v), w) \}$ such that: $$ -\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\} +\begin{array}{ll|l} + 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] \\[0.3ex] + 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] \\[0.3ex] + \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] \\[0.3ex] + \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 \\[0.3ex] + \mathsf{LOOK}_v \subseteq [0,n), \ q_{v,s} \mathrel{⦂} \mathbb{F}^m \mapsto \mathbb{F}, \ \mathsf{TAB}_v \subseteq \mathbb{F}^{L_v} & & j \in \mathsf{LOOK}_v \Rightarrow [q_{v,s}(\vec{w}_j) : s \leftarrow 0 \text{..} L_v] \in \mathsf{TAB}_v +\end{array} $$ ### 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: +There are four types of constraints that a Plonkish statement $(x, w) \in \mathcal{R}_{\mathsf{Plonkish}}$ must satisfy: +* Fixed constraints * Copy constraints * Custom constraints * Lookup constraints +#### Fixed constraints + +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_I \Rightarrow w[i, j] = \phi[k]$ | The $k$ th instance entry is equal to the $(i,j)$ th advice entry for all $((i,j),k) \in S_I$. | -| $((i,j),(k,\ell)) \in S_F \Rightarrow w[i, j] = f[k, \ell]$ | The $(k, \ell)$ th fixed entry is equal to the $(i,j)$ th advice entry for all $((i,j),(k,\ell)) \in S_F$. | -| $(i,j) \equiv_A (k,\ell) \Rightarrow w[i, j] = w[k, \ell]$ | $\equiv_A$ is an equivalence relation indicating which advice entries are constrained to be equal. | +| $((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 -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 | | -------- | -------- | -| $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. | - - +| $j \in \mathsf{CUS}_u \Rightarrow p_u(\vec{w}_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. | -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)): +Here $p_u \mathrel{⦂} \mathbb{F}^m \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}$. +> Given $\eta$ symbols $X_0, \dots, X_{\eta-1}$ called indeterminates, a multivariate polynomial $P$ in these indeterminates, with coefficients in $\mathbb{F}$, +> is a finite linear combination $$P(X_0, \dots, X_{\eta-1}) = \sum_{z=0}^{\nu-1} \Big(c_z\, {\small\prod_{b=0}^{\eta-1}}\, X_b^{\alpha_{z,b}}\Big)$$ where $\nu \mathrel{⦂} \mathbb{N}$, $c_z \mathrel{⦂} \mathbb{F}$, and $\alpha_{z,b} \mathrel{⦂} \mathbb{N}$. #### 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 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. +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. | Lookup Constraints | Description | | -------- | -------- | -| $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. | +| $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: \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$. +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$.