Skip to main content

🦏 Sc_rollup_game_repr.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.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.

Module Proof_start_state_hash_mismatch.
  Record record : Set := Build {
    start_state_hash : option Sc_rollup_repr.State_hash.t;
    start_proof : Sc_rollup_repr.State_hash.t;
  }.
  Definition with_start_state_hash start_state_hash (r : record) :=
    Build start_state_hash r.(start_proof).
  Definition with_start_proof start_proof (r : record) :=
    Build r.(start_state_hash) start_proof.
End Proof_start_state_hash_mismatch.
Definition Proof_start_state_hash_mismatch :=
  Proof_start_state_hash_mismatch.record.

Module Proof_stop_state_hash_failed_to_refute.
  Record record : Set := Build {
    stop_state_hash : option Sc_rollup_repr.State_hash.t;
    stop_proof : option Sc_rollup_repr.State_hash.t;
  }.
  Definition with_stop_state_hash stop_state_hash (r : record) :=
    Build stop_state_hash r.(stop_proof).
  Definition with_stop_proof stop_proof (r : record) :=
    Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_refute.
Definition Proof_stop_state_hash_failed_to_refute :=
  Proof_stop_state_hash_failed_to_refute.record.

Module Proof_stop_state_hash_failed_to_validate.
  Record record : Set := Build {
    stop_state_hash : option Sc_rollup_repr.State_hash.t;
    stop_proof : option Sc_rollup_repr.State_hash.t;
  }.
  Definition with_stop_state_hash stop_state_hash (r : record) :=
    Build stop_state_hash r.(stop_proof).
  Definition with_stop_proof stop_proof (r : record) :=
    Build r.(stop_state_hash) stop_proof.
End Proof_stop_state_hash_failed_to_validate.
Definition Proof_stop_state_hash_failed_to_validate :=
  Proof_stop_state_hash_failed_to_validate.record.

Definition pp_hash_opt
  (fmt : Format.formatter)
  (function_parameter : option Sc_rollup_repr.State_hash.t) : unit :=
  match function_parameter with
  | None
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "None"
          CamlinternalFormatBasics.End_of_format) "None")
  | Some x_valueSc_rollup_repr.State_hash.pp fmt x_value
  end.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let description := "Dissection choice not found" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissection_choice_not_found" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (choice : Sc_rollup_tick_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "No section starting with tick "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " found"
                      CamlinternalFormatBasics.End_of_format)))
                "No section starting with tick %a found") Sc_rollup_tick_repr.pp
              choice))
      (Data_encoding.obj1
        (Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissection_choice_not_found" then
            let tick := cast Sc_rollup_tick_repr.t payload in
            Some tick
          else None
        end)
      (fun (tick : Sc_rollup_tick_repr.t) ⇒
        Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
          tick) in
  let description := "The distance for a proof should be equal to 1" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Dissection_unexpected_section_size" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (n_value : Z.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Distance should be equal to 1 in a proof, but got "
                  (CamlinternalFormatBasics.Alpha
                    CamlinternalFormatBasics.End_of_format))
                "Distance should be equal to 1 in a proof, but got %a")
              Z.pp_print n_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "n" Data_encoding.n_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_unexpected_section_size" then
            let n_value := cast Z.t payload in
            Some n_value
          else None
        end)
      (fun (n_value : Z.t) ⇒
        Build_extensible "Proof_unexpected_section_size" Z.t n_value) in
  let description := "The start state hash of the proof is invalid" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Proof_start_state_hash_mismatch" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
            let '(start_state_hash, start_proof) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "start("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ") should be equal to start_proof("
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal ")" % char
                          CamlinternalFormatBasics.End_of_format)))))
                "start(%a) should be equal to start_proof(%a)") pp_hash_opt
              start_state_hash Sc_rollup_repr.State_hash.pp start_proof))
      (Data_encoding.obj2
        (Data_encoding.req None None "start_state_hash"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
        (Data_encoding.req None None "start_proof"
          Sc_rollup_repr.State_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_start_state_hash_mismatch" then
            let '{|
              Proof_start_state_hash_mismatch.start_state_hash := start_state_hash;
                Proof_start_state_hash_mismatch.start_proof := start_proof
                |} := cast Proof_start_state_hash_mismatch payload in
            Some (start_state_hash, start_proof)
          else None
        end)
      (fun (function_parameter :
        option Sc_rollup_repr.State_hash.t × Sc_rollup_repr.State_hash.t) ⇒
        let '(start_state_hash, start_proof) := function_parameter in
        Build_extensible "Proof_start_state_hash_mismatch"
          Proof_start_state_hash_mismatch
          {|
            Proof_start_state_hash_mismatch.start_state_hash :=
              start_state_hash;
            Proof_start_state_hash_mismatch.start_proof := start_proof; |}) in
  let description := "Failed to refute the stop state hash with the proof" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Proof_stop_state_hash_failed_to_refute" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            option Sc_rollup_repr.State_hash.t ×
              option Sc_rollup_repr.State_hash.t) ⇒
            let '(stop_state_hash, stop_proof) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Trying to refute "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ", the stop_proof must not be equal to "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "Trying to refute %a, the stop_proof must not be equal to %a")
              pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
      (Data_encoding.obj2
        (Data_encoding.req None None "stop_state_hash"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
        (Data_encoding.req None None "stop_proof"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_stop_state_hash_failed_to_refute" then
            let '{|
              Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state_hash;
                Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof
                |} := cast Proof_stop_state_hash_failed_to_refute payload in
            Some (stop_state_hash, stop_proof)
          else None
        end)
      (fun (function_parameter :
        option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
        ⇒
        let '(stop_state_hash, stop_proof) := function_parameter in
        Build_extensible "Proof_stop_state_hash_failed_to_refute"
          Proof_stop_state_hash_failed_to_refute
          {|
            Proof_stop_state_hash_failed_to_refute.stop_state_hash :=
              stop_state_hash;
            Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |})
    in
  let description := "Failed to validate the stop state hash with the proof" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Proof_stop_state_hash_failed_to_validate" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            option Sc_rollup_repr.State_hash.t ×
              option Sc_rollup_repr.State_hash.t) ⇒
            let '(stop_state_hash, stop_proof) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Trying to validate "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ", the stop_proof must not be equal to "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "Trying to validate %a, the stop_proof must not be equal to %a")
              pp_hash_opt stop_state_hash pp_hash_opt stop_proof))
      (Data_encoding.obj2
        (Data_encoding.req None None "stop_state_hash"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
        (Data_encoding.req None None "stop_proof"
          (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_stop_state_hash_failed_to_validate" then
            let '{|
              Proof_stop_state_hash_failed_to_validate.stop_state_hash := stop_state_hash;
                Proof_stop_state_hash_failed_to_validate.stop_proof :=
                  stop_proof
                |} := cast Proof_stop_state_hash_failed_to_validate payload in
            Some (stop_state_hash, stop_proof)
          else None
        end)
      (fun (function_parameter :
        option Sc_rollup_repr.State_hash.t × option Sc_rollup_repr.State_hash.t)
        ⇒
        let '(stop_state_hash, stop_proof) := function_parameter in
        Build_extensible "Proof_stop_state_hash_failed_to_validate"
          Proof_stop_state_hash_failed_to_validate
          {|
            Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
              stop_state_hash;
            Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof;
            |}) in
  let description := "Tried to play a dissecting when the final move started" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dissecting_during_final_move" description description
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf description)) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Dissecting_during_final_move" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Dissecting_during_final_move" unit tt) in
  tt.

