feat: Timestamps for Random Access Memory

[DavePearce]

Summary

The purpose of this feature is to introduce an additional lowering step which introduces the needed timestamps for reads / writes to random access memories. This is a preliminary step towards implementing constraints for random access memories.

Example

Consider the following ZkC minimal example:

memory data(addr:u16) -> (byte:u8)

fn read<data>(addr:u16) -> (r:u8) {
   r = data[addr]
}

We can see the internal IR representation generated from this like so:

> zkc compile --wir test.zkc

which generates the following

memory data(u16 addr) -> (u8 byte)

fn read(u16 addr) -> (u8 r) {
[0]     r = data[addr] ; ret
}

The goal of this lowering step is to introduce threaded timestamps values for all RAMs accessed by a given function. So, roughly speaking, when this lowering step is enabled we would expect to see something like this at the IR level:

memory data(addr:u16) -> (byte:u8)

fn read(data$stamp:u16, addr:u16) -> (data$stamp':u16, r:u8) {
[0]     r = data[data$stamp; addr] ; data$stamp' = data$stamp + 1; ret
}

Here, the instruction r = data[s; a] can be interpreted as saying: read value at address a in the data memory at timestamp s.

Approach

There are quite a few details still to be worked out here, including:

• (Reads / Writes) the MemRead / MemWrite instruction forms do not currently support the notion of a timestamp, and this needs to be added.
• (Stamp Width) Currently, there is no way in the ZkC source to specify the timestamp bitwidth, but this is necessary to determine whether it needs splitting into limbs. The suggested syntax would be (where u16; sets the stamp bitwidth):

memory data(u16; addr:u16) -> (byte:u8)

Finally, there are a bunch of other details. For example, when we are not lowering to constraints, do we want to still record the timestamp? It adds a small overhead. For preflight, this might be important to know.