Behavioral Programming with Petri Nets à la Functional Way — Smart Contracts
Hello everyone! As promised, this post continues the story about behavioral programming done with Petri nets. In the last post, we modeled the dining philosophers problem to highlight how and why behavioral programming can be useful. In this blogpost we focus on modeling a smart contract using Petri net. For the video explanation, click below.
The net we drafted this time describes the behavior of a putative smart contract for online gambling. The kind of gambling game we want to describe is a rather simple one, like roulette or dices. We start by making the following assumptions:
- The player plays against the casino, as in a game of roulette.
- The player can bet only once per game;
- A certain amount of randomness is needed to establish if the player wins or loses.
We drew inspiration from an already popular and deployed gaming platform on Ethereum, Etheroll. In Etheroll, as the name suggests, you essentially make a bet, “roll” an imaginary dice and either win or lose. The smart contract describes the behavior of the game and how bets are handled is a clear use case for behavioral programming. We want to be certain that the contract satisfies certain properties, such as:
- ensure that the game is provably fair
- guarantee that we will always be able to pay bets back without going bankrupt.
The process starts with the transition highlighted in red, “Place bet”: It is the player that fires it, when a bet is placed. Then, the first thing that the contract does is query its current balance and establish if the bet can be covered or not (namely: would we end up being bankrupt if the player were to win?). If the bet cannot be covered, the contract gives the money back to the player, which is represented by the “Pay back” transition highlighted in green.
If the bet can instead be covered, the contract needs to get some random numbers to determine if the player wins or loses. Random number generation is a rather hard problem for Ethereum and blockchains in general, and diving into it is not in the scope of this post. To make things smooth, we just supposed that we can outsource the random number generation process by querying an oracle. Notice that this is not a crazy assumption since companies providing exactly this kind of services are already operating on Ethereum.
An oracle is fundamentally a smart contract which, when queried, produces a random number. We also expect this random number to come with some sort of proof of integrity that the random generation process has not been tampered with.
Firstly, our casino contract checks that we defined an address for the oracle. If this is not the case the query cannot be performed and so the process has to abort (which again means that the player gets the money back). This is implemented by falling back again to the red “Pay back” transition.
If on the other hand the oracle address is defined, we proceed by calculating the oracle fee. This is because the oracle represents a third party service and we are not expecting it to work for free. So we calculate how much money we have to give to the oracle, and we forward a request. Now three things can happen:
- The oracle doesn’t answer.
- The oracle does answer, by firing the purple “Oracle Callback” transition. We get a random number back but the integrity proof doesn’t check out.
- The oracle does answer, by firing the purple “Oracle Callback” transition. We get a random number back and we are satisfied with the proof.
The third case is clearly the easiest one: We just use the number to calculate the outcome of the bet and we pay the user back.
In the other two cases, we resort to some alternatives: The second case is handled with a fallback strategy (e.g. we could just ignore the proof and keep going), while the first case can either be handled by trying to query the oracle again or by switching to a different random source (e.g. by using block numbers as entropy. Please, if you are really trying to set up an online casino don’t do this!).
So, this is our contract draft. At a first glance, it seems legit, right? No! It has all sorts of problems, which luckily enough we can formally spot. For instance, “Can Cover” produces two tokens in two different places, while “Address Undefined” just processes one of them. This means that the net can be driven to a situation where the output place of “Can Cover” on the right becomes unbounded, accumulating an infinite number of tokens which will be stuck forever. This situation is shown in the picture below, and it is ultimately a consequence of the fact that “Place Bet”, “Retry” and “Can Cover” all produce two tokens in two different places, leading to an unnecessary level of concurrency for this application.
Another problem is that we estimate a bet can be covered but we didn’t specify the corresponding amount of money on the side while the outcome gets calculated. So, if one hundred high bets come in at the same time, and we estimate that we can separately cover all of them, we may nevertheless end up broke if they are all winning.
Well, so what’s the point? The point is that we have been able to spot these sort of problems without writing one line of code. This is where Statebox shines: We can spend time to refine our casino process before starting with the actual implementation, that will be formally driven by the Statebox compiler from the net to EVM code.
Note moreover how we are able to have a high-level overview of who-gets-to-call-what in the contract: “Oracle Callback” can be called only by the Oracle contract, while “Place Bet” is an external call. All the other transitions are internal, meaning that they get to be fired by the contract itself. This helps us understand how to define the interaction that the contract has with the “external world”.
Congrats for reading up to here! What follows is not covered in our video. Let’s continue by updating our contract taking all the above considerations into account.
As you can see many things have changed. First, so many colors! As before, we marked in red the transitions fired by the player, and in purple the ones fired by the oracle. Green transitions are now interpreted as “final”, representing when the process comes to an end. Moreover, we used blue to highlight transitions that send money out. Note how green transitions and blue ones coincided in the previous version of the contract.
Let’s spell this process out. The first thing we do when a bet comes is lock the bet money up via “Lock Bet Money”. Now, in case another bet comes in, the inbound money from the first bet won’t be used in the calculations of the second. This is part of the fix for the “putting money on the side” issue we highlighted above.
After, we calculate the free balance (that is, the amount of free money we can allocate to bets) and the fee needed to pay the oracle. If we determine that we can indeed cover our costs, we lock that money up via “Lock Win Money”. This is again to be sure that even if other bets alter the overall balance of the contract, this won’t affect the bet we are processing now.
In the new contract, moreover, we subtract the fee to the locked up money via “Subtract Fee To Win Money”. Note how this happens after the oracle request — along with the money to pay the fee — is sent.
Most notably, we introduced new, but similar transitions: “Free Win Money 1”, “Free Win Money 2” and “Free Win Money 3”. These are deputed to free the locked up money needed to pay the player in case of victory. Using Statebox, these transitions will be all mapped to the same function, so you won’t have to type it over two times. Nevertheless, they are different transitions in the net. This shows how in behavioral programming functions cannot be considered equal just by looking at the computation they perform: The context in which they are used also matters!
Has the smart contract example helped with your understanding of how Statebox works? Feel free to leave a comment below. More examples will follow in the next weeks, so stay tuned!
