Thrust is a refinement type checking and inference tool for Rust.
- Make sure Z3 is installed.
- The main binary,
thrust-rustc, behaves likerustcbut includes Thrust's verification. - In the following instructions, we assume the Thrust source code is cloned locally and commands are executed within it.
Take the following Rust code (gcd.rs):
fn gcd(mut a: i32, mut b: i32) -> i32 {
while a != b {
let (l, r) = if a < b {
(&mut a, &b)
} else {
(&mut b, &a)
};
*l -= *r;
}
a
}
#[thrust::callable]
fn check_gcd(a: i32, b: i32) {
assert!(gcd(a, b) <= a);
}
fn main() {}Let Thrust verify that the program is correct. Here, we use cargo run in the Thrust source tree to build and run thrust-rustc. Note that you need to disable the debug overflow assertions in rustc, as they are currently not supported in Thrust.
$ cargo run -- -Adead_code -C debug-assertions=false gcd.rs && echo 'safe'
Compiling thrust v0.1.0 (/home/coord_e/rust-refinement/thrust)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.08s
Running `target/debug/thrust-rustc -Adead_code -C debug-assertions=false gcd.rs`
error: verification error: Unsat
error: aborting due to 1 previous errorThrust says the program is not safe (possible to panic). In fact, we have a bug in our gcd function:
fn gcd(mut a: i32, mut b: i32) -> i32 {
while a != b {
- let (l, r) = if a < b {
+ let (l, r) = if a > b {
(&mut a, &b)
} else {
(&mut b, &a)Now Thrust verifies the program is actually safe.
$ cargo run -- -Adead_code -C debug-assertions=false gcd_fixed.rs && echo 'safe'
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.08s
Running `target/debug/thrust-rustc -Adead_code -C debug-assertions=false gcd.rs`
safeIntegration test examples are located under tests/ui/ and can be executed using cargo test. You can review these examples to understand what the current Thrust implementation can handle.
Thrust can verify a wide range of programs without explicit annotations, but you can use #[thrust::requires(expr)] and #[thrust::ensures(expr)] to annotate the precondition and postcondition of a function, aiding in verification or specifying the specification. Here, expr is a logical expression that supports basic integer, boolean, and reference operations.
#[thrust::requires(n >= 0)]
#[thrust::ensures((result * 2) == n * (n + 1))]
fn sum(n: i32) -> i32 {
if n == 0 {
0
} else {
n + sum(n - 1)
}
}You can use the ^ unary operator to denote the value of a mutable reference after the function is called. Note that in the current implementation, you need to specify both requires and ensures when using either one.
#[thrust::requires(true)]
#[thrust::ensures(^ma == *ma + a)]
fn add(ma: &mut i32, a: i32) {
*ma += a;
}The conditions on thrust::requires and thrust::ensures are internally encoded as refinement types for the parameter and return types. You can also specify these refinement types directly using #[thrust::param(param: type)] and #[thrust::ret(type)].
#[thrust::param(n: { x: int | x >= 0 })]
#[thrust::ret({ x: int | (x * 2) == n * (n + 1) })]
fn sum(n: i32) -> i32 {
if n == 0 {
0
} else {
n + sum(n - 1)
}
}The bodies of functions marked with #[thrust::trusted] are not analyzed by Thrust. Additionally, #[thrust::callable] is an alias for #[thrust::requires(true)] and #[thrust::ensures(true)].
#[thrust::trusted]
#[thrust::callable]
fn rand() -> i32 { unimplemented!() }Several environment variables are used by Thrust to configure its behavior:
THRUST_SOLVER: A CHC solver command used to solve CHC constraints generated by Thrust. Default:z3THRUST_SOLVER_ARGS: Whitespace-separated command-line flags passed to the solver. The default isfp.spacer.global=true fp.validate=truewhen the solver isz3.THRUST_SOLVER_TIMEOUT_SECS: Timeout for waiting on results from the solver. Default:30THRUST_OUTPUT_DIR: When configured, Thrust outputs intermediate smtlib2 files into this directory.THRUST_ENUM_EXPANSION_DEPTH_LIMIT: When Thrust works with enums, it "expands" the structure of the enum value onto its environment. This configuration value sets the limit on the depth of recursion during this expansion to handle enums that are defined recursively. It is our future work to discover a sensible value for this automatically. Default:2
The implementation of the Thrust is largely divided into the following modules.
analyze: MIR analysis. Further divided into the modules corresponding to the program units:analyze::crate_,analyze::local_def, andanalyze::basic_block.refine: Typing environment and related implementations.rty: Refinement type primitives.chc: CHC and logic primitives, and it also implements an invocation of the underlying CHC solver.annot: Refinement type annotation parser.
The implementation generates subtyping constraints in the form of CHCs (chc::System). The entry point is analyze::crate_::Analyzer::run, followed by analyze::local_def::Analyzer::run and analyze::basic_block::Analyzer::run, while accumulating the necessary information in analyze::Analyzer. Once chc::System is collected for the entire input, it invokes an external CHC solver via the chc::solver module and subsequently reports the result.
Hiromi Ogawa, Taro Sekiyama, and Hiroshi Unno. Thrust: A Prophecy-based Refinement Type System for Rust. PLDI 2025.
Licensed under either of
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.