Thrust: A Prophecy-Based Refinement Type System for Rust

(authored by agents unless marked 🧑) Tag: ogawa2025thrust, paper

what Thrust contributes

Thrust is an automated Rust verifier that combines dependent refinement types, prophecy variables for mutable borrows, and constrained Horn clause (CHC) solving. The abstract states that it supports “synthesis of inductive invariants for loops and recursive functions” and “precise verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification” (abstract, p. 230:1). It targets safe Rust and delegates “aliasing XOR mutability” and well-borrowedness (in the stacked borrows sense) to Rust’s type system. The authors prove soundness of the type system for a core calculus λCOR under that assumption, implement Thrust as a Rust compiler plugin, and evaluate it against RustHorn, Flux, and Prusti.

technique 1: infer refinement types with CHCs

What it is. A refinement type is a base type constrained by a logical predicate. The paper’s incr example has the type (x : i32) → {ν : i32 | ν = x + 1} and annotations #[thrust::requires(true)] and #[thrust::ensures(result == x + 1)] (Fig. 1, p. 230:6). Thrust infers missing predicates by generating CHCs and solving them with Spacer, a solver based on property directed reachability (PDR). The implementation “prepares refinement type templates, generates type derivations based on them, and collects subtyping constraints to form a system of CHC constraints” (Section 5, p. 230:17).

When to use it. Inference: use inference for arithmetic postconditions, loop invariants, recursive summaries, and functional correctness where a solver can synthesize predicates; use annotations when synthesis fails. The paper says annotations serve “as hints to its backend CHC solver” (Section 1.1, p. 230:3).

How to apply it. Inference: the paper gives no step list; these steps are reconstructed from Sections 1.1 and 5. (1) Write Rust and optional requires/ensures refinement annotations. (2) Compile to the optimized MIR the Rust compiler provides “after desugaring, type checking, borrow checking, and certain optimizations” (Section 5, p. 230:17). (3) Prepare refinement type templates. (4) Generate type derivations and collect subtyping constraints as CHCs. (5) Solve them with Spacer. (6) If solving fails, add function-signature or subexpression annotations and rerun. The experiments use a 180-second time limit (Section 5.1, p. 230:17).

Verus form (Inference: Thrust does not use Verus). Translate a refinement to requires and ensures on an executable fn; express loop facts with invariant declarations and arithmetic lemmas in proof fns. A Verus spec fn can define a pure predicate, but the executable function carries the contract. CHC inference is not a Verus construct; the analogous workflow is solver-assisted invariant discovery followed by explicit Verus proof. Keep the contract on the executable function, and use proof functions only in verification code.

Evidence and limits. Table 2 (p. 230:18) has 32 rows: 4 categories (prec, ho-funs, adt, mod) × 4 programs × a safe and an unsafe variant. Thrust returns the expected result on all 32 rows (16 safe, 16 unsafe), while RustHorn, Flux, and Prusti each return unknown, abort, or timeout on some rows. This is a small benchmark set, not a claim about all Rust. The unsafe results carry a dagger: “We manually confirmed that the program is indeed unsafe when Thrust concludes that the program is unsafe, since we have not formally proved the completeness of Thrust” (Table 2 footnote, p. 230:18). Inference: completeness is conjectured, not proved, so an “unsafe” answer from Thrust is not a proved counterexample.

technique 2: strong updates from Rust’s aliasing XOR mutability

What it is. Rust guarantees that a memory location has either multiple immutable references or a single mutable reference, not both (Section 1, p. 230:2). Thrust uses this to update a pointed-to value precisely (a strong update). In incr_max, the type system guarantees the two &mut i32 arguments p and q do not alias; the function increments only the referent of the larger one. The return type records both cases: ∗p ≥ ∗q ∧ ◦p = ∗p + 1 ∧ ◦q = ∗q, or ∗p < ∗q ∧ ◦p = ∗p ∧ ◦q = ∗q + 1, where ∗ is the value at call time and ◦ the value at return (Fig. 2, pp. 230:6–7). The paper says Thrust can also synthesize this predicate automatically by type inference (Section 2, pp. 230:6–7) and achieves precision “without sacrificing full automation” (Section 1.1, p. 230:3).

How to apply it. Inference: steps reconstructed from Section 2. (1) Keep mutable references as ordinary &mut. (2) Rely on the borrow checker for non-aliasing. (3) At a write through a mutable reference, update the current value in that reference’s logical representation. (4) Infer or annotate the function’s dependent return type. Dynamic selection of a mutable reference is the stress case: Flux “cannot assign precise types to programs that dynamically select the target for writing through mutable references based on runtime values” (Section 2, p. 230:7), because its strong references “are tracked as singleton types” (Section 5.2, p. 230:19).

Verus form (Inference). Use &mut T in executable signatures and maintain a ghost snapshot of each referent. State branch-specific postconditions with ensures implications or a disjunction. A proof of non-aliasing must come from Verus’s accepted mutable-reference rules; do not invent a modifies clause. Update ghost values in proof code and prove the executable assignment preserves them. If references are stored in an enum or collection, the representation and aliasing facts need explicit invariants.

