From 85d621e70b6c1454e582047eb75889848c53ed77 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 | 118 +++++++++++++++++++++++++++++++++-- src/analyze/did_cache.rs | 8 +++ src/main.rs | 9 +++ std.rs | 26 ++++++++ tests/ui/fail/ghost_const.rs | 15 +++++ tests/ui/fail/ghost_field.rs | 23 +++++++ tests/ui/fail/ghost_local.rs | 16 +++++ tests/ui/pass/ghost_const.rs | 15 +++++ tests/ui/pass/ghost_field.rs | 23 +++++++ tests/ui/pass/ghost_local.rs | 16 +++++ thrust-macros/src/ghost.rs | 68 ++++++++++++++++++++ thrust-macros/src/lib.rs | 15 +++++ 14 files changed, 358 insertions(+), 6 deletions(-) create mode 100644 tests/ui/fail/ghost_const.rs 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_const.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 f7eb1534..781b53e3 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 8d844fde..19bb8293 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -9,7 +9,7 @@ use rustc_middle::mir::{ use rustc_middle::ty::{self as mir_ty, TyCtxt}; use rustc_span::def_id::{DefId, LocalDefId}; -use crate::analyze; +use crate::analyze::{self, annot_fn::FormulaFn}; use crate::chc; use crate::pretty::PrettyDisplayExt as _; use crate::refine::{ @@ -968,6 +968,104 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } } + /// The formula function a ghost marker call carries, or `None` for any other call. + 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)) + } + + /// Forges an operand for a live variable named `name` using var_debug_info + /// + /// Shadowing can leave several entries sharing a name, and debug info does not say + /// which one the source that named it meant, so this refuses to guess. + fn operand_of_name(&self, name: rustc_span::Symbol) -> Option> { + let mut found: Option> = None; + for vdi in self + .body + .var_debug_info + .iter() + .filter(|vdi| vdi.name == name) + { + let operand = match &vdi.value { + mir::VarDebugInfoContents::Place(place) => { + if !place.projection.is_empty() || !self.is_defined(place.local) { + continue; + } + Operand::Copy(*place) + } + mir::VarDebugInfoContents::Const(constant) => { + Operand::Constant(Box::new(*constant)) + } + }; + match &found { + None => found = Some(operand), + Some(prev) if *prev == operand => {} + Some(_) => self.tcx.dcx().fatal(format!( + "ghost term refers to `{name}`, which is ambiguous here: multiple live \ + variables share this name (e.g. through shadowing). Rename the variables \ + to disambiguate." + )), + } + } + + found + } + + /// Types the introduction of a ghost value as a call to the function the ghost term + /// denotes: one from the live variables it names to a value refined by the term. + fn type_ghost_value(&mut self, formula_fn: FormulaFn<'tcx>, expected: &rty::RefinedType) { + let (value_ty, param_tys) = formula_fn + .params() + .raw + .split_first() + .expect("ghost formula function takes the ghost value as its first parameter"); + let mut params: IndexVec<_, _> = param_tys + .iter() + .map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous()) + .collect(); + if params.is_empty() { + // elaboration: we need at least one predicate variable in parameter + params.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous()); + } + 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 args = formula_fn + .param_idents() + .iter() + .skip(1) + .map(|ident| { + let operand = self.operand_of_name(ident.name).unwrap_or_else(|| { + self.tcx.dcx().fatal(format!( + "ghost term refers to `{ident}`, which is not a live variable here" + )) + }); + self.operand_refined_type(operand) + }) + .collect(); + + let clauses = self.relate_fn_sub_type(func_ty, args, expected.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 +1326,19 @@ 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) { + let formula_fn = self + .ctx + .formula_fn_with_args(formula_def_id, generic_args) + .expect("ghost formula function is not registered"); + self.type_ghost_value(formula_fn, &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..af74cb42 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()); + // Refinements live on MIR locals, and `RemoveZsts` rewrites reads of zero-sized + // locals into constants, losing 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..96d88669 100644 --- a/std.rs +++ b/std.rs @@ -412,6 +412,32 @@ mod thrust_models { unimplemented!() } + /// Proof-only data, introduced by `thrust_macros::ghost!`. In the logic it is its + /// content, so a specification refers to a `Ghost` as if it were a `T`. + #[allow(dead_code)] + pub struct Ghost(std::marker::PhantomData); + + 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; + } + + #[doc(hidden)] + #[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_const.rs b/tests/ui/fail/ghost_const.rs new file mode 100644 index 00000000..2cc9cf57 --- /dev/null +++ b/tests/ui/fail/ghost_const.rs @@ -0,0 +1,15 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +#[thrust_macros::requires(s.len() == 0)] +fn expect_empty(s: Ghost>) { + let _ = s; +} + +fn main() { + let s = thrust_macros::ghost!(|| -> Seq { Seq::singleton(Seq::::empty().len()) }); + expect_empty(s); +} diff --git a/tests/ui/fail/ghost_field.rs b/tests/ui/fail/ghost_field.rs new file mode 100644 index 00000000..70aafb7e --- /dev/null +++ b/tests/ui/fail/ghost_field.rs @@ -0,0 +1,23 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +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_const.rs b/tests/ui/pass/ghost_const.rs new file mode 100644 index 00000000..6e2158ef --- /dev/null +++ b/tests/ui/pass/ghost_const.rs @@ -0,0 +1,15 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +#[thrust_macros::requires(s.len() == 0)] +fn expect_empty(s: Ghost>) { + let _ = s; +} + +fn main() { + let s = thrust_macros::ghost!(|| -> Seq { Seq::empty() }); + expect_empty(s); +} diff --git a/tests/ui/pass/ghost_field.rs b/tests/ui/pass/ghost_field.rs new file mode 100644 index 00000000..1edee942 --- /dev/null +++ b/tests/ui/pass/ghost_field.rs @@ -0,0 +1,23 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off -A unused-variables + +use thrust_models::model::{Int, Seq}; +use thrust_models::Ghost; + +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..794b173d --- /dev/null +++ b/thrust-macros/src/ghost.rs @@ -0,0 +1,68 @@ +//! Expansion of `thrust_macros::ghost!` into a `#[thrust::formula_fn]` relating the +//! introduced value to the ghost term, plus a marker call the analyzer intercepts. +//! +//! The value is parameter `0`, as in an `ensures` formula function: that is the layout +//! the analyzer reads the term back with. Unlike `ensures`, it is bound to a synthetic +//! name, leaving `result` free for a term to name a live variable with. + +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 { .. }`", + )); + }; + + // Synthetic, so that a term may name a live variable called `result`. + let value = format_ident!("__thrust_ghost_value"); + let mut fn_params: Vec = vec![syn::parse_quote!(#value: #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!({ + #[thrust::formula_fn] + fn #name(#model_ty_params) -> bool { + #value == (#body) + } + + thrust_models::__ghost_marker::<_, #value_ty>(#name) + })) +} diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs index ddda2388..165409a3 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,20 @@ 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!(|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 0f352fdd5e5dc16b2f7a24df3819198c49c1904d Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 16 Aug 2026 17:26:47 +0900 Subject: [PATCH 2/2] Introduce param_idents to FormulaFn --- src/analyze/annot_fn.rs | 16 ++++++++++++++++ src/analyze/basic_block.rs | 1 + src/analyze/local_def.rs | 10 +++++----- 3 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 781b53e3..7d0200a8 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -13,6 +13,9 @@ use crate::rty; #[derive(Debug, Clone)] pub struct FormulaFn<'tcx> { params: IndexVec>, + // TODO: remove once we stop relying on debug info to map parameters + // `None` for a parameter bound by a pattern, as the closure upvars tuple is. + param_idents: IndexVec>, formula: chc::Formula, } @@ -47,6 +50,12 @@ impl<'tcx> FormulaFn<'tcx> { &self.params } + pub fn param_idents( + &self, + ) -> &IndexVec> { + &self.param_idents + } + pub fn to_require_formula(&self) -> chc::Formula { self.formula.clone() } @@ -386,8 +395,15 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { .skip_binder() .inputs() .to_vec(); + let param_idents = self + .tcx + .fn_arg_idents(self.local_def_id.to_def_id()) + .iter() + .copied() + .collect(); FormulaFn { params: IndexVec::from_raw(params), + param_idents, formula, } } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 19bb8293..97ae3ec0 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1053,6 +1053,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .iter() .skip(1) .map(|ident| { + let ident = ident.expect("ghost term parameters must be named"); let operand = self.operand_of_name(ident.name).unwrap_or_else(|| { self.tcx.dcx().fatal(format!( "ghost term refers to `{ident}`, which is not a live variable here" diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 68b0d646..a98eb1ce 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -836,15 +836,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .ctx .formula_fn_with_args(formula_def_id, generic_args) .expect("invariant formula function is not registered"); - let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id()); + let idents = formula_fn.param_idents(); let sig = self .tcx .fn_sig(formula_def_id.to_def_id()) .instantiate(self.tcx, generic_args); let mut mapping: Vec = Vec::with_capacity(idents.len()); - for (ident_opt, input_ty) in idents.iter().zip(sig.skip_binder().inputs()) { - let name = ident_opt.expect("invariant parameters must be named").name; + for (ident, input_ty) in idents.iter().zip(sig.skip_binder().inputs()) { + let ident = ident.expect("invariant parameters must be named"); let input_ty = { let typing_env = mir_ty::TypingEnv::post_analysis(self.tcx, formula_def_id.to_def_id()); @@ -855,10 +855,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // The synthetic `__thrust_self` parameter (emitted when an invariant refers to the receiver // `self`) maps to the loop-carried receiver, which appears as `self` in debug info. - let name = if name.as_str() == "__thrust_self" { + let name = if ident.name.as_str() == "__thrust_self" { rustc_span::Symbol::intern("self") } else { - name + ident.name }; if input_ty