From 48ea00df5b1a09d7fb160a1ac8f081db926e6613 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 16:14:41 +0000 Subject: [PATCH 01/12] =?UTF-8?q?docs:=20interprocedural=20roadmap=20?= =?UTF-8?q?=E2=80=94=20staged=20path=20from=20D5=20today=20to=20'proper=20?= =?UTF-8?q?interprocedural'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Consolidates the scattered interprocedural state (d5 note's shipped slices, tech-debt register §3 prerequisite, deferred trackers #122/#146, the arity residual of d5 §10 q2) into one sequenced roadmap: - stage 0: spec the verdict-determining bridge inference + golden facts (the P-022 hard prerequisite, unlocks everything else) - stage 1: observability first — OWN051 advisory + MOS summary dump - stage 2: arity/signature key on call ops (additive optional field, no OWNIR_VERSION bump) to stop conservative overload merging - stage 3: aliasOf:i through return + out/ref fresh (Dapper/Polly become oracle anchors with a recorded reason) - stage 4: publisher provenance (#146) on top of stage 3's skeletons - stage 5: exclusivity axis (#122) strictly on its consumer trigger - stage 6: Tier C annotations + pessimistic mode Includes a definition of done, a dependency graph, on-record rejections (context sensitivity, IL decompilation, frontend inference), and a reading path into ownership.py/ownir.py for newcomers. Cross-linked from the d5 note's §10 open questions. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/d5-ownership-transfer.md | 3 + docs/notes/interprocedural-roadmap.md | 234 ++++++++++++++++++++++++++ 2 files changed, 237 insertions(+) create mode 100644 docs/notes/interprocedural-roadmap.md diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index b8999982..9240aca7 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -470,6 +470,9 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa ## 10. Open questions remaining +> Sequencing for closing these — together with the deferred §7 slices, #122 and +> #146 — lives in [interprocedural-roadmap.md](interprocedural-roadmap.md). + 1. ~~`aliasOf` in the core: shared resource id vs a synthetic discharge edge.~~ **Resolved → §11 (the obligation-identity model): Variant B, a shared RID / alias-set.** 2. ~~Signature-key canonicalisation across overloads / generics / partial classes (the diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md new file mode 100644 index 00000000..3d9a0dc1 --- /dev/null +++ b/docs/notes/interprocedural-roadmap.md @@ -0,0 +1,234 @@ +# Дорожная карта — путь к «нормальной межпроцедурке» + +> Статус: **живая дорожная карта** (не нормативная спека, не proposal). Собрана из +> [d5-ownership-transfer.md](d5-ownership-transfer.md) (дизайн и shipped-срезы), +> [tech-debt-register.md](tech-debt-register.md) §3 (мост как пререквизит), +> [architecture-review-2026-07.md](architecture-review-2026-07.md) (риск R2) и +> живых трекеров [#122](https://github.com/PhysShell/Own.NET/issues/122), +> [#146](https://github.com/PhysShell/Own.NET/issues/146). Она **ссылается, а не +> дублирует**: детали каждого шага живут в первоисточнике, здесь — порядок, +> зависимости и критерий «готово». +> +> Приоритет прежний: карта **подчинена альфе** +> ([alpha-readiness.md](alpha-readiness.md)) — ни один этап ниже не вытесняет +> упаковку `ownsharp check MyApp.sln`. Этапы 0–1 — days-scale и совместимы с ней. + +## 0. Что значит «норм» (целевое состояние, definition of done) + +Межпроцедурка считается «нормальной», когда выполняются пять условий: + +1. **Инференция — first-class.** Слой, который сегодня определяет вердикты + (~900 строк в мосте `ownlang/ownir.py`: `_build_skeletons`, + `_infer_param_effect`, `_infer_return_skeleton`, hoisting + решатель + `ownership.py`), либо нормативно описан в `spec/`, либо живёт в `ownlang/` + как обычный pass. «Ядро» и «то, что придётся портировать» — одно и то же + множество (сегодня — нет, и это признанный крупнейший gap P-022). +2. **Сводка выразительна по всем четырём осям**: transfer (есть), + freshness/alias возврата (есть частично — `aliasOf:i` через границу не + доносится), эксклюзивность займов (нет — #122), провенанс параметра + («сконструирован-и-возвращён» — нет, #146). +3. **Перегрузки различимы.** Сводки не сливаются консервативно по голому имени + (`_merge_skeletons`, open question 2 d5-заметки): ключ несёт как минимум + арность, в пределе — сигнатуру. +4. **Неопределённость видима.** `may`/`unknown`-transfer'ы доступны как + advisory (OWN051-класс, никогда не валит CI) + пессимистичный режим opt-in; + «мы не смогли доказать» перестаёт быть неотличимым от «мы проверили, чисто». +5. **Пол не тронут.** `own-only 0` на оракуле, зелёный corpus, Dapper/Polly — + регрессионные якоря «чисто *с записанной причиной*», а не случайно. + +## 1. Где мы сейчас (карта фактического состояния) + +Четыре направления переноса владения (§2 d5-заметки) и их статус: + +| Напр. | Что это | Статус | Код | +|---|---|---|---| +| T1 return-out | fresh-возврат → acquire у вызывающего | ✅ D5.2 + Tier B таблица (D5.3) | `_infer_return_skeleton`, `_callee_returns_fresh`, `_BCL_FRESH_BY_NS` | +| T2 arg-consume | параметр ушёл (dispose/adopt/forward-к-consume) → `consume` | ✅ D5.1a/b (включая `$consume`-канал) | `_build_skeletons` → `solve` → `_infer_param_effect` | +| T3 arg-borrow | параметр только читается → `borrow`, утечка остаётся у вызывающего | ✅ D5.1a/b | там же | +| T4 wrap/adopt | обёртка делит обязательство с внутренним ресурсом | ◑ ctor-adopt на месте конструирования есть (D5.4 шаги 0–2); `aliasOf:i` **через return** — нет | `alias_join` + RID-модель (`analysis.py`), `TryAdoptedArgIndex` (extractor) | + +Решатель: `ownlang/ownership.py` — чистый, без зависимостей; SCC-конденсация +(Тарьян), фикспойнт снизу вверх, решётка `Transfer{no,must,may,unknown}`, +без depth cap. Одна контекстно-нечувствительная сводка на метод. + +Отложенное (каждый пункт — записанное решение с триггером, не дыра): + +| Что | Почему отклонено сейчас | Триггер возврата | Трекер | +|---|---|---|---| +| Арность/сигнатура в ключе сводки | `call.callee` = `{Type}.{Method}` без сигнатуры; слияние precision-safe, но грубее per-arity | этот roadmap, этап 2 | d5 §10 q2 | +| `aliasOf:i` через return (Dapper `Create(reader)`) | нужен return-скелет `aliasOf` + caller-side lowering | этап 3 | d5 D5.4 «step 2 remainder» | +| Ось эксклюзивности в сводке | у межпроцедурной эксклюзивности **нет потребителя** (OWN006/011/012/013 — интрапроцедурные) | первый межпроцедурный потребитель | #122 | +| Провенанс паблишера («returned-fresh») | требует обратного (caller→callee) прохода, которого нет | этап 4 (после этапа 3) | #146 | +| `out`/`ref`-owned как источник fresh | отдельный extractor-срез | этап 3, попутно | d5 D5.2 «remaining» | +| OWN051 advisory + пессимистичный режим | дизайн готов (d5 §5), не реализован | этап 1 (поднят: наблюдаемость) | d5 D5.x | + +## 2. Этап 0 — норма для того, что уже есть (дни; разблокирует всё) + +**Проблема:** инференция определяет вердикты, но не имеет нормативного описания — +её нет ни в `spec/`, ни в `ownir.schema.json`; она закреплена только примерами в +`tests/test_ownir.py`. Это риск R2 ревью и жёсткий пререквизит tech-debt §3 +(«spec it or relocate it — до любого порта»). Каждый следующий этап меняет именно +этот слой; менять неспецифицированное — дороже всего. + +**Делаем:** + +- `spec/Inference.md` (или раздел в `spec/OwnIR.md`): нормативные правила + вывода — когда параметр `dispose`/`forward`/`borrow`, правило + «single unconditional straight-line forward», правила return-скелета + (returned-param ≠ fresh и т.д.), правила слияния перегрузок, политика + optimistic-по-умолчанию. По объёму это перенос докстрингов + (`_build_skeletons`, `_merge_skeletons`, `solve`) в нормативный текст + + привязка к `test_spec.py`-стилю. +- Golden facts snapshots в CI (N3 из регистра) — шов extractor→bridge diff'ится + на уровне фактов, а не только отрендеренных диагностик. +- **Не делаем сейчас:** физический перенос инференции из моста в `ownlang/` — + это «seam re-cut» из tech-debt §3, его триггер (P-017 multi-stack или + рестарт ядра P-022) не сработал. Спека делает перенос механическим, когда + сработает. + +**Критерий готовности:** новый разработчик (или порт) может реализовать +инференцию по спеке, не читая `ownir.py`; расхождение спеки и кода ловится CI. + +## 3. Этап 1 — наблюдаемость: OWN051 + дамп сводок (дни) + +d5-заметка ставит advisory в хвост (D5.x); эта карта его **поднимает**: канал +«ownership transfer unverified» — самый дешёвый способ *увидеть* межпроцедурку +и главный ответ на «непонятки». Вся фактура уже считается (§5 d5: «we compute +the full must/may/escape evidence regardless of mode»), не хватает поверхности: + +- **OWN051** (OWN05x-band, как OWN050): `transfer:may` и honest-`unknown` + показываются с `--verbosity normal`+, никогда не валят CI. +- **Дамп сводок**: `MethodSummary.to_dict()` уже существует (сериализация + `summaries[]` из d5 §6) — вывести таблицу MOS по флагу (`--dump-summaries` + или в `explain`), плюс extern-границы из `solve_with_log`. Смотришь на метод — + видишь, что решатель про него думает и почему вызов остался plain. + +**Критерий готовности:** на любом прогоне можно ответить «почему этот вызов +не consume/borrow/fresh» без чтения кода моста. + +## 4. Этап 2 — сигнатурный ключ: закрыть арность (1–2 недели) + +**Проблема (d5 §10 q2):** узел `call` и `functions[].name` именуют метод +`{Type}.{Method}`; перегрузки сливаются в одну консервативную сводку: +`must` — только если *каждая* перегрузка consume'ит индекс, `fresh` — только +если *все* fresh. Precision-safe, но грубо: одна borrow-перегрузка глушит +consume-сводку всех остальных, а overload-неоднозначные имена вообще исключены +из Tier B (`Process.Start`, `new StreamReader(stream)`). + +**Делаем (аддитивно, без бампа `OWNIR_VERSION`):** + +- Extractor кладёт **опциональное** поле на `call`-оп и на `functions[]`-запись: + минимум `arity` (int), лучше сразу `signature` (канонический список типов + параметров — SemanticModel это знает). По политике эволюции (IR-правила, + `spec/OwnIR.md` §2) опциональное поле не бампает версию; продюсер без типов + (ownts) просто его не пишет. +- Мост группирует скелеты по `(name, arity|signature)` с фолбэком на слияние по + имени, когда поле отсутствует (старые факты — прежнее поведение, ничего не + ломается). `solve` резолвит forward-рёбра по тому же ключу. +- Пересматриваем исключения Tier B, введённые из-за неоднозначности перегрузок. + +**Выигрыш:** recall на `must`/`fresh` у перегруженных имён; двусмысленные +фабрики возвращаются в таблицу. **Остаток (записать честно):** перегрузки +одной арности с разными типами при варианте `arity` остаются слитыми — потому +предпочтителен сразу `signature`, чтобы не делать двух миграций. + +## 5. Этап 3 — дожать T1/T4: `aliasOf:i` через return, out/ref (2–3 недели) + +Самый большой прикладной выигрыш из оставшихся — «step 2 remainder» D5.4: + +- **Shape (a), return-alias:** `var r = Create(reader)`, где `Create` + `alias_join`-ит обёртку к параметру и возвращает её → return-скелет + `aliasOf:i`; на месте вызова обязательство `reader` дисчарджится через `r` + (а прямой `reader.Dispose()` после — OWN003). Механика per-RID в ядре уже + вся есть (шаги 0–1), нужен вывод `aliasOf` в `_infer_return_skeleton` + + caller-side lowering (дизайн — d5 §6). Must-only правило §11 сохраняется: + недоказанный alias — не заявка. +- **Field-store-to-this** форма adopt'а (Polly `BulkheadPolicy(factory())`) и + случаи, которые v1-гейт сознательно отклонил (`using`/убегающая обёртка). +- **`out`/`ref`-owned параметры** как ещё один источник fresh (extractor-срез). + +**Критерий готовности:** Dapper и Polly — оракул-якоря `own-only 0` *с +записанной причиной* (кросс-линк в `field-notes-patterns.md`), а не по +совпадению; это явный exit-criterion в d5 §8. + +## 6. Этап 4 — провенанс паблишера, #146 (после этапа 3) + +Дуал ownership transfer: `+=` на паблишере, который вызывающий сконструировал +и **вернул**, ограничен временем жизни возвращённого объекта — не утечка. +Требуется новый вид факта о параметре: «во *всех* вызывающих аргумент на этой +позиции — локально сконструированный и возвращённый объект». + +Почему после этапа 3: это **обратное** направление распространения +(caller→callee; текущий фикспойнт — callee→caller) поверх тех же return-скелетов +и call-графа. Join — must-стиль по всем вызывающим (один DI-singleton-вызов → +остаёмся `injected`), так что DI-кейс реальной утечки не трогается. До тех пор +консервативный advisory warning — честная поза (сам issue это фиксирует). + +## 7. Этап 5 — ось эксклюзивности, #122 (строго по триггеру, не по календарю) + +Ничего не делать, пока не появится **первый межпроцедурный потребитель** +эксклюзивности (конфликт класса OWN006/011/012/013 через границу вызова). +Ось без читателя не даёт наблюдаемых false negatives, а работа уже аддитивна: +forward-рёбра сохранены в скелете (`PathAction(kind="forward")`), нужен +leaf borrow-kind + join + поле на `ParamSummary` — не пересборка решателя. +Появление такого потребителя — например, когда займы полей/статиков начнут +проверяться через сводки — и есть момент, когда этап входит в план. + +## 8. Этап 6 — граница third-party: Tier C + пессимистичный режим + +- **Tier C аннотации** (`[OwnTransfers]`, `[OwnsReturn]`, `[MustCallAlias]`-стиль + + external-annotations side file): авторитетный оверрайд для кода без тел. + Единственный систематический ответ на extern-границы, которые `solve_with_log` + уже логирует (Tier B-таблицы масштабируются только на «знаменитые» API). +- **Пессимистичный режим** (unknown → borrow → репортим): opt-in, никогда не + дефолт; вместе с OWN051 из этапа 1 закрывает пункт 4 целевого состояния. + +## 9. Порядок и зависимости + +```text +Этап 0 (спека + golden facts) ──► всё остальное (менять слой без нормы — дороже) +Этап 1 (OWN051 + дамп) ──► независим; ускоряет отладку этапов 2–5 +Этап 2 (арность/сигнатура) ──► усиливает 3 и 4 (точнее ключ — точнее рёбра), + но жёстко не блокирует +Этап 3 (aliasOf через return) ──► этап 4 (#146 стоит на return-скелетах) +Этап 5 (#122) ──► вне очереди: ждёт потребителя, не места в списке +Этап 6 (Tier C, pessimistic) ──► после 1 (advisory-поверхность уже есть) +``` + +Связь с остальным репозиторием: этап 0 — одновременно крупнейший gap P-022 +(мост никому не принадлежит в крейтовой топологии) и «during the rewrite»-ловушка, +которую tech-debt-register уже разминировал; Gate A +([incremental-computation.md](incremental-computation.md)) открывается ровно +тогда, когда этапы 3–4 сделают межпроцедурку whole-program по-настоящему — тогда +инкрементальность перестаёт быть оверинжинирингом. + +## 10. Чего не делать (отказы на запись) + +- **Контекстная чувствительность / points-to.** Прайор-арт (RLC/RLC#) и наш + собственный опыт: context-insensitive сводок достаточно; наш пол — precision, + а не soundness, и каждый спорный случай уже решается «молчим». +- **IL/Cecil-декомпиляция third-party** — Tier C закрывает потребность без + нового фронтира (d5 §9, подтверждено terrain map). +- **Перенос инференции во фронтенд** — «second checker», запрещён хартией + (`ownir.py:5-7`, ROADMAP «One checker»). +- **Datalog/инкрементальность сейчас** — до Gate A/B это оверинжиниринг + (incremental-computation.md, решение стоит). + +## 11. Как читать этот слой (входные точки) + +Порядок чтения, который делает межпроцедурку обозримой за один заход: + +1. `ownlang/ownership.py` (~450 строк, без зависимостей): решётка `Transfer`, + `PathAction`/`ParamSkeleton`/`MethodSkeleton` (вход), `ParamSummary`/ + `MethodSummary` (выход), `solve`/`solve_with_log` (SCC-фикспойнт). + Тесты: `tests/test_ownership.py`. +2. `ownlang/ownir.py`: `_build_skeletons` (тело → скелет; правила precision + в докстринге), `_merge_skeletons` (слияние перегрузок — арность), + `_infer_return_skeleton` + `_callee_returns_fresh` (T1/Tier B), + `_infer_param_effect` (сводка → effect на call-site). + Тесты: `tests/test_ownir.py` (синтетический OwnIR). +3. RID/alias-модель ядра: d5 §11 (прочесть раньше кода), затем `analysis.py` + (state на RID, `alias_join`) и `tests/test_rid.py`. +4. Линза для любого «почему не ловится»: сначала спросить «а можем ли мы это + *доказать*?» — если нет, молчание почти наверняка сознательное (optimistic, + `own-only 0`), и у отказа есть записанный триггер (§1 таблица). From adc14969452186a66e41c4129df8a13e15c7ac3c Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 16:32:08 +0000 Subject: [PATCH 02/12] docs(roadmap): re-key the interprocedural stages to the Rust rewrite (P-022) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Records the decision that the core rewrite is now in execution and applies the 'one checker' guardrail to the roadmap: a feature freeze on verdict-changing inference until parity/cutover (a new axis in Rust before parity diverges from the reference; a new axis in Python moves the parity target the port must chase). Stage re-keying: stage 0 (spec the bridge inference) is language-neutral and is the port's prerequisite — do now; stage 1's summary dump is requalified as a parity artifact (diff Python vs Rust MOS summaries); stage 2's extractor half runs parallel to the port while its consuming half, stages 3-4 and 6 land in Rust after cutover; #122 is unaffected. Also records what ports cheaply (the pure ownership.py solver, the language-neutral synthetic OwnIR tests) and the on-record caveat that an urgent precision fix during the port goes into Python and knowingly moves the parity target. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-roadmap.md | 92 +++++++++++++++++++++------ 1 file changed, 72 insertions(+), 20 deletions(-) diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md index 3d9a0dc1..11014005 100644 --- a/docs/notes/interprocedural-roadmap.md +++ b/docs/notes/interprocedural-roadmap.md @@ -3,7 +3,9 @@ > Статус: **живая дорожная карта** (не нормативная спека, не proposal). Собрана из > [d5-ownership-transfer.md](d5-ownership-transfer.md) (дизайн и shipped-срезы), > [tech-debt-register.md](tech-debt-register.md) §3 (мост как пререквизит), -> [architecture-review-2026-07.md](architecture-review-2026-07.md) (риск R2) и +> [architecture-review-2026-07.md](architecture-review-2026-07.md) (риск R2), +> [P-022](../proposals/P-022-rust-core-migration.md) + +> [p022-review-notes.md](p022-review-notes.md) (Rust-порт, §2 ниже) и > живых трекеров [#122](https://github.com/PhysShell/Own.NET/issues/122), > [#146](https://github.com/PhysShell/Own.NET/issues/146). Она **ссылается, а не > дублирует**: детали каждого шага живут в первоисточнике, здесь — порядок, @@ -62,7 +64,53 @@ | `out`/`ref`-owned как источник fresh | отдельный extractor-срез | этап 3, попутно | d5 D5.2 «remaining» | | OWN051 advisory + пессимистичный режим | дизайн готов (d5 §5), не реализован | этап 1 (поднят: наблюдаемость) | d5 D5.x | -## 2. Этап 0 — норма для того, что уже есть (дни; разблокирует всё) +## 2. Поправка на Rust-переписывание (P-022): что где делается + +> Записанное решение (2026-07-04): ядро переписывается на Rust — P-022 переходит +> из «draft, design-only» в исполнение (`rust/crates/own-syntax` и `own-ir` уже +> в дереве, оракул — `scripts/oracle_exact.py`). Эта секция перепривязывает +> этапы карты к порту; содержание этапов не меняется. + +Несущее ограничение — «one checker» (P-022; guardrail из +[incremental-computation.md](incremental-computation.md)): новое ядро — это +*оптимизация, а не новый решатель*; оно обязано давать бит-в-бит те же вердикты, +что Python-ядро, на всём корпусе, доказано дифференциальным оракулом. Следствие, +применённое к этой карте: + +**Фиче-фриз на вердикт-меняющей инференции до cutover.** Новая ось в Rust до +паритета — намеренное расхождение с эталоном (оракул теряет смысл: «какой из +двух прав?»); новая ось в Python — движущийся паритет-таргет, который порт +обязан догонять (классический убийца переписываний). Обе двери закрыты, пока +Rust не станет решателем. + +| Этап | Когда и где | +|---|---| +| 0 — спека инференции | **сейчас; языко-нейтрален.** Это определение того, *что* портировать — жёсткий пререквизит порта (tech-debt §3) и крупнейший gap P-022 (мостом `ownir.py` не владеет ни один крейт) | +| 1 — OWN051 + дамп сводок | **сейчас, в Python.** Дамп переквалифицирован в **паритетный артефакт**: нормализованный дифф MOS-сводок Python↔Rust проверяет порт инференции точнее, чем сравнение конечных диагностик | +| 2 — арность, экстрактор-половина | параллельно с портом — это C#-сторона (`Program.cs`), OwnIR-шов её изолирует от вопроса Python-vs-Rust | +| 2 — арность, потребление в мосте | **Rust, после cutover** инференц-слоя | +| 3 — `aliasOf:i` через return, out/ref | **Rust, после cutover** | +| 4 — провенанс паблишера (#146) | **Rust, после cutover** (стоит на этапе 3) | +| 5 — эксклюзивность (#122) | без изменений: ждёт потребителя, язык ядра не важен | +| 6 — Tier C + пессимистичный режим | **Rust, после cutover** (advisory-поверхность этапа 1 переносится) | + +Что при этом переносится почти бесплатно: + +- **Решатель `ownership.py` — самая лёгкая часть порта**: ~450 чистых строк без + зависимостей; `Transfer`-решётка, исчерпывающий match по `PathAction`, + SCC-фикспойнт — Rust-native фактура. Сложность слоя никогда не была в + решателе — она в неспецифицированной обвязке моста, что и закрывает этап 0. +- **Синтетические OwnIR-тесты (`tests/test_ownir.py`) языко-нейтральны**: + JSON-факты на входе, ожидаемые диагностики на выходе — готовый + конформанс-набор для Rust-ядра через CLI, без переписывания. + +Оговорка на запись: до cutover Python **остаётся решателем**. Срочный +precision-баг с оракула в период порта чинится в Python — и осознанно двигает +паритет-таргет (решение, не сюрприз); такое изменение сопровождается +обновлением golden-сводок этапа 1, чтобы Rust-сторона догоняла по диффу, а не +по археологии. + +## 3. Этап 0 — норма для того, что уже есть (дни; разблокирует всё) **Проблема:** инференция определяет вердикты, но не имеет нормативного описания — её нет ни в `spec/`, ни в `ownir.schema.json`; она закреплена только примерами в @@ -89,7 +137,7 @@ **Критерий готовности:** новый разработчик (или порт) может реализовать инференцию по спеке, не читая `ownir.py`; расхождение спеки и кода ловится CI. -## 3. Этап 1 — наблюдаемость: OWN051 + дамп сводок (дни) +## 4. Этап 1 — наблюдаемость: OWN051 + дамп сводок (дни) d5-заметка ставит advisory в хвост (D5.x); эта карта его **поднимает**: канал «ownership transfer unverified» — самый дешёвый способ *увидеть* межпроцедурку @@ -104,9 +152,11 @@ the full must/may/escape evidence regardless of mode»), не хватает п видишь, что решатель про него думает и почему вызов остался plain. **Критерий готовности:** на любом прогоне можно ответить «почему этот вызов -не consume/borrow/fresh» без чтения кода моста. +не consume/borrow/fresh» без чтения кода моста. С началом Rust-порта у этапа +появляется вторая роль (§2): нормализованный дамп сводок — паритетный артефакт, +по которому диффуются Python- и Rust-стороны инференции. -## 4. Этап 2 — сигнатурный ключ: закрыть арность (1–2 недели) +## 5. Этап 2 — сигнатурный ключ: закрыть арность (1–2 недели) **Проблема (d5 §10 q2):** узел `call` и `functions[].name` именуют метод `{Type}.{Method}`; перегрузки сливаются в одну консервативную сводку: @@ -132,7 +182,7 @@ consume-сводку всех остальных, а overload-неоднозна одной арности с разными типами при варианте `arity` остаются слитыми — потому предпочтителен сразу `signature`, чтобы не делать двух миграций. -## 5. Этап 3 — дожать T1/T4: `aliasOf:i` через return, out/ref (2–3 недели) +## 6. Этап 3 — дожать T1/T4: `aliasOf:i` через return, out/ref (2–3 недели) Самый большой прикладной выигрыш из оставшихся — «step 2 remainder» D5.4: @@ -151,7 +201,7 @@ consume-сводку всех остальных, а overload-неоднозна записанной причиной* (кросс-линк в `field-notes-patterns.md`), а не по совпадению; это явный exit-criterion в d5 §8. -## 6. Этап 4 — провенанс паблишера, #146 (после этапа 3) +## 7. Этап 4 — провенанс паблишера, #146 (после этапа 3) Дуал ownership transfer: `+=` на паблишере, который вызывающий сконструировал и **вернул**, ограничен временем жизни возвращённого объекта — не утечка. @@ -164,7 +214,7 @@ consume-сводку всех остальных, а overload-неоднозна остаёмся `injected`), так что DI-кейс реальной утечки не трогается. До тех пор консервативный advisory warning — честная поза (сам issue это фиксирует). -## 7. Этап 5 — ось эксклюзивности, #122 (строго по триггеру, не по календарю) +## 8. Этап 5 — ось эксклюзивности, #122 (строго по триггеру, не по календарю) Ничего не делать, пока не появится **первый межпроцедурный потребитель** эксклюзивности (конфликт класса OWN006/011/012/013 через границу вызова). @@ -174,7 +224,7 @@ leaf borrow-kind + join + поле на `ParamSummary` — не пересбор Появление такого потребителя — например, когда займы полей/статиков начнут проверяться через сводки — и есть момент, когда этап входит в план. -## 8. Этап 6 — граница third-party: Tier C + пессимистичный режим +## 9. Этап 6 — граница third-party: Tier C + пессимистичный режим - **Tier C аннотации** (`[OwnTransfers]`, `[OwnsReturn]`, `[MustCallAlias]`-стиль + external-annotations side file): авторитетный оверрайд для кода без тел. @@ -183,26 +233,28 @@ leaf borrow-kind + join + поле на `ParamSummary` — не пересбор - **Пессимистичный режим** (unknown → borrow → репортим): opt-in, никогда не дефолт; вместе с OWN051 из этапа 1 закрывает пункт 4 целевого состояния. -## 9. Порядок и зависимости +## 10. Порядок и зависимости ```text -Этап 0 (спека + golden facts) ──► всё остальное (менять слой без нормы — дороже) -Этап 1 (OWN051 + дамп) ──► независим; ускоряет отладку этапов 2–5 -Этап 2 (арность/сигнатура) ──► усиливает 3 и 4 (точнее ключ — точнее рёбра), +Этап 0 (спека + golden facts) ──► всё остальное; одновременно пререквизит порта (§2) +Этап 1 (OWN051 + дамп) ──► независим; паритетный артефакт порта (§2) +паритет + cutover (P-022) ──► открывает этапы 2(потребление)–4 и 6 — в Rust +Этап 2 (арность/сигнатура) ──► экстрактор-половина — параллельно порту; + усиливает 3 и 4 (точнее ключ — точнее рёбра), но жёстко не блокирует Этап 3 (aliasOf через return) ──► этап 4 (#146 стоит на return-скелетах) Этап 5 (#122) ──► вне очереди: ждёт потребителя, не места в списке Этап 6 (Tier C, pessimistic) ──► после 1 (advisory-поверхность уже есть) ``` -Связь с остальным репозиторием: этап 0 — одновременно крупнейший gap P-022 -(мост никому не принадлежит в крейтовой топологии) и «during the rewrite»-ловушка, -которую tech-debt-register уже разминировал; Gate A +Связь с остальным репозиторием: перепривязка к Rust-порту — §2 (этап 0 — +крупнейший gap P-022, «during the rewrite»-ловушка разминирована +tech-debt-register'ом); Gate A ([incremental-computation.md](incremental-computation.md)) открывается ровно -тогда, когда этапы 3–4 сделают межпроцедурку whole-program по-настоящему — тогда -инкрементальность перестаёт быть оверинжинирингом. +тогда, когда этапы 3–4 сделают межпроцедурку whole-program по-настоящему — и +в Rust-ядре названный кандидат на инкрементальность (Salsa) уже под рукой. -## 10. Чего не делать (отказы на запись) +## 11. Чего не делать (отказы на запись) - **Контекстная чувствительность / points-to.** Прайор-арт (RLC/RLC#) и наш собственный опыт: context-insensitive сводок достаточно; наш пол — precision, @@ -214,7 +266,7 @@ leaf borrow-kind + join + поле на `ParamSummary` — не пересбор - **Datalog/инкрементальность сейчас** — до Gate A/B это оверинжиниринг (incremental-computation.md, решение стоит). -## 11. Как читать этот слой (входные точки) +## 12. Как читать этот слой (входные точки) Порядок чтения, который делает межпроцедурку обозримой за один заход: From d25a8b425c4542baf720755ce93d55c713e519a3 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 16:42:34 +0000 Subject: [PATCH 03/12] =?UTF-8?q?docs:=20working=20spec=20(TZ)=20for=20the?= =?UTF-8?q?=20interprocedural=20layer=20=E2=80=94=20rules=20as-is,=20invar?= =?UTF-8?q?iants,=20Rust-port=20requirements?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deep-dive companion to interprocedural-roadmap.md. Pins the layer's actual semantics to code at adc1496 with file:line references: - normative rules as implemented: the Transfer lattice and path contributions, skeleton derivation (S), return inference (R), overload merging (M), the SCC fixpoint (F), call-site application (A) and tier precedence — the raw material for spec/Inference.md (stage 0) - five spec decision points (D1-D5), including a REPRODUCED precision defect: any-path release infers consume, so a callee that disposes a parameter conditionally fabricates OWN002 at a careful caller and OWN001 in the callee itself (violates the own-only-0 floor; verified by executing check_facts on synthetic facts). Recommended fix: branch-sensitive release derivation (all-paths -> dispose, partial -> may -> plain), to be decided BEFORE the port so bit-parity does not enshrine the bug. Also: the dead escapes axis, reserved adopt/return path kinds, the aliasOf hop degradation, and the silent solver degrade (except -> empty MOS) that should become observable - twelve numbered invariants (precision floor, determinism-from-input, tier precedence, closed op vocabulary, byte-exact output texts) as review blockers - Rust-port requirements for own-bridge: type mapping, determinism rules (no hash-order reaching output), error policy matching the Python degrade, --dump-summaries as a third oracle_exact surface, and the port order (solver -> derivation -> application), each phase behind its parity gate - concrete work cards for roadmap stages 2-4: signature key with fallback rules that preserve Tier A suppression, aliasOf:i through return (first slice, direct calls only), and #146 with a hard visibility gate — each with its test matrix and DoD Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-roadmap.md | 5 +- docs/notes/interprocedural-tz.md | 380 ++++++++++++++++++++++++++ 2 files changed, 384 insertions(+), 1 deletion(-) create mode 100644 docs/notes/interprocedural-tz.md diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md index 11014005..5cd493ec 100644 --- a/docs/notes/interprocedural-roadmap.md +++ b/docs/notes/interprocedural-roadmap.md @@ -9,7 +9,10 @@ > живых трекеров [#122](https://github.com/PhysShell/Own.NET/issues/122), > [#146](https://github.com/PhysShell/Own.NET/issues/146). Она **ссылается, а не > дублирует**: детали каждого шага живут в первоисточнике, здесь — порядок, -> зависимости и критерий «готово». +> зависимости и критерий «готово». Рабочее ТЗ слоя — нормативные правила +> как-есть, инварианты, найденные расхождения (включая воспроизведённый +> precision-дефект D1) и требования к Rust-порту — в +> [interprocedural-tz.md](interprocedural-tz.md). > > Приоритет прежний: карта **подчинена альфе** > ([alpha-readiness.md](alpha-readiness.md)) — ни один этап ниже не вытесняет diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md new file mode 100644 index 00000000..1f20c619 --- /dev/null +++ b/docs/notes/interprocedural-tz.md @@ -0,0 +1,380 @@ +# ТЗ — межпроцедурный слой: нормативная семантика, инварианты, порт в Rust + +> Статус: **рабочее ТЗ** (черновик нормы + критические требования). Дополняет +> [interprocedural-roadmap.md](interprocedural-roadmap.md): карта отвечает «что и +> когда», это ТЗ — «что именно, как и с какими инвариантами». Из §2–§4 напрямую +> выделяется `spec/Inference.md` (этап 0 карты). Всё описанное «как есть» сверено +> с кодом на коммите `adc1496`; каждое правило несёт ссылку `файл:строка`. +> Расхождение D1 (§3) **воспроизведено исполнением**, не выведено из чтения. + +## 1. Объект: слой — это три компонента, у каждого свой дом + +| # | Компонент | Вход → выход | Код сегодня | Дом в Rust (P-022) | +|---|---|---|---|---| +| A | Деривация скелетов | `functions[]`-факты → `MethodSkeleton` | `ownir.py:1415` `_build_skeletons` + walkers (`_param_signals:1305`, `_forward_targets:1333`), merge `:1388` | `own-bridge` | +| B | Решатель | скелеты → `MethodSummary` (MOS) | `ownership.py:246` `solve_with_log` | `own-bridge` (чистый модуль) | +| C | Применение | MOS → `consume`/`borrow`/`acquire`/`alias_join` на call-site | `_lower_fn_params:1529`, call-handler `_lower_flow:1819`, `_callee_returns_fresh:1276` | `own-bridge` | + +P-022 уже закрепил: всё это — крейт `own-bridge` (facts→AST lowering, MOS, +hoisting, `check_facts`); типы фактов — `own-ir`; зависеть от `own-bridge` могут +только entry-point-крейты (`own-cli`, будущие `own-lsp`/`own-capi`). Тела +`functions[].body` в `own-ir` **сознательно нетипизированы** («the bridge's +concern») — значит, закрытый enum флоу-опов обязан появиться в `own-bridge` +(см. INV11). + +## 2. Нормативная семантика «как есть» (база для `spec/Inference.md`) + +### 2.1 Решётка Transfer + +Элементы `no | must | may | unknown` (`ownership.py:46`). Join (`:61`): +`join(a,a)=a`; `unknown` поглощает; любая иная смесь → `may`. +Дно ⊥ (`None`) — только посев фикспойнта (`:164-173`): идентичность join'а, +никогда не покидает решатель, финализируется в `no` («никто доказуемо не +потребил ⇒ оставлен/одолжен», `:325-327`). + +### 2.2 Вклад пути (contrib, `ownership.py:290`) + +`dispose | adopt | return` → `must`; `borrow` → `no`; `forward(callee,arg)` → +`lookup`; нераспознанный kind → `unknown` (fail closed). Пустой список путей → +`no` (`:303`). `lookup` (`:270`): extern-callee → `unknown` + запись в лог +строкой `"{callee}#{arg} (extern, no summary)"`; отсутствующий у callee индекс → +`unknown` без лога; недиспозабельный параметр → `no`; решённый — финал; свой +SCC — текущая итерация (возможно ⊥); недостижимая ветка → `unknown` fail-closed +(`:288`). + +### 2.3 Деривация скелета параметра (S-правила, `ownir.py:1444-1494`) + +- **S1** Явный `effect` в факте — авторитет: `consume`→`[dispose]`, + `borrow|borrow_mut`→`[borrow]`, иная строка→`[]` (не-владеющий). Инференция + никогда не оспаривает явный контракт. +- **S2** Иначе — по сигналам `(rel, passed, used)` (`_param_signals`, рекурсия в + `if`/`while`), с приоритетом: `rel`→`[dispose]` (⚠ D1); + иначе `passed`→ forward-рёбра всех вызовов, и если НЕ (ровно одно ребро всего + ∧ ровно одно на верхнем уровне) — добавить `[borrow]`, чтобы join дал + `may`/`no`, а не ложный `must` (`:1482-1486`); иначе `used`→`[borrow]`; + иначе `[]`. +- **S3** Forward в sink-extern резолвится на месте (`_forward_path_action:1361`): + `$consume`→`dispose`, `$borrow`→`borrow`; `$borrow_mut` **сознательно + отсутствует** в `_SINK_PATH_ACTION:1192` — остаётся forward-ребром к + несуммаризируемому → `unknown` → параметр обёртки plain (INV5, трекер #122). +- **S4** Ось `escapes` скелета существует, но деривация её **не заполняет** + (всегда `False`) — см. D2. + +### 2.4 Деривация return-скелета (R-правила, `_infer_return_skeleton:1098`) + +- **R1** Нет `return ` → `none`. +- **R2** Есть хоть один bare `return` / `return null` → `none`, никакой заявки + (не «равномерно fresh»). +- **R3** `fresh` ⇔ **каждый** возвращаемый var: acquired в этом теле ∧ не + параметр ∧ нигде не результат `call` (смешанное происхождение — деградация). +- **R4** Ровно один возвращаемый var, он результат `call`, не параметр, не + acquired: callee first-party → `forward(callee)` (Tier A разрешит); иначе + BCL-fresh (`_is_bcl_fresh_factory`) → `fresh` (тонкая обёртка над фабрикой); + иначе `forward(callee)`. +- **R5** Всё остальное → `none` (недоказуемо ⇒ нет заявки). + +### 2.5 Слияние перегрузок (M-правила, `_merge_skeletons:1388`, `_merge_returns:1372`) + +- **M1** Группировка по сырому имени `{Type}.{Method}`. По параметрам — union + индексов; перегрузка, ничего не делающая с индексом, вносит `[borrow]` + («держит»), так что join даёт `must` только при единогласии. +- **M2** Return: `{fresh}`→`fresh`, `{none}`→`none`, `{aliased}`→`aliased`; + любая смесь / `forward` / `aliasOf` в группе → `unknown` (fail closed — + `aliasOf`-индекс перегрузко-специфичен). +- **M3** Прямой вызов перегруженного имени: `Call` в ядро **не** эмитится + (сигнатурная таблица ядра last-wins — применила бы контракт одной перегрузки); + вместо этого merged-контракт по-аргументно через канал + `_CHANNEL_FOR_TRANSFER:1197` (`must`→`$consume`, `no`→`$borrow`, + `may|unknown`→ничего) — `ownir.py:1838-1851`. + +### 2.6 Решатель (F-правила, `ownership.py:246-395`) + +- **F1** Граф: рёбра M→C по forward-путям параметров и forward-return, только в + пределах множества скелетов (`_call_graph:231`). +- **F2** SCC — итеративный Тарьян, смежность отсортирована ⇒ детерминизм и + reverse-topological порядок «callee раньше caller» (`:176-228`). +- **F3** Пофикспойнтно на SCC: посев ⊥ по (метод, дисп. параметр), наивная + итерация до неподвижной точки (решётка высоты 3 — сходится быстро), ⊥ + финализируется `no`. Именно посев ⊥ (а не `no`) делает рекурсию точной: + dispose в базовом случае даёт `must` через весь SCC. +- **F4** Дубликат ключа скелета → `ValueError` немедленно (`:264`) — last-wins + коррумпировал бы граф и сделал результат зависимым от порядка входа. +- **F5** Return-цепочки: итеративная мемоизированная прогонка (не рекурсия — RE: + глубокая цепочка обёрток не должна ронять решатель, см. F6); цикл → `unknown`; + extern → `unknown` + лог; **`aliasOf:i` на хопе → `unknown`** — переиндексация + требует карту аргументов вызова, которой скелет не несёт (`:373-380`, D4); + нераспознанный терминальный kind → `unknown`, никогда «none» (`:346`). +- **F6** Контракт сбоя: мост оборачивает `solve(_build_skeletons(...))` в + `except Exception: mos = {}` (`ownir.py:906-909`) — деградация к пустому MOS + для **всех** методов, молча (⚠ D5). Отсюда правило: любой отказ решателя + на одном методе не смеет быть исключением (иначе гаснет весь слой). +- **F7** Лог unresolved — только extern-границы, отсортирован; внутренние + деградации (цикл, aliasOf-хоп, отсутствующий индекс) детерминированы от входа + и не логируются. + +### 2.7 Применение на call-site (A-правила) + +- **A1** Параметры функции: явный `effect` > инференция; для `passed`-параметра + решённый transfer: `must`→`consume`, `no`→`borrow`, `may|unknown`→plain + (`_infer_param_effect:1500`, `_lower_fn_params:1545-1559`). +- **A2** Перегруженное имя → M3-канал. +- **A3** Иначе `Call` эмитится только для резолвимого callee (есть summary или + sink-extern) — нерезолвимые дропаются без заявки и без OWN040-крэша + (`:1852-1861`). +- **A4** Ребинд результата **убивает** прежнее обязательство локала + (`localmap.pop`, `:1874`), кроме hoisted-локалов; потерянное обязательство + читается как утечка, не как чистота. +- **A5** Fresh-результат минтит `acquire` (`:1876-1883`); + `_callee_returns_fresh:1276` — **единственный** источник истины о freshness, + разделяемый leak-pre-scan'ом, hoist-safety-обходом и lowering'ом (INV9): + Tier A авторитетен (summary есть → верим его `returns`); first-party без + summary → `False` (сброшенная перегрузка не получает Tier B); только чужой + callee → таблица `_BCL_FRESH_BY_NS:1216` (точная идентичность bare + `Type.Method` или FQN под родным namespace; `global::` канонизируется на + обеих сторонах, `:1254`). +- **A6** `alias_join` над неотслеживаемым `src` — молчание (must-only alias, + d5 §11). +- **A7** Branch-hoist (`_hoisted_branch_locals` + `_branch_hoist_safe:1574`) — + условный acquire поднимается на верхний скоуп только под гейтом + definite-assignment; известные ограничения — xfail-замки `nested_branch`, + `loop_acq`, `guard` (лучше громкий OWN030, чем тихая ложь). + +## 3. Расхождения нормы и кода — решения, которые ТЗ обязано принять + +### D1 (подтверждено исполнением): release на любом пути ⇒ `consume` — фабрикует OWN002/OWN001 + +Дизайн-нота (d5 §1) определяет `must` как «released on **all** normal-return +paths», но S2 коллапсирует сигнал в булев: `_param_signals` рекурсивно засчитывает +release **на любом пути**, и деривация кладёт единственный путь `[dispose]` без +join'а с не-освобождающей веткой. Репро (проверено на `adc1496`): + +```python +# callee: if c: release x (else: ничего) ; caller: acquire r; call(r); release r +check_facts(...) # → +# OWN001 t.cs:1 'x' may not be disposed on every path (в callee — от ложного consume) +# OWN002 t.cs:10 'r' is used after it is disposed (в caller — ЛОЖНЫЙ: его +# защитный Dispose() наказан контрактом, которого не было) +``` + +Контроль с безусловным release даёт тот же OWN002 — там он легитимен (T2 +double-dispose и существует ради этого). Значит, класс FP: любой idiom +«условный/защитный dispose чужого аргумента» (`if (x != null) x.Dispose()` в +хелпере) на уровне фактов ⇒ ложный OWN002 у аккуратного вызывающего + ложный +OWN001 в самом хелпере. Это удар ровно по полу `own-only 0`. + +**Решение (принять до порта — иначе bit-parity заставит Rust воспроизводить +баг как норму):** + +- **Вариант A (рекомендуемый): ветко-чувствительная деривация release.** + Release на всех путях → `[dispose]`; на части путей → `[dispose, borrow]` + (join ⇒ `may` ⇒ plain на call-site — молчание); прямая инференция + `_infer_param_effect` возвращает `consume` только при all-paths-release. + Требует заменить булев `rel` на пер-ветвевой обход (walkers сегодня плоские). + Цена по recall: защитные dispose-хелперы уходят из `consume` в plain — это + движение **к** точности, в духе проекта. Чинить в Python сейчас, осознанно + двинув паритет-таргет (roadmap §2, оговорка), с обновлением golden-сводок. +- **Вариант B (если A откладывается): узаконить as-is в спеке** + возложить на + экстрактор обязательство не оборачивать null-guard-dispose в `if`-оп + (нормировать `x?.Dispose()`/`if(x!=null) x.Dispose()` в плоский `release`). + Дёшево, но хрупко: негласное правило для каждого будущего фронтенда, и + синтетические OwnIR-факты останутся ловушкой. Годится только как временная + фиксация с трекером. + +**Тест-матрица к D1:** условный release (silent при A); безусловный (consume, +OWN002 у переиспользующего вызывающего — сохранить); release в обеих ветках +`if/else` (= all paths ⇒ consume); release в `while`-теле (zero-trip ⇒ НЕ +all-paths ⇒ may); release + throw-ветка (по политике `--flow-locals`). + +### D2: ось `escapes` мертва + +`ParamSkeleton.escapes` есть в модели (d5 §1 требует «отдельную ось»), но +деривация никогда её не ставит, и `ParamSummary.escapes` всегда `False`. +Потребителя сегодня нет — но сериализация `to_dict` её **эмитит**, т.е. дамп +сводок (этап 1) вморозит ложь в паритетный артефакт. Решение: либо заполнять +(экстрактор уже считает эскейпы для своих нужд), либо исключить из дампа v0 и +пометить в спеке «reserved». Не оставлять как есть. + +### D3: `adopt`/`return` — вклады без продюсера + +`contrib` понимает `adopt` и `return` как `must`, но деривация их не эмитит +(adopt — T4b-межпроцедурный, return-of-param — сознательно не консьюм, +`:1510-1513`). В спеке пометить оба kind'а «reserved, производитель отсутствует» +— иначе порт унесёт мёртвую семантику как живую. + +### D4: `aliasOf` гаснет на первом же хопе forward-цепочки + +Документированная деградация (`ownership.py:373-380`). В спеку — как правило, +в ТЗ этапа 3 (§6.2) — как ограничение первого среза: применение `aliasOf:i` +только на прямом вызове, без переиндексации через цепочку. + +### D5: сбой решателя молчит + +`except Exception: mos = {}` (`ownir.py:906-909`) гасит **весь** межпроцедурный +слой без следа — против культуры honest-skip (OWN050). Решение: деградация +остаётся (никогда не ронять чекер), но становится наблюдаемой — OWN050-класс +advisory «interprocedural summaries unavailable: » + счётчик в `--stats`. +Требование к Rust-порту: то же поведение через `Result`, не через панику +(clippy `panic="deny"` это уже гарантирует). + +## 4. Инварианты слоя (нарушение любого — блокер ревью) + +- **INV1 Пол точности.** Никакое правило не смеет фабриковать `must`/`fresh`/ + alias. Каждый PR в слой несёт явный ответ: «может ли это изменение породить + ложный OWN001/002/003?» (D1 — прецедент того, что бывает без этого вопроса.) +- **INV2** `unknown` поглощает; ⊥ — только посев, наружу не выходит, + финализируется `no`. +- **INV3** Дубликат ключа скелета — громкий отказ, не last-wins (F4). +- **INV4** Tier A > Tier B всегда, включая методы без summary (сброшенные + перегрузки): first-party имя глушит BCL-таблицу. +- **INV5** `$borrow_mut` не суммаризируется транзитивно, пока у решётки нет оси + эксклюзивности (#122): обёртка остаётся plain, прямой вызов сохраняет + эксклюзивность. +- **INV6** Ребинд убивает обязательство; потерянное обязательство = утечка, не + чистота. +- **INV7** Map-or-raise (OWN030) не смягчать — он ловит дрейф lowering'а. +- **INV8 Детерминизм от входа.** Никакой зависимости результата, порядка находок + или лога от порядка хеш-итерации: смежность сортируется, лог сортируется, + любые выходные коллекции — с закреплённым порядком. +- **INV9** `_callee_returns_fresh` — единственный источник истины о freshness + для pre-scan/hoist/lowering; три потребителя не смеют разойтись. +- **INV10** Сбой решателя → пустой MOS у всех + наблюдаемый след (после D5); + никогда не крэш чекера. +- **INV11 Закрытый словарь опов.** Walkers имеют право игнорировать только опы, + не несущие владения; любой оп, способный **спрятать** `release`/`acquire`/ + `call` (будущий `try`/`using`), обязан сначала упасть в fail-loud `_lower_flow` + (N1-гейт) — то же тело лоуэрится всегда, поэтому скелет не успевает соврать. + В Rust: типизировать флоу-опы закрытым enum в `own-bridge` с отказом на + неизвестный `op` при десериализации — гарантия становится структурной. +- **INV12 Паритет текстов.** Все строки, достигающие вывода (unresolved-лог, + коды, сообщения, дамп сводок), — byte-exact, закреплены общими фикстурами + (образец: `syntax_parity.json`). + +## 5. ТЗ на Rust-порт слоя (`own-bridge`) + +### 5.1 Отображение типов + +`Transfer` → `enum` + serde `rename_all="lowercase"`; ⊥ → `Option` +(только внутри фикспойнта); `PathAction` → enum с payload +`Forward { callee: Sym, arg: u32 }`; `ParamKey` → `(Sym, u32)`; строки — +интернированные символы (`lasso`, по перф-принципам P-022). Дамп сводок обязан +сериализоваться в формат, байт-в-байт равный Python `to_dict` (после +канонизации sorted-keys). + +### 5.2 Детерминизм (расшифровка INV8 для Rust) + +`FxHashMap` внутри допустим; **любой итерируемый выход** — `BTreeMap` или +сортировка на эмиссии: множество скелетов, смежность SCC (Python сортирует — +`ownership.py:198,208`), unresolved-лог (`:395`), порядок сводок в дампе, +порядок находок (P-022: «pin intra-tie ordering»). Правило ревью: `for` по +хеш-коллекции, результат которого достигает вывода, — дефект. + +### 5.3 Политика ошибок + +Без паники (workspace-линты уже `panic="deny"`, `unwrap_used="deny"`). +Решатель возвращает `Result`; вызывающий деградирует к пустому MOS + +наблюдаемый след (D5) — семантика идентична Python-стороне. Дубликат ключа — +`Err`, не паника (это данные, не инвариант программы). + +### 5.4 Паритетная сбруя (расширение `oracle_exact.py`) + +Сегодня две поверхности: `check --format sarif`, `cfg --format json` +(`oracle_exact.py:55`). Добавить **третью**: `check --dump-summaries` +(канонизированный JSON: сводки + unresolved-лог), сначала заморозив её на +Python-стороне — тот же ход, что уже сделан для CFG-шва. Снапшот-манифест +(corpus hash + reference hash) поддерживает это без доработок. Это этап 1 +карты, переквалифицированный в артефакт порта. + +### 5.5 Порядок портирования внутри слоя + +1. **Решатель** (чистый, без зависимостей): порт + property-тесты (монотонность + join, сходимость на случайных SCC, детерминизм от перестановки входа — + `proptest`), конформанс по golden-сводкам. +2. **Деривация** (S/R/M-правила) + типизация флоу-опов закрытым enum (INV11). +3. **Применение** (A-правила) — последним: сцеплено с lowering/hoisting, самая + широкая поверхность регрессий; гейт — синтетические OwnIR-фикстуры (они + языко-нейтральны: JSON → диагностики) + полный corpus. + +Каждая фаза за своим паритетным гейтом до перехода к следующей. + +## 6. ТЗ на этапы 2–4 карты (конкретика) + +### 6.1 Этап 2 — сигнатурный ключ (арность) + +- **Формат:** опциональное поле `sig` на `functions[]`-записи и `call`-опе — + канонический список типов параметров: FQ-имена, без пробелов, generic-арность + через backtick, `global::` снят. Ключ скелета = `name` + `(` + `sig` + `)`. + По политике эволюции (`spec/OwnIR.md` §2, IR-правила) опциональное поле не + бампает `OWNIR_VERSION`; продюсер без типовой информации (ownts) поле не пишет. +- **Fallback-правила (критично):** отсутствует `sig` на любой стороне ребра → + ребро резолвится по слитому-по-имени скелету (сегодняшнее поведение), никогда + не «мимо». `first_party`/`overloaded`-подавления работают по **голому имени** + независимо от `sig` — иначе Tier B-таблица выстрелит по первопартийному + callee, чей вызов пришёл без сигнатуры (INV4). +- **Тест-матрица:** перегрузки consume/borrow разных арностей (обе стороны с + `sig` — раздельные контракты); вызов без `sig` в функцию с `sig` (fallback); + смешанные продюсеры в одном факт-файле; `global::`-qualified вызов с `sig`; + регресс: uniformly-fresh перегруженная фабрика остаётся fresh при fallback. +- **DoD:** пересмотрены Tier B-исключения, введённые из-за неоднозначности + перегрузок; `_merge_skeletons` вызывается только для реально одноключевых + групп; паритетный дамп сводок расширен ключом. + +### 6.2 Этап 3 — `aliasOf:i` через return (первый срез) + +- **Деривация:** `ReturnSkeleton("aliasOf", i)` ⇔ ровно один возвращаемый var + `v`; в теле ровно один straight-line `alias_join var=v src=p`, где `p` — + параметр с индексом `i`; нет bare return; `v` не acquired и не результат + иного `call`. Любое отклонение → сегодняшняя классификация (нет заявки). +- **Решатель:** терминал уже готов (`aliasOf:`); переиндексацию через + forward-хоп **не делать** (D4 остаётся) — применение только на прямом вызове. +- **Применение:** `call callee=... args=[..., x@i, ...] result=r` с summary + `aliasOf:i` → lowering эмитит `alias_join r ← x` (готовый примитив ядра, + шаги 0–1 D5.4) вместо acquire; арг не на позиции `i` — без заявки. +- **Тест-матрица:** dispose-обёртки / dispose-внутреннего / обоих (OWN003) / + никого (один OWN001); возврат из фабрики с bare-return веткой (silent); + перегруженное имя с `aliasOf` (M2 глушит — регресс); merged-fallback без + `sig`. +- **DoD:** Dapper `DbWrappedReader.Create` и Polly-адопт — оракул-якоря + «own-only 0 с записанной причиной», кросс-линк в `field-notes-patterns.md` + (exit-criterion d5 §8). + +### 6.3 Этап 4 — #146, провенанс паблишера + +- **Гейт по видимости — жёсткий:** заявка «параметр `j` метода `M` — + сконструирован-и-возвращён вызывающим» допустима только для non-public `M` + (private; internal — только при видимой всей компиляции). Public / делегат / + рефлексия / DI-регистрация / любой не-анализируемый call-site → `injected` + как сегодня (advisory-warning остаётся честной позой). +- **Правило:** must-join по **всем** call-site'ам `M` в первопартийном + множестве: в каждом аргумент `j` — локал, который (a) acquired/fresh в + вызывающем и (b) возвращается им (`return v`). Один несоответствующий сайт → + нет заявки. Потребитель: subscription-tiering (`injected` → bounded/`local`). +- **Тест:** worked example из #146 (Newtonsoft `Create`/`ApplySerializerSettings`, + `private static` — проходит гейт); DI-singleton-двойник (`Wire(bus, s)`) — + обязан остаться warning'ом. + +## 7. Тест-план слоя (сводно) и критерии приёмки + +1. Синтетические OwnIR-фикстуры — двусторонний конформанс-набор (Python и Rust + через CLI); каждая ячейка тест-матриц §3/§6 — отдельная фикстура. +2. Golden-дампы сводок (`--dump-summaries`) в снапшотах `oracle_exact`. +3. Property-тесты решателя (обе стороны): монотонность, идемпотентность join, + сходимость, инвариантность к перестановке входа. +4. Полный corpus зелёный; оракул-якоря Dapper/Polly (§6.2), Newtonsoft (§6.3). +5. Перф — только через ратчет `iai-callgrind` (P-022), без ручных бенчей. + +Приёмка любого изменения слоя: INV1-анализ в описании PR + не сломан ни один +xfail-замок (A7) + дамп сводок диффнут и объяснён. + +## 8. Чек-лист ревью PR в слой (вешать на каждый PR) + +- [ ] Может ли изменение породить ложный `must`/`fresh`/alias? (INV1 — написать + ответ, не подразумевать) +- [ ] Все новые деградации — к молчанию, не к заявке; `unknown` не превращён в + `no`/`must` по дороге +- [ ] Выходные порядки закреплены (INV8); в Rust — нет хеш-итерации до вывода +- [ ] Tier A/B-старшинство не задето (INV4); `_callee_returns_fresh` остался + единственным судьёй (INV9) +- [ ] Тексты, достигающие вывода, — в общих фикстурах (INV12) +- [ ] Синтетическая фикстура на новую ветку поведения добавлена в обе стороны +- [ ] Паритет: golden-сводки перегенерированы осознанно (ключи манифеста + обновлены), diff в описании PR From 9860c50fb869c74cb4eb8152bfe76d96090649fe Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 16:52:09 +0000 Subject: [PATCH 04/12] fix(d5): a partial release infers `may`, not a flattened `consume` (TZ D1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The skeleton derivation and the direct contract inference collapsed the release signal to a boolean: a release on ANY path produced a lone dispose path action, so a callee that disposes a parameter conditionally (the ubiquitous null-guard dispose-helper idiom, `if (x != null) x.Dispose()`) was inferred `consume`. That flattened `must` charged a caller's defensive dispose a false OWN002 and the helper itself a false OWN001 — reproduced on synthetic facts before the fix, and a direct hit on the own-only-0 precision floor. The d5 note always defined `must` as 'released on ALL normal-return paths'; the code now matches it. `_definite_release` walks the op tree tracking the release state of live paths (released on none / some / all) plus whether every early `return` was reached already-released: release in both branches or before every exit stays a definite dispose (consume recall preserved — the careless caller keeps its true OWN002); a one-branch, in-loop (zero-trip), or guarded-by-early-return release now also emits a kept path, so the lattice joins to `may` and the caller stays plain (silent). The walk ignores only ops that cannot hide a release — anything new fails loud in _lower_flow first (IR4), so the walk can never be lied to. Six regression tests pin the matrix from the TZ: conditional release silent, both-branch consume kept, while-body release silent, early return blocks the claim, release-then-return credited, and a wrapper forwarding to a partial releaser degrading to plain transitively. Full suite green (ownir 236/236); no existing behaviour depended on the flattened consume. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-tz.md | 8 +++ ownlang/ownir.py | 85 ++++++++++++++++++++++++++-- tests/test_ownir.py | 95 ++++++++++++++++++++++++++++++++ 3 files changed, 183 insertions(+), 5 deletions(-) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index 1f20c619..c520bb90 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -143,6 +143,14 @@ SCC — текущая итерация (возможно ⊥); недостиж ### D1 (подтверждено исполнением): release на любом пути ⇒ `consume` — фабрикует OWN002/OWN001 +> **Статус: исправлено (вариант A).** Деривация release теперь ветко-чувствительна: +> `_definite_release`/`_walk_release` в `ownir.py` считают release-путём только +> освобождение на **всех** normal-return путях (early-return без release блокирует +> заявку; release-then-return засчитывается; `while`-тело — никогда не definite); +> частичный release кладёт `(dispose, borrow)` → join `may` → plain. То же правило +> — в прямой инференции `_infer_param_effect`. Матрица ниже — 6 регрессионных +> тестов в `test_ownir.py` (TZ D1). Код и нота d5 §1 теперь совпадают. + Дизайн-нота (d5 §1) определяет `must` как «released on **all** normal-return paths», но S2 коллапсирует сигнал в булев: `_param_signals` рекурсивно засчитывает release **на любом пути**, и деривация кладёт единственный путь `[dispose]` без diff --git a/ownlang/ownir.py b/ownlang/ownir.py index ff6cac15..cc164b51 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -1330,6 +1330,62 @@ def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]: return rel, passed, used +def _walk_release(pname: str, nodes: Any, rel_in: int) -> tuple[int, bool, bool]: + """Definite-release walk over one op sequence, for `_definite_release`. + + Returns `(rel_out, falls_through, exits_ok)`: `rel_out` is the release state + of the paths leaving the sequence bottom (0 = released on none, 1 = on some, + 2 = on all), `falls_through` is whether any path reaches the bottom at all, + and `exits_ok` is whether every `return` op seen so far was reached with the + param already released. Ops that cannot affect or bypass a release are + neutral by design: a compound op that COULD hide one (a future `try`/`using`) + fails loud in `_lower_flow` first (the IR4 gate), so this walk never sees it.""" + rel = rel_in + exits_ok = True + if not isinstance(nodes, list): + return rel, True, exits_ok + for n in nodes: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == "release" and str(n.get("var")) == pname: + rel = 2 + elif op == "return": + # a normal-return path ends here carrying the current state; the rest + # of THIS sequence is unreachable. + return rel, False, exits_ok and rel == 2 + elif op == "if": + rt, lt, okt = _walk_release(pname, n.get("then"), rel) + re_, le, oke = _walk_release(pname, n.get("else"), rel) + exits_ok = exits_ok and okt and oke + if lt and le: + rel = rt if rt == re_ else 1 + elif lt or le: + rel = rt if lt else re_ + else: + return rel, False, exits_ok # both branches returned + elif op == "while": + rb, lb, okb = _walk_release(pname, n.get("body"), rel) + exits_ok = exits_ok and okb + # zero-trip entry joins with a completed iteration's exit state: a + # release inside a loop is never definite for the fall-through. A + # body that never completes (always returns) leaves only the + # zero-trip path, so the entry state stands. + if lb and rb != rel: + rel = 1 + return rel, True, exits_ok + + +def _definite_release(pname: str, nodes: Any) -> bool: + """True only when EVERY normal-return path through the body releases `pname` + — the d5 note's `must` ("released on all normal-return paths"). A partial + (one-branch / in-loop / guarded-by-early-return) release must join to `may` + instead: flattening it to `consume` charges a caller's defensive dispose a + false OWN002 and the helper itself a false OWN001 (TZ D1, reproduced).""" + rel, falls_through, exits_ok = _walk_release(pname, nodes, 0) + return exits_ok and (not falls_through or rel == 2) + + def _forward_targets(pname: str, nodes: Any, recurse: bool = True) -> list[tuple[str, int]]: """Every `(callee, arg_index)` a `call` op hands `pname` to. The argument @@ -1421,11 +1477,17 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: bridge's local inference on the non-forward cases and only *resolves* the forwarded one. - Two precision rules keep `solve()` from ever inferring a false `must` (which + Three precision rules keep `solve()` from ever inferring a false `must` (which would upgrade a caller to `consume` and fabricate OWN002/OWN001): - an **explicit** `effect` seeds the skeleton (it is a documented override — `consume`→`dispose`, `borrow`/`borrow_mut`→`borrow`, anything else owns nothing), so a contract-only callee resolves correctly even with no body; + - a release counts as a `dispose` path alone only when it is **definite** — + on every normal-return path (`_definite_release`). A partial release + (one branch / in a loop / behind an early return) also emits a kept + (`borrow`) path, so the join is `may` and the caller stays plain — a + flattened `must` would charge a defensive caller-side dispose a false + OWN002/OWN003 (TZ D1); - a forward is resolved only when it is a **single, unconditional, straight-line** handoff. A conditional / looped / multi-target forward also emits a non-transfer (`borrow`) path, so the lattice yields `may`/`no` @@ -1474,7 +1536,15 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: else: rel, passed, used = _param_signals(cname, body) if rel: - paths = (PathAction("dispose"),) + if _definite_release(cname, body): + paths = (PathAction("dispose"),) + else: + # released on SOME paths only (TZ D1): a kept path exists, + # so record it beside the dispose and let the lattice join + # yield `may` — the caller stays plain, never a flattened + # `must` that would charge its defensive dispose a false + # OWN002/OWN003. + paths = (PathAction("dispose"), PathAction("borrow")) elif passed: allt = _forward_targets(cname, body) top = _forward_targets(cname, body, recurse=False) @@ -1501,8 +1571,11 @@ def _infer_param_effect(pname: str, nodes: Any, forward_transfer: Transfer | None = None) -> str | None: """Infer a parameter's ownership CONTRACT from the callee's OWN body — the bounded inter-procedural step that lets first-party C# be checked without - annotating every method. A param the body discharges (release) is CONSUME - (ownership taken and discharged); one only read and retained is a BORROW (the + annotating every method. A param the body discharges (release) on EVERY + normal-return path is CONSUME (ownership taken and discharged); a partial + release (one branch / in a loop / behind an early return) is `may` and stays + plain — flattening it to consume would charge a caller's defensive dispose a + false OWN002 (TZ D1). One only read and retained is a BORROW (the caller keeps ownership, must still release). A param handed to another call used to be ambiguous and stay plain; **P-005 D5.1** resolves it through the call graph: `forward_transfer` is the solved transfer of that param (must → @@ -1514,7 +1587,9 @@ def _infer_param_effect(pname: str, nodes: Any, fact always wins over inference.""" rel, passed, used = _param_signals(pname, nodes) if rel: - return "consume" + if _definite_release(pname, nodes): + return "consume" + return None # released on SOME paths only -> `may` -> plain (TZ D1) if passed: if forward_transfer == Transfer.MUST: return "consume" diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 55f996f1..46f5d8a1 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1498,6 +1498,101 @@ def _sub(source: str | None) -> list[Finding]: if cond: gotc = [(x.component, x.code) for x in cond] fails.append(f"D5.1 conditional forward must be `may`: caller stays silent, got {gotc}") + # (TZ D1) a CONDITIONAL release joins to `may`, not a flattened `consume`: + # `cond_rel(x){ if(c) release x; }` keeps x on the other path, so a caller that + # disposes defensively after the call stays SILENT. Before the fix the inferred + # consume charged that caller a false OWN002 and the helper a false OWN001 — + # the null-guard-dispose-helper idiom read as two findings. + checks += 1 + d1c = check_facts({"module": "M", "functions": [ + {"name": "cond_rel", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "careful", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "cond_rel", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + if d1c: + fails.append("TZ D1: a partial release must join to `may` (caller silent), " + f"got {[(x.component, x.code) for x in d1c]}") + # (TZ D1) release in BOTH branches IS all-paths: consume survives, and the + # careless caller keeps its true OWN002 — the refinement costs no recall here. + checks += 1 + d1b = check_facts({"module": "M", "functions": [ + {"name": "both_rel", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], + "else": [{"op": "release", "var": "x", "line": 4}]}]}, + {"name": "reuse_b", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "both_rel", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + gotd1b = [(x.component, x.line, x.code) for x in d1b] + if gotd1b != [("reuse_b", 10, "OWN002")]: + fails.append("TZ D1: an all-paths (both-branch) release is still consume, " + f"got {gotd1b}") + # (TZ D1) a release inside a `while` body is never definite (zero-trip): plain. + checks += 1 + d1w = check_facts({"module": "M", "functions": [ + {"name": "loop_rel", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "while", "line": 2, + "body": [{"op": "release", "var": "x", "line": 3}]}]}, + {"name": "loop_user", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "loop_rel", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + if d1w: + fails.append("TZ D1: a while-body release is zero-trip-partial (caller " + f"silent), got {[(x.component, x.code) for x in d1w]}") + # (TZ D1) an early `return` on an unreleased path blocks the definite claim: + # `guard(x){ if(c) return; release x; }` does not release on the guard path. + checks += 1 + d1g = check_facts({"module": "M", "functions": [ + {"name": "guard_rel", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, "then": [{"op": "return", "line": 3}], + "else": []}, + {"op": "release", "var": "x", "line": 4}]}, + {"name": "guard_user", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "guard_rel", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + if d1g: + fails.append("TZ D1: an early-return-unreleased path blocks consume (caller " + f"silent), got {[(x.component, x.code) for x in d1g]}") + # (TZ D1) release-then-return in a branch plus a fall-through release IS + # all-paths — the walk credits a released early exit, so consume survives. + checks += 1 + d1rr = check_facts({"module": "M", "functions": [ + {"name": "rel_ret", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}, + {"op": "return", "line": 4}], + "else": []}, + {"op": "release", "var": "x", "line": 5}]}, + {"name": "rel_ret_user", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "rel_ret", "args": ["r"], "line": 11}, + {"op": "use", "var": "r", "line": 12}]}]}) + gotrr = [(x.component, x.line, x.code) for x in d1rr] + if gotrr != [("rel_ret_user", 10, "OWN002")]: + fails.append("TZ D1: release-then-return + fall-through release is all-paths " + f"consume, got {gotrr}") + # (TZ D1) a wrapper forwarding to a partial releaser inherits `may` through the + # solver — the transitive claim degrades to plain (silence) too. + checks += 1 + d1f = check_facts({"module": "M", "functions": [ + {"name": "cond_rel2", "file": "D.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "via", "file": "D.cs", "params": [{"name": "s", "line": 6}], + "body": [{"op": "call", "callee": "cond_rel2", "args": ["s"], "line": 7}]}, + {"name": "via_user", "file": "D.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "via", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + if d1f: + fails.append("TZ D1: forwarding to a partial releaser must stay plain " + f"(caller silent), got {[(x.component, x.code) for x in d1f]}") # (§10 q2) same-name OVERLOADS are merged, not dropped: when EVERY overload of a # name consumes the forwarded arg, a forward to that name resolves to `must`, so a # caller using the local after the handoff is OWN002. Before the merge the name was From b5c0bd4b6642c2b5cd7c2a0fe78c037fa910b95a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:04:49 +0000 Subject: [PATCH 05/12] =?UTF-8?q?feat(d5):=20OWN052=20=E2=80=94=20a=20fail?= =?UTF-8?q?ed=20MOS=20solve=20degrades=20observably,=20not=20silently=20(T?= =?UTF-8?q?Z=20D5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The bridge wraps the interprocedural summary solve in a blanket 'except Exception: mos = {}': the right call (never crash the checker), but it put the ENTIRE interprocedural layer out silently — every cross-method consume/borrow/fresh contract skipped with no trace, against the honest-skip culture every other coverage gap follows (OWN050). to_module now takes an optional notes out-list (the loc-counter house pattern) and records the degrade reason; check_facts surfaces each as an advisory OWN052 finding — file-level (no single C# site failed), module-scoped, advisory like OWN050: rendered as a warning, level:note in SARIF (region omitted for line 0), never the exit code. The __main__ summary names the advisory codes actually present instead of the hard-coded '(OWN050)' label — byte-identical output when only OWN050 notes exist. 'explain OWN052' answers with the long form. Tests: a patched-to-raise solver yields exactly one OWN052 and zero fabricated verdicts (forwards degrade to plain, the caller stays silent); the same facts with a healthy solver carry no OWN052 and keep their true OWN002. No real facts input can make solve() throw today — which is exactly why the silent except went unnoticed. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-tz.md | 9 ++++++++ ownlang/__main__.py | 5 ++++- ownlang/diagnostics.py | 9 ++++++++ ownlang/ownir.py | 33 +++++++++++++++++++++++----- tests/test_ownir.py | 37 ++++++++++++++++++++++++++++++++ 5 files changed, 87 insertions(+), 6 deletions(-) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index c520bb90..2b4fac92 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -224,6 +224,15 @@ advisory «interprocedural summaries unavailable: » + счётчик в `- Требование к Rust-порту: то же поведение через `Result`, не через панику (clippy `panic="deny"` это уже гарантирует). +> **Статус: исправлено.** Новый advisory **OWN052** («interprocedural summary +> inference failed — method summaries skipped»): `to_module` принимает +> опциональный `notes`-аут-лист, `check_facts` поднимает каждую причину как +> file-level advisory (никогда не rc), сводка `__main__` называет реальные коды +> advisory-нот вместо жёсткого «(OWN050)» (байт-в-байт совместимо, когда есть +> только OWN050). `explain OWN052` отвечает; SARIF — `level: note` без region. +> Тесты: сломанный решатель → ровно один OWN052 и ноль сфабрикованных +> вердиктов; здоровый — ноль OWN052, прежний OWN002 на месте. + ## 4. Инварианты слоя (нарушение любого — блокер ревью) - **INV1 Пол точности.** Никакое правило не смеет фабриковать `must`/`fresh`/ diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 900d6d04..f901502d 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -351,8 +351,11 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error", n = len(leaks) summary = f"\n{n} finding{'s' if n != 1 else ''}" if notes: + # name the advisory codes actually present (OWN050, OWN052, ...): with only + # OWN050 notes this renders byte-identically to the historical fixed label. + note_codes = ", ".join(sorted({f.code for f in notes})) summary += (f" ({len(notes)} unchecked hidden)" if verbosity == "quiet" - else f", {len(notes)} unchecked (OWN050)") + else f", {len(notes)} unchecked ({note_codes})") print(summary + ".", file=summary_to) if verbosity == "verbose" and findings: by_code: dict[str, int] = {} diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 6b803b92..317f5ad6 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -80,6 +80,7 @@ class Severity(Enum): "OWN041": "call argument mismatch", # ---- C# front-end resolution coverage (P-014; advisory) ---- "OWN050": "declaring type unresolved -- leakage analysis skipped", + "OWN052": "interprocedural summary inference failed -- method summaries skipped", # ---- DI container lifetimes (P-006; emitted by the OwnIR bridge) ---- "DI001": "captive dependency: a shorter-lived service is captured by a longer-lived one", "DI002": "singleton captures a scoped service (captive dependency)", @@ -151,6 +152,14 @@ class Severity(Enum): "Fix (to check it): give the extractor the type's assembly via `--ref-dir ` so the " "SemanticModel can bind the event." ), + "OWN052": ( + "Advisory, not a leak verdict: computing the method ownership summaries (the " + "interprocedural pass that resolves cross-method ownership transfer) failed, so the " + "bridge degraded to intraprocedural checking only for this run — every cross-method " + "consume/borrow/fresh contract was skipped, not guessed. It never fails a build.\n" + "Fix: this indicates malformed `functions[]` facts or a bridge bug — re-extract the " + "facts, and report the message's inner error if it persists." + ), "DI002": ( "A singleton captures a scoped service: the scoped instance is pinned to the singleton " "for the whole app lifetime, defeating per-scope (e.g. per-request) semantics and often " diff --git a/ownlang/ownir.py b/ownlang/ownir.py index cc164b51..dcd33acc 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -780,14 +780,17 @@ def _prelude_resources() -> list[ResourceDecl]: ] -def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]]: +def to_module(facts: dict[str, Any], + notes: list[str] | None = None) -> tuple[Module, dict[str, dict[str, Any]]]: """Build the core `Module` AST **directly** from OwnIR facts — no `.own` source text and no re-parse (P-016 B0a; the round-trip `to_own` + `parse` has existed since P-001). Mirrors `to_own`'s lowering exactly: each owned-resource fact becomes `let = acquire ();`, with a `release` iff the extractor found a matching teardown. Returns the Module plus the handle->fact map; a diagnostic names a handle via its symbol `origin` (`#`, - cfg.py), which maps straight back to the C# location.""" + cfg.py), which maps straight back to the C# location. `notes`, when given, + collects coverage-degradation reasons (a failed MOS solve — TZ D5) the caller + should surface as advisory findings rather than lose.""" handles: dict[str, dict[str, Any]] = {} functions: list[FnDecl] = [] gid = 0 @@ -902,11 +905,16 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] # D5.1: resolve interprocedural ownership transfer once, up front, so a # forwarded `consume`/`borrow` param is checked compositionally (the give-up # case `_infer_param_effect` used to leave plain). Never let summary - # computation crash the bridge — degrade to no-MOS (the old behaviour). + # computation crash the bridge — degrade to no-MOS (the old behaviour) — + # but the whole interprocedural layer going dark must be OBSERVABLE, not + # silent (honest-skip; TZ D5): record the reason for the caller to surface + # as an advisory OWN052. try: mos: dict[str, Any] = solve(_build_skeletons(raw_fns)) - except Exception: + except Exception as exc: mos = {} + if notes is not None: + notes.append(f"{type(exc).__name__}: {exc}") # every first-party method name: the Tier B BCL table must never fire for a callee we # compiled from source — Tier A is authoritative even with no usable summary # (CodeRabbit). Threaded into the freshness checks so direct calls agree with the @@ -2035,7 +2043,8 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: # a module-level cycle (ownir is a leaf consumer). from .__main__ import check_module - mod, handles = to_module(facts) + mos_notes: list[str] = [] + mod, handles = to_module(facts, mos_notes) diags = check_module(mod) # registration site of each DI service, to anchor a subscription-escape slice's @@ -2276,6 +2285,20 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: # this side path so it bypasses the ERROR-only diagnostic mapping above. findings.extend(_unresolved_findings(facts)) + # OWN052 (TZ D5): the MOS solve failed and the bridge degraded to no-MOS, so + # EVERY cross-method ownership contract was skipped this run. Same honest-skip + # posture as OWN050 — a coverage note, never a verdict, never the exit code. + # Anchorless by nature (no single C# site failed): file-level, module-scoped. + module_name = str(facts.get("module", "?")) + for reason in mos_notes: + findings.append(Finding( + file="?", line=0, code="OWN052", component=module_name, + event="", handler="", + message=(f"interprocedural summary inference failed ({reason}); " + f"method summaries skipped — cross-method ownership " + f"transfer was not checked this run"), + kind="method summaries", advisory=True)) + # A resource that leaks on more than one exit yields one core OWN001 per exit: # e.g. the try-lowering injects an exceptional exit before each may-throw # statement, so a local never disposed leaks on BOTH that exit and the normal diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 46f5d8a1..2cf0e4c7 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1593,6 +1593,43 @@ def _sub(source: str | None) -> list[Finding]: if d1f: fails.append("TZ D1: forwarding to a partial releaser must stay plain " f"(caller silent), got {[(x.component, x.code) for x in d1f]}") + # (TZ D5) a failed MOS solve must degrade OBSERVABLY: the bridge drops to + # no-MOS (checker stays alive, forwards stay plain — no fabricated verdicts) + # and surfaces ONE advisory OWN052 naming the inner error. Before the fix the + # whole interprocedural layer went dark silently. Patch the solver to raise — + # no real facts input can make it throw today, which is exactly why the silent + # `except` was never noticed. + checks += 1 + import ownlang.ownir as _oi + _mos_facts = {"module": "Dark", "functions": [ + {"name": "sink3", "file": "S.cs", + "params": [{"name": "x", "line": 1}], + "body": [{"op": "release", "var": "x", "line": 2}]}, + {"name": "hand", "file": "S.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "sink3", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]} + _real_solve = _oi.solve + def _boom(_sk): # type: ignore[no-untyped-def] + raise RuntimeError("synthetic solver failure") + _oi.solve = _boom # type: ignore[assignment] + try: + dark = check_facts(_mos_facts) + finally: + _oi.solve = _real_solve + gotdark = [(x.code, x.component, x.advisory) for x in dark] + if gotdark != [("OWN052", "Dark", True)] or \ + "synthetic solver failure" not in dark[0].message: + fails.append("TZ D5: a failed solve must yield exactly one advisory OWN052 " + f"(and no fabricated verdicts), got {gotdark}") + # ... and the SAME facts with a healthy solver carry no OWN052 — the consume + # resolves interprocedurally again and the careless caller's OWN002 is back. + checks += 1 + lit = check_facts(_mos_facts) + gotlit = [(x.component, x.line, x.code) for x in lit] + if gotlit != [("hand", 10, "OWN002")]: + fails.append("TZ D5: healthy solve must carry no OWN052 and keep the true " + f"OWN002, got {gotlit}") # (§10 q2) same-name OVERLOADS are merged, not dropped: when EVERY overload of a # name consumes the forwarded arg, a forward to that name resolves to `must`, so a # caller using the local after the handoff is OWN002. Before the merge the name was From 1dd9a1f0a6d2f8ac651b45e1988b27ee289bd275 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:06:50 +0000 Subject: [PATCH 06/12] fix(d5): stop serializing the unproduced `escapes` axis in MOS to_dict (TZ D2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The two-axis d5 model reserves an escape axis orthogonal to transfer, but no producer sets it: skeleton derivation always leaves False, so ParamSummary.escapes is constant False in every real run. to_dict still emitted it — and the summary dump is about to become the stage-1 Python<->Rust parity artifact, which would freeze an always-False lie into the frozen surface (and force the Rust port to reproduce a field that carries no information). to_dict now omits the field until a producer lands; the model keeps the axis (fields stay, documented RESERVED in ownership.py), and a test pins the omission so re-adding it is a deliberate act paired with the producer, not a drive-by. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-tz.md | 6 ++++++ ownlang/ownership.py | 12 ++++++++++-- tests/test_ownership.py | 6 ++++++ 3 files changed, 22 insertions(+), 2 deletions(-) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index 2b4fac92..746971a8 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -202,6 +202,12 @@ all-paths ⇒ may); release + throw-ветка (по политике `--flow-lo (экстрактор уже считает эскейпы для своих нужд), либо исключить из дампа v0 и пометить в спеке «reserved». Не оставлять как есть. +> **Статус: исправлено (вариант «reserved»).** `to_dict` больше не сериализует +> `escapes`; поля модели остаются (ось d5-дизайна), помечены RESERVED в +> докстрингах `ownership.py`; тест пиннит отсутствие ключа в дампе до появления +> продюсера. Когда продюсер появится — сериализацию вернуть вместе с ним и +> перевернуть тест. + ### D3: `adopt`/`return` — вклады без продюсера `contrib` понимает `adopt` и `return` как `must`, но деривация их не эмитит diff --git a/ownlang/ownership.py b/ownlang/ownership.py index 0bb3bbb3..98ceaaf9 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -93,7 +93,11 @@ class ParamSkeleton: name: str = "" disposable: bool = True paths: tuple[PathAction, ...] = () - escapes: bool = False # the reference outlives the call (field/collection/return) + # RESERVED axis (TZ D2): "the reference outlives the call" (field / collection + # / return). The d5 model keeps escape orthogonal to transfer, but NO producer + # sets it yet (`_build_skeletons` always leaves False) — it is carried, + # unserialized, and must not be read as evidence until a producer lands. + escapes: bool = False @dataclass(frozen=True) @@ -147,9 +151,13 @@ def to_dict(self) -> dict[str, object]: "file": self.file, "line": self.line, "source": self.source, + # `escapes` is deliberately NOT serialized (TZ D2): no producer sets + # the axis yet, so emitting it would freeze an always-False lie into + # the parity artifact this dump becomes (the roadmap's stage-1 + # Python↔Rust diff surface). Serialize it the day a producer lands. "params": [ {"index": p.index, "name": p.name, "disposable": p.disposable, - "transfer": p.transfer.value, "escapes": p.escapes} + "transfer": p.transfer.value} for p in self.params ], "returns": {"owned": self.returns}, diff --git a/tests/test_ownership.py b/tests/test_ownership.py index 42006ea8..a66017c0 100644 --- a/tests/test_ownership.py +++ b/tests/test_ownership.py @@ -237,6 +237,12 @@ def expect(cond, msg): expect(d["params"][1]["transfer"] == "no", "to_dict serializes the second param") expect(d["returns"] == {"owned": "none"}, "to_dict serializes the return") expect(d["source"] == "inferred", "to_dict defaults source to inferred") + # (TZ D2) the reserved `escapes` axis has no producer yet, so it must NOT be + # serialized — emitting an always-False field would freeze a lie into the + # parity artifact the summary dump becomes. Pin the omission until a producer + # lands (then flip this expectation together with the producer). + expect(all("escapes" not in p for p in d["params"]), + "to_dict omits the unproduced `escapes` axis (TZ D2)") # duplicate method keys must fail fast: key collision-freedom is an open design # question, and silently keeping the last would make summaries input-order From 52b9c0324a1f091b3fe9e3f4dc17dc227e52d68f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:07:42 +0000 Subject: [PATCH 07/12] docs(d5): mark the producer-less adopt/return path kinds RESERVED (TZ D3) The solver's contrib() understands adopt and return as must-transfer, but skeleton derivation never emits them (adopt awaits interprocedural T4b ctor-adopt summaries; a returned param is deliberately not a consume signal until owned return values are modelled). Without the marker a port would carry dead semantics as live and could expect them from real facts. The PathAction docstring now names both as RESERVED with each kind's activation condition. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-tz.md | 5 +++++ ownlang/ownership.py | 9 ++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index 746971a8..fa9748ef 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -215,6 +215,11 @@ all-paths ⇒ may); release + throw-ветка (по политике `--flow-lo `:1510-1513`). В спеке пометить оба kind'а «reserved, производитель отсутствует» — иначе порт унесёт мёртвую семантику как живую. +> **Статус: зафиксировано.** Докстринг `PathAction` (`ownership.py`) теперь +> явно помечает оба kind'а RESERVED с условием активации каждого (adopt — +> T4b-сводки, return — owned-return-value modelling) и указанием порту: нести +> семантику, не ожидать появления из реальных фактов. + ### D4: `aliasOf` гаснет на первом же хопе forward-цепочки Документированная деградация (`ownership.py:373-380`). В спеку — как правило, diff --git a/ownlang/ownership.py b/ownlang/ownership.py index 98ceaaf9..b32239dd 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -80,7 +80,14 @@ class PathAction: kind: `dispose` (releases it) | `adopt` (stores it into an owning field) | `return` (returns it — escapes to the caller of *this* method) | `borrow` (only reads/uses) | `forward` (passes it to `callee` at position `arg`). - The first three are ownership *leaving the caller* on that path (`must`).""" + The first three are ownership *leaving the caller* on that path (`must`). + + RESERVED kinds (TZ D3): `adopt` and `return` are understood by the solver but + have NO production producer yet — `_build_skeletons` (ownir.py) emits only + `dispose`/`borrow`/`forward`. `adopt` awaits interprocedural T4b (a ctor-adopt + summary), `return` awaits owned-return-value modelling (a returned param is + deliberately NOT a consume signal today, see `_infer_param_effect`). A port + must carry their semantics but must not expect to see them from real facts.""" kind: str callee: str = "" From c6262c051296bfe408e0be0571f2252e1c0bcb49 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:14:06 +0000 Subject: [PATCH 08/12] =?UTF-8?q?feat(d5):=20`summaries`=20verb=20?= =?UTF-8?q?=E2=80=94=20deterministic=20MOS=20dump=20(roadmap=20stage=201,?= =?UTF-8?q?=20parity=20surface)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 'python -m ownlang summaries facts.json' prints the solved Method Ownership Summaries plus the extern-boundary log as one deterministic JSON document: summaries sorted by method key, the unresolved log sorted by solve_with_log, fixed field order — byte-identical output under any functions[] input permutation (pinned by test). Two consumers, one contract: the debugging answer to 'why did this call stay plain/consume/fresh' without reading bridge code, and the frozen surface the Rust port of the inference layer will be diffed against — summary- level parity is finer than diffing final diagnostics, where an inference bug can hide behind an unrelated silence. Skeletons now carry the declaring file from the facts (merged overloads take the smallest (file, line) pair so the dump stays input-order- independent); a failed solve degrades exactly like the checking path — empty summaries with the reason in 'degraded', rc stays 0 (the surface reports state, it does not judge), rc 2 only for unreadable facts. Wiring into oracle_exact SURFACES rides with the Rust own-bridge consumer, which does not exist yet. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-roadmap.md | 9 ++--- docs/notes/interprocedural-tz.md | 10 ++++++ ownlang/__main__.py | 29 ++++++++++++++-- ownlang/ownir.py | 50 +++++++++++++++++++++++++-- tests/test_ownir.py | 50 +++++++++++++++++++++++++++ 5 files changed, 140 insertions(+), 8 deletions(-) diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md index 5cd493ec..daf558a3 100644 --- a/docs/notes/interprocedural-roadmap.md +++ b/docs/notes/interprocedural-roadmap.md @@ -149,10 +149,11 @@ the full must/may/escape evidence regardless of mode»), не хватает п - **OWN051** (OWN05x-band, как OWN050): `transfer:may` и honest-`unknown` показываются с `--verbosity normal`+, никогда не валят CI. -- **Дамп сводок**: `MethodSummary.to_dict()` уже существует (сериализация - `summaries[]` из d5 §6) — вывести таблицу MOS по флагу (`--dump-summaries` - или в `explain`), плюс extern-границы из `solve_with_log`. Смотришь на метод — - видишь, что решатель про него думает и почему вызов остался plain. +- **Дамп сводок** ✅ *(shipped)*: глагол `python -m ownlang summaries facts.json` + — один детерминированный JSON-документ (сводки по ключу метода + extern-лог + + `degraded`), байт-стабильный под перестановкой входа; это и отладочная + поверхность, и замороженный паритетный артефакт порта (ТЗ §5.4). Смотришь на + метод — видишь, что решатель про него думает и почему вызов остался plain. **Критерий готовности:** на любом прогоне можно ответить «почему этот вызов не consume/borrow/fresh» без чтения кода моста. С началом Rust-порта у этапа diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index fa9748ef..8aa0270f 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -312,6 +312,16 @@ Python-стороне — тот же ход, что уже сделан для (corpus hash + reference hash) поддерживает это без доработок. Это этап 1 карты, переквалифицированный в артефакт порта. +> **Статус: Python-сторона заморожена.** Поверхность — глагол +> `python -m ownlang summaries facts.json` (`dump_summaries` в `ownir.py`): +> один детерминированный JSON-документ — сводки, отсортированные по ключу +> метода (`file` наследуется из фактов; у слитых перегрузок — min по +> (file, line), независимо от порядка входа), отсортированный extern-лог, +> `degraded` с причиной при сбое решателя (rc остаётся 0 — поверхность +> сообщает состояние, не судит). Байт-детерминизм под перестановкой +> `functions[]` запиннен тестом. В `SURFACES` oracle_exact заводить вместе с +> Rust-консюмером (`own-bridge`), которого ещё нет. + ### 5.5 Порядок портирования внутри слоя 1. **Решатель** (чистый, без зависимостей): порт + property-тесты (монотонность diff --git a/ownlang/__main__.py b/ownlang/__main__.py index f901502d..b1662978 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -9,6 +9,8 @@ python -m ownlang report file.own # buffer storage report + .ownreport.json python -m ownlang ownir facts.json # check OwnIR facts extracted from C# (P-001) python -m ownlang ownir facts.json --format github|msbuild|human|sarif + python -m ownlang summaries facts.json # dump solved method-ownership summaries + # (MOS) + extern log — deterministic JSON python -m ownlang explain OWN001 [DI002 ...] # explain diagnostic code(s): what/why/fix python -m ownlang explain --json findings.json # explain every code in a findings/SARIF file @@ -300,6 +302,27 @@ def cmd_explain(codes: list[str], json_path: str | None) -> int: return 0 +def cmd_summaries(path: str) -> int: + """Dump the solved Method Ownership Summaries (MOS) + the extern-boundary + log for an OwnIR facts file as one deterministic JSON document on stdout + (roadmap stage 1). The debugging answer to "why did this call stay plain / + consume / fresh?" — and the frozen parity surface the Rust port of the + inference layer is diffed against, so its output contract is byte-stable: + sorted method keys, sorted extern log, fixed field order. Exit code is 0 + even when the solve degraded (the `degraded` field carries the reason — + this surface reports state, it does not judge); 2 only for unreadable + facts, like `ownir`.""" + import json + from .ownir import OwnIRError, dump_summaries, load + try: + doc = dump_summaries(load(path)) + except OwnIRError as e: + print(f"{path}: error: {e}", file=sys.stderr) + return 2 + print(json.dumps(doc, indent=2, sort_keys=True)) + return 0 + + def cmd_ownir(path: str, fmt: str = "human", severity: str = "error", verbosity: str = "normal") -> int: """Check OwnIR facts (extracted from real C# by the Roslyn frontend) through @@ -372,7 +395,8 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error", def main(argv: list[str]) -> int: - if not argv or argv[0] not in {"check", "emit", "cfg", "report", "ownir", "explain"}: + if not argv or argv[0] not in {"check", "emit", "cfg", "report", "ownir", + "summaries", "explain"}: print(__doc__) return 2 cmd = argv[0] @@ -475,7 +499,8 @@ def main(argv: list[str]) -> int: return cmd_check(path, fmt, severity) if cmd == "cfg": return cmd_cfg(path, fmt) - return {"emit": cmd_emit, "report": cmd_report}[cmd](path) + return {"emit": cmd_emit, "report": cmd_report, + "summaries": cmd_summaries}[cmd](path) if __name__ == "__main__": diff --git a/ownlang/ownir.py b/ownlang/ownir.py index dcd33acc..d7b26bb3 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -153,6 +153,7 @@ ReturnSkeleton, Transfer, solve, + solve_with_log, ) # The OwnIR schema version this core understands. Bump it whenever the fact @@ -1473,7 +1474,11 @@ def _merge_skeletons(group: list[MethodSkeleton]) -> MethodSkeleton: params = tuple( ParamSkeleton(i, names[i], True, tuple(by_index[i])) for i in sorted(by_index) ) - return MethodSkeleton(group[0].key, params, _merge_returns([sk.ret for sk in group])) + # the merged location must not depend on `functions[]` input order (the summary + # dump is a deterministic parity surface): take the smallest (file, line) pair. + floc = min((sk.file, sk.line) for sk in group) + return MethodSkeleton(group[0].key, params, + _merge_returns([sk.ret for sk in group]), floc[0], floc[1]) def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: @@ -1569,7 +1574,10 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: params.append(ParamSkeleton(i, cname, True, paths)) pnames = {str(p.get("name", "")) for p in raw_params if isinstance(p, dict)} ret = _infer_return_skeleton(body, pnames, first_party) - by_key.setdefault(key, []).append(MethodSkeleton(key, tuple(params), ret)) + # carry the declaration file so the summary dump is navigable (functions[] + # entries carry no line of their own — params do; line stays 0). + by_key.setdefault(key, []).append( + MethodSkeleton(key, tuple(params), ret, str(fn.get("file", "?")))) # one skeleton per name: solve() keys by name (a forward names its callee with no # signature), so same-name overloads are joined into a single conservative summary. return [_merge_skeletons(group) for group in by_key.values()] @@ -2027,6 +2035,44 @@ def _flow_local_steps(sub: dict[str, Any], code: str, dline: int, return ((f, acq, origin), (f, dline, viol)) +def dump_summaries(facts: dict[str, Any]) -> dict[str, Any]: + """The MOS observability / parity surface (roadmap stage 1, TZ §5.4): derive + the skeletons, run the solver, and return the solved summaries plus the + extern-boundary log as ONE deterministic document. + + Two consumers, one contract: + - a human asking "why did this call stay plain?" reads the method's summary + (transfer per param, return kind) and the `unresolved` extern boundaries + without reading bridge code; + - the Rust port of the inference layer is diffed against this document + (`oracle_exact`-style), which checks the port at the summary level — finer + than diffing final diagnostics, where an inference bug can hide behind an + unrelated silence. + + Determinism is the contract: summaries are sorted by method key, the + unresolved log arrives sorted from `solve_with_log`, and `to_dict` field + order is fixed — the same facts yield byte-identical JSON regardless of + `functions[]` input order. A failed solve degrades exactly like + `check_facts` (empty summaries), with the reason in `degraded` — the same + honesty OWN052 gives the checking path.""" + raw_fns = facts.get("functions", []) + raw_fns = raw_fns if isinstance(raw_fns, list) else [] + degraded: str | None = None + summaries: dict[str, Any] = {} + unresolved: list[str] = [] + try: + summaries, unresolved = solve_with_log(_build_skeletons(raw_fns)) + except Exception as exc: + degraded = f"{type(exc).__name__}: {exc}" + return { + "module": str(facts.get("module", "?")), + "ownir_version": OWNIR_VERSION, + "summaries": [summaries[k].to_dict() for k in sorted(summaries)], + "unresolved": unresolved, + "degraded": degraded, + } + + def check_facts(facts: dict[str, Any]) -> list[Finding]: """Run the core checker over the lowered facts and return findings mapped back to their original C# locations (v0: the `event += without -=` leak). diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 2cf0e4c7..eb9afc48 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1630,6 +1630,56 @@ def _boom(_sk): # type: ignore[no-untyped-def] if gotlit != [("hand", 10, "OWN002")]: fails.append("TZ D5: healthy solve must carry no OWN052 and keep the true " f"OWN002, got {gotlit}") + # --- roadmap stage 1: the `summaries` dump (dump_summaries / `python -m + # ownlang summaries`). One deterministic document: solved MOS per method + # (sorted by key), the extern-boundary log (sorted), a `degraded` reason. + # This is the parity surface the Rust port of the inference layer will be + # diffed against, so its byte-stability IS the contract. + from ownlang.ownir import dump_summaries + _dump_facts = {"module": "M", "functions": [ + {"name": "B.Fwd", "file": "b.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "Extern.Gone", "args": ["s"], "line": 2}]}, + {"name": "A.Make", "file": "a.cs", + "body": [{"op": "acquire", "var": "r", "line": 1}, + {"op": "return", "var": "r", "line": 2}]}, + {"name": "C.Sink", "file": "c.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "release", "var": "x", "line": 2}]}]} + checks += 1 + doc = dump_summaries(_dump_facts) + keys = [s["method"] for s in doc["summaries"]] + kinds = {s["method"]: s["returns"]["owned"] for s in doc["summaries"]} + transfers = {s["method"]: [p["transfer"] for p in s["params"]] + for s in doc["summaries"]} + files = {s["method"]: s["file"] for s in doc["summaries"]} + if (keys != ["A.Make", "B.Fwd", "C.Sink"] # sorted by method key + or kinds["A.Make"] != "fresh" or transfers["C.Sink"] != ["must"] + or transfers["B.Fwd"] != ["unknown"] + or doc["unresolved"] != ["Extern.Gone#0 (extern, no summary)"] + or files["A.Make"] != "a.cs" or doc["degraded"] is not None): + fails.append(f"summaries dump content wrong: {doc}") + # byte-determinism: permuting `functions[]` input order must not change one byte + # of the canonical dump — this is what makes it a parity artifact, not a debug log. + checks += 1 + blob1 = json.dumps(doc, indent=2, sort_keys=True) + _dump_facts["functions"].reverse() + blob2 = json.dumps(dump_summaries(_dump_facts), indent=2, sort_keys=True) + if blob1 != blob2: + fails.append("summaries dump must be byte-identical under functions[] " + "input permutation") + # a failed solve degrades the dump exactly like the checking path: empty + # summaries + the reason in `degraded` — never a crash, never a half-document. + checks += 1 + _real_swl = _oi.solve_with_log + def _boom2(_sk): # type: ignore[no-untyped-def] + raise RuntimeError("synthetic dump failure") + _oi.solve_with_log = _boom2 # type: ignore[assignment] + try: + darkdoc = dump_summaries(_dump_facts) + finally: + _oi.solve_with_log = _real_swl + if (darkdoc["summaries"] != [] or darkdoc["unresolved"] != [] + or "synthetic dump failure" not in (darkdoc["degraded"] or "")): + fails.append(f"degraded summaries dump wrong: {darkdoc}") # (§10 q2) same-name OVERLOADS are merged, not dropped: when EVERY overload of a # name consumes the forwarded arg, a forward to that name resolves to `must`, so a # caller using the local after the handoff is OWN002. Before the merge the name was From f9e4f04df22942608a0690633b51d4a2cda87e18 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:26:27 +0000 Subject: [PATCH 09/12] =?UTF-8?q?feat(d5):=20OWN051=20+=20real=20optimisti?= =?UTF-8?q?c=20silence=20=E2=80=94=20untrack=20a=20local=20at=20a=20may/un?= =?UTF-8?q?known=20call=20(TZ=20D6)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit d5 §5's optimistic default says an unverified-ownership call site resolves to 'the caller no longer owns' -> silence. The implementation lowered may/unknown contracts to a PLAIN arg instead — which is not silence: plain leaves the obligation with the caller, so DROPPING a local after a may-call fabricated OWN001. The channel predates D1 (conditional forwards), but the D1 fix widened it to every null-guard dispose helper: 'var r = new X(); Cleanup(r);' — the normal usage, Cleanup IS the disposer — read as a leak. Untrack makes the default real: _unverified_transfer_calls collects every arg at a may/unknown position of a summarized callee; such locals are not minted at all (acquire / fresh result / alias target skipped, branch-hoist excluded), so neither a missing nor a defensive dispose after the call can be charged. A call with may/unknown positions routes through the existing per-argument $consume/$borrow channel (the overload path, now shared) so an untracked name is never referenced in emitted code — the first run's loud OWN030 (map-or-raise doing its job) proved why. Verified contracts are untouched: borrow-drop keeps its true OWN001 (T3) and consume-reuse its OWN002 (T2), both pinned. The gap is now honest instead of silent-or-wrong: advisory OWN051 ('ownership transfer unverified — local not checked past this call') at the call site, gated on args that actually carry an obligation (acquired or fresh-factory locals — no noise for plain values), advisory like OWN050/052: warning, SARIF note, never the exit code, hidden at --verbosity quiet. explain OWN051 answers. Seven existing may-shape tests updated from 'empty' to 'exactly one OWN051 advisory'; three new tests pin the closed FP, the preserved T3 recall, and the owned-local gate. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-roadmap.md | 6 +- docs/notes/interprocedural-tz.md | 24 ++++ ownlang/__main__.py | 9 +- ownlang/diagnostics.py | 13 +++ ownlang/ownir.py | 156 ++++++++++++++++++++++---- tests/test_ownir.py | 93 +++++++++++---- 6 files changed, 253 insertions(+), 48 deletions(-) diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md index daf558a3..22fff70b 100644 --- a/docs/notes/interprocedural-roadmap.md +++ b/docs/notes/interprocedural-roadmap.md @@ -147,8 +147,10 @@ d5-заметка ставит advisory в хвост (D5.x); эта карта и главный ответ на «непонятки». Вся фактура уже считается (§5 d5: «we compute the full must/may/escape evidence regardless of mode»), не хватает поверхности: -- **OWN051** (OWN05x-band, как OWN050): `transfer:may` и honest-`unknown` - показываются с `--verbosity normal`+, никогда не валят CI. +- **OWN051** ✅ *(shipped)*: владелец, переданный на `may`/`unknown`-позицию, + оптимистично перестаёт отслеживаться (ТЗ D6 — настоящее «молчание», а не + plain), и это честно фиксируется advisory OWN051 на месте вызова — warning в + выводе, `note` в SARIF, никогда не rc; `--verbosity quiet` скрывает. - **Дамп сводок** ✅ *(shipped)*: глагол `python -m ownlang summaries facts.json` — один детерминированный JSON-документ (сводки по ключу метода + extern-лог + `degraded`), байт-стабильный под перестановкой входа; это и отладочная diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index 8aa0270f..227b4d96 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -173,6 +173,9 @@ OWN001 в самом хелпере. Это удар ровно по полу `o **Решение (принять до порта — иначе bit-parity заставит Rust воспроизводить баг как норму):** +- ⚠ Дополнение пост-фактум: вариант A сам по себе **расширяет** D6-канал + (may-параметры множатся) — он полон только вместе с untrack-семантикой D6. + Оба шага сделаны; см. D6 ниже. - **Вариант A (рекомендуемый): ветко-чувствительная деривация release.** Release на всех путях → `[dispose]`; на части путей → `[dispose, borrow]` (join ⇒ `may` ⇒ plain на call-site — молчание); прямая инференция @@ -226,6 +229,27 @@ all-paths ⇒ may); release + throw-ветка (по политике `--flow-lo в ТЗ этапа 3 (§6.2) — как ограничение первого среза: применение `aliasOf:i` только на прямом вызове, без переиндексации через цепочку. +### D6 (обнаружено при реализации OWN051): `may`/`unknown` → plain — это не молчание + +Политика §5 d5 требует: неизвестный контракт ⇒ optimistic ⇒ **тишина**. Но +реализация опускала `may`/`unknown` в plain-эффект — а plain оставляет +обязательство у вызывающего: **брошенный** после `may`-вызова ресурс давал +OWN001. Канал существовал до D1 (условные forward'ы), а фикс D1 его расширил: +нормальное использование null-guard-хелпера (`Cleanup(r)` без dispose после — +хелпер и есть освободитель) стало ложным OWN001. + +> **Статус: исправлено (untrack).** Аргумент на `may`/`unknown`-позиции +> суммаризированного callee **прекращает отслеживаться** в вызывающем +> (`_unverified_transfer_calls` + гейты в лоуэринге: acquire/fresh/alias не +> минтятся, hoist исключён): ни пропущенный, ни защитный dispose после такого +> вызова не наказуем. Вызов с `may`/`unknown`-позициями эмитится через +> по-аргументные `$`-каналы (расширение M3-маршрутизации) — untracked-имя не +> упоминается в эмитируемом коде (иначе map-or-raise OWN030, что и поймал +> первый прогон). Проверенные контракты не тронуты: borrow-drop (T3 OWN001) и +> consume-reuse (T2 OWN002) запиннены тестами. `$`-синки и несуммаризированные +> callee не затронуты (первые — проверенные контракты, вторые экстрактор +> escape-дропает сам). + ### D5: сбой решателя молчит `except Exception: mos = {}` (`ownir.py:906-909`) гасит **весь** межпроцедурный diff --git a/ownlang/__main__.py b/ownlang/__main__.py index b1662978..1dcc4ce5 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -28,9 +28,10 @@ `--severity` (ownir only) picks how the host shows a finding — `error` (default, fails a build / red check) or `warning` (advisory). It is a presentation choice; the finding is still the core's verdict. -`--verbosity` (ownir only) is `quiet` (errors only — hide the advisory OWN050 -"leakage analysis skipped" notes, P-014 Tier A), `normal` (default), or `verbose` -(also print a per-code breakdown). +`--verbosity` (ownir only) is `quiet` (errors only — hide the advisory notes: +OWN050 "leakage analysis skipped", OWN051 "ownership transfer unverified", +OWN052 "summaries skipped"), `normal` (default), or `verbose` (also print a +per-code breakdown). Exit code is non-zero if any error-level diagnostic was produced. """ @@ -330,7 +331,7 @@ def cmd_ownir(path: str, fmt: str = "human", severity: str = "error", selects the surface: human (CLI), github (CI annotations), msbuild (VS), sarif (SARIF 2.1.0 log); `severity` picks how the host shows them (error/warning); `verbosity` is - `quiet` (errors only — hide the advisory OWN050 notes), `normal` (default), or + `quiet` (errors only — hide the advisory OWN05x notes), `normal` (default), or `verbose` (also print a per-code breakdown).""" from .ownir import OwnIRError, build_sarif, check_facts, load, render_finding try: diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 317f5ad6..6ebf920e 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -80,6 +80,7 @@ class Severity(Enum): "OWN041": "call argument mismatch", # ---- C# front-end resolution coverage (P-014; advisory) ---- "OWN050": "declaring type unresolved -- leakage analysis skipped", + "OWN051": "ownership transfer unverified -- local not checked past this call", "OWN052": "interprocedural summary inference failed -- method summaries skipped", # ---- DI container lifetimes (P-006; emitted by the OwnIR bridge) ---- "DI001": "captive dependency: a shorter-lived service is captured by a longer-lived one", @@ -152,6 +153,18 @@ class Severity(Enum): "Fix (to check it): give the extractor the type's assembly via `--ref-dir ` so the " "SemanticModel can bind the event." ), + "OWN051": ( + "Advisory, not a leak verdict: an owned local was passed to a method whose ownership " + "contract for that argument could not be verified — the inferred transfer is `may` " + "(the callee disposes it on some paths only) or `unknown` (the evidence crosses an " + "unanalyzable boundary). Per the optimistic default (own-only 0) the checker assumes " + "ownership left the caller and stops tracking the local at that call: a missing " + "dispose after it is NOT reported, and neither is a defensive one. This note is the " + "honest record of that gap. It never fails a build.\n" + "Fix (to make it checkable): make the callee's contract definite — dispose the " + "parameter on every path (or none), or annotate the intended contract when " + "annotations land (P-005 Tier C)." + ), "OWN052": ( "Advisory, not a leak verdict: computing the method ownership summaries (the " "interprocedural pass that resolves cross-method ownership transfer) failed, so the " diff --git a/ownlang/ownir.py b/ownlang/ownir.py index d7b26bb3..ce4f42d2 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -782,7 +782,9 @@ def _prelude_resources() -> list[ResourceDecl]: def to_module(facts: dict[str, Any], - notes: list[str] | None = None) -> tuple[Module, dict[str, dict[str, Any]]]: + notes: list[str] | None = None, + advisories: list["Finding"] | None = None, + ) -> tuple[Module, dict[str, dict[str, Any]]]: """Build the core `Module` AST **directly** from OwnIR facts — no `.own` source text and no re-parse (P-016 B0a; the round-trip `to_own` + `parse` has existed since P-001). Mirrors `to_own`'s lowering exactly: each owned-resource fact @@ -791,7 +793,9 @@ def to_module(facts: dict[str, Any], map; a diagnostic names a handle via its symbol `origin` (`#`, cfg.py), which maps straight back to the C# location. `notes`, when given, collects coverage-degradation reasons (a failed MOS solve — TZ D5) the caller - should surface as advisory findings rather than lose.""" + should surface as advisory findings rather than lose; `advisories` collects + ready-made advisory Findings minted during lowering (OWN051 unverified-transfer + notes) for the caller to append.""" handles: dict[str, dict[str, Any]] = {} functions: list[FnDecl] = [] gid = 0 @@ -947,11 +951,43 @@ def to_module(facts: dict[str, Any], localmap: dict[str, str] = {} fparams = _lower_fn_params(fn, ffile, fname, handles, loc, localmap, released, mos) + # The optimistic default (d5 §5), made real: an argument at a call + # position whose contract resolved `may`/`unknown` means "we cannot + # verify whether ownership left the caller" — so the caller's local is + # UNTRACKED from that call's function (its acquire is not minted), and + # neither a missing nor a defensive dispose after the call can be + # charged. Anything less is not silence: a plain arg leaves the + # obligation with the caller, so dropping it fabricates OWN001 on the + # ubiquitous null-guard-helper idiom (TZ итерация 6). + unverified = _unverified_transfer_calls(nodes, mos) + untracked = frozenset(a for a, _c, _t, _l in unverified) + if advisories is not None and unverified: + # OWN051, gated on args that actually carry an obligation here (an + # acquired local or a fresh factory result) — a plain value passed + # to a may-position is not a gap worth a note. + owned_here = _collect_vars(nodes, "acquire", "var") | { + v for v, c in _call_result_callees(nodes).items() + if c and _callee_returns_fresh(c, mos, first_party)} + for arg, callee, transfer, cline in unverified: + if arg not in owned_here: + continue + advisories.append(Finding( + file=ffile, line=cline, code="OWN051", + component=fname, event=arg, handler=callee, + message=(f"cannot verify whether '{callee}' takes " + f"ownership of '{arg}' (inferred contract: " + f"{transfer}); optimistically assuming it does — " + f"'{arg}' is not checked past this call"), + kind="ownership transfer", advisory=True)) # Cross-branch locals (acquired inside an `if`/`while` branch but referenced # after the merge) must be declared once at the function's outer scope, or # the core rejects the post-merge reference as OWN030 (the bridge branch- # scope fix). Pre-declare them here, then skip their in-branch acquire. - hoist = _hoisted_branch_locals(nodes, mos, first_party) + # An untracked local must not be hoisted either — the hoisted `Let` + # would re-mint the very obligation the untrack removed. + hoist = {k: v for k, v in + _hoisted_branch_locals(nodes, mos, first_party).items() + if k not in untracked} hoisted_lets: list[Stmt] = [] for hname in sorted(hoist): hh = f"loc_{loc[0]}" @@ -964,7 +1000,8 @@ def to_module(facts: dict[str, Any], hoisted_lets.append(Let(hh, Acquire("Disposable", [], hline), hline)) fbody = [*hoisted_lets, *_lower_flow(nodes, ffile, fname, handles, loc, localmap, - released, mos, set(hoist), first_party, overloaded)] + released, mos, set(hoist), first_party, overloaded, + untracked)] # A body that returns a value gets an owned return type, so the core # models `return s` as a valid ESCAPE (the value is discharged to the # caller) instead of a void-return mismatch that would leave `s` looking @@ -1008,6 +1045,56 @@ def _released_vars(nodes: list[Any]) -> set[str]: return out +def _unverified_transfer_calls( + nodes: Any, mos: dict[str, Any] | None) -> list[tuple[str, str, str, int]]: + """Every `(arg_name, callee, transfer, line)` where a call op hands an argument + to a summarized callee position whose resolved transfer is `may` or `unknown` — + the ownership contract the solver could NOT verify (d5 §5's advisory channel). + + Two consumers in `to_module`: the arg names become the per-function UNTRACK set + (the optimistic default made real — "caller no longer owns" means the local's + obligation stops being tracked at that call, so neither a missing NOR a + defensive dispose after it can be charged), and each hit on an owned local + surfaces as an advisory OWN051 (the honest record of the gap; TZ итерация 6). + Callees with no summary at all are NOT collected: the extractor already + escape-drops locals it hands to unanalyzable callees, and the `$`-sink externs + are verified contracts, not gaps.""" + out: list[tuple[str, str, str, int]] = [] + if mos is None: + return out + + def walk(ns: Any) -> None: + if not isinstance(ns, list): + return + for n in ns: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == "call": + callee = str(n.get("callee", "")) + summ = mos.get(callee) if callee else None + if summ is None and callee: + identity = _canonical_callee_name(callee) + if identity != callee: + summ = mos.get(identity) + args = n.get("args", []) + if summ is not None and isinstance(args, list): + for j, a in enumerate(args): + ps = next((q for q in summ.params if q.index == j), None) + if ps is not None and ps.transfer in (Transfer.MAY, + Transfer.UNKNOWN): + out.append((str(a), callee, ps.transfer.value, + _as_int(n.get("line", 0)))) + elif op == "if": + walk(n.get("then")) + walk(n.get("else")) + elif op == "while": + walk(n.get("body")) + + walk(nodes) + return out + + def _returns_value(nodes: Any) -> bool: """True if a flow body returns a VALUE on some path (a `return` op carrying a `var`), recursing into if/while. The bridge then gives the function an owned @@ -1804,7 +1891,8 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, mos: dict[str, Any] | None = None, hoisted: set[str] | None = None, first_party: frozenset[str] = frozenset(), - overloaded: frozenset[str] = frozenset()) -> list[Stmt]: + overloaded: frozenset[str] = frozenset(), + untracked: frozenset[str] = frozenset()) -> list[Stmt]: """Lower one OwnIR flow body (B0b/B2) into core statements. acquire/use/release/ return reference a C# local by name (`var`); `if` carries `then`/`else` sub-bodies; `while` carries a `body` (a back-edge — the core's worklist fixpoint @@ -1821,7 +1909,13 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, outer scope by the caller, so an in-branch acquire of such a name is SKIPPED here (the hoisted `Let` already declared+acquired it) — this keeps a cross-branch local in scope after the merge instead of emitting a branch-scoped `Let` the core would - reject as OWN030.""" + reject as OWN030. + + `untracked` names (see `_unverified_transfer_calls`) are locals handed to a + `may`/`unknown`-contract position: the optimistic default assumes ownership + left the caller, so their acquires / fresh mints / alias mints are NOT emitted + — later releases/uses of them resolve to nothing and stay silent, and the gap + is surfaced as an advisory OWN051 instead of a fabricated verdict.""" hoisted = hoisted or set() body: list[Stmt] = [] for n in nodes: @@ -1835,6 +1929,11 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # declared+acquired once at the outer scope (cross-branch local) — the # hoisted `Let` stands in for this in-branch acquire; emit nothing. continue + if name in untracked: + # handed to a may/unknown-contract position later: optimistically + # not ours to check (OWN051 carries the honest note). No obligation + # is minted, so neither dropping nor disposing it can be charged. + continue handle = f"loc_{loc[0]}" loc[0] += 1 localmap[name] = handle @@ -1863,7 +1962,7 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # A hoisted local keeps its single outer-scope handle (declared once). if name not in hoisted: localmap.pop(name, None) - if src_h is not None and name not in hoisted: + if src_h is not None and name not in hoisted and name not in untracked: handle = f"loc_{loc[0]}" loc[0] += 1 localmap[name] = handle @@ -1896,16 +1995,16 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, en = n.get("else", []) then_b = _lower_flow(tn if isinstance(tn, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded) + first_party, overloaded, untracked) else_b = _lower_flow(en if isinstance(en, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded) + first_party, overloaded, untracked) body.append(If("?", then_b, else_b, line)) elif op == "while": bn = n.get("body", []) body_b = _lower_flow(bn if isinstance(bn, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded) + first_party, overloaded, untracked) body.append(While("?", body_b, line)) elif op == "call": # A call to a CONTRACTED callee (a function/extern whose signature the @@ -1926,18 +2025,28 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # signature table (which would raise OWN040). merged = summ if summ is not None else ( mos.get(identity) if (mos is not None and identity != callee) else None) - if identity in overloaded and merged is not None and isinstance(raw_args, list): - # OVERLOADED name: do NOT emit a `Call` resolved against the core's last-wins - # signature table (it stores one same-name FnDecl, so it would mis-apply one - # overload's effect — a false OWN002 when overloads disagree). Apply the MERGED - # MOS contract per argument through the `$consume`/`$borrow` channel instead, - # exactly as a FORWARD to this name resolves (`must`→consume, `no`→borrow, - # `may`/`unknown`→plain). The channel emits sink externs (never the callee name), - # so a qualified callee is safe here. (Codex P2 / CodeRabbit.) + if merged is not None and isinstance(raw_args, list) and ( + identity in overloaded + or any(q.transfer in (Transfer.MAY, Transfer.UNKNOWN) + for q in merged.params)): + # Per-argument channel routing, for two shapes that must NOT emit a + # direct `Call`: + # - an OVERLOADED name: the core's last-wins signature table stores + # one same-name FnDecl, so a direct Call would mis-apply one + # overload's effect — a false OWN002 when overloads disagree; + # - a callee with a MAY/UNKNOWN param: its arg is UNTRACKED (the + # optimistic default + advisory OWN051), so a direct Call would + # reference an undeclared name — a loud OWN030 (map-or-raise). + # Apply the MOS contract per argument through the `$consume`/ + # `$borrow` channel instead, exactly as a FORWARD to this name + # resolves (`must`→consume, `no`→borrow, `may`/`unknown`→nothing: + # the untracked arg is never referenced). The channel emits sink + # externs (never the callee name), so a qualified callee is safe + # here. (Codex P2 / CodeRabbit.) for j, a in enumerate(raw_args): ps = next((q for q in merged.params if q.index == j), None) channel = _CHANNEL_FOR_TRANSFER.get(ps.transfer) if ps else None - if channel is not None: + if channel is not None and str(a) not in untracked: body.append(Call(channel, [VarRef(localmap.get(str(a), str(a)), line)], line)) # Only emit the `Call` when the callee is RESOLVABLE — a first-party function @@ -1965,6 +2074,7 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, if isinstance(result, str) and result and result not in hoisted: localmap.pop(result, None) if (isinstance(result, str) and result and result not in hoisted + and result not in untracked and _callee_returns_fresh(callee, mos, first_party)): handle = f"loc_{loc[0]}" loc[0] += 1 @@ -2090,7 +2200,8 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: from .__main__ import check_module mos_notes: list[str] = [] - mod, handles = to_module(facts, mos_notes) + transfer_notes: list[Finding] = [] + mod, handles = to_module(facts, mos_notes, transfer_notes) diags = check_module(mod) # registration site of each DI service, to anchor a subscription-escape slice's @@ -2331,6 +2442,11 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: # this side path so it bypasses the ERROR-only diagnostic mapping above. findings.extend(_unresolved_findings(facts)) + # OWN051 (d5 §5's advisory channel): each owned local handed to a + # may/unknown-contract position was optimistically untracked at that call — + # surface the honest "not checked past here" note minted during lowering. + findings.extend(transfer_notes) + # OWN052 (TZ D5): the MOS solve failed and the bridge degraded to no-MOS, so # EVERY cross-method ownership contract was skipped this run. Same honest-skip # posture as OWN050 — a coverage note, never a verdict, never the exit code. diff --git a/tests/test_ownir.py b/tests/test_ownir.py index eb9afc48..39586821 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1495,9 +1495,10 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "s", "line": 10}, {"op": "call", "callee": "maybe", "args": ["s"], "line": 11}, {"op": "release", "var": "s", "line": 12}]}]}) - if cond: - gotc = [(x.component, x.code) for x in cond] - fails.append(f"D5.1 conditional forward must be `may`: caller stays silent, got {gotc}") + gotc = [(x.component, x.code, x.advisory) for x in cond] + if gotc != [("user_c", "OWN051", True)]: + fails.append("D5.1 conditional forward must be `may`: no verdicts, one " + f"honest OWN051 advisory (d5 §5), got {gotc}") # (TZ D1) a CONDITIONAL release joins to `may`, not a flattened `consume`: # `cond_rel(x){ if(c) release x; }` keeps x on the other path, so a caller that # disposes defensively after the call stays SILENT. Before the fix the inferred @@ -1512,9 +1513,10 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "r", "line": 10}, {"op": "call", "callee": "cond_rel", "args": ["r"], "line": 11}, {"op": "release", "var": "r", "line": 12}]}]}) - if d1c: - fails.append("TZ D1: a partial release must join to `may` (caller silent), " - f"got {[(x.component, x.code) for x in d1c]}") + gotd1c = [(x.component, x.code, x.advisory) for x in d1c] + if gotd1c != [("careful", "OWN051", True)]: + fails.append("TZ D1: a partial release must join to `may` — no verdicts, " + f"one OWN051 advisory, got {gotd1c}") # (TZ D1) release in BOTH branches IS all-paths: consume survives, and the # careless caller keeps its true OWN002 — the refinement costs no recall here. checks += 1 @@ -1541,9 +1543,10 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "r", "line": 10}, {"op": "call", "callee": "loop_rel", "args": ["r"], "line": 11}, {"op": "release", "var": "r", "line": 12}]}]}) - if d1w: - fails.append("TZ D1: a while-body release is zero-trip-partial (caller " - f"silent), got {[(x.component, x.code) for x in d1w]}") + gotd1w = [(x.component, x.code, x.advisory) for x in d1w] + if gotd1w != [("loop_user", "OWN051", True)]: + fails.append("TZ D1: a while-body release is zero-trip-partial — no " + f"verdicts, one OWN051 advisory, got {gotd1w}") # (TZ D1) an early `return` on an unreleased path blocks the definite claim: # `guard(x){ if(c) return; release x; }` does not release on the guard path. checks += 1 @@ -1556,9 +1559,10 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "r", "line": 10}, {"op": "call", "callee": "guard_rel", "args": ["r"], "line": 11}, {"op": "release", "var": "r", "line": 12}]}]}) - if d1g: - fails.append("TZ D1: an early-return-unreleased path blocks consume (caller " - f"silent), got {[(x.component, x.code) for x in d1g]}") + gotd1g = [(x.component, x.code, x.advisory) for x in d1g] + if gotd1g != [("guard_user", "OWN051", True)]: + fails.append("TZ D1: an early-return-unreleased path blocks consume — no " + f"verdicts, one OWN051 advisory, got {gotd1g}") # (TZ D1) release-then-return in a branch plus a fall-through release IS # all-paths — the walk credits a released early exit, so consume survives. checks += 1 @@ -1590,9 +1594,53 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "r", "line": 10}, {"op": "call", "callee": "via", "args": ["r"], "line": 11}, {"op": "release", "var": "r", "line": 12}]}]}) - if d1f: - fails.append("TZ D1: forwarding to a partial releaser must stay plain " - f"(caller silent), got {[(x.component, x.code) for x in d1f]}") + gotd1f = [(x.component, x.code, x.advisory) for x in d1f] + if gotd1f != [("via_user", "OWN051", True)]: + fails.append("TZ D1: forwarding to a partial releaser degrades to `may` " + f"transitively — no verdicts, one OWN051 advisory, got {gotd1f}") + # (итерация 6) the optimistic default made REAL: an owned local DROPPED after + # a may-call must be silent (untracked), not an OWN001 — before this fix a + # plain arg left the obligation with the caller, so the ubiquitous null-guard + # helper usage `var r = new X(); Cleanup(r);` (no dispose after — Cleanup IS + # the disposer) fabricated a leak. The gap is the OWN051 advisory instead. + checks += 1 + d6drop = check_facts({"module": "M", "functions": [ + {"name": "cond_rel3", "file": "U.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "drop_user", "file": "U.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "cond_rel3", "args": ["r"], "line": 11}]}]}) + gotd6 = [(x.component, x.line, x.code, x.advisory) for x in d6drop] + if gotd6 != [("drop_user", 11, "OWN051", True)]: + fails.append("untrack: dropping a local after a may-call must be silent " + f"(one OWN051 advisory, no OWN001), got {gotd6}") + # ... while a VERIFIED borrow keeps the obligation with the caller: dropping + # after a borrow-only callee is the T3 recall win (a real OWN001, no OWN051) — + # the untrack must never widen to verified contracts. + checks += 1 + d6borrow = check_facts({"module": "M", "functions": [ + {"name": "peek3", "file": "U.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "use", "var": "x", "line": 2}]}, + {"name": "drop_b", "file": "U.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "peek3", "args": ["r"], "line": 11}]}]}) + gotd6b = [(x.component, x.line, x.code, x.advisory) for x in d6borrow] + if gotd6b != [("drop_b", 10, "OWN001", False)]: + fails.append("untrack: a verified borrow must keep the caller's obligation " + f"(true OWN001 on drop, no advisory), got {gotd6b}") + # a plain (never-acquired) value at a may-position is not a gap worth a note: + # the OWN051 owned-local gate keeps the advisory channel quiet. + checks += 1 + d6plain = check_facts({"module": "M", "functions": [ + {"name": "cond_rel4", "file": "U.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "plain_user", "file": "U.cs", + "body": [{"op": "call", "callee": "cond_rel4", "args": ["v"], "line": 11}]}]}) + if d6plain: + fails.append("untrack: a non-owned value at a may-position must stay quiet, " + f"got {[(x.component, x.code) for x in d6plain]}") # (TZ D5) a failed MOS solve must degrade OBSERVABLY: the bridge drops to # no-MOS (checker stays alive, forwards stay plain — no fabricated verdicts) # and surfaces ONE advisory OWN052 naming the inner error. Before the fix the @@ -1715,10 +1763,10 @@ def _boom2(_sk): # type: ignore[no-untyped-def] "body": [{"op": "acquire", "var": "s", "line": 20}, {"op": "call", "callee": "ovn_fwd", "args": ["s"], "line": 21}, {"op": "release", "var": "s", "line": 22}]}]}) - if ovd: - gotn = [(x.component, x.code) for x in ovd] - fails.append("§10 q2 disagreeing overloads must join to `may` (caller stays " - f"silent), got {gotn}") + gotn = [(x.component, x.code, x.advisory) for x in ovd] + if gotn != [("ovn_use", "OWN051", True)]: + fails.append("§10 q2 disagreeing overloads must join to `may` — no " + f"verdicts, one OWN051 advisory, got {gotn}") # (Codex P2) a DIRECT call to disagreeing overloads must NOT mis-apply the last same-name # signature: the merged contract is `may`, so `acquire s; C.N(s); release s` stays silent. # (Before the fix the core's last-wins signature consumed s → a false OWN002.) @@ -1732,9 +1780,10 @@ def _boom2(_sk): # type: ignore[no-untyped-def] "body": [{"op": "acquire", "var": "s", "line": 10}, {"op": "call", "callee": "C.N", "args": ["s"], "line": 11}, {"op": "release", "var": "s", "line": 12}]}]}) - if ovdir: - fails.append("§10 q2 direct call to disagreeing overloads must stay silent (merged " - f"may), got {[(x.component, x.code) for x in ovdir]}") + gotdir = [(x.component, x.code, x.advisory) for x in ovdir] + if gotdir != [("dN", "OWN051", True)]: + fails.append("§10 q2 direct call to disagreeing overloads carries no " + f"verdicts, one OWN051 advisory (merged may), got {gotdir}") # the same DIRECT path DOES apply consume when every overload agrees: both consume, so # `acquire s; C.M(s); use s` is use-after-consume OWN002 (the channel carries the merged # `must`, not a dropped effect). From 4177327552ded5f02296b310602c2d93608398c0 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 4 Jul 2026 17:53:06 +0000 Subject: [PATCH 10/12] =?UTF-8?q?spec:=20Inference.md=20=E2=80=94=20normat?= =?UTF-8?q?ive=20spec=20of=20the=20interprocedural=20ownership=20layer=20(?= =?UTF-8?q?roadmap=20stage=200)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lifts the verdict-determining inference layer from an undocumented bridge concern (architecture-review R2, tech-debt-register §3's hard port prerequisite) into a normative, descriptive spec pinned by tests — the same posture as OwnIR.md. Covers: the MOS artifact and its two axes; the transfer lattice and join (INF-L); parameter skeleton derivation (INF-S, incl. the definite-release rule from D1 and the reserved adopt/return kinds from D3); return inference (INF-R); overload merge and the arity residual (INF-M); the SCC-condensation fixpoint (INF-F, incl. the observable-degradation rule from D5); call-site application and the tier ladder (INF-A, incl. the optimistic untrack from D6); the reporting policy and advisories OWN051/OWN052 (INF-P); the deterministic summary-dump serialization (incl. the omitted escapes axis from D2). Honestly marks every reserved element (escapes, adopt/return, strict mode, Tier C, source tiers beyond 'inferred') as 'in the model, no producer'. §11 maps every INF-* rule to its pinning test in test_ownership.py / test_ownir.py; registered in spec/README.md; OWN051/052 documented in spec/Diagnostics.md with a new interprocedural-advisory section. A conformance check pins the codes the spec names to the catalogue. Full suite green (ownir 245/245). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01LBmDyLWHqoQUGqiydSxroi --- docs/notes/interprocedural-roadmap.md | 25 +- docs/notes/interprocedural-tz.md | 10 +- spec/Diagnostics.md | 18 ++ spec/Inference.md | 342 ++++++++++++++++++++++++++ spec/README.md | 4 + tests/test_ownir.py | 7 + 6 files changed, 392 insertions(+), 14 deletions(-) create mode 100644 spec/Inference.md diff --git a/docs/notes/interprocedural-roadmap.md b/docs/notes/interprocedural-roadmap.md index 22fff70b..9a9bc490 100644 --- a/docs/notes/interprocedural-roadmap.md +++ b/docs/notes/interprocedural-roadmap.md @@ -121,17 +121,19 @@ precision-баг с оракула в период порта чинится в («spec it or relocate it — до любого порта»). Каждый следующий этап меняет именно этот слой; менять неспецифицированное — дороже всего. -**Делаем:** - -- `spec/Inference.md` (или раздел в `spec/OwnIR.md`): нормативные правила - вывода — когда параметр `dispose`/`forward`/`borrow`, правило - «single unconditional straight-line forward», правила return-скелета - (returned-param ≠ fresh и т.д.), правила слияния перегрузок, политика - optimistic-по-умолчанию. По объёму это перенос докстрингов - (`_build_skeletons`, `_merge_skeletons`, `solve`) в нормативный текст + - привязка к `test_spec.py`-стилю. -- Golden facts snapshots в CI (N3 из регистра) — шов extractor→bridge diff'ится - на уровне фактов, а не только отрендеренных диагностик. +**Сделано:** + +- ✅ **`spec/Inference.md`** (shipped) — нормативная спека слоя: MOS-артефакт, + решётка transfer, деривация параметров/возвратов/перегрузок (правила + S/R/M-*), решатель (F-*), применение на call-site (A-*), оптимистичный + дефолт + advisories OWN051/OWN052 (P-*), сериализация. Правила `INF-*` + привязаны к `test_ownership.py`/`test_ownir.py` (§11 Conformance); + зарегистрирована в `spec/README.md`, коды заведены в `spec/Diagnostics.md`. + Спека честно фиксирует и reserved-элементы (`escapes`-ось, `adopt`/`return` + path-kinds, strict-режим, Tier C) как «есть в модели, продюсера нет». +- **Осталось:** Golden facts snapshots в CI (N3 из регистра) — шов + extractor→bridge diff'ится на уровне фактов, а не только отрендеренных + диагностик (C#-сторона; отдельный срез). - **Не делаем сейчас:** физический перенос инференции из моста в `ownlang/` — это «seam re-cut» из tech-debt §3, его триггер (P-017 multi-stack или рестарт ядра P-022) не сработал. Спека делает перенос механическим, когда @@ -139,6 +141,7 @@ precision-баг с оракула в период порта чинится в **Критерий готовности:** новый разработчик (или порт) может реализовать инференцию по спеке, не читая `ownir.py`; расхождение спеки и кода ловится CI. +✅ по спеке; golden facts — остаток. ## 4. Этап 1 — наблюдаемость: OWN051 + дамп сводок (дни) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index 227b4d96..f7b6f980 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -3,9 +3,13 @@ > Статус: **рабочее ТЗ** (черновик нормы + критические требования). Дополняет > [interprocedural-roadmap.md](interprocedural-roadmap.md): карта отвечает «что и > когда», это ТЗ — «что именно, как и с какими инвариантами». Из §2–§4 напрямую -> выделяется `spec/Inference.md` (этап 0 карты). Всё описанное «как есть» сверено -> с кодом на коммите `adc1496`; каждое правило несёт ссылку `файл:строка`. -> Расхождение D1 (§3) **воспроизведено исполнением**, не выведено из чтения. +> выделена нормативная спека **[`spec/Inference.md`](../../spec/Inference.md)** +> (этап 0 карты, ✅ shipped — правила `INF-*`, привязаны к +> `test_ownership.py`/`test_ownir.py`); это ТЗ остаётся расширенным рабочим +> черновиком с воспроизведёнными дефектами и требованиями к порту. Всё описанное +> «как есть» сверено с кодом на коммите `adc1496`; каждое правило несёт ссылку +> `файл:строка`. Расхождение D1 (§3) **воспроизведено исполнением**, не выведено +> из чтения. ## 1. Объект: слой — это три компонента, у каждого свой дом diff --git a/spec/Diagnostics.md b/spec/Diagnostics.md index a3171d58..1748dcfa 100644 --- a/spec/Diagnostics.md +++ b/spec/Diagnostics.md @@ -83,6 +83,24 @@ guess a leak; we report, honestly, that it was not checked. Rendered as a |------|-------| | OWN050 | declaring type unresolved — leakage analysis skipped | +## Interprocedural ownership coverage (P-005 D5) + +Advisory only — coverage notes from the interprocedural inference layer +([Inference.md](Inference.md)), never verdicts. Rendered as `warning` regardless +of `--severity`, excluded from the exit code, hidden at `--verbosity quiet`. + +| Code | Title | +|------|-------| +| OWN051 | ownership transfer unverified — local not checked past this call | +| OWN052 | interprocedural summary inference failed — method summaries skipped | + +- **OWN051** anchors at a call site where an owned local is handed to a parameter + position whose resolved transfer is `may` or `unknown` ([Inference §A5, §7](Inference.md)): + the caller's obligation is optimistically dropped there (own-only 0), so the + gap is recorded rather than guessed. +- **OWN052** is module-level (no single site): the summary solve failed and the + bridge degraded to intraprocedural-only checking ([Inference §F6](Inference.md)). + ## Rendering The CLI renders rustc-style: `file:line:col`, the source line, and a caret under diff --git a/spec/Inference.md b/spec/Inference.md new file mode 100644 index 00000000..eae95bd3 --- /dev/null +++ b/spec/Inference.md @@ -0,0 +1,342 @@ +# Interprocedural Ownership Inference Specification + +> **Status: normative, descriptive.** This document specifies the interprocedural +> ownership-inference layer *as it is today*, derived from the working solver +> ([`ownlang/ownership.py`](../ownlang/ownership.py)) and the bridge that feeds and +> applies it ([`ownlang/ownir.py`](../ownlang/ownir.py)), and pinned by tests (see +> [§10 Conformance](#10-conformance)). Forward-looking design lives in +> [`docs/proposals/P-005-idisposable-ownership.md`](../docs/proposals/P-005-idisposable-ownership.md) +> and [`docs/notes/d5-ownership-transfer.md`](../docs/notes/d5-ownership-transfer.md); +> the staged plan and open decisions live in +> [`docs/notes/interprocedural-roadmap.md`](../docs/notes/interprocedural-roadmap.md) +> and [`docs/notes/interprocedural-tz.md`](../docs/notes/interprocedural-tz.md). +> Never here. + +## 0. What this layer is + +The core checker ([OwnCore.md](OwnCore.md)) is **intraprocedural**: it reasons +about one function body. When an owned `IDisposable` crosses a method boundary — +passed to a callee, or returned from one — the caller cannot know what happened to +it without a *contract* for that boundary. This layer computes those contracts. + +It is **not a second checker**. It computes, per first-party method, a compact +**Method Ownership Summary (MOS)**, then **lowers** each summary to the core's +existing vocabulary at the call site (`consume` / `borrow` effects, an `acquire` +for a fresh result, an `alias_join` for an adopt). No verdict originates here: the +core still renders every OWN0xx. This is a *summary-contract* layer, not a +borrow-checker core (the Checker Framework's Resource Leak Checker is the closest +shipped analogue; Polonius is not the template). + +The **precision floor is `own-only 0`**: no rule in this document may fabricate a +`must`/`fresh`/alias contract. Every degradation resolves toward *silence*, and a +genuinely-unverifiable boundary is recorded as an advisory (§7), never guessed. + +## 1. The MOS artifact + +For each method `M` whose body is visible (first-party / same compilation) the +layer computes one `MethodSummary` ([`ownership.py`](../ownlang/ownership.py), +`MethodSummary`). It has two axes plus provenance: + +- **Per-parameter transfer** (only for the disposable-typed params the frontend + marks): `transfer ∈ {no, must, may, unknown}` (§2). +- **Per-return ownership**: `returns ∈ {fresh, aliasOf:, aliased, none, + unknown}` (§4). +- **`source ∈ {inferred, bcl, annotation, heuristic}`** — which tier produced the + summary. **Today production emits only `inferred`** (Tier A, §6): the BCL and + per-call-site tiers act at the *application* layer (§6), not as stamped + summaries. The field is reserved for the annotation/heuristic tiers. + +A second, **reserved** per-parameter axis, `escapes` ("the reference outlives the +call"), exists in the model but has **no producer** — derivation always leaves it +`False`, and it is deliberately **not serialized** (§8, `INF-R2`). The d5 design +keeps escape orthogonal to transfer; until a producer lands it must not be read as +evidence. + +The summary is **context-insensitive**: exactly one MOS per method, independent of +caller or call depth. The summary *is* the memoization. + +## 2. The transfer lattice + +`Transfer` ([`ownership.py`](../ownlang/ownership.py), `Transfer`, +`join`): did ownership of a disposable parameter leave the caller on the call? + +| value | meaning | +|---|---| +| `no` | borrowed — the caller keeps ownership (a leak if the caller never disposes) | +| `must` | transferred on **every** normal-return path | +| `may` | transferred on **some** paths, kept on others (partial consume) | +| `unknown` | insufficient evidence (extern callee, or an unresolved boundary) | + +- **INF-L1 (join).** `join(a, a) = a`; if either side is `unknown` the join is + `unknown` (absorbing); any other mix of distinct values is `may`. So one + un-characterizable path makes the whole parameter `unknown`, and a + transfer-path joined with a keep-path is `may` (path-dependent, and we know it). +- **INF-L2 (bottom).** `⊥` (Python `None`) is the fixpoint seed only (§5); it is + the identity of the join and **never escapes a solved summary** — a residual `⊥` + finalizes as `no` ("nothing demonstrably consumes it ⇒ it is kept"). + +## 3. Skeleton derivation — parameters (S-rules) + +Before solving, the bridge derives a per-method **skeleton** +([`ownir.py`](../ownlang/ownir.py), `_build_skeletons`): each disposable parameter +gets a set of **path actions** (`dispose` | `borrow` | `forward(callee, arg)`; +the `adopt`/`return` kinds are **reserved**, see `INF-S5`) that the solver joins. + +- **INF-S1 (explicit override).** An explicit `effect` on the parameter fact wins + over all inference: `consume → [dispose]`, `borrow`/`borrow_mut → [borrow]`, any + other string → `[]` (explicitly non-owning). A contract-only callee (no body) + therefore still resolves. +- **INF-S2 (definite release ⇒ dispose).** A body that releases the parameter is a + `dispose` path **only when the release is definite** — on **every** + normal-return path (`_definite_release`). A **partial** release (one branch, a + `while` body which may run zero times, or behind an early `return` that does not + release) emits **both** a `dispose` and a `borrow` path, so the join is `may` and + the caller stays plain. Flattening a partial release to `must` would charge a + caller's defensive dispose a false OWN002/OWN003 — the precision floor forbids it. +- **INF-S3 (single straight-line forward ⇒ resolved).** A parameter handed to + exactly one callee at exactly one top-level (straight-line) call site emits a + single `forward(callee, arg)` path (the solver resolves it, §5). Any + conditional / looped / multi-target forward **also** emits a `borrow` path, so + the join is `may`/`no`, never a fabricated `must`. +- **INF-S4 (used ⇒ borrow; else nothing).** A parameter only read/used emits + `[borrow]`; a parameter the body does nothing with emits `[]` (→ `no`). +- **INF-S5 (reserved kinds).** The path kinds `adopt` (store into an owning field, + interprocedural T4b) and `return` (return the parameter) are understood by the + solver as `must` but have **no production producer**: `_build_skeletons` never + emits them, and a returned parameter is deliberately **not** a consume signal + (that is wrap/alias, §4/§6, not consume). A port must carry their semantics but + must not expect them from real facts. +- **INF-S6 (sink channel resolves in place).** A forward to a fixed + ownership-sink extern (`$consume`/`$borrow`, §6) is recorded as a **resolved** + path directly (`$consume → dispose`, `$borrow → borrow`), not a forward edge. + `$borrow_mut` is **deliberately excluded** from this shortcut: the transfer + lattice has no shared-vs-exclusive axis, so summarizing it transitively would + downgrade an exclusive loan to a shared one — the wrapper param stays plain + instead (the direct `$borrow_mut` call keeps full exclusivity; tracker #122). + +## 4. Skeleton derivation — returns (R-rules) + +The return kind is inferred from the body +([`ownir.py`](../ownlang/ownir.py), `_infer_return_skeleton`): + +- **INF-R1.** No `return ` → `none` (void / no owned value). +- **INF-R2.** Any bare `return` / `return null` on some path → `none` (not + uniformly owned; a caller dropping the result must not be charged on that path). +- **INF-R3 (fresh).** `fresh` **iff every** returned local is `acquire`d in this + body **and** is not a parameter **and** is not also a `call` result on any path + (mixed origin degrades — claiming fresh there would make a caller acquire a value + it does not own on the non-acquire path). +- **INF-R4 (forward / BCL wrapper).** A single returned local that is a `call` + result (not a param, not acquired): if the callee is first-party → + `forward(callee)` (the solver resolves it through the callee's own return kind, + factory-of-factory); else if the callee is a curated BCL fresh-factory (§6, Tier + B) → `fresh` (a thin wrapper over a BCL factory is itself fresh); else + `forward(callee)` (which the solver degrades to `unknown` at the extern boundary). +- **INF-R5.** Anything else → `none` (not provably owned ⇒ no claim). + +## 5. The fixpoint solver (F-rules) + +The solver ([`ownership.py`](../ownlang/ownership.py), `solve` / `solve_with_log`) +resolves every method's MOS over the call graph. + +- **INF-F1 (graph).** Edges `M → C` for every first-party callee a parameter + forwards to (`forward` paths) and every forwarded return target — only within + the analyzed skeleton set (`_call_graph`). +- **INF-F2 (SCC order).** The graph is condensed into strongly-connected + components (iterative Tarjan) emitted bottom-up = reverse-topological, with + sorted adjacency for determinism. A callee in a lower SCC is resolved (and reused) + before any caller reads it; only same-SCC callees are still mid-iteration. +- **INF-F3 (param least fixpoint).** Within an SCC, each `(method, disposable + param)` is seeded at `⊥` and iterated to the least fixpoint on the height-3 + lattice; a residual `⊥` finalizes as `no`. Seeding at `⊥` (not a spurious `no`) + is what makes recursion **exact**: a method that disposes on its base case and + recurses otherwise resolves to `must`, and mutual recursion grounded by a dispose + carries `must` across the whole SCC, while recursion that never disposes settles + at `no`. +- **INF-F4 (no duplicate keys).** Two skeletons with the same method key raise + immediately (`ValueError`) — silently keeping the last would make summaries + input-order-dependent and corrupt the call graph. (Key collision-freedom for + overloads is handled by merging *before* the solver, §M-rules.) +- **INF-F5 (return chase).** A return has at most one forward target, so it is + resolved by an iterative (non-recursive, so a deep acyclic wrapper chain cannot + overflow), memoized, cycle-safe walk along forward-return edges: a + forward-return **cycle** → `unknown`; an **extern** target → `unknown` (logged); + an **`aliasOf:` propagated across a hop** → `unknown`, because remapping the + callee-space index to the caller's arguments needs a call argument map the + skeleton does not carry (the obligation-identity model, D5.4). `fresh` / `aliased` + / `none` / `unknown` propagate as-is; an unrecognised kind fails closed to + `unknown`, never silently `none`. +- **INF-F6 (observable degradation).** A failure of the solve degrades the **whole + interprocedural layer** to the empty MOS (the checker never crashes, forwards + stay plain), and the reason is surfaced as an advisory **OWN052** (§7) — never a + silent skip. In the Rust port this degradation is a `Result`, never a panic. +- **INF-F7 (extern log).** `solve_with_log` returns the sorted list of forwards — + param or return — that cross an **extern** (unsummarized) boundary: the `unknown`s + that come from *outside* the analyzed set. It is **not** a log of all `unknown`s; + the intrinsic precision-safe degradations (return-forward cycle, un-remappable + `aliasOf`, missing index, unrecognised shape) are deterministic from the input + and not logged. + +## M-rules — overloads + +The call node names a callee `{Type}.{Method}` **without a parameter signature** +([OwnIR §5](OwnIR.md)), so same-name overloads share a key and are **merged into +one conservative summary before solving** ([`ownir.py`](../ownlang/ownir.py), +`_merge_skeletons`, `_merge_returns`): + +- **INF-M1 (param join).** Union the parameter indices across overloads; an + overload that does nothing with an index contributes a `borrow` path (it *keeps* + the arg), so a parameter is `must` **only when every overload consumes it** — + never a fabricated `must` from an ambiguous name. +- **INF-M2 (return join).** `{fresh}` → `fresh`, `{none}` → `none`, `{aliased}` → + `aliased`; any mix, or a `forward`/`aliasOf` in the group (whose index is + overload-specific), degrades to `unknown` — never a fabricated `fresh`. +- **INF-M3 (arity residual).** Merging is by name only; disambiguation by arity or + argument type would need call-site type information the fact stream does not carry + today. The merge is precision-safe (never a false `must`/`fresh`), just coarser + than a per-signature split would be. (Roadmap stage 2.) + +## 6. Application at the call site (A-rules) and the tier ladder + +The solved MOS is **lowered** to the core's vocabulary during +`to_module`/`_lower_flow` ([`ownir.py`](../ownlang/ownir.py)). The precision floor +stays `own-only 0`; the tiers raise recall, higher overriding lower: + +- **Tier A — first-party inferred summaries** (§3–§5). The bulk of coverage; + `source = inferred`. +- **Tier B — curated BCL fresh-factory table** (`_BCL_FRESH_BY_NS`): well-known + static factories whose result the caller owns (`File.Open*`, `SHA256.Create`, + `XmlReader.Create`, `JsonDocument.Parse`, …), matched only on the exact bare + `Type.Method` or its fully-qualified identity under the real namespace. A + **first-party summary always overrides** the table (`INF-A4`). +- **Per-call-site contract channel** — the fixed sink externs + `$consume`/`$borrow`/`$borrow_mut`: an ownership effect the extractor pins at the + call site (e.g. `StreamReader(s, leaveOpen: false/true)`), resolved through the + same core signature path as any contracted call. + +Lowering rules: + +- **INF-A1 (param effect).** A parameter's lowered effect is: explicit `effect` > + inferred. For a forwarded parameter the solved transfer applies: `must → consume`, + `no → borrow`, `may`/`unknown → plain` (precision-first, §7). +- **INF-A2 (T1 fresh result).** A `call` binding a `result` whose callee summary + `returns = fresh` (or a Tier-B fresh factory) mints an `acquire` for that local — + the call site is a factory, so the result is a new owned obligation the leak / + double-release / use-after checks apply to. `_callee_returns_fresh` is the + **single source of truth** shared by the leak pre-scan, the branch-hoist safety + walk, and the lowering, so all three agree (`INF-A6`). +- **INF-A3 (T4 alias_join).** An `alias_join` op lowers the return-alias/adopt case + (D5.4): the new handle joins `src`'s obligation set (release/escape through + either discharges the one resource; both → OWN003; use-after → OWN002). An + `alias_join` over an untracked `src` makes **no claim** (must-only alias). +- **INF-A4 (tier precedence).** Tier A overrides Tier B for **every first-party + name**, including a name dropped from the summary set (an overload): a first-party + method never receives a fabricated BCL `fresh`. +- **INF-A5 (optimistic untrack).** A local handed to a summarized callee parameter + whose transfer is `may` or `unknown` is **untracked at that call** — its + obligation is not minted (its `acquire`/fresh-result/`alias_join` is skipped, and + it is excluded from branch-hoisting). Under the optimistic default this means + "the caller no longer owns it": neither a missing **nor** a defensive dispose + after the call is charged. The gap is recorded as advisory **OWN051** (§7). A + call carrying such positions is emitted through the per-argument `$`-channel (as + overloads are, `INF-M`), so an untracked name is never referenced in emitted core + code (which would raise OWN030, map-or-raise). +- **INF-A6 (kill on rebind).** Overwriting a tracked local (a re-bound `call` + result or `alias_join` target) kills its previous ownership binding first, so a + lost prior obligation leaks rather than reading as clean ([OwnIR §5](OwnIR.md)). + +## 7. The optimistic default and advisories + +The fact model and the *reporting policy* are separate. + +- **INF-P1 (optimistic default = own-only 0).** At an unverifiable-ownership call + site, resolve toward "caller no longer owns" → silent. A mis-`consume` loses a + real leak (recall — tolerable); a mis-`borrow` demands a dispose that may be wrong + (precision — not tolerable). This is the whole project's stance and the default. +- **INF-P2 (advisory OWN051).** When an **owned** local (an acquired local or a + fresh-factory result — not a plain value) is untracked by `INF-A5`, the layer + emits advisory **OWN051** at the call site: the honest record that ownership past + this call was not verified. Advisory means rendered as a `warning`, `level:note` + in SARIF, **excluded from the exit code**, hidden at `--verbosity quiet`. +- **INF-P3 (advisory OWN052).** When the solve degrades (`INF-F6`), the layer emits + advisory **OWN052**, module-level, with the inner error — the honest record that + cross-method contracts were skipped this run. +- **INF-P4 (strict mode — reserved).** A pessimistic mode (unknown call site → + assume borrow → report the leak) is designed (d5 §5) but **not implemented**; the + advisory channel and full `must`/`may` evidence exist regardless of mode. + +## 8. Serialization — the summary dump + +The solved summaries are observable and diffable via +`python -m ownlang summaries facts.json` ([CLI.md](CLI.md), +[`ownir.py`](../ownlang/ownir.py), `dump_summaries`): one deterministic JSON +document — summaries sorted by method key, the extern log sorted, a `degraded` +reason on solve failure. + +- **INF-R1 (determinism).** The document is **byte-identical** under any + `functions[]` input permutation: summaries sorted by key, extern log sorted, + fixed field order, merged-overload location taken as the min `(file, line)`. This + is what makes it a parity artifact (the Rust port of this layer is diffed against + it), not a debug log. +- **INF-R2 (no unproduced fields).** The reserved `escapes` axis (§1) is **not** + serialized — emitting an always-`False` field would freeze a lie into the parity + surface. Serialize it the day a producer lands, together with the producer. + +## 9. Scope / non-goals + +First-party (Tier A) + curated BCL (Tier B) + the per-call-site channel only. **No +IL/Cecil decompilation of third-party assemblies**; no cross-thread / async +disposal races; no context sensitivity or points-to (context-insensitive summaries +suffice — the floor is precision, not soundness). Annotations (Tier C) and a +pessimistic mode are reserved (§7, `INF-P4`). + +## 10. Rules + +- **INF-L1/L2** — lattice join; `⊥` is seed-only and finalizes `no`. +- **INF-S1–S6** — parameter skeleton derivation (explicit override; definite + release ⇒ dispose, partial ⇒ may; single straight-line forward; used ⇒ borrow; + reserved `adopt`/`return`; sink channel + `$borrow_mut` exclusion). +- **INF-R1–R5** — return skeleton derivation (none / bare-return / fresh / forward + / BCL-wrapper). +- **INF-M1–M3** — overload merge (param join, return join, arity residual). +- **INF-F1–F7** — the solver (graph, SCC order, param fixpoint, no duplicate keys, + return chase, observable degradation, extern log). +- **INF-A1–A6** — call-site application (param effect, fresh result, alias_join, + tier precedence, optimistic untrack, kill-on-rebind). +- **INF-P1–P4** — reporting policy (optimistic default, OWN051, OWN052, reserved + strict mode). +- **INF-R1/R2** (serialization) — deterministic dump; no unproduced fields. +- **The floor.** No rule may fabricate a `must`/`fresh`/alias contract; every + degradation resolves toward silence, and an unverifiable boundary is an advisory, + never a guess. + +## 11. Conformance + +Pinned by [`tests/test_ownership.py`](../tests/test_ownership.py) (the solver +lattice, `python tests/test_ownership.py`) and +[`tests/test_ownir.py`](../tests/test_ownir.py) (derivation + application + +serialization, `python tests/test_ownir.py`) — not `test_spec.py` (this is a +bridge/solver contract, not a surface-language rule): + +- **INF-L / INF-F** — `test_ownership.py`: join monotonicity, SCC convergence, + deep-chain termination, extern-boundary logging, duplicate-key raise, the + `aliasOf`-through-forward degradation, `to_dict` serialization. +- **INF-S2 (definite release)** — `test_ownir.py` "TZ D1": conditional / while-body + / early-return-guarded releases degrade to `may` (one OWN051, no verdict); + both-branch and release-then-return stay `consume`. +- **INF-S3 / INF-A1** — transitive consume/borrow through single vs conditional + forwards; two-hop chains. +- **INF-M1–M3** — agreeing overloads resolve `must`; disagreeing join to `may` + (OWN051); direct call to overloads routes through the channel. +- **INF-A2 / INF-A4** — first-party fresh result mints an acquire; Tier A overrides + the BCL table; BCL fresh factories and wrappers over them. +- **INF-A5 / INF-P2** — an owned local dropped/disposed after a `may`/`unknown` + call is silent with one OWN051; a verified borrow keeps the caller's obligation + (true OWN001); a plain value at a `may` position stays quiet. +- **INF-F6 / INF-P3** — a patched-to-raise solver yields exactly one OWN052 and no + fabricated verdicts; a healthy solve carries none. +- **INF-R1/R2 (serialization)** — the `summaries` dump is byte-identical under + input permutation; the `escapes` axis is omitted. + +A change to this spec without a matching change under `tests/test_ownership.py` / +`tests/test_ownir.py` (or vice-versa) is a red build. diff --git a/spec/README.md b/spec/README.md index ceef0d6c..f6b144ea 100644 --- a/spec/README.md +++ b/spec/README.md @@ -15,6 +15,7 @@ stop aspirational docs from lying about the code. | [Diagnostics.md](Diagnostics.md) | every OWN code, grouped, linked to the rule that raises it | | [CodegenContract.md](CodegenContract.md) | the checker↔codegen contract C1–C4, lowering modes | | [OwnIR.md](OwnIR.md) | the frontend↔core fact seam (JSON): envelope, versioning + evolution policy, resource-kind + flow-op vocabulary, DI graph, rules IR1–IR6 | +| [Inference.md](Inference.md) | the interprocedural ownership-inference layer: the MOS artifact, transfer lattice, derivation (S/R/M-rules), the solver (F-rules), call-site application (A-rules), optimistic default + advisories (OWN051/052), rules INF-* | | [ownir.schema.json](ownir.schema.json) | the machine-readable OwnIR schema (JSON Schema 2020-12) — the single source the Python core and the Rust `own-ir` crate are checked against; its enums are pinned to the code's authoritative sets by `tests/test_ownir.py` | | [CLI.md](CLI.md) | the `check` / `emit` / `cfg` / `report` commands | @@ -29,6 +30,9 @@ checker cannot silently drift: buffer specifics) are covered by the suites below. - `tests/test_gallery.py`, `tests/test_lifetimes.py`, `tests/test_wpf.py`, `tests/test_corpus.py` — broader pinned examples. +- `tests/test_ownir.py`, `tests/test_ownership.py` — the bridge/solver contracts + ([OwnIR.md](OwnIR.md) rules IR*, [Inference.md](Inference.md) rules INF*), + pinned at the facts/summary level rather than via `.own` source. A spec change without a matching test change (or vice-versa) is a red build. To add a rule: write it here with an ID, add its example to `test_spec.py`, and add diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 39586821..c908dd30 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1728,6 +1728,13 @@ def _boom2(_sk): # type: ignore[no-untyped-def] if (darkdoc["summaries"] != [] or darkdoc["unresolved"] != [] or "synthetic dump failure" not in (darkdoc["degraded"] or "")): fails.append(f"degraded summaries dump wrong: {darkdoc}") + # spec/Inference.md conformance: the advisory codes the spec names (OWN051, + # OWN052) must be registered in the catalogue — a spec that references an + # unregistered code, or a dropped code, is drift the build must catch. + checks += 1 + missing = [c for c in ("OWN051", "OWN052") if c not in TITLES] + if missing: + fails.append(f"Inference.md names unregistered code(s): {missing}") # (§10 q2) same-name OVERLOADS are merged, not dropped: when EVERY overload of a # name consumes the forwarded arg, a forward to that name resolves to `must`, so a # caller using the local after the handoff is OWN002. Before the merge the name was From fc94b5751e054ae01f163aac403e849c09d35b17 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 8 Jul 2026 06:02:15 +0000 Subject: [PATCH 11/12] fix: satisfy lint for the summaries bridge (Codex follow-up) Codex's follow-up run flagged two Ruff findings its sandbox commit never reached this branch with: the un-formatted import block in cmd_summaries (I001) and the quoted Finding annotation in to_module (UP037). Applied the same fixes here. --- ownlang/__main__.py | 1 + ownlang/ownir.py | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/ownlang/__main__.py b/ownlang/__main__.py index f2efbf6f..75b89b1e 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -314,6 +314,7 @@ def cmd_summaries(path: str) -> int: this surface reports state, it does not judge); 2 only for unreadable facts, like `ownir`.""" import json + from .ownir import OwnIRError, dump_summaries, load try: doc = dump_summaries(load(path)) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index acd1e870..74a5b79a 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -824,7 +824,7 @@ def _prelude_resources() -> list[ResourceDecl]: def to_module(facts: dict[str, Any], notes: list[str] | None = None, - advisories: list["Finding"] | None = None, + advisories: list[Finding] | None = None, ) -> tuple[Module, dict[str, dict[str, Any]]]: """Build the core `Module` AST **directly** from OwnIR facts — no `.own` source text and no re-parse (P-016 B0a; the round-trip `to_own` + `parse` has existed From 77446cd63708eb2e9b7b06d659a97c6189f85723 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 8 Jul 2026 06:12:04 +0000 Subject: [PATCH 12/12] fix(d5): early-return forwards join to may; untrack keeps pre-call verdicts (Codex P1+P2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two review findings on the interprocedural layer, both reproduced before fixing: P2 (S2 / INF-S3): a body like 'if (c) return; Sink(x)' kept exactly one top-level forward, so the shape counted as an unconditional handoff and solved to must — leaking the callee's own parameter on the guard path and charging the caller's defensive Dispose a false OWN002. The unconditional test now also requires no return reachable before the forward (_early_return_before_forward), the forward twin of D1's partial-release rule. Recorded as TZ D7. P1 (INF-A5): the optimistic untrack applied to the whole body, so a local passed to a may/unknown position anywhere lost its PRE-call verdicts too (acquire s; release s; use s; maybe(s) reported nothing but OWN051). Split into two mechanisms (_kill_sites_for_unverified): a top-level unverified call keeps the local fully tracked up to the call, discharges it there with a $consume on the handle (sound: a top-level call lies on every path to the exit), and unmaps it after — so the checked region now matches OWN051's 'not checked past this call'. In-branch calls keep the conservative whole-body untrack (a branch-local discharge would fabricate OWN001/OWN009 on the other path); the residual is recorded in TZ D6 and INF-A5b. Spec: INF-S3 + INF-A5a/A5b updated, conformance list extended. Tests: 3 new pins (pre-call OWN002 beside OWN051, post-call silence, early-return forward), 248/248 bridge checks green. --- docs/notes/interprocedural-tz.md | 71 +++++++++--- ownlang/ownir.py | 180 +++++++++++++++++++++++++++---- spec/Inference.md | 46 +++++--- tests/test_ownir.py | 56 ++++++++++ 4 files changed, 308 insertions(+), 45 deletions(-) diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md index f7b6f980..c8ac42a5 100644 --- a/docs/notes/interprocedural-tz.md +++ b/docs/notes/interprocedural-tz.md @@ -46,7 +46,7 @@ concern») — значит, закрытый enum флоу-опов обяза SCC — текущая итерация (возможно ⊥); недостижимая ветка → `unknown` fail-closed (`:288`). -### 2.3 Деривация скелета параметра (S-правила, `ownir.py:1444-1494`) +### 2.3 Деривация скелета параметра (S-правила, `_build_skeletons` + `_param_signals`, ownir.py) - **S1** Явный `effect` в факте — авторитет: `consume`→`[dispose]`, `borrow|borrow_mut`→`[borrow]`, иная строка→`[]` (не-владеющий). Инференция @@ -54,9 +54,9 @@ SCC — текущая итерация (возможно ⊥); недостиж - **S2** Иначе — по сигналам `(rel, passed, used)` (`_param_signals`, рекурсия в `if`/`while`), с приоритетом: `rel`→`[dispose]` (⚠ D1); иначе `passed`→ forward-рёбра всех вызовов, и если НЕ (ровно одно ребро всего - ∧ ровно одно на верхнем уровне) — добавить `[borrow]`, чтобы join дал - `may`/`no`, а не ложный `must` (`:1482-1486`); иначе `used`→`[borrow]`; - иначе `[]`. + ∧ ровно одно на верхнем уровне ∧ нет `return`, достижимого ДО этого вызова — + D7) — добавить `[borrow]`, чтобы join дал `may`/`no`, а не ложный `must`; + иначе `used`→`[borrow]`; иначе `[]`. - **S3** Forward в sink-extern резолвится на месте (`_forward_path_action:1361`): `$consume`→`dispose`, `$borrow`→`borrow`; `$borrow_mut` **сознательно отсутствует** в `_SINK_PATH_ACTION:1192` — остаётся forward-ребром к @@ -244,15 +244,60 @@ OWN001. Канал существовал до D1 (условные forward'ы), > **Статус: исправлено (untrack).** Аргумент на `may`/`unknown`-позиции > суммаризированного callee **прекращает отслеживаться** в вызывающем -> (`_unverified_transfer_calls` + гейты в лоуэринге: acquire/fresh/alias не -> минтятся, hoist исключён): ни пропущенный, ни защитный dispose после такого -> вызова не наказуем. Вызов с `may`/`unknown`-позициями эмитится через -> по-аргументные `$`-каналы (расширение M3-маршрутизации) — untracked-имя не -> упоминается в эмитируемом коде (иначе map-or-raise OWN030, что и поймал -> первый прогон). Проверенные контракты не тронуты: borrow-drop (T3 OWN001) и -> consume-reuse (T2 OWN002) запиннены тестами. `$`-синки и несуммаризированные -> callee не затронуты (первые — проверенные контракты, вторые экстрактор -> escape-дропает сам). +> (`_unverified_transfer_calls` + гейты в лоуэринге): ни пропущенный, ни +> защитный dispose после такого вызова не наказуем. Вызов с +> `may`/`unknown`-позициями эмитится через по-аргументные `$`-каналы +> (расширение M3-маршрутизации) — untracked-имя не упоминается в эмитируемом +> коде (иначе map-or-raise OWN030, что и поймал первый прогон). Проверенные +> контракты не тронуты: borrow-drop (T3 OWN001) и consume-reuse (T2 OWN002) +> запиннены тестами. `$`-синки и несуммаризированные callee не затронуты +> (первые — проверенные контракты, вторые экстрактор escape-дропает сам). +> +> **Уточнение (Codex P1): untrack — с точки вызова, не на всё тело.** Первая +> реализация снимала отслеживание на всей функции (acquire не минтился вовсе), +> и вместе с ним глотала **до-вызовные** вердикты: в `acquire s; release s; +> use s; maybe(s)` реальный use-after-release исчезал, оставался только OWN051 — +> хотя advisory обещает «not checked past this call». Исправлено раздвоением +> механизма (`_kill_sites_for_unverified`): +> +> - **top-level вызов ⇒ kill-site.** Локал, чей unverified-вызов стоит на +> верхнем уровне тела, трекается нормально ДО вызова (до-вызовный OWN002 +> всплывает), в точке вызова гасится честным `$consume` по его handle +> (top-level вызов лежит на каждом пути от предшествующих op'ов к выходу — +> discharge корректен на всех путях) и размапливается после (пост-вызовная +> тишина прежняя). +> - **вызов в ветке/цикле ⇒ старый whole-body untrack (остаточный дефект).** +> Точки discharge, покрывающей все пути, у ветвевого вызова нет: `$consume` +> внутри ветки погасил бы только её путь и сфабриковал OWN001/OWN009 на +> другом (защитный `Dispose()` после merge — ровно та идиома, ради которой +> канал строился). Пока в ядре нет maybe-moved состояния, такие локалы не +> минтятся вовсе — «no-call branch leak» из примера Codex P1 остаётся +> незамеченным (честная цена, записана здесь и в INF-A5b). + +### D7 (Codex P2, воспроизведено исполнением): ранний `return` не делал forward условным + +`if (c) return; Sink(x)` — единственный forward, и он на верхнем уровне, так что +S2-проверка «ровно одно ребро ∧ на верхнем уровне» считала передачу +безусловной: `[forward]` → join `must`. Но guard-путь выходит из тела, не +передав владение — ровно тот же класс, что частичный release из D1, только для +forward-ветки правила. Репро (два ложных вердикта на корректном защитном коде): + +```text +# callee: if c: return; sink(x) (sink: consume+release); caller: acquire r; call(r); release r +# было: +# OWN001 'x' is never disposed (leak) (в callee — параметр «утёк» на guard-пути) +# OWN002 'r' is used after it is disposed (в caller — ЛОЖНЫЙ: защитный Dispose наказан) +# стало: 0 findings, 1 advisory OWN051 (join = may) +``` + +> **Статус: исправлено.** Условие безусловности S2 расширено третьим конъюнктом: +> нет `return`, достижимого до самого forward-вызова +> (`_early_return_before_forward`: обход тела по порядку, `return` на любой +> глубине до первого top-level вызова с `pname` ⇒ передача частична ⇒ +> добавляется `[borrow]`, join даёт `may`). Симметрия с D1 намеренная: у release +> путь-чувствительность даёт `_definite_release`/`exits_ok`, у forward — этот +> хелпер. Норма — INF-S3 в `spec/Inference.md`; тест — «S2 early return» в +> `test_ownir.py`. ### D5: сбой решателя молчит diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 74a5b79a..c178e4d8 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -994,14 +994,22 @@ def to_module(facts: dict[str, Any], released, mos) # The optimistic default (d5 §5), made real: an argument at a call # position whose contract resolved `may`/`unknown` means "we cannot - # verify whether ownership left the caller" — so the caller's local is - # UNTRACKED from that call's function (its acquire is not minted), and - # neither a missing nor a defensive dispose after the call can be - # charged. Anything less is not silence: a plain arg leaves the - # obligation with the caller, so dropping it fabricates OWN001 on the - # ubiquitous null-guard-helper idiom (TZ итерация 6). + # verify whether ownership left the caller" — so the caller's local + # stops being checked AT that call, and neither a missing nor a + # defensive dispose after it can be charged. Anything less is not + # silence: a plain arg leaves the obligation with the caller, so + # dropping it fabricates OWN001 on the ubiquitous null-guard-helper + # idiom (TZ итерация 6). Two mechanisms, by call position (Codex P1): + # - a TOP-LEVEL unverified call dominates the function exit, so the + # local is tracked NORMALLY up to it (a pre-call use-after-release + # still surfaces) and discharged at the call site (`kill_sites` — + # a `$consume` on the handle), with later references unmapped; + # - an IN-BRANCH unverified call has no all-paths discharge point the + # core could accept without a maybe-moved state, so those locals + # keep the conservative whole-body untrack (acquire never minted). unverified = _unverified_transfer_calls(nodes, mos) - untracked = frozenset(a for a, _c, _t, _l in unverified) + kill_sites = _kill_sites_for_unverified(nodes, mos) + untracked = frozenset(a for a, _c, _t, _l in unverified) - kill_sites.keys() if advisories is not None and unverified: # OWN051, gated on args that actually carry an obligation here (an # acquired local or a fresh factory result) — a plain value passed @@ -1042,7 +1050,7 @@ def to_module(facts: dict[str, Any], fbody = [*hoisted_lets, *_lower_flow(nodes, ffile, fname, handles, loc, localmap, released, mos, set(hoist), first_party, overloaded, - untracked)] + untracked, kill_sites)] # A body that returns a value gets an owned return type, so the core # models `return s` as a valid ESCAPE (the value is discharged to the # caller) instead of a void-return mismatch that would leave `s` looking @@ -1136,6 +1144,76 @@ def walk(ns: Any) -> None: return out +def _kill_sites_for_unverified( + nodes: Any, mos: dict[str, Any] | None) -> dict[str, int]: + """`local name -> id()` of the TOP-LEVEL call op where its tracking stops — + the flow-aware half of the optimistic default (Codex P1). A local handed to + a `may`/`unknown`-contract position used to be untracked across the WHOLE + body, which also swallowed real pre-call verdicts (`acquire s; release s; + use s; maybe(s)` lost its use-after-release). A top-level unverified call + lies on every path from the ops before it to the function exit, so the + bridge can do better with no maybe-moved core state: keep the local fully + tracked up to the call, discharge it there (`$consume` on the handle — the + optimistic "ownership left"), and unmap it after (later uses/releases stay + silent, exactly what OWN051 advertises). + + Only a name already MINTED in this body before the call (an `acquire`, an + `alias_join`, or a call `result`) gets a kill site — anything else (a param, + a plain value, a mint that oddly follows the call) keeps the conservative + whole-body untrack. Calls inside `if`/`while` never produce a kill site: a + branch-local `$consume` discharges only that path and would fabricate an + OWN001/OWN009 on the other one, so those stay whole-body untracked too.""" + sites: dict[str, int] = {} + if mos is None or not isinstance(nodes, list): + return sites + minted: set[str] = set() + + def collect_mints(n: Any) -> None: + if not isinstance(n, dict): + return + op = n.get("op") + if op in ("acquire", "alias_join"): + v = n.get("var") + if isinstance(v, str): + minted.add(v) + elif op == "call": + r = n.get("result") + if isinstance(r, str) and r: + minted.add(r) + elif op == "if": + for key in ("then", "else"): + sub = n.get(key) + if isinstance(sub, list): + for x in sub: + collect_mints(x) + elif op == "while": + sub = n.get("body") + if isinstance(sub, list): + for x in sub: + collect_mints(x) + + for n in nodes: + if not isinstance(n, dict): + continue + if n.get("op") == "call": + callee = str(n.get("callee", "")) + summ = mos.get(callee) if callee else None + if summ is None and callee: + identity = _canonical_callee_name(callee) + if identity != callee: + summ = mos.get(identity) + args = n.get("args", []) + if summ is not None and isinstance(args, list): + for j, a in enumerate(args): + ps = next((q for q in summ.params if q.index == j), None) + if (ps is not None + and ps.transfer in (Transfer.MAY, Transfer.UNKNOWN) + and str(a) in minted and str(a) not in sites): + sites[str(a)] = id(n) + collect_mints(n) + return sites + + def _returns_value(nodes: Any) -> bool: """True if a flow body returns a VALUE on some path (a `return` op carrying a `var`), recursing into if/while. The bridge then gives the function an owned @@ -1551,6 +1629,47 @@ def _forward_targets(pname: str, nodes: Any, return out +def _contains_return(node: Any) -> bool: + """True if `node` (one op dict) is a `return` or can reach one inside its + `if` branches / `while` body. Used to spot an exit that BYPASSES a later + forward.""" + if not isinstance(node, dict): + return False + op = node.get("op") + if op == "return": + return True + if op == "if": + subs = [node.get("then"), node.get("else")] + elif op == "while": + subs = [node.get("body")] + else: + return False + return any(isinstance(s, list) and any(_contains_return(x) for x in s) + for s in subs) + + +def _early_return_before_forward(pname: str, nodes: Any) -> bool: + """True when a `return` op can exit the body BEFORE its single top-level + forward of `pname` runs. `if (c) return; Sink(x)` leaves the forward + top-level and unique, but the early-return path never transfers ownership — + calling that shape "unconditional" flattens the join to `must`, leaks the + callee's own parameter on the guarded path and charges the caller's + defensive dispose a false OWN002 (Codex P2; the forward twin of TZ D1's + partial release). Ops at or after the forward cannot bypass it, so the walk + stops at the first top-level op that hands `pname` on.""" + if not isinstance(nodes, list): + return False + for n in nodes: + if not isinstance(n, dict): + continue + if n.get("op") == "call" and any( + str(a) == pname for a in (n.get("args") or [])): + return False # reached the forward first — nothing bypassed it + if _contains_return(n): + return True + return False + + def _forward_path_action(callee: str, arg: int) -> PathAction: """The skeleton path action for one forward edge. A forward to a fixed ownership-sink extern (D5.1b) is a *resolved* transfer recorded directly @@ -1690,9 +1809,11 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: allt = _forward_targets(cname, body) top = _forward_targets(cname, body, recurse=False) paths = tuple(_forward_path_action(c, j) for c, j in allt) - if not (len(allt) == 1 and len(top) == 1): + if not (len(allt) == 1 and len(top) == 1 + and not _early_return_before_forward(cname, body)): # not a single unconditional handoff: a no-transfer path - # exists (other branch / zero-trip loop / sibling call), so + # exists (other branch / zero-trip loop / sibling call / + # early return skipping the forward — Codex P2), so # the join is `may`/`no`, never a false `must`. paths = (*paths, PathAction("borrow")) elif used: @@ -1933,7 +2054,8 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, hoisted: set[str] | None = None, first_party: frozenset[str] = frozenset(), overloaded: frozenset[str] = frozenset(), - untracked: frozenset[str] = frozenset()) -> list[Stmt]: + untracked: frozenset[str] = frozenset(), + kill_sites: dict[str, int] | None = None) -> list[Stmt]: """Lower one OwnIR flow body (B0b/B2) into core statements. acquire/use/release/ return reference a C# local by name (`var`); `if` carries `then`/`else` sub-bodies; `while` carries a `body` (a back-edge — the core's worklist fixpoint @@ -1953,10 +2075,18 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, reject as OWN030. `untracked` names (see `_unverified_transfer_calls`) are locals handed to a - `may`/`unknown`-contract position: the optimistic default assumes ownership - left the caller, so their acquires / fresh mints / alias mints are NOT emitted - — later releases/uses of them resolve to nothing and stay silent, and the gap - is surfaced as an advisory OWN051 instead of a fabricated verdict.""" + `may`/`unknown`-contract position INSIDE a branch or loop: the optimistic + default assumes ownership left the caller, so their acquires / fresh mints / + alias mints are NOT emitted — later releases/uses of them resolve to nothing + and stay silent, and the gap is surfaced as an advisory OWN051 instead of a + fabricated verdict. + + `kill_sites` (see `_kill_sites_for_unverified`) carries the flow-aware case + (Codex P1): a local whose unverified handoff is a TOP-LEVEL call is tracked + normally up to that call (pre-call bugs still surface), discharged there with + a `$consume` on its handle, and unmapped after it — the post-call silence is + the same, but the checked region now honestly matches OWN051's "not checked + past this call".""" hoisted = hoisted or set() body: list[Stmt] = [] for n in nodes: @@ -2036,16 +2166,16 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, en = n.get("else", []) then_b = _lower_flow(tn if isinstance(tn, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded, untracked) + first_party, overloaded, untracked, kill_sites) else_b = _lower_flow(en if isinstance(en, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded, untracked) + first_party, overloaded, untracked, kill_sites) body.append(If("?", then_b, else_b, line)) elif op == "while": bn = n.get("body", []) body_b = _lower_flow(bn if isinstance(bn, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party, overloaded, untracked) + first_party, overloaded, untracked, kill_sites) body.append(While("?", body_b, line)) elif op == "call": # A call to a CONTRACTED callee (a function/extern whose signature the @@ -2100,6 +2230,20 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, arg_refs: list[Expr] = [VarRef(localmap.get(str(a), str(a)), line) for a in raw_args] body.append(Call(callee, arg_refs, line)) + # The kill site of a tracked local (Codex P1): THIS top-level call hands + # it to a may/unknown position, so discharge the obligation here — the + # optimistic "ownership left the caller" as a real `$consume` on the + # handle — and unmap the name, silencing every later reference. Pre-call + # verdicts (a use-after-release before this line) already surfaced from + # the normally-emitted statements above. + if kill_sites and isinstance(raw_args, list): + for a in raw_args: + aname = str(a) + if kill_sites.get(aname) == id(n): + killed = localmap.pop(aname, None) + if killed is not None: + body.append(Call("$consume", + [VarRef(killed, line)], line)) # P-005 D5.2 (T1): if the call binds a result and the callee is a known # `fresh`-returning factory, the result is a newly-owned local — mint an # acquire for it (the args' effects, if any, were applied by the Call diff --git a/spec/Inference.md b/spec/Inference.md index eae95bd3..b43b4628 100644 --- a/spec/Inference.md +++ b/spec/Inference.md @@ -94,10 +94,13 @@ the `adopt`/`return` kinds are **reserved**, see `INF-S5`) that the solver joins the caller stays plain. Flattening a partial release to `must` would charge a caller's defensive dispose a false OWN002/OWN003 — the precision floor forbids it. - **INF-S3 (single straight-line forward ⇒ resolved).** A parameter handed to - exactly one callee at exactly one top-level (straight-line) call site emits a - single `forward(callee, arg)` path (the solver resolves it, §5). Any - conditional / looped / multi-target forward **also** emits a `borrow` path, so - the join is `may`/`no`, never a fabricated `must`. + exactly one callee at exactly one top-level (straight-line) call site, with + **no `return` op reachable before that call** (an early return would exit the + body without transferring — the forward twin of the partial release in + `INF-S2`), emits a single `forward(callee, arg)` path (the solver resolves + it, §5). Any conditional / looped / multi-target / return-skippable forward + **also** emits a `borrow` path, so the join is `may`/`no`, never a fabricated + `must`. - **INF-S4 (used ⇒ borrow; else nothing).** A parameter only read/used emits `[borrow]`; a parameter the body does nothing with emits `[]` (→ `no`). - **INF-S5 (reserved kinds).** The path kinds `adopt` (store into an owning field, @@ -233,14 +236,26 @@ Lowering rules: name**, including a name dropped from the summary set (an overload): a first-party method never receives a fabricated BCL `fresh`. - **INF-A5 (optimistic untrack).** A local handed to a summarized callee parameter - whose transfer is `may` or `unknown` is **untracked at that call** — its - obligation is not minted (its `acquire`/fresh-result/`alias_join` is skipped, and - it is excluded from branch-hoisting). Under the optimistic default this means - "the caller no longer owns it": neither a missing **nor** a defensive dispose - after the call is charged. The gap is recorded as advisory **OWN051** (§7). A - call carrying such positions is emitted through the per-argument `$`-channel (as - overloads are, `INF-M`), so an untracked name is never referenced in emitted core - code (which would raise OWN030, map-or-raise). + whose transfer is `may` or `unknown` stops being checked **at that call**. Under + the optimistic default this means "the caller no longer owns it": neither a + missing **nor** a defensive dispose after the call is charged. The gap is + recorded as advisory **OWN051** (§7). A call carrying such positions is emitted + through the per-argument `$`-channel (as overloads are, `INF-M`), so an + untracked name is never referenced in emitted core code (which would raise + OWN030, map-or-raise). Two mechanisms, by call position: + - **INF-A5a (top-level call ⇒ kill site).** A local already minted in the body + whose unverified handoff is a **top-level** call is tracked normally **up to** + that call (a pre-call use-after-release still surfaces), discharged **at** it + (a `$consume` on its handle — the optimistic "ownership left" made real, sound + because a top-level call lies on every path from the preceding ops to the + exit), and unmapped after it (later references stay silent). + - **INF-A5b (in-branch call ⇒ whole-body untrack).** A local whose unverified + handoffs are all inside `if`/`while` has **no** all-paths discharge point: a + branch-local `$consume` would discharge only that path and fabricate an + OWN001/OWN009 on the other. Its obligation is therefore not minted at all + (its `acquire`/fresh-result/`alias_join` is skipped, and it is excluded from + branch-hoisting) — the conservative residual, checked by nothing but the + OWN051 note, until the core grows a maybe-moved state. - **INF-A6 (kill on rebind).** Overwriting a tracked local (a re-bound `call` result or `alias_join` target) kills its previous ownership binding first, so a lost prior obligation leaks rather than reading as clean ([OwnIR §5](OwnIR.md)). @@ -325,14 +340,17 @@ bridge/solver contract, not a surface-language rule): / early-return-guarded releases degrade to `may` (one OWN051, no verdict); both-branch and release-then-return stay `consume`. - **INF-S3 / INF-A1** — transitive consume/borrow through single vs conditional - forwards; two-hop chains. + forwards; two-hop chains; an early-return-skipped forward joins to `may` (one + OWN051, no leaked callee param, no charged defensive dispose). - **INF-M1–M3** — agreeing overloads resolve `must`; disagreeing join to `may` (OWN051); direct call to overloads routes through the channel. - **INF-A2 / INF-A4** — first-party fresh result mints an acquire; Tier A overrides the BCL table; BCL fresh factories and wrappers over them. - **INF-A5 / INF-P2** — an owned local dropped/disposed after a `may`/`unknown` call is silent with one OWN051; a verified borrow keeps the caller's obligation - (true OWN001); a plain value at a `may` position stays quiet. + (true OWN001); a plain value at a `may` position stays quiet; a use-after-release + **before** a top-level `may` call keeps its OWN002 beside the advisory + (INF-A5a), while post-call defensive dispose/use stays silent. - **INF-F6 / INF-P3** — a patched-to-raise solver yields exactly one OWN052 and no fabricated verdicts; a healthy solve carries none. - **INF-R1/R2 (serialization)** — the `summaries` dump is byte-identical under diff --git a/tests/test_ownir.py b/tests/test_ownir.py index c908dd30..89f5da28 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1641,6 +1641,62 @@ def _sub(source: str | None) -> list[Finding]: if d6plain: fails.append("untrack: a non-owned value at a may-position must stay quiet, " f"got {[(x.component, x.code) for x in d6plain]}") + # (Codex P1) the untrack must not swallow PRE-call verdicts: a local is + # tracked normally up to its top-level may-call, so a use-after-release + # BEFORE the handoff still surfaces (before the fix the whole-body untrack + # skipped the acquire and the real OWN002 vanished, leaving only OWN051). + checks += 1 + p1pre = check_facts({"module": "M", "functions": [ + {"name": "cond_rel5", "file": "K.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "pre_bug", "file": "K.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "release", "var": "r", "line": 11}, + {"op": "use", "var": "r", "line": 12}, + {"op": "call", "callee": "cond_rel5", "args": ["r"], "line": 13}]}]}) + gotp1 = sorted((x.component, x.code, x.advisory) for x in p1pre) + if gotp1 != [("pre_bug", "OWN002", False), ("pre_bug", "OWN051", True)]: + fails.append("kill-site untrack: a pre-call use-after-release must keep its " + f"OWN002 beside the OWN051 advisory, got {gotp1}") + # (Codex P1) ... while the POST-call region keeps the optimistic silence: the + # kill-site `$consume` discharges the obligation on every path through the + # top-level call, so a defensive dispose after it is still uncharged. + checks += 1 + p1post = check_facts({"module": "M", "functions": [ + {"name": "cond_rel6", "file": "K.cs", "params": [{"name": "x", "line": 1}], + "body": [{"op": "if", "line": 2, + "then": [{"op": "release", "var": "x", "line": 3}], "else": []}]}, + {"name": "post_guard", "file": "K.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "cond_rel6", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}, + {"op": "use", "var": "r", "line": 13}]}]}) + gotp1p = [(x.component, x.code, x.advisory) for x in p1post] + if gotp1p != [("post_guard", "OWN051", True)]: + fails.append("kill-site untrack: post-call defensive dispose/use must stay " + f"silent (one OWN051 advisory), got {gotp1p}") + # (Codex P2) an early return SKIPPING the single top-level forward makes the + # handoff conditional: `guarded(x){ if(c) return; sink(x); }` must join to + # `may`, so the guarded helper does not leak its own param and a caller's + # defensive dispose is not charged a false OWN002 (the forward twin of D1). + checks += 1 + p2er = check_facts({"module": "M", "functions": [ + {"name": "sink_er", "file": "K.cs", + "params": [{"name": "x", "effect": "consume", "line": 1}], + "body": [{"op": "release", "var": "x", "line": 2}]}, + {"name": "guarded", "file": "K.cs", "params": [{"name": "s", "line": 5}], + "body": [{"op": "if", "line": 6, "then": [{"op": "return", "line": 7}], + "else": []}, + {"op": "call", "callee": "sink_er", "args": ["s"], "line": 8}]}, + {"name": "guarded_user", "file": "K.cs", + "body": [{"op": "acquire", "var": "r", "line": 10}, + {"op": "call", "callee": "guarded", "args": ["r"], "line": 11}, + {"op": "release", "var": "r", "line": 12}]}]}) + gotp2 = [(x.component, x.code, x.advisory) for x in p2er] + if gotp2 != [("guarded_user", "OWN051", True)]: + fails.append("S2 early return: a return-skipped forward must join to `may` " + f"— no verdicts, one OWN051 advisory, got {gotp2}") # (TZ D5) a failed MOS solve must degrade OBSERVABLY: the bridge drops to # no-MOS (checker stays alive, forwards stay plain — no fabricated verdicts) # and surfaces ONE advisory OWN052 naming the inner error. Before the fix the