Centralize Model type lowering logic in thrust-macros to FormulaFnTypeLowering

[coord-e]

extracted from #104

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, you can upgrade your account or add credits to your account and enable them for code reviews in your settings.

[Copilot]

Pull request overview

This PR refactors thrust-macros to centralize formula-function type lowering and Model-predicate generation into a new FormulaFnTypeLowering helper, replacing previously duplicated logic scattered across macro expansions.

Changes:

• Introduces FormulaFnTypeLowering to handle parameter/return type lowering and generation of Model/PartialEq where-predicates.
• Migrates #[predicate], #[requires]/#[ensures], and invariant-related expansions to use the shared lowering helper.
• Removes the old lowering/predicate helpers from thrust-macros/src/lib.rs in favor of the new module.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
thrust-macros/src/spec.rs	Switches requires/ensures/predicate expansion to use centralized type lowering + predicate generation.
thrust-macros/src/lib.rs	Registers new module and removes old helper functions that were moved into the new lowering helper.
thrust-macros/src/invariant.rs	Uses centralized lowering/predicate generation when expanding invariants.
thrust-macros/src/invariant_context.rs	Uses centralized predicate generation when threading generic context into invariants.
thrust-macros/src/formula_fn_type_lowering.rs	New shared implementation for parameter/return lowering and Model where-predicate generation.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.