package tezos-protocol-013-PtJakart

  1. Overview
  2. Docs
Tezos/Protocol: economic-protocol definition

Install 

dune-project
 Dependency

www.tezos.com Readme Edit opam file Versions (8)

Authors

  1. T
    Tezos devteam

Maintainers

  1. C
    contact@tezos.com

Sources

tezos-16.0.tar.gz
sha256=ad9e08819871c75ba6f4530b125f7d157799398e4d77a1e6bfea9d91ff37ff55
sha512=c5dc4d40cc09bc6980fbbdb5c2e105bf4252cf9cfcb2b49660b0ebe4dc789f6709ec3b3bf2f87d81580d3eed9521eeb1c960f24d9b14eb0285aaba1f84d10a9b

doc/tezos-protocol-013-PtJakart.raw/Tezos_raw_protocol_013_PtJakart/Sc_rollup_game/Make/index.html

Module Sc_rollup_game.MakeSource

Parameters

Signature

module PVM : Sc_rollup_PVM_sem.S with type state = PVM.state and type proof = PVM.proof and type context = PVM.context
Sourcemodule Section : sig ... end
Sourcetype player =
  1. | Committer
  2. | Refuter

The game has two players. The refuter starts.

Sourceval opponent : player -> player

opponent player is the other player.

Sourcetype t = {
  1. turn : player;
  2. start_state : PVM.hash;
  3. start_at : tick;
  4. player_stop_state : PVM.hash;
  5. opponent_stop_state : PVM.hash;
  6. stop_at : tick;
  7. current_dissection : Section.dissection option;
}

A game state is characterized by:

  • turn, the player that must provide the next move.
  • start_state/start_at, the state the two players agree on.
  • player_stop_state and opponent_stop_state are distinct as the two players disagree on the final state.
  • stop_at is the position of the final state.
  • If the cardinal of current_dissection is strictly greater than 1, the current player must choose one of its section and produce a dissection of this section.
  • If the cardinal of current_dissection is equal to 1, the game has reached its second phase and the current player must provide a proof of the execution step at start_at.

Invariants: -----------

  • current_dissection cannot be empty.
  • start_at is strictly less than stop_at.
  • player_stop_state is distinct from opponent_stop_state.
Sourcetype conflict_resolution_step =
  1. | Refine of {
    1. stop_state : PVM.hash;
    2. next_dissection : Section.dissection;
    }
    (*

    Assuming a current dissection, a section has been chosen and next_dissection is a dissection of this section. stop_state is a state which is different from the one exposed in for the section in the current dissection.

    *)
  2. | Conclude of Sc_rollup_PVM_sem.input option * PVM.proof
    (*

    When the current dissection contains a single section of length 1, the conflict tick has been found. The player provides a PVM.proof to demonstrate that her final state is the correct one.

    If the current state is an input state (see Sc_rollup_PVM_sem), the player must provide the input received by the PVM. Notice that the validity of this input is externally verified using the Sc_rollup_inbox proofs.

    *)

The conflict resolution is done in two phases: the refinement phase composed of refinement steps and a final step, the conclusion.

Sourcetype move =
  1. | ConflictInside of {
    1. choice : Section.section;
    2. conflict_resolution_step : conflict_resolution_step;
    }

A game move is a conflict resolution step performed in a given section of the PVM execution trace.

Sourcetype commit =
  1. | Commit of Section.section

To start the game, the committer must have made a section public...

Sourcetype refutation =
  1. | RefuteByConflict of conflict_resolution_step

... and the refuter must have started a dispute.

Sourcetype reason =
  1. | InvalidMove
    (*

    One of the player did not respect the game rules, typically by providing a refinement step which is inconsistent with the current dissection.

    *)
  2. | ConflictResolved
    (*

    The game reached the conclusion and the arbiter was able to determine how the conflict must be resolved in conformance with the PVM semantics.

    *)

The game can stop for two reasons:

Sourcetype outcome = {
  1. winner : player option;
  2. reason : reason;
}

The game can end with no winner if both players have wrong final states at the conflicting step.

Sourcetype move_result =
  1. | Over of outcome
  2. | Ongoing of t

After one game move, the game can be over or ongoing.

initial is the initial game state from the commit and the refutation. The first player to play is the refuter, this function also returns refuter's first move.

play game move returns the result of the given move applied on game.