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.V7.
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_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_proof_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.

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

Module V1.
  Module dissection_chunk.
    Record record : Set := Build {
      state_hash : option Sc_rollup_repr.State_hash.t;
      tick : Sc_rollup_tick_repr.t;
    }.
    Definition with_state_hash state_hash (r : record) :=
      Build state_hash r.(tick).
    Definition with_tick tick (r : record) :=
      Build r.(state_hash) tick.
  End dissection_chunk.
  Definition dissection_chunk := dissection_chunk.record.

  Definition pp_state_hash
    : Format.formatter option Sc_rollup_repr.State_hash.t unit :=
    Format.pp_print_option
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "None"
                  CamlinternalFormatBasics.End_of_format) "None")))
      Sc_rollup_repr.State_hash.pp.

  Definition pp_dissection_chunk
    (ppf : Format.formatter) (function_parameter : dissection_chunk) : unit :=
    let '{|
      dissection_chunk.state_hash := state_hash;
        dissection_chunk.tick := tick
        |} := function_parameter in
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "State hash:"
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@ " 1 0)
              (CamlinternalFormatBasics.String_literal "Tick: "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format)))))
        "State hash:%a@ Tick: %a") pp_state_hash state_hash
      Sc_rollup_tick_repr.pp tick.

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;
      level : Raw_level_repr.t;
      pvm_name : string;
      game_state : game_state;
    }.
    Definition with_turn turn (r : record) :=
      Build turn r.(inbox_snapshot) r.(level) r.(pvm_name) r.(game_state).
    Definition with_inbox_snapshot inbox_snapshot (r : record) :=
      Build r.(turn) inbox_snapshot r.(level) r.(pvm_name) r.(game_state).
    Definition with_level level (r : record) :=
      Build r.(turn) r.(inbox_snapshot) level r.(pvm_name) r.(game_state).
    Definition with_pvm_name pvm_name (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(level) pvm_name r.(game_state).
    Definition with_game_state game_state (r : record) :=
      Build r.(turn) r.(inbox_snapshot) r.(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 dissection_chunk_equal (function_parameter : dissection_chunk)
    : dissection_chunk bool :=
    let '{|
      dissection_chunk.state_hash := state_hash;
        dissection_chunk.tick := tick
        |} := function_parameter in
    fun (chunk2 : dissection_chunk) ⇒
      (Option.equal Sc_rollup_repr.State_hash.equal state_hash
        chunk2.(dissection_chunk.state_hash)) &&
      (Sc_rollup_tick_repr.equal tick chunk2.(dissection_chunk.tick)).

  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 dissection_chunk_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
            |})
      (dissection_chunk_equal agreed_start_chunk1 agreed_start_chunk2) &&
      (dissection_chunk_equal refuted_stop_chunk1 refuted_stop_chunk2)
    | (Final_move _, _)false
    end.

  Definition equal (function_parameter : t) : t bool :=
    let '{|
      t.turn := turn1;
        t.inbox_snapshot := inbox_snapshot1;
        t.level := level1;
        t.pvm_name := pvm_name1;
        t.game_state := game_state1
        |} := function_parameter in
    fun (function_parameter : t) ⇒
      let '{|
        t.turn := turn2;
          t.inbox_snapshot := inbox_snapshot2;
          t.level := level2;
          t.pvm_name := pvm_name2;
          t.game_state := game_state2
          |} := function_parameter in
      (player_equal turn1 turn2) &&
      ((Sc_rollup_inbox_repr.equal_history_proof inbox_snapshot1 inbox_snapshot2)
      &&
      ((Raw_level_repr.equal level1 level2) &&
      ((String.equal pvm_name1 pvm_name2) &&
      (game_state_equal game_state1 game_state2)))).

  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.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.End_of_format) "%s")
      (string_of_player player_value).

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

  Definition dissection_chunk_encoding
    : Data_encoding.encoding dissection_chunk :=
    Data_encoding.conv
      (fun (function_parameter : dissection_chunk) ⇒
        let '{|
          dissection_chunk.state_hash := state_hash;
            dissection_chunk.tick := tick
            |} := function_parameter in
        (state_hash, tick))
      (fun (function_parameter :
        option Sc_rollup_repr.State_hash.t × Sc_rollup_tick_repr.t) ⇒
        let '(state_hash, tick) := function_parameter in
        {| dissection_chunk.state_hash := state_hash;
          dissection_chunk.tick := tick; |}) None
      (Data_encoding.obj2
        (Data_encoding.opt None None "state" Sc_rollup_repr.State_hash.encoding)
        (Data_encoding.req None None "tick" Sc_rollup_tick_repr.encoding)).

  Definition dissection_encoding
    : Data_encoding.encoding (list dissection_chunk) :=
    Data_encoding.list_value None dissection_chunk_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 dissection_chunk × 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"
              dissection_chunk_encoding)
            (Data_encoding.req None None "refuted_stop_chunk"
              dissection_chunk_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 × dissection_chunk × dissection_chunk) ⇒
            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.level := level;
            t.pvm_name := pvm_name;
            t.game_state := game_state
            |} := function_parameter in
        (turn, inbox_snapshot, level, pvm_name, game_state))
      (fun (function_parameter :
        player × Sc_rollup_inbox_repr.history_proof × Raw_level_repr.t × string
          × game_state) ⇒
        let '(turn, inbox_snapshot, level, pvm_name, game_state) :=
          function_parameter in
        {| t.turn := turn; t.inbox_snapshot := inbox_snapshot; t.level := level;
          t.pvm_name := pvm_name; t.game_state := game_state; |}) None
      (Data_encoding.obj5 (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 "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 dissection_chunk) : 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" "")))
      pp_dissection_chunk 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")
        pp_dissection_chunk agreed_start_chunk pp_dissection_chunk
        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 "; 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; 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.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 :=
  {| V1.dissection_chunk.state_hash := state_hash;
    V1.dissection_chunk.tick := tick; |}.

Definition initial
  (inbox_value : Sc_rollup_inbox_repr.history_proof) (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 :=
          if Sc_rollup_tick_repr.equal tick Sc_rollup_tick_repr.initial then
            [
              make_chunk
                (Some
                  child.(Sc_rollup_commitment_repr.V1.t.compressed_state))
                Sc_rollup_tick_repr.initial;
              make_chunk None
                (Sc_rollup_tick_repr.next Sc_rollup_tick_repr.initial)
            ]
          else
            [
              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.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 '{|
            V1.dissection_chunk.state_hash := state_hash;
              V1.dissection_chunk.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)).

Records for the constructor parameters
Module ConstructorRecords_invalid_move.
  Module invalid_move.
    Module Dissection_number_of_sections_mismatch.
      Record record {expected given : Set} : Set := Build {
        expected : expected;
        given : given;
      }.
      Arguments record : clear implicits.
      Definition with_expected {t_expected t_given} expected
        (r : record t_expected t_given) :=
        Build t_expected t_given expected r.(given).
      Definition with_given {t_expected t_given} given
        (r : record t_expected t_given) :=
        Build t_expected t_given r.(expected) given.
    End Dissection_number_of_sections_mismatch.
    Definition Dissection_number_of_sections_mismatch_skeleton :=
      Dissection_number_of_sections_mismatch.record.

    Module Dissection_start_hash_mismatch.
      Record record {expected given : Set} : Set := Build {
        expected : expected;
        given : given;
      }.
      Arguments record : clear implicits.
      Definition with_expected {t_expected t_given} expected
        (r : record t_expected t_given) :=
        Build t_expected t_given expected r.(given).
      Definition with_given {t_expected t_given} given
        (r : record t_expected t_given) :=
        Build t_expected t_given r.(expected) given.
    End Dissection_start_hash_mismatch.
    Definition Dissection_start_hash_mismatch_skeleton :=
      Dissection_start_hash_mismatch.record.

    Module Dissection_edge_ticks_mismatch.
      Record record {dissection_start_tick dissection_stop_tick chunk_start_tick
        chunk_stop_tick : Set} : Set := Build {
        dissection_start_tick : dissection_start_tick;
        dissection_stop_tick : dissection_stop_tick;
        chunk_start_tick : chunk_start_tick;
        chunk_stop_tick : chunk_stop_tick;
      }.
      Arguments record : clear implicits.
      Definition with_dissection_start_tick
        {t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick} dissection_start_tick
        (r :
          record t_dissection_start_tick t_dissection_stop_tick
            t_chunk_start_tick t_chunk_stop_tick) :=
        Build t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick dissection_start_tick r.(dissection_stop_tick)
          r.(chunk_start_tick) r.(chunk_stop_tick).
      Definition with_dissection_stop_tick
        {t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick} dissection_stop_tick
        (r :
          record t_dissection_start_tick t_dissection_stop_tick
            t_chunk_start_tick t_chunk_stop_tick) :=
        Build t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick r.(dissection_start_tick) dissection_stop_tick
          r.(chunk_start_tick) r.(chunk_stop_tick).
      Definition with_chunk_start_tick
        {t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick} chunk_start_tick
        (r :
          record t_dissection_start_tick t_dissection_stop_tick
            t_chunk_start_tick t_chunk_stop_tick) :=
        Build t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick r.(dissection_start_tick) r.(dissection_stop_tick)
          chunk_start_tick r.(chunk_stop_tick).
      Definition with_chunk_stop_tick
        {t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick} chunk_stop_tick
        (r :
          record t_dissection_start_tick t_dissection_stop_tick
            t_chunk_start_tick t_chunk_stop_tick) :=
        Build t_dissection_start_tick t_dissection_stop_tick t_chunk_start_tick
          t_chunk_stop_tick r.(dissection_start_tick) r.(dissection_stop_tick)
          r.(chunk_start_tick) chunk_stop_tick.
    End Dissection_edge_ticks_mismatch.
    Definition Dissection_edge_ticks_mismatch_skeleton :=
      Dissection_edge_ticks_mismatch.record.

    Module Proof_start_state_hash_mismatch.
      Record record {start_state_hash start_proof : Set} : Set := Build {
        start_state_hash : start_state_hash;
        start_proof : start_proof;
      }.
      Arguments record : clear implicits.
      Definition with_start_state_hash {t_start_state_hash t_start_proof}
        start_state_hash (r : record t_start_state_hash t_start_proof) :=
        Build t_start_state_hash t_start_proof start_state_hash r.(start_proof).
      Definition with_start_proof {t_start_state_hash t_start_proof} start_proof
        (r : record t_start_state_hash t_start_proof) :=
        Build t_start_state_hash t_start_proof r.(start_state_hash) start_proof.
    End Proof_start_state_hash_mismatch.
    Definition Proof_start_state_hash_mismatch_skeleton :=
      Proof_start_state_hash_mismatch.record.

    Module Proof_stop_state_hash_failed_to_refute.
      Record record {stop_state_hash stop_proof : Set} : Set := Build {
        stop_state_hash : stop_state_hash;
        stop_proof : stop_proof;
      }.
      Arguments record : clear implicits.
      Definition with_stop_state_hash {t_stop_state_hash t_stop_proof}
        stop_state_hash (r : record t_stop_state_hash t_stop_proof) :=
        Build t_stop_state_hash t_stop_proof stop_state_hash r.(stop_proof).
      Definition with_stop_proof {t_stop_state_hash t_stop_proof} stop_proof
        (r : record t_stop_state_hash t_stop_proof) :=
        Build t_stop_state_hash t_stop_proof r.(stop_state_hash) stop_proof.
    End Proof_stop_state_hash_failed_to_refute.
    Definition Proof_stop_state_hash_failed_to_refute_skeleton :=
      Proof_stop_state_hash_failed_to_refute.record.

    Module Proof_stop_state_hash_failed_to_validate.
      Record record {stop_state_hash stop_proof : Set} : Set := Build {
        stop_state_hash : stop_state_hash;
        stop_proof : stop_proof;
      }.
      Arguments record : clear implicits.
      Definition with_stop_state_hash {t_stop_state_hash t_stop_proof}
        stop_state_hash (r : record t_stop_state_hash t_stop_proof) :=
        Build t_stop_state_hash t_stop_proof stop_state_hash r.(stop_proof).
      Definition with_stop_proof {t_stop_state_hash t_stop_proof} stop_proof
        (r : record t_stop_state_hash t_stop_proof) :=
        Build t_stop_state_hash t_stop_proof r.(stop_state_hash) stop_proof.
    End Proof_stop_state_hash_failed_to_validate.
    Definition Proof_stop_state_hash_failed_to_validate_skeleton :=
      Proof_stop_state_hash_failed_to_validate.record.
  End invalid_move.
End ConstructorRecords_invalid_move.
Import ConstructorRecords_invalid_move.

Reserved Notation "'invalid_move.Dissection_number_of_sections_mismatch".
Reserved Notation "'invalid_move.Dissection_start_hash_mismatch".
Reserved Notation "'invalid_move.Dissection_edge_ticks_mismatch".
Reserved Notation "'invalid_move.Proof_start_state_hash_mismatch".
Reserved Notation "'invalid_move.Proof_stop_state_hash_failed_to_refute".
Reserved Notation "'invalid_move.Proof_stop_state_hash_failed_to_validate".

Inductive invalid_move : Set :=
| Dissection_choice_not_found : Sc_rollup_tick_repr.t invalid_move
| Dissection_number_of_sections_mismatch :
  'invalid_move.Dissection_number_of_sections_mismatch invalid_move
| Dissection_invalid_number_of_sections : Z.t invalid_move
| Dissection_start_hash_mismatch :
  'invalid_move.Dissection_start_hash_mismatch invalid_move
| Dissection_stop_hash_mismatch :
  option Sc_rollup_repr.State_hash.t invalid_move
| Dissection_edge_ticks_mismatch :
  'invalid_move.Dissection_edge_ticks_mismatch invalid_move
| Dissection_ticks_not_increasing : invalid_move
| Dissection_invalid_distribution : invalid_move
| Dissection_invalid_successive_states_shape : invalid_move
| Proof_unexpected_section_size : Z.t invalid_move
| Proof_start_state_hash_mismatch :
  'invalid_move.Proof_start_state_hash_mismatch invalid_move
| Proof_stop_state_hash_failed_to_refute :
  'invalid_move.Proof_stop_state_hash_failed_to_refute invalid_move
| Proof_stop_state_hash_failed_to_validate :
  'invalid_move.Proof_stop_state_hash_failed_to_validate invalid_move
| Proof_invalid : string invalid_move

where "'invalid_move.Dissection_number_of_sections_mismatch" :=
  (invalid_move.Dissection_number_of_sections_mismatch_skeleton Z.t Z.t)
and "'invalid_move.Dissection_start_hash_mismatch" :=
  (invalid_move.Dissection_start_hash_mismatch_skeleton
    (option Sc_rollup_repr.State_hash.t) (option Sc_rollup_repr.State_hash.t))
and "'invalid_move.Dissection_edge_ticks_mismatch" :=
  (invalid_move.Dissection_edge_ticks_mismatch_skeleton Sc_rollup_tick_repr.t
    Sc_rollup_tick_repr.t Sc_rollup_tick_repr.t Sc_rollup_tick_repr.t)
and "'invalid_move.Proof_start_state_hash_mismatch" :=
  (invalid_move.Proof_start_state_hash_mismatch_skeleton
    (option Sc_rollup_repr.State_hash.t) Sc_rollup_repr.State_hash.t)
