feat(p022): port the obligation-protocol analysis and wire it through the bridge (#259 cp4b) - #340
Merged
Merged
Conversation
…259 cp4b.0) Checkpoint 4b is the one #259 family with no Rust side at all: the bridge refuses a protocol-bearing document instead of answering for it, and the two reference documents sit in the verdict ledger's exclusion list. Before any production code, write down what has to be reproduced and what already is. The note is the checkpoint's completeness ledger: every behaviour read off ownlang/obligations.py (the lattice, the matchers, the leaf order, the exits, the loop's two-phase emission, the evidence and the sort key) and off the bridge's BR-P3 mapping, each named with what will pin it — a row in the new analysis-level fact-parity family, a synthetic Layer 3 case, or both. It also records, measured rather than assumed, how little the existing corpus reaches: one OBL001 barrier crossing with a late close. The two-step slice has no golden at all, and neither do OBL002/003/004/005, any exit anchor, any loop, the opaque-write asymmetry, args-narrowing, exact scope matching, duplicate names or the malformed-entry skip. No count is typed in the note; the surface inventory and the census already render them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
…gainst Python (#259 cp4b.1) `ownlang/obligations.py` had no Rust side at all. This ports the checker — the {OPEN, CLOSED} set lattice with its min-line provenance, the opens-before-closes-before-barriers leaf order, allow beating barrier, the never-invent asymmetry of an opaque write, the exit rules with the anchor-at-open precedent, the branch join, the loop's silent fixpoint and single emitting pass, the reachability-blind close-line evidence and the four-part sort key — into `own-analysis/src/obligation.rs`, beside `di.rs` and `effect.rs`, where the analysis owns its verdict (BR-B1). Codes, messages and evidence slices stay the bridge's and are not here. The typed values come from ONE implementation of the grammar with two consumers, not a second parser: `own-ir/src/protocol.rs` grows from validate-only to validate-and-construct, the strict door keeps taking the record identity it needs, and the analysis takes the value. No strict-door error text or category moves — the cp1 ledger's protocol controls stay green. The oracle is a third fact-parity family, built like the DI/effect one: `tests/test_obligation_fact_parity.py` runs the REAL `check_protocols` / `unmatched_scopes` over raw protocol and event documents and freezes every violation whole — line, kind, definite, open_line, barrier_desc, close_line — plus the dead-rule list. `own-analysis/tests/obligation_parity.rs` replays the same documents with zero Python and compares every member. Cases carry raw documents rather than pre-parsed values, so each side builds them with its own half of the shared grammar and a grammar divergence surfaces as a verdict divergence instead of hiding. Production dependency change: own-analysis -> own-ir, already an allowed DAG edge, made explicit rather than borrowed through own-cfg's re-export. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
…n found (#259 cp4b.1) The first campaign run caught 30 of 33 and named what the corpus could not see. All three survivors were real, and two of them were inherited from the reference's own suite: * `allow beats barrier` was unobservable. `DOC_LOAD`'s barrier arguments ({Document, Rows}) and its allow arguments ({IsBusy, IsLoaded}) are disjoint, so no event can match both and deleting the allow check changes nothing. A protocol whose barrier matches every `OnPropertyChanged` and whose allow names one argument is the only shape where the rule fires. * `exit_barriers: false` was only exercised against the end-of-method leak, which `run()` guards separately — the `_exit` guard on `return`/`throw` had no case at all. * the unknown-argument rule was masked by the allow list: with the narrowing inverted, an unknown argument matches the ALLOW entry too, and allow wins. A protocol with no allow list isolates the barrier. The fourth finding is a measurement, not a gap: the `if !self.silent` guard around a loop's emitting pass is provably redundant, because `_emit` re-checks the flag — so removing it is an equivalent mutant and survived correctly. The mutation now attacks `_emit`'s guard, which is where the two-phase discipline is actually enforced. The reference carries the same redundant guard, and the port keeps it for shape. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
Re-run on the clean tree after the three blind spots were closed. Every mutation is caught, and every one is caught by the layer the definition names: the lattice, the definite/maybe split, the leaf order, the exit rules, the branch join, the loop's two-phase emission, the evidence hop and the sort key through the fact-parity replay; the shared grammar's scope, tracked-flag and narrowing rules through both the replay and the own-ir unit controls. Two mutations attack the control rather than the port — they corrupt the frozen oracle and require the replay to fail, because a replay that survives a drifting oracle is comparing against nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Team Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…259 cp4b.2) `refuse_protocols` is gone. `own_bridge::check_facts` now runs the obligation family in its BR-V1 place — after effects, before OWN050 — through the shared grammar and `own_analysis`'s walk, and does the half the bridge owns: the (kind, definite) -> OBL001-004 table, the four deliberately line-free wordings with both exit_desc branches, the component/handler derivations, the anchorless advisory OBL005 with its sorted CPython-repr scope list, and the opened -> barrier (or exit) -> late-close slice with its line guard. The two reference documents leave `rust_replay_excluded` and the replay's pinned exclusion set drops from eight names to six. That is the contract change this checkpoint exists to make. Neither golden was regenerated: the port converges on `protocol_isloaded_violation` and its silent twin exactly as committed, on every `Finding` member. Seven synthetic Layer 3 cases close every row the corpus could not reach — OBL002/003/004/005, all four wordings, the two-, one- and zero-step slices, the identity derivations including the awkward splits, the tolerant door's skip-whole and first-wins rules, and the family composing with DI, effects and OWN050. Insertion-stable: zero existing records rewritten. An eighth case freezes the rendered surfaces — OD-6's literal `?` URI with the region omitted at level note, and a `codeFlows` built from a protocol slice. Two things measured rather than assumed, and recorded instead of faked into controls: the BR-V5 "a slice shorter than two steps is dropped" rule is NOT applied by the protocol path (a leak off the end carries a one-step slice, and one whose open has no line carries none), and the family's append POSITION is unobservable end to end because the sort key's code component decides before insertion order can. The surface inventory follows: the `.*` placeholder row becomes five wordings and two exit_desc tails, the two protocol slice families become five precise shapes plus an empty-slice degradation, and every one of them is now counted over the REPLAYED set instead of carrying a "row 4b" disposition. Shadow: the Rust engine's `verdicts` layer for the protocol document moves from `refused` to `produced`, so its artifact and trace regenerate — the only goldens this checkpoint rewrites, for the same reason #339 recorded when the capture moved partial -> full. The reducer's scope is untouched and still refuses Layer 3: that line is #260's. One gate is knowingly red until the next commit: cp4's mutation M14 attacked the refusal this checkpoint removes, so its definition is re-anchored on the rule as it is now stated (the family must not go silently missing) and the recorded result no longer matches its definition. The re-run follows immediately, exactly as d80359e did for the previous re-anchor. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
… 30/30 caught M14 attacked the refusal cp4b removes. Re-anchored on the rule as it is now stated — the obligation family must never go silently missing from a verdict list — and re-run on the clean tree, so the recorded result matches its definition again and the checkpoint-status gate is green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
…cp4b.2) The first bridge campaign caught 24 of 28 and named four things the controls could not see. Every one was real: * **first-wins was rescued by dedup.** The two duplicate `Dup` records named the SAME barrier, so keeping both produced two byte-identical findings that BR-V7 collapsed — the rule was unobservable through its own control. The second record now names a different barrier, so keeping it adds a finding at a different line. * **the malformed-method skip only proved the easy half.** The bad record was last, so a port that stopped at the first bad entry behaved identically. It is now first. * **the non-list-block control was vacuous.** With no protocols there is nothing to report either way; the rule is observable only through a SCOPED protocol, where an empty method list makes the rule dead and a silenced family says nothing. The control now carries both twins and says why. * **the rendered surfaces reached two of the five codes.** The render case had no exit leak and a single-entry scope list, so neither exit wording nor the `, ` CPython puts between scope entries was in the compared bytes. Both are now. The fifth finding was a broken mutation, not a gap: the "drop the opened step" rewrite did not compile, so it measured nothing. It now anchors that step at line 0 and lets the BR-V5 guard do the dropping. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
Re-run on the clean tree after the four blind spots were closed. Every mutation of the bridge's half of the obligation family is caught, and by the layer the definition names: the code table, the wordings and the identity derivations through the Layer 3 verdict replay; the slice, the anchorless advisory and the kind tag through the verdict replay AND the byte-exact rendered replay; the door-unreachable non-list rule through its raw-document unit control. Three mutations attack the controls rather than the port: two corrupt the frozen Layer 3 and rendered oracles, and one re-declares the exclusion this checkpoint promoted — so the promotion is a fact the replay enforces, not a sentence in a note. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
…cp4b.3) The obligation family is ported, replayed and promoted, so every surface that still said otherwise is corrected — and none of them gains a number: * **P-022** row 4b goes from "not started" to complete, with the wording this checkpoint earns and links to the generated fragments; the preferred queue drops 4b and now reads coordinate-domain decision → #259 final acceptance → #260 acceptance / #261. Two stale claims elsewhere in the table go with it: cp5's "what remains is row 4b and the coordinate decision", and step 7a's typed shadow counts — which 4b changed, which is exactly why that row now points at the census instead of restating it. * **`spec/Bridge.md` §6** no longer lists a protocol-bearing document among the declared boundaries; it records that it did until 4b and that a re-declared exclusion is a red build, not a note. * **`spec/BridgeBehaviorMatrix.md`** gains two rows — the analysis (core suite, with its own fact-parity family) and the verdict mapping (L3 ✅) — and the paragraph in (e) is rewritten: one row family is outside the replayed set now, not two. * **cp4 and cp5 notes** carry a "read as history" banner where they describe the refusal, so a reader cannot mistake a checkpoint record for current state. * **The proposals index** records row 4b and carries no measured count at all. * **Both campaigns are registered** in `render_checkpoint_status.py` (a new `p022-cp4b-mutations.md` fragment) and in `test_checkpoint_status.DEFINITIONS`, so they are rendered from evidence and re-anchored by the gate like every other campaign in the tree. * Two remaining live claims are fixed rather than left to rot: the verdict fixture harness's docstring and the repro manifest's pin for the protocol artifact. The checkpoint note gains its results package: what landed, the frozen fixtures and their regeneration commands, the one production dependency change, the zero-on-every-axis differential, what both campaigns found before they were green, and the two things measured rather than claimed — that the protocol path does not apply BR-V5's short-slice rule, and that the family's append position is unobservable end to end. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3
…d caveat BR-V5 Two places where a document said less, or other, than the evidence: * The cp4b note's §3.2 (written at 4b.0) claimed the tolerant door's protocol rules — malformed-entry skip and first-wins — are unreachable through the typed Rust constructor and pinned only by unit controls. The constructor checks protocol blocks for nesting depth alone; the grammar runs in the strict door, so the rules are reachable end to end, the synthetic case verdict_protocol_tolerant_door_rules replays them against Python's golden, and cp4b.2's M21–M23 are caught by that replay. The section now says so and names the one rule (non-list block) that is a unit control. * spec/Bridge.md BR-V5 states a slice shorter than two steps is dropped; _protocol_findings does not do that, so a leak off the end carries a one-step slice, and the port reproduces the reference. The sentence now carries the exception and points at the note that records the open Python-first decision, instead of a normative line one family knowingly does not implement. No code, fixtures or evidence change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016vuEiNoEXaooMDRu6tXrZ6
This was referenced Sep 7, 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.
Что и зачем
Checkpoint 4b issue #259: единственное семейство анализов, которого не было на Rust-стороне, — обязательственные протоколы (OBL001–005,
ownlang/obligations.py). Мост ОТКАЗЫВАЛ документу с непустымprotocols[], а два референсных документа сидели вrust_replay_excluded. Этот PR портирует анализ, проводит его через мост по BR-P3 и снимает оба исключения промоушеном. Python остаётся авторитетным ораклом; ни один голден не регенерируется, кроме shadow-артефактов документа с протоколом — по объяснённой причине.Тип изменения
Как проверено
python tests/run_tests.pyruff check .иmypycargo fmt --check,cargo clippy --workspace --all-targets(ноль предупреждений),cargo test --workspace --no-fail-fastp022-cp4b-133/33,p022-cp4b-228/28,p022-cp4(переякоренная M14) 30/30 — все с попаданием в названные catcher'ыСвязанные issue
Refs #259 (checkpoint 4b), #250, #260. Не закрывает #259: решение по домену координат этот PR не принимает.
Чеклист
feat:,fix:,docs:…)Формулировка, которую 4b зарабатывает
Не «#259 complete», не «shadow mode», не «P-022 done».
Что внутри
4b.0 — инвентаризация, без production-кода.
docs/notes/p022-bridge-verdict-checkpoint4b.md: каждое поведениеobligations.pyи маппинга BR-P3 с указанием, чем оно будет запинено, и измеренная картина того, как мало достигал корпус — ровно одна форма (definite-барьер с поздним close). Двухшагового слайса, OBL002/003/004/005, exit-анкоров, циклов, allow, opaque write, args-narrowing, дубликатов имён и malformed-записей не было вообще.4b.1 — порт анализа.
own-analysis/src/obligation.rsрядом сdi.rs/effect.rs(BR-B1). Типизированные значения строит ОДНА реализация грамматики с двумя потребителями:own-ir/src/protocol.rsвырастает из «только валидация» в «валидация и построение» — строгая дверь берёт идентичность, анализ берёт значение. Ни один текст и ни одна категория ошибок строгой двери не сдвинулись (cp1-ledger зелёный). Оракл — третья fact-parity семья по образцу DI/effect:tests/test_obligation_fact_parity.pyгоняет НАСТОЯЩИЕcheck_protocols/unmatched_scopesи замораживает нарушения целиком;own-analysis/tests/obligation_parity.rsреплеит те же сырые документы без Python, так что расхождение грамматики всплывает как расхождение вердикта.4b.2 — мост.
refuse_protocolsудалён; BR-P3 на своём месте по BR-V1 (после effects, до OWN050): таблица(kind, definite), четыре намеренно безстрочных сообщения, деривации component/handler, анкорлесс-advisory OBL005 с sorted CPython-repr списком scope, слайс opened→barrier(→late close) с line-guard'ом. Оба исключения сняты, pinned set 8 → 6. Голдены не регенерировались — порт сошёлся с ними как есть. Семь синтетических Layer 3 кейсов и один rendered-кейс (OD-6: URI?, region опущен, level note, и protocolcodeFlows) закрывают каждую строку, до которой корпус не доставал; insertion-stable, ноль переписанных записей.4b.3 — статусные поверхности. P-022 строка 4b → complete и очередь → «coordinate-domain decision → #259 final acceptance → #260 acceptance / #261»;
spec/Bridge.md§6; BehaviorMatrix (две новые строки, абзац в (e) переписан); баннеры «read as history» в cp4/cp5; индекс proposals — без набранных чисел; обе кампании зарегистрированы в рендерере и вDEFINITIONS.Найденные расхождения и их классификация
Над измеренным множеством: Python-only 0 / Rust-only 0 / changed 0 / ordering-only 0 / unexplained 0 — не подсчитано, а утверждено: реплеи собирают все расхождения без fail-fast и краснеют при любом. Ссылки: census, surface inventory, campaigns.
Два наблюдения измерены, а не объявлены:
_protocol_findingsфильтрует шаги сline < 1и на этом останавливается — утечка с конца метода несёт одношаговый слайс, а с открытием без строки — пустой. Порт воспроизводит референс точно; инвентарь расширен под реальные формы, а не порт подогнан под прозу. Что именно неправо — предложение спеки или код — вопрос Python-first, который 4b не решает.(file, line, column, code), а две находки разных семейств никогда не делят код.Что нашли кампании (обе прогонялись дважды)
4b.1: три выживших, два унаследованы из самого
tests/test_obligations.py— «allow побеждает barrier» было ненаблюдаемо (множества аргументов барьера и allow непересекающиеся),exit_barriers: falseпроверялся только против конца метода, а правило неизвестного аргумента маскировалось allow-списком. Четвёртая мутация выжила корректно: guardif !self.silentвокруг эмитирующего прохода доказуемо избыточен (_emitперепроверяет флаг) — эквивалентный мутант, и мутация перенесена на guard самого_emit.4b.2: first-wins спасался dedup'ом (дубликаты называли ОДИН барьер), skip malformed-метода проверял только лёгкую половину, контроль на non-list блок был вакуумным (правило наблюдаемо только через scoped протокол), а rendered-поверхности доставали два кода из пяти.
Регенерированные голдены
Ровно одно семейство:
tests/fixtures/repro/protocol_isloaded_violation.{repro,trace}.json— слойverdictsRust-движка переходитrefused→produced. Та же форма изменения, что #339 записал дляpartial→full. Редьюсерown-shadowне тронут: scope остался["lowered", "summaries"], Layer 3 по-прежнему refused — это граница #260.🤖 Generated with Claude Code
https://claude.ai/code/session_01WbgYFv2UW3iRJ3L33naVC3