tezos-protocol-015-PtLimaPt 19.1

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.

module V1 : sig ... end

Versioning, see Sc_rollup_data_version_sig.S for more information.

include Sc_rollup_data_version_sig.S with type t = V1.t

type versioned

val versioned_encoding : 
  versioned Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

val of_versioned : versioned -> V1.t

val to_versioned : V1.t -> versioned

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 dissection_chunk = V1.dissection_chunk = {

state_hash : Sc_rollup_repr.State_hash.t option;
tick : Sc_rollup_tick_repr.t;

}

A dissection chunk is made of a state hash (that could be None, see invariants below), and a tick count.

val pp_dissection_chunk : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  dissection_chunk ->
  unit

val dissection_chunk_encoding : 
  dissection_chunk Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

type game_state = V1.game_state =

| Dissecting of {
1. 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.
  *)
2. 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 {
1. agreed_start_chunk : dissection_chunk;
2. 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.

val game_state_encoding : 
  game_state Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

val game_state_equal : game_state -> game_state -> bool

type t = V1.t = {

turn : player;
inbox_snapshot : Sc_rollup_inbox_repr.history_proof;
level : Raw_level_repr.t;
pvm_name : string;
game_state : game_state;

}

A game 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.

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 never changes once the game is created

val equal : t -> t -> bool

equal g1 g2 returns true iff g1 is equal to g2.

val opponent : player -> player

Return the other player

val encoding : t Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

val pp_dissection : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  dissection_chunk list ->
  unit

val player_equal : player -> player -> bool

val player_encoding : 
  player Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

val pp : Tezos_protocol_environment_015_PtLimaPt.Format.formatter -> t -> unit

module Index : sig ... end

val initial : 
  Sc_rollup_inbox_repr.history_proof ->
  pvm_name:string ->
  parent:Sc_rollup_commitment_repr.t ->
  child:Sc_rollup_commitment_repr.t ->
  refuter:Sc_rollup_repr.Staker.t ->
  defender:Sc_rollup_repr.Staker.t ->
  default_number_of_sections:int ->
  t

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

type step =

| Dissection of dissection_chunk list
| Proof of Sc_rollup_proof_repr.t

A step in the game is either a new dissection (if there are intermediate ticks remaining to put in it) or a proof.

type refutation = {

choice : Sc_rollup_tick_repr.t;
step : step;

}

A refutation is a move in the game. choice is the final tick in the current dissection at which the two players agree.

val pp_refutation : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  refutation ->
  unit

val refutation_encoding : 
  refutation Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

type invalid_move =

| Dissection_choice_not_found of Sc_rollup_tick_repr.t
(*
The given choice in a refutation is not a starting tick of any of the sections in the current dissection.
*)
| Dissection_number_of_sections_mismatch of {
1. expected : Tezos_protocol_environment_015_PtLimaPt.Z.t;
2. given : Tezos_protocol_environment_015_PtLimaPt.Z.t;
}
(*
There are more or less than the expected number of sections in the given dissection.
*)
| Dissection_invalid_number_of_sections of Tezos_protocol_environment_015_PtLimaPt.Z.t
(*
There are less than two sections in the given dissection, which is not valid.
*)
| Dissection_start_hash_mismatch of {
1. expected : Sc_rollup_repr.State_hash.t option;
2. given : Sc_rollup_repr.State_hash.t option;
}
(*
The given start hash in a dissection is None or doesn't match the expected one.
*)
| Dissection_stop_hash_mismatch of Sc_rollup_repr.State_hash.t option
(*
The given stop state hash in a dissection should not match the last hash of the section being refuted.
*)
| Dissection_edge_ticks_mismatch of {
1. dissection_start_tick : Sc_rollup_tick_repr.t;
2. dissection_stop_tick : Sc_rollup_tick_repr.t;
3. chunk_start_tick : Sc_rollup_tick_repr.t;
4. chunk_stop_tick : Sc_rollup_tick_repr.t;
}
(*
The given dissection's edge ticks don't match the edge ticks of the section being refuted.
*)
| Dissection_ticks_not_increasing
(*
Invalid provided dissection because ticks are not increasing between two successive sections.
*)
| Dissection_invalid_distribution
(*
Invalid provided dissection because ticks split is not well balanced across sections
*)
| Dissection_invalid_successive_states_shape
(*
A dissection cannot have a section with no state hash after another section with some state hash.
*)
| Proof_unexpected_section_size of Tezos_protocol_environment_015_PtLimaPt.Z.t
(*
Invalid proof step because there is more than one tick.
*)
| Proof_start_state_hash_mismatch of {
1. start_state_hash : Sc_rollup_repr.State_hash.t option;
2. start_proof : Sc_rollup_repr.State_hash.t;
}
(*
The given proof's starting state doesn't match the expected one.
*)
| Proof_stop_state_hash_failed_to_refute of {
1. stop_state_hash : Sc_rollup_repr.State_hash.t option;
2. stop_proof : Sc_rollup_repr.State_hash.t option;
}
(*
The given proof's ending state should not match the state being refuted.
*)
| Proof_stop_state_hash_failed_to_validate of {
1. stop_state_hash : Sc_rollup_repr.State_hash.t option;
2. stop_proof : Sc_rollup_repr.State_hash.t option;
}
(*
The given proof's ending state should match the state being refuted.
*)
| Proof_invalid of string
(*
The given proof is not valid.
*)

An invalid game move during a dissection or a proof step has one of the following values:

val pp_invalid_move : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  invalid_move ->
  unit

Pretty-printer for values of invalid_move type

type reason =

| Conflict_resolved
| Invalid_move of invalid_move
| 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.

val pp_reason : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  reason ->
  unit

val reason_encoding : 
  reason Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

type game_result =

| Loser of {
1. reason : reason;
2. loser : Sc_rollup_repr.Staker.t;
}
(*
One player lost.
*)
| Draw
(*
The game ended in a draw
*)

The game result.

val pp_game_result : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  game_result ->
  unit

val game_result_encoding : 
  game_result Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

type status =

| Ongoing
| Ended of game_result

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.

val pp_status : 
  Tezos_protocol_environment_015_PtLimaPt.Format.formatter ->
  status ->
  unit

val status_encoding : 
  status Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

val loser_of_results : alice_result:bool -> bob_result:bool -> player option

Decide the loser of the game, if it exists.

val play : 
  stakers:Index.t ->
  t ->
  refutation ->
  (game_result, t) Tezos_protocol_environment_015_PtLimaPt.Either.t
    Tezos_protocol_environment_015_PtLimaPt.Lwt.t

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.

type timeout = {

alice : int;
(*
Timeout of Alice.
*)
bob : int;
(*
Timeout of Bob.
*)
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.

val timeout_encoding : 
  timeout Tezos_protocol_environment_015_PtLimaPt.Data_encoding.t

module Internal_for_tests : sig ... end

package tezos-protocol-015-PtLimaPt