Module Mavryk_raw_protocol_alpha.Sc_rollup_game_repr

The smart contract rollup refutation game types are defined here, as well as the basic pure logic for:

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:

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 Mavryk_protocol_environment_alpha.Error_monad.error +=
  1. | 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.

    *)
  2. | Proof_unexpected_section_size of Mavryk_protocol_environment_alpha.Z.t
    (*

    Invalid proof step because there is more than one tick.

    *)
  3. | 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.

    *)
  4. | 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.

    *)
  5. | 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.

    *)
  6. | Dissecting_during_final_move
    (*

    The step move is a dissecting where the final move has started already.

    *)
type player =
  1. | Alice
  2. | 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 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
type game_state = V1.game_state =
  1. | 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.

    *)
  2. | 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_equal : game_state -> game_state -> bool
type t = V1.t = {
  1. turn : player;
  2. inbox_snapshot : Sc_rollup_inbox_repr.history_proof;
  3. dal_snapshot : Dal_slot_repr.History.t;
  4. start_level : Raw_level_repr.t;
  5. inbox_level : Raw_level_repr.t;
  6. game_state : game_state;
}

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 -> bool

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

val opponent : player -> player

Return the other player

val player_equal : player -> player -> bool
module Index : sig ... end

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

type refutation =
  1. | Start of {
    1. player_commitment_hash : Sc_rollup_commitment_repr.Hash.t;
    2. opponent_commitment_hash : Sc_rollup_commitment_repr.Hash.t;
    }
  2. | Move of {
    1. choice : Sc_rollup_tick_repr.t;
    2. step : step;
    }
    (*

    choice is the final tick in the current dissection at which the two players agree.

    *)

A refutation is a move in the game.

type reason =
  1. | Conflict_resolved
  2. | Timeout

A game ends for one of two reasons: the conflict has been resolved via a proof or a player has been timed out.

type game_result =
  1. | Loser of {
    1. reason : reason;
    2. loser : Sc_rollup_repr.Staker.t;
    }
    (*

    One player lost.

    *)
  2. | Draw
    (*

    The game ended in a draw

    *)

The game result.

type status =
  1. | Ongoing
  2. | 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 play : Sc_rollups.Kind.t -> Dal_slot_repr.parameters -> dal_activation_level:Raw_level_repr.t option -> dal_attestation_lag:int -> dal_number_of_slots:int -> stakers:Index.t -> Sc_rollup_metadata_repr.t -> t -> step:step -> choice:Sc_rollup_tick_repr.t -> is_reveal_enabled:Sc_rollup_PVM_sig.is_reveal_enabled -> dal_attested_slots_validity_lag:int -> (game_result, t) Mavryk_protocol_environment_alpha.Either.t Mavryk_protocol_environment_alpha.Error_monad.tzresult Mavryk_protocol_environment_alpha.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.

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.
val cost_play : step:step -> choice:Sc_rollup_tick_repr.t -> Gas_limit_repr.cost

cost_play ~step ~choice returns the gas cost of play applied withstep, and choice.

type timeout = {
  1. alice : int;
    (*

    Timeout of Alice.

    *)
  2. bob : int;
    (*

    Timeout of Bob.

    *)
  3. 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.

module Internal_for_tests : sig ... end