Implement remainder verification procedure using probabilistic argument about miden-vm

[Al-Kindi-0]

Yep, I remember that. So, for folding factor = 4, once we figure out optimal remainder length, we'll only have to implement 2 procedures. E.g., it could be for size 64 and 32, or for 128 and 64 etc.

That's correct.

I actually think this will be non-negligible because if we know the size, we don't need any conditional logic. But if we don't know the size we need to run a while loop and for each iteration we need to increment the counter and perform inequality comparison. This could add up.

I agree, a while loop is unavoidable. Then I am onboard.

Yep, makes sense. I assumed that would be constructed by evaluating individual queries, and it wouldn't come from the advice tape. Then, we'd compute sequential hash of the and compare it to the commitment in the proof. Would this work, or am I missing something?

Here is how I am thinking about it and let's forget about the hashing for this part. The calling procedure (of fri_verify) would read $q$ from the advice tape and lay it out in memory starting from ptr. Then, for each query that we want to verify, at the last step of a query verification we would get an index (i.e. the folded position) in the range $[0,l-1]$ which we can use, together with ptr, to compare the output of the last fold_4 with q[index].
This is equivalent to this part.

[bobbinth]

at the last step of a query verification we would get an index (i.e. the folded position) in the range [0,l−1] which we can use, together with ptr, to compare the output of the last fold_4 with q[index].

As discussed offline, it may actually make sense to skip the initial reading from the advice tape and just put outputs of the last fold_4 steps at appropriate q[index]. Then, we can hash them and compare with remainder commitment.

[bobbinth]

I wonder if we should simplify this a little. Specifically, instead of making length $l$ an input parameter, let's fix the length at 64. So, the procedure could be verify_remainder_64. My thinking is that knowing size of the domain upfront will simplify procedure logic quite a bit. Once we have it working for one size, I think creating procedures for other sizes would not be too complicated and we could create verify_remainder_128 etc. (I don't think we'll need more than a handful of these once we find the optimal size).

So, for remainder of size 64, size of $q$ would be 64, and size of $p$ would be 8 - right?

Another thing I wonder is whether $p$ should be already assumed to be in memory, or whether procedure should "read it in" non-deterministically. And similarly for $\tau$ - maybe it should also be something that the procedure computes internally.

Assuming the above works, the only parameter for verify_remainder_64 would be ptr which holds the address of the first two coefficients of $q$. Then, the procedure would need to do the following:

1. Non-deterministically get $\tau$ from the advice provider.
2. Compute $\beta$ using the formula described in the original description.
3. Get coefficients of $p$ from the advice provider.
4. Compute $\alpha$ using the formal described in the original description.
5. Verify that $\alpha = \beta$.
6. Verify that $\tau$ was provided correctly. To confirm my understanding, $\tau$ is computed by sequentially hashing elements of $q$ and $p$ - right?

Assuming the above is correct, we'll need to add a new decorator the advice injector decorators. This decorator would take domain length $l$ and memory address $i$ as inputs and perform the follwoing:

• Interpolate values in mem[i], ..., mem[i + l - 1] into polynomial coefficients.
• Injected these coefficients into the advice tape.
• Compute $\tau$.
• Inject $\tau$ into the advice tape.

The name of decorator could be adv.invnttext2 - but I'm open to other suggestions.

Then, the first couple instructions of verify_remainder_64 would look like this:

export.verify_remainder_64
  push.64         # put the size of domain on the stack to prepare for adv.invfft
  adv.invnttext2  # set up the advice tape to contain tau and coefficients of p
  ...
end

[Al-Kindi-0]

I wonder if we should simplify this a little. Specifically, instead of making length an input parameter, let's fix the length at 64. So, the procedure could be verify_remainder_64. My thinking is that knowing size of the domain upfront will simplify procedure logic quite a bit. Once we have it working for one size, I think creating procedures for other sizes would not be too complicated and we could create verify_remainder_128 etc. (I don't think we'll need more than a handful of these once we find the optimal size).

Yes, I agree but then, if the initial domain size is not fixed, we would have to implement both versions. This is because of what we discussed some time ago which is that for folding factors higher than $2$ the remainder length can take different values. Off the top of my head, I think the number of possibilities is $h$ where $2^h$ is the folding factor. My thinking is that, with the layout I have used for both $p$ and $q$, the delta from a specific procedure to one that is generic is relatively small.

So, for remainder of size 64, size of $q$ would be 64, and size of $p$ would be 8 - right?

That's is exactly right.

Another thing I wonder is whether $p$ should be already assumed to be in memory...

I am assuming that the calling procedure would read the $q$ from the advice tape, followed by $p$ (which is put on the advice tape by a decorator), and lastly $\tau$, and then put these in the configuration I laid out above. My thinking is that this would make hashing, in order to get $\tau$, more straight forward but I like the neatness of your proposal.

To confirm my understanding, $\tau$ is computed by sequentially hashing elements of $q$ and $p$ - right?

That is correct.

[bobbinth]

This is because of what we discussed some time ago which is that for folding factors higher than 2 the remainder length can take different values.

Yep, I remember that. So, for folding factor = 4, once we figure out optimal remainder length, we'll only have to implement 2 procedures. E.g., it could be for size 64 and 32, or for 128 and 64 etc.

My thinking is that, with the layout I have used for both and , the delta from a specific procedure to one that is generic is relatively small.

I actually think this will be non-negligible because if we know the size, we don't need any conditional logic. But if we don't know the size we need to run a while loop and for each iteration we need to increment the counter and perform inequality comparison. This could add up.

I am assuming that the calling procedure would read the q from the advice tape, followed by p (which is put on the advice tape by a decorator), and lastly τ, and then put these in the configuration I laid out above. My thinking is that this would make hashing, in order to get τ, more straight forward

Yep, makes sense. I assumed that $q$ would be constructed by evaluating individual queries, and it wouldn't come from the advice tape. Then, we'd compute sequential hash of the $q$ and compare it to the commitment in the proof. Would this work, or am I missing something?

[Al-Kindi-0]

Sounds great, I have mentioned this in facebook/winterfell#126

[itzmeanjan]

I add advice provider for iNTT over qudratic extension field in #598

[itzmeanjan]

I implement verify_remainder_64 routine in #644

[bobbinth]

Closed by #644