Support some of std::vec::Vec methods

[coord-e]

• Add array type/sort that corresponds to the theory of arrays in spacer
• Support store/select calls in annotations
• Adjust some behavior in trait resolution
• Model Vec as (Array<int, T>, int) and add extern_spec_fns

[Copilot]

Pull request overview

Adds first-class CHC array support and uses it to model Vec<T> as (Array<int, T>, int), enabling specifications for common Vec operations and extending annotation parsing to support select/store.

Changes:

• Introduce Array sort/type across CHC + refined types, including formatting/unboxing/subtyping support.
• Model Vec<T> as a tuple (Array<int, T>, int) and add extern_spec_fn specs for several Vec methods.
• Extend annotation parsing to accept postfix .select(i) / .store(i, v) terms; add UI tests for Vec.

Reviewed changes

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

Show a summary per file

File	Description
std.rs	Adds extern_spec_fn contracts for Vec::{new,push,len,index,index_mut,clear,pop,is_empty,truncate} using store/select.
src/rty.rs	Adds ArrayType and Type::Array, including sort mapping and substitutions/unification.
src/rty/subtyping.rs	Adds subtyping relation for array refined types.
src/refine/template.rs	Lowers Rust Vec<T> to (Array<int, T>, int) in type building.
src/chc.rs	Adds Sort::Array, array pretty-printing, store/select functions, and Term::{select,store} helpers.
src/chc/unbox.rs	Unboxing support for array sorts.
src/chc/format_context.rs	Adjusts sort symbol formatting and adds SMT-LIB formatting for (Array ...).
src/chc/hoice.rs	Updates to renamed SortSymbol helper for datatype reference collection.
src/annot.rs	Extends postfix parsing to support .select(..) / .store(..) and adds UnknownMethod error.
src/analyze/local_def.rs	Resolves extern_spec_fn inner def_id via Instance::resolve.
src/analyze/basic_block.rs	Improves const handling for uints; resolves const_fn_def instances with args.
tests/ui/pass/vec_1.rs	Pass test for Vec::new/push/len/index.
tests/ui/pass/vec_2.rs	Pass test for IndexMut + pop.
tests/ui/pass/vec_3.rs	Pass test for truncate/clear.
tests/ui/fail/vec_1.rs	Fail test for incorrect len after push.
tests/ui/fail/vec_2.rs	Fail test for incorrect second pop result.
tests/ui/fail/vec_3.rs	Fail test for incorrect len/index after truncate/clear.

---

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