zk-STARK: イーサリアム上での複雑な自動戦闘計算の検証

DAOrayaki

特邀专栏作者

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

この記事は約12818文字で、全文を読むには約19分かかります

この投稿では、STARK がどのように機能するかについてはあまり深く説明しませんが、実際に STARK がどのように使用されるかについての実用的な概要を説明します。

AI要約

原作者：キラリ

原題: STARKs: Ethereum での複雑な自動戦闘計算の検証 — 分散型ゲームのスケーリング

イーサリアム上で複雑な関数を実行することは常に禁止事項であり、決して実行すべきではありません。ブロックチェーンの計算は、その正しさを検証するためにすべてのノードが同じ計算を実行する必要があるため、非常にコストがかかります。

StarkWare は、STARK (Scalable Transparent Proof of Knowledge) 証明を使用してイーサリアムのスケーリングを試みるイーサリアムスケーリングサービスの 1 つです。この投稿では、STARK がどのように機能するかについてはあまり深く説明しませんが、実際に STARK がどのように使用されるかについての実用的な概要を説明します。

STARK には、「ゼロ知識証明」を意味する「zk-」という接頭辞が付けられることがあります。これにより、証明しようとしている事柄に関するすべての情報を明らかにすることなく、STARK が何かを証明できるようになります。 StarkWare は、今後パイプラインに ZK を含めることに取り組んでいますが、現時点ではスケーラビリティのみに焦点を当てており、これを達成するために知識がゼロである必要はありません。

Vitalik のブログ投稿は、zk-SNARK がユーザーにどのように表示されるかを示しています。

Vitalik は記事の中で STARK の概要を簡単に説明しました。 STARK パート 1: 多項式による証明では、これらの暗号化プリミティブがどのように機能するかを簡単に説明します。 SNARK (Succinct Non-Interactive Arguments of Knowledge) もあり、これは STARK と似たものを実現しますが、少し異なります。 zk-SNARK を理解することにさらに興味がある場合は、この説明文書を強くお勧めします: zk-SNARK の原理と実装、Maksym Petkus による権威ある説明。 Petkus 氏は、先人の肩に立って、非常に基本的な数学から始めて、徐々により複雑な数学を深めながら、zk-SNARK の原理を説明しました。素晴らしい読書体験。

Petkus は zk-SNARK を次のように要約しています。

副題

STARK とオートバトルゲーム

自動戦闘ゲーム（自動戦闘機、オートチェスとも呼ばれる）は、プレイヤーがキャラクターの成長を選択するタイプのゲームであるが、戦闘中は何も選択することができず、自動的に進行する。このようなゲームをイーサリアム L1 上で実行できれば楽しいでしょうが、現時点ではそのようなゲームは実行できません。

では、STARK はオートバトルゲームにどのようなメリットをもたらすのでしょうか?自動戦闘ゲームのシミュレーションは非常に複雑なため、実行するのが困難です。 1 回だけ実行するテクノロジーがあり、誰も嘘をついていないことを確認しながら他のプレイヤーがこの計算を信頼することができれば、分散型自動プレイが可能になります。

行動計画は次のとおりです。

1) Pythonで自動戦闘ロジックを書きます。

2) StarkNet の Cairo 言語でバリデータを構築します (STARK 証明に必要)。

3) プログラム実行の STARK 証明を作成するために構築した Cairo バリデータを使用して、自動戦闘のコードを実行します。

副題

Python で自動戦闘システムを作成する

旅を始めるには、通常のように自動戦闘のロジックをプログラムするだけです。ここでは STARK 魔法は必要ありません。

2人のキャラクター間の自動戦闘シミュレーターを作成します。これらの役割には 4 つの状態があります。

- 健康。彼らが受けるダメージの合計に等しい。

@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
}

次に、この壮大な戦いを誰が行うかを選択しましょう:

ここでは、攻撃ごとに 48 ダメージを与えますが、攻撃の間に 80 回待機する長い体力バー (体力 1000!) を備えたオーガを用意します。オーガはまた、ターンごとに 3 ヘルスポイントを回復します。

私たちの挑戦者ヒーローの体力ははるかに低く、体力はわずか 240、体力の回復はまったくなく、攻撃ごとのダメージ (20) が少なくなりますが、私たちのヒーローは攻撃する前に 2 ターン待つだけです。つまり、少なくとも私たちのヒーローはオーガよりも優れているのです。これが私たちのヒーローです。これは本当のダビデとゴリアテの戦いです。

コード内で次のように役割を定義できます。

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

