Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395

Описание

The H1 harmless predicate is deliberately strict. A call inside a protocol region is admitted only when its summary has:

• every parameter and the receiver ≤ borrow;
• writes.instance, writes.static and writes.indirect all none;
• returns == [];
• no Unknown.

H0 summaries record that a method writes instance, static or indirect memory, but not what it writes. So a write that provably cannot reach the region's entity is refused exactly like one that can, for example:

• a counter in an unrelated static class;
• a field of a freshly allocated local object.

Proposal: extend the H0 vocabulary with typed write targets: the declaring type or field of each write, or "unrelated to type family T". Then add a region-resource predicate that admits a call whose writes are all provably outside the entity's type family, and the token's.

Мотивация / сценарий

• docs/notes/heap-effect-summaries.md §7.2: "Region-resource precision … needs typed write targets, which H0 does not carry. Without them H1 is the strict predicate, which is sound."
• docs/notes/h1-proven-call.md, "Not in this slice": typed write targets.
• TB-MVP-01 (samples/OrderBackend) did not need them: its helper is pure. The rejected fixture corpus/negative/C12a_harmful_helper.cs.txt (a static counter, writes.static is may) shows the shape this would make admissible only when the target provably cannot alias the entity.

This is a soundness-sensitive change. It needs:

• a vocabulary bump of the heap-effects schema, and likely OwnIR, with the owner ruling and T0 handling of feat(ownir)!: OwnIR v2 — must-understand proven_call (H1) + T0 Amendment 2 #390;
• Python and Rust parity;
• mutants proving that an aliasing write (into the entity's family, a base type, object, or an interface the entity implements) stays refused.

Альтернативы

• Keep the strict predicate. Sound, and enough for the MVP. Wait for a real consumer that is blocked; the TB-MVP brief explicitly said not to build this "to make examples prettier".
• Per-call annotations ([NoEntityWrites]). Cheaper, but it moves the proof to trust (see the external-summaries issue).

Область

analyzer (dataflow / loans / permissions)

Refs: #390 (H0/H1), #391 (TB-MVP-01), #122 (interprocedural exclusivity axis for MOS).