Define abstract trait for MemoryChecking

[DoHoonKim8]

This will be useful for Jolt library

[DoHoonKim8]

@jeong0982 Would you please list up in which situation to use offline memory checking and how will gonna use it?

[jeong0982]

Emulator in riscu-jolt works with Memory trait:

pub trait Memory {
    fn read_u8(&mut self, addr: u64) -> u8;

    // Used for memory fetching
    fn read_u32(&mut self, addr: u64) -> u32 {
        assert!(addr % 4 == 0, "read-address-misaligned");
        let data = [0, 1, 2, 3].map(|i| self.read_u8(addr + i));
        u32::from_le_bytes(data)
    }

    // Used for instruction fetching
    fn fetch_u32(&mut self, addr: u64) -> u32 {
        assert!(addr % 4 == 0, "read-address-misaligned");
        let data = [0, 1, 2, 3].map(|i| self.read_u8(addr + i));
        u32::from_le_bytes(data)
    }

    fn read_u64(&mut self, addr: u64) -> u64 {
        assert!(addr % 8 == 0, "read-address-misaligned");
        let data = [0, 1, 2, 3, 4, 5, 6, 7].map(|i| self.read_u8(addr + i));
        u64::from_le_bytes(data)
    }

    fn write_u8(&mut self, addr: u64, value: u8);

    fn write_u64(&mut self, addr: u64, value: u64) {
        assert!(addr % 8 == 0, "write-address-misaligned");
        let data = value.to_le_bytes();
        data.iter()
            .enumerate()
            .for_each(|(i, b)| self.write_u8(addr + i as u64, *b));
    }

    // Return inital stack pointer
    fn sp(&self) -> u64;

    fn entry_point(&self) -> u64;

    // Return part of memory corresponding to the executable program, as (address, length)
    fn text(&self) -> (u64, u64);
}

Simulator will check all memory operation such as r/w for program, regs, memory. In Jolt, it should collect all reads and writes, and then in MemoryChecking, it will prove

[jeong0982]

MemoryTracer:

pub struct MemoryTracer<M: Memory> {
    pub mem: M,            // Memory state
    pub trace: Vec<MemOp>, // Chronological trace of memory operations
    pub t: u64,            // Timestamp counter
}

It collects all memory operations MemOp

// Memory operation (read or write)
#[derive(Debug, Clone)]
pub struct MemOp {
    addr: u64,
    t: u64,
    rw: RW,
    value: u8,
}

[ed255]

I think to simplify the implementation we can skip the trait, and have a single implementation. What would be the pros of defining a trait?

For the implementation, I think a simple solution would be to follow the same approach we do in the zkEVM, which is also described in Jolt Appendix B.2. We would need the following:

• In the execution trace area of the circuit, we will need the columns (addr, t, rw, value) that contain the rw operations done by each step. Jolt describes that each rw operation is 1 byte. This complicates things a bit because it means each step can do 1, 2, 4 or 8 memory operations. At the end we should end with the commitment to (addr, t, rw, value) which form a table of memory operations sorted chronologically (we can call this mem_chrono), and each element of the table is constrained by the instructions (except for the read values, which are non-deterministic witnesses, and will be verified via the later permutation)
• In another area of the circuit, we will lay out another set of (addr, t, rw, value) columns where operations are sorted by [addr, t] (we can call this mem_byaddr). This table contains 2 constraints:
  • [addr.prev, t.prev] < [addr.next, t.next]. Both addr and t cab be bounded in range, for example 32 bits for each. This means we can easily use a LT table with LT[addr.prev + 2^32 * t.prev, addr.next + 2^32 * t.next] == 1
  • if addr.next == addr.prev { t.next == t.prev }

Finally we do a permutation check between mem_chrono and mem_byaddr

[DoHoonKim8]

I see. My intention was since there are multiple arguments to check memory consistency, we can have one trait to abstract all of them.

Appendix B.3 in Jolt paper is Thaler's offline memory checking(which uses GKR), and also there is another version of memory checking argument which reduces the proof size of Thaler's argument(https://eprint.iacr.org/2020/1275.pdf). This is explained in Appendix E of Lasso paper. I thought it would be useful to have implementations for each of them and then compare.

However if Jolt library will gonna only use the method explained in Appendix B.2 for memory checking, I agree with that we can have single implementation.

[ed255]

I see. My intention was since there are multiple arguments to check memory consistency, we can have one trait to abstract all of them.

Appendix B.3 in Jolt paper is Thaler's offline memory checking(which uses GKR), and also there is another version of memory checking argument which reduces the proof size of Thaler's argument(https://eprint.iacr.org/2020/1275.pdf). This is explained in Appendix E of Lasso paper. I thought it would be useful to have implementations for each of them and then compare.

Let me add this new one hehe: https://eprint.iacr.org/2023/1555.pdf

However if Jolt library will gonna only use the method explained in Appendix B.2 for memory checking, I agree with that we can have single implementation.

Now I understand why you were thinking about a trait. I was thinking about implementing a single method for the sake of simplicity, and if we identify that it's a performance bottleneck we could replace it with another method. Defining a trait for the memory checking sounds very interesting in theory but I fear that it may need a lot of work to get the trait right (one that encapsulates the problem well but also allows having well optimized implementations of the memory checking). Personally I would prefer to start without a trait and choose one memory checking method; and after we get everything working revisit the idea of a trait.

[DoHoonKim8]

Makes sense. Let's revisit this issue later after we have working memory checking implementation and if it has performance issue!