package tezos-protocol-013-PtJakart

  1. Overview
  2. Docs
package tezos-protocol-013-PtJakart
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

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

The game has two players. The refuter starts.

val opponent : player -> player

opponent player is the other player.

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

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

type commit =
  1. | Commit of Section.section

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

type refutation =
  1. | RefuteByConflict of conflict_resolution_step

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

type 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:

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

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

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

val initial : commit -> conflict_resolution_step -> t * move

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct