VerifyThis 2021: Shearsort (modified)
solution to VerifyThis 2021 challenge 3
Auteurs: Andrei Paskevich / Jean-Christophe Filliâtre
Catégories: Array Data Structure / Sorting Algorithms
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 3: Shearsort
See https://www.pm.inf.ethz.ch/research/verifythis.html
Authors: - Jean-Christophe FilliĆ¢tre (CNRS) - Andrei Paskevich (Univ. Paris-Saclay)
Summary:
- sequential code only (no parallelism in Why3)
- termination verified under some assumptions over the number of
inversions in functions sort_row
and sort_column
- *CHANGE IN CODE*
We were not able to show that ceil(log(n))+1 steps suffices.
Therefore, we replaced the repeat
loop infinite loop from which
we exit as soon as none of the calls to sort_column
makes a
change to the matrix.
We argue that this does not increase the complexity. Indeed, it can be proved, independently, that the loops will never execute more than ceil(log(n))+1 steps. Actually, our change even *improves* the performance of the code, as we may perform fewer steps in some cases (e.g. when the matrix is already snake-sorted).
use int.Int use int.ComputerDivision use matrix.Matrix use map.Occ use int.NumOf use int.Sum meta coercion function elts function mocc (x: int) (m: matrix int) : int = sum (fun i -> occ x (m i) 0 m.columns) 0 m.rows predicate lt (i j k l: int) = i < k \/ i = k /\ if mod i 2 = 0 then j < l else l < j predicate snake_order (m: matrix int) = let rw = m.rows in let cl = m.columns in forall i j k l. 0 <= i < rw -> 0 <= j < cl -> 0 <= k < rw -> 0 <= l < cl -> lt i j k l -> m i j <= m k l function inversions (m: matrix int) : int = sum (fun i -> sum (fun j -> sum (fun k -> numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns) 0 m.rows) 0 m.columns) 0 m.rows let lemma inv_nonneg (m: matrix int) ensures { 0 <= inversions m } = let zero = pure { fun (_:int) -> 0 } in assert { forall i j k. zero k <= numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns }; assert { forall i j. zero j <= sum (fun k -> numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns) 0 m.rows }; assert { forall i. zero i <= sum (fun j -> sum (fun k -> numof (fun l -> lt i j k l /\ m i j > m k l) 0 m.columns) 0 m.rows) 0 m.columns }; assert { 0 = sum zero 0 m.rows <= inversions m }; () predicate sorted_row (m: matrix int) (row: int) (ascending: bool) = 0 <= row < m.rows /\ if ascending then forall j l. 0 <= j <= l < m.columns -> m row j <= m row l else forall j l. 0 <= j <= l < m.columns -> m row j >= m row l val sort_row (m: matrix int) (row: int) (ascending: bool) : unit requires { 0 <= row < m.rows } writes { m } ensures { (* frame *) forall i j. 0 <= i < m.rows -> 0 <= j < m.columns -> i <> row -> m i j = old m i j } ensures { forall x. mocc x m = mocc x (old m) } ensures { sorted_row m row ascending } ensures { inversions m <= old inversions m } predicate sorted_column (m: matrix int) (column: int) = 0 <= column < m.columns /\ forall i k. 0 <= i <= k < m.rows -> m i column <= m k column val sort_column (m: matrix int) (column: int) : (nochange: bool) requires { 0 <= column < m.columns } writes { m } ensures { (* frame *) forall i j. 0 <= i < m.rows -> 0 <= j < m.columns -> j <> column -> m i j = old m i j } ensures { forall x. mocc x m = mocc x (old m) } ensures { nochange -> forall i. 0 <= i < m.rows -> m i column = old m i column } ensures { sorted_column m column } ensures { inversions m <= old inversions m } ensures { not nochange -> inversions m < old inversions m } let shearsort (n: int) (m: matrix int) : unit requires { m.rows = m.columns = n } writes { m } (* TASK 3 *) ensures { snake_order m } (* TASK 2 *) ensures { forall x. mocc x m = mocc x (old m) } = label Init in while true do (* <-- CHANGE instead of ceil(log(n))+1 steps *) invariant { forall x. mocc x m = mocc x (old m) } variant { inversions m } label L1 in for i = 0 to n - 1 do invariant { forall k. 0 <= k < i -> sorted_row m k (mod k 2 = 0) } invariant { forall x. mocc x m = mocc x (old m) } invariant { inversions m <= (inversions m at L1) } sort_row m i (mod i 2 = 0) done; label L2 in let ref nochange = true in for j = 0 to n - 1 do invariant { nochange -> forall i j. 0 <= i < m.rows -> 0 <= j < m.columns -> m i j = (m i j at L2) } invariant { forall l. 0 <= l < j -> sorted_column m l } invariant { forall x. mocc x m = mocc x (old m) } invariant { inversions m <= (inversions m at L2) } invariant { not nochange -> inversions m < (inversions m at L2) } let nch = sort_column m j in if not nch then nochange <- false done; if nochange then break done; let lemma ordered (i j k l: int) requires { 0 <= i < n } requires { 0 <= j < n } requires { 0 <= k < n } requires { 0 <= l < n } requires { lt i j k l } ensures { m i j <= m k l } = if i = k then return; assert { sorted_column m j }; assert { sorted_column m l }; if j <= l then ( if mod i 2 = 0 then assert { m i j <= m i l <= m k l } else ( assert { mod (i+1) 2 = 0 }; assert { sorted_row m (i+1) true }; assert { m i j <= m (i+1) j <= m (i+1) l <= m k l } ) ) in () (* Notes The verification tasks for shearsort are: 1. Verify that shearsort terminates, and is memory safe. PARTIAL: memory safety DONE (enforced by Why3) termination using hypotheses over number of inversions 2. Verify that shearsort permutes the input matrix. DONE 3. Verify that shearsort sorts the matrix in a snake-like manner. DONE 4. Verify that (parallel) shearsort satisfies the same specification as sequenti al shearsort, in which all parallel for-loops are replaced by sequential ones. 5. Verify that shearsort and alternative-shearsort satisfy the same specification. 6. Extra: give implementations to sort-row, sort-column and transpose, and verify these as well. *)
download ZIP archive
Why3 Proof Results for Project "verifythis_2021_shearsort_modified"
Theory "verifythis_2021_shearsort_modified.Top": fully verified
Obligations | CVC5 1.0.5 | Z3 4.12.2 | |||||||
VC for inv_nonneg | --- | --- | |||||||
split_vc | |||||||||
assertion | 0.08 | --- | |||||||
assertion | 0.31 | --- | |||||||
assertion | --- | 0.04 | |||||||
assertion | --- | --- | |||||||
split_vc | |||||||||
assertion | 0.06 | --- | |||||||
assertion | --- | --- | |||||||
unfold inversions | |||||||||
assertion | --- | --- | |||||||
apply sum_le | |||||||||
apply premises | --- | --- | |||||||
split_vc | |||||||||
apply premises | --- | --- | |||||||
compute_specified | |||||||||
apply premises | --- | 0.18 | |||||||
postcondition | 0.06 | --- | |||||||
VC for shearsort | --- | --- | |||||||
split_vc | |||||||||
loop invariant init | 0.04 | --- | |||||||
loop invariant init | 0.03 | --- | |||||||
loop invariant init | 0.05 | --- | |||||||
loop invariant init | 0.03 | --- | |||||||
precondition | 0.03 | --- | |||||||
precondition | 0.04 | --- | |||||||
loop invariant preservation | --- | --- | |||||||
case (k=i) | |||||||||
true case (loop invariant preservation) | 0.06 | --- | |||||||
false case (loop invariant preservation) | 2.34 | --- | |||||||
loop invariant preservation | 0.04 | --- | |||||||
loop invariant preservation | 0.05 | --- | |||||||
loop invariant init | 0.04 | --- | |||||||
loop invariant init | 0.03 | --- | |||||||
loop invariant init | 0.05 | --- | |||||||
loop invariant init | 0.04 | --- | |||||||
loop invariant init | 0.04 | --- | |||||||
precondition | 0.04 | --- | |||||||
loop invariant preservation | 0.06 | --- | |||||||
loop invariant preservation | --- | --- | |||||||
case (l = j) | |||||||||
true case (loop invariant preservation) | 0.06 | --- | |||||||
false case (loop invariant preservation) | --- | --- | |||||||
unfold sorted_column | |||||||||
VC for shearsort | --- | --- | |||||||
split_vc | |||||||||
VC for shearsort | 0.04 | --- | |||||||
VC for shearsort | 0.04 | --- | |||||||
VC for shearsort | --- | --- | |||||||
rewrite Ensures5 | |||||||||
VC for shearsort | --- | --- | |||||||
unfold sorted_column in LoopInvariant4 | |||||||||
VC for shearsort | 0.20 | --- | |||||||
rewrite premises | 0.05 | --- | |||||||
rewrite premises | 0.05 | --- | |||||||
rewrite premises | 0.04 | --- | |||||||
loop invariant preservation | 0.05 | --- | |||||||
loop invariant preservation | 0.05 | --- | |||||||
loop invariant preservation | 0.06 | --- | |||||||
loop invariant preservation | 0.04 | --- | |||||||
loop invariant preservation | --- | --- | |||||||
case (l = j) | |||||||||
true case (loop invariant preservation) | 0.03 | --- | |||||||
false case (loop invariant preservation) | --- | --- | |||||||
unfold sorted_column | |||||||||
VC for shearsort | --- | --- | |||||||
split_vc | |||||||||
VC for shearsort | 0.03 | --- | |||||||
VC for shearsort | 0.05 | --- | |||||||
VC for shearsort | --- | --- | |||||||
rewrite Ensures5 | |||||||||
VC for shearsort | --- | --- | |||||||
rewrite Ensures5 | |||||||||
VC for shearsort | --- | --- | |||||||
unfold sorted_column in LoopInvariant4 | |||||||||
VC for shearsort | 0.08 | --- | |||||||
rewrite premises | 0.06 | --- | |||||||
rewrite premises | 0.06 | --- | |||||||
rewrite premises | 0.04 | --- | |||||||
rewrite premises | 0.06 | --- | |||||||
rewrite premises | 0.06 | --- | |||||||
rewrite premises | 0.05 | --- | |||||||
loop invariant preservation | 0.06 | --- | |||||||
loop invariant preservation | 0.04 | --- | |||||||
loop invariant preservation | 0.04 | --- | |||||||
postcondition | 1.66 | --- | |||||||
assertion | 0.05 | --- | |||||||
assertion | 0.05 | --- | |||||||
precondition | 0.04 | --- | |||||||
assertion | --- | --- | |||||||
split_vc | |||||||||
assertion | 0.24 | --- | |||||||
assertion | 0.07 | --- | |||||||
assertion | 0.19 | --- | |||||||
assertion | 0.16 | --- | |||||||
assertion | --- | --- | |||||||
split_vc | |||||||||
assertion | 0.08 | --- | |||||||
assertion | 0.08 | --- | |||||||
assertion | 0.10 | --- | |||||||
postcondition | 0.71 | --- | |||||||
postcondition | 0.16 | --- | |||||||
postcondition | 0.05 | --- | |||||||
loop variant decrease | --- | --- | |||||||
split_vc | |||||||||
loop variant decrease | 0.05 | --- | |||||||
loop variant decrease | 0.05 | --- | |||||||
loop invariant preservation | 0.04 | --- | |||||||
out of loop bounds | 0.04 | --- | |||||||
out of loop bounds | 0.09 | --- |