search

scroll-tech / ceno

Accelerate Zero-knowledge Virtual Machine by Non-uniform Prover Based on GKR Protocol
Apache License 2.0
60 stars 10 forks source link

Make the emulator match the circuits #630

Open matthiasgoergens opened 3 days ago

matthiasgoergens commented 3 days ago

Programming is hard. Programming in an emulator like ours without proper debugging tools is even harder. Programming without any debugging tools at all, just by 'proofed failed / succeeded' is hardest.

At the moment, our emulator and circuits don's implement the same machine. So you might do a lot of debugging to barely get your code working in the emulator, but then it still fails proving.

One example: if your guest program accesses random uninitialised memory in the emulator, you get a 0. But in the prover you might get a 0, or your program might fail, depending on the address and the phase of the moon. (Eg some parts of the private IO space behave like that.)

The circuits have their limitations (mostly!) for good technical reasons. So let's make the emulator reflect the limitations of the circuits.

The goal is that ideally, if your execution works in the emulator, you should be able to prove it.

As much as possible, we should make the emulator match the circuits by making them implement the same logic. (When that's not possible, we can add some bandaids and patch up the difference in behaviour on a case by case basis.)

_Originally posted by @matthiasgoergens in https://github.com/scroll-tech/ceno/pull/622#discussion_r1855845216_

lispc commented 3 days ago

in this function, we assert adjacent memory access value should be same https://github.com/scroll-tech/zkevm-circuits/blob/de04c6668125b732b47668d3bcd04723125762eb/zkevm-circuits/src/witness/rw.rs#L55

matthiasgoergens commented 3 days ago

@lispc Thanks, I'll have a look. Could you give more context, please?

Purely formally: it looks like what you linked is in the circuits (of the zkevm)? One of the problems that we are having is that our emulator allows certain executions that our circuits don't like. Adding extra checks in the circuits wouldn't help with that: we need extra checks in the emulator. (Or better: a bit of refactoring, so that the logic matches, instead of trying to catch discrepancies after the fact.)