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..9a9bc490 --- /dev/null +++ b/docs/notes/interprocedural-roadmap.md @@ -0,0 +1,295 @@ +# Дорожная карта — путь к «нормальной межпроцедурке» + +> Статус: **живая дорожная карта** (не нормативная спека, не 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), +> [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). Она **ссылается, а не +> дублирует**: детали каждого шага живут в первоисточнике, здесь — порядок, +> зависимости и критерий «готово». Рабочее ТЗ слоя — нормативные правила +> как-есть, инварианты, найденные расхождения (включая воспроизведённый +> precision-дефект D1) и требования к Rust-порту — в +> [interprocedural-tz.md](interprocedural-tz.md). +> +> Приоритет прежний: карта **подчинена альфе** +> ([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. Поправка на 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`; она закреплена только примерами в +`tests/test_ownir.py`. Это риск R2 ревью и жёсткий пререквизит tech-debt §3 +(«spec it or relocate it — до любого порта»). Каждый следующий этап меняет именно +этот слой; менять неспецифицированное — дороже всего. + +**Сделано:** + +- ✅ **`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) не сработал. Спека делает перенос механическим, когда + сработает. + +**Критерий готовности:** новый разработчик (или порт) может реализовать +инференцию по спеке, не читая `ownir.py`; расхождение спеки и кода ловится CI. +✅ по спеке; golden facts — остаток. + +## 4. Этап 1 — наблюдаемость: OWN051 + дамп сводок (дни) + +d5-заметка ставит advisory в хвост (D5.x); эта карта его **поднимает**: канал +«ownership transfer unverified» — самый дешёвый способ *увидеть* межпроцедурку +и главный ответ на «непонятки». Вся фактура уже считается (§5 d5: «we compute +the full must/may/escape evidence regardless of mode»), не хватает поверхности: + +- **OWN051** ✅ *(shipped)*: владелец, переданный на `may`/`unknown`-позицию, + оптимистично перестаёт отслеживаться (ТЗ D6 — настоящее «молчание», а не + plain), и это честно фиксируется advisory OWN051 на месте вызова — warning в + выводе, `note` в SARIF, никогда не rc; `--verbosity quiet` скрывает. +- **Дамп сводок** ✅ *(shipped)*: глагол `python -m ownlang summaries facts.json` + — один детерминированный JSON-документ (сводки по ключу метода + extern-лог + + `degraded`), байт-стабильный под перестановкой входа; это и отладочная + поверхность, и замороженный паритетный артефакт порта (ТЗ §5.4). Смотришь на + метод — видишь, что решатель про него думает и почему вызов остался plain. + +**Критерий готовности:** на любом прогоне можно ответить «почему этот вызов +не consume/borrow/fresh» без чтения кода моста. С началом Rust-порта у этапа +появляется вторая роль (§2): нормализованный дамп сводок — паритетный артефакт, +по которому диффуются Python- и Rust-стороны инференции. + +## 5. Этап 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`, чтобы не делать двух миграций. + +## 6. Этап 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. + +## 7. Этап 4 — провенанс паблишера, #146 (после этапа 3) + +Дуал ownership transfer: `+=` на паблишере, который вызывающий сконструировал +и **вернул**, ограничен временем жизни возвращённого объекта — не утечка. +Требуется новый вид факта о параметре: «во *всех* вызывающих аргумент на этой +позиции — локально сконструированный и возвращённый объект». + +Почему после этапа 3: это **обратное** направление распространения +(caller→callee; текущий фикспойнт — callee→caller) поверх тех же return-скелетов +и call-графа. Join — must-стиль по всем вызывающим (один DI-singleton-вызов → +остаёмся `injected`), так что DI-кейс реальной утечки не трогается. До тех пор +консервативный advisory warning — честная поза (сам issue это фиксирует). + +## 8. Этап 5 — ось эксклюзивности, #122 (строго по триггеру, не по календарю) + +Ничего не делать, пока не появится **первый межпроцедурный потребитель** +эксклюзивности (конфликт класса OWN006/011/012/013 через границу вызова). +Ось без читателя не даёт наблюдаемых false negatives, а работа уже аддитивна: +forward-рёбра сохранены в скелете (`PathAction(kind="forward")`), нужен +leaf borrow-kind + join + поле на `ParamSummary` — не пересборка решателя. +Появление такого потребителя — например, когда займы полей/статиков начнут +проверяться через сводки — и есть момент, когда этап входит в план. + +## 9. Этап 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 целевого состояния. + +## 10. Порядок и зависимости + +```text +Этап 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-поверхность уже есть) +``` + +Связь с остальным репозиторием: перепривязка к Rust-порту — §2 (этап 0 — +крупнейший gap P-022, «during the rewrite»-ловушка разминирована +tech-debt-register'ом); Gate A +([incremental-computation.md](incremental-computation.md)) открывается ровно +тогда, когда этапы 3–4 сделают межпроцедурку whole-program по-настоящему — и +в Rust-ядре названный кандидат на инкрементальность (Salsa) уже под рукой. + +## 11. Чего не делать (отказы на запись) + +- **Контекстная чувствительность / 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, решение стоит). + +## 12. Как читать этот слой (входные точки) + +Порядок чтения, который делает межпроцедурку обозримой за один заход: + +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 таблица). diff --git a/docs/notes/interprocedural-tz.md b/docs/notes/interprocedural-tz.md new file mode 100644 index 00000000..c8ac42a5 --- /dev/null +++ b/docs/notes/interprocedural-tz.md @@ -0,0 +1,491 @@ +# ТЗ — межпроцедурный слой: нормативная семантика, инварианты, порт в Rust + +> Статус: **рабочее ТЗ** (черновик нормы + критические требования). Дополняет +> [interprocedural-roadmap.md](interprocedural-roadmap.md): карта отвечает «что и +> когда», это ТЗ — «что именно, как и с какими инвариантами». Из §2–§4 напрямую +> выделена нормативная спека **[`spec/Inference.md`](../../spec/Inference.md)** +> (этап 0 карты, ✅ shipped — правила `INF-*`, привязаны к +> `test_ownership.py`/`test_ownir.py`); это ТЗ остаётся расширенным рабочим +> черновиком с воспроизведёнными дефектами и требованиями к порту. Всё описанное +> «как есть» сверено с кодом на коммите `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-правила, `_build_skeletons` + `_param_signals`, ownir.py) + +- **S1** Явный `effect` в факте — авторитет: `consume`→`[dispose]`, + `borrow|borrow_mut`→`[borrow]`, иная строка→`[]` (не-владеющий). Инференция + никогда не оспаривает явный контракт. +- **S2** Иначе — по сигналам `(rel, passed, used)` (`_param_signals`, рекурсия в + `if`/`while`), с приоритетом: `rel`→`[dispose]` (⚠ D1); + иначе `passed`→ forward-рёбра всех вызовов, и если НЕ (ровно одно ребро всего + ∧ ровно одно на верхнем уровне ∧ нет `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-ребром к + несуммаризируемому → `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 + +> **Статус: исправлено (вариант 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]` без +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 сам по себе **расширяет** D6-канал + (may-параметры множатся) — он полон только вместе с untrack-семантикой D6. + Оба шага сделаны; см. D6 ниже. +- **Вариант 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». Не оставлять как есть. + +> **Статус: исправлено (вариант «reserved»).** `to_dict` больше не сериализует +> `escapes`; поля модели остаются (ось d5-дизайна), помечены RESERVED в +> докстрингах `ownership.py`; тест пиннит отсутствие ключа в дампе до появления +> продюсера. Когда продюсер появится — сериализацию вернуть вместе с ним и +> перевернуть тест. + +### D3: `adopt`/`return` — вклады без продюсера + +`contrib` понимает `adopt` и `return` как `must`, но деривация их не эмитит +(adopt — T4b-межпроцедурный, return-of-param — сознательно не консьюм, +`:1510-1513`). В спеке пометить оба kind'а «reserved, производитель отсутствует» +— иначе порт унесёт мёртвую семантику как живую. + +> **Статус: зафиксировано.** Докстринг `PathAction` (`ownership.py`) теперь +> явно помечает оба kind'а RESERVED с условием активации каждого (adopt — +> T4b-сводки, return — owned-return-value modelling) и указанием порту: нести +> семантику, не ожидать появления из реальных фактов. + +### D4: `aliasOf` гаснет на первом же хопе forward-цепочки + +Документированная деградация (`ownership.py:373-380`). В спеку — как правило, +в ТЗ этапа 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` + гейты в лоуэринге): ни пропущенный, ни +> защитный 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: сбой решателя молчит + +`except Exception: mos = {}` (`ownir.py:906-909`) гасит **весь** межпроцедурный +слой без следа — против культуры honest-skip (OWN050). Решение: деградация +остаётся (никогда не ронять чекер), но становится наблюдаемой — OWN050-класс +advisory «interprocedural summaries unavailable: » + счётчик в `--stats`. +Требование к 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`/ + 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 +карты, переквалифицированный в артефакт порта. + +> **Статус: 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-тесты (монотонность + 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 diff --git a/ownlang/__main__.py b/ownlang/__main__.py index ac74c7ac..75b89b1e 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 @@ -26,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. """ @@ -300,6 +303,28 @@ 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 @@ -351,8 +376,9 @@ 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: - # the advisory band is no longer only OWN050 (OBL005 rides it too) — - # name the codes actually present instead of hardcoding one. + # the advisory band is no longer only OWN050 (OBL005 and the OWN051/OWN052 + # interprocedural notes ride it too) — name the codes actually present + # instead of hardcoding one. note_codes = "/".join(sorted({x.code for x in notes})) summary += (f" ({len(notes)} advisory hidden)" if verbosity == "quiet" else f", {len(notes)} advisory ({note_codes})") @@ -372,7 +398,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 +502,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/diagnostics.py b/ownlang/diagnostics.py index bc2fdbd2..24b55b81 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -83,6 +83,8 @@ 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", "DI002": "singleton captures a scoped service (captive dependency)", @@ -160,6 +162,26 @@ 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 " + "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/ownership.py b/ownlang/ownership.py index 0bb3bbb3..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 = "" @@ -93,7 +100,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 +158,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/ownlang/ownir.py b/ownlang/ownir.py index 6aee86cf..c178e4d8 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -163,6 +163,7 @@ ReturnSkeleton, Transfer, solve, + solve_with_log, ) # The OwnIR schema version this core understands. Bump it whenever the fact @@ -821,14 +822,21 @@ 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, + 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 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; `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 @@ -943,11 +951,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 @@ -979,11 +992,51 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, 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 + # 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) + 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 + # 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]}" @@ -996,7 +1049,8 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, 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, 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 @@ -1040,6 +1094,126 @@ 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 _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 @@ -1371,6 +1545,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 @@ -1399,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 @@ -1450,7 +1721,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]: @@ -1462,11 +1737,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` @@ -1515,14 +1796,24 @@ 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) 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: @@ -1532,7 +1823,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()] @@ -1542,8 +1836,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 → @@ -1555,7 +1852,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" @@ -1754,7 +2053,9 @@ 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(), + 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 @@ -1771,7 +2072,21 @@ 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 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: @@ -1785,6 +2100,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 @@ -1813,7 +2133,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 @@ -1846,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) + 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) + 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) + 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 @@ -1876,18 +2196,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 @@ -1900,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 @@ -1915,6 +2259,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 @@ -1985,6 +2330,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). @@ -2001,7 +2384,9 @@ 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] = [] + 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 @@ -2249,6 +2634,25 @@ 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. + # 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/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..b43b4628 --- /dev/null +++ b/spec/Inference.md @@ -0,0 +1,360 @@ +# 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, 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, + 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` 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)). + +## 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; 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; 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 + 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_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 diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 55f996f1..89f5da28 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1495,9 +1495,302 @@ 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 + # 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}]}]}) + 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 + 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}]}]}) + 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 + 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}]}]}) + 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 + 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}]}]}) + 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]}") + # (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 + # 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}") + # --- 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}") + # 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 @@ -1533,10 +1826,10 @@ def _sub(source: str | None) -> list[Finding]: "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.) @@ -1550,9 +1843,10 @@ def _sub(source: str | None) -> list[Finding]: "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).