feat(ownir): bound source coordinates and nesting depth (Python-first) - #326
Open
PhysShell wants to merge 4 commits into
Open
feat(ownir): bound source coordinates and nesting depth (Python-first)#326PhysShell wants to merge 4 commits into
PhysShell wants to merge 4 commits into
Conversation
`OwnIR` is a file some frontend wrote, and two of its shapes had no bound at all. The reference accepted both because PYTHON has no bound — integers are arbitrary-precision, recursion is limited only by the interpreter's stack. That is not generosity in the contract, it is an accident of the reference's implementation leaking into it. #259 cp1 measured the consequence: the Rust port refuses documents the reference accepts, across nine coordinate paths and both nesting trees. The honest reading is not "the port is over-strict" — it is that the fact vocabulary was only implementable in a language with bignums and a deep stack. Widening Rust to match (arbitrary precision, unbounded recursion) would spread the accident instead of fixing it. So, per the standing migration rule that a divergence is a Rust bug UNLESS behaviour changes in a separate Python-first PR: this is that PR. spec/OwnIR.md §4.2 the contract, normative ownlang/ownir.py line/column ranges, flow-body depth ownlang/obligations.py event-tree depth, event line range **Coordinates fit a signed 64-bit integer.** Every `line` is in [-2^63, 2^63-1] — services, ctor_line, root_resolve_sites[], scope_cache_sites[], effects, bindings, params, protocol events — and every `column` is 1..=2^63-1, absent, or null. A coordinate nothing downstream can hold is not a usable coordinate. **Flow bodies and event trees nest at most 32 levels.** Measured from both ends rather than picked: the deepest nesting in any OwnIR fixture in this repository is 3 (events: 2), and a parser with the widespread 128-level JSON recursion cap stops accepting these documents at 62, because each `if` costs two JSON levels. 32 is an order of magnitude above what producers emit and about half way to the ceiling consumers can parse. It is stated in the OwnIR domain — nested bodies — not in JSON levels, because nested bodies are what a frontend can reason about. Both are rejections at the strict door. `check_facts()` on un-validated facts keeps degrading to absent: two entry points, two contracts, as with `column` already. Twelve mutations. Ten caught, one invalid (raising the limit to 1000 makes CPython itself hit RecursionError, which is its own argument), and one SURVIVED and had to be fixed: P11 widening INT64_MAX to 2^64-1 was NOT caught. Because the test imported the constants it was testing, so every boundary case moved with them: it could prove the limits were enforced consistently and could not prove they were the right limits. The spec's numbers are now literals in the test. This is the same failure the cp1 ledger had one layer up — a test written in terms of the value under test asserts self-consistency, not correctness — and it is worth having hit it twice, in two places, to see that it is a pattern and not an incident. The off-by-one is also measured rather than reasoned: `_check_flow_columns` probes every op for then/else/body whether or not it has them, so checking depth before the early return counted the absent ones and rejected a body at exactly the limit. Only the at-limit case catches that, which is why every limit here is pinned at three points. No existing fixture changes: nothing in the tree nests past 3 or carries an out-of-range coordinate. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
📝 WalkthroughWalkthroughThe PR bounds validated OwnIR source coordinates to signed 64-bit values and limits recursive flow and protocol event trees to 32 levels. Python parsing and validation enforce these limits. The specification, schema, and tests define and verify the contract. ChangesOwnIR defensive limits
Estimated code review effort: 3 (Moderate) | ~20 minutes Possibly related PRs
Suggested reviewers: 🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
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 |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit:bc8790c5ba
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+183
to
+188
| **Source-coordinate integers fit a signed 64-bit integer.** | ||
| - every `line` — on services, `ctor_line`, `root_resolve_sites[]`, | ||
| `scope_cache_sites[]`, effects, bindings, params, and protocol events — lies | ||
| in `[-2^63, 2^63 - 1]`; | ||
| - every `column` (§4.1) is `1..=2^63 - 1`, or absent, or `null`. |
There was a problem hiding this comment.
When an owned-resource record or flow operation contains a line outside the signed 64-bit range, load() still accepts it: components[].subscriptions[].line is never checked, and _check_flow_columns() validates only column and nesting. For example, both a subscription and a return flow op with line: 2**80 pass the strict door, contradicting this new normative “every line” limit and preserving the Python/port divergence this change is intended to eliminate. Apply the integer type/range check to these records recursively as well.
AGENTS.md reference: AGENTS.md:L14-L14
Useful? React with 👍 / 👎.
Comment on lines
+185
to
+188
| - every `line` — on services, `ctor_line`, `root_resolve_sites[]`, | ||
| `scope_cache_sites[]`, effects, bindings, params, and protocol events — lies | ||
| in `[-2^63, 2^63 - 1]`; | ||
| - every `column` (§4.1) is `1..=2^63 - 1`, or absent, or `null`. |
There was a problem hiding this comment.
When a producer or non-Python consumer validates facts using spec/ownir.schema.json, out-of-range coordinates remain valid because sourceColumn has no maximum and every line schema still has only type: integer. The schema describes itself as the shared contract used to keep Python and Rust synchronized, so leaving these new normative bounds out recreates the exact cross-consumer acceptance mismatch this commit addresses; add the signed-64 constraints to the schema and bind them to the implementation with parity tests.
AGENTS.md reference: AGENTS.md:L14-L14
Useful? React with 👍 / 👎.
…in §4.2 Two review findings on bc8790c, both real, one with a wrong consequence attached. **The schema had to carry the bounds too.** `spec/ownir.schema.json` is what a NON-Python consumer validates against. With the bounds only in `load()`, a producer could be schema-valid and still refused at the door — the same cross-consumer mismatch this change exists to remove, one layer further out. Added `$defs.sourceLine` (signed-64) and a `maximum` on `sourceColumn`, and rebound all 21 inline `"line": {"type": "integer"}` fields to it. The test now asserts the schema's four numbers against the same literals as the code, so the two cannot drift. Mutation-proved both ways: widening `sourceLine.maximum` to `2^64-1` and dropping `sourceColumn.maximum` are each caught. **§4.2 said "every `line`" and two line-bearing fields escaped it.** The finding is right that the sentence overclaimed. Its stated consequence — that this "preserves the Python/port divergence" — is not: measured, both implementations accept those fields, because neither types them. python subscription line 2^80 : ACCEPT rust: ACCEPT python subscription line "x" : ACCEPT rust: ACCEPT python flow op line 2^80 : ACCEPT rust: ACCEPT python flow op line "x" : ACCEPT rust: ACCEPT `components[].subscriptions[].line` and the `line` on a flow op inside `functions[].body` are checked NOWHERE by `load()` — not for range, and not even for type. #325's validator has no check for them either (grep `"line"` in strict.rs: services, effects, bindings, params, sites — not these two). So this is not a parity gap, and closing it is not part of removing one. It is a separate contract question: whether a coordinate no rule reads should nevertheless have to be well-formed. Extending the check would be a new restriction on documents accepted today, arriving inside a PR whose job is to close a measured divergence — so §4.2 now enumerates exactly the fields it enforces, marks the word "validated" as load-bearing, and records the two exceptions with the measurement instead of quietly widening or quietly overclaiming. Corpus scan for the record: 150 JSON files, zero offenders on either path, so extending it later would break nothing in the tree. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@spec/ownir.schema.json`:
- Around line 305-307: Update the ctor_line property in the schema definition to
reference the existing sourceLine definition instead of accepting an
unrestricted integer, matching the validation used by ownlang/ownir.py. Add a
schema-path assertion in tests/test_ownir_defensive_limits.py that verifies
services[].ctor_line is bound to sourceLine.
- Around line 49-54: Update the sourceColumn schema definition to accept either
a 1-based integer within the existing bounds or an explicit null value, matching
OwnIR §4.2 and the behavior of ownlang/ownir.py while preserving validation for
non-null values.
- Line 111: Restore unrestricted integer schemas for resourceRecord.line at
spec/ownir.schema.json:111-111 and every flow-operation line at
spec/ownir.schema.json:193-287, replacing the sourceLine references so schema
validation remains consistent with load()’s documented unchecked paths; no
direct changes are required outside these schema sites.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: e516b20b-fceb-4fff-986d-7c28e81939d2
📒 Files selected for processing (5)
ownlang/obligations.pyownlang/ownir.pyspec/OwnIR.mdspec/ownir.schema.jsontests/test_ownir_defensive_limits.py
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
Three review findings on 9f909c7. All three real, and the middle one is mine — the schema edit was a blanket search-and-replace and it overshot. 1. `sourceColumn` refused `null`. `load()` accepts `column: null` (`_check_column` returns early on None) and §4.2 says so in the same commit, so the schema contradicted both. Now `["integer", "null"]`; `minimum`/`maximum` only constrain numbers, so real values keep their bounds. Pre-existing, but §4.2 made it visible. 2. `resourceRecord.line` and every `flowOp.line` were bound to `sourceLine` — the two paths §4.2 documents, in this same PR, as validated NOWHERE by `load()`. Binding them makes a producer schema-invalid on documents the door accepts, which is the same cross-consumer mismatch this change exists to remove, pointing the other way. Ten sites reverted to unrestricted integers. 3. `services[].ctor_line` was NOT bound, and `load()` does check it, so a schema-valid document could fail at the door. The blanket replace matched `"line"` and this key is `ctor_line`. Now bound. Both directions are defects, and this file shipped one of each. So the test no longer spot-checks four numbers — it asserts the whole binding map: bound service.line, service.ctor_line, site.line, effect.line, binding.line, param.line, protocolEvent.line unbound resourceRecord.line, flowOp.line with the reason attached to each side: bound because `load()` checks it, unbound because §4.2 records that it does not. A stale entry fails too — a def that no longer has the key stops being evidence. Three mutations, all caught: binding `flowOp.line`, unbinding `ctor_line`, and reverting `sourceColumn` to integer-only. Also: the first attempt at this fix round-tripped the schema through `json.dumps` and produced a 604-line reformat for a 12-line change. Redone as text edits. A diff nobody can read is not a small change however few things it means to say. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
@coderabbitai review |
✅ Action performedReview finished.
|
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@tests/test_ownir_defensive_limits.py`:
- Around line 204-234: Update `_line_refs` to retain each matched property
schema rather than only its `$ref` or `type` value. In the `UNBOUND` validation
branch, require a direct integer schema with no `$ref` and no numeric
constraints; keep the existing `sourceLine` reference check for `BOUND` and
preserve stale-binding detection.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 551179bd-e0ac-44e6-a92c-d7ef631fbe0b
📒 Files selected for processing (2)
spec/ownir.schema.jsontests/test_ownir_defensive_limits.py
Comment on lines
+204
to
+234
| def _line_refs(node: Any, key: str, out: list[Any]) -> None: | ||
| if isinstance(node, dict): | ||
| for k, v in node.items(): | ||
| if k == key and isinstance(v, dict): | ||
| out.append(v.get("$ref") or v.get("type")) | ||
| else: | ||
| _line_refs(v, key, out) | ||
| elif isinstance(node, list): | ||
| for v in node: | ||
| _line_refs(v, key, out) | ||
| for group, expect_bound in ((BOUND, True), (UNBOUND, False)): | ||
| for def_name, keys in group.items(): | ||
| for key in keys: | ||
| found: list[Any] = [] | ||
| _line_refs(defs.get(def_name, {}), key, found) | ||
| if not found: | ||
| failures += _fail( | ||
| f"$defs.{def_name} has no {key!r} — the binding map is " | ||
| f"stale, which means it is no longer evidence") | ||
| for ref in found: | ||
| is_bound = ref == "#/$defs/sourceLine" | ||
| if is_bound != expect_bound: | ||
| want = ("$ref sourceLine" if expect_bound | ||
| else "an unrestricted integer") | ||
| why = ("`load()` checks this path" | ||
| if expect_bound else | ||
| "`load()` does NOT check this path (§4.2)") | ||
| failures += _fail( | ||
| f"$defs.{def_name}.{key} is {ref!r}, expected " | ||
| f"{want} — {why}") |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win
Verify that unbound fields are unrestricted integers.
For UNBOUND, is_bound only rejects #/$defs/sourceLine. A mutation to #/$defs/sourceColumn or an inline bounded integer still passes this test.
Retain each property schema in _line_refs. For UNBOUND, assert a direct unrestricted integer schema with no $ref or numeric constraints. Otherwise, resourceRecord.line or flowOp.line can become schema-invalid while load() still accepts the value.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@tests/test_ownir_defensive_limits.py` around lines 204 - 234, Update
`_line_refs` to retain each matched property schema rather than only its `$ref`
or `type` value. In the `UNBOUND` validation branch, require a direct integer
schema with no `$ref` and no numeric constraints; keep the existing `sourceLine`
reference check for `BOUND` and preserve stale-binding detection.
The binding map added in 4125978 checked `ref != "#/$defs/sourceLine"` for the unbound paths, which is not the property it claims. Measured, both of these SURVIVED: flowOp.line -> $ref sourceColumn SURVIVED flowOp.line -> {"type":"integer","maximum":1000} SURVIVED Either one makes an unbound path narrower than `load()`, which is the mismatch the map exists to prevent — the assertion just could not see it, because it only knew one way of being narrow. `_line_refs` collapsed each property to `$ref or type` and threw the rest away. It now keeps the subschema, and the unbound side requires a plain `{"type": "integer"}` with none of `$ref`, `minimum`, `maximum`, `exclusiveMinimum`, `exclusiveMaximum`, `enum`, `const`, `multipleOf`. Four mutations, all caught: the two above, `line` retyped to string, and `service.line` losing its binding (the other direction, kept as a regression). Third time this PR that an assertion has been too loose to distinguish the mutation it was written for — the constants, then the binding direction, now the binding shape. Each was found by mutating rather than by reading, which is the only reason any of them are in the diff. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
10 tasks
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 freeto 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.
Что и зачем
Две формы в
OwnIRне имели никакой границы, и reference принимал их потому что границы нет у Python: целые произвольной точности, рекурсия ограничена только стеком интерпретатора. Это не щедрость контракта, а особенность конкретной реализации, протёкшая в контракт. Ставим границы Python-first: signed-64 для координат и 32 уровня вложенности для flow-тел и деревьев событий.Разблокирует #325 (#259 cp1). Пока этих границ нет, cp1 не может быть закрыт честно — см. ниже.
Тип изменения
Как проверено
python tests/run_tests.pyruff check .иmypy(30 файлов)python tests/test_ownir_defensive_limits.py— новый, в suite подхватывается авто-discoveryRust не менялся: он здесь пострадавшая сторона, а не предмет правки.
Связанные issue
Refs #250, #259. Ничего не закрывает; блокирует merge #325.
Чеклист
spec/OwnIR.md§4.2 — нормативный текст,spec/ownir.schema.json— машинный контракт)Откуда это взялось
#259 cp1 измерил расхождение: Rust-порт отвергает документы, которые reference принимает — по девяти координатным путям и обоим деревьям вложенности.
Соблазнительное прочтение — «порт слишком строг». Честное — что словарь фактов был реализуем только на языке с bignum'ами и глубоким стеком. Расширять Rust (arbitrary precision,
unbounded_depth,serde_stacker) означало бы разнести случайность дальше вместо того, чтобы её убрать.Действующее правило миграции: расхождение Rust/Python — баг Rust, если только поведение не меняется отдельным Python-first PR. Это он.
Что именно ограничено
Координаты помещаются в signed 64-bit. Каждый валидируемый
lineв[-2^63, 2^63-1]:services[].line,ctor_line,root_resolve_sites[].line,scope_cache_sites[].line,effects[].line,bindings[].line,params[].line,protocol_functions[].events[].line. Каждыйcolumn—1..=2^63-1, либо отсутствует, либоnull.Слово «валидируемый» несущее:
components[].subscriptions[].lineиlineна flow-операции не проверяютсяload()вообще — ни на диапазон, ни даже на тип. Замерено,{"line": "x"}принимается на обоих. Это предшествует данному PR, и обе реализации ведут себя одинаково, поэтому это не parity-разрыв. Записано в §4.2 как отдельный открытый вопрос контракта, а не закрыто молча расширением acceptance внутри PR, чья задача — устранить расхождение. Скан корпуса: 150 файлов, 0 нарушителей, так что расширить позже ничего не сломает.Flow-тела и деревья событий вложены не глубже 32 уровней. Граница выведена измерением с двух сторон:
OwnIR-фикстуре репозитория — 3 (tests/fixtures/lowered/hoist_neg_nested_depth.facts.json); самое глубокое дерево событий — 2;ifстоит двух JSON-уровней.32 — на порядок выше всего, что производят фронтенды, и примерно вполовину до потолка, который потребитель ещё разбирает. Записано в домене OwnIR — вложенные тела, — а не в JSON-уровнях.
Обе границы — отказы строгой двери, не приведение.
check_facts()сохраняет degrade-to-absent: две точки входа, два контракта.Схема несёт те же числа
spec/ownir.schema.json— то, против чего валидируется не-Python потребитель. Если границы живут только вload(), производитель может быть schema-valid и всё равно получить отказ на двери — тот же cross-consumer mismatch, слоем наружу.Добавлен
$defs.sourceLine(signed-64),maximumнаsourceColumn, иsourceColumnтеперь допускаетnull(load()его принимает — расхождение было и до этого PR, §4.2 сделала его видимым).И binding-карта проверяется как карта:
sourceLineservice.line,service.ctor_line,site.line,effect.line,binding.line,param.line,protocolEvent.lineresourceRecord.line,flowOp.lineПричина прикреплена к каждой стороне: привязано, потому что
load()проверяет; не привязано, потому что §4.2 фиксирует, что не проверяет. Устаревшая запись тоже валит тест —$def, потерявший ключ, перестаёт быть свидетельством.Mutation-кампания: 18 мутаций, 15 пойманы, 1 invalid, 2 выжили
whileINT64_MAXдо2^64-1RecursionErrorsourceLine.maximum, убратьsourceColumn.maximumflowOp.line→$ref sourceColumnflowOp.line→ инлайновыйmaximumflowOp.line→ stringservice.lineтеряет привязкуВыжившие важнее пойманных, и обе — одна и та же ошибка в двух местах.
(1) Тест импортировал константы, которые проверял, поэтому каждый граничный случай двигался вместе с ними. Он мог доказать, что лимиты применяются согласованно, и не мог доказать, что они правильные. Числа спеки теперь литералы.
(2) Binding-карта проверяла
ref != sourceLine— то есть знала ровно один способ быть узким. Привязка кsourceColumnили инлайновыйmaximumпроходили. Теперь сохраняется весь subschema, и непривязанная сторона требует чистый{"type": "integer"}без$ref,minimum,maximum,exclusiveMinimum,exclusiveMaximum,enum,const,multipleOf.Оба раза утверждение было слишком слабым, чтобы отличить мутацию, ради которой написано. Оба найдены мутированием, ни одно — чтением. Это тот же провал, что ledger в cp1 одним слоем выше: тест, написанный в терминах проверяемого значения, утверждает самосогласованность, а не корректность.
Off-by-one тоже измерен, а не выведен
_check_flow_columnsопрашивает каждый op наthen/else/bodyнезависимо от того, есть ли они. Проверка глубины до early-return считала отсутствующие и отвергала тело ровно на лимите. Поймал это только at-limit случай — поэтому каждый лимит закреплён в трёх точках: ниже, ровно на, и на один сверх.Раунд ревью
Codex на
bc8790c, 2 находки. Схемную взял. Вторую («§4.2 говорит every line, а два поля ускользают») взял как правку формулировки, а её заявленное следствие опроверг измерением: components/flow-oplineне валидируются нигде и принимаются обеими реализациями, так что это не parity-разрыв.CodeRabbit на
9f909c7, 3 находки, все верные, средняя — моя. Правка схемы была сплошным search-and-replace по"line"и промахнулась в обе стороны сразу: привязалаresourceRecord.lineи девятьflowOp.line— ровно те пути, которые §4.2 в том же коммите объявляет непроверяемыми, — и пропустилаctor_line, потому что ключ другой. Схема стала строже двери в одном месте и слабее в другом. Из одной механической правки.CodeRabbit на
4125978, 1 находка, верная — binding-карта, выжившая (2) выше.Первая попытка схемной правки прогнала файл через
json.dumpsи дала 604 строки переформатирования на изменение в 12 строк. Переделано текстовыми правками: диff, который нельзя прочитать, не является маленьким изменением, сколько бы мало он ни хотел сказать.Почему это блокирует #325
Сейчас cp1 отчитывается «0/0/0 на 193 контролях», но эти два семейства из ledger'а намеренно исключены. Буквально: «0/0/0 на множестве, из которого удалены два известных расхождения». #259 требует parity, а не «parity кроме двух известных мест».
Последовательность: этот PR → rebase #325 → boundary-контроли для обоих семейств → регенерация ledger'а → безусловное 0/0/0 → merge #325.
Существующие фикстуры не меняются: в дереве ничто не вложено глубже 3 и не несёт координат вне диапазона.
Generated by Claude Code