Evidence and limits. In Table 2 (p. 230:18), prec-1-inc-max-plain-safe is verified safe by Thrust (0 annotation lines, 0.05 s), RustHorn (0.04 s), and Prusti (0 annotation lines, 3.77 s); Flux reports unknown (0.07 s). In the prec category the Flux and Prusti inputs were inlined “in order to avoid the need for annotations” (Section 5.2, p. 230:18). This single row shows the targeted precision, not general superiority. The design covers safe Rust only; the conclusion calls precise, automated verification of interior mutability and unsafe code “an important challenge” (Section 7, p. 230:22).

technique 3: prophecy variables for borrow release

What it is. A mutable borrow is represented by its current value and a prophecy for its value when the borrow is released. The paper explains: “From the time the borrow is created until it is released, the prophecy refers to the ‘future value’ of the mutable borrow” (Section 1.2, p. 230:5). In Fig. 3’s main, x starts as ⟨2⟩; creating m = &mut *x gives m the representation ⟨2, l⟩ with a fresh prophecy l and changes x to ⟨l⟩. Inside decr, the argument starts as ⟨x0, ℓ⟩ and becomes ⟨x0 − 1, ℓ⟩ after the decrement; at the end of its lifetime ℓ is fixed to x0 − 1, so the return type gives ◦x = ∗x − 1. At the call site this yields l = 2 − 1, which proves assert!(*x == 1) (Fig. 3 and Section 2, pp. 230:6–7).

How to apply it. Steps follow rules T_MutBorrow, T_Assign, and T_DropMut (Section 4.2, pp. 230:12–14). (1) At a mutable borrow, create a fresh prophecy variable y. (2) Give the new reference the representation ⟨current, y⟩ and replace the borrowed part of the owner by y. (3) When the reference is released by drop, fix its future value to its current value; λCOR releases a pointer after assignment, so an assignment fixes the future value to the assigned value. (4) Continue checking with the owner’s value equal to the prophecy. For a reborrow n = &mut *m (Fig. 4, p. 230:8), create l2, change m from ⟨2, l1⟩ to ⟨l2, l1⟩, give n ⟨2, l2⟩; *n -= 1 fixes l2 = 2 − 1, then *m -= 1 fixes l1 = l2 − 1.

Verus form (Inference). Model the future value with a ghost variable or a ghost cell associated with the borrow lifetime. Use old(x) in contracts for the entry value and an explicit ghost result for the value transferred back at release. A proof function can establish the relation between the current value and the prophecy; executable code must not call it. The precise encoding depends on Verus’s borrow support, so this is a conceptual translation, not a claim that Verus exposes Thrust’s prophecy primitive.

Evidence and limits. The paper says “Thrust propagates update information to the original owner upon mutable borrow release” (Section 1.1, p. 230:3). Theorem 4.1 (Section 4.3, p. 230:16) shows a well-typed program either finishes, steps, or hits BorrowError (a stacked-borrows violation); the paper then relies on the fact that “Rust’s borrow checker guarantees that BorrowError never happens”. Inference: prophecy reasoning itself does not establish well-borrowedness; it trusts the borrow checker. The system also separates program variables from logical variables because changing a variable referenced by a refinement could otherwise make the refinement invalid (Section 2, p. 230:8).

technique 4: immutable logical snapshots and modular verification

What it is. Refinements depend only on implicit logical variables, not mutable program variables. The paper says, “Logical variables represent static values, that is, their meaning does not change even as the program evaluation proceeds” (Section 2, p. 230:8). Without this, a refinement {y : i32 | y = ∗x} would become invalid after decr changes the referent of x, even though y is not modified (Section 2, p. 230:8). Formally, typing contexts Γ hold implicit variables and place contexts Δ map program variables to logical forms (Section 4.1, p. 230:10). Thrust also supports “function- and subexpression-level modular verification” with user annotations as solver hints (Section 1.1, p. 230:3).

How to apply it. Inference: steps reconstructed from Sections 2 and 4. (1) At each binding (rule T_Let), introduce implicit variables for the bound value. (2) Write refinements only over implicit and prophecy variables. (3) On mutation, change the logical form assigned to the program variable, not old implicit variables. (4) At a function call, use the callee’s inferred or annotated type as its summary. (5) For nonlinear arithmetic or hard recursive invariants, add annotations rather than rely on inference.

Verus form (Inference). Use old(...) and ghost snapshots in requires/ensures; use loop invariant clauses to carry stable facts. Define pure relations in spec fns and prove them in proof fns. The key change is that Verus requires explicit ghost state and lemmas where Thrust inserts implicit variables. This technique is directly applicable to avoiding accidental dependence on mutable state.

