## VerifyThis 2021: Shearsort

solution to VerifyThis 2021 challenge 3

Authors: Martin Clochard

Tools: Why3

References: VerifyThis @ ETAPS 2021

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

# VerifyThis @ ETAPS 2021 competition Challenge 3: Shearsort

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

Author: Martin Clochard (ETH Zurich)

```module ShearSort

use int.Sum
use int.Int
use int.NumOf
use int.Power
use int.ComputerDivision
use map.Map as MP
use map.MapExt as MP
use array.Array
use matrix.Matrix as M
use map.Occ
use map.MapPermut

function column (m: M.matrix 'a) (j:int) : int -> 'a = fun i -> m.M.elts i j

function moccf (x:'a) (e:int -> int -> 'a) (c:int) : int -> int =
fun (i:int) -> occ x (e i) 0 c
function mocc (x:'a) (e:int -> int -> 'a) (r c:int) : int =
sum (moccf x e c) 0 r

let rec ghost transpose_count (x:'a) (e1 e2:int -> int -> 'a) (r c:int) : unit
requires { 0 <= r && 0 <= c }
requires { forall i j:int. 0 <= i < r /\ 0 <= j < c ->
e1 i j = e2 j i }
ensures { mocc x e1 r c = mocc x e2 c r }
variant { r }
= if r = 0 then begin
assert { mocc x e2 c r = 0
by forall j:int. 0 <= j && j < c ->
moccf x e2 r j = 0
}
end else begin
let rm = r - 1 in
let f = pure{moccf x e2 r} in
let g = pure{moccf x e2 rm} in
let rec ghost scan (j:int) : unit
requires { 0 <= j <= c }
ensures  { sum f 0 j = sum g 0 j + occ x (e1 rm) 0 j }
variant { j }
= if j <> 0 then scan (j-1)
in
scan c;
transpose_count x e1 e2 rm c
end

val sort(a: array int) : unit
writes { a }
ensures { forall i j:int. 0 <= i <= j < a.length ->
a[i] <= a[j] }
ensures { permut a.elts (old a).elts 0 a.length }

let ghost permut_swap (a b:int -> 'a)(x y l u:int)
requires { l <= x < u && l <= y < u }
requires { forall i:int. l <= i <= u && i <> x && i <> y ->
a i = b i }
requires { a x = b y && a y = b x }
ensures { permut a b l u }
= let c = MP.(a[x <- a y][y <- a x]) in
assert { MP.(a == a[x <- a x][y <- a y]) };
assert { permut a c l u };
assert { forall i: int. l <= i < u -> b i = c i };
assert { permut b c l u }

function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c =
fun x -> g (f x)

let rec ghost numoff_occ (a:int -> 'a) (l u:int) (p q:'a -> bool) (x:'a)
requires { l <= u }
requires { p x }
requires { forall y:'a. q y <-> p y /\ y <> x }
ensures { numof (compose p a) l u = numof (compose q a) l u + occ x a l u }
variant { u - l }
= if l <> u then numoff_occ a (l+1) u p q x

let rec ghost permut_numoff (a b:int -> 'a) (l u:int) (p:'a -> bool)
requires { l <= u }
requires { permut a b l u }
ensures { numof (compose p a) l u = numof (compose p b) l u }
variant { numof (compose p b) l u, numof (compose p a) l u}
= if pure {numof (compose p a) l u } = 0 then begin
if pure {numof (compose p b) l u} <> 0 then permut_numoff b a l u p
end else begin
let rec find (i:int) : int
requires { i <= u }
requires { numof (compose p a) i u > 0 }
ensures { i <= result <= u }
ensures { compose p a result }
ensures { occ (a result) a i u > 0 }
variant { u - i }
= if compose p a i then i else find (i+1)
in
let j = find l in
let v = a j in
let q = MP.(p[v <- false]) in
numoff_occ a l u p q v;
numoff_occ b l u p q v;
permut_numoff a b l u q
end

let sort_row(m : M.matrix int) (i: int) (ascending: bool) : unit
requires { 0 <= i < m.M.rows }
writes { m }
ensures { forall j k:int.
0 <= j /\ j < m.M.rows /\ 0 <= k < m.M.columns /\ j <> i ->
m.M.elts j k = (old m).M.elts j k }
ensures { forall j k: int. 0 <= j <= k < m.M.columns ->
let a = m.M.elts i j in let b = m.M.elts i k in
if ascending then a <= b else b <= a }
ensures { permut (m.M.elts i) ((old m).M.elts i) 0 m.M.columns }
=
let a = make m.M.columns 0 in
for j = 0 to m.M.columns - 1 do
invariant { forall k:int. 0 <= k < j ->
a.elts k = m.M.elts i k }
a[j]<- M.get m i j
done;
assert { permut a.elts (m.M.elts i) 0 a.length };
sort a;
label L in
if not(ascending) then begin
let ref u = 0 in
let ref v = a.length - 1 in
while u < v do
invariant { 0 <= u <= v + 1 <= a.length }
invariant { u + v = a.length - 1 }
invariant { forall j:int. u <= j <= v ->
a.elts j = (a.elts at L) j
}
invariant { forall j:int. 0 <= j < u \/ v < j < a.length ->
a.elts j = (a.elts at L) (a.length - 1 - j)
}
invariant { permut (a.elts at L) a.elts 0 a.length }
variant { v - u }
let e = a.elts in
let tmp = a[v] in
a[v] <- a[u];
a[u] <- tmp;
permut_swap a.elts e u v 0 a.length;
u <- u + 1;
v <- v - 1
done
end;
for j = 0 to m.M.columns - 1 do
invariant { forall k:int. 0 <= k < j ->
a.elts k = m.M.elts i k }
invariant { forall k l:int.
0 <= k < m.M.rows /\ 0 <= l < m.M.columns /\ k <> i ->
m.M.elts k l = (m at L).M.elts k l }
M.set m i j a[j]
done;
assert { permut a.elts (m.M.elts i) 0 a.length }

let sort_column(m : M.matrix int) (j: int) : unit
requires { 0 <= j < m.M.columns }
writes { m }
ensures { forall i k:int.
0 <= i /\ i < m.M.rows /\ 0 <= k < m.M.columns /\ k <> j ->
m.M.elts i k = (old m).M.elts i k }
ensures { forall i k: int. 0 <= i <= k < m.M.rows ->
m.M.elts i j <= m.M.elts k j }
ensures { permut (column m j) (column (old m) j) 0 m.M.rows }
= let a = make m.M.rows 0 in
for i = 0 to m.M.rows - 1 do
invariant { forall k:int. 0 <= k < i ->
a.elts k = m.M.elts k j }
a[i]<- M.get m i j
done;
assert { permut a.elts (column m j) 0 a.length };
sort a;
label L in
for i = 0 to m.M.rows - 1 do
invariant { forall k:int. 0 <= k < i ->
a.elts k = m.M.elts k j }
invariant { forall k l:int.
0 <= k < m.M.rows /\ 0 <= l < m.M.columns /\ l <> j ->
m.M.elts k l = (m at L).M.elts k l }
M.set m i j a[i]
done;
assert { permut a.elts (column m j) 0 a.length }

(* Isolate the loops sorting all rows/columns in isolated functions
for modular verification (also makes easier to verify alternative
implementation with transpose) *)
let sort_all_rows(m : M.matrix int) : unit
writes { m }
ensures { forall i:int. 0 <= i < m.M.rows ->
permut (m.M.elts i) ((old m).M.elts i) 0 m.M.columns }
ensures { forall i j k:int. 0 <= i < m.M.rows /\
0 <= j <= k < m.M.columns ->
let a = m.M.elts i j in let b = m.M.elts i k in
if mod i 2 = 0 then a <= b else b <= a }
= label L in
for tid = 0 to m.M.rows - 1 do
invariant { forall i:int. 0 <= i < m.M.rows ->
permut (m.M.elts i) ((m at L).M.elts i) 0 m.M.columns }
invariant { forall i j k:int. 0 <= i < tid /\
0 <= j <= k < m.M.columns ->
let a = m.M.elts i j in let b = m.M.elts i k in
if mod i 2 = 0 then a <= b else b <= a }
label L2 in
let ascending = mod tid 2 = 0 in
sort_row m tid ascending;
assert { forall i:int. 0 <= i < m.M.rows ->
permut (m.M.elts i) ((m at L2).M.elts i) 0 m.M.columns }
done

val transpose (m: M.matrix int) : unit
requires { m.M.rows = m.M.columns }
writes { m }
ensures { forall i j:int. 0 <= i < m.M.rows /\
0 <= j < m.M.columns -> (old m).M.elts i j = m.M.elts j i }

let sort_all_columns (m : M.matrix int) : unit
writes { m }
ensures { forall j:int. 0 <= j < m.M.columns ->
permut (column m j) (column (old m) j) 0 m.M.rows }
ensures { forall i j k:int. 0 <= i <= k < m.M.rows /\
0 <= j < m.M.columns ->
m.M.elts i j <= m.M.elts k j }
= label L in
if any bool ensures { result \/ m.M.rows = m.M.columns } then begin
for tid = 0 to m.M.columns - 1 do
invariant { forall j:int. 0 <= j < m.M.columns ->
permut (column m j) (column (old m) j) 0 m.M.rows }
invariant { forall i j k:int. 0 <= i <= k < m.M.rows /\
0 <= j < tid -> m.M.elts i j <= m.M.elts k j }
label L2 in
sort_column m tid;
assert { forall j:int. 0 <= j < m.M.columns ->
permut (column m j) (column (m at L2) j) 0 m.M.rows }
done
end else begin
let n = m.M.rows in
transpose m;
assert { forall j:int. 0 <= j < n ->
permut (column (old m) j) (m.M.elts j) 0 n
by forall i:int. 0 <= i < n ->
column (old m) j i = m.M.elts j i
};
for tid = 0 to m.M.columns - 1 do
invariant { forall j:int. 0 <= j < n ->
permut (m.M.elts j) (column (old m) j) 0 n }
invariant { forall i j k:int. 0 <= i <= k < n /\
0 <= j < tid -> m.M.elts j i <= m.M.elts j k }
label L2 in
sort_row m tid true;
assert { forall j:int. 0 <= j < n ->
permut (m.M.elts j) ((m.M.elts at L2) j) 0 n }
done;
let et2 = pure{m.M.elts} in
transpose m;
assert {
forall j:int. 0 <= j < n ->
permut (column m j) (et2 j) 0 n
by forall i:int. 0 <= i < n ->
column m j i = et2 j i
}
end

predicate below_column (e:int -> int -> int) (col v row:int) =
e row col <= v
predicate above_column (e:int -> int -> int) (col v row:int) =
e row col > v

let shear_sort(m: M.matrix int) : unit
ensures {
forall i j1 j2 k:int.
0 <= i < k < m.M.rows &&
0 <= j1 < m.M.columns && 0 <= j2 < m.M.columns ->
m.M.elts i j1 <= m.M.elts k j2
}
ensures {
forall i j k:int.
0 <= i < m.M.rows && 0 <= j <= k < m.M.columns ->
if mod i 2 = 0 then m.M.elts i j <= m.M.elts i k else
m.M.elts i k <= m.M.elts i j
}
ensures {
forall x:int.
mocc x (old m.M.elts) m.M.rows m.M.columns
= mocc x m.M.elts m.M.rows m.M.columns
}
writes { m }
= label L0 in
let n = m.M.rows in
let ghost c = m.M.columns in
(* FIX: n need to be non-zero for the log to be computable ! *)
if n <> 0 then
(* Compute log_2(n). *)
let ref l = 0 in
let ref p = n - 1 in
while p <> 0 do
invariant { l >= 0 && p >= 0 }
invariant { l <> 0 -> power 2 (l-1) <= n }
invariant { p * power 2 l < n <= power 2 l * (p+1) }
variant { p }
l <- l + 1;
let ghost q = p in
p <- div p 2;
assert { 2 * p <= q <= 2 * p + 1 };
assert { p * power 2 l
= (2 * p) * power 2 (l-1)
<= q * power 2 (l-1) < n };
assert { (p+1) * power 2 l
= (2 * p + 2) * power 2 (l-1)
>= (q + 1) * power 2 (l-1) >= n }
done;
(* Check against defining property of ceil(log2(n)) *)
assert { power 2 l >= n };
assert { l <> 0 -> power 2 (l-1) <= n };
(* Maximum width of the gap between zero rows and one rows
under 0-1 abstractions. *)
let ghost ref k = n in
let ghost ref zeros = pure { fun (_:int) -> 0 } in
let ghost ref ones = pure { fun (_:int) -> n } in
let ghost column_sorted () : unit
requires { forall v:int. 0 <= zeros v <= ones v <= n }
requires { forall v:int. ones v <= zeros v + 1 }
requires { forall v i j:int.
0 <= i < zeros v /\ 0 <= j < c ->
m.M.elts i j <= v }
requires { forall v i j:int.
ones v <= i < n /\ 0 <= j < c ->
m.M.elts i j > v }
ensures { forall i j1 j2 k:int.
0 <= i < k < n && 0 <= j1 < c && 0 <= j2 < c ->
m.M.elts i j1 <= m.M.elts k j2 }
=
let rec lemma aux (i j1 j2 k:int)
requires { 0 <= i < k < n && 0 <= j1 < c && 0 <= j2 < c }
ensures { m.M.elts i j1 <= m.M.elts k j2 }
= let v = m.M.elts k j2 in
if m.M.elts i j1 > v then begin
assert { ones v >= i &&
zeros v <= k + 1 &&
false }
end
in ()
in
(* Repeat l+1 times. *)
for ind = 0 to l do
invariant { forall v:int. 0 <= zeros v <= ones v <= n }
invariant { forall v:int. ones v <= zeros v + k }
invariant { forall v i j:int.
0 <= i < zeros v /\ 0 <= j < c ->
m.M.elts i j <= v (* p(v)(m.M.elts i j) = 0 *) }
invariant { forall v i j:int.
ones v <= i < n /\ 0 <= j < c ->
m.M.elts i j > v (* p(v)(m.M.elts i j) = 1 *) }
invariant { k > 0 }
invariant { (k-1) * power 2 ind < n <= k * power 2 ind }
invariant { ind > l ->
forall i j k:int.
0 <= i < n /\ 0 <= j <= k < c ->
let a = m.M.elts i j in
let b = m.M.elts i k in
if mod i 2 = 0 then a <= b else b <= a }
invariant { forall x:int.
mocc x (m.M.elts at L0) n c
= mocc x m.M.elts n c }
let e0 = m.M.elts in
sort_all_rows m;
let e = m.M.elts in
assert { forall v i j:int. 0 <= i < zeros v /\ 0 <= j < c ->
e i j <= v
by occ (e i j) (e i) 0 c > 0
so occ (e i j) (e0 i) 0 c > 0
so exists k. 0 <= k /\ k < c /\ e0 i k = e i j
so e0 i k <= v
};
assert { forall v i j:int.
ones v <= i < n /\ 0 <= j < c ->
e i j > v
by occ (e i j) (e i) 0 c > 0
so occ (e i j) (e0 i) 0 c > 0
so exists k. 0 <= k /\ k < c /\ e0 i k = e i j
so e0 i k > v
};
assert { forall x:int.
mocc x e0 n c = mocc x e n c
by forall i:int. 0 <= i < n ->
moccf x e0 c i = moccf x e c i
};
let zs = zeros in
let os = ones in
let kd = div (k+1) 2 in
let ghost function nzo (v:int) : (int,int)
ensures { match result with nz, no ->
0 <= nz <= no <= n &&
no <= nz + kd &&
forall j:int. 0 <= j < c ->
numof (below_column e j v) 0 n >= nz /\
numof (above_column e j v) 0 n >= n - no
end
}
=
let z = zs v in
let rec lemma fillz (i:int) (j:int)
requires { 0 <= i <= z /\ 0 <= j < c }
ensures { numof (below_column e j v) 0 i >= i }
variant { i }
= if i <> 0 then begin
assert { below_column e j v (i-1) };
assert { numof (below_column e j v) (i-1) i = 1 };
fillz (i-1) j
end
in
let o = os v in
let rec lemma fillo (i:int) (j:int)
requires { o <= i <= n /\ 0 <= j < c }
ensures { numof (above_column e j v) i n >= n - i }
variant { n - i }
= if i <> n then begin
assert { above_column e j v i };
assert { numof (above_column e j v) i (i+1) = 1 };
fillo (i+1) j
end
in
let ref nz = z in
let ref no = o in
let ref index = z in
while index + 1 < o do
invariant { z <= index /\ index <= o }
invariant { nz >= z /\ no <= o }
invariant { index - z = 2 * (nz - z + o - no) }
invariant { forall j:int. 0 <= j < c ->
numof (below_column e j v) 0 index >= nz /\
numof (above_column e j v) 0 index
+ numof (above_column e j v) o n >= n - no }
variant { o - index }
let rec select (r1 r2:int -> int) (b:bool) : bool
requires { forall j k:int. 0 <= j <= k < c ->
if b then r1 j <= r1 k else r1 k <= r1 j }
requires { forall j k:int. 0 <= j <= k < c ->
if b then r2 k <= r2 j else r2 j <= r2 k }
ensures { result -> forall i:int. 0 <= i < c ->
r1 i <= v || r2 i <= v }
ensures { not(result) -> forall i:int. 0 <= i < c ->
r1 i > v || r2 i > v }
variant { if b then 0 else 1 }
=
if not(b) then select r2 r1 true else
let ref i = 0 in
while i <> c && r1 i <= v && r2 i > v do
invariant { 0 <= i <= c }
invariant { forall j:int. 0 <= j < i ->
r1 j <= v && r2 j > v }
variant { c - i }
i <- i + 1
done;
i = c || r2 i <= v
in
if select (e index) (e (index + 1)) (mod index 2 = 0) then begin
nz <- nz + 1;
assert { forall j:int. 0 <= j < c ->
numof (below_column e j v) index (index+2) > 0 }
end else begin
no <- no - 1;
assert { forall j:int. 0 <= j < c ->
numof (above_column e j v) index (index+2) > 0 }
end;
index <- index + 2
done;
nz, no
in
let ghost function newz (v:int) : int
ensures { result = match nzo v with (x,_) -> x end }
= match nzo v with (x,_) -> x end
in
let ghost function newo (v:int) : int
ensures { result = match nzo v with (_,y) -> y end }
= match nzo v with (_,y) -> y end
in
let lemma newzo (v:int)
ensures { let nz = newz v in let no = newo v in
0 <= nz <= no <= n &&
no <= nz + kd &&
forall j:int. 0 <= j < c ->
numof (below_column e j v) 0 n >= nz /\
numof (above_column e j v) 0 n >= n - no
}
= let (x,y) = nzo v in assert { newz v = x /\ newo v = y }
in
let cl1 = pure {column m} in
assert { forall v j:int. 0 <= j < c ->
MP.(below_column e j v == compose ((>=) v) (cl1 j))
/\ MP.(above_column e j v == compose ((<) v) (cl1 j)) };
if ind = l then column_sorted ();
zeros <- pure{newz};
ones <- pure{newo};
sort_all_columns m;
label L in
let cl2 = pure {column m} in
let rec lemma column_permutation (x:int) : unit
ensures { mocc x (m.M.elts at L) n c = mocc x e n c }
= transpose_count x e cl1 n c;
transpose_count x (pure{m.M.elts at L}) cl2 n c;
assert { mocc x cl1 c n = mocc x cl2 c n
by forall j:int. 0 <= j < c ->
moccf x cl1 n j = moccf x cl2 n j }
in
if ind = l then begin
let lemma column_preserved (j:int)
requires { 0 <= j < c }
ensures { forall i:int. 0 <= i < n ->
m.M.elts i j = e i j }
= let rec ghost no_occ (m:int -> int) (i:int) (x:int) : unit
requires { 0 <= i <= n }
requires { forall u v:int. i <= u <= v < n ->
m u <= m v }
requires { forall u:int. i <= u < n -> m u > x }
ensures { occ x m i n = 0 }
variant { n - i }
= if i <> n then no_occ m (i+1) x
in
let rec ghost scan (i:int) : unit
requires { 0 <= i <= n }
requires { permut (cl1 j) (cl2 j) i n }
ensures { forall k:int. i <= k < n ->
cl1 j k = cl2 j k }
variant { n - i }
= if i <> n then
let u = cl1 j i in let v = cl2 j i in
if u < v then no_occ (cl2 j) i u else
if v < u then no_occ (cl1 j) i v else
scan (i+1)
in
scan 0
in
()
end;
let e = m.M.elts in
assert { forall v j:int. 0 <= j < c ->
MP.(below_column e j v == compose ((>=) v) (cl2 j))
/\ MP.(above_column e j v == compose ((<) v) (cl2 j)) };
let rec ghost auxT (v i j:int) : unit
requires { 0 <= i < n }
requires { numof (below_column e j v) (i+1) n > 0 /\ 0 <= j < c }
requires { cl2 j i > v }
ensures { false }
variant { n - i }
=
auxT v (i+1) j
in
let lemma auxT1 (v i j:int) : unit
requires { 0 <= i < zeros v }
requires { 0 <= j < c }
ensures { cl2 j i <= v }
= if cl2 j i > v then begin
permut_numoff (cl1 j) (cl2 j) 0 n ((>=) v);
assert {
let a = numof (below_column e j v) 0 i in
let b = numof (below_column e j v) i n in
numof (below_column e j v) 0 n = a + b
&& a <= i
&& b > 0
};
auxT v i j
end
in
let rec ghost auxB (v i j:int) : unit
requires { 0 <= i < n }
requires { numof (above_column e j v) 0 i > 0 /\ 0 <= j < c }
requires { cl2 j i <= v }
ensures { false }
variant { i }
=
auxB v (i-1) j
in
let lemma auxB1 (v i j:int) : unit
requires { ones v <= i < n }
requires { 0 <= j < c }
ensures { cl2 j i > v }
= if cl2 j i <= v then begin
permut_numoff (cl1 j) (cl2 j) 0 n ((<) v);
assert {
let a = numof (above_column e j v) 0 (i+1) in
let b = numof (above_column e j v) (i+1) n in
numof (above_column e j v) 0 n = a + b
&& b <= n - i
&& a > 0
};
auxB v i j
end
in
assert { 2 * kd <= k+1 <= 2 * kd + 1 };
assert { (kd-1) * power 2 (ind+1)
= (2 * kd - 2) * power 2 ind
<= (k-1) * power 2 ind < n };
assert { kd * power 2 (ind+1)
= 2 * kd * power 2 ind
>= k * power 2 ind >= n };
k <- kd
done;
column_sorted ()

end

(* Duplicated from Why3's gallery. *)
module Quicksort

use int.Int
use ref.Ref
use array.Array
use array.IntArraySorted
use array.ArraySwap
use array.ArrayPermut
use array.ArrayEq

predicate qs_partition (a1 a2: array int) (l m r: int) (v: int) =
permut_sub a1 a2 l r /\
(forall j: int. l <= j < m -> a2[j] < v) /\
(forall j: int. m < j < r -> v <= a2[j]) /\
a2[m] = v

(* partitioning Ã  la Bentley, that is

l            i          m          r
+-+----------+----------+----------+
|v|   < v    |    ?     |   >= v   |
+-+----------+----------+----------+     *)

let rec quick_rec (a: array int) (l: int) (r: int) : unit
requires { 0 <= l <= r <= length a }
ensures  { sorted_sub a l r }
ensures  { permut_sub (old a) a l r }
variant  { r - l }
= if l + 1 < r then begin
let v = a[l] in
let m = ref l in
label L in
for i = l + 1 to r - 1 do
invariant { a[l] = v /\ l <= !m < i }
invariant { forall j:int. l < j <= !m -> a[j] < v }
invariant { forall j:int. !m < j <  i -> a[j] >= v }
invariant { permut_sub (a at L) a l r }
label K in
if a[i] < v then begin
m := !m + 1;
swap a i !m;
assert { permut_sub (a at K) a l r }
end
done;
label M in
swap a l !m;
assert { qs_partition (a at M) a l !m r v };
label N in
quick_rec a l !m;
assert { qs_partition (a at N) a l !m r v };
label O in
quick_rec a (!m + 1) r;
assert { qs_partition (a at O) a l !m r v };
assert { qs_partition (a at N) a l !m r v };
end

let quicksort (a: array int) =
ensures { sorted a }
ensures { permut_all (old a) a }
quick_rec a 0 (length a)

end

(* Instantiate leftover sort routine. *)
module ShearSortComplete
use Quicksort

clone ShearSort with val sort = quicksort

end

```