Inductive player : Set :=
| Alice : player
| Bob : player.

Module V1.
  Definition dissection_chunk : Set := Sc_rollup_dissection_chunk_repr.t.

Records for the constructor parameters
  Module ConstructorRecords_game_state.
    Module game_state.
      Module Dissecting.
        Record record {dissection default_number_of_sections : Set} : Set := Build {
          dissection : dissection;
          default_number_of_sections : default_number_of_sections;
        }.
        Arguments record : clear implicits.
        Definition with_dissection {t_dissection t_default_number_of_sections}
          dissection (r : record t_dissection t_default_number_of_sections) :=
          Build t_dissection t_default_number_of_sections dissection
            r.(default_number_of_sections).
        Definition with_default_number_of_sections
          {t_dissection t_default_number_of_sections} default_number_of_sections
          (r : record t_dissection t_default_number_of_sections) :=
          Build t_dissection t_default_number_of_sections r.(dissection)
            default_number_of_sections.
      End Dissecting.
      Definition Dissecting_skeleton := Dissecting.record.

      Module Final_move.
        Record record {agreed_start_chunk refuted_stop_chunk : Set} : Set := Build {
          agreed_start_chunk : agreed_start_chunk;
          refuted_stop_chunk : refuted_stop_chunk;
        }.
        Arguments record : clear implicits.
        Definition with_agreed_start_chunk
          {t_agreed_start_chunk t_refuted_stop_chunk} agreed_start_chunk
          (r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
          Build t_agreed_start_chunk t_refuted_stop_chunk agreed_start_chunk
            r.(refuted_stop_chunk).
        Definition with_refuted_stop_chunk
          {t_agreed_start_chunk t_refuted_stop_chunk} refuted_stop_chunk
          (r : record t_agreed_start_chunk t_refuted_stop_chunk) :=
          Build t_agreed_start_chunk t_refuted_stop_chunk r.(agreed_start_chunk)
            refuted_stop_chunk.
      End Final_move.
      Definition Final_move_skeleton := Final_move.record.
    End game_state.
  End ConstructorRecords_game_state.
  Import ConstructorRecords_game_state.

  Reserved Notation "'game_state.Dissecting".
  Reserved Notation "'game_state.Final_move".

  Inductive game_state : Set :=
  | Dissecting : 'game_state.Dissecting game_state
  | Final_move : 'game_state.Final_move game_state
  
  where "'game_state.Dissecting" :=
    (game_state.Dissecting_skeleton (list dissection_chunk) int)
  and "'game_state.Final_move" :=
    (game_state.Final_move_skeleton dissection_chunk dissection_chunk).

  Module game_state.
    Include ConstructorRecords_game_state.game_state.
    Definition Dissecting := 'game_state.Dissecting.
    Definition Final_move := 'game_state.Final_move.
  End game_state.

  Module t.
    Record record : Set := Build {
      turn : player;
      inbox_snapshot : Sc_rollup_inbox_repr.history_proof;
      dal_snapshot : Dal_slot_repr.History.t;
      start_level : Raw_level_repr.t;
      inbox_level : Raw_level_repr.t;
      pvm_name : string;
      game_state : game_state;
    }.
    Definition with_turn turn (r : record) :=
      Build turn r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
        r.(inbox_level) r.(pvm_name) r.(game_state).
    Definition with_inbox_snapshot inbox_snapshot (r : record) :=
      Build r.(turn) inbox_snapshot r.(dal_snapshot) r.(start_level)
        r.(inbox_level) r.(pvm_name) r.(game_state).
    Definition with_dal_snapshot dal_snapshot (r : record) :=
      Build r.(turn) r.(inbox_snapshot) dal_snapshot r.(start_level)
        r.(inbox_level) r.(pvm_name) r.(game_state).
    Definition with_start_level start_level (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) start_level
        r.(inbox_level) r.(pvm_name) r.(game_state).
    Definition with_inbox_level inbox_level (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
        inbox_level r.(pvm_name) r.(game_state).
    Definition with_pvm_name pvm_name (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
        r.(inbox_level) pvm_name r.(game_state).
    Definition with_game_state game_state (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(dal_snapshot) r.(start_level)
        r.(inbox_level) r.(pvm_name) game_state.
  End t.
  Definition t := t.record.

  Definition player_encoding : Data_encoding.encoding player :=
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [
        Data_encoding.case_value "Alice" None (Data_encoding.Tag 0)
          (Data_encoding.constant "alice")
          (fun (function_parameter : player) ⇒
            match function_parameter with
            | AliceSome tt
            | _None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Alice);
        Data_encoding.case_value "Bob" None (Data_encoding.Tag 1)
          (Data_encoding.constant "bob")
          (fun (function_parameter : player) ⇒
            match function_parameter with
            | BobSome tt
            | _None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Bob)
      ].

  Definition player_equal (p1 : player) (p2 : player) : bool :=
    match (p1, p2) with
    | (Alice, Alice)true
    | (Bob, Bob)true
    | (_, _)false
    end.

  Definition game_state_equal (gs1 : game_state) (gs2 : game_state) : bool :=
    match (gs1, gs2) with
    |
      (Dissecting {|
        game_state.Dissecting.dissection := dissection1;
          game_state.Dissecting.default_number_of_sections :=
            default_number_of_sections1
          |},
        Dissecting {|
          game_state.Dissecting.dissection := dissection2;
            game_state.Dissecting.default_number_of_sections :=
              default_number_of_sections2
            |})
      (Compare.Int.equal default_number_of_sections1 default_number_of_sections2)
      &&
      (List.equal Sc_rollup_dissection_chunk_repr.equal dissection1 dissection2)
    | (Dissecting _, _)false
    |
      (Final_move {|
        game_state.Final_move.agreed_start_chunk := agreed_start_chunk1;
          game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk1
          |},
        Final_move {|
          game_state.Final_move.agreed_start_chunk := agreed_start_chunk2;
            game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk2
            |})
      (Sc_rollup_dissection_chunk_repr.equal agreed_start_chunk1
        agreed_start_chunk2) &&
      (Sc_rollup_dissection_chunk_repr.equal refuted_stop_chunk1
        refuted_stop_chunk2)
    | (Final_move _, _)false
    end.

  Definition equal (function_parameter : t) : t bool :=
    let '{|
      t.turn := turn;
        t.inbox_snapshot := inbox_snapshot;
        t.dal_snapshot := dal_snapshot;
        t.start_level := start_level;
        t.inbox_level := inbox_level;
        t.pvm_name := pvm_name;
        t.game_state := game_state
        |} := function_parameter in
    fun (g2 : t) ⇒
      (player_equal turn g2.(t.turn)) &&
      ((Sc_rollup_inbox_repr.equal_history_proof inbox_snapshot
        g2.(t.inbox_snapshot)) &&
      ((Dal_slot_repr.History.equal dal_snapshot g2.(t.dal_snapshot)) &&
      ((Raw_level_repr.equal start_level g2.(t.start_level)) &&
      ((Raw_level_repr.equal inbox_level g2.(t.inbox_level)) &&
      ((String.equal pvm_name g2.(t.pvm_name)) &&
      (game_state_equal game_state g2.(t.game_state))))))).

  Definition string_of_player (function_parameter : player) : string :=
    match function_parameter with
    | Alice ⇒ "alice"
    | Bob ⇒ "bob"
    end.

  Definition pp_player (ppf : Format.formatter) (player_value : player)
    : unit := Format.pp_print_string ppf (string_of_player player_value).

  Definition opponent (function_parameter : player) : player :=
    match function_parameter with
    | AliceBob
    | BobAlice
    end.

  Definition dissection_encoding
    : Data_encoding.encoding (list Sc_rollup_dissection_chunk_repr.t) :=
    Data_encoding.list_value None Sc_rollup_dissection_chunk_repr.encoding.

  Definition game_state_encoding : Data_encoding.encoding game_state :=
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [
        Data_encoding.case_value "Dissecting" None (Data_encoding.Tag 0)
          (Data_encoding.obj3
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "Dissecting"))
            (Data_encoding.req None None "dissection"
              dissection_encoding)
            (Data_encoding.req None None "default_number_of_sections"
              Data_encoding.uint8))
          (fun (function_parameter : game_state) ⇒
            match function_parameter with
            |
              Dissecting {|
                game_state.Dissecting.dissection := dissection;
                  game_state.Dissecting.default_number_of_sections
                    :=
                    default_number_of_sections
                  |} ⇒
              Some (tt, dissection, default_number_of_sections)
            | _None
            end)
          (fun (function_parameter :
            unit × list Sc_rollup_dissection_chunk_repr.t × int) ⇒
            let '(_, dissection, default_number_of_sections) :=
              function_parameter in
            Dissecting
              {| game_state.Dissecting.dissection := dissection;
                game_state.Dissecting.default_number_of_sections
                  := default_number_of_sections; |});
        Data_encoding.case_value "Final_move" None (Data_encoding.Tag 1)
          (Data_encoding.obj3
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "Final_move"))
            (Data_encoding.req None None "agreed_start_chunk"
              Sc_rollup_dissection_chunk_repr.encoding)
            (Data_encoding.req None None "refuted_stop_chunk"
              Sc_rollup_dissection_chunk_repr.encoding))
          (fun (function_parameter : game_state) ⇒
            match function_parameter with
            |
              Final_move {|
                game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
                  game_state.Final_move.refuted_stop_chunk
                    :=
                    refuted_stop_chunk
                  |} ⇒
              Some (tt, agreed_start_chunk, refuted_stop_chunk)
            | _None
            end)
          (fun (function_parameter :
            unit × Sc_rollup_dissection_chunk_repr.t ×
              Sc_rollup_dissection_chunk_repr.t) ⇒
            let '(_, agreed_start_chunk, refuted_stop_chunk) :=
              function_parameter in
            Final_move
              {|
                game_state.Final_move.agreed_start_chunk :=
                  agreed_start_chunk;
                game_state.Final_move.refuted_stop_chunk :=
                  refuted_stop_chunk; |})
      ].

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.turn := turn;
            t.inbox_snapshot := inbox_snapshot;
            t.dal_snapshot := dal_snapshot;
            t.start_level := start_level;
            t.inbox_level := inbox_level;
            t.pvm_name := pvm_name;
            t.game_state := game_state
            |} := function_parameter in
        (turn, inbox_snapshot, dal_snapshot, start_level, inbox_level, pvm_name,
          game_state))
      (fun (function_parameter :
        player × Sc_rollup_inbox_repr.history_proof × Dal_slot_repr.History.t ×
          Raw_level_repr.t × Raw_level_repr.t × string × game_state) ⇒
        let
          '(turn, inbox_snapshot, dal_snapshot, start_level, inbox_level,
            pvm_name, game_state) := function_parameter in
        {| t.turn := turn; t.inbox_snapshot := inbox_snapshot;
          t.dal_snapshot := dal_snapshot; t.start_level := start_level;
          t.inbox_level := inbox_level; t.pvm_name := pvm_name;
          t.game_state := game_state; |}) None
      (Data_encoding.obj7 (Data_encoding.req None None "turn" player_encoding)
        (Data_encoding.req None None "inbox_snapshot"
          Sc_rollup_inbox_repr.history_proof_encoding)
        (Data_encoding.req None None "dal_snapshot"
          Dal_slot_repr.History.encoding)
        (Data_encoding.req None None "start_level" Raw_level_repr.encoding)
        (Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
        (Data_encoding.req None None "pvm_name" Data_encoding.string_value)
        (Data_encoding.req None None "game_state" game_state_encoding)).

  Definition pp_dissection
    (ppf : Format.formatter) (d_value : list Sc_rollup_dissection_chunk_repr.t)
    : unit :=
    Format.pp_print_list
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf (";" ++ String.String "010" "")))
      Sc_rollup_dissection_chunk_repr.pp ppf d_value.

  Definition pp_game_state (ppf : Format.formatter) (game_state : game_state)
    : unit :=
    match game_state with
    |
      Dissecting {|
        game_state.Dissecting.dissection := dissection;
          game_state.Dissecting.default_number_of_sections :=
            default_number_of_sections
          |} ⇒
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Dissecting "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal " using "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal " number of sections"
                    CamlinternalFormatBasics.End_of_format)))))
          "Dissecting %a using %d number of sections") pp_dissection dissection
        default_number_of_sections
    |
      Final_move {|
        game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
          game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
          |} ⇒
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Final move to refute "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal " from "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ", opponent failed to refute"
                    CamlinternalFormatBasics.End_of_format)))))
          "Final move to refute %a from %a, opponent failed to refute")
        Sc_rollup_dissection_chunk_repr.pp agreed_start_chunk
        Sc_rollup_dissection_chunk_repr.pp refuted_stop_chunk
    end.

  Definition pp (ppf : Format.formatter) (game : t) : unit :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal " playing; inbox snapshot = "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal "; start level = "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal "; inbox level = "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal "; pvm_name = "
                        (CamlinternalFormatBasics.String
                          CamlinternalFormatBasics.No_padding
                          (CamlinternalFormatBasics.String_literal
                            "; game_state = "
                            (CamlinternalFormatBasics.Alpha
                              CamlinternalFormatBasics.End_of_format)))))))))))
        "%a playing; inbox snapshot = %a; start level = %a; inbox level = %a; pvm_name = %s; game_state = %a")
      pp_player game.(t.turn) Sc_rollup_inbox_repr.pp_history_proof
      game.(t.inbox_snapshot) Raw_level_repr.pp game.(t.start_level)
      Raw_level_repr.pp game.(t.inbox_level) game.(t.pvm_name) pp_game_state
      game.(t.game_state).
End V1.

Inductive versioned : Set :=
| V1 : V1.t versioned.

Definition versioned_encoding : Data_encoding.encoding versioned :=
  Data_encoding.union None
    [
      Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
        (fun (function_parameter : versioned) ⇒
          let 'V1 game := function_parameter in
          Some game) (fun (game : V1.t) ⇒ V1 game)
    ].

Include V1.

Definition of_versioned (function_parameter : versioned) : V1.t :=
  let 'V1 game := function_parameter in
  game.

Definition to_versioned (game : V1.t) : versioned := V1 game.

Module Index.
  Module t.
    Record record : Set := Build {
      alice : Signature.public_key_hash;
      bob : Signature.public_key_hash;
    }.
    Definition with_alice alice (r : record) :=
      Build alice r.(bob).
    Definition with_bob bob (r : record) :=
      Build r.(alice) bob.
  End t.
  Definition t := t.record.

  Definition make
    (a_value : Signature.public_key_hash) (b_value : Signature.public_key_hash)
    : t :=
    let '(alice, bob) :=
      if
        (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
          b_value) >i 0
      then
        (b_value, a_value)
      else
        (a_value, b_value) in
    {| t.alice := alice; t.bob := bob; |}.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{| t.alice := alice; t.bob := bob |} := function_parameter in
        (alice, bob))
      (fun (function_parameter :
        Signature.public_key_hash × Signature.public_key_hash) ⇒
        let '(alice, bob) := function_parameter in
        make alice bob) None
      (Data_encoding.obj2
        (Data_encoding.req None None "alice"
          Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
        (Data_encoding.req None None "bob"
          Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))).

  Definition compare (function_parameter : t) : t int :=
    let '{| t.alice := a_value; t.bob := b_value |} := function_parameter in
    fun (function_parameter : t) ⇒
      let '{| t.alice := c_value; t.bob := d_value |} := function_parameter in
      match
        Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) a_value
          c_value with
      | 0 ⇒
        Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) b_value
          d_value
      | x_valuex_value
      end.

  Definition to_path (function_parameter : t) : list string list string :=
    let '{| t.alice := alice; t.bob := bob |} := function_parameter in
    fun (p_value : list string) ⇒
      cons
        (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
        (cons
          (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob)
          p_value).

  Definition both_of_b58check_opt (function_parameter : string × string)
    : option t :=
    let '(a_value, b_value) := function_parameter in
    let op_letstar {A B : Set} : option A (A option B) option B :=
      Option.bind in
    op_letstar
      (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
        a_value)
      (fun a_staker
        op_letstar
          (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt)
            b_value) (fun b_stakerSome (make a_staker b_staker))).

  Definition of_path {A : Set} (function_parameter : list string)
    : Pervasives.result (option t) A :=
    match function_parameter with
    | cons a_value (cons b_value []) ⇒
      return? (both_of_b58check_opt (a_value, b_value))
    | _return? None
    end.

  Definition path_length {A : Set} : Pervasives.result int A := return? 2.

  Definition rpc_arg : RPC_arg.arg t :=
    let descr_value :=
      "A pair of stakers that index a smart contract rollup refutation game." in
    let construct (function_parameter : t) : string :=
      let '{| t.alice := alice; t.bob := bob |} := function_parameter in
      Format.sprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.Char_literal "-" % char
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format))) "%s-%s")
        (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) alice)
        (Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check) bob) in
    let destruct (s_value : string) : Pervasives.result t string :=
      match String.split_on_char "-" % char s_value with
      | cons a_value (cons b_value []) ⇒
        match both_of_b58check_opt (a_value, b_value) with
        | Some stakersreturn? stakers
        | None
          Result.error_value
            (Format.sprintf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid game index notation "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format))
                "Invalid game index notation %s") s_value)
        end
      | _
        Result.error_value
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid game index notation "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "Invalid game index notation %s") s_value)
      end in
    RPC_arg.make (Some descr_value) "game_index" destruct construct tt.

  Definition staker (function_parameter : t)
    : player Signature.public_key_hash :=
    let '{| t.alice := alice; t.bob := bob |} := function_parameter in
    fun (function_parameter : player) ⇒
      match function_parameter with
      | Alicealice
      | Bobbob
      end.
