added solutions for VerifyThis 2017

parent af08d5c4
(* VerifyThis 2017 challenge 2
(**
Maximum-sum submatrix (2D version of Kadane's algorithm)
{1 VerifyThis @ ETAPS 2017 competition
Challenge 2: Maximum-sum submatrix}
See https://formal.iti.kit.edu/ulbrich/verifythis2017/
Author: Jean-Christophe Filliâtre (CNRS)
*)
(* note: this is a 2D-version of maximum-sum subarray, for which several
verified implementations can be found in maximum_subarray.mlw,
including Kadane's linear algorithm *)
module Kadane2D
use import int.Int
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../kadane_2d.mlw">
<file name="../verifythis_2017_maximum_sum_submatrix.mlw">
<theory name="Kadane2D" sum="09fbb7ac5139de301e5efc628ae0287e">
<goal name="VC maximum_submatrix" expl="VC for maximum_submatrix">
<transf name="split_goal_wp">
......
(**
{1 VerifyThis @ ETAPS 2017 competition
Challenge 3: Odd-Even Transposition Sort}
See https://formal.iti.kit.edu/ulbrich/verifythis2017/
Author: Jean-Christophe Filliâtre (CNRS)
*)
(* note: this is only a solution for the sequential (single processor) version
of the challenge *)
module Challenge3
use import int.Int
use import int.Sum
use import int.NumOf
use import int.ComputerDivision
use import ref.Refint
use import array.Array
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
(* odd-sorted up to n exclusive *)
predicate odd_sorted (a: array int) (n: int) =
forall i. 0 <= i -> 2*i + 2 < n -> a[2*i+1] <= a[2*i+2]
(* even-sorted up to n exclusive *)
predicate even_sorted (a: array int) (n: int) =
forall i. 0 <= i -> 2*i + 1 < n -> a[2*i] <= a[2*i+1]
let lemma odd_even_sorted (a: array int) (n: int)
requires { 0 <= n <= length a }
requires { odd_sorted a n }
requires { even_sorted a n }
ensures { sorted_sub a 0 n }
= if n > 0 && length a > 0 then
for i = 1 to n - 1 do
invariant { sorted_sub a 0 i }
assert { forall j. 0 <= j < i -> a[j] <= a[i]
by a[i-1] <= a[i]
by i-1 = 2 * div (i-1) 2 \/
i-1 = 2 * div (i-1) 2 + 1 }
done
(* to prove termination, we count the total number of inversions *)
predicate inversion (a: array int) (i j: int) =
a[i] > a[j]
function inversions_for (a: array int) (i: int) : int =
numof (inversion a i) i (length a)
function inversions (a: array int) : int =
sum (inversions_for a) 0 (length a)
(* the key lemma to prove termination: whenever we swap two consecutive
values that are ill-sorted, the total number of inversions decreases *)
let lemma exchange_inversion (a1 a2: array int) (i0: int)
requires { 0 <= i0 < length a1 - 1 }
requires { a1[i0] > a1[i0 + 1] }
requires { exchange a1 a2 i0 (i0 + 1) }
ensures { inversions a2 < inversions a1 }
= assert { inversion a1 i0 (i0+1) };
assert { not (inversion a2 i0 (i0+1)) };
assert { forall i. 0 <= i < i0 ->
inversions_for a2 i = inversions_for a1 i
by numof (inversion a2 i) i (length a2)
= numof (inversion a2 i) i i0
+ numof (inversion a2 i) i0 (i0+1)
+ numof (inversion a2 i) (i0+1) (i0+2)
+ numof (inversion a2 i) (i0+2) (length a2)
/\ numof (inversion a1 i) i (length a1)
= numof (inversion a1 i) i i0
+ numof (inversion a1 i) i0 (i0+1)
+ numof (inversion a1 i) (i0+1) (i0+2)
+ numof (inversion a1 i) (i0+2) (length a1)
/\ numof (inversion a2 i) i0 (i0+1)
= numof (inversion a1 i) (i0+1) (i0+2)
/\ numof (inversion a2 i) (i0+1) (i0+2)
= numof (inversion a1 i) i0 (i0+1)
/\ numof (inversion a2 i) i i0 = numof (inversion a1 i) i i0
/\ numof (inversion a2 i) (i0+2) (length a2)
= numof (inversion a1 i) (i0+2) (length a1)
};
assert { forall i. i0 + 1 < i < length a1 ->
inversions_for a2 i = inversions_for a1 i };
assert { inversions_for a2 i0 = inversions_for a1 (i0+1)
by numof (inversion a1 (i0+1)) (i0+2) (length a1)
= numof (inversion a2 i0 ) (i0+2) (length a1) };
assert { 1 + inversions_for a2 (i0+1) = inversions_for a1 i0
by numof (inversion a1 i0) i0 (length a1)
= numof (inversion a1 i0) (i0+1) (length a1)
= 1 + numof (inversion a1 i0) (i0+2) (length a1) };
let sum_decomp (a: array int) (i j k: int)
requires { 0 <= i <= j <= k <= length a = length a1 }
ensures { sum (inversions_for a) i k =
sum (inversions_for a) i j + sum (inversions_for a) j k }
= () in
let decomp (a: array int)
requires { length a = length a1 }
ensures { inversions a = sum (inversions_for a) 0 i0
+ inversions_for a i0
+ inversions_for a (i0+1)
+ sum (inversions_for a) (i0+2) (length a) }
= sum_decomp a 0 i0 (length a);
sum_decomp a i0 (i0+1) (length a);
sum_decomp a (i0+1) (i0+2) (length a);
in
decomp a1; decomp a2;
()
(* note: program variable "sorted" renamed into "is_sorted"
(clash with library predicate "sorted" on arrays) *)
let odd_even_transposition_sort (a: array int)
ensures { sorted a }
ensures { permut_all (old a) a }
= let is_sorted = ref false in
while not !is_sorted do
invariant { permut_all (old a) a }
invariant { !is_sorted -> sorted a }
variant { if !is_sorted then 0 else 1, inversions a }
is_sorted := true;
let i = ref 1 in
let ghost half_i = ref 0 in
label L in
while !i < length a - 1 do
invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i + 1 }
invariant { permut_all (old a) a }
invariant { odd_sorted a !i }
invariant { if !is_sorted then inversions a = inversions (a at L)
else inversions a < inversions (a at L) }
variant { length a - !i }
if a[!i] > a[!i+1] then begin
swap a !i (!i+1);
is_sorted := false;
end;
i := !i + 2;
ghost half_i := !half_i + 1
done;
assert { odd_sorted a (length a) };
i := 0;
ghost half_i := 0;
while !i < length a - 1 do
invariant { 0 <= !half_i /\ 0 <= !i = 2 * !half_i }
invariant { 0 <= !i }
invariant { permut_all (old a) a }
invariant { !is_sorted -> odd_sorted a (length a) }
invariant { even_sorted a !i }
invariant { if !is_sorted then inversions a = inversions (a at L)
else inversions a < inversions (a at L) }
invariant { !is_sorted \/ inversions a < inversions (a at L) }
variant { length a - !i }
if a[!i] > a[!i+1] then begin
swap a !i (!i+1);
is_sorted := false;
end;
i := !i + 2;
ghost half_i := !half_i + 1
done;
assert { !is_sorted -> even_sorted a (length a) }
done
end
(**
{1 VerifyThis @ ETAPS 2017 competition
Challenge 1: Pair Insertion Sort}
See https://formal.iti.kit.edu/ulbrich/verifythis2017/
Author: Jean-Christophe Filliâtre (CNRS)
*)
module Challenge1
use import int.Int
use import ref.Refint
use import array.Array
use import array.ArrayPermut
let pair_insertion_sort (a: array int)
ensures { forall k l. 0 <= k <= l < length a -> a[k] <= a[l] }
ensures { permut_all (old a) a }
= let i = ref 0 in (* i is running index (inc by 2 every iteration)*)
while !i < length a - 1 do
invariant { 0 <= !i <= length a }
invariant { forall k l. 0 <= k <= l < !i -> a[k] <= a[l] }
invariant { permut_all (old a) a }
variant { length a - !i }
let x = ref a[!i] in (* let x and y hold the next to elements in A *)
let y = ref a[!i + 1] in
if !x < !y then (* ensure that x is not smaller than y *)
begin let tmp = !x in x := !y; y := tmp end (* swap x and y *)
else begin
label L in
assert { exchange (a at L) a[(!i-1)+1 <- !y][(!i-1)+2 <- !x]
((!i-1)+1) ((!i-1)+2) }
end;
let j = ref (!i - 1) in
(* j is the index used to find the insertion point *)
while !j >= 0 && a[!j] > !x do (* find the insertion point for x *)
invariant { -1 <= !j < !i }
invariant { forall k l.
0 <= k <= l <= !j -> a[k] <= a[l] }
invariant { forall k l.
0 <= k <= !j -> !j+2 < l < !i+2 -> a[k] <= a[l] }
invariant { forall k l.
!j+2 < k <= l < !i+2 -> a[k] <= a[l] }
invariant { forall l.
!j+2 < l < !i+2 -> !x < a[l] }
invariant { permut_all (old a) a[!j+1 <- !y][!j+2 <- !x] }
variant { !j }
label L in
a[!j + 2] <- a[!j]; (* shift existing content by 2 *)
assert { exchange (a at L)[!j+2 <- !x] a[!j <- !x] !j (!j + 2) };
assert { exchange (a at L)[!j+1 <- !y][!j+2 <- !x]
a[!j+1 <- !y][!j <- !x] !j (!j + 2) };
assert { exchange (a at L)[!j+1 <- !y][!j+2 <- a[!j]][!j <- !x]
a[!j <- !y][!j+1 <- !x][!j+2 <- a[!j]] !j (!j + 1) };
j := !j - 1
done;
a[!j + 2] <- !x; (* store x at its insertion place *)
(* A[j+1] is an available space now *)
while !j >= 0 && a[!j] > !y do (* #ind the insertion point for y *)
invariant { -1 <= !j < !i }
invariant { forall k l.
0 <= k <= l <= !j -> a[k] <= a[l] }
invariant { forall k l.
0 <= k <= !j -> !j+1 < l < !i+2 -> a[k] <= a[l] }
invariant { forall k l.
!j+1 < k <= l < !i+2 -> a[k] <= a[l] }
invariant { forall l.
!j+1 < l < !i+2 -> !y <= a[l] }
invariant { permut_all (old a) a[!j+1 <- !y] }
variant { !j }
label L in
a[!j + 1] <- a[!j]; (* shift existing content by 1 *)
assert { exchange (a at L)[!j+1 <- !y] a[!j <- !y] !j (!j + 1) };
j := !j - 1
done;
a[!j + 1] <- !y; (* store y at its insertion place *)
i := !i + 2
done;
if !i = length a - 1 then begin (* if length(A) is odd, an extra *)
let y = a[!i] in (* single insertion is needed for *)
let j = ref (!i - 1) in (* the last element *)
while !j >= 0 && a[!j] > y do
invariant { -1 <= !j < !i }
invariant { forall k l.
0 <= k <= l <= !j -> a[k] <= a[l] }
invariant { forall k l.
0 <= k <= !j -> !j+1 < l < length a -> a[k] <= a[l] }
invariant { forall k l.
!j+1 < k <= l < length a -> a[k] <= a[l] }
invariant { forall l.
!j+1 < l < length a -> y < a[l] }
invariant { permut_all (old a) a[!j+1 <- y] }
variant { !j }
label L in
a[!j+1] <- a[!j];
assert { exchange (a at L)[!j+1 <- y] a[!j <- y] !j (!j + 1) };
j := !j - 1
done;
a[!j + 1] <- y
end
end
This diff is collapsed.
(**
{1 VerifyThis @ ETAPS 2017 competition
Challenge 4: Tree Buffer}
See https://formal.iti.kit.edu/ulbrich/verifythis2017/
Author: Jean-Christophe Filliâtre (CNRS)
*)
(* default implementation *)
module Spec
use export int.Int
use export list.List
type buf 'a = { h: int; xs: list 'a }
let rec function take (n: int) (l: list 'a) : list 'a =
match l with
| Nil -> Nil
| Cons x xs -> if n = 0 then Nil
else Cons x (take (n-1) xs) end
let function empty (h: int) : buf 'a =
{ h = h; xs = Nil }
let function add (x: 'a) (b: buf 'a) : buf 'a =
{ b with xs = Cons x b.xs }
let function get (b: buf 'a) : list 'a =
take b.h b.xs
(* the following lemma is useful to verify both Caterpillar and
RealTime implementations below *)
use import list.Append
use import list.Length
let rec lemma take_lemma (l1 l2 l3: list 'a) (n: int)
requires { 0 <= n <= length l1 }
ensures { take n (l1 ++ l2) = take n (l1 ++ l3) }
variant { l1 }
= match l1 with Nil -> ()
| Cons _ ll1 -> if n > 0 then take_lemma ll1 l2 l3 (n-1) end
end
(* task 1 *)
module Caterpillar
use import Spec
use import list.Append
use import list.Length
type cat 'a = {
ch: int;
xs: list 'a;
xs_len: int;
ys: list 'a;
ghost b: buf 'a; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
}
(* for the three operations, the postcondition uses the default
implementation *)
let cat_empty (h: int) : cat 'a
requires { 0 < h }
ensures { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }
let cat_add (x: 'a) (c: cat 'a) : cat 'a
ensures { result.b = add x c.b }
= if c.xs_len = c.ch - 1 then
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }
let cat_get (c: cat 'a) : list 'a
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)
end
(* task 2 *)
(* important note: Why3 assumes a garbage collector and so it makes
little sense to implement the real time solution in Why3.
Yet I stayed close to the C++ code, with a queue to_delete where
lists are added when discarded and then destroyed progressively
(at most two conses at a time) in process_queue.
The C++ code seems to be missing the insertion into to_delete,
which I added to rt_add; see my comment below.
*)
module RealTime
use import Spec
use import list.Append
use import list.Length
(* For technical reasons, the global queue cannot contain
polymorphic values, to we assume values to be of some
abstract type "elt". Anyway, the C++ code assumes integer
elements. *)
type elt
(* not different from the Caterpillar implementation
replacing 'a with elt everywhere *)
type rt = {
ch: int;
xs: list elt;
xs_len: int;
ys: list elt;
ghost b: buf elt; (* the model is the default implementation *)
} invariant {
b.h = ch /\
xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
}
(* garbage collection *)
use queue.Queue as Q
(* note: when translating Why3 to OCaml, this module is mapped
to OCaml's Queue module, where push and pop are O(1) *)
val to_delete: Q.t (list elt)
let de_allocate (l: list elt)
= match l with Nil -> () | Cons _ xs -> Q.push xs to_delete end
let process_queue ()
= try
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete);
if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete)
with Q.Empty -> absurd end
(* no difference wrt Caterpillar *)
let rt_empty (h: int) : rt
requires { 0 < h }
ensures { result.b = empty h }
= { ch = h; xs = Nil; xs_len = 0; ys = Nil;
b = empty h }
(* no difference wrt Caterpillar *)
let rt_get (c: rt) : list elt
ensures { result = get c.b }
= take c.ch (c.xs ++ c.ys)
(* this is where we introduce explicit garbage collection
1. process_queue is called first (as in the C++ code)
2. when ys is discarded, it is added to the queue (which
seems to be missing in the C++ code) *)
let rt_add (x: elt) (c: rt) : rt
ensures { result.b = add x c.b }
= process_queue ();
if c.xs_len = c.ch - 1 then begin
Q.push c.ys to_delete;
{ c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
b = add x c.b }
end else
{ c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
b = add x c.b }
end
(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
(* this is a prelude for Alt-Ergo integer arithmetic *)
logic match_bool : bool, 'a, 'a -> 'a
axiom match_bool_True :
(forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
axiom match_bool_False :
(forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))
axiom CompatOrderMult :
(forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
((x * z) <= (y * z)))))
type 'a list
logic Nil : 'a list
logic Cons : 'a, 'a list -> 'a list
logic match_list : 'a list, 'a1, 'a1 -> 'a1
axiom match_list_Nil :
(forall z:'a. forall z1:'a. (match_list((Nil : 'a1 list), z, z1) = z))
axiom match_list_Cons :
(forall z:'a. forall z1:'a. forall u:'a1. forall u1:'a1 list.
(match_list(Cons(u, u1), z, z1) = z1))
logic index_list : 'a list -> int
axiom index_list_Nil : (index_list((Nil : 'a list)) = 0)
axiom index_list_Cons :
(forall u:'a. forall u1:'a list [Cons(u, u1)]. (index_list(Cons(u,
u1)) = 1))
logic Cons_proj_1 : 'a list -> 'a
axiom Cons_proj_1_def :
(forall u:'a. forall u1:'a list. (Cons_proj_1(Cons(u, u1)) = u))
logic Cons_proj_2 : 'a list -> 'a list
axiom Cons_proj_2_def :
(forall u:'a. forall u1:'a list. (Cons_proj_2(Cons(u, u1)) = u1))
axiom list_inversion :
(forall u:'a list. ((u = (Nil : 'a list)) or (u = Cons(Cons_proj_1(u),
Cons_proj_2(u)))))
predicate is_nil(l: 'a list) =
(forall x:'a. forall x1:'a list. (not (l = Cons(x, x1))))
axiom is_nil_spec : (forall l:'a list. (is_nil(l) -> (l = (Nil : 'a list))))
axiom is_nil_spec1 : (forall l:'a list. ((l = (Nil : 'a list)) -> is_nil(l)))
type 'a buf = { h : int; xs : 'a list
}
logic take : int, 'a list -> 'a list
axiom take_def : (forall n:int. (take(n, (Nil : 'a list)) = (Nil : 'a list)))
axiom take_def1 :
(forall n:int.
(forall x:'a. forall xs1:'a list. ((n = 0) -> (take(n, Cons(x,
xs1)) = (Nil : 'a list)))))
axiom take_def2 :
(forall n:int.
(forall x:'a. forall xs1:'a list. ((not (n = 0)) -> (take(n, Cons(x,
xs1)) = Cons(x, take((n - 1), xs1))))))
function add(x: 'a, b: 'a buf) : 'a buf = { h = (b).h; xs = Cons(x, (b).xs) }
function get(b: 'a buf) : 'a list = take((b).h, (b).xs)
logic infix_plpl : 'a list, 'a list -> 'a list
axiom infix_plpl_def :
(forall l2:'a list. (infix_plpl((Nil : 'a list), l2) = l2))
axiom infix_plpl_def1 :
(forall l2:'a list.
(forall x1:'a. forall r1:'a list. (infix_plpl(Cons(x1, r1), l2) = Cons(x1,
infix_plpl(r1, l2)))))
axiom Append_assoc :
(forall l1:'a list. forall l2:'a list. forall l3:'a list. (infix_plpl(l1,
infix_plpl(l2, l3)) = infix_plpl(infix_plpl(l1, l2), l3)))
axiom Append_l_nil : (forall l:'a list. (infix_plpl(l, (Nil : 'a list)) = l))
logic length : 'a list -> int
axiom length_def : (length((Nil : 'a list)) = 0)
axiom length_def1 :
(forall x:'a. forall x1:'a list. (length(Cons(x, x1)) = (1 + length(x1))))
axiom Length_nonnegative : (forall l:'a list. (0 <= length(l)))
axiom Length_nil :
(forall l:'a list. ((length(l) = 0) -> (l = (Nil : 'a list))))
axiom Length_nil1 :
(forall l:'a list. ((l = (Nil : 'a list)) -> (length(l) = 0)))
axiom Append_length :
(forall l1:'a list. forall l2:'a list. (length(infix_plpl(l1,
l2)) = (length(l1) + length(l2))))
logic mem : 'a, 'a list -> prop
axiom mem_def : (forall x:'a. (not mem(x, (Nil : 'a list))))
axiom mem_def1 :
(forall x:'a.
(forall y:'a. forall r:'a list. (mem(x, Cons(y, r)) -> ((x = y) or mem(x,
r)))))
axiom mem_def2 :
(forall x:'a.
(forall y:'a. forall r:'a list. (((x = y) or mem(x, r)) -> mem(x, Cons(y,
r)))))
axiom mem_append :
(forall x:'a. forall l1:'a list. forall l2:'a list. (mem(x, infix_plpl(l1,
l2)) -> (mem(x, l1) or mem(x, l2))))
axiom mem_append1 :
(forall x:'a. forall l1:'a list. forall l2:'a list. ((mem(x, l1) or mem(x,
l2)) -> mem(x, infix_plpl(l1, l2))))
axiom mem_decomp :
(forall x:'a. forall l:'a list. (mem(x, l) ->
(exists l1:'a list. exists l2:'a list. (l = infix_plpl(l1, Cons(x, l2))))))
goal VC_take_lemma :
(forall l1:'a list. forall l2:'a list. forall l3:'a list. forall n:int.
(((0 <= n) and (n <= length(l1))) ->
((exists x:'a. exists x1:'a list. ((l1 = Cons(x, x1)) and (not (0 < n)))) ->
(take(n, infix_plpl(l1, l2)) = take(n, infix_plpl(l1, l3))))))
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2017_tree_buffer.mlw" expanded="true">
<theory name="Spec" sum="6ee3c869c821f40375f941acf3f4e979" expanded="true">
<goal name="VC take" expl="VC for take">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty">