Memory Circuit 是一個用來驗證存儲操作（例如，讀取和寫入操作）的零知識證明電路。

Memory Circuit 的核心元素

在Memory Circuit中，Prover 需要執行以下操作：

• 收集所有的 MLOAD 和 MSTORE 操作。
• 通過 key 對這些操作進行排序，然後通過 gc（可能指的是全局計數器 global counter）進一步排序。
• 建立一個布局（可能是一個表或數據結構），包括列 key、val、rw 和 gc。

這些列分別代表：

• key - 我們正在操作的記憶體的關鍵（地址）。
• val - 操作後的 memory[key] 的值。
• rw - 存取枚舉，其值可以是：
  • 0 - 讀取（Read）
  • 1 - 寫入（Write）

還使用了一些輔助標註：

• key_prev - 上一行的 key 值。
• gc_prev - 上一行的 gc 值。
• val_prev - 上一行的 val 值。

約束條件

此外，還有一些約束條件與注意事項：

• INIT: rw 必須等於 Write 且 val 必須等於 0。這是電路的第一行，並且它不查詢上一行的值。
• rw 必須屬於 [0, 1]，確保它是一個有效的讀/寫標記。
• key - key_prev 必須在 [0, ?] 範圍內，保證它是非嚴格單調的。
• val 必須屬於 [0, 255]，以確保它是一個位元組值。
• 當 key 不等於 key_prev 時，rw 必須等於 Write 且 val 必須等於 0，確保新鍵值被初始化為0。
• 當 key 等於 key_prev 時，gc 必須大於 gc_prev，確保它是嚴格單調的。
• 當 rw 等於 Read 時，val 必須等於 val_prev，確保它是之前寫入的值。

實現方法

def check_memory(row: Row, row_prev: Row):
    get_memory_address = lambda row: row.address()

    # 2.0. Unused keys are 0
    assert row.field_tag() == 0
    assert row.storage_key() == Word(0)
    assert row.value.hi == 0
    assert row.initial_value.hi == 0

    # 2.1. First access for a set of all keys
    #
    # When the set of all keys changes (first access of an address in a call)
    # - If READ, value must be 0
    if not all_keys_eq(row, row_prev) and row.is_write == 0:
        assert row.value.value() == 0

    # 2.2. mem_addr in range
    assert_in_range(get_memory_address(row), 0, MAX_MEMORY_ADDRESS)

    # 2.3. value is a byte
    assert_in_range(row.value.value(), 0, 2**8 - 1)

    # 2.4. Start initial value is 0
    assert row.initial_value.value() == 0

    # 2.5. state root does not change
    assert row.root == row_prev.root

參考資料

https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/src/zkevm_specs/state_circuit.py