Anchor macro-emitted model paths at the crate root

[coord-e]

Fixes #252.

thrust_models is injected as a crate-root mod of the crate under verification, so the unqualified thrust_models::… paths the annotation macros expanded to only resolved at the crate root. Every annotation on an item inside a mod failed with E0433, leaving a program unable to be both modularised and specified.

Every emission site now writes crate::thrust_models::…:

• formula_fn_type_lowering.rs — <T as Model>::Ty for parameters and return type, model::Closure<F>, and the Model / PartialEq where-predicates
• rty.rs — the binder type of param/ret/sig
• invariant.rs — __invariant_marker
• ghost.rs — __ghost_marker
• formula.rs — implies for ==>
• pre_post.rs — closure_precondition / closure_postcondition

crate:: resolves the same way under edition 2015, which the driver currently uses, and under 2018+.

Two UI test pairs cover annotations inside a mod: mod_annot (requires/ensures on a function in a module) and mod_invariant (invariant! in a module).

Verification

• cargo test — 338 UI tests and the unit tests pass, no regression against the existing 334; cargo fmt --all -- --check and cargo clippy -- -D warnings are clean.
• Reproductions (1), (2) and (3) from the issue all compile and verify. (2) reports safe, and breaking its assertion to start + 11 reports Unsat, so the module case is checked in both directions.
• ghost!, sig, pre!/post! and #[thrust::predicate] inside a mod were checked separately.
• That crate:: resolves under edition 2015 was confirmed by compiling a crate-root-private mod referenced from a submodule with rustc --edition 2015.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LxfDwbBfdK9zRC7jBRCArW

---

Generated by Claude Code

[Copilot]

🟡 Changes recommended

Several independently modified macro emission paths lack nested-module regression coverage.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Anchors generated model paths at the crate root so annotations work inside modules.

Changes:

• Updated all macro emission sites to use crate::thrust_models.
• Updated implication expansion unit tests.
• Added pass/fail UI tests for modular annotations and invariants.

File summaries

File	Description
thrust-macros/src/rty.rs	Anchors refinement binder model types.
thrust-macros/src/pre_post.rs	Anchors closure contract markers.
thrust-macros/src/invariant.rs	Anchors invariant markers.
thrust-macros/src/ghost.rs	Anchors ghost markers.
thrust-macros/src/formula.rs	Anchors implication expansion and expectations.
thrust-macros/src/formula_fn_type_lowering.rs	Anchors generated model types and bounds.
tests/ui/pass/mod_invariant.rs	Adds passing modular invariant coverage.
tests/ui/fail/mod_invariant.rs	Adds failing modular invariant coverage.
tests/ui/pass/mod_annot.rs	Adds passing modular contract coverage.
tests/ui/fail/mod_annot.rs	Adds failing modular contract coverage.

Review details

• Files reviewed: 10/10 changed files
• Comments generated: 1
• Review effort level: Balanced

---

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