Note: under construction

# Introduction

The ECCVM circuit is designed to efficiently evaluate variable-base elliptic curve operations over a SNARK-friendly embedded curve. Specific attention is paid to efficiently evaluating multi-scalar multiplications.

The goal of the ECCVM is to be integrated as a component of Goblin Plonk.

Specifically, if the ECCVM is defined over a curve $\mathbb{G}_a \in \mathbb{F}_q^2$ with group order $r$, the ECCVM can efficiently evaluate group operations over cuve $\mathbb{G}_b \in \mathbb{F}_r^2$ with group order $q$. In practise we intend $\mathbb{G}_a$ to be the grumpkin curve and $\mathbb{G}_b$ to be the BN254 curve.

The VM is designed to execute a range of ECC operations. Both the ordering of VM operations and their inputs are arbitrary (i.e. not precomputed).

# High-level VM architecture

**Note:** this section describes the _virtual machine_ architecture, not the circuit architecture that evaluates the VM.

## Notation and nomencalture

The VM performs elliptic curve operations over a curve $\mathbb{G} \in \mathbb{F}_q^2$. The field associated with the prime-order subgroup of $\mathbb{G}$ is $\mathbb{F}_r$.

We require $\mathbb{G}$ to have an efficiently computible endomorphism: i.e. both $\mathbb{F}_q$ and $\mathbb{F}_r$ have cube roots of unity.
We denote the cube root in $\mathbb{F}_r$ by $\lambda$, where $\lambda^3 = 1 \in \mathbb{F}_r$ and $\lambda^2 + \lambda + 1 = 0$.
For a point $[P] \in \mathbb{G}$, we denote the efficiently-computible endomorphism point as $[P']$, where $[P'] = \lambda \cdot [P]$.

**Note:** For the grumpkin curve, if $[P] = \{ x, y \} \in \mathbb{F}_q^2$, then $[P'] = \{ \beta x, -y \} \in \mathbb{F}_q^2$ where $\beta^2 + \beta + 1 = 0 \in \mathbb{F}_q$ ($\beta$ is a cube root of unity in $\mathbb{F}_q$).

## VM State

Each opcode has up to 4 operands, each operand is $\in \mathbb{F}$. The VM only has one register, the "accumulator" register, which stores an elliptic curve point.
We refer to the point in the accumulator register as $[A]$.

The starting state of $[A]$ is the point at infinity.

## List of VM Opcodes

The VM opcode is defined by a 4-bit integer $op$. $op$ is decomposed into opcode flags $\{ q_{add}, q_{mul}, q_{eq}, q_{reset} \} \in \{0, 1\}^4$ where $op = 16q_{add} + 4q_{mul} + 2q_{eq} + q_{reset}$.

The flags $q_{add}, q_{mul}, q_{eq}, q_{reset}$ are all mutually exclusive with the exception being both $q_{eq}$ and $q_{reset}$ can be $1$.

If $q_{eq} = 1$ and $q_{reset} = 1$, the $reset$ operation is applied _after_ the $eq$ operation.

### Add(x, y)

For the point $[P] := \{x, y\} \in \mathbb{F}^2$, set $[A] := [A] + [P]$

### Mul(x, y, z1, z2)

For the point $[P] := \{x, y\} \in \mathbb{F}^2$ and the scalar $s := z1 + \lambda z2 \in \mathbb{F}_r$, set $[A] := [A] + s \cdot [P]$.

**Notes:** using $\mathbb{G}$'s efficiently-computable endomorphism, we can split the full-width scalar multiplication $s \cdot [P]$ into two half-width scalar multiplications $z1 \cdot [P], z2 \cdot [P']$. This reduces the amount of redundant computation performed in the case where the input scalar multiplier is half-width (e.g. 128-bit challenges).

### Eq(x, y)

For the point $[P] = \{x, y \} \in \mathbb{F}_p^2$ assert $[A] == [P]$

### Reset

Set $[A]$ to the point at infinity.

# Circuit Architecture

**Note:** This specification describes the circuit architecture in terms of evaluating algebraic operations over column vectors. These operations are then compiled into a zero-knowledge proving system, in our case the Honk proving system.

The VM opcodes and associated operands are described by 5 column vectors that collectively form the **input trace**.

The $Mul$ opcode is the only opcode that is not trivial to evaluate. The VM circuit tackles $Mul$ opcodes by evaluating the following:

1. The fundamental primitive we evaluate is the multiscalar multiplication
2. Contiguous sequences of $Mul$ opcodes are treated as a single multiscalar-multiplication operation
3. An isolated $Mul$ opcode (e.g. "Add, Mul, Add" is treated as a multiscalar-multiplication operation of size 1)

The circuit evaluates the Straus multiscalar multiplication algorithm, as it has the best constants for MSMs of size <128 (which we expect to be common in Goblin Plonk).

## The Straus MSM Algorithm

**Note:** for an example of this algorithm, see `element::batch_mul_with_endomorphism` in `barretenberg/ecc/groups/element_impl.hpp`

Given input tuples $\{ [P_1], \ldots, [P_m] \} \in \mathbb{G}^m$, $\{ s_1, \ldots, s_m \} \in \mathbb{F}_r$, the Strauss MSM computes $\sum_{i =1}^m s_i \cdot [P_i]$.
The algorithm is split into two sequential algorithm: a _precomputation algorithm_ and a _main msm algorithm_

The Straus algorithm is parametrised by the integer $k$, which describes the number of bits of each scalar multiplier being processed per iteration of the MSM algorithm.
We denote the maximum number of bits in each scalar multiplier to be $t$ i.e. $2^t > max(s_1, \ldots, s_m)$ and $2^{t-1} < max(s_1, \ldots, s_m)$

We describe a variant of the Straus algorithm that uses a "windowed non-adjacent form" representation of integers. A $k$-bit wnaf can take the values $\{ -2^k + 1, -2^k + 3, \ldots, 2^k - 1 \}$.

### Straus Precomputation Algorithm

The precomputation step computes point lookup tables $\{ T_1, \ldots, T_m \}$.
Each table $T_i$ is a size-$2^k$ tuple of points $\{ T_{i, 0}, \ldots, T_{i, 2^k - 1} \}$ where

