Documentation improvements for a Rust verifier
external page Rust is a modern system programming language with a strong focus on speed, safety, and concurrency. Its strong type system prevents most memory-related errors such as dangling references without the need to have a garbage collector. In our group we are developing Prusti, a verifier for Rust programs, that leverages the strong type system to significantly reduce the effort required for proving properties that go beyond simple memory safety. For example, with Prusti one can specify and get automatically checked by the tool that the result of a sorting function is actually sorted. Internally, Prusti translates Rust programs to the Viper intermediate verification language.
Verification of any real-world codebase includes interaction with standard library code and third-party code. Prusti can be given specifications to such code, even when the implementation itself is not available, to be used during verification. More recently, the specifications for important parts of the standard library have been contributed, as part of a MSc thesis project.
However, it might not be clear to a developer using Prusti which parts of the standard library are annotated with specifications (without browsing Prusti's source code), or, for the annotated methods, which properties were specified.
Goals
The primary goal of this project is to improve the workflow of a Prusti user working with standard library code and third-party code. The core milestones are:
- Create a tool to generate browsable HTML documentation from a set of crates containing Prusti specifications. The result should be familiar to Rust developers, i.e. by basing the tool on external page rustdoc.
- Extend the Prusti annotation language with informal descriptions of specifications. For a trivial example, the precondition "x ≥ 0" can be described informally as "input x must not be negative". Use these additional annotations in the generated documentation.
Prerequisites
Experience with Rust is required, especially since the second core milestone would involve small modifications to Prusti. Some experience with documentation systems, such as external page rustdoc, external page doxygen, or external page sphinx, as well as some knowledge of Viper or deductive verification in general is recommended.
Opportunities
The project offers the following opportunities:
- Make an important contribution to the Rust community.
- Gain experience with the Rust programming language.