Repository navigation
Adjust field indices past .. in spec parameter patterns - #326
Conversation
build_env_from_pat enumerated a tuple or tuple-struct pattern's sub-patterns directly, ignoring its `..` rest, so every binding after the rest was bound to the wrong field in requires/ensures: in `(a, .., c): (i64, i64, i64)`, the spec's `c` denoted field 1. Shift the indices past the rest with rustc's enumerate_and_adjust, as rustc's own pattern lowering does. Fixes #325 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014QLtzjY5sB9iS1pK4nJixa
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9b225a6590
ℹ️ 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".
There was a problem hiding this comment.
🟡 Changes recommended
Tuple-enum patterns can panic during field counting, and the tuple-struct path lacks regression coverage.
2 open findings
What changed in this PR
Fixes annotation bindings after .. in tuple and tuple-struct parameter patterns.
Changes:
- Adjusts projected field indices using rustc’s pattern helper.
- Adds paired pass/fail UI regression tests.
| File | Description |
|---|---|
src/analyze/annot_fn.rs |
Corrects field-index calculation after rest patterns. |
tests/ui/pass/annot_param_rest_pattern.rs |
Adds the valid regression case. |
tests/ui/fail/annot_param_rest_pattern.rs |
Adds the invalid regression case. |
🧠 Review effort: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| let pat_ty = self.pat_ty(pat); | ||
| let field_count = match pat_ty.ty_adt_def() { | ||
| Some(adt) => adt.non_enum_variant().fields.len(), | ||
| None => pat_ty.tuple_fields().len(), | ||
| }; |
|
|
||
| #[thrust_macros::requires(true)] | ||
| #[thrust_macros::ensures(result == d)] | ||
| fn last((_a, .., _c, d): (i64, i64, i64, i64)) -> i64 { |
Fixes #325.
AnnotFnTranslator::build_env_from_patbound a tuple or tuple-struct parameter pattern's sub-patterns with a plainenumerate()and ignored the pattern's..rest. As a result, every binding after the rest referred to the wrong field inrequires/ensures. For example, in(a, .., c): (i64, i64, i64)the spec'scwastuple_proj(1). A#[thrust::trusted]spec was then assumed about the wrong field, which made panicking programs verify assafe. Correct programs were also rejected.This change shifts the indices past the rest with
rustc_hir::pat_util::EnumerateAndAdjustIterator::enumerate_and_adjust, the helper rustc's own pattern handling uses. The field count comes from the pattern's type.Tests
tests/ui/{pass,fail}/annot_param_rest_pattern.rsdestructure(_a, .., _c, d)and stateensures(result == d). The two files differ only in the body (dvs_c). Before this change, the pair fails in both directions:passis rejected withUnsat, andfailverifies because the spec'sdwas mapped to the body's_c.cargo fmt --check,cargo clippy -- -D warnings, andcargo test(396 UI tests, with PCSat) all pass locally.🤖 Generated with Claude Code
https://claude.ai/code/session_014QLtzjY5sB9iS1pK4nJixa
Generated by Claude Code