Convert kernel ROM chiplet into a lookup table #1518
Labels
air
Related to Miden AIR and constraints
enhancement
New feature or request
processor
Related to Miden VM processor
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
andaddr
columns are converted to a singlemultiplicity
column.The "kernel lookup table" would have 5 columns:
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.The text was updated successfully, but these errors were encountered: