Stack Circuit 是關於如何管理與堆疊（stack）操作的電路設計。

Stack Circuit 基本概念：

• Stack Pointer (sp): 記錄當前堆疊頂部位置的指針。例如，在一個 PUSH 操作中，sp 遞減 (sp--)；在 POP 操作中，sp 遞增 (sp++)。
• INIT 條件和基本約束: 和 Memory Circuit 類似，但還包括 Stack Poimter 的管理和操作。
• Read/Write 運算的驗證: 確保讀/寫操作遵循 EVM 的規則並正確反映在堆疊上。

約束條件：

堆疊電路定義了一系列的約束和條件來保證堆疊操作的正確性：

• INIT:
  • rw === Write 並且 val === 0：不查詢先前的值。
• 基本約束:
  • rw 必須在 [0, 1] 範圍內（有效的讀/寫標記）。
  • key - key_prev 應在 [0, 1023] 範圍內。
  • key 必須在 [0, 1023] 範圍內。
• 特定條件的約束:
  • 當 key 不等於 key_prev 時：rw === Write 並且 val === 0（應初始化為0）。
  • 當 key 等於 key_prev 時：gc > gc_prev（應嚴格）。
  • 當 rw == Read 時：val === val_prev（應該是先前寫入的值）。

運算與約束：

堆疊操作（例如 PUSH, DUPX, MLOAD, MSTORE, 和 SWAPX）涉及不同的讀/寫和其他操作的約束條件，以確保它們正確無誤地反映在堆疊的狀態上。每個操作在 bus_mapping 中可能需要多個查找（lookup）來確保多個讀/寫操作在同一時間發生。

• 例如: 對於 DUPX 操作，我們需要確保來源值和新推送的值相等，所以它同時需要一個讀取和一個寫入在 bus mapping 中。

實現方法

@is_circuit_code
def check_stack(row: Row, row_prev: Row):
    get_call_id = lambda row: row.id()
    get_stack_ptr = lambda row: row.address()

    # 3.0. Unused keys are 0
    assert row.field_tag() == 0
    assert row.storage_key() == Word(0)

    # 3.1. First access for a set of all keys
    #
    # The first stack operation in a stack position is always a write (can't
    # read if it isn't written before)
    #
    # When the set of all keys changes (first access of a stack position in a call)
    # - It must be a WRITE
    if not all_keys_eq(row, row_prev):
        assert row.is_write == 1

    # 3.2. stack_ptr in range
    stack_ptr = get_stack_ptr(row)
    assert_in_range(stack_ptr, 0, MAX_STACK_PTR)

    # 3.3. stack_ptr only increases by 0 or 1
    if row.tag() == row_prev.tag() and get_call_id(row) == get_call_id(row_prev):
        stack_ptr_diff = get_stack_ptr(row) - get_stack_ptr(row_prev)
        assert_in_range(stack_ptr_diff, 0, 1)

    # 3.4. Stack initial value is 0
    assert row.initial_value == Word(0)

    # 3.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