Introduce ghost variables

[coord-e]

A ghost variable is proof-only data: it has no runtime representation, and program code cannot observe its content, but a specification refers to it as if it were the value it stands for.

thrust_macros::ghost! introduces one from a logical term over the live variables the term names:

let s = thrust_macros::ghost!(|x: i64| -> Seq<Int> { Seq::singleton(x) });

How it works

The term expands into a #[thrust::formula_fn] laid out like an ensures one — parameter 0 is the introduced value, the rest are the named variables — so it reads as the return refinement of a function over those variables, and the introduction as a call to that function. The analyzer intercepts the marker call and feeds that function type to the existing relate_fn_sub_type.

Ghost<T> has T's model, so ghost values flow through struct fields and function boundaries on the machinery that already exists for any other value; nothing along those paths needed changing.

The parameters name live variables with their types, the same convention invariant! uses. The return type names the logical type of the introduced value.

Disabling RemoveZsts

This MIR pass rewrites reads of zero-sized locals into constants, which drops the refinement of every value whose type carries no runtime data. Without disabling it, passing a ghost value to a function arrives as const Ghost(PhantomData) and the binding is lost:

inconsistent types: got=(), expected=(own Array<int, int>, own int)

This is not specific to ghost: it covers the model types (Seq, Int, …) equally. Until now nothing constructed a model-typed value in program code — they only ever appeared as parameters — so the limitation had no way to show up.

Tests

ghost_local	introduce a ghost value, cross a function boundary, check it in a specification
ghost_field	ghost field of a struct, updated through &mut, tied to a real field by pre/postconditions

Each as a pass/fail pair.

Known gaps

• A variable referred to only by a ghost term looks unused to rustc, so the tests pass -A unused-variables.
• A struct holding a ghost field must spell its model out as a tuple, losing named-field access in specifications. This is the existing convention for any struct whose field models differ from their types (see annot_struct_impl.rs), not something ghost introduces. Giving Ghost<T> a Deref impl plus an identity case in annot_fn would let type Ty = Self keep named fields.
• ghost! inside a generic impl needs the context threading invariant_context does for invariants. Not implemented here.

🤖 Generated with Claude Code

https://claude.ai/code/session_014jTCnjoii4e5r4VLEU733b

---

Generated by Claude Code