Formal account of ghost snapshots in a verification tool for Rust

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

scope and result

This internship report studies the interaction between Creusot’s ghost snapshots and prophecy based encoding of mutable borrows. Its central result is a mechanised RustHornBelt model in Rocq that validates a restriction on that interaction. The report states: “We successfully proved that the restriction proposal is sound and expressive enough to prove each case that the initial model could solve.” (Your contribution, p. 1.) It also says that the implementation “does not constitute a formal proof and could lead to other unsoundness when dealing with deeper interactions (e.g. unsafe Rust code).” (General context, p. 1.) Thus the paper’s evidence is a foundational proof for the modified model and a case study, not a proof of all of Creusot or all Rust.

technique 1: prophetic encoding of mutable borrows

Use this when translating Rust with mutable references into first-order specifications without an explicit heap. RustHorn’s key construction represents a mutable reference by its current value and a prophecy for its final value. The report gives the complete procedure:

1. At &mut x, create a fresh prophecy α, replace the lender’s logical value with α, and represent the borrower as (x, α). The paper says: “This encoding is a tuple of the current value being modified throughout the execution, and the final value being the value when the borrow ends.” (Section 2.1, p. 6.)
2. For each write through the borrow, update only the current component. In the example, *bor_x = 1 changes bor_x ↦ (0, α) to bor_x ↦ (1, α).
3. Before the borrow lifetime ends, resolve the prophecy by equating current and final values, α = 1 in the example, then use the lender’s value in later assertions. Resolution is ghost code generated by the verification translation.
4. Compose each instruction’s postcondition backwards with a predicate transformer. The report’s bounded addition example has specification λ Φ '[a,b]. a+b ≤ M ∧ Φ[a+b]; applying this style to the borrow program reduces its precondition to ∀α. α = 1 → ⊤ → α = 1, equivalent to true (Section 3.2.2 and 3.2.4, pp. 10–12).

The model gives mutable references mathematical type ⌊T⌋ × ⌊T⌋, with current *x and final ^x values (Figure 5, p. 9). MutNew, MutWrite, MutEnd, and LftEnd are the corresponding typing rules. MutEnd may resolve before lifetime death; LftEnd later releases the frozen lender. The paper emphasizes that the lender need not remain in context during MutWrite or MutEnd, enabling local reasoning (Section 3.2.3, p. 11).

Inference: In Verus, the analogous proof shape is an executable Rust function with requires and ensures, ghost state in proof code, and lemmas establishing that a mutable reference’s post-state satisfies its contract. This is a suggested contract-level analogy; the report neither studies Verus nor specifies how its mutable-reference reasoning is implemented. A Verus proof cannot treat proof fn code as runtime code; proof-only facts are erased.

Evidence and limits: RustHornBelt’s type system is stated to be sound: “a closed and semantically well-typed Rust program, under the precondition ⊤, will never encounter undefined behaviour” (Section 3.2, p. 9). The claim is for the formalised λRust model and its adequacy proof. The report notes that λRust omits Rust places, and that the resolution point in realistic Rust MIR needs a separate analysis (Summary, p. 2; Related work, p. 18). The trusted base includes Rocq, Iris, the adequacy proof, and the translation assumptions.

technique 2: snapshots and the causality-loop counterexample

Use snapshots to retain a logical value while leaving executable ownership unchanged. A snapshot is a zero-sized Snapshot<T> value erased at compilation. The paper says: “Since Creusot allows developers to include snapshots’ results as part of the code, snapshots’ values are converted into unit values during compilation.” (Section 2.2, p. 6.) To apply it, take s = snapshot!(v), continue mutating v, and use proof_assert!(s[0] == 1) to read the old logical value while ordinary assert! checks runtime state. The example changes [1,2] to [3,2] while retaining [1,2] in s (Figure 3, p. 7).

The report’s unsoundness test combines snapshots with two mutable borrows:

1. Snapshot false, creating logical s ↦ ⊥.
2. Borrow s as bor_s1; its prophecy α is immediately resolved to ⊥.
3. Borrow s again as bor_s2, with prophecy β.
4. Snapshot the equality bor_s1 == bor_s2. Because a borrow is a pair (current, final), simplification makes this snapshot equal to ¬β.
5. Write that result into bor_s2; its current value becomes ¬β, while its final value remains β.
6. Resolve bor_s2, requiring β = ¬β, and prove false.

The paper explains the defect: “The key problem is a causality loop, whereby the final value of a prophecy depends on its own current value.” (Section 2.3, p. 7.) The naive snapshot rule duplicates any value, including one containing a resolved mutable borrow (Section 3.3, p. 12). Therefore the issue is semantic, not a runtime snapshot bug.

Inference: For Verus, a snapshot-like specification value should be a ghost/spec value captured before mutation, while executable code receives no snapshot object. A proof must ensure that a captured value cannot expose a mutable borrow’s hidden final state. This is a design constraint for any Verus library that models borrow histories; it is not a Verus result in the paper.

technique 3: non-extensional borrow identities

Use this repair when values of mutable borrows may be compared or copied in ghost code. Replace (current, final) with (current, identifier), where every borrow gets a unique identity. The report says: “The proposed representation, as briefly discussed in Section 2.3, is a triple of a current value, a final value, and a unique identifier for each new mutable borrow, making them non-extensionals.” (Section 4.1, p. 13.) Operationally, the model stores current value c and identifier i; a global invariant maps each identifier to one final value. Two distinct borrows therefore compare unequal even if their current and eventual values coincide, so the Figure 4 comparison is always false rather than ¬β.

