sudoku reloaded fully proved, thanks Martin

configure.in

@@ -292,11 +292,21 @@ if test "$USEOCAMLFIND" = yes; then
    fi
 fi
 
-#if ocamlfind is used it gives the install path for ocaml library
-if test "$USEOCAMLFIND" = yes; then
-   OCAMLINSTALLLIB=$(ocamlfind printconf destdir)
+if test "$enable_local" = no; then
+   LOCALDIR=''
 else
-   OCAMLINSTALLLIB=$OCAMLLIB
+   LOCALDIR="${PWD}"
+fi
+
+if test "$enable_local" = yes ; then
+   OCAMLINSTALLLIB=$LOCALDIR/lib
+else
+   #if ocamlfind is used it gives the install path for ocaml library
+   if test "$USEOCAMLFIND" = yes; then
+      OCAMLINSTALLLIB=$(ocamlfind printconf destdir)
+   else
+      OCAMLINSTALLLIB=$OCAMLLIB
+   fi
 fi
 
 # bin-annot
@@ -672,12 +682,6 @@ if test "$enable_frama_c" = yes ; then
    fi
 fi
 
-if test "$enable_local" = no; then
-   LOCALDIR=''
-else
-   LOCALDIR="${PWD}"
-fi
-
 #For the META
 if test "$enable_hypothesis_selection" = yes; then
    META_OCAMLGRAPH="ocamlgraph"

examples/in_progress/sudoku_reloaded.mlw

@@ -142,7 +142,6 @@ module Grid
 
 end
 
-
 (** {2 Concrete Values of Chunks for the Classical Sudoku Grid} *)
 module TheClassicalSudokuGrid
 
@@ -334,7 +333,6 @@ module TheClassicalSudokuGrid
 end
 
 
-
 (** {2 A Sudoku Solver} *)
 
 module Solver
@@ -444,6 +442,7 @@ module Solver
     forall g i x. is_index i /\ full_up_to g i
     -> 1 <= t x <= 9 -> full_up_to (Map.set g i x) (i + 1)
 
+(*
   let rec lemma full_up_to_frame (g1 g2:grid) (i:int)
     requires { 0 <= i <= 81 }
     requires { grid_eq_sub g1 g2 0 i }
@@ -455,6 +454,7 @@ module Solver
         assert { full_up_to g1 (i-1) };
         full_up_to_frame g1 g2 (i-1)
       end
+*)
 
   let lemma full_up_to_frame_all (g1 g2:grid) (i:int)
     requires { 0 <= i <= 81 }
@@ -530,6 +530,22 @@ this is true but with 2 different possible reasons:
   (** {3 The main solver loop} *)
   exception SolutionFound
 
+  let lemma valid_chunk_eq (start offsets:array int31) (g1 g2:grid) (i:int) : unit
+     requires { chunk_valid_indexes start offsets }
+     requires { 0 <= i < 81 }
+     requires { grid_eq g1 g2 }
+     requires { valid_chunk g1 i start offsets }
+     ensures { valid_chunk g2 i start offsets }
+  = ()
+
+  let lemma valid_up_to_eq (s:sudoku_chunks) (g1 g2:grid) (i:int) : unit
+     requires { well_formed_sudoku s }
+     requires { 0 <= i <= 81 }
+     requires { grid_eq g1 g2 }
+     requires { valid_up_to s g1 i }
+     ensures { valid_up_to s g2 i }
+  = ()
+
   let rec solve_aux (s:sudoku_chunks) (g : array int31) (i : int31)
     requires { well_formed_sudoku s }
     requires { t g.length = 81 }
@@ -587,6 +603,8 @@ this is true but with 2 different possible reasons:
         with Invalid ->
           assert {
             grid_eq g.elts (Map.set (at g 'L).elts (t i) !k) };
+          assert { (* for completeness *)
+            not (valid s g.elts) };
           assert { (* for completeness *)
             not (valid s (Map.set (at g 'L).elts (t i) !k)) };
           assert { (* for completeness *)
@@ -637,6 +655,7 @@ end
 
 (** {2 Some Tests} *)
 
+
 module Test
 
   use import Grid
@@ -723,6 +742,7 @@ module Test
 
 end
 
+
 (***
 Local Variables:
 compile-command: "why3 ide sudoku_reloaded.mlw"

examples/in_progress/sudoku_reloaded/Makefile

+
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3.opt
+  WHY3SHARE=../../share
+else
+  ifeq ($(BINDIR),)
+    WHY3=why3
+  else
+    WHY3=$(BINDIR)/why3
+  endif
+  WHY3SHARE=$(shell $(WHY3) --print-datadir)
+endif
+
+include $(WHY3SHARE)/Makefile.config
+
+ifeq ($(BENCH),yes)
+  INCLUDE += -I ../../lib/why3
+endif
+
+MAIN=main
+GEN = map__Map sudoku_reloaded__Grid sudoku_reloaded__TheClassicalSudokuGrid sudoku_reloaded__Solver
+OBJ=$(GEN)
+
+GENML = $(addsuffix .ml, $(GEN))
+ML = $(addsuffix .ml, $(OBJ))
+CMO = $(addsuffix .cmo, $(OBJ))
+CMX = $(addsuffix .cmx, $(OBJ))
+
+OCAMLOPT = ocamlopt -noassert -inline 1000
+
+all: $(MAIN).opt
+
+extract: $(GENML)
+
+doc:
+	$(WHY3) doc ../sudoku_reloaded.mlw
+	$(WHY3) session html .
+
+$(MAIN).byte: $(CMO) $(MAIN).cmo
+	ocamlc -g $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
+
+$(MAIN).opt: $(CMX) $(MAIN).cmx
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
+
+$(MAIN).cmx: $(CMX)
+
+$(GENML): ../sudoku_reloaded.mlw
+	$(WHY3) extract -D ocaml32 ../sudoku_reloaded.mlw -o .
+
+# javascript
+
+
+JSMAIN=jsmain
+
+JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
+          -syntax camlp4o
+
+$(JSMAIN).js: $(JSMAIN).byte
+	js_of_ocaml +nat.js $(JSMAIN).byte
+
+$(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
+	$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
+
+%.cmo: %.ml
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
+%.cmx: %.ml
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
+
+clean::
+	rm -f $(GENML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
+	rm -f sudoku__*.ml why3__*.ml
+	rm -f int__Int.ml map__Map.ml array__Array.ml

examples/in_progress/sudoku_reloaded/index.html

+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
+        "http://www.w3.org/TR/html4/strict.dtd">
+<html>
+  <head>
+    <title>Sudoku Solver using Why3</title>
+    <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+  </head>
+  <body id="body" style="background-color:#e0e0a0">
+    <h1>Sudoku Solver</h1>
+        <p>This solver was developed and formally proved correct using
+        <a href="http://why3.lri.fr/">Why3</a>, extracted to OCaml and
+        then compiled to JavaScript
+        using <a href="http://ocsigen.org/js_of_ocaml/">Js_of_ocaml</a></p>
+
+    <div id="board"></div>
+    <p>
+      <button id="solve">Solve</button>
+      <button id="reset">Reset</button>
+    </p>
+    <p>
+      <button id="sample1">Example 1</button>
+      <button id="sample2">Example 2</button>
+      <button id="sample3">Example 3 (hard)</button>
+    </p>
+    <script type="text/javascript" src="jsmain.js"></script>
+        <p>See also
+          <ul>
+            <li> The <a href="http://toccata.lri.fr/gallery/sudoku.en.html">Why3 source of this solver</a>
+            <li> A <a href="http://www-sop.inria.fr/marelle/Laurent.Thery/Sudoku/Sudoku.html">Sudoku Solver formally proved using Coq</a>
+          </ul>
+        </p>
+  </body>
+</html>

examples/in_progress/sudoku_reloaded/jsmain.ml

+
+
+module D = Dom_html
+
+let d = D.document
+
+(* Grid Layout *)
+
+let make_board () =
+  let make_input () =
+    let input =
+      D.createInput ~_type:(Js.string "text") ~name:(Js.string "input") d
+    in
+    input##size <- 1;
+    input##maxLength <- 1;
+    input##align <- Js.string "center";
+    let style = input##style in
+    style##border <- Js.string "none";
+    style##fontFamily <- Js.string "monospace";
+    style##fontSize <- Js.string "20px";
+    style##fontWeight <- Js.string "bold";
+    style##paddingBottom <- Js.string "5px";
+    style##paddingTop <- Js.string "5px";
+    style##paddingLeft <- Js.string "10px";
+    style##paddingRight <- Js.string "10px";
+    let enforce_digit _ =
+      begin
+        match Js.to_string input##value with
+        | "1" | "2" | "3" | "4" | "5"
+        | "6" | "7" | "8" | "9" -> ()
+        | _ -> input##value <- Js.string ""
+      end;
+      Js._false
+    in
+    input##onchange <- Dom_html.handler enforce_digit;
+    input
+  in
+  let make_td i j input =
+    let td = D.createTd d in
+    td##align <- Js.string "center";
+    let style = td##style in
+    style##borderStyle <- Js.string "solid";
+    style##borderColor <- Js.string "#000000";
+    let widths = function
+      | 0 -> 3, 0 | 2 -> 1, 1 | 3 -> 1, 0
+      | 5 -> 1, 1 | 6 -> 1, 0 | 8 -> 1, 3
+      | _ -> 1, 0 in
+    let (top, bottom) = widths i in
+    let (left, right) = widths j in
+    let px k = Js.string (string_of_int k ^ "px") in
+    style##borderTopWidth <- px top;
+    style##borderBottomWidth <- px bottom;
+    style##borderLeftWidth <- px left;
+    style##borderRightWidth <- px right;
+    Dom.appendChild td input;
+    td
+  in
+  let rows = Array.init 9 (fun i -> Array.init 9 (fun j -> make_input ())) in
+  let table = D.createTable d in
+  table##cellPadding <- Js.string "0px";
+  table##cellSpacing <- Js.string "0px";
+  let tbody = D.createTbody d in
+  Dom.appendChild table tbody;
+  ArrayLabels.iteri rows ~f:(fun i row ->
+    let tr = D.createTr d in
+    ArrayLabels.iteri row ~f:(fun j cell ->
+      let td = make_td i j cell in
+      ignore (Dom.appendChild tr td));
+    ignore (Dom.appendChild tbody tr));
+  (rows, table)
+
+
+(* Solver *)
+
+open Why3extract
+
+let display_sol rows a =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##value <- Js.string (Why3__BigInt.to_string a.(9*i+j));
+      cell##style##backgroundColor <- Js.string "#ffffff"
+    done
+  done
+
+let no_sol rows =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##style##backgroundColor <- Js.string "#ff0000"
+    done
+  done
+
+let solve_board rows _ =
+  let sudoku = Sudoku__TheClassicalSudokuGrid.classical_sudoku () in
+  let input_grid = Array.make 81 Why3__BigInt.zero in
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      let v =
+        match Js.to_string cell##value with
+        | "" -> 0
+        | s -> Char.code s.[0] - Char.code '0'
+      in
+      input_grid.(9*i+j) <- Why3__BigInt.of_int v
+    done
+  done;
+  begin
+    try
+      let a = Sudoku__Solver.check_then_solve sudoku input_grid in
+      display_sol rows a
+    with Sudoku__Solver.NoSolution -> no_sol rows
+  end;
+  Js._false
+
+(* reset board to empty cells *)
+
+let reset_board rows _ =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##value <- Js.string "";
+      cell##style##backgroundColor <- Js.string "#ffffff";
+    done
+  done;
+  Js._false
+
+(* load examples *)
+
+let load_board rows test _ =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      let v = test.(9*i+j) in
+      let v = if v = 0 then "" else string_of_int v in
+      cell##value <- Js.string v;
+      cell##style##backgroundColor <- Js.string "#ffffff";
+    done
+  done;
+  Js._false
+
+let test1 =
+[| 2;0;9;0;0;0;0;1;0;
+   0;0;0;0;6;0;0;0;0;
+   0;5;3;8;0;2;7;0;0;
+   3;0;0;0;0;0;0;0;0;
+   0;0;0;0;7;5;0;0;3;
+   0;4;1;2;0;8;9;0;0;
+   0;0;4;0;9;0;0;2;0;
+   8;0;0;0;0;1;0;0;5;
+   0;0;0;0;0;0;0;7;6 |]
+
+let test2 =
+[| 7;0;0;0;0;0;0;0;8;
+   0;9;0;7;0;6;0;3;0;
+   0;0;1;0;0;0;9;0;0;
+   0;7;0;1;0;4;0;5;0;
+   0;0;0;0;6;0;0;0;0;
+   0;5;0;3;0;7;0;1;0;
+   0;0;2;0;0;0;1;0;0;
+   0;1;0;9;0;8;0;7;0;
+   8;0;0;0;0;0;0;0;6 |]
+
+let test3 =
+[| 0;0;0;0;0;0;0;0;0;
+   0;0;0;0;0;3;0;8;5;
+   0;0;1;0;2;0;0;0;0;
+   0;0;0;5;0;7;0;0;0;
+   0;0;4;0;0;0;1;0;0;
+   0;9;0;0;0;0;0;0;0;
+   5;0;0;0;0;0;0;7;3;
+   0;0;2;0;1;0;0;0;0;
+   0;0;0;0;4;0;0;0;9 |]
+
+let onload (_event : #Dom_html.event Js.t) : bool Js.t =
+  let (rows, table) = make_board () in
+  let solve = Js.Opt.get (d##getElementById (Js.string "solve"))
+    (fun () -> assert false) in
+  solve##onclick <- Dom_html.handler (solve_board rows);
+  let reset = Js.Opt.get (d##getElementById (Js.string "reset"))
+    (fun () -> assert false) in
+  reset##onclick <- Dom_html.handler (reset_board rows);
+  let sample1 = Js.Opt.get (d##getElementById (Js.string "sample1"))
+    (fun () -> assert false) in
+  sample1##onclick <- Dom_html.handler (load_board rows test1);
+  let sample2 = Js.Opt.get (d##getElementById (Js.string "sample2"))
+    (fun () -> assert false) in
+  sample2##onclick <- Dom_html.handler (load_board rows test2);
+  let sample3= Js.Opt.get (d##getElementById (Js.string "sample3"))
+    (fun () -> assert false) in
+  sample3##onclick <- Dom_html.handler (load_board rows test3);
+  let board = Js.Opt.get (d##getElementById (Js.string "board"))
+    (fun () -> assert false) in
+  Dom.appendChild board table;
+  board##style##padding <- Js.string "40px";
+  Js._false
+
+let _ = Dom_html.window##onload <- Dom_html.handler onload

examples/in_progress/sudoku_reloaded/main.ml

+
+open Why3extract
+open Format
+
+let usage () =
+  eprintf "Sudoku: solve a Sudoku puzzle@.";
+  eprintf "Usage: %s <comma separated sequence of 81 non-zero digits>@." Sys.argv.(0);
+  exit 2
+
+let input =
+  if Array.length Sys.argv <> 2 then usage ();
+  Sys.argv.(1)
+
+let input_grid =
+  if String.length input <> 161 then usage ();
+  for i=0 to 79 do
+    if input.[i+i+1] <> ',' then usage ();
+  done;
+  let a = Array.make 81 0 in
+  for i=0 to 80 do
+    match input.[i+i] with
+      | '0'..'9' as c -> a.(i) <- Char.code c - Char.code '0'
+      | _ -> usage ()
+  done;
+  a
+
+let print_grid fmt a =
+  fprintf fmt "@[";
+  for i=0 to 80 do
+    if i mod 9 = 8
+    then fprintf fmt "%d@\n" a.(i)
+    else fprintf fmt "%d " a.(i)
+  done;
+  fprintf fmt "@]"
+
+let () =
+  let sudoku = Sudoku_reloaded__TheClassicalSudokuGrid.classical_sudoku () in
+  printf "Problem: %a@." print_grid input_grid;
+  let a = Sudoku_reloaded__Solver.solve sudoku input_grid
+  in
+  printf "Solution: %a@." print_grid a
+
+(*
+test:
+
+2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
+
+that is
+
+2 0 9 0 0 0 0 1 0
+0 0 0 0 6 0 0 0 0
+0 5 3 8 0 2 7 0 0
+3 0 0 0 0 0 0 0 0
+0 0 0 0 7 5 0 0 3
+0 4 1 2 0 8 9 0 0
+0 0 4 0 9 0 0 2 0
+8 0 0 0 0 1 0 0 5
+0 0 0 0 0 0 0 7 6
+
+should give:
+
+2 6 9 3 5 7 8 1 4
+1 8 7 9 6 4 5 3 2
+4 5 3 8 1 2 7 6 9
+3 7 5 6 4 9 2 8 1
+9 2 8 1 7 5 6 4 3
+6 4 1 2 3 8 9 5 7
+7 1 4 5 9 6 3 2 8
+8 3 6 7 2 1 4 9 5
+5 9 2 4 8 3 1 7 6
+
+Other tests:
+         
+0,0,0,0,0,0,0,0,0,0,0,0,0,0,3,0,8,5,0,0,1,0,2,0,0,0,0,0,0,0,5,0,7,0,0,0,0,0,4,0,0,0,1,0,0,0,9,0,0,0,0,0,0,0,5,0,0,0,0,0,0,7,3,0,0,2,0,1,0,0,0,0,0,0,0,0,4,0,0,0,9