commit 7efbcb75cf29c5ab5c49a2f721f27c579f3d55d9
Author: MysaaJava <samyavrillon@netcourrier.com>
Date:   Mon Jan 29 17:31:08 2024 +0100

    First Commit - As the teacher gave it

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..79fa0fc
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,23 @@
+
+default:
+	@echo 'type `make <target>` where <target> is either ide, replay, test or doc'
+
+ide:
+	why3 ide min_game.mlw
+
+replay:
+	why3 replay min_game
+
+tests:
+	why3 execute min_game.mlw --use MinGame "config0 ()"
+	why3 execute min_game.mlw --use MiniMax "test0 ()"
+	why3 execute min_game.mlw --use AlphaBeta "test_alphabeta ()"
+
+test_min_game:
+	why3 extract -D ocaml64 min_game.mlw -o minGameExtract.ml
+	ocamlbuild -pkg unix -pkg zarith test_min_game.native
+	./test_min_game.native
+
+doc:
+	why3 doc min_game.mlw
+	why3 session html min_game
diff --git a/enonce.pdf b/enonce.pdf
new file mode 100644
index 0000000..78812c2
Binary files /dev/null and b/enonce.pdf differ
diff --git a/min_game.mlw b/min_game.mlw
new file mode 100644
index 0000000..7b9134c
--- /dev/null
+++ b/min_game.mlw
@@ -0,0 +1,341 @@
+
+
+(** {1 Two-Player Games
+
+  MPRI course 2-36-1 Proof of Programs - Project 2023-2024
+
+*)
+
+
+(** {2 Dummy symbols to fill holes in the remainder} *)
+
+module DummySymbols
+
+predicate __FORMULA_TO_BE_COMPLETED__
+constant __TERM_TO_BE_COMPLETED__ : 'a
+constant __VARIANT_TO_BE_COMPLETED__ : int
+let function __EXPRESSION_TO_BE_COMPLETED__ () : 'a = absurd
+let constant __CONDITION_TO_BE_COMPLETED__ : bool = False
+let constant __CODE_TO_BE_COMPLETED__ : unit = ()
+
+end
+
+
+(** {2 The "Min" Game} *)
+
+module MinGame
+
+use export int.Int
+use export array.Array
+use export option.Option
+use export DummySymbols
+
+
+(** type for players *)
+type player = Alice | Bob
+
+(** type for configurations of the game *)
+type config = {
+  stack : array int; (* stack of numbers, e.g. [ 20 ; 17 ; 24 ; -30 ; 27 ] *)
+  pos : int;         (* position in the stack, i.e. index of the first number
+                        to be picked *)
+  turn : player;     (* player who will play next move *)
+  score_alice : int; (* current score of Alice *)
+  score_bob : int;   (* current score of Bob *)
+}
+
+(** initial configuration from a given stack of numbers *)
+function initial_config (stack: array int) : config =
+  { stack = stack; pos = 0; turn = Alice; score_alice = 0; score_bob = 0 }
+
+(** QUESTION 1 *)
+
+(** invariant on configurations *)
+predicate inv(c:config) =
+  __FORMULA_TO_BE_COMPLETED__
+
+(** type for possible moves, here only two choices: pick one or pick
+    two numbers on top of the stack. *)
+type move = PickOne | PickTwo
+
+(** QUESTION 2 *)
+
+(** set of possible moves in a given configuration. It is either empty,
+    represented as `None` or a pair of two moves represented as
+    `Some(m1,m2)` *)
+let function legal_moves (c:config) : option (move, move) =
+  if __CONDITION_TO_BE_COMPLETED__ then None else __EXPRESSION_TO_BE_COMPLETED__ ()
+
+(** QUESTION 3 *)
+
+(** `do_move c m` returns the new configuration obtained from
+    configuration `c` after playing move `m` *)
+let function do_move (c:config) (m:move) : config
+  requires { inv c }
+  requires { __FORMULA_TO_BE_COMPLETED__ }
+  ensures { inv result }
+=
+  match m, c.turn with
+  | PickOne, Alice ->
+    let x = c.stack[c.pos] in
+    { c with turn = Bob; pos = c.pos + 1; score_alice = c.score_alice + x }
+  | PickOne, Bob ->
+    let x = c.stack[c.pos] in
+    __EXPRESSION_TO_BE_COMPLETED__ ()
+  | PickTwo, Alice ->
+    __EXPRESSION_TO_BE_COMPLETED__ ()
+  | PickTwo,Bob ->
+    __EXPRESSION_TO_BE_COMPLETED__ ()
+  end
+
+(** `config_value c` is an heuristic evaluation of the config `c`,
+     Alice wants to minimize it whereas Bob wants to maximize it *)
+let function config_value (c:config) : int =
+   c.score_alice - c.score_bob
+
+use array.Init
+
+(* QUESTION 4 *)
+let config0 () : config
+  ensures { result.stack.length = 5 }
+  ensures { result.stack[0] = 20 }
+  ensures { result.stack[1] = 17 }
+  ensures { result.stack[2] = 24 }
+  ensures { result.stack[3] = -30 }
+  ensures { result.stack[4] = 27 }
+  ensures { result.pos = 0 }
+  ensures { result.turn = Alice }
+  ensures { result.score_alice = 0 }
+  ensures { result.score_bob = 0 }
+  ensures { inv result }
+  =
+   let s = init 5 [| 20; 17; 24; -30; 27 |] in
+   { stack = s;
+     pos = 0;
+     turn = Alice;
+     score_alice = 0;
+     score_bob = 0;
+   }
+
+(* You can run the test above using:
+    why3 execute min_game.mlw --use MinGame "config0 ()"
+*)
+
+
+end
+
+
+
+
+(** {2 The MiniMax value of a tree of moves} *)
+
+module MiniMax
+
+  use MinGame
+  use int.MinMax
+
+(* QUESTION 5 *)
+
+  (** [minimax c d] returns the minimax evaluation of config [p]
+      at depth [d].  *)
+  let rec function minimax (c:config) (d:int) : int
+    requires { inv c }
+    variant { __VARIANT_TO_BE_COMPLETED__ }
+  = if d <= 0 then __EXPRESSION_TO_BE_COMPLETED__ () else
+    match legal_moves c with
+    | None -> __EXPRESSION_TO_BE_COMPLETED__ ()
+    | Some(m1,m2) ->
+      match c.turn with
+      | Alice -> (* Alice wants to minimize the config value *)
+        min (minimax (do_move c m1) (d-1)) (minimax (do_move c m2) (d-1))
+      | Bob -> (* Bob wants to maximize the config value *)
+        __EXPRESSION_TO_BE_COMPLETED__ ()
+      end
+    end
+
+(* QUESTION 6 *)
+
+(** Testing `minimax` on the sample configuration by concrete execution *)
+let test0 () =
+  let c0 = config0 () in
+  (minimax c0 0,
+   minimax c0 1,
+   minimax c0 2,
+   minimax c0 3,
+   minimax c0 4,
+   minimax c0 5)
+
+(* You can run the tests above using:
+    why3 execute min_game.mlw --use MiniMax "test0 ()"
+*)
+
+(** Testing `minimax` on the sample configuration with provers *)
+let test_minimax () =
+  let c0 = config0 () in
+  assert { minimax c0 0 = 0 };
+  assert { minimax c0 1 = 20 };
+  assert { minimax c0 2 = 3 };
+  assert { minimax c0 3 = -3 }
+
+
+
+end
+
+
+
+
+
+(** {2 The alpha-beta algorithm} *)
+
+module AlphaBeta
+
+  use int.MinMax
+  use MinGame
+  use MiniMax
+
+  (** `lt_alpha_n alpha n` means `alpha < n` *)
+  let predicate lt_alpha_n (alpha: option int) (n:int) =
+    match alpha with
+    | None -> true
+    | Some a -> a < n
+    end
+
+  (** `lt_n_beta n beta` means `n < beta` *)
+  let predicate lt_n_beta (n:int) (beta: option int) =
+    match beta with
+    | None -> true
+    | Some b -> n < b
+    end
+
+  (** `max_alpha alpha n` is the maximum of `alpha` and `n` *)
+  let max_alpha (alpha: option int) (n:int) : option int =
+    match alpha with
+    | None -> Some n
+    | Some a -> Some (max a n)
+    end
+
+  (** `min_beta n beta` is the minimum of `n` and `beta` *)
+  let min_beta (n:int) (beta: option int) : option int =
+    match beta with
+    | None -> Some n
+    | Some b -> Some (min n b)
+    end
+
+(* QUESTIONS 7 and 8 *)
+
+  let rec alpha_beta (alpha beta:option int) (c:config) (d:int) : int
+    requires { inv c }
+    requires { __FORMULA_TO_BE_COMPLETED__ } 
+    variant  { __VARIANT_TO_BE_COMPLETED__ }
+    ensures  { __FORMULA_TO_BE_COMPLETED__ }
+  = __EXPRESSION_TO_BE_COMPLETED__ ()
+
+  (* QUESTIONS 9 and 10 *)
+
+  exception GameEnded
+
+  let best_move (c:config) (d:int) : move
+    requires { inv c } 
+    ensures { __FORMULA_TO_BE_COMPLETED__ }
+    raises { GameEnded -> __FORMULA_TO_BE_COMPLETED__ }
+  = raise GameEnded (* TO BE COMPLETED *)
+
+  let test_alphabeta () =
+    let c0 = config0 () in
+    try
+    (best_move c0 1,
+     best_move c0 2,
+     best_move c0 3,
+     best_move c0 4)
+     with GameEnded -> absurd
+     end
+
+  (* You can run the test above using:
+      why3 execute num_game.mlw --use AlphaBeta "test_alphabeta ()"
+  *)
+
+end
+
+
+
+
+
+
+(** {2 An efficient algorithm for the Min game} *)
+
+(** Best move found by dynamic programming *)
+
+
+
+module Dynamic
+
+
+
+use int.Int
+use int.MinMax
+use array.Array
+
+use MinGame
+use MiniMax
+
+
+(** QUESTION 13 *)
+
+(* Lemma relating the minimax value of a configuration to the minimax
+value of the same configuration with score set to zero.  *)
+
+  let rec lemma minimax_independence (c:config) (d:int) : unit
+    requires { inv c }
+    requires { __FORMULA_TO_BE_COMPLETED__ }
+    variant { __VARIANT_TO_BE_COMPLETED__ }
+    ensures { minimax c d =
+              minimax { c with score_alice = 0 ; score_bob = 0 } d +
+              __TERM_TO_BE_COMPLETED__ }
+  = __EXPRESSION_TO_BE_COMPLETED__ ()
+
+
+
+
+(* QUESTION 16 *)
+
+predicate dynamic_inv_at_index  (stack:array int) (i:int) (a:array int) =
+  forall t:player, sa sb : int, d:int. 
+    let c =
+      { stack = stack; pos = i; turn = t; score_alice = sa; score_bob = sb }
+    in
+    (* relating `minimax c d` to a[i] *)
+    __FORMULA_TO_BE_COMPLETED__
+
+(* QUESTION 15 and 17 *)
+
+let dynamic (stack : array int) : int
+  requires { __FORMULA_TO_BE_COMPLETED__ }
+  ensures { forall d:int. __FORMULA_TO_BE_COMPLETED__ }
+	    (* relating the result to minimax *)
+=
+  let l = stack.length in
+  let a = Array.make (l+1) 0 in
+  for n = l-2 downto 0 do
+    invariant { __FORMULA_TO_BE_COMPLETED__ }
+    a[n] <- __EXPRESSION_TO_BE_COMPLETED__ ();
+  done;
+  a[0]
+
+  let test () =
+    let c0 = config0 () in
+    dynamic c0.stack
+  (* You can run the test above using:
+      why3 execute min_game.mlw --use Dynamic "test ()"
+   *)
+
+
+
+(* QUESTION 18 *)
+
+let dynamic_opt (stack : array int) : int
+  requires { __FORMULA_TO_BE_COMPLETED__ }
+  ensures { __FORMULA_TO_BE_COMPLETED__ }
+= __EXPRESSION_TO_BE_COMPLETED__ ()
+
+
+end
diff --git a/test_min_game.ml b/test_min_game.ml
new file mode 100644
index 0000000..ada0ec7
--- /dev/null
+++ b/test_min_game.ml
@@ -0,0 +1,82 @@
+
+open Format
+
+let run msg f d =
+  let t = Unix.gettimeofday () in
+  let x = f d in
+  let t = Unix.gettimeofday () -. t in
+  printf "@[[%2.2f] %s(%d): %a@]@." t msg d Z.pp_print x
+
+let z = Z.of_int
+
+(* pseudo-random arrays as test *)
+let random_array size =
+  let () = Random.init 2024 in
+  Array.init size (fun _ -> z (Random.int 2024 - 1000))
+
+open MinGameExtract
+
+let random_config size : config = {
+  stack = random_array size;
+  pos = z 0;
+  turn = Alice;
+  score_alice = z 0;
+  score_bob = z 0;
+}
+
+let () =
+  (* testing alpha-beta *)
+  let f d = MinGameExtract.alpha_beta None None (random_config d) (z d) in
+  run "alpha_beta" f 0;
+  run "alpha_beta" f 1;
+  run "alpha_beta" f 2;
+  run "alpha_beta" f 3;
+  run "alpha_beta" f 5;
+  run "alpha_beta" f 10;
+  run "alpha_beta" f 15;
+  run "alpha_beta" f 20;
+  run "alpha_beta" f 25;
+  run "alpha_beta" f 30;
+  run "alpha_beta" f 35;
+  (* comment some of the tests below if it takes too long time *)
+  run "alpha_beta" f 40;
+  run "alpha_beta" f 41;
+  run "alpha_beta" f 42;
+  run "alpha_beta" f 43;
+  run "alpha_beta" f 44;
+  run "alpha_beta" f 45;
+  run "alpha_beta" f 46;
+  run "alpha_beta" f 47;
+  run "alpha_beta" f 48;
+  run "alpha_beta" f 49;
+  run "alpha_beta" f 50;
+  run "alpha_beta" f 51;
+  (* testing dynamic programming *)
+  let h d = MinGameExtract.dynamic (random_array d)  in
+  run "dynamic" h 0;
+  run "dynamic" h 1;
+  run "dynamic" h 2;
+  run "dynamic" h 3;
+  run "dynamic" h 5;
+  run "dynamic" h 10;
+  run "dynamic" h 15;
+  run "dynamic" h 20;
+  run "dynamic" h 25;
+  run "dynamic" h 30;
+  run "dynamic" h 35;
+  run "dynamic" h 40;
+  run "dynamic" h 41;
+  run "dynamic" h 42;
+  run "dynamic" h 43;
+  run "dynamic" h 44;
+  run "dynamic" h 45;
+  run "dynamic" h 46;
+  run "dynamic" h 47;
+  run "dynamic" h 48;
+  run "dynamic" h 49;
+  run "dynamic" h 50;
+  run "dynamic" h 51;
+  run "dynamic" h 100;
+  run "dynamic" h 1024;
+  run "dynamic" h 2024;
+  ()