and "'invalid_move.Proof_stop_state_hash_failed_to_refute" :=
  (invalid_move.Proof_stop_state_hash_failed_to_refute_skeleton
    (option Sc_rollup_repr.State_hash.t) (option Sc_rollup_repr.State_hash.t))
and "'invalid_move.Proof_stop_state_hash_failed_to_validate" :=
  (invalid_move.Proof_stop_state_hash_failed_to_validate_skeleton
    (option Sc_rollup_repr.State_hash.t) (option Sc_rollup_repr.State_hash.t)).

Module invalid_move.
  Include ConstructorRecords_invalid_move.invalid_move.
  Definition Dissection_number_of_sections_mismatch :=
    'invalid_move.Dissection_number_of_sections_mismatch.
  Definition Dissection_start_hash_mismatch :=
    'invalid_move.Dissection_start_hash_mismatch.
  Definition Dissection_edge_ticks_mismatch :=
    'invalid_move.Dissection_edge_ticks_mismatch.
  Definition Proof_start_state_hash_mismatch :=
    'invalid_move.Proof_start_state_hash_mismatch.
  Definition Proof_stop_state_hash_failed_to_refute :=
    'invalid_move.Proof_stop_state_hash_failed_to_refute.
  Definition Proof_stop_state_hash_failed_to_validate :=
    'invalid_move.Proof_stop_state_hash_failed_to_validate.
End invalid_move.

Definition pp_invalid_move (fmt : Format.formatter) : invalid_move unit :=
  let 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 in
  fun (function_parameter : invalid_move) ⇒
    match function_parameter with
    | Dissection_choice_not_found tick
      Format.fprintf fmt
        (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 tick
    |
      Dissection_number_of_sections_mismatch {|
        invalid_move.Dissection_number_of_sections_mismatch.expected := expected;
          invalid_move.Dissection_number_of_sections_mismatch.given := given
          |} ⇒
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "The number of sections must be equal to "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal " instead of "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format))))
          "The number of sections must be equal to %a instead of %a") Z.pp_print
        expected Z.pp_print given
    | Dissection_invalid_number_of_sections n_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "A dissection with "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal
                " sections can never be valid"
                CamlinternalFormatBasics.End_of_format)))
          "A dissection with %a sections can never be valid") Z.pp_print n_value
    |
      Dissection_start_hash_mismatch {|
        invalid_move.Dissection_start_hash_mismatch.given := None |} ⇒
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "The start hash must not be None"
            CamlinternalFormatBasics.End_of_format)
          "The start hash must not be None")
    |
      Dissection_start_hash_mismatch {|
        invalid_move.Dissection_start_hash_mismatch.expected := expected;
          invalid_move.Dissection_start_hash_mismatch.given := given
          |} ⇒
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "The start hash should be equal to "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal
                ", but the provided hash is "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format))))
          "The start hash should be equal to %a, but the provided hash is %a")
        pp_hash_opt expected pp_hash_opt given
    | Dissection_stop_hash_mismatch h_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "The stop hash should not be equal to "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))
          "The stop hash should not be equal to %a") pp_hash_opt h_value
    |
      Dissection_edge_ticks_mismatch {|
        invalid_move.Dissection_edge_ticks_mismatch.dissection_start_tick :=
          dissection_start_tick;
          invalid_move.Dissection_edge_ticks_mismatch.dissection_stop_tick :=
            dissection_stop_tick;
          invalid_move.Dissection_edge_ticks_mismatch.chunk_start_tick :=
            chunk_start_tick;
          invalid_move.Dissection_edge_ticks_mismatch.chunk_stop_tick :=
            chunk_stop_tick
          |} ⇒
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "We should have dissection_start_tick("
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal ") = "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " and dissection_stop_tick("
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal ") = "
                        (CamlinternalFormatBasics.Alpha
                          CamlinternalFormatBasics.End_of_format))))))))
          "We should have dissection_start_tick(%a) = %a and dissection_stop_tick(%a) = %a")
        Sc_rollup_tick_repr.pp dissection_start_tick Sc_rollup_tick_repr.pp
        chunk_start_tick Sc_rollup_tick_repr.pp dissection_stop_tick
        Sc_rollup_tick_repr.pp chunk_stop_tick
    | Dissection_ticks_not_increasing
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Ticks should only increase in dissection"
            CamlinternalFormatBasics.End_of_format)
          "Ticks should only increase in dissection")
    | Dissection_invalid_successive_states_shape
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Cannot return to a Some state after being at a None state"
            CamlinternalFormatBasics.End_of_format)
          "Cannot return to a Some state after being at a None state")
    | Dissection_invalid_distribution
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Maximum tick increment in a section cannot be more than half total dissection length"
            CamlinternalFormatBasics.End_of_format)
          "Maximum tick increment in a section cannot be more than half total dissection length")
    | Proof_unexpected_section_size n_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "dist should be equal to 1 in a proof, but got "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))
          "dist should be equal to 1 in a proof, but got %a") Z.pp_print n_value
    |
      Proof_start_state_hash_mismatch {|
        invalid_move.Proof_start_state_hash_mismatch.start_state_hash :=
          start_state_hash;
          invalid_move.Proof_start_state_hash_mismatch.start_proof :=
            start_proof
          |} ⇒
      Format.fprintf fmt
        (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
    |
      Proof_stop_state_hash_failed_to_refute {|
        invalid_move.Proof_stop_state_hash_failed_to_refute.stop_state_hash :=
          stop_state_hash;
          invalid_move.Proof_stop_state_hash_failed_to_refute.stop_proof :=
            stop_proof
          |} ⇒
      Format.fprintf fmt
        (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
    |
      Proof_stop_state_hash_failed_to_validate {|
        invalid_move.Proof_stop_state_hash_failed_to_validate.stop_state_hash :=
          stop_state_hash;
          invalid_move.Proof_stop_state_hash_failed_to_validate.stop_proof :=
            stop_proof
          |} ⇒
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Trying to validate "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal
                ", the stop_proof must be equal to "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format))))
          "Trying to validate %a, the stop_proof must be equal to %a")
        pp_hash_opt stop_state_hash pp_hash_opt stop_proof
    | Proof_invalid s_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Invalid proof: "
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.End_of_format)) "Invalid proof: %s")
        s_value
    end.

