DAOrayaki ｜zk-STARK: 在以太坊上验证复杂的自动对战计算

Zero-knowledge and layer2

8 months ago • 20 min read

DAOrayaki ｜zk-STARK: 在以太坊上验证复杂的自动对战计算

Zero-knowledge and layer2

8 months ago • 20 min read • Loading Views

DAOrayaki DAO研究奖金池：

资助地址: DAOrayaki.eth

投票进展：DAO Reviewer 2/0 通过

赏金总量：40 USD

研究种类：ZK

原文作者: Killari

创作者：Xinyang@DAOrayaki.org

审核者：DAOctor@DAOrayaki.org

原文: 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 的原理，从非常基本的数学，然后逐步深入更复杂的数学，站在前人的肩膀上眺望。非常棒的阅读体验。

Petkus 对 zk-SNARK 总结如下：

零知识简明非交互式知识论证（zk-SNARK）是真正巧妙的方法，可以证明某件事情是真实的，而不透露任何其他信息。

STARK 和自动对战游戏

自动对战游戏（也叫自动对战机、自走棋）是一种游戏类型，玩家在其中做出角色成长的选择，但在战斗当中不能做出任何选择，而是自动进行。如果有这样的游戏在以太坊 L1 上运行，会很好玩，但目前这样的游戏做不起来。

那么，STARK 能给自动对战游戏带来什么好处呢？自动对战游戏的模拟可能是非常复杂的，所以很难跑起来。如果有一种技术可以使它只运行一次，而其他玩家可以只相信这种计算，同时确信没有人在说谎，这将使我们能够拥有一个去中心化的自动对战。

以下是行动计划：

1) 用 Python 编写自动对战逻辑。

2) 用 StarkNet 的 Cairo 语言建立一个验证器（STARK 证明需要）。

3) 执行自动战斗的代码，用我们建立的 Cairo 验证器创建一个关于程序执行的 STARK 证明。

4) 观察我们如何在以太坊的 Solidity 环境利用自动战斗器的战斗结果。

用 Python 编写自动战斗系统

为了开始我们的旅程，我们简单地对自动对战的逻辑进行编程，就像我们平时做的那样，这里不需要 STARK 的魔法。

我们在两个角色之间做一个自动对战的模拟器。这些角色有四种状态：

- 健康。等于他们能承受的伤害总量。

@dataclassclass 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) # Ogreplayer2 = 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 = 1000assert player1.damage < ZERO_HP_POINTassert player2.damage < ZERO_HP_POINTdata = {    '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 的许多要求之一是，所有的输入都必须是非负数。这是我们开发人员的不幸，但是我们英雄的幸事，食人魔的健康值会变负，这就是一个负数 :(

为了绕过这个限制，我们将在所有的健康值上加上1000，如果一个角色的健康值低于1000，就认为他已经死亡。为了使这个方法适用于不同的角色伤害值，我们还需要确保一个角色的伤害永远不会超过1000，因为那样的话某人的健康状况可能会再次变成负数。以下是代码：

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