その後、combat 関数を呼び出して戦闘をシミュレートできます。

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 の多くの要件の 1 つは、すべての入力が負でないことです。これは私たちの開発者の不幸ですが、私たちのヒーローの祝福です、オーガの健康状態がマイナスになります、それは負の数です:(

この制限を回避するために、すべての体力値に 1000 を追加します。キャラクターの体力が 1000 未満の場合、そのキャラクターは死亡したものとみなされます。このメソッドがさまざまなキャラクターのダメージ値で機能するためには、キャラクターのダメージが 1000 を超えないようにする必要もあります。1000 を超えると、誰かの健康状態が再びマイナスになる可能性があるからです。コードは次のとおりです。

副題

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

Cairo バリデータの作成

次に、Python プログラムの実行を STARK できるようにする検証プログラムを作成する必要があります。プログラムは、初期のプレーヤー属性を指定して、シミュレーションコードの実行時にシミュレーターがログ領域に表示される正確な出力を生成することを検証できる必要があります。これを達成するために、カイロ言語でのプログラミングに切り替えます。

Python で見られるものと非常によく似た方法で、Cairo でロール構造を定義します。

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

ここでの Python との大きな違いは、すべての変数を見慣れないデータ型 (field 要素の略) に割り当てる必要があることです。フェルトデータ型は、(-P/2, P/2) の間で定義された 252 ビット (奇妙ですよね?) 変数型です。ここで、P は大きな 252 ビットの素数です。

奇妙に思えるかもしれませんが、私たちの目的では、フェルトは整数のように動作します。このデータ型の重要性は、実際に整数または浮動小数点の変数型を扱う場合よりも、Cairo コンパイラがコードから STARK 証明を作成する方が簡単であることです。フェルト変数タイプの詳細については、Cairo のドキュメントを参照してください。

さて、カイロプログラムの作成を開始して、戦闘が計画どおりに進んだこと、およびプログラムの実行者が他のプレイヤーに嘘をつかないことを確認しましょう。フェルト型と入力変数の非負性に加えて、Cairo には他にもいくつかの制限があります。 Python コードで while ループを使用しましたが、動的な長さのループは Cairo では不可能です。同じロジックを実装するには再帰が必要です。そこで、戦闘の 1 ラウンドを検証し、その後、他のすべての戦闘ラウンドを再帰的に検証する再帰関数を定義しましょう。

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)
)

この関数は、2 人のキャラクター、現在の体力と最後の攻撃タイマー、現在の戦闘ラウンド、およびシミュレートする戦闘ラウンドの数を受け取ります。次に、検証ラウンドの後に最後の攻撃の更新されたヘルスとタイマーを返し、次のラウンドを再帰的に検証できるようにします。

関数の先頭に range_check_ptr があることに気づいたかもしれません。 range_check_ptr は範囲チェックに使用する必要があるポインタです (演算子)<, >, >=,<=)。これらの操作はカイロでも困難ですが、幸いなことにカイロの 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

Cairo コードは、Python とは少し異なる方法で書かれています。これは、カイロでは定数変数しか使用できないためです (これも興味深い制限です)。変数に値を設定すると、その内容を変更することはできなくなります。そのため、体力回復のためにプレイヤーの体力を増やすときは、ダメージと同時に計算しました。

次に、必要なラウンド数をシミュレートしたかどうかを確認し、そうであればシミュレーションを終了します。シミュレーションがまだ終了していない場合は、両方のプレイヤーがまだ生きているかどうかを確認する必要があります。このチェックがなかった場合、悪意のあるエミュレータランナーは両方のプレイヤーが死亡するまで戦闘のシミュレーションを続けることができ、すでに死亡しているプレイヤーが戦闘を続けることが可能になってしまいます。私たちはそのような狂気を許すことはできません、私たちのアリーナにアンデッドの戦士が現れることを許すことはできません!

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 が false の場合、実行は失敗し、エミュレータを実行している人が嘘をついたことがわかります。

最後に、関数を呼び出してシミュレーションの次のラウンドを取得し、最終的なシミュレーション結果を返します。

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

シミュレーションロジックのコードを作成したら、Cairo プログラムの main 関数を作成する必要があります。プログラムは、Python プログラムの出力を読み取り、作成したばかりの SimulateCombat 関数を呼び出す必要があります。この関数は最終的なヘルス値を返します。その後、Python プログラムの出力と比較する必要があります。コードは次のとおりです。

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

副題

なぜ 2 つのプログラムが必要なのでしょうか?

副題

走る！

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

次のコマンドを使用して、パイファイルが正しいことを確認することもできます。

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

Battle-input.json ファイル内の結果のヘルス値を変更してみることができますが、Cairo から検証エラーが発生しないと変更できないことに注意してください。開始入力 (プレイヤー 1、プレイヤー 2、ターン数) ごとに、戦闘の解決策は 1 つだけです。たとえば、戦いの終わりにヒーローに追加の体力バーを与えて不正行為をしようとした場合、バリデーターは私たちが不正行為をしようとしていることに気づきます。

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、およびラウンド数) に対して、ファクトハッシュが与えられた場合、プログラムは最終的なヘルス値を出力する必要があることがわかったので、計算をオンチェーンで検証する必要がなくなります。オンチェーンでもう一度実行して計算を実行します。

実際、欠けている情報がもう 1 つあり、それはプログラムのハッシュです。

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

これは、これまでのすべての作業の集大成であり、現代の暗号技術の驚異であり、事実を検証し、programOutput が有効であることをチェックする単純な Solidity 関数です。計算自体はすべて不要です。

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.
}