repsel: Ptr<Shape> element reads — the four forms #7034 §3 does not cover

[proggeramlug]

PR #7149 (#7034 §3) licenses const r = A[i] on an element-shape-proven local
array and promotes r. It deliberately covers one read form. The others
are listed here so the gap is a decision, not an oversight.

Covered

• const r = A[i] under for (let i = 0; i < A.length; i++).
• for (const r of A) — the desugar
  (lower/stmt_loops.rs::lazy_or_index_elem) produces exactly the above, so
  this is covered by the same proof rather than by a second one.

Not covered

1. Direct A[i].field with no binding. total += rows[i].weight.
ArrayWalk admits it (a declared-chain field read/write cannot transition
the shape, so it does not disqualify the array), but nothing promotes it:
FnCtx::ptr_shape_receiver_fact matches only Expr::LocalGet and
Expr::This. Extending it to Expr::IndexGet needs the fact keyed on the
site — (array root, index local) is a sound key given E5 already requires
the index local to have exactly one governing loop — and each consumption site
(property_get.rs, property_get/helpers.rs, property_set.rs,
instance_misc1.rs, lower_call/property_get/dynamic_dispatch.rs) needs the
receiver lowered per access, which is one array element read per access rather
than one reload from a slot. Worth measuring against just asking users to bind
the element.

2. A.map(cb) / A.forEach(cb) / A.reduce(cb, …) callback parameters.
This is the call argument position (#7034 §1) — it needs clone-and-route,
not a containment relaxation. It is where batch.ts's hot field traffic
actually lives (acc[idx] inside the reducer).

3. Element reads bound to a let. E1's mutable: false on the array and
the single-Let requirement on the element local are both conservative; a
let r reassigned only from A[i] is provable but not proven.

4. Non-empty array literals. const a = [new C(1), new C(2)] is refused
because a literal can carry elisions, whose slots read back as undefined and
would break E5's density argument. A literal with no holes is fine and could
be admitted.

5. Shape-preserving mutators. sort, reverse, slice, concat of two
proven arrays, and fill with a class-C value all preserve "every element
is an instance of C" but are refused outright by E2, which admits only
push. pop/shift/splice/unshift/IndexSet must stay refused — they
are what E5's in-bounds argument rests on.

Each is independently landable, and each should be measured before it is
built: on the corpus measured in #7149, the element position accounts for 1 of
746 Ptr<Shape> candidates in dependency JS, so widening the READ side is only
worth it where app-shaped TypeScript is the target.

[proggeramlug]

Correction to the "Not covered" list, after review of PR #7149 found a soundness hole and closed it:

Direct A[i].field is no longer merely unpromoted — it now DISQUALIFIES the array.

The original wording said an unlicensed element read "cannot transition a shape, so it does not disqualify the array". That is true of the read and false of the reference it produces:

const rows: Row[] = [];
rows.push(new Row(…));
f(rows[i]);                 // callee does x.extra = 1
for (let k = 0; k < rows.length; k++) {
  const s = rows[k];
  total += s.weight;        // guard-free, fixed offset, on a reshaped object
}

const r = A[0] (literal index, so unlicensed) is the same hazard one step shorter: rule 2 never walks a binding the pass did not seed, so r.extra = 1 is invisible.

So ArrayWalk now disqualifies the array on any IndexGet occurrence outside the licensed Stmt::Let init. Two red tests cover it (an_element_passed_to_a_callee_denies_the_array, an_unlicensed_element_binding_denies_the_array), each with its own sabotage case.

Consequence for this issue: covering direct A[i].field is now worth more than it looked, because today it does not just fail to promote — it takes the whole array's group with it. Doing it needs the element class available inside ArrayWalk, which is only known after the push scan, so it wants a two-phase walk or a deferred check.