Add Seq<T> as a model of Vec<T>

[coord-e]

Introduces thrust_models::model::Seq as (Array<Int, T>, Int), equipped with basic sequence operations and concatenation.

https://claude.ai/code/session_01A7nMxM1sJ8wxVJmMvsEvSX

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 5182f5650e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Handle ADT elements in empty sequence arrays

Seq::empty() and Seq::singleton() create ArrayEmpty(elem_sort), and SMT formatting asks Term::default_for(elem_sort) for the const-array value. For element models that lower to datatypes, such as Option<Int>/Result<..> or user enums, this newly added branch panics before the solver runs, so otherwise valid specs like comparing Seq::<Option<Int>>::empty() cannot be checked. Either provide a datatype default or avoid needing a concrete default value for empty arrays.

Useful? React with 👍 / 👎.

[coord-e]

yes this is TODO

[Copilot]

Pull request overview

This PR introduces a new logical sequence model thrust_models::model::Seq<T> (represented as (Array<Int, T>, Int)) and uses it as the underlying model for Rust Vec<T>, adding core sequence operations (empty/singleton/len/push/concat) plus SMT encoding support and UI tests.

Changes:

• Add Seq<T> model definitions and switch Vec<T>’s model type to Seq<T> in std.rs.
• Extend the CHC term language + SMT-LIB2 backend to support empty arrays and array concatenation (including a concat-recursive helper function).
• Add UI pass/fail tests covering Seq basics, concat properties, and Vec specs expressed via the Seq model.

Reviewed changes

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

Show a summary per file

File	Description
std.rs	Defines model::Seq<T> and maps Vec<T>’s model to Seq, updating extern specs accordingly.
src/chc.rs	Adds ArrayEmpty/ArrayConcat term forms, ite, and select peephole rewrites for concat.
src/chc/smtlib2.rs	Prints SMT for ArrayEmpty and ArrayConcat; emits per-element-sort seq_concat_arr recursion.
src/chc/format_context.rs	Tracks array element sorts to decide which seq_concat_arr helpers to emit.
src/chc/unbox.rs	Extends unboxing pass to traverse/transform new array terms.
src/rty.rs	Substitutes type params through the new CHC term variants.
src/annot.rs	Tightens Resolver output bound to Clone to support term construction needs.
src/analyze/did_cache.rs	Adds DefId caching for seq_* annotated defs.
src/analyze/annot.rs	Adds attribute-path helpers for seq_* annotations.
src/analyze/annot_fn.rs	Translates Seq operations and indexing into CHC terms (incl. concat -> ArrayConcat).
tests/ui/pass/seq_basic.rs	Pass test for empty/singleton/len/push/index properties.
tests/ui/pass/seq_concat.rs	Pass test for concat length property.
tests/ui/pass/seq_concat_index.rs	Pass test for left-side index behavior under concat.
tests/ui/pass/seq_concat_const.rs	Pass test for concat identity with empty.
tests/ui/pass/seq_specs_vec_build.rs	Pass test showing Vec can be specified using Seq model structure/ops.
tests/ui/fail/seq_basic.rs	Fail test with intentionally wrong push length spec.
tests/ui/fail/seq_concat.rs	Fail test with intentionally wrong concat length spec.
tests/ui/fail/seq_concat_index.rs	Fail test with intentionally wrong concat index spec.
tests/ui/fail/seq_concat_const.rs	Fail test with intentionally wrong concat identity spec.
tests/ui/fail/seq_specs_vec_build.rs	Fail test with intentionally wrong Vec element spec via Seq.

---

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