zk-STARK: 在以太坊上驗證複雜的自動對戰計算

DAOrayaki

特邀专栏作者

2022-08-14 13:08 (UTC+8)

本文約12818字，閱讀全文需要約19分鐘

在這篇文章中，我不會太深入於STARK是如何工作的，但我將對它在實踐中的應用做一個實際的概述。

AI總結

展開

在這篇文章中，我不會太深入於STARK是如何工作的，但我將對它在實踐中的應用做一個實際的概述。

原文作者: Killari

原文標題: STARKs: Verifying complex auto battler calculation on Ethereum — Scaling decentralized games

在以太坊上執行複雜的函數一直是一個大忌，永遠不應該這麼做。區塊鏈計算是非常昂貴的，因為需要所有節點執行相同的計算來驗證其正確性。

StarkWare 是以太坊擴展服務之一，它試圖使用STARK（可擴展的透明知識論證）證明來擴展以太坊。在這篇文章中，我不會太深入於STARK 是如何工作的，但我將對它在實踐中的應用做一個實際的概述。

有時在STARK 前面加上“zk-”前綴，表示“零知識證明”，這使得STARK 能夠在不透露我們試圖證明的事物的所有信息的情況下證明一些東西。 StarkWare 公司正致力於在以後的管道中加入ZK，但現在他們只關注可擴展性，而要實現這一點並不需要零知識。

Vitalik 的博客文章對於zk-SNARK 如何呈現在用戶面前所繪製的插圖。

Vitalik 在他的文章中對STARK做了一個簡短的概述。 STARK 第一部分：用多項式進行證明，簡要解釋了這些加密基元的工作原理。還有SNARK（簡潔的非交互式知識論證），可以實現與STARK 類似的東西，但有點不同。如果對理解zk-SNARK 更感興趣，強烈推薦這篇解釋論文：zk-SNARK 的原理和實現，Maksym Petkus 的權威解釋。 Petkus 解釋了zk-SNARK 的原理，從非常基本的數學，然後逐步深入更複雜的數學，站在前人的肩膀上眺望。非常棒的閱讀體驗。

二級標題

STARK 和自動對戰遊戲

自動對戰遊戲（也叫自動對戰機、自走棋）是一種遊戲類型，玩家在其中做出角色成長的選擇，但在戰鬥當中不能做出任何選擇，而是自動進行。如果有這樣的遊戲在以太坊L1 上運行，會很好玩，但目前這樣的遊戲做不起來。

那麼，STARK 能給自動對戰遊戲帶來什麼好處呢？自動對戰遊戲的模擬可能是非常複雜的，所以很難跑起來。如果有一種技術可以使它只運行一次，而其他玩家可以只相信這種計算，同時確信沒有人在說謊，這將使我們能夠擁有一個去中心化的自動對戰。

以下是行動計劃：

1) 用Python 編寫自動對戰邏輯。

2) 用StarkNet 的Cairo 語言建立一個驗證器（STARK 證明需要）。

二級標題

用Python 編寫自動戰鬥系統

為了開始我們的旅程，我們簡單地對自動對戰的邏輯進行編程，就像我們平時做的那樣，這裡不需要STARK 的魔法。

我們在兩個角色之間做一個自動對戰的模擬器。這些角色有四種狀態：

- 健康。等於他們能承受的傷害總量。

@dataclass
class Character:
  health: int
  damage: int
  attackRecoverTime: int
  healthPerTurn: int

- 傷害。他們每次攻擊會給對方造成多大的傷害。

- 攻擊恢復時間：每次攻擊後，攻擊者需要等待多長時間才可以再次攻擊。

- 每回合健康：角色每回合恢復多少健康值。

這些屬性可以在Python 中定義為一個類，如下所示。

以下是關於戰鬥將如何滾動的詳述：

我們有一個遊戲循環，會循環進行各輪戰鬥。
在每一次迭代中，我們為兩個角色恢復健康，並讓他們以最快的速度互相毆打。
我們將使這些角色戰鬥到死亡。如果其中一個角色死了，或者兩個角色都死了，視為戰鬥結束。

