Supporting RAPs about winterfell

[irakliyk]

This would be an awesome addition to the library and will enable lots of interesting use cases. I haven't really dug into what machinery would be required to implement this - so, my thoughts on potential interfaces are rather preliminary. But I can think of couple of approaches:

One approach might be to modify the interface of ExecutionTrace struct so that the user can build columns in stages. This could be tricky because we use ProveChannel struct to draw randomness, and prover channels are constructed after the call to the prover's prove() function. So, it might potentially require fairly significant interface changes to the library.

Another approach might be to introduce a concept of "lookup tables". These tables could be used to represent read-only memory (like in Cairo), but also other things (e.g., for checking if a value in a valid range). These tables could then be passed to the prover (together with some other info) and the prover can figure out how to build the execution trace from them.

I kind of like the second approach, but there are still quite a few things to figure. For example:

• I imagine lookup tables could be public or private. In case of public tables, it might make sense to make them a part of AIR definition. In case of private tables, they would need to be passed to prover directly (potentially as one of the arguments to prove() function).
• How would the user define the rest of the execution trace in relation to these lookup tables? Right now, an execution trace is just a matrix of values, would it need to become more complex than that?
• What kind of new constraints would we need to introduce to support these tables. Right now, the set of constraints is relatively simple: we have boundary constraints (defined via Assertions) and transition constraints (defined via evaluate_transition() function). I imagine we'd need to introduce a separate set of constraints for permutation checks.

There are probably many more things to consider - but it would be really cool to start thinking about them sooner rather than later.

[irakliyk]

I spent a bit more time looking into RAPs, and I now think that abstracting all the mechanics behind a lookup table interface might be too difficult (at least at first). But an alternative approach shouldn't be much simpler and would support quite a bit more flexibility.

First, a bit of explanation on how RAPs work in STARK context (or at least my understanding of it). The core primitive we are trying to support is verifying that two columns have exactly the same values in them, but these values might be in different order. Here is an example:

a	a'
0	4
1	3
1	1
2	2
3	1
3	0
3	3
4	3

Once we have a way to prove that these columns contain a set of identical values, we can build read-only RAM, read-write RAM, lookup tables etc. etc. And to prove this we can use something similar to multiset equality check.

The core idea is that we pick some random value z, and then for each a_i we compute b_i = z + a_i, and then compute a product of all b_i values. We do the same for values a'_i (using the same z) and then make sure the the product we got are the same. A straight-forward way to implement this in AIR is to introduce two new columns, c and c'. These columns will keep a running product of b_i and b'_i values.

