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 ====================
The first step consists of dissecting the commitment's number of ticks. 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.
If a player failed to prove that the current dissection is valid. We reach the final move of the game. The other player will have a chance to prove that the dissection is valid. If both player fails to invalidate each other, the game ends in a draw.
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 challenges 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.
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 dissection_chunk = V1.dissection_chunk
and type game_state = V1.game_state
and type t = V1.t
type game_state = V1.game_state = | Dissecting of {dissection : dissection_chunk list;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.
default_number_of_sections : int;default_number_of_sections is the number of sections a disection should contain in the more general case where we still have a high enough number of disputed ticks.
}When the state is Dissecting, both player are still dissecting the commitment to find the tick to refute.
| Final_move of {agreed_start_chunk : dissection_chunk;refuted_stop_chunk : dissection_chunk;
}When the state is Final_move, either Alice or Bob already played an invalid proof.
The other player will have a chance to prove that the refuted_stop_state is valid. If both players fail to either validate or refute the stop state, the current game state describes a draw situation. In the same way, the draw can be described by the situation where the two players manage to validate or refute the stop state.
Describes the current state of a game.
A game is characterized by:
refuter_commitment_hash, the hash of the commitment of the player that has initiated the game.
defender_commitment_hash, the hash of the commitment of the player that is tentatively refuted.
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.
dal_snapshot, a snapshot of the DAL's confirmed slots history at the moment the game is created. In fact, since the confirmed slots history at initialization would likely evolve during the game, we need a (fixed) reference w.r.t. which Dal input proofs would be produced and verified if needed.
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.
game_state, the current state of the game, see game_state for more information.
Invariants: -----------
dissection must contain at least 2 values (normally it will be 32 values, but smaller if there isn't enough space for a dissection that size. The initial game dissection will be 3 values except in the case of a zero-tick commit when it will have 2 values.)- the first state hash value in
dissection must not be None inbox_snapshot and dal_snapshot never change once the game is created
val equal : t -> t -> boolequal g1 g2 returns true iff g1 is equal to g2.
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 dal_slots_history ~start_level ~parent_commitment
~defender_commitment ~refuter ~defender ~default_number_of_sections 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_commitment, the commitment that both stakers agree on.
- secondly, the state and tick count of
defender_commitment, the commitment that defender has staked on.
- thirdly, a
None state which is a single tick after the defender_commitment 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.
type reason = | Conflict_resolved| Timeout
A game ends for one of two reasons: the conflict has been resolved via a proof or a player has been timed out.
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.
Applies the move refutation to the game. Returns the game status after applying the move.
In the case of the game continuing, this swaps the current player and returns a Ongoing status. Otherwise, it returns a Ended <game_result> status.
The provided DAL related parameters are used in case the game needs to:
- Check that a page's content is part of a slot (using the slot's commitment) when refuting a DAL page reveal.
- Check that the parameters are correct when refuting a DAL parameter reveal.
cost_play ~step ~choice returns the gas cost of play applied withstep, and choice.
type timeout = {alice : int;bob : int;last_turn_level : Raw_level_repr.t;Block level of the last turn move.
}A type that represents the number of blocks left for players to play. Each player has her timeout value. `timeout` is expressed in the number of blocks.
Timeout logic is similar to a chess clock. Each player starts with the same timeout. Each game move updates the timeout of the current player by decreasing it by the amount of time she took to play, i.e. number of blocks since the opponent last move. See Sc_rollup_refutation_storage.game_move to see the implementation.