[WIP] Design for recursive lookups (global and local interactions)

[LindaGuiga]

This is still work in progress, but I am opening a draft PR so that we can decide early on whether we can agree on this design.

The goal is to create a design for recursive lookups.
The trait RecursiveAirLookupVerification contains the methods necessary for an AIR to check its own lookup constraints. Thus, it enables a RecursiveAir to:

• get the permutation columns (the auxiliary columns, like the running sum)
• get the challenges associated to the local lookups
• for local lookups, check that the auxiliary columns are updated correctly, and that the final cumulative sum (for LogUp) is 0
• for global lookups, check that the auxiliary columns are updated correctly, and that the final cumulative sum (for LogUp) is the same as the one provided by the prover.

Note that for global lookups (= global interactions), we need the index of the table with which we are interacting, as well as the direction of the lookup (sending or receiving), to determine whether the multiplicities should be negated. This is why I introduced Direction and Table.

In order to facilitate the use of airs without lookups, I introduced a wrapper AirWithoutLookups which implements RecursiveAirLookupVerification.

[4l0n50]

Just took a quick look. It would be nice to see an example, but I guess it needs non-recursive lookups first.

[4l0n50]

why do we need dynamic dispatch now?

[LindaGuiga]

It's so we can have &[&dyn A] in the multi-table verifier

[4l0n50]

ah yes, I saw that later and forgot to remove the comment.

[4l0n50]

don't you need to compute folded_constrais = folded_constraints + alpha * self.eval_global_constraints(..) in the circuit?

[LindaGuiga]

eval_global_constraints takes folded_constraints as an argument, so what it should do is use that start of the accumulator to keep folding (so it adds the global constraints as though they were part of the AIR constraints themselves)

[4l0n50]

I see, thkns!