Here is how it would look like for the two columns from above (I'm computing everything mod 7 to keep the numbers small, and setting z = 5):

a	c	a'	c'
0	5	4	1
1	6	3	2
1	3	1	1
2	2	2	3
3	4	1	5
3	1	0	4
3	2	3	1
4	2	3	2

Here, c₀ = z + a₀ and c_i = c_{i - 1} * (z + a_i) for i > 0. Values in c'_i are computed similarly. As we can see, values of c and c' columns in the last row are the same (c₇ = c'₇ = 2) - this means that the sets of values in a and a' are identical.

There is a way to do this a bit more efficiently though - using only 1 extra column (and that's what is described in the Cairo paper). Instead of tracking running products of each columns separately, we can track a quotient of running products in a single column. Let's call this column p. Using this approach, our toy execution trace will look like so:

a	a'	p
0	4	5
1	3	3
1	1	3
2	2	3
3	1	5
3	0	2
3	3	2
4	3	1

Here, p_i = a_i / a'_i, though we don't track values a and a' explicitly. If the products are equal, the quotient should end up being 1, which is indeed the case (p₇ = 1).

Thus, for this execution trace, the prover would need to perform the following steps:

1. Build an execution trace consisting of columns a and a'. This could be done same as now.
2. Commit to this trace via a Merkle tree (same as now).
3. Use the root of the commitment tree to draw pseudo-random value z.
4. Compute column p.
5. Commit to p via a Merkle tree.
6. Execute the rest of the STARK protocol more or less unchanged.

Steps 3 and 4 could be can be done via a function which could look something like this:

fn build_aux_columns<B, H>(trace: &ExecutionTrace<B>, coin: &mut RandomCoin<B, H>) -> Vec<Vec<B>>
where
    B: StarkField,
    H: Hasher;

The implementer of the function would draw a random value z from the coin, read the appropriate columns from the trace, and compute and return column p. This approach is also general enough to support other scenarios - e.g. when we need to draw more than one random value and return more than one column.

One question is where to put this function. My preliminary thought is that we could create a trait which would be responsible for building execution trace, and then this trait would be passed to the prover's prove() function (instead of an already built trace). The trait could look like this:

pub trait TraceBuilder {

    type BaseField: StarkField;
    type Inputs;

    fn build_trace(inputs: Self::Inputs) -> ExecutionTrace<Self::BaseField>;

    fn build_aux_columns<H: Hasher>(
        _trace: &ExecutionTrace<Self::BaseField>, 
        _coin: &mut RandomCoin<Self::BaseField, H>
    ) -> Vec<Vec<Self::BaseField>> {
        vec![]
    }
}

Any feedback is welcome!

[Nashtare]

Hi! We (at Toposware) have been actually working recently on this! As you've opened a PR a few days ago related to RAPs integration, I was thinking we could find a way to work together on the task so that we don't take too distinct paths for future collaboration! Are you actually planning to integrate RAPs soon or is it just a standalone PR? If you're aiming for RAPs then let us help! 😄

We were currently thinking of dividing this in three stages:

• an interactive trace generation, currently available here, where the user is responsible for handling everything related to the permutation argument (auxiliary columns filling through closures, boundary assertions and constraints). It sets the logic on the prover/verifier side for handling this extra round (currently only 1) of adding auxiliary columns, extending and committing to them once the original trace has been committed to and randomness from the Merkle root has been extracted for the RAP coins.
• abstracting the permutation argument away from the user to be handled directly on the prover side. The user would then only be responsible for providing the pairs of cells she wants to copy.
• refactoring the logic of the Trace and Air (currently all the logic is in Air and Trace traits and TraceTable struct, regardless of whether a program uses RAPs or not. It may be better to handle this logic on separate subtraits like RandomizedTrace and RandomizedAir).

These two last points are being still under investigation / starting to get implemented but nothing yet close from being complete. As you've been doing some important refactoring on the prover side with the ongoing PR, we may want to rethink our approach to incorporate your latest changes. Do you already have a clear path in mind to share for RAP integration or should we discuss one first?

[irakliyk]

@Nashtare hi! sorry - just noticed this comment.

My plan is to integrate RAPs (the first bullet point from your list) within the next week or so and do a v0.4 release of the library. I actually just pushed another PR #78 (still work in progress) which, once complete, should get it most of the way there.

I took a brief look at how you did it - and I think my approach is fairly close to yours. There are some interface differences, but I don't think they are that big. Btw, feel free to leave comments on either of the PRs, if there are things that you'd do differently as compared to what I have.

[irakliyk]

@4l0n50 if we didn't have to deal with extension fields, the whole thing would have been way simpler - but the downside of that approach is that we'd be leaving a lot of potential performance improvements on the table.

I believe doing two (or more) FFTs over columns in the base field is different from doing one FFT over a single column defined over an extension field. I didn't verify this - but would be very surprised if this turned out to be wrong.

There was another possible option: we keep auxiliary columns in the base field, and to get enough soundness just have multiple indepenent columns. This would work, but it wouldn't be as efficient.

For example, if our base field is 64 bits, we'd need 3 independent base field columns to get ~100 bits of security. Contrast this with a single degree 2 extension of the same field, which would give the desired security level. The reasoning for this is that we can (roughly) define soundness as [length of execution trace] / [field size]. So, assuming our execution trace is 2^20, we'd get the following:

• With a degree 2 extension we get: 2^20 / 2^128 ≈ 108 bits
• With independent base field columns we get: 2^20 / 2^64 ≈ 44 bits per column. So, 2 columns give us 88 bits, and 3 columns 132.

In my benchmarks, doing an FFT for 3 base field columns is about 2x slower than doing an FFT on a single column in degree 2 extension (this is all for the 64-bit base field).

[irakliyk]

I guess it depends on your definition of "extremely efficient" and the specifics of your computation. Yes, the proof size will increase somewhat (though, the increase should be between 10% - 20% in most cases), and yes, proving time would also increase somewhat (this may be significant or negligible, depending on the specifics of a computation).

[irakliyk]

@Nashtare - I'm more or less done with #78 - though, I haven't tested it much. I could use some help with reviewing and putting together an example which uses RAPs (I believe you had an example like this in your PR).

If you are able to migrate your example to the structure I came up with would love to get your feedback on the overall interface. And of course, if you notice any bugs, do let me know and I can fix them.

[Nashtare]

Sure! I'll have a look!

[pgrinaway]

Thanks for the reply!

I'm just getting familiar with winterfell myself, so my opinions on what you wrote might be a bit naive. The second approach you mentioned feels "cleaner" in a way, or at least easier to use, and I think it would accommodate the use cases I am imagining at least.

How would the user define the rest of the execution trace in relation to these lookup tables? Right now, an execution trace is just a matrix of values, would it need to become more complex than that?

I think the main added complexity is that the values of the new columns would be dependent on the commitment to the first set of columns--so I think the choice becomes either building in a particular lookup table protocol or having some kind of callback for the new columns to be properly filled in. More specifically, if it is specifically desired to support range checks and lookup tables, we can hard-code the generation of the new columns from the first set & challenge. Alternatively, we'd need to have the original caller of prove supply some mechanism for filling in the new columns.

What kind of new constraints would we need to introduce to support these tables. Right now, the set of constraints is relatively simple: we have boundary constraints (defined via Assertions) and transition constraints (defined via evaluate_transition() function). I imagine we'd need to introduce a separate set of constraints for permutation checks.

I think we can get away with using the current set of constraint definitions. Other than the enforcement of the challenge itself--which I suppose we can represent as a constant column or simply as a part of the AIR--they should remain the same semantically. Of course, they can't be applied until all columns are filled. API-wise, it might be made even simpler by hardcoding the lookup table / range check protocols as mentioned above (obviating the need for a prover to specify those constraints manually), but I haven't thought about how limiting this would be.

Thanks again for your thoughts, and I hope my take isn't too naive!

[irakliyk]

Yes, the more I think about it, the more I like the "lookup table" approach better. I think building the "filled out" execution trace from some set of columns and lookup tables, shouldn't be too challenging (at least from the API standpoint). We already have two structs to describe execution trace:

1. ExecutionTrace which is provided by the user.
2. TraceTable which is built by the prover from the execution trace provided by the user.

We could re-define these to match the new requirements (e.g. ExecutionTrace could be the partial execution trace, and TraceTable could be the final trace table with columns built in stages). We could even introduce another internal struct, if needed. And since this transformation can be done by the prover, doing it in stages and committing to intermediate results shouldn't be an issue.

One question is how would a user tie the ExecutionTrace to a set of lookup tables (i.e. lookup table protocol). One approach might be to redefine values in the table to be enums (right now these values are base field elements). This enum might look like this:

pub enum TraceCell<B: StarkField> {
    Value(B),
    Lookup(usize, B),
}

So, when we need to have a value in a given sell, we'll just use TraceCell::Value, but when we want to do a lookup, then we could use TraceCell::Lookup. The parameters to lookup would specify the index of the table (assuming there are several tables) and index of the value within the table. Then, the prover would transform this table into the filled out execution trace by performing appropriate lookups.

There are few open questions I have about this approach though:

1. Can we mix and match Value and Lookup cells in the same column? Or should this be done at the column level (i.e., a column is either a value column or a lookup column)?
2. Is lookup table always mapping one field element to another (e.g., B -> B), or could it be a mapping of one field element to many (e.g., B -> [B; N])?
3. What are the performance implications of switching from simple field elements to more complicated enums?

It is also possible that we don't really needs such a structure at all. Maybe the lookups are implicit and we need to care about them only when defining transition constraints.

[pgrinaway]

Awesome! Thanks for the detailed writeup. I like your idea a lot. In the coming days I'm going to play around with it a little and see what I can do.

One question--how does this look on the verifier side? The verifier needs to know to check that the challenge value is used in the constraint, and needs to know that the challenge was drawn correctly. My impression (but correct me if I'm wrong) is that changes on the verifier side are a lot smaller than those on the prover side, but there are still a few things to iron out.

[irakliyk]

So, besides this, we'll need to change quite a few other things - but these should be fairly mechanical changes. Some of these include:

• Update StarkProof struct so that it can handle variable number of trace commitments.
• Update EvaluationFrame so that it can keep track of auxiliary columns (these probably should be tracked separately from regular columns).
• Update Air trait so that it is aware of how many random values need to be drawn after the first trace commitment.
  • This would also include updating the signature of evaluate_transition() function so that it can accept a list of random values.
• Finally, prover and verifier code would need to updated to handle the new process in an optional way (i.e., if a specific computation does not need RAP functionality, there should be no impact as compared to now).

It might make sense to implement these changes incrementally. I'm going to try to push a PR which introduces TraceBuilder trait in the next few days, and we more forward from there.

Btw, one open question for me is whether there are use cases when we need to go beyond two commits (e.g., could there ever be a need to to commit to some columns, build more columns, then commit to them, and then build a third set of columns)?

[Nashtare]

Alright, great! If you're aiming at integrating RAPs soon then we'll probably be better off waiting with you to keep the same interface!
I'll have a look at how you handle things and share any comment that I might find relevant :)

[4l0n50]

I took a brief look at how you did it - and I think my approach is fairly close to yours.

Great! then I would like to check something. As far as I can see, it seems unavoidable to commit to the auxiliary columns using a separate commitment. Therefore, it is also unavoidable to double the number of authentication paths since now you also need to prove correct openings of the second commitment. I would like to double check this because in the Cairo paper they just say "This mechanism is extremely efficient", but doubling the number of authentication paths + adding the permutation argument constraints is not what I would call "extremely efficient".

[irakliyk]

@Nashtare I noticed that in your approach the auxiliary columns are treated in the same way as the main trace columns (e.g., when building an evaluation frame). I was also planning to do it that way, but then realized that when we use an extension field, auxiliary columns need to be in the extension field.

So, it seems like I can't use evaluate_transition() (at least in its current form) to evaluate constraints which involve both main trace columns and auxiliary trace columns. I am thinking of introducing another method, maybe something like evaluate_aux_transition() which would have the following signature:

    fn evaluate_aux_transition<E1, E2>(
        &self,
        frame: &EvaluationFrame<E1>,
        aux_frame: &EvaluationFrame<E2>,
        periodic_values: &[E1],
        aux_rand_elements: &AuxTraceRandElements<E2>,
        result: &mut [E2],
    ) where
        E1: FieldElement<BaseField = Self::BaseField>,
        E2: FieldElement + From<E1>

This is just an idea so far (not sure if I'll run into any issues with this yet), but curious what you think about this, or if you see a better way to handle it.

[Nashtare]

@irakliyk You're right, this was not addressed in our first approach, though it had been mentioned. We hadn't yet put much thoughts into this, though the way you have organized the RAPs integration so far, it feels like this approach may indeed be the best. Dealing with everything together within the sole evaluate_transition() function would require too much changes to make it work, and I'm afraid it wouldn't be super readable / easy to maintain. At least that way will be much clearer.

[4l0n50]

but then realized that when we use an extension field, auxiliary columns need to be in the extension field

You can always have more auxiliary columns and treat the auxiliary rows as elements in the extension field. In that way you can still use evaluate_transition() for evaluating all the constraints

[irakliyk]

@4l0n50 that's how I wanted to do it initially, but ran into a couple of issues:

1. We need to do low-degree extension on aux columns. For this purpose we need to treat each aux column as a single column with values in the extension field, rather than as a set of several columns in the base field.
2. We need to evaluate constraints at an out-of-domain point (which is in the extension field). If we treat an aux column polynomial as several polynomials in the base field, each of them will evaluate to a value in the extension field. So, we'll end up with several values in the extension field for a single aux column.

[4l0n50]

Thanks @irakliyk for you quick answer. I was pretty sure about this, but you make me doubt.
In any case, we agree it is something at most about efficiency and not soundness? Because I have the impression you could solve this issue treating the proof system as a black box. In the end you just compile your constraints over the extension field to constraints over the base field. (and what about large modulus? you don't need to use the extension field for the permutation argument there no?).

Regarding 1, is there any difference in doing two FFTs for the two columns (assuming quadratic extension field) than doing a single FFT for 1 column with values in the extension field?. In 2, you either have 1 polynomial over the extension field evaluated at the OOD point or 2 polynomials over the base field evaluated at the OOD point. Again, can you save something? And in case you can gain in efficiency, then you might also win from using computations over the extension field on the normal columns.

[4l0n50]

Thanks for your answer @irakliyk !

I believe doing two (or more) FFTs over columns in the base field is different from doing one FFT over a single column defined over an extension field. I didn't verify this - but would be very surprised if this turned out to be wrong.

Yes it makes sense because with two independent columns you could encode more than extension field operations so it may be harder to interpolate (I'm also not really sure of what I'm saying, it is just my intuition).

For example, if our base field is 64 bits, we'd need 3 independent base field columns to get ~100 bits of security.

That's one option but you can do it also with two columns by encoding the extension field operation "inside the circuit". For example, if you want to add a constraint of the form c = multiplication_over_Fp2(a, b) you add constraints c_1 = a_1*b_1 + u²*a_2*b_2 and c_2 = a_1*b_2 + a_2*b_1 such that x = x_1 + u*x_2 and Fp2 = Fp[u] / (u^2 - \beta). So basically you can compute the products for the permutation argument over a quadratic extension encoding the constraints over the base field. In that way the soundness error will be as in the first case. (btw I think you could also copy two values at once, i.e. copy an element of the extension field?)

In my benchmarks, doing an FFT for 3 base field columns is about 2x slower than doing an FFT on a single column in degree 2 extension (this is all for the 64-bit base field).

Consequently with what I tried to argue before, I think here you should compare an FFT for 2 base field columns vs an FFT on a single degree 2 extension.
In any case, I agree that avoiding compiling explicitly the constraint over the extension field into base field constraint is the best solution. I just wonder if having also base field auxiliary columns could have any realistic use case. Probably not.

[irakliyk]

Closed by #78 and #85