@@ -0,0 +1,38 @@
+// resource-effects Stage 3 inference suite (pre-registered in Own.NET-paperwork
+// paper-eval/resource-effects/stage3-inference-prereg-v1.json, tests T01-T14). One class per test; the
+// expected summaries live in the prereg and the measured ones in stage3-inference-v1.json.
+using System;
+
+sealed class R : IDisposable { public bool IsOpen => true; public void Touch() { } public void Dispose() { } }
+
+sealed class Conn : IDisposable
+{
+    public void Kill() { Dispose(); }
+    public void Touch() { }
+    public void Dispose() { }
+}
+
+interface IFactory { R Make(); }
+interface IKill { void Kill(); }
+
+static class T01 { public static R Make() { var r = new R(); return r; } }
+static class T02 { public static R Make2() { return T01.Make(); } public static R Make3() { return new R(); } }
+static class T03 { public static R Outer() => T02.Make2(); }
+static class T04 { static void Run() { var c = new Conn(); c.Kill(); } static void RunUse() { var c = new Conn(); c.Kill(); c.Touch(); } }
+static class T05 { public static void Drop(Conn c) { c.Kill(); } static void Run() { var c = new Conn(); Drop(c); } }
+static class T06 { public static void Finish(R r, bool b) { if (b) { r.Dispose(); } } }
+static class T07 { public static void Finish(R r, bool keep) { if (!keep) { r.Dispose(); } } }
+static class T08 { public static R Make7(bool b) { if (b) { return new R(); } return T01.Make(); } static void Drop(bool b) { var a = Make7(b); a.Touch(); } }
+static class T09 { public static void Finish(R r) { r.Dispose(); } public static void Fwd(R r) { Finish(r); } }
+static class T10 { public static void Use(R r) { r.Touch(); } }
+static class T11 { public static R Id(R x) => x; static void Run() { var r = new R(); var s = Id(r); s.Dispose(); } }
+static class T11B { public static R Id(R x) { return x; } static void Run() { var r = new R(); var s = Id(r); s.Dispose(); } static void RunBoth() { var r = new R(); var s = Id(r); s.Dispose(); r.Dispose(); } }
+static class T12 { public static R A(bool b) => b ? new R() : B(); public static R B() => A(false); static void Drop() { var a = A(true); a.Touch(); } }
+static class T13 { public static R Ext() => Unknown.Get(); static void Drop() { var a = Ext(); a.Touch(); } }
+static class T14
+{
+    public static R Via(IFactory f) => f.Make();
+    public static void ViaKill(IKill k) { k.Kill(); }
+    static void Drop(IFactory f) { var a = Via(f); a.Touch(); }
+    static void Run(IFactory f, IKill k) { var r = new R(); ViaKill(k); r.Touch(); }
+}
@@ -0,0 +1,51 @@
+# resource-effects Stage 3 — first-party summary inference over the algebra (EXPLORATORY)
+
+Research branch `research/resource-effects-v1`. Pre-registered in Own.NET-paperwork
+`paper-eval/resource-effects/stage3-inference-prereg-v1.json`; evidence in `stage3-inference-v1.json`.
+#304 frozen and unchanged; #382 untouched; nothing here is a production result.
+
+## 1. E3 — the one engine rule (both engines, opt-in `OWEN_RE_MIXED_RETURN=1`, verdict-identical off)
+
+INF-R3′: a MIXED return skeleton — every returned local acquired in this body on some paths and bound to
+ONE first-party callee's result on the others (`if (b) return new R(); return Make();`) — is a forward to
+that callee, fresh iff the callee is fresh at the fixpoint. Two different callees stay ambiguous (`none`);
+a returned parameter is never fresh. Python `_infer_return_skeleton` (+17 lines) and the Rust bridge
+`infer_return_skeleton` (+33) carry the same block; off the opt-in the R3/R4 separation is unchanged.
+
+## 2. The 14-test suite (`corpus/re-inference/t-suite.cs`): 13 of 14 met, Python == Rust in every arm
+
+| test | expected | measured (body + E3) |
+|---|---|---|
+| T01 direct factory | fresh | fresh |
+| T02 wrapper (`return Make()`, `return new R()`) | fresh / fresh | fresh / fresh |
+| T03 two-level (`=> Make2()`) | fresh | fresh |
+| T04 receiver release (`c.Kill()`) | Run clean, RunUse OWN002 | as expected |
+| T05 release wrapper (`Drop(c) { c.Kill(); }`) | c must | c must |
+| T06 conditional / T07 negated guard | r may | r may / r may |
+| T08 ambiguous branch (mixed) | fresh (none today) | none without E3, **fresh with E3**; the caller's leak appears |
+| T09 forwarded ownership | r must | r must |
+| T10 borrowed param | r no | r no |
+| T11 returned param (`=> x`, `{ return x; }`) | never fresh | no record / `none` |
+| T12 recursive / SCC (`A => b ? new R() : B(); B => A(false)`) | fresh (fixpoint) | **unknown**: INF-F5 resolves a forward-return CYCLE to `unknown` (fail-closed) — the expectation assumed an optimistic cycle policy the engine does not have; NOT MET, recorded, not repaired |
+| T13 unresolved external | never fresh | no record; the caller is silent |
+| T14 virtual / interface | never fresh; never a release | `unknown`; no release |
+
+## 3. Fact-level mutants (each applied to the extracted facts; each MUST fail its target)
+
+- **M3 ignore a branch** — fails as required: T06/T07 become a fabricated `must`, T12 becomes `fresh`, a new
+  finding appears.
+- **M5 ignore overload identity** — fails as required on the P-037-X control x2b-c3: both callers degrade to
+  OWN051 and the guarded selection is lost.
+- **M7 ignore virtual/interface** — fails as required: `Via` becomes fresh and its caller gets a false OWN001.
+- **M4 ignore return aliasing** — NOT APPLICABLE at the fact level: the frontend never emits
+  `return <parameter>` (the return is a bare exit) and the engine claims `fresh` only for a local it saw
+  acquired, so the mutant cannot be expressed without fabricating an acquire. The aliasing rule holds by
+  construction; the mutant is retired and the reason recorded.
+
+## 4. Reading
+
+The intra-body effects the algebra names are inferred as pre-registered. The additions of this track so
+far are E1 (+ expression bodies), E2 and E3: no OwnIR field, no lattice value, one skeleton-derivation rule.
+The two departures are policy, not effect failures (the fail-closed cycle rule; aliasing by construction).
+Stage 4 now asks where the two EXTERNAL effects of the frozen witnesses can come from — the dependency
+source through exactly these rules, or the explicit two-row model.
@@ -1681,6 +1681,12 @@ def visit(ns: Any) -> None:
     return out
 
 
+
+def _re_mixed_return_enabled() -> bool:
+    """resource-effects Stage 3 E3 opt-in (EXPLORATORY; research branch only, never a default)."""
+    import os
+    return os.environ.get("OWEN_RE_MIXED_RETURN") == "1"
+
 def _infer_return_skeleton(nodes: Any, param_names: set[str],
                            first_party: frozenset[str] = frozenset(),
                            call_key: Callable[[str, str | None], str] | None = None,
@@ -1717,6 +1723,26 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str],
     if all(v in acquired and v not in param_names and v not in call_results
            for v in returned):
         return ReturnSkeleton("fresh")
+    # resource-effects Stage 3 E3 (research/resource-effects-v1, EXPLORATORY; pre-registered in
+    # Own.NET-paperwork stage3-inference-prereg-v1.json; opt-in OWEN_RE_MIXED_RETURN=1):
+    # INF-R3prime — a MIXED skeleton whose every returned local is acquired here on some
+    # paths and bound to ONE first-party callee's result on the others (`if (b) return new R();
+    # return Make();`) is a forward to that callee: fresh iff the callee is fresh at the
+    # fixpoint. Two different callees stay ambiguous (none); a returned parameter is never
+    # fresh. Off the opt-in the R3/R4 separation above is unchanged.
+    if _re_mixed_return_enabled() and returned and all(
+            v not in param_names and (v in acquired or call_results.get(v) is not None)
+            for v in returned):
+        entries = {call_results[v] for v in returned if call_results.get(v) is not None}
+        if entries and len({e[0] for e in entries}) == 1:
+            callee = next(iter(entries))[0]
+            sigs = {e[1] for e in entries}
+            csig = next(iter(sigs)) if len(sigs) == 1 else None
+            if _canonical_callee_name(callee) not in first_party \
+                    and _is_bcl_fresh_factory(callee):
+                return ReturnSkeleton("fresh")
+            return ReturnSkeleton(
+                "forward", callee=call_key(callee, csig) if call_key else callee)
     if len(returned) == 1:
         (v,) = tuple(returned)
         entry = call_results.get(v)
 
