Support multi-crate projects (cargo)

[coord-e]

Goal

Run Thrust over a cargo workspace: a crate compiled by thrust-rustc publishes its specifications, and a downstream crate checks calls into that crate against them.

Specifications cannot be exported as lowered rty

The obvious design — build rty::FunctionType at the definition site, export it, instantiate it downstream — does not work.

Three kinds of type-relative thing can appear in a specification:

1. closure pre/postconditions (pre! / post!)
2. predicates dispatched through a trait (<T as Foo>::pred)
3. associated types (<T as Iterator>::Item)

Instantiating an rty type is an rty→rty substitution (filling Type::Param with an rty::Type), so a polymorphic rty::FunctionType is only instantiable if all three can be resolved during that substitution. None of them can:

• (1) needs the closure's DefId, but a closure reaches rty as a TupleType — replace_closure_model turns it into its upvars tuple and the DefId is gone.
• (2) needs to find the impl, which needs the implementer's mir_ty::Ty.
• (3) is normalization, which needs mir_ty::Ty — both at the substituted position and for the projection's non-param arguments.

So resolving them requires rty::Type -> mir_ty::Ty, and that is impossible in principle because the lowering is not injective:

• every integer type maps to Type::Int (std.rs:258, int_model! expanded for all of them via Model::Ty)
• every struct maps to a TupleType of its field types (src/refine/template.rs:250), so struct A(i32), struct B(i32) and (i32,) are indistinguishable
• a closure maps to its upvars tuple

Moving the instantiation outside rty — substituting mir_ty::Ty into an rty::Type — would mostly handle (1) and (2), but not (3).

Conclusion: exported signatures are not instantiated. The downstream crate constructs the rty::FunctionType itself, at the point where the types are filled in. Associated types, which have no image in chc::Sort, do not belong in rty::Type.

This is about function signatures only. Type::Param in datatype declarations indexes a datatype's own arguments and is substituted with rty::Types during enum unfolding, which involves none of the three; that stays as it is.

What has to cross the boundary

Building the specification downstream means running the annotation translation there, and that reads HIR today (extract_require_annot → extract_path_with_attr → tcx.hir_maybe_body_owned_by). HIR is not in crate metadata and cannot be: it is arena-allocated and HirId-keyed. TypeckResults is encodable for the incremental cache but is also HirId-keyed and useless without the HIR.

MIR is in metadata — for generic functions. That splits the work along exactly the line rustc draws:

	dependency MIR available?	approach
non-generic def	no	pre-translate at the definition site, export the concrete spec
generic def	yes	downstream rebuilds the spec from MIR

Plan

A. Non-generic defs — independent of the rest

Export the concrete rty::RefinedType of each exportable non-generic def to a side file; load dependencies' files into defs before analysis.

• File next to the crate's metadata output, found for dependencies via tcx.used_crate_source(cnum) — what both Prusti (lib*.specs) and Creusot (*.cmeta) do. Keys are DefPathHash; skip entries whose StableCrateId is not loaded. A stale file is a real hazard: Prusti catches it and tells the user to cargo clean -p <crate>.
• The payload is plain data, so serde/JSON is enough here.
• Export only defs whose spec contains no Pred::Var — assert it. PredVarId indexes this crate's System::pred_vars, and solve never extracts a model, so an inferred spec cannot cross. In practice that is is_fully_annotated plus trusted / extern_spec_fn.
• rty::EnumType carries only a DatatypeSymbol (src/rty.rs:715), so an imported spec naming a datatype cannot be traced back to a DefId to register it. Carry the identity instead — a DefPathHash on EnumType, or a symbol -> DefPathHash table in the file — so the importer can call get_or_register_enum_def with a real DefId. Nothing else about datatypes needs exporting: every query build_enum_def uses (adt_def, type_of, generics_of, predicates_of, const_eval_poly) works on foreign DefIds, which is already how Option/Result/Vec are handled today.
• #[thrust::predicate] bodies must be in the file: an imported spec mentioning Pred::UserDefined needs its define-fun downstream, and predicate functions are usually non-generic, so the MIR path in B will not reach them. Same for a crate-level #[thrust::raw_command] that a spec depends on.