# Why3 Proof Results for Project "verifythis_2021_shearsort"

## Theory "verifythis_2021_shearsort.ShearSort": fully verified

 Obligations Alt-Ergo 2.3.3 Alt-Ergo 2.4.1 CVC4 1.7 CVC4 1.8 Eprover 2.0 Z3 4.8.6 VC for transpose_count --- --- --- --- --- --- split_goal_right assertion --- --- 0.25 --- --- --- variant decrease --- --- 0.11 --- --- --- precondition --- --- 0.12 --- --- --- postcondition --- --- --- --- --- 0.07 precondition --- --- 0.12 --- --- --- variant decrease --- --- 0.10 --- --- --- precondition --- --- 0.13 --- --- --- precondition --- --- 0.19 --- --- --- postcondition --- --- 0.22 --- --- --- VC for permut_swap --- --- 0.39 --- --- --- split_goal_right assertion --- --- 0.11 --- --- --- assertion --- --- 0.11 --- --- --- assertion --- --- 0.08 --- --- --- assertion --- --- 0.12 --- --- --- postcondition --- --- 0.13 --- --- --- VC for numoff_occ --- --- --- --- --- --- split_goal_right variant decrease --- --- 0.07 --- --- --- precondition --- --- 0.10 --- --- --- precondition --- --- 0.07 --- --- --- precondition --- --- 0.08 --- --- --- postcondition --- --- 0.24 --- --- --- VC for permut_numoff --- --- --- --- --- --- split_goal_right variant decrease --- --- 0.19 --- --- --- precondition --- --- 0.14 --- --- --- precondition --- --- 0.14 --- --- --- variant decrease --- --- 0.07 --- --- --- precondition --- --- 0.16 --- --- --- precondition --- --- 0.15 --- --- --- postcondition --- --- 0.15 --- --- --- postcondition --- --- 0.11 --- --- --- postcondition --- --- 0.22 --- --- --- precondition --- --- 0.08 --- --- --- precondition --- --- 0.16 --- --- --- precondition --- --- 0.10 --- --- --- precondition --- --- 0.16 --- --- --- precondition --- --- 0.14 --- --- --- precondition --- --- 0.11 --- --- --- precondition --- --- 0.12 --- --- --- precondition --- --- 0.12 --- --- --- variant decrease --- --- 0.21 --- --- --- precondition --- --- 0.08 --- --- --- precondition --- --- 0.10 --- --- --- postcondition --- --- 0.12 --- --- --- VC for sort_row --- --- --- --- --- --- split_goal_right array creation size --- --- 0.13 --- --- --- loop invariant init --- --- 0.15 --- --- --- index in matrix bounds --- --- 0.19 --- --- --- index in array bounds --- --- 0.06 --- --- --- loop invariant preservation --- --- 0.18 --- --- --- assertion --- --- 0.20 --- --- --- loop invariant init --- --- 0.08 --- --- --- loop invariant init --- --- 0.11 --- --- --- loop invariant init --- --- 0.07 --- --- --- loop invariant init --- --- 0.09 --- --- --- loop invariant init --- --- 0.17 --- --- --- index in array bounds --- --- 0.14 --- --- --- index in array bounds --- --- 0.08 --- --- --- index in array bounds --- --- 0.17 --- --- --- index in array bounds --- --- 0.15 --- --- --- precondition --- --- 0.17 --- --- --- precondition --- --- 0.19 --- --- --- precondition --- --- 0.14 --- --- --- loop variant decrease --- --- 0.17 --- --- --- loop invariant preservation --- --- 0.14 --- --- --- loop invariant preservation --- --- 0.13 --- --- --- loop invariant preservation --- --- 0.18 --- --- --- loop invariant preservation --- --- --- --- --- 0.08 loop invariant preservation --- --- 0.24 --- --- --- loop invariant init --- --- 0.10 --- --- --- loop invariant init --- --- 0.06 --- --- --- index in array bounds --- --- 0.16 --- --- --- index in matrix bounds --- --- 0.18 --- --- --- loop invariant preservation --- --- 0.19 --- --- --- loop invariant preservation --- --- 0.20 --- --- --- assertion --- --- 0.16 --- --- --- postcondition --- --- 0.20 --- --- --- postcondition --- --- 0.12 --- --- --- postcondition --- --- 0.22 --- --- --- out of loop bounds --- --- 0.12 --- --- --- loop invariant init --- --- 0.11 --- --- --- loop invariant init --- --- 0.08 --- --- --- index in array bounds --- --- 0.17 --- --- --- index in matrix bounds --- --- 0.18 --- --- --- loop invariant preservation --- --- 0.18 --- --- --- loop invariant preservation --- --- 0.08 --- --- --- assertion --- --- 0.16 --- --- --- postcondition --- --- 0.17 --- --- --- postcondition --- --- 0.09 --- --- --- postcondition --- --- 0.10 --- --- --- out of loop bounds --- --- 0.11 --- --- --- out of loop bounds --- --- 0.14 --- --- --- VC for sort_column --- --- --- --- --- --- split_goal_right array creation size --- --- 0.16 --- --- --- loop invariant init --- --- 0.12 --- --- --- index in matrix bounds --- --- 0.17 --- --- --- index in array bounds --- --- 0.17 --- --- --- loop invariant preservation --- --- 0.17 --- --- --- assertion --- --- 0.15 --- --- --- loop invariant init --- --- 0.12 --- --- --- loop invariant init --- --- 0.10 --- --- --- index in array bounds --- --- 0.15 --- --- --- index in matrix bounds --- --- 0.10 --- --- --- loop invariant preservation --- --- 0.18 --- --- --- loop invariant preservation --- --- 0.20 --- --- --- assertion --- --- 0.16 --- --- --- postcondition --- --- 0.18 --- --- --- postcondition --- --- 0.11 --- --- --- postcondition --- --- 0.10 --- --- --- out of loop bounds --- --- 0.12 --- --- --- out of loop bounds --- --- 0.09 --- --- --- VC for sort_all_rows --- --- --- --- --- --- split_goal_right loop invariant init --- --- 0.15 --- --- --- loop invariant init --- --- 0.10 --- --- --- precondition --- --- 0.10 --- --- --- precondition --- --- 0.07 --- --- --- assertion --- --- 0.18 --- --- --- loop invariant preservation --- --- 0.11 --- --- --- loop invariant preservation --- --- 0.13 --- --- --- postcondition --- --- 0.17 --- --- --- postcondition --- --- 0.16 --- --- --- out of loop bounds --- --- 0.13 --- --- --- VC for sort_all_columns --- --- --- --- --- --- split_goal_right witness existence --- --- 0.08 --- --- --- loop invariant init --- --- 0.13 --- --- --- loop invariant init --- --- 0.11 --- --- --- precondition --- --- 0.17 --- --- --- assertion --- --- 0.25 --- --- --- loop invariant preservation --- --- 0.09 --- --- --- loop invariant preservation --- --- 0.16 --- --- --- postcondition --- --- 0.13 --- --- --- postcondition --- --- 0.15 --- --- --- out of loop bounds --- --- 0.08 --- --- --- precondition --- --- 0.07 --- --- --- assertion --- --- 0.11 --- --- --- loop invariant init --- --- 0.09 --- --- --- loop invariant init --- --- 0.08 --- --- --- precondition --- --- 0.13 --- --- --- assertion --- --- 0.14 --- --- --- loop invariant preservation --- --- 0.21 --- --- --- loop invariant preservation --- --- 0.20 --- --- --- precondition --- --- 0.15 --- --- --- assertion --- --- 0.25 --- --- --- postcondition --- --- 0.17 --- --- --- postcondition --- --- 0.17 --- --- --- out of loop bounds --- --- 0.14 --- --- --- VC for shear_sort --- --- --- --- --- --- split_goal_right loop invariant init --- --- 0.13 --- --- --- loop invariant init --- --- 0.08 --- --- --- loop invariant init --- --- --- --- --- 0.04 precondition --- --- 0.08 --- --- --- assertion --- 0.02 --- --- --- --- assertion 0.10 --- --- --- --- --- assertion 0.13 --- --- --- --- --- loop variant decrease --- --- 0.11 --- --- --- loop invariant preservation --- --- 0.08 --- --- --- loop invariant preservation --- --- --- --- 0.35 --- loop invariant preservation --- --- 0.10 --- --- --- assertion --- --- 0.08 --- --- --- assertion --- --- 0.08 --- --- --- assertion --- --- --- --- --- --- split_goal_right VC for shear_sort --- --- 0.19 --- --- --- VC for shear_sort --- --- 0.17 --- --- --- VC for shear_sort --- --- 0.18 --- --- --- postcondition --- --- 0.12 --- --- --- postcondition --- --- 0.06 --- --- --- loop invariant init --- --- 0.13 --- --- --- loop invariant init --- --- 0.12 --- --- --- loop invariant init --- --- 0.14 --- --- --- loop invariant init --- --- 0.07 --- --- --- loop invariant init --- --- 0.10 --- --- --- loop invariant init 0.05 --- --- --- --- --- loop invariant init --- --- 0.08 --- --- --- loop invariant init --- --- 0.09 --- --- --- assertion --- --- --- --- --- --- split_goal_right assertion --- --- 0.20 --- --- --- VC for shear_sort --- --- --- 0.21 --- --- VC for shear_sort --- --- 0.14 --- --- --- VC for shear_sort --- --- 0.11 --- --- --- VC for shear_sort --- --- 0.13 --- --- --- assertion --- --- --- --- --- --- split_goal_right assertion --- --- 0.19 --- --- --- VC for shear_sort --- --- 0.18 --- --- --- VC for shear_sort --- --- 0.23 --- --- --- VC for shear_sort --- --- 0.12 --- --- --- VC for shear_sort --- --- 0.10 --- --- --- assertion --- --- --- --- --- --- split_goal_right assertion --- --- --- 0.19 --- --- VC for shear_sort --- --- 0.22 --- --- --- precondition --- --- 0.12 --- --- --- assertion --- --- 0.12 --- --- --- assertion --- --- 0.17 --- --- --- variant decrease --- --- 0.19 --- --- --- precondition --- --- 0.14 --- --- --- postcondition --- --- 0.16 --- --- --- assertion --- --- 0.21 --- --- --- assertion --- --- 0.19 --- --- --- variant decrease --- --- 0.17 --- --- --- precondition --- --- 0.14 --- --- --- postcondition --- --- --- 0.21 --- --- loop invariant init --- --- 0.18 --- --- --- loop invariant init --- --- 0.18 --- --- --- loop invariant init --- --- 0.16 --- --- --- loop invariant init --- --- 0.19 --- --- --- variant decrease --- --- 0.09 --- --- --- precondition --- --- 0.20 --- --- --- precondition --- --- 0.19 --- --- --- postcondition --- --- 0.19 --- --- --- postcondition --- --- 0.19 --- --- --- loop invariant init --- --- 0.20 --- --- --- loop invariant init --- --- 0.17 --- --- --- loop variant decrease --- --- 0.17 --- --- --- loop invariant preservation --- --- 0.14 --- --- --- loop invariant preservation --- --- 0.20 --- --- --- postcondition --- --- 0.21 --- --- --- postcondition --- --- 0.20 --- --- --- precondition --- --- 0.16 --- --- --- precondition --- --- 0.21 --- --- --- precondition 0.26 --- --- --- --- --- assertion --- --- --- 0.55 --- --- loop variant decrease --- --- 0.08 --- --- --- loop invariant preservation --- --- 0.16 --- --- --- loop invariant preservation --- --- 0.15 --- --- --- loop invariant preservation --- --- 0.09 --- --- --- loop invariant preservation --- --- --- 0.24 --- --- assertion --- --- --- 0.56 --- --- loop variant decrease --- --- 0.08 --- --- --- loop invariant preservation --- --- 0.24 --- --- --- loop invariant preservation --- --- 0.17 --- --- --- loop invariant preservation --- --- 0.10 --- --- --- loop invariant preservation --- --- --- 0.24 --- --- postcondition --- --- --- --- --- --- split_goal_right VC for shear_sort --- --- 0.22 --- --- --- VC for shear_sort --- --- 0.16 --- --- --- VC for shear_sort --- --- 0.20 --- --- --- VC for shear_sort --- --- 0.25 --- --- --- VC for shear_sort --- --- --- 0.35 --- --- VC for shear_sort --- --- --- 2.64 --- --- postcondition --- --- 0.18 --- --- --- postcondition --- --- 0.18 --- --- --- assertion --- --- 0.23 --- --- --- postcondition --- --- 0.25 --- --- --- assertion --- --- --- 0.36 --- --- precondition --- --- 0.24 --- --- --- precondition 0.16 --- --- --- --- --- precondition --- --- 0.23 --- --- --- precondition --- --- 0.24 --- --- --- precondition --- --- 0.24 --- --- --- precondition --- --- 0.26 --- --- --- precondition --- --- 0.27 --- --- --- precondition --- --- 0.27 --- --- --- assertion --- --- --- --- --- --- split_goal_right VC for shear_sort --- --- --- 1.04 --- --- VC for shear_sort --- --- --- 0.34 --- --- postcondition --- --- 0.21 --- --- --- variant decrease --- --- 0.23 --- --- --- precondition --- --- 0.22 --- --- --- precondition --- --- 0.27 --- --- --- precondition --- --- 0.28 --- --- --- postcondition --- --- 0.30 --- --- --- precondition --- --- 0.21 --- --- --- precondition --- --- --- 0.61 --- --- precondition --- --- 0.27 --- --- --- precondition --- --- 0.21 --- --- --- precondition --- --- 0.74 --- --- --- precondition --- --- 0.28 --- --- --- variant decrease --- --- 0.13 --- --- --- precondition --- --- 0.21 --- --- --- precondition --- --- --- 0.75 --- --- postcondition --- --- --- 0.44 --- --- precondition --- --- 0.19 --- --- --- precondition --- --- --- 0.39 --- --- postcondition --- --- 0.34 --- --- --- assertion --- --- --- 0.43 --- --- variant decrease --- --- 0.20 --- --- --- precondition --- --- --- 0.30 --- --- precondition --- --- --- 2.51 --- --- precondition --- --- --- 0.55 --- --- postcondition --- --- 0.08 --- --- --- precondition --- --- 0.22 --- --- --- precondition --- --- --- 0.39 --- --- assertion --- --- --- --- --- --- split_goal_right assertion --- --- 0.34 --- --- --- assertion --- --- 0.27 --- --- --- assertion --- --- --- 1.37 --- --- precondition --- --- 0.26 --- --- --- precondition --- --- --- --- --- 0.78 precondition --- --- 0.19 --- --- --- postcondition --- --- 0.22 --- --- --- variant decrease --- --- 0.21 --- --- --- precondition --- --- 0.26 --- --- --- precondition --- --- --- 0.80 --- --- precondition --- --- --- 0.57 --- --- postcondition --- --- 0.11 --- --- --- precondition --- --- 0.23 --- --- --- precondition --- --- --- 0.40 --- --- assertion --- --- --- --- --- --- split_goal_right assertion --- --- 0.35 --- --- --- assertion --- --- 0.28 --- --- --- assertion --- --- --- 0.38 --- --- precondition --- --- --- --- --- --- split_goal_right VC for shear_sort --- --- 0.30 --- --- --- VC for shear_sort --- --- 0.14 --- --- --- precondition --- --- --- --- --- 0.21 precondition --- --- --- 0.26 --- --- postcondition --- --- 0.21 --- --- --- assertion --- --- 0.30 --- --- --- assertion --- --- --- --- --- --- split_goal_right VC for shear_sort 0.10 --- --- --- --- --- VC for shear_sort 0.06 --- --- --- --- --- VC for shear_sort --- --- 0.12 --- --- --- assertion --- --- --- --- --- --- split_goal_right VC for shear_sort --- --- 0.26 --- --- --- VC for shear_sort 0.05 --- --- --- --- --- VC for shear_sort --- --- 0.12 --- --- --- loop invariant preservation --- --- 0.29 --- --- --- loop invariant preservation --- --- 0.28 --- --- --- loop invariant preservation --- --- --- 0.47 --- --- loop invariant preservation --- --- --- 0.46 --- --- loop invariant preservation --- --- 0.24 --- --- --- loop invariant preservation --- --- 0.23 --- --- --- loop invariant preservation --- --- --- 0.45 --- --- loop invariant preservation --- --- 0.29 --- --- --- precondition --- --- 0.17 --- --- --- precondition --- --- --- --- --- --- split_vc precondition 0.08 --- --- --- --- --- precondition --- --- 0.18 --- --- --- precondition --- --- 0.19 --- --- --- postcondition --- --- 0.16 --- --- --- postcondition --- --- 0.15 --- --- --- postcondition --- --- 0.14 --- --- --- out of loop bounds --- --- 0.17 --- --- --- postcondition --- --- 0.15 --- --- --- postcondition --- --- 0.15 --- --- --- postcondition --- --- 0.07 --- --- ---

