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

Executing complex functions on chain Ethereum has always been a big no-no, something that you should never do. Blockchain computation is very expensive as all the nodes are needed to execute the same calculation to verify its correctness.

StarkWare is one of the Ethereum scaling services that is attempting to scale Ethereum using STARKs (Scalable Transparent ARgument of Knowledge) proofs. I will not go too deep into how STARKs work in this blogpost, but I am going to give a practical overview on how they can be used in practice.

Sometimes the “zk-” prefix is added in front of STARKs of STARKs, to denote “Zero Knowledge proofs”, which makes STARK’s able to prove something without revealing all the information about the thing we are trying to prove. StarkWare is focusing on adding these ZK’s later on in their pipeline, but now they are focusing on scalability only, and Zero Knowledge is not needed to achieve that.

Vitalik’s blog post has a nice visualization on how zk-SNARK can appear to users.

Vitalik gives a short overview in his blogpost about STARKs: STARKs, Part I: Proofs with Polynomials that explains shortly how these cryptographic primitives work. There are also SNARK’s (Succinct Non-Interactive ARgument of Knowledge) that can achieve similar things compared to STARK’s but a bit differently. If you are more interested in understanding zk-SNARKs, I highly recommend this explanation paper Why and How zk-SNARK Works: Definitive Explanation by Maksym Petkus. Petkus explains how zk-SNARK’s work starting from very basic mathematics while progressively moving into more complex mathematics while building on top of the previously built foundation. A great read!

Petkus summarizes zk-SNARKs as follows:

Zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARK) is the truly ingenious method of proving that something is true without revealing any other information.

STARK’s and auto battlers

An Auto battler is a game genre where players make character development choices, but they can’t make any choices during the combat itself, it happens automatically. It would be cool to have such games running on Ethereum L1, but currently such games are priced out.

So how can we benefit from STARKs in auto battlers? Auto battler simulations can be really complex beasts, and running such complex simulations is simply not feasible. If only there was a technology that could enable it to be run only once, and the other players could just trust that computation while being sure that no one is lying, this would enable us to have a decentralized auto battler.

Here’s the action plan:
1) Program the auto battling logic in Python.
2) Build a verifier with StarkNet’s Cairo language (required for the STARK proof).
3) Execute the auto battler code and create a STARK proof about the execution of the program using the Cairo verifier we built.
4) Observe how we can utilize the auto battler combat results in Ethereum’s Solidity side.

Programing an auto battler in Python

To start our journey, we simply program the auto battler logic as we would do normally, no STARK magic needed here!

We make an auto battler simulator between two characters. These characters have four kinds of stats:
— Health: How much damage they can withstand.
— Damage: How much damage they’ll inflict on the other party each hit.
— Attack Recover Time: How long after each attack, the attacker needs to wait until they can hit again.
— Health Per Turn: How much health the character recovers per turn.

These attributes can be defined as a class in Python as follows:

Here are the specifications on how the combat will roll:

• We have a game loop that will loop through the rounds of combat.
• For each iteration we recover health for both characters and make them smack each other as fast as they can.
• We will make the characters fight until death. The combat is considered finished if either of the characters have died, or both have died.

It’s also possible to choose character stats such that the battle never ends and would go on forever. This could be avoided for example by limiting the number of rounds our combat can last at maximum, and then consider the battle to resolve in a tie, however we are not going to consider this situation in our example code.

At the end of the simulation, let’s return how much health each character has left and how many rounds it took to calculate the fight.

Here’s the specifications programmed in Python code:

Next, lets define who are going to have this epic fight:

We will have an Ogre that has a huge amount of health (1000 hp!) that deals 48 dmg per hit, but it takes 80 ticks between each attack. The ogre also recovers three health per turn.

Our challenger hero has a significantly lower amount of health, only 240 hp, with no health recovery at all, smaller damage per hit (20), but our hero can attack after waiting for only 2 turns. So at least our hero is better than the ogre somehow! A true battle between David and Goliath.

We can get our characters defined in the code as follows

We can then simulate the fight by calling the fight function:

simulateFight(player1, player2)

and we will get a back the fight results:

We can read from the results that the battle lasted 272 rounds and that the battle ended because ogre was beaten. Our hero is victorious with generous 96 health to spare!

Next let’s store all the necessary important information about the fight in a file, so that we can prove the fight using STARK proofs later on. All we need is the program input (player 1 and player 2 definitions) and the program output, the ending health's and how many rounds it took. Our verifier will not be needing the program itself at all!