End Index.

Definition make_chunk
  (state_hash : option Sc_rollup_repr.State_hash.t)
  (tick : Sc_rollup_tick_repr.t) : dissection_chunk :=
  {| Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
    Sc_rollup_dissection_chunk_repr.t.tick := tick; |}.

Definition initial
  (inbox_value : Sc_rollup_inbox_repr.history_proof)
  (dal_snapshot : Dal_slot_repr.History.t) (start_level : Raw_level_repr.t)
  (pvm_name : string) (parent : Sc_rollup_commitment_repr.t)
  (child : Sc_rollup_commitment_repr.t) (refuter : Signature.public_key_hash)
  (defender : Signature.public_key_hash) (default_number_of_sections : int)
  : t :=
  let '{| Index.t.alice := alice |} := Index.make refuter defender in
  let alice_to_play :=
    Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) alice refuter in
  let tick :=
    Sc_rollup_tick_repr.of_number_of_ticks
      child.(Sc_rollup_commitment_repr.V1.t.number_of_ticks) in
  let game_state :=
    V1.Dissecting
      {|
        game_state.Dissecting.dissection :=
          [
            make_chunk
              (Some
                parent.(Sc_rollup_commitment_repr.V1.t.compressed_state))
              Sc_rollup_tick_repr.initial;
            make_chunk
              (Some
                child.(Sc_rollup_commitment_repr.V1.t.compressed_state))
              tick;
            make_chunk None (Sc_rollup_tick_repr.next tick)
          ];
        game_state.Dissecting.default_number_of_sections :=
          default_number_of_sections; |} in
  {|
    V1.t.turn :=
      if alice_to_play then
        Alice
      else
        Bob; V1.t.inbox_snapshot := inbox_value;
    V1.t.dal_snapshot := dal_snapshot; V1.t.start_level := start_level;
    V1.t.inbox_level := child.(Sc_rollup_commitment_repr.V1.t.inbox_level);
    V1.t.pvm_name := pvm_name; V1.t.game_state := game_state; |}.

