explain the various cross-table arguments used in Triton VM

specification/src/SUMMARY.md

@@ -6,7 +6,6 @@
     + [Instructions](instructions.md)
     + [Pseudo Instructions](pseudo-instructions.md)
 - [Arithmetization](arithmetization.md)
-    + [Permutation and Evaluation Arguments]()
     + [Program Table](program-table.md)
     + [Processor Table](processor-table.md)
         * [Instruction Groups](instruction-groups.md)
@@ -16,12 +15,16 @@
     + [Jump Stack Table](jump-stack-table.md)
     + [Hash Table](hash-table.md)
     + [U32 Table](u32-table.md)
-    + [Memory-Consistency](memory-consistency.md)
-        * [Contiguity of Memory-Pointer Regions](contiguity-of-memory-pointer-regions.md)
-        * [Clock Jump Differences and Inner Sorting](clock-jump-differences-and-inner-sorting.md)
-        * [Proof of Memory Consistency](proof-of-memory-consistency.md)
-        * [Appendix: Modified Memory Pointers by Instruction](modified-memory-pointers-by-instruction.md)
+- [Table Linking](table-linking.md)
+    + [Permutation Argument](permutation-argument.md)
+    + [Evaluation Argument](evaluation-argument.md)
+    + [Bézout Argument](bezout-argument.md)
+    + [Lookup Argument](lookup-argument.md)
+- [Memory-Consistency](memory-consistency.md)
+    + [Contiguity of Memory-Pointer Regions](contiguity-of-memory-pointer-regions.md)
+    + [Clock Jump Differences and Inner Sorting](clock-jump-differences-and-inner-sorting.md)
+    + [Proof of Memory Consistency](proof-of-memory-consistency.md)
+    + [Appendix: Modified Memory Pointers by Instruction](modified-memory-pointers-by-instruction.md)
 ---
-- [Copy Constraints](copy-constraints.md)
 - [Index Sampling](index-sampling.md)
 - [Sum Check](sum-check.md)

specification/src/bezout-argument.md

