Tic Tac Toe with ReasonML

ReasonML provides an alternative syntax for OCaml, which Imandra can read. Let's walk through an example ReasonML model of Tic Tac Toe and use Imandra to understand and verify some properties of it.

This model is wired into some ReasonReact components in order to produce this final, playable version. You can see the model code and components as a ReasonReact project in this github repo.

Setting up the model

Let's start by adding some definitions for the player, state of a square on the game grid, and the grid itself.

In [1]:
type player =
  | X
  | O;

/* the state of a particular square - None = (no move yet), Some(X/O) = either X or O has moved there */
type square_state = option(player);

/* each letter represents a square on the grid, starting in the top left and going along each row */
type grid = {
  a: square_state,
  b: square_state,
  c: square_state,
  d: square_state,
  e: square_state,
  f: square_state,
  g: square_state,
  h: square_state,
  i: square_state,
};
Out[1]:
type player = X | O
type square_state = player option
type grid = {
  a : square_state;
  b : square_state;
  c : square_state;
  d : square_state;
  e : square_state;
  f : square_state;
  g : square_state;
  h : square_state;
  i : square_state;
}

(NB: we're inputting in Reason syntax, but Imandra currently outputs OCaml syntax - this is something we'll have resolved very soon!).

Grid document printer

Here's an example grid:

In [2]:
let a_grid = {
  a: Some(O),
  b: Some(X),
  c: Some(O),
  d: None,
  e: None,
  f: Some(X),
  g: None,
  h: None,
  i: None,
};
Out[2]:
val a_grid : grid =
  {a = Some O; b = Some X; c = Some O; d = None; e = None; f = Some X;
   g = None; h = None; i = None}

As you can tell, it's not the easiest thing to interpret from Imandra's output given the way we've described the grid. Let's setup a custom document mapping for the grid type. Imandra will render the Document data structures as richer output to display our types in a clearer way:

In [3]:
[@program] let doc_of_square_state = (s : square_state) =>
  Document.s(switch (s) {
  | Some(X) => "❌" /* emojis! */
  | Some(O) => "⭕"
  | None => "·"
});

[@program] let doc_of_grid = (g: grid) => {
  let f = doc_of_square_state;
  Document.tbl([[f(g.a), f(g.b), f(g.c)], [f(g.d), f(g.e), f(g.f)], [f(g.g), f(g.h), f(g.i)]])
};
[@install_doc doc_of_grid];
Out[3]:
val doc_of_square_state : square_state -> Document.t = <fun>
val doc_of_grid : grid -> Document.t = <fun>
In [4]:
a_grid
Out[4]:
- : grid = <document>
··
···

Much better! The [@program] annotation tells Imandra that we're only going to be using these functions for non-analytical (and potentially side-effecting) operations, and that it doesn't have to worry about analysing them. See Logic and program modes for more information.

More definitions

Let's continue adding some more definitions:

In [5]:
/* maps to the grid entries */
type move =
  | A
  | B
  | C
  | D
  | E
  | F
  | G
  | H
  | I;

/* the full game state - the current grid, and who went last */
type game_state = {
  grid,
  last_player: option(player),
};

type game_status =
  | Won(player)
  | InProgress
  | InvalidMove(move)
  | Tied;

let initial_game = {
  grid: {
    a: None,
    b: None,
    c: None,
    d: None,
    e: None,
    f: None,
    g: None,
    h: None,
    i: None,
  },
  last_player: None,
};

let initial_player = X;

/* convenience function from our move variant to the value in that grid position */
let value = ({grid: {a, b, c, d, e, f, g, h, i}, _}) =>
  fun
  | A => a
  | B => b
  | C => c
  | D => d
  | E => e
  | F => f
  | G => g
  | H => h
  | I => i;
Out[5]:
type move = A | B | C | D | E | F | G | H | I
type game_state = { grid : grid; last_player : player option; }
type game_status = Won of player | InProgress | InvalidMove of move | Tied
val initial_game : game_state = {grid = <document>; last_player = None}
val initial_player : player = X
val value : game_state -> move -> square_state = <fun>
···
···
···

Game state document printer

Let's also add another document for printing game_states, showing both the grid and who went last:

In [6]:
[@program] let doc_of_game_state = (gs: game_state) => {
  Document.tbl([[doc_of_grid(gs.grid), Document.s("Last:"), doc_of_square_state(gs.last_player)]])
};

[@install_doc doc_of_game_state];

initial_game;
Out[6]:
val doc_of_game_state : game_state -> Document.t = <fun>
- : game_state = <document>
···
···
···
Last:·

Some logic and our first instance

Now for our first bit of proper logic - whether or not a game is won for a particular player:

In [7]:
let is_winning = ({grid: {a, b, c, d, e, f, g, h, i}, _}, player) => {
  let winning_state = (Some(player), Some(player), Some(player));
  (a, b, c) == winning_state
  || (d, e, f) == winning_state
  || (g, h, i) == winning_state
  || (a, d, g) == winning_state
  || (b, e, h) == winning_state
  || (c, f, i) == winning_state
  || (a, e, i) == winning_state
  || (c, e, g) == winning_state;
};
Out[7]:
val is_winning : game_state -> player -> bool = <fun>

Let's use Imandra to get a feel for this function - let's ask for an instance of a game where the game is being won by the player X. We use Imandra's instance mechanism, and ask for a game g where the predicate is_winning(g, X) is true:

