The smart contract rollup refutation game types are defined here, as well as the basic pure logic for:
- how to create a new game from a pair of commits in the commit tree;
- how to update a game or complete a game when a move is played.
This game logic is used by the protocol when two commitments are in conflict to determine which one of the commitments is wrong.
Game state and moves ====================
At any given moment, the game stores a list dissection of state hashes and tick counts. These are the claims about the PVM history made by the player who has just moved.
The next player to move will specify a tick count which appears in the dissection; this is the last of the state hashes which she agrees with. She will then either:
- provide a new
dissection by giving a list of state hashes and tick counts that starts at the chosen tick count and ends at the next tick count in the previous dissection. It must agree at the start but disagree with the final state.
- if the tick difference between this state and the next is one, there is no 'room' for a new
dissection. In this case she must provide a Merkle proof that shows the step in the current dissection is invalid.
Initializing a game ===================
In order to trigger the start of a game, one player must publish a first move.
The initial function is called at this point. It converts a parent-child pair of commitments (belonging to the other player) into an initial dissection. The first move is immediately applied to this to give the first state of the game.
Note: it is quite possible for the game to end immediately after this first move, either if the commitment has a tick count of one or more probably if the refutation proves that the commitment was 'premature' (the state is not blocked---there are further computation steps to do or more inbox messages to read).
Expected properties ===================
P1 - If dissection is honest, the next move must be dishonest:
There is only one honest state hash for a given tick count. The next player must provide a different hash to the honest hash in the dissection.
P2 - If dissection is dishonest, there is a strategy for a player equipped with a perfect PVM to play an honest next move:
The player with a perfect PVM can calculate honest hashes until one disagrees with the dissection, and challenge the dissection at that point, publishing either an honest dissection or an honest Proof.
Each dissection has a maximum tick count step shorter than the last, so by induction using P1 and P2 we have
P1' - If dissection is honest, the last player has a winning strategy.
P2' - If dissection is dishonest, the next player has a winning strategy.
This allows us to see the following. (We use refuter to mean the first player to move, and defender to mean the other player.)
Honest refuter wins: An honest refuter will be refuting a dishonest commitment, because there is only one honest state possible per level. Therefore the initial dissection will be dishonest. By P2' the refuter has a winning strategy.
Honest defender wins: An honest defender will have made an honest commitment which will be translated into an honest initial dissection. By P1' the defender has a winning strategy.
In the case that both players are dishonest the outcome is slightly harder to determine---it basically comes down to which player gets to play the final move. That means that in this case the refutation game is equivalent to a finite game of nim (by the Sprague-Grundy Theorem, see en.wikipedia.org/wiki/Sprague-Grundy_theorem). However, this fact is completely irrelevant, because if the rollup is working correctly the winner will subsequently be defeated by some honest opponent.
type player = | Alice| Bob
The two stakers index the game in the storage as a pair of public key hashes which is in lexical order. We use Alice and Bob to represent the first and second player in the pair respectively.
include module type of V1 with type t = V1.t
A game state is characterized by:
turn, the player that must provide the next move.
inbox_snapshot, a snapshot of the inbox state at the moment the game is created. This is only used when checking Input_step and Blocked_step proofs; it makes the proofs easier to create--- otherwise they would have a 'moving target' because the actual inbox may be updated continuously.
level, the inbox level of the commitment the game is refuting. This is only used when checking Blocked_step proofs---the proof will show that the next message available in inbox_snapshot is at level, so shouldn't be included in this commitment.
pvm_name identifies the PVM used in this rollup. It is useful to have here so we can check that the proof provided in a refutation is of the correct kind.
dissection, a list of states with tick counts. The current player will specify, in the next move, a tick count that indicates the last of these states that she agrees with.
Invariants: -----------
dissection must contain at least 3 values- the first state hash value in
dissection must not be None inbox_snapshot never changes once the game is created
module Index : sig ... endTo begin a game, first the conflict point in the commit tree is found, and then this function is applied.
initial inbox parent child refuter defender will construct an initial game where refuter is next to play. The game has dissection with three states:
- firstly, the state (with tick zero) of
parent, the commitment that both stakers agree on.
- secondly, the state and tick count of
child, the commitment that defender has staked on.
- thirdly, a
None state which is a single tick after the child commitment. This represents the claim, implicit in the commitment, that the state given is blocked.
This gives refuter a binary choice: she can refute the commit itself by providing a new dissection between the two committed states, or she can refute the claim that the child commit is a blocked state by immediately providing a proof of a single tick increment from that state to its successor.
A step in the game is either a new dissection (if there are intermediate ticks remaining to put in it) or a proof.
A refutation is a move in the game. choice is the final tick in the current dissection at which the two players agree.
type reason = | Conflict_resolved| Invalid_move of string| Timeout
A game ends for one of three reasons: the conflict has been resolved via a proof, a player has been timed out, or a player has forfeited because of attempting to make an invalid move.
A type that represents the current game status in a way that is useful to the outside world (using actual Staker.t values instead of the internal player type).
The Staker.t in the Ended case is the loser of the game: the staker who will have their stake slashed.
Used in operation result types.
A game ends with a single loser and the reason for the game ending. This type uses Alice or Bob to refer to the players without knowing which stakers they are---so it cannot identify an actual staker who should be punished without the associated game index.
Checks that the tick count chosen by the current move is one of the ones in the current dissection. Returns a tuple containing the current dissection interval (including the two states) between this tick and the next.
We check firstly that dissection is the correct length. It must be 32 values long, unless the distance between start_tick and stop_tick is too small to make this possible, in which case it should be as long as possible. (If the distance is one we fail immediately as there is no possible legal dissection).
Then we check that dissection starts at the correct tick and state, and that it ends at the correct tick and with a different state to the current dissection.
Finally, we check that dissection is well formed: it has correctly ordered the ticks, and it begins with a real hash of the form Some
s not a None state. Note that we have to allow the possibility of multiple None states because the restrictions on dissection shape (which are necessary to prevent a 'linear-time game' attack) will mean that sometimes the honest play is a dissection with multiple None states.
Applies the move refutation to the game. Checks the move is valid and returns an Invalid_move outcome if not.
In the case of the game continuing, this swaps the current player and updates the dissection. In the case of a Proof being provided this returns an outcome.