ZERO_HP_POINT = 1000assert player1.damage < ZERO_HP_POINTassert player2.damage < ZERO_HP_POINTdata = {    '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)

这段代码为我们产生了最终的模拟输出，它将被储存在 combat-input.json 文件中。

{    "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: feltend

与 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_localslocal nextHealths: (felt, felt)local nextLastAttacks: (felt, felt)local ZERO_HP_POINT = 1000if lastAttacks[1] == player2.attackRecoverTime: tempvar afterDamage = currentHealths[0] - player2.damage nextHealths[0] = afterDamage + player1.healthPerTurn nextLastAttacks[1] = 0else: nextHealths[0] = currentHealths[0] + player1.healthPerTurn nextLastAttacks[1] = lastAttacks[1] + 1endif lastAttacks[0] == player1.attackRecoverTime: tempvar afterDamage = currentHealths[1] - player1.damage nextHealths[1] = afterDamage + player2.healthPerTurn nextLastAttacks[0] = 0else: nextHealths[1] = currentHealths[1] + player2.healthPerTurn nextLastAttacks[0] = lastAttacks[0] + 1end

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

一旦我们有了模拟逻辑的代码，我们就需要为我们的 Cairo 程序编写主函数。该程序需要读取 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

除了检查这些战士的 nCombatRounds 模拟结果是否为给定的健康值外，我们还应该检查在战斗结束时是否有一个或两个角色已经死亡。如果想让战斗持续下去，直到有人死亡。我们没有在这个简单的例子中实现这一点，可以由读者来实现。在目前的代码中，只能模拟运行几轮，并在给定回合后，在任何一个玩家死之前停止战斗。然而，执行者不能对模拟回合的进行情况撒谎，因为这是我们要检查的。

为什么我们需要两个程序？

我们本来可以把 Python 和 Cairo 程序写在一起，作为一个单一的 Cairo 程序，以大大减少代码量。然而，在实践中，我们需要在 Python 程序中添加更多的功能，这样我们就可以为我们的终端用户制作战斗的动画。例如，我们希望记录每个玩家每轮的健康状况，以及每轮发生的情况。这些逻辑在验证器部分是完全不需要的。我也喜欢想象有两个程序：一个战斗逻辑计算器和一个战斗结果验证器。这类似于我们经常有的程序和测试用例的逻辑分割。

运行！

我们可以运行 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 != 1097assert simulatedEndHealths[1] = endHealths[1]^*******************************************^

.pie 文件包含了 SHARP 为我们进行证明生成所需的所有信息。SHARP 是由 StarkWare 运营的一项服务，它可以生成证明，证明 Cairo 程序执行的有效性。然后，它将这些证明发送到以太坊测试网（Goerli），由以太坊智能合约进行验证。

目前，SHARP 不能在本地运行，从 Cairo 程序中生成证明的唯一方法是利用 StarkWare 的服务器来做证明验证。希望这种情况在未来会有所改变，任何人都可以生成关于任何东西的证明。StarkWare 公司计划在稍后阶段发布 SHARP 的源代码。目前现状来说，去中心化的游戏无法使用 Cairo 来构建。

让我们向 SHARP 提交我们的工作吧：

> cairo-sharp submit -- cairo_pie combat.pieSubmitting to SHARP...Job sent.Job key: f48c551e-c0c6-4cf5-8a52-a0aa1c43728cFact: 0x17ee903dfb54b55e53cc03d5a47602e83ed0ff9e219fe4567b8d59fa2666f682

过了很久，我们应该能看到我们的事实（fact）被验证了，而且是有效的：

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

我们也可以从 Cairo 的游乐场找到这个结果。

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

在以太坊智能合约上利用证明

现在我们知道，对于给定的输入值（玩家1、玩家2和回合数），给定事实哈希值，程序应该输出最终的健康值，我们能够在链上验证计算，而无需在链上再次执行计算。

实际上，我们还缺少一个信息，那就是程序的哈希值。

> cairo-hash-program -program combat-compiled.json0x248070cb7b7f20b0b9445a382fdb4faa6b69c1f3653355077ae05b82c636ddf

这是我们之前所有工作的高潮，现代密码学的奇迹，一个简单的 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.}

这里 cairoVerifier._isValid(fact) 是一个 Goerli 的合约。

https://goerli.etherscan.io/address/0xAB43bA48c9edF4C2C4bB01237348D1D7B28ef168

可以在这里找到文章中文件的源代码：https://github.com/KillariDev/STARK-Combat

通过 DAO，研究组织和媒体可以打破地域的限制，以社区的方式资助和生产内容。DAOrayaki将会通过DAO的形式，构建一个代表社区意志并由社区控制的功能齐全的去中心化媒体。欢迎通过文末方式提交与DAO、量子计算、星际移民、DA相关的内容，瓜分10000USDC赏金池！欢迎加入DAOrayaki社区，了解去中心化自治组织（DAO），探讨最新话题！

官方网站：https://daorayaki.org

Media：https://media.daorayaki.org

Discord server: https://discord.gg/wNUPmsGsa4

Medium: https://medium.com/@daorayaki

Email: daorayaki@dorafactory.org

Twitter: @daorayaki_

微信助手：DAOrayaki-Media

小宇宙：DAOrayaki