0xPolygonMiden / miden-vm

STARK-based virtual machine
MIT License
620 stars 157 forks source link

multiset checks: running product column should explicitly shift multiplicand #1185

Open plafer opened 8 months ago

plafer commented 8 months ago

In our multiset checks docs, we currently describe our strategy for implementing multiset checks as a running product column, where values of a are multiplied in, values of b divided out, and confirm that the last row equals the first row. This explanation reflects our implementation (where multiplicand is either $a_i$ or $1/b_i$). This, in isolation, is incorrect because we don't shift the multiplicand by a random $\gamma$, and so can't appeal to the Schwartz-Zippel lemma (as described here).

For virtual tables (which use this multiset check strategy), we happen to "implicitly" shift each value, as described in a later subsection, where we see that when a virtual table row is collapsed, it is shifted by a random $\alpha_0$. Our implementation also properly does that (e.g. the stack overflow virtual table).

Although virtual tables are properly implemented now, future uses of multiset checks could forget to "implicitly" shift their values by $\alpha_0$.

To reduce confusion and future bugs, we should

In my opinion, this also leads to a clean way to think about virtual tables: collapse the columns of a virtual table by taking a random linear combination, and then run a multiset check between all "added" and "removed" values.

iammadab commented 8 months ago

I and @ginika-chinonso would like to work on this next. We noticed that build_aux_column is implemented very differently in the next branch and the al-simplify-aux branch.

We're wondering which branch would be best to start working on this?

plafer commented 8 months ago

This is very appreciated! We are working to merge the al-simplify-aux branch soon; I think we're pretty much ready to merge after https://github.com/0xPolygonMiden/miden-vm/pull/1214. So I would either wait for the branch to be merged, to start working off of it right away.

cc @bobbinth @Al-Kindi-0