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

[chatgpt-codex-connector]

Handle model deref in named field access

When a spec uses Rust's valid auto-deref field syntax on a mutable model reference, for example #[requires(s.length > 0)] fn f(s: &mut [T]), the receiver expression has type model::Mut<Seq<_>>, not a Rust reference, so peel_refs() leaves the Mut ADT and this path reports unknown named field in formula. Since this change makes Seq::length a public named field, specs for &mut Vec/&mut [T] can now hit this ICE unless users spell (*s).length; the translator needs to follow the model Deref/use mut_current before resolving the field, or reject the syntax without panicking.

Useful? React with 👍 / 👎.