Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Using a Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool

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

problem and result

The paper takes the prophecy-based encoding of mutable borrows, so far described only for a core calculus, and scales it to the Creusot verifier for Rust. It identifies four open problems (Section 1, §1.2 to §1.5): where to place resolution, sound modular resolution for containers, sound ghost code, and type invariants. Its solutions are implemented in Creusot and evaluated on case studies (the Abstract gives “4k LOC”). The abstract states, “All of our work has been implemented as an extension of Creusot, and was evaluated on several case studies (4k LOC).” The paper also says, “Mutable borrows are challenging because mutating a borrow modifies a value held in a different location, in a way that becomes observable as soon as the borrow ends.” Inference: the work is especially relevant when a verifier must handle mutable references that are returned, nested, or stored in data structures.

technique 1: separate prophetic logic from ghost logic

why. Unrestricted ghost expressions can inspect a prophecy and write a value that depends on that same prophecy, creating a causality loop. The paper summarizes the fix as follows: “To prevent these issues, we introduce two mechanisms: first, in §2.1, we introduce a separation between ghost code and specifications, by layering the specification language.” The paper’s counterexample stores a snapshot boolean, borrows it, writes snapshot!(!^bor) through the borrow, resolves the borrow, and proves false (Section 1.4, p. 5). Equality of mutable borrows can leak the prophecy indirectly, so forbidding only the final operator (^) in ghost code is insufficient (Section 2, Fig. 3, p. 7).

how. Stratify the specification language. Put formulas that may mention final values in #[logic(prophetic)]; put ghost computations and snapshots in ordinary #[logic]. Allow prophetic logic to call ordinary logic, but forbid ordinary logic from calling prophetic logic (Section 2.1, p. 7). Also, if a trait method is declared #[logic], forbid its implementations from being annotated #[logic(prophetic)] (Section 2.1, p. 8). Change each borrow model from (current, final) to (current, final, identity). Allocate a fresh identity on borrow creation; two borrows with the same identity must have the same prophecy, so equality on distinct borrows cannot reveal a final value (Section 2.2, pp. 8–9).

A fresh identity would make harmless compiler reborrows hard to specify. Permit identity sharing for a final reborrow only when static analysis proves that the parent is not modified and therefore the parent and child prophecies coincide. For field projections, use an opaque deterministic function such as field0(parent.id) to distinguish fields while preserving the parent’s prophecy relation (Section 2.3, p. 9). The paper’s analysis is a backward greatest-fixed-point dataflow analysis over MIR. For each program location λ, compute a set Ίλ of places whose immediate reborrow is final; on an assignment, remove the places that conflict with either side and add the places one dereference deeper than the written place (Section 2.4.2, pp. 10–12).

evidence and limitations. The paper says, “Since the analysis only considers syntactic and typing information, the computed sets are under-approximations, but we believe that this is enough to prove most programs in practice.” (Section 2.4.2, p. 10). The identity field restores soundness for the presented ghost paradox, while final-reborrow sharing restores specifications such as identity functions and field projections (Sections 2.2–2.4, pp. 8–12). Inference: this mechanism does not prove all borrow analyses correct; the paper explicitly leaves a full foundational proof of the extensions for future work (Section 7, p. 21).

Verus form. Inference: represent non-prophetic ghost state with Verus ghost values and proof functions, and keep any final-value relation in explicit contracts or lemmas. Verus does not use the paper’s #[logic(prophetic)] annotations; do not invent those constructs. Inference: if VL needs a borrow identity model, encode it as a ghost field and prove equality/alias lemmas, while executable Rust retains ordinary references.

technique 2: prophetic type invariants

why. A type invariant must hold at public function boundaries, but a mutable borrow’s final value is chosen by later caller writes. The implementation rule is explicit: “The implementation of type invariants that we choose is to implicitly add pre- and postconditions to all functions that manipulate values of a type with an invariant.” Adding inv(^borrow) directly to a callee postcondition is too early: for a function returning one of two borrows, the caller controls which prophecy becomes final (Section 1.5, pp. 6–7).

