search

0xPolygonMiden / miden-vm

STARK-based virtual machine
MIT License
632 stars 161 forks source link

Convert kernel ROM chiplet into a lookup table #1518

Open plafer opened 1 month ago

plafer commented 1 month ago

The current kernel ROM chiplet was designed with the assumption that it would be proved using a running product column (i.e. a "vanilla multiset check"). Specifically, if a program makes 10 syscalls to the same kernel procedure, we will add 10 entries to the kernel ROM (with the same addr).

After we've switched to LogUp-GKR, we could make this a simple lookup table, where the s0 and addr columns are converted to a single multiplicity column.

The "kernel lookup table" would have 5 columns:

| multiplicity | root0 | root1 | root2 | root3 |

Each kernel procedure (whether it's called or not) would be added exactly once to the table, with multiplicity = 0 for all kernel procedures that were not called during a program so that the kernel virtual table can account for them.

bobbinth commented 1 month ago

I think this approach would work for regular LogUp as well.