Implement #[thrust::formula_fn] and requires/ensures annotation using it

[coord-e]

for #57

#[thrust::formula_fn] allows building chc::Formula with Rust expression. annot_fn:AnnotFnTranslator translates Rust HIR into chc::Formula. Users can specify formula_fn as requires/ensures annotations by specifying them using #[thrust::requires_path] and #[thrust::ensures_path].

Basic integer arithmetic and box/mut operations are supported. Support for ADTs and existentials will be added later.

[Copilot]

Pull request overview

This PR adds support for expressing requires/ensures annotations via actual Rust functions marked with #[thrust::formula_fn], and referencing those functions from annotated code using #[thrust::requires_path] / #[thrust::ensures_path].

Changes:

• Introduce AnnotFnTranslator to translate Rust HIR expressions in #[thrust::formula_fn] bodies into chc::Formula.
• Add requires_path / ensures_path extraction by scanning attributed path statements inside function bodies.
• Extend the injected std.rs model types (Int/Mut/Box/Array) with trait ops used by formula functions, and skip MIR borrowck for formula functions.

Reviewed changes

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

Show a summary per file

File	Description
src/analyze/annot_fn.rs	New HIR→chc::Formula translator for #[thrust::formula_fn].
src/analyze.rs	Registers formula functions, caches translated formulas, extracts requires_path/ensures_path, and adds a borrowck-skip query provider for formula fns.
src/analyze/local_def.rs	Threads generic_args through annotation extraction and recognizes path-based requires/ensures.
src/analyze/crate_.rs	Registers #[thrust::formula_fn] items and skips normal analysis for them.
src/analyze/annot.rs	Adds attribute paths for formula_fn, requires_path, ensures_path, and model constructors.
src/analyze/did_cache.rs	Caches DefIds for Mut::new / Box::new model constructors and searches impl items for annotated defs.
src/main.rs	Overrides mir_borrowck to skip borrow-checking formula functions.
src/lib.rs	Exposes the borrowck override hook and adds rustc crate imports needed for query override wiring.
std.rs	Adds operator traits and constructors (Mut::new, Box::new, arithmetic/eq/ord) required by formula function expressions; adjusts extern spec swap to be a tail call.
tests/ui/pass/annot_formula_fn.rs	New passing UI test for requires/ensures via formula_fn + *_path.
tests/ui/fail/annot_formula_fn.rs	New failing UI test (unsat) for requires/ensures via formula_fn + *_path.
tests/ui/pass/annot_formula_fn_mut.rs	New passing UI test for mut-term reasoning via formula_fn.
tests/ui/fail/annot_formula_fn_mut.rs	New failing UI test for mut-term reasoning via formula_fn.
tests/ui/pass/annot_mut_term_formula_fn.rs	New passing UI test for Mut::new usage in ensures formula.
tests/ui/fail/annot_mut_term_formula_fn.rs	New failing UI test variant (unsat).
tests/ui/pass/annot_mut_term_formula_fn_poly.rs	New passing UI test covering generic swap annotated via *_path.
tests/ui/fail/annot_mut_term_formula_fn_poly.rs	New failing UI test variant (unsat).

---

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