Verification of the ShearSort algorithm

This page gives a description of the verification of the ShearSort algorithm with KIV, that sorts a matrix using parallel sorts of rows and columns. The verification of this algorithm was one of the challenges of the VerifyThis competition 2021. A description of the challenge can be found at: Challenge 3 - ShearSort ⤓ (PDF) (external link to ETH Zürich)

More details on the concepts used here are now given in the submitted paper [KIV21] (a copy can be obtained by mailing the authors).

Check the overview over the specifications first. From there you can also find links to the theorem base of each specification, and to all proofs. Here is a description of the main important ones:

• Specifications matrix, matrix+array, and rwocol-upd specify (two-dimensional) matrices and operations on them, e.g. "#r mx" is its number of rows "mx[m,n,a]" is the modified matrix mx, where The element in row m, column n has been updated to a. "mx.toArr" concatenates the rows of the matrix into one array, "mx.toArc" does the same, but column-wise.
• The basic predicate used is count(a, p) from specification filter-count, which counts the number of elements that satisfy predicate p. Since this is a generally useful predicate, its specification has been put into the library. It is used with p = "λ j. j < i" to count the number of elements less than i (i.e. zeros) and with p = "λ j. ¬ j < i" to count the number of ones. A "clean0row" is a row where this count is zero, i.e. where all elements are less than i.
• Predicates #clean0rows" and "#clean1rows" from the toplevel specification ShearSort count the number of consecutive clean rows from the bottom/top with respect to element i. "#dirtyrows" are the other rows in the middle of the matrix, and "mx.dirtyrows≤(bound)" states that there at most bound dirty rows. Initially, predicats #clean0rows/#clean1rows were specified to count all rows that have 0/1 only (not just the consecutive ones at the bottom /top), but with this definition the main lemma "every iteration (consisting of sorting rows/columns) halves #dirtyrows" is not provable.
• "colsorted(mx0, n, mx)" specifies that matrix mx is a permutation of matrix mx0, where the first n columns have been sorted (in ascending order), while the remaining ones are identical. The index n is needed while sorting columns, the index is equal to "#c mx" after the loop.
• Similarly, "srowsorted(mx0, n, mx)" specifies that the first n columns of mx0 have been snake-sorted in mx: Even rows have been sorted in ascending order, odd rows in descending order (where sorted in descending order is described simply sorted in ascending order for the reverted row). Note that "srowsorted(mx, #r mx, mx)" simply indicates that all rows are snake-sorted.
• "rowsincreasing(mx,r)" indicates that all rows below row r are increasing: the elements in row r0 are all smaller than each element from row r1, when r0 < r1 < r. In the proof the predicate is always used with r = #r mx, the second argument is just used for inductive lemmas.

• The algorithms to sort a row in ascending order (psortrow#) and a row in descending order (psortrowrev#) are derived from the algorithm to sort a color using two instantiations. The first swaps rows and columns, the second exchanges the order on elements with its dual order.
• Sorting all rows/columns in parallel is specified using the "forall∥nf" operator (the "nf" indicates that concurrency is not assumed to be fair here). The RG calculus rule to handle this construct is detailed in [KIV21]. It is applied three times:
  • in the proof, that sorting columns (psortcols#) is correct.
  • in the proof that sorting rows (psortsrows#) is correct and
  • finally in the proof that snake-sorting rows (psortsrows#) is correct, where lemma sortrowsnake-correct is used that combines the two cases of sorting a single even or odd row into one lemma.
• The main loop of shearsort maintains the crucial invariant "mx.dirtyrows≤((#r mx) /↑ (2^ n))" where n is the number of iterations that the loop has already done (where "m /↑ n" is integer division, but rounding up). Proving this invariant (and understanding why it holds) is the main difficulty of the proof, that we will detail below.

• sorting rows never changes #clean0rows or #clean1rows" as stated by lemmas rowperms-clean0unchanged and rowperms-clean1unchanged. Therefore the number of dirty rows also stays the same when sorting rows.
• The main difficulty for showing that the invariant of shearsort holds is therefore to show that when a rowsorted matrix mx0 is sorted column-wise the resulting matrix mx has at most half the dirtyrows of the mx0. This is asserted by lemma colsort-dirtyboundhalf. We could not find a precise argument on the internet, our proof essentially follows the proof of [Hagerup16]. The proof is broken down into several lemmas:
  • First, the final matrix mx has a column cmax with a maximum number n of zeros (Lemma exists-max0column proves that every matrix has such a column). Since mx is column-sorted, the 0's in column cmax are in the first n rows (Lemma sortedperm-count-splits), and all rows above n are 1's only.
  • Since all other columns have fewer 0's (also in low rows) it is implied that the number of clean 1-rows in mx is #r mx - n as stated by Lemma max0column-determines-clean1rows.
  • The number of zeros in column cmax of mx0 is n too (column-sorting does not change this number), and since all rows below #clean0rows(mx0) contain 0's only, there must be some k >= 0 of extra rows such that n = #clean0rows(mx0,i) + k. k can be at most the number of dirty rows in mx0, since no zero is in a clean 1-row of mx0. The k additional 0's in column cmax are distributed among even and odd rows, so counting zeros in even/odd rows in mx0[cmax]c above #clean0rows(mx0) will give two number keven and kodd, such that k = keven + kodd.
  • Formally, "countevn(a, p)/countodd(a, p)" are used count the elements of an array (here: a column of the matrix) that have an even/odd index and satisfy predicate p. Since k ≤ #dirtyrows(mx0, i), we get that both keven, kodd ≤ #dirtyrows(mx0, i) /↑ 2 (Lemmas countevn-maxcol0-bounded and countodd-maxcol0-bounded).
  • Since mx0 is snakerow-sorted, all columns left of cmax have at least keven zero's, all columns right of cmax have at least kodd zeros above #clean0rows(mx0,i). (Lemma rowsorted-smallercol-evnbounded and rowsorted-biggercol-oddbounded). Therefore every column of mx0 has at least #clean0rows(mx0,i) + min(keven,kodd) zeros.
  • Again, since the number of zero's in a column does not change (Lemma max0column-clean0rowsbounded) the number #clean0rows(mx,i) of clean 0-rows in mx is at least #clean0rows(mx0,i) + min(keven,kodd) too. Combining these facts, the number of clean 0-rows increases by min(keven,kodd), the number of clean 1-rows drops by #dirtyrows(mx0,i) - k, Since k - min(keven,kodd) = max(keven,kodd) ≤ #dirtyrows(mx0, i) /↑ 2 the main lemma colsort-dirtyboundhalf is implied.
• After "log2↑(#r mx)" iterations (where log2↑(0) = 1, and log2↑(n) is the logarithm with base 2 rounded up to the next integer otherwise) of row and column sorting the number of dirty columns has decreased to at most one (see Lemma log2ub-lem). Since this is the case for every element i, it can be proved that the matrix then has increasing rows, i.e rowsincreasing(mx,#r mx)". This is stated by Lemma dirtyrowsone-rowsincreasing. With increasing rows, sorting all rows in ascending order produces a sorted (not snake-sorted!) matrix, expressed as the postcondition "ordered≤(mx.toArr)" of the total correctness theorem pshearsort-correct.

Bibliography

Used basic libraries:

• The basic KIV library with basic data types
• The KIV separation library gives an embedding of Separation Logic with separation formulas and reasoning support

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

[Imprint] [Data Privacy Statement]