# Evaluating Rust Verifier’s Suitability for the Verification of Rust's Sorting Algorithm

## I. Introduction

Rust is an open-source systems programming language that focuses on speed, memory safety and parallelism. Developers are using Rust to create a wide range of new software applications, such as game engines, operating systems, file systems, browser components and simulation engines for virtual reality[1]. Rust’s standard library algorithms are used in the development of many of these applications, and are assumed to be correct. However, this might not always be the case, as some library implementations of famous algorithms turned out to be buggy in the past, like the Java’s OpenJDK TimSort implementation[2]. One of the ways of making sure that a certain algorithm is correct is by using formal verification.

Software formal verification is used to prove that an algorithm works as intended by making sure that it satisfies some formal specifications stated by the programmer. This can help ensure that an algorithm is correct without the need of running it on a large set of test cases that might be missing a corner case.

Software tools, called verifiers, have been developed to add support for formal verification in different programming languages. One of these tools is Prusti, which is a Rust verifier that allows the verification of the correctness of Rust programs. This is done by allowing the programmer to add functional specifications to Rust code and then Prusti verifies that the code satisfies these conditions.

Code here to show example of verification

> Explanation of code here

Improving software verification tools is important as it makes the verification of different algorithms easier, faster and cheaper. This is achieved by extending their capabilities to enable the verification of additional and more complex parts of the code like closuers, deal with complex mathematical structures like sets and sequences, and decrease the verification time. Deciding on which features to add or change in Prusti requires evaluating its suitability for the verification of different algorithms and then compare these verification attempts with previous ones done with other verification tools.

Previous research tackled the formal verification of algorithms in Prusti. As we can see in the attempt of verifying sorting in rust by (Schilling, 2021)[3]. In their work, an implementation of Selection Sort was verified, it was mentioned that some features were required to be implemented in order to verify Rust’s standard library stable sorting algorithm, which is based on TimSort. TimSort is infamous for its buggy implementations[2], which makes it an ideal candidate to attempt to formally verify it with Prusti.

The main goal of the thesis is to evaluate Prusti's suitability for the verification of TimSort, and based on the results determine which features needs to be added to make the verification easier.

## II. Our Approach

### 1. Algorithm Description

We will start by explaining how TimSort algorithm works.

The current implementation of TimSort in Rust standard library is an adaptive, iterative merge sort algorithm that combines insertion sort and merge sort. It starts by trying to partition the input array into a series of sorted parts. This is done by finding the maximum length of a sorted subarray from the start of the input array. If its length is too short, then this sorted subarray is expanded using insertion sort (but its maximum size will be 20). After identifying these sorted subarrays, they are called runs and put into a stack.

The stack has pending runs that will be merged together by the end of the algorithm to make the final sorted array. When a new run is inserted into the stack, the algorithm merges two runs from the three runs on top of the stack, turning them into one run. This is done several times and stops when the following conditions are met
1. $$\forall i \in 1..\text{runs_stack.len()} \, . \, \text{runs} \_ \text{stack[i - 1].len()} > \text{runs} \_ \text{stack[i].len()} $$
2. $$\forall i \in 2..\text{runs_stack.len()} \, . \, \text{runs} \_ \text{stack[i - 2].len()} > \text{runs} \_ \text{stack[i - 1].len()} + \text{runs} \_ \text{stack[i].len()} $$
3. $$\forall i \in 3..\text{runs_stack.len()} \, . \, \text{runs} \_ \text{stack[i - 3].len()} > \text{runs} \_ \text{stack[i - 2].len()} + \text{runs} \_ \text{stack[i - 1].len()} + \text{runs} \_ \text{stack[i].len()} $$

> runs_stack is the stack that contains the sorted subarrays called runs. runs_stack.len() - 1 is the index of the run at top of stack. runs_stack[i].len indicates the number of elements in the ith run.

### 2. Algorithm Verification

After giving an overview of the main parts of the algorithm, we need to tackle the problem of verifying the termination and the correctness of the algorithm.

#### A. Abscence of Panics

In order to make sure that the algorithm is working correctly, we need to verify that the algorithm terminates successfully, which means that it does not produce run-time errors. Rust deals with error handling a little different than other languages. It groups errors into two categories. The first one is recoverable errors, these are errors that do not require program termination, an example is a file not found error, it’s reasonable to report the problem to the user and retry the operation. In the case of recoverable errors a data type `Result<T, E>` is returned that carries information about the error, and the program continues execution normally. The second category is unrecoverable errors, these are serious errors that point to a bug, one example is trying to access a location out of an array’s bounds. In this case, the program terminates. Unrecoverable errors are fired using `panic!` macros[4].

