Rewrite slice index uses past the bounds check's target block

[coord-e]

Fixes #322.

Slice index reconstruction used to rewrite the indexed place (*slice)[index] only in the bounds check's target block. MIR also uses that place in later blocks of the same expression:

• the inner bounds check of grid[i][j] re-reads grid[i] in its own target;
• with -C overflow-checks=on, s[i] += 1 writes s[i] in the target of the overflow assert.

The leftover Index projection then panicked in Path::from / elaborate_place_for_borrow. In the += case, the only use the pass saw was the read, so it chose Index::index even though the expression writes.

Changes

• blocks_using_indexed_place follows the blocks entered only from the target (the same single-predecessor condition the pass already asserts for the target). It stops at the next bounds check on the same slice and index, because that check starts a separate indexing expression; at opt-level >= 1 GVN reuses the index local across statements.
• checks_slice_within keeps the inner check of grid[i][i] from counting as that stopping point: the inner check uses the same index local, but its length is read through the indexed place.
• IndexedPlaceFinder now ORs the mutability over every use of the found place, and replace_indexed_place rewrites all of the access's blocks.

Tests

• slice_index_nested (pass/fail): grid[i][i] on &[&[i64]]. This is the nested case and the same-index-local stop rule.
• slice_index_add_assign_overflow_checked (pass/fail): s[i] += 1 with -C overflow-checks=on. This checks that uses are rewritten across the overflow assert and that index_mut is selected.

cargo test passes locally (396 UI tests plus unit tests) with Z3 5.0.0 and the pinned PCSat wrapper. cargo fmt --check and cargo clippy --all-targets are clean.

Remaining limitation (not touched here): grid[i][j] = 0 on &mut [&mut [i64]] no longer panics, but a caller that reads the row back afterwards is still rejected. The rows are &mut stored in a Seq, whose prophecy is never resolved (#202).

🤖 Generated with Claude Code

https://claude.ai/code/session_019sxU2nknAtpn8CJu7xZeQt

---

Generated by Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-04T21:46:11.034582Z	cc491d6	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.