B. Generic defs

1. Build FormulaFn from MIR instead of HIR.
2. Make the {requires,ensures,refinement}_path links survive into MIR. They are path statements today (thrust-macros/src/spec.rs:415, rty.rs:484, with #[allow(path_statements)]), and a path expression naming a fn item is a ZST const that does not reach MIR. invariant! and ghost! already use real marker calls, so this makes the mechanism uniform. Note that refinement_path carries data in the attribute (the position steps), so those have to be encoded into the call — a &'static str const argument, or const generics — not just turned into a marker.
3. Do not analyze the body in def_ty_with_args when the def is not local; treat it as trusted.

After 1 and 2, constructing an rty::FunctionType is the same code path whether the def is local or foreign, so 3 is the only behavioural change left. Two things it needs beyond the flag:

• DeferredDefTy holds local_def_id: LocalDefId (src/analyze.rs:170); it has to become DefId.
• Nothing registers foreign defs today. refine_fn_def iterates tcx.mir_keys(()), which is local-only, and a miss in def_ty_with_args panics. Registering lazily on that miss fits naturally: if the def is foreign, pull its optimized_mir and look for the markers. "Has MIR" is then exactly the generic/non-generic split, so the side file stays purely non-generic specs.

invariant! and ghost! never need to cross the boundary, because foreign bodies are never analyzed.

Soundness posture

A dependency's generic function is proved only at the instantiations that dependency exercised. A downstream crate instantiating it at a new type uses a contract that was never discharged there.

Re-checking the foreign body at the importing crate's instantiations is the principled fix, but it needs a spec for everything the body transitively calls, and an unannotated non-generic callee has neither an exportable spec (pred vars) nor MIR in metadata. So the boundary is: an exported contract is trusted at instantiations the defining crate did not exercise. That is the same trust #[extern_spec] carries in Prusti and Creusot, where it is unconditional.

Calls to defs with no spec

Give them requires false and report a warn-by-default tool lint at the call site, as Creusot does with contractless_external_function. A silently trusting true/true contract hides exactly what a user needs to see, and #[thrust::trusted] already covers the deliberate case; a lint keeps #[allow(..)] available for a dependency nobody intends to verify. Needed as soon as A lands, since calls into unspecified dependency code become routine then.

Also needed

• after_analysis returns Compilation::Stop (src/main.rs:69), so no artifacts are produced. Under cargo it has to continue, so downstream crates have something to --extern (Creusot: if self.opts.in_cargo { Continue } else { Stop }).
• Which crates get verified is the wrapper choice: RUSTC_WORKSPACE_WRAPPER for workspace members, RUSTC_WRAPPER for dependencies as well. Build scripts and proc-macro crates must pass through to the real rustc.
• A spec-only crate does not appear in tcx.crates(()) unless referenced. --extern force:name=path should avoid the extern crate workaround Prusti documents.
• DefIdCache::annotated_def (src/analyze/did_cache.rs:97) scans tcx.hir_free_items(), so it sees only the local crate. Once the model types live in a real crate the #[thrust::def::*] attributes lose their purpose — they exist because std.rs is injected and therefore has no stable path. Resolve by path from the named dependency's root (module_children, plus associated_items for Model::Ty), and delete both the attributes and the scan.
• datatype_symbol (src/refine.rs:35) uses def_path_str, which has no crate disambiguator. Two versions of one crate now collide inside a single downstream chc::System.

Open

enum A<T: Trait> { V1(T::Assoc) } ICEs today at build_enum_def (unimplemented!("unrefined_ty: Alias(Projection, ..)"), src/refine/template.rs:269), independently of any of this — and even when the use site is fully concrete, because the datatype is registered generically. Consistent with the conclusion above, the fix is to instantiate before lowering (key get_or_register_enum_def on (DefId, args)) rather than to give rty a representation for projections.

That is in tension with #93, which adds an rty node for unresolved projections in service of def-site verification of generic functions. Which mode a crate uses for body checking is a local choice and the two can coexist, but the form a specification takes when it crosses a crate boundary has to be decided once. Worth settling before B starts.