@@ -0,0 +1,16 @@
+# Bézout Argument
+
+The Bézout Argument establishes that some list $A = (a_0, \dots, a_n)$ does not contain any duplicate elements.
+It uses [Bézout's identity for univariate polynomials](https://en.wikipedia.org/wiki/Polynomial_greatest_common_divisor#B%C3%A9zout's_identity_and_extended_GCD_algorithm).
+Concretely, the prover shows that for the polynomial $f_A(X)$ with all elements of $A$ as roots, _i.e._,
+$$
+f_A(X) = \prod_{i=0}^n X - a_i
+$$
+and its formal derivative $f'_A(X)$, there exist $u(X)$ and $v(X)$ with appropriate degrees such that
+$$
+u(X) \cdot f_A(X) + v(X) \cdot f'_A(X) = 1.
+$$
+In other words, the Bézout Argument establishes that the greatest common divisor of $f_A(X)$ and $f'_A(X)$ is 1.
+This implies that all roots of $f_A(X)$ have multiplicity 1, which holds if and only if there are no duplicate elements in list $A$.
+
+For an example, a more in-depth explanation, the arithmetization, as well as proofs of completeness, soundness, and Zero-Knowledge, we refer to the later [section on continuity of the RAM pointer regions](contiguity-of-memory-pointer-regions.md#contiguity-for-ram-table).

specification/src/evaluation-argument.md

@@ -0,0 +1,45 @@
+# Evaluation Argument
+
+The Evaluation Argument establishes that two lists $A = (a_0, \dots, a_n)$ and $B = (b_0, \dots, b_n)$ are identical.
+To achieve this, the lists' elements are interpreted as the coefficients of polynomials $f_A(X)$ and $f_B(X)$, respectively:
+
+$$
+\begin{aligned}
+f_A(X) &= X^{n+1} + \sum_{i=0}^n a_{n-i}X^i \\
+f_B(X) &= X^{n+1} + \sum_{i=0}^n b_{n-i}X^i \\
+\end{aligned}
+$$
+
+The two lists $A$ and $B$ are identical if and only if the two polynomials $f_A(X)$ and $f_B(X)$ are identical.
+By the [Schwartz–Zippel lemma](https://en.wikipedia.org/wiki/Schwartz%E2%80%93Zippel_lemma), probing the polynomials in a single point $\alpha$ establishes the polynomial identity with high probability.[^1]
+
+In Triton VM, the Evaluation Argument is generally used to show that (parts of) some row appear in two tables in the same order.
+To establish this, the prover
+
+- commits to the base column in question,[^2]
+- samples a random challenge $\alpha$ through the Fiat-Shamir heuristic,
+- computes the _running evaluation_ of $f_A(\alpha)$ and $f_B(\alpha)$ in the respective tables' extension column.
+
+For example, in both Table A and B:
+
+| base column | extension column: running evaluation                       |
+|------------:|:-----------------------------------------------------------|
+|           0 | $\alpha^1 + 0\alpha^0$                                     |
+|           1 | $\alpha^2 + 0\alpha^1 + 1\alpha^0$                         |
+|           2 | $\alpha^3 + 0\alpha^2 + 1\alpha^1 + 2\alpha^0$             |
+|           3 | $\alpha^4 + 0\alpha^3 + 1\alpha^2 + 2\alpha^1 + 3\alpha^0$ |
+
+It is possible to establish a subset relation by skipping over certain elements when computing the running evaluation.
+The running evaluation must incorporate the same elements in both tables.
+Otherwise, the Evaluation Argument will fail.
+
+Examples for subset Evaluation Arguments can be found between the [Hash Table](hash-table.html#extension-columns) and the [Processor Table](processor-table.md#extension-colums).
+
+---
+
+[^1]: This depends on the length $n$ of the lists $A$ and $B$ as well as the field size.
+For Triton VM, $n < 2^{32}$.
+The polynomials $f_A(X)$ and $f_B(X)$ are evaluated over the extension field with $p^3 \approx 2^{192}$ elements.
+The false positive rate is therefore $n / |\mathbb{F}_{p^3}| \leqslant 2^{-160}$.
+
+[^2]: See “[Compressing Multiple Elements](table-linking.md#compressing-multiple-elements).”

specification/src/lookup-argument.md

@@ -0,0 +1,105 @@
+# Lookup Argument
+
+The [Lookup Argument](https://eprint.iacr.org/2023/107.pdf) establishes that all elements of list $A = (a_0, \dots, a_\ell)$ also occur in list $B = (b_0, \dots, b_n)$.
+In this context, $A$ contains the values that are being looked up, while $B$ is the lookup table.[^1]
+Both lists $A$ and $B$ may contain duplicates.
+However, it is inefficient if $B$ does, and is therefor assumed not to.
+
+The example at the end of this section summarizes the necessary computations for the Lookup Argument.
+The rest of the section derives those computations.
+The first step is to interpret both lists' elements as the roots of polynomials $f_A(X)$ and $f_B(X)$, respectively:
+
+$$
+\begin{aligned}
+f_A(X) &= \prod_{i=0}^\ell X - a_i \\
+f_B(X) &= \prod_{i=0}^n X - b_i
+\end{aligned}
+$$
+
+By counting the number of occurrences $m_i$ of unique elements $a_i \in A$ and eliminating duplicates, $f_A(X)$ can equivalently be expressed as:
+
+$$
+f_A(X) = \prod_{i=0}^n (X - a_i)^{m_i}
+$$
+
+
+The next step uses
+- the formal derivative $f'_A(X)$ of $f_A(X)$, and
+- the multiplicity-weighted formal derivative $f'^{(m)}_B(X)$ of $f_B(X)$.
+
+The former is the familiar formal derivative:
+
+$$
+f'_A(X) = \sum_{i=0}^n m_i (X - a_i)^{m_i - 1} \prod_{j \neq i}(X - a_j)^{m_j}
+$$
+
+The multiplicity-weighted formal derivative uses the lookup-multiplicities $m_i$ as additional factors:
+
+$$
+f'^{(m)}_B(X) = \sum_{i=0}^n m_i \prod_{j \neq i}(X - b_j)
+$$
+
+Let $g(X)$ the greatest common divisor of $f_A(X)$ and $f'_A(X)$.
+The polynomial $f_A(X) / g(X)$ has the same roots as $f_A(X)$, but all roots have multiplicity 1.
+This polynomial is identical to $f_B(X)$ if and only if all elements in list $A$ also occur in list $B$.
+
+A similar property holds for the formal derivatives:
+The polynomial $f'_A(x) / g(X)$ is identical to $f'^{(m)}_B(X)$ if and only if all elements in list $A$ also occur in list $B$.
+By solving for $g(X)$ and equating, the following holds:
+
+$$
+f_A(X) \cdot f'^{(m)}_B(X) = f'_A(X) \cdot f_B(X)
+$$
+
+## Optimization through Logarithmic Derivatives
+
+The [logarithmic derivative](https://eprint.iacr.org/2022/1530.pdf) of $f(X)$ is defined as $f'(X) / f(X)$.
+Furthermore, the equality of [monic polynomials](https://en.wikipedia.org/wiki/Monic_polynomial) $f(X)$ and $g(X)$ is equivalent to the equality of their logarithmic derivatives.[^2]
+This allows rewriting above equation as:
+
+$$
+\frac{f'_A(X)}{f_A(X)} = \frac{f'^{(m)}_B(X)}{f_B(X)}
+$$
+
+Using logarithmic derivatives for the equality check decreases the computational effort for both prover and verifier.
+Concretely, instead of four running products – one each for $f_A$, $f'_A$, $f_B$, and $f'^{(m)}_B$ – only two logarithmic derivatives are needed.
+Namely, considering once again list $A$ _containing_ duplicates, above equation can be written as:
+
+$$
+\sum_{i=0}^\ell \frac{1}{X - a_i} = \sum_{i=0}^n \frac{m_i}{X - b_i}
+$$
+
+To compute the sums, the lists $A$ and $B$ are base columns in the two respective tables.
+Additionally, the lookup multiplicity is recorded explicitly in a base column of the lookup table.
+
+## Example
+
+In Table A:
+
+| base column A | extension column A: logarithmic derivative                           |
+|--------------:|:---------------------------------------------------------------------|
+|             0 | $\frac{1}{\alpha - 0}$                                               |
+|             2 | $\frac{1}{\alpha - 0} + \frac{1}{\alpha - 2}$                        |
+|             2 | $\frac{1}{\alpha - 0} + \frac{2}{\alpha - 2}$                        |
+|             1 | $\frac{1}{\alpha - 0} + \frac{2}{\alpha - 2} + \frac{1}{\alpha - 1}$ |
+|             2 | $\frac{1}{\alpha - 0} + \frac{3}{\alpha - 2} + \frac{1}{\alpha - 1}$ |
+
+And in Table B:
+
+| base column B | multiplicity | extension column B: logarithmic derivative                           |
+|--------------:|-------------:|:---------------------------------------------------------------------|
+|             0 |            1 | $\frac{1}{\alpha - 0}$                                               |
+|             1 |            1 | $\frac{1}{\alpha - 0} + \frac{1}{\alpha - 1}$                        |
+|             2 |            3 | $\frac{1}{\alpha - 0} + \frac{1}{\alpha - 1} + \frac{3}{\alpha - 2}$ |
+
+It is possible to establish a subset relation by skipping over certain elements when computing the logarithmic derivative.
+The logarithmic derivative must incorporate the same elements with the same multiplicity in both tables.
+Otherwise, the Lookup Argument will fail.
+
+An example for a Lookup Argument can be found between the [Program Table](program-table.md) and the [Processor Table](processor-table.md#extension-colums).
+
+---
+
+[^1]: The lookup table may represent a mapping from one or more “input” elements to one or more “output” elements – see “[Compressing Multiple Elements](table-linking.md#compressing-multiple-elements).”
+
+[^2]: See Lemma 3 in [this paper](https://eprint.iacr.org/2022/1530.pdf) for a proof.