tezos-protocol-013-PtJakart 20.1 (latest)

Parameters

module PVM : Sc_rollup_PVM_sem.S

Signature

module PVM : 
  Sc_rollup_PVM_sem.S
    with type state = PVM.state
     and type proof = PVM.proof
     and type context = PVM.context

type tick = Sc_rollup_tick_repr.t

module Section : sig ... end

type player =

| Committer
| Refuter

The game has two players. The refuter starts.

val player_encoding : 
  player Tezos_protocol_environment_013_PtJakart.Data_encoding.t

val pp_player : 
  Tezos_protocol_environment_013_PtJakart.Format.formatter ->
  player ->
  unit

val opponent : player -> player

opponent player is the other player.

type t = {

turn : player;
start_state : PVM.hash;
start_at : tick;
player_stop_state : PVM.hash;
opponent_stop_state : PVM.hash;
stop_at : tick;
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.

val encoding : t Tezos_protocol_environment_013_PtJakart.Data_encoding.t

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

type conflict_resolution_step =

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

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

| Commit of Section.section

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

type refutation =

| RefuteByConflict of conflict_resolution_step

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

type reason =

| InvalidMove
(*
One of the player did not respect the game rules, typically by providing a refinement step which is inconsistent with the current dissection.
*)
| 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:

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

type outcome = {

winner : player option;
reason : reason;

}

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

val pp_outcome : 
  Tezos_protocol_environment_013_PtJakart.Format.formatter ->
  outcome ->
  unit

type move_result =

| Over of outcome
| Ongoing of t

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

val pp_move : 
  Tezos_protocol_environment_013_PtJakart.Format.formatter ->
  move ->
  unit

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.

val play : 
  t ->
  move ->
  move_result Tezos_protocol_environment_013_PtJakart.Lwt.t

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

package tezos-protocol-013-PtJakart

Parameters

Signature