Commit b4aea4a1 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

In progress: bitwalker, n-queens

parent 9e9decde
......@@ -9,7 +9,45 @@ module Bitwalker
use bv.BVConverter_32_64 as C32_64
use bv.BVConverter_8_32 as C8_32
(* file missing in repository
use import mach.bv.BV
*)
val int8_check (a:int) : BV8.t
requires { 0 <= a < BV8.two_power_size }
ensures { BV8.to_uint result = a }
ensures { result = BV8.of_int a }
val int32_check (a:int) : BV32.t
requires { 0 <= a < BV32.two_power_size }
ensures { BV32.to_uint result = a }
ensures { result = BV32.of_int a }
val int64_check (a:int) : BV64.t
requires { 0 <= a < BV64.two_power_size }
ensures { BV64.to_uint result = a }
ensures { result = BV64.of_int a }
val add32_check (a b:BV32.t) : BV32.t
requires { 0 <= BV32.to_uint a + BV32.to_uint b < BV32.two_power_size }
ensures { BV32.to_uint result = BV32.to_uint a + BV32.to_uint b }
ensures { result = BV32.add a b }
val sub32_check (a b:BV32.t) : BV32.t
requires { 0 <= BV32.to_uint a - BV32.to_uint b < BV32.two_power_size }
ensures { BV32.to_uint result = BV32.to_uint a - BV32.to_uint b }
ensures { result = BV32.sub a b }
val sub8_check (a b:BV8.t) : BV8.t
requires { 0 <= BV8.to_uint a - BV8.to_uint b < BV8.two_power_size }
ensures { BV8.to_uint result = BV8.to_uint a - BV8.to_uint b }
ensures { result = BV8.sub a b }
val udiv32_check (a b:BV32.t) : BV32.t
ensures { result = BV32.udiv a b }
val urem32_check (a b:BV32.t) : BV32.t
ensures { result = BV32.urem a b }
function nth8_stream (stream : array BV8.t) (pos : int) : bool =
BV8.nth stream[div pos 8] (7 - mod pos 8)
......
(**
{1 N-queens problem}
Verification of the following 2-lines C program solving the N-queens problem:
{h <pre>
t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
</pre>}
*)
(**
{2 finite sets of integers, with succ and pred operations }
*)
theory S
use export set.Fsetint
function succ (set int) : set int
axiom succ_def:
forall s: set int, i: int. mem i (succ s) <-> i >= 1 /\ mem (i-1) s
function pred (set int) : set int
axiom pred_def:
forall s: set int, i: int. mem i (pred s) <-> i >= 0 /\ mem (i+1) s
end
(** {2 first task: termination of the algorithm} *)
module NQueensSetsTermination
use import S
use import ref.Refint
let rec t (a b c : set int)
variant { cardinal a } =
if not (is_empty a) then begin
let e = ref (diff (diff a b) c) in
let f = ref 0 in
'L:
while not (is_empty !e) do
variant { cardinal !e }
invariant { subset !e (diff (diff a b) c) }
let d = min_elt !e in
f += t (remove d a) (succ (add d b)) (pred (add d c));
e := remove d !e
done;
!f
end
else 1
end
(** {2 Formalization of the set of solutions of the N-queens problem} *)
theory Solution
use import int.Int
use export map.Map
(** the number of queens *)
constant n : int
type solution = map int int
(** solutions [t] and [u] have the same prefix [[0..i[] *)
predicate eq_prefix (t u: map int 'a) (i: int) =
forall k: int. 0 <= k < i -> t[k] = u[k]
predicate eq_sol (t u: solution) = eq_prefix t u n
(** [s] stores a partial solution, for the rows [0..k-1] *)
predicate partial_solution (k: int) (s: solution) =
forall i: int. 0 <= i < k ->
0 <= s[i] < n /\
(forall j: int. 0 <= j < i -> s[i] <> s[j] /\
s[i]-s[j] <> i-j /\
s[i]-s[j] <> j-i)
predicate solution (s: solution) = partial_solution n s
lemma partial_solution_eq_prefix:
forall u t: solution, k: int.
partial_solution k t -> eq_prefix t u k -> partial_solution k u
predicate lt_sol (s1 s2: solution) =
exists i: int. 0 <= i < n /\ eq_prefix s1 s2 i /\ s1[i] < s2[i]
type solutions = map int solution
(** [s[a..b[] is sorted for [lt_sol] *)
predicate sorted (s: solutions) (a b: int) =
forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]
(** a sorted array of solutions contains no duplicate *)
lemma no_duplicate:
forall s: solutions, a b: int. sorted s a b ->
forall i j: int. a <= i < j < b -> not (eq_sol s[i] s[j])
end
(**
{2 Abstract version of the code using sets (not ints)
*)
module NQueensSets
use import S
use import ref.Refint
use import Solution
val ghost col: ref solution (** solution under construction *)
val ghost k : ref int (** current row in the current solution *)
val ghost sol: ref solutions (** all solutions *)
val ghost s : ref int (** next slot for a solution
= current number of solutions *)
let rec t (a b c : set int)
variant { cardinal a }
requires { 0 <= !k }
requires { !k + cardinal a = n }
requires { !s >= 0 }
requires { forall i: int. mem i a <->
( 0 <= i < n /\ forall j: int. 0 <= j < !k -> !col[j] <> i) }
requires { forall i: int. i >= 0 ->
( not (mem i b) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k)) }
requires { forall i: int. i >= 0 ->
( not (mem i c) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j)) }
requires { partial_solution !k !col }
ensures { result = !s - old !s >= 0 }
ensures { !k = old !k }
ensures { sorted !sol (old !s) !s }
ensures { forall t: solution.
( (solution t /\ eq_prefix !col t !k) <->
(exists i: int. old !s <= i < !s /\ eq_sol t !sol[i])) }
(* assigns *)
ensures { eq_prefix (old !col) !col !k }
ensures { eq_prefix (old !sol) !sol (old !s) }
= if not (is_empty a) then begin
let e = ref (diff (diff a b) c) in
let f = ref 0 in
'L:
while not (is_empty !e) do
variant { cardinal !e }
invariant { !f = !s - at !s 'L >= 0 }
invariant { !k = at !k 'L }
invariant { subset !e (diff (diff a b) c) }
invariant { partial_solution !k !col }
invariant { sorted !sol (at !s 'L) !s }
invariant { forall i j: int.
mem i (diff (at !e 'L) !e) /\ mem j !e -> i < j }
invariant { forall t: solution.
(solution t /\ eq_prefix !col t !k /\ mem t[!k] (diff (at !e 'L) !e))
<->
(exists i: int. (at !s 'L) <= i < !s /\ eq_sol t !sol[i]) }
(* assigns *)
invariant { eq_prefix (at !col 'L) !col !k }
invariant { eq_prefix (at !sol 'L) !sol (at !s 'L) }
let d = min_elt !e in
ghost col := !col[!k <- d];
ghost incr k;
f += t (remove d a) (succ (add d b)) (pred (add d c));
ghost decr k;
e := remove d !e
done;
!f
end else begin
ghost sol := !sol[!s <- !col];
ghost incr s;
1
end
let queens (q: int)
requires { 0 <= q = n }
requires { !s = 0 }
requires { !k = 0 }
ensures { result = !s }
ensures { sorted !sol 0 !s }
ensures { forall t: solution.
solution t <-> (exists i: int. 0 <= i < result /\ eq_sol t !sol[i])
}
=
t (interval 0 q) empty empty
end
(** {2 More realistic code with bitwise operations} *)
module BitsSpec
use import S
constant size : int = 32
type t = {
ghost mdl: set int;
}
val empty () : t
ensures { is_empty result.mdl }
val is_empty (x:t) : bool
ensures { result <-> is_empty x.mdl }
val remove_singleton (a b: t) : t
requires { b.mdl = singleton (min_elt b.mdl) }
requires { mem (min_elt b.mdl) a.mdl }
ensures { result.mdl = remove (min_elt b.mdl) a.mdl }
val add_singleton (a b: t) : t
requires { b.mdl = singleton (min_elt b.mdl) }
(* requires { not (mem (min_elt b.mdl) a.mdl) } *)
(* this is not required if the implementation uses or instead of add *)
ensures { result.mdl = S.add (min_elt b.mdl) a.mdl }
val mul2 (a: t) : t
ensures { result.mdl = remove size (succ a.mdl) }
val div2 (a: t) : t
ensures { result.mdl = pred a.mdl }
val diff (a b: t) : t
ensures { result.mdl = diff a.mdl b.mdl }
use import ref.Ref
val rightmost_bit_trick (a: t) (ghost min : ref int) : t
requires { not (is_empty a.mdl) }
writes { min }
ensures { !min = min_elt a.mdl }
ensures { result.mdl = singleton !min }
use bv.BV32
val below (n: BV32.t) : t
requires { BV32.ule n (BV32.of_int 32) }
ensures { result.mdl = interval 0 (BV32.to_uint n) }
end
module Bits "the 1-bits of an integer, as a set of integers"
use import S
use import bv.BV32
constant size : int = 32
type t = {
bv : BV32.t;
ghost mdl: set int;
}
invariant {
forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl
}
let empty () : t
ensures { is_empty result.mdl }
=
{ bv = zero; mdl = empty }
let is_empty (x:t) : bool
ensures { result <-> is_empty x.mdl }
=
assert {is_empty x.mdl -> BV32.eq x.bv zero};
x.bv = zero
let remove_singleton (a b: t) : t
requires { b.mdl = singleton (min_elt b.mdl) }
requires { mem (min_elt b.mdl) a.mdl }
ensures { result.mdl = remove (min_elt b.mdl) a.mdl }
=
{ bv = bw_and a.bv (bw_not b.bv);
mdl = remove (min_elt b.mdl) a.mdl }
(* { bv = sub a.bv b.bv; mdl = remove (min_elt b.mdl) a.mdl } *)
let add_singleton (a b: t) : t
requires { b.mdl = singleton (min_elt b.mdl) }
(* requires { not (mem (min_elt b.mdl) a.mdl) } *)
(* this is not required if the implementation uses or instead of add *)
ensures { result.mdl = S.add (min_elt b.mdl) a.mdl }
=
{ bv = bw_or a.bv b.bv;
mdl = S.add (min_elt b.mdl) a.mdl }
(* { bv = add a.bv b.bv; mdl = add (min_elt b.mdl) a.mdl } *)
let mul2 (a: t) : t
ensures { result.mdl = remove size (succ a.mdl) }
=
{ bv = lsl_bv a.bv (of_int 1); mdl = remove size (succ a.mdl) }
let div2 (a: t) : t
ensures { result.mdl = pred a.mdl }
=
{ bv = lsr_bv a.bv (of_int 1); mdl = pred a.mdl }
let diff (a b: t) : t
ensures { result.mdl = diff a.mdl b.mdl }
=
{ bv = bw_and a.bv (bw_not b.bv);
mdl = diff a.mdl b.mdl }
lemma not_neg: forall n. add (bw_not n) (of_int 1) = neg n
let rightmost_bit_trick (a: t) : t
requires { not (is_empty a.mdl) }
ensures { result.mdl = singleton (min_elt a.mdl) }
=
let res = bw_and a.bv (neg a.bv) in
let ghost n = min_elt a.mdl in
let ghost n_bv = of_int n in
assert {forall i. ult i n_bv -> not (nth_bv a.bv i)};
assert {nth_bv a.bv n_bv};
assert {forall i. ult i n_bv -> nth_bv (bw_not a.bv) i};
assert {
let mask = lsr_bv ones (BV32.sub BV32.size (BV32.add n_bv (BV32.of_int 1))) in
bw_and a.bv mask = mask
};
assert {not (nth_bv (bw_not a.bv) n_bv)};
assert {nth_bv (neg a.bv) n_bv};
assert {forall i. 0 <= i < n -> not (nth a.bv i)};
assert {nth a.bv n};
assert {not (nth (bw_not a.bv) n)};
assert {forall i. 0 <= i < n -> nth (bw_not a.bv) i};
assert {forall i. n < i < 32 -> nth (bw_not a.bv) i = not (nth a.bv i)};
assert {nth (neg a.bv) n};
assert {forall i. n < i < 32 -> nth (BV32.neg a.bv) i = not (nth a.bv i)};
assert {forall i. 0 <= i < n -> not (nth res i)};
assert {forall i. n < i < 32 -> not (nth res i)};
assert {nth res n};
{ bv = res;
mdl = singleton n }
let below (n: BV32.t) : t
requires { BV32.ule n (BV32.of_int 32) }
ensures { result.mdl = interval 0 (to_uint n) }
=
{ bv = bw_not (lsl_bv ones n);
mdl = interval 0 (to_uint n) }
end
(*** Work in progress *)
module NQueensBits
use import BitsSpec
use import ref.Ref
use import Solution
use import int.Int
val ghost col: ref solution (* solution under construction *)
val ghost k : ref int (* current row in the current solution *)
val ghost sol: ref solutions (* all solutions *)
val ghost s : ref int (* next slot for a solution =
number of solutions *)
let rec t (a b c: BitsSpec.t)
requires { 0 <= !k }
requires { !k + S.cardinal a.mdl = n }
requires { !s >= 0 }
requires { forall i: int. S.mem i a.mdl <->
( 0 <= i < n /\ forall j: int. 0 <= j < !k -> !col[j] <> i) }
requires { forall i: int. i >= 0 ->
( not (S.mem i b.mdl) <->
forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k ) }
requires { forall i: int. i >= 0 ->
( not (S.mem i c.mdl) <->
forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j ) }
requires { partial_solution !k !col }
variant { S.cardinal a.mdl }
ensures { result = !s - old !s >= 0 }
ensures { !k = old !k }
ensures { sorted !sol (old !s) !s }
ensures { forall u: solution.
solution u /\ eq_prefix !col u !k <->
exists i: int. old !s <= i < !s /\ eq_sol u !sol[i] }
(* assigns *)
ensures { eq_prefix (old !col) !col !k }
ensures { eq_prefix (old !sol) !sol (old !s) }
= if not (is_empty a) then begin
let e = ref (diff (diff a b) c) in
let f = ref 0 in
'L:
while not (is_empty !e) do
variant { S.cardinal !e.mdl }
invariant { !f = !s - at !s 'L >= 0 }
invariant { !k = at !k 'L }
invariant { S.subset !e.mdl (S.diff (S.diff a.mdl b.mdl) c.mdl) }
invariant { partial_solution !k !col }
invariant { sorted !sol (at !s 'L) !s }
invariant { forall i j: int.
S.mem i (S.diff (at !e.mdl 'L) !e.mdl) /\ S.mem j !e.mdl -> i < j }
invariant { forall u: solution.
(solution u /\ eq_prefix !col u !k /\
S.mem u[!k] (S.diff (at !e.mdl 'L) !e.mdl))
<->
exists i: int. (at !s 'L) <= i < !s /\ eq_sol u !sol[i] }
(* assigns *)
invariant { eq_prefix (at !col 'L) !col !k }
invariant { eq_prefix (at !sol 'L) !sol (at !s 'L) }
let ghost min = ref 0 in
let d = rightmost_bit_trick !e min in
ghost col := !col[!k <- !min];
ghost k := !k + 1;
f := !f + t (remove_singleton a d)
(mul2 (add_singleton b d)) (div2 (add_singleton c d));
ghost k := !k - 1;
e := remove_singleton !e d
done;
!f
end else begin
ghost sol := !sol[!s <- !col];
ghost s := !s + 1;
1
end
let queens (q: BV32.t)
requires { BV32.to_uint q = n }
requires { BV32.ule q BV32.size }
requires { !s = 0 }
requires { !k = 0 }
ensures { result = !s }
ensures { sorted !sol 0 !s }
ensures { forall u: solution.
solution u <-> exists i: int. 0 <= i < result /\ eq_sol u !sol[i] }
=
t (below q) (empty()) (empty())
let test8 ()
requires { size = 32 }
requires { n = 8 }
=
s := 0; k := 0;
queens (BV32.of_int 8)
end
(***)
\ No newline at end of file
This diff is collapsed.
......@@ -108,10 +108,10 @@ module NQueensSets
requires { 0 <= !k /\ !k + cardinal a = n /\ !s >= 0 /\
(forall i: int. mem i a <->
(0<=i<n /\ forall j: int. 0 <= j < !k -> !col[j] <> i)) /\
(forall i: int. i>=0 -> not (mem i b) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k)) /\
(forall i: int. i>=0 -> not (mem i c) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j)) /\
(forall i: int. i>=0 -> (not (mem i b) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k))) /\
(forall i: int. i>=0 -> (not (mem i c) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j))) /\
partial_solution !k !col }
ensures { result = !s - old !s >= 0 /\ !k = old !k /\
sorted !sol (old !s) !s /\
......@@ -162,6 +162,8 @@ module NQueensSets
end
(* obsolete : see in_progress/nqueens.mlw
(** {2 More realistic code with bitwise operations} *)
module BitsSpec
......@@ -276,7 +278,6 @@ module Bits "the 1-bits of an integer, as a set of integers"
lemma not_neg: forall n. add (bw_not n) (of_int 1) = neg n
(***
let rightmost_bit_trick (a: t) : t
requires { not (is_empty a.mdl) }
ensures { result.mdl = singleton (min_elt a.mdl) }
......@@ -306,7 +307,7 @@ module Bits "the 1-bits of an integer, as a set of integers"
assert {nth res n};
{ bv = res;
mdl = singleton n }
***)
let below (n: BV32.t) : t
requires { BV32.ule n (BV32.of_int 32) }
......@@ -316,7 +317,7 @@ module Bits "the 1-bits of an integer, as a set of integers"
mdl = interval 0 (to_uint n) }
end
(*** Work in progress
module NQueensBits
use import BitsSpec
......@@ -332,52 +333,59 @@ module NQueensBits
number of solutions *)
let rec t (a b c: BitsSpec.t)
variant { S.cardinal a.mdl }
requires { 0 <= !k /\ !k + S.cardinal a.mdl = n /\ !s >= 0 /\
(forall i: int. S.mem i a.mdl <->
(0<=i<n /\ forall j: int. 0 <= j < !k -> !col[j] <> i)) /\
(forall i: int. i>=0 -> not (S.mem i b.mdl) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k)) /\
(forall i: int. i>=0 -> not (S.mem i c.mdl) <->
(forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j)) /\
partial_solution !k !col }
ensures { result = !s - old !s >= 0 /\ !k = old !k /\
sorted !sol (old !s) !s /\
(forall u: solution.
((solution u /\ eq_prefix !col u !k) <->
(exists i: int. old !s <= i < !s /\ eq_sol u !sol[i]))) /\
(* assigns *)
eq_prefix (old !col) !col !k /\
eq_prefix (old !sol) !sol (old !s) }
requires { 0 <= !k }
requires { !k + S.cardinal a.mdl = n }
requires { !s >= 0 }
requires { forall i: int. S.mem i a.mdl <->
( 0 <= i < n /\ forall j: int. 0 <= j < !k -> !col[j] <> i) }
requires { forall i: int. i >= 0 ->
( not (S.mem i b.mdl) <->
forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k ) }
requires { forall i: int. i >= 0 ->
( not (S.mem i c.mdl) <->
forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j ) }
requires { partial_solution !k !col }
variant { S.cardinal a.mdl }
ensures { result = !s - old !s >= 0 }
ensures { !k = old !k }
ensures { sorted !sol (old !s) !s }
ensures { forall u: solution.
solution u /\ eq_prefix !col u !k <->
exists i: int. old !s <= i < !s /\ eq_sol u !sol[i] }
(* assigns *)
ensures { eq_prefix (old !col) !col !k }
ensures { eq_prefix (old !sol) !sol (old !s) }
= if not (is_empty a) then begin
let e = ref (diff (diff a b) c) in
let f = ref 0 in
'L:while not (is_empty !e) do
invariant {
!f = !s - at !s 'L >= 0 /\ !k = at !k 'L /\
S.subset !e.mdl (S.diff (S.diff a.mdl b.mdl) c.mdl) /\
partial_solution !k !col /\
sorted !sol (at !s 'L) !s /\
(forall i j: int. S.mem i (S.diff (at !e.mdl 'L) !e.mdl) ->
S.mem j !e.mdl -> i < j) /\
(forall u: solution.
(solution u /\ eq_prefix !col u !k /\
let e = ref (diff (diff a b) c) in
let f = ref 0 in
'L:
while not (is_empty !e) do
variant { S.cardinal !e.mdl }
invariant { !f = !s - at !s 'L >= 0 }
invariant { !k = at !k 'L }
invariant { S.subset !e.mdl (S.diff (S.diff a.mdl b.mdl) c.mdl) }
invariant { partial_solution !k !col }
invariant { sorted !sol (at !s 'L) !s }
invariant { forall i j: int.
S.mem i (S.diff (at !e.mdl 'L) !e.mdl) /\ S.mem j !e.mdl -> i < j }
invariant { forall u: solution.
(solution u /\ eq_prefix !col u !k /\
S.mem u[!k] (S.diff (at !e.mdl 'L) !e.mdl))
<->
(exists i: int. (at !s 'L) <= i < !s /\ eq_sol u !sol[i])) /\
(* assigns *)
eq_prefix (at !col 'L) !col !k /\
eq_prefix (at !sol 'L) !sol (at !s 'L) }
variant { S.cardinal !e.mdl }
let ghost min = ref 0 in
let d = rightmost_bit_trick !e min in
ghost col := !col[!k <- !min];
ghost k := !k + 1;
f := !f + t (remove_singleton a d) (mul2 (add_singleton b d)) (div2 (add_singleton c d));
ghost k := !k - 1;
e := remove_singleton !e d
done;
!f
<->
exists i: int. (at !s 'L) <= i < !s /\ eq_sol u !sol[i] }
(* assigns *)
invariant { eq_prefix (at !col 'L) !col !k }
invariant { eq_prefix (at !sol 'L) !sol (at !s 'L) }
let ghost min = ref 0 in
let d = rightmost_bit_trick !e min in
ghost col := !col[!k <- !min];
ghost k := !k + 1;
f := !f + t (remove_singleton a d)
(mul2 (add_singleton b d)) (div2 (add_singleton c d));
ghost k := !k - 1;
e := remove_singleton !e d
done;
!f
end else begin
ghost sol := !sol[!s <- !col];