zk-STARK: Verifying Complex Automated Battle Computations on Ethereum

特邀专栏作者

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

This article is about 12818 words, reading the full article takes about 19 minutes

In this post, I won't go too deep into how STARK works, but I will give a practical overview of how it is used in practice.

AI Summary

Expand

In this post, I won't go too deep into how STARK works, but I will give a practical overview of how it is used in practice.

Original Author: Killari

Original title: STARKs: Verifying complex auto battler calculation on Ethereum — Scaling decentralized games

Executing complex functions on Ethereum has always been a big no-no and should never be done. Blockchain computations are very expensive as all nodes are required to perform the same computation to verify its correctness.

StarkWare is one of the Ethereum scaling services that tries to scale Ethereum using STARK (Scalable Transparent Proof of Knowledge) proofs. In this post, I won't go too deep into how STARK works, but I will give a practical overview of how it is used in practice.

Sometimes STARK is prefixed with "zk-", which means "zero-knowledge proof", which allows STARK to prove something without revealing all the information about the thing we are trying to prove. StarkWare is working on including ZK in the pipeline later, but right now they are only focusing on scalability, and zero knowledge is not required to achieve this.

Vitalik's blog post is an illustration of how zk-SNARKs render to the user.

Vitalik gave a short overview of STARK in his article. STARK Part 1: Proofs with Polynomials briefly explains how these cryptographic primitives work. There are also SNARKs (Succinct Non-Interactive Arguments of Knowledge), which achieve something similar to STARKs, but a bit different. If you are more interested in understanding zk-SNARK, I strongly recommend this explanation paper: The principle and implementation of zk-SNARK, the authoritative explanation of Maksym Petkus. Petkus explained the principle of zk-SNARK, starting from very basic mathematics, and then gradually deepening more complex mathematics, standing on the shoulders of predecessors. Great reading experience.

Petkus summarizes zk-SNARK as follows:

secondary title

STARK and auto battle games

Automatic battle games (also called automatic battle machines, auto chess) are a type of game in which players make choices for character growth, but they cannot make any choices during battles, but proceed automatically. It would be fun to have such a game running on Ethereum L1, but currently such a game cannot be done.

So, what benefits can STARK bring to auto-battle games? The simulation of auto-battle games can be very complex, so it is difficult to run. If there is a technology that makes it run only once, and other players can just trust this calculation, while being sure that no one is lying, it will allow us to have a decentralized auto-play.

Here is the action plan:

1) Write the automatic battle logic in Python.

2) Build a validator in StarkNet's Cairo language (required for STARK proofs).

3) Execute the code for the automatic battle, using the Cairo validator we built to create a STARK proof of program execution.

secondary title

Write an automatic combat system in Python

To start our journey, we simply program the logic of the autobattle as we normally do, no STARK magic required here.

We make an automatic battle simulator between two characters. These roles have four states:

- healthy. Equal to the total amount of damage they can take.

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

- harm. How much damage each attack will cause each other.

- Attack Recovery Time: After each attack, how long the attacker needs to wait before attacking again.

- Health per round: how much health the character recovers per round.

These attributes can be defined as a class in Python as shown below.

Here's a breakdown of how the fight will roll:

We have a game loop that cycles through rounds of combat.
In each iteration, we restore health to both characters and have them beat each other up as fast as they can.
We'll make these characters fight to the death. If one of the characters dies, or both characters die, the battle is considered over.

By choosing specific character attributes, it is possible to have situations where the battle never ends, but continues forever. This can be avoided by, for example, limiting the maximum number of rounds our battles can last, and then considering resolving the battle in a draw, which is not intended to be considered in our sample code.

At the end of the simulation, let's return how much health each character has left, and count how many rounds the battle took.

Here's a version written in Python code:

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
}

Next, let's pick who will have this epic battle:

We'll have an ogre with a long health bar (1000 health!) that deals 48 damage per attack, but waits 80 times between attacks. The ogre also restores three health points per turn.

Our challenger hero has much lower health, only 240 health, no health regeneration at all, and less damage per attack (20), but our hero only has to wait 2 turns before attacking. So at least our hero is somehow better than the ogre! This is our hero. This is a real David and Goliath battle.

We can define our roles in code as follows

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

We can then simulate combat by calling the combat function.