In the implementation of TimSort in Rust, the sorting function might panic if the `is_less` comparator function panics[5], we will try to verify that in case `is_less` does not panic, then the code will be fully executed and terminate successfully. We will work on verifying that the algorithm terminates and does not panic.

#### B. Correctness

After verifying the abscence of panics, we also need to make sure that the algorithm produces correct output, by verifying that the sorting is done correctly. To do that, we need to determine the formal specifications needed to prove the correctness of the algorithm, we will build on previous research to determine the specifications, mainly the verification of Java’s OpenJDK’s TimSort algorithm by de Gouw et al. [2].

We will figure out the necessary specification to prove that these two main properties hold:
1. The sortedness property: This will involve verifying that the output array after the execution of the algorithm is sorted correctly.
2. The permutation property: This will involve verifying that the output array’s elements are a permutation of the of the input array’s elements.

Using Prusti to do the verification will require re-writing some parts of the code that are unsupported like unsafe code, closures, iterators and reference-typed fields. Our goal will be to verify TimSort algorithm's correctness with the current capabilities of Prusti.

### 3. Prusti's Verification Suitability

After verifying the correction of the algorithm and the abscence of panics using Prusti. We will evaluate our verification experience, and compare it to the verification of the same algorithm using other verification tools. This comparison will be based on data like which properties could be verified, how many lines of specifications were needed, how much time the verifier takes to verify the code examples, and the amount of code that needs to be re-written by the programmer to verify a program that contains code with functionalities not yet supported by Prusti.

### 4. Improving Prusti

After evaluating the verification of TimSort using Prusti, we will identify which features should be added to Prusti to make the verification effort easier and to verify the algorithm’s original code without the need to re-write some of its parts, which can be determined based on which pieces of code were re-written during the verification stage. Additionally, We will choose the most important features from the identified list of the features needed to make verifing the algorithm easier, and we will add support for them in Prusti.

### 5. Extra Goals

After achieving our main goal of evaluating Prusti's suitability for algorithms verification, we will try to extend our work by completing extra goals. We will work on ensuring panic safety, that means making sure through formal verification that in case a panic occurs, the input array’s data will not be lost or incorrectly altered in memory, simply, we need to show that in case of early termination of the algorithm, the array in the memory is still a permutation of the original input array. The integrity of the array’s data in case of a panic is said to be guaranteed by the algorithm, we will make sure that this is the case.

Finally, we will work on verifying the correctness of one or more of the other heavily-used algorithms in the standard library. Some examples are the binary search algorithm (binary_search), Rust’s QuickSelect algorithm (select_nth_unstable), and Rust’s QuickSort-based unstable sorting algorithm (unstable_sort). Some of these algorithms like binary search were previously verified using other tools, we can verify them in Prusti and compare the verification experience with the previous attempts.

## III. Core Goals

1. Replace the unsupported features in the implementation with ones that are supported by Prusti.
2. Verifying the absence of panics.
3. Verifying the algorithm’s correctness.
4. Evaluating Prusti’s capability of verifying the algorithm compared to previous attempts with different tools.
5. Identify the features that are missing from Prusti that would make verification easier.

## IV. Extension Goals

1. Implement the most important features identified.
2. Ensuring data integrity if panics happen.
3. Verify another piece of code from the Rust standard library.

## V. Schedule

1. Finish studying Rust and Prusti
1 Week -- 07/03 -> 13/03

2. Replace the unsupported features in the implementation with ones that are supported by Prusti.
1 Week -- 14/03 -> 20/03

3. Verifying the absence of panics - Core Goal 2
2 Weeks - 21/03 -> 03/04

4. Verifying the algorithm - Core Goal 3
3 Weeks - 04/04 -> 24/04

5. Evaluating Prusti’s verification suitability, identify which features are needed in Prusti and writing the corresponding thesis chapter - Core Goal 4, 5
1 Week - 25/04 -> 01/05

6. Extension Goals Part 1
3 Weeks - Week 02/05 -> 22/05

7. Writing the thesis
3 Weeks - 23/05 -> 12/06

8. Extension Goals Part 2
2 Weeks - Week 13/06 -> 26/06

9. Presentation
1 Week - 27/06 -> 03/07

## References

[1] Rust language: https://research.mozilla.org/rust/

+
[2] de Gouw, S., de Boer, F.S., Bubel, R. et al. Verifying OpenJDK’s Sort Method for Generic Collections. J Autom Reasoning 62, 93–126 (2019). https://doi.org/10.1007/s10817-017-9426-4

[3] Schilling, J. (2021). Specifying and Verifying Sequences and Array Algorithms in a Rust Verifier (thesis).

[4] The Rust Programming Language Book: Error Handling https://doc.rust-lang.org/book/ch09-00-error-handling.html

[5] Rust Standard Library sort algorithm source code: https://doc.rust-lang.org/src/alloc/slice.rs.html