Introduce ghost variables by coord-e · Pull Request #220 · coord-e/thrust

coord-e · 2026-08-14T14:49:35Z

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) });

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

How it works

A ghost 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:

thrust_macros::ghost!(|s: Ghost<Seq<Int>>, x: i64| -> Seq<Int> { s.push(x) })

{
    #[thrust::formula_fn]
    fn _thrust_ghost_0(result: <Seq<Int> as thrust_models::Model>::Ty,
        s: <Ghost<Seq<Int>> as thrust_models::Model>::Ty,
        x: <i64 as thrust_models::Model>::Ty) -> bool {
        result == ({ s.push(x) })
    }
    thrust_models::__ghost_marker::<_, Seq<Int>>(_thrust_ghost_0)
}

That layout is the one to_refinement already reads, so the analyzer takes the formula function for

fn(s: Seq<Int>, x: Int) -> { v | v == s.push(x) }

resolves s and x to the live values of those names at the marker call, and hands the whole thing to the existing relate_fn_sub_type. The introduction of a ghost value is then typed as a call to that function, and nothing else in the analyzer has to know about ghost.

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.

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

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 735a0c69c4

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-08-16T08:35:23Z

+                    if place.projection.is_empty() && self.is_defined(place.local) {
+                        return Some(Operand::Copy(*place));


Reject ambiguous shadowed ghost operands

When a ghost term names a shadowed variable, var_debug_info can contain multiple entries with the same symbol, including stale Const entries or multiple locals that remain live because an outer value is borrowed. Returning the first match does not respect lexical scope, so the ghost may be refined with the outer value rather than the variable visible at the macro call, potentially validating a false assertion. Detect ambiguity or carry a source-level identity instead of selecting the first name match.

Useful? React with 👍 / 👎.

Fixed in 34b6376. operand_of_name no longer returns the first match: it scans every entry with the name and reports them as ambiguous, the way local_of_name_in_bb already does for invariants, rather than picking one.

Resolving by lexical scope is the better answer and remains open; refusing to guess at least turns a wrong proof into a diagnostic.

Generated by Claude Code

chatgpt-codex-connector · 2026-08-16T08:35:23Z

+        let func_ty = rty::FunctionType::new(
+            params,
+            rty::RefinedType::new(value_ty.vacuous(), formula_fn.to_refinement()),
+        );


Handle ghost terms without captured variables

A valid constant ghost such as ghost!(|| -> Int { 0 }) leaves params empty here. relate_fn_param_sub_types_with_builder then adds its synthetic unit parameter only to the expected argument list and asserts that its length equals this empty function parameter list, causing the verifier to panic. Construct the same unit parameter representation used for ordinary zero-argument Rust functions, or bypass that normalization for ghost terms.

Useful? React with 👍 / 👎.

Confirmed and fixed in 34b6376. ghost!(|| -> Seq<Int> { Seq::empty() }) did panic on assertion failed: got_args.len() == expected_args.len(). type_ghost_value now pushes the same unrefined unit parameter refine/template.rs gives every other zero-argument function type, and the ghost_const pass/fail pair covers the path.

Generated by Claude Code

Copilot

Pull request overview

Introduces proof-only ghost values that retain logical refinements without runtime representation.

Changes:

Adds ghost!, Ghost<T>, and analyzer marker handling.
Preserves zero-sized MIR locals by disabling RemoveZsts.
Adds pass/fail UI coverage for local and field usage.

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
`thrust-macros/src/lib.rs`	Exports `ghost!`.
`thrust-macros/src/ghost.rs`	Implements macro expansion.
`std.rs`	Defines `Ghost<T>` and its marker.
`src/main.rs`	Disables `RemoveZsts`.
`src/analyze/annot.rs`	Registers the marker path.
`src/analyze/did_cache.rs`	Caches the marker definition.
`src/analyze/annot_fn.rs`	Retains formula parameter identifiers.
`src/analyze/local_def.rs`	Uses stored parameter identifiers.
`src/analyze/basic_block.rs`	Types ghost marker calls.
`tests/ui/pass/ghost_local.rs`	Tests valid local ghost usage.
`tests/ui/fail/ghost_local.rs`	Tests invalid local refinement.
`tests/ui/pass/ghost_field.rs`	Tests valid ghost fields.
`tests/ui/fail/ghost_field.rs`	Tests invalid ghost-field updates.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

coord-e · 2026-08-16T08:57:46Z

+        let params = param_tys
+            .iter()
+            .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous())
+            .collect();


