package tezos-protocol-013-PtJakart

This module provides a refutation game logic for smart contract rollups.

It is in fact a functor that takes a PVM semantic implemented by a Sc_rollup_PVM_sem.S module and produces a game logic.

This game logic is used by the protocol when two commitments are in conflict to determine which one of the commitments is wrong.

A commitment characterizes a section of the PVM execution trace. When two commitments are in conflict, they agree on the first state of the section and disagree on the last one. The game runs in two steps: first, the two players alternatively refine the section they disagree on until they reach an atomic section of length 1, that is a single execution step of the PVM ; second, the player must provide a Merkle proof that a valid execution step corresponds to her final state.

Important invariants ====================

• The committer and the refuter agree on the first state of the current section and disagree on its final state. If they agree on both then whoever plays loses by InvalidMove.

Expected properties ===================

Honest-committer-wins:

• If a committer has posted a valid commit and has a perfect PVM at hand, there is a winning strategy which consists in choosing the first section of the current dissection and in producing a regular dissection until the conflict is reached.

Honest-refuter-wins:

• If a refuter has detected an invalid commit and has a perfect PVM at hand, the same strategy is also winning.

Here "winning strategy" means that the player actually wins (a draw is not enough).

Remarks =======

There are several subtle cornercases:

• If the refuter and the committer both post only invalid states, the game may end in a conflict state where both are wrong. By convention, we decide that these games have no winner.

• If the refuter and the committer both post only states, the game never has any conflicts. By convention, we decide that in this case the commiter wins by InvalidMove.

• If the refuter and the committer both post valid and invalid states, all outcomes are possible. This means that if a committer wins a game we have no guarantee that she has posted a valid commit.