通過選擇特定的角色屬性，有可能出現戰鬥永遠不會結束，而是一直持續的情況。這可以通過，例如，限制我們的戰鬥能持續的最大回合數來避免，然後考慮以平局解決戰鬥，我們的示例代碼中不打算考慮這種情況。

在模擬結束時，讓我們返回每個角色還剩下多少健康值，以及計算戰鬥花了多少個回合。

下面是用Python 代碼編寫的版本：

def simulateFight(character1, character2):
currentTick = 0
lastAttack = [0, 0]

while 1:
     # Health regeneration
     character1.health += character1.healthPerTurn
     character2.health += character2.healthPerTurn

     # Player 1 hits player 2
     if (lastAttack[0] == character1.attackRecoverTime):
         character2.health -= character1.damage
         lastAttack[0] = 0
     else:
         lastAttack[0] = lastAttack[0] + 1

     # Player 2 hits player 1
     if (lastAttack[1] == character2.attackRecoverTime):
         character1.health -= character2.damage
         lastAttack[1] = 0
     else:
         lastAttack[1] = lastAttack[1] + 1

     if character1.health <= 0 or character2.health <= 0:
         # one of the characters have died
         break
     currentTick = currentTick + 1

return {
     'endHealths': [character1.health, character2.health],
     'nCombatRounds': currentTick
}

接下來，讓我們選出誰將會有這場史詩般的戰鬥：

我們將有一個食人魔，它有很長的血條（1000 血量！），每次攻擊造成48點傷害，但每次攻擊之間需要等80下。食人魔每回合還能恢復三點健康值。

我們的挑戰者英雄的生命值要低得多，只有240血，完全沒有生命值恢復，每次攻擊的傷害較小（20），但我們的英雄只需等待2個回合就可以攻擊。因此，至少我們的英雄在某種程度上比食人魔要好！這就是我們的英雄。這是一場真正的大衛和歌利亞之間的戰鬥。

我們可以在代碼中定義我們的角色，如下所示

player1 = Character(1000, 48, 80, 3) # Ogre
player2 = Character(240, 20, 2, 0) # Hero

然後我們可以通過調用戰鬥函數來模擬戰鬥。