Definition invalid_move_encoding : Data_encoding.encoding invalid_move :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "sc_rollup_dissection_choice_not_found" None
        (Data_encoding.Tag 0)
        (Data_encoding.obj2
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_choice_not_found"))
          (Data_encoding.req None None "tick" Sc_rollup_tick_repr.encoding))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_choice_not_found tickSome (tt, tick)
          | _None
          end)
        (fun (function_parameter : unit × Sc_rollup_tick_repr.t) ⇒
          let '(_, tick) := function_parameter in
          Dissection_choice_not_found tick);
      Data_encoding.case_value
        "sc_rollup_dissection_number_of_sections_mismatch" None
        (Data_encoding.Tag 1)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              "dissection_number_of_sections_mismatch"))
          (Data_encoding.req None None "expected" Data_encoding.n_value)
          (Data_encoding.req None None "given" Data_encoding.n_value))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          |
            Dissection_number_of_sections_mismatch {|
              invalid_move.Dissection_number_of_sections_mismatch.expected := expected;
                invalid_move.Dissection_number_of_sections_mismatch.given
                  := given
                |} ⇒ Some (tt, expected, given)
          | _None
          end)
        (fun (function_parameter : unit × Z.t × Z.t) ⇒
          let '(_, expected, given) := function_parameter in
          Dissection_number_of_sections_mismatch
            {|
              invalid_move.Dissection_number_of_sections_mismatch.expected
                := expected;
              invalid_move.Dissection_number_of_sections_mismatch.given
                := given; |});
      Data_encoding.case_value "sc_rollup_dissection_invalid_number_of_sections"
        None (Data_encoding.Tag 2)
        (Data_encoding.obj2
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              "dissection_invalid_number_of_sections"))
          (Data_encoding.req None None "value" Data_encoding.n_value))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_invalid_number_of_sections value_value
            Some (tt, value_value)
          | _None
          end)
        (fun (function_parameter : unit × Z.t) ⇒
          let '(_, value_value) := function_parameter in
          Dissection_invalid_number_of_sections value_value);
      Data_encoding.case_value "sc_rollup_dissection_unexpected_start_hash" None
        (Data_encoding.Tag 3)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_unexpected_start_hash"))
          (Data_encoding.req None None "expected"
            (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding))
          (Data_encoding.req None None "given"
            (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          |
            Dissection_start_hash_mismatch {|
              invalid_move.Dissection_start_hash_mismatch.expected := expected;
                invalid_move.Dissection_start_hash_mismatch.given :=
                  given
                |} ⇒ Some (tt, expected, given)
          | _None
          end)
        (fun (function_parameter :
          unit × option Sc_rollup_repr.State_hash.t ×
            option Sc_rollup_repr.State_hash.t) ⇒
          let '(_, expected, given) := function_parameter in
          Dissection_start_hash_mismatch
            {|
              invalid_move.Dissection_start_hash_mismatch.expected :=
                expected;
              invalid_move.Dissection_start_hash_mismatch.given :=
                given; |});
      Data_encoding.case_value "sc_rollup_dissection_stop_hash_mismatch" None
        (Data_encoding.Tag 4)
        (Data_encoding.obj2
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_stop_hash_mismatch"))
          (Data_encoding.req None None "hash"
            (Data_encoding.option_value Sc_rollup_repr.State_hash.encoding)))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_stop_hash_mismatch hoptSome (tt, hopt)
          | _None
          end)
        (fun (function_parameter : unit × option Sc_rollup_repr.State_hash.t)
          ⇒
          let '(_, hopt) := function_parameter in
          Dissection_stop_hash_mismatch hopt);
      Data_encoding.case_value "sc_rollup_dissection_edge_ticks_mismatch" None
        (Data_encoding.Tag 5)
        (Data_encoding.obj5
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_edge_ticks_mismatch"))
          (Data_encoding.req None None "dissection_start_tick"
            Sc_rollup_tick_repr.encoding)
          (Data_encoding.req None None "dissection_stop_tick"
            Sc_rollup_tick_repr.encoding)
          (Data_encoding.req None None "chunk_start_tick"
            Sc_rollup_tick_repr.encoding)
          (Data_encoding.req None None "chunk_stop_tick"
            Sc_rollup_tick_repr.encoding))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_edge_ticks_mismatch e_value
            Some
              (tt,
                e_value.(invalid_move.Dissection_edge_ticks_mismatch.dissection_start_tick),
                e_value.(invalid_move.Dissection_edge_ticks_mismatch.dissection_stop_tick),
                e_value.(invalid_move.Dissection_edge_ticks_mismatch.chunk_start_tick),
                e_value.(invalid_move.Dissection_edge_ticks_mismatch.chunk_stop_tick))
          | _None
          end)
        (fun (function_parameter :
          unit × Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t ×
            Sc_rollup_tick_repr.t × Sc_rollup_tick_repr.t) ⇒
          let
            '(_, dissection_start_tick, dissection_stop_tick,
              chunk_start_tick, chunk_stop_tick) := function_parameter
            in
          Dissection_edge_ticks_mismatch
            {|
              invalid_move.Dissection_edge_ticks_mismatch.dissection_start_tick
                := dissection_start_tick;
              invalid_move.Dissection_edge_ticks_mismatch.dissection_stop_tick
                := dissection_stop_tick;
              invalid_move.Dissection_edge_ticks_mismatch.chunk_start_tick
                := chunk_start_tick;
              invalid_move.Dissection_edge_ticks_mismatch.chunk_stop_tick
                := chunk_stop_tick; |});
      Data_encoding.case_value "sc_rollup_dissection_ticks_not_increasing" None
        (Data_encoding.Tag 6)
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_ticks_not_increasing")))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_ticks_not_increasingSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Dissection_ticks_not_increasing);
      Data_encoding.case_value "sc_rollup_dissection_invalid_distribution" None
        (Data_encoding.Tag 7)
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "dissection_invalid_distribution")))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_invalid_distributionSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Dissection_invalid_distribution);
      Data_encoding.case_value
        "sc_rollup_dissection_invalid_successive_states_shape" None
        (Data_encoding.Tag 8)
        (Data_encoding.obj1
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              "dissection_invalid_successive_states_shape")))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Dissection_invalid_successive_states_shapeSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Dissection_invalid_successive_states_shape);
      Data_encoding.case_value "sc_rollup_proof_unexpected_section_size" None
        (Data_encoding.Tag 9)
        (Data_encoding.obj2
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "proof_unexpected_section_size"))
          (Data_encoding.req None None "value" Data_encoding.n_value))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Proof_unexpected_section_size n_valueSome (tt, n_value)
          | _None
          end)
        (fun (function_parameter : unit × Z.t) ⇒
          let '(_, n_value) := function_parameter in
          Proof_unexpected_section_size n_value);
      Data_encoding.case_value "sc_rollup_proof_start_state_hash_mismatch" None
        (Data_encoding.Tag 10)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "proof_start_state_hash_mismatch"))
          (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 : invalid_move) ⇒
          match function_parameter with
          | Proof_start_state_hash_mismatch e_value
            Some
              (tt,
                e_value.(invalid_move.Proof_start_state_hash_mismatch.start_state_hash),
                e_value.(invalid_move.Proof_start_state_hash_mismatch.start_proof))
          | _None
          end)
        (fun (function_parameter :
          unit × option Sc_rollup_repr.State_hash.t ×
            Sc_rollup_repr.State_hash.t) ⇒
          let '(_, start_state_hash, start_proof) := function_parameter in
          Proof_start_state_hash_mismatch
            {|
              invalid_move.Proof_start_state_hash_mismatch.start_state_hash
                := start_state_hash;
              invalid_move.Proof_start_state_hash_mismatch.start_proof
                := start_proof; |});
      Data_encoding.case_value
        "sc_rollup_proof_stop_state_hash_failed_to_refute" None
        (Data_encoding.Tag 11)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              "proof_stop_state_hash_failed_to_refute"))
          (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 : invalid_move) ⇒
          match function_parameter with
          | Proof_stop_state_hash_failed_to_refute e_value
            Some
              (tt,
                e_value.(invalid_move.Proof_stop_state_hash_failed_to_refute.stop_state_hash),
                e_value.(invalid_move.Proof_stop_state_hash_failed_to_refute.stop_proof))
          | _None
          end)
        (fun (function_parameter :
          unit × option Sc_rollup_repr.State_hash.t ×
            option Sc_rollup_repr.State_hash.t) ⇒
          let '(_, stop_state_hash, stop_proof) := function_parameter in
          Proof_stop_state_hash_failed_to_refute
            {|
              invalid_move.Proof_stop_state_hash_failed_to_refute.stop_state_hash
                := stop_state_hash;
              invalid_move.Proof_stop_state_hash_failed_to_refute.stop_proof
                := stop_proof; |});
      Data_encoding.case_value
        "sc_rollup_proof_stop_state_hash_failed_to_validate" None
        (Data_encoding.Tag 12)
        (Data_encoding.obj3
          (Data_encoding.req None None "kind"
            (Data_encoding.constant
              "proof_stop_state_hash_failed_to_validate"))
          (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 : invalid_move) ⇒
          match function_parameter with
          | Proof_stop_state_hash_failed_to_validate e_value
            Some
              (tt,
                e_value.(invalid_move.Proof_stop_state_hash_failed_to_validate.stop_state_hash),
                e_value.(invalid_move.Proof_stop_state_hash_failed_to_validate.stop_proof))
          | _None
          end)
        (fun (function_parameter :
          unit × option Sc_rollup_repr.State_hash.t ×
            option Sc_rollup_repr.State_hash.t) ⇒
          let '(_, stop_state_hash, stop_proof) := function_parameter in
          Proof_stop_state_hash_failed_to_validate
            {|
              invalid_move.Proof_stop_state_hash_failed_to_validate.stop_state_hash
                := stop_state_hash;
              invalid_move.Proof_stop_state_hash_failed_to_validate.stop_proof
                := stop_proof; |});
      Data_encoding.case_value "sc_rollup_proof_invalid" None
        (Data_encoding.Tag 13)
        (Data_encoding.obj2
          (Data_encoding.req None None "kind"
            (Data_encoding.constant "proof_invalid"))
          (Data_encoding.req None None "message" Data_encoding.string_value))
        (fun (function_parameter : invalid_move) ⇒
          match function_parameter with
          | Proof_invalid s_valueSome (tt, s_value)
          | _None
          end)
        (fun (function_parameter : unit × string) ⇒
          let '(_, s_value) := function_parameter in
          Proof_invalid s_value)
    ].

Inductive reason : Set :=
| Conflict_resolved : reason
| Invalid_move : invalid_move 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")
  | Invalid_move mv
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "invalid move("
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Char_literal ")" % char
              CamlinternalFormatBasics.End_of_format))) "invalid move(%a)")
      pp_invalid_move mv
  | 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 "Invalid_move" None (Data_encoding.Tag 1)
        invalid_move_encoding
        (fun (function_parameter : reason) ⇒
          match function_parameter with
          | Invalid_move reason_valueSome reason_value
          | _None
          end) (fun (s_value : invalid_move) ⇒ Invalid_move s_value);
      Data_encoding.case_value "Timeout" None (Data_encoding.Tag 2)
        (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)
    ].

Definition invalid_move_value {A : Set} (reason_value : invalid_move)
  : Pervasives.result A reason :=
  Error_monad.Lwt_result_syntax.fail (Invalid_move reason_value).

#[bypass_check(guard)]
Definition find_choice
  (dissection : list dissection_chunk) (tick : Sc_rollup_tick_repr.t)
  : Pervasives.result (dissection_chunk × dissection_chunk) reason :=
  let fix traverse (states : list dissection_chunk) {struct states}
    : Pervasives.result (dissection_chunk × dissection_chunk) reason :=
    match states with
    |
      cons
        ({|
          V1.dissection_chunk.state_hash := _;
            V1.dissection_chunk.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)
    | _invalid_move_value (Dissection_choice_not_found tick)
    end in
  traverse dissection.

Definition check (pred : bool) (reason_value : invalid_move)
  : Pervasives.result unit reason :=
  if pred then
    return? tt
  else
    invalid_move_value reason_value.

#[bypass_check(guard)]
Definition check_dissection
  (default_number_of_sections : int) (start_chunk : dissection_chunk)
  (stop_chunk : dissection_chunk) (dissection : list dissection_chunk)
  : Pervasives.result unit reason :=
  let len := Z.of_int (List.length dissection) in
  let dist :=
    Sc_rollup_tick_repr.distance start_chunk.(V1.dissection_chunk.tick)
      stop_chunk.(V1.dissection_chunk.tick) in
  let should_be_equal_to (expected : Z.t) : invalid_move :=
    Dissection_number_of_sections_mismatch
      {|
        invalid_move.Dissection_number_of_sections_mismatch.expected :=
          expected;
        invalid_move.Dissection_number_of_sections_mismatch.given := len; |} in
  let num_sections := Z.of_int default_number_of_sections in
  let? '_ :=
    if Z.geq dist num_sections then
      check (Z.equal len num_sections) (should_be_equal_to num_sections)
    else
      if Z.gt dist Z.one then
        check (Z.equal len (Z.succ dist)) (should_be_equal_to (Z.succ dist))
      else
        invalid_move_value (Dissection_invalid_number_of_sections len) in
  let? '_ :=
    match ((List.hd dissection), (List.last_opt dissection)) with
    |
      (Some {|
        V1.dissection_chunk.state_hash := a_value;
          V1.dissection_chunk.tick := a_tick
          |},
        Some {|
          V1.dissection_chunk.state_hash := b_value;
            V1.dissection_chunk.tick := b_tick
            |})
      let? '_ :=
        check
          ((Option.equal Sc_rollup_repr.State_hash.equal a_value
            start_chunk.(V1.dissection_chunk.state_hash)) &&
          (Pervasives.not (Option.is_none a_value)))
          (Dissection_start_hash_mismatch
            {|
              invalid_move.Dissection_start_hash_mismatch.expected :=
                start_chunk.(V1.dissection_chunk.state_hash);
              invalid_move.Dissection_start_hash_mismatch.given := a_value; |})
        in
      let? '_ :=
        check
          (Pervasives.not
            (Option.equal Sc_rollup_repr.State_hash.equal b_value
              stop_chunk.(V1.dissection_chunk.state_hash)))
          (Dissection_stop_hash_mismatch
            stop_chunk.(V1.dissection_chunk.state_hash)) in
      check
        ((Sc_rollup_tick_repr.op_eq a_tick
          start_chunk.(V1.dissection_chunk.tick)) &&
        (Sc_rollup_tick_repr.op_eq b_tick stop_chunk.(V1.dissection_chunk.tick)))
        (Dissection_edge_ticks_mismatch
          {|
            invalid_move.Dissection_edge_ticks_mismatch.dissection_start_tick :=
              a_tick;
            invalid_move.Dissection_edge_ticks_mismatch.dissection_stop_tick :=
              b_tick;
            invalid_move.Dissection_edge_ticks_mismatch.chunk_start_tick :=
              start_chunk.(V1.dissection_chunk.tick);
            invalid_move.Dissection_edge_ticks_mismatch.chunk_stop_tick :=
              stop_chunk.(V1.dissection_chunk.tick); |})
    | _invalid_move_value (Dissection_invalid_number_of_sections len)
    end in
  let half_dist := Z.succ (dist /Z (Z.of_int 2)) in
  let fix traverse (states : list dissection_chunk) {struct states}
    : Pervasives.result unit reason :=
    match states with
    |
      cons {| V1.dissection_chunk.state_hash := None |}
        (cons {| V1.dissection_chunk.state_hash := Some _ |} _) ⇒
      invalid_move_value Dissection_invalid_successive_states_shape
    |
      cons {| V1.dissection_chunk.tick := tick |}
        (cons
          ({|
            V1.dissection_chunk.state_hash := _;
              V1.dissection_chunk.tick := next_tick
              |} as next) others) ⇒
      if Sc_rollup_tick_repr.op_lt tick next_tick then
        let incr := Sc_rollup_tick_repr.distance tick next_tick in
        if Z.leq incr half_dist then
          traverse (cons next others)
        else
          invalid_move_value Dissection_invalid_distribution
      else
        invalid_move_value Dissection_ticks_not_increasing
    | _return? tt
    end in
  traverse dissection.

Check that the chosen interval is a single tick.
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)
  : Pervasives.result unit reason :=
  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
  check
    (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
      Proof_stop_state_hash_failed_to_validate
        {|
          invalid_move.Proof_stop_state_hash_failed_to_validate.stop_state_hash
            := stop_state;
          invalid_move.Proof_stop_state_hash_failed_to_validate.stop_proof :=
            stop_proof; |}
    else
      Proof_stop_state_hash_failed_to_refute
        {|
          invalid_move.Proof_stop_state_hash_failed_to_refute.stop_state_hash :=
            stop_state;
          invalid_move.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.
Definition check_proof_refute_stop_state {A : Set}
  (stop_state : option Sc_rollup_repr.State_hash.t) (input : option A)
  (input_request : Sc_rollup_PVM_sig.input_request)
  (proof_value : Sc_rollup_proof_repr.t) : Pervasives.result unit reason :=
  check_proof_stop_state stop_state input input_request proof_value false.

Definition validity_final_move
  (first_move : bool) (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.level := level;
        V1.t.pvm_name := pvm_name
        |} := game in
    let valid :=
      Sc_rollup_proof_repr.valid inbox_snapshot level pvm_name proof_value in
    let? '_ :=
      if first_move then
        check_proof_distance_is_one start_chunk.(V1.dissection_chunk.tick)
          stop_chunk.(V1.dissection_chunk.tick)
      else
        Error_monad.Lwt_result_syntax.return_unit in
    let? '_ :=
      check_proof_start_state start_chunk.(V1.dissection_chunk.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.(V1.dissection_chunk.state_hash) input input_request
            proof_value
        else
          check_proof_validate_stop_state
            stop_chunk.(V1.dissection_chunk.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
  (agreed_start_chunk : dissection_chunk)
  (refuted_stop_chunk : dissection_chunk) (game : t)
  (proof_value : Sc_rollup_proof_repr.t) : bool :=
  validity_final_move false 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 (stakers : Index.t) (game : t) (refutation : refutation)
  : Either.t game_result t :=
  let mk_loser {A : Set} (reason_value : reason) (loser : player)
    : Either.t game_result A :=
    let loser := Index.staker stakers loser in
    Either.Left
      (Loser
        {| game_result.Loser.reason := reason_value;
          game_result.Loser.loser := loser; |}) in
  let result_value :=
    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? '_ :=
        check_dissection 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.level := game.(V1.t.level);
            V1.t.pvm_name := game.(V1.t.pvm_name);
            V1.t.game_state := new_game_state; |})
    | (Dissection _, V1.Final_move _)
      invalid_move_value
        (Proof_invalid "Final move has started, unexpected dissection")
    |
      (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 proof_value game start_chunk stop_chunk in
      if player_result then
        return? (mk_loser Conflict_resolved (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.level := game.(V1.t.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 agreed_start_chunk refuted_stop_chunk game
          proof_value in
      if player_result then
        return? (mk_loser Conflict_resolved (opponent game.(V1.t.turn)))
      else
        return? (Either.Left Draw)
    end in
  match result_value with
  | Pervasives.Ok x_valuex_value
  | Pervasives.Error reason_valuemk_loser reason_value game.(V1.t.turn)
  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)).