Open georgwiese opened 1 month ago
@georgwiese I think the first constraint should be fixed from
h' * (alpha - A) * (alpha - B) = h * (alpha - A) * (alpha - B) + (alpha - B) + m * (alpha - A);
to
h' * (alpha - A) * (alpha - B) + m * (alpha - A) = h * (alpha - A) * (alpha - B) + (alpha - B);
Similar to how we already implemented a permutation argument in PIL (see #1297 and #1306), we could implement a variant of LogUp (also see this summary).
As a first version, it could look like this:
m
is added, containing the multiplicities. For now, we can only provide them via a hint for a concrete example (adding support by automatic witness generation is a next step).h
is added for each lookup, supposed to contain $hi = h{i - 1} + \frac{1}{\alpha - a_i} - \frac{m_i}{\alpha - b_i}$ (with $h0 := 0$). This can also be provided via a hint. Note that in the original LogUp, they don't add $h{i - 1}$ and instead run the sum-check protocol on the entire column. But our backends don't expose sum-check, and I don't see a big downside of this approach!So I think, the constraints would look something like this:
(Note that because of wrapping $h_0 = h_4 = 0$, so row $1$ does not have to be handled separately.)
This leaves out two details, which should be handled analogously to the permutation argument:
Compared to the original LogUp, this implementation lacks some optimization applicable to multiple lookups, especially if they have the same left-hand side. But I think it would be a good first step and allow for some first benchmarks already.