fix(mir-importer): preserve non-terminating drops

[YunusMutlu]

What this adds

The importer erases a destructor call when its no-op proof says the destructor does nothing visible. The proof never asked whether the destructor returns, so a Drop that loops forever, or recurses into itself, was deleted and the kernel ran on past it. The proof is now a three-state depth-first walk: a reachable cycle, or a call back into an instance already under proof, fails it and the call stays.

struct LoopingDrop(u8);  impl Drop for LoopingDrop { fn drop(&mut self) { loop {} } }
kernel: store A; { let _g = LoopingDrop(0); } store B;

before: st.global.b32 [%rd1], 0x22222222;  ret;          // B ran, and A was deleted too
after:  st.global.b32 [%rd1], 0x11111111;  bra.uni <self>; // A ran, then the destructor's loop

What we fixed

• LoopingDrop and RecursiveDrop keep their glue call. A reconverging if/else destructor is still proven harmless and erased.
• The drop_glue example asserts the importer's own decision in the pre-opt drop_glue.ll (the glue call present for the diverging probes, absent for the control) and keeps the PTX checks.
• The module doc and the STATUS contract line state the termination rule.

Implementation

• drop_glue.rs: the proof tracks Unseen, InProgress and Proven per block and per instance. A successor that is still InProgress is a back edge; a Proven one is a join. The same rule covers a call back into a destructor already under proof.
• All four call sites of the predicate (the Drop terminator, explicit drop_in_place elision, the collector and device codegen) share it, so there is no copied policy.
• Probes: diverging_cfg_drop_probe, diverging_recursive_drop_probe and the new reconverging_drop_probe, all compile-only, checked by verify-code-shape.sh.

Verification

Checked at 4efe8baf7 (nightly-2026-10-11, RTX 5090):

• ✅ cargo test -p mir-importer --all-targets, clippy and rustdoc with warnings as errors, fmt, the example's fmt and clippy gates, the 18 repository guards and the lock check: clean.
• ✅ Fails before, passes after: the same drop_glue source built with main's backend fails verify-code-shape.sh (no glue call, store A gone); this branch passes on the pre-opt IR and the PTX.
• ✅ cargo oxide run drop_glue: SUCCESS, 8 PASS, memcheck clean. array_for_loop, acyclic diamonds and the assert_unchecked path keep per-kernel identical PTX.
• ✅ Scratch kernels: mutual recursion, a hanging field behind a struct without its own Drop, Option of a hanging type, a loop behind a runtime if, mem::drop, closures and a diamond followed by a loop are all kept.

Caveats

• A zero-sized type with a destructor still hits a pre-existing emit gap (cannot compute in-memory address for dropped place) on both backends. It now fails closed instead of being erased silently. Separate issue.
• The diverging probes are compile-only by design.

Closes #1360.

[copy-pr-bot]

This pull request requires additional validation before any workflows can run on NVIDIA's runners.

Pull request vetters can view their responsibilities here.

Contributors can view more details about this message here.

[nihalpasham]

/ok to test 4efe8ba

[nihalpasham]

Thanks, this is the right fix: the proof was erasing a destructor call it never proved returns, and the one predicate all four call sites share is where the rule belongs. Three small things on top:

• verify-code-shape.sh now asserts the importer's own decision in the pre-opt drop_glue.ll, not only the PTX after opt inlined the glue.
• Added a reconverging if/else destructor as a control that must stay erased, so a regression to "any revisit fails" cannot pass.
• Stated the termination rule in the module doc and the STATUS contract line, with a one-page figure in the compiler chapter.

At 4efe8baf7, same source, two backends on the 5090: main compiles the looping probe to st 0x22222222; ret with the pre-drop store deleted, this branch keeps the call, stores 0x11111111 and spins. mir-importer tests, clippy, rustdoc, the guards and all CI checks passed. That takes care of #1360. A zero-sized Drop type still trips a pre-existing emit gap; I will file that separately.