We will write the prover in Cairo. Cairo is a programming language for writing provable programs. One of the many requirements for Cairo is that all the inputs need to be non-negative numbers. Unfortunately for us developers, but fortunately for our hero, ogres health goes negative and this is a negative number :(.

To get around this limitation we’ll add 1000 to all the health numbers, and consider that a character has died if their health goes below 1000. To make this work with different character damage values, we also need to make sure that a character can never make more damage than 1000 as then someone’s health could get negative again. Here’s the code:

This code produces the final simulation output for us that will be stored into combat-input.json file:

Writing the Cairo verifier

Next, we need to write a verifier program to be able to make STARK proofs about the execution of our Python program. This program needs to be able to verify that given the initial player stats, when the simulation code is run, the simulation would result in the exact output displayed in the log field. To make this happen, we’ll switch to program in Cairo.

We’ll define the character structure in Cairo in a very similar manner than we do that in python:

A big difference here compared to Python is that we need to specify all our variables to be in some alien datatype felt(short for field element). The felt datatype is a 252 bit (weird, eh?) variable type that is defined between (-P/2, P/2) , where P is a big 252 bit prime.

As weird as it might sound, for our purposes the felt behaves like an integer. The point of this data type is that it’s significantly easier for Cairo compiler to make a STARK proof out of our code, compared to if we actually dealt with integers or floating point variable types. You can read more about the felt variable type from Cairo’s documentation.

Now, let’s start writing the Cairo program to ensure that the combat has gone as it was intended and the executor of the program cannot lie to other players. In addition to felt and non-negativity of the input variables, Cairo has some other limitations. We are using a while loop in our Python code, but dynamic length loops are not possible in Cairo and we need to implement the same logic via recursion. So let’s define a recursive function that will verify a single round of a combat, and then recursively verify all the other rounds of the combat:

The function takes in our two characters, their current health and the last attack timers, the current combat round and number of combat rounds to simulate. We will then return the updated health and last attack timers after we have verified the round to be able to verify the next round via recursion.

You might have noticed the range_check_ptr at the beginning of our function. range_check_ptr is a pointer that we need to use to be able to do range checks (operators <, >, >=, <=). These operations are also difficult in Cairo, but luckily we still manage to do these by using the range_check_ptr builtin of Cairo.

Next, let’s start to define the inner contents of the function. We basically implement the exact the same logic that we have in python side for a combat round:

The code is written a bit differently in Cairo compared to Python. This is because we can only utilize constant variables in Cairo (a yet another interesting limitation). Once we have set a value to a variable, we cannot change its contents anymore. Thus when we are incrementing players health for health regeneration, we calculate it at the same time with the damage calculation.

Next we’ll check that if we have already simulated the asked number of rounds and if so, we end the simulation. And if the simulation has not already ended, we need to check that both players are still alive. If we didn’t have this check, the malicious simulator runner could keep simulating the combat until both players have died, while having an already dead player keep on fighting! We can’t allow such madness, we can’t allow undead fighters in our arena!

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

Finally, let’s call our function to get a simulation for the next round and then we will return the final simulation results.

Once we have the simulation logic coded, 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. The function will then return the final health values, which we then need to check against the output of the Python program. Here’s the code:

In addition to checking that the simulation for nCombatRounds for these fighters will result as the given health values, we should also check that either or both of the characters have died at the end of the combat. This is if we want to have the battle to go on until death. However, this is left out from this simple example, and could be implemented by a reader. With the current code, someone could only run simulation for a couple of rounds and stop the fight at any given round before either of the players have passed. However, the executor cannot lie about how the simulated rounds go as that is something we check.

Why do we need two programs?

It would have been possible to write the Python and Cairo program together as a single Cairo program to get away with a significantly smaller amount of code. However, in practice we would need to add more features to our Python program so that we would be able to animate the battle for our end users. For example, we would like to log each player’s health for each round and also what happened during each round. Logic that is not required in the prover part at all. I also like to imagine that there are two programs: a battle logic calculator and a battle outcome verifier. A similar logical split that we often have with programs and test cases.

Enough coding, let’s execute!

We can run the Python simulator and compile our Cairo verifier with following commands:

> 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 to produce 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 to modify the combat-input.json files outcome health values, to notice that you cannot modify them without getting verification errors from Cairo. There’s only one way the combat can resolve for each starting input (player1, player2 and number of rounds). For example if we try to cheat a bit and give our hero one more health point at the end of the combat, the verifier 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 required for SHARP to do proof generation for us. SHARP is a service operated by StarkWare that generates proofs attesting to the validity of the executions of Cairo programs. Then, it sends those proofs to an Ethereum testnet (Goerli) where they are verified by an Ethereum smart contract.

Currently SHARP cannot be run locally, the only way to generate proofs from Cairo programs is to utilize StarkWare’s servers to do proof attestations. Hopefully this will change in the future and anyone could generate proofs about anything. StarkWare is planning to release the SHARP’s source code at a later stage. With the current state of the matters, decentralized games cannot be built using Cairo.

Let’s submit our job 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 long while we should be able to see that our fact was verified and it’s valid:

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

We can also find this result from Cairo’s playground:
https://www.cairo-lang.org/playground/sharp.html?job_key=f48c551e-c0c6-4cf5-8a52-a0aa1c43728c

Utilizing the proof on an Ethereum smart contract

Now that we know that for given input values (player1, player2 and number of rounds), given the fact hash, the program should output the final health values, we are able to verify the computation on chain without performing the computation again on chain.

Actually, there’s still one piece of information that we are missing, and it’s the programs hash:

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

Here’s the culmination of all of our prior work, a marvel of modern cryptography, a simple Solidity function that will verify a fact and check that the programOutput is valid. All without doing the computation itself.

Here cairoVerifier._isValid(fact) is a contract on Goerli:

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

If you are interested in learning more about decentralized gaming I recommend joining Decentralized Gaming Association’s discord and if you are interested in learning more about STARK’s I’ll recommend StarkWare’s discord on top of the highly recommended writings :).

You can find the source code for the files of this writeup here: https://github.com/KillariDev/STARK-Combat

Thank you

Thank you for very helpful people at StarkNets #cairo channel that helped me to make this writeup: @Lior Goldberg#6041, @FeedTheFed | StarkWare#8826, @perama#6895, @guthl | StarkWare#2832, @jmall#4962 and @cecco_#0181

@Killari