In [8]:
instance((g : game_state) => is_winning(g, X));
Out[8]:
- : game_state -> bool = <fun>
module CX : sig val g : game_state end
Instance (after 0 steps, 0.024s):
 let (g : game_state) =
  {grid =
    {a = (Some X); b = (Some X); c = (Some X); d = (Some X); e = (Some X);
     f = None; g = (Some X); h = (Some X); i = (Some X)};
   last_player = None}
Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.024s
details
Expand
smt_stats
num checks1
arith-make-feasible2
arith-max-columns4
rlimit count2521
mk clause43
datatype occurs check1
mk bool var87
datatype splits23
decisions42
propagations57
eliminated applications1
conflicts10
datatype accessor ax7
minimized lits6
datatype constructor ax28
num allocs1515255
final checks1
added eqs149
time0.011000
memory6.850000
max memory7.300000
Expand
  • start[0.024s]
      let (_x_0 : grid) = ( :var_0: ).grid in
      let (_x_1 : player option) = _x_0.a in
      let (_x_2 : player option) = _x_0.b in
      let (_x_3 : player option) = _x_0.c in
      let (_x_4 : player option) = Some X in
      let (_x_5 : (player option * player option * player option))
          = (_x_4, _x_4, _x_4)
      in
      let (_x_6 : player option) = _x_0.d in
      let (_x_7 : player option) = _x_0.e in
      let (_x_8 : player option) = _x_0.f in
      let (_x_9 : player option) = _x_0.g in
      let (_x_10 : player option) = _x_0.h in
      let (_x_11 : player option) = _x_0.i in
      (_x_1, _x_2, _x_3) = _x_5
      || (_x_6, _x_7, _x_8) = _x_5
         || (_x_9, _x_10, _x_11) = _x_5
            || (_x_1, _x_6, _x_9) = _x_5
               || (_x_2, _x_7, _x_10) = _x_5
                  || (_x_3, _x_8, _x_11) = _x_5
                     || (_x_1, _x_7, _x_11) = _x_5 || (_x_3, _x_7, _x_9) = _x_5
  • simplify

    into
    let (_x_0 : grid) = ( :var_0: ).grid in
    let (_x_1 : player option) = Some X in
    let (_x_2 : bool) = _x_0.a = _x_1 in
    let (_x_3 : bool) = _x_0.b = _x_1 in
    let (_x_4 : bool) = _x_0.c = _x_1 in
    let (_x_5 : bool) = _x_0.d = _x_1 in
    let (_x_6 : bool) = _x_0.e = _x_1 in
    let (_x_7 : bool) = _x_0.f = _x_1 in
    let (_x_8 : bool) = _x_0.g = _x_1 in
    let (_x_9 : bool) = _x_0.h = _x_1 in
    let (_x_10 : bool) = _x_0.i = _x_1 in
    (((((((_x_2 && _x_3) && _x_4 || (_x_5 && _x_6) && _x_7)
         || (_x_8 && _x_9) && _x_10)
        || (_x_2 && _x_5) && _x_8)
       || (_x_3 && _x_6) && _x_9)
      || (_x_4 && _x_7) && _x_10)
     || (_x_2 && _x_6) && _x_10)
    || (_x_4 && _x_6) && _x_8
    expansions
    []
    rewrite_steps
      forward_chaining
      • Sat (Some let (g : game_state) = {grid = {a = (Some X); b = (Some X); c = (Some X); d = (Some X); e = (Some X); f = None; g = (Some X); h = (Some X); i = (Some X)}; last_player = None} )

      Rather than executing our function with random inputs as you might imagine, Imandra has examined our definitions mathematically, and generated an instance that matches what we asked for based on the code itself, without executing it directly. This means we don't have to write generators as we would if we were using a library like QuickCheck for example. We can also use Imandra's other tools, such as state space decomposition, to identify edge cases we may not have thought about. See the other documentation pages/notebooks for more detail.

      In this case we explicitly annotated the type of g as game_state, but if this can be inferred using the usual ReasonML/OCaml inference rules, it can be omitted.

      instance has also reflected the value it found back into our Imandra session, so we can take a look at it:

      In [9]:
      CX.g
      
      Out[9]:
      - : game_state = <document>
      
      ·
      Last:·

      and compute with it:

      In [10]:
      is_winning(CX.g, X)
      
      Out[10]:
      - : bool = true
      

      We can see here that X is definitely 'winning', although the game doesn't look particularly valid. O hasn't made any moves, and the game state hasn't got a last_player set. That's fine for now though, we'll build up additional layers in our logic to handle these other cases. It can be very useful to see a concrete example of our function in action!

      Valid grids

      Let's continue:

      In [11]:
      let other_player =
        fun
        | X => O
        | O => X;
      
      /* count up the number of moves for each player across the whole grid - sounds useful! */
      let move_counts = ({a, b, c, d, e, f, g, h, i}) =>
        List.fold_right(
          (el, (x, o)) =>
            switch (el) {
            | None => (x, o)
            | Some(X) => (x + 1, o)
            | Some(O) => (x, o + 1)
            },
          ~base=(0, 0),
          [a, b, c, d, e, f, g, h, i],
        );
      
      /* whether a grid is 'valid' - the difference between move totals should never be more than 1 */
      let is_valid_grid = (grid, last_player) => {
        let (x, o) = move_counts(grid);
      
        (x + o == 0 && last_player == None) ||
        (x - o == 1 && last_player == Some(X)) ||
        (x == o && last_player == Some(O));
      };
      
      Out[11]:
      val other_player : player -> player = <fun>
      val move_counts : grid -> int * int = <fun>
      val is_valid_grid : grid -> player option -> bool = <fun>
      

      Let's grab a game where the grid is valid:

      In [12]:
      instance((game) => is_valid_grid(game.grid, game.last_player));
      
      Out[12]:
      - : game_state -> bool = <fun>
      module CX : sig val game : game_state end
      
      Instance (after 10 steps, 0.038s):
       let (game : game_state) =
        {grid =
          {a = None; b = None; c = None; d = None; e = None; f = None; g = None;
           h = None; i = None};
         last_player = None}
      
      Instance
      proof attempt
      ground_instances10
      definitions0
      inductions0
      search_time
      0.038s
      details
      Expand
      smt_stats
      num checks21
      arith-assume-eqs5
      arith-make-feasible115
      arith-max-columns65
      rlimit count21688
      arith-cheap-eqs225
      mk clause300
      datatype occurs check236
      mk bool var1427
      arith-lower169
      arith-diseq34
      datatype splits58
      decisions379
      arith-propagations37
      propagations447
      interface eqs5
      arith-bound-propagations-cheap37
      arith-max-rows41
      conflicts29
      datatype accessor ax47
      arith-bound-propagations-lp2
      datatype constructor ax756
      num allocs4419754
      final checks16
      added eqs3252
      del clause149
      arith eq adapter150
      arith-upper211
      time0.001000
      memory10.870000
      max memory10.870000
      Expand
      • start[0.038s]
          let (_x_0 : (int * int))
              = List.fold_right
                (fun el _x
                 -> let (x, o) = _x in
                    begin match (el : player option) with
                      | None -> (x, o)
                      | Some (_pat_87 : player) ->
                        begin match (_pat_87 : player) with
                          | X -> (x + 1, o)
                          | O -> (x, o + 1)
                        end
                    end)
                (0, 0) (….a :: (… :: …))
          in
          let (_x_1 : int) = _x_0.0 in
          let (_x_2 : int) = _x_0.1 in
          let (_x_3 : player option) = ( :var_0: ).last_player in
          _x_1 + _x_2 = 0 && _x_3 = None
          || _x_1 - _x_2 = 1 && _x_3 = Some X || _x_1 = _x_2 && _x_3 = Some O
      • simplify

        into
        let (_x_0 : (int * int))
            = List.fold_right
              (fun el _x
               -> let (x, o) = _x in
                  begin match (el : player option) with
                    | None -> (x, o)
                    | Some (_pat_87 : player) ->
                      begin match (_pat_87 : player) with
                        | X -> (x + 1, o)
                        | O -> (x, o + 1)
                      end
                  end)
              (0, 0) (….a :: (… :: …))
        in
        let (_x_1 : int) = _x_0.0 in
        let (_x_2 : int) = _x_0.1 in
        let (_x_3 : player option) = ( :var_0: ).last_player in
        (_x_1 + _x_2 = 0 && _x_3 = None || _x_1 = _x_2 && _x_3 = Some O)
        || _x_1 + -1 * _x_2 = 1 && _x_3 = Some X
        expansions
        []
        rewrite_steps
          forward_chaining
          • unroll
            expr
            (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                               (|::_3| (i_31 (grid_48 game_117)) |[…
            expansions
            • unroll
              expr
              (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                 (|::_3| (i_31 (grid_48 game_117)) |[…
              expansions
              • unroll
                expr
                (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                   (|::_3| (i_31 (grid_48 game_117)) |[…
                expansions
                • unroll
                  expr
                  (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                     (|::_3| (i_31 (grid_48 game_117)) |[…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                       (|::_3| (i_31 (grid_48 game_117)) |[…
                    expansions
                    • unroll
                      expr
                      (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                         (|::_3| (i_31 (grid_48 game_117)) |[…
                      expansions
                      • unroll
                        expr
                        (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                           (|::_3| (i_31 (grid_48 game_117)) |[…
                        expansions
                        • unroll
                          expr
                          (let ((a!1 (|::_3| (h_30 (grid_48 game_117))
                                             (|::_3| (i_31 (grid_48 game_117)) |[…
                          expansions
                          • unroll
                            expr
                            (|`List.fold_right anon_fun.move_counts.1[0]`_1848|
                              (tuple_mk_1842 0 0)
                              (|::_3| (i_31 (grid_48 g…
                            expansions
                            • unroll
                              expr
                              (|`List.fold_right anon_fun.move_counts.1[0]`_1848| (tuple_mk_1842 0 0) |[]_2|)
                              expansions
                              • Sat (Some let (game : game_state) = {grid = {a = None; b = None; c = None; d = None; e = None; f = None; g = None; h = None; i = None}; last_player = None} )
                              In [13]:
                              CX.game;
                              
                              Out[13]:
                              - : game_state = <document>
                              
                              ···
                              ···
                              ···
                              Last:·

                              This is a bit better - the grid looks more like a real game of Tic Tac Toe now.

                              Let's also see what happens if we ask for an instance that we know shouldn't be possible - if player X is more than 1 move ahead:

                              In [14]:
                              instance((game) => {
                                 let (x, o) = move_counts(game.grid);
                                 is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2)
                              });
                              
                              Out[14]:
                              - : game_state -> bool = <fun>
                              
                              Unsatisfiable
                              proof
                              ground_instances10
                              definitions0
                              inductions0
                              search_time
                              0.109s
                              details
                              Expand
                              smt_stats
                              num checks21
                              arith-assume-eqs34
                              arith-make-feasible623
                              arith-max-columns138
                              arith-conflicts29
                              rlimit count69679
                              arith-cheap-eqs2705
                              mk clause2858
                              datatype occurs check671
                              restarts2
                              mk bool var4957
                              arith-lower1793
                              arith-diseq777
                              datatype splits196
                              decisions836
                              arith-propagations642
                              propagations6216
                              interface eqs34
                              arith-bound-propagations-cheap642
                              arith-max-rows114
                              conflicts241
                              datatype accessor ax185
                              minimized lits260
                              arith-bound-propagations-lp527
                              datatype constructor ax1744
                              num allocs10904509
                              final checks44
                              added eqs10585
                              del clause1348
                              arith eq adapter821
                              arith-upper1436
                              time0.079000
                              memory15.620000
                              max memory15.620000
                              Expand
                              • start[0.109s]
                                  let (_x_0 : (int * int))
                                      = List.fold_right
                                        (fun el _x
                                         -> let (x, o) = _x in
                                            begin match (el : player option) with
                                              | None -> (x, o)
                                              | Some (_pat_87 : player) ->
                                                begin match (_pat_87 : player) with
                                                  | X -> (x + 1, o)
                                                  | O -> (x, o + 1)
                                                end
                                            end)
                                        (0, 0) (….a :: (… :: …))
                                  in
                                  let (_x_1 : int) = _x_0.0 in
                                  let (_x_2 : int) = _x_0.1 in
                                  let (_x_3 : player option) = ( :var_0: ).last_player in
                                  let (_x_4 : int) = _x_1 - _x_2 in
                                  (_x_1 + _x_2 = 0 && _x_3 = None
                                   || _x_4 = 1 && _x_3 = Some X || _x_1 = _x_2 && _x_3 = Some O)
                                  && _x_4 >= 2
                              • simplify

                                into
                                let (_x_0 : (int * int))
                                    = List.fold_right
                                      (fun el _x
                                       -> let (x, o) = _x in
                                          begin match (el : player option) with
                                            | None -> (x, o)
                                            | Some (_pat_87 : player) ->
                                              begin match (_pat_87 : player) with
                                                | X -> (x + 1, o)
                                                | O -> (x, o + 1)
                                              end
                                          end)
                                      (0, 0) (….a :: (… :: …))
                                in
                                let (_x_1 : int) = _x_0.0 in
                                let (_x_2 : int) = _x_0.1 in
                                let (_x_3 : player option) = ( :var_0: ).last_player in
                                let (_x_4 : int) = _x_1 + -1 * _x_2 in
                                ((_x_1 + _x_2 = 0 && _x_3 = None || _x_1 = _x_2 && _x_3 = Some O)
                                 || _x_4 = 1 && _x_3 = Some X)
                                && _x_4 >= 2
                                expansions
                                []
                                rewrite_steps
                                  forward_chaining
                                  • unroll
                                    expr
                                    (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                       (|::_3| (i_31 (grid_48 game_119)) |[…
                                    expansions
                                    • unroll
                                      expr
                                      (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                         (|::_3| (i_31 (grid_48 game_119)) |[…
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                           (|::_3| (i_31 (grid_48 game_119)) |[…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                             (|::_3| (i_31 (grid_48 game_119)) |[…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                               (|::_3| (i_31 (grid_48 game_119)) |[…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                                 (|::_3| (i_31 (grid_48 game_119)) |[…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                                   (|::_3| (i_31 (grid_48 game_119)) |[…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|::_3| (h_30 (grid_48 game_119))
                                                                     (|::_3| (i_31 (grid_48 game_119)) |[…
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|`List.fold_right anon_fun.move_counts.1[0]`_1966|
                                                      (tuple_mk_1960 0 0)
                                                      (|::_3| (i_31 (grid_48 g…
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (|`List.fold_right anon_fun.move_counts.1[0]`_1966| (tuple_mk_1960 0 0) |[]_2|)
                                                      expansions
                                                      • Unsat

                                                      As this is invalid according to the description we've provided, Imandra can't find an instance. In fact, this Unsatisfiable judgment tells us that Imandra has actually constructed a mathematical proof that no such instance exists.

                                                      Verifying

                                                      We can invert this question, and turn it into a verification statement and ask Imandra to check it for us - similar to a test, but mathematically checked for all possible games (as game is the free argument to the verification function).

                                                      In [15]:
                                                      verify((game) => {
                                                         let (x, o) = move_counts(game.grid);
                                                         not(is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2))
                                                      });
                                                      
                                                      Out[15]:
                                                      File "jupyter cell 15", line 3, characters 3-6:
                                                      3 |    not(is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2))
                                                             ^^^
                                                      Error: Unbound value not_
                                                      Hint: Did you mean not?
                                                      

                                                      Valid games

                                                      Let's continue adding some more definitions - we haven't really covered winning criteria as part of is_valid_grid, so let's include a few:

                                                      In [16]:
                                                      let is_tie = ({grid: {a, b, c, d, e, f, g, h, i}, _}) =>
                                                        List.for_all((!=)(None), [a, b, c, d, e, f, g, h, i]);
                                                      
                                                      Out[16]:
                                                      val is_tie : game_state -> bool = <fun>
                                                      
                                                      In [17]:
                                                      let is_valid_game = game => {
                                                        let winning_X = is_winning(game, X);
                                                        let winning_O = is_winning(game, O);
                                                        is_valid_grid(game.grid, game.last_player)
                                                        && (! winning_X && ! winning_O || winning_X != winning_O);
                                                      };
                                                      
                                                      Out[17]:
                                                      val is_valid_game : game_state -> bool = <fun>
                                                      

                                                      ... and let's ask for a valid game where O is winning:

                                                      In [18]:
                                                      instance((game) => is_valid_game(game) && is_winning(game, O));
                                                      
                                                      Out[18]:
                                                      - : game_state -> bool = <fun>
                                                      module CX : sig val game : game_state end
                                                      
                                                      Instance (after 10 steps, 0.069s):
                                                       let (game : game_state) =
                                                        {grid =
                                                          {a = (Some O); b = (Some X); c = None; d = (Some O); e = None;
                                                           f = (Some X); g = (Some O); h = None; i = (Some X)};
                                                         last_player = (Some O)}
                                                      
                                                      Instance
                                                      proof attempt
                                                      ground_instances10
                                                      definitions0
                                                      inductions0
                                                      search_time
                                                      0.069s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      arith-assume-eqs16
                                                      arith-make-feasible462
                                                      arith-max-columns105
                                                      arith-conflicts28
                                                      arith-gcd-calls1
                                                      datatype occurs check351
                                                      arith-lower977
                                                      arith-diseq317
                                                      datatype splits158
                                                      arith-propagations279
                                                      arith-patches-success1
                                                      propagations4073
                                                      arith-patches1
                                                      interface eqs16
                                                      arith-bound-propagations-cheap279
                                                      conflicts200
                                                      datatype constructor ax1455
                                                      num allocs22847152
                                                      final checks27
                                                      added eqs10191
                                                      del clause508
                                                      num checks21
                                                      rlimit count60536
                                                      arith-cheap-eqs1094
                                                      mk clause1433
                                                      restarts1
                                                      mk bool var3197
                                                      decisions1118
                                                      arith-max-rows81
                                                      datatype accessor ax137
                                                      minimized lits153
                                                      arith-bound-propagations-lp145
                                                      arith eq adapter516
                                                      arith-upper696
                                                      time0.035000
                                                      memory20.610000
                                                      max memory20.610000
                                                      Expand
                                                      • start[0.069s]
                                                          let (_x_0 : player option) = ….a in
                                                          let (_x_1 : (int * int))
                                                              = List.fold_right
                                                                (fun el _x
                                                                 -> let (x, o) = _x in
                                                                    begin match (el : player option) with
                                                                      | None -> (x, o)
                                                                      | Some (_pat_87 : player) ->
                                                                        begin match (_pat_87 : player) with
                                                                          | X -> (x + 1, o)
                                                                          | O -> (x, o + 1)
                                                                        end
                                                                    end)
                                                                (0, 0) (_x_0 :: (… :: …))
                                                          in
                                                          let (_x_2 : int) = _x_1.0 in
                                                          let (_x_3 : int) = _x_1.1 in
                                                          let (_x_4 : player option) = ( :var_0: ).last_player in
                                                          let (_x_5 : player option) = Some X in
                                                          let (_x_6 : player option) = Some O in
                                                          let (_x_7 : (player option * player option * player option))
                                                              = (_x_5, _x_5, _x_5)
                                                          in
                                                          let (_x_8 : grid) = ( :var_0: ).grid in
                                                          let (_x_9 : player option) = _x_8.a in
                                                          let (_x_10 : player option) = _x_8.d in
                                                          let (_x_11 : player option) = _x_8.g in
                                                          let (_x_12 : (player option * player option * player option))
                                                              = (_x_9, _x_10, _x_11)
                                                          in
                                                          let (_x_13 : player option) = _x_8.b in
                                                          let (_x_14 : player option) = _x_8.e in
                                                          let (_x_15 : player option) = _x_8.h in
                                                          let (_x_16 : (player option * player option * player option))
                                                              = (_x_13, _x_14, _x_15)
                                                          in
                                                          let (_x_17 : player option) = _x_8.c in
                                                          let (_x_18 : player option) = _x_8.f in
                                                          let (_x_19 : player option) = _x_8.i in
                                                          let (_x_20 : (player option * player option * player option))
                                                              = (_x_17, _x_18, _x_19)
                                                          in
                                                          let (_x_21 : (player option * player option * player option))
                                                              = (_x_9, _x_14, _x_19)
                                                          in
                                                          let (_x_22 : (player option * player option * player option))
                                                              = (_x_17, _x_14, _x_11)
                                                          in
                                                          let (_x_23 : bool)
                                                              = (_x_0, …, ….c) = _x_7
                                                                || (….d, ….e, ….f) = _x_7
                                                                   || (….g, ….h, ….i) = _x_7
                                                                      || _x_12 = _x_7
                                                                         || _x_16 = _x_7
                                                                            || _x_20 = _x_7 || _x_21 = _x_7 || _x_22 = _x_7
                                                          in
                                                          let (_x_24 : (player option * player option * player option))
                                                              = (_x_6, _x_6, _x_6)
                                                          in
                                                          let (_x_25 : bool)
                                                              = (_x_9, _x_13, _x_17) = _x_24
                                                                || (_x_10, _x_14, _x_18) = _x_24
                                                                   || (_x_11, _x_15, _x_19) = _x_24
                                                                      || _x_12 = _x_24
                                                                         || _x_16 = _x_24
                                                                            || _x_20 = _x_24 || _x_21 = _x_24 || _x_22 = _x_24
                                                          in
                                                          ((_x_2 + _x_3 = 0 && _x_4 = None
                                                            || _x_2 - _x_3 = 1 && _x_4 = _x_5 || _x_2 = _x_3 && _x_4 = _x_6)
                                                           && (not _x_23 && not _x_25 || not (_x_23 = _x_25)))
                                                          && _x_25
                                                      • simplify

                                                        into
                                                        let (_x_0 : grid) = ( :var_0: ).grid in
                                                        let (_x_1 : player option) = _x_0.a in
                                                        let (_x_2 : player option) = _x_0.b in
                                                        let (_x_3 : (int * int))
                                                            = List.fold_right
                                                              (fun el _x
                                                               -> let (x, o) = _x in
                                                                  begin match (el : player option) with
                                                                    | None -> (x, o)
                                                                    | Some (_pat_87 : player) ->
                                                                      begin match (_pat_87 : player) with
                                                                        | X -> (x + 1, o)
                                                                        | O -> (x, o + 1)
                                                                      end
                                                                  end)
                                                              (0, 0) (_x_1 :: (_x_2 :: …))
                                                        in
                                                        let (_x_4 : int) = _x_3.0 in
                                                        let (_x_5 : int) = _x_3.1 in
                                                        let (_x_6 : player option) = ( :var_0: ).last_player in
                                                        let (_x_7 : player option) = Some O in
                                                        let (_x_8 : player option) = Some X in
                                                        let (_x_9 : bool) = _x_1 = _x_8 in
                                                        let (_x_10 : bool) = _x_2 = _x_8 in
                                                        let (_x_11 : player option) = _x_0.c in
                                                        let (_x_12 : bool) = _x_11 = _x_8 in
                                                        let (_x_13 : player option) = _x_0.d in
                                                        let (_x_14 : bool) = _x_13 = _x_8 in
                                                        let (_x_15 : player option) = _x_0.e in
                                                        let (_x_16 : bool) = _x_15 = _x_8 in
                                                        let (_x_17 : player option) = _x_0.f in
                                                        let (_x_18 : bool) = _x_17 = _x_8 in
                                                        let (_x_19 : player option) = _x_0.g in
                                                        let (_x_20 : bool) = _x_19 = _x_8 in
                                                        let (_x_21 : player option) = _x_0.h in
                                                        let (_x_22 : bool) = _x_21 = _x_8 in
                                                        let (_x_23 : player option) = _x_0.i in
                                                        let (_x_24 : bool) = _x_23 = _x_8 in
                                                        let (_x_25 : bool)
                                                            = not
                                                              ((((((((_x_9 && _x_10) && _x_12 || (_x_14 && _x_16) && _x_18)
                                                                    || (_x_20 && _x_22) && _x_24)
                                                                   || (_x_9 && _x_14) && _x_20)
                                                                  || (_x_10 && _x_16) && _x_22)
                                                                 || (_x_12 && _x_18) && _x_24)
                                                                || (_x_9 && _x_16) && _x_24)
                                                               || (_x_12 && _x_16) && _x_20)
                                                        in
                                                        let (_x_26 : bool) = _x_1 = _x_7 in
                                                        let (_x_27 : bool) = _x_2 = _x_7 in
                                                        let (_x_28 : bool) = _x_11 = _x_7 in
                                                        let (_x_29 : bool) = _x_13 = _x_7 in
                                                        let (_x_30 : bool) = _x_15 = _x_7 in
                                                        let (_x_31 : bool) = _x_17 = _x_7 in
                                                        let (_x_32 : bool) = _x_19 = _x_7 in
                                                        let (_x_33 : bool) = _x_21 = _x_7 in
                                                        let (_x_34 : bool) = _x_23 = _x_7 in
                                                        let (_x_35 : bool)
                                                            = (((((((_x_26 && _x_27) && _x_28 || (_x_29 && _x_30) && _x_31)
                                                                   || (_x_32 && _x_33) && _x_34)
                                                                  || (_x_26 && _x_29) && _x_32)
                                                                 || (_x_27 && _x_30) && _x_33)
                                                                || (_x_28 && _x_31) && _x_34)
                                                               || (_x_26 && _x_30) && _x_34)
                                                              || (_x_28 && _x_30) && _x_32
                                                        in
                                                        (((_x_4 + _x_5 = 0 && _x_6 = None || _x_4 = _x_5 && _x_6 = _x_7)
                                                          || _x_4 + -1 * _x_5 = 1 && _x_6 = _x_8)
                                                         && (_x_25 && not _x_35 || _x_25 = _x_35))
                                                        && _x_35
                                                        expansions
                                                        []
                                                        rewrite_steps
                                                          forward_chaining
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                               (|::_3| (i_31 (grid_48 game_139)) |[…
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                 (|::_3| (i_31 (grid_48 game_139)) |[…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                   (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                     (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                       (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                         (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                           (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (let ((a!1 (|::_3| (h_30 (grid_48 game_139))
                                                                                             (|::_3| (i_31 (grid_48 game_139)) |[…
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|`List.fold_right anon_fun.move_counts.1[0]`_2143|
                                                                              (tuple_mk_2137 0 0)
                                                                              (|::_3| (i_31 (grid_48 g…
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (|`List.fold_right anon_fun.move_counts.1[0]`_2143| (tuple_mk_2137 0 0) |[]_2|)
                                                                              expansions
                                                                              • Sat (Some let (game : game_state) = {grid = {a = (Some O); b = (Some X); c = None; d = (Some O); e = None; f = (Some X); g = (Some O); h = None; i = (Some X)}; last_player = (Some O)} )
                                                                              In [19]:
                                                                              CX.game;
                                                                              
                                                                              Out[19]:
                                                                              - : game_state = <document>
                                                                              
                                                                              ·
                                                                              ·
                                                                              ·
                                                                              Last:

                                                                              Valid moves

                                                                              Looks good! We're on the home stretch now - let's add the last few helper functions around playing moves:

                                                                              In [20]:
                                                                              let is_valid_move = (game, player, move) =>
                                                                                ! (is_winning(game, X) || is_winning(game, O) || is_tie(game))
                                                                                && is_valid_game(game)
                                                                                && (
                                                                                  game.last_player == None
                                                                                  && player == initial_player
                                                                                  || game.last_player == Some(other_player(player))
                                                                                );
                                                                              
                                                                              let play_move = ({grid, _}, player, move) => {
                                                                                let play = Some(player);
                                                                                let grid =
                                                                                  switch (move) {
                                                                                  | A => {...grid, a: play}
                                                                                  | B => {...grid, b: play}
                                                                                  | C => {...grid, c: play}
                                                                                  | D => {...grid, d: play}
                                                                                  | E => {...grid, e: play}
                                                                                  | F => {...grid, f: play}
                                                                                  | G => {...grid, g: play}
                                                                                  | H => {...grid, h: play}
                                                                                  | I => {...grid, i: play}
                                                                                  };
                                                                                {grid, last_player: play};
                                                                              };
                                                                              
                                                                              let status = game =>
                                                                                if (is_winning(game, X)) {
                                                                                  Won(X);
                                                                                } else if (is_winning(game, O)) {
                                                                                  Won(O);
                                                                                } else if (is_tie(game)) {
                                                                                  Tied;
                                                                                } else {
                                                                                  InProgress;
                                                                                };
                                                                              
                                                                              Out[20]:
                                                                              val is_valid_move : game_state -> player -> 'a -> bool = <fun>
                                                                              val play_move : game_state -> player -> move -> game_state = <fun>
                                                                              val status : game_state -> game_status = <fun>
                                                                              

                                                                              And finally, the function we call from the ReasonReact frontend to actually play the game!

                                                                              In [21]:
                                                                              let play = ({last_player, _} as game, move) => {
                                                                                let player =
                                                                                  switch (last_player) {
                                                                                  | None => initial_player
                                                                                  | Some(player) => other_player(player)
                                                                                  };
                                                                                if (is_valid_move(game, player, move)) {
                                                                                  let game = play_move(game, player, move);
                                                                                  (game, status(game));
                                                                                } else {
                                                                                  (game, InvalidMove(move));
                                                                                };
                                                                              };
                                                                              
                                                                              Out[21]:
                                                                              val play : game_state -> move -> game_state * game_status = <fun>
                                                                              

                                                                              ...and we're done! Let's add one more verification statement to check that these functions work as we expect. If we've got a valid game, and a valid move, then if we play the move on the game, we should still have a valid game.

                                                                              verify((game, player, move) =>
                                                                                (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                ==> is_valid_game(play_move(game, player, move))
                                                                              );

                                                                              The a ==> b operator here is the logical "implies" - "if a is true, then b is also true". It's defined as a regular infix operator in the Imandra prelude:

                                                                              In [22]:
                                                                              (==>)
                                                                              
                                                                              Out[22]:
                                                                              - : bool -> bool -> bool = <fun>
                                                                              

                                                                              Anyway! Let's actually run the statement:

                                                                              In [23]:
                                                                              verify((game, player, move) =>
                                                                                (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                ==> is_valid_game(play_move(game, player, move))
                                                                              );
                                                                              
                                                                              Out[23]:
                                                                              - : game_state -> player -> move -> bool = <fun>
                                                                              module CX : sig val game : game_state val player : player val move : move end
                                                                              
                                                                              Counterexample (after 23 steps, 0.427s):
                                                                               let (game : game_state) =
                                                                                {grid =
                                                                                  {a = (Some X); b = (Some X); c = (Some O); d = None; e = (Some O);
                                                                                   f = (Some X); g = None; h = None; i = (Some O)};
                                                                                 last_player = (Some O)}
                                                                               let (player : player) = X
                                                                               let (move : move) = A
                                                                              
                                                                              Refuted
                                                                              proof attempt
                                                                              ground_instances23
                                                                              definitions0
                                                                              inductions0
                                                                              search_time
                                                                              0.427s
                                                                              details
                                                                              Expand
                                                                              smt_stats
                                                                              arith-assume-eqs97
                                                                              arith-make-feasible3529
                                                                              arith-max-columns299
                                                                              arith-conflicts66
                                                                              arith-gcd-calls2
                                                                              datatype occurs check3827
                                                                              arith-lower11158
                                                                              arith-diseq6278
                                                                              datatype splits788
                                                                              arith-propagations5577
                                                                              arith-patches-success1
                                                                              propagations45079
                                                                              arith-patches2
                                                                              interface eqs96
                                                                              arith-bound-propagations-cheap5577
                                                                              conflicts645
                                                                              datatype constructor ax12071
                                                                              num allocs69621187
                                                                              final checks122
                                                                              added eqs81017
                                                                              del clause1880
                                                                              arith-branch1
                                                                              num checks47
                                                                              rlimit count544771
                                                                              arith-cheap-eqs22268
                                                                              mk clause11097
                                                                              restarts4
                                                                              mk bool var17146
                                                                              decisions7292
                                                                              arith-max-rows256
                                                                              datatype accessor ax456
                                                                              minimized lits946
                                                                              arith-bound-propagations-lp2388
                                                                              arith eq adapter1960
                                                                              arith-upper11193
                                                                              time0.315000
                                                                              memory31.040000
                                                                              max memory31.040000
                                                                              Expand
                                                                              • start[0.427s]
                                                                                  let (_x_0 : (int * int)) = (0, 0) in
                                                                                  let (_x_1 : player option) = ….a in
                                                                                  let (_x_2 : player option list) = _x_1 :: (… :: …) in
                                                                                  let (_x_3 : (int * int))
                                                                                      = List.fold_right
                                                                                        (fun el _x
                                                                                         -> let (x, o) = _x in
                                                                                            begin match (el : player option) with
                                                                                              | None -> (x, o)
                                                                                              | Some (_pat_87 : player) ->
                                                                                                begin match (_pat_87 : player) with
                                                                                                  | X -> (x + 1, o)
                                                                                                  | O -> (x, o + 1)
                                                                                                end
                                                                                            end)
                                                                                        _x_0 _x_2
                                                                                  in
                                                                                  let (_x_4 : int) = _x_3.0 in
                                                                                  let (_x_5 : int) = _x_3.1 in
                                                                                  let (_x_6 : player option) = ( :var_0: ).last_player in
                                                                                  let (_x_7 : bool) = _x_6 = None in
                                                                                  let (_x_8 : player option) = Some X in
                                                                                  let (_x_9 : player option) = Some O in
                                                                                  let (_x_10 : player option) = ….c in
                                                                                  let (_x_11 : (player option * player option * player option))
                                                                                      = (_x_1, …, _x_10)
                                                                                  in
                                                                                  let (_x_12 : (player option * player option * player option))
                                                                                      = (_x_8, _x_8, _x_8)
                                                                                  in
                                                                                  let (_x_13 : player option) = ….d in
                                                                                  let (_x_14 : player option) = ….e in
                                                                                  let (_x_15 : player option) = ….f in
                                                                                  let (_x_16 : (player option * player option * player option))
                                                                                      = (_x_13, _x_14, _x_15)
                                                                                  in
                                                                                  let (_x_17 : player option) = ….g in
                                                                                  let (_x_18 : player option) = ….h in
                                                                                  let (_x_19 : player option) = ….i in
                                                                                  let (_x_20 : (player option * player option * player option))
                                                                                      = (_x_17, _x_18, _x_19)
                                                                                  in
                                                                                  let (_x_21 : (player option * player option * player option))
                                                                                      = (_x_1, _x_13, _x_17)
                                                                                  in
                                                                                  let (_x_22 : (player option * player option * player option))
                                                                                      = (…, _x_14, _x_18)
                                                                                  in
                                                                                  let (_x_23 : (player option * player option * player option))
                                                                                      = (_x_10, _x_15, _x_19)
                                                                                  in
                                                                                  let (_x_24 : (player option * player option * player option))
                                                                                      = (_x_1, _x_14, _x_19)
                                                                                  in
                                                                                  let (_x_25 : (player option * player option * player option))
                                                                                      = (_x_10, _x_14, _x_17)
                                                                                  in
                                                                                  let (_x_26 : bool)
                                                                                      = _x_11 = _x_12
                                                                                        || _x_16 = _x_12
                                                                                           || _x_20 = _x_12
                                                                                              || _x_21 = _x_12
                                                                                                 || _x_22 = _x_12
                                                                                                    || _x_23 = _x_12 || _x_24 = _x_12 || _x_25 = _x_12
                                                                                  in
                                                                                  let (_x_27 : (player option * player option * player option))
                                                                                      = (_x_9, _x_9, _x_9)
                                                                                  in
                                                                                  let (_x_28 : bool)
                                                                                      = _x_11 = _x_27
                                                                                        || _x_16 = _x_27
                                                                                           || _x_20 = _x_27
                                                                                              || _x_21 = _x_27
                                                                                                 || _x_22 = _x_27
                                                                                                    || _x_23 = _x_27 || _x_24 = _x_27 || _x_25 = _x_27
                                                                                  in
                                                                                  let (_x_29 : bool)
                                                                                      = (_x_4 + _x_5 = 0 && _x_7
                                                                                         || _x_4 - _x_5 = 1 && _x_6 = _x_8 || _x_4 = _x_5 && _x_6 = _x_9)
                                                                                        && (not _x_26 && not _x_28 || not (_x_26 = _x_28))
                                                                                  in
                                                                                  let (_x_30 : player option) = ….a in
                                                                                  let (_x_31 : (int * int))
                                                                                      = List.fold_right
                                                                                        (fun el _x
                                                                                         -> let (x, o) = _x in
                                                                                            begin match (el : player option) with
                                                                                              | None -> (x, o)
                                                                                              | Some (_pat_87 : player) ->
                                                                                                begin match (_pat_87 : player) with
                                                                                                  | X -> (x + 1, o)
                                                                                                  | O -> (x, o + 1)
                                                                                                end
                                                                                            end)
                                                                                        _x_0 (_x_30 :: (… :: …))
                                                                                  in
                                                                                  let (_x_32 : int) = _x_31.0 in
                                                                                  let (_x_33 : int) = _x_31.1 in
                                                                                  let (_x_34 : player option) = ….c in
                                                                                  let (_x_35 : (player option * player option * player option))
                                                                                      = (_x_30, …, _x_34)
                                                                                  in
                                                                                  let (_x_36 : player option) = ….d in
                                                                                  let (_x_37 : player option) = ….e in
                                                                                  let (_x_38 : player option) = ….f in
                                                                                  let (_x_39 : (player option * player option * player option))
                                                                                      = (_x_36, _x_37, _x_38)
                                                                                  in
                                                                                  let (_x_40 : player option) = ….g in
                                                                                  let (_x_41 : player option) = ….h in
                                                                                  let (_x_42 : player option) = ….i in
                                                                                  let (_x_43 : (player option * player option * player option))
                                                                                      = (_x_40, _x_41, _x_42)
                                                                                  in
                                                                                  let (_x_44 : (player option * player option * player option))
                                                                                      = (_x_30, _x_36, _x_40)
                                                                                  in
                                                                                  let (_x_45 : (player option * player option * player option))
                                                                                      = (…, _x_37, _x_41)
                                                                                  in
                                                                                  let (_x_46 : (player option * player option * player option))
                                                                                      = (_x_34, _x_38, _x_42)
                                                                                  in
                                                                                  let (_x_47 : (player option * player option * player option))
                                                                                      = (_x_30, _x_37, _x_42)
                                                                                  in
                                                                                  let (_x_48 : (player option * player option * player option))
                                                                                      = (_x_34, _x_37, _x_40)
                                                                                  in
                                                                                  let (_x_49 : bool)
                                                                                      = _x_35 = _x_12
                                                                                        || _x_39 = _x_12
                                                                                           || _x_43 = _x_12
                                                                                              || _x_44 = _x_12
                                                                                                 || _x_45 = _x_12
                                                                                                    || _x_46 = _x_12 || _x_47 = _x_12 || _x_48 = _x_12
                                                                                  in
                                                                                  let (_x_50 : bool)
                                                                                      = _x_35 = _x_27
                                                                                        || _x_39 = _x_27
                                                                                           || _x_43 = _x_27
                                                                                              || _x_44 = _x_27
                                                                                                 || _x_45 = _x_27
                                                                                                    || _x_46 = _x_27 || _x_47 = _x_27 || _x_48 = _x_27
                                                                                  in
                                                                                  _x_29
                                                                                  && not (_x_26 || _x_28 || List.for_all ((<>) None) _x_2)
                                                                                     && _x_29
                                                                                        && (_x_7 && ( :var_1: ) = X
                                                                                            || _x_6 = Some (if Is_a(X, ( :var_1: )) then O else X))
                                                                                  ==> (_x_32 + _x_33 = 0 && … = None
                                                                                       || _x_32 - _x_33 = 1 && … = _x_8 || _x_32 = _x_33 && … = _x_9)
                                                                                      && (not _x_49 && not _x_50 || not (_x_49 = _x_50))
                                                                              • simplify

                                                                                into
                                                                                let (_x_0 : (int * int)) = (0, 0) in
                                                                                let (_x_1 : player option) = ….a in
                                                                                let (_x_2 : player option list) = _x_1 :: (… :: …) in
                                                                                let (_x_3 : (int * int))
                                                                                    = List.fold_right
                                                                                      (fun el _x
                                                                                       -> let (x, o) = _x in
                                                                                          begin match (el : player option) with
                                                                                            | None -> (x, o)
                                                                                            | Some (_pat_87 : player) ->
                                                                                              begin match (_pat_87 : player) with
                                                                                                | X -> (x + 1, o)
                                                                                                | O -> (x, o + 1)
                                                                                              end
                                                                                          end)
                                                                                      _x_0 _x_2
                                                                                in
                                                                                let (_x_4 : int) = _x_3.0 in
                                                                                let (_x_5 : int) = _x_3.1 in
                                                                                let (_x_6 : player option) = ( :var_0: ).last_player in
                                                                                let (_x_7 : bool) = _x_6 = None in
                                                                                let (_x_8 : player option) = Some O in
                                                                                let (_x_9 : player option) = Some X in
                                                                                let (_x_10 : bool) = _x_1 = _x_9 in
                                                                                let (_x_11 : bool) = … = _x_9 in
                                                                                let (_x_12 : player option) = ….c in
                                                                                let (_x_13 : bool) = _x_12 = _x_9 in
                                                                                let (_x_14 : bool) = (_x_10 && _x_11) && _x_13 in
                                                                                let (_x_15 : player option) = ….d in
                                                                                let (_x_16 : bool) = _x_15 = _x_9 in
                                                                                let (_x_17 : player option) = ….e in
                                                                                let (_x_18 : bool) = _x_17 = _x_9 in
                                                                                let (_x_19 : player option) = ….f in
                                                                                let (_x_20 : bool) = _x_19 = _x_9 in
                                                                                let (_x_21 : bool) = (_x_16 && _x_18) && _x_20 in
                                                                                let (_x_22 : player option) = ….g in
                                                                                let (_x_23 : bool) = _x_22 = _x_9 in
                                                                                let (_x_24 : player option) = ….h in
                                                                                let (_x_25 : bool) = _x_24 = _x_9 in
                                                                                let (_x_26 : player option) = ….i in
                                                                                let (_x_27 : bool) = _x_26 = _x_9 in
                                                                                let (_x_28 : bool) = (_x_23 && _x_25) && _x_27 in
                                                                                let (_x_29 : bool) = (_x_10 && _x_16) && _x_23 in
                                                                                let (_x_30 : bool) = (_x_11 && _x_18) && _x_25 in
                                                                                let (_x_31 : bool) = (_x_13 && _x_20) && _x_27 in
                                                                                let (_x_32 : bool) = (_x_10 && _x_18) && _x_27 in
                                                                                let (_x_33 : bool) = (_x_13 && _x_18) && _x_23 in
                                                                                let (_x_34 : bool)
                                                                                    = not
                                                                                      (((((((_x_14 || _x_21) || _x_28) || _x_29) || _x_30) || _x_31) || _x_32)
                                                                                       || _x_33)
                                                                                in
                                                                                let (_x_35 : bool) = _x_1 = _x_8 in
                                                                                let (_x_36 : bool) = … = _x_8 in
                                                                                let (_x_37 : bool) = _x_12 = _x_8 in
                                                                                let (_x_38 : bool) = (_x_35 && _x_36) && _x_37 in
                                                                                let (_x_39 : bool) = _x_15 = _x_8 in
                                                                                let (_x_40 : bool) = _x_17 = _x_8 in
                                                                                let (_x_41 : bool) = _x_19 = _x_8 in
                                                                                let (_x_42 : bool) = (_x_39 && _x_40) && _x_41 in
                                                                                let (_x_43 : bool) = _x_22 = _x_8 in
                                                                                let (_x_44 : bool) = _x_24 = _x_8 in
                                                                                let (_x_45 : bool) = _x_26 = _x_8 in
                                                                                let (_x_46 : bool) = (_x_43 && _x_44) && _x_45 in
                                                                                let (_x_47 : bool) = (_x_35 && _x_39) && _x_43 in
                                                                                let (_x_48 : bool) = (_x_36 && _x_40) && _x_44 in
                                                                                let (_x_49 : bool) = (_x_37 && _x_41) && _x_45 in
                                                                                let (_x_50 : bool) = (_x_35 && _x_40) && _x_45 in
                                                                                let (_x_51 : bool) = (_x_37 && _x_40) && _x_43 in
                                                                                let (_x_52 : bool)
                                                                                    = ((((((_x_38 || _x_42) || _x_46) || _x_47) || _x_48) || _x_49) || _x_50)
                                                                                      || _x_51
                                                                                in
                                                                                let (_x_53 : bool) = ( :var_1: ) = X in
                                                                                let (_x_54 : player option) = ….a in
                                                                                let (_x_55 : (int * int))
                                                                                    = List.fold_right
                                                                                      (fun el _x
                                                                                       -> let (x, o) = _x in
                                                                                          begin match (el : player option) with
                                                                                            | None -> (x, o)
                                                                                            | Some (_pat_87 : player) ->
                                                                                              begin match (_pat_87 : player) with
                                                                                                | X -> (x + 1, o)
                                                                                                | O -> (x, o + 1)
                                                                                              end
                                                                                          end)
                                                                                      _x_0 (_x_54 :: (… :: …))
                                                                                in
                                                                                let (_x_56 : int) = _x_55.0 in
                                                                                let (_x_57 : int) = _x_55.1 in
                                                                                let (_x_58 : bool) = Is_a(C, ( :var_2: )) in
                                                                                let (_x_59 : player option) = Some ( :var_1: ) in
                                                                                let (_x_60 : grid)
                                                                                    = {a = _x_1; b = _x_59; c = _x_12; d = _x_15; e = _x_17; f = _x_19;
                                                                                       g = _x_22; h = _x_24; i = _x_26}
                                                                                in
                                                                                let (_x_61 : bool) = Is_a(B, ( :var_2: )) in
                                                                                let (_x_62 : grid)
                                                                                    = {a = _x_59; b = …; c = _x_12; d = _x_15; e = _x_17; f = _x_19;
                                                                                       g = _x_22; h = _x_24; i = _x_26}
                                                                                in
                                                                                let (_x_63 : bool) = Is_a(A, ( :var_2: )) in
                                                                                let (_x_64 : player option)
                                                                                    = (if _x_63 then _x_62
                                                                                       else if _x_61 then _x_60 else if _x_58 then … else …).e
                                                                                in
                                                                                let (_x_65 : bool) = _x_64 = _x_9 in
                                                                                let (_x_66 : player option) = ….c in
                                                                                let (_x_67 : player option) = ….d in
                                                                                let (_x_68 : player option) = ….e in
                                                                                let (_x_69 : player option) = ….f in
                                                                                let (_x_70 : player option) = ….g in
                                                                                let (_x_71 : player option) = ….h in
                                                                                let (_x_72 : player option) = ….i in
                                                                                let (_x_73 : grid)
                                                                                    = {a = …; b = _x_59; c = _x_66; d = _x_67; e = _x_68; f = _x_69;
                                                                                       g = _x_70; h = _x_71; i = _x_72}
                                                                                in
                                                                                let (_x_74 : grid)
                                                                                    = {a = _x_59; b = ….b; c = _x_66; d = _x_67; e = _x_68; f = _x_69;
                                                                                       g = _x_70; h = _x_71; i = _x_72}
                                                                                in
                                                                                let (_x_75 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).f
                                                                                in
                                                                                let (_x_76 : bool) = _x_75 = _x_9 in
                                                                                let (_x_77 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).g
                                                                                in
                                                                                let (_x_78 : bool) = _x_77 = _x_9 in
                                                                                let (_x_79 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).h
                                                                                in
                                                                                let (_x_80 : bool) = _x_79 = _x_9 in
                                                                                let (_x_81 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).i
                                                                                in
                                                                                let (_x_82 : bool) = _x_81 = _x_9 in
                                                                                let (_x_83 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).a
                                                                                in
                                                                                let (_x_84 : bool) = _x_83 = _x_9 in
                                                                                let (_x_85 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).d
                                                                                in
                                                                                let (_x_86 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).b
                                                                                in
                                                                                let (_x_87 : player option)
                                                                                    = (if _x_63 then _x_74
                                                                                       else if _x_61 then _x_73 else if _x_58 then … else …).c
                                                                                in
                                                                                let (_x_88 : bool) = _x_87 = _x_9 in
                                                                                let (_x_89 : bool)
                                                                                    = not
                                                                                      ((((((((_x_54 = _x_9 && … = _x_9)
                                                                                             && (if _x_63 then _x_62
                                                                                                 else if _x_61 then _x_60 else if _x_58 then … else …).c
                                                                                                = _x_9
                                                                                             || ((if _x_63 then _x_62
                                                                                                  else if _x_61 then _x_60 else if _x_58 then … else …).d
                                                                                                 = _x_9 && _x_65)
                                                                                                && _x_76)
                                                                                            || (_x_78 && _x_80) && _x_82)
                                                                                           || (_x_84 && _x_85 = _x_9) && _x_78)
                                                                                          || (_x_86 = _x_9 && _x_65) && _x_80)
                                                                                         || (_x_88 && _x_76) && _x_82)
                                                                                        || (_x_84 && _x_65) && _x_82)
                                                                                       || (_x_88 && _x_65) && _x_78)
                                                                                in
                                                                                let (_x_90 : bool) = _x_83 = _x_8 in
                                                                                let (_x_91 : bool) = _x_86 = _x_8 in
                                                                                let (_x_92 : bool) = _x_87 = _x_8 in
                                                                                let (_x_93 : bool) = _x_85 = _x_8 in
                                                                                let (_x_94 : bool) = _x_64 = _x_8 in
                                                                                let (_x_95 : bool) = _x_75 = _x_8 in
                                                                                let (_x_96 : bool) = _x_77 = _x_8 in
                                                                                let (_x_97 : bool) = _x_79 = _x_8 in
                                                                                let (_x_98 : bool) = _x_81 = _x_8 in
                                                                                let (_x_99 : bool)
                                                                                    = (((((((_x_90 && _x_91) && _x_92 || (_x_93 && _x_94) && _x_95)
                                                                                           || (_x_96 && _x_97) && _x_98)
                                                                                          || (_x_90 && _x_93) && _x_96)
                                                                                         || (_x_91 && _x_94) && _x_97)
                                                                                        || (_x_92 && _x_95) && _x_98)
                                                                                       || (_x_90 && _x_94) && _x_98)
                                                                                      || (_x_92 && _x_94) && _x_96
                                                                                in
                                                                                not
                                                                                (((((_x_4 + _x_5 = 0 && _x_7 || _x_4 = _x_5 && _x_6 = _x_8)
                                                                                    || _x_4 + -1 * _x_5 = 1 && _x_6 = _x_9)
                                                                                   && (_x_34 && not _x_52 || _x_34 = _x_52))
                                                                                  && not
                                                                                     ((((((((((((((((List.for_all ((<>) None) _x_2 || _x_14) || _x_21)
                                                                                                   || _x_28)
                                                                                                  || _x_29)
                                                                                                 || _x_30)
                                                                                                || _x_31)
                                                                                               || _x_32)
                                                                                              || _x_33)
                                                                                             || _x_38)
                                                                                            || _x_42)
                                                                                           || _x_46)
                                                                                          || _x_47)
                                                                                         || _x_48)
                                                                                        || _x_49)
                                                                                       || _x_50)
                                                                                      || _x_51))
                                                                                 && (_x_7 && _x_53 || _x_6 = Some (if Is_a(X, ( :var_1: )) then O else X)))
                                                                                || (_x_56 + -1 * _x_57 = 1 && _x_53 || _x_56 = _x_57 && ( :var_1: ) = O)
                                                                                   && (_x_89 && not _x_99 || _x_89 = _x_99)
                                                                                expansions
                                                                                []
                                                                                rewrite_steps
                                                                                  forward_chaining
                                                                                  • unroll
                                                                                    expr
                                                                                    (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                    (|rec_mk.grid_2497|
                                                                                                …
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                         (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                           (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                          (|rec_mk.grid_2497|
                                                                                                      …
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                               (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                 (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                (|rec_mk.grid_2497|
                                                                                                            …
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                  (|rec_mk.grid_2497|
                                                                                                              …
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                    (|rec_mk.grid_2497|
                                                                                                                …
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                         (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                        (|rec_mk.grid_2497|
                                                                                                                    …
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                          (|rec_mk.grid_2497|
                                                                                                                      …
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                            (|rec_mk.grid_2497|
                                                                                                                        …
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (let ((a!1 (ite ((_ is (H_43 () move_35)) move_166)
                                                                                                                              (|rec_mk.grid_2497|
                                                                                                                          …
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                   (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                     (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                       (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                         (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                           (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                             (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (let ((a!1 (|::_3| (h_30 (grid_48 game_164))
                                                                                                                                               (|::_3| (i_31 (grid_48 game_164)) |[…
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (|`List.fold_right anon_fun.move_counts.1[0]`_2512|
                                                                                                                                (tuple_mk_2506 0 0)
                                                                                                                                (|::_3| (i_31 (grid_48 g…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (|`List.fold_right anon_fun.move_counts.1[0]`_2512| (tuple_mk_2506 0 0) |[]_2|)
                                                                                                                                expansions
                                                                                                                                • Sat (Some let (game : game_state) = {grid = {a = (Some X); b = (Some X); c = (Some O); d = None; e = (Some O); f = (Some X); g = None; h = None; i = (Some O)}; last_player = (Some O)} let (player : player) = X let (move : move) = A )

                                                                                                                                Uh oh! What's gone wrong?

                                                                                                                                In this case, the problem is clear - the player is trying to play a move in a square that's already occupied:

                                                                                                                                In [24]:
                                                                                                                                value(CX.game, CX.move)
                                                                                                                                
                                                                                                                                Out[24]:
                                                                                                                                - : square_state = Some X
                                                                                                                                

                                                                                                                                If you try out the initial version of the game based on the code so far, you'll see the bug if you try and make a move in a square that's already filled.

                                                                                                                                Imandra has spotted the issue for us from a straightforward statement about the logic of the game!

                                                                                                                                The culprit is the is_valid_move function - we don't check that the square is empty. Let's add && value(game, move) == None to our check:

                                                                                                                                In [25]:
                                                                                                                                let is_valid_move = (game, player, move) =>
                                                                                                                                  ! (is_winning(game, X) || is_winning(game, O) || is_tie(game))
                                                                                                                                  && is_valid_game(game)
                                                                                                                                  && (
                                                                                                                                    game.last_player == None
                                                                                                                                    && player == initial_player
                                                                                                                                    || game.last_player == Some(other_player(player))
                                                                                                                                  )
                                                                                                                                  && value(game, move) == None
                                                                                                                                ;
                                                                                                                                
                                                                                                                                Out[25]:
                                                                                                                                val is_valid_move : game_state -> player -> move -> bool = <fun>
                                                                                                                                

                                                                                                                                ... and verify once more (using [@blast] to speed it up):

                                                                                                                                In [26]:
                                                                                                                                [@blast]
                                                                                                                                verify((game, player, move) =>
                                                                                                                                  (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                                                                  ==> is_valid_game(play_move(game, player, move))
                                                                                                                                );
                                                                                                                                
                                                                                                                                Out[26]:
                                                                                                                                - : game_state -> player -> move -> bool = <fun>
                                                                                                                                
                                                                                                                                proof from "blast" (after 3.87s)!
                                                                                                                                Proved

                                                                                                                                Much better! You can play the final version here, and you'll see that the bug is fixed. Hopefully this gives you a feel for an interactive development workflow with Imandra, in particular how seeing concrete examples can be really useful to understanding what's going on.