Fix enum-drop of aggregate mutable-reference fields

[coord-e]

Bug

Dropping a value whose enum variant holds an aggregate of mutable references panics in refine/env.rs with assert!(assumption_existentials.is_empty()). Minimum repro (panics on current main during CHC generation):

enum Pair<'a> {
    Two((&'a mut i32, &'a mut i32)),
    None,
}

#[thrust::callable]
fn check(a: &mut i32, b: &mut i32) {
    let _p = Pair::Two((a, b)); // constructed and dropped — that's all it takes
}

fn main() {}

The same shape arises naturally from split_first_mut, whose Option<(&mut T, &mut [T])> return value hits this panic when dropped.

Cause

The enum-drop path in dropping_assumption built each field's drop assumption by re-deriving it through a fresh Path::PlaceTy. But projecting an aggregate field (PlaceType::tuple_proj / deref) allocates fresh existentials via subsume_rty, so the recursive call returns an assumption whose existentials the caller never merges — the assert guarded a case the code simply didn't handle. (A field that is directly &mut T produces no new existentials, which is why only aggregate fields trip it.)

Fix

Rewrite dropping_assumption around a structural drop_prophecy helper that walks the type once:

• tuple elements and box targets are threaded as term expressions over the value (tuple_proj / box_current), so a nested sub-value stays shared across all the mutable references it contains and needs no fresh existentials;
• only enum fields allocate existentials (they cannot be projected without a selector), and they go into a single shared namespace tied back to the value with the matcher predicate.

This resolves every packed prophecy to identity correctly. The now-dead Path::PlaceTy variant and Path::{deref,tuple_proj} helpers are removed.

Verification

• The repro above no longer panics.
• New regression tests tests/ui/{pass,fail}/enum_tuple_mut_drop.rs: the pass variant verifies drop resolves both prophecies to identity (sat), the fail variant confirms the encoding is not vacuous (*a == 11 is rejected as Unsat).
• Full tests/ui suite compared against main: identical results everywhere else (the only failures in my environment are the docker-dependent pcsat tests, equally failing on main).

Note: this is the standalone extraction of the fix from d44c6b8; the tests/lambda-chc fixture changes in that commit depend on other unmerged work and are intentionally not included here.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QmZGoGNQRhg6aZsGhhSaDF

---

Generated by Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: bf84002f41

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

[chatgpt-codex-connector]

Preserve nested refinements during drop

When the dropped value has a refined aggregate element (for example a generic enum or tuple element whose type argument is {v: &mut i64 | ...}), this recurses on only elem.ty and never substitutes term.tuple_proj(i) for the element's Value in elem.refinement. The previous path_type(...).tuple_proj() path went through subsume_rty, which added those nested refinements before emitting the prophecy-equality constraints. Dropping such an aggregate now produces a weaker CHC clause and can accept bad postconditions whenever the refined field is dropped without being projected elsewhere.

Useful? React with 👍 / 👎.