Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394

Описание

H1 (#390) admits a call inside a [ProtocolRegion] only when the shared H0 heap-effect summaries prove it harmless. Any method without source has no summary, so it is Unknown, and Unknown poisons the site:

• an extern/BCL call;
• an interface or virtual dispatch.

Two consequences:

• logger.LogInformation(...) inside a region is refused by the extractor (… runs code with no stated contract);
• a direct helper that transitively reaches the BCL is refused by the core (writes.instance is unknown).

Proposal: a separate, explicitly trusted summary source for code without a body (P-036's source: bcl | annotation):

• a curated, versioned table of summaries for a small, motivated set of BCL members, starting with Microsoft.Extensions.Logging.LoggerExtensions.Log* and pure string/Math members;
• and/or user annotations on a method or delegate, with the declared effect checked where the body exists.

Unknown stays the default for everything not covered.

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

• The H1 notes name this as the next separate slice, which needs its own trust argument: docs/notes/h1-proven-call.md ("Not in this slice: logger, BCL or annotation summaries") and docs/notes/heap-effect-summaries.md §7.3.
• In TB-MVP-01 (samples/OrderBackend), the handlers keep logging and the clock outside the region. Fixture corpus/negative/C12b_logger_in_region.cs.txt pins the refusal.
• In real handlers, "log inside the transition" is a common shape.

Acceptance (indicative):

• the curated table is data with a pinned digest, loaded by both engines with byte parity;
• each entry is justified, and a mutant table that marks a writing method harmless turns a pinned negative red;
• C12b flips only under an explicit policy; every un-annotated external call keeps failing closed;
• R18/R19 (Console.WriteLine, interface call) behave per the policy, and their texts are pinned.

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

• Keep the current rule: read what you need, and log, outside the region. It works and is sound, but it is ergonomic friction.
• A blanket "logging is harmless" allowlist. Rejected: an allowlist is not an effect proof. Loggers have sinks with arbitrary side effects, and the H1 brief explicitly forbade an allowlist.

Out of scope: devirtualization, typed write targets (separate issue), and changes to the H1 predicate itself.

Область

analyzer (dataflow / loans / permissions)

Refs: #390 (H1), #391 (TB-MVP-01), #274 (protocol/barrier effect summaries: a related but different domain).