add new built-in $x for accessing x value at each row

[grjte]

In order do define some constraints, we may want to be able to define lagrange polynomials directly. In such cases, the domain value that is used for interpolation is needed, so we need a shortcut for referring to this x-value at each row.

We can do this by adding a new built-in value $x that represents x at any given row.

Here's an example from @dlubarov at Polygon Zero of how this could give more flexibility in defining constraints:

// Boundary constraint.
a * l_0(x) = 0

// Every other row.
a * odd_row(x) = 0

def odd_row(x) = (x^(n/2) - 1)

def l_0(x) = (x^n - 1) / (x - 1)

Required changes:

• parser
• IR
• codegen

This adds flexibility to AirScript, but Miden VM does not need this at the moment, so we could keep updates to the miden codegen very minimal (i.e. just throw an error if this is used)

[Al-Kindi-0]

Just to give a bit more context on the functionality $x.
We usually have a trace matrix with $n$ rows and to index each of these rows we use what is called a primitive $n$-th root of unity $\omega$. This just means that the set $\{ \omega^i: i\in [0,\cdots, n-1]\}$ has size $n$.
What is also nice is that the concept of next row is easy to describe in this setting. More specifically, if $row_i := \omega^i$ then $row_{i+1}$ can be found as $next(row_i) := \omega^{i+1}$.
The set $\{ \omega^i: i\in [0,\cdots, n-1]\}$ is called the set of n-th roots of unity and these are the roots of the polynomial $P(X) := X^n -1$. This means that $P(X) = \Pi_{i = 0}^{n-1}{\left(X - \omega^i\right)}$ i.e. $P(\omega^i) = 0$.
Thus, taking any polynomial $Q(X)$, we have that $P(\omega^i)\cdot Q(\omega^i) = 0$ but this is not very useful as is.
Instead we can use what we have so far to force a polynomial to evaluate to some value at one of the $\omega^i$. More specifically, say we want to force column $a$ to take value $0$ at the 0th row. First we construct a polynomial that is equal to $1$ at the 0th row and is equal to $0$ everywhere else. This is easily done by observing that $\frac{P(X)}{(X - \omega^0)}$ is equal to $\Pi_{i = 1}^{n-1}{\left(X - \omega^i\right)}$ and the latter expression is zero on all $\omega^i$ except for $\omega^0$.
Thus, what we have now is: $\frac{P(X)}{(X - \omega^0)}$ is equal to a non-zero constant $k_0$ (I haven't shown this but can explain more if needed) when evaluated at $\omega^0$ and is equal to zero when evaluated at any $\omega^i$ with $i \neq 0$.
Now going back to our example, if $A(X)$ denote the polynomial representing column $a$ then we can force $a$ to be equal to $0$ at the 0th row by writing the following polynomial equation:
$$A(X) \cdot L_0(X) = 0 $$
over the domain $\{ \omega^i: i\in [0,\cdots, n-1]\}$ where $L_0$ is the Lagrange polynomial defined as
$$L_0(X) := \frac{1}{k_0}\frac{X^n - 1}{X - 1}$$ where we used $\omega^0 = 1$.

Similarly we can construct other Lagrange polynomials $L_j$ as $$L_j(X) := \frac{1}{k_j}\frac{X^n - 1}{X - \omega^j}$$ and these are the polynomials that are equal to 0 on all $\omega_i$ except for $\omega_j$ where they are equal to $1$.

A good mental model of these polynomials is to think of the numerator as the set of where the constraints will hold (all $n$ rows in the case of $L_i$) and the denominator as the set of exceptions (row $i$ in the case of $L_i$). We take this mental model and construct even more complex constraints. For example, the polynomial $S(X) := X^{n/2} - 1$ should evaluate to 0 for each other $\omega$ i.e. $\omega^0, \omega^2, \cdots, \omega^{n - 2}$ and thus can be used to force a constraint on each other row. Moreover, we can divide by another polynomial to introduce exceptions to the latter set of constraints.

One last point that I didn't touch upon is the concept of an offset e.g. instead of counting from row $0$ we can start counting from row $3$. A good point of reference for this and other related ideas is in this Winterfell section.

So the next question that poses itself is how much should we expose/abstract away in AirScript through the $x operator?

[tohrnii]

Thank you @Al-Kindi-0 for the write-up.

[dlubarov]

Glad to see this progressing!

One second thought about my suggestion... if AirScript were to support multivariate systems in the future, that could complicate it a bit. E.g. I guess the analog of L_1(x) for would be \prod (1 - x_i). Seems a bit harder to encode expressions like that that are dynamic with respect to the number of variables.