feat(d5.4): RID indirection in the core flow analysis (step 0, no-op)

ownlang/analysis.py

@@ -89,15 +89,64 @@ class Loan:
 
 @dataclass
 class State:
+    # `var` is keyed by **RID** (resource id), not by handle identity. A RID is the
+    # obligation that carries the {OWNED,MOVED,RELEASED,ESCAPED} state; a handle
+    # (local/param symbol) denotes a RID through `handle_rid`. See the class note in
+    # `rid_of`. (D5.4 step 0 — the no-op identity refactor that lets step 1 add
+    # `alias_join`: two handles → one RID. Until an alias is minted the map is 1:1
+    # and the analysis is byte-for-byte the pre-RID behaviour.)
     var: dict[int, set[VarState]] = field(default_factory=dict)
     loans: dict[int, Loan] = field(default_factory=dict)
+    handle_rid: dict[int, int] = field(default_factory=dict)
 
     def copy(self) -> State:
         return State(
             var={k: set(v) for k, v in self.var.items()},
             loans=dict(self.loans),
+            handle_rid=dict(self.handle_rid),
         )
 
+    def rid_of(self, sym: Symbol) -> int:
+        """Resolve a handle to its resource id (RID).
+
+        Default is **1:1**: a handle that has not been explicitly aliased denotes
+        its own resource, keyed by the originating symbol's identity. Choosing
+        ``RID == id(sym)`` for an un-aliased handle is what makes step 0 a no-op —
+        every ``var`` key is the same int it was before the indirection, so
+        ``_sym_by_id`` still resolves a RID straight back to its symbol. D5.4
+        step 1's ``alias_join`` is the only operation that points a *second* handle
+        at an existing RID; until then this is the identity map."""
+        return self.handle_rid.get(id(sym), id(sym))
+
+    def mint(self, sym: Symbol) -> int:
+        """Bind `sym` to a fresh resource (its own RID) — the 1:1 acquire. Records
+        the mapping explicitly so the handle is a known owning alias of the RID."""
+        rid = id(sym)
+        self.handle_rid[id(sym)] = rid
+        return rid
+
+
+def _join_handle_rid(a: dict[int, int], b: dict[int, int]) -> dict[int, int]:
+    """Join the handle→RID maps of two merging paths. Under the step-0 1:1 invariant
+    a handle resolves to the same RID on every path that knows it (RIDs are minted
+    deterministically as ``id(sym)``), so the union cannot conflict. Assert that —
+    locking the invariant the way `join` already locks the block-scoped-loan one —
+    rather than silently picking a side. Step 1 (aliasing) will revisit this join."""
+    out = dict(a)
+    for handle, rid in b.items():
+        if handle in out:
+            # An explicit raise, not `assert`: `python -O` strips asserts, and a
+            # silently-kept wrong mapping would defeat the whole point of locking
+            # the invariant. Keep it loud in every build.
+            if out[handle] != rid:
+                raise AssertionError(
+                    "a handle maps to two different RIDs at a control-flow merge; "
+                    "the D5.4 step-0 invariant is a single 1:1 handle->RID mapping"
+                )
+        else:
+            out[handle] = rid
+    return out
+
 
 def join(a: State, b: State) -> State:
     out = State()
@@ -112,6 +161,7 @@ def join(a: State, b: State) -> State:
         "for block-scoped borrows (they close within the scope that opened them)"
     )
     out.loans = dict(a.loans)
+    out.handle_rid = _join_handle_rid(a.handle_rid, b.handle_rid)
     return out
 
 
@@ -130,7 +180,7 @@ def initial_state(self) -> State:
         s = State()
         for p in self.cfg.params:
             if p.kind == Kind.OWNED:
