feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001)

[PhysShell]

Что и зачем

Own.NET сегодня проверяет safety-свойства: ресурс должен быть освобождён, borrow не должен пережить владельца, короткоживущий объект не должен быть пришпилен к более длинному lifetime.

Не покрыта соседняя liveness-ошибка:

если цикл продолжает работу, он обязан продвигать состояние, управляющее его условием.

Это не проверка банального while (true) и не попытка доказать termination произвольного C#. Цель — узкий production-класс зависаний, где достижимый путь возвращается к голове цикла, не меняя распознаваемую монотонную меру и не выходя из цикла.

while (reader.Position < reader.Length)
{
 if (!TryReadNode(reader, out var node))
 continue;

 nodes.Add(node);
}

Если TryReadNode(...)=false не двигает reader.Position, failure-path бесконечно перечитывает тот же вход. Компилятор, обычные линтеры и happy-path тесты довольны; повреждённый файл кладёт production.

Текущий OwnIR моделирует while как body + back-edge для fixpoint, но не несёт guard/measure/outcome-sensitive progress contract, поэтому этот класс сейчас принципиально невыразим.

Product claim

Owen detects loops that can continue without consuming the state that controls them.

Не “general termination prover”, не temporal-logic engine и не dumb syntax rule.

Первая диагностика

PRG001 — reachable loop back-edge neither advances the recognized guard measure nor exits

Пример:

while (queue.Count > 0)
{
 var job = queue.Peek();

 if (!CanExecute(job))
 continue; // PRG001: queue.Count unchanged

 Execute(job);
 queue.Dequeue();
}

Ожидаемое сообщение:

PRG001 loop can repeat without progress: 'queue.Count' controls the loop, but the path
loop header -> !CanExecute(job) -> continue -> loop header neither decreases
'queue.Count' nor exits the loop. Remove/advance the item, break, or use a bounded retry policy.

Finding обязан нести ordered evidence path для SARIF codeFlows:

loop guard -> branch bypassing progress -> continue/back-edge -> unchanged measure

Scope: только распознаваемые монотонные меры

MVP поддерживает ограниченный каталог:

Guard / measure	Progress
i < end	i гарантированно увеличивается
remaining > 0	remaining гарантированно уменьшается
queue.Count > 0	queue.Count гарантированно уменьшается
reader.Position < reader.Length	reader.Position гарантированно увеличивается
enumerator/iterator loop	успешная итерация гарантированно продвигает enumerator

Путь к back-edge безопасен, только если:

1. мера гарантированно продвинулась; или
2. выполнен break, return или throw; или
3. путь доказан недостижимым.

Unsupported guard / opaque arithmetic / concurrency-sensitive state => никакого definite finding. Precision floor остаётся прежним: не умеем доказать — молчим и считаем honest skip/advisory, не выдумываем Must.

Ключевая фича: outcome-sensitive progress summaries

Нужна не просто отметка “callee may mutate cursor”, а контракт по исходу:

Progress ∈ { Never, Must, May, Unknown }

TryReadNode(reader, out node):
 returns true -> reader.Position MUST increase
 returns false -> reader.Position NEVER increases

Тогда:

while (reader.Position < reader.Length)
{
 if (!TryReadNode(reader, out var node))
 continue;
}

даёт PRG001, а оба варианта ниже молчат:

if (!TryReadNode(reader, out var node))
{
 reader.Position++; // discard malformed byte
 continue;
}

if (!TryReadNode(reader, out var node))
 break;

Summary requirements

• per-overload resolution через существующий sig;
• safe fallback к name-merged summary, если sig отсутствует/не совпал;
• SCC/fixpoint для recursive/mutually-recursive helpers;
• Unknown на extern/opaque boundaries;
• никакого fabricated Must;
• deterministic output и observable degradation.

Архитектура

Sidecar analysis, не новый ownership instruction zoo

Предпочтительная форма — отдельный Own.Progress analysis по образцу di.py, effects.py, obligations.py:

• frontend сообщает syntax/symbol facts;
• core вычисляет verdict;
• никаких verdict-гейтов в Roslyn extractor;
• отсутствие progress-блоков означает “analysis disabled”.

Черновая additive OwnIR shape:

{
 "progress_functions": [
 {
 "name": "Parser.TryReadNode",
 "sig": "Reader,Node&",
 "measures": [
 {
 "symbol": "arg0.Position",
 "direction": "increase",
 "outcomes": {
 "true": "must",
 "false": "never"
 }
 }
 ]
 }
 ],
 "progress_loops": [
 {
 "file": "Parser.cs",
 "line": 84,
 "guard": {
 "measure": "reader.Position",
 "relation": "<",
 "bound": "reader.Length",
 "direction": "increase"
 },
 "body": []
 }
 ]
}

Это направление, не замороженная schema. До implementation PR нужен отдельный schema checkpoint: identity measures, branch outcomes, break/continue, aliasing и evidence handles должны быть определены без строковой магии.

Внутренние discriminator-вокабуляции должны быть fail-loud. Добавление top-level optional blocks может оставаться additive только при безопасном default и явной versioning-политике, согласованной с spec/OwnIR.md.

Повторное использование существующего фундамента

• sig и conservative overload fallback;
• method-summary / call-graph / SCC infrastructure;
• Rust generic monotone worklist из P-022;
• existing evidence + SARIF codeFlows seam;
• Python reference -> Rust parity discipline.

