repsel Phase 5a: the `delete` shape barrier is module-scoped, but a proven-`this` receiver is aliased across modules by construction

[proggeramlug]

Noticed while establishing the soundness envelope for #7141 / #7142. Not
introduced by either — this is about the Phase 5a mechanism as shipped in
#6925. Filing because the reasoning that makes the freeze family a module-wide
kill applies verbatim to delete, and was not carried over.

The asymmetry

collectors/proven_this.rs documents that a proven this differs from a
Phase 3b local in exactly one way that matters: the receiver is owned by the
caller and aliased by construction, so the analysis cannot enumerate stores to
it (collectors/proven_this.rs:41-45). That is why the phase added a separate
module-wide freeze_barrier_sites kill for write-containing clones — a Phase 3b
local needs no such kill because containment bounds its aliases, and a proven
this does.

delete has the same property and did not get the same treatment. It is in
expr_is_shape_barrier (collectors/ptr_shape.rs:163-166 — Expr::Delete,
Expr::ReflectDelete), and method_proven_this does consult
has_shape_barrier_sites(). But that fact is computed per module:

pub fn collect_module_dispatch_facts(hir: &Module) -> ModuleDispatchFacts

(collectors/scalar_method_dispatch.rs:181)

So delete inst.declaredField in module B sets no barrier flag in module A, and
module A's __pshape clone keeps its bare fixed-slot loads.

Why that is not merely theoretical

delete is the only operation that relocates a declared field's packed slot
index. js_object_delete_field reaches the keys-scan/compaction path for any
GC_TYPE_OBJECT with a keys array — which is what
js_object_alloc_class_inline_keys installs for class instances
(crates/perry-runtime/src/object/alloc.rs:275) — with no class-instance
tombstone branch (delete_rest.rs:291-344; field_count recomputed at :380).
On class C { a; b; c }, delete inst.b moves c from slot 2 to slot 1 and
leaves class_id untouched. A clone compiled against the pre-delete indices
then reads the wrong field.

What currently prevents it

Both shipped routing sites are protected by something other than the barrier
scan:

• method_direct.fast — dominated by the class-id + keys-token guard, and
  the keys array pointer changes on compaction.
• the Phase 3b Ptr<Shape> receiver arm — dominated by containment, which
  bounds every alias to one function, so no other module can hold the object.

So this may well be unreachable today. But it is unreachable by accident of
which sites happen to exist, not by the admission rule — and #7142 proposes a
third site whose protection would have to be argued from scratch.

Suggested resolution

Either promote the Delete / ReflectDelete arms of expr_is_shape_barrier to
a whole-program fact (the way the umbrella already treats cross-module hazards),
or state explicitly in collectors/proven_this.rs that the phase relies on a
per-site guard rather than on the module-wide delete scan — so the next site
added does not inherit a guarantee that was never there.

A cross-module repro would be a two-file gap test: module A holds
class C { a; b; c } plus a method reading this.c; module B does
delete inst.b on an instance A handed it, then calls the method.

[proggeramlug]

Closed by #7722 (v0.5.1417). Investigated and no miscompile exists — the asymmetry this issue describes is real, but in Phase 5a the per-module fact is a cost heuristic only; every routing site that can reach a $pshape clone re-derives soundness at runtime via a keys-token guard. That argument is now pinned by a sabotage-verified test rather than left implicit, because nothing in the source distinguishes the advisory use from the load-bearing one in ptr_shape.rs rule 2 — and a future tidy-up merging the two would silently break whichever way it went.