From 9b225a65903c6e76ba27a10358ac209837b7b9e4 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 6 Oct 2026 21:51:43 +0000
Subject: [PATCH] Adjust field indices past `..` in spec parameter patterns

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
---
 src/analyze/annot_fn.rs                   | 10 ++++++++--
 tests/ui/fail/annot_param_rest_pattern.rs | 12 ++++++++++++
 tests/ui/pass/annot_param_rest_pattern.rs | 12 ++++++++++++
 3 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 tests/ui/fail/annot_param_rest_pattern.rs
 create mode 100644 tests/ui/pass/annot_param_rest_pattern.rs

diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 23218e26..55b7ebb9 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -1,6 +1,7 @@
 use std::collections::HashMap;
 
 use pretty::{termcolor, Pretty};
+use rustc_hir::pat_util::EnumerateAndAdjustIterator as _;
 use rustc_hir::{def_id::LocalDefId, HirId};
 use rustc_index::IndexVec;
 use rustc_middle::mir;
@@ -377,8 +378,13 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
             PatKind::Binding(_, hir_id, _, None) => {
                 self.env.insert(hir_id, param);
             }
-            PatKind::TupleStruct(_, subpats, _) | PatKind::Tuple(subpats, _) => {
-                for (idx, subpat) in subpats.iter().enumerate() {
+            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(),
+                    None => pat_ty.tuple_fields().len(),
+                };
+                for (idx, subpat) in subpats.iter().enumerate_and_adjust(field_count, dotdot_pos) {
                     let field_term = param.clone().tuple_proj(idx);
                     self.build_env_from_pat(field_term, subpat);
                 }
diff --git a/tests/ui/fail/annot_param_rest_pattern.rs b/tests/ui/fail/annot_param_rest_pattern.rs
new file mode 100644
index 00000000..73a04d15
--- /dev/null
+++ b/tests/ui/fail/annot_param_rest_pattern.rs
@@ -0,0 +1,12 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == d)]
+fn last((_a, .., _c, d): (i64, i64, i64, i64)) -> i64 {
+    _c
+}
+
+fn main() {
+    last((1, 2, 3, 4));
+}
diff --git a/tests/ui/pass/annot_param_rest_pattern.rs b/tests/ui/pass/annot_param_rest_pattern.rs
new file mode 100644
index 00000000..67722382
--- /dev/null
+++ b/tests/ui/pass/annot_param_rest_pattern.rs
@@ -0,0 +1,12 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == d)]
+fn last((_a, .., _c, d): (i64, i64, i64, i64)) -> i64 {
+    d
+}
+
+fn main() {
+    last((1, 2, 3, 4));
+}