diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/README.md b/barretenberg/cpp/src/barretenberg/translator_vm/README.md new file mode 100644 index 000000000000..2255dec4ddd9 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/translator_vm/README.md @@ -0,0 +1,1446 @@ +# The Translator Circuit + +> **Warning**: This document provides a technical overview of the Translator Circuit used in the Goblin Plonk proving system. It is intended for understanding the design and optimizations. The code is the source of truth for implementation specifics. + +## Table of Contents + +1. [Overview](#overview) +2. [High-Level Statement](#high-level-statement) +3. [Architecture and Constants](#architecture-and-constants) +4. [Witness Trace Structure](#witness-trace-structure) +5. [Interleaving: The Key Optimization](#interleaving-the-key-optimization) +6. [Witness Generation and Proving Key Construction](#witness-generation-and-proving-key-construction) +7. [Translator Relations](#translator-relations) + +--- + +## Overview + +The Translator circuit is a critical component of the Goblin Plonk proving system in Aztec. It serves as a bridge between the Mega and ECCVM circuits. + +| Curve | Base Field | Scalar Field | Usage | +| -------- | -------------- | -------------- | ----------------------------------------- | +| BN254 | $\mathbb{F}_q$ | $\mathbb{F}_r$ | Used in Mega circuits | +| Grumpkin | $\mathbb{F}_r$ | $\mathbb{F}_q$ | Used in ECCVM for efficient EC operations | + +When proving recursive circuits with Mega circuit builder, we accumulate elliptic curve operations in an `EccOpQueue`. Proving these ECC operations is delegated to the ECCVM circuit, which operates over the Grumpkin curve. However, the same operations have different representations in the two circuits because: + +- Mega circuit operates over the BN254 scalar field $\mathbb{F}_r$ so elements in $\mathbb{F}_q$ are non-native (i.e., since $q > r$ they need to be decomposed into limbs in $\mathbb{F}_r$) +- ECCVM operates over the Grumpkin scalar field $\mathbb{F}_q$ so elements in $\mathbb{F}_q$ (as well as $\mathbb{F}_r$) are circuit native + +For example, consider the operation $(z \cdot P)$ where $P \equiv (P_x, P_y) \in \mathbb{F}_q^2$ is a point on the curve and $z \in \mathbb{F}_r$ is a scalar. The ECCVM arithmetisation represents this operation (in 1 row) as: + +| Opcode | $x$-coordinate | $y$-coordinate | Scalar $z_1$ | Scalar $z_2$ | Full scalar $z$ | +| ------ | -------------- | -------------- | ------------ | ------------ | --------------- | +| `MUL` | $P_x$ | $P_y$ | $z_1$ | $z_2$ | $z$ | +| | | | | | | + +The Mega circuit arithmetisation represents the same operation (in 2 rows) as: + +| Column 1 | Column 2 | Column 3 | Column 4 | +| -------- | -------------------- | -------------------- | -------------------- | +| `MUL` | $P_{x, \textsf{lo}}$ | $P_{x, \textsf{hi}}$ | $P_{y, \textsf{lo}}$ | +| $0$ | $P_{y, \textsf{hi}}$ | $z_1$ | $z_2$ | +| | | | | + +where $P_x = (P_{x, \textsf{lo}} + 2^{136} \cdot P_{x, \textsf{hi}}), \ P_y = (P_{y, \textsf{lo}} + 2^{136} \cdot P_{y, \textsf{hi}})$ and the scalar $z = (z_1 + 2^{128} \cdot z_2)$. Note that the limbs $P_{x/y, \textsf{lo}}, P_{x/y, \textsf{hi}}$ are elements in $\mathbb{F}_r$. + +We need to prove that these two representations are consistent, i.e., that the polynomial evaluations computed in the ECCVM circuit (over $\mathbb{F}_q$) match those computed in the Mega circuit (over $\mathbb{F}_r$). +The Translator circuit is a custom circuit designed to solve this problem. It: + +1. **Receives** the ECC op queue in Mega arithmetisation and the batched polynomial evaluation problem from ECCVM (operating over $\mathbb{F}_q$), +2. **Computes** the batched polynomial evaluation using non-native field arithmetic in $\mathbb{F}_r$ and, +3. **Verifies** that the result matches the evaluation provided by ECCVM. + +## High-Level Statement + +The Translator proves that the ECCVM's batched polynomial evaluation of the ECC operations is computed correctly. +Given: + +- A sequence of `UltraOp` operations from the `EccOpQueue` (each containing: $\text{op}, P_x, P_y, z_1, z_2$) +- An evaluation challenge $x \in \mathbb{F}_q$ +- A batching challenge $v \in \mathbb{F}_q$ + +Prove that: +$$\boxed{\text{accumulator}_{\text{final}} = \sum_{i=0}^{n-1} x^{n-1-i} \cdot \left( \text{op}_i + v \cdot P_x^{(i)} + v^2 \cdot P_y^{(i)} + v^3 \cdot z_1^{(i)} + v^4 \cdot z_2^{(i)} \right) \pmod{q}}$$ + +The batching via powers of $v$ combines the 5 values per operation into a single field element, and the powers of $x$ combine all operations into a single accumulator. + +Specifically, for each accumulation step (every 2 rows), prove: + +$$\text{acc}_{\text{curr}} = \text{acc}_{\text{prev}} \cdot x + \text{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 \pmod{q}$$ + +Note that we process the `EccOpQueue` in reverse order while computing the accumulator in steps: + +$$ +\begin{aligned} +\textcolor{orange}{\text{acc}_0} &= \textcolor{lightgrey}{0} \cdot x + \text{op}_{n-1} + P_x^{(n-1)} \cdot v + P_y^{(n-1)} \cdot v^2 + z_1^{(n-1)} \cdot v^3 + z_2^{(n-1)} \cdot v^4 \\ +\textcolor{lightgreen}{\text{acc}_1} &= \textcolor{orange}{\text{acc}_0} \cdot x + \text{op}_{n-2} + P_x^{(n-2)} \cdot v + P_y^{(n-2)} \cdot v^2 + z_1^{(n-2)} \cdot v^3 + z_2^{(n-2)} \cdot v^4 \\ +\textcolor{skyblue}{\text{acc}_2} &= \textcolor{lightgreen}{\text{acc}_1} \cdot x + \text{op}_{n-3} + P_x^{(n-3)} \cdot v + P_y^{(n-3)} \cdot v^2 + z_1^{(n-3)} \cdot v^3 + z_2^{(n-3)} \cdot v^4 \\ +&\ \ \vdots \\ +\textcolor{brown}{\text{acc}_{n-2}} &= \textcolor{grey}{\text{acc}_{n-3}} \cdot x + \text{op}_1 + P_x^{(1)} \cdot v + P_y^{(1)} \cdot v^2 + z_1^{(1)} \cdot v^3 + z_2^{(1)} \cdot v^4 \\ +\textcolor{violet}{\text{acc}_{n-1}} &= \textcolor{brown}{\text{acc}_{n-2}} \cdot x + \text{op}_0 + P_x^{(0)} \cdot v + P_y^{(0)} \cdot v^2 + z_1^{(0)} \cdot v^3 + z_2^{(0)} \cdot v^4 \\ +\end{aligned} +$$ + +The final accumulator value $\textcolor{violet}{\text{acc}_{n-1}}$ is what we need to verify against the ECCVM's output. +Note that the "previous" accumulator for the _last_ operation must be 0. + +**Method:** Since we cannot directly compute in $\mathbb{F}_q$ using $\mathbb{F}_r$ arithmetic (as $q \neq r$, and in fact $q > r$), we use non-native field arithmetic. Similar to the technique in [bigfield](../stdlib/primitives/bigfield/README.md), we prove the equation holds in integers: + +$$\text{acc}_{\text{prev}} \cdot x + \text{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 - \text{quotient} \cdot q - \text{acc}_{\text{curr}} = 0$$ + +We verify this by proving the equation holds: + +1. modulo $2^{272}$ (via 68-bit limb arithmetic split into two 136-bit checks) +2. modulo $r$ (natively in $\mathbb{F}_r$) +3. with range constraints on all limbs (prevents overflow/underflow) + +By the Chinese Remainder Theorem, since $2^{272} \cdot r > 2^{514}$ exceeds the maximum possible value, the equation must hold in integers, and thus modulo $q$. More details on this relation are in [RELATIONS.md](RELATIONS.md#non-native-field-relations). + +## Witness Trace Structure + +The Translator circuit has 81 witness columns, organized into: + +- 4 columns: `EccOpQueue` transcript ($\texttt{op}, P_x, P_y, z_1, z_2$ encoded across 2 rows) +- 13 columns: Limb decompositions (68-bit limbs for non-native arithmetic) +- 64 columns: Microlimb decompositions (14-bit microlimbs for range constraints) + +The circuit operates on a 2-row cycle structure. Each `EccOpQueue` entry occupies exactly 2 rows: + +- Row $2i$ (Even rows): Computation rows where the non-native field relation is actively checked +- Row $2i+1$ (Odd rows): Data storage rows that hold values accessed via shifts + +While enforcing constraints on the even rows, we can access values from the "next" row (which is odd) using shifted column polynomials. +As hinted earlier, the "previous" accumulator value needed for computation is stored at odd row $(2i+1)$. +This value becomes the "current" accumulator for the next even row $(2i+2)$: + +| Operation index | $0$ | $1$ | $\quad \dots \quad$ | $(n-2)$ | $(n-1)$ | +| -------------------- | -------------------------------------- | ------------------------------------- | ------------------- | ---------------------------------------- | ------------------------------------ | +| Current accumulator | $\textcolor{violet}{\text{acc}_{n-1}}$ | $\textcolor{brown}{\text{acc}_{n-2}}$ | $\quad \dots \quad$ | $\textcolor{lightgreen}{\text{acc}_{1}}$ | $\textcolor{orange}{\text{acc}_{0}}$ | +| Previous accumulator | $\textcolor{brown}{\text{acc}_{n-2}}$ | $\textcolor{grey}{\text{acc}_{n-3}}$ | $\quad \dots \quad$ | $\textcolor{orange}{\text{acc}_{0}}$ | $0$ | +| | | | | | | + +#### 1. EccOpQueue Transcript Columns (4 columns) + +These columns directly represent the EccOpQueue transcript: + +| Column Name | Even Row $(2i)$ | Odd Row $(2i+1)$ | Description | +| ----------- | -------------------------------- | ---------------------------- | ------------------------------------------------------------------ | +| `OP` | $\texttt{op} \in \{0, 3, 4, 8\}$ | 0 (no-op) | Opcode (the type of elliptic curve operation) | +| `X_LO_Y_HI` | $P_{x,\text{lo}}$ (136 bits) | $P_{y,\text{hi}}$ (118 bits) | Low 136 bits of $x$-coordinate and high 118 bits of $y$-coordinate | +| `X_HI_Z_1` | $P_{x,\text{hi}}$ (118 bits) | $z_1$ (128 bits) | High 118 bits of $x$-coordinate and first scalar | +| `Y_LO_Z_2` | $P_{y,\text{lo}}$ (136 bits) | $z_2$ (128 bits) | Low 136 bits of $y$-coordinate and second scalar | +| | | | | + +**Encoding scheme**: Point coordinates $P_x$ and $P_y$ are each 254 bits, split as: + +- $P_x = (P_{x,\text{hi}}$ (118 bits) $\|$ $P_{x,\text{lo}}$ (136 bits) $)$ +- $P_y = (P_{y,\text{hi}}$ (118 bits) $\|$ $P_{y,\text{lo}}$ (136 bits) $)$ + +#### 2. Limb Decomposition Columns (13 columns) + +These columns store finer-grained limb decompositions for non-native arithmetic: + +| Column Group | Even Row $(2i)$ | Odd Row $(2i+1)$ | Bits | Purpose | +| ----------------------------- | --------------------- | --------------------- | ------ | ---------------------------------------- | +| `P_X_LOW_LIMBS` | $P_{x,0}^{\text{lo}}$ | $P_{x,1}^{\text{lo}}$ | 68 | Limbs 0 & 1 of $P_{x}$ | +| `P_X_HIGH_LIMBS` | $P_{x,0}^{\text{hi}}$ | $P_{x,1}^{\text{hi}}$ | 68, 50 | Limbs 2 & 3 of $P_{x}$ | +| `P_Y_LOW_LIMBS` | $P_{y,0}^{\text{lo}}$ | $P_{y,1}^{\text{lo}}$ | 68 | Limbs 0 & 1 of $P_{y}$ | +| `P_Y_HIGH_LIMBS` | $P_{y,0}^{\text{hi}}$ | $P_{y,1}^{\text{hi}}$ | 68, 50 | Limbs 2 & 3 of $P_{y}$ | +| `Z_LOW_LIMBS` | $z_{1,0}$ | $z_{2,0}$ | 68 | Low limbs of $z_1$ and $z_2$ | +| `Z_HIGH_LIMBS` | $z_{1,1}$ | $z_{2,1}$ | 60 | High limbs of $z_1$ and $z_2$ | +| `ACCUMULATORS_BINARY_LIMBS_0` | $a_0^{\text{curr}}$ | $a_0^{\text{prev}}$ | 68 | Limb 0 of current/previous accumulator | +| `ACCUMULATORS_BINARY_LIMBS_1` | $a_1^{\text{curr}}$ | $a_1^{\text{prev}}$ | 68 | Limb 1 of current/previous accumulator | +| `ACCUMULATORS_BINARY_LIMBS_2` | $a_2^{\text{curr}}$ | $a_2^{\text{prev}}$ | 68 | Limb 2 of current/previous accumulator | +| `ACCUMULATORS_BINARY_LIMBS_3` | $a_3^{\text{curr}}$ | $a_3^{\text{prev}}$ | 50 | Limb 3 of current/previous accumulator | +| `QUOTIENT_LOW_BINARY_LIMBS` | $q_0$ | $q_1$ | 68 | Limbs 0 & 1 of quotient $\mathcal{Q}$ | +| `QUOTIENT_HIGH_BINARY_LIMBS` | $q_2$ | $q_3$ | 68, 52 | Limbs 2 & 3 of quotient $\mathcal{Q}$ | +| `RELATION_WIDE_LIMBS` | $c^{\text{lo}}$ | $c^{\text{hi}}$ | 84 | Carry/overflow from mod $2^{136}$ checks | + +**Key insight**: The accumulator columns demonstrate the shift mechanism: + +- Even row stores $a^{\text{curr}}$ (result of current computation) +- Odd row stores what will become $a^{\text{prev}}$ (input to next computation) +- Via shifts, even row $2i$ reads odd row $2i+1$ to get "previous" values + +#### 3. Range Constraint Microlimb Columns (64 columns) + +Each limb is further decomposed into 14-bit microlimbs for range checking. Each 68-bit limb has 5 microlimbs (14 bits each) plus a "tail" microlimb that enforces tight range constraints. The columns are organized as follows: + +| Column Group | Even Row $(2i)$ | Odd Row $(2i+1)$ | +| ---------------------------------------------- | -------------------------------------------------------- | --------------------------------------------------------- | +| Coordinate $P_x$ microlimbs | | | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_0` | $P_{x,0}[0]$ | $P_{x,1}[0]$ | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_1` | $P_{x,0}[1]$ | $P_{x,1}[1]$ | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_2` | $P_{x,0}[2]$ | $P_{x,1}[2]$ | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_3` | $P_{x,0}[3]$ | $P_{x,1}[3]$ | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_4` | $P_{x,0}[4]$ | $P_{x,1}[4]$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_0` | $P_{x,2}[0]$ | $P_{x,3}[0]$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_1` | $P_{x,2}[1]$ | $P_{x,3}[1]$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_2` | $P_{x,2}[2]$ | $P_{x,3}[2]$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_3` | $P_{x,2}[3]$ | $P_{x,3}[3]$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_4` | $P_{x,2}[4]$ | $\textcolor{yellow}{P_{x,3}[\textsf{tail}]}$ (reassigned) | +| Coordinate $P_y$ microlimbs | | | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_0` | $P_{y,0}[0]$ | $P_{y,1}[0]$ | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_1` | $P_{y,0}[1]$ | $P_{y,1}[1]$ | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_2` | $P_{y,0}[2]$ | $P_{y,1}[2]$ | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_3` | $P_{y,0}[3]$ | $P_{y,1}[3]$ | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_4` | $P_{y,0}[4]$ | $P_{y,1}[4]$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_0` | $P_{y,2}[0]$ | $P_{y,3}[0]$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_1` | $P_{y,2}[1]$ | $P_{y,3}[1]$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_2` | $P_{y,2}[2]$ | $P_{y,3}[2]$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_3` | $P_{y,2}[3]$ | $P_{y,3}[3]$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_4` | $P_{y,2}[4]$ | $\textcolor{yellow}{P_{y,3}[\textsf{tail}]}$ (reassigned) | +| Coordinate $z_1$ and $z_2$ microlimbs | | | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_0` | $z_{1,0}[0]$ | $z_{2,0}[0]$ | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_1` | $z_{1,0}[1]$ | $z_{2,0}[1]$ | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_2` | $z_{1,0}[2]$ | $z_{2,0}[2]$ | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_3` | $z_{1,0}[3]$ | $z_{2,0}[3]$ | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_4` | $z_{1,0}[4]$ | $z_{2,0}[4]$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_0` | $z_{1,1}[0]$ | $z_{2,1}[0]$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_1` | $z_{1,1}[1]$ | $z_{2,1}[1]$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_2` | $z_{1,1}[2]$ | $z_{2,1}[2]$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_3` | $z_{1,1}[3]$ | $z_{2,1}[3]$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_4` | $z_{1,1}[4]$ | $z_{2,1}[4]$ | +| Current and previous accumulator microlimbs | | | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_0` | $a_{0}^{\text{curr}}[0]$ | $a_{1}^{\text{curr}}[0]$ | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_1` | $a_{0}^{\text{curr}}[1]$ | $a_{1}^{\text{curr}}[1]$ | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_2` | $a_{0}^{\text{curr}}[2]$ | $a_{1}^{\text{curr}}[2]$ | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_3` | $a_{0}^{\text{curr}}[3]$ | $a_{1}^{\text{curr}}[3]$ | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_4` | $a_{0}^{\text{curr}}[4]$ | $a_{1}^{\text{curr}}[4]$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_0` | $a_{2}^{\text{curr}}[0]$ | $a_{3}^{\text{curr}}[0]$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_1` | $a_{2}^{\text{curr}}[1]$ | $a_{3}^{\text{curr}}[1]$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_2` | $a_{2}^{\text{curr}}[2]$ | $a_{3}^{\text{curr}}[2]$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_3` | $a_{2}^{\text{curr}}[3]$ | $a_{3}^{\text{curr}}[3]$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_4` | $a_{2}^{\text{curr}}[4]$ | $\textcolor{yellow}{a_{3}[\textsf{tail}]}$ (reassigned) | +| Quotient microlimbs | | | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_0` | $q_{0}[0]$ | $q_{1}[0]$ | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_1` | $q_{0}[1]$ | $q_{1}[1]$ | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_2` | $q_{0}[2]$ | $q_{1}[2]$ | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_3` | $q_{0}[3]$ | $q_{1}[3]$ | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_4` | $q_{0}[4]$ | $q_{1}[4]$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_0` | $q_{2}[0]$ | $q_{3}[0]$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_1` | $q_{2}[1]$ | $q_{3}[1]$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_2` | $q_{2}[2]$ | $q_{3}[2]$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_3` | $q_{2}[3]$ | $q_{3}[3]$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_4` | $q_{2}[4]$ | $\textcolor{yellow}{q_{3}[\textsf{tail}]}$ (reassigned) | +| Carry microlimbs | | | +| `RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_0` | $c^{\text{lo}}[0]$ | $c^{\text{hi}}[0]$ | +| `RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_1` | $c^{\text{lo}}[1]$ | $c^{\text{hi}}[1]$ | +| `RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_2` | $c^{\text{lo}}[2]$ | $c^{\text{hi}}[2]$ | +| `RELATION_WIDE_LIMBS_RANGE_CONSTRAINT_3` | $c^{\text{lo}}[3]$ | $c^{\text{hi}}[3]$ | +| Tail microlimbs | | | +| `P_X_LOW_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{P_{x,0}[\textsf{tail}]}$ | $\textcolor{yellow}{P_{x,1}[\textsf{tail}]}$ | +| `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{P_{x,2}[\textsf{tail}]}$ | $c^{\text{lo}}[4]$ (reassigned) | +| `P_Y_LOW_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{P_{y,0}[\textsf{tail}]}$ | $\textcolor{yellow}{P_{y,1}[\textsf{tail}]}$ | +| `P_Y_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{P_{y,2}[\textsf{tail}]}$ | $c^{\text{hi}}[4]$ (reassigned) | +| `Z_LOW_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{z_{1,0}[\textsf{tail}]}$ | $\textcolor{yellow}{z_{2,0}[\textsf{tail}]}$ | +| `Z_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{z_{1,1}[\textsf{tail}]}$ | $\textcolor{yellow}{z_{2,1}[\textsf{tail}]}$ | +| `ACCUMULATOR_LOW_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{a_{0}^{\text{curr}}[\textsf{tail}]}$ | $\textcolor{yellow}{a_{1}^{\text{curr}}[\textsf{tail}]}$ | +| `ACCUMULATOR_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{a_{2}^{\text{curr}}[\textsf{tail}]}$ | $c^{\text{lo}}[5]$ (reassigned) | +| `QUOTIENT_LOW_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{q_{0}[\textsf{tail}]}$ | $\textcolor{yellow}{q_{1}[\textsf{tail}]}$ | +| `QUOTIENT_HIGH_LIMBS_RANGE_CONSTRAINT_TAIL` | $\textcolor{yellow}{q_{2}[\textsf{tail}]}$ | $c^{\text{hi}}[5]$ (reassigned) | +| | | | + +The tail microlimbs (shown in yellow) enforce tight range constraints by ensuring top limbs use exactly the required number of bits (explained in the Decomposition Relation section of [RELATIONS.md](RELATIONS.md)). + +**Column reuse optimization:** Some columns are reassigned in odd rows to hold tail microlimbs for limbs that don't need all 5 microlimbs. For example, limb $P_{x, 3}$ is only 50 bits (= 3×14 + 8), requiring only 4 microlimbs. The 5th microlimb column `P_X_HIGH_LIMBS_RANGE_CONSTRAINT_4` at odd rows is therefore reassigned to hold the tail microlimb for $P_{x,3}$ (and carry values $c^{\text{lo}}[4]$, $c^{\text{hi}}[4]$, etc.). + +### Virtual Columns + +Some columns are "virtual" and not explicitly stored in the witness trace. Instead, they are computed on-the-fly during relation evaluation using existing columns. These include: + +- Interleaved columns for range constraint microlimbs (computed from the physical microlimb columns) +- Sorted (ordered) columns for range constraint microlimbs (computed by sorting the physical microlimb columns) + +### Mini-Circuit Layout + +The mini-circuit layout is illustrated below: + +- The first 4 columns represent the `EccOpQueue` transcript +- The next 13 columns represent limb decompositions +- The last 64 columns represent microlimb decompositions +- Let $n$ = total number of rows in the mini-circuit +- Let $r_{\textsf{start}}$ = number of rows for randomness at start +- Let $r_{\textsf{end}}$ = number of rows for randomness at the end +- Let $z_1$ = number of initial no-op rows (to ensure column polynomials are shiftable) + +Color coding in the diagram: + +- Purple boxes ($\textcolor{violet}{\textsf{purple}}$): Zero values or initial values + - For all columns: initial no-op row contains zeros + - For non-OP columns (13 limb + 64 microlimb): end randomness region initially contain zeros, later overwritten with random values for ZK sumcheck +- Grey boxes ($\textcolor{grey}{\textsf{grey}}$): Random values (no-op) in the 4 OP queue columns only + - These remain as random values from the random op processing + - Serve Merge Protocol ZK hiding +- Orange boxes ($\textcolor{orange}{\textsf{orange}}$): Main operation rows + - Contains actual ECC operation data for circuit computation + +$$ +\begin{array}{rlllll} +z_1 +& +\overbrace{ + \textcolor{violet}{ + \boxed{ + \hspace{0.95cm} + } + } +}^{4} +& +\textsf{\scriptsize $\longleftarrow$ initial no-op} +& +\overbrace{ +\textcolor{violet}{ + \boxed{ + \hspace{1.45cm} + } +} +}^{13} +& +\overbrace{ +\textcolor{violet}{ + \boxed{ + \hspace{3.85cm} + } +} +}^{64} +\\[2pt] +r_{\textsf{start}} +& +\textcolor{grey}{ + \boxed{ + \begin{array}{c} + \hspace{0.6cm} + \\ + \end{array} + } +} +& +\textsf{\scriptsize $\longleftarrow$ start randomness} +& +\textcolor{violet}{ + \boxed{ + \begin{array}{c} + \hspace{1.1cm} + \\ + \end{array} + } +} +& +\textcolor{violet}{ + \boxed{ + \begin{array}{c} + \hspace{3.5cm} + \\ + \end{array} + } +} +\\ \\[-10pt] +n - r_{\textsf{start}} - r_{\textsf{end}} - z_1 & +\textcolor{orange}{ + \boxed{ + \begin{array}{c} + \hspace{0.6cm} + \\ \\ \\ \\ \\ \\ \\ + \end{array} + } +} +& +\textsf{\scriptsize $\longleftarrow$ main ops} +& +\textcolor{orange}{ + \boxed{ + \begin{array}{c} + \hspace{1.1cm} + \\ \\ \\ \\ \\ \\ \\ + \end{array} + } +} +& +\textcolor{orange}{ + \boxed{ + \begin{array}{c} + \hspace{3.5cm} + \\ \\ \\ \\ \\ \\ \\ + \end{array} + } +} +\\ \\[-10pt] +r_{\textsf{end}} +& +\textcolor{grey}{ + \boxed{ + \begin{array}{c} + \hspace{0.6cm} + \\ + \end{array} + } +} +& +\textsf{\scriptsize $\longleftarrow$ end randomness} +& +\textcolor{violet}{ + \boxed{ + \begin{array}{c} + \hspace{1.1cm} + \\ + \end{array} + } +} +& +\textcolor{violet}{ + \boxed{ + \begin{array}{c} + \hspace{3.5cm} + \\ + \end{array} + } +} +\end{array} +$$ + +In our implementation, mini-circuit size is $n = 2^{13}$. We have $z_1 = 2$ (one no-op at the start to ensure shiftability), $r_{\textsf{start}} = 6$ (rows for three random ops at start), and $r_{\textsf{end}} = 4$ (rows for two random ops at end). Thus, the number of main operation rows is $n - r_{\textsf{start}} - r_{\textsf{end}} - z_1 = 8180$. + +The random ops serve dual purposes for zero-knowledge: + +**1. Merge Protocol ZK** (Grey boxes in 4 OP columns): + +- The 3 random ops at start add random values to the 4 ECC op queue columns (tail kernel blinding, ops prepended) +- The 2 random ops at end add random values to the 4 ECC op queue columns (hiding kernel blinding, ops appended) +- Together these contribute 40 random coefficients (10 per wire) to hide merge protocol evaluations +- See [MERGE_PROTOCOL.md](../goblin/MERGE_PROTOCOL.md#zk-considerations) for the degree-of-freedom analysis + +**2. ZK Sumcheck Masking** (Initially purple, then filled with random for non-OP columns): + +- The last $r_{\textsf{end}} = 4$ rows align exactly with `NUM_DISABLED_ROWS_IN_SUMCHECK = 4` (denoted as $m$ in the Lagrange table below) +- For the 4 OP queue columns: random values remain from the random ops +- For the remaining 77 columns (13 limb + 64 microlimb): + - Initially filled with zeros during random op processing + - These zeros are overwritten with random field elements during proving key construction + - This masking hides polynomial evaluations in ZK sumcheck + +### Lagrange Polynomials (Precomputed) + +The circuit uses Lagrange polynomials to control which constraints are active: ($I_{\text{size}} = 16$ is the number of columns interleaved together) + +| Polynomial | Description | Active Rows | +| ------------------------------ | ----------------------------------------- | ----------------------------------------------------------------------------------------------- | +| `lagrange_first` | First row | $i = 0$ | +| `lagrange_real_last` | Last row in full circuit (before masking) | $i = 2^{17} - m \cdot I_{\text{size}} - 1$ | +| `lagrange_last` | Last row in full circuit | $i = 2^{17} - 1$ | +| `lagrange_masking` | Masking rows in full circuit | $i \in [2^{17} - m \cdot I_{\text{size}}, \ 2^{17})$ | +| `lagrange_mini_masking` | Masking rows in mini circuit | $i \in [z_1, \ z_1 + r_{\textsf{start}}) \cup [n - r_{\textsf{end}}, \ n)$ | +| `lagrange_even_in_minicircuit` | Even indices in real mini-circuit | $i \in \{u \ \| \ u \ \% \ 2 = 0, \ (z_1 + r_{\textsf{start}}) \leq u < n - r_{\textsf{end}}\}$ | +| `lagrange_odd_in_minicircuit` | Odd indices in real mini-circuit | $i \in \{u \ \| \ u \ \% \ 2 = 1, \ (z_1 + r_{\textsf{start}}) \leq u < n - r_{\textsf{end}}\}$ | +| `lagrange_last_in_minicircuit` | Last row in mini-circuit | $i = 8191$ (mini) | +| `lagrange_result_row` | Row containing final accumulator result | $i = (z_1 + r_{\textsf{start}})$ | +| `lagrange_last_in_minicircuit` | Last real row in mini-circuit | $i = (n - r_{\textsf{end}}) - 1$ | +| | | | + +## Interleaving: The Key Optimization + +The Translator must range-constrain approximately 64 different microlimb sets using permutation argument (and the delta range constraint). The permutation argument's degree equals $1 + \textsf{NUM\_COLS}$, where NUM_COLS is the number of columns being permuted: + +$$ +z_{\textsf{perm}}[i+1] \cdot \prod_{j=1}^{\textsf{NUM\_COLS}} (\textsf{ordered}[j] + \gamma) = +z_{\textsf{perm}}[i] \cdot \prod_{j=1}^{\textsf{NUM\_COLS}} (\textsf{interleaved}[j] + \gamma) +$$ + +The Problem: Permuting all ~64 microlimb columns simultaneously would require us to commit to all of them. Further, since the relation degree would be $1 + 64 = 65$, computing the sumcheck univariates could be a significant overhead for the prover. The prover would need to then commit to the univariates (instead of sending evaluations directly). + +The Solution: Interleave 16 logical columns into one virtual column, and create 4 such columns (plus 1 for the extra column). Each group can then perform an independent permutation check with degree $1 + 5 = 6$ (or 7 with Lagrange selector). This reduces the relation degree from 65 to 7. + +### Circuit Structure + +``` +Mini-circuit size: 2^13 = 8,192 rows (actual computation) +Full circuit size: 2^13 x 16 = 2^17 = 131,072 rows (after interleaving) +``` + +To compute the interleaved polynomials, we group 16 polynomials together and interleave their coefficients. Consider the following 16 polynomials each of size $n=2^{13}$ in the mini-circuit: + +$$ +\newcommand{\arraystretch}{1.2} +\begin{array}{|c|c|c|c|c|c|} +\hline +\textsf{index} & \textsf{poly 1} & \textsf{poly 2} & \textsf{poly 3} & \ldots & \textsf{poly 16} \\ +\hline +0 & \textcolor{skyblue}{a_0} & \textcolor{orange}{b_0} & \textcolor{lightgreen}{c_0} & \quad \ldots \quad & \textcolor{firebrick}{p_0} \\ +1 & \textcolor{skyblue}{a_1} & \textcolor{orange}{b_1} & \textcolor{lightgreen}{c_1} & \quad \ldots \quad & \textcolor{firebrick}{p_1} \\ +2 & \textcolor{skyblue}{a_2} & \textcolor{orange}{b_2} & \textcolor{lightgreen}{c_2} & \quad \ldots \quad & \textcolor{firebrick}{p_2} \\ +3 & \textcolor{skyblue}{a_3} & \textcolor{orange}{b_3} & \textcolor{lightgreen}{c_3} & \quad \ldots \quad & \textcolor{firebrick}{p_3} \\[5pt] +\vdots & \vdots & \vdots & \vdots & \ddots & \vdots \\[5pt] +n-1 & \textcolor{skyblue}{a_{n-1}} & \textcolor{orange}{b_{n-1}} & \textcolor{lightgreen}{c_{n-1}} & \quad \ldots \quad & \textcolor{firebrick}{p_{n-1}} \\ +\hline +\end{array} +\quad \longrightarrow \quad +\begin{array}{|c|c|c|} +\hline +\textsf{group} & \textsf{index} & \textsf{interleaved} \\ +\hline +0 & 0 & \textcolor{skyblue}{a_0} \\ +0 & 1 & \textcolor{orange}{b_0} \\ +0 & 2 & \textcolor{lightgreen}{c_0} \\ +\vdots & \vdots & \vdots \\[3pt] +0 & 15 & \textcolor{firebrick}{p_0} \\ \hline +1 & 16 & \textcolor{skyblue}{a_1} \\ +1 & 17 & \textcolor{orange}{b_1} \\ +1 & 18 & \textcolor{lightgreen}{c_1} \\ +\vdots & \vdots & \vdots \\[3pt] +1 & 31 & \textcolor{firebrick}{p_1} \\ \hline +\vdots & \vdots & \vdots \\ \hline +n-1 & 16n-16 & \textcolor{skyblue}{a_{n-1}} \\ +n-1 & 16n-15 & \textcolor{orange}{b_{n-1}} \\ +n-1 & 16n-14 & \textcolor{lightgreen}{c_{n-1}} \\ +\vdots & \vdots & \vdots \\[3pt] +n-1 & 16n-1 & \textcolor{firebrick}{p_{n-1}} \\ +\hline +\end{array} +$$ + +For 64 microlimb columns, we have 4 groups of 16 columns each, resulting in four interleaved polynomials each of size $16n = 2^{17}$. Note that the interleaved polynomials are not "physical" wires in the circuit trace: we refer to them as virtual polynomials. Each of these groups performs an independent permutation check: + +- Numerator: 4 interleaved wires + 1 extra = 5 terms +- Denominator: 5 ordered wires = 5 terms +- Degree: $1 + 5 = 6$ (or 7 with Lagrange) + +The permutation argument verifies that within each group, the interleaved values are a permutation of the ordered (sorted) values. Due to interleaving, the total circuit size increases 16×, requiring more zero-padding. Interleaving trades circuit size (inexpensive) for relation degree (expensive). The 16× size increase is acceptable given the 9× degree reduction. + +> **Effect on Commitment Scheme**: For polynomials $p_0, \dots, p_{15}$ of size $n$, the interleaved polynomial of size $16n$ is: +> $$p_{\textsf{interleaved}}(x) = \sum_{i=0}^{15} x^i \cdot p_{i}(x^{16})$$ +> The interleaved polynomials don't need to be committed explicitly; they can be opened (at, say $\gamma$) by using the commitments to the original polynomials and their evaluations (at $\gamma^{16}$). This is explained in more detail in the [Gemini](../commitment_schemes/gemini/README.md) documentation. + +## Witness Generation and Proving Key Construction + +This section details how the Translator circuit's witness polynomials are populated and how zero-knowledge is achieved through masking. + +### Overview + +Witness generation transforms the `EccOpQueue` from the Mega circuit into the 91 polynomials required by the Translator circuit: + +``` +Input: EccOpQueue (n operations) + Evaluation challenge x ∈ Fq + Batching challenge v ∈ Fq + +Output: 91 polynomials of size 2^17 + - 81 witness polynomials + - 5 ordered range constraint polynomials + - 4 interleaved range constraint polynomials (virtual) + - 1 precomputed extra numerator +``` + +**Note:** Witness generation happens in the **mini-circuit size** (2¹³ = 8,192 rows), then is expanded to **full circuit size** (2¹⁷ = 131,072 rows) through interleaving and zero-padding. + +### Step 1: Populate Transcript Polynomials + +The prover receives the `EccOpQueue` from the Mega circuit. Each entry contains: + +$$\texttt{UltraOp} = \{\texttt{op}, P_x, P_y, z_1, z_2\}$$ + +For operation $i$ at rows $2i$ (even) and $2i+1$ (odd), populate: + +**Even row ($2i$):** + +$$ +\begin{aligned} +\texttt{OP}[2i] &= \texttt{op}_i \\ +\texttt{X\_LO\_Y\_HI}[2i] &= P_{x,\text{lo}} = P_x \bmod 2^{136} \\ +\texttt{X\_HI\_Z\_1}[2i] &= P_{x,\text{hi}} = \lfloor P_x / 2^{136} \rfloor \\ +\texttt{Y\_LO\_Z\_2}[2i] &= P_{y,\text{lo}} = P_y \bmod 2^{136} +\end{aligned} +$$ + +**Odd row ($2i+1$):** + +$$ +\begin{aligned} +\texttt{OP}[2i+1] &= 0 \\ +\texttt{X\_LO\_Y\_HI}[2i+1] &= P_{y,\text{hi}} = \lfloor P_y / 2^{136} \rfloor \\ +\texttt{X\_HI\_Z\_1}[2i+1] &= z_1 \\ +\texttt{Y\_LO\_Z\_2}[2i+1] &= z_2 +\end{aligned} +$$ + +### Step 2: Compute Binary Limb Decompositions + +Each 136-bit transcript value is further decomposed into two 68-bit limbs. For $P_{x,\text{lo}}$: + +$$P_{x,\text{lo}} = P_{x,0}^{\text{lo}} + 2^{68} \cdot P_{x,1}^{\text{lo}}$$ + +where: + +- $P_{x,0}^{\text{lo}} = P_{x,\text{lo}} \bmod 2^{68}$ + +- $P_{x,1}^{\text{lo}} = \lfloor P_{x,\text{lo}} / 2^{68} \rfloor$ + +Even row ($2i$) limb assignments: + +$$ +\begin{aligned} +\texttt{P\_X\_LOW\_LIMBS}[2i] &= P_{x,0}^{\text{lo}} \\ +\texttt{P\_X\_HIGH\_LIMBS}[2i] &= P_{x,0}^{\text{hi}} \\ +\texttt{P\_Y\_LOW\_LIMBS}[2i] &= P_{y,0}^{\text{lo}} \\ +\texttt{P\_Y\_HIGH\_LIMBS}[2i] &= P_{y,0}^{\text{hi}} \\ +\texttt{Z\_LOW\_LIMBS}[2i] &= z_{1,0} \\ +\texttt{Z\_HIGH\_LIMBS}[2i] &= z_{1,1} +\end{aligned} +$$ + +Odd row ($2i+1$) limb assignments: + +$$ +\begin{aligned} +\texttt{P\_X\_LOW\_LIMBS}[2i+1] &= P_{x,1}^{\text{lo}} \\ +\texttt{P\_X\_HIGH\_LIMBS}[2i+1] &= P_{x,1}^{\text{hi}} \\ +\texttt{P\_Y\_LOW\_LIMBS}[2i+1] &= P_{y,1}^{\text{lo}} \\ +\texttt{P\_Y\_HIGH\_LIMBS}[2i+1] &= P_{y,1}^{\text{hi}} \\ +\texttt{Z\_LOW\_LIMBS}[2i+1] &= z_{2,0} \\ +\texttt{Z\_HIGH\_LIMBS}[2i+1] &= z_{2,1} +\end{aligned} +$$ + +### Step 3: Compute Accumulator and Quotient + +For each even row $2i$, compute the accumulator update and quotient. The accumulator evolves as: + +$$a^{\text{curr}} = a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 \pmod{q}$$ + +The current and the previous accumulators are decomposed into 4 limbs each: + +$$ +\begin{aligned} +a^{\text{curr}} &= +a_0^{\text{curr}} ++ +2^{68} \cdot a_1^{\text{curr}} ++ +2^{136} \cdot a_2^{\text{curr}} ++ +2^{204} \cdot a_3^{\text{curr}} +\\[5pt] +a^{\text{prev}} &= +a_0^{\text{prev}} ++ +2^{68} \cdot a_1^{\text{prev}} ++ +2^{136} \cdot a_2^{\text{prev}} ++ +2^{204} \cdot a_3^{\text{prev}} +\end{aligned} +$$ + +Since we're working in $\mathbb{F}_r$ (not $\mathbb{F}_q$), we must compute the quotient $\mathcal{Q}$ such that: + +$$a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 = \mathcal{Q} \cdot q + a^{\text{curr}}$$ + +$$ +\implies \mathcal{Q} = \left\lfloor \frac{a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4}{q} \right\rfloor +$$ + +The quotient is then decomposed into 4 limbs (68 + 68 + 68 + 52 bits): + +$$\mathcal{Q} = q_0 + 2^{68} \cdot q_1 + 2^{136} \cdot q_2 + 2^{204} \cdot q_3$$ + +**Carry computation:** The relation-wide limbs $c^{\text{lo}}$ and $c^{\text{hi}}$ (84 bits each) capture overflow from the mod $2^{136}$ checks: + +$$c^{\text{lo}} = \left\lfloor \frac{T_0 + 2^{68} \cdot T_1}{2^{136}} \right\rfloor, \quad c^{\text{hi}} = \left\lfloor \frac{c^{\text{lo}} + T_2 + 2^{68} \cdot T_3}{2^{136}} \right\rfloor$$ + +where $T_0, T_1, T_2, T_3$ are the limb contributions defined in [RELATIONS.md](RELATIONS.md). + +### Step 4: Microlimb Decomposition + +Each 68-bit limb is decomposed into five 14-bit microlimbs plus a tail microlimb for range tightening. For a general 68-bit limb $\ell$: + +$$\ell = \sum_{k=0}^{4} 2^{14k} \cdot m_k$$ + +where each $m_k \in [0, 2^{14})$ and $m_4 \in [0, 2^{12})$ (since $68 = 14 \times 4 + 12$). + +**Tail microlimb:** To enforce $m_4 < 2^{12}$, compute: + +$$m_{\text{tail}} = m_4 \cdot 2^{14-12} = m_4 \cdot 4$$ + +The decomposition relation enforces $m_{\text{tail}} \in [0, 2^{14})$, which implies $m_4 \in [0, 2^{12})$. For limbs with fewer bits, the tail microlimb is adjusted accordingly. + +- 50-bit limbs (top limb): $m_3 \in [0, 2^8) \implies$ tail shift is $2^{14-8} = 64$ +- 60-bit limbs (z high): $m_4 \in [0, 2^4)\implies$ tail shift is $2^{14-4} = 1024$ + +### Step 5: Construct Interleaved Polynomials + +The 64 microlimb columns are organized into 4 groups of 16 columns each. Each group is **interleaved** into a single polynomial at full circuit size. + +**Interleaving formula:** For group polynomials $\{p_0, p_1, \ldots, p_{15}\}$ each of mini-size $n = 2^{13}$: + +$$p_{\text{interleaved}}(x) = \sum_{j=0}^{15} x^j \cdot p_j(x^{16})$$ + +**In coefficient form:** Element at position $i \cdot 16 + j$ in the interleaved polynomial comes from row $i$ of polynomial $p_j$: + +$$p_{\text{interleaved}}[i \cdot 16 + j] = p_j[i] \quad \text{for } i \in [0, n), \ j \in [0, 16)$$ + +This expands the circuit from mini-size $2^{13}$ to full size $2^{17} = 2^{13} \times 16$. + +**Illustration:** We have a total of 64 microlimb columns, each with $n = 2^{13}$ rows (mini-circuit size). We illustrate the microlimb distribution and interleaving process below: + +1. Let $I_{\textsf{size}} = 16$ be the number of microlimb columns in one group. Since we have 64 microlimb columns, we will have 4 groups. + +2. Each group separates the microlimbs into circuit witnesses ($n-m$ rows in orange) and masking values ($m$ rows in gray). + +3. For each group, we interleave the microlimbs to create one interleaved polynomial of size $(n - m) \cdot I_{\textsf{size}}$ for circuit witnesses and $m \cdot I_{\textsf{size}}$ for masking values. + +$$ +\begin{array}{rllll} +n - m +& +\overbrace{ +\textcolor{orange}{ + \boxed{ + \begin{array}{ccccc} + \\ + \\ + \\ + & & W & & \\ + \\ + \\ + \\ + \end{array} + } +} +}^{I_{\textsf{size}}} +\ +\overbrace{ +\textcolor{orange}{ + \boxed{ + \begin{array}{ccccc} + \\ + \\ + \\ + & & W & & \\ + \\ + \\ + \\ + \end{array} + } +} +}^{I_{\textsf{size}}} +\ +\overbrace{ +\textcolor{orange}{ + \boxed{ + \begin{array}{ccccc} + \\ + \\ + \\ + & & W & & \\ + \\ + \\ + \\ + \end{array} + } +} +}^{I_{\textsf{size}}} +\ +\overbrace{ +\textcolor{orange}{ + \boxed{ + \begin{array}{ccccc} + \\ + \\ + \\ + & & W & & \\ + \\ + \\ + \\ + \end{array} + } +} +}^{I_{\textsf{size}}} +\\[2pt] +m +& +\textcolor{grey}{ + \boxed{ + \begin{array}{ccccc} + & & M & & \\ + \end{array} + } +} +\ +\textcolor{grey}{ + \boxed{ + \begin{array}{ccccc} + & & M & & \\ + \end{array} + } +} +\ +\textcolor{grey}{ + \boxed{ + \begin{array}{ccccc} + & & M & & \\ + \end{array} + } +} +\ +\textcolor{grey}{ + \boxed{ + \begin{array}{ccccc} + & & M & & \\ + \end{array} + } +} +\end{array} + +\xrightarrow[]{\textsf{interleaved polys}} + +\begin{array}{lllll} +I_1 \quad I_2 \quad I_3 \quad I_4 \\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +& +N - m \cdot I_{\textsf{size}} +\\ +\\[-10pt] +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +& +m \cdot I_{\textsf{size}} +\end{array} +$$ + +### Step 6: Construct Ordered (Sorted) Polynomials + +The permutation argument requires proving that the interleaved microlimbs equal the **sorted** microlimbs. The prover constructs 5 ordered polynomials by collecting microlimbs from all 64 columns, sorting them, and distributing across ordered polynomials with inserted step values. We first describe the mathematical setup and then illustrate the construction steps. + +**Constants:** + +- Mini-circuit size: $n = 2^{13} = 8{,}192$ +- Number of masked rows in mini-circuit: $m = 4$ +- Mini-circuit size without masking: $(n - m) = 8{,}188$ +- Number of interleaving groups: $G = 4$ +- Group size: $I_{\text{size}} = 16$ (polynomials per group) +- Full circuit size: $N := n \cdot I_{\text{size}} = 2^{17} = 131{,}072$ +- Circuit size without masking: $N_{\text{no-mask}} = N - m \cdot I_{\textsf{size}}$ +- Step sequence size: $N_{\text{steps}} = 5{,}462$ + +**Step sequence:** The sorted steps $\mathcal{S} = \{s_0, s_1, \ldots, s_{5461}\}$ where: +$$s_i = 3i \quad \text{for } i \in [0, 5461], \quad s_{5461} = 16{,}383 = 2^{14} - 1$$ + +This ensures coverage of all values in $[0, 2^{14})$ with max gap of 3. + +#### Step 6.1: Collect Microlimbs from Each Group + +For each group $g \in \{0, 1, 2, 3\}$, collect all microlimbs from its 16 polynomials: + +$$\mathcal{M}_g = \bigcup_{j=0}^{15} \Big\{ p_{g,j}[i] : i \in [0, (n-m)) \Big\}$$ + +where $p_{g,j}$ is the $j$-th polynomial in group $g$. Size of each group microlimb set: + +$$|\mathcal{M}_g| = 16 \times (n - m)$$ + +and total microlimbs across all groups: +$$|\mathcal{M}_0 \cup \mathcal{M}_1 \cup \mathcal{M}_2 \cup \mathcal{M}_3| = 64 \times (n - m).$$ + +#### Step 6.2: Determine Capacity for Each Ordered Polynomial + +Each ordered polynomial has size $N$ but must accommodate: + +1. Microlimbs from the circuit (actual witness values) +2. Step values $\mathcal{S}$ (for delta range constraint) + +**Capacity per ordered polynomial (for circuit microlimbs):** +$$C_{\text{capacity}} = N_{\text{no-mask}} - N_{\text{steps}} = N_{\text{no-mask}} - 5{,}462$$ + +This is the maximum number of witnesses each ordered polynomial can hold before adding step values. + +#### Step 6.3: Distribute Microlimbs to Ordered Polynomials + +For groups 0-3, construct `ordered_range_constraints_i` by: + +1. Collect microlimbs from group $g$: $\mathcal{M}_g$ +2. Take first $C_{\text{capacity}}$ elements (arbitrarily ordered at this point) +3. Add step values $\mathcal{S}$ +4. Sort the combined set + +Mathematically, for $g \in \{0, 1, 2, 3\}$: + +$$ +\text{ordered}[g]_{\text{unsorted}} = \begin{cases} +\mathcal{M}_g[k] & \text{if } k < C_{\text{capacity}} \\ +\mathcal{S}[k - C_{\text{capacity}}] & \text{if } C_{\text{capacity}} \leq k < N_{\text{no-mask}} \\ +0 & \text{if } k \geq N_{\text{no-mask}} \text{ (masking region)} +\end{cases} +$$ + +Then sort: +$$\text{ordered}[g] = \text{sort}(\text{ordered}[g]_{\text{unsorted}})$$ + +Overflow microlimbs: If $|\mathcal{M}_g| > C_{\text{capacity}}$, the excess microlimbs go to group 4: + +$$\mathcal{M}_{g,\text{overflow}} = \left\{ \mathcal{M}_g[k] : k \geq C_{\text{capacity}} \right\}$$ + +$$|\mathcal{M}_{g,\text{overflow}}| = |\mathcal{M}_g| - C_{\text{capacity}}$$ + +#### Step 6.4: Construct the 5th Ordered Polynomial + +The 5th ordered polynomial (`ordered_range_constraints_4`) collects all overflow: + +$$\mathcal{M}_{\text{overflow}} = \bigcup_{g=0}^{3} \mathcal{M}_{g,\text{overflow}}$$ + +Size of overflow: +$$|\mathcal{M}_{\text{overflow}}| = 4 \times |\mathcal{M}_{g,\text{overflow}}| = 4 \times (16 \times (n - m) - C_{\text{capacity}})$$ + +Then construct: + +$$ +\text{ordered}[4]_{\text{unsorted}} = \begin{cases} +\mathcal{M}_{\text{overflow}}[k] & \text{if } k < |\mathcal{M}_{\text{overflow}}| \\ +\mathcal{S}[k - |\mathcal{M}_{\text{overflow}}|] & \text{if } |\mathcal{M}_{\text{overflow}}| \leq k < |\mathcal{M}_{\text{overflow}}| + N_{\text{steps}} \\ +0 & \text{otherwise} +\end{cases} +$$ + +Then sort: +$$\text{ordered}[4] = \text{sort}(\text{ordered}[4]_{\text{unsorted}})$$ + +**Illustration:** We start with the 4 interleaved polynomials constructed earlier: + +1. First, we add an extra numerator polynomial $I_5$ containing the step values (shown in green, repeated 5 times) to enable the delta range constraint. + +2. The remainder of $I_5$ is filled with zero-padding (shown in violet) to match the size $N$ of the interleaved polynomials. + +3. In the four interleaved polynomials, we have circuit witness values (orange) and masking values (gray). We also show the overflow microlimbs that will go into the 5th ordered polynomial (smaller orange boxes). + +4. We then construct the ordered polynomials $O_1, \dots, O_5$ by adding the step values into each interleaved polynomial and sorting the witness values appropriately. + +5. The randomess in the masking region (gray) is redistributed to ensure that the multisets of the interleaved polynomials plus extra numerator equal the multisets of the ordered polynomials. Hence, the number of masking rows in each of the ordered polynomials is at least $\left\lfloor\frac{4 \cdot m \cdot I_{\textsf{size}}}{5}\right\rfloor$. The remainder of the rows in each ordered polynomial is filled with zero-padding. + +$$ +\begin{array}{rllll} +& I_1 \quad I_2 \quad I_3 \quad I_4 \\ +N - m \cdot I_{\textsf{size}} +& +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[60pt] +\end{array} +}} +\\ +\\[-10pt] +m \cdot I_{\textsf{size}} +& +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\end{array} + +\xrightarrow[]{\textsf{add extra numerator}} + +\begin{array}{lrrrrr} +I_1 \quad I_2 \quad I_3 \quad I_4 \\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\\ +\\[-10pt] +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\\ +\\[-10pt] +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-3pt]\\[-3pt] +\end{array} +}} +\end{array} + +\begin{array}{l} + I_5 \\ + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + s \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + s \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + s \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + s \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + s \\[1pt] + \end{array} + }} + \\ + \\[-13pt] + \textcolor{violet}{ + \boxed{ + \begin{array}{c} + \\ \\ z \\ \\[2pt] + \end{array} + }} +\end{array} + +\xrightarrow[]{\textsf{sort into ordered polys}} + + +\begin{array}{lrrrrr} +O_1 \quad O_2 \ \ O_3 \quad O_4 \\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\ +\textcolor{orange}{ +\boxed{ +\begin{array}{c} +\\ \\ \\ \\ \\ \\ \\[25pt] +\end{array} +}} +\\ +\\[-10pt] +\textcolor{lightgreen}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{lightgreen}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{lightgreen}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\ +\textcolor{lightgreen}{ +\boxed{ +\begin{array}{c} +\\[1pt] +\end{array} +}} +\\ +\\[-10pt] \hline\hline +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-6pt]\\[-6pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-6pt]\\[-6pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-6pt]\\[-6pt] +\end{array} +}} +\ +\textcolor{gray}{ +\boxed{ +\begin{array}{c} +\\[-6pt]\\[-6pt] +\end{array} +}} +\\ +\\[-10pt] +\textcolor{violet}{ +\boxed{ +\begin{array}{c} +\\[-2pt] +\end{array} +}} +\ +\textcolor{violet}{ +\boxed{ +\begin{array}{c} +\\[-2pt] +\end{array} +}} +\ +\textcolor{violet}{ +\boxed{ +\begin{array}{c} +\\[-2pt] +\end{array} +}} +\ +\textcolor{violet}{ +\boxed{ +\begin{array}{c} +\\[-2pt] +\end{array} +}} +\end{array} + +\begin{array}{l} + O_5 \\ + \textcolor{orange}{ + \boxed{ + \begin{array}{c} + \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{orange}{ + \boxed{ + \begin{array}{c} + \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{orange}{ + \boxed{ + \begin{array}{c} + \\[1pt] + \end{array} + }} + \\ + \\[-10pt] + \textcolor{orange}{ + \boxed{ + \begin{array}{c} + \\[1pt] + \end{array} + }} + \\ + \\[-12pt] + \textcolor{lightgreen}{ + \boxed{ + \begin{array}{c} + \\[1pt] + \end{array} + }} + \\ + \\[-13pt] + \textcolor{violet}{ + \boxed{ + \begin{array}{c} + \\[10pt] + \end{array} + }} + \\ + \\[-10pt] \hline\hline + \textcolor{gray}{ + \boxed{ + \begin{array}{c} + \\[-6pt]\\[-6pt] + \end{array} + }} + & + \longleftarrow {\scriptsize \textsf{randomness of size}} \left\lfloor\frac{4 \cdot m \cdot I_{\textsf{size}}}{5}\right\rfloor + \\ + \\[-10pt] + \textcolor{violet}{ + \boxed{ + \begin{array}{c} + \\[-2pt] + \end{array} + }} +\end{array} +$$ + +> In our case, we have $m=4$ and $I_{\textsf{size}}=16$ which results in $(m \cdot I_{\textsf{size}}) = 64$ masked rows in each interleaved polynomials. Thus, each ordered polynomial will have at least $\left\lfloor\frac{4 \cdot 64}{5}\right\rfloor = 51$ masked rows. The remainder masked rows are added to the respective ordered polynomials. The masking rows in each ordered polynomial are padded with zero values to ensure the multiset equality holds. +> +> As illustrated, the two sets of interleaved and ordered polynomials satisfy the multiset equality: +> $$\bigcup_{i=1}^5 I_i = \bigcup_{i=1}^5 O_i.$$ + +### Step 7: Zero-Knowledge Masking + +To achieve zero-knowledge, the translator uses two independent masking mechanisms: + +#### ZK Sumcheck Masking (Non-OP-Queue Wires) + +To hide polynomial evaluations used in ZK sumcheck, random values are added to the last $m = r_{\textsf{end}} = 4$ rows of the mini-circuit for all non-OP-queue wires (13 limb decomposition columns, 64 microlimb columns). + +1. During random op processing, these columns are initially filled with zeros +2. During proving key construction, these zeros are overwritten with random field elements +3. The Lagrange polynomial `lagrange_mini_masking` marks these last 4 rows as masked + +#### Permutation Argument Masking (Ordered Polynomials) + +For the permutation argument over microlimbs, a separate masking mechanism is used. +For each of the witness polynomials, the masking region is defined as the last $m = r_{\textsf{end}}$ rows of the mini-circuit size, indexed as: + +$$[n - m, \ n).$$ + +After interleaving, the 4 interleaved polynomials have random values at positions: + +$$[N - m \cdot I_{\textsf{size}}, \ N).$$ + +Where $m = r_{\textsf{end}} = 4$ (the same 4 rows used for ZK sumcheck masking). + +#### Redistributing Randomness to Ordered Polynomials + +The ordered polynomials must be committed (unlike interleaved polynomials, which are virtual). To maintain zero-knowledge, the prover redistributes the random values from the 4 interleaved to the 5 ordered polynomials. As illustrated above, each ordered polynomial receives approximately an equal share of the randomness from the interleaved polynomials. The total number of random values in the interleaved polynomials: + +$$M = 4 \cdot m \cdot I_{\textsf{size}}.$$ + +To distribute these $M$ random values to 5 ordered polynomials, each ordered polynomial receives $\left\lfloor\frac{M}{5}\right\rfloor$ random values in its masking region. The remaining random values (if $M$ is not divisible by 5) are distributed one per ordered polynomial starting from the first. Further, since + +$$ +\underbrace{(m \cdot I_{\textsf{size}})}_{\textsf{size of masking region}} > +\underbrace{\left\lfloor \left(\frac{4}{5} \cdot m \cdot I_{\textsf{size}}\right) \right\rfloor}_{\textsf{size of randomness in ordered polys}}, +$$ + +the remaining positions in the ordered masking region are filled with zeros. + +**Note:** The same random values appear in both interleaved and ordered polynomials (just at different positions within the masking region). This is why the $\beta \cdot L_{\text{mask}}$ term is needed in the permutation relation - see [RELATIONS.md](RELATIONS.md#permutation-relation-mathematical-specification) for details. + +Some positions in the ordered masking region contain random values, others contain zeros. The `ordered_extra_range_constraints_numerator` compensates for these zeros in the permutation check. + +### Step 8: Precomputed Polynomials + +Several polynomials are precomputed and independent of the witness. + +#### Lagrange Polynomials + +Define row-specific selectors: + +$$ +\begin{aligned} +\texttt{lagrange\_first}[i] &= \begin{cases} 1 & i = 0 \\ 0 & \text{otherwise} \end{cases} \\ +\texttt{lagrange\_last}[i] &= \begin{cases} 1 & i = 2^{17} - 1 \\ 0 & \text{otherwise} \end{cases} \\ +\texttt{lagrange\_even}[i] &= \begin{cases} 1 & i \in [0, 2^{13}), \ i \text{ even} \\ 0 & \text{otherwise} \end{cases} \\ +\texttt{lagrange\_odd}[i] &= \begin{cases} 1 & i \in [0, 2^{13}), \ i \text{ odd} \\ 0 & \text{otherwise} \end{cases} +\end{aligned} +$$ + +#### Ordered Extra Range Constraints Numerator + +This polynomial contains the "step values" repeated to balance the permutation: + +$$\texttt{ordered\_extra}[i \cdot 5 + j] = \text{sorted\_steps}[i] \quad \text{for } i \in [0, 5462), \ j \in [0, 5)$$ + +where $\text{sorted\_steps} = \{0, 3, 6, 9, \ldots, 16383\}$. + +This ensures the multisets balance: + +- **Numerator:** 4 interleaved + 1 extra (with 5 copies of each step value) +- **Denominator:** 5 ordered (each with 1 copy of each step value) + +## Translator Relations + +Constraints for the translator VM are specified in [RELATIONS.md](RELATIONS.md). diff --git a/barretenberg/cpp/src/barretenberg/translator_vm/RELATIONS.md b/barretenberg/cpp/src/barretenberg/translator_vm/RELATIONS.md new file mode 100644 index 000000000000..6f6f5e5472de --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/translator_vm/RELATIONS.md @@ -0,0 +1,699 @@ +# Translator Relations + +The translator VM enforces several relations/constraints to ensure the correctness of non-native field arithmetic and other operations. The primary relation is the **Non-Native Field Relation**, which verifies that certain accumulations hold in a non-native field (the BN254 base field $\mathbb{F}_q$) while operating in the native field (the BN254 scalar field $\mathbb{F}_r$). + +Since we follow a two-row trace structure, some relations are only active on even rows, while others are only active on odd rows. Below is a summary of the relations and their activation patterns. + +| Constraint | No of subrelations | Active on even rows | Active on odd rows | +| ----------------------------- | ------------------ | ------------------- | ------------------ | +| Non-Native Field Relation | 3 | ✓ | ✗ | +| Decomposition Relation | 48 | ✓ | ✓ | +| Permutation Relation | 2 | ✓ | ✓ | +| Delta Range Constraint | 10 | ✓ | ✓ | +| Opcode Constraint Relation | 5 | ✓ | ✓ | +| Accumulator Transfer Relation | 12 | ✗ | ✓ (propagation) | +| Zero Constraints Relation | 68 | ✓ | ✓ | + +Lagrange selectors for activation: + +- $L_{\text{even}}$: Equals 1 on even rows, 0 elsewhere +- $L_{\text{odd}}$: Equals 1 on odd rows, 0 elsewhere + +## Table of Contents + +1. [Limb Decomposition Structure](#limb-decomposition-structure) +2. [Non-Native Field Relations](#non-native-field-relations) +3. [Decomposition Relation](#decomposition-relation) +4. [Permutation Relation](#permutation-relation) +5. [Delta Range Constraint Relation](#delta-range-constraint-relation) +6. [Extra Relations](#extra-relations) + - (a) [Opcode Constraint Relation](#opcode-constraint-relation) + - (b) [Accumulator Transfer Relation](#accumulator-transfer-relation) + - (c) [Zero Constraints Relation](#zero-constraints-relation) + +--- + +## Limb Decomposition Structure + +This table establishes all notation used in the relations: + +| Value | Description | Binary Limbs | Native $\mathbb{F}_r$ | +| ------------------------------- | -------------------- | ------------------------------------------------------------------------------------ | --------------------- | +| **Evaluation challenge** | +| $x$ | Evaluation point | $x_0, x_1, x_2, x_3$ | $x_4$ | +| **Batching challenges** | +| $v$ | Batching challenge | $v_0, v_1, v_2, v_3$ | $v_4$ | +| $v^2$ | v squared | $(v^2)_0, (v^2)_1, (v^2)_2, (v^2)_3$ | $(v^2)_4$ | +| $v^3$ | v cubed | $(v^3)_0, (v^3)_1, (v^3)_2, (v^3)_3$ | $(v^3)_4$ | +| $v^4$ | v to fourth | $(v^4)_0, (v^4)_1, (v^4)_2, (v^4)_3$ | $(v^4)_4$ | +| **Point coordinates (witness)** | +| $P_x$ | Point x-coordinate | $P_{x,0}^{\text{lo}}, P_{x,1}^{\text{lo}}, P_{x,0}^{\text{hi}}, P_{x,1}^{\text{hi}}$ | (reconstructed) | +| $P_y$ | Point y-coordinate | $P_{y,0}^{\text{lo}}, P_{y,1}^{\text{lo}}, P_{y,0}^{\text{hi}}, P_{y,1}^{\text{hi}}$ | (reconstructed) | +| **Z-values (witness, 128-bit)** | +| $z_1$ | 128-bit value | $z_{1,0}, z_{1,1}$ (only 2 limbs) | (reconstructed) | +| $z_2$ | 128-bit value | $z_{2,0}, z_{2,1}$ (only 2 limbs) | (reconstructed) | +| **Accumulator (witness)** | +| $a^{\text{prev}}$ | Previous accumulator | $a_0^{\text{prev}}, a_1^{\text{prev}}, a_2^{\text{prev}}, a_3^{\text{prev}}$ | (reconstructed) | +| $a^{\text{curr}}$ | Current accumulator | $a_0^{\text{curr}}, a_1^{\text{curr}}, a_2^{\text{curr}}, a_3^{\text{curr}}$ | (reconstructed) | +| **Quotient (witness)** | +| $\mathcal{Q}$ | Division quotient | $q_0, q_1, q_2, q_3$ | (reconstructed) | +| **Negative $q$ constant** | +| $\bar{q}$ | $-q \pmod{2^{272}}$ | $\bar{q}_0, \bar{q}_1, \bar{q}_2, \bar{q}_3$ | $\bar{q}_4$ | +| **Carries (witness)** | +| $c^{\text{lo}}$ | Lower carry | (single 84-bit value) | - | +| $c^{\text{hi}}$ | Higher carry | (single 84-bit value) | - | +| **Opcode (witness, small)** | +| $\texttt{op}$ | Operation code | (no decomposition, ≤ 8) | $\texttt{op}$ | + +#### Reconstruction Formula (General) + +For a 254-bit value decomposed as $\ell_0, \ell_1, \ell_2, \ell_3$: + +$$\boxed{\text{Value} = \ell_0 + 2^{68} \cdot \ell_1 + 2^{136} \cdot \ell_2 + 2^{204} \cdot \ell_3}$$ + +**Specific reconstructions:** + +The coordinates $P_x$ and $P_y$ are reconstructed as: + +$$P_x = P_{x,0}^{\text{lo}} + 2^{68} \cdot P_{x,1}^{\text{lo}} + 2^{136} \cdot P_{x,0}^{\text{hi}} + 2^{204} \cdot P_{x,1}^{\text{hi}}$$ + +$$P_y = P_{y,0}^{\text{lo}} + 2^{68} \cdot P_{y,1}^{\text{lo}} + 2^{136} \cdot P_{y,0}^{\text{hi}} + 2^{204} \cdot P_{y,1}^{\text{hi}}$$ + +The scalars $z_1$ and $z_2$ (both 128-bit) are reconstructed as: + +$$z_1 = z_{1,0} + 2^{68} \cdot z_{1,1}$$ + +$$z_2 = z_{2,0} + 2^{68} \cdot z_{2,1}$$ + +The accumulators are reconstructed as: + +$$a^{\text{prev}} = a_0^{\text{prev}} + 2^{68} \cdot a_1^{\text{prev}} + 2^{136} \cdot a_2^{\text{prev}} + 2^{204} \cdot a_3^{\text{prev}}$$ + +$$a^{\text{curr}} = a_0^{\text{curr}} + 2^{68} \cdot a_1^{\text{curr}} + 2^{136} \cdot a_2^{\text{curr}} + 2^{204} \cdot a_3^{\text{curr}}$$ + +The quotient $\mathcal{Q}$ is reconstructed as: + +$$\mathcal{Q} = q_0 + 2^{68} \cdot q_1 + 2^{136} \cdot q_2 + 2^{204} \cdot q_3$$ + +## Non-Native Field Relations + +We want to prove the following accumulation identity holds in $\mathbb{F}_q$: + +$$\boxed{a^{\text{curr}} = a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 \pmod{q}}$$ + +We can only perform arithmetic in $\mathbb{F}_r$, but we need to prove correctness in $\mathbb{F}_q$ (the base field). +To do this, we rewrite the above equation as an integer equation with quotient $\mathcal{Q}$: + +$$a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4 - \mathcal{Q} \cdot q - a^{\text{curr}} = 0 \quad (\text{in integers})$$ + +If this equation holds: + +1. Modulo $2^{272}$ (via limb arithmetic in $\mathbb{F}_r$), and +2. Modulo $r$ (native $\mathbb{F}_r$ computation), and +3. All values are properly range-constrained + +then it must hold in integers. This is because the Chinese Remainder Theorem guarantees that if an equation holds modulo two coprime moduli whose product exceeds the maximum possible value of the equation, then it holds over the integers. +Since all values are in $\mathbb{F}_q$, i.e., they are less than $q$, we have: + +$$ +\begin{aligned} +\textsf{max}(a^{\text{prev}} \cdot x + \texttt{op} + P_x \cdot v + P_y \cdot v^2 + z_1 \cdot v^3 + z_2 \cdot v^4) &< 5q^2 < 5 \cdot (2^{254})^2 < 2^{511} +\\ +\textsf{max}(\mathcal{Q} \cdot q) &< q^2 < (2^{254})^2 < 2^{508} +\end{aligned} +$$ + +Therefore, the maximum possible value of the left-hand side is less than $2^{511}$, while the moduli product is $2^{272} \cdot r > 2^{525} > 2^{511}$. +See [bigfield documentation](../stdlib/primitives/bigfield/README.md) for more details on non-native field arithmetic. + +The non-native field relation is enforced through three separate subrelations: + +| Subrelation | Purpose | Modulus | Limbs checked | +| ----------- | -------------------------- | --------- | ------------------------------------------ | +| 1 | Lower mod $2^{272}$ check | $2^{136}$ | Limbs 0, 1 | +| 2 | Higher mod $2^{272}$ check | $2^{136}$ | Limbs 2, 3 (with carry from subrelation 1) | +| 3 | Native field check | $r$ | Full native reconstruction | + +Together, these prove the relation holds in integers. + +### Subrelation 1: Lower Mod $2^{136}$ Check + +Prove that when we compute the accumulation formula using limbs 0 and 1, the result is a multiple of $2^{136}$. + +We compute the accumulation using: + +- Limb 0 terms (contribute at weight $2^0$) +- Limb 1 terms (contribute at weight $2^{68}$) + +The result should be: $\text{Result} = c^{\text{lo}} \cdot 2^{136}$ for some carry $c^{\text{lo}}$. +The limb 0 contribution is: + +$$ +\boxed{ + \begin{align*} + T_0 := &\; a_0^{\text{prev}} \cdot x_0 & \\ + &+ \texttt{op} \\ + &+ P_{x,0}^{\text{lo}} \cdot v_0 \\ + &+ P_{y,0}^{\text{lo}} \cdot (v^2)_0 \\ + &+ z_{1,0} \cdot (v^3)_0 \\ + &+ z_{2,0} \cdot (v^4)_0 \\ + &+ q_0 \cdot \bar{q}_0 \\ + &- a_0^{\text{curr}} + \end{align*} +} +$$ + +The limb 1 contribution is: + +$$ +\boxed{\begin{align*} +T_1 := &\; a_1^{\text{prev}} \cdot x_0 + a_0^{\text{prev}} \cdot x_1 & \\ +&+ P_{x,0}^{\text{lo}} \cdot v_1 + P_{x,1}^{\text{lo}} \cdot v_0 \\ +&+ P_{y,0}^{\text{lo}} \cdot (v^2)_1 + P_{y,1}^{\text{lo}} \cdot (v^2)_0 \\ +&+ z_{1,0} \cdot (v^3)_1 + z_{1,1} \cdot (v^3)_0 \\ +&+ z_{2,0} \cdot (v^4)_1 + z_{2,1} \cdot (v^4)_0 \\ +&+ q_0 \cdot \bar{q}_1 + q_1 \cdot \bar{q}_0 \\ +&- a_1^{\text{curr}} +\end{align*}} +$$ + +Thus, the combined subrelation is: + +$$\boxed{L_{\text{even}} \cdot \texttt{op} \cdot \left( T_0 + 2^{68} \cdot T_1 - 2^{136} \cdot c^{\text{lo}} \right) = 0}$$ + +Interpretation: + +- Compute $T_0$ (limb 0 contribution) +- Compute $T_1 \cdot 2^{68}$ (limb 1 contribution, shifted by 68 bits) +- Their sum should equal $c^{\text{lo}} \cdot 2^{136}$ +- If this holds, the lower 136 bits of the accumulation equation are correct + +This subrelation is only active when: + +- $L_{\text{even}} = 1$ (even rows in mini-circuit) +- $\texttt{op} \neq 0$ (not a no-op) + +### Subrelation 2: Higher Mod $2^{136}$ Check + +Prove that when we compute the accumulation formula using limbs 2 and 3, plus the carry from subrelation 1, the result is a multiple of $2^{136}$. + +We compute using: + +- The carry $c^{\text{lo}}$ from subrelation 1 +- Limb 2 terms (contribute at weight $2^{136}$) +- Limb 3 terms (contribute at weight $2^{204}$) + +The result should be: $\text{Result} = c^{\text{hi}} \cdot 2^{136}$ for some carry $c^{\text{hi}}$. +The limb 2 contribution (with carry) is: + +$$ +\boxed{\begin{align*} +T_2 := &\; c^{\text{lo}} \quad \textsf{(carry from subrelation 1)} & \\ +&+ a_2^{\text{prev}} \cdot x_0 + a_1^{\text{prev}} \cdot x_1 + a_0^{\text{prev}} \cdot x_2 \\ +&+ P_{x,0}^{\text{hi}} \cdot v_0 + P_{x,1}^{\text{lo}} \cdot v_1 + P_{x,0}^{\text{lo}} \cdot v_2 \\ +&+ P_{y,0}^{\text{hi}} \cdot (v^2)_0 + P_{y,1}^{\text{lo}} \cdot (v^2)_1 + P_{y,0}^{\text{lo}} \cdot (v^2)_2 \\ +&+ z_{1,1} \cdot (v^3)_1 + z_{1,0} \cdot (v^3)_2 \\ +&+ z_{2,1} \cdot (v^4)_1 + z_{2,0} \cdot (v^4)_2 \\ +&+ q_2 \cdot \bar{q}_0 + q_1 \cdot \bar{q}_1 + q_0 \cdot \bar{q}_2 \\ +&- a_2^{\text{curr}} +\end{align*}} +$$ + +The limb 3 contribution is: + +$$ +\boxed{\begin{align*} +T_3 := &\; a_3^{\text{prev}} \cdot x_0 + a_2^{\text{prev}} \cdot x_1 + a_1^{\text{prev}} \cdot x_2 + a_0^{\text{prev}} \cdot x_3 & \\ +&+ P_{x,1}^{\text{hi}} \cdot v_0 + P_{x,0}^{\text{hi}} \cdot v_1 + P_{x,1}^{\text{lo}} \cdot v_2 + P_{x,0}^{\text{lo}} \cdot v_3 \\ +&+ P_{y,1}^{\text{hi}} \cdot (v^2)_0 + P_{y,0}^{\text{hi}} \cdot (v^2)_1 + P_{y,1}^{\text{lo}} \cdot (v^2)_2 + P_{y,0}^{\text{lo}} \cdot (v^2)_3 \\ +&+ z_{1,1} \cdot (v^3)_2 + z_{1,0} \cdot (v^3)_3 \\ +&+ z_{2,1} \cdot (v^4)_2 + z_{2,0} \cdot (v^4)_3 \\ +&+ q_3 \cdot \bar{q}_0 + q_2 \cdot \bar{q}_1 + q_1 \cdot \bar{q}_2 + q_0 \cdot \bar{q}_3 \\ +&- a_3^{\text{curr}} +\end{align*}} +$$ + +The combined subrelation 2 is: + +$$\boxed{L_{\text{even}} \cdot \texttt{op} \cdot \left( T_2 + 2^{68} \cdot T_3 - 2^{136} \cdot c^{\text{hi}} \right) = 0}$$ + +Interpretation: + +- Start with carry $c^{\text{lo}}$ from subrelation 1 +- Add limb 2 contribution $T_2$ +- Add limb 3 contribution $T_3 \cdot 2^{68}$ +- Result should be $c^{\text{hi}} \cdot 2^{136}$ +- If this holds, the higher 136 bits are correct + +Together with Subrelation 1: We've proven the relation holds modulo $2^{272}$. + +### Subrelation 3: Native Field Check + +Prove the accumulation formula holds when computed directly in $\mathbb{F}_r$ (the native field). +First, reconstruct all values from their limbs: + +$$ +\begin{align*} +\tilde{P}_x &= P_{x,0}^{\text{lo}} + 2^{68} \cdot P_{x,1}^{\text{lo}} + 2^{136} \cdot P_{x,0}^{\text{hi}} + 2^{204} \cdot P_{x,1}^{\text{hi}} \pmod{r} \\ +\tilde{P}_y &= P_{y,0}^{\text{lo}} + 2^{68} \cdot P_{y,1}^{\text{lo}} + 2^{136} \cdot P_{y,0}^{\text{hi}} + 2^{204} \cdot P_{y,1}^{\text{hi}} \pmod{r} \\ +\tilde{z}_1 &= z_{1,0} + 2^{68} \cdot z_{1,1} \pmod{r} \\ +\tilde{z}_2 &= z_{2,0} + 2^{68} \cdot z_{2,1} \pmod{r} \\ +\tilde{a}^{\text{prev}} &= a_0^{\text{prev}} + 2^{68} \cdot a_1^{\text{prev}} + 2^{136} \cdot a_2^{\text{prev}} + 2^{204} \cdot a_3^{\text{prev}} \pmod{r} \\ +\tilde{a}^{\text{curr}} &= a_0^{\text{curr}} + 2^{68} \cdot a_1^{\text{curr}} + 2^{136} \cdot a_2^{\text{curr}} + 2^{204} \cdot a_3^{\text{curr}} \pmod{r} \\ +\tilde{\mathcal{Q}} &= q_0 + 2^{68} \cdot q_1 + 2^{136} \cdot q_2 + 2^{204} \cdot q_3 \pmod{r} +\end{align*} +$$ + +**Note:** The tilde indicates these are native field reconstructions in $\mathbb{F}_r$, not the original $\mathbb{F}_q$ values. + +The subrelation 3 is then: + +$$ +\boxed{\begin{align*} +L_{\text{even}} \cdot \texttt{op} \cdot \Big( &\tilde{a}^{\text{prev}} \cdot x_4 & \\ +&+ \texttt{op} \\ +&+ \tilde{P}_x \cdot v_4 \\ +&+ \tilde{P}_y \cdot (v^2)_4 \\ +&+ \tilde{z}_1 \cdot (v^3)_4 \\ +&+ \tilde{z}_2 \cdot (v^4)_4 \\ +&+ \tilde{\mathcal{Q}} \cdot \bar{q}_4 \\ +&- \tilde{a}^{\text{curr}} \Big) = 0 +\end{align*}} +$$ + +where: + +- All arithmetic is performed in $\mathbb{F}_{r}$ +- $x_4, v_4, (v^2)_4, (v^3)_4, (v^4)_4$ are the native field representations of the challenges +- $\bar{q}_4 = -q \pmod{r}$ + +Interpretation: + +- Reconstruct all limbed values back to native $\mathbb{F}_{r}$ elements +- Compute the accumulation formula directly in $\mathbb{F}_{r}$ +- If subrelations 1 and 2 prove it holds mod $2^{272}$, and subrelation 3 proves it holds mod $r$, then it holds in integers + +## Decomposition Relation + +The Decomposition Relation enforces the integrity of the limb decomposition system. While the Non-Native Field Relation proves the accumulation formula is correct, the Decomposition Relation proves all limb decompositions are valid. It consists of 48 subrelations organized into five categories: + +| Category | No. of Subrelations | Note | +| -------------------------------------- | ------------------- | --------------------------------------------------- | +| Accumulator microlimb decomposition | 4 | Active when $L_{\text{even}} \cdot \texttt{op} = 1$ | +| Point & scalar microlimb decomposition | 16 | Active when $L_{\text{even}} = 1$ | +| Wide limb decomposition | 2 | Decompose 84-bit carry limbs | +| Range constraint tightening | 20 | Enforce stricter bounds on highest microlimbs | +| Transcript decomposition | 6 | Prove 68-bit limbs reconstruct transcript values | +| | | | + +These work with the Permutation Relation and Delta Range Constraint which together prove each microlimb is in $[0, 2^{14})$. + +--- + +### The 14-bit Microlimb System + +Two-level decomposition hierarchy: + +1. Level 1 (68-bit limbs): 254-bit values → 68 + 68 + 68 + 50 bits +2. Level 2 (14-bit microlimbs): 68-bit limbs → 14 + 14 + 14 + 14 + 12 bits + +Microlimb reconstruction formula for a 68-bit limb $\ell$ with microlimbs $m_0, \ldots, m_4$: + +$$\boxed{\ell = m_0 + m_1 \cdot 2^{14} + m_2 \cdot 2^{28} + m_3 \cdot 2^{42} + m_4 \cdot 2^{56}}$$ + +Range constraints: + +- All microlimbs $m_j \in [0, 2^{14})$ (enforced by permutation) +- For 68-bit limbs: $m_4 \in [0, 2^{12})$ +- For 50-bit limbs: $m_3 \in [0, 2^{8})$ +- For 52-bit limbs: $m_3 \in [0, 2^{10})$ +- For 60-bit limbs: $m_4 \in [0, 2^{4})$ + +### Categories 1 and 2: Microlimb Decomposition (Subrelations 0-19) + +General pattern for decomposing a limb $\ell_i$ into microlimbs $\{\ell_{i,j}\}$: +$$\boxed{L_{\text{selector}} \cdot \left( \sum_{j=0}^{k} \ell_{i,j} \cdot 2^{14j} - \ell_i \right) = 0}$$ + +where $k=4$ for 68/60-bit limbs and $k=3$ for 50/52-bit limbs. + +**Subrelations 0-3:** Accumulator limbs $(a_0, a_1, a_2, a_3)$ with selector $L_{\text{even}} \cdot \texttt{op}$ + +- $a_3$ is 50-bit (uses only 4 microlimbs) + +**Subrelations 4-19:** Point coordinates and scalars with selector $L_{\text{even}}$ + +| Element | Limbs decomposed | Number of subrelations | Note | +| ------------- | ------------------------------------------------------------------------------------------ | ---------------------- | --------------------------------- | +| $P_y$ | $P_{y,0}^{\text{lo}}, \ P_{y,1}^{\text{lo}}, \ P_{y,0}^{\text{hi}}, \ P_{y,1}^{\text{hi}}$ | 4 | 68 + 68 + 68 + 50 bits | +| $z_1, z_2$ | $z_{1,0}, \ z_{2,0}, \ z_{1,1}, \ z_{2,1}$ | 4 | Each $z$ is 128-bit: 68 + 60 bits | +| $P_x$ | $P_{x,0}^{\text{lo}}, \ P_{x,1}^{\text{lo}}, \ P_{x,0}^{\text{hi}}, \ P_{x,1}^{\text{hi}}$ | 4 | 68 + 68 + 68 + 50 bits | +| $\mathcal{Q}$ | $q_0, q_1, q_2, q_3$ | 4 | 68 + 68 + 68 + 52 bits | +| | | | | + +### Category 3: Wide Limb Decomposition (Subrelations 20-21) + +Carry limbs $c^{\text{lo}}, c^{\text{hi}}$ are 84 bits (6 × 14-bit microlimbs). To save space, the 5th and 6th microlimbs are stored in unused "tail" columns: + +$$\boxed{L_{\text{even}} \cdot \left( \sum_{j=0}^{3} c_{i,j} \cdot 2^{14j} + c_{i,4} \cdot 2^{56} + c_{i,5} \cdot 2^{70} - c^{(i)} \right) = 0}$$ + +where $c^{(0)} = c^{\text{lo}}$, $c^{(1)} = c^{\text{hi}}$. +Microlimb reuse: + +- $c_{0,4}^{\text{micro}}$ = `p_x_high_limbs_range_constraint_tail_shift` +- $c_{0,5}^{\text{micro}}$ = `accumulator_high_limbs_range_constraint_tail_shift` +- $c_{1,4}^{\text{micro}}$ = `p_y_high_limbs_range_constraint_tail_shift` +- $c_{1,5}^{\text{micro}}$ = `quotient_high_limbs_range_constraint_tail_shift` + +### Category 4: Range Constraint Tightening (Subrelations 22-41) + +For limbs with $b = 14k + r$ bits (where $0 < r < 14$), the highest microlimb $m_k$ must satisfy $m_k < 2^r$. + +**Shift-and-scale technique:** + +For proving $m_k < 2^r$, we add a new variable $m_k^{\text{tail}}\in [0, 2^{14})$ defined as: + +$$m_k^{\text{tail}} := m_k \ll (14 - r).$$ + +Then enforce: + +$$\boxed{L_{\text{even}} \cdot \left( m_k \cdot 2^{14-r} - m_k^{\text{tail}} \right) = 0}$$ + +implying $m_k \in [0, 2^r)$. + +Shift factors: + +- for 68-bit limbs: $2^2 = 4$: Constrains to 12 bits +- for 52-bit limbs: $2^4 = 16$: Constrains to 10 bits +- for 50-bit limbs: $2^6 = 64$: Constrains to 8 bits +- for 60-bit limbs: $2^{10} = 1024$: Constrains to 4 bits + +Subrelations 22-41 apply this pattern to: + +| Elements | No of subrelations | Tail bits | +| ----------- | ------------------ | ------------------- | +| $P_x$ limbs | 4 | 12, 12, 12, 8 bits | +| $P_y$ limbs | 4 | 12, 12, 12, 8 bits | +| $z_1$ limbs | 2 | 12, 4 bits | +| $z_2$ limbs | 2 | 12, 4 bits | +| Accumulator | 4 | 12, 12, 12, 8 bits | +| Quotient | 4 | 12, 12, 12, 10 bits | +| | | | + +### Category 5: Transcript Value Reconstruction (Subrelations 42-47) + +These prove that 68-bit limbs correctly reconstruct EccOpQueue transcript values. +General pattern for composing two limbs into a transcript value: +$$\boxed{L_{\text{even}} \cdot \left( \ell_{\text{low}} + 2^{68} \cdot \ell_{\text{high}} - \text{transcript}_{\text{value}} \right) = 0}$$ + +Subrelations: + +| Column | Even row | Odd row | No. of subrelations | +| ----------- | ---------------------------- | ---------------------------- | ------------------- | +| `X_LO_Y_HI` | $P_{x,\text{lo}}$ (136 bits) | $P_{y,\text{hi}}$ (118 bits) | 2 | +| `X_HI_Z_1` | $P_{x,\text{hi}}$ (118 bits) | $z_1$ (128 bits) | 2 | +| `Y_LO_Z_2` | $P_{y,\text{lo}}$ (136 bits) | $z_2$ (128 bits) | 2 | +| | | | | + +#### Interaction with Delta Range Constraint + +The Decomposition Relation works in tandem with the Delta Range Constraint (a separate permutation argument): + +Delta Range Constraint proves: Every microlimb column (all `*_range_constraint_*` columns) contains only values in $[0, 2^{14})$. + +Decomposition Relation proves: + +1. Large limbs are correctly reconstructed from microlimbs +2. Highest microlimbs are more strictly bounded (4, 8, 10, or 12 bits) +3. Transcript values are correctly formed from 68-bit limbs + +Together they guarantee: All limb decompositions are valid and all values are correctly range-constrained. + +## Permutation Relation + +The Permutation Relation is the foundation of all range constraints in the Translator circuit. It proves that every microlimb value used in the circuit belongs to the set $[0, 2^{14} - 1]$. The relation uses a grand product argument comparing two multisets: + +- **Interleaved multiset:** All microlimbs as they appear in the circuit (spread across 16 segments due to interleaving) +- **Ordered multiset:** The same values, but sorted in ascending order + +If the two multisets are equal (i.e., one is a permutation of the other), then all values are valid. + +The relation consists of 2 subrelations: + +1. Grand product identity (degree 7) +2. Finalization check (degree 3) + +#### Interaction with the Delta Range Constraints + +The Permutation Relation works alongside the Delta Range Constraints to enforce microlimb ranges. We use a permutation argument to show that the multiset of microlimb values used in the circuit matches an ordered multiset containing all integers from $0$ to $2^{14} - 1 = 16383$. Instead of including all integers in the range $[0, 2^{14} - 1]$ explicitly, we use a "step" sequence with a fixed step size of 3: + +$$\{0, 3, 6, 9, \ldots, 16380, 16383\}$$ + +resulting in $\left\lceil\frac{16384}{3}\right\rceil = 5462$ values. This ensures that any microlimb value $ \leq 16383$ can be proven to be in range by showing it appears in the ordered multiset. We prove equality of multisets using a grand product argument. The correctness of the ordered multiset is proven by the Delta Range Constraints described in the next section. + +**Balancing the multisets:** The 4 interleaved wires contain only circuit microlimbs, while each of the 5 ordered wires contains circuit microlimbs plus the step sequence. To balance this, we add a 5th numerator wire (`ordered_extra_range_constraints_numerator`) containing 5 copies of the step sequence—one for each ordered wire. This ensures the multisets have equal cardinality. The Delta Range Constraints enforce that each value in the ordered multiset differs from the previous by at most 3. + +--- + +### Subrelation 1: Grand Product Identity + +**Purpose:** Prove the interleaved and ordered multisets are equal via grand product. + +The grand product polynomial $z_{\text{perm}}$ is defined recursively: + +$$\boxed{z_{\text{perm}}[i+1] \cdot \prod_{j=0}^{4} \left( w_j^{\text{ordered}}[i] + \beta \cdot L_{\text{mask}}[i] + \gamma \right) = z_{\text{perm}}[i] \cdot \prod_{j=0}^{4} \left( w_j^{\text{interleaved}}[i] + \beta \cdot L_{\text{mask}}[i] + \gamma \right)}$$ + +where: + +- $w_j^{\text{interleaved}}[i]$: The $j$-th interleaved range constraint wire at row $i$ +- $w_j^{\text{ordered}}[i]$: The $j$-th ordered (sorted) range constraint wire at row $i$ +- $\beta, \gamma$: Random challenges (from Fiat-Shamir) +- $L_{\text{mask}}[i]$: Lagrange polynomial indicating masking rows (for zero-knowledge) + +The term $(\beta \cdot L_{\text{mask}}[i])$ on both sides enforces that the zero-knowledge masking values in both sets are identical. +It is added only to the masking region, to avoid interfering with the actual circuit values (which must be in the range $[0, 2^{14} - 1]$). +The subrelation is then expressed, with boundary conditions, as: + +$$\boxed{\left( z_{\text{perm}} + L_{\text{first}} \right) \cdot \prod_{j=0}^{4} \left( w_j^{\text{interleaved}} + \beta \cdot L_{\text{mask}} + \gamma \right) = \left( z_{\text{perm}}^{\text{shift}} + L_{\text{last}} \right) \cdot \prod_{j=0}^{4} \left( w_j^{\text{ordered}} + \beta \cdot L_{\text{mask}} + \gamma \right)}$$ + +where: + +- $L_{\text{first}}$: Lagrange polynomial for first row ($z_{\text{perm}}[0] = 0$ is enforced implicitly) +- $L_{\text{last}}$: Lagrange polynomial for last row (we enforce $z_{\text{perm}}[\text{last}] = 0$ in subrelation 2) +- $z_{\text{perm}}^{\text{shift}}$: Shifted grand product polynomial ($z_{\text{perm}}[i+1]$) + +Note that $z_{\text{perm}}[0] = 0$ follows implicitly from the fact that we are opening $z_{\text{perm}}$ and $z_{\text{perm}}^{\text{shift}}$ both at the same challenge. +If the two multisets are equal: + +1. At each step, the products telescope: contributions cancel out +2. After processing all rows, the grand product returns to 1 (accounting for initialization/finalization) +3. If any value is out of range or missing from the sorted set, the product cannot telescope correctly + +Active when: All rows (both even and odd in the full interleaved circuit) + +Degree: 6 (each side is linear polynomial × product of 5 linear terms) + +--- + +### Subrelation 2: Finalization Check + +Purpose: Ensure the grand product polynomial returns to the correct value at the circuit boundary. + +$$\boxed{L_{\text{last}} \cdot z_{\text{perm}}^{\text{shift}} = 0}$$ + +Interpretation: + +- At the last row, $L_{\text{last}} = 1$ +- The shifted grand product $z_{\text{perm}}^{\text{shift}}$ (which is $z_{\text{perm}}$ at the row after last) must be 0 +- This ensures the telescoping completed correctly + +Active when: Last row only ($L_{\text{last}} = 1$) + +Degree: 2 (Lagrange × shifted polynomial) + +## Delta Range Constraint Relation + +The Delta Range Constraint Relation works in tandem with the Permutation Relation to prove that the ordered (sorted) multiset is actually sorted and bounded correctly. + +What it proves: + +1. The "ordered" wires are actually in non-descending order +2. Consecutive values differ by at most `SORT_STEP = 3` +3. The final value in each column is exactly $2^{14} - 1 = 16383$ + +The Permutation Relation only proves the multisets are equal. Without the Delta Range Constraint, an attacker could provide out of range values and the permutation would still pass if the interleaved set matches. + +The relation consists of 10 subrelations: + +- 5 consecutive difference checks (one per ordered wire) +- 5 maximum value checks (one per ordered wire) + +--- + +### Subrelations 1-5: Consecutive Difference Constraints + +Purpose: Enforce that each ordered wire is in non-descending order with maximum step 3. + +For each ordered wire $j \in \{0, 1, 2, 3, 4\}$: + +$$\boxed{\left( L_{\text{real\_last}} - 1 \right) \cdot \left( L_{\text{mask}} - 1 \right) \cdot \Delta_j \cdot (\Delta_j - 1) \cdot (\Delta_j - 2) \cdot (\Delta_j - 3) = 0}$$ + +where: +$$\Delta_j := w_j^{\text{ordered}}[i+1] - w_j^{\text{ordered}}[i].$$ + +When active, it forces: $\Delta_j \in \{0, 1, 2, 3\}$. The constraint is active when: + +- $L_{\text{real\_last}} = 0$ (not the last real row) +- $L_{\text{mask}} = 0$ (not a masking row) + +Why maximum step 3? +To ensure full coverage of $[0, 2^{14} - 1]$, we insert "step values" into the sorted array: + +- Start at 0 +- Insert values: 0, 3, 6, 9, ..., 16383 +- This creates `SORTED_STEPS_COUNT = (2^14 - 1) / 3 + 1 = 5462` steps + +Between these steps, actual microlimbs fill in the gaps. With $\Delta \in \{0, 1, 2, 3\}$: + +- No value can "jump over" a step value +- Every value $\leq 16383$ has a step value within distance 3 +- Therefore, all values in range can be represented + +Degree: 6 (product of 6 linear polynomials) + +--- + +### Subrelations 6-10: Maximum Value Constraints + +Ensure the final value in each sorted column is exactly $2^{14} - 1 = 16383$. +For each ordered wire $j \in \{0, 1, 2, 3, 4\}$: + +$$\boxed{L_{\text{real\_last}} \cdot \left( w_j^{\text{ordered}} - (2^{14} - 1) \right) = 0}$$ + +At the last real row ($L_{\text{real\_last}} = 1$): +$$w_j^{\text{ordered}}[\text{last}] = 2^{14} - 1 = 16383$$ + +This ensures: + +1. No value in the column exceeds $2^{14} - 1$ +2. The maximum value $2^{14} - 1$ is present in the sorted multiset +3. Combined with the difference constraint, all values are $\leq 2^{14} - 1$ + +Active when: Last real row only ($L_{\text{real\_last}} = 1$) + +Degree: 2 (Lagrange × difference) + +## Extra Relations + +To enforce the correctness of the opcodes and the accumulator lifecycle, we have a few additional relations. + +### Opcode Validity Check + +The Opcode Validity Check enforces that all operation codes (`op`) belong to the valid set: + +$$\boxed{\texttt{op} \in \{0, 3, 4, 8\}}$$ + +Valid opcodes: + +- `0`: No-op +- `3`: Equality and reset accumulator +- `4`: Scalar multiplication +- `8`: Point addition + +The constraint is expressed as a polynomial that has roots at the valid opcode values: + +$$\boxed{\left( L_{\text{mini\_mask}} - 1 \right) \cdot \texttt{op} \cdot (\texttt{op} - 3) \cdot (\texttt{op} - 4) \cdot (\texttt{op} - 8) = 0}$$ + +The constraint is active when $L_{\text{mini\_mask}} = 0$ (i.e., not a masking row in the mini-circuit). + +Degree: 5 (degree-1 Lagrange × degree-4 polynomial in `op`) + +--- + +### Accumulator Consistency with No-op + +These subrelations ensure that when the opcode is `0` (no-op), the accumulator remains unchanged between even rows. +For the other opcodes (`3`, `4`, `8`), this constraint does not apply and must be skipped. +Thus, for each accumulator limb $i \in \{0, 1, 2, 3\}$, we must enforce: + +$$\boxed{L_{\text{even}} \cdot (\texttt{op} - 3) \cdot (\texttt{op} - 4) \cdot (\texttt{op} - 8) \cdot \left( a_i^{\text{current}} - a_i^{\text{shifted}} \right) = 0}$$ + +Degree: 5 + +--- + +### Accumulator Transfer Relation + +The Accumulator Transfer Relation manages the lifecycle of the accumulator across the circuit: + +1. Initialization: Start with zero accumulator +2. Propagation: Copy accumulator from each odd row to the next even row +3. Finalization: Verify final accumulator matches expected result + +The relation consists of 12 subrelations: + +- 4 for propagation +- 4 for initialization (set to zero) +- 4 for finalization (check against expected result) + +#### Subrelations 1-4: Odd Row Propagation + +Ensure that we correctly copy the accumulator from each odd row to the next even row. +This is because the previous accumulator value (in this iteration) becomes the "current" value on the next iteration. +Refer to the [Witness Trace Structure](../translator_vm/README.md#witness-trace-structure) for details on how we compute the accumulator iteratively. + +Thus, for each limb $i \in \{0, 1, 2, 3\}$: + +$$\boxed{L_{\text{odd}} \cdot (L_{\text{real\_last}} - 1) \cdot \left( a_i^{\text{current}} - a_i^{\text{shifted}} \right) = 0}$$ + +This correctly "propagates" the accumulator value in computing the final accumulator. + +Active when: Odd rows only except the last real row in the mini-circuit (before masking). + +Degree: 3 + +#### Subrelations 5-8: Initialization + +Ensure the accumulator starts at zero at the beginning of the computation. Recall that we process the opcodes in reverse order, so the first "previous" accumulator corresponds to the last opcode processed. Thus, for each limb $i \in \{0, 1, 2, 3\}$: + +$$\boxed{L_{\text{real\_last}} \cdot a_i^{\text{current}} = 0}$$ + +This implies that at the last real row (before masking), all limbs of the accumulator are zero, ensuring the accumulator starts at 0. + +Degree: 2 (Lagrange × limb) + +#### Subrelations 9-12: Finalization + +Verify the final accumulator value matches the expected result from ECCVM. +For each limb $i \in \{0, 1, 2, 3\}$: + +$$\boxed{L_{\text{result}} \cdot \left( a_i^{\text{current}} - a_i^{\text{expected}} \right) = 0}$$ + +where $a_i^{\text{expected}}$ is provided as a relation parameter (derived from ECCVM output). The ECCVM circuit computes the batched evaluation: + +$$a^{\text{expected}} = \sum_{j=0}^{n-1} x^{n-1-j} \cdot \left( \texttt{op}_j + v \cdot P_{x,j} + v^2 \cdot P_{y,j} + v^3 \cdot z_{1,j} + v^4 \cdot z_{2,j} \right) \pmod{q}$$ + +The Translator must prove it computed the same value. The finalization check ensures that Translator's computation matches ECCVM's computation + +Active when: Result row only ($L_{\text{result}} = 1$), this row corresponds to the first real opcode in the mini-circuit. + +Degree: 2 (Lagrange × difference) + +--- + +### Zero Constraints Relation + +The Zero Constraints Relation enforces that certain witness wires are zero outside the mini-circuit. +Due to interleaving, the full circuit is 16× larger than the mini-circuit: + +- Mini-circuit: $2^{13} = 8,192$ rows (actual computation) +- Full circuit: $2^{17} = 131,072$ rows (for interleaving optimization) + +Rows outside the mini-circuit (rows 8,192 to 131,071) must be zero. All the range constraint microlimb wires and transcript wires should be zero outside the mini-circuit. Thus, for each such wire $w$, we enforce: + +$$\boxed{\left( L_{\text{even}} + L_{\text{odd}} - 1 \right) \cdot (L_{\text{mini\_mask}} - 1) \cdot w = 0}$$ + +Note that the Lagrange product is $0$ in the mini-circuit and $-1$ outside the mini-circuit, so this forces $w = 0$ there. + +Degree: 3 (Lagrange product × wire) + +--- diff --git a/noir/noir-repo b/noir/noir-repo index c9a8bf882069..1a930357477f 160000 --- a/noir/noir-repo +++ b/noir/noir-repo @@ -1 +1 @@ -Subproject commit c9a8bf882069681672e68b2612e4119592c4485a +Subproject commit 1a930357477fc0c210dc5a8960680282d4cfa24e