Key basic block types by generic args as well as def id

[coord-e]

Fixes #328.

A generic function is analyzed once per instantiation, but its basic-block types were stored under LocalDefId alone. When one instantiation was analyzed from inside another (for example, g::<i32>'s body calls g::<i64>), the nested run overwrote the outer run's block entries. The outer analysis then carried on with the inner instantiation's block types and predicate variables. Depending on the CFG, this either panicked with precondition is already registered for basic block or, with no error, verified the outer instantiation against the inner one's behaviour. In the second case, a panicking program verified as safe.

Changes

• Added LocalDefInstantiation, which pairs a LocalDefId with the GenericArgsRef it is instantiated with.
• Analyzer::basic_blocks is now keyed by LocalDefInstantiation. The register and lookup methods take one instead of a bare LocalDefId.
• basic_block::Analyzer holds the LocalDefInstantiation it analyzes, which local_def::Analyzer builds from its local_def_id and generic_args.
• Added the fn_poly_nested_instantiation.rs pass/fail UI test pair, built from the issue's reproducer. On main both files get the wrong verdict (pass → Unsat, fail → safe).

Validation

• cargo test: all 396 UI tests pass, run with the pinned Z3 5.0.0 and PCSat wrapper.
• cargo clippy -- -D warnings and cargo fmt --all -- --check are clean.
• The crash reproducer from the issue (W<W<i32>> delegating trait impl) now verifies, and its broken variant is rejected.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Q3Dt425cRNNW8aSShzGyDA

[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-13T02:15:45.294089Z	604ae4e	New commits

ℹ️ 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.

[Copilot]

🟢 Approval recommended

The implementation consistently isolates per-instantiation block state and includes a focused bidirectional regression test.

0 open findings

What changed in this PR

Keys basic-block analysis state by both definition and generic arguments, preventing nested generic instantiations from corrupting each other.

Changes:

• Introduces LocalDefInstantiation and threads it through analysis.
• Keys basic-block types by full instantiation.
• Adds pass/fail regression tests for nested polymorphic calls.

File	Description
src/​analyze.rs	Adds instantiation-aware basic-block storage APIs.
src/​analyze/​local_def.rs	Supplies generic instantiation keys during analysis.
src/​analyze/​basic_block.rs	Uses instantiation keys for block lookups and registration.
tests/​ui/​pass/​fn_poly_nested_instantiation.rs	Verifies the correct nested-instantiation result.
tests/​ui/​fail/​fn_poly_nested_instantiation.rs	Rejects the incorrect result.

🧠 Review effort: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.