feat(ownir)!: OwnIR v2 — must-understand proven_call (H1) + T0 Amendment 2 - #390
Merged
Merged
Conversation
A call inside a state-protocol region that touches neither the entity nor the
token used to be refused by the extractor. It is now handed to the core as the
must-understand flow op `proven_call` (site, callee) together with the H0
heap-effect FACTS it is judged against (a new top-level `heap_effects`
section), and the core admits it only when the shared summary layer proves it
harmless. Everything unproven stays refused; nothing the frontend could not
classify `direct` reaches the core at all, so external, virtual, delegate and
local-function calls are refused exactly as before, with the same text.
Twice(21) in a region admitted, clean
TouchesGlobalState() refused by the core: writes.static is may
A -> B -> Console.WriteLine refused by the core: writes.instance is unknown
Console.WriteLine("x") refused by the extractor, unchanged
Mutates(order)/Escapes(order) use -> OWN013, unchanged
The decision lives in the summary layer (heap_effects.harmless/site_verdict)
and is applied by one document-level pass before anything is lowered
(ownir.py _admit_proven_calls, own-bridge proven.rs), so no lowering path can
carry a proven_call past the proof. Predicate v1 is strict: every parameter
and the receiver <= borrow, no write of any kind, nothing returned, no Unknown,
checked on every callee in the site and on the site itself. The frontend
emits facts only; the dispatch classifier is shared with H0.
A new flow op is a vocabulary change, so OWNIR_VERSION moves 1 -> 2 on every
producer (core, Rust door, extractor, OwnTS). A v1 core refuses v2 facts on
the stamp and, with the stamp stripped, on the unknown op; a v2 core refuses
v1 facts. No shim either way. LOWERED_VERSION does not move: an admitted
proven_call lowers to nothing.
Evidence: the protocol-sample cases H1a-H1j (positive, transitive, SCC,
global, polluted SCC, transitive Unknown, outer mutation, entity use) and
refused R18/R19; R9's backdoor is now refused by the core
(writes.instance is may). tests/test_proven_call.py holds C1 (the real v1
core, taken out of git history, refuses v2 facts), C2/C3 (eleven derived
refusals pinned by the Layer 2 goldens and replayed by Rust), C4 (an
Unknown-is-harmless mutant is caught) and C5 (a dropped admission or a dropped
op is caught). Python and Rust refusal texts are byte-identical.
Migration: current input documents restamped by a JSON-aware move (top-level
key only, verified by re-parse); the C#-derived typestate documents
regenerated from C# (one line each); every golden family regenerated by its
own writer (Layer 2, summaries, verdicts, renders, CLI, validation ledger,
repro two-phase); the SARIF stamp copy in own-bridge render.rs bumped and
tied to own_ir::OWNIR_VERSION at compile time. The S0 additivity fixture
gains a protocol region so the new section is covered; the flag-off golden
moves one line (third amendment, tests/goldens/README.md). Historical evidence
(corpus/ownership-lab/h29, docs/evidence) is not rewritten.
The T0 instrument's generated facts follow in the next commit (Amendment 2);
until then `perf-calibration-facts-current` is red by design.
BREAKING CHANGE: `ownir_version` is 2. Facts stamped 1 are refused; build the
extractor and the core from the same commit.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
OwnIR moved to v2 in the previous commit (the must-understand `proven_call`
of H1). The instrument's `facts` calibration generator stamps `ownir_version`
on every document it writes, so one literal moves: "ownir_version": 1 -> 2.
Nothing else in the harness source set changes. That literal is the only
cause of the identity move:
1a26aa63fd5fbbe06e7ae72dd5e1c8f2d611bff8856af4a5b93ae36d2d23a9b1 before
b92f08c990fcf6d74df29aad333b330b6c3c4f9e1c1bad55efe8164c39dea57c after
Re-bound, in the order the chain runs, exactly as Amendment 1 did: the digest
in the policy freeze (step 4), in the ratified design constants (step 5), and
in the training preregistration's bindings (step 6) — and with it
design_constants_blob_sha1 (0ff316d -> 1059a69), which moved because
the design-constants artifact itself was re-bound. The pyproject comment that
names the identity follows.
The frozen T0 records this as Amendment 2, a new state of the contract under
the owner's ruling (OwnIR v2 and this amendment approved for H1, on the
Amendment 1 principle, for nothing else): T0-1 names the new identity, 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, host predicate or retry budget
changes; the measurement methodology is untouched — this is a schema-transport
change carried by the generated calibration documents, not a change to the
experiment. Committed evidence of past runs is not rewritten.
Merge gate, observed: with the literal moved and nothing re-bound it REFUSED
(instrument_matches_t0: b92f08c990fc vs T0's 1a26aa63fd5f); after the
re-binding it allows. perf-calibration-facts-current was red between the
core's version move and this literal, and holds after it.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
This was referenced Oct 3, 2026
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
2 participants
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.
Что и зачем
H1: state-protocol регионы впервые потребляют общую межпроцедурную heap-effect summary-архитектуру (H0). Вызов внутри
[ProtocolRegion], который не касается ни entity, ни токена и диспатчитсяdirect, больше не отказывается экстрактором: он уходит в ядро как must-understand flow opproven_callвместе с H0 source facts (новая секцияheap_effects). Ядро допускает его только если общий summary-слой доказал, что вызов безвреден. Всё недоказанное остаётся отказом. Для этогоOWNIR_VERSION1 → 2 (по решению владельца) и T0 Amendment 2 (минимальная перепривязка harness identity из-за литерала версии).Twice(21): direct, ничего не трогает, доказан harmlessTouchesGlobalState()/ A→B→global / polluted SCCwrites.static is mayConsole.WriteLine(transitive Unknown)writes.instance is unknownFill(buffer), внешний массивparameter 0 is borrow_mutMutates(order)/Escapes(order)use→ OWN013Console.WriteLine("x"), вызов через интерфейсAnnotateLast()writes.instance is mayTransport.
proven_call {site, callee, line}, только внутриborrow_mut.heap_effectsнесёт только факты: запись call-site (выражение вызова; любая внешняя переменная читается какheap) и записи методов, достижимых поdirect-рёбрам. Решает ядро.Решение. Принимается одним проходом по всему документу до любого lowering (
ownlang/ownir.py::_admit_proven_calls,own-bridge/src/proven.rs).Предикат (
heap_effects.harmless/site_verdict) живёт в summary-слое, а не в typestate:borrow;returns == [];Вне scope: logger/BCL allowlist, annotations, devirtualization, getters/ctors/operators в регионе, DB-side gaps.
Подробно:
docs/notes/h1-proven-call.md, spec/OwnIR.md §2/§5.4, spec/Bridge.md BR-L14, T0 Amendment 2 вdocs/notes/p022-263-t0-protocol-freeze.md.Тип изменения
Как проверено
python tests/run_tests.py(rc=0, ноль FAIL)ruff check .иmypypython scripts/<...>.py --selftest, audit selftests)cargo fmt --check,cargo clippy --all-targets(новых предупреждений нет),cargo test --no-fail-fastpython scripts/protocol_gate.py --rust …/own-cli: 28 кейсов, 19 refusals, EF backend 24/24, 29 документов байт-в-байт на обоих CLI, 0 failurespython scripts/heap_effects_gate.py: H0 sidecar не сдвинулся, 50 inertness-прогоновtests/test_proven_call.py:ownlang/@ 1c70e86 из git history) отказывает на v2-фактах, со штампом и без него;heap_effects), flag-off golden отличается одной строкой (третий amendment записан)b92f08c990fcvs1a26aa63fd5f);OWN_TIERB_REQUIRED=1(verify-delta 28/28, verify-target 65/65, certify 32/32);mainпри запуске под root: root игнорирует права на запись. Это артефакт контейнера, не этого PR; на GitHub runner'ах (non-root) они проверяются по-настоящему.Связанные issue
Refs P-036 / P-037 / P-022 #263 (T0 Amendment 2). Отдельного issue нет.
Чеклист
feat:,fix:,docs:…)🤖 Generated with Claude Code
https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
Generated by Claude Code