An universal memory prover in Zero-Knowledge Proof

Overview

The idea is to create an independent module that can be used by any zkVM. You might aware that the memory can be constructed as a simple state machine with $2$ instructions READ and WRITE, and configurable WORD_SIZE. Our memory state machine is only able access the exactly WORD_SIZE for every executed instruction. That is, if you want to access arbitrary data size, it must be translated to multiple accesses.

These instructions need to be satisfied following conditions:

• READ instruction
  • READ on a memory was not wrote should return 0
  • EveryREAD access for the same location, must have the value to be equal to the previous WRITE.
• WRITE instruction
  • Every WRITE access must write on writable memory chunks (some areas of the memmory might be read only).

Features

Configurable Word Size

For now we support U256, u64, and u32 word size.

• U256 word size with this feature it can be generate the execution trace for the following for zkEVM.
• u64 and u32 word size allow us to emulate wide range of VM namely RISC-V, x86, ARM, etc.

Memory Layout

The memory layout is configurable with ConfigArgs::head_layout, the buffer was used to prevent the memory access out of bound. The buffer size is configurable with ConfigArgs::buffer_size.

Head layout:

┌──────────────────┐ ┌──────┐ ┌──────────────────┐ ┌──────┐ ┌──────────────────┐
│  Stack Section   │ │Buffer│ │ Register Section │ │Buffer│ │  Memory Section  │
└──────────────────┘ └──────┘ └──────────────────┘ └──────┘ └──────────────────┘

Tail layout:

┌──────────────────┐ ┌──────┐ ┌──────────────────┐ ┌──────┐ ┌──────────────────┐
│  Memory Section  │ │Buffer│ │  Stack Section   │ │Buffer│ │ Register Section │
└──────────────────┘ └──────┘ └──────────────────┘ └──────┘ └──────────────────┘

Simulate Stack

                 ┌─────────┐
               ┌─┤Stack Ptr│
               │ └─────────┘
               │
┌───────────┐ ┌▼──────────┐ ┌───────────┐
│Memory Cell│ │Memory Cell│ │Memory Cell│
└───────────┘ └───────────┘ └───────────┘

We use memory cell and stack pointer to simulate the stack. We defined two new instruction to simulate the stack PUSH and POP.

• The PUSH instruction will write the value to the memory cell pointed by the stack pointer, and then increment the stack pointer.
• The POP instruction will decrement the stack pointer, and then read the value from the memory cell pointed by the stack pointer.

These two instructions should be consider as aliases of WRITE and READ instructions, the differences are these read and write are always happen on the stack memory area and bound to stack_depth and stack_ptr.

Simulate Register

An section of memory will be reserved to simulate the register. Each memory cell will be mapped to a register by method RegisterMachine::register(register_index);.

/// Register Machine with 3 simple opcodes (mov, set, get)
pub trait RegisterMachine<K, V, const S: usize>
where
    K: Base<S>,
{
    /// Get address for a register
    fn register(&self, register_index: usize) -> Result<Register<K, S>, Error>;
    /// Move a value from one register to another
    fn mov(&mut self, to: Register<K, S>, from: Register<K, S>) -> Result<(), Error>;
    /// Set a value to a register
    fn set(&mut self, register: Register<K, S>, value: V) -> Result<(), Error>;
    /// Read a value from a register
    fn get(&mut self, register: Register<K, S>) -> Result<V, Error>;
}

Code coverage

cargo llvm-cov --html --open

For more detail check 64bits-machine example

In this example we tried to simulate a 64bits machine with 64bits word size with 4 registers (r0, r1, r2, r3).

cargo run --example 64bits-machine

Execution trace:

Pop value: 0x0000000000000506
Read value: 0x0a0c0e1012141618
Execution record format is: Instruction(address, time_log, stack_depth, value)
        Write (0000000000000008, 0000000000000001, 0000000000000000, 0102030405060708)
        Read  (0000000000000008, 0000000000000002, 0000000000000000, 0102030405060708)
        Write (fffffffffffffef0, 0000000000000003, 0000000000000000, 0102030405060708)
        Write (0000000000000000, 0000000000000004, 0000000000000000, 090a0b0c0d0e0f10)
        Read  (0000000000000000, 0000000000000005, 0000000000000000, 090a0b0c0d0e0f10)
        Write (fffffffffffffef8, 0000000000000006, 0000000000000000, 090a0b0c0d0e0f10)
        Read  (fffffffffffffef0, 0000000000000007, 0000000000000000, 0102030405060708)
        Read  (fffffffffffffef8, 0000000000000008, 0000000000000000, 090a0b0c0d0e0f10)
        Write (fffffffffffffef0, 0000000000000009, 0000000000000000, 0a0c0e1012141618)
        Read  (fffffffffffffef0, 000000000000000a, 0000000000000000, 0a0c0e1012141618)
        Write (0000000000000010, 000000000000000b, 0000000000000000, 0a0c0e1012141618)
        Push  (ffffffffffffdee8, 000000000000000c, 0000000000000001, 0000000000000102)
        Push  (ffffffffffffdef0, 000000000000000d, 0000000000000002, 0000000000000304)
        Push  (ffffffffffffdef8, 000000000000000e, 0000000000000003, 0000000000000506)
        Pop   (ffffffffffffdef8, 000000000000000f, 0000000000000002, 0000000000000506)
        Read  (0000000000000010, 0000000000000010, 0000000000000002, 0a0c0e1012141618)

License

This project licensed under the Apache License, Version 2.0.

build with ❤️ and 🦀