Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 46 additions & 5 deletions ownlang/obligations.py
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,33 @@
# matcher vocabulary for `opens`/`closes`/`barriers`/`allow`.
MATCHER_KINDS = frozenset({"assign", "call"})

# ---------------------------------------------------------------------------
# defensive limits on externally supplied structure (spec/OwnIR.md §4.2)
# ---------------------------------------------------------------------------

# The representable range of an OwnIR source-coordinate integer.
#
# Python integers are unbounded; a consumer's are not. Leaving the range open
# means the fact vocabulary is only *implementable* in a language with bignums,
# which is a contract accident rather than a decision — so the bound is stated
# here and enforced, instead of being discovered downstream as a port bug.
INT64_MIN = -(2 ** 63)
INT64_MAX = 2 ** 63 - 1

# Maximum nesting of `if`/`while` bodies in a flow body or an event tree.
#
# Chosen by measurement, from both ends:
# * the deepest nesting in any OwnIR fixture in this repository is 3
# (`tests/fixtures/lowered/hoist_neg_nested_depth.facts.json`);
# * a JSON parser applying the common 128-level recursion cap stops accepting
# these documents at 62 levels, because each `if` costs two JSON levels.
# 32 sits an order of magnitude above anything a producer has emitted and
# roughly half way to the ceiling every consumer can still parse.
#
# The limit is on the OwnIR *domain* — nested bodies — not on JSON nesting,
# because that is the thing a frontend can reason about.
MAX_NESTING_DEPTH = 32


class ProtocolFactsError(ValueError):
"""A malformed protocol/event fact. `load()` wraps this in `OwnIRError`
Expand Down Expand Up @@ -212,6 +239,10 @@ def _opt_line(raw: dict[str, Any], ctx: str) -> int:
v = raw.get("line", 0)
if not isinstance(v, int) or isinstance(v, bool):
raise ProtocolFactsError(f"{ctx}: 'line' must be an integer, got {v!r}")
if not INT64_MIN <= v <= INT64_MAX:
raise ProtocolFactsError(
f"{ctx}: 'line' must fit a signed 64-bit integer, got {v} "
f"(spec/OwnIR.md §4.2)")
return v


Expand Down Expand Up @@ -296,9 +327,18 @@ def parse_protocol(raw: Any) -> Protocol:
methods=tuple(methods_raw), description=desc)


def parse_events(raw: Any, ctx: str) -> tuple[Event, ...]:
def parse_events(raw: Any, ctx: str, depth: int = 0) -> tuple[Event, ...]:
"""Parse an ordered event list (recursive over `if`/`while`), fail-loud on
an unknown `ev` — the same rule as an unknown flow op (OwnIR IR4)."""
an unknown `ev` — the same rule as an unknown flow op (OwnIR IR4).

`depth` counts enclosing `if`/`while` bodies; the top-level list is 0. The
bound is a defensive limit on external input (spec/OwnIR.md §4.2), not a
reachable property of real code — the deepest event tree in this
repository's fixtures is 2."""
if depth > MAX_NESTING_DEPTH:
raise ProtocolFactsError(
f"{ctx}: events nested deeper than {MAX_NESTING_DEPTH} levels "
f"(spec/OwnIR.md §4.2)")
if not isinstance(raw, list):
raise ProtocolFactsError(f"{ctx}: events must be an array, got {raw!r}")
out: list[Event] = []
Expand Down Expand Up @@ -332,10 +372,11 @@ def parse_events(raw: Any, ctx: str) -> tuple[Event, ...]:
out.append(ThrowEv(line=line))
elif ev == "if":
out.append(IfEv(line=line,
then=parse_events(e.get("then", []), ctx),
orelse=parse_events(e.get("else", []), ctx)))
then=parse_events(e.get("then", []), ctx, depth + 1),
orelse=parse_events(e.get("else", []), ctx, depth + 1)))
else: # "while" — EVENT_KINDS is closed, checked above
out.append(WhileEv(line=line, body=parse_events(e.get("body", []), ctx)))
out.append(WhileEv(
line=line, body=parse_events(e.get("body", []), ctx, depth + 1)))
return tuple(out)


