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.030s):
let g : game_state =
  let (_x_0 : player option) = Some X in
  {grid =
   {a = None; b = _x_0; c = _x_0; d = _x_0; e = _x_0; f = None; g = _x_0;
    h = _x_0; i = None};
   last_player = None}
Instance
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.030s
details:
Expand
smt_stats:
num checks:1
rlimit count:2550
mk clause:41
datatype occurs check:1
mk bool var:88
datatype splits:21
decisions:30
propagations:25
eliminated applications:1
conflicts:8
datatype accessor ax:6
minimized lits:4
datatype constructor ax:36
num allocs:7499261
final checks:1
added eqs:161
time:0.014000
memory:17.010000
max memory:17.460000
Expand
  • start[0.030s]
      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 = let (_x_0 : player option) = Some X in {grid = {a = None; b = _x_0; c = _x_0; d = _x_0; e = _x_0; f = None; g = _x_0; h = _x_0; i = None}; 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 -> Z.t * Z.t = <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.027s):
      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_instances:10
      definitions:0
      inductions:0
      search_time:
      0.027s
      details:
      Expand
      smt_stats:
      arith offset eqs:199
      arith assert lower:211
      arith patches_succ:4
      datatype occurs check:684
      datatype splits:67
      arith bound prop:37
      propagations:530
      arith patches:4
      interface eqs:30
      conflicts:37
      arith fixed eqs:257
      datatype constructor ax:1079
      num allocs:14694318
      final checks:42
      added eqs:4746
      del clause:152
      num checks:21
      arith tableau max rows:56
      arith tableau max columns:79
      arith pivots:198
      rlimit count:48754
      mk clause:320
      mk bool var:1805
      arith gcd tests:40
      arith assert upper:251
      decisions:708
      arith row summations:1099
      arith assume eqs:30
      datatype accessor ax:56
      minimized lits:2
      arith conflicts:2
      arith num rows:56
      arith assert diseq:37
      arith eq adapter:185
      memory:18.600000
      max memory:18.600000
      Expand
      • start[0.027s]
          let (_x_0 : (int * int))
              = List.fold_right anon_fun.move_counts.1 (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 anon_fun.move_counts.1 (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 (|::| (h_1267/client (grid_1285/client game_1352/client))
                             (|::| (i_1268/…
            expansions:
            • unroll
              expr:
              (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                               (|::| (i_1268/…
              expansions:
              • unroll
                expr:
                (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                 (|::| (i_1268/…
                expansions:
                • unroll
                  expr:
                  (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                   (|::| (i_1268/…
                  expansions:
                  • unroll
                    expr:
                    (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                     (|::| (i_1268/…
                    expansions:
                    • unroll
                      expr:
                      (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                       (|::| (i_1268/…
                      expansions:
                      • unroll
                        expr:
                        (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                         (|::| (i_1268/…
                        expansions:
                        • unroll
                          expr:
                          (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1352/client))
                                           (|::| (i_1268/…
                          expansions:
                          • unroll
                            expr:
                            (|List.fold_right_523/server|
                              (tuple_mk_517/server 0 0)
                              (|::| (i_1268/client (grid_1285/client g…
                            expansions:
                            • unroll
                              expr:
                              (|List.fold_right_523/server| (tuple_mk_517/server 0 0) |[]|)
                              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_instances:10
                              definitions:0
                              inductions:0
                              search_time:
                              0.042s
                              details:
                              Expand
                              smt_stats:
                              arith offset eqs:914
                              num checks:21
                              arith assert lower:725
                              arith tableau max rows:100
                              arith tableau max columns:123
                              arith pivots:375
                              rlimit count:124862
                              mk clause:1282
                              datatype occurs check:655
                              restarts:1
                              mk bool var:3100
                              arith assert upper:888
                              datatype splits:187
                              decisions:1061
                              arith row summations:3432
                              arith bound prop:266
                              propagations:3178
                              interface eqs:30
                              conflicts:169
                              arith fixed eqs:852
                              arith assume eqs:30
                              datatype accessor ax:116
                              minimized lits:98
                              arith conflicts:24
                              arith num rows:100
                              arith assert diseq:286
                              datatype constructor ax:1193
                              num allocs:26609220
                              final checks:40
                              added eqs:9478
                              del clause:726
                              arith eq adapter:567
                              time:0.019000
                              memory:19.650000
                              max memory:19.650000
                              Expand
                              • start[0.042s]
                                  let (_x_0 : (int * int))
                                      = List.fold_right anon_fun.move_counts.1 (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 anon_fun.move_counts.1 (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 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                     (|::| (i_1268/…
                                    expansions:
                                    • unroll
                                      expr:
                                      (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                       (|::| (i_1268/…
                                      expansions:
                                      • unroll
                                        expr:
                                        (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                         (|::| (i_1268/…
                                        expansions:
                                        • unroll
                                          expr:
                                          (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                           (|::| (i_1268/…
                                          expansions:
                                          • unroll
                                            expr:
                                            (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                             (|::| (i_1268/…
                                            expansions:
                                            • unroll
                                              expr:
                                              (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                               (|::| (i_1268/…
                                              expansions:
                                              • unroll
                                                expr:
                                                (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                                 (|::| (i_1268/…
                                                expansions:
                                                • unroll
                                                  expr:
                                                  (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1354/client))
                                                                   (|::| (i_1268/…
                                                  expansions:
                                                  • unroll
                                                    expr:
                                                    (|List.fold_right_591/server|
                                                      (tuple_mk_585/server 0 0)
                                                      (|::| (i_1268/client (grid_1285/client g…
                                                    expansions:
                                                    • unroll
                                                      expr:
                                                      (|List.fold_right_591/server| (tuple_mk_585/server 0 0) |[]|)
                                                      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]:
                                                      Error:
                                                        Type error (env): Unbound value not_
                                                        Hint: Did you mean not?
                                                        At jupyter cell 15:3,3--6
                                                        3 |    not(is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2))
                                                               ^^^
                                                        
                                                        related locations:
                                                          At jupyter cell 15:1,0--130
                                                          1 | verify((game) => {
                                                          2 |    let (x, o) = move_counts(game.grid);
                                                          3 |    not(is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2))
                                                          4 | }).
                                                          

                                                      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.043s):
                                                      let game : game_state =
                                                        let (_x_0 : player option) = Some O in
                                                        let (_x_1 : player option) = Some X in
                                                        {grid =
                                                         {a = None; b = _x_0; c = None; d = None; e = _x_0; f = _x_1; g = _x_1;
                                                          h = _x_0; i = _x_1};
                                                         last_player = _x_0}
                                                      
                                                      Instance
                                                      proof attempt
                                                      ground_instances:10
                                                      definitions:0
                                                      inductions:0
                                                      search_time:
                                                      0.043s
                                                      details:
                                                      Expand
                                                      smt_stats:
                                                      arith offset eqs:991
                                                      num checks:21
                                                      arith assert lower:844
                                                      arith tableau max rows:84
                                                      arith tableau max columns:107
                                                      arith pivots:350
                                                      rlimit count:149634
                                                      mk clause:1141
                                                      datatype occurs check:263
                                                      restarts:1
                                                      mk bool var:2467
                                                      arith assert upper:890
                                                      datatype splits:209
                                                      decisions:1106
                                                      arith row summations:3300
                                                      arith bound prop:227
                                                      propagations:4463
                                                      interface eqs:11
                                                      conflicts:180
                                                      arith fixed eqs:901
                                                      arith assume eqs:11
                                                      datatype accessor ax:127
                                                      minimized lits:125
                                                      arith conflicts:30
                                                      arith num rows:84
                                                      arith assert diseq:329
                                                      datatype constructor ax:821
                                                      num allocs:47477379
                                                      final checks:22
                                                      added eqs:9861
                                                      del clause:425
                                                      arith eq adapter:485
                                                      time:0.021000
                                                      memory:21.010000
                                                      max memory:21.010000
                                                      Expand
                                                      • start[0.043s]
                                                          let (_x_0 : player option) = ….a in
                                                          let (_x_1 : (int * int))
                                                              = List.fold_right anon_fun.move_counts.1 (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) = ….c in
                                                          let (_x_8 : (player option * player option * player option))
                                                              = (_x_0, …, _x_7)
                                                          in
                                                          let (_x_9 : (player option * player option * player option))
                                                              = (_x_5, _x_5, _x_5)
                                                          in
                                                          let (_x_10 : player option) = ….d in
                                                          let (_x_11 : player option) = ….e in
                                                          let (_x_12 : player option) = ….f in
                                                          let (_x_13 : (player option * player option * player option))
                                                              = (_x_10, _x_11, _x_12)
                                                          in
                                                          let (_x_14 : player option) = ….g in
                                                          let (_x_15 : player option) = ….h in
                                                          let (_x_16 : player option) = ….i in
                                                          let (_x_17 : (player option * player option * player option))
                                                              = (_x_14, _x_15, _x_16)
                                                          in
                                                          let (_x_18 : (player option * player option * player option))
                                                              = (_x_6, _x_6, _x_6)
                                                          in
                                                          let (_x_19 : grid) = ( :var_0: ).grid in
                                                          let (_x_20 : player option) = _x_19.a in
                                                          let (_x_21 : player option) = _x_19.d in
                                                          let (_x_22 : player option) = _x_19.g in
                                                          let (_x_23 : (player option * player option * player option))
                                                              = (_x_20, _x_21, _x_22)
                                                          in
                                                          let (_x_24 : player option) = _x_19.b in
                                                          let (_x_25 : player option) = _x_19.e in
                                                          let (_x_26 : player option) = _x_19.h in
                                                          let (_x_27 : (player option * player option * player option))
                                                              = (_x_24, _x_25, _x_26)
                                                          in
                                                          let (_x_28 : player option) = _x_19.c in
                                                          let (_x_29 : player option) = _x_19.f in
                                                          let (_x_30 : player option) = _x_19.i in
                                                          let (_x_31 : (player option * player option * player option))
                                                              = (_x_28, _x_29, _x_30)
                                                          in
                                                          let (_x_32 : (player option * player option * player option))
                                                              = (_x_20, _x_25, _x_30)
                                                          in
                                                          let (_x_33 : (player option * player option * player option))
                                                              = (_x_28, _x_25, _x_22)
                                                          in
                                                          let (_x_34 : bool)
                                                              = (_x_8 = _x_18)
                                                                || ((_x_13 = _x_18)
                                                                    || ((_x_17 = _x_18)
                                                                        || ((_x_23 = _x_18)
                                                                            || ((_x_27 = _x_18)
                                                                                || ((_x_31 = _x_18)
                                                                                    || ((_x_32 = _x_18) || (_x_33 = _x_18)))))))
                                                          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_8 = _x_9)
                                                                || ((_x_13 = _x_9)
                                                                    || ((_x_17 = _x_9)
                                                                        || (((_x_0, _x_10, _x_14) = _x_9)
                                                                            || (((…, _x_11, _x_15) = _x_9)
                                                                                || (((_x_7, _x_12, _x_16) = _x_9)
                                                                                    || (((_x_0, _x_11, _x_16) = _x_9)
                                                                                        || ((_x_7, _x_11, _x_14) = _x_9))))))))
                                                               && not _x_34)
                                                              || not
                                                                 ((((_x_20, _x_24, _x_28) = _x_9)
                                                                   || (((_x_21, _x_25, _x_29) = _x_9)
                                                                       || (((_x_22, _x_26, _x_30) = _x_9)
                                                                           || ((_x_23 = _x_9)
                                                                               || ((_x_27 = _x_9)
                                                                                   || ((_x_31 = _x_9)
                                                                                       || ((_x_32 = _x_9) || (_x_33 = _x_9))))))))
                                                                  = _x_34))
                                                          && _x_34
                                                      • 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 anon_fun.move_counts.1 (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 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                             (|::| (i_1268/…
                                                            expansions:
                                                            • unroll
                                                              expr:
                                                              (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                               (|::| (i_1268/…
                                                              expansions:
                                                              • unroll
                                                                expr:
                                                                (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                 (|::| (i_1268/…
                                                                expansions:
                                                                • unroll
                                                                  expr:
                                                                  (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                   (|::| (i_1268/…
                                                                  expansions:
                                                                  • unroll
                                                                    expr:
                                                                    (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                     (|::| (i_1268/…
                                                                    expansions:
                                                                    • unroll
                                                                      expr:
                                                                      (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                       (|::| (i_1268/…
                                                                      expansions:
                                                                      • unroll
                                                                        expr:
                                                                        (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                         (|::| (i_1268/…
                                                                        expansions:
                                                                        • unroll
                                                                          expr:
                                                                          (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1374/client))
                                                                                           (|::| (i_1268/…
                                                                          expansions:
                                                                          • unroll
                                                                            expr:
                                                                            (|List.fold_right_716/server|
                                                                              (tuple_mk_710/server 0 0)
                                                                              (|::| (i_1268/client (grid_1285/client g…
                                                                            expansions:
                                                                            • unroll
                                                                              expr:
                                                                              (|List.fold_right_716/server| (tuple_mk_710/server 0 0) |[]|)
                                                                              expansions:
                                                                              • Sat (Some let game : game_state = let (_x_0 : player option) = Some O in let (_x_1 : player option) = Some X in {grid = {a = None; b = _x_0; c = None; d = None; e = _x_0; f = _x_1; g = _x_1; h = _x_0; i = _x_1}; last_player = _x_0} )
                                                                              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.162s):
                                                                              let game : game_state =
                                                                                let (_x_0 : player option) = Some X in
                                                                                {grid =
                                                                                 {a = Some O; b = None; c = None; d = _x_0; e = None; f = _x_0; g = None;
                                                                                  h = None; i = None};
                                                                                 last_player = _x_0}
                                                                              let player : player = O
                                                                              let move : move = F
                                                                              
                                                                              Refuted
                                                                              proof attempt
                                                                              ground_instances:23
                                                                              definitions:0
                                                                              inductions:0
                                                                              search_time:
                                                                              0.163s
                                                                              details:
                                                                              Expand
                                                                              smt_stats:
                                                                              arith offset eqs:4855
                                                                              arith assert lower:2952
                                                                              arith patches_succ:2
                                                                              datatype occurs check:5550
                                                                              datatype splits:709
                                                                              arith bound prop:1028
                                                                              propagations:19046
                                                                              arith patches:2
                                                                              interface eqs:118
                                                                              conflicts:421
                                                                              arith fixed eqs:3686
                                                                              datatype constructor ax:4190
                                                                              num allocs:100034260
                                                                              final checks:143
                                                                              added eqs:47529
                                                                              del clause:994
                                                                              num checks:47
                                                                              arith tableau max rows:226
                                                                              arith tableau max columns:267
                                                                              arith pivots:718
                                                                              rlimit count:608061
                                                                              mk clause:3283
                                                                              restarts:3
                                                                              mk bool var:8422
                                                                              arith gcd tests:11
                                                                              arith assert upper:3996
                                                                              decisions:4853
                                                                              arith row summations:11654
                                                                              arith assume eqs:118
                                                                              datatype accessor ax:266
                                                                              minimized lits:476
                                                                              arith conflicts:41
                                                                              arith num rows:226
                                                                              arith assert diseq:1450
                                                                              arith eq adapter:1405
                                                                              time:0.080000
                                                                              memory:25.330000
                                                                              max memory:25.360000
                                                                              Expand
                                                                              • start[0.163s]
                                                                                  let (_x_0 : player option) = ….a in
                                                                                  let (_x_1 : player option list) = _x_0 :: (… :: …) in
                                                                                  let (_x_2 : (int * int))
                                                                                      = List.fold_right anon_fun.move_counts.1 (0, 0) _x_1
                                                                                  in
                                                                                  let (_x_3 : int) = _x_2.0 in
                                                                                  let (_x_4 : int) = _x_2.1 in
                                                                                  let (_x_5 : bool) = _x_3 + _x_4 = 0 in
                                                                                  let (_x_6 : player option) = ( :var_0: ).last_player in
                                                                                  let (_x_7 : bool) = _x_6 = None in
                                                                                  let (_x_8 : bool) = _x_3 - _x_4 = 1 in
                                                                                  let (_x_9 : player option) = Some X in
                                                                                  let (_x_10 : bool) = _x_3 = _x_4 in
                                                                                  let (_x_11 : player option) = Some O in
                                                                                  let (_x_12 : player option) = ….c in
                                                                                  let (_x_13 : (player option * player option * player option))
                                                                                      = (_x_0, …, _x_12)
                                                                                  in
                                                                                  let (_x_14 : (player option * player option * player option))
                                                                                      = (_x_9, _x_9, _x_9)
                                                                                  in
                                                                                  let (_x_15 : player option) = ….d in
                                                                                  let (_x_16 : player option) = ….e in
                                                                                  let (_x_17 : player option) = ….f in
                                                                                  let (_x_18 : (player option * player option * player option))
                                                                                      = (_x_15, _x_16, _x_17)
                                                                                  in
                                                                                  let (_x_19 : bool) = _x_18 = _x_14 in
                                                                                  let (_x_20 : player option) = ….g in
                                                                                  let (_x_21 : player option) = ….h in
                                                                                  let (_x_22 : player option) = ….i in
                                                                                  let (_x_23 : (player option * player option * player option))
                                                                                      = (_x_20, _x_21, _x_22)
                                                                                  in
                                                                                  let (_x_24 : bool) = _x_23 = _x_14 in
                                                                                  let (_x_25 : (player option * player option * player option))
                                                                                      = (_x_0, _x_15, _x_20)
                                                                                  in
                                                                                  let (_x_26 : bool) = _x_25 = _x_14 in
                                                                                  let (_x_27 : (player option * player option * player option))
                                                                                      = (…, _x_16, _x_21)
                                                                                  in
                                                                                  let (_x_28 : (player option * player option * player option))
                                                                                      = (_x_12, _x_17, _x_22)
                                                                                  in
                                                                                  let (_x_29 : (player option * player option * player option))
                                                                                      = (_x_0, _x_16, _x_22)
                                                                                  in
                                                                                  let (_x_30 : (player option * player option * player option))
                                                                                      = (_x_12, _x_16, _x_20)
                                                                                  in
                                                                                  let (_x_31 : bool)
                                                                                      = (_x_28 = _x_14) || ((_x_29 = _x_14) || (_x_30 = _x_14))
                                                                                  in
                                                                                  let (_x_32 : bool)
                                                                                      = (_x_13 = _x_14)
                                                                                        || (_x_19 || (_x_24 || (_x_26 || ((_x_27 = _x_14) || _x_31))))
                                                                                  in
                                                                                  let (_x_33 : bool) = not _x_32 in
                                                                                  let (_x_34 : (player option * player option * player option))
                                                                                      = (_x_11, _x_11, _x_11)
                                                                                  in
                                                                                  let (_x_35 : bool) = _x_13 = _x_34 in
                                                                                  let (_x_36 : bool) = _x_18 = _x_34 in
                                                                                  let (_x_37 : bool) = _x_23 = _x_34 in
                                                                                  let (_x_38 : bool) = _x_25 = _x_34 in
                                                                                  let (_x_39 : bool)
                                                                                      = (_x_28 = _x_34) || ((_x_29 = _x_34) || (_x_30 = _x_34))
                                                                                  in
                                                                                  let (_x_40 : bool)
                                                                                      = _x_35 || (_x_36 || (_x_37 || (_x_38 || ((_x_27 = _x_34) || _x_39))))
                                                                                  in
                                                                                  let (_x_41 : bool)
                                                                                      = ((_x_5 && _x_7)
                                                                                         || ((_x_8 && (_x_6 = _x_9)) || (_x_10 && (_x_6 = _x_11))))
                                                                                        && ((_x_33 && not _x_40) || not (_x_32 = _x_40))
                                                                                  in
                                                                                  let (_x_42 : bool) = ( :var_1: ) = X in
                                                                                  let (_x_43 : player option) = ….b in
                                                                                  let (_x_44 : (player option * player option * player option))
                                                                                      = (_x_43, _x_16, _x_21)
                                                                                  in
                                                                                  let (_x_45 : bool)
                                                                                      = _x_35 || (_x_36 || (_x_37 || (_x_38 || ((_x_44 = _x_34) || _x_39))))
                                                                                  in
                                                                                  _x_41
                                                                                  && (not (_x_32 || (_x_40 || List.for_all ((<>) None) _x_1))
                                                                                      && (_x_41
                                                                                          && ((_x_7 && _x_42) || (_x_6 = Some (if _x_42 then O else X)))))
                                                                                  ==> ((_x_5 && (… = None))
                                                                                       || ((_x_8 && (… = _x_9)) || (_x_10 && (… = _x_11))))
                                                                                      && ((_x_33 && not _x_45)
                                                                                          || not
                                                                                             ((((_x_0, _x_43, _x_12) = _x_14)
                                                                                               || (_x_19 || (_x_24 || (_x_26 || ((_x_44 = _x_14) || _x_31)))))
                                                                                              = _x_45))
                                                                              • simplify

                                                                                into:
                                                                                let (_x_0 : player option) = ….a in
                                                                                let (_x_1 : (int * int))
                                                                                    = List.fold_right anon_fun.move_counts.1 (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 : bool) = _x_4 = None in
                                                                                let (_x_6 : bool) = _x_2 = _x_3 in
                                                                                let (_x_7 : player option) = Some O in
                                                                                let (_x_8 : bool) = _x_2 + (-1) * _x_3 = 1 in
                                                                                let (_x_9 : player option) = Some X in
                                                                                let (_x_10 : grid) = ( :var_0: ).grid in
                                                                                let (_x_11 : player option) = _x_10.a in
                                                                                let (_x_12 : bool) = _x_11 = _x_9 in
                                                                                let (_x_13 : player option) = _x_10.b in
                                                                                let (_x_14 : bool) = _x_13 = _x_9 in
                                                                                let (_x_15 : player option) = _x_10.c in
                                                                                let (_x_16 : bool) = _x_15 = _x_9 in
                                                                                let (_x_17 : bool) = _x_12 && _x_14 && _x_16 in
                                                                                let (_x_18 : player option) = _x_10.d in
                                                                                let (_x_19 : bool) = _x_18 = _x_9 in
                                                                                let (_x_20 : player option) = _x_10.e in
                                                                                let (_x_21 : bool) = _x_20 = _x_9 in
                                                                                let (_x_22 : player option) = _x_10.f in
                                                                                let (_x_23 : bool) = _x_22 = _x_9 in
                                                                                let (_x_24 : bool) = _x_19 && _x_21 && _x_23 in
                                                                                let (_x_25 : player option) = _x_10.g in
                                                                                let (_x_26 : bool) = _x_25 = _x_9 in
                                                                                let (_x_27 : player option) = _x_10.h in
                                                                                let (_x_28 : bool) = _x_27 = _x_9 in
                                                                                let (_x_29 : player option) = _x_10.i in
                                                                                let (_x_30 : bool) = _x_29 = _x_9 in
                                                                                let (_x_31 : bool) = _x_26 && _x_28 && _x_30 in
                                                                                let (_x_32 : bool) = _x_12 && _x_19 && _x_26 in
                                                                                let (_x_33 : bool) = _x_14 && _x_21 && _x_28 in
                                                                                let (_x_34 : bool) = _x_16 && _x_23 && _x_30 in
                                                                                let (_x_35 : bool) = _x_12 && _x_21 && _x_30 in
                                                                                let (_x_36 : bool) = _x_16 && _x_21 && _x_26 in
                                                                                let (_x_37 : bool)
                                                                                    = not
                                                                                      (_x_17 || _x_24 || _x_31 || _x_32 || _x_33 || _x_34 || _x_35 || _x_36)
                                                                                in
                                                                                let (_x_38 : bool) = _x_11 = _x_7 in
                                                                                let (_x_39 : bool) = _x_13 = _x_7 in
                                                                                let (_x_40 : bool) = _x_15 = _x_7 in
                                                                                let (_x_41 : bool) = _x_38 && _x_39 && _x_40 in
                                                                                let (_x_42 : bool) = _x_18 = _x_7 in
                                                                                let (_x_43 : bool) = _x_20 = _x_7 in
                                                                                let (_x_44 : bool) = _x_22 = _x_7 in
                                                                                let (_x_45 : bool) = _x_42 && _x_43 && _x_44 in
                                                                                let (_x_46 : bool) = _x_25 = _x_7 in
                                                                                let (_x_47 : bool) = _x_27 = _x_7 in
                                                                                let (_x_48 : bool) = _x_29 = _x_7 in
                                                                                let (_x_49 : bool) = _x_46 && _x_47 && _x_48 in
                                                                                let (_x_50 : bool) = _x_38 && _x_42 && _x_46 in
                                                                                let (_x_51 : bool) = _x_39 && _x_43 && _x_47 in
                                                                                let (_x_52 : bool) = _x_40 && _x_44 && _x_48 in
                                                                                let (_x_53 : bool) = _x_38 && _x_43 && _x_48 in
                                                                                let (_x_54 : bool) = _x_40 && _x_43 && _x_46 in
                                                                                let (_x_55 : bool)
                                                                                    = _x_41 || _x_45 || _x_49 || _x_50 || _x_51 || _x_52 || _x_53 || _x_54
                                                                                in
                                                                                let (_x_56 : bool) = ( :var_1: ) = X in
                                                                                let (_x_57 : bool) = _x_0 = _x_9 in
                                                                                let (_x_58 : bool) = … = _x_9 in
                                                                                let (_x_59 : player option) = Some ( :var_1: ) in
                                                                                let (_x_60 : grid)
                                                                                    = if ( :var_2: ) = A
                                                                                      then
                                                                                        {a = _x_59; b = _x_13; c = _x_15; d = _x_18; e = _x_20; f = _x_22;
                                                                                         g = _x_25; h = _x_27; i = _x_29}
                                                                                      else
                                                                                      if ( :var_2: ) = B
                                                                                      then
                                                                                        {a = _x_11; b = _x_59; c = _x_15; d = _x_18; e = _x_20; f = _x_22;
                                                                                         g = _x_25; h = _x_27; i = _x_29}
                                                                                      else if ( :var_2: ) = C then … else …
                                                                                in
                                                                                let (_x_61 : player option) = _x_60.c in
                                                                                let (_x_62 : bool) = _x_61 = _x_9 in
                                                                                let (_x_63 : player option) = _x_60.d in
                                                                                let (_x_64 : bool) = _x_63 = _x_9 in
                                                                                let (_x_65 : player option) = _x_60.e in
                                                                                let (_x_66 : bool) = _x_65 = _x_9 in
                                                                                let (_x_67 : player option) = _x_60.f in
                                                                                let (_x_68 : bool) = _x_67 = _x_9 in
                                                                                let (_x_69 : player option) = _x_60.g in
                                                                                let (_x_70 : bool) = _x_69 = _x_9 in
                                                                                let (_x_71 : player option) = _x_60.h in
                                                                                let (_x_72 : bool) = _x_71 = _x_9 in
                                                                                let (_x_73 : player option) = _x_60.i in
                                                                                let (_x_74 : bool) = _x_73 = _x_9 in
                                                                                let (_x_75 : bool)
                                                                                    = not
                                                                                      ((_x_57 && _x_58 && _x_62) || (_x_64 && _x_66 && _x_68)
                                                                                       || (_x_70 && _x_72 && _x_74) || (_x_57 && _x_64 && _x_70)
                                                                                       || (_x_58 && _x_66 && _x_72) || (_x_62 && _x_68 && _x_74)
                                                                                       || (_x_57 && _x_66 && _x_74) || (_x_62 && _x_66 && _x_70))
                                                                                in
                                                                                let (_x_76 : bool) = _x_0 = _x_7 in
                                                                                let (_x_77 : bool) = … = _x_7 in
                                                                                let (_x_78 : bool) = _x_61 = _x_7 in
                                                                                let (_x_79 : bool) = _x_63 = _x_7 in
                                                                                let (_x_80 : bool) = _x_65 = _x_7 in
                                                                                let (_x_81 : bool) = _x_67 = _x_7 in
                                                                                let (_x_82 : bool) = _x_69 = _x_7 in
                                                                                let (_x_83 : bool) = _x_71 = _x_7 in
                                                                                let (_x_84 : bool) = _x_73 = _x_7 in
                                                                                let (_x_85 : bool)
                                                                                    = (_x_76 && _x_77 && _x_78) || (_x_79 && _x_80 && _x_81)
                                                                                      || (_x_82 && _x_83 && _x_84) || (_x_76 && _x_79 && _x_82)
                                                                                      || (_x_77 && _x_80 && _x_83) || (_x_78 && _x_81 && _x_84)
                                                                                      || (_x_76 && _x_80 && _x_84) || (_x_78 && _x_80 && _x_82)
                                                                                in
                                                                                not
                                                                                ((((_x_2 + _x_3 = 0) && _x_5) || (_x_6 && (_x_4 = _x_7))
                                                                                  || (_x_8 && (_x_4 = _x_9)))
                                                                                 && ((_x_37 && not _x_55) || (_x_37 = _x_55))
                                                                                 && not
                                                                                    (List.for_all ((<>) None) (_x_11 :: (_x_13 :: (_x_15 :: …))) || _x_17
                                                                                     || _x_24 || _x_31 || _x_32 || _x_33 || _x_34 || _x_35 || _x_36 || _x_41
                                                                                     || _x_45 || _x_49 || _x_50 || _x_51 || _x_52 || _x_53 || _x_54)
                                                                                 && ((_x_5 && _x_56) || (_x_4 = Some (if _x_56 then O else X))))
                                                                                || (((_x_8 && _x_56) || (_x_6 && (( :var_1: ) = O)))
                                                                                    && ((_x_75 && not _x_85) || (_x_75 = _x_85)))
                                                                                expansions:
                                                                                []
                                                                                rewrite_steps:
                                                                                  forward_chaining:
                                                                                  • unroll
                                                                                    expr:
                                                                                    (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                     (|::| (i_1268/…
                                                                                    expansions:
                                                                                    • unroll
                                                                                      expr:
                                                                                      (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                      (|rec_mk.grid_1034/server|
                                                                                            …
                                                                                      expansions:
                                                                                      • unroll
                                                                                        expr:
                                                                                        (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                         (|::| (i_1268/…
                                                                                        expansions:
                                                                                        • unroll
                                                                                          expr:
                                                                                          (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                           (|::| (i_1268/…
                                                                                          expansions:
                                                                                          • unroll
                                                                                            expr:
                                                                                            (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                            (|rec_mk.grid_1034/server|
                                                                                                  …
                                                                                            expansions:
                                                                                            • unroll
                                                                                              expr:
                                                                                              (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                               (|::| (i_1268/…
                                                                                              expansions:
                                                                                              • unroll
                                                                                                expr:
                                                                                                (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                (|rec_mk.grid_1034/server|
                                                                                                      …
                                                                                                expansions:
                                                                                                • unroll
                                                                                                  expr:
                                                                                                  (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                   (|::| (i_1268/…
                                                                                                  expansions:
                                                                                                  • unroll
                                                                                                    expr:
                                                                                                    (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                    (|rec_mk.grid_1034/server|
                                                                                                          …
                                                                                                    expansions:
                                                                                                    • unroll
                                                                                                      expr:
                                                                                                      (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                       (|::| (i_1268/…
                                                                                                      expansions:
                                                                                                      • unroll
                                                                                                        expr:
                                                                                                        (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                         (|::| (i_1268/…
                                                                                                        expansions:
                                                                                                        • unroll
                                                                                                          expr:
                                                                                                          (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                          (|rec_mk.grid_1034/server|
                                                                                                                …
                                                                                                          expansions:
                                                                                                          • unroll
                                                                                                            expr:
                                                                                                            (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                             (|::| (i_1268/…
                                                                                                            expansions:
                                                                                                            • unroll
                                                                                                              expr:
                                                                                                              (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                              (|rec_mk.grid_1034/server|
                                                                                                                    …
                                                                                                              expansions:
                                                                                                              • unroll
                                                                                                                expr:
                                                                                                                (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                                 (|::| (i_1268/…
                                                                                                                expansions:
                                                                                                                • unroll
                                                                                                                  expr:
                                                                                                                  (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                                   (|::| (i_1268/…
                                                                                                                  expansions:
                                                                                                                  • unroll
                                                                                                                    expr:
                                                                                                                    (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                                    (|rec_mk.grid_1034/server|
                                                                                                                          …
                                                                                                                    expansions:
                                                                                                                    • unroll
                                                                                                                      expr:
                                                                                                                      (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                                       (|::| (i_1268/…
                                                                                                                      expansions:
                                                                                                                      • unroll
                                                                                                                        expr:
                                                                                                                        (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                                        (|rec_mk.grid_1034/server|
                                                                                                                              …
                                                                                                                        expansions:
                                                                                                                        • unroll
                                                                                                                          expr:
                                                                                                                          (let ((a!1 (|::| (h_1267/client (grid_1285/client game_1398/client))
                                                                                                                                           (|::| (i_1268/…
                                                                                                                          expansions:
                                                                                                                          • unroll
                                                                                                                            expr:
                                                                                                                            (|List.fold_right_1049/server|
                                                                                                                              (tuple_mk_1043/server 0 0)
                                                                                                                              (|::| (i_1268/client (grid_1285/client…
                                                                                                                            expansions:
                                                                                                                            • unroll
                                                                                                                              expr:
                                                                                                                              (let ((a!1 (ite (= move_1400/client H_1280/client)
                                                                                                                                              (|rec_mk.grid_1034/server|
                                                                                                                                    …
                                                                                                                              expansions:
                                                                                                                              • unroll
                                                                                                                                expr:
                                                                                                                                (|List.fold_right_1049/server| (tuple_mk_1043/server 0 0) |[]|)
                                                                                                                                expansions:
                                                                                                                                • Sat (Some let game : game_state = let (_x_0 : player option) = Some X in {grid = {a = Some O; b = None; c = None; d = _x_0; e = None; f = _x_0; g = None; h = None; i = None}; last_player = _x_0} let player : player = O let move : move = F )

                                                                                                                                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 1.22s)!
                                                                                                                                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.