Inductive step : Set :=
| Dissection : list dissection_chunk step
| Proof : Sc_rollup_proof_repr.t step.

Definition step_encoding : Data_encoding.encoding step :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Dissection" None (Data_encoding.Tag 0)
        dissection_encoding
        (fun (function_parameter : step) ⇒
          match function_parameter with
          | Dissection d_valueSome d_value
          | _None
          end) (fun (d_value : list dissection_chunk) ⇒ Dissection d_value);
      Data_encoding.case_value "Proof" None (Data_encoding.Tag 1)
        Sc_rollup_proof_repr.encoding
        (fun (function_parameter : step) ⇒
          match function_parameter with
          | Proof p_valueSome p_value
          | _None
          end) (fun (p_value : Sc_rollup_proof_repr.t) ⇒ Proof p_value)
    ].

Definition pp_step (ppf : Format.formatter) (step : step) : unit :=
  match step with
  | Dissection states
    let '_ :=
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Dissection:"
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              CamlinternalFormatBasics.End_of_format)) "Dissection:@ ") in
    Format.pp_print_list
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string ppf
              (";" ++ String.String "010" (String.String "010" ""))))
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : dissection_chunk) ⇒
          let '{|
            Sc_rollup_dissection_chunk_repr.t.state_hash := state_hash;
              Sc_rollup_dissection_chunk_repr.t.tick := tick
              |} := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Tick: "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "," % char
                    (CamlinternalFormatBasics.Formatting_lit
                      (CamlinternalFormatBasics.Break "@ " 1 0)
                      (CamlinternalFormatBasics.String_literal "State: "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Char_literal "010" % char
                            CamlinternalFormatBasics.End_of_format)))))))
              ("Tick: %a,@ State: %a" ++ String.String "010" ""))
            Sc_rollup_tick_repr.pp tick
            (Format.pp_print_option None Sc_rollup_repr.State_hash.pp)
            state_hash) ppf states
  | Proof proof_value
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "proof: "
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
        "proof: %a") Sc_rollup_proof_repr.pp proof_value
  end.

