diff --git a/.github/workflows/merge-acceptance.yaml b/.github/workflows/merge-acceptance.yaml new file mode 100644 index 0000000..7ac08bb --- /dev/null +++ b/.github/workflows/merge-acceptance.yaml @@ -0,0 +1,18 @@ +name: 'Check Rendering' +on: pull_request +jobs: + check-render: + runs-on: 'ubuntu-latest' + steps: + - name: Rust Toolchain Version Diagnostics + run: cargo --version --verbose && rustup --version + - uses: taiki-e/cache-cargo-install-action@v1 + with: + tool: mdbook@0.4.37 + - uses: taiki-e/cache-cargo-install-action@v1 + with: + tool: mdbook-katex@0.6.0 + - uses: actions/checkout@v3 + - run: mdbook build + - name: Check for Orphaned Files + run: ./util/find-orphaned-files.sh diff --git a/.github/workflows/render-site.yaml b/.github/workflows/render-site.yaml new file mode 100644 index 0000000..4750555 --- /dev/null +++ b/.github/workflows/render-site.yaml @@ -0,0 +1,64 @@ +# Reference: https://nathan-at-least.github.io/auto-deploy-howto.html +name: Deploy Rendered Site + +on: + push: + branches: [ main ] + +env: + CARGO_TERM_COLOR: always + +jobs: + render-and-deploy: + + runs-on: ubuntu-latest + + steps: + # These initial steps set up the toolchain: + - name: Rust Toolchain Version Diagnostics + run: cargo --version --verbose && rustup --version + with: + tool: mdbook@0.4.37 + - uses: taiki-e/cache-cargo-install-action@v1 + with: + tool: mdbook-katex@0.6.0 + + # Now get the user content: + - uses: actions/checkout@v3 + + # Now render to the site: + + # Each deploy overwrites the contents of `gh-pages` branch from + # `main`, but also introduces a merge structure so that the history of + # `gh-pages` is tracked: + - name: Overwrite gh-pages branch with main branch + run: | + set -x + BASE_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + git config --global user.name 'autodeploy' + git config --global user.email 'autodeploy' + git fetch + git checkout gh-pages # ensure we have local branch + git checkout "$BASE_BRANCH" + TMP='local-temp-branch' + git checkout -b "$TMP" # Same tree state as main branch + git merge \ + --strategy ours \ + --commit \ + -m 'Auto-deploy: overwriting with `main` branch' \ + --allow-unrelated-histories \ + gh-pages + git checkout gh-pages + git merge --ff-only "$TMP" + git branch -d "$TMP" + - run: mdbook build + - name: Rendered manifest + run: find ./docs -type f -exec ls -ld '{}' \; + - name: Disable jekyll + run: touch .nojekyll + - name: Commit and Push render to gh-pages + run: | + set -x + git add --all + git commit -m 'Auto-deploy: rendered output' + git push diff --git a/.gitignore b/.gitignore index 28cbceb..19fc66b 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,6 @@ # Editor temporary files .*.swp *~ + +# mdbook output +/docs diff --git a/LICENSE-MIT b/LICENSE-MIT index aa85842..5842c0e 100644 --- a/LICENSE-MIT +++ b/LICENSE-MIT @@ -1,6 +1,6 @@ The MIT License (MIT) -Copyright (c) 2023 The ZKProof Standards contributors +Copyright (c) 2023-2024 The ZKProof Standards contributors Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/README.md b/README.md index 2d31598..95ac234 100644 --- a/README.md +++ b/README.md @@ -17,6 +17,17 @@ for this standardization effort. The software and specifications in this repository are currently under development and have not been fully reviewed. +## Rust prerequisites + +- `cargo install mdbook` +- `cargo install mdbook-katex` + +## Rendering + +- `mdbook build` + +The rendered documents can be viewed at [docs/index.html](docs/index.html). + ## License All files in this repository are licensed under any of: diff --git a/book.toml b/book.toml new file mode 100644 index 0000000..38375b4 --- /dev/null +++ b/book.toml @@ -0,0 +1,24 @@ +[book] +authors = [ + "Daira-Emma Hopwood", + "Mary Maller", + "Jack Grigg", +] +language = "en" +multilingual = false +src = "src" +title = "Plonkish Constraint System Working Group" + +[build] +# GitHub pages renders content under `docs/`; see https://nathan-at-least.github.io/auto-deploy-howto.html +build-dir = "docs" + +[preprocessor.katex] +macros = "src/macros.txt" +renderer = ["html"] +# Uncomment this if we need \href and \url links in KaTeX to work (which we currently don't). +#trust = true + +[output.html] +default-theme = "light" +additional-css = ["css/style.css"] diff --git a/css/style.css b/css/style.css new file mode 100644 index 0000000..e962007 --- /dev/null +++ b/css/style.css @@ -0,0 +1,8 @@ +table { + margin: 0 auto; + width: 100%; +} + +table tbody tr { + background: var(--table-alternate-bg); +} diff --git a/ABSTRACT.md b/src/ABSTRACT.md similarity index 97% rename from ABSTRACT.md rename to src/ABSTRACT.md index e5dd39b..30317c2 100644 --- a/ABSTRACT.md +++ b/src/ABSTRACT.md @@ -1,4 +1,4 @@ -# Plonkish Constraint System Working Group +# Abstract — Plonkish Constraint System Working Group ## Contributors - Jack Grigg, Electric Coin Company @@ -19,7 +19,7 @@ The initial deliverable will be split into two draft specifications: - The Plonkish constraint system specification. - The optimised Plonkish constraint specification. -The constraint system specifications will be agnostic to the underlying prime-order field. The output is expected to be used as input to e.g., an Interactive Oracle Proof. +The constraint system specifications will be agnostic to the underlying prime-order field. The output is expected to be used as input to e.g., an Interactive Oracle Proof. The Plonkish constraint system specification will detail: - The fixed, public, and private inputs (which are field elements) to the Plonkish relation. diff --git a/src/SUMMARY.md b/src/SUMMARY.md new file mode 100644 index 0000000..05955ea --- /dev/null +++ b/src/SUMMARY.md @@ -0,0 +1,6 @@ +# Contents + +- [Abstract](ABSTRACT.md) +- [Specification of the Plonkish Relation](relation.md) +- [Plonkish Backend Optimizations](optimizations.md) +- [Change Log](changelog.md) diff --git a/src/changelog.md b/src/changelog.md new file mode 100644 index 0000000..9483753 --- /dev/null +++ b/src/changelog.md @@ -0,0 +1,47 @@ +# Change Log + +Changes are listed most-recent-first. + +## Changes made by Daira-Emma and Mary on 2023-03-15 + +* Make the instance entries just a flat vector. +* Improved consistency of notation. + +## Changes made by Mary on 2023-28-03 + +* Added $q_v$ scaling functions to describe input to lookup tables. +* Completed first attempt at describing lookup constraints +* Have not yet tackled dynamic tables. + +## Changes made by Daira-Emma and Str4d on 2023-03-17 + +* Rename some variables for consistency, and use $\triangledown$ also in Mary's definition of rotation constraints. +* Complete the "Greedy algorithm for choosing $\mathbf{r}$". +* Daira-Emma: Delete the paragraph describing the $\mathsf{Rot}$ constraints as hints, and add a note explaining the disadvantages of that approach. + +## Changes made by Mary since 2023-15-03 + +* Add rotation constraints into copy constraints + * This is an alternative proposal to Option B of the hint suggestion. + * If we use this approach we could keep the description for copy constraints as is. + +* Suggest enforcing that rotation constraints must be fully implied by $S_A$ + * Avoids having to define "used" cells and therefore simplifies. + * We can use the (under construction) greedy algorithm anyway. + +* Tried to be more precise about what $p_u$ constraints are valid. + * Before we just said $p_u$ is constructed using addition and multiplication gates which is potentially too vague. + * Current suggestion is a bit ugly and needs checking for correctness. + +## Changes made by Daira-Emma since the 2023-03-03 meeting + +* Change $S_A$ to an equivalence relation + * This removes unnecessary degrees of freedom in specifying copy constraints between advice cells, and makes it easier to define correctness of the abstract $\rightarrow$ concrete compilation. +* Use $u$ instead of $k$ to index custom constraints, and $v$ instead of $k$ to index lookups. + * This avoids overloading of $k$. +* Define the $\triangledown$ operator for addition modulo $n$. +* Define "used" cells. +* For "With rotations (option A)", change $E_u$ to be a list of rotations. + * This avoids the need for $z_u$ as a separate variable. +* For "With rotations (option B)", give more detail and specify a correctness condition for compiling an abstract circuit to a concrete circuit using hints. + diff --git a/src/macros.txt b/src/macros.txt new file mode 100644 index 0000000..e69de29 diff --git a/src/optimizations.md b/src/optimizations.md new file mode 100644 index 0000000..fbe1b57 --- /dev/null +++ b/src/optimizations.md @@ -0,0 +1,103 @@ +# Plonkish Backend Optimizations + +## 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. + +> 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. +> +> 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). + +## Compiling to a concrete circuit + +TODO: define variables, and make this consistent with changes to [the relation](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)$ is "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: +$$ +\begin{array}{rcl} +\exists (k, \ell) \neq (i, j) &:& (i, j) \equiv_A (k, \ell) \\ +\exists k, \ell &:& (i, j, k, \ell) \in S_I \\ +\exists k, \ell &:& (i, j, k, \ell) \in S_F \\ +\exists u &:& j \in \mathsf{CUS}_u \text{ and the } w[i, \_] \text{ argument to } p_u \text{ is used nontrivially}. +\end{array} +$$ + +$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). + +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). + +For convenience define: + +$$ +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 $\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: +$$ +\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)) +$$ + +> 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. + +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'}$: +$$ +\mathsf{used}(i, j) \Rightarrow w'(\mathbf{H}(i, \mathbf{r}(j))) = 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 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: +$$ +f'(i, \mathbf{r}(j)) = f(i, j) \\ +f'(i, j') = 0\text{ if } j' \not\in Im(\mathbf{r}) +$$ + +The abstract coordinates appearing in $\equiv_A$, $S_I$, and $S_F$ 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 +$$ + +### 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 +$$ +\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} +$$ +That is, $\mathsf{ok\_up\_to}(t, \mathbf{r})$ means that the correctness criterion above holds for the subset $[0, t]$ 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$ | +| 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. diff --git a/src/relation.md b/src/relation.md new file mode 100644 index 0000000..fd18250 --- /dev/null +++ b/src/relation.md @@ -0,0 +1,107 @@ +# Specification of the Plonkish Relation + +## Objectives +- Need to agree on the API between “zkInterface for Plonkish” and the proving system. Specify a general statement that the proving system has to implement. +- Section 2 of [[Thomas 2022]](https://eprint.iacr.org/2022/777.pdf) : describes high level API of zk Interface for Plonkish statements + +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 + +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. + +$$ +\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 +$$ +\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}}$ + +| Public Inputs | Description | +| ----------------- | -------- | +| $\mathbb{F}$ | A prime field. | +| $t_I$ | Number of instance entries. | +| $\phi$ | Instance entries $\phi : \mathbb{F}^{t_I}$. | +| $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_{Q,v}$ | The width of 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}}$. | + +> 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}$. | + +### 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: + +* Copy constraints +* Custom constraints +* Lookup constraints + +#### 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. | + +#### 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 | 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. | + + + +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. + +#### 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. + +| 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. | + +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} +$$ diff --git a/util/find-orphaned-files.sh b/util/find-orphaned-files.sh new file mode 100755 index 0000000..9d084b4 --- /dev/null +++ b/util/find-orphaned-files.sh @@ -0,0 +1,41 @@ +#!/bin/bash +# +# Print out any md files within `./src` which aren't linked from SUMMARY. +# +# If there are any, exit with non-zero status + +set -efuo pipefail + +function main +{ + # Move to src dir regardless of `pwd`: + cd "$(dirname "$(readlink -f "$0")")/../src" + + local DATADIR="$(mktemp --directory)" + local LINKED="${DATADIR}/linked" + local ACTUAL="${DATADIR}/actual" + local DIFF="${DATADIR}/diff" + + parse-linked-files < './SUMMARY.md' > "$LINKED" + find-actual-files > "$ACTUAL" + + set +o pipefail # It's ok for this pipeline to fail: + diff -u "$LINKED" "$ACTUAL" | grep -Eve '^(\+\+\+|---)' | grep '^[+-]' | tee "$DIFF" + + if [ "$(wc -l < "$DIFF")" -eq 0 ] + then exit 0 + else exit 1 + fi +} + +function parse-linked-files +{ + grep '(' | sed 's@^.*(@./@; s@)$@@' | grep -v '^$' | sort +} + +function find-actual-files +{ + find . -type f -not -name 'SUMMARY.md' -name '*.md' | sort +} + +main "$@"