-                s.var[id(p)] = {VarState.OWNED}
+                s.var[s.mint(p)] = {VarState.OWNED}
         return s
 
     def err(self, code: str, msg: str, line: int,
@@ -163,7 +213,7 @@ def binding_live(self, st: State, sym: Symbol) -> bool:
     # operation `verb` is attempted on owned symbol `sym`. Handles the
     # gone / maybe-gone cases shared by use/move/release/borrow/consume.
     def _state_problem(self, st: State, sym: Symbol, verb: str, line: int) -> bool:
-        S = st.var.get(id(sym), {VarState.OWNED})
+        S = st.var.get(st.rid_of(sym), {VarState.OWNED})
         subj = sym.origin
         kind = sym.resource_kind
         if VarState.OWNED not in S:
@@ -281,13 +331,13 @@ def first_line(self) -> int:
 
     def leak_check(self, st: State, at_line: int, context: str,
                    exclude: Symbol | None = None) -> None:
-        excl = id(exclude) if exclude is not None else None
-        for symid, states in st.var.items():
-            if symid == excl:
+        excl = st.rid_of(exclude) if exclude is not None else None
+        for rid, states in st.var.items():
+            if rid == excl:
                 continue
             if VarState.OWNED in states:
-                sym = self._sym_by_id(symid)
-                name = sym.name if sym else f"#{symid}"
+                sym = self._sym_by_id(rid)
+                name = sym.name if sym else f"#{rid}"
                 self.err("OWN001",
                          f"'{name}' is owned but not released {context} "
                          f"(leaks on at least one path)", at_line,
@@ -322,23 +372,23 @@ def transfer(self, blk: Block, st: State) -> State:
 
     def step(self, ins: Instr, st: State) -> None:
         if isinstance(ins, Acquire):
-            st.var[id(ins.sym)] = {VarState.OWNED}
+            st.var[st.mint(ins.sym)] = {VarState.OWNED}
             return
 
         if isinstance(ins, AcquireBuffer):
-            st.var[id(ins.sym)] = {VarState.OWNED}
+            st.var[st.mint(ins.sym)] = {VarState.OWNED}
             return
 
         if isinstance(ins, MoveInto):
             self._consume_like(st, ins.src, "move", ins.line, code_borrowed="OWN007")
-            st.var[id(ins.src)] = {VarState.MOVED}
-            st.var[id(ins.dst)] = {VarState.OWNED}
+            st.var[st.rid_of(ins.src)] = {VarState.MOVED}
+            st.var[st.mint(ins.dst)] = {VarState.OWNED}
             return
 
         if isinstance(ins, Release):
             subj = ins.sym.origin
             rkind = ins.sym.resource_kind
-            S = st.var.get(id(ins.sym), {VarState.OWNED})
+            S = st.var.get(st.rid_of(ins.sym), {VarState.OWNED})
             if {VarState.RELEASED} == S:
                 self.err("OWN003", f"'{ins.sym.name}' is released twice",
                          ins.line, subject=subj, resource_kind=rkind)
@@ -353,7 +403,7 @@ def step(self, ins: Instr, st: State) -> None:
                     self.err("OWN008",
                              f"cannot release '{ins.sym.name}' while it is borrowed",
                              ins.line, subject=subj, resource_kind=rkind)
-            st.var[id(ins.sym)] = {VarState.RELEASED}
+            st.var[st.rid_of(ins.sym)] = {VarState.RELEASED}
             return
 
         if isinstance(ins, Use):
@@ -411,7 +461,7 @@ def step(self, ins: Instr, st: State) -> None:
             if ins.sym is not None:
                 subj = ins.sym.origin
                 rkind = ins.sym.resource_kind
-                S = st.var.get(id(ins.sym), {VarState.OWNED})
+                S = st.var.get(st.rid_of(ins.sym), {VarState.OWNED})
                 if VarState.OWNED not in S:
                     if VarState.MOVED in S:
                         self.err("OWN005",
@@ -442,7 +492,7 @@ def step(self, ins: Instr, st: State) -> None:
                                  f"escaping buffer to faithful .NET (the caller gets "
                                  f"no handle to Return/Free), so returning it is "
                                  f"rejected", ins.line, subject=subj)
-                st.var[id(ins.sym)] = {VarState.ESCAPED}
+                st.var[st.rid_of(ins.sym)] = {VarState.ESCAPED}
             return
 
         assert_never(ins)
@@ -498,7 +548,7 @@ def _apply_effect(self, st: State, sym: Symbol, eff: Effect,
                              f"the PoC code generator cannot lower an escaping "
                              f"buffer, so consuming it in '{callee}' is rejected",
                              line, subject=sym.origin)
-                st.var[id(sym)] = {VarState.ESCAPED}
+                st.var[st.rid_of(sym)] = {VarState.ESCAPED}
             elif eff == Effect.BORROW_MUT:
                 self._check_mut_borrowable(st, sym, line)
             elif eff == Effect.BORROW:

tests/run_tests.py

@@ -1106,6 +1106,12 @@ def run() -> int:
     import test_ownership
     own5_rc = test_ownership.run()
 
+    # RID indirection (P-005 D5.4 step 0): the no-op handle->RID layer the alias
+    # model (step 1) builds on — 1:1 identity, the join invariant, behaviour
+    # unchanged.
+    import test_rid
+    rid_rc = test_rid.run()
+
     # Diagnostic rendering (P-015): the empty-evidence invariant (render()/render_pretty()
     # byte-for-byte unchanged) plus the ordered `note:` slice and the SARIF evidence builders.
     import test_diagnostics
@@ -1115,7 +1121,7 @@ def run() -> int:
                  or escape_fails or branchy_fails or nest_fails
                  or order_fails or helper_fails or cc_rc or pf_rc
                  or gl_rc or co_rc or wpf_rc or lt_rc or loops_rc
-                 or spec_rc or ownir_rc or own5_rc or diag_rc) else 0
+                 or spec_rc or ownir_rc or own5_rc or rid_rc or diag_rc) else 0
 
 
 if __name__ == "__main__":

