Unelaborate the Box deref temps GVN rewrites into copies

[coord-e]

ElaborateBoxDerefs lowers *boxed into a Unique/NonNull/Transmute chain, and Derefer hoists the base of that chain into a deref temp. That temp is what unelaborate_derefs recognizes by its CopyForDeref rvalue, so that the deref below it is analyzed on the place the box lives in rather than on the temp.

From -C opt-level=1 upward, GVN rewrites _t = deref_copy P into _t = copy P. The temp then survived unelaboration and the chain was resolved against it instead of against P. A Box is modeled by value, so the temp took a copy of the box's contents: the write landed on the copy while P kept its pre-write value, and every later read of P saw the stale one. A Box behind one more projection — a struct field, a tuple element, an enum payload, a nested Box — was thus verified against the wrong value, silently in both directions: a program whose assertion is false at run time verified as safe, and one whose assertion holds was rejected with Unsat.

Match the rewritten shape too, for the locals an ElaborateBoxDerefs chain dereferences as a whole. Those are exactly the deref temps: a chain reads its base through Unique/NonNull field projections, which no local other than a hoisted temp stands in for. Operand::Move stays untouched — that is a real ownership transfer — and so does a box copy that no chain dereferences.

Fixes #244

Verification

All with -Adead_code -C debug-assertions=false, at every level 0, 1, 2, 3, s, z:

program	before	after
tuple, assert!(*t.0 == 1) — false	Unsat at 0, safe at 1..z	Unsat everywhere
struct field, assert!(*s.b == 1) — false	Unsat at 0, safe at 1..z	Unsat everywhere
nested box, assert!(**x == 1) — false	Unsat at 0, safe at 1..z	Unsat everywhere
the true-assertion counterparts	safe at 0, Unsat at 1..z	safe everywhere
tests/ui/pass/box_nested.rs	safe at 0, Unsat at 1..z	safe everywhere
single Box local	safe everywhere	unchanged

tests/ui/{pass,fail}/box_field_optimized.rs pin the struct-field shape at -C opt-level=1; both fail on main and pass here. The full suite is green (328 tests).

A sweep of all 166 tests/ui/pass files at -C opt-level=1 differs in exactly two lines, box_field_optimized.rs and box_nested.rs, both Unsat → ok. The 44 files that already fail at that level on main — 42 ICEs, plus the ghost_field.rs regression the issue notes — behave identically.

Left alone

• The &mut Box<i64> parameter shape is fixed at 1, s and z, but at 2/3 it still reaches the pre-existing src/refine/env.rs:399 unwrap the issue mentions.
• The enum-payload shape turns from a wrong answer into a panic. With the temp unelaborated the write becomes a direct &mut ((_1 as A).0), GVN having removed the reference indirection, and Env::borrow_var has no flow binding for that place: borrowing unbound var at src/refine/env.rs:1014. That is a separate gap in borrowing an enum payload place, and per CLAUDE.md the ICE path is left as it is rather than worked around.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YXdyimRB3Fpje8fbfmqhiB

---

Generated by Claude Code