P1: Add Obligation Protocols for project-specific barrier-sensitive rules

[PhysShell]

Type

Enhancement / new analysis core slice.

Priority

P1 / High.

Tags

ownir, ownlang-core, protocols, obligations, barriers, project-specific-verification, legacy-dotnet, wpf

Context

Own.NET already has the right foundation for ownership/resource reasoning: OwnIR facts, Roslyn extraction, CFG, flow-sensitive state, loans/permissions, and method summaries. The next high-value slice is not another generic linter. It is a project-specific obligation checker.

The motivating failure mode:

IsLoaded = false;
// heavy document rebuild
OnPropertyChanged(nameof(Document)); // unsafe: observers can see inconsistent state
IsLoaded = true;

This is not a universal C# rule. It is a project/domain protocol: IsLoaded == false temporarily breaks the "document loaded / consistent" invariant, and selected notifications must not happen until that obligation is closed.

Proposed core model

Add an obligation/barrier vocabulary to OwnIR / Own.NET:

open obligation
close obligation
barrier
require obligation closed before barrier
require obligation closed before return/throw
allow selected barriers while obligation is open

First target rule shape:

DocumentLoading opens  when assign(this.IsLoaded, false)
DocumentLoading closes when assign(this.IsLoaded, true)
UnsafeNotification barrier when OnPropertyChanged(Document | Rows | Totals | SelectedItem)
Allowed notifications: IsLoaded, IsBusy, Progress, StatusText

Scope

MVP should be intraprocedural only:

• one method;
• CFG/path-sensitive;
• no interprocedural summaries yet;
• no generic theorem proving;
• no SMT;
• no mandatory user-authored OwnLang.

Acceptance criteria

• Clean method passes:
  • IsLoaded=false;
  • work;
  • IsLoaded=true;
  • OnPropertyChanged(nameof(Document)).
• Unsafe barrier before close fails.
• Early return before close fails.
• throw path before close fails unless guarded by finally.
• try/finally restoration passes.
• Allowed notifications, for example OnPropertyChanged(nameof(Progress)), can be configured as safe while open.
• Diagnostic includes a path witness, not just a vague warning.
• Diagnostic maps back to the original C# location when facts come from the Roslyn extractor.

Non-goals

• Do not build a generic temporal logic language.
• Do not require users to write .own by hand.
• Do not put this in OwnAudit. OwnAudit should only consume/report findings.
• Do not mix this with perf gates yet.

Suggested diagnostic

OWN201: open obligation crosses forbidden barrier.

Example:

OWN201: DocumentLoading is still open before OnPropertyChanged(Document).
Path: IsLoaded=false -> if (...) -> OnPropertyChanged(Document)
Expected: close DocumentLoading with IsLoaded=true before publishing Document.

Why this matters

This catches human-factor regressions that ordinary Roslyn analyzers, type checks, and architecture metrics do not understand, because they do not know the project-specific meaning of IsLoaded. That is the whole point: small verification-style guardrails for real legacy C# without rewriting the codebase or making developers learn a new language.