## Theory "verifythis_2021_shearsort.Quicksort": fully verified

 Obligations Alt-Ergo 2.3.3 CVC4 1.7 Z3 4.8.6 VC for quick_rec --- --- --- split_goal_right index in array bounds --- 0.08 --- loop invariant init --- 0.06 --- loop invariant init --- 0.07 --- loop invariant init --- 0.07 --- loop invariant init --- 0.12 --- index in array bounds --- 0.13 --- precondition --- 0.12 --- assertion --- 0.16 --- loop invariant preservation --- 0.08 --- loop invariant preservation --- 0.10 --- loop invariant preservation --- 0.15 --- loop invariant preservation --- 0.11 --- loop invariant preservation --- 0.08 --- loop invariant preservation --- 0.09 --- loop invariant preservation --- 0.10 --- loop invariant preservation --- 0.09 --- precondition --- 0.08 --- assertion --- --- 0.10 variant decrease --- 0.10 --- precondition --- 0.08 --- assertion 0.21 --- --- variant decrease --- 0.07 --- precondition --- 0.07 --- assertion 0.19 --- --- assertion --- 0.10 --- postcondition --- 0.16 --- postcondition --- 0.20 --- out of loop bounds --- 0.08 --- postcondition --- 0.11 --- postcondition --- 0.10 --- VC for quicksort --- 0.09 ---

## Theory "verifythis_2021_shearsort.ShearSortComplete": fully verified

 Obligations CVC4 1.7 VC for sort'refn 0.22