Не строить второй solver только потому, что человечество любит плодить почти одинаковые fixpoint-циклы.

Built-in progress specifications

Стартовый curated каталог:

• Queue<T>.Dequeue() => receiver Count decreases;
• Stack<T>.Pop() => receiver Count decreases;
• List<T>.RemoveAt(...) => receiver Count decreases;
• i++, i += positiveConstant;
• remaining--, remaining -= positiveConstant;
• Stream.Read(...) / reader-like API => progress только при доказанном положительном результате;
• iterator/enumerator primitives, если frontend может связать outcome с measure без догадок.

Project APIs подключаются через approved config, например .owen-progress.json:

{
 "BrokerReader.TryMoveNext": {
 "measure": "arg0.Offset",
 "direction": "increase",
 "outcomes": {
 "true": "must",
 "false": "never"
 }
 }
}

Rules-as-data, не новый DSL для пользователей.

Proposed delivery slices

Slice 1 — direct intra-procedural progress

• распознать guard measure;
• моделировать continue/back-edge и exits;
• direct increment/decrement / curated collection consumers;
• один code: PRG001, только definite cases;
• ordered evidence path.

Slice 2 — interprocedural Try* summaries

• infer Must/May/Never/Unknown по boolean outcome;
• resolve exact overload through sig;
• SCC/fixpoint;
• extern => Unknown;
• project config contracts.

Slice 3 — real-world oracle

• mine parser/import/queue-processing loops;
• validate on at least one internal legacy target and one OSS C# target;
• manually classify every new finding before enabling any gate;
• retain “own-only 0 unexplained” precision discipline.

Slice 4 — optional runtime confirmation (later, separate scope)

A watchdog/stack-sample artifact may later correlate static PRG001 with repeated runtime stacks at the same loop and produce confirmed-progress-stall. This is explicitly not part of the first implementation.

Phase 1 acceptance contract

1. queue.Count > 0 + reachable continue bypassing Dequeue() => exactly one PRG001.
2. Every reachable back-edge contains definite Dequeue() => silent.
3. Non-progress branch ending in break, return, or throw => silent.
4. i < end with i++ on every back-edge => silent.
5. i < end with one branch bypassing i++ via continue => PRG001.
6. Unsupported guard/opaque mutation => no definite finding; skip/degradation observable.
7. Finding contains loop header, bypass branch, and back-edge as ordered evidence.
8. Existing OwnIR/ownership/lifetime/DI/effects/obligations fixtures remain unchanged.
9. Unknown progress event vocabulary fails loudly, never silently skips.
10. Deterministic ordering and stable line-free message fingerprint.

Phase 2 acceptance contract

1. First-party Try* method infers per-outcome progress.
2. false => Never followed by continue => PRG001.
3. false => Never followed by break => silent.
4. true/false => Must => safe on both continuing branches.
5. Mixed paths => May, not fabricated Must.
6. Exact overload selected via sig; unmatched/missing sig degrades conservatively.
7. Recursive and mutually-recursive helpers converge correctly.
8. Extern/opaque callees remain Unknown and do not create definite findings.
9. Python and Rust agree on (path, line, code, evidence path).
10. Real-world sweep records TP/FP/uncertain classification and blocks rollout on unexplained removals/additions.

Repository boundary

• Own.NET: facts, Roslyn extraction, Python reference analysis, Rust parity, PRG diagnostics, case studies.
• OwnAudit: normalization/category/severity, baseline ratchet, dashboard/SARIF consumption, optional later runtime correlation.
• Do not implement a second detector in OwnAudit.

Companion OwnAudit consumer issue will be linked here after creation.

Explicit non-goals

• proving termination of arbitrary C#;
• arbitrary ranking functions or symbolic arithmetic;
• deadlock/livelock under concurrency;
• async scheduling/fairness proofs;
• warning on every while (true);
• general temporal logic;
• auto-fixing loops in v1;
• runtime collector in the first implementation.

Definition of success

A convincing demo is not “we detect a suspicious loop”. It is:

PRG001 at Parser.cs:84
loop guard reader.Position < reader.Length
 -> TryReadNode returned false
 -> continue
 -> back-edge
reader.Position unchanged

The reviewer can click through the exact non-progress cycle and understand the fix without reverse-engineering the analyzer’s mood.

[PhysShell]

Companion consumer/integration issue created in OwnAudit: PhysShell/OwnAudit#49.

Repository boundary is now explicit: Own.NET owns facts, summaries, PRG diagnostics, Roslyn extraction, and Python↔Rust parity; OwnAudit only consumes the frozen finding shape for taxonomy, SARIF/codeFlows, baseline ratchets, dashboard triage, and any later runtime confirmation.

[PhysShell]

Documented the follow-on trust architecture in draft PR #276: P-035 — Proof-carrying findings and replayable derivation certificates.

For PRG001, the proposal defines the intended first certificate shape:

loop guard -> outcome-sensitive no-progress premise -> reachable non-exit back-edge -> PRG001.INTRO

The scope is deliberately separate from the detector implementation: #275 may ship ordinary evidence first; certificate support begins only after a schema/verifier checkpoint. Product wording is pinned to verified derivation over canonical facts, not “formally proven arbitrary C# bug.”

Companion OwnAudit consumption design: PhysShell/OwnAudit#50.