feat(ownir)!: OwnIR v1 (move, borrow_mut) + C# state protocols; T0 Amendment 1 - #385
Merged
Merged
Conversation
…tract' into feat/ownir-v1-state-protocols
…ut' into feat/ownir-v1-state-protocols
Two flow ops join the vocabulary, and an incompatible vocabulary change bumps
the version (spec/OwnIR.md §2): OWNIR_VERSION 0 -> 1, LOWERED_VERSION 1 -> 2.
A v0 document is refused at the door by both engines; nothing accepts both.
move src -> var `var` takes the obligation, `src` is dead
borrow_mut owner as binding { .. } a BLOCK-scoped exclusive loan
`borrow_mut` is compound on purpose: the core's loans are block-scoped, so the
vocabulary must not be able to say "open a loan" without saying where it
closes. Inference reads a region as transparent, so a region never changes a
summary. Together the two ops are enough for a frontend to express a state
protocol: an affine token over an exclusively borrowed entity.
The bridge REFUSES four shapes instead of lowering them (spec/Bridge.md,
BR-L12/BR-L13), because each would otherwise reach the verdict as "the core
raised, the bridge filtered it, clean": a region whose owner is not tracked; a
call inside a region to an unresolvable callee that passes a tracked local; a
tracked local on a plain position inside a region; and any may/unknown position
in a function that opens a region.
The loan diagnostics the regions exercise (OWN005/007/008/011/012/013) get
flow-local wordings and a `subject`, on both engines.
Python is the reference and Rust replays it: own-ir, own-lowered, own-bridge
and own-analysis carry the same ops, the same refusals and the same wordings,
and the Layer 2/3, summary, CLI, repro and validation ledgers are regenerated
at v1. The handwritten `typestate_*` documents and the `typestate_cs_*` /
`typestate_ef_*` documents (the frozen output of the Roslyn lowering that lands
in the next commit) are byte-identical on both public CLIs: exit code, stdout
and stderr, 37 of 37.
BREAKING CHANGE: `ownir_version` is 1. Facts stamped 0 are refused; build the
extractor and the core from the same commit.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…irst slice)
With --flow-locals the extractor lowers a state-protocol surface into `move` /
`borrow_mut`. The surface is two attributes matched by name, so a domain takes
no dependency on Own.NET: a [ProtocolRegion] method `(entity, callback)` opens
an exclusive region and hands out a [ProtocolToken] ref struct; a method on the
token is a transition that spends it. It is a lowering, not an analysis — the
verdicts are the core's (a stale token is OWN002, a copied one OWN005, a raw
touch of the entity inside the region OWN013).
It runs on the instance an ORM tracks. frontend/roslyn/protocol-samples/efcore
is an ordinary ASP.NET Core minimal API over EF Core + SQLite: no base entity,
no repository, no custom LINQ, no attribute in the handler file. Its acceptance
runner drives real HTTP against a real database file and checks that the
transition reaches the tracked instance, the ChangeTracker and the saved row.
What is claimed is the local C# capabilities and aliases of an entity that
already exists. Writes that bypass the entity's C# surface (ExecuteUpdate, a
change-tracker metadata write, raw SQL) are outside it, and two of them are
pinned under efcore/known-gaps so the limit is stated rather than forgotten.
A recognised protocol construct that cannot be lowered safely is REFUSED for
the whole scan (exit 2, no facts):
* inside a region the rule is default-deny: transitions, token reads, `if`,
locals and built-in operators are read; a call, a constructor, a property
getter, a loop, `return` are refused. Around a region anything goes;
* admission: the state a transition writes may have no PUBLIC mutator on the
entity — that would be a transition nobody declared;
* boundary: outside the protocol's own types, creating a token, calling a
non-public method of the entity or the protocol, and writing their
non-publicly-writable state are refused, in one assembly or two. `nameof`,
`typeof` and reads are mentions, not operations;
* source: the protocol and its entity must be in the scan as source;
* binding: the scan does not read obj/, so a region whose entity only binds
through IMPLICIT usings is refused, not silently dropped.
scripts/protocol_gate.py ties every committed `typestate_cs_*` /
`typestate_ef_*` fact back to the C# it came from: 18 programs lowered and
judged, 14 refused, 5 rejected by the C# compiler, 5 one-assembly programs, 24
checks on the backend. A new CI job runs it on Linux and Windows, and on Linux
also compares the two public CLIs on those documents.
Outside --flow-locals, and for a scan with no protocol in it, the extractor's
output is unchanged: 122 of 122 comparisons against main over every C# sample
CI scans.
The samples live under frontend/roslyn/ rather than examples/: examples/ is
swept as one document by the #260 shadow sweep, and a backend whose references
a directory walk does not have is, correctly, a refusal of the whole scan.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The `facts` calibration generator stamps `ownir_version` on every document it
writes. Left on 0 against a v1 core it hands both engines a document they refuse
at the door, so every `facts` rung would be a cell that times the version gate.
One literal changes: "ownir_version": 0 -> 1. Nothing else in the harness source
set moves. This is a change to an INSTRUMENT SOURCE, so it moves the harness
identity on purpose:
104c384d01bf6060bdec1e7c916053ddb04b97fcbd0b39f8a4fc57b8f139672f before
1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1 after
Steps 4, 5 and 6 are re-bound in the next commit, which is separate so that the
re-acceptance can be reviewed as one. Between the two, four controls say so by
name: freeze-harness-untouched, constants-bound-to-freeze,
training-prereg-bindings, envcapture-frozen-untouched.
No existing control could see the defect: with the core on v1 and the generator
on v0, the whole instrument suite was green. `perf-calibration-facts-current`
is new: it runs the reference on what the generator writes and requires the
`facts` workloads to be analysed and the `refused` workload to be refused. It
fails on the old literal (three workloads, exit 2, "facts are schema v0") and
holds on the new one. It lives outside the harness source set and moves no
identity.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The instrument's generated facts moved to OwnIR v1 in the previous commit, and
with them `measurement_harness_digest`
104c384d01bf6060bdec1e7c916053ddb04b97fcbd0b39f8a4fc57b8f139672f before
1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1 after
Re-bound, in the order the chain runs: the digest in the policy freeze, in the
ratified design constants, and in the training preregistration's bindings — and
with it `design_constants_blob_sha1` (fa02f43 -> 0ff316d), which moved
because the design-constants artifact itself was re-bound. The same chain in the
same order as the S8 re-binding (5e7215a).
The frozen T0 records this as Amendment 1, a new state of the contract: T0-1
names the new identity (the merge gate reads it there and recomputes it from the
tree being merged), the status block points at the amendment, and the amendment
says what moved and what did not. FROZEN and collection_authorized are
unchanged. No rule, budget, population, statistic, roll-up or host predicate
changes. The freeze commit is untouched and stays an ancestor.
Not touched: the committed evidence of runs that actually happened. No
T0-governed clock has run under any identity, so there is no training or
decisive observation to re-evaluate.
The gate's own files do not change in this merge (the co-change rule).
Controls after re-binding: perf instrument 17/17, round 7 apparatus 10/10,
calibration policy 10/10, calibration freeze 7/7, calibration constants 4/4,
training preregistration 9/9, step 7 environment capture 12/12, host
qualification 26/26, merge gate 15/15, merge gate wiring 12/12.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ed, not skipped
The types that declare a protocol are trusted: their bodies implement it and
are not lowered. The lowering skipped every method of such a type — including
one that USES the protocol. A handler written in the same class as the region
entry it calls was therefore never analysed, and read as clean:
public static class ParcelHandlers
{
[ProtocolRegion] public static void WithPacked(...) => ...;
public static void Dispatch(Parcel parcel)
{
WithPacked(parcel, packed => { packed.Send(); packed.Send(); });
}
}
Before: exit 0, no function emitted, verdict clean — a token spent twice.
After: exit 2. Trusted is not the same as checked, and an unanalysed region
must not read as a clean one. The remedy is in the message: use the protocol
from outside the types that declare it.
Found while probing what an unrelated attribute that merely shares the name
[ProtocolRegion] does to a scan. refused/R15 pins it; no committed fact moves
(18 cases, 15 refused, 0 failures), and the extractor's output on every C#
sample CI scans is still equal to main's, 122 of 122.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…odel The previous commit refused a region opened inside a type that declares the protocol, and documented it as one more thing the extractor refuses. That undersells what it is. The declaring types are the profile's trusted definition surface — token construction, region entry, transition plumbing — and everything else is the analysed surface. A type is one or the other, never both, because consumer code inside a declaring type is not a violation the core missed: it is a program the core never saw. The README states that as the model, next to what the profile claims, and the refusal list points at it. The lowering's header says the same. No behaviour changes: comments and prose only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…sion `tests/check_fix_candidates_facts.py` asserted `ownir_version == 0` under the message "ownir_version must stay 0". What it meant is that `--fix-candidates` is additive metadata and does not move the vocabulary version; what it checked was a literal, which held only until the vocabulary first moved. OwnIR v1 moved it, and the `C# leak extractor (Roslyn) -> OwnIR -> core` job went red on that line — with the extractor doing exactly the right thing. It now checks the claim: the flag-on facts are stamped with the core's current OWNIR_VERSION, and with the same value as the flag-off facts. This is the third control of this shape the bump has found (the validation ledger in #383, the instrument's generated facts in this branch), and the only one that needed the server to find it: the script takes the extractor's output as its argument, so it is not part of `tests/run_tests.py` and no local run of that suite could reach it. The job's steps were then run locally as written, from this one to the end of the job, on a Linux clone of the committed tree. tests/goldens/README.md records the golden's second amendment: one line, `"ownir_version": 0` -> `1`, made in the vocabulary commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
main gained the OWN053 orphaned-awaitable advisory (#386) after this branch was cut. #386 was written against OwnIR v0; this branch moves the whole contract to v1. The merged tree is one OwnIR v1 that carries both: OWNIR_VERSION 1, LOWERED_VERSION 2 flow ops move, borrow_mut (this branch) top level orphaned_awaitables[] (#386, additive, both strict doors) advisory OWN053, two frozen families (#386) Nothing of either side is dropped, and there is no dual-version reading. Textual conflicts: three, all generated status documents (docs/generated/p022-{coord-census,cp4-census,shadow-census}.md). Resolved by regenerating them with their writer, not by picking a side. The conflict that mattered did not conflict. Git merged frontend/roslyn/OwnSharp.Extractor/Program.cs cleanly and left #386's new envelope — the one that carries `orphaned_awaitables` — stamped `ownir_version = 0`, between two envelopes stamped 1. A scan with an OWN053 site would have produced facts the v1 core refuses at the door. The IR2 check in tests/test_ownir.py did not see it: it read only the FIRST stamp in each producer. It now reads every stamp (`[1, 0, 1]` fails it), and the envelope is stamped 1. #386's documents that mean "the current version" are migrated to it, stamp only: tests/fixtures/verdicts/verdict_own053_orphaned_awaitable.facts.json and the four H-29 documents under corpus/ownership-lab/h29 (promo-u and the three malformed door inputs). Their recorded outputs are unchanged, byte for byte, on both engines, and the merged extractor reproduces promo-u.facts.json exactly from fx/Orphan.cs: five sites, lines 11/12/21/22/23. Regenerated with the repository's writers: the validation ledger (294 + 50 controls = 344, the inputs now stamped by OWNIR_VERSION), the Layer 3 verdict goldens (132 + 1 = 133 cases), the repro digests (135 + 1 = 136 documents) and the generated status documents. The merge result differs from this branch's previous head in exactly #386's 56 paths and from both parents in 20; no ledger outside those moved. T0: scripts/perf_baseline.py, the workload manifest, the three bindings, the T0 document and the merge-gate files are untouched by this merge. The harness identity is still 1a26aa63fd5f, the value Amendment 1 recorded. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
PhysShell
marked this pull request as ready for review
October 2, 2026 01:32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что и зачем
OwnIR v1: в словарь потока добавлены
moveи составнаяborrow_mut(эксклюзивный регион),OWNIR_VERSION0 → 1,LOWERED_VERSION1 → 2, на обоих движках. Поверх них Roslyn-фронтенд понижает C#-поверхность state-протоколов (P-010, столп 9, первый срез): состояние —ref struct-токен, регион — эксклюзивный заём сущности, в том числе той, которую отслеживает EF Core. Инструмент #263 переведён на v1, шаги 4/5/6 перепривязаны, T0 записывает это как Amendment 1.#383 и #384 уже слиты в
main. Ветка содержит их коммиты через локальный merge, сделанный до их слияния, поэтому в списке коммитов PR есть два merge-коммита, а из-за двух баз слияния GitHub может показывать в diff файл из #383. По содержимому относительноmainиз этих двух файлов отличается толькоtests/test_repro_fixtures.py, одной строкой (литерал версии в контроле).Семь коммитов этой работы и merge
main, каждый читается отдельно:feat(ownir)!— словарь, версия, отказы моста (BR-L12/BR-L13), формулировки займов, Rust-порт, перегенерированные эталоны.feat(roslyn)— lowering, образцы (frontend/roslyn/protocol-samples),scripts/protocol_gate.py, job в CI, документация.fix(perf)— один литерал в инструменте ("ownir_version": 0 → 1) и новый контрольperf-calibration-facts-current.docs(calibration)— перепривязка шагов 4/5/6 и T0 Amendment 1.fix(roslyn)— регион, открытый внутри собственных типов протокола, отклоняется, а не пропускается (до исправления обработчик в одном классе со входом в регион не анализировался и читался как чистый).docs(roslyn)— граница доверия описана как часть модели: типы, объявляющие протокол, — доверенная definition surface, остальной код — анализируемый; тип либо одно, либо другое. Только текст и комментарии.fix(tests)— контроль S0 проверял литералownir_version == 0вместо «флаг--fix-candidatesне двигает версию»; на нём упал jobC# leak extractor (Roslyn) -> OwnIR -> core. Теперь сверяет с текущейOWNIR_VERSIONи с flag-off фактами.main(с feat: add OWN053 orphaned-awaitable advisory #386, OWN053) в ветку, обычный merge без rebase. Итог — один OwnIR v1, в котором одновременноmove,borrow_mutиorphaned_awaitables/ OWN053; ничего ни с одной стороны не выброшено. Текстовых конфликтов три, все в генерируемых документах (перегенерированы). Настоящий дефект слияния конфликтом не был: git чисто слилProgram.csи оставил конверт фактов сorphaned_awaitablesсо штампомownir_version = 0; проверка IR2 читала только первый штамп и была зелёной. Теперь читает все ([1, 0, 1]её валит), штамп исправлен. Пять документов feat: add OWN053 orphaned-awaitable advisory #386, означающих «текущая версия», переведены на v1 (только штамп); их записанные выводы на обоих движках не изменились побайтово.Что заявлено: профиль защищает локальные C#-capabilities и алиасы уже существующей сущности. Он не защищает сохранённую строку от других способов её изменить (
ExecuteUpdate, запись через метаданные change tracker, сырой SQL) — два таких случая закреплены как заявленные пределы вprotocol-samples/efcore/known-gaps.Что отклоняется (exit 2, весь скан): код без контракта внутри региона; протокол с публичным мутатором состояния, которым владеют переходы; создание токена, вызов не-public метода и запись не-public состояния вне типов протокола (в одной сборке или в двух;
nameof,typeofи чтение — не операции); протокол, пришедший только скомпилированной ссылкой; регион, открытый внутри типов, которые сам протокол и объявляют; регион, чья сущность связывается лишь через неявные using (скан не читаетobj/).T0: изменён один литерал в
scripts/perf_baseline.py, digest инструмента104c384d01bf → 1a26aa63fd5f.FROZENиcollection_authorized: trueне менялись, как и все правила, бюджеты, популяции и предикаты. Файлы самого merge gate не тронуты (co-change). Свидетельства уже состоявшихся прогонов не переписаны.Тип изменения
Как проверено
python tests/run_tests.pyruff check .иmypypython scripts/<...>.py --selftest)Всё ниже — на закоммиченной ветке, в свежем клоне на Linux (WSL NixOS;
ruff 0.15.8,mypy 1.19.1,dotnet 8.0.422), если не сказано иное.python tests/run_tests.py— exit 0. 15 реестров эталонов в режиме verify — все в синхроне.cargo fmt --check,cargo clippy --all-targets— exit 0;cargo test --no-fail-fast— 288 прошли, 0 упали.python -m ownlang ownirиown-cli ownir) на всех 37 документахtypestate_*: код выхода, stdout и stderr побайтово одинаковы.python scripts/protocol_gate.py --rust <own-cli>на Linux и без--rustна Windows: 18 программ понижены и оценены, 15 отклонены lowering, 5 отклонены компилятором C#, 5 программ «одна сборка», 24 проверки на бэкенде (13 из них — прогон по настоящему HTTP и файлу SQLite), 0 провалов.main: 122 из 122 сравнений (каждый C#-образец из CI, с--flow-localsи без) равны с точностью доownir_version.perf_baseline.py --selftestиenvcapture.py --selftest— exit 0.scripts/step7/mergegate_ci.pyна симулированном merge-коммите этой ветки вmain:gate_unchangedи все шесть предикатов — ok,merge gate: allowed.Отрицательные контроли:
С ядром v1 и генератором на v0 весь набор инструмента был зелёным; новый
perf-calibration-facts-currentна старом литерале падает (три workload, exit 2, «facts are schema v0»), на новом проходит.До перепривязки сдвиг digest назвали четыре контроля:
freeze-harness-untouched,constants-bound-to-freeze,training-prereg-bindings,envcapture-frozen-untouched.Сломанный переход в бэкенде (
MarkShippedбез записи статуса) валит 4 проверки прогона и красит gate.25 враждебных проб границы и допуска (каждая компилируется): операции отклонены, упоминания и чтения приняты.
Шаги job
C# leak extractor (Roslyn) -> OwnIR -> core, начиная с упавшего на сервере S0 и до конца job (7 шагов, которые на сервере после падения не исполнялись), прогнаны локально как написаны вci.yml, на Linux-клоне закоммиченного дерева: все exit 0. Тот же раннер на предыдущей голове воспроизвёл серверный отказ дословно.После merge (
821c459), свежий Linux-клон: 15 реестров в синхроне (реестр валидации 344 контроля, вердикты 133 случая); паритет CLI 37/37;cargo test288/0;ruff,mypy,fmt,clippy;run_tests.pyexit 0; контроли инструмента;mergegate_ci.pyна симулированном merge в7310f78— allowed, digest инструмента прежний (1a26aa63fd5f);protocol_gate.py --rust— 0 провалов; контроли OWN053 (экстрактор воспроизводитpromo-u.facts.jsonточно, 5 сайтов; оба движка дают записанный вывод; три искажённых документа отклонены на строгой двери с записанным текстом); весь jobC# leak extractor (Roslyn) -> OwnIR -> core(24 шага, с SDK 8 и 9) — все exit 0. Экстрактор ветки против экстрактораmain: 122 из 122 сравнений равны с точностью доownir_version.Не проверено: раскладка Domain + Web двумя проектами (только имитация); net9/net10 и C# 13 как целевые для образцов; остальные job CI после merge локально не гонялись.
Связанные issue
Отдельного issue нет. Затрагивает контракт #263 (T0 Amendment 1), сам #263 не закрывает. Шёл после #383 и #384 (оба слиты).
Чеклист
feat:,fix:,docs:…)Документация:
frontend/roslyn/README.md(раздел State protocols),spec/OwnIR.md§5.3,spec/Bridge.mdBR-L12/BR-L13,docs/proposals/P-010-type-disciplines.md,docs/notes/p022-263-t0-protocol-freeze.md(Amendments).🤖 Generated with Claude Code