proof splitter

[katat]

No description provided.

[mimoo]

two things here:

• you're missing a h1 header
• you're also missing the registration of memory pages no?

[mimoo]

oh, also this is not going to show up in the book if you don't add it to the summary file :o

[katat]

you're also missing the registration of memory pages no?

Indeed, registration of memory pages is part of the splitter, although empty bootloader doesn't require submitting main or continuous memory.

I guess I can add this part once I got a better understanding of how the bootloader works and implemented the registration of continuous memory.

[mimoo]

I think you should be able to link to this by just writing something like ./starkex/facts.html instead of an absolute URL (which might change if we change domain name at some point)

[mimoo]

maybe a good way to explain these could be that they are subproofs that have been verified already :D

[mimoo]

this is an h3 header instead of an h2

[mimoo]

you haven't defined what "main proof" means here at this point.

[mimoo]

this is the first time you talk about the deep composition polynomial but you haven't defined it. I guess we should either have a short description here, or a link to some other section that talks more about that :o

[katat]

created a backlog :)
#3

[mimoo]

all these links lead to the same page for me:

[mimoo]

so the verifier wants to check that a commitment to $h = p_0$ is computed correctly based on the constraints and the registers. To do that they check that at a random point $z$. In other word, they check

$$h(z) == \sum_{j=1}^{k} C_j(z) (\alpha_j z^{D-D_j^{-1}} + \beta_j)$$

Since $h$ is actually given as chunks $h_i$ instead (such that $h(x) = \sum_{i=0}^{M_2-1} x^i h_i(x^{M_2})$) the check is actually the following:

$$\sum_{i=0}^{M_2-1} z^i h_i(z^{M_2}) == \sum_{j=1}^{k} C_j(z) (\alpha_j z^{D-D_j^{-1}} + \beta_j)$$

To perform this check, the verifier computes the left hand side and the right hand side separately, then check that they match.

To compute the left hand side, they use FRI as a PCS to obtain an evaluation proof of the different $h_i(z^{M_2})$.

To compute the right hand side, they do the same but with the $C_j(z)$.

Is that it?

[katat]

I think your reasoning on the equations are correct. Thanks for providing these detailed math. I will add them to that part.

IIUC it is mainly for checking the consistency between the masks values of execution trace and evaluations of composition trace. Passing the consistency check implies the prover holds the correct trace values.

But it wants to improve the soundness using FRI. That is why the $p_0$ is derived from these oods values and get tested by FRI. So I think $h≠p_0$.

[katat]

The polynomial for execution trace, which involves two rows of mask values, is

$$h(x) = \sum_{j=1}^{k} C_j(x) (\alpha_j x^{D-D_j^{-1}} + \beta_j)$$

while composition trace, which involves a single row, is

$$h(x) = \sum_{i=0}^{M_2-1} x^i h_i(x^{M_2})$$

I think the oods is majorly testing if these two traces are consistent.

But for FRI low degree test, it needs to use induced mask values to come up with a quotient polynomial $p_0$ of degree $d(h) - 1$. If the FRI failed, then the quotient polynomial $p_0$ is incorrect, implying the oods mask values are incorrect thus the consistency check is unsound actually.

[mimoo]

ah yeah, the first OODS test only checks that h (or rather the chunks h_i) are correctly computed, meaning that they correctly encode the values you get by aggregating all the constraint polynomials (which are quotients) with random challenges.

But I don't think it's enough because originally you wanted to prove that all these quotients polynomials exist and were of some maximum degree, so you still need to do that but on the aggregated polynomials h_i this time

In other words, thanks to the OODS check, we reduced the problem of checking that each constraint is correct, to checking that a single polynomial (called the composition polynomial) is correct.

[mimoo]

first mention of OODS which needs to be defined (or point to a link that explains what that is :D)

[katat]

#4

[mimoo]

to prepare* and verify*

[mimoo]

requires the evaluation domain of $p_0$ to be within the expected domain for low degree linear extension

not sure what that means :D

[mimoo]

(at this point we don't care if p_0 is an LDE or not, most likely it isn't)

[mimoo]

The FRI protocol cannot process queries for out-of-domain evaluation points due to computational feasibility constraints for the prover

mmm, I'm not sure what this means either. What does it mean "process a query" here? Do you mean during the query phase of FRI the points have to be points that are committed to in the merkle tree, and since the field has a very large domain it would take too much work to commit to all evaluations (what is the size of the STARK field?)

[katat]

Do you mean during the query phase of FRI the points have to be points that are committed to in the merkle tree, and since the field has a very large domain it would take too much work to commit to all evaluations (what is the size of the STARK field?)

That is what I am trying to convey. I am trying to discuss the out of domain issue when applying the FRI as explained in the thaler lecture: https://www.youtube.com/watch?v=A3edAQDPnDY&t=5255s

[mimoo]

I admit I don't understand this paragraph either, I think there is a lot to unpack here:

1. the trace values and evaluations of the decomposed composition polynomial should be induced from a domain aligned with a low-degree extension -> not sure what you mean here, I think I understand that the random evaluation point should be sampled from the main multiplicative subgroup used in the protocol?
2. These newly induced values, as opposed to those used for the OODS consistency check, are utilized to derive the deep composition polynomial -> what is the OODS consistency check? how are they used to derive the composition polynomial?

[katat]

Maybe my comments above help on this part? Let me know if not.
I guess I really need to dive into the field extension and subgroup stuffs to better explain this part.

[mimoo]

I'm not sure I understand how p_0 is computed here :D

[mimoo]

what is f_{jl} ?

[mimoo]

oh OK, I think there's a typo here, it should be f_{l}.

Now I think I understand this specific p_0, it is FRI used as PCS: you're proving aggregating $M_1 + M_2$ evaluation proofs, that $f_i(zg^e_i) = y_i$ for all $i$ and $h_j(z^{M_2}) = \hat{y}_j$ for all $j$

(what is $zg^e_l$)

[mimoo]

I think you should explain more clearly what is happening here. You need to have evaluations of:

• the different registers $f_i$ at the random point $z$, so that you can evaluate all the constraints at $z$, so that you can evaluate $h$ at $z$ (LHS in my other comment)
• the different $h_i$ at the random point $z$ so that you can evaluate $h$ at $z$ (RHS in my other comment)

so you use FRI as a PCS, and in addition aggregate all of these evaluation proofs together as an optimization.

Doing this means that the prover has to prove that p_0 exists and is of degree $d$ (for some $d$). During FRI the verifier will obtain different evaluations of $p_0$. For example if they want an evaluation of $p_0(3)$ the prover would have to produce merkle proofs for $f_i(3)$ for all $i$ and $h_j(3)$ for all $j$

[mimoo]

I'm not a fan of these massive list of links :D I think having snippets and names of functions (for example what I did here https://zksecurity.github.io/stark-book/starkex/facts.html and here https://zksecurity.github.io/stark-book/starkex/starkex.html with the different links and snippets) is cleaner

[mimoo]

same comment on h3 that should be h2 (and previous header as well)

[katat]

Thanks a lot for the comments @mimoo

I created #5 to update the writing according to the comments.