Support enum/existentials in formula_fn

[coord-e]

for #57
continued from #65

[Copilot]

Pull request overview

This PR extends #[thrust::formula_fn] translation to cover (1) existential quantification via an exists helper and (2) enum variant constructors, enabling requires/ensures specifications to mention these constructs directly in Rust expressions (continuing the work from #57 / #65).

Changes:

• Add thrust_models::exists(...) as a definitional hook and teach AnnotFnTranslator to translate exists(|...| ...) into chc::Formula::exists.
• Add enum variant-constructor term translation (X::A(...), unit variants, etc.) to formula_fn translation.
• Add UI pass/fail tests validating existential and enum usage in formula_fn annotations.

Reviewed changes

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

Show a summary per file

File	Description
src/analyze/annot_fn.rs	Adds TypeBuilder usage, enum constructor term translation, and exists closure lowering to CHC existentials.
src/analyze/did_cache.rs	Caches the DefId for the new #[thrust::def::exists] hook.
src/analyze/annot.rs	Adds the attribute path helper for thrust::def::exists.
std.rs	Introduces the #[thrust::def::exists] stub in the injected thrust_models module.
tests/ui/pass/annot_exists_formula_fn.rs	New passing test for existential quantification in formula_fn ensures.
tests/ui/fail/annot_exists_formula_fn.rs	New failing test ensuring existential postcondition is rejected when not satisfied.
tests/ui/pass/annot_enum_simple_formula_fn.rs	New passing test for enum constructor equality in formula_fn requires.
tests/ui/fail/annot_enum_simple_formula_fn.rs	New failing counterpart for the enum constructor formula_fn test.

---

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