Repository navigation
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".
| PatKind::TupleStruct(_, subpats, dotdot_pos) | PatKind::Tuple(subpats, dotdot_pos) => { | ||
| let pat_ty = self.pat_ty(pat); | ||
| let field_count = match pat_ty.ty_adt_def() { | ||
| Some(adt) => adt.non_enum_variant().fields.len(), |
There was a problem hiding this comment.
When an annotated function uses an irrefutable tuple-style enum pattern, such as a single-variant enum E { V(i32) } with fn f(E::V(_): E), the generated formula function preserves that parameter pattern and reaches this branch. Its pattern type returns the enum AdtDef, but non_enum_variant() is only valid for structs/unions and panics for enums, so translating even a trivial requires(true) now ICEs despite no .. being present. Resolve the tuple-struct pattern's matched variant and count that variant's fields instead.
Useful? React with 👍 / 👎.
This branch has not been deployed
2 participants
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