$$
T_{i, j} = (-2^k + 2j + 1) \cdot [P_i]
$$

<!--
For $i \in [1, \ldots, m]$, $T_i = \{ T_{i, 0}, \ldots, T_{i, 2^k} \}$

$$
T_i = \{ (-2^k+1) \cdot [P_i], (-2^k + 3) \cdot [P_i], \ldots, (2^k + 1) \cdot [P_i] \}
$$ -->

The precomputation step also computes the k-bit windowed non-adjacent form representation of scalars $\{ s_1, \ldots, s_m \}$.
For all $j \in \{0, 1, \ldots, \frac{t}{k} - 1 \}$, let:

$$
w_{i, j} \in \{ -2^k + 1, -2^k + 3, \ldots, 2^k - 1 \} \\
skew_i \in \{0, 1 \} \\
\text{ such that } s_i = -skew_i + \sum_{j = 0}^{\frac{t}{k} - 1} 2^{kj} w_{i, j}
$$

### Straus Main MSM Algorithm

The Main MSM algorithm uses the precomputed outputs to implement a double-and-add subroutine:

1. Set $[Acc]$ to the point at infinity
2. For all $j \in [0, \ldots, \frac{t}{k} - 1]$ do the following:
1. set $[Acc] := 2^k \cdot [Acc]$ (i.e. double $[Acc]$, $k$ times)
2. for all $i \in [1, \ldots, m]$:
1. let $\ell := \frac{w_{i, j} + 2^k - 1}{2}$
2. set $[Acc] := [Acc] + [T_{i, \ell}]$
3. For all $i \in [1, \ldots, m]:$
1. set $[Acc] := [Acc] - skew_i \cdot [P_i]$
4. Return $[Acc]$

**Note:** The VM circuit evaluates Straus where $t$ is hardcoded to $128$ and $k$ is hardcoded to $4$ (the optimal size when $t = 128$)

## Circuit Components

The VM circuit can be split into three contiguous components, with disctinct sets of column vectors:

- **Transcript Column Section**: Evaluates all VM opcodes _excluding mul opcodes_ (mul opcodes treated separately due to their evaluation complexity)
- Note: the input trace columns are included as part of the transcript column section
- **Straus Precomputation Column Section**: Evaluates the "precomputation" step of the Straus MSM algorithm
- **Straus Main MSM Column Section**: Evaluates the "main msm" step of the Straus MSM algorithm

Lookup arguments and list-equivalence arguments are used to copy information between the three column sections.

**Note:** A "list equivalence argument" is referred to as "set membership" in our codebase. The term "set" is not accurate as the list can contain duplicate values.

**Note:** List equivalence argument validates that two lists of field elements contain the same values, without specifying any particular ordering.

# Columns used in circuit components

The following sections describe the columns used in the elliptic curve VM. These are transformed into polynomials via the Honk polynomial IOP. The complete description of ECCVM columns is in `barretenberghonk/flavor/ecc_vm.hpp`.

