Rustproof

Rustproof is a compiler plugin for the Rust programming language. It generates verification conditions for functions with supplied preconditions(P) and postconditions(Q). That is, given a supplied postcondition on a function, rustproof uses predicate transformer semantics to generate a weakest precondition(WP(S, Q)) from the postcondition and a body of statements(S). The verification condition P->WP(S,Q) is then checked for validity by a SMT solver (z3). This process results in a proof of function correctness.

Dependencies

• rustc 1.12.0-nightly (2016-08-12).

• z3

Your installation of z3 needs to be in your PATH for rustproof to work.

Supported Rust Language Features

• Integer arithmetic
  • isize and usize are unsupported
• Boolean expressions, variables, and literals
• Assertions (integer/boolean)
  • assert_eq!() is unsupported
• If statements

Usage

Including Rustproof in Your Project

Add rustproof as a dependency in Cargo.toml

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git" }

Using Rustproof

#![plugin(rustproof)] is required in each file where rustproof is used. Typically this is placed at the beginning of a file.

Rustproof uses a custom attribute condition to allow declaring pre/postconditions on functions.

The attribute is supplied as: #[condition(pre=" ", post=" ")] and must be supplied before a function definition.

See USAGE for a detailed explanation of the attribute system.

See EXAMPLES for example functions with condition attributes.

Additionally, #![plugin(rustproof(debug))] prints out basic blocks of each function annotated with #[condition(..)], as well as a step-by-step view of generating the verification condition.

Contributors

Matthew Slocum
Sami Sahli
Vincent Schuster
Michael Salter
Bradley Rasmussen
Drew Gohman
Matthew O'Brien

Reporting Issues

Please report all issues on the github issue tracker.

License

Rustproof is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

See LICENSE-APACHE, LICENSE-MIT, and COPYRIGHT for details.