tests/test_rid.py

@@ -0,0 +1,159 @@
+#!/usr/bin/env python3
+"""
+D5.4 step 0 — the RID (resource-id) indirection layer.
+
+Resource state in the core flow analysis (`ownlang/analysis.py`) now lives on a
+**RID**, an obligation a *handle* (a local/param `Symbol`) denotes through
+`State.handle_rid`. Step 0 is a deliberate *no-op*: every handle maps 1:1 to its
+own RID, keyed by the originating symbol's identity (`RID == id(sym)`), so the
+analysis is byte-for-byte the pre-RID behaviour. The whole green corpus is the
+behaviour-preservation proof; these checks pin the new *layer* directly so D5.4
+step 1 (`alias_join`: a second handle joins an existing RID) builds on a tested
+invariant rather than re-deriving it.
+
+What is locked here:
+  * `rid_of` defaults to `id(sym)` for an un-minted handle (the 1:1 identity).
+  * `mint` records the handle->RID mapping and returns `id(sym)`.
+  * `_join_handle_rid` unions agreeing maps and *asserts* on a conflicting one
+    (the step-0 single-mapping invariant — the analogue of `join`'s loan assert).
+  * end-to-end: a 1:1 acquire still leaks (OWN001) when dropped and stays silent
+    when released — i.e. routing every `var` access through the RID layer changed
+    no observable behaviour.
+
+Run:  python tests/test_rid.py
+      python tests/run_tests.py     (runs it as part of the suite)
+"""
+
+from __future__ import annotations
+
+import os
+import sys
+
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), ".."))
+
+from ownlang.analysis import State, _join_handle_rid, analyze
+from ownlang.cfg import Kind, Symbol, build_cfg, collect_signatures
+from ownlang.diagnostics import Severity
+from ownlang.lexer import LexError
+from ownlang.parser import ParseError, parse
+
+_PRELUDE = (
+    "module Rid\n"
+    "resource Conn { acquire open release close }\n"
+)
+
+
+def _codes(body: str) -> set[str]:
+    """Error codes for one function body (Conn prelude prepended)."""
+    try:
+        mod = parse(_PRELUDE + body)
+    except (ParseError, LexError):
+        return {"OWN020"}
+    rnames = {r.name for r in mod.resources}
+    sigs = collect_signatures(mod)
+    out: set[str] = set()
+    for fn in mod.functions:
+        cfg, d1 = build_cfg(fn, rnames, sigs)
+        d2 = analyze(cfg)
+        out |= {d.code for d in (d1 + d2) if d.severity == Severity.ERROR}
+    return out
+
+
+# Every `_check` call appends its outcome here, so the summary derives its total
+# from the checks that actually ran — it cannot drift out of sync with a hardcoded
+# constant when checks are added or removed.
+_RAN: list[bool] = []
+
+
+def _check(name: str, ok: bool, detail: str = "") -> int:
+    _RAN.append(ok)
+    mark = "ok  " if ok else "FAIL"
+    suffix = f"  ({detail})" if detail and not ok else ""
+    print(f"  {mark} {name}{suffix}")
+    return 0 if ok else 1
+
+
+def run() -> int:
+    print("rid (D5.4 step 0 — RID indirection):")
+    _RAN.clear()
+    fails = 0
+
+    # -- rid_of: an un-minted handle denotes its own resource (1:1 identity) ----
+    st = State()
+    a = Symbol("a", Kind.OWNED, 1)
+    fails += _check("rid_of defaults to id(sym)",
+                    st.rid_of(a) == id(a) and not st.handle_rid,
+                    "un-minted handle should resolve to id(sym) without recording")
+
+    # -- mint: records the mapping, returns id(sym), stays 1:1 -----------------
+    rid = st.mint(a)
+    fails += _check("mint returns id(sym) and records it",
+                    rid == id(a) and st.handle_rid[id(a)] == id(a)
+                    and st.rid_of(a) == id(a))
+
+    b = Symbol("b", Kind.OWNED, 2)
+    fails += _check("distinct handles mint distinct RIDs",
+                    st.mint(b) != rid and st.rid_of(b) != st.rid_of(a),
+                    "1:1 means no two un-aliased handles share a RID")
+
+    # -- copy carries the handle->RID map --------------------------------------
+    st2 = st.copy()
+    fails += _check("copy() preserves handle_rid",
+                    st2.handle_rid == st.handle_rid
+                    and st2.handle_rid is not st.handle_rid)
+
+    # -- _join_handle_rid: agreeing maps union; conflicting maps assert ---------
+    left = {id(a): id(a)}
+    right = {id(b): id(b)}
+    merged = _join_handle_rid(left, right)
+    fails += _check("_join_handle_rid unions disjoint maps",
+                    merged == {id(a): id(a), id(b): id(b)})
+
+    overlap = _join_handle_rid({id(a): id(a)}, {id(a): id(a)})
+    fails += _check("_join_handle_rid keeps an agreeing shared mapping",
+                    overlap == {id(a): id(a)})
+
+    conflicted = False
+    try:
+        # the same handle resolving to two different RIDs violates the step-0
+        # single-mapping invariant — must be loud, not silently merged.
+        _join_handle_rid({id(a): id(a)}, {id(a): id(b)})
+    except AssertionError:
+        conflicted = True
+    fails += _check("_join_handle_rid asserts on a conflicting mapping",
+                    conflicted, "a handle -> two RIDs must raise, not pick a side")
+
+    # -- end-to-end behaviour is unchanged by the indirection ------------------
+    leak = _codes("fn f(){ let c = acquire Conn(1); }")
+    fails += _check("1:1 acquire still leaks (OWN001)",
+                    leak == {"OWN001"}, f"got {leak}")
+
+    clean = _codes("fn f(){ let c = acquire Conn(1); release c; }")
+    fails += _check("1:1 acquire+release stays silent",
+                    clean == set(), f"got {clean}")
+
+    double = _codes("fn f(){ let c = acquire Conn(1); release c; release c; }")
+    fails += _check("1:1 double-release still OWN003",
+                    "OWN003" in double, f"got {double}")
+
+    # Return/escape path: the refactor routes the Return state-write and
+    # leak_check's `exclude` through rid_of, so cover them directly. Returning an
+    # owned resource escapes its RID (clean); a *sibling* RID left owned still
+    # leaks — proving the exclude spares only the returned RID, not all of them.
+    escape = _codes("fn f() -> Conn { let c = acquire Conn(1); return c; }")
+    fails += _check("returning an owned resource escapes clean",
+                    escape == set(), f"got {escape}")
+
+    leak_before_ret = _codes(
+        "fn f() -> Conn { let a = acquire Conn(1); let c = acquire Conn(1); "
+        "return c; }")
+    fails += _check("a sibling RID still leaks before return (OWN001)",
+                    leak_before_ret == {"OWN001"}, f"got {leak_before_ret}")
+
+    n = len(_RAN)
+    print(f"rid: {n - fails}/{n} RID-layer checks pass")
+    return 1 if fails else 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(run())