From 5b414c2e65fb667eeb853d41c293444326b8a48e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 14:47:57 +0000 Subject: [PATCH 1/2] Introduce ghost variables 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 { 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` 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` 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 Claude-Session: https://claude.ai/code/session_014jTCnjoii4e5r4VLEU733b --- src/analyze/annot.rs | 8 +++ src/analyze/annot_fn.rs | 4 ++ src/analyze/basic_block.rs | 107 +++++++++++++++++++++++++++++++++-- src/analyze/did_cache.rs | 8 +++ src/main.rs | 9 +++ std.rs | 30 ++++++++++ tests/ui/fail/ghost_field.rs | 24 ++++++++ tests/ui/fail/ghost_local.rs | 16 ++++++ tests/ui/pass/ghost_field.rs | 24 ++++++++ tests/ui/pass/ghost_local.rs | 16 ++++++ thrust-macros/src/ghost.rs | 93 ++++++++++++++++++++++++++++++ thrust-macros/src/lib.rs | 16 ++++++ 12 files changed, 350 insertions(+), 5 deletions(-) create mode 100644 tests/ui/fail/ghost_field.rs create mode 100644 tests/ui/fail/ghost_local.rs create mode 100644 tests/ui/pass/ghost_field.rs create mode 100644 tests/ui/pass/ghost_local.rs create mode 100644 thrust-macros/src/ghost.rs diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index a4df8ae0..390518dc 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -202,6 +202,14 @@ pub fn invariant_marker_path() -> [Symbol; 3] { ] } +pub fn ghost_marker_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("ghost_marker"), + ] +} + pub fn fn_param_wrapper_path() -> [Symbol; 3] { [ Symbol::intern("thrust"), diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 1eea3402..22d7d912 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -43,6 +43,10 @@ impl<'tcx> FormulaFn<'tcx> { &self.formula } + pub fn params(&self) -> &IndexVec> { + &self.params + } + pub fn to_require_formula(&self) -> chc::Formula { self.formula.clone() } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 4ed04196..70476ea8 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -968,6 +968,99 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } } + /// The formula function a ghost marker call carries, or `None` for any other call. + /// + /// The marker's argument is the formula function item `thrust_macros::ghost!` + /// introduces, whose parameter `0` is the ghost value and whose remaining parameters + /// name the live variables the ghost term refers to. + fn ghost_marker_formula_fn( + &self, + func: &Operand<'tcx>, + args: &[rustc_span::source_map::Spanned>], + ) -> Option<(LocalDefId, mir_ty::GenericArgsRef<'tcx>)> { + let (def_id, _) = func.const_fn_def()?; + if Some(def_id) != self.ctx.def_ids().ghost_marker() { + return None; + } + + let arg_ty = args[0].node.ty(&self.local_decls, self.tcx); + let mir_ty::TyKind::FnDef(formula_def_id, generic_args) = arg_ty.kind() else { + panic!("ghost marker argument must be a formula function item"); + }; + let formula_def_id = formula_def_id + .as_local() + .expect("ghost formula function must be local"); + Some((formula_def_id, generic_args)) + } + + /// Resolves the value a ghost term refers to by source variable name. + /// + /// A variable whose value is a constant is held in the debug info itself rather than + /// in a local of its own, so both forms are read back here. + fn operand_of_name(&self, name: rustc_span::Symbol) -> Option> { + self.body + .var_debug_info + .iter() + .filter(|vdi| vdi.name == name) + .find_map(|vdi| match &vdi.value { + mir::VarDebugInfoContents::Place(place) => (place.projection.is_empty() + && self.is_defined(place.local)) + .then(|| Operand::Copy(*place)), + mir::VarDebugInfoContents::Const(constant) => { + Some(Operand::Constant(Box::new(constant.clone()))) + } + }) + } + + /// Types the introduction of a ghost value: the value is the one its term denotes in + /// the current environment. + /// + /// A ghost term is a formula function laid out like an `ensures` — parameter `0` is + /// the value, the rest are free — so it reads as the return refinement of a function + /// over the live variables it names, and the introduction as a call to that function. + fn type_ghost_value( + &mut self, + formula_def_id: LocalDefId, + generic_args: mir_ty::GenericArgsRef<'tcx>, + expected_value: &rty::RefinedType, + ) { + let formula_fn = self + .ctx + .formula_fn_with_args(formula_def_id, generic_args) + .expect("ghost formula function is not registered"); + let (value_ty, param_tys) = formula_fn + .params() + .raw + .split_first() + .expect("ghost formula function takes the ghost value as its first parameter"); + let params = param_tys + .iter() + .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous()) + .collect(); + let value_ty = self.type_builder.build(*value_ty); + let func_ty = rty::FunctionType::new( + params, + rty::RefinedType::new(value_ty.vacuous(), formula_fn.to_refinement()), + ); + + let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id()).to_vec(); + let args = idents[1..] + .iter() + .map(|ident| { + let name = ident.expect("ghost term parameters must be named").name; + let operand = self.operand_of_name(name).unwrap_or_else(|| { + self.tcx.dcx().fatal(format!( + "ghost term refers to `{name}`, which is not a live variable here" + )) + }); + self.operand_refined_type(operand) + }) + .collect(); + + let clauses = self.relate_fn_sub_type(func_ty, args, expected_value.clone()); + self.ctx.extend_clauses(clauses); + } + fn elaborate_place(&self, place: &mir::Place<'tcx>) -> mir::Place<'tcx> { let mut projection = Vec::new(); if self.is_mut_local(place.local) { @@ -1228,11 +1321,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .for_template(&mut self.ctx) .with_scope(&self.env) .build_refined(decl.ty); - self.type_call( - func.clone(), - args.clone().iter().map(|a| a.node.clone()), - &rty, - ); + if let Some((formula_def_id, generic_args)) = self.ghost_marker_formula_fn(func, args) { + self.type_ghost_value(formula_def_id, generic_args, &rty); + } else { + self.type_call( + func.clone(), + args.clone().iter().map(|a| a.node.clone()), + &rty, + ); + } self.bind_local(destination, rty); } } diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index 4dbcf110..d29f8510 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -35,6 +35,7 @@ struct DefIds { forall: OnceCell>, implies: OnceCell>, invariant_marker: OnceCell>, + ghost_marker: OnceCell>, fn_param_wrapper: OnceCell>, fn_param_at_entry: OnceCell>, @@ -256,6 +257,13 @@ impl<'tcx> DefIdCache<'tcx> { .get_or_init(|| self.annotated_def(&crate::analyze::annot::invariant_marker_path())) } + pub fn ghost_marker(&self) -> Option { + *self + .def_ids + .ghost_marker + .get_or_init(|| self.annotated_def(&crate::analyze::annot::ghost_marker_path())) + } + pub fn fn_param_wrapper(&self) -> Option { *self .def_ids diff --git a/src/main.rs b/src/main.rs index 960ebc1b..d0846602 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,6 +19,15 @@ impl Callbacks for CompilerCalls { attrs.push("feature(register_tool)".to_owned()); attrs.push("register_tool(thrust)".to_owned()); + // Thrust refines values, which it tracks through MIR locals. `RemoveZsts` rewrites + // reads of zero-sized locals into constants, which loses the refinement of every + // value whose type carries no runtime data -- the model types and `Ghost`. + config + .opts + .unstable_opts + .mir_enable_passes + .push(("RemoveZsts".to_owned(), false)); + config.override_queries = Some(|_sess, providers| { providers.mir_borrowck = thrust::mir_borrowck_skip_formula_fn; }); diff --git a/std.rs b/std.rs index 105c8807..5414881a 100644 --- a/std.rs +++ b/std.rs @@ -412,6 +412,36 @@ mod thrust_models { unimplemented!() } + /// Proof-only data, introduced by `thrust_macros::ghost!`. + /// + /// A `Ghost` has no runtime representation, and program code cannot observe its + /// content: the only operations on it are moving and copying it around. In the logic + /// it *is* its content, so a specification refers to it as if it were a `T`. + #[allow(dead_code)] + pub struct Ghost(std::marker::PhantomData); + + // `PhantomData` is `Copy` whatever `T` is, so these are unconditional; deriving them + // would demand `T: Copy`. + impl Clone for Ghost { + #[thrust::ignored] + fn clone(&self) -> Self { + *self + } + } + + impl Copy for Ghost {} + + impl Model for Ghost where T: Model { + type Ty = ::Ty; + } + + #[thrust::def::ghost_marker] + #[thrust::ignored] + #[inline(never)] + pub fn __ghost_marker(_f: F) -> Ghost { + Ghost(std::marker::PhantomData) + } + #[allow(dead_code)] #[thrust::def::fn_param_wrapper] pub struct FnParam(std::marker::PhantomData); diff --git a/tests/ui/fail/ghost_field.rs b/tests/ui/fail/ghost_field.rs new file mode 100644 index 00000000..79a9c331 --- /dev/null +++ b/tests/ui/fail/ghost_field.rs @@ -0,0 +1,24 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +/// Counts how many values were recorded, and remembers them in a ghost field. +struct Counter { + count: i64, + seen: Ghost>, +} + +impl thrust_models::Model for Counter { + type Ty = (Int, Seq); +} + +#[thrust_macros::requires((*c).1.len() == (*c).0)] +#[thrust_macros::ensures((!c).1.len() == (!c).0)] +fn record(c: &mut Counter, x: i64) { + c.count += 1; + c.seen = thrust_macros::ghost!(|c: &mut Counter, x: i64| -> Seq { (*c).1 }); +} + +fn main() {} diff --git a/tests/ui/fail/ghost_local.rs b/tests/ui/fail/ghost_local.rs new file mode 100644 index 00000000..010e8356 --- /dev/null +++ b/tests/ui/fail/ghost_local.rs @@ -0,0 +1,16 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +#[thrust_macros::requires(s.len() == 1)] +fn expect_len_one(s: Ghost>) { + let _ = s; +} + +fn main() { + let x: i64 = 3; + let s = thrust_macros::ghost!(|x: i64| -> Seq { Seq::singleton(x).push(x) }); + expect_len_one(s); +} diff --git a/tests/ui/pass/ghost_field.rs b/tests/ui/pass/ghost_field.rs new file mode 100644 index 00000000..89a23e08 --- /dev/null +++ b/tests/ui/pass/ghost_field.rs @@ -0,0 +1,24 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +/// Counts how many values were recorded, and remembers them in a ghost field. +struct Counter { + count: i64, + seen: Ghost>, +} + +impl thrust_models::Model for Counter { + type Ty = (Int, Seq); +} + +#[thrust_macros::requires((*c).1.len() == (*c).0)] +#[thrust_macros::ensures((!c).1.len() == (!c).0)] +fn record(c: &mut Counter, x: i64) { + c.count += 1; + c.seen = thrust_macros::ghost!(|c: &mut Counter, x: i64| -> Seq { (*c).1.push(x) }); +} + +fn main() {} diff --git a/tests/ui/pass/ghost_local.rs b/tests/ui/pass/ghost_local.rs new file mode 100644 index 00000000..8eefbfcf --- /dev/null +++ b/tests/ui/pass/ghost_local.rs @@ -0,0 +1,16 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +#[thrust_macros::requires(s.len() == 1)] +fn expect_len_one(s: Ghost>) { + let _ = s; +} + +fn main() { + let x: i64 = 3; + let s = thrust_macros::ghost!(|x: i64| -> Seq { Seq::singleton(x) }); + expect_len_one(s); +} diff --git a/thrust-macros/src/ghost.rs b/thrust-macros/src/ghost.rs new file mode 100644 index 00000000..6d2d279a --- /dev/null +++ b/thrust-macros/src/ghost.rs @@ -0,0 +1,93 @@ +//! Expansion of `thrust_macros::ghost!`. +//! +//! A ghost expression is a logical term over the live variables it names, so it expands +//! into a `#[thrust::formula_fn]` relating the introduced value to that term, laid out +//! like an `ensures` formula function (parameter `0` is the value), plus a marker call +//! the analyzer intercepts to bind the value: +//! +//! ```ignore +//! ghost!(|s: Ghost>, x: i64| -> Seq { s.push(x) }) +//! ``` +//! +//! becomes +//! +//! ```ignore +//! { +//! #[thrust::formula_fn] +//! fn _thrust_ghost_0( +//! result: as Model>::Ty, +//! s: > as Model>::Ty, +//! x: ::Ty, +//! ) -> bool { +//! result == (s.push(x)) +//! } +//! thrust_models::__ghost_marker::<_, Seq>(_thrust_ghost_0) +//! } +//! ``` +//! +//! The parameters name the live variables the term refers to, with their types, exactly +//! as in [`crate::invariant`]; the return type names the logical type of the introduced +//! value. + +use std::sync::atomic::{AtomicUsize, Ordering}; + +use proc_macro::TokenStream; +use quote::{format_ident, ToTokens}; +use syn::FnArg; + +use crate::FormulaFnTypeLowering; + +static COUNTER: AtomicUsize = AtomicUsize::new(0); + +pub fn expand(input: TokenStream) -> TokenStream { + let input = crate::formula::wrap_closure_body(input.into()); + let closure = match syn::parse2::(input) { + Ok(closure) => closure, + Err(e) => return e.to_compile_error().into(), + }; + match expand_ghost(&closure) { + Ok(expr) => expr.into_token_stream().into(), + Err(e) => e.to_compile_error().into(), + } +} + +fn expand_ghost(closure: &syn::ExprClosure) -> syn::Result { + let syn::ReturnType::Type(_, value_ty) = &closure.output else { + return Err(syn::Error::new_spanned( + closure, + "ghost expression must have an explicit type, e.g. `|x: i64| -> Seq { .. }`", + )); + }; + + // Parameter `0` is the introduced value, named `result` as in an `ensures` formula. + let mut fn_params: Vec = vec![syn::parse_quote!(result: #value_ty)]; + for param in &closure.inputs { + let syn::Pat::Type(pt) = param else { + return Err(syn::Error::new_spanned( + param, + "ghost expression parameters must have explicit types, e.g. `|x: i64| ...`", + )); + }; + let pat = &pt.pat; + let ty = &pt.ty; + fn_params.push(syn::parse_quote!(#pat: #ty)); + } + + let dummy_sig = syn::parse_quote!(fn f()); + let model_ty_params = FormulaFnTypeLowering::new(&dummy_sig).lower_params(&fn_params); + + let body = &closure.body; + let id = COUNTER.fetch_add(1, Ordering::Relaxed); + let name = format_ident!("_thrust_ghost_{}", id); + + Ok(syn::parse_quote!({ + #[allow(unused_variables)] + #[allow(non_snake_case)] + #[thrust::formula_fn] + fn #name(#model_ty_params) -> bool { + result == (#body) + } + + thrust_models::__ghost_marker::<_, #value_ty>(#name) + })) +} diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs index ddda2388..62ed39eb 100644 --- a/thrust-macros/src/lib.rs +++ b/thrust-macros/src/lib.rs @@ -6,6 +6,7 @@ mod context; mod fn_outer_item; mod formula; mod formula_fn_type_lowering; +mod ghost; mod invariant; mod invariant_context; mod pre_post; @@ -38,6 +39,21 @@ pub fn closure(input: TokenStream) -> TokenStream { closure::expand(input) } +/// Introduces a ghost value: proof-only data with no runtime representation. +/// +/// ```ignore +/// let s = thrust_macros::ghost!(|| -> Seq { Seq::empty() }); +/// let s = thrust_macros::ghost!(|s: Ghost>, x: i64| -> Seq { s.push(x) }); +/// ``` +/// +/// The argument is a closure whose parameters name the live variables the ghost term +/// refers to (with their types) and whose return type is the logical type of the value. +/// See [`mod@ghost`]. +#[proc_macro] +pub fn ghost(input: TokenStream) -> TokenStream { + ghost::expand(input) +} + #[proc_macro_attribute] pub fn context(_attr: TokenStream, item: TokenStream) -> TokenStream { context::expand(item) From fa11a24ed36cbb7c002c0a5d533af3a94716d05f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 14:52:29 +0000 Subject: [PATCH 2/2] Satisfy clippy in the ghost value binding Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_014jTCnjoii4e5r4VLEU733b --- src/analyze/basic_block.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 70476ea8..d01327d6 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1005,9 +1005,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .find_map(|vdi| match &vdi.value { mir::VarDebugInfoContents::Place(place) => (place.projection.is_empty() && self.is_defined(place.local)) - .then(|| Operand::Copy(*place)), + .then_some(Operand::Copy(*place)), mir::VarDebugInfoContents::Const(constant) => { - Some(Operand::Constant(Box::new(constant.clone()))) + Some(Operand::Constant(Box::new(*constant))) } }) }