diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 39b1cbf3..a0bc477d 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -359,13 +359,41 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa C#-extractor table (the bool literal is a per-call-site fact the extractor sees), so it is CI/C#-only, not a pure-Python slice. - **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit - cadence** so the core change is de-risked: **(step 0)** a *no-op identity refactor* — - move resource state from per-binding to per-RID with a 1:1 binding↔RID mapping, behaviour - unchanged, validated against the green D5.0–D5.3 corpus; **(step 1)** add the `alias_join` - lowering; **(step 2)** turn on the extractor branches that emit `aliasOf:i` for *verified* - wrapper / factory / ctor-adopt sites. Result: **Dapper / Polly** modelled explicitly and - added as oracle regression anchors that now resolve *with a recorded reason* (cross-link - `field-notes-patterns.md`). + cadence** so the core change is de-risked. + - **Step 0 — the no-op RID identity refactor (shipped).** Resource state in the core flow + analysis (`analysis.py`) moved from per-binding to per-**RID**: `State.var` is keyed by an + obligation id, and a handle (local/param `Symbol`) denotes a RID through `State.handle_rid`. + The mapping is **1:1** (each `acquire`/owned-param `mint`s its own RID, `RID == id(sym)`), + so the analysis is byte-for-byte the pre-RID behaviour — the whole green corpus is the + proof. `join` merges `handle_rid` and raises (always-on, `-O`-safe) on a conflicting + mapping, locking the single-mapping invariant. Tested directly in `test_rid.py` (rid_of + 1:1 default, mint, the join union/raise, and end-to-end leak/release/double/return-escape + unchanged). + - **Step 1 — the `alias_join` lowering (shipped).** A new core primitive `AliasJoin(handle, + src)` (AST + CFG + `analysis.step`) makes `handle` a **new owning alias of `src`'s RID**: + the two handles denote one obligation, `src` stays owning (unlike `move`). Because state + lives on the RID, the existing per-RID checks now do T4 for free — releasing or escaping + through **either** alias discharges the one resource (clean), a leak of the shared RID is + reported **once**, releasing **both** is OWN003, and using either after release is OWN002. + The OwnIR bridge lowers an `alias_join` flow op (`var` = the new owning handle, `src` = the + adopted local) to it; an `alias_join` over an untracked `src` makes no claim (optimistic- + silent, the v1 must-only rule, §11). **T4a ≡ T4b**: one primitive, two extractor recognisers + (step 2). The **Dapper precision win** is proven — a factory that acquires `inner` locally, + `alias_join`s a wrapper `w`, and **returns `w`** drops `inner` as a local but its obligation + escaped through `w`, so per-RID evaluation reports **no leak** (the own-only-0-with-a-reason + case the model exists for). Tests in `test_ownir.py` (release-wrapper / release-inner clean, + drop-both leaks once, double-release OWN003, use-after-release OWN002, untracked-src silent, + return-wrapper precision). *Limitation (deferred):* `alias_join` is straight-line only — an + alias minted inside one branch of an `if` that merges with a non-aliasing path is out of v1 + scope (the bridge emits it straight-line at the wrapper site); the conflicting-merge raise + in `_join_handle_rid` keeps that loud rather than silently wrong. + - **Step 2 — extractor emission (next).** Turn on the Roslyn recogniser branches that emit + the `alias_join` flow op for *verified* wrapper / factory / ctor-adopt sites: **(a)** the arg + is forwarded to an `aliasOf` position and the method returns that call's result, or **(b)** + the arg is stored into a single owning field whose `Dispose()` releases it (§11). Result: + **Dapper / Polly** (`BulkheadSemaphoreFactory` → owning fields) modelled explicitly and added + as oracle regression anchors that resolve *with a recorded reason* (cross-link + `field-notes-patterns.md`). - **D5.5 — Tier C annotations** (`[OwnTransfers]` / `[MustCallAlias]` + external file). - **D5.x — advisory** `OWN051` for `may`/`unknown`, and the strict/pessimistic mode. diff --git a/ownlang/analysis.py b/ownlang/analysis.py index f457fd11..d6f5b09a 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -51,6 +51,7 @@ CFG, Acquire, AcquireBuffer, + AliasJoin, Block, BorrowEnd, BorrowStart, @@ -82,7 +83,8 @@ class LoanKind(Enum): @dataclass(frozen=True) class Loan: loan_id: int # we use id(binding_symbol): unique per borrow scope - owner: int # id(owner_symbol) + owner: int # the owner's RID (rid_of(owner)) — so the loan is seen + # through every owning alias of the borrowed resource binding: int # id(binding_symbol) kind: LoanKind @@ -194,10 +196,16 @@ def err(self, code: str, msg: str, line: int, # -- loan / permission helpers ----------------------------------------- def loans_on(self, st: State, owner: Symbol) -> tuple[int, bool]: + # A loan's owner is recorded by RID (see BorrowStart), so a borrow of one + # owning alias is seen through ALL aliases of the same resource: releasing + # or using a different owning handle of a borrowed resource is still caught + # (OWN008 / OWN013). In the 1:1 case `rid_of` is identity, so this is the + # pre-alias behaviour exactly. (Codex P2 — alias loans follow the RID.) + owner_rid = st.rid_of(owner) shared = 0 mut = False for ln in st.loans.values(): - if ln.owner == id(owner): + if ln.owner == owner_rid: if ln.kind == LoanKind.SHARED: shared += 1 else: @@ -351,7 +359,7 @@ def _sym_by_id(self, symid: int) -> Symbol | None: idx[id(p)] = p for b in self.cfg.blocks: for ins in b.instrs: - for attr in ("sym", "dst", "src", "owner", "binding"): + for attr in ("sym", "dst", "src", "owner", "binding", "handle"): s = getattr(ins, attr, None) if isinstance(s, Symbol): idx[id(s)] = s @@ -385,6 +393,18 @@ def step(self, ins: Instr, st: State) -> None: st.var[st.mint(ins.dst)] = {VarState.OWNED} return + if isinstance(ins, AliasJoin): + # `handle` joins `src`'s resource obligation: it becomes an owning + # alias of the SAME RID (no new resource is minted). State lives on the + # RID, so the per-RID checks already do the right thing — releasing or + # escaping through either handle discharges the one obligation, a second + # release is OWN003, and a leak of the shared RID is reported once. We do + # NOT touch `src`'s state (it stays owning, unlike a move). If `src` was + # already released/escaped, point at its RID anyway so a later use/release + # of `handle` resolves to that (released) RID and reports correctly. + st.handle_rid[id(ins.handle)] = st.rid_of(ins.src) + return + if isinstance(ins, Release): subj = ins.sym.origin rkind = ins.sym.resource_kind @@ -446,8 +466,11 @@ def step(self, ins: Instr, st: State) -> None: else: self._check_shared_borrowable(st, ins.owner, ins.line) kind = LoanKind.SHARED + # Record the owner by RID so the loan is visible through every owning + # alias of the resource (Codex P2). `loan_id`/`binding` stay keyed by the + # binding handle (the borrow binding is its own handle, never aliased). st.loans[id(ins.binding)] = Loan( - loan_id=id(ins.binding), owner=id(ins.owner), + loan_id=id(ins.binding), owner=st.rid_of(ins.owner), binding=id(ins.binding), kind=kind) return diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index f3006e1a..a585c8de 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -132,6 +132,21 @@ class Call: line: int +@dataclass(frozen=True) +class AliasJoin: + """`name` is a *new owning handle* on the SAME resource obligation as `src` + (a resource-alias / RLC's `@MustCallAlias`). Releasing or escaping either + handle discharges the one underlying resource; releasing both is a double- + release; using either after the resource is released is a use-after-release. + The T4 wrap/adopt primitive (P-005 D5.4): a factory returning a wrapper of + `src`, or a constructor adopting `src` into an owning field, both reduce to + the same fact — a new owning handle joined `src`'s alias set (T4a ≡ T4b). + Unlike `move`, `src` stays owning (it is not invalidated).""" + name: str # the new owning handle that joins the alias set + src: str # an existing handle whose resource obligation `name` shares + line: int + + @dataclass(frozen=True) class BorrowBlock: owner: str @@ -176,8 +191,8 @@ class Subscribe: line: int -Stmt = (Let | Release | Use | Overspan | Call | BorrowBlock | If | While - | Return | Subscribe) +Stmt = (Let | Release | Use | Overspan | Call | AliasJoin | BorrowBlock | If + | While | Return | Subscribe) # ---- top level ------------------------------------------------------------ diff --git a/ownlang/cfg.py b/ownlang/cfg.py index ad38e160..df004b76 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -151,6 +151,17 @@ class BorrowEnd: line: int +@dataclass +class AliasJoin: + """`handle` becomes a new owning alias of `src`'s resource obligation (its + RID): the two handles denote one underlying resource. Releasing/escaping + either discharges it; releasing both is a double-release. The T4 wrap/adopt + primitive (P-005 D5.4). `src` is NOT invalidated (unlike `MoveInto`).""" + handle: Symbol + src: Symbol + line: int + + @dataclass class Return: sym: Symbol | None @@ -158,7 +169,7 @@ class Return: Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Overspan | Invoke - | BorrowStart | BorrowEnd | Return) + | BorrowStart | BorrowEnd | AliasJoin | Return) # --------------------------------------------------------------------------- @@ -354,6 +365,8 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: return cur if isinstance(st, A.Call): return self.lower_call(st, cur) + if isinstance(st, A.AliasJoin): + return self.lower_alias_join(st, cur) if isinstance(st, A.BorrowBlock): return self.lower_borrow(st, cur) if isinstance(st, A.If): @@ -424,6 +437,28 @@ def lower_let(self, st: A.Let, cur: Block) -> Block: return cur assert_never(rhs) + def lower_alias_join(self, st: A.AliasJoin, cur: Block) -> Block: + """`name` joins `src`'s resource obligation as a new owning alias. `src` + must be an owned resource; `name` is a fresh owning handle that shares + `src`'s RID (and inherits its origin/type/kind so a per-RID finding + attributes to the one underlying resource). Unlike `move`, `src` stays + owning.""" + src = self.lookup(st.src, st.line) + if src is not None and src.kind != Kind.OWNED: + self.diags.append(Diagnostic( + "OWN034", + f"cannot alias '{st.src}': it is not an owned resource " + f"({src.kind.name.lower()})", st.line)) + src = None + handle = self.declare(st.name, Kind.OWNED, st.line) + if src is not None: + handle.origin = src.origin + handle.type_name = src.type_name + handle.resource_kind = src.resource_kind + handle.buffer = src.buffer + cur.instrs.append(AliasJoin(handle, src, st.line)) + return cur + def lower_buffer(self, st: A.Let, rhs: A.BufferIntent, cur: Block) -> Block: if rhs.ns != "Buffer": self.diags.append(Diagnostic( diff --git a/ownlang/codegen.py b/ownlang/codegen.py index 4fbf7581..722727ba 100644 --- a/ownlang/codegen.py +++ b/ownlang/codegen.py @@ -450,6 +450,22 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: f"// full-length view over the pooled tail (over-read)"] if isinstance(st, A.Call): return [f"{ind}{st.callee}({', '.join(self._arg(a) for a in st.args)});"] + if isinstance(st, A.AliasJoin): + # a (re)declaration of this name shadows any stale buffer bookkeeping from + # an earlier same-named buffer, exactly as the Let branch does — else a later + # `release {st.name}` could emit that stale cleanup (CodeRabbit). + self.buffer_cleanup.pop(st.name, None) + self.buffer_vars.pop(st.name, None) + # `name` is an owning alias of `src` (they share one obligation). Carry + # the resource/buffer bookkeeping across so a later release of either + # emits the right cleanup; `src` stays valid (no move-out comment). + if st.src in self.buffer_cleanup: + self.buffer_cleanup[st.name] = self.buffer_cleanup[st.src] + if st.src in self.buffer_vars: + self.buffer_vars[st.name] = self.buffer_vars[st.src] + self.owned_resource[st.name] = self.owned_resource.get(st.src, "") + return [f"{ind}var {st.name} = {st.src}; " + f"// owning alias of {st.src} (shared obligation)"] if isinstance(st, A.BorrowBlock): kind = "mutable" if st.kind == A.BorrowKind.MUT else "shared" rt = self.owned_resource.get(st.owner, "") diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 0b5fe3c5..3b17d0f9 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -105,6 +105,7 @@ from .ast_nodes import ( Acquire, + AliasJoin, Call, Effect, EffectParam, @@ -1539,6 +1540,33 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # partial-path leak reads as a "pooled buffer", not "disposable". "pool": n.get("kind") == "pool"} body.append(Let(handle, Acquire("Disposable", [], line), line)) + elif op == "alias_join": + # P-005 D5.4 (T4 wrap/adopt): `var` is a new owning handle on the SAME + # resource obligation as `src` — a factory returning a wrapper of `src`, + # or a ctor adopting `src` into an owning field (T4a ≡ T4b). The result + # joins `src`'s alias set: dropping the wrapper while `src` is released is + # NOT a leak, releasing both is OWN003, using either after release is + # OWN002 — all evaluated per-RID by the core. Emitted only when `src` is a + # tracked local; an unknown `src` makes no claim (precision-first). + name = str(n.get("var", "?")) + src_h = localmap.get(str(n.get("src", ""))) + # Overwriting a tracked local KILLS its previous ownership binding — the + # same rule as a call-result overwrite (D5.2). Drop the stale mapping FIRST, + # even when the new alias's `src` is untracked: we make no claim on the new + # handle, but the OLD obligation must not be silently discharged by a later + # `release name` resolving to the dead handle (Codex P2). It leaks instead. + # A hoisted local keeps its single outer-scope handle (declared once). + if name not in hoisted: + localmap.pop(name, None) + if src_h is not None and name not in hoisted: + handle = f"loc_{loc[0]}" + loc[0] += 1 + localmap[name] = handle + handles[handle] = {"file": ffile, "line": line, "event": name, + "component": fname, "resource": "flow-local", + "ever_released": name in released_vars, + "pool": False} + body.append(AliasJoin(handle, src_h, line)) elif op == "use": h = localmap.get(str(n.get("var"))) if h is not None: diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 158746a5..7e5eb2b9 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1806,6 +1806,115 @@ def _bcl(body: list) -> list: if gotpl != [("OWN001", "pooled buffer")]: fails.append("bridge branch-scope: a hoisted ArrayPool rent that leaks must stay tagged " f"kind='pooled buffer' (kind preserved through the hoist), got {gotpl}") + # --- P-005 D5.4 (T4 wrap/adopt): the `alias_join` flow op. `var w` becomes a NEW + # owning handle on the SAME resource obligation as `src` (a factory returning a + # wrapper of `src`, or a ctor adopting `src` into an owning field — T4a ≡ T4b). + # Errors are evaluated per-RID, so disposing EITHER alias discharges the one + # resource and disposing BOTH is a double-dispose. This is the Dapper/Polly + # wrapper-adoption shape modelled explicitly. (The extractor recognisers that + # EMIT this op land in D5.4 step 2; here the op is driven by synthetic facts.) + # + # disposing the wrapper alone discharges the obligation for both -> clean. + checks += 1 + aw = check_facts({"module": "M", "functions": [ + {"name": "adopt_release_wrapper", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}, + {"op": "release", "var": "w", "line": 3}]}]}) + if aw: + fails.append("D5.4 T4: releasing the wrapper alias must discharge the shared " + f"obligation (clean), got {[(x.component, x.code) for x in aw]}") + # disposing the inner directly (the Dapper dispose-the-inner path) is ALSO clean — + # the alias set is satisfied through any member. + checks += 1 + ai = check_facts({"module": "M", "functions": [ + {"name": "adopt_release_inner", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}, + {"op": "release", "var": "inner", "line": 3}]}]}) + if ai: + fails.append("D5.4 T4: releasing the inner directly must also discharge the shared " + f"obligation (clean), got {[(x.component, x.code) for x in ai]}") + # dropping BOTH (neither released) leaks the ONE underlying resource exactly ONCE, + # not once per alias — per-RID leak evaluation. + checks += 1 + al = check_facts({"module": "M", "functions": [ + {"name": "adopt_leak", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}]}]}) + gotal = [(x.component, x.line, x.code) for x in al] + if gotal != [("adopt_leak", 1, "OWN001")]: + fails.append("D5.4 T4: dropping both aliases must leak the shared resource ONCE " + f"(OWN001@1, attributed to the inner), got {gotal}") + # releasing BOTH aliases is a double-dispose (OWN003) — the second release hits an + # already-Released RID through the other handle. + checks += 1 + ad = check_facts({"module": "M", "functions": [ + {"name": "adopt_double", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}, + {"op": "release", "var": "inner", "line": 3}, + {"op": "release", "var": "w", "line": 4}]}]}) + # the finding anchors at the shared resource's origin (the `inner` acquire, line 1) — + # the bridge remaps every flow-local diagnostic back to its acquire site, as the D5.2 + # use-after case does; the flow slice carries the release path. + gotad = [(x.line, x.code) for x in ad] + if gotad != [(1, "OWN003")]: + fails.append("D5.4 T4: releasing both aliases must be a double-dispose (OWN003, " + f"anchored at the inner acquire @1), got {gotad}") + # using an alias after the resource was released (through the OTHER handle) is a + # use-after-release (OWN002). + checks += 1 + au = check_facts({"module": "M", "functions": [ + {"name": "adopt_uar", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}, + {"op": "release", "var": "w", "line": 3}, + {"op": "use", "var": "inner", "line": 4}]}]}) + gotau = [(x.line, x.code) for x in au] + if gotau != [(1, "OWN002")]: + fails.append("D5.4 T4: using an alias after release through the other handle must be " + f"OWN002 (anchored at the inner acquire @1), got {gotau}") + # PRECISION: an `alias_join` whose `src` is NOT a tracked local makes NO claim — no + # acquire is fabricated for the wrapper, so a later release of it is silently dropped + # (never a phantom OWN003/OWN002). Optimistic-silent, per the v1 must-only rule. + checks += 1 + an = check_facts({"module": "M", "functions": [ + {"name": "adopt_unknown_src", "file": "T4.cs", + "body": [{"op": "alias_join", "var": "w", "src": "ghost", "line": 2}, + {"op": "release", "var": "w", "line": 3}]}]}) + if an: + fails.append("D5.4 T4: an alias_join over an untracked src must make no claim " + f"(silent), got {[(x.component, x.code) for x in an]}") + # THE PRECISION WIN (§11 Dapper shape): a factory acquires `inner` as a LOCAL, wraps it + # (`w` aliases inner), and RETURNS the wrapper. `inner` is dropped as a local, but its + # obligation escaped through `w` — so per-RID leak evaluation sees the shared RID escape + # and reports NO leak. Without the alias set this dropped local would be a false OWN001; + # this is the own-only-0-with-a-reason case the whole D5.4 model exists to model. + checks += 1 + rw = check_facts({"module": "M", "functions": [ + {"name": "Wrap.Create", "file": "T4.cs", + "body": [{"op": "acquire", "var": "inner", "line": 1}, + {"op": "alias_join", "var": "w", "src": "inner", "line": 2}, + {"op": "return", "var": "w", "line": 3}]}]}) + if rw: + gotrw = [(x.component, x.code) for x in rw] + fails.append("D5.4 T4: returning the wrapper escapes the shared obligation, so the " + f"dropped inner local must NOT leak, got {gotrw}") + # OVERWRITE kills the prior binding even when the new alias is UNTRACKED (Codex P2): + # `acquire w; alias_join w <- ghost; release w` overwrites `w` with an alias whose src + # is not tracked. The original `w` obligation is lost (it leaks OWN001@1); the later + # `release w` must NOT resolve to the dead handle and silently discharge it. + checks += 1 + aov = check_facts({"module": "M", "functions": [ + {"name": "C.M", "file": "T4.cs", + "body": [{"op": "acquire", "var": "w", "line": 1}, + {"op": "alias_join", "var": "w", "src": "ghost", "line": 2}, + {"op": "release", "var": "w", "line": 3}]}]}) + gotaov = [(x.line, x.code) for x in aov] + if gotaov != [(1, "OWN001")]: + fails.append("D5.4 T4: an alias_join overwriting an owned local with an UNTRACKED src " + f"must leak the original (OWN001@1), not read clean, got {gotaov}") # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; # the buffer is still returned, so there is no OWN001 leak. Routes through the diff --git a/tests/test_rid.py b/tests/test_rid.py index 7977dc77..3e5e437e 100644 --- a/tests/test_rid.py +++ b/tests/test_rid.py @@ -32,7 +32,21 @@ 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.cfg import ( + CFG, + Acquire, + AliasJoin, + Block, + BorrowEnd, + BorrowStart, + Instr, + Kind, + Release, + Symbol, + Use, + build_cfg, + collect_signatures, +) from ownlang.diagnostics import Severity from ownlang.lexer import LexError from ownlang.parser import ParseError, parse @@ -150,6 +164,32 @@ def run() -> int: fails += _check("a sibling RID still leaks before return (OWN001)", leak_before_ret == {"OWN001"}, f"got {leak_before_ret}") + # -- alias loans follow the shared RID (Codex P2) -------------------------- + # The OwnIR bridge has no borrow op, so the alias<->loan interaction is checked + # directly on a CFG: an owning alias of a borrowed resource is still subject to + # the loan, so releasing/using it through the OTHER handle is caught. + def _cfg_codes(instrs: list[Instr]) -> set[tuple[int, str]]: + cfg = CFG("f", [Block(id=0, instrs=instrs, succ=[])], 0, [], False) + return {(d.line, d.code) for d in analyze(cfg)} + + inner = Symbol("inner", Kind.OWNED, 1) + w = Symbol("w", Kind.OWNED, 2) + b = Symbol("b", Kind.BORROW, 3) + # releasing an owning alias while the resource is borrowed through the other + # handle is OWN008 — the loan owner resolves through the shared RID. + rel_borrowed = _cfg_codes([ + Acquire(inner, "R", 1), AliasJoin(w, inner, 2), + BorrowStart(inner, b, False, 3), Release(w, 4), BorrowEnd(inner, b, False, 5)]) + fails += _check("releasing an owning alias of a borrowed RID is OWN008", + rel_borrowed == {(4, "OWN008")}, f"got {rel_borrowed}") + # using an owning alias while the resource is mutably borrowed is OWN013. + use_mutborrowed = _cfg_codes([ + Acquire(inner, "R", 1), AliasJoin(w, inner, 2), + BorrowStart(inner, b, True, 3), Use(w, 4), BorrowEnd(inner, b, True, 5), + Release(inner, 6)]) + fails += _check("using an owning alias of a mut-borrowed RID is OWN013", + use_mutborrowed == {(4, "OWN013")}, f"got {use_mutborrowed}") + n = len(_RAN) print(f"rid: {n - fails}/{n} RID-layer checks pass") return 1 if fails else 0