From 027998a953b73923efdcc97051cfeabdc7aeb867 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 10 Jun 2024 02:26:51 +0100 Subject: [PATCH] Updates from the June 7 meeting. * Fix a bug in the definition of $q_v$: it needs to be a vector of polynomials of width given by the table width $L_v$. * Treat fixed columns as a special case of abstract columns, removing the need for $S_F$. * Simplify notation: * $t_I$ -> $t$ * $m_F + m_A$ -> $m$ * $m_F$ -> $m_f$ * $\equiv_A$ -> $\equiv$ * $S_I$ and $S_F$ -> $S$ * $q_v$ -> $q_{v,s}$ * $\mathsf{ROW}_j$ -> $\vec{w}_j$ * update variable names for multivariate polynomials to avoid clashes * improve notation for comprehensions and type declarations. * Simplify the definition of optimization hints, allowing only offsets and not rotations. * Take into account lookups in optimization. Co-authored-by: Mary Maller Signed-off-by: Daira-Emma Hopwood --- src/optimizations.md | 103 ++++++++++++++++++++----------------------- src/relation.md | 101 ++++++++++++++++++++++-------------------- 2 files changed, 103 insertions(+), 101 deletions(-) diff --git a/src/optimizations.md b/src/optimizations.md index e494d4e..ba301d0 100644 --- a/src/optimizations.md +++ b/src/optimizations.md @@ -2,113 +2,108 @@ ## 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 tradeoff 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 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). ## Compiling to a concrete circuit -TODO: define variables, and make this consistent with changes to [the relation](relation.md). +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 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 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: $$ \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: - +> 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}$. -$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$. +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). +$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). -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). +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). -For convenience define: +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. -$$ -j \;\triangledown\; e = (j + e) \bmod n \\ -\mathbf{H}(i, j') = (i', j' \;\triangledown\; e_i) \text{ where }\mathbf{h}(i) = (i', e_i) -$$ - -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. +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. -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)$. - -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: +In order for this compilation to be correct, we must choose $\mathbf{r}$ so that every *constrained* abstract cell is represented by a distinct concrete cell, except that abstract cells that are equivalent under $\equiv$ *may* be identified. That is, $\mathbf{r}$ must be chosen such that: $$ -\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)) +\forall (i, j), (k, \ell) \in ([0, m) \times [0, n)) \times ([0, m) \times [0, n)) : \\ +\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) $$ -> 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. +> 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. 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 advice cells $w : \mathbb{F}^{m \times n}$ are translated to concrete advice 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 abstract fixed cells $f : \mathbb{F}^{m_f \times n}$ are similarly translated to concrete fixed 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. +Concrete fixed 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 +$$ + +and similarly for lookups: +$$ +\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 $$ ### 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 +For $g \in [0, n)$, define $$ \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)) +\mathsf{ok\_up\_to}(g, \mathbf{r}) &=& \forall (i, j), (k, \ell) \in ([0, m) \times [0, g]) \times ([0, m) \times [0, g]) : +\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} $$ -That is, $\mathsf{ok\_up\_to}(t, \mathbf{r})$ means that the correctness criterion above holds for the subset $[0, t]$ of abstract rows. +That is, $\mathsf{ok\_up\_to}(g, \mathbf{r})$ means that the correctness criterion above holds for the subset $[0, g]$ of abstract rows. | 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$ | +| for $g$ from $0$ up to $n-1$: | +| $\hspace{2em}$ find the minimal $u \geq v$ such that $\mathsf{ok\_up\_to}(g, \mathbf{r} \cup \{g \mapsto u\})$ | +| $\hspace{2em}$ set $\mathbf{r} := \mathbf{r} \cup \{g \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. +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{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. diff --git a/src/relation.md b/src/relation.md index 75730c8..a0b565f 100644 --- a/src/relation.md +++ b/src/relation.md @@ -6,108 +6,115 @@ 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$. +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 Plonkish Relation $\mathcal{R}_{\mathsf{plonkish}}$ + +The relation $\mathcal{R}_{\mathsf{plonkish}}$ contains pairs of instances $\mathsf{instance}$, and witnesses $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. -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. In the setting of a zero-knowledge proof system, the witness is private and the proof leaks no additional information about it. + +### 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$ | Number of instance entries. | +| $\phi$ | Instance entries $\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 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. | +| $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. -| Private Inputs | Description | +### Witnesses + +The relation $\mathcal{R}_{\mathsf{plonkish}}$ takes a witness of the following form: + +| Witness | Description | | ----------------- | -------- | -| $w$ | Advice columns $w : \mathbb{F}^{m_A \times n}$. | +| $w$ | Columns $w \mathrel{⦂} \mathbb{F}^{m \times n}$. | + +Define $\vec{w}_j$ as the row vector $[w[i, j] : i \leftarrow 0 \text{..} m]$. -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]]$. +### Definition of the relation 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 + (\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] \\ + 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 \\ + \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} \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: +There are four types of constraints that a Plonkish statement $(\mathsf{instance}, 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 | 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 advice 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. +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. | 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. -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. | 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 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$.