A zk-evm specification

@tchapuischkaiban Hi, I have some questiions about ram:

  • As described in example 2.1.2, if read/write a word which interior offset is not 0, parent will dispatch two task, let child read/write one word address after another which means child read/write only one word address each time. But why 6.1 say “Store to/load from the memory at most 32 bytes at two consecutive word addresses”? If child read/write only one word address each time, shouldn’t CRAM_BWd_Offset always be equal to Curr_Wd_Offset?
  • In child ram, data is read/write word by word or byte by byte in a row?

@Softcloud:

  • First note that, in any case (even if the interior offset is 0), the parent RAM will treat the RETURN operation (the one of example 2.1.2, and any operation that requires interaction between two different memories) using a succession of READ/WRITE requests to the child RAM. Besides, you are right: what is described in the example 2.1.2 is an optimization. If the starting reading interior offset is non zero, we have deliberately chosen to read the last bytes of the first word of the called contract returned memory to perform more efficiently the further READ operations (that would have a zero starting interior offset) - hence, we do not exploit deliberately the fact that one can read/write at most two consecutive word addresses. This read/write at two consecutive word addresses property is however very useful for operations like MSTORE/MLOAD as they can be sent as a single request to the child RAM.
  • In the child RAM we can read/write single bytes of the 32-byte words contained at word multiple addresses - hence, in a single row we can either read/modify a single byte of a 32-byte word, or read/replace the full 32-byte word contained at a given word multiple address (optimization for requests that have a zero interior offset).

This is great and very detailed descriptions of the operational mode.
If there is an operational semantics for this zk-extension, it could be fed into existing models of the EVM, e.g. the K-framework.
This may help designing a prototype implementation/simulator quickly and, as the K-tools generate the simulator you may be able to debug/tune the semantics.

@franck44, thanks a lot for your positive feedback, we will have a look at the K-framework !

Could you please see if you can share the other modules you designed? My curiosity is piqued. Thanks!

@spartucus, we will provide the full low level module design in another publication that would be accompanied with some performance metrics from our implementation.

3 Likes