Evidence and limits. In Table 2 (p. 230:18), Thrust verifies all four mod safe programs in 0.05–0.08 s; the two nonlinear-arithmetic programs (mod-3-nonlin-sum, mod-4-nonlin-mult-mut) use 2 annotation lines each, and RustHorn times out on both safe variants. The “Annot.” column counts “the number of lines used for user-specified invariants in function signatures” (Section 5.2, p. 230:18). Section 5.3 (p. 230:20) reports a cost: introducing implicit variables at each binding over MIR’s simple operands creates many implicit variables, which increases the load on the CHC solver.

technique 5: refine higher-order functions and algebraic data

Thrust’s type-based approach assigns refinement types to higher-order functions and to elements of algebraic data types. The paper says this “allows compositional verification by inferring refinement types for higher-order functions and data elements within algebraic data types” (Section 1.1, p. 230:4). For polymorphic collections such as lists, Thrust introduces “a predicate variable that enables per-element refinement for the type parameter” (Section 5.2, p. 230:19), so the CHC solver need not synthesize recursive functions over the data type.

How to apply it. Inference: steps reconstructed from Sections 1.1 and 5.2. (1) Give a function parameter a refinement type describing its input/output relation. (2) Check each actual function against it by subtyping (rule S_Fun, Fig. 9, p. 230:15). (3) For a list or tree, attach a predicate variable to the element type. (4) Let CHC solving find the predicates.

Verus form (Inference). Encode higher-order contracts as spec fn relations passed as ghost arguments, or prove each closure’s contract separately. For recursive datatypes, define a recursive spec fn predicate and prove list/tree lemmas by induction. Verus does not infer Thrust’s refinement types automatically, so the user supplies the predicate and lemmas.

Evidence and limits. In Table 2 (p. 230:18), Thrust verifies all eight ho-funs rows (four safe, four unsafe) in 0.04–0.12 s with 0 annotation lines; RustHorn aborts on all eight. On the four adt safe programs Thrust takes 0.09–4.09 s; adt-2-dict-pos needs 2 annotation lines. The formal calculus λCOR does not support general recursive ADTs, and its functions “must not contain free variables”; introducing existential types for boxed closures “is left for future work” (Section 4.4, pp. 230:16–17).

implementation, trust, and product implications

The implementation is a Rust compiler plugin over optimized MIR with the CHC solver Spacer. Experiments ran on Ubuntu 24.04 with 32 GB RAM and 16 logical CPU cores on an AMD EPYC 7R13, using Spacer bundled with Z3 4.13.0 and a 180-second time limit (Section 5.1, p. 230:17). The paper says MIR gives “stability against changes in the source code” (Section 5, p. 230:17), but Thrust “interprets MIR more rigorously compared to RustHorn, resulting in more complex constraints being generated” (Section 5.3, p. 230:20), and is “sometimes slower” than RustHorn on the RustHorn benchmark set. The RustHorn-benchmark results appear only as a scatter plot (Fig. 10, p. 230:20); the paper defers the full results to the supplementary material, which this study does not check.

The proved result is soundness of the type system for λCOR assuming well-borrowed executions (Theorem 4.1, Section 4.3, p. 230:16). Inference: the trusted base includes Rust’s borrow checker, the correspondence between λCOR and MIR (discussed only in the supplementary material, Section 5, p. 230:17), the CHC solver, and the implementation. Inference: the threat to VL is moderate and direct. Prophecy and immutable snapshots address the hardest mutation/borrow precision problems, while CHC inference could reduce annotation burden. VL should reuse the explicit soundness boundary and avoid claiming that solver success proves completeness. Existing Verus support for mutable references, old, invariant, requires, ensures, and proof functions should be checked before importing any Thrust notation.

techniques for the catalog

• CHC refinement inference: generate Horn constraints from refinement templates and solve them to infer loop, recursion, and function predicates
• aliasing-aware strong updates: use Rust’s exclusive mutable-reference guarantee to update the selected referent precisely
• prophecy borrow summaries: track a borrow’s future release value and propagate it back to the owner
• immutable logical snapshots: keep refinements over stable implicit variables while program values mutate
• modular higher-order and ADT refinement: attach predicates to function types and data elements for compositional proofs Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Because Rust’s borrow checker guarantees that BorrowError never happens, we can ensure that (safe) Rust programs well-typed in our refinement type system never get stuck.”): checked every quotation, number, section and page reference, and technique step against the paper text, including every Table 2 row cited; changed the Table 2 counts (4 safe programs per category, not 8; 32 rows are 16 safe/unsafe pairs), the prec-1 times (RustHorn 0.04 s, Prusti 3.77 s, RustHorn has no annotation column), the mod safe time range (0.05–0.08 s), the ho-funs row count, the Table 2 page (p. 230:18 only), several section/page references (Flux singleton types in Section 5.2; propagation quote from Section 1.1), the Fig. 3 and Fig. 4 walk-throughs, the Section 4.4 limits (they apply to λCOR), marked reconstructed steps and the trusted-base list “Inference:”, and deleted unsupported claims (a branch-join disjunction step, a claim that modular summaries may hide incorrect contracts, a claim about the memory logic unsafe code needs); did not check the supplementary material, the Fig. 10 scatter-plot values, or any Verus statement.

Last edited: 2026-10-17