Module refutation.
  Record record : Set := Build {
    choice : Sc_rollup_tick_repr.t;
    step : step;
  }.
  Definition with_choice choice (r : record) :=
    Build choice r.(step).
  Definition with_step step (r : record) :=
    Build r.(choice) step.
End refutation.
Definition refutation := refutation.record.

Definition pp_refutation
  (ppf : Format.formatter) (function_parameter : refutation) : unit :=
  let '{| refutation.choice := choice; refutation.step := step |} :=
    function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "Tick: "
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@ " 1 0)
            (CamlinternalFormatBasics.String_literal "Step: "
              (CamlinternalFormatBasics.Alpha
                CamlinternalFormatBasics.End_of_format))))) "Tick: %a@ Step: %a")
    Sc_rollup_tick_repr.pp choice pp_step step.

Definition refutation_encoding : Data_encoding.encoding refutation :=
  Data_encoding.conv
    (fun (function_parameter : refutation) ⇒
      let '{| refutation.choice := choice; refutation.step := step |} :=
        function_parameter in
      (choice, step))
    (fun (function_parameter : Sc_rollup_tick_repr.t × step) ⇒
      let '(choice, step) := function_parameter in
      {| refutation.choice := choice; refutation.step := step; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "choice" Sc_rollup_tick_repr.encoding)
      (Data_encoding.req None None "step" step_encoding)).

Inductive reason : Set :=
| Conflict_resolved : reason
| Timeout : reason.

Definition pp_reason (ppf : Format.formatter) (reason_value : reason) : unit :=
  match reason_value with
  | Conflict_resolved
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "conflict resolved"
          CamlinternalFormatBasics.End_of_format) "conflict resolved")
  | Timeout
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "timeout"
          CamlinternalFormatBasics.End_of_format) "timeout")
  end.

Definition reason_encoding : Data_encoding.encoding reason :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Conflict_resolved" None (Data_encoding.Tag 0)
        (Data_encoding.constant "conflict_resolved")
        (fun (function_parameter : reason) ⇒
          match function_parameter with
          | Conflict_resolvedSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Conflict_resolved);
      Data_encoding.case_value "Timeout" None (Data_encoding.Tag 1)
        (Data_encoding.constant "timeout")
        (fun (function_parameter : reason) ⇒
          match function_parameter with
          | TimeoutSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Timeout)
    ].

Records for the constructor parameters
Module ConstructorRecords_game_result.
  Module game_result.
    Module Loser.
      Record record {reason loser : Set} : Set := Build {
        reason : reason;
        loser : loser;
      }.
      Arguments record : clear implicits.
      Definition with_reason {t_reason t_loser} reason
        (r : record t_reason t_loser) :=
        Build t_reason t_loser reason r.(loser).
      Definition with_loser {t_reason t_loser} loser
        (r : record t_reason t_loser) :=
        Build t_reason t_loser r.(reason) loser.
    End Loser.
    Definition Loser_skeleton := Loser.record.
  End game_result.
End ConstructorRecords_game_result.
Import ConstructorRecords_game_result.

Reserved Notation "'game_result.Loser".

Inductive game_result : Set :=
| Loser : 'game_result.Loser game_result
| Draw : game_result

where "'game_result.Loser" :=
  (game_result.Loser_skeleton reason Signature.public_key_hash).

Module game_result.
  Include ConstructorRecords_game_result.game_result.
  Definition Loser := 'game_result.Loser.
End game_result.

Definition pp_game_result (ppf : Format.formatter) (r_value : game_result)
  : unit :=
  match r_value with
  |
    Loser {|
      game_result.Loser.reason := reason_value;
        game_result.Loser.loser := loser
        |} ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal " lost because: "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))) "%a lost because: %a")
      Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) loser pp_reason
      reason_value
  | Draw
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Draw"
          CamlinternalFormatBasics.End_of_format) "Draw")
  end.

Definition game_result_encoding : Data_encoding.encoding game_result :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Loser" None (Data_encoding.Tag 0)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "loser"))
          (Data_encoding.req None None "reason" reason_encoding)
          (Data_encoding.req None None "player"
            Sc_rollup_repr.Staker.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
        (fun (function_parameter : game_result) ⇒
          match function_parameter with
          |
            Loser {|
              game_result.Loser.reason := reason_value;
                game_result.Loser.loser := loser
                |} ⇒ Some (tt, reason_value, loser)
          | _None
          end)
        (fun (function_parameter : unit × reason × Signature.public_key_hash)
          ⇒
          let '(_, reason_value, loser) := function_parameter in
          Loser
            {| game_result.Loser.reason := reason_value;
              game_result.Loser.loser := loser; |});
      Data_encoding.case_value "Draw" None (Data_encoding.Tag 1)
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "draw")))
        (fun (function_parameter : game_result) ⇒
          match function_parameter with
          | DrawSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Draw)
    ].

Inductive status : Set :=
| Ongoing : status
| Ended : game_result status.