Note: apart from three lagrange columns (in #[Other_Uncategorized_Columns](#Other-Uncategorized-Columns)), all columns are either:

a. part of the input trace
b. witness columns committed to by the Prover.

In the following tables, each column has a defined "value range". If the range is not $\in \mathbb{F}_q$, the column must be range constrained, either with an explicit range check or implicitly through range constraints placed on other columns that define relations over the target column.

# Transcript Columns

| name | value range | description |
| ------------------------------- | ------------------ | ---------------------------------------------- |
| transcript_op | $\{0, ..., 15 \}$ | (input trace) opcode value |
| transcript_x | $\in \mathbb{F}_q$ | (input trace) x-coordinate parameter |
| transcript_y | $\in \mathbb{F}_q$ | (input trace) y-coordinate parameter |
| transcript_z1 | $< 2^{128}$ | (input trace) scalar multiplier parameter (lo) |
| transcript_z2 | $< 2^{128}$ | (input trace) scalar multiplier parameter (hi) |
| transcript_pc | $\in \mathbb{F}_q$ | point counter |
| q_transcript_add | $\{0, 1\}$ | is opcode add? |
| q_transcript_mul | $\{0, 1\}$ | is opcode mul? |
| q_transcript_eq | $\{0, 1\}$ | is opcode eq? |
| q_transcript_reset_accumulator | $\{ 0, 1 \}$ | does opcode reset accumulator? |
| q_transcript_msm_transition | $\{ 0, 1 \}$ | 1 if current op = mul & next op != mul |
| transcript_z1zero | $\{ 0, 1 \}$ | asserts(z1 == 0) if 1 |
| transcript_z2zero | $\{ 0, 1 \}$ | asserts(z2 == 0) if 1 |
| transcript_accumulator_x | $\in \mathbb{F}_q$ | x-coordinate of accumulator |
| transcript_accumulator_y | $\in \mathbb{F}_q$ | y-coordinate of accumulator |
| transcript_msm_count | $\in \mathbb{F}_q$ | counts number of muls in current msm |
| transcript_msm_x | $\in \mathbb{F}_q$ | x-coordinate of claimed msm output |
| transcript_msm_y | $\in \mathbb{F}_q$ | y-coordinate of claimed msm output |
| transcript_is_accumulator_empty | $\{ 0, 1 \}$ | is 1 if accumulator is point at infinity |

## Notes on transcript columns

### pc notes

Point counter tracks the number of **point multiplications** that have been processed so far by the transcript.

The value of `pc` tracks the above in _descending_ order. For example, if the VM input trace describes 10 multiplications, `pc` starts at 10.

This is so the end state of `pc` is 0.
One design heuristic of the ECCVM is to enable the end state of all columns to be `0` . This allows us to construct an ECCVM evaluation circuit with a large circuit size, without greatly affecting prover times (if most rows are not used, the column values are all `0` => no cost to commit to unused rows + no cost to evaluate relations for empty rows in the sumcheck IOP)

If `z1` and `z2` are both nonzero for a single row, the row will contribute **two** scalar multiplications (i.e. `pc` decrements by 2)

### z1zero, z2zero

(n.b. the below specifies `z1zero`/`z1` but also applies for `z2zero`/`z2`).

If `z1zero = 0` this does not enforce that `z1 != 0`. The purpose of `z1zero` is to prevent the creation of redundant multiplication operations if `z1 = 0`. We only enforce that `z1 == 0` if `z1zero = 1`.

### msm_count

`msm_count` tracks the number of point multipliations created by consecutive `mul` operations.
When `msm_transition = 1`, we use a lookup argument to validate the tuple `pc, msm_count, msm_x, msm_y` also appears in our Straus MSM Columns.

# Straus Precomputation Columns

| name | value range | description |
| --------------------------- | ------------------- | ----------------------------------------------------------------------- |
| precompute_select | $\{ 0, 1 \} | precompute relations only active if `precompute_select == 1` |
| precompute_pc | $\in \mathbb{F}$ | point counter for precompute columns |
| precompute_point_transition | $\{0, 1\}$ | is `1` if current row/next row process different points |
| precompute_round | $\{0, \ldots, 7 \}$ | 1 row per round. Need 8 rows to fully process a point |
| precompute_scalar_sum | $< 2^{128}$ | accumulating sum of scalar multiplier being decomposed into WNAF slices |
| precompute_s1hi | $\{0, \ldots, 3 \}$ | high 2 bits of 1st WNAF slice |
| precompute_s1lo | $\{0, \ldots, 3 \}$ | low 2 bits of 1st WNAF slice |
| precompute_s2hi | $\{0, \ldots, 3 \}$ | high 2 bits of 2nd WNAF slice |
| precompute_s2lo | $\{0, \ldots, 3 \}$ | low 2 bits of 2nd WNAF slice |
| precompute_s3hi | $\{0, \ldots, 3 \}$ | high 2 bits of 3rd WNAF slice |
| precompute_s3lo | $\{0, \ldots, 3 \}$ | low 2 bits of 3rd WNAF slice |
| precompute_s4hi | $\{0, \ldots, 3 \}$ | high 2 bits of 4th WNAF slice |
| precompute_s4lo | $\{0, \ldots, 3 \}$ | low 2 bits of 4th WNAF slice |
| precompute_skew | $\{0, 7 \}$\* | skew value of scalar multiplier (if round = 7, else value is 0) |
| precompute_tx | $\in \mathbb{F}_q$ | x-coordinate of precomputed point table entry |
| precompute_ty | $\in \mathbb{F}_q$ | y-coordinate of precomputed point table entry |
| precompute_dx | $\in \mathbb{F}_q$ | x-coordinate of 2 \* [point being processed] |
| precompute_dy | $\in \mathbb{F}_q$ | y-coordinate of 2 \* [point being proessed] |

### Notes

The relations applied to Straus precomputation columns evaluate the Straus precomputation algorithm for a point `[P]` and scalar `s`.

If `precompute_point_transition_shift = 1`, we do the following:

1. Set `precompute_round_shift = 7`
2. Set `precompute_tx, precompute_ty` to equal `15[P]`
3. Set `precompute_scalar_sum_shift` to equal `0`

The row transition relation will evaluate the following per row:

1. Add 4 WNAF slices into `precompute_scalar_sum_shift` (starting with most significant slice)
2. For point $[T] = (tx, ty)$, $[D] = (dx, dy)$, set $[T'] = (tx_shift, ty_shift) = [T] - [D]$

At each row, $[T]$ is added into a lookup table (see Lookup Tables Used In Lookup Protocol)

# Straus MSM Columns

The Straus MSM columns evaluate the main Straus MSM algorithm. Rows can evaluate one of three subalgorithms:

- (add round) Add up to 4 points into an accumulator
- (double round) Double the accumulator 4 times
- (skew round) Add up to 4 points into an accumulator to account for "skew" parameter

The algorithm executes a multiscalar multiplication of `msm_size` points over 33 rounds. The points are described via the value of `pc` and `msm_size`. (i.e. $pc, pc - 1, ..., pc - msm_size + 1$)

For rounds $0, \ldots, 31$, each row adds up to 4 points into the MSM accumulator. At the end of the round, the accumulator is doubled 4 times.

For round $32$, each point's "skew" variable is used to conditionally subtract the input point from the accumulator.

| e name | value range | description |
| ----------------- | --------------------- | -------------------------------------------------------------------- |
| msm_pc | $\in \mathbb{F}_q$ | point counter for MSM columns |
| msm_size | $\in \mathbb{F}_q$ | number of multiplications in current MSM being processed |
| msm_round | $\{ 0, \ldots, 32 \}$ | current round of current MSM |
| msm_count | $\in \mathbb{F}_q$ | number of multiplications processed so far in current MSM round |
| msm_transition | $\{ 0, 1 \}$ | is $1$ if next row processes a different MSM compared to current row |
| msm_add | $\{ 0, 1 \}$ | are we adding points at the current row? |
| msm_double | $\{ 0, 1 \}$ | are we doubling the accumulator at the current row? |
| msm_skew | $\{ 0, 1 \}$ | are we accounting for skew at the current row? |
| msm_accumulator_x | $\in \mathbb{F}_q$ | x-coordinate of MSM accumulator |
| msm_accumulator_y | $\in \mathbb{F}_q$ | y-coordinate of MSM accumulator |
| msm_add1 | $\{0 , 1\}$ | is 1 if we add (msm_x1, msm_y1) into accumulator |
| msm_slice1 | $\{ 0, \ldots, 15 \}$ | WNAF slice of point to add into accumulator |
| msm_x1 | $\in \mathbb{F}_q$ | x-coordinate of point to add into accumulator |
| msm_y1 | $\in \mathbb{F}_q$ | y-coordinate of point to add into accumulator |
| msm_lambda1 | $\in \mathbb{F}_q$ | intermediate used to add (x1, y1) into accumulator |
| msm_collision_x1 | $\in \mathbb{F}_q$ | used to validate point addition is not incomplete |
| msm_add2 | $\{0 , 1\}$ | is 1 if we add (msm_x2, msm_y2) into accumulator |
| msm_slice2 | $\{ 0, \ldots, 15 \}$ | WNAF slice of point to add into accumulator |
| msm_x2 | $\in \mathbb{F}_q$ | x-coordinate of point to add into accumulator |
| msm_y2 | $\in \mathbb{F}_q$ | y-coordinate of point to add into accumulator |
| msm_lambda2 | $\in \mathbb{F}_q$ | intermediate used to add (x1, y1) into accumulator |
| msm_collision_x2 | $\in \mathbb{F}_q$ | used to validate point addition is not incomplete |
| msm_add3 | $\{0 , 1\}$ | is 1 if we add (msm_x3, msm_y3) into accumulator |
| msm_slice3 | $\{ 0, \ldots, 15 \}$ | WNAF slice of point to add into accumulator |
| msm_x3 | $\in \mathbb{F}_q$ | x-coordinate of point to add into accumulator |
| msm_y3 | $\in \mathbb{F}_q$ | y-coordinate of point to add into accumulator |
| msm_lambda3 | $\in \mathbb{F}_q$ | intermediate used to add (x1, y1) into accumulator |
| msm_collision_x3 | $\in \mathbb{F}_q$ | used to validate point addition is not incomplete |
| msm_add4 | $\{0 , 1\}$ | is 1 if we add (msm_x4, msm_y4) into accumulator |
| msm_slice4 | $\{ 0, \ldots, 15 \}$ | WNAF slice of point to add into accumulator |
| msm_x4 | $\in \mathbb{F}_q$ | x-coordinate of point to add into accumulator |
| msm_y4 | $\in \mathbb{F}_q$ | y-coordinate of point to add into accumulator |
| msm_lambda4 | $\in \mathbb{F}_q$ | intermediate used to add (x1, y1) into accumulator |
| msm_collision_x4 | $\in \mathbb{F}_q$ | used to validate point addition is not incomplete |

### Notes

The "collision" columns are used to validate the x-coordinate of points being added do not equal one another

e.g. $(x_2 - x_1) * x_{collision} - 1 = 0$

### Notes on msm_pc

The value of $msm_{pc}$ is fixed while a multiscalar multiplication is being processed. When $msm_transition = 1$, the value of $msm_{pc}$ is increased by $msm_{size}$

# Other Uncategorized Columns

| name | value range | description |
| -------------------- | ------------------ | ------------------------------------- |
| lagrange_first | $\in \{0, 1\}$ | is $1$ at first index, $0$ otherwise |
| lagrange_second | $\in \{0, 1\}$ | is $1$ at second index, $0$ otherwise |
| lagrange_last | $\in \{0, 1\}$ | is $1$ at last index, $0$ otherwise |
| lookup_read_counts_0 | $\in \mathbb{F}_q$ | used in lookup argument |
| lookup_read_counts_1 | $\in \mathbb{F}_q$ | used in lookup argument |
| lookup_inverses | $\in \mathbb{F}_q$ | used in lookup argument |
| z_perm | $\in \mathbb{F}_q$ | used in list equivalence argument |

# Lists used in list equivalence check

N.B. the list equivalence check is called "set equivalence" in the code, need to change.

The following describes the types of lists used in the protocol and the values that are "written" to the list and "read" from. This is slight nomenclature abuse; each list element "written" into the list must be "read" once (and only once).

### Mapping between transcript points/scalars and precompute points/scalars

If $transcript\_mul = 1$ and $z1zero = 0$, write $\{ pc, x, y ,z1 \}$ into list.

If $transcript\_mul = 1$ and $z2zero = 0$, write $\{ pc, \beta \cdot x, -y, z2 \}$ into list.

If $precompute\_point\_transition = 1$:

1. let $s1 = 4s1hi + s1lo, s2 = 4s2hi + s2lo, s3 = 4s3hi + s3lo, s4 = 4s4hi + s4lo$
2. let $slice = 2^{12} s1 + 2^{8} s2 + 2^{4} s3 + s4 - skew$
3. let sum := 2^{16} scalar_sum + slice
4. add $\{ pc, t\_x, t\_y, slice \}$ into list\*

**Note** \* The value of $scalar\_sum$ is derived from the current row value of $scalar\_sum$ and $s1hi, s1lo, \ldots, s4hi, s4lo, skew$.

### Mapping between precompute WNAF slices and Straus MSM slices

**writes:**
If $precompute\_select = 1$, write the following into list:

- $\{ precompute\_pc, 4 \cdot round, 4 \cdot s1\_hi + s1\_lo \}$
- $\{ precompute\_pc, 4 \cdot round + 1, 4 \cdot s2\_hi + s2\_lo \}$
- $\{ precompute\_pc, 4 \cdot round + 2, 4 \cdot s3\_hi + s3\_lo \}$
- $\{ precompute\_pc, 4 \cdot round + 3, 4 \cdot s4\_hi + s4\_lo \}$
If $precompute\_select = 1$ and $precompute\_point\_transition = 1$, write $\{ precompute\_pc, 32, skew \}$ into list

**reads:**
If $msm\_add1 = 1$, read $\{ msm\_pc, msm\_round, msm\_slice1 \}$ from list
If $msm\_add2 = 1$, read $\{ msm\_pc - 1, msm\_round, msm\_slice2 \}$ from list
If $msm\_add3 = 1$, read $\{ msm\_pc - 2, msm\_round, msm\_slice3 \}$ from list
If $msm\_add4 = 1$, read $\{ msm\_pc - 3, msm\_round, msm\_slice4 \}$ from list

### Mapping between Straus MSM output and Transcript MSM output

**writes:**
If $msm\_transition = 1$, write $\{ msm\_pc, msm\_size, msm\_accumulator\_x\_shift, msm\_accumulator\_y\_shift \}$ into list

**reads:**
If $transcript\_msm\_transition = 1$:

- let $count := transcript\_msm\_count + (1 - z1\_zero) + (1 - z2\_zero)$
- read $\{ pc, transcript\_msm\_count, transcript\_msm\_x, transcript\_msm\_y \}$ from list

# Lookup tables used in lookup protocol

The only lookup table in the ECCVM is the table that describes point multiples (as part of the Straus precomputation step).

**writes:**

- $\{ pc, round*, t_x, t_y \}$
- $\{ pc, round*, t_x, -t_y \}$

N.B. we use the value of $precompute_round$ to derive the WNAF slice value that corresponds to the lookup table point.

**reads:**

- If $msm\_add1 = 1$, read $\{ pc, slice1, x1, y1 \}$
- If $msm\_add2 = 1$, read $\{ pc, slice2, x2, y2 \}$
- If $msm\_add3 = 1$, read $\{ pc, slice3, x3, y3 \}$
- If $msm\_add4 = 1$, read $\{ pc, slice4, x4, y4 \}$

# ECCVM Algebraic Relations

The following describes the relations applied to the columns in the ECCVM. The explicit algebraic formulae are not included as they may change rapidly over time until the specification stabilizes. Instead we describe the *statements* that must be validated. In each subsection we refer the reader to the specific files in `barretenberg` where the relation algebra is defined.

# Transcript Relations

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_transcript_relation.hpp`

### Validate correctness of z1_zero, z2_zero.

- If z1_zero = 0 and operation is a MUL, we will write a scalar mul instruction into our multiplication table.
- If z1_zero = 1 and operation is a MUL, we will NOT write a scalar mul instruction.
- (same with z2_zero).
- z1_zero / z2_zero is user-defined.
- We constraint z1_zero such that if z1_zero == 1, we require z1 == 0. (same for z2_zero).
- We do _NOT_ constrain z1 != 0 if z1_zero = 0. If the user sets z1_zero = 0 and z1 = 0,

### Validate `op` opcode is well formed.

* `op` is defined to be q_reset_accumulator + 2 * q_eq + 2 * q_mul + 4 * q_add,
* where q_reset_accumulator, q_eq, q_mul, q_add are all boolean

### Validate `pc` is updated correctly.

* pc stands for Point Counter. It decrements by 1 for every 128-bit multiplication operation.
* If q_mul = 1, pc decrements by !z1_zero + !z2_zero, else pc decrements by 0
* @note pc starts out at its max value and decrements down to 0. This keeps the degree of the pc polynomial smol

### Validate `q_msm_transition` is well-formed.

* If the current row is the last mul instruction in a multiscalar multiplication, q_msm_transition = 1.
* i.e. if q_mul == 1 and q_mul_shift == 0, q_msm_transition = 1, else is 0

### Validate `msm_count` resets when we end a multiscalar multiplication.

* msm_count tracks the number of scalar muls in the current active multiscalar multiplication.
* (if no msm active, msm_count == 0)
* If current row ends an MSM, `msm_count_shift = 0` (msm_count value at next row)

### Validate `msm_count` updates correctly for mul operations.

* msm_count updates by (!z1_zero + !z2_zero) if current op is a mul instruction (and msm is not terminating at next row).

### Add multiscalar multiplication result into transcript accumulator.

* If `q_msm_transition == 1`, we expect msm output to be present on (transcript_msm_x, transcript_msm_y).
* (this is enforced via a lookup protocol).
* If `is_accumulator_empty == 0`, we ADD msm output into transcript_accumulator.
* If `is_accumulator_empty = =1`, we ASSIGN msm output to transcript_accumulator.
* @note the output of an msm cannot be point at infinity (will create unsatisfiable constraints in
* ecc_msm_relation). We assume this does not affect statistical completeness for honest provers. We should validate this!

### If is_accumulator_empty == 1, assign transcript_accumulator output into accumulator

* @note The accumulator point for all operations at row `i` is the accumulator point at row `i + 1`!

### Constrain `add` opcode.

* add will add the input point in (transcript_x, transcript_y) into the accumulator.
* Correctly handles case where accumulator is point at infinity.

### Opcode exclusion tests. We have the following assertions:

* 1. If q_mul = 1, (q_add, eq, reset) are zero
* 2. If q_reset = 1, is_accumulator_empty at next row = 1
* 3. If q_add = 1 OR q_msm_transition = 1, is_accumulator_empty at next row = 0
* 4. If q_add = 0 AND q_msm_transition = 0 AND q_reset_accumulator = 0, is_accumulator at next row = current row value
* @note point 3: both q_add = 1, q_msm_transition = 1 cannot occur because of point 1 (q_msm_transition only 1 when
* q_mul 1) we can use a slightly more efficient relation than a pure binary OR

### `eq` opcode.

* If eq = 1, assert transcript_x/y = transcript_accumulator_x/y.
* If eq = 1, assert is_accumulator_empty = 0 (input point cannot be point at infinity)

### Initial condition check on 1st row.

* We require the following values are 0 on 2nd row:
* is_accumulator_empty = 1
* msm_count = 0
* NOTE: we want pc = 0 when lagrange_last = 1

### On-curve validation checks.

* If q_mul = 1 OR q_add = 1 OR q_eq = 1, require (transcript_x, transcript_y) is valid ecc point
* q_mul/q_add/q_eq mutually exclusive, can represent as sum of 3

### If performing an add, validate x-coordintes of inputs do not collide.

* If adding msm output into accumulator, validate x-coordinates of inputs do not collide

# Straus Precomputation: WNAF Relations

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_wnaf_relation.hpp`

### Constrain each of our scalar slice chunks (s1, ..., s8) to be 2 bits.

* Doing range checks this way vs permutation-based range check removes need to create sorted list + grand product
* polynomial. Probably cheaper even if we have to split each 4-bit WNAF slice into 2-bit chunks.

### If we are processing a new scalar (q_transition = 1), validate that the first slice is positive.

* This requires us to validate slice1 is in the range [8, ... 15]. (when converted into wnaf form this maps to the range [1, 3, ..., 15]).
* We do this to ensure the final scalar sum is positive.
* We already know slice1 is in the range [0, ..., 15]
* To check the range [8, ..., 15] we validate the most significant 2 bits (s1) are >=2

### Convert each pair of 2-bit scalar slices into a 4-bit windowed-non-adjacent-form slice.

* Conversion from binary -> wnaf = 2 * binary - 15.
* Converts a value in [0, ..., 15] into [-15, -13, -11, -9, -7, -5, -3, -1, 1, 3, 5, 7, 9, 11 , 13, 15].
* We use WNAF representation to avoid case where we are conditionally adding a point in our MSM algo.

### Slice consistency check.

* We require that `scalar_sum` on the next row correctly accumulates the 4 WNAF slices present on the current row
* (i.e. 16 WNAF bits).
* i.e. next_scalar_sum - 2^{16} * current_scalar_sum - 2^12 * w_0 - 2^8 * w_1 - 2^4 * w_2 - w_3 = 0
* @note We only perform slice_consistency check when next row is processing the same scalar as the current row!
* i.e. when q_transition = 0
* TODO(@zac-williamson) Future work; probably don't need to convert to WNAF here. We can convert the final scalar
* sum into WNAF form when comparing scalar_sum with original input scalar

### Round transition logic.

* Goal: `round` is an integer in [0, ... 7] that tracks how many slices we have processed for a given scalar.
* i.e. number of 4-bit WNAF slices processed = round * 4.
* We apply the following constraints:
* If q_transition = 0, round increments by 1 between rows.
* If q_transition = 1, round value at current row = 7
* If q_transition = 1, round value at next row = 0
* Question: is this sufficient? We don't actually range constrain `round` (expensive if we don't need to!).
* Let us analyse...
* 1. When `q_transition = 1`, we use a set membership check to map the tuple of (pc, scalar_sum) into a set.
* We compare this set with an equivalent set generated from the transcript columns. The sets must match.
* 2. Only case where, at row `i`, a Prover can set `round` to value > 7 is if `q_transition = 0` for all j > i.
* `precompute_pc` decrements by 1 when `q_transition` = 1
* We can infer from 1, 2, that if `round > 7`, the resulting wnafs will map into a set at a value of `pc` that is
* greater than all valid msm pc values (assuming the set equivalence check on the scalar sums is satisfied).
* The resulting msm output of such a computation cannot be mapped into the set of msm outputs in
* the transcript columns (see relations in ecc_msm_relation.cpp).
* Conclusion: not applying a strict range-check on `round` does not affect soundness (TODO validate this!)

### Scalar transition checks.

* 1: if q_transition = 1, scalar_sum_new = 0
* 2: if q_transition = 0, pc at next row = pc at current row
* 3: if q_transition = 1, pc at next row = pc at current row - 1 (decrements by 1)
* (we combine 2 and 3 into a single relation)

### Validate skew is 0 or 7

* 7 is the wnaf representation of -1.
* We have one skew variable per scalar multiplier. We can only represent odd integers in WNAF form.
* If input scalar is even, we must subtract 1 from WNAF scalar sum to get actual value (i.e. where skew = 7)
* We use skew in two places.
* 1: when validating sum of wnaf slices matches input scalar (we add skew to scalar_sum in ecc_set_relation)
* 2: in ecc_msm_relation. Final MSM round uses skew to conditionally subtract a point from the accumulator

# Straus Precomputation: Point Table Relations

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_point_table_relation.hpp`

### Row structure

Consider the set of (128-bit scalar multiplier, point, pc) tuples in the transcript columns.
The point table columns process one tuple every 8 rows.
The tuple with the largest pc value is first.
When transitioning between tuple elements, pc decrements by 1.
This ensures that `precompute_pc = 0` for empty rows.

The following table gives an example row structure for two points.
In the table, the point associated with `pc = 1` is labelled P.
the point associated with `pc = 0` is labelled Q.

| precompute_pc | precompute_point_transition | precompute_round | Tx | Ty | Dx | Dy |
| -------- | ----------------------- | ----------- | ----- | ----- | ---- | ---- |
| 1 | 0 | 0 |15P.x | 15P.y | 2P.x | 2P.y |
| 1 | 0 | 1 |13P.x | 13P.y | 2P.x | 2P.y |
| 1 | 0 | 2 |11P.x | 11P.y | 2P.x | 2P.y |
| 1 | 0 | 3 | 9P.x | 9P.y | 2P.x | 2P.y |
| 1 | 0 | 4 | 7P.x | 7P.y | 2P.x | 2P.y |
| 1 | 0 | 5 | 5P.x | 5P.y | 2P.x | 2P.y |
| 1 | 0 | 6 | 3P.x | 3P.y | 2P.x | 2P.y |
| 1 | 1 | 7 | P.x | P.y | 2P.x | 2P.y |
| 0 | 0 | 0 |15Q.x | 15Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 1 |13Q.x | 13Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 2 |11Q.x | 11Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 3 | 9Q.x | 9Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 4 | 7Q.x | 7Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 5 | 5Q.x | 5Q.y | 2Q.x | 2Q.y |
| 0 | 0 | 6 | 3Q.x | 3Q.y | 2Q.x | 2Q.y |
| 0 | 1 | 7 | Q.x | Q.y | 2Q.x | 2Q.y |

We apply the following relations to constrain the above table:

1. If precompute_point_transition = 0, (Dx, Dy) = (Dx_shift, Dy_shift)
2. If precompute_point_transition = 1, (Dx, Dy) = 2 (Px, Py)
3. If precompute_point_transition = 0, (Tx, Ty) = (Tx_shift, Ty_shift) + (Dx, Dy)

The relations that constrain `precompute_point_transition` and `precompute_pc` are in `ecc_wnaf_relation.hpp`

When precompute_point_transition = 1, we use a strict lookup protocol in `ecc_set_relation.hpp` to validate (pc, Tx,
Ty) belong to the set of points present in our transcript columns.
("strict" lookup protocol = every item in the table must be read from once, and only once)

For every row, we use a lookup protocol in `ecc_lookup_relation.hpp` to write the following tuples into a lookup
table:
1. (pc, 15 - precompute_round, Tx, Ty)
2. (pc, precompute_round, Tx, -Ty)

The value `15 - precompute_round` describes the multiplier applied to P at the current row.
(this can be expanded into a wnaf value by taking `2x - 15` where `x = 15 - precompute_round`) .
The value `precompute_round` describes the *negative multiplier* applied to P at the current row.
This is also expanded into a wnaf value by taking `2x - 15` where `x = precompute_round`.

The following table describes how taking (15 - precompute_round) for positive values and (precompute_round) for negative
values produces the WNAF slice values that correspond to the multipliers for (Tx, Ty) and (Tx, -Ty):

| Tx | Ty | x = 15 - precompute_round | 2x - 15 | y = precompute_round | 2y - 15 |
| ----- | ----- | -------------------- | ------- | --------------- | ------- |
| 15P.x | 15P.y | 15 | 15 | 0 | -15 |
| 13P.x | 13P.y | 14 | 13 | 1 | -13 |
| 11P.x | 11P.y | 13 | 11 | 2 | -11 |
| 9P.x | 9P.y | 12 | 9 | 3 | -9 |
| 7P.x | 7P.y | 11 | 7 | 4 | -7 |
| 5P.x | 5P.y | 10 | 5 | 5 | -5 |
| 3P.x | 3P.y | 9 | 3 | 6 | -3 |
| P.x | P.y | 8 | 1 | 7 | -1 |

### Validate Dx, Dy correctness relation

* When computing a point table for point [P] = (Px, Py), we require [D] (Dx, Dy) = 2.[P]
* If all other relations are satisfied, we know that (Tx, Ty) = (Px, Py)
* i.e. (Dx, Dy) = 2(Px, Py) when precompute_round_transition = 1.
*
* Double formula:
* x_3 = 9x^4 / 4y^2 - 2x
* y_3 = (3x^2 / 2y) * (x - x_3) - y
*
* Expanding into relations:
* (x_3 + 2x) * 4y^2 - 9x^4 = 0
* (y3 + y) * 2y - 3x^2 * (x - x_3) = 0

### If precompute_round_transition = 0, (Dx_shift, Dy_shift) = (Dx, Dy)

* 1st row is empty => don't apply if lagrange_first == 1

### Valdiate (Tx, Ty) is correctly computed from (Tx_shift, Ty_shift), (Dx, Dy).

* If precompute_round_transition = 0, [T] = [T_shift] + [D].
*
* Add formula:
* x_3 = (y_2 - y_1)^2 / (x_2 - x_1)^2 - x_2 - x_1
* y_3 = ((y_2 - y_1) / (x_2 - x_1)) * (x_1 - x_3) - y_1
*
* Expanding into relations:
* (x_3 + x_2 + x_1) * (x_2 - x_1)^2 - (y_2 - y_1)^2 = 0
* (y_3 + y_1) * (x_2 - x_1) + (x_3 - x_1) * (y_2 - y_1) = 0
*
* We don't need to check for incomplete point addition edge case (x_1 == x_2)
* TODO explain why (computing simple point multiples cannot trigger the edge cases, but need to serve a proof of
* this...)

# MSM Relation

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_msm_relation.hpp`

### Evaluating ADDITION rounds

*
* This comment describes the algorithm we want the Prover to perform.
* The relations we constrain are supposed to make an honest Prover compute witnesses consistent with the following:
*
* For an MSM of size-k...
*
* Algorithm to determine if round at shifted row is an ADDITION round:
* 1. count_shift < msm_size
* 2. round != 32
*
* Algorithm to process MSM ADDITION round:
* 1. If `round == 0` set `count = 0`
* 2. For j = pc + count, perform the following:
* 2a. If j + 3 < k: [P_{j + 3}] = T_{j+ 3}[slice_{j + 3}]
* 2b. If j + 2 < k: [P_{j + 2}] = T_{j+ 2}[slice_{j + 2}]
* 2c. If j + 1 < k: [P_{j + 1}] = T_{j+ 1}[slice_{j + 1}]
* 2d. [P_{j}] = T_{j}[slice_{j}]
* 2e. If j + 3 < k: [Acc_shift] = [Acc] + [P_j] + [P_{j+1}] + [P_{j+2}] + [P_{j+3}]
* 2f. Else If j + 2 < k: [Acc_shift] = [Acc] + [P_j] + [P_{j+1}] + [P_{j+2}]
* 2g. Else IF j + 1 < k: [Acc_shift] = [Acc] + [P_j] + [P_{j+1}]
* 2h. Else : [Acc_shift] = [Acc] + [P_j]
* 3. `count_shift = count + 1 + (j + 1 < k) + (j + 2 < k) + (j + 3 < k)`

### Constraining addition rounds

*
* The boolean column q_add describes whether a round is an ADDITION round.
* The values of q_add are Prover-defined. We need to ensure they set q_add correctly.
* We rely on the following statements that we assume are constrained to be true (from other relations):
* 1. The set of reads into (pc, round, wnaf_slice) is constructed when q_add = 1
* 2. The set of reads into (pc, round, wnaf_slice) must match the set of writes from the point_table columns
* 3. The set of writes into (pc, round, wnaf_slice) from the point table columns is correct
* 4. `round` only updates when `q_add = 1` at current row and `q_add = 0` at next row
* If a Prover sets `q_add = 0` when an honest Prover would set `q_add = 1`,
* this will produce an inequality in the set of reads / writes into the (pc, round, wnaf_slice) table.
*
* The addition algorithm has several IF/ELSE statements based on comparing `cound` with `msm_size`.
* Instead of directly constraining these, we define 4 boolean columns `q_add1, q_add2, q_add3, q_add4`.
* Like `q_add`, their values are Prover-defined. We need to ensure they are set correctly.
* We update the above conditions on reads into (pc, round, wnaf_slice) to the following:
* 1. The set of reads into (pc_{count}, round, wnaf_slice_{count}) is constructed when q_add = 1 AND q_add1 =
* 1
* 2. The set of reads into (pc_{count + 1}, round, wnaf_slice_{count + 1}) is constructed when q_add = 1 AND
* q_add2 = 1
* 3. The set of reads into (pc_{count + 2}, round, wnaf_slice_{count + 2}) is constructed when q_add = 1 AND
* q_add3 = 1
* 4. The set of reads into (pc_{count + 3}, round, wnaf_slice_{count + 3}) is constructed when q_add = 1 AND
* q_add4 = 1
*
* To ensure that all q_addi values are correctly set we apply consistency checks to q_add1/q_add2/q_add3/q_add4:
* 1. If q_add2 = 1, require q_add1 = 1
* 2. If q_add3 = 1, require q_add2 = 1
* 3. If q_add4 = 1, require q_add3 = 1
* 4. If q_add1_shift = 1 AND round does not update between rows, require q_add4 = 1
*
* We want to use all of the above to reason about the set of reads into (pc, round, wnaf_slice).
* The goal is to conclude that any case where the Prover incorrectly sets q_add/q_add1/q_add2/q_add3/q_add4 will
* produce a set inequality between the reads/writes into (pc, round, wnaf_slice)

### Addition relation

* All addition operations are conditional additions!
* This method returns two Accumulators that represent x/y coord of output.
* Output is either an addition of inputs, or xa/ya dpeending on value of `selector`.
* Additionally, we require `lambda = 0` if `selector = 0`.
* The `collision_relation` accumulator tracks a subrelation that validates xb != xa.
* Repeated calls to this method will increase the max degree of the Accumulator output
* Degree of x_out, y_out = max degree of x_a/x_b + 1
* 4 Iterations will produce an output degree of 6
* If q_msm_transition = 1, we have started a new MSM. We need to treat the current value of [Acc] as the point at
* infinity!

### Doubling Relation

* Algorithm to determine if round is a DOUBLE round:
* 1. count_shift >= msm_size
* 2. round != 32
*
* Algorithm to process MSM DOUBLE round:
* [Acc_shift] = (([Acc].double()).double()).double()
*
* As with additions, the column q_double describes whether row is a double round. It is Prover-defined.
* The value of `msm_round` can only update when `q_double = 1` and we use this to ensure Prover correctly sets
* `q_double`. (see round transition relations further down)

### Evaluating SKEW operations

* When computing x * [P], if x is even we must subtract [P] from accumulator
* (this is because our windowed non-adjacent-form can only represent odd numbers)
* Round 32 represents "skew" round.
* If scalar slice == 7, we add into accumulator (point_table[7] maps to -[P])
* If scalar slice == 0, we do not add into accumulator
* i.e. for the skew round we can use the slice values as our "selector" when doing conditional point adds
* add skew points iff row is a SKEW row AND slice = 7 (point_table[7] maps to -[P])
* N.B. while it would be nice to have one `add` relation for both ADD and SKEW rounds,
* this would increase degree of sumcheck identity vs evaluating them separately.
* This is because, for add rounds, the result of adding [P1], [Acc] is [P1 + Acc] or [P1]
* but for skew rounds, the result of adding [P1], [Acc] is [P1 + Acc] or [Acc]

### Validate accumulator output matches SKEW output if q_skew = 1

* (this is a degree-6 relation)

### Check x-coordinates do not collide if row is an ADD row or a SKEW row

* if either q_add or q_skew = 1, an inverse should exist for each computed relation

### Validate that if q_add = 1 or q_skew = 1, add1 also is 1

* If add_i = 0, slice_i = 0
* When add_i = 0, force slice_i to ALSO be 0
* only one of q_skew, q_double, q_add can be nonzero
* if q_msm_transition = 0, round_shift - round = 0 or 1

### ROUND TRANSITION LOGIC (when round does not change)

* If q_msm_transition = 0 (next row) then round_delta = 0 or 1

### ROUND TRANSITION LOGIC (when round DOES change)

* round_transition describes whether we are transitioning between rounds of an MSM
* If round_transition = 1, the next row is either a double (if round != 31) or we are adding skew (if round ==
* 31) round_transition * skew * (round - 31) = 0 (if round tx and skew, round == 31) round_transition * (skew +
* double - 1) = 0 (if round tx, skew XOR double = 1) i.e. if round tx and round != 31, double = 1
* if no double or no skew, round_delta = 0
* if double, next double != 1
* if double, next add = 1

### Updating count

* if q_msmsm_m_transition = 0 and round_transition = 0, count_shift = count + add1 + add2 + add3 + add4
* if q_msm_transition = 1, count_shift = 0
* if q_msm_transition = 1, pc = pc_shift + msm_size

### Addition continuity checks

* We want to RULE OUT the following scenarios:
* Case 1: add2 = 1, add1 = 0
* Case 2: add3 = 1, add2 = 0
* Case 3: add4 = 1, add3 = 0
* These checks ensure that the current row does not skip points (for both ADD and SKEW ops)
* This is part of a wider set of checks we use to ensure that all point data is used in the assigned
* multiscalar multiplication operation.
* (and not in a different MSM operation)

### Final continuity check.

* If an addition spans two rows, we need to make sure that the following scenario is RULED OUT:
* add4 = 0 on the CURRENT row, add1 = 1 on the NEXT row
* We must apply the above for the two cases:
* Case 1: q_add = 1 on the CURRENT row, q_add = 1 on the NEXT row
* Case 2: q_skew = 1 on the CURRENT row, q_skew = 1 on the NEXT row
* (i.e. if q_skew = 1, q_add_shift = 1 this implies an MSM transition so we skip this continuity check)

# List Correctness Relations

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_set_relation.hpp`

We validate list correctness relations using a generalized permutation argument (the source of the `z_perm` column).

The `eta` challenge is used to combine multiple values into a single lookup term.

See [Lists used in list equivalence check](#Lists-used-in-list-equivalence-check) for description of terms written into/read from lists

# Lookup Relations

Relation algebra in `barretenberg/proof_system/relations/ecc_vm/ecc_lookup_relation.hpp`

We use a logarithmic derivative lookup protocol to perform lookup relations.

For table write values $\vec{t}$ and read values $\vec{f}$, let $\vec{a}$ be a vector where $a_i$ describes the number of times that $t_i$ appears in $\vec{f}$.

Let $\vec{I}$ be an inverse vector where $I_i = \frac{1}{(f_i + \gamma)(t_i + \gamma)}$.

The lookup relation validate the following for all $i \in [n]$ ($n$ = circuit size):

$$
I_i * (f_i + \gamma)(t_i + \gamma) - 1 = 0
$$

In addition the lookup relation validates the following:

$$
\sum_{i \in [n]} I_i \cdot (g_i + \gamma) - a_i \cdot I_i \cdot (f_i + \gamma) = 0
$$

(this is equialent to checking $\sum_{i \in [n]} \frac{1}{f_i + \gamma} - \frac{a_i}{t_i + \gamma} = 0$)

See [Lookup-tables-used-in-lookup-protocol](#Lookup-tables-used-in-lookup-protocol) for description of terms written into/read from the lookup table.