Skip to content

docs(evidence): N1-F0 — KILL-N1 at F0-B (may-throw model, not ownership) #418

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
PhysShell merged 3 commits into from
Oct 20, 2026
Merged

docs(evidence): N1-F0 — KILL-N1 at F0-B (may-throw model, not ownership) #418

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
66731cc
docs(evidence): N1-F0 pre-registration and oracle controls
PhysShell Oct 20, 2026
081b68e
docs(evidence): N1-F0 oracle frozen before the real-file run; F0-A co…
PhysShell Oct 20, 2026
ac094bd
docs(evidence): N1-F0 — KILL-N1 at F0-B (may-throw model, not ownership)
PhysShell Oct 20, 2026
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
117 changes: 117 additions & 0 deletions docs/evidence/n1-f0-2026-10/00-preregistration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
# N1-F0 — ownership feasibility gate — pre-registration

Written 2026-10-20, 21:51 +05, before any F0 run. Authority: owner decision
`ACCEPT-N1-COMPETITOR-GATE / GO-N1-OWNERSHIP-FEASIBILITY / NO-PRODUCTION`, on #417.

- **Budget.** 0.25 agent-day for F0-A, F0-B and F0-C together.
- **Outcome.** One verdict, `PASS-F0` or `KILL-N1`. `PASS-F0` does not authorise production work or a PoC.
- **Rules of the work.** No production, OwnIR, CI or golden change. No third-party build and no package download (D13).

## F0-A — finish the competitor check

**Run.** The four reproductions of #417 (`n1-competitor-gate-2026-10/repro`, stubs as a separate assembly), under:

| K | CA2000 settings |
|---|---|
| A1 | `AllPaths`, `interprocedural_analysis_kind = None` |
| A2 | `AllPaths`, `NonContextSensitive` |
| A3 | `AllPaths`, `ContextSensitive` |
| A4–A6 | A1–A3 plus `dispose_ownership_transfer_at_constructor = true` and `…_at_method_call = true` |

plus K1–K5 of #417 again, so that every configuration uses the new collector.

**Collector.** Every diagnostic whose location is inside the buggy **method** of each pair, from the first line of
its declaration to its closing brace, not only on the `ACQ` line. A diagnostic is **disposal-related** if its rule
is one of the following, or its message contains `dispos` (case-insensitive):

- CA2000, CA1001, CA2213, CA2215, CA2216;
- IDISP001–IDISP026;
- S2930, S2931, S3966, S4487.

**Verdict per pair.**

- **`CAUGHT`:** at least one disposal-related diagnostic in the buggy method names the leaked resource (its
acquisition expression or its variable) in any configuration.
- **`ADJACENT`:** disposal-related diagnostics that name another object. They are listed and do not count.
- **`MISSED`:** otherwise.

**F0-A kill.** Fewer than 2 pairs `MISSED` → `KILL-N1`. The other parts are then not scored.

## F0-B — ownership oracle

**Oracle (fixed now).** A call result `r` acquired in method `M` of type `T` is **owned by `M`** only when all of
the following hold:

1. **Hand-over target.** On the success path, `M` hands `r` to one of:
- (a) an instance field `f` of `T`;
- (b) an element of a collection field `f` of `T` (indexer store, `Add`, `TryAdd`);
- (c) a constructor argument of an in-source type `W` whose constructor stores it in a field `g` of `W`, where
the `W` instance is returned or stored as in (a)/(b).
2. **The repository itself disposes that target.** The same type (`T`, or `W` for (c)) contains a
`Dispose`/`DisposeAsync`/`Close`/`CloseAsync` call whose receiver is:
- `f` or `g`;
- a local obtained from `f` by `TryRemove(…, out x)`, `Remove(…, out x)`, an indexer read, or `foreach` over
`f` / `f.Values`;
- or `using` / `await using` of one of those.
3. **Not a borrow.** The acquisition call is not in the borrow table: `IServiceProvider.GetService`,
`GetRequiredService`, `GetServices`, `GetKeyedService*`, `ActivatorUtilities.GetServiceOrCreateInstance`. The
table only suppresses; it never creates ownership.