simulateFight(player1, player2

We will get the result of the battle:

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

We can read from the result that the battle lasted 272 rounds and the battle ended because the ogre was defeated. Our hero won with a huge 96 points of blood! This is our hero.

Next let's store all the necessary important information about the battle in a file so we can later prove the battle with a STARK proof. All we need are program inputs (definitions of player 1 and player 2) and program outputs (health at the end and number of turns it takes). Our validator doesn't need the program itself at all!

We will write the validator in Cairo. Cairo is a programming language for writing verifiable programs. One of Cairo's many requirements is that all inputs must be non-negative. It's our devs' misfortune, but our hero's blessing, ogre health goes negative, that's a negative number :(

To get around this limitation, we'll add 1000 to all health values, and if a character's health is below 1000, he's considered dead. In order for this method to work with different character damage values, we also need to make sure that a character's damage never exceeds 1000, because then someone's health could become negative again. Here is the code:

secondary title

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

Writing a Cairo validator

Next, we need to write a verifier program to be able to STARK the execution of our Python program. The program needs to be able to verify that, given the initial player attributes, when the simulation code is run, the simulator produces the exact output shown in the log area. To achieve this, we'll switch to programming in the Cairo language.

We'll define the role structure in Cairo in a very similar way to what we see in python:

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

A big difference here compared to Python is that we need to assign all variables to some unfamiliar data type felt (short for field element). The felt data type is a 252-bit (weird, isn't it?) variable type defined between (-P/2, P/2), where P is a large 252-bit prime.

Although it may seem odd, for our purposes felt behaves like an integer. The significance of this data type is that it is easier for the Cairo compiler to make STARK proofs from our code than if we actually deal with integer or floating point variable types. You can read more about felt variable types from Cairo's documentation.

Now, let's start writing the Cairo program to make sure that the battle has gone according to plan and that the executor of the program cannot lie to the other players. In addition to the felt type and non-negativity of input variables, Cairo has some other restrictions. We have used a while loop in the Python code, but dynamic length loops are not possible in Cairo, we need recursion to implement the same logic. So let's define a recursive function that will validate a single round of combat, and then recursively validate all other rounds of combat:

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

The function takes in our two characters, their current health and last attack timer, the current combat round and the number of combat rounds to simulate. We will then return the updated health and timer of the last attack after the validation round to be able to validate the next round recursively.

You may have noticed the range_check_ptr at the beginning of our function. range_check_ptr is a pointer we need to use for range checking (operator<, >, >=,<=). These operations are also difficult in Cairo, but luckily we can still do them by using Cairo's range_check_ptr built-in function.

Next, let's start defining the internals of the function. We basically implement the exact same logic as our battle round in 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 code is written a little differently compared to Python. This is because in Cairo we can only use constant variables (another interesting limitation). Once we set a value to a variable, we can no longer change its content. So when we increased the player's health for health regeneration, we calculated it at the same time as the damage.

Next we check to see if we have simulated the required number of rounds, if so we end the simulation. If the simulation is not over yet, we need to check if both players are still alive. If we didn't have this check, a malicious emulator runner could keep simulating combat until both players were dead, which would allow an already dead player to continue fighting! We cannot allow such madness, we cannot allow undead warriors to appear in our arenas!

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

Here we are using the assert_nn function which is checking if the value inside the function is non-negative: nextHealths[0] > ZERO_HP_POINT. If assert is false, the execution fails, and we know that the person running the emulator lied to us.

Finally, let's call our function to get the next round of the simulation, and then we'll return the final simulation result.

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

Once we have the code for the simulation logic, we need to write the main function for our Cairo program. The program needs to read the output of the Python program and then call the simulateCombat function we just created. This function will return the final health value, which we then need to compare with the output of the Python program. Here is the code:

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

secondary title

Why do we need two programs?

secondary title

run!

We can run the Python emulator to compile our Cairo validator with:

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

We can then run the Cairo program with the input file we generated with combat.py, generating the combat.pie file:

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

We can also verify that the pie file is correct with the following command:

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

You can try modifying the resulting health values in the battle-input.json file, be aware that you cannot modify them without getting a validation error from Cairo. For each starting input (Player 1, Player 2, and number of turns), the battle has only one resolution. For example, if we try to cheat by giving our hero an extra health bar at the end of a fight, the validator will notice that we are trying to cheat.

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

The .pie file contains all the information SHARP needs to do the proof generation for us. SHARP is a service operated by StarkWare that generates proofs of the validity of Cairo program execution. It then sends these proofs to the Ethereum testnet (Goerli) to be verified by Ethereum smart contracts.

Currently, SHARP cannot be run locally, and the only way to generate proofs from Cairo programs is to use StarkWare's servers for proof verification. Hopefully this will change in the future and anyone can generate proofs about anything. StarkWare plans to release the source code for SHARP at a later stage. Currently, decentralized games cannot be built using Cairo.

Let's submit our work to SHARP:

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

After a while, we should see our fact validated and valid:

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

secondary title

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

Proof of use on Ethereum smart contracts

Now that we know that for a given input value (Player 1, Player 2, and number of rounds), given the fact hash, the program should output the final health value, we are able to verify the calculation on-chain without having to do it again on-chain Perform calculations.

In fact, there is one more piece of information we are missing, which is the hash of the program.

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

This is the culmination of all our previous work, a marvel of modern cryptography, a simple Solidity function that verifies a fact and checks that programOutput is valid. All without the computation itself.

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