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 👍 / 👎.

[coord-e]

The behavioral difference is real — element refinements are no longer lowered into the drop assumption — but the claimed impact direction is inverted, so I'm leaving the code as is.

Drop assumptions are emitted into the body (premise side) of CHC clauses, with their existentials becoming fresh clause variables (see Env::clause_builder in refine/env.rs). Omitting true conjuncts from a premise makes the clause stronger, i.e. the verifier strictly more conservative: the worst case is a spurious rejection of a safe program, never accepting a bad postcondition. Consistent with that, the full tests/ui suite keeps identical verdicts to main.

Restoring the old behavior for enum fields would actually reintroduce a latent unsoundness hazard: matcher_pred(x0, v) is a disjunction over variants, so refinement(x0) would be asserted unconditionally even when the runtime value is a fieldless variant (e.g. None). If an instantiated field refinement is uninhabited, the premise becomes unsatisfiable and everything after the drop is treated as unreachable — a genuine "accept bad programs" failure mode. (The old path never robustly handled refined fields anyway: it panicked with cannot handle existentials in field_rty.) The prophecy-identity constraints kept by this PR are always satisfiable, so no such vacuity can arise.

For tuple elements and box targets the refinements are unconditionally justified, so threading them back is safe — happy to do that as a follow-up if a concrete completeness regression shows up.

---

Generated by Claude Code

[Copilot]

Pull request overview

Fixes a CHC-generation panic when dropping enums whose variants contain aggregates (e.g., tuples) of &mut references, by restructuring drop-assumption construction to avoid introducing unmerged existentials during structural projections.

Changes:

• Refactors dropping_assumption to build a single Assumption via a structural dropping_formula_for_term walker (threading tuple/box projections as term expressions).
• Removes the now-dead Path::PlaceTy variant and related Path helper methods.
• Adds UI regression tests covering the enum-of-tuple-of-&mut drop case (both SAT and expected-Unsat).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
src/refine/env.rs	Reworks drop-assumption construction to avoid fresh existentials from structural projections and fixes the enum-drop panic.
tests/ui/pass/enum_tuple_mut_drop.rs	New passing regression test ensuring enum drop resolves packed prophecies to identity (no mutation observed).
tests/ui/fail/enum_tuple_mut_drop.rs	New failing companion test ensuring the encoding is non-vacuous (rejects *a == 11 as Unsat).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.