如何为Cairo程序生成并验证STARK证明？本地实现疑问

一、15-puzzle场景下的完整工作流 #

以验证15-puzzle解的合法性为例，可通过Cairo官方工具链完成本地的证明生成与验证，流程如下：

1. 编写Cairo验证程序 #

需要编写核心功能为验证15-puzzle移动序列合法且最终达到目标状态的Cairo程序，需实现：

• 检查每一步移动的合法性（空白块仅能与上下左右方块交换）
• 确认初始状态经所有移动后与目标状态完全匹配

简化示例代码：

from starkware.cairo.common.math import assert_eq
from starkware.cairo.common.alloc import alloc

# 定义15-puzzle状态为16个元素的数组（4x4）
def is_valid_move(prev_state: felt*, curr_state: felt*) -> felt:
    # 定位空白块在前后状态中的位置
    let mut blank_prev = 0
    let mut blank_curr = 0
    for i in 0..16:
        if prev_state[i] == 0:
            blank_prev = i
        if curr_state[i] == 0:
            blank_curr = i
    # 验证空白块仅移动一格（上下左右）
    let diff = abs(blank_curr - blank_prev)
    if diff == 1 or diff == 4:
        # 检查非空白块位置元素一致
        let mut valid = 1
        for i in 0..16:
            if i != blank_prev and i != blank_curr:
                if prev_state[i] != curr_state[i]:
                    valid = 0
        return valid
    return 0

def apply_move(state: felt*, move: felt) -> felt*:
    # 根据移动方向生成新状态
    let new_state = alloc()
    for i in 0..16:
        new_state[i] = state[i]
    let blank_pos = 0
    for i in 0..16:
        if state[i] == 0:
            blank_pos = i
    # move=0上，1下，2左，3右
    match move {
        0: if blank_pos >=4 {
            new_state[blank_pos] = state[blank_pos-4]
            new_state[blank_pos-4] = 0
        },
        1: if blank_pos <12 {
            new_state[blank_pos] = state[blank_pos+4]
            new_state[blank_pos+4] = 0
        },
        2: if blank_pos %4 !=0 {
            new_state[blank_pos] = state[blank_pos-1]
            new_state[blank_pos-1] = 0
        },
        3: if blank_pos %4 !=3 {
            new_state[blank_pos] = state[blank_pos+1]
            new_state[blank_pos+1] = 0
        },
        _: assert_eq(0, 1, 'Invalid move')
    }
    return new_state

def verify_15_puzzle(initial_state: felt*, moves: felt*, move_count: felt, target_state: felt*) -> felt:
    let mut curr_state = alloc()
    for i in 0..16:
        curr_state[i] = initial_state[i]
    for i in 0..move_count:
        let new_state = apply_move(curr_state, moves[i])
        assert_eq(is_valid_move(curr_state, new_state), 1, 'Invalid move step')
        curr_state = new_state
    # 验证最终状态匹配目标
    for i in 0..16:
        assert_eq(curr_state[i], target_state[i], 'Final state mismatch')
    return 1

2. 编译Cairo程序 #

使用cairo-compile将源代码编译为可执行JSON格式：

cairo-compile 15_puzzle.cairo --output 15_puzzle.json

3. 生成执行轨迹与内存快照 #

通过cairo-run执行程序，同时保存证明所需的执行轨迹和内存快照：

cairo-run --program=15_puzzle.json --layout=small --trace_file=trace.bin --memory_file=memory.bin --program_input=input.json

• --layout=small：选择适合小规模计算的STARK参数，平衡速度与证明大小
• --program_input=input.json：传入初始状态、移动序列、目标状态的输入数据（需按Cairo输入格式提前编写）

4. 本地生成STARK证明 #

使用cairo-prove基于轨迹和内存文件生成STARK证明：

cairo-prove --program=15_puzzle.json --trace_file=trace.bin --memory_file=memory.bin --output=proof.json

5. 本地验证证明 #

用cairo-verify验证生成的证明有效性：

cairo-verify --program=15_puzzle.json --proof_file=proof.json

二、关于cairo-run的功能说明 #

cairo-run核心作用是执行Cairo程序并输出结果，同时可生成执行轨迹（trace）和内存快照（memory）文件，但它本身不直接生成STARK证明。生成的trace和memory是后续STARK prover生成证明的核心输入——STARK证明本质是对程序执行轨迹的合法性做密码学证明，这两个文件包含了完整的执行过程信息。

若不指定--trace_file和--memory_file参数，cairo-run仅输出程序执行结果，不会保存轨迹相关文件。

三、不依赖SHARP的本地证明方案 #

完全可以不依赖SHARP服务，通过Cairo官方工具链完成本地证明生成与验证：

• 依赖条件：安装完整的cairo-lang工具包（包含cairo-compile、cairo-run、cairo-prove、cairo-verify等工具）
• 核心逻辑：利用Cairo程序的执行轨迹和内存快照，通过STARK prover直接在本地生成证明，无需上传至第三方服务
• 注意事项：根据计算复杂度选择合适的layout参数（small/medium/large），15-puzzle这类简单场景用small即可，大规模计算可选择更大的layout保证安全性。

内容的提问来源于stack exchange，提问作者sinoTrinity