# Ceno prover frontend design

This is a detailed design on top of [this intuition (Section 1)](https://hackmd.io/@P4deJs5uRSyvHnXF8yyQJQ/r1CuuqQ8C).

## Replace product list by expressions.

Previously we have `pub expression: Vec<(E, Vec<usize>)>` and `pub flattened_ml_extensions: Vec<ArcMultilinearExtension<'a, E>>,` tp denote the product lists and mle lists after fixed variables, but this will be inefficient when computing the univariate polynomial for the verifier under the following case:
$$
\sum_b eq(rx, b)(f1(b)g1(b) + f2(b)g2(b) + \cdots)
$$
Therefore we introduce expressions.

- The output layers: a list of records
- The intermediate layers should be a list of operations, with the same input points.
- merge or split or linear combine by some challenges.
- prove a list of expressions
- each layer has a point, and each sub expression use a subrange of it.

### GKR layers

The GKR layer is defined as linear / non-linear layers. The non-linear layers is an RLC of expressions, see the next section.

The linear layer is between non-linear layers. It is check and combine.

For the check step, it is for the `merge` and other linear operation, therefore, it is given a list of `out = merge(in_0, in_1, ...)` or `out = linear_combine(in_0, in_1, ...)`

For the combine step, the verifier generates new challenges, setup the points and vectors.

### Expressions

We use `expressions: Vec<(Point<E>, Expressions<E>)>` instead, and the sumcheck will be applied on an RLC of this prover.

    r^0out_0(ry_0) + r^1 out_1(ry_1) + ... = \sum_x r^0 * eq_0(x)expr_0(x) + r^1 eq_1(x)expr_1(x) + ...

Then the expression is defined as follows:

enum Expression {
    Poly(i, start, end, is_ext)
    Sum(expr_0, expr_1, is_ext)
    Prod(expr_0, expr_1, is_ext)
}

## Optimizations

Use the optimizations from [this paper](https://eprint.iacr.org/2024/108).

## Precompile circuits

### Intuition

Precompile is like constructed by different Fp, uint operatoins. So we can think of them as opcodes.

### Detailed design

We hand writing circuits for necessary uint opcodes and prime field opcodes, with a similar structure of riscv opcode in ceno, but don't use registers.

## Examples

### Uint

### Prime field

### Keccak

A keccak-f function is discribed as follows applied on the state $a(x, y, z)$, $x, y, \in [5], z \in [2^\ell]$, and the number of rounds $n_r = 12 + 2 * \ell$. When $\ell = 6$, $n_r = 24$.

$$
R = \iota \circ \chi \circ \pi \circ \rho \circ \theta
$$
where
$$
\begin{equation*}
\begin{aligned}
&\theta: &a(x, y, z) \leftarrow a(x, y, z) \oplus \sum_{y' = 0}^4, a(x - 1, y', z) \oplus \sum_{y' = 0}^4 a(x + 1, y', z) \, \\
&rho: &a(x, y, z) \leftarrow a(x, y, z - (t + 1)(t + 2) / 2) \, \\
&pi: &a(x, y) \leftarrow a(x', y') \\
&\chi: &a(x) \leftarrow a(x) \oplus (a(x + 1) \oplus 1) \cdot a(x + 2) \\
&\iota: &a \leftarrow RC[i]
\end{aligned}
\end{equation*}
$$
where $\begin{pmatrix}0 & 1 \\ 2 & 3\end{pmatrix}^t \begin{pmatrix}1 \\ 0\end{pmatrix} = \begin{pmatrix}x \\ y\end{pmatrix}$ or $t = -1$ when $x = y - 0$. and $\begin{pmatrix}x \\ y\end{pmatrix} = \begin{pmatrix}0 & 1 \\ 2 & 3\end{pmatrix}\begin{pmatrix}x' \\ y'\end{pmatrix}$

### ECDSA