This Website documents the KIV solutions of the VerifyThis Competition held at ETAPS 2021 in Luxembourg, Luxembourg (virtual event). All proofs for challenge 2 were done during the competition, the solutions for challenges 1 and 3 were completed after the event.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.

The **Project Overview** gives an overview of the entire specification hierarchy of our solution for challenge 1.

We were able to solve all tasks of Challenge 2 during the competition because we could use our library for Separation Logic as seen in the **Project Overview**.
Here the heap is defined as an algebraic data type over references `r`

and objects `o`

with operations for allocation (`h ++ r`

), deallocation (`h -- r`

), and reading or updating objects at certain locations (`h[r]`

or `h[r, o]`

resp.).
The specification heap-sep defines the common Separation Logic operators like the separating conjunction or the separating implication as higher order predcicates over the heap.
The library also provides a heap-based definition of binary trees using generic nodes with left and right pointers.
We reused these nodes for our definition of doubly-linked lists.
The predicate `dll(r, x)(h)`

abstracts the content of a heap `h`

to an algebraic list `x`

starting from reference `r`

.
An auxiliary predicate `dlls(r, r0, r1, x)(h)`

is used to describe list segments in the heap, the references `r0`

and `r1`

point to the nodes to the left and right of the segment.
Thus, `dlls(r, null, null, x)`

is equivalent to `dlls(r, x)`

.

Having abstractions of the heap content to algebraic lists and to algebraic trees allows to formulate the required properties using these algebraic data types.
The specification linked-tree-list defines the predicates `ordered≤(t)`

and `balanced(t)`

that in combination ensure that the algebraic tree `t`

is a balanced search tree.
An additional function `t.toList`

calculates a algebraic list for a tree `t`

that contains the same elements as `t`

and maintains the order of `t`

.

The algorithm for the construction of the binary search tree is implemented in the specification DLL2BST with the procedure `dll_to_bst#`

.
The auxiliary procedures `size#`

and `dll_to_bst_rec#`

are implemented in this specification as well.
Note that we used natural numbers instead of integers in the declarations since negative values are not relevant for the task.

First, we proved the correctness of the `size#`

procedure with the lemma dll-size-correct which states that if we have a valid doubly-linked list in the heap representing an algebraic list `x`

, the result in `count`

is the length `# x`

of the list.
The proof is by induction over the length of the list and was straightforward, however it was necessary to generalize the lemma by allowing a list segment separated from an arbitrary heap predicate `hP`

.

The main effort was to prove the contract for `dll_to_bst_rec#`

.
We have to ensure that, given a valid list segment `x`

in the heap, the execution of `dll_to_bst_rec#`

yields a heap that contains the list segment `x`

without its first `n`

elements (`restn(n, x)`

) and a balanced tree t containing the first n elements of `x`

(`t.toList = firstn(n, x)`

).
The contract can be proven by induction over `n`

, which again requires generalization to a heap with an additional separated heap predicate `hP`

.
After applying the induction hypothesis for both recursive calls it remains mainly to show that both subtrees and the new root node form a combined tree, see goal.

... (right0 => mknode(left0, b, root0) * tr(left0, t) * tr(root0, t0) * ...)(h2) ... ⊦ ∃ t. (tr(right0, t) * ...)(h2) ...This is done with a few interactions by choosing the algebraic tree

`mkbranch(t, b, t0)`

for `t`

and applying some lemmas from the Separation Logic library.
The balanced and same-elements properties for the combined tree are proven automatically using lemmas from linked-tree-list.
Finally, the main proof obligation dll_to_bst_correct can be proven by simply applying the contracts of the two auxiliary procedures:

dll(head, x)(h), ordered≤(x) ⊦ ⦉dll_to_bst#(head; h; root)⦊ ∃ t. tr(root, t)(h) ∧ t.toList = x ∧ ordered≤(t) ∧ balanced(t)Note that we did not have to prove in dll_to_bst_rec_correct that the resulting tree is

`ordered≤`

.
Instead, `ordered≤(t)`

follows directly from `ordered≤(x)`

and `t.toList = x`

(see this lemma).
We also solved the additional task and implemented an iterative version of `size#`

: `size_iter#`

.
The correctness proof dll-size-iter-correct could be performed analogously using induction over the length of the list and the correctness of the corresponding main procedure `dll_to_bst_iter#`

is again proven by using the contracts dll-size-iter-correct and dll_to_bst_rec_correct, see dll_to_bst_iter_correct.

**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.