Fix enum-drop of aggregate mutable-reference fields (#167)

* Fix enum-drop of aggregate mutable-reference fields

Dropping a value whose enum variant holds an aggregate of mutable
references (e.g. `Pair::Two((&mut i32, &mut i32))`, or the
`Option<(&mut T, &mut [T])>` returned by `split_first_mut`) panicked in
`refine/env.rs` with `assert!(assumption_existentials.is_empty())`. The
enum-drop path built each field's drop assumption by re-deriving it
through a fresh `Path`, but projecting an aggregate field
(`PlaceType::tuple_proj`/`deref`) allocates fresh existentials, so the
recursive call returned an assumption with existentials the assert
never expected. Minimum repro:

    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));
    }

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QmZGoGNQRhg6aZsGhhSaDF

* fixup! Fix enum-drop of aggregate mutable-reference fields

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: coord-e

src/refine/env.rs

@@ -1050,7 +1050,6 @@ where
 
 #[derive(Debug, Clone)]
 enum Path {
-    PlaceTy(Box<PlaceType>),
     Local(Local),
     Deref(Box<Path>),
     TupleProj(Box<Path>, usize),
@@ -1079,23 +1078,12 @@ impl<'tcx> From<Place<'tcx>> for Path {
     }
 }
 
-impl Path {
-    fn deref(self) -> Self {
-        Path::Deref(Box::new(self))
-    }
-
-    fn tuple_proj(self, idx: usize) -> Self {
-        Path::TupleProj(Box::new(self), idx)
-    }
-}
-
 impl<T> Env<T>
 where
     T: EnumDefProvider,
 {
     fn path_type(&self, path: &Path) -> PlaceType {
         match path {
-            Path::PlaceTy(pty) => *pty.clone(),
             Path::Local(local) => self.local_type(*local),
             Path::Deref(path) => self.path_type(path).deref(),
             Path::TupleProj(path, idx) => self.path_type(path).tuple_proj(*idx),
@@ -1111,81 +1099,73 @@ where
     }
 
     fn dropping_assumption(&mut self, path: &Path) -> Assumption {
-        let ty = self.path_type(path);
-        if ty.ty.is_mut() {
-            let mut builder = PlaceTypeBuilder::default();
-            let (_, term) = builder.subsume(ty);
-            builder.push_formula(term.clone().mut_final().equal_to(term.mut_current()));
-            builder.build_assumption()
-        } else if ty.ty.is_own() {
-            self.dropping_assumption(&path.clone().deref())
-        } else if let Some(tty) = ty.ty.as_tuple() {
-            (0..tty.elems.len())
-                .map(|i| self.dropping_assumption(&path.clone().tuple_proj(i)))
-                .collect()
-        } else if let Some(ety) = ty.ty.as_enum() {
+        let PlaceType {
+            ty,
+            mut existentials,
+            term,
+            mut formula,
+        } = self.path_type(path);
+        formula.push_conj(self.dropping_formula_for_term(&mut existentials, &ty, term));
+        Assumption::new(existentials, formula)
+    }
+
+    fn dropping_formula_for_term(
+        &self,
+        existentials: &mut IndexVec<rty::ExistentialVarIdx, chc::Sort>,
+        ty: &rty::Type<Var>,
+        term: chc::Term<PlaceTypeVar>,
+    ) -> chc::Body<PlaceTypeVar> {
+        if ty.is_mut() {
+            term.clone().mut_final().equal_to(term.mut_current()).into()
+        } else if ty.is_own() {
+            let inner = &ty.as_pointer().unwrap().elem.ty;
+            self.dropping_formula_for_term(existentials, inner, term.box_current())
+        } else if let Some(tty) = ty.as_tuple() {
+            let mut body = chc::Body::default();
+            for (i, elem) in tty.elems.iter().enumerate() {
+                body.push_conj(self.dropping_formula_for_term(
+                    existentials,
+                    &elem.ty,
+                    term.clone().tuple_proj(i),
+                ));
+            }
+            body
+        } else if let Some(ety) = ty.as_enum() {
+            let mut body = chc::Body::default();
+
             let enum_def = self.enum_defs.enum_def(&ety.symbol);
             let matcher_pred = chc::MatcherPred::new(ety.symbol.clone(), ety.arg_sorts());
 
-            let PlaceType {
-                ty: _,
-                mut existentials,
-                term,
-                mut formula,
-            } = ty;
-
             let mut pred_args = vec![];
             for field_ty in enum_def.field_tys() {
                 let mut field_rty = rty::RefinedType::unrefined(field_ty.clone().vacuous());
                 field_rty.instantiate_ty_params(ety.args.clone());
+                let field_type = field_rty.ty;
 
-                let ev = existentials.push(field_rty.ty.to_sort());
-                pred_args.push(chc::Term::var(ev.into()));
+                let ev = existentials.push(field_type.to_sort());
+                let field_term = chc::Term::var(ev.into());
+                pred_args.push(field_term.clone());
 
-                if let Some(p) = field_rty.ty.as_pointer() {
+                if let Some(p) = field_type.as_pointer() {
                     if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
                         // TODO: we need recursively defined drop_pred for the recursive ADTs!
                         tracing::warn!("skipping recursive variant");
                         continue;
                     }
                 }
 
-                let field_pty = {
-                    let rty::RefinedType {
-                        ty: field_ty,
-                        refinement,
-                    } = field_rty;
-                    let rty::Refinement { body, existentials } = refinement;
-                    PlaceType {
-                        ty: field_ty,
-                        existentials,
-                        term: chc::Term::var(ev.into()),
-                        formula: body.map_var(|v| match v {
-                            rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(ev),
-                            rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v),
-                            // TODO: (but otherwise we can't distinguish field existentials from them...)
-                            rty::RefinedTypeVar::Existential(_) => {
-                                panic!("cannot handle existentials in field_rty")
-                            }
-                        }),
-                    }
-                };
-
-                let Assumption {
-                    existentials: assumption_existentials,
-                    body: assumption_body,
-                } = self.dropping_assumption(&Path::PlaceTy(Box::new(field_pty)));
-                // dropping assumption should not generate any existential
-                assert!(assumption_existentials.is_empty());
-                formula.push_conj(assumption_body);
+                body.push_conj(self.dropping_formula_for_term(
+                    existentials,
+                    &field_type,
+                    field_term,
+                ));
             }
 
             pred_args.push(term);
-            formula.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
-
-            Assumption::new(existentials, formula)
+            body.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
+            body
         } else {
-            Assumption::default()
+            chc::Body::default()
         }
     }
 

tests/ui/fail/enum_tuple_mut_drop.rs

@@ -0,0 +1,21 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[allow(dead_code)]
+enum Pair<'a> {
+    Two((&'a mut i32, &'a mut i32)),
+    None,
+}
+
+#[thrust::callable]
+fn check(a: &mut i32, b: &mut i32) {
+    *a = 10;
+    *b = 20;
+    {
+        let _p = Pair::Two((a, b));
+    }
+    // wrong: `*a` is 10, not 11
+    assert!(*a == 11);
+}
+
+fn main() {}

tests/ui/pass/enum_tuple_mut_drop.rs

@@ -0,0 +1,23 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+#[allow(dead_code)]
+enum Pair<'a> {
+    Two((&'a mut i32, &'a mut i32)),
+    None,
+}
+
+#[thrust::callable]
+fn check(a: &mut i32, b: &mut i32) {
+    *a = 10;
+    *b = 20;
+    {
+        // Construct and drop the enum without mutating through the packed references.
+        let _p = Pair::Two((a, b));
+    }
+    // Dropping resolves both prophecies to identity, so the values are unchanged.
+    assert!(*a == 10);
+    assert!(*b == 20);
+}
+
+fn main() {}