The final value is obtained only through a prophecy assignment π. Define lookup π ↓ i as the final value associated with identifier i. Change MutEnd from f = c to π ↓ i = c; this prevents a snapshot, which has no π, from inspecting prophetic values. In the paper’s words: “Because the rule SnapshotTake has no access to the prophecy assignment 𝜋, as more detailed in Section 5.2, the rule is now sound.” (Section 4.1, p. 13.)

The transformation must be applied consistently:

• MutNew quantifies an identifier and passes (x,i) plus π ↓ i to the continuation
• MutWrite changes c but preserves i
• MutEnd checks π ↓ i = c
• MutTupleSplit creates child identifiers and asserts that the parent’s prophecy equals the tuple of child prophecies

The report states: “The changes performed are (1) the prophecy assignment π is now received and given back, (2) prophecy variables α are now identifiers i and (3) rules that require prophesied values use the prophecy lookup.” (Section 4.2, p. 14.)

Inference: In Verus, use a ghost identifier and an explicitly maintained map or relation in a proof-oriented abstraction. Keep the identifier invariant in invariant clauses or lemmas, and expose final values only through a specification function that receives the ghost map. Verus syntax and solver behavior differ from the paper’s predicate transformers, so this is a translation design, not a claim about existing Verus primitives.

technique 4: prophetic predicate transformers and Iris model

The identifier repair requires every predicate transformer to receive the prophecy assignment: its type changes to (ProphAsn → ⌊T'⌋ → Prop) → ProphAsn → ⌊T⌋ → Prop. The report’s modified rules thread π through MutNew, MutWrite, MutEnd, and subdivision (Section 4.2, pp. 13–14). This makes ordinary specifications prophetic while keeping snapshots non-prophetic.

The semantic proof uses Iris resources. Each type has size, owned predicate, and shared predicate. A mutable borrow owns a value observer VOξ and a prophecy controller PCξ; UniqResolve consumes the observer to emit the observation π ξ = v and returns the controller so the borrow invariant can be restored. The report describes observer/controller agreement as linked Iris ghost state that can only be updated jointly (§5.3, p.17). The paper states: “Once the value observer and the prophecy controller have agreed on the value v, the value observer is given to produce the observation that the prophecy assignment π on ξ is now the value v.” (Section 5.3, p. 17.) Prophecy tokens prevent duplicate resolution; lifetime tokens and dead-lifetime tokens control access to borrowed propositions.

The evidence is a Rocq mechanisation of the modified RustHornBelt model, plus the InvCell case study. In Creusot, InvCell supplies a trusted interface for std::cell::Cell<T> with a snapshot mapping and new, get, and set; cell_repeat is proved against it. The report says: “In the former case, we proved the interface and the example, whereas in the latter case, we axiomatised the interface thanks to the model, and successfully proved the same example using the axiomatisation” (contribution summary, p.2). Here the former is RustHornBelt and the latter is Creusot. The invariant says the cell contains a multiple of the input integer. The report describes “the verification in Creusot” as “significantly easier and proved within seconds” while RustHornBelt required manual translation and proofs (Section 4.3, p. 14). No runtime benchmark denominator is supplied, so that timing is qualitative.

Inference: A Verus product should treat such axiomatized unsafe interfaces as explicit trusted boundaries. Verus can prove clients against contracts, but the paper’s Rocq model is the evidence that the contract and borrow semantics are sound for its formal language. Inference: an unproved snapshot or interior-mutability abstraction could invalidate a client proof. This report establishes a specific counterexample and model repair, not a measured risk level or vulnerability in Verus.

what is proved, measured, and trusted

The report proves soundness and expressiveness of the modified RustHornBelt type system in Rocq and demonstrates InvCell. It does not prove complete Creusot soundness, arbitrary unsafe Rust, Rust’s full operational semantics, or the proposed type-invariant extension. Its future-work list explicitly includes type invariants, places/final-borrow analysis, and relaxed memory (Summary, p. 2). The only timing statement is “within seconds” for one example; no repeated-run count or timing distribution is provided. The report’s semantic explanation explicitly omits step-indexing details (§5, p.15); the adequacy proof is reported unchanged (validity summary, p.2).

Inference: VL should reuse the paper’s borrow-identity and restricted prophecy-access ideas rather than independently inventing snapshot semantics. If VL introduces a comparable prophecy-based abstraction, its soundness argument must explain how snapshot expressions are prevented from inspecting the relevant prophetic state. The paper does not show that existing Verus snapshots have this defect.

techniques for the catalog

• prophetic mutable-borrow encoding: represent a borrow by current and final values, update current values, and resolve by equality at borrow end
• erased logical snapshots: duplicate a value in specification state while compiling the runtime snapshot to a zero-sized value
• non-extensional borrow identities: add a fresh borrow identity and expose final values only through a prophecy assignment
• prophetic predicate transformers: thread the prophecy assignment through creation, writes, resolution, and borrow subdivision
• Iris observer/controller proof: link an interior value observer and exterior prophecy controller to prove unique resolution

Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “Thanks to the RustHorn’s representation, the lender x is not required to be present in the context of neither MutWrite nor MutEnd, allowing local reasoning as desired.”): read the entire supplied 19-page report text, including bibliography, and the entire study; compared quotations, representations, typing-rule changes, case-study scope, and page references; corrected page locations, removed an ellipsis from a quotation, distinguished proved and axiomatized interfaces, clarified observer consumption and the unchanged adequacy proof, corrected the tag, and qualified unsupported Verus-risk claims; did not run Rocq or Creusot, inspect mechanisation code, validate references, or visually inspect PDF figures.

Last edited: 2026-10-16