Definition pp_status (ppf : Format.formatter) (status : status) : unit :=
  match status with
  | Ongoing
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Game ongoing"
          CamlinternalFormatBasics.End_of_format) "Game ongoing")
  | Ended game_result
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Game ended: "
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
        "Game ended: %a") pp_game_result game_result
  end.

Definition status_encoding : Data_encoding.encoding status :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Ongoing" None (Data_encoding.Tag 0)
        (Data_encoding.constant "ongoing")
        (fun (function_parameter : status) ⇒
          match function_parameter with
          | OngoingSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Ongoing);
      Data_encoding.case_value "Ended" None (Data_encoding.Tag 1)
        (Data_encoding.obj1
          (Data_encoding.req None None "result" game_result_encoding))
        (fun (function_parameter : status) ⇒
          match function_parameter with
          | Ended r_valueSome r_value
          | _None
          end) (fun (r_value : game_result) ⇒ Ended r_value)
    ].

#[bypass_check(guard)]
Definition find_choice
  (dissection : list dissection_chunk) (tick : Sc_rollup_tick_repr.t)
  : M? (dissection_chunk × dissection_chunk) :=
  let fix traverse (states : list dissection_chunk) {struct states}
    : M? (dissection_chunk × dissection_chunk) :=
    match states with
    |
      cons
        ({|
          Sc_rollup_dissection_chunk_repr.t.state_hash := _;
            Sc_rollup_dissection_chunk_repr.t.tick := state_tick
            |} as curr) (cons next others) ⇒
      if Sc_rollup_tick_repr.op_eq tick state_tick then
        return? (curr, next)
      else
        traverse (cons next others)
    | _
      Error_monad.Result_syntax.tzfail
        (Build_extensible "Dissection_choice_not_found" Sc_rollup_tick_repr.t
          tick)
    end in
  traverse dissection.

Check that the chosen interval is a single tick.
Definition check_proof_distance_is_one
  (start_tick : Sc_rollup_tick_repr.t) (stop_tick : Sc_rollup_tick_repr.t)
  : M? unit :=
  let dist := Sc_rollup_tick_repr.distance start_tick stop_tick in
  Error_monad.error_unless (Z.equal dist Z.one)
    (Build_extensible "Proof_unexpected_section_size" Z.t dist).