how. Attach an Invariant trait with a logical invariant predicate to each type. The invariant of a type is the conjunction of the user-defined part and a structural part derived automatically from the type definition: Option<Even> requires the invariant of the payload for Some, a pair requires both fields, and Box<Even> requires the pointed value’s invariant (Section 3.1, p. 12). Enforce invariants as implicit preconditions and postconditions at function boundaries, while allowing temporary violation inside a function for non-atomic updates (Section 3.1, p. 12). When creating a mutable borrow, assume that its prophecy satisfies the type invariant. Immediately before resolving that borrow, generate a verification condition proving that the current value satisfies the invariant; this is when the prophecy’s final value becomes known (Section 3.3, pp. 13–14). Before borrowing, reestablish the invariant of the place so that the assumed invariant is inhabited; otherwise an uninhabited predicate could yield false (Section 3.3, p. 14).

The paper’s call_pair_bor_mut example borrows two Even values, passes both borrows through pair_bor_mut, adds 2 to the returned borrow, and checks the invariant when that borrow is resolved (Section 3.4, p. 14). The caller can rely on the invariant without knowing the callee’s complete borrow choice, because the resolution check is generated at the point where the final value is available.

evidence and limits. This solves the modularity problem for arbitrary borrow-returning functions, but it adds proof obligations at every resolution. Inference: it does not make an incorrect invariant meaningful; the invariant predicate remains part of the trusted specification. Its approach deliberately allows invariants to be temporarily broken (Section 3.1, p. 12). Footnote 3 (p. 6) says that implementing invariants as subset types, as in Why3, “would lead to similar problems”; Section 8 (p. 24) adds that subset types would be hard to add to Creusot because its SMT solvers assume all types are inhabited.

Verus form. Inference: use a Verus spec fn for the invariant, require it at API entry, ensure it for returned values, and add a proof obligation before a mutable borrow’s final state is used. Use requires, ensures, and invariant clauses only in their Verus roles; the paper’s implicit invariant insertion is an implementation technique for a verifier, not a Verus keyword.

technique 3: sound modular resolution for containers

why. A vector or user-defined structure can contain mutable borrows. Resolving the outer value must recover final-value equalities for every nested borrow. Earlier Creusot let library authors provide a trusted Resolve trait implementation, so an implementation such as false could silently enlarge the trusted computing base (Section 4, p. 15).

how. For a vector, the paper’s example resolution clause is forall<i : Int> 0 <= i && i < v.len() ==> v[i].resolve() (Section 4, p. 14). A built-in structural_resolve predicate is defined automatically and is shallow: it uses the resolution predicates of a type’s components (pair: both fields resolve; &mut T: ^x == *x; Box<T>: (*x).resolve()). A user-defined resolve is allowed, but the implementor must prove the lemma resolve_coherence, which requires inv(self) and structural_resolve(self) and ensures (*self).resolve() (Section 4, pp. 15–16). The paper concludes that custom definitions “can thus only be used for information hiding” and that a definition of false would be rejected. For the 19 Resolve instances in the case studies, the paper says the verification conditions “were automatically discharged by SMT solvers” (Section 6, p. 21).

Verus form. Inference: express a container’s relation with a spec fn over its sequence/map model and prove a lemma that each element’s final-state relation follows from the structural invariant. Keep any external-body library model explicitly trusted; do not make a proof function executable.

technique 4: choose resolution points with backward MIR analysis

why. Resolution must happen after the last mutation through a borrow. Resolving too late can reject correct programs (the Fig. 1 assertion cannot be proved if y is resolved after line 8), and because type invariants are checked at resolution, footnote 1 (p. 4) says it may also be unsound. The paper rejects both resolving at drop and resolving at the end of the lifetime as the general rule (Section 1.2, p. 4). Section 5.1 (pp. 16–18) lists four constraints: resolve a variable only when its value will no longer be used (5.1.1); resolve a borrow before its lifetime ends (5.1.2); do not resolve uninitialized places, which are tracked per place, not per variable (5.1.3); avoid resolving frozen borrows, since their value is not yet known (5.1.4). Resolving early weakens the context in which the invariant is proved (Section 5, p. 16).