@@ -654,6 +654,40 @@ fn infer_return_skeleton(
     {
         return ReturnSkeleton::Fresh;
     }
+    // resource-effects Stage 3 E3 (EXPLORATORY; opt-in `OWEN_RE_MIXED_RETURN=1`; see the Python
+    // twin `_infer_return_skeleton`): a mixed skeleton — every returned local acquired here on
+    // some paths and bound to ONE first-party callee's result on the others — is a forward to
+    // that callee (fresh iff the callee is fresh at the fixpoint). Two callees stay ambiguous.
+    if re_mixed_return_enabled()
+        && returned.iter().all(|v| {
+            !param_names.contains(v)
+                && (acquired.contains(v) || matches!(call_results.get(v), Some(Some(_))))
+        })
+    {
+        let entries: Vec<&CallOrigin> = returned
+            .iter()
+            .filter_map(|v| call_results.get(v))
+            .filter(|e| e.is_some())
+            .collect();
+        let callees: HashSet<&str> = entries
+            .iter()
+            .filter_map(|e| e.as_ref().map(|(c, _)| c.as_str()))
+            .collect();
+        if callees.len() == 1 {
+            let callee = *callees.iter().next().expect("len == 1");
+            let sigs: HashSet<Option<&str>> = entries
+                .iter()
+                .filter_map(|e| e.as_ref().map(|(_, s)| s.as_deref()))
+                .collect();
+            let csig = if sigs.len() == 1 { *sigs.iter().next().expect("len == 1") } else { None };
+            if !first_party.contains(canonical(callee)) && is_bcl_fresh_factory(callee) {
+                return ReturnSkeleton::Fresh;
+            }
+            return ReturnSkeleton::Forward {
+                callee: call_key(callee, csig),
+            };
+        }
+    }
     if returned.len() == 1 {
         let v = returned.iter().next().expect("len == 1");
         if let Some(Some((callee, csig))) = call_results.get(v) {
@@ -1495,6 +1529,11 @@ fn p037x_guarded_enabled() -> bool {
     std::env::var_os("OWEN_P037X_GUARDED").is_some_and(|v| v == "1")
 }
 
+/// resource-effects Stage 3 E3 opt-in: `OWEN_RE_MIXED_RETURN=1` (EXPLORATORY; never a default).
+fn re_mixed_return_enabled() -> bool {
+    std::env::var_os("OWEN_RE_MIXED_RETURN").is_some_and(|v| v == "1")
+}
+
 fn p037x_guarded_doc(facts: &OwnIr) -> Option<own_guarded::GuardedDoc> {
     p037x_guarded_enabled().then(|| own_guarded::GuardedDoc::solve(facts))
 }
 
@@ -83,6 +83,14 @@
     "s08b-caller": ["OWN001", "OWN001", "OWN001"],
 }
 _SHAPES = os.path.join("corpus", "re-cfg-probe")
+# Stage 3: the inference suite (corpus/re-inference/t-suite.cs) verdict codes under the body arm and
+# under the body arm with the engine rule E3 (OWEN_RE_MIXED_RETURN=1: T08 Make7's caller leaks);
+# the summaries are recorded in paper-eval/resource-effects/stage3-inference-v1.json
+_RECORD_3: dict[str, list[str]] = {
+    "body": ["OWN001", "OWN002"],
+    "body+E3": ["OWN001", "OWN001", "OWN002"],
+}
+_SUITE = os.path.join("corpus", "re-inference")
 
 
 def _codes(text: str) -> list[str]:
@@ -96,8 +104,9 @@ def _run(argv: list[str], env: dict[str, str]) -> str:
 
 def _check(name: str, arm: str, want: list[str], ext_env: dict[str, str], tmp: str,
            rust: str | None, env: dict[str, str], fails: list[str],
-           folder: str = _CONTROLS) -> None:
+           folder: str = _CONTROLS, eng_env: dict[str, str] | None = None) -> None:
     src = os.path.join(folder, f"{name}.cs")
+    env = {**env, **(eng_env or {})}
     facts = os.path.join(tmp, f"{name}.{arm}.json")
     try:
         subprocess.run(["dotnet", "run", "--project", _EXT, "--", "--flow-locals", src,
@@ -127,7 +136,7 @@ def run() -> int:
     if rust and not os.path.isfile(rust):
         rust = None
     env = {**os.environ, "PYTHONPATH": _REPO}
-    for k in ("OWEN_RE_ORACLE", "OWEN_RE_MINTED_RETURN", "OWEN_RE_BODY"):
+    for k in ("OWEN_RE_ORACLE", "OWEN_RE_MINTED_RETURN", "OWEN_RE_BODY", "OWEN_RE_MIXED_RETURN"):
         env.pop(k, None)
         os.environ.pop(k, None)
     key = os.path.join(_REPO, _KEYS, "answer-key.json")
@@ -152,10 +161,14 @@ def run() -> int:
         for name, want in sorted(_RECORD_2.items()):
             _check(name, "body", want, {"OWEN_RE_MINTED_RETURN": "1", "OWEN_RE_BODY": "1"}, tmp,
                    rust, env, fails, folder=_SHAPES)
+        for arm, want in sorted(_RECORD_3.items()):
+            _check("t-suite", arm, want, {"OWEN_RE_MINTED_RETURN": "1", "OWEN_RE_BODY": "1"}, tmp,
+                   rust, env, fails, folder=_SUITE,
+                   eng_env={"OWEN_RE_MIXED_RETURN": "1"} if arm == "body+E3" else None)
     for f in fails:
         print(f"FAIL: {f}")
     n = (sum(len(a) for a in _RECORD.values()) + len(_OBSERVATION)
-         + sum(len(a) for a in _RECORD_1B.values()) + len(_RECORD_2))
+         + sum(len(a) for a in _RECORD_1B.values()) + len(_RECORD_2) + len(_RECORD_3))
     print(f"re controls: {n} row(s), {len(fails)} failed"
           + ("" if rust else " (Rust parity not checked: OWEN_RUST_CORE unset)"))
     return 1 if fails else 0