simulateFight(player1, player2

我們將得到戰鬥的結果：

{
    "player1": {
     "stats": [
      2000,
      48,
      80,
      3
     ]
    },
    "player2": {
     "stats": [
      1240,
      20,
      2,
      0
     ]
    },
    "log": {
     "endHealths": [
      999,
      1096
     ],
     "nCombatRounds": 272
    }
}ZERO_HP_POINT = 1000
assert player1.damage < ZERO_HP_POINT
assert player2.damage < ZERO_HP_POINT
data = {
    'player1': {
     'stats': [ZERO_HP_POINT + player1.health, player1.damage, player1.attackRecoverTime, player1.healthPerTurn]
    },
    'player2': {
     'stats': [ZERO_HP_POINT + player2.health, player2.damage, player2.attackRecoverTime, player2.healthPerTurn]
    },
  'log': simulateFight(player1, player2)
}
data['log']['endHealths'] = [h + ZERO_HP_POINT for h in data['log']['endHealths']]
with open('combat-input.json', 'w') as outfile:
json.dump(data, outfile)

我們可以從結果中讀出，這場戰鬥持續了272個回合，戰鬥結束是因為食人魔被打敗了。我們的英雄以巨多的96點血取得了勝利！這就是我們的英雄。

接下來讓我們把所有關於戰鬥的必要的重要信息存儲在一個文件中，這樣我們就可以在以後用STARK 證明來證明這場戰鬥。我們所需要的是程序輸入（玩家1和玩家2的定義）和程序輸出（結束時的生命值和所花的回合數）。我們的驗證器根本不需要程序本身！

我們將用Cairo 編寫驗證器。 Cairo 是一種用於編寫可驗證程序的編程語言。 Cairo 的許多要求之一是，所有的輸入都必須是非負數。這是我們開發人員的不幸，但是我們英雄的幸事，食人魔的健康值會變負，這就是一個負數:(

二級標題

{
    "player1": {
     "stats": [
      2000,
      48,
      80,
      3
     ]
    },
    "player2": {
     "stats": [
      1240,
      20,
      2,
      0
     ]
    },
    "log": {
     "endHealths": [
      999,
      1096
     ],
     "nCombatRounds": 272
    }
}

編寫Cairo 驗證器

接下來，我們需要編寫一個驗證器程序，以便能夠對我們的Python 程序的執行進行STARK 證明。這個程序需要能夠驗證，在給定初始玩家屬性的情況下，當模擬代碼運行時，模擬器會產生顯示在log 區域的確切輸出。為了實現這一點，我們將改用Cairo 語言編程。

我們將在Cairo 中定義角色結構，其方式與我們在python 中看到的非常相似：

struct Character:
    member health: felt
    member damage: felt
    member attackRecoverTime: felt
    member healthPerTurn: felt
end

與Python 相比，這裡的一個很大的區別是，我們需要將所有的變量指定為某種陌生的數據類型felt （域元素field element 的縮寫）。 felt 數據類型是一個252位（很奇怪，不是嗎？）的變量類型，定義在(-P/2, P/2) 之間，其中P是一個252位的大素數。

雖然看起來很奇怪，但對於我們的目的來說，felt 的行為就像一個整數。這種數據類型的意義在於，與我們實際處理整數或浮點變量類型相比，Cairo 編譯器更容易從我們的代碼中做出STARK 證明。你可以從Cairo 的文檔中閱讀更多關於felt 變量類型的信息。

現在，讓我們開始編寫Cairo程序，以確保戰鬥已經按計劃進行，而且程序的執行者不能對其他玩家撒謊。除了輸入變量的felt 類型和非負性之外，Cairo 還有一些其他的限制。我們在Python 代碼中使用了一個while 循環，但是動態長度循環在Cairo 中是不可能的，我們需要通過遞歸來實現同樣的邏輯。因此，讓我們定義一個遞歸函數，它將驗證一個單一回合的戰鬥，然後再遞歸驗證所有其他回合的戰鬥：

func simulateCombat{ range_check_ptr } (
player1: Character,
player2: Character,
currentHealths: (felt, felt),
lastAttacks: (felt, felt),
currentRound: felt,
nCombatRounds: felt
) -> (
simNextHealths: (felt, felt),
simNextLastAttacks: (felt, felt)
)

該函數接收我們的兩個角色，他們當前的健康狀況和最後一次攻擊的計時器，當前的戰鬥回合和要模擬的戰鬥回合數。然後，我們將在驗證回合後返回更新的健康和最後一次攻擊的計時器，以便能夠通過遞歸驗證下一個回合。

你可能已經註意到了我們函數開頭的range_check_ptr。 range_check_ptr 是一個指針，我們需要用它來進行範圍檢查（運算符<, >, >=,<=）。這些運算在Cairo 中也很困難，但幸運的是，我們仍然能夠通過使用Cairo 的range_check_ptr 內置函數來完成這些運算。

接下來，讓我們開始定義函數的內部內容。我們基本上實現了與我們在Python 中的戰鬥回合完全相同的邏輯：

alloc_locals
local nextHealths: (felt, felt)
local nextLastAttacks: (felt, felt)
local ZERO_HP_POINT = 1000
if lastAttacks[1] == player2.attackRecoverTime:
tempvar afterDamage = currentHealths[0] - player2.damage
nextHealths[0] = afterDamage + player1.healthPerTurn
nextLastAttacks[1] = 0
else:
nextHealths[0] = currentHealths[0] + player1.healthPerTurn
nextLastAttacks[1] = lastAttacks[1] + 1
end
if lastAttacks[0] == player1.attackRecoverTime:
tempvar afterDamage = currentHealths[1] - player1.damage
nextHealths[1] = afterDamage + player2.healthPerTurn
nextLastAttacks[0] = 0
else:
nextHealths[1] = currentHealths[1] + player2.healthPerTurn
nextLastAttacks[0] = lastAttacks[0] + 1
end

與Python 相比，Cairo 代碼的編寫方式有些不同。這是因為在Cairo 中我們只能利用常數變量（這是另一個有趣的限制）。一旦我們為一個變量設置了一個值，我們就不能再改變它的內容。因此，當我們為健康恢復而增加玩家的生命值時，我們在計算傷害的同時也計算了它。

接下來我們將檢查我們是否已經模擬了所要求的回合數，如果是，我們就結束模擬。如果模擬還沒有結束，我們需要檢查兩個玩家是否還活著。如果我們沒有這個檢查，惡意的模擬器運行者可以一直模擬戰鬥，直到兩個玩家都死了，這會讓一個已經死了的玩家繼續戰鬥！我們不能允許這樣的瘋狂行為，我們不能允許不死的戰士出現在我們的競技場上！

if currentRound == nCombatRounds:
return(nextHealths, nextLastAttacks)
else:
# if the combat has not ended, nobody can be dead
assert_nn(nextHealths[0] - ZERO_HP_POINT)
assert_nn(nextHealths[1] - ZERO_HP_POINT)
end

這裡我們使用的是assert_nn 函數，它正在檢查函數內部的值是否為非負值：nextHealths[0] > ZERO_HP_POINT。如果assert 為假，則執行失敗，我們知道運行模擬器的人對我們撒謊了。

最後，讓我們調用我們的函數來獲得下一輪的模擬，然後我們將返回最終的模擬結果。

let (simulatedEndHealths, simulatedLastAttacks) = simulateCombat(
player1 = player1,
player2 = player2,
currentHealths = nextHealths,
lastAttacks = nextLastAttacks,
currentRound = currentRound + 1,
nCombatRounds = nCombatRounds
)
return(
simNextHealths = simulatedEndHealths,
simNextLastAttacks = simulatedLastAttacks
)

二級標題

func main{ output_ptr: felt*, range_check_ptr }() -> ():
alloc_locals
local range_check_ptr = range_check_ptr
local pl1: Character*
local pl2: Character*
local endHealths: felt*
local nCombatRounds: felt
%{
     log = program_input['log']
     dat_endHealths = log['endHealths']
     dat_nCombatRounds = log['nCombatRounds']

     ids.pl1 = pl1 = segments.add()
     for i, val in enumerate(program_input['player1']['stats']):
         memory[pl1 + i] = val

     ids.pl2 = pl2 = segments.add()
     for i, val in enumerate(program_input['player2']['stats']):
         memory[pl2 + i] = val
     ids.endHealths = endHealths = segments.add()
     for i, val in enumerate(dat_endHealths):
         memory[endHealths + i] = val
     ids.nCombatRounds = dat_nCombatRounds
     assert len(program_input['player1']['stats']) == 4
     assert len(program_input['player2']['stats']) == 4
     assert len(dat_endHealths) == 2
%}

local player1: Character = pl1[0]
local player2: Character = pl2[0]

local currentHealths: (felt, felt) = (player1.health, player2.health)
local lastAttacks: (felt, felt) = (0, 0)

let (simulatedEndHealths, lastSimulatedAttacks) = simulateCombat(
     player1 = player1,
     player2 = player2,
     currentHealths = currentHealths,
     lastAttacks = lastAttacks,
     currentRound = 0,
     nCombatRounds = nCombatRounds
)

# Check that the healths will match what was claimed
assert simulatedEndHealths[0] = endHealths[0]
assert simulatedEndHealths[1] = endHealths[1]
# Return the program input and output
serialize_word(player1.health)
serialize_word(player1.damage)
serialize_word(player1.attackRecoverTime)
serialize_word(player1.healthPerTurn)

serialize_word(player2.health)
serialize_word(player2.damage)
serialize_word(player2.attackRecoverTime)
serialize_word(player2.healthPerTurn)

serialize_word(simulatedEndHealths[0])
serialize_word(simulatedEndHealths[1])

return ()
end

二級標題

運行！

我們可以運行Python 模擬器，用以下命令編譯我們的Cairo 驗證器：

> python combat.py
> cairo-compile combat.cairo -- output combat-compiled.json

然後我們可以用我們用combat.py 生成的輸入文件來運行Cairo 程序，生成combat.pie 文件：

> cairo-run -- program=combat-compiled.json -- program_input=combat-input.json -- layout=small -- cairo_pie_output=combat.pie

我們還可以用以下命令驗證pie 文件是否正確：

> cairo-run -- layout=small -- run_from_cairo_pie=combat.pie

你可以嘗試修改battle-input.json 文件的結果健康值，要注意的是，如果不得到Cairo 的驗證錯誤，你就不能修改它們。對於每個起始輸入（玩家1，玩家2和回合數），戰鬥只有一種解決方式。例如，如果我們試圖作弊，在戰鬥結束時給我們的英雄多加一個健康值，驗證器會注意到我們在試圖作弊。

combat.cairo:120:5: Error at pc=0:201:
An ASSERT_EQ instruction failed: 1096 != 1097
assert simulatedEndHealths[1] = endHealths[1]
^*******************************************^

.pie 文件包含了SHARP 為我們進行證明生成所需的所有信息。 SHARP 是由StarkWare 運營的一項服務，它可以生成證明，證明Cairo 程序執行的有效性。然後，它將這些證明發送到以太坊測試網（Goerli），由以太坊智能合約進行驗證。

目前，SHARP 不能在本地運行，從Cairo 程序中生成證明的唯一方法是利用StarkWare 的服務器來做證明驗證。希望這種情況在未來會有所改變，任何人都可以生成關於任何東西的證明。 StarkWare 公司計劃在稍後階段發布SHARP 的源代碼。目前現狀來說，去中心化的遊戲無法使用Cairo 來構建。

讓我們向SHARP 提交我們的工作吧：

> cairo-sharp submit -- cairo_pie combat.pie
Submitting to SHARP...
Job sent.
Job key: f48c551e-c0c6-4cf5-8a52-a0aa1c43728c
Fact: 0x17ee903dfb54b55e53cc03d5a47602e83ed0ff9e219fe4567b8d59fa2666f682

二級標題

> cairo-sharp is_verified 0x17ee903dfb54b55e53cc03d5a47602e83ed0ff9e219fe4567b8d59fa2666f682 -- node_url=https://goerli-light.eth.linkpool.io/
True

二級標題

https://www.cairo-lang.org/playground/sharp.html?job_key=f48c551e-c0c6-4cf5-8a52-a0aa1c43728c

在以太坊智能合約上利用證明

現在我們知道，對於給定的輸入值（玩家1、玩家2和回合數），給定事實哈希值，程序應該輸出最終的健康值，我們能夠在鏈上驗證計算，而無需在鏈上再次執行計算。

實際上，我們還缺少一個信息，那就是程序的哈希值。

> cairo-hash-program -program combat-compiled.json
0x248070cb7b7f20b0b9445a382fdb4faa6b69c1f3653355077ae05b82c636ddf

這是我們之前所有工作的高潮，現代密碼學的奇蹟，一個簡單的Solidity 函數可以驗證一個事實並檢查程序輸出programOutput 是否有效。所有這些都不需要計算本身。

function verifyCombatOutput(uint256[] memory programOutput) public
bytes32 cairoProgramHash_ = 0x248070cb7b7f20b0b9445a382fdb4faa6b69c1f3653355077ae05b82c636ddf
// Ensure that a corresponding proof was verified.
bytes32 outputHash = keccak256(abi.encodePacked(programOutput));
bytes32 fact = keccak256(abi.encodePacked(cairoProgramHash_, outputHash));
require(cairoVerifier_.isValid(fact), "MISSING_CAIRO_PROOF");
// Ensure the output consistency with current system state.
require(programOutput.length == 10, "INVALID_PROGRAM_OUTPUT");
require(player1.health == programOutput[0], "INVALID_PROGRAM_OUTPUT 0");
require(player1.damage == programOutput[1], "INVALID_PROGRAM_OUTPUT 1");
require(player1.attackRecoverTime == programOutput[2], "INVALID_PROGRAM_OUTPUT 2");
require(player1.healthPerTurn == programOutput[3], "INVALID_PROGRAM_OUTPUT 3");

require(player2.health == programOutput[4], "INVALID_PROGRAM_OUTPUT 4");
require(player2.damage == programOutput[5], "INVALID_PROGRAM_OUTPUT 5");
require(player2.attackRecoverTime == programOutput[6], "INVALID_PROGRAM_OUTPUT 6");
require(player2.healthPerTurn == programOutput[7], "INVALID_PROGRAM_OUTPUT 7");

// Now we know that programOutput[8] and programOutput[9] represent the resulting health values,
// given the initial combat state variables programOutput[0..7]!.

// Pure Magic.
}