Soundness: the #293 teardown/guard predicates swallow a leak behind an early-return guard and in the else-branch of `if (disposing)` — adversarial audit, 2 P1 holes pinned red

[PhysShell]

Classification

• Change type: soundness fix (false negative), not a precision fix
• Priority: P1 — both holes silently swallow a leak class, and both sit one mechanical rewrite away from shapes the corpus already pins
• Found by: adversarial code reading of the landed predicates (enumerate implicit axioms → attack each → verify against Program.cs), full record in docs/notes/teardown-predicate-adversarial-audit.md
• Doctrine: Soundness regression from #225: empty-Dispose exemption trusts source emptiness, but IL weaving (Janitor.Fody) adds real cleanup — 263 silent exemptions in ClosedXML (+ explicit-interface Dispose coverage gap) #238 — "the worst case of an exemption must be 'keeps today's honest warning', never 'silently swallows a leak class'"
• Related: Soundness: OWN001 treats any -= in the class as a release — a -= behind a flag, or in a method nobody calls, silently swallows a real leak (heap-proven on SectorTS) #278 / fix(extractor): #278 — a -= releases only in a proven, unguarded teardown context #293 (the predicates under audit), fix(extractor): WPF002 Stop() teardown soundness — one doctrine with -= #302 (Stop() shares the same predicate — every hole applies verbatim to WPF002), Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304 (the general post-cutover answer), P-036

Hole A — a parameter guard spelled as an early return is invisible

public void Dispose() { Cleanup(keepAlive: true); }   // the only caller
public void Cleanup(bool keepAlive)
{
    if (keepAlive) return;                            // sibling, not ancestor
    _properties.PropertyChanged -= OnPropertiesChanged;  // never reached — CREDITED
}

IsParamGuardedRelease walks lexical ancestors of the -=; an early return is a preceding sibling, so the caller-controlled skip is invisible — while the symbol closure credits Cleanup because Dispose calls it, regardless of argument values. The SectorTS UnregOnlyGoodys guard — the exact leak #293 was built to catch — reopens under a semantics-preserving rewrite from if (!flag) { -= } to if (flag) return; -=. This is the C#-side twin of the bridge's D7 defect, fixed there as INF-S3.

Red fixture: corpus/wpf/subscription-teardown-early-return-guard (.own reduction caught by the core; extractor silent).

Hole B — the canonical if (disposing) exception credits the ELSE branch

private void Dispose(bool disposing)
{
    if (disposing) { }
    else { _properties.PropertyChanged -= OnPropertiesChanged; }  // CREDITED
}

IsCanonicalDisposingGuardUse classifies the parameter identifier's use in the condition (positive vs negated) and never asks which branch holds the site. The else-branch runs only via ~Finalizer → Dispose(false) — the path the extractor's own finalizer doctrine (#278 follow-up 1) declares unreachable while the subscription pins the subscriber. The predicate contradicts its own doctrine one branch away from the case it handles.

Red fixture: corpus/wpf/subscription-disposing-else-branch-release.

Also recorded (audit §2, no fixtures yet)

• C (P2): parameter laundered through a local (bool s = skip; if (!s) { -= }) — guard check sees only IParameterSymbol;
• E (minor): switch-arm when-clauses are outside the inspected condition set;
• D (Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304 family): name-root Dispose credited on a type that does not implement IDisposable (effect without enrollment) — cheap bounded improvement available;
• F (known extractor: normalize new-delegate handlers in event release-matching #163 family): receiver reassignment between +=/-= — dataflow, honestly out of S0.

Eleven attacks the predicate survives are recorded in audit §3 (positive assurance).

Fix direction (bounded, lexical — the #293 style, no call graph)

1. Demote when a parameter-conditioned return lexically precedes the site within the enclosing callable — EXCEPT the canonical negated-disposing exit (if (!disposing) return;), which guarantees the site runs;
2. the canonical-disposing exception applies only to sites in the THEN branch of the positive guard;
3. (with C/E) taint parameter-initialized locals in guard conditions; include when clauses.

Worst case of each rule stays "kept warning". Timer twins (timer-stop-*) land with the fix — same predicate, same holes.

Acceptance

• both red fixtures flip to caught; subscription-param-guarded-unregister and the canonical positive-branch shape (WinFormsDisposalSample) stay exactly as today;
• no new FP on any after.cs (benchmark: fixes clean, 0 FPs);
• oracle sweep shows no regression on the "-= genuinely in Dispose" shapes.