Confirmed and fixed in 34b6376 — it panicked on assertion failed: got_args.len() == expected_args.len(). params now gets the same unrefined unit parameter that refine/template.rs adds for zero-argument functions, and ghost_const pins both directions.

Generated by Claude Code

coord-e · 2026-08-16T08:57:28Z

+    fn operand_of_name(&self, name: rustc_span::Symbol) -> Option<Operand<'tcx>> {
+        for vdi in self
+            .body
+            .var_debug_info
+            .iter()
+            .filter(|vdi| vdi.name == name)
+        {
+            match &vdi.value {
+                mir::VarDebugInfoContents::Place(place) => {
+                    if place.projection.is_empty() && self.is_defined(place.local) {
+                        return Some(Operand::Copy(*place));


Fixed in 34b6376, by rejecting rather than resolving: operand_of_name now scans every entry with the name and reports multiple distinct candidates as ambiguous, matching what local_of_name_in_bb does for invariants. Lexical scope resolution is still the better answer and remains open.

Generated by Claude Code

coord-e · 2026-08-16T08:57:55Z

+        ));
+    };
+
+    let mut fn_params: Vec<FnArg> = vec![syn::parse_quote!(result: #value_ty)];


Fixed in 34b6376. The value is now bound to __thrust_ghost_value, following the __thrust_self convention the invariant expansion already uses, so result stays free for a term to name a live variable with. ghost!(|result: i64| -> Int { result }) verifies.

Nothing reads the binder by name — to_refinement maps parameter 0 positionally — so the rename is confined to the macro.

Generated by Claude Code

coord-e · 2026-08-16T08:58:48Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 34b637663f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

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) }); The term expands into a formula function 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. `Ghost<T>` has `T`'s model, so ghost values pass through struct fields and function boundaries with the machinery that already exists for any other value. Disable the `RemoveZsts` MIR pass along the way. It rewrites reads of zero-sized locals into constants, which drops the refinement of every value whose type carries no runtime data. That covers `Ghost<T>` and the model types alike: until now nothing constructed a model-typed value in program code, so the limitation had no way to show up. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014jTCnjoii4e5r4VLEU733b

coord-e requested a balanced review from Copilot August 16, 2026 08:31

coord-e marked this pull request as ready for review August 16, 2026 08:31

Copilot started reviewing on behalf of coord-e August 16, 2026 08:32 View session

chatgpt-codex-connector Bot reviewed Aug 16, 2026

View reviewed changes

Copilot AI reviewed Aug 16, 2026

View reviewed changes

coord-e force-pushed the claude/ghost-code-implementation-vsz1tg branch from dfdaf0d to 34b6376 Compare August 16, 2026 08:57

chatgpt-codex-connector Bot reviewed Aug 16, 2026

View reviewed changes

Comment thread thrust-macros/src/ghost.rs

Comment thread std.rs Outdated

coord-e force-pushed the claude/ghost-code-implementation-vsz1tg branch from 34b6376 to 5dbfe35 Compare August 16, 2026 09:04

claude and others added 2 commits August 16, 2026 18:04

Introduce param_idents to FormulaFn

0f352fd

coord-e force-pushed the claude/ghost-code-implementation-vsz1tg branch from 5dbfe35 to 0f352fd Compare August 16, 2026 09:04

coord-e merged commit 2ab5271 into main Aug 16, 2026
6 checks passed

coord-e deleted the claude/ghost-code-implementation-vsz1tg branch August 16, 2026 09:06

coord-e mentioned this pull request Aug 16, 2026

Let a ghost term name generic- and Self-typed variables #232

Draft

Navigation Menu

Introduce ghost variables - #220

Introduce ghost variables#220
coord-e merged 2 commits into
mainfrom
claude/ghost-code-implementation-vsz1tg

coord-e commented Aug 14, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Aug 16, 2026

Uh oh!

coord-e Aug 16, 2026

Uh oh!

chatgpt-codex-connector Bot Aug 16, 2026

Uh oh!

coord-e Aug 16, 2026

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

coord-e Aug 16, 2026

Uh oh!

coord-e Aug 16, 2026

Uh oh!

coord-e Aug 16, 2026

Uh oh!

Uh oh!

coord-e commented Aug 16, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		if place.projection.is_empty() && self.is_defined(place.local) {
		return Some(Operand::Copy(*place));

Conversation

coord-e commented Aug 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

How it works

Disabling RemoveZsts

Tests

Known gaps

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

coord-e Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

coord-e Aug 16, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

coord-e commented Aug 16, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

coord-e commented Aug 14, 2026 •

edited

Loading

Disabling `RemoveZsts`