## VerifyThis 2021: Lexicographic Permutations (version 2)

solution to VerifyThis 2021 challenge 1

**Auteurs:** Quentin Garchery / Xavier Denis

**Catégories:** Array Data Structure / Permutation

**Outils:** Why3

**Références:** VerifyThis @ ETAPS 2021

see also the index (by topic, by tool, by reference, by year)

# VerifyThis @ ETAPS 2021 competition Challenge 1: Lexicographic Permutations

See https://www.pm.inf.ethz.ch/research/verifythis.html

Authors: - Quentin Garchery (Université Paris-Saclay) - Xavier Denis (Université Paris-Saclay)

module ArrayListConversions use int.Int use array.Array use export array.ArrayEq use list.List as L use list.Nth use list.Length as L use option.Option let rec function to_list_from (i : int) (a : array int) : L.list int variant { length a - i } requires { 0 <= i <= length a } ensures { L.length result = length a - i } ensures { forall k. 0 <= k < length a - i -> nth k result = Some a[k+i] } = if i = length a then L.Nil else L.Cons a[i] (to_list_from (i+1) a) let function to_list a = to_list_from 0 a let lemma to_list_array_eq (a1 a2 : array int) : unit requires { array_eq a1 a2 } ensures { to_list a1 = to_list a2 } = let rec lemma to_list_array_eq_from (a1 a2 : array int) (i : int) : unit variant { length a1 - i } requires { 0 <= i <= length a1} requires { array_eq a1 a2 } ensures { to_list_from i a1 = to_list_from i a2 } = if i < length a1 then to_list_array_eq_from a1 a2 (i+1) in to_list_array_eq_from a1 a2 0 let function of_list (l : L.list int) : array int ensures { length result = L.length l } ensures { forall k. 0 <= k < L.length l -> nth k l = Some result[k] } = let a = make (L.length l) 0 in let rec update_from l' i variant { l' } writes { a } requires { 0 <= i } requires { L.length l' = L.length l - i } requires { forall k. 0 <= k < L.length l' -> nth (k+i) l = nth k l' } ensures { forall k. i <= k < L.length l -> nth k l = Some a[k] } ensures { forall k. 0 <= k < i -> a[k] = old a[k] } = match l' with | L.Nil -> () | L.Cons v t -> a[i] <- v; assert { forall k. 0 < k < L.length t -> nth (k+i+1) l = nth k t by nth ((k+1)+i) l = nth (k+1) l' }; update_from t (i+1) end in update_from l 0; a let rec lemma eq_nth (l1 l2 : L.list 'a) requires { L.length l1 = L.length l2 } requires { forall k. 0 <= k < L.length l1 -> nth k l1 = nth k l2 } ensures { l1 = l2 } = match l1, l2 with | L.Cons a1 t1, L.Cons a2 t2 -> assert { a1 = a2 && L.length t1 = L.length t2 }; assert { forall k. 0 <= k < L.length t1 -> nth k t1 = nth k t2 by nth (k+1) l1 = nth (k+1) l2 }; eq_nth t1 t2 | L.Nil, L.Nil -> () | _ -> assert {false}; () end lemma of_to_list : forall a. array_eq (of_list (to_list a)) a lemma to_of_list : forall l. to_list (of_list l) = l meta remove_prop axiom eq_nth end module BoxedIntArrays use int.Int use int.Abs use int.MinMax use int.Power use array.Array use array.ArrayPermut predicate boxed (u : int) (a : array int) = forall i. 0 <= i < length a -> 2 * abs a[i] < u lemma boxed_permut : forall a a' u. boxed u a -> permut_all a a' -> boxed u a' let function greater a ensures { result >= 0 } ensures { forall i. 0 <= i < length a -> 2 * abs a[i] < result } = let rec function great a l variant { length a - l } requires { 0 <= l <= length a } ensures { result >= 0 } ensures { forall i. l <= i < length a -> 2 * abs a[i] < result } = if l = length a then 0 else let r = great a (l+1) in max r (2 * abs a[l] + 1) in great a 0 lemma boxed_greater : forall a. boxed (greater a) a let function maxi base (a : array int) requires { boxed base a } = power base (length a) end module Permut use int.Int use array.Array use array.ArrayPermut use array.ArrayExchange use array.ArrayEq use array.IntArraySorted clone array.Sorted as Decr with type elt = int, predicate le = (>=) predicate le (a1 a2 : array int) = length a1 = length a2 && exists i. 0 <= i <= length a1 && (forall j. 0 <= j < i -> a1[j] = a2[j]) && (i < length a1 -> a1[i] < a2[i]) predicate lt (a1 a2 : array int) = le a1 a2 && not array_eq a1 a2 let rec function find_eq (a1 a2 : array int) (i : int) : int variant { length a1 - i } requires { length a1 = length a2 } requires { 0 <= i <= length a1 } requires { array_eq_sub a1 a2 0 i } ensures { 0 <= result <= length a1 } ensures { array_eq_sub a1 a2 0 result } ensures { result < length a1 -> a1[result] <> a2[result] } = if i = length a1 || a1[i] <> a2[i] then i else find_eq a1 a2 (i+1) lemma lt_trans : forall a1 a2 a3 : array int. lt a1 a2 -> lt a2 a3 -> lt a1 a3 by let i = find_eq a1 a2 0 in let j = find_eq a2 a3 0 in i < length a1 && j < length a1 so i <= j -> array_eq_sub a1 a3 0 i && a1[i] < a3[i] so j < i -> array_eq_sub a1 a3 0 j && a1[j] < a3[j] let function find_le a1 a2 ensures { result <-> le a1 a2 } = length a1 = length a2 && let i = find_eq a1 a2 0 in i = length a1 || a1[i] < a2[i] lemma eq_le_compat : forall a1 a2 b1 b2 : array int. array_eq a1 b1 -> array_eq a2 b2 -> le a1 a2 -> le b1 b2 by let i = find_eq a1 a2 0 in array_eq_sub b1 b2 0 i && i < length a1 -> b1[i] <= b2[i] lemma eq_lt_compat : forall a1 a2 b1 b2 : array int. array_eq a1 b1 -> array_eq a2 b2 -> lt a1 a2 -> lt b1 b2 lemma le_or_lt : forall a1 a2 : array int. length a1 = length a2 -> le a1 a2 \/ lt a2 a1 by not le a1 a2 -> let i = find_eq a1 a2 0 in i < length a1 && a1[i] > a2[i] && array_eq_sub a1 a2 0 i lemma lt_not_le : forall a1 a2 : array int. lt a1 a2 -> not le a2 a1 by let i = find_eq a1 a2 0 in i < length a1 && a1[i] < a2[i] && array_eq_sub a1 a2 0 i let lemma eq_sub_permut (a1 a2 : array int) (u : int) requires { permut_all a1 a2 } requires { array_eq_sub a1 a2 0 u } ensures { permut_sub a1 a2 u (length a1) } = let rec lemma eq_sub_permut_ind (a1 a2 : array int) (i1 i2 i3 : int) variant { i2 - i1 } requires { i1 <= i2 <= i3 } requires { permut_sub a1 a2 i1 i3 } requires { array_eq_sub a1 a2 i1 i2 } ensures { permut_sub a1 a2 i2 i3 } = if i1 < i2 then eq_sub_permut_ind a1 a2 (i1+1) i2 i3 in eq_sub_permut_ind a1 a2 0 u (length a1) lemma le_permut_sorted : forall a1 a2 i. length a1 = length a2 -> permut_sub a1 a2 i (length a1) -> sorted_sub a1 i (length a1) -> le a1 a2 by let i' = find_eq a1 a2 0 in i' >= i so i' < length a1 -> permut_sub a1 a2 i' (length a1) so a1[i'] <= a2[i'] lemma le_permut_decr_sorted : forall a1 a2 i. length a1 = length a2 -> permut_sub a1 a2 i (length a1) -> Decr.sorted_sub a1 i (length a1) -> le a2 a1 by let i' = find_eq a1 a2 0 in i' >= i so i' < length a1 -> permut_sub a1 a2 i' (length a1) so a1[i'] >= a2[i'] let next (a : array int) writes { a } ensures { permut_all a (old a) } ensures { not result -> a = old a && forall a'. permut_all a a' -> le a a' -> array_eq a a' by Decr.sorted a } ensures { result -> lt (old a) a && forall a'. permut_all (old a) a' -> lt (old a) a' -> le a a' } = let ref i = length a - 1 in while (i > 0 && a[i-1] >= a[i]) do variant { i } invariant { i <= length a - 1} invariant { Decr.sorted_sub a i (length a) } i <- i-1 done; if i <= 0 then false else begin let ref j = length a - 1 in while (a[j] <= a[i-1]) do variant { j } invariant { i <= j <= length a - 1 } invariant { forall k. j < k < length a -> a[k] <= a[i-1] } j <- j-1 done; assert { a[j] > a[i-1] }; assert { forall k. i <= k < length a -> a[k] > a[i-1] -> a[k] >= a[j] }; let ghost i0 = i in let ref temp = a[i-1] in a[i-1] <- a[j]; a[j] <- temp; assert { exchange a (old a) (i-1) j }; j <- length a - 1; label L in while (i<j) do variant { j-i } invariant { i0 <= i < length a } invariant { i0 <= j < length a } invariant { permut_all a (a at L) } invariant { array_eq_sub a (a at L) 0 i0 } invariant { forall k1 k2. i0 <= k1 < k2 < i -> a[k1] <= a[k2] } invariant { forall k1 k2. i <= k1 < k2 < j+1 -> a[k1] >= a[k2] } invariant { forall k1 k2. j+1 <= k1 < k2 < length a -> a[k1] <= a[k2] } invariant { forall k1 k2. i0 <= k1 < i -> i <= k2 <= j -> a[k1] <= a[k2] } invariant { forall k1 k2. i <= k1 <=j -> j < k2 < length a -> a[k1] <= a[k2] } invariant { forall k1 k2. i0 <= k1 < i -> j < k2 < length a -> a[k1] <= a[k2] } label StartLoop in temp <- a[i]; a[i] <- a[j]; a[j] <- temp; assert { exchange a (a at StartLoop) i j }; i <- i+1; j <- j-1 done; assert { sorted_sub a i0 (length a) }; assert { forall a'. permut_all (old a) a' -> lt (old a) a' -> le a a' by let i = find_eq (old a) a' 0 in if i = length a then array_eq (old a) a' so le a a' else if i < i0-1 then a'[i] > (old a)[i] so le a a' else if i > i0-1 then a'[i0-1] = (old a)[i0-1] < a[i0-1] so false else i = i0-1 so if a'[i0-1] <> a[i0-1] then (old a)[i0-1] < a'[i0-1] so permut_sub (old a) a' (i0 -1) (length a) so a[i0-1] <= a'[i0-1] so le a a' else array_eq_sub a a' 0 (i0-1) so array_eq_sub a a' 0 i0 so permut_sub a a' i0 (length a) so le a a' }; true end use queue.Queue as Queue use list.List as L use int.Abs use int.Power use BoxedIntArrays val sort (a : array int) : unit writes { a } ensures { permut_all a (old a) } ensures { sorted a } let rec function as_num base a i variant { length a - i } requires { boxed base a } requires { 0 <= i <= length a } ensures { 2 * abs result < power base (length a - i) } = if i = length a then 0 else begin let rest = as_num base a (i+1) in assert { 2 * abs (a[i] * power base (length a - 1 - i) + rest) <= 2 * abs a[i] * power base (length a - 1 - i) + 2 * abs rest < (2 * abs a[i] + 1) * power base (length a - 1 - i) <= base * power base (length a - 1 - i) <= power base (length a - i) by (forall x y : int. x >= 0 -> y >= 0 -> x * y >= 0) so forall x y z : int. x <= y -> z >= 0 -> x * z <= y * z by (y - x) * z >= 0 }; a[i] * power base (length a - 1 - i) + rest end let function as_number base a requires { boxed base a } ensures { abs result <= maxi base a } = as_num base a 0 let rec lemma as_number_ind (a a' : array int) (base i j : int) variant { j - i } requires { 0 <= i <= j < length a } requires { boxed base a } requires { boxed base a' } requires { array_eq_sub a a' 0 j } requires { a[j] < a'[j] } ensures { as_num base a i < as_num base a' i } = if i < j then (assert { a[i] = a'[i] }; as_number_ind a a' base (i+1) j) else assert { as_num base a i = a[i] * power base (length a - 1 - i) + as_num base a (i+1) /\ as_num base a' i = a'[i] * power base (length a - 1 - i) + as_num base a' (i+1) /\ 2 * (as_num base a (i+1) - as_num base a' (i+1)) <= 2 * abs (as_num base a (i+1)) + 2 * abs (as_num base a' (i+1)) < 2 * power base (length a - 1 - i) <= 2 * (a'[i] - a[i]) * power base (length a - 1 - i) } let lemma as_number_strict a a' base requires { length a = length a'} requires { boxed base a } requires { boxed base a' } requires { lt a a' } ensures { as_number base a < as_number base a' } = let n = length a in for i = 0 to n - 1 do invariant { array_eq_sub a a' 0 i } if a[i] <> a'[i] then (as_number_ind a a' base 0 i; return) done use seq.Seq use seq.Mem use ArrayListConversions lemma seq_snoc_mem : forall s : seq 'a, x y. mem x (snoc s y) <-> mem x s \/ x = y let permut (a : Array.array int) : Queue.t (L.list int) ensures { forall i1 i2. 0 <= i1 < i2 < length result -> lt (of_list result[i1]) (of_list result[i2]) } ensures { forall a'. permut_all a a' -> mem (to_list a') result } = let ghost base = greater a in let res = Queue.create () in if length a = 0 then begin Queue.push L.Nil res; assert { forall a'. permut_all a a' -> mem (to_list a') res }; res end else begin sort a; let ref cont = true in let ghost ref cont_int = 1 in assert { forall a'. permut_all a' a -> lt a' a -> false by permut_sub a a' 0 (Array.length a) }; while cont do invariant { permut_all a (old a) } invariant { boxed base a } invariant { cont_int = 1 <-> cont } invariant { cont -> forall a'. permut_all a' a -> lt a' a -> mem (to_list a') res } invariant { not cont -> forall a'. permut_all a' a -> le a' a -> mem (to_list a') res} invariant { cont -> forall a'. mem (to_list a') res -> lt a' a } invariant { not cont -> forall a'. permut_all a a' -> le a a' -> array_eq a a' } invariant { forall i1 i2. 0 <= i1 < i2 < length res -> lt (of_list res[i1]) (of_list res[i2]) } variant { cont_int, maxi base a - as_number base a } label SL in Queue.push (to_list a) res; cont <- next a; if cont then begin assert { forall a'. permut_all a' a -> lt a' a -> mem (to_list a') res by not le a a' so le a' (a at SL) }; assert { forall a'. mem (to_list a') res -> lt a' a by le a a' -> lt (a at SL) a' so not mem (to_list a') (res at SL) so to_list a' = to_list (a at SL) so lt a' a }; () end else cont_int <- 0; assert { boxed base a }; assert { forall i1 i2. 0 <= i1 < i2 < length res -> lt (of_list res[i1]) (of_list res[i2]) by i2 = length res - 1 -> array_eq (of_list res[i2]) (a at SL) && lt (of_list res[i1]) (a at SL)}; done; res end end

download ZIP archive

# Why3 Proof Results for Project "verifythis_2021_lexicographic_permutations_2"

## Theory "verifythis_2021_lexicographic_permutations_2.ArrayListConversions": fully verified

Obligations | Alt-Ergo 2.4.0 | CVC4 1.7 | Z3 4.12.2 | ||

VC for to_list_from | --- | 0.15 | --- | ||

VC for to_list | --- | 0.04 | --- | ||

VC for to_list_array_eq | --- | 0.05 | --- | ||

VC for of_list | --- | --- | --- | ||

split_vc | |||||

array creation size | --- | 0.04 | --- | ||

postcondition | --- | 0.05 | --- | ||

postcondition | --- | 0.04 | --- | ||

index in array bounds | --- | 0.06 | --- | ||

assertion | --- | --- | --- | ||

split_vc | |||||

assertion | --- | 0.04 | --- | ||

VC for of_list | --- | 0.04 | --- | ||

variant decrease | --- | 0.04 | --- | ||

precondition | --- | 0.03 | --- | ||

precondition | --- | 0.03 | --- | ||

precondition | 0.08 | --- | --- | ||

postcondition | --- | 0.08 | --- | ||

postcondition | --- | 0.08 | --- | ||

precondition | --- | 0.03 | --- | ||

precondition | --- | 0.03 | --- | ||

precondition | --- | 0.04 | --- | ||

postcondition | --- | 0.04 | --- | ||

postcondition | --- | 0.05 | --- | ||

VC for eq_nth | --- | --- | --- | ||

split_vc | |||||

assertion | 0.04 | --- | --- | ||

assertion | --- | --- | --- | ||

split_vc | |||||

assertion | --- | 0.03 | --- | ||

VC for eq_nth | --- | 0.04 | --- | ||

precondition | --- | 0.04 | --- | ||

precondition | --- | 0.05 | --- | ||

assertion | --- | 0.03 | --- | ||

assertion | --- | 0.03 | --- | ||

postcondition | --- | --- | 0.01 | ||

of_to_list | 0.45 | --- | --- | ||

to_of_list | 0.01 | --- | --- |

## Theory "verifythis_2021_lexicographic_permutations_2.BoxedIntArrays": fully verified

Obligations | Alt-Ergo 2.3.0 | Alt-Ergo 2.4.3 | CVC4 1.7 | Z3 4.12.2 |

boxed_permut | --- | 0.01 | --- | 0.03 |

VC for greater | --- | --- | 0.06 | --- |

boxed_greater | --- | --- | 0.04 | --- |

VC for maxi | 0.00 | --- | --- | --- |

## Theory "verifythis_2021_lexicographic_permutations_2.Permut": fully verified

Obligations | Alt-Ergo 2.3.0 | Alt-Ergo 2.4.0 | Alt-Ergo 2.4.1 | Alt-Ergo 2.4.2 | Alt-Ergo 2.4.3 | CVC4 1.7 | CVC4 1.8 | CVC5 1.0.4 | CVC5 1.0.5 | Z3 4.11.2 | Z3 4.12.2 | ||||

VC for find_eq | --- | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

lt_trans | --- | 0.05 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for find_le | --- | --- | --- | --- | --- | 0.15 | --- | --- | --- | --- | --- | ||||

eq_le_compat | --- | --- | --- | --- | --- | 0.41 | --- | --- | --- | --- | --- | ||||

eq_lt_compat | --- | --- | --- | --- | --- | 0.13 | --- | --- | --- | --- | --- | ||||

le_or_lt | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

le_or_lt.0 | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

le_or_lt.1 | --- | --- | --- | --- | --- | 0.03 | --- | --- | --- | --- | --- | ||||

le_or_lt.2 | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

le_or_lt.3 | --- | --- | --- | --- | --- | 0.16 | --- | --- | --- | --- | --- | ||||

lt_not_le | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

lt_not_le.0 | --- | --- | --- | --- | --- | 0.15 | --- | --- | --- | --- | --- | ||||

lt_not_le.1 | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

lt_not_le.2 | --- | --- | --- | --- | --- | 0.16 | --- | --- | --- | --- | --- | ||||

lt_not_le.3 | --- | --- | --- | --- | --- | 0.19 | --- | --- | --- | --- | --- | ||||

VC for eq_sub_permut | --- | 0.55 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

le_permut_sorted | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

le_permut_sorted.0 | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

le_permut_sorted.1 | --- | --- | --- | --- | --- | 0.25 | --- | --- | --- | --- | --- | ||||

le_permut_sorted.2 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | 0.02 | ||||

le_permut_sorted.3 | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

le_permut_decr_sorted | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

le_permut_decr_sorted.0 | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

le_permut_decr_sorted.1 | --- | --- | --- | --- | --- | 0.32 | --- | --- | --- | --- | --- | ||||

le_permut_decr_sorted.2 | --- | 0.05 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

le_permut_decr_sorted.3 | --- | --- | --- | --- | --- | 0.12 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

loop invariant init | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop variant decrease | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | 0.02 | ||||

postcondition | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop variant decrease | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.13 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | 1.13 | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.16 | --- | --- | --- | --- | --- | ||||

loop variant decrease | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | 0.14 | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | 0.39 | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | 0.03 | ||||

loop invariant preservation | --- | --- | --- | 0.42 | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | 0.25 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | --- | 0.31 | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | --- | 0.16 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | --- | 0.38 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | 0.18 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.12 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.30 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.22 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

VC for next | --- | --- | --- | --- | --- | --- | --- | --- | 7.37 | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | --- | --- | --- | --- | 0.21 | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.32 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.21 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | 0.03 | ||||

VC for next | --- | --- | --- | --- | --- | 0.89 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.13 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.18 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

VC for next | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.29 | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

variant decrease | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | --- | 0.03 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | 0.10 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | --- | --- | --- | --- | 0.07 | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | 1.51 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_num | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

index in array bounds | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

postcondition | --- | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_number | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

VC for as_number_ind | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | 0.21 | --- | --- | --- | --- | --- | ||||

variant decrease | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | --- | ||||

precondition | --- | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | --- | ||||

assertion | --- | 2.50 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

postcondition | --- | 0.04 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for as_number_strict | --- | --- | --- | --- | --- | 4.51 | --- | --- | --- | --- | --- | ||||

seq_snoc_mem | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

seq_snoc_mem.0 | --- | --- | --- | --- | 0.02 | --- | --- | --- | --- | --- | --- | ||||

seq_snoc_mem.1 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

inline_goal | |||||||||||||||

seq_snoc_mem.1.0 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_all_full | |||||||||||||||

seq_snoc_mem.1.0.0 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

seq_snoc_mem.1.0.0.0 | --- | --- | --- | --- | --- | --- | --- | 2.37 | --- | --- | --- | ||||

VC for permut | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | 0.18 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.13 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.12 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | --- | --- | --- | --- | --- | 0.23 | --- | --- | --- | --- | --- | ||||

VC for permut | --- | --- | --- | --- | --- | 0.14 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.09 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.70 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.09 | --- | --- | --- | --- | --- | ||||

loop invariant init | --- | --- | --- | --- | --- | 0.12 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for permut | --- | --- | --- | --- | --- | 0.45 | --- | --- | --- | --- | --- | ||||

VC for permut | 0.22 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.14 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | 0.45 | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | 0.04 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | 0.12 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for permut | 0.15 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop variant decrease | 0.20 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | 0.10 | --- | --- | --- | --- | --- | ||||

assertion | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

split_vc | |||||||||||||||

assertion | 0.03 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

assertion | 0.15 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

VC for permut | 0.20 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop variant decrease | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.03 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.17 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.19 | --- | --- | --- | --- | --- | ||||

postcondition | --- | --- | --- | --- | --- | 0.19 | --- | --- | --- | --- | --- |