how. The algorithm works on MIR and combines three data-flow analyses: per-place initializedness I(λ) (reused from the Rust compiler), per-place liveness Λ(λ), and per-place frozenness F(λ) (reused from the borrow checker). Places that contain a dereference of a mutable borrow are not considered; the lender resolves that memory, and such a place is resolved only right before it is overwritten. For each location it computes N(λ) = I(λ) ∩ (Λ(λ) âˆȘ F(λ)) and R(λ) = I(λ) \ N(λ) (Section 5.2, pp. 18–19). Resolution is inserted (Section 5.2, p. 19, continuing on p. 20):

  • at function entry, for places in R(λ);
  • when a local variable leaves its scope, for its subplaces in N(λ);
  • around each statement, split into a pure step and a side-effect step with points λ1, λ2, λ3: before the statement for places in N(λ1) ∩ R(λ2), and for a written place before the statement if it is in N(λ2) or after it if it is in R(λ3);
  • along a control-flow edge from λ to λ’, for places in N(λ) \ N(λ’). The paper says it “can easily prove that constraints 5.1.1, 5.1.2 and 5.1.3 are satisfied by this algorithm” (p. 20). Constraint 5.1.4 cannot always be met: for fn g(e: &mut Even) -> &mut i32 { &mut e.x } the parameter is resolved when it leaves scope, which gives an unsolvable goal, as expected (Section 5.1.4, p. 18). Memory leaks can cost precision but not soundness (footnote 7, p. 17).

Inference: the backward greatest-fixed-point analysis of technique 1 (Ίλ, Section 2.4.2) and this resolution-placement algorithm (Section 5.2) are separate analyses. The paper does not give a proof of the placement algorithm for constraint 5.1.4, and Section 7 says soundness of the constraints is not yet formalized.

evaluation, trust, and product implications

The authors run the extensions on Creusot’s “test suite”, “a comprehensive repository (10k LOC)” that includes the case studies from earlier Creusot publications (Section 6, p. 20). They report that they “were able to update all the case studies to use our extensions”; Table 1 (p. 20) lists seven case studies (red-black trees, hashmap, binary decision diagrams, sparse arrays, Knuth shuffle, iterators, sorting algorithms) and the features each uses. They remove “about 80 lines of specification” of repetitive type-invariant conditions, verify 19 Resolve instances automatically, and report that the only remaining trusted instances are in Creusot’s standard library and correspond to abstract types (Section 6, p. 21). For final borrows, “one line of specification in Creusot’s standard library had to be changed, and one line of specification in the IterMut iterator test needed to be reformulated and was replaced by 4 lines” (Section 6, p. 21). The paper does not say how the 4k LOC of the Abstract relates to the 10k LOC test suite, so the two numbers should not be combined as one benchmark. The evaluation reports no verification times or other performance numbers.

The authors have not yet formally established soundness of all extensions in RustHornBelt; they propose adding borrow identities, prophetic/non-prophetic assertion classes, and a resolution type class (Section 7, pp. 21–22). Ghost snapshots are non-linear and duplicable; the paper identifies linear ghost values, pledge-like point assertions, and richer foundational proofs as future work (Section 7, p. 22). Inference: for VeruLaw, the main threat is unsound generated borrow/specification glue, especially at container resolution and type-invariant boundaries. Inference: VL could reuse these ideas and focus new experiments on generated contracts, dependency changes, and the remaining trusted boundaries; the paper itself does not address VL.

techniques for the catalog

  • stratified prophetic and ghost logic: prevent ghost code from observing or self-dependently resolving mutable-borrow prophecies
  • identity-bearing borrows and final reborrows: add borrow identities and share them only when backward MIR analysis proves prophecy equality
  • prophetic type invariants: assume a final-value invariant at borrow creation and prove the current value satisfies it immediately before resolution
  • modular structural resolution: require a coherence lemma showing each custom resolution predicate follows from a shallow, automatically defined structural predicate, instead of trusting it
  • resolution-point placement: combine per-place initializedness, liveness and frozenness analyses over MIR to insert resolution at function entry, scope exit, statements and control-flow edges
  • final-borrow analysis: compute final-reborrow places by a backward greatest-fixed-point dataflow over MIR Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Implementations of Resolve are required to demonstrate that this lemma holds, ensuring that no unsound definition can be admitted.”): I read the whole paper text and the whole study and checked every quotation, number, section and page reference and technique step. Changed: rewrote technique 4, which had wrongly merged the final-borrows analysis (Section 2.4.2) with the resolution-placement algorithm (Section 5.2, initializedness, liveness and frozenness analyses); fixed structural resolution (shallow, with a resolve_coherence lemma, not recursive); fixed the footnote 3 claim (the paper says “similar problems”); fixed the Section 3.4 example, several page and section pointers, and the evaluation description (10k LOC suite includes earlier case studies; 4k vs 10k not explained by the paper); marked unsupported conclusions as Inference. Tag kept; link from the fetch record (the paper text has only a placeholder DOI). Not checked: the PDF figures beyond the extracted text, the cited prior work, and the Verus-form suggestions (the study’s own inferences).

Last edited: