Give the Seq model named array and length fields

[coord-e]

Summary

This is PR 1 of 4 in a restructuring of #153 into reviewable steps.

Replace the positional Seq<T>(Array<Int, T>, Int) tuple struct with a named-field struct Seq { array, length }, and refer to the fields by name (.array / .length) throughout the extern specs and tests instead of .0 / .1.

Details

• Struct literals are now supported in specification formulas: an ExprKind::Struct is lowered to a tuple with fields placed at their declaration position, mirroring how struct field access already resolves named fields to positions.
• Named field access does not auto-deref. The old positional .0 / .1 access only worked through references incidentally (via unboxing), so dereferences through & / &mut receivers are now written explicitly in the annotations, e.g. (*slice).length.

Validation

• cargo build, cargo fmt --all -- --check, cargo clippy -- -D warnings
• cargo test — all Spacer-backed UI tests and the reconstruction unit tests pass. (The PCSat-backed tests were not run in this environment as they require the CoAR Docker image.)

Stack

1. this PR — named fields
2. concat_int_array takes sequence tuples
3. offset field
4. subsequence + split_first/split_last(_mut)

🤖 Generated with Claude Code

https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit:84a3441e3b

ℹ️ 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".

[Copilot]

Pull request overview

This PR is the first step in a larger refactor to replace the positional Seq<T>(Array<Int, T>, Int) tuple model with a named-field Seq { array, length }, updating extern specs and UI tests accordingly and adding support for struct literals in specification formulas.

Changes:

• Convert the Seq model definition from a tuple struct to a named-field struct (array, length).
• Update extern specs and UI tests to use .array / .length instead of .0 / .1 (with explicit * where needed).
• Lower ExprKind::Struct specification formulas into tuple terms in declaration order.

Reviewed changes

Copilot reviewed 18 out of 18 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/ui/pass/slice_methods.rs	Update slice spec assertions to use array/length named fields (explicit deref).
tests/ui/pass/slice_methods_mut.rs	Update mut slice spec assertions to use array/length.
tests/ui/pass/slice_last_mut.rs	Update last-element spec assertions to use array/length.
tests/ui/pass/slice_index.rs	Update indexing spec assertions to use array/length.
tests/ui/pass/slice_index_mut.rs	Update mut indexing spec assertions to use array/length.
tests/ui/pass/slice_first_mut.rs	Update first-element spec assertions to use array/length.
tests/ui/pass/seq_specs_vec_build.rs	Update Vec build spec to compare against result.array/result.length.
tests/ui/pass/loop_invariant_fn_param_at_entry.rs	Update invariant/spec to use .length field access.
tests/ui/fail/slice_methods.rs	Update failing slice spec to use array/length named fields.
tests/ui/fail/slice_methods_mut.rs	Update failing mut slice spec to use array/length.
tests/ui/fail/slice_last_mut.rs	Update failing last-element spec to use array/length.
tests/ui/fail/slice_index.rs	Update failing indexing spec to use array/length.
tests/ui/fail/slice_index_mut.rs	Update failing mut indexing spec to use array/length.
tests/ui/fail/slice_first_mut.rs	Update failing first-element spec to use array/length.
tests/ui/fail/seq_specs_vec_build.rs	Update failing Vec build spec to use array/length.
tests/ui/fail/loop_invariant_fn_param_at_entry.rs	Update failing invariant/spec to use .length field access.
std.rs	Redefine Seq with named fields and update Vec/slice extern specs to refer to them.
src/analyze/annot_fn.rs	Add lowering for struct literals in spec formulas (ExprKind::Struct).

---

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