Expand Down
52 changes: 48 additions & 4 deletions ownlang/ownir.py
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,9 @@
from .effects import find_effect_storms
from .evidence import code_flow, di_path_steps
from .obligations import (
INT64_MAX,
INT64_MIN,
MAX_NESTING_DEPTH,
MethodEvents,
Protocol,
ProtocolFactsError,
Expand Down Expand Up @@ -536,6 +539,21 @@ def build_sarif(findings: list[Finding], severity: str = "error") -> dict[str, A
}


def _check_int_range(v: int, where: str, field: str = "line") -> None:
"""The representable range of an OwnIR source coordinate (spec/OwnIR.md §4.2).

Python integers are unbounded; a consumer's are not. Without this bound the
fact vocabulary is only implementable in a language with bignums, which is a
contract accident rather than a decision — and it surfaces downstream as a
port rejecting a document the reference accepted. Stated and enforced here
instead, Python-first.
"""
if not INT64_MIN <= v <= INT64_MAX:
raise OwnIRError(
f"{where} {field!r} must fit a signed 64-bit integer, got {v} "
f"(spec/OwnIR.md §4.2)")


def _check_column(v: Any, where: str) -> None:
"""Fail-loud shape check for an optional source `column` (#317).

Expand All @@ -554,21 +572,38 @@ def _check_column(v: Any, where: str) -> None:
if isinstance(v, bool) or not isinstance(v, int) or v < 1:
raise OwnIRError(
f"{where} 'column' must be a 1-based integer or absent, got {v!r}")
# …and bounded above, for the same reason `line` is (spec/OwnIR.md §4.2):
# a column no consumer can represent is not a usable coordinate.
_check_int_range(v, where, "column")


def _check_flow_columns(nodes: Any, where: str) -> None:
"""Validate `column` on every flow op, including inside `if`/`while` bodies.
def _check_flow_columns(nodes: Any, where: str, depth: int = 0) -> None:
"""Validate `column` on every flow op, including inside `if`/`while` bodies,
and bound how deeply those bodies may nest.

Recursive because a hoisted branch acquire - the path most likely to be
forgotten - lives inside a nested body, not at the top level."""
forgotten - lives inside a nested body, not at the top level.

`depth` counts enclosing bodies; the top-level list is 0. The bound is a
defensive limit on external input (spec/OwnIR.md §4.2), not a property real
code reaches - the deepest flow body in this repository's fixtures is 3."""
# The early return comes FIRST. Every op is probed for `then`/`else`/`body`
# whether or not it has them, so checking depth before this would count the
# absent ones and reject a body at exactly the limit — measured, not
# reasoned: `body nesting 32 (at limit)` was rejected until this order was
# fixed. Only a list that actually exists is a level.
if not isinstance(nodes, list):
return
if depth > MAX_NESTING_DEPTH:
raise OwnIRError(
f"{where} nested deeper than {MAX_NESTING_DEPTH} levels "
f"(spec/OwnIR.md §4.2)")
for n in nodes:
if not isinstance(n, dict):
continue
_check_column(n.get("column"), f"{where} op {n.get('op')!r}")
for key in ("then", "else", "body"):
_check_flow_columns(n.get(key), where)
_check_flow_columns(n.get(key), where, depth + 1)


def load(path: str) -> dict[str, Any]:
Expand Down Expand Up @@ -679,12 +714,14 @@ def load(path: str) -> dict[str, Any]:
ln = s.get("line", 0)
if not isinstance(ln, int) or isinstance(ln, bool):
raise OwnIRError("service 'line' must be an integer")
_check_int_range(ln, "service")
# the consuming-constructor location (optional, P-006 Q#1) is validated like file/line.
if not isinstance(s.get("ctor_file", "?"), str):
raise OwnIRError("service 'ctor_file' must be a string")
cln = s.get("ctor_line", 0)
if not isinstance(cln, int) or isinstance(cln, bool):
raise OwnIRError("service 'ctor_line' must be an integer")
_check_int_range(cln, "service", "ctor_line")
if not isinstance(s.get("ctor_type", ""), str):
raise OwnIRError("service 'ctor_type' must be a string")
# DI004 call-site metadata (optional): an array of {type, file, line} objects.
Expand All @@ -697,6 +734,8 @@ def load(path: str) -> dict[str, Any]:
raise OwnIRError(
"service 'root_resolve_sites' must be an array of "
"{type:str, file:str, line:int} objects")
for site in sites:
_check_int_range(site.get("line", 0), "service root_resolve_site")
# DI005 (scope-cached captive): types resolved from a self-created scope and cached
# into a field, plus their field-store sites — validated like root_resolves / its sites.
scope_cached = s.get("scope_cached", [])
Expand All @@ -712,6 +751,8 @@ def load(path: str) -> dict[str, Any]:
raise OwnIRError(
"service 'scope_cache_sites' must be an array of "
"{type:str, file:str, line:int} objects")
for site in csites:
_check_int_range(site.get("line", 0), "service scope_cache_site")
# Optional reactive-effect graph (EFF001 — effect storm, P-020). Additive and
# optional: an older core simply ignores it. Each effect carries its render-scope
# binding table; the core (ownlang/effects.py) decides identity stability.
Expand All @@ -728,6 +769,7 @@ def load(path: str) -> dict[str, Any]:
eln = eff.get("line", 0)
if not isinstance(eln, int) or isinstance(eln, bool):
raise OwnIRError("effect 'line' must be an integer")
_check_int_range(eln, "effect")
binds = eff.get("bindings", [])
if not isinstance(binds, list) or not all(isinstance(b, dict) for b in binds):
raise OwnIRError("effect 'bindings' must be a JSON array of objects")
Expand All @@ -742,6 +784,7 @@ def load(path: str) -> dict[str, Any]:
bln = b.get("line", 0)
if not isinstance(bln, int) or isinstance(bln, bool):
raise OwnIRError("binding 'line' must be an integer")
_check_int_range(bln, "binding")
# Optional per-method flow bodies (P-016 B0b/B2 — local IDisposable
# acquire/use/release over a CFG). Additive/optional; an older core ignores it.
fns = result.get("functions", [])
Expand Down Expand Up @@ -777,6 +820,7 @@ def load(path: str) -> dict[str, Any]:
if not isinstance(pl, int) or isinstance(pl, bool):
raise OwnIRError(
f"parameter 'line' must be an integer, got {pl!r}")
_check_int_range(pl, "parameter")
_check_column(p.get("column"), "parameter")
peff = p.get("effect")
if peff is not None and peff not in _PARAM_EFFECTS:
Expand Down
58 changes: 58 additions & 0 deletions spec/OwnIR.md
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,64 @@ when a real `startLine` is present. It is what OwnAudit's `finding-occurrence/v1
physical anchor reads (Own.NET#317, PhysShell/OwnAudit#58); a finding without one
is anchored line-only, which is a degradation rather than a failure.

### 4.2 Defensive limits on externally supplied structure (normative)

`OwnIR` is untrusted input: a file a frontend wrote, that `load()` reads. Two of
its shapes were unbounded, and an unbounded contract is only *implementable* in
a language that happens to have the same capabilities the reference does. Both
are now bounded, and the bound is part of the vocabulary rather than a property
of whichever consumer reads it first.

**Source-coordinate integers fit a signed 64-bit integer.**

- every **validated** `line` — `services[].line`, `services[].ctor_line`,
`services[].root_resolve_sites[].line`, `services[].scope_cache_sites[].line`,
`effects[].line`, `effects[].bindings[].line`, `functions[].params[].line`,
`protocol_functions[].events[].line` — lies in `[-2^63, 2^63 - 1]`;
- every `column` (§4.1) is `1..=2^63 - 1`, or absent, or `null`.
Comment on lines +183 to +189

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Bound every line-bearing OwnIR record

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 👍 / 👎.


The word *validated* is load-bearing, and the exception is recorded rather than
papered over. Two line-bearing fields are checked **nowhere** by `load()` — not
for range, and not even for type: `components[].subscriptions[].line` and the
`line` on a flow op inside `functions[].body`. Measured, `{"line": "x"}` and
`{"line": true}` are accepted on both. That predates this section, and both
implementations agree about it — neither the reference nor the Rust port types
those fields — so it is **not** a parity gap and closing it is not part of
removing one. It is a separate contract question: whether a coordinate that no
rule reads should nevertheless be well-formed. Until it is answered, the bound
above claims exactly the fields it covers.

Python integers are unbounded, so the reference accepted coordinates no other
consumer could represent. That is not a generosity worth keeping: a coordinate
nothing downstream can hold is not a usable coordinate, and leaving it legal
turns every port into a source of "the reference accepted this and I cannot".
The bound is stated here and enforced in `load()`.

**Flow bodies and protocol event trees nest at most 32 levels.**

`functions[].body` and `protocol_functions[].events` nest through `then`,
`else` and `body`. The limit counts those enclosing bodies — the top-level list
is level 0 — so a document nesting exactly 32 is accepted and 33 is rejected.

32 is chosen from measurement at both ends:

- the deepest nesting in any `OwnIR` fixture in this repository is **3**
(`tests/fixtures/lowered/hoist_neg_nested_depth.facts.json`); the deepest
event tree is **2**;
- a JSON parser applying the widespread 128-level recursion cap stops accepting
these documents at **62** levels, because each `if` costs two JSON levels
(an object and an array).

So the limit sits an order of magnitude above anything a producer has emitted
and roughly half way to the ceiling a consumer can still parse. It is expressed
in the `OwnIR` domain — nested bodies — and not in JSON levels, because nested
bodies are the thing a frontend can reason about; the ratio between the two is
an encoding detail.

Both limits are **rejections at the strict door**, not coercions. `check_facts()`
on un-validated facts keeps its existing degrade-to-absent behaviour: two entry
points, two contracts, as with `column` in §4.1.

## 5. Flow bodies (`functions[]`)

A flow function has a `name`, a `file`, and a `body`: an ordered list of flow
Expand Down
33 changes: 20 additions & 13 deletions spec/ownir.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,15 @@
"$defs": {
"sourceColumn": {
"description": "1-based source column of the SAME node `line` anchors on. Optional and additive, so OWNIR_VERSION stays 0 (spec/OwnIR.md §2): a producer that does not report one omits it and no consumer substitutes a value — not 0, not 1, and never recovered by re-reading the source line. Rides to SARIF as region.startColumn, where the OwnAudit occurrence anchor reads it (Own.NET#317).",
"type": ["integer", "null"],
"minimum": 1,
"maximum": 9223372036854775807
},
Comment thread
coderabbitai[bot] marked this conversation as resolved.
"sourceLine": {
"description": "A source line. Bounded to a signed 64-bit integer (spec/OwnIR.md \u00a74.2): Python integers are unbounded and the reference used to accept coordinates no other consumer could represent, which made the vocabulary implementable only in a language with bignums. A coordinate nothing downstream can hold is not a usable coordinate. Pinned to ownlang/obligations.py::INT64_MIN/INT64_MAX.",
"type": "integer",
"minimum": 1
"minimum": -9223372036854775808,
"maximum": 9223372036854775807
},
"resourceKind": {
"description": "The resource-kind discriminator (spec/OwnIR.md §4). It selects the analysis path, so a present-but-unknown value is rejected at load (fail-loud) and a new kind must bump OWNIR_VERSION. Pinned to ownlang/ownir.py::_KNOWN_RESOURCE_KINDS.",
Expand Down Expand Up @@ -82,7 +89,7 @@
"properties": {
"type": { "type": "string" },
"file": { "type": "string" },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
}
},
"component": {
Expand Down Expand Up @@ -168,7 +175,7 @@
"required": ["name"],
"properties": {
"name": { "type": "string" },
"line": { "type": "integer" },
"line": { "$ref": "#/$defs/sourceLine" },
"column": { "$ref": "#/$defs/sourceColumn" },
"effect": { "$ref": "#/$defs/paramEffect" }
}
Expand Down Expand Up @@ -295,9 +302,9 @@
"weak_deps": { "type": "array", "items": { "type": "string" } },
"root_resolves": { "type": "array", "items": { "type": "string" } },
"file": { "type": "string" },
"line": { "type": "integer" },
"line": { "$ref": "#/$defs/sourceLine" },
"ctor_file": { "type": "string" },
"ctor_line": { "type": "integer" },
"ctor_line": { "$ref": "#/$defs/sourceLine" },
"ctor_type": { "type": "string" },
"root_resolve_sites": { "type": "array", "items": { "$ref": "#/$defs/site" } },
"scope_cached": { "type": "array", "items": { "type": "string" } },
Expand All @@ -311,7 +318,7 @@
"description": "Whether the effect performs I/O (default false).",
"type": "boolean"
},
"line": { "type": "integer" },
"line": { "$ref": "#/$defs/sourceLine" },
"deps": {
"description": "The effect's dependency-array names.",
"type": "array",
Expand All @@ -333,7 +340,7 @@
"type": "string"
},
"refs": { "type": "array", "items": { "type": "string" } },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
}
},
"protocolMatcher": {
Expand Down Expand Up @@ -420,7 +427,7 @@
"ev": { "const": "assign" },
"target": { "type": "string", "minLength": 1 },
"value": { "type": ["boolean", "null"] },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
},
"required": ["ev", "target"]
},
Expand All @@ -431,7 +438,7 @@
"ev": { "const": "call" },
"callee": { "type": "string", "minLength": 1 },
"arg": { "type": ["string", "null"] },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
},
"required": ["ev", "callee"]
},
Expand All @@ -440,7 +447,7 @@
"description": "A normal method exit.",
"properties": {
"ev": { "const": "return" },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
},
"required": ["ev"]
},
Expand All @@ -449,7 +456,7 @@
"description": "An exceptional method exit. Frontends thread finally bodies onto exits, like the flow lowering (§5).",
"properties": {
"ev": { "const": "throw" },
"line": { "type": "integer" }
"line": { "$ref": "#/$defs/sourceLine" }
},
"required": ["ev"]
},
Expand All @@ -458,7 +465,7 @@
"description": "A branch with both arms lowered.",
"properties": {
"ev": { "const": "if" },
"line": { "type": "integer" },
"line": { "$ref": "#/$defs/sourceLine" },
"then": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } },
"else": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } }
},
Expand All @@ -469,7 +476,7 @@
"description": "A loop; the checker solves the body to a local fixpoint.",
"properties": {
"ev": { "const": "while" },
"line": { "type": "integer" },
"line": { "$ref": "#/$defs/sourceLine" },
"body": { "type": "array", "items": { "$ref": "#/$defs/protocolEvent" } }
},
"required": ["ev"]
Expand Down
Loading
Loading