Make the emulator match the circuits #630
Comments
|
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 |
|
@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.) |
This was referenced Nov 26, 2024
matthiasgoergens
added a commit
that referenced
this issue
Dec 5, 2024
Our circuits use a [modified](Modified_Harvard_architecture) [Harvard architecture](https://en.wikipedia.org/wiki/Harvard_architecture) where the memory space for instructions and data are completely separated, even though they are both addressed with 32 bits. That is a Good Thing. That means writing to the data cell with address x does not change the value of the instruction cell with address x. In contrast, our emulator uses a [von Neumann architecture](https://en.wikipedia.org/wiki/Von_Neumann_architecture) at its core, but goes through quite a few gymnastics to hide that fact. > In a von Neumann architecture, data memory and stored program memory are intermixed. Modern computers have moved away from this architecture for [security](https://en.wikipedia.org/wiki/W%5EX) and performance reasons. In this PR, we turn our emulator into a Harvard Architecture machine as well to match what our circuits are doing. That means we change the emulator to explicitly load instructions not from the data RAM, but from the program ROM, which we are already storing separately anyway. > Instead of thinking about separate address spaces for data and code, you can also imagine that we have an [instruction cache and a data cache](https://en.wikipedia.org/wiki/Modified_Harvard_architecture#Split-cache_(or_almost-von-Neumann)_architecture), and that we load the instructions into their cache once at the start of the program, and then never invalidate that cache. This works towards #630
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 #622 (comment)
See #688 for a step in this direction.
The text was updated successfully, but these errors were encountered: