🦏 Sc_rollup_refutation_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_errors.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_storage.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.

Module Store := Storage.Sc_rollup.

Module Commitment := Sc_rollup_commitment_repr.

Module Commitment_storage := Sc_rollup_commitment_storage.

Module Commitment_hash := Commitment.Hash.

Module Stake_storage := Sc_rollup_stake_storage.

Module point.
  Record record : Set := Build {
    commitment : Sc_rollup_commitment_repr.t;
    hash : Commitment_hash.t;
  }.
  Definition with_commitment commitment (r : record) :=
    Build commitment r.(hash).
  Definition with_hash hash (r : record) :=
    Build r.(commitment) hash.
End point.
Definition point := point.record.

Definition conflict_point : Set := point × point.

[initial_timeout ctxt] set the initial timeout of players. The initial timeout of each player is equal to [sc_rollup_timeout_period_in_blocks].

Definition initial_timeout (ctxt : Raw_context.t)
  : Sc_rollup_game_repr.timeout :=
  let last_turn_level := (Raw_context.current_level ctxt).(Level_repr.t.level)
    in
  let timeout_period_in_blocks :=
    Constants_storage.sc_rollup_timeout_period_in_blocks ctxt in
  {| Sc_rollup_game_repr.timeout.alice := timeout_period_in_blocks;
    Sc_rollup_game_repr.timeout.bob := timeout_period_in_blocks;
    Sc_rollup_game_repr.timeout.last_turn_level := last_turn_level; |}.

[update_timeout ctxt rollup game idx] update the timeout left for the current player [game.turn]. Her new timeout is equal to [nb_of_block_left - (current_level - last_turn_level)] where [nb_of_block_left] is her current timeout.

Definition update_timeout
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (game : Sc_rollup_game_repr.t) (idx : Sc_rollup_game_repr.Index.t)
  : M? Raw_context.t :=
  let? '(ctxt, timeout) :=
    Store.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      (ctxt, rollup) idx in
  let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
  let sub_block_left (nb_of_block_left : int) : int :=
    nb_of_block_left -i
    (Int32.to_int
      (Raw_level_repr.diff_value current_level
        timeout.(Sc_rollup_game_repr.timeout.last_turn_level))) in
  let new_timeout :=
    match game.(Sc_rollup_game_repr.V1.t.turn) with
    | Sc_rollup_game_repr.Alice ⇒
      let nb_of_block_left :=
        sub_block_left timeout.(Sc_rollup_game_repr.timeout.alice) in
      Sc_rollup_game_repr.timeout.with_last_turn_level current_level
        (Sc_rollup_game_repr.timeout.with_alice nb_of_block_left timeout)
    | Sc_rollup_game_repr.Bob ⇒
      let nb_of_block_left :=
        sub_block_left timeout.(Sc_rollup_game_repr.timeout.bob) in
      Sc_rollup_game_repr.timeout.with_last_turn_level current_level
        (Sc_rollup_game_repr.timeout.with_bob nb_of_block_left timeout)
    end in
  let? '(ctxt, _) :=
    Store.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      (ctxt, rollup) idx new_timeout in
  return? ctxt.

Definition get_ongoing_game
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker1 : Signature.public_key_hash) (staker2 : Signature.public_key_hash)
  : M?
    (option (Sc_rollup_game_repr.V1.t × Sc_rollup_game_repr.Index.t) ×
      Raw_context.t) :=
  let stakers := Sc_rollup_game_repr.Index.make staker1 staker2 in
  let? '(ctxt, game) :=
    Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) stakers in
  let answer :=
    Option.map (fun (game : Sc_rollup_game_repr.V1.t) ⇒ (game, stakers)) game
    in
  return? (answer, ctxt).

Definition get_ongoing_game_for_staker
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash)
  : M?
    (option (Sc_rollup_game_repr.V1.t × Sc_rollup_game_repr.Index.t) ×
      Raw_context.t) :=
  let? '(ctxt, opponent) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) staker in
  match opponent with
  | Some opponent ⇒ get_ongoing_game ctxt rollup staker opponent
  | None ⇒ return? (None, ctxt)
  end.

[goto_inbox_level ctxt rollup inbox_level commit] Follows the predecessors of [commit] until it arrives at the exact [inbox_level]. The result is the commit hash at the given inbox level.

#[bypass_check(guard)]
Definition goto_inbox_level
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (inbox_level : Raw_level_repr.raw_level)
  (commit : Commitment_storage.Commitment_hash.t)
  : M? (Commitment_storage.Commitment_hash.t × Raw_context.t) :=
  let fix go
    (ctxt : Raw_context.t) (commit : Commitment_storage.Commitment_hash.t)
    {struct commit}
    : M? (Commitment_storage.Commitment_hash.t × Raw_context.t) :=
    let? '(info_value, ctxt) :=
      Commitment_storage.get_commitment_unsafe ctxt rollup commit in
    if
      Raw_level_repr.op_lteq
        info_value.(Sc_rollup_commitment_repr.V1.t.inbox_level) inbox_level
    then
      if
        Raw_level_repr.op_eq
          info_value.(Sc_rollup_commitment_repr.V1.t.inbox_level)
          inbox_level
      then
        return? (commit, ctxt)
      else
        Error_monad.error_value (Build_extensible "Asserted" unit tt)
    else
      go ctxt info_value.(Sc_rollup_commitment_repr.V1.t.predecessor) in
  go ctxt commit.

#[bypass_check(guard)]
Definition get_conflict_point
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker1 : Signature.public_key_hash) (staker2 : Signature.public_key_hash)
  : M? ((point × point) × Raw_context.t) :=
  let? '(lcc, ctxt) := Commitment_storage.last_cemented_commitment ctxt rollup
    in
  let? '(commit1, ctxt) := Stake_storage.find_staker ctxt rollup staker1 in
  let? '(commit2, ctxt) := Stake_storage.find_staker ctxt rollup staker2 in
  let? '_ :=
    Error_monad.fail_when
      ((Commitment_hash.op_eq commit1 Commitment_hash.zero) ||
      ((Commitment_hash.op_eq commit2 Commitment_hash.zero) ||
      ((Commitment_hash.op_eq commit1 lcc) ||
      (Commitment_hash.op_eq commit2 lcc))))
      (Build_extensible "Sc_rollup_no_conflict" unit tt) in
  let? '(commit1_info, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup commit1 in
  let? '(commit2_info, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup commit2 in
  let target_inbox_level :=
    Raw_level_repr.min commit1_info.(Sc_rollup_commitment_repr.V1.t.inbox_level)
      commit2_info.(Sc_rollup_commitment_repr.V1.t.inbox_level) in
  let? '(commit1, ctxt) :=
    goto_inbox_level ctxt rollup target_inbox_level commit1 in
  let? '(commit2, ctxt) :=
    goto_inbox_level ctxt rollup target_inbox_level commit2 in
  let fix traverse_in_parallel
    (ctxt : Raw_context.t) (commit1 : Commitment_storage.Commitment_hash.t)
    (commit2 : Commitment_storage.Commitment_hash.t) {struct commit1}
    : M? ((point × point) × Raw_context.t) :=
    let? '(commit1_info, ctxt) :=
      Commitment_storage.get_commitment_unsafe ctxt rollup commit1 in
    let? '(commit2_info, ctxt) :=
      Commitment_storage.get_commitment_unsafe ctxt rollup commit2 in
    if
      Raw_level_repr.op_eq
        commit1_info.(Sc_rollup_commitment_repr.V1.t.inbox_level)
        commit2_info.(Sc_rollup_commitment_repr.V1.t.inbox_level)
    then
      if
        Commitment_hash.op_eq
          commit1_info.(Sc_rollup_commitment_repr.V1.t.predecessor)
          commit2_info.(Sc_rollup_commitment_repr.V1.t.predecessor)
      then
        return?
          (({| point.commitment := commit1_info; point.hash := commit1; |},
            {| point.commitment := commit2_info; point.hash := commit2; |}),
            ctxt)
      else
        traverse_in_parallel ctxt
          commit1_info.(Sc_rollup_commitment_repr.V1.t.predecessor)
          commit2_info.(Sc_rollup_commitment_repr.V1.t.predecessor)
    else
      Error_monad.error_value (Build_extensible "Asserted" unit tt) in
  let? '_ :=
    Error_monad.fail_when (Commitment_hash.op_eq commit1 commit2)
      (Build_extensible "Sc_rollup_no_conflict" unit tt) in
  traverse_in_parallel ctxt commit1 commit2.

Definition get_game
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (stakers : Sc_rollup_game_repr.Index.t)
  : M? (Sc_rollup_game_repr.V1.t × Raw_context.t) :=
  let? '(ctxt, game) :=
    Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) stakers in
  match game with
  | Some g_value ⇒ return? (g_value, ctxt)
  | None ⇒
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Sc_rollup_no_game" unit tt)
  end.

[start_game ctxt rollup refuter defender] initialises the game or if it already exists fails with `Sc_rollup_game_already_started`.

The game is created with `refuter` as the first player to move. The initial state of the game will be obtained from the commitment pair belonging to [defender] at the conflict point. See [Sc_rollup_game_repr.initial] for documentation on how a pair of commitments is turned into an initial game state.

This also deals with the other bits of data in the storage around the game. It checks neither staker is already in a game (and also marks them as in a game once the new game is created). The reason we only allow a staker to play one game at a time is to keep the end-of-game logic simple---this way, a game can't end suddenly in the middle because one player lost their stake in another game, it can only end due to it's own moves or timeouts.

It also initialises the timeout level to the current level plus [timeout_period_in_blocks] (which will become a protocol constant soon) to mark the block level at which it becomes possible for anyone to end the game by timeout.

May fail with: {ul {li [Sc_rollup_does_not_exist] if [rollup] does not exist} {li [Sc_rollup_no_conflict] if [refuter] is staked on an ancestor of the commitment staked on by [defender], or vice versa} {li [Sc_rollup_not_staked] if one of the [refuter] or [defender] is not actually staked} {li [Sc_rollup_staker_in_game] if one of the [refuter] or [defender] is already playing a game} }

Definition start_game
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (refuter : Signature.public_key_hash) (defender : Signature.public_key_hash)
  : M? Raw_context.t :=
  let stakers := Sc_rollup_game_repr.Index.make refuter defender in
  let? '(ctxt, game_exists) :=
    Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
      (ctxt, rollup) stakers in
  let? '_ :=
    Error_monad.fail_when game_exists
      (Build_extensible "Sc_rollup_game_already_started" unit tt) in
  let? '(ctxt, opp_1) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) refuter in
  let? '(ctxt, opp_2) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) defender in
  let? '_ :=
    match (opp_1, opp_2) with
    | (None, None) ⇒ return? tt
    | (Some _refuter_opponent, None) ⇒
      Error_monad.Lwt_result_syntax.tzfail
        (Build_extensible "Sc_rollup_staker_in_game"
          Sc_rollup_errors.sc_rollup_staker_in_game_error
          (Sc_rollup_errors.Refuter refuter))
    | (None, Some _defender_opponent) ⇒
      Error_monad.Lwt_result_syntax.tzfail
        (Build_extensible "Sc_rollup_staker_in_game"
          Sc_rollup_errors.sc_rollup_staker_in_game_error
          (Sc_rollup_errors.Defender defender))
    | (Some _refuter_opponent, Some _defender_opponent) ⇒
      Error_monad.Lwt_result_syntax.tzfail
        (Build_extensible "Sc_rollup_staker_in_game"
          Sc_rollup_errors.sc_rollup_staker_in_game_error
          (Sc_rollup_errors.Both refuter defender))
    end in
  let?
    '(({| point.commitment := _info; point.hash := _refuter_commit |}, {|
      point.commitment := child_info; point.hash := _defender_commit |}),
      ctxt) := get_conflict_point ctxt rollup refuter defender in
  let? '(parent_info, ctxt) :=
    Commitment_storage.get_commitment_unsafe ctxt rollup
      child_info.(Sc_rollup_commitment_repr.V1.t.predecessor) in
  let? '(inbox_value, ctxt) := Sc_rollup_inbox_storage.get_inbox ctxt in
  let? '(ctxt, kind_value) :=
    Store.PVM_kind.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  let default_number_of_sections :=
    Constants_storage.sc_rollup_number_of_sections_in_dissection ctxt in
  let? slots_history_snapshot := Dal_slot_storage.get_slot_headers_history ctxt
    in
  let current_level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
  let game :=
    Sc_rollup_game_repr.initial (Sc_rollup_inbox_repr.take_snapshot inbox_value)
      slots_history_snapshot current_level (Sc_rollups.Kind.name_of kind_value)
      parent_info child_info refuter defender default_number_of_sections in
  let? '(ctxt, _) :=
    Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      (ctxt, rollup) stakers game in
  let? '(ctxt, _) :=
    Store.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      (ctxt, rollup) stakers (initial_timeout ctxt) in
  let? '(ctxt, _) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      (ctxt, rollup) refuter defender in
  let? '(ctxt, _) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      (ctxt, rollup) defender refuter in
  return? ctxt.

Definition game_move
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (player_value : Signature.public_key_hash)
  (opponent : Signature.public_key_hash)
  (refutation : Sc_rollup_game_repr.refutation)
  : M? (option Sc_rollup_game_repr.game_result × Raw_context.t) :=
  let stakers := Sc_rollup_game_repr.Index.make player_value opponent in
  let? '(game, ctxt) := get_game ctxt rollup stakers in
  let? '_ :=
    Error_monad.fail_unless
      (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) player_value
        (Sc_rollup_game_repr.Index.staker stakers
          game.(Sc_rollup_game_repr.V1.t.turn)))
      (Build_extensible "Sc_rollup_wrong_turn" unit tt) in
  let? '(ctxt, metadata) := Sc_rollup_storage.get_metadata ctxt rollup in
  let dal :=
    (Constants_storage.parametric_value ctxt).(Constants_parametric_repr.t.dal)
    in
  let? move_result :=
    Sc_rollup_game_repr.play
      dal.(Constants_parametric_repr.dal.cryptobox_parameters)
      dal.(Constants_parametric_repr.dal.attestation_lag) stakers metadata game
      refutation in
  match move_result with
  | Either.Left game_result ⇒ return? ((Some game_result), ctxt)
  | Either.Right new_game ⇒
    let? '(ctxt, _) :=
      Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
        (ctxt, rollup) stakers new_game in
    let? ctxt := update_timeout ctxt rollup game stakers in
    return? (None, ctxt)
  end.

Definition get_timeout
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (stakers : Sc_rollup_game_repr.Index.t)
  : M? (Sc_rollup_game_repr.timeout × Raw_context.t) :=
  let? '(ctxt, timeout_opt) :=
    Storage.Sc_rollup.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) stakers in
  match timeout_opt with
  | Some timeout ⇒ return? (timeout, ctxt)
  | None ⇒
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Sc_rollup_no_game" unit tt)
  end.

Definition timeout
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (stakers : Sc_rollup_game_repr.Index.t)
  : M? (Sc_rollup_game_repr.game_result × Raw_context.t) :=
  let level := (Raw_context.current_level ctxt).(Level_repr.t.level) in
  let? '(game, ctxt) := get_game ctxt rollup stakers in
  let? '(ctxt, timeout) :=
    Store.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      (ctxt, rollup) stakers in
  let? '_ :=
    let block_left_before_timeout :=
      match game.(Sc_rollup_game_repr.V1.t.turn) with
      | Sc_rollup_game_repr.Alice ⇒ timeout.(Sc_rollup_game_repr.timeout.alice)
      | Sc_rollup_game_repr.Bob ⇒ timeout.(Sc_rollup_game_repr.timeout.bob)
      end in
    let? level_of_timeout :=
      Raw_level_repr.add timeout.(Sc_rollup_game_repr.timeout.last_turn_level)
        block_left_before_timeout in
    Error_monad.fail_unless (Raw_level_repr.op_gt level level_of_timeout)
      (let blocks_left := Raw_level_repr.diff_value level_of_timeout level in
      let staker :=
        match game.(Sc_rollup_game_repr.V1.t.turn) with
        | Sc_rollup_game_repr.Alice ⇒
          stakers.(Sc_rollup_game_repr.Index.t.alice)
        | Sc_rollup_game_repr.Bob ⇒ stakers.(Sc_rollup_game_repr.Index.t.bob)
        end in
      Build_extensible "Sc_rollup_timeout_level_not_reached"
        (int32 × Signature.public_key_hash) (blocks_left, staker)) in
  let game_result :=
    match game.(Sc_rollup_game_repr.V1.t.game_state) with
    | Sc_rollup_game_repr.V1.Dissecting _ ⇒
      let loser :=
        Sc_rollup_game_repr.Index.staker stakers
          game.(Sc_rollup_game_repr.V1.t.turn) in
      Sc_rollup_game_repr.Loser
        {|
          Sc_rollup_game_repr.game_result.Loser.reason :=
            Sc_rollup_game_repr.Timeout;
          Sc_rollup_game_repr.game_result.Loser.loser := loser; |}
    |
      Sc_rollup_game_repr.V1.Final_move {|
        Sc_rollup_game_repr.game_state.Final_move.agreed_start_chunk := _;
          Sc_rollup_game_repr.game_state.Final_move.refuted_stop_chunk := _
          |} ⇒ Sc_rollup_game_repr.Draw
    end in
  return? (game_result, ctxt).

Definition reward (ctxt : Raw_context.t) (winner : Signature.public_key_hash)
  : M? (Raw_context.t × Receipt_repr.balance_updates) :=
  let winner_contract := Contract_repr.Implicit winner in
  let stake := Constants_storage.sc_rollup_stake_amount ctxt in
  let? reward := Tez_repr.op_divquestion stake 2 in
  Token.transfer None ctxt
    (Token.Source_infinite Token.Sc_rollup_refutation_rewards)
    (Token.Sink_container (Token.Contract winner_contract)) reward.

Definition apply_game_result
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (stakers : Sc_rollup_game_repr.Index.t)
  (game_result : Sc_rollup_game_repr.game_result)
  : M?
    (Sc_rollup_game_repr.status × Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let status := Sc_rollup_game_repr.Ended game_result in
  let? '(ctxt, balances_updates) :=
    match game_result with
    |
      Sc_rollup_game_repr.Loser {|
        Sc_rollup_game_repr.game_result.Loser.reason := _;
          Sc_rollup_game_repr.game_result.Loser.loser := loser
          |} ⇒
      let losing_staker := loser in
      let winning_staker :=
        let '{|
          Sc_rollup_game_repr.Index.t.alice := alice;
            Sc_rollup_game_repr.Index.t.bob := bob
            |} := stakers in
        if
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq) alice
            loser
        then
          bob
        else
          alice in
      let? '(ctxt, balance_updates_winner) := reward ctxt winning_staker in
      let? '(ctxt, _, _) :=
        Store.Game.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
          (ctxt, rollup) stakers in
      let? '(ctxt, balance_updates_loser) :=
        Stake_storage.remove_staker ctxt rollup losing_staker in
      let balances_updates :=
        Pervasives.op_at balance_updates_loser balance_updates_winner in
      return? (ctxt, balances_updates)
    | Sc_rollup_game_repr.Draw ⇒
      let? '(ctxt, balances_updates_alice) :=
        Stake_storage.remove_staker ctxt rollup
          stakers.(Sc_rollup_game_repr.Index.t.alice) in
      let? '(ctxt, balances_updates_bob) :=
        Stake_storage.remove_staker ctxt rollup
          stakers.(Sc_rollup_game_repr.Index.t.bob) in
      return?
        (ctxt, (Pervasives.op_at balances_updates_alice balances_updates_bob))
    end in
  let? '(ctxt, _, _) :=
    Store.Game_timeout.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
      (ctxt, rollup) stakers in
  let? '(ctxt, _, _) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
      (ctxt, rollup) stakers.(Sc_rollup_game_repr.Index.t.alice) in
  let? '(ctxt, _, _) :=
    Store.Opponent.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
      (ctxt, rollup) stakers.(Sc_rollup_game_repr.Index.t.bob) in
  return? (status, ctxt, balances_updates).

Module conflict.
  Record record : Set := Build {
    other : Signature.public_key_hash;
    their_commitment : Sc_rollup_commitment_repr.t;
    our_commitment : Sc_rollup_commitment_repr.t;
    parent_commitment : Sc_rollup_commitment_repr.Hash.t;
  }.
  Definition with_other other (r : record) :=
    Build other r.(their_commitment) r.(our_commitment) r.(parent_commitment).
  Definition with_their_commitment their_commitment (r : record) :=
    Build r.(other) their_commitment r.(our_commitment) r.(parent_commitment).
  Definition with_our_commitment our_commitment (r : record) :=
    Build r.(other) r.(their_commitment) our_commitment r.(parent_commitment).
  Definition with_parent_commitment parent_commitment (r : record) :=
    Build r.(other) r.(their_commitment) r.(our_commitment) parent_commitment.
End conflict.
Definition conflict := conflict.record.

Definition conflict_encoding : Data_encoding.encoding conflict :=
  Data_encoding.conv
    (fun (function_parameter : conflict) ⇒
      let '{|
        conflict.other := other;
          conflict.their_commitment := their_commitment;
          conflict.our_commitment := our_commitment;
          conflict.parent_commitment := parent_commitment
          |} := function_parameter in
      (other, their_commitment, our_commitment, parent_commitment))
    (fun (function_parameter :
      Signature.public_key_hash × Sc_rollup_commitment_repr.t ×
        Sc_rollup_commitment_repr.t × Sc_rollup_commitment_repr.Hash.t) ⇒
      let '(other, their_commitment, our_commitment, parent_commitment) :=
        function_parameter in
      {| conflict.other := other; conflict.their_commitment := their_commitment;
        conflict.our_commitment := our_commitment;
        conflict.parent_commitment := parent_commitment; |}) None
    (Data_encoding.obj4
      (Data_encoding.req None None "other"
        Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "their_commitment"
        Sc_rollup_commitment_repr.encoding)
      (Data_encoding.req None None "our_commitment"
        Sc_rollup_commitment_repr.encoding)
      (Data_encoding.req None None "parent_commitment"
        Sc_rollup_commitment_repr.Hash.encoding)).

Definition conflicting_stakers_uncarbonated
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (staker : Signature.public_key_hash) : M? (list conflict) :=
  let make_conflict
    (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
    (other : Signature.public_key_hash) (function_parameter : point × point)
    : M? conflict :=
    let '(our_point, their_point) := function_parameter in
    let our_hash : Commitment_hash.t :=
      our_point.(point.hash)
    in let their_hash : Commitment_hash.t :=
      their_point.(point.hash) in
    let get := Sc_rollup_commitment_storage.get_commitment_unsafe ctxt rollup in
    let? '(our_commitment, _) := get our_hash in
    let? '(their_commitment, _) := get their_hash in
    let parent_commitment :=
      our_commitment.(Sc_rollup_commitment_repr.V1.t.predecessor) in
    return?
      {| conflict.other := other; conflict.their_commitment := their_commitment;
        conflict.our_commitment := our_commitment;
        conflict.parent_commitment := parent_commitment; |} in
  let? '(_ctxt, stakers) := Store.stakers ctxt rollup in
  List.fold_left_es
    (fun (conflicts : list conflict) ⇒
      fun (function_parameter :
        Signature.public_key_hash × Sc_rollup_commitment_repr.Hash.t) ⇒
        let '(other_staker, _) := function_parameter in
        let res := get_conflict_point ctxt rollup staker other_staker in
        match res with
        | Pervasives.Ok (conflict_point, _) ⇒
          let? conflict := make_conflict ctxt rollup other_staker conflict_point
            in
          return? (cons conflict conflicts)
        | Pervasives.Error _ ⇒ return? conflicts
        end) nil stakers.