Implement more expressions in formula_fn

[coord-e]

follow-up of #65
extracted from #57

[Copilot]

Pull request overview

Follow-up to #65/#57 to expand the set of Rust expressions supported inside #[thrust::formula_fn], primarily around array operations and additional term constructors.

Changes:

• Add Array indexing and Array::store model definitions and wire up DefId lookup for array_store.
• Extend AnnotFnTranslator to translate &expr, *expr on shared refs, array[index], array.store(i, v), and struct constructors.
• Adjust the injected model Vec representation (length uses Int) and add missing Model impl for model::Array.

Reviewed changes

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

File	Description
std.rs	Adds Array indexing + store model hooks; tweaks model Vec and adds Model for model::Array.
src/analyze/did_cache.rs	Caches the DefId for the #[thrust::def::array_store]-annotated method.
src/analyze/annot_fn.rs	Implements new HIR-to-CHC translations for index/method-call/address-of/deref and struct ctors.
src/analyze/annot.rs	Adds the attribute path helper for thrust::def::array_store.

---

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