Check the proof begins with the correct state.
Check the proof stops with a different state than refuted one.
Definition check_proof_stop_state {A : Set}
  (stop_state : option Sc_rollup_repr.State_hash.t) (input_given : option A)
  (input_request : Sc_rollup_PVM_sig.input_request)
  (proof_value : Sc_rollup_proof_repr.t) (validate : bool) : M? unit :=
  let stop_proof :=
    match (input_given, input_request) with
    |
      ((None, Sc_rollup_PVM_sig.No_input_required) |
      (Some _, Sc_rollup_PVM_sig.Initial) |
      (Some _, Sc_rollup_PVM_sig.First_after _ _) |
      (Some _, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒
      Some (Sc_rollup_proof_repr.stop proof_value)
    |
      ((Some _, Sc_rollup_PVM_sig.No_input_required) |
      (None, Sc_rollup_PVM_sig.Initial) |
      (None, Sc_rollup_PVM_sig.First_after _ _) |
      (None, Sc_rollup_PVM_sig.Needs_reveal _)) ⇒ None
    end in
  Error_monad.error_unless
    (let b_value :=
      Option.equal Sc_rollup_repr.State_hash.equal stop_state stop_proof in
    if validate then
      b_value
    else
      Pervasives.not b_value)
    (if validate then
      Build_extensible "Proof_stop_state_hash_failed_to_validate"
        Proof_stop_state_hash_failed_to_validate
        {|
          Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
            stop_state;
          Proof_stop_state_hash_failed_to_validate.stop_proof := stop_proof; |}
    else
      Build_extensible "Proof_stop_state_hash_failed_to_refute"
        Proof_stop_state_hash_failed_to_refute
        {| Proof_stop_state_hash_failed_to_refute.stop_state_hash := stop_state;
          Proof_stop_state_hash_failed_to_refute.stop_proof := stop_proof; |}).

Check the proof validates the stop state.
Check the proof refutes the stop state.
Returns the validity of the first final move on top of a dissection.
Definition validity_final_move
  (dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
  (first_move : bool) (metadata : Sc_rollup_metadata_repr.t)
  (proof_value : Sc_rollup_proof_repr.t) (game : t)
  (start_chunk : dissection_chunk) (stop_chunk : dissection_chunk) : bool :=
  let res :=
    let '{|
      V1.t.inbox_snapshot := inbox_snapshot;
        V1.t.dal_snapshot := dal_snapshot;
        V1.t.inbox_level := inbox_level;
        V1.t.pvm_name := pvm_name
        |} := game in
    let valid :=
      Sc_rollup_proof_repr.valid metadata inbox_snapshot inbox_level
        dal_snapshot dal_parameters dal_attestation_lag pvm_name proof_value in
    let? '_ :=
      if first_move then
        check_proof_distance_is_one
          start_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
          stop_chunk.(Sc_rollup_dissection_chunk_repr.t.tick)
      else
        return? tt in
    let? '_ :=
      check_proof_start_state
        start_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) proof_value
      in
    match valid with
    | Pervasives.Ok (input, input_request)
      let? '_ :=
        if first_move then
          check_proof_refute_stop_state
            stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
            input_request proof_value
        else
          check_proof_validate_stop_state
            stop_chunk.(Sc_rollup_dissection_chunk_repr.t.state_hash) input
            input_request proof_value in
      Error_monad.Lwt_result_syntax.return_true
    | _Error_monad.Lwt_result_syntax.return_false
    end in
  Result.value_value res false.

Returns the validity of the first final move on top of a dissection.
It is valid if and only: The distance of the refuted dissection is [1]. The proof start on the agreed start state. The proof stop on the state different than the refuted one. The proof is correctly verified.
Returns the validity of the second final move.
It is valid if and only: The proof start on the agreed start state. The proof stop on the state validates the refuted one. The proof is correctly verified.
Definition validity_second_final_move
  (dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
  (metadata : Sc_rollup_metadata_repr.t) (agreed_start_chunk : dissection_chunk)
  (refuted_stop_chunk : dissection_chunk) (game : t)
  (proof_value : Sc_rollup_proof_repr.t) : bool :=
  validity_final_move dal_parameters dal_attestation_lag false metadata
    proof_value game agreed_start_chunk refuted_stop_chunk.

Definition loser_of_results (alice_result : bool) (bob_result : bool)
  : option player :=
  match (alice_result, bob_result) with
  | (true, true)None
  | (false, false)None
  | (false, true)Some Alice
  | (true, false)Some Bob
  end.

Definition play
  (dal_parameters : Dal_slot_repr.parameters) (dal_attestation_lag : int)
  (stakers : Index.t) (metadata : Sc_rollup_metadata_repr.t) (game : t)
  (refutation : refutation) : M? (Either.t game_result t) :=
  let mk_loser {A : Set} (loser : player) : Either.t game_result A :=
    let loser := Index.staker stakers loser in
    Either.Left
      (Loser
        {| game_result.Loser.reason := Conflict_resolved;
          game_result.Loser.loser := loser; |}) in
  match (refutation.(refutation.step), game.(V1.t.game_state)) with
  |
    (Dissection states,
      V1.Dissecting {|
        game_state.Dissecting.dissection := dissection;
          game_state.Dissecting.default_number_of_sections :=
            default_number_of_sections
          |})
    let? '(start_chunk, stop_chunk) :=
      find_choice dissection refutation.(refutation.choice) in
    let? '_ :=
      Sc_rollup_dissection_chunk_repr.default_check default_number_of_sections
        start_chunk stop_chunk states in
    let new_game_state :=
      V1.Dissecting
        {| game_state.Dissecting.dissection := states;
          game_state.Dissecting.default_number_of_sections :=
            default_number_of_sections; |} in
    return?
      (Either.Right
        {| V1.t.turn := opponent game.(V1.t.turn);
          V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
          V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
          V1.t.start_level := game.(V1.t.start_level);
          V1.t.inbox_level := game.(V1.t.inbox_level);
          V1.t.pvm_name := game.(V1.t.pvm_name);
          V1.t.game_state := new_game_state; |})
  | (Dissection _, V1.Final_move _)
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Dissecting_during_final_move" unit tt)
  |
    (Proof proof_value,
      V1.Dissecting {|
        game_state.Dissecting.dissection := dissection;
          game_state.Dissecting.default_number_of_sections := _
          |})
    let? '(start_chunk, stop_chunk) :=
      find_choice dissection refutation.(refutation.choice) in
    let player_result :=
      validity_first_final_move dal_parameters dal_attestation_lag metadata
        proof_value game start_chunk stop_chunk in
    if player_result then
      return? (mk_loser (opponent game.(V1.t.turn)))
    else
      let new_game_state :=
        let agreed_start_chunk := start_chunk in
        let refuted_stop_chunk := stop_chunk in
        V1.Final_move
          {| game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
            game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk; |}
        in
      return?
        (Either.Right
          {| V1.t.turn := opponent game.(V1.t.turn);
            V1.t.inbox_snapshot := game.(V1.t.inbox_snapshot);
            V1.t.dal_snapshot := game.(V1.t.dal_snapshot);
            V1.t.start_level := game.(V1.t.start_level);
            V1.t.inbox_level := game.(V1.t.inbox_level);
            V1.t.pvm_name := game.(V1.t.pvm_name);
            V1.t.game_state := new_game_state; |})
  |
    (Proof proof_value,
      V1.Final_move {|
        game_state.Final_move.agreed_start_chunk := agreed_start_chunk;
          game_state.Final_move.refuted_stop_chunk := refuted_stop_chunk
          |})
    let player_result :=
      validity_second_final_move dal_parameters dal_attestation_lag metadata
        agreed_start_chunk refuted_stop_chunk game proof_value in
    if player_result then
      return? (mk_loser (opponent game.(V1.t.turn)))
    else
      return? (Either.Left Draw)
  end.

Module timeout.
  Record record : Set := Build {
    alice : int;
    bob : int;
    last_turn_level : Raw_level_repr.t;
  }.
  Definition with_alice alice (r : record) :=
    Build alice r.(bob) r.(last_turn_level).
  Definition with_bob bob (r : record) :=
    Build r.(alice) bob r.(last_turn_level).
  Definition with_last_turn_level last_turn_level (r : record) :=
    Build r.(alice) r.(bob) last_turn_level.
End timeout.
Definition timeout := timeout.record.

Definition timeout_encoding : Data_encoding.encoding timeout :=
  Data_encoding.conv
    (fun (function_parameter : timeout) ⇒
      let '{|
        timeout.alice := alice;
          timeout.bob := bob;
          timeout.last_turn_level := last_turn_level
          |} := function_parameter in
      (alice, bob, last_turn_level))
    (fun (function_parameter : int × int × Raw_level_repr.t) ⇒
      let '(alice, bob, last_turn_level) := function_parameter in
      {| timeout.alice := alice; timeout.bob := bob;
        timeout.last_turn_level := last_turn_level; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "alice" Data_encoding.int31)
      (Data_encoding.req None None "bob" Data_encoding.int31)
      (Data_encoding.req None None "last_turn_level" Raw_level_repr.encoding)).