Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement remainder verification procedure using probabilistic argument #592

Closed
Tracked by #548 ...
Al-Kindi-0 opened this issue Dec 7, 2022 · 9 comments
Closed
Tracked by #548 ...
Assignees
Labels
stdlib Related to Miden standard library

Comments

@Al-Kindi-0
Copy link
Contributor

Al-Kindi-0 commented Dec 7, 2022

In what follows we make the assumption that the blow-up factor is a fixed constant equal to $8$.
The procedure that we want to implement, call it verify_remainder, takes as input:

  1. $l$ the length of the final domain i.e. the length of the remainder codeword.
  2. The memory address ptr of the word containing the first two coefficients of the remainder $q_0,q_1$. The remaining coefficients are stored in the subsequent addresses ptr + i for $i\in [1,\frac{l}{2} - 1]$. The remainder polynomial coefficients $p_i$ are stored in the subsequent memory addresses i.e. ptr + i for $i\in [\frac{l}{2}, \frac{l}{2} + \frac{\frac{l}{8}}{2}-1]$. Finally, the challenge $\tau$ is stored in address $\frac{l}{2} +\frac{\frac{l}{8}}{2}$.

Using the above, the procedure computes two quantities:

  1. $$\beta := \frac{\sum\limits_{j=0}^{l-1}\frac{\omega_j}{\tau - \omega_j}q_j}{\sum_\limits{j=0}^{l-1}\frac{\omega_j}{\tau - \omega_j}}$$ where $\omega_j := \omega^j$ and $\omega$ is the inverse of the final domain generator which can be computed from the initial domain generator $g$ as $$g^{N^{nlayers}}$$
  2. $$\alpha := \sum\limits_{i = 0}^{\frac{l}{8}-1} p_i \tau^{i}$$ using Horner's rule. To do this efficiently, it is better to have the coefficients of the remainder polynomial stored in descending order in memory.

Finally, the procedure asserts that $\alpha = \beta$.
To compute $\beta$ efficiently, non-deterministic inversion in the extension field has to be implemented i.e. #591 .

@Al-Kindi-0 Al-Kindi-0 changed the title Implement the procedure for doing remainder verification using the probabilistic argument in the current issue. Implement procedure for doing remainder verification using the probabilistic argument in #568 Dec 7, 2022
@bobbinth bobbinth changed the title Implement procedure for doing remainder verification using the probabilistic argument in #568 Implement remainder verification procedure using the probabilistic argument Dec 8, 2022
@bobbinth bobbinth changed the title Implement remainder verification procedure using the probabilistic argument Implement remainder verification procedure using probabilistic argument Dec 8, 2022
@bobbinth
Copy link
Contributor

bobbinth commented Dec 8, 2022

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
Copy link
Contributor Author

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
Copy link
Contributor

bobbinth commented Dec 8, 2022

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
Copy link
Contributor Author

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
Copy link
Contributor

bobbinth commented Dec 8, 2022

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.

@Al-Kindi-0
Copy link
Contributor Author

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

@itzmeanjan
Copy link
Contributor

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

@itzmeanjan
Copy link
Contributor

I implement verify_remainder_64 routine in #644

@bobbinth
Copy link
Contributor

Closed by #644

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
stdlib Related to Miden standard library
Projects
None yet
Development

No branches or pull requests

3 participants