Ownership is **never** inferred from the result type being `IDisposable`/`IAsyncDisposable`, from a `Create*` name,
or from `await`. The result type matters only because rule 2 needs something to dispose.

**Defect, given ownership.** A call that can throw (any invocation or `await`, other than `nameof`/`typeof`) lies
between the acquisition and the hand-over, and no enclosing `try` disposes `r` on the way out (`catch` or
`finally` that disposes `r`, or a `published`-style flag guarding a dispose).

**F0-B inputs.**

- **Real code**, as single files from GitHub at the pairs' SHAs, parsed with framework references only:
- R: rockbot `McpBridgeService.cs` base and fix;
- B: BareWire `RabbitMqTransportAdapter.cs` base and fix;
- X: NexusKit `PluginHostBuilder.cs` base and fix, plus `PluginHost.cs` at the same SHAs.
- **Negative controls** (`controls/OwnershipControls.cs`, written before the first run). Each must be **silent**:

| # | Control |
|---|---|
| N1 | DI-resolved: `var s = sp.GetRequiredService<IFoo>(); await X(); _foo = s;` with `T` disposing `_foo` (borrow table) |
| N2 | borrowed reference: a parameter stored into a field `T` disposes (not acquired by a call) |
| N3 | shared instance stored in a field `T` never disposes: `var c = Cache.Get(k); await X(); _c = c;` |
| N4 | caching factory into a dictionary `T` never disposes from |
| N5 | factory result handed over **before** any throwing call |
| N6 | the throwing step inside `try`/`catch` that disposes `r` and rethrows (the fixes' shape) |
| N7 | `published` flag + `finally` disposal (the rockbot fix's shape) |
| N8 | factory result used and disposed locally with `using` (no hand-over) |
| N9 | factory result returned to the caller (rule 1 has no return case: silent by design, an inter-procedural case) |

- **Positive samples**, which must be reported: the R, X and B shapes in synthetic form, P-R, P-X and P-B.

**F0-B pass.** All three of:

- the oracle reports the real R, X and B base files at the acquisition, with ownership established by rules 1–2,
each citing the disposing line it found;
- it is silent on their fix files;
- N1–N9 are silent and P-R, P-X and P-B are reported.

Any failure → `KILL-N1`. The oracle must not be changed after the first run on the real files; control files may
be extended.

The oracle is a throwaway research scan (Roslyn, the same build route as the #416 PoC). It is not an Own.NET
implementation.

## F0-C — cost

Read the extractor (`frontend/roslyn/OwnSharp.Extractor/Program.cs`) and OwnIR (`ownlang/ownir.py`) and answer
three questions with file and line references:

1. Can the extractor emit an acquisition for a call result (rather than `new`) using an existing OwnIR fact kind?
2. Can it emit the hand-over (field, collection or wrapper store) as an existing release/move fact?
3. Are throw edges between acquisition and hand-over already expressible (the `--body-throw-edges` tier)?

**F0-C kill.** Any of the three needs a new OwnIR fact kind, a version bump, or a new interprocedural pass in the
core → `KILL-N1`. Needing only extractor-side work (emitting existing facts from new syntax) is acceptable, and
the estimate is reported.

## Verdict

`PASS-F0` only if F0-A, F0-B and F0-C all pass. Otherwise `KILL-N1`, naming the first failing part.
107 changes: 107 additions & 0 deletions docs/evidence/n1-f0-2026-10/REPORT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
# N1-F0 — ownership feasibility gate — report

**Result: `KILL-N1`. The first failing part is F0-B, and the failure is in the may-throw model, not in ownership.**

| Part | Verdict | Short reason |
|---|---|---|
| F0-A competitor check | **pass** | R, X, B stay `MISSED` under every `interprocedural_analysis_kind` and ownership-transfer setting, with every disposal-related diagnostic inside the method collected |
| F0-B ownership oracle | **fail** | ownership is established on all three real base files without name/type/`await` heuristics, but the **BareWire fixed file is flagged**: `Guid.NewGuid().ToString("N")` counts as a may-throw call before the hand-over |
| F0-C cost | pass (not decisive) | acquisition, hand-over and throw edges fit existing OwnIR ops; the existing throw model is the same coarse one that failed F0-B |

Rules: [`00-preregistration.md`](00-preregistration.md), committed in `66731cc2` before any F0 run. The oracle was
frozen in `081b68ee`, after its control-only debugging and before the one scored run on real files. Time used:
21:51–21:58 +05 on 2026-10-20 for the runs, inside the 0.25 agent-day budget.

No production, OwnIR, CI or golden change. Nothing third-party was built or downloaded.

## F0-A

[`scripts/run_f0a.py`](scripts/run_f0a.py) rebuilt the #417 reproductions under 11 configurations: A1–A6 cover
`interprocedural_analysis_kind` `None` / `NonContextSensitive` / `ContextSensitive`, each with and without both
ownership-transfer switches; K1–K5 repeat the #417 set. The collector takes every disposal-related diagnostic
located inside the buggy method's line span (`data/f0a_spans.tsv`), not only on the `ACQ` line.

Result (`data/f0a_method_diagnostics.tsv`):

| Pair | Result |
|---|---|
| W | CA2000 on `new ServiceBusClient(…)` in A1–A6 and K2–K4 (`CAUGHT`) |
| R | only CA2000 on `out var oldClient`, line 28, in all 11 configurations. That is another object, `ADJACENT`, so R stays `MISSED` |
| X | nothing (`MISSED`) |
| B | nothing (`MISSED`) |

3 pairs missed, against the required ≥ 2, so F0-A passes. No interprocedural setting changes anything.

## F0-B

**The oracle.** [`oracle/Program.cs`](oracle/Program.cs), a Roslyn scan, applies rules 1–3 as registered.
Ownership needs a hand-over target that the repository itself disposes, and the borrow table only suppresses. Two
details were fixed in the code header before the real run:

- **"Disposes r"** means any of: `Dispose`/`DisposeAsync`/`Close`/`CloseAsync` on `r`; the same call on an owning
wrapper `new W(r)`; or `r` passed to a method of the same type that disposes its parameter.
- **One control-driven fix.** A dispose of `r` inside the `catch` is not a throwing site (control N6).

**Controls** (`data/f0b_controls.tsv`). N1–N9 are silent: DI-resolved, borrowed parameter, shared and cached
instances never disposed, hand-over first, `try`/`catch` dispose, `published` flag, `using`, returned. P-R, P-B and
P-X are reported.

**Real files** (`data/f0b_real.tsv`). Single files at the pairs' SHAs (hashes in `data/f0b_inputs.sha256`), parsed
with framework references only.

| File | Oracle | Ownership evidence it found |
|---|---|---|
| R base `McpBridgeService.cs` | reported at `McpClient.CreateAsync` (l. 561); throw at `await newClient.ListToolsAsync` (l. 564); hand-over `_clients[name]` (l. 577) | `_clients` element disposed: `oldClient.DisposeAsync()` (l. 573), with `oldClient` taken by `_clients.Remove(name, out var oldClient)` |
| R fix | silent | **no owned acquisition**: the fix hands the client over through `new ConnectionResources(newClient)` assigned to a local and an object-initializer member, which rules 1a–1c do not cover. Silent, but not because the cleanup was recognised |
| X base `PluginHostBuilder.cs` + `PluginHost.cs` | reported at `BuildServiceProvider` (l. 90); first throw at `provider.GetService<…>()` (l. 92); hand-over `return new PluginHost(provider)` (l. 136) | wrapper rule 1c: `PluginHost.mProvider` disposed at `PluginHost.cs:27` |
| X fix | silent | the `catch` disposes `new PluginHost(provider)`, an owning wrapper |
| B base `RabbitMqTransportAdapter.cs` | reported at `CreateChannelAsync` (l. 285); first throw listed at `Math.Min(…)` (l. 294), and `BasicQosAsync` lies in the same window; hand-over `_activeConsumerChannels[id]` (l. 321) | `channel.CloseAsync(…)` (l. 249) on a channel taken from `_activeConsumerChannels` |
| **B fix** | **reported** (FP) | ownership is right, but the only calls between `CreateChannelAsync` (l. 286) and the early hand-over (l. 300) are `Guid.NewGuid().ToString("N")` (l. 299). The registered rule "any invocation can throw" counts them |

By the registered pass rule, which requires silence on every fix file, F0-B fails. The oracle was not changed after
this run.

**What the failure means.**
- **Confirmed.** The ownership half works on these inputs:
- it found the disposing line for all three real targets;
- it stayed silent on all nine negative controls without any `IDisposable`, `Create*` or `await` cue;
- in X and B it established ownership across a wrapper and across a collection.
- **Confirmed.** The registered may-throw rule is too coarse. One of three fixes is flagged only because of
non-throwing BCL calls.
- **Inference, not scored.** A may-throw model that exempts such calls would clear B fix while keeping B base,
because `BasicQosAsync` lies inside its window. Nothing was run to show it.
- **Limit.** The R fix shows a recall gap: a hand-over through a local wrapper or an object initializer establishes
no ownership. A bug in that shape would be missed.

## F0-C

Read with line references in `main` (`38fb952d`):

1. **Acquisition from a call.** Already expressible: the flow-locals pass emits `acquire` for `new`, pool rents and a
curated owning-factory table (`IsOwningFactory`, `frontend/roslyn/OwnSharp.Extractor/Program.cs:3832-3837`).
For first-party factories the core can mint the acquire itself from a `call` op (P-005 D5.2,
`Program.cs:3849`). An oracle-based acquire would be extractor-side only.
2. **Hand-over.** The existing `release` op can discharge the obligation (`ownlang/ownir.py:343-347`,
`_FLOW_OPS`). Today a local stored to a field "escapes" and is not flow-tracked at all (`--flow-locals` covers
non-escaping locals only, `Program.cs:84-87`). Changing that is extractor-side work.
3. **Throw edges.** These exist (`InjectThrowEdge`, `Program.cs:3569-3587`, `--body-throw-edges`). They use
`StatementMayThrow` (`Program.cs:3590-3599`): any non-dispose call or `new` may throw. That is the same coarse
model that failed F0-B, and the extractor itself calls this tier "the CA2000 firehose" (`Program.cs:100-103`).

None of the three needs a new OwnIR op, a version bump or a core interprocedural pass, so F0-C passes by its rule.
It also shows that a precise may-throw model does not exist yet; it would be new extractor work.

Estimate, an inference: the oracle port plus escape tracking is roughly several days of extractor work. A may-throw
model precise enough to clear cases like B fix has no estimate, because nothing like it exists in the repository.

## Files

- [`00-preregistration.md`](00-preregistration.md)
- [`controls/OwnershipControls.cs`](controls/OwnershipControls.cs)
- [`oracle/`](oracle/): the oracle, a Roslyn console, built like the #416 PoC.
- [`scripts/run_f0a.py`](scripts/run_f0a.py)
- `data/`:
- `f0a_method_diagnostics.tsv`, `f0a_spans.tsv`: F0-A;
- `f0b_controls.tsv`, `f0b_real.tsv`, `f0b_inputs.sha256`: F0-B.

The third-party source files are not committed; they are named by SHA and hash.
157 changes: 157 additions & 0 deletions docs/evidence/n1-f0-2026-10/controls/OwnershipControls.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,157 @@
// N1-F0 oracle controls (00-preregistration.md, F0-B). Written before the first run.
// Methods N<n>_* must be SILENT; methods P_* must be REPORTED.
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Threading.Tasks;
using Microsoft.Extensions.DependencyInjection;

namespace OwnershipControls;

public interface IFoo : IAsyncDisposable { Task PingAsync(); }
public interface IConn : IAsyncDisposable { Task<IFoo> OpenAsync(); }

public static class Cache
{
public static IFoo Get(string key) => throw new NotSupportedException();
}

public static class Remote
{
public static Task<IFoo> CreateAsync(string url) => throw new NotSupportedException();
}

public sealed class Wrap : IAsyncDisposable
{
private readonly IFoo _inner;
public Wrap(IFoo inner) { _inner = inner; }
public ValueTask DisposeAsync() => _inner.DisposeAsync();
}

public sealed class Holder : IAsyncDisposable
{
private readonly IServiceProvider _sp;
private readonly IConn _conn;
private IFoo? _foo;
private IFoo? _shared;
private readonly ConcurrentDictionary<string, IFoo> _owned = new();
private readonly Dictionary<string, IFoo> _cache = new();

public Holder(IServiceProvider sp, IConn conn) { _sp = sp; _conn = conn; }

private static Task StepAsync() => Task.Delay(1);

// ---- negative controls: must be silent ----

public async Task N1_DiResolved()
{
var s = _sp.GetRequiredService<IFoo>();
await StepAsync();
_foo = s;
}

public async Task N2_Borrowed(IFoo given)
{
await StepAsync();
_foo = given;
}

public async Task N3_SharedNeverDisposed(string k)
{
var c = Cache.Get(k);
await StepAsync();
_shared = c;
}

public async Task N4_CachingFactoryNeverDisposed(string k)
{
var c = await Remote.CreateAsync(k);
await c.PingAsync();
_cache[k] = c;
}

public async Task N5_HandOverFirst(string k)
{
var c = await Remote.CreateAsync(k);
_owned[k] = c;
await c.PingAsync();
}

public async Task N6_TryCatchDispose(string k)
{
var c = await Remote.CreateAsync(k);
try
{
await c.PingAsync();
}
catch
{
await c.DisposeAsync();
throw;
}
_owned[k] = c;
}

public async Task N7_PublishedFlag(string k)
{
IFoo? c = null;
var published = false;
try
{
c = await Remote.CreateAsync(k);
await c.PingAsync();
_owned[k] = c;
published = true;
}
finally
{
if (!published && c is not null) await c.DisposeAsync();
}
}

public async Task N8_LocalUsing(string k)
{
await using var c = await Remote.CreateAsync(k);
await c.PingAsync();
}

public async Task<IFoo> N9_Returned(string k)
{
var c = await Remote.CreateAsync(k);
await c.PingAsync();
return c;
}

// ---- positive samples: must be reported ----

// P-R: awaited factory, throwing call on the result, then stored into a dictionary T disposes from
public async Task P_R(string k)
{
var c = await Remote.CreateAsync(k);
await c.PingAsync();
_owned[k] = c;
}

// P-B: awaited interface factory, throwing call, then dictionary store
public async Task P_B(string k)
{
IFoo ch = await _conn.OpenAsync();
await ch.PingAsync();
_owned[k] = ch;
}

// P-X: factory result wrapped in an in-source type that disposes it, after a throwing call
public async Task<Wrap> P_X()
{
var c = await Remote.CreateAsync("x");
await StepAsync();
return new Wrap(c);
}

public async ValueTask DisposeAsync()
{
if (_foo is not null) await _foo.DisposeAsync();
foreach (var v in _owned.Values) await v.DisposeAsync();
if (_owned.TryRemove("k", out var one)) await one.DisposeAsync();
}
}
Loading
Loading