examples/queens_bv.mlw

   1
   2 (**
   3
   4 {1 N-queens problem}
   5
   6 Verification of the following 2-lines C program solving the N-queens problem:
   7
   8 {h <pre>
   9    t(a,b,c){int d=0,e=a&amp;~b&amp;~c,f=1;if(a)for(f=0;d=(e-=d)&amp;-e;f+=t(a-d,(b+d)*2,(
  10    c+d)/2));return f;}main(q){scanf("%d",&amp;q);printf("%d\n",t(~(~0&lt;&lt;q),0,0));}
  11 </pre>}
  12
  13 *)
  14
  15 (**
  16
  17 {2 finite sets of integers, with succ and pred operations }
  18
  19 *)
  20
  21 theory S
  22
  23   use int.Int
  24   use export set.FsetInt
  25
  26   function succ (fset int) : fset int
  27
  28   axiom succ_def:
  29     forall s: fset int, i: int. mem i (succ s) <-> i >= 1 /\ mem (i-1) s
  30
  31   function pred (fset int) : fset int
  32
  33   axiom pred_def:
  34     forall s: fset int, i: int. mem i (pred s) <-> i >= 0 /\ mem (i+1) s
  35
  36 end
  37
  38 (** {2 Formalization of the set of solutions of the N-queens problem} *)
  39
  40 theory Solution
  41
  42   use int.Int
  43   use export map.Map
  44
  45   (** the number of queens *)
  46   constant n : int
  47
  48   type solution = map int int
  49
  50   (** solutions `t` and `u` have the same prefix `[0..i[` *)
  51   predicate eq_prefix (t u: map int 'a) (i: int) =
  52     forall k: int. 0 <= k < i -> t[k] = u[k]
  53
  54   predicate eq_sol (t u: solution) = eq_prefix t u n
  55
  56   (** `s` stores a partial solution, for the rows `0..k-1` *)
  57   predicate partial_solution (k: int) (s: solution) =
  58     forall i: int. 0 <= i < k ->
  59       0 <= s[i] < n /\
  60       (forall j: int. 0 <= j < i -> s[i]      <> s[j] /\
  61                                     s[i]-s[j] <> i-j  /\
  62                                     s[i]-s[j] <> j-i)
  63
  64   predicate solution (s: solution) = partial_solution n s
  65
  66   lemma partial_solution_eq_prefix:
  67     forall u t: solution, k: int.
  68     partial_solution k t -> eq_prefix t u k -> partial_solution k u
  69
  70   predicate lt_sol (s1 s2: solution) =
  71     exists i: int. 0 <= i < n /\ eq_prefix s1 s2 i /\ s1[i] < s2[i]
  72
  73   type solutions = map int solution
  74
  75   (** `s[a..b[` is sorted for `lt_sol` *)
  76   predicate sorted (s: solutions) (a b: int) =
  77     forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]
  78
  79   (** a sorted array of solutions contains no duplicate *)
  80   lemma no_duplicate:
  81     forall s: solutions, a b: int. sorted s a b ->
  82     forall i j: int. a <= i < j < b -> not (eq_sol s[i] s[j])
  83
  84 end
  85
  86 (** {2 More realistic code with bitwise operations} *)
  87
  88 module BitsSpec
  89
  90   use int.Int
  91   use S
  92
  93   constant size : int = 32
  94
  95   type t = private {
  96     ghost mdl: fset int;
  97   }
  98   invariant { forall i. mem i mdl -> 0 <= i < size }
  99
 100   val empty () : t
 101     ensures { is_empty result.mdl }
 102
 103   val is_empty (x:t) : bool
 104     ensures { result  <-> is_empty x.mdl }
 105
 106   val remove_singleton (a b: t) : t
 107     requires { b.mdl = singleton (min_elt b.mdl) }
 108     requires { mem (min_elt b.mdl) a.mdl }
 109     ensures  { result.mdl = remove (min_elt b.mdl) a.mdl }
 110
 111   val add_singleton (a b: t) : t
 112     requires { b.mdl = singleton (min_elt b.mdl) }
 113     (* requires { not (mem (min_elt b.mdl) a.mdl) } *)
 114     (* this is not required if the implementation uses or instead of add *)
 115     ensures  { result.mdl = S.add (min_elt b.mdl) a.mdl }
 116
 117   val mul2 (a: t) : t
 118     ensures { result.mdl = remove size (succ a.mdl) }
 119
 120   val div2 (a: t) : t
 121     ensures { result.mdl = pred a.mdl }
 122
 123   val diff (a b: t) : t
 124     ensures { result.mdl = diff a.mdl b.mdl }
 125
 126   use ref.Ref
 127   val rightmost_bit_trick (a: t) (ghost min : ref int) : t
 128     requires { not (is_empty a.mdl) }
 129     writes   { min }
 130     ensures  { !min = min_elt a.mdl }
 131     ensures  { result.mdl = singleton !min }
 132
 133   use bv.BV32 as BV32
 134   val below (n: BV32.t) : t
 135     requires { BV32.ule n (32:BV32.t) }
 136     ensures  { result.mdl = interval 0 (BV32.t'int n) }
 137 end
 138
 139 (** {2 The 1-bits of an integer, as a set of integers} *)
 140
 141 module Bits
 142
 143   use int.Int
 144   use S
 145   use bv.BV32
 146
 147   constant size : int = 32
 148
 149   type t = {
 150           bv : BV32.t;
 151     ghost mdl: fset int;
 152   }
 153   invariant {
 154     forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl
 155   }
 156
 157   let empty () : t
 158     ensures { is_empty result.mdl }
 159   = { bv = 0x0; mdl = empty }
 160
 161   let is_empty (x:t) : bool
 162     ensures { result  <-> is_empty x.mdl }
 163   = assert {is_empty x.mdl -> x.bv = zeros by x.bv == zeros};
 164     BV32.eq x.bv 0x0
 165
 166   let remove_singleton (a b: t) : t
 167     requires { b.mdl = singleton (min_elt b.mdl) }
 168     requires { mem (min_elt b.mdl) a.mdl }
 169     ensures  { result.mdl = remove (min_elt b.mdl) a.mdl }
 170   =
 171     { bv = bw_and a.bv (bw_not b.bv);
 172       mdl = ghost remove (min_elt b.mdl) a.mdl }
 173     (* { bv = sub a.bv b.bv; mdl = remove (min_elt b.mdl) a.mdl } *)
 174
 175   let add_singleton (a b: t) : t
 176     requires { b.mdl = singleton (min_elt b.mdl) }
 177     (* requires { not (mem (min_elt b.mdl) a.mdl) } *)
 178     (* this is not required if the implementation uses or instead of add *)
 179     ensures  { result.mdl = S.add (min_elt b.mdl) a.mdl }
 180   =
 181     { bv = bw_or a.bv b.bv;
 182       mdl = ghost S.add (min_elt b.mdl) a.mdl }
 183     (* { bv = add a.bv b.bv; mdl = add (min_elt b.mdl) a.mdl } *)
 184
 185   let mul2 (a: t) : t
 186     ensures { result.mdl = remove size (succ a.mdl) }
 187   =
 188     { bv = lsl_bv a.bv (1:BV32.t);
 189       mdl = ghost remove size (succ a.mdl) }
 190
 191   let div2 (a: t) : t
 192     ensures { result.mdl = pred a.mdl }
 193   =
 194     { bv = lsr_bv a.bv (1:BV32.t);
 195       mdl = ghost pred a.mdl }
 196
 197   let diff (a b: t) : t
 198     ensures { result.mdl = diff a.mdl b.mdl }
 199   =
 200     { bv = bw_and a.bv (bw_not b.bv);
 201       mdl = ghost diff a.mdl b.mdl }
 202
 203   predicate bits_interval_is_zeros_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
 204     eq_sub_bv a zeros i n
 205
 206   predicate bits_interval_is_one_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
 207     eq_sub_bv a ones i n
 208
 209   predicate bits_interval_is_zeros (a:BV32.t) (i : int) (n : int) =
 210     eq_sub a zeros i n
 211
 212   predicate bits_interval_is_one (a:BV32.t) (i : int) (n : int) =
 213     eq_sub a ones i n
 214
 215   let rightmost_bit_trick (a: t) : t
 216     requires { not (is_empty a.mdl) }
 217     ensures  { result.mdl = singleton (min_elt a.mdl) }
 218   =
 219     let ghost n = min_elt a.mdl in
 220     let ghost n_bv = of_int n in
 221     assert {bits_interval_is_zeros_bv a.bv zeros n_bv};
 222     assert {nth_bv a.bv n_bv};
 223     assert {nth_bv (neg a.bv) n_bv};
 224     let res = bw_and a.bv (neg a.bv) in
 225     assert {forall i. 0 <= i < n -> not (nth res i)};
 226     assert {bits_interval_is_zeros_bv res (add n_bv (1:BV32.t)) (sub (31:BV32.t) n_bv )};
 227     assert {bits_interval_is_zeros res (n + 1) (31 - n)};
 228     { bv = res;
 229       mdl = singleton n }
 230
 231   let below (n: BV32.t) : t
 232     requires { BV32.ule n (32:BV32.t) }
 233     ensures  { result.mdl = interval 0 (t'int n) }
 234   =
 235     { bv = bw_not (lsl_bv 0xFFFF_FFFF n);
 236       mdl = ghost interval 0 (t'int n) }
 237
 238 end
 239
 240 module NQueensBits
 241
 242   use BitsSpec
 243   use ref.Ref
 244   use Solution
 245   use int.Int
 246
 247   val ghost col: ref solution  (* solution under construction *)
 248   (* val ghost k  : ref int       (* current row in the current solution *) *)
 249
 250   val ghost sol: ref solutions (* all solutions *)
 251   val ghost s  : ref int       (* next slot for a solution =
 252                                   number of solutions *)
 253
 254   let rec t (a b c: BitsSpec.t) (ghost k : int)
 255     requires { n <= size }
 256     requires { 0 <= k }
 257     requires { k + S.cardinal a.mdl = n }
 258     requires { !s >= 0 }
 259     requires { forall i: int. S.mem i a.mdl <->
 260         ( 0 <= i < n /\ forall j: int. 0 <= j < k ->  !col[j] <> i) }
 261     requires { forall i: int.  0 <= i < size ->
 262         ( not (S.mem i b.mdl) <->
 263           forall j: int. 0 <= j < k -> i - !col[j] <> k - j) }
 264     requires { forall i: int. 0 <= i < size ->
 265         ( not (S.mem i c.mdl) <->
 266           forall j: int. 0 <= j < k -> i - !col[j] <> j - k ) }
 267     requires { partial_solution k !col }
 268     variant { S.cardinal a.mdl }
 269     ensures { result = !s - old !s >= 0 }
 270     ensures { sorted !sol (old !s) !s }
 271     ensures { forall i:int. old !s <= i < !s -> solution !sol[i] /\ eq_prefix !col !sol[i] k }
 272     ensures { forall u: solution.
 273         solution u /\ eq_prefix !col u k ->
 274         exists i: int. old !s <= i < !s /\ eq_sol u !sol[i] }
 275     (* assigns *)
 276     ensures { eq_prefix (old !col) !col k }
 277     ensures { eq_prefix (old !sol) !sol (old !s) }
 278   = if not (is_empty a) then begin
 279     let e = ref (diff (diff a b) c) in
 280     (* first, you show that if u is a solution with the same k-prefix as col, then
 281        u[k] (the position of the queen on the row k) must belong to e *)
 282     assert { forall u:solution. solution u /\ eq_prefix !col u k -> S.mem u[k] !e.mdl };
 283     let f = ref 0 in
 284     let ghost min = ref (-1) in
 285     label L in
 286     while not (is_empty !e) do
 287       variant { S.cardinal !e.mdl }
 288       invariant { not (S.is_empty !e.mdl) -> !min < S.min_elt !e.mdl }
 289       invariant { !f = !s - (!s at L) >= 0 }
 290       invariant { S.subset !e.mdl (S.diff (S.diff a.mdl b.mdl) c.mdl) }
 291       invariant { partial_solution k !col }
 292       invariant { sorted !sol (!s at L) !s }
 293       invariant { forall i: int. S.mem i (!e.mdl at L) /\ not (S.mem i !e.mdl) -> i <= !min }
 294       invariant { forall i:int. (!s at L) <= i < !s -> solution !sol[i] /\ eq_prefix !col !sol[i] k /\ 0 <= !sol[i][k] <= !min }
 295       invariant { forall u: solution.
 296         (solution u /\ eq_prefix !col u k /\ 0 <= u[k] <= !min)
 297         ->
 298         S.mem u[k] (!e.mdl at L) && not (S.mem u[k] !e.mdl) &&
 299         exists i: int. (!s at L) <= i < !s /\ eq_sol u !sol[i] }
 300       (* assigns *)
 301       invariant { eq_prefix (!col at L) !col k }
 302       invariant { eq_prefix (!sol at L) !sol (!s at L) }
 303       label N in
 304       let d = rightmost_bit_trick !e min in
 305       ghost col := !col[k <- !min];
 306       assert { 0 <= !col[k] < size };
 307       assert { not (S.mem !col[k] b.mdl) };
 308       assert { not (S.mem !col[k] c.mdl) };
 309
 310       assert { eq_prefix (!col at L) !col k };
 311       assert { forall i: int. S.mem i a.mdl -> (forall j: int. 0 <= j < k ->  !col[j] <> i) };
 312       assert { forall i: int. S.mem i (S.remove (S.min_elt d.mdl) a.mdl) <-> (0 <= i < n /\ (forall j: int. 0 <= j < k + 1 ->  !col[j] <> i)) };
 313
 314       let ghost b' = mul2 (add_singleton b d) in
 315       assert { forall i: int.  0 <= i < size ->
 316         S.mem i b'.mdl -> (i = !min + 1 \/ S.mem (i - 1) b.mdl) && not (forall j:int. 0 <= j < k + 1 -> i - !col[j] <> k + 1 - j) };
 317
 318       let ghost c' = div2 (add_singleton c d) in
 319       assert { forall i: int.  0 <= i < size ->
 320         S.mem i c'.mdl -> (i = !min - 1 \/ (i + 1 < size /\ S.mem (i + 1) c.mdl)) && not (forall j:int. 0 <= j < k + 1 -> i - !col[j] <> j - k - 1) };
 321
 322       label M in
 323       f := !f + t (remove_singleton a d)
 324                   (mul2 (add_singleton b d)) (div2 (add_singleton c d)) (k + 1);
 325
 326       assert { forall i j. (!s at L) <= i < (!s at M) <= j < !s -> (eq_prefix !sol[i] !sol[j] k /\ !sol[i][k] <= (!min at N) < !min = !sol[j][k]) && lt_sol !sol[i] !sol[j]};
 327
 328       e := remove_singleton !e d
 329     done;
 330     assert { forall u:solution. solution u /\ eq_prefix !col u k -> S.mem u[k] (!e.mdl at L) && 0 <= u[k] <= !min  };
 331     !f
 332     end else begin
 333       ghost sol := !sol[!s <- !col];
 334       ghost s := !s + 1;
 335       1
 336     end
 337
 338   let queens (q: BV32.t)
 339     requires { BV32.t'int q = n }
 340     requires { BV32.ule q BV32.size_bv }
 341     requires { !s = 0 }
 342     ensures  { result = !s }
 343     ensures  { sorted !sol 0 !s }
 344     ensures  { forall u: solution.
 345       solution u <-> exists i: int. 0 <= i < result /\ eq_sol u !sol[i] }
 346     =
 347     t (below q) (empty()) (empty()) 0
 348
 349
 350   let test8 ()
 351     requires { size = 32 }
 352     requires { n = 8 }
 353   =
 354     s := 0;
 355     queens (BV32.of_int 8)
 356
 357 end