From 780220d7e814522396e0b716c2e3ade4c55f19ef Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 12:04:33 +0000 Subject: [PATCH 1/2] docs: digest 2026 research-landscape survey + record LLM-layer position Add docs/notes/research-landscape-2026.md, a companion to the consolidation-and-positioning note: that one covers form (naming, schema, splits); this one covers research positioning (landscape, gaps, LLM role). Captures the external survey's thesis (external static contracts for .NET resource/lifetime bugs; resource-leak / specify-and-check family; hybrid LLM+static keeping the deterministic checker as decider; the missing public .NET lifetime/resource benchmark as the opening), then records the three places our reading diverges: - We already have a *deterministic* spec miner (contract-inference / _infer_param_effect), which the survey files under far-horizon LLM work. - Differentiation is already demonstrated (3-way oracle on WalletWasabi), so the benchmark ask is "formalize what we did", not net-new. - The LLM layer must be a falsifiable fix/refactor assistant downstream of the verifier, never a trusted spec source: an LLM fix is locally falsifiable (re-run checker + tests), an LLM spec is trusted-base and fails silently. Any spec miner must be validator-gated, not trust-the-source. Records the implied backlog (SARIF exporter, benchmark corpus as first-class artifact, metamorphic robustness harness, validator-gated boundary-API spec miner) without scheduling it, and explicitly de-duplicates the SUB/DIS rename against the already-logged WPFxxx rename decision. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- docs/notes/research-landscape-2026.md | 158 ++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 docs/notes/research-landscape-2026.md diff --git a/docs/notes/research-landscape-2026.md b/docs/notes/research-landscape-2026.md new file mode 100644 index 00000000..d8e07acc --- /dev/null +++ b/docs/notes/research-landscape-2026.md @@ -0,0 +1,158 @@ +# Research landscape 2026 — digest + Own.NET reading + +Working notes digesting an external research-landscape survey (shared 2026-06: +"Статический анализ в 2026 и окно возможностей для Own.NET") and reading it +against where Own.NET actually stands. Companion to +`consolidation-and-positioning.md`: that note is about **form** (naming, schema, +file splits); this one is about **research positioning** — landscape, gaps, and +the role of an LLM layer. The survey's own conclusion is *"don't change focus, +finish the line you're on"*, and that is taken; the value of this note is the +three places where our reading **diverges** from the survey, recorded so they +don't evaporate. + +## The survey's thesis (fair summary) + +- **Direction.** Don't build "Rust for C#". Build an external static-contract + layer for concrete, expensive, reproducible .NET resource/lifetime bugs: + events/WPF subscriptions, `IDisposable`, DI lifetime mismatch, `ArrayPool`/ + `Span` misuse. (This is already our ROADMAP.) +- **Three landscape currents.** + 1. Abstract-interpretation foundations remain the base, but industry trades + soundness for speed / explainability / CI-fit (rule- and query-driven + analyzers, not whole-program soundness). + 2. The **resource-leak / must-call / specify-and-check** family is proven — + Checker Framework resource-leak (`@MustCall`), *RLC# for C#* on CodeQL + (24 real leaks in OSS + Azure), *Inference of Resource Management + Specifications* — but is bottlenecked on **manual specs** and weak coverage + of project-specific APIs. + 3. 2024–2026 **hybrid LLM + static**: the strong results keep the LLM in + *narrow* roles (spec inference, path-feasibility triage, summary + generation) and let a **deterministic checker decide** (InferROI, IRIS, + LLM4PFA, MemHint; the "LLMs vs static tools on C#" benchmark: LLMs win + recall, lose precision + localization → hybrid recommended). +- **Biggest gap, biggest opening.** There is **no public .NET lifetime/resource + benchmark** (Java has DroidLeaks / JLeaks; security has CWE-Bench-Java / + CASTLE). Own.NET could be the analyzer **and** the benchmark/corpus — the path + to reproducibility and a citeable result. +- **Priority shape.** Quick wins: subscription, `IDisposable`, DI captive-dep, + and a benchmark + SARIF + reproducible corpus. Mid: `ArrayPool`/`Span` + borrow-view. Far: an effects layer and a general spec miner. **Do not** build + a full-C# ownership checker, whole-program alias analysis, a port of the core + to C#, a general effect system, or first-class LINQ/async/generics/source-gen. + +## Where we agree (and where we are already ahead) + +The survey is **descriptive of where we already stand** — one core, narrow +frontend, bug-driven scope, `OWN001` vs `OWN014` lifetime ordering, semantic +resolution killing the syntactic FP wall (P-014). It is a confirmation, not a +redirect. Two places we are already **ahead of the doc's own roadmap**: + +- **A deterministic spec miner already exists.** The survey files "spec miner" + under far-horizon LLM work. But our `contract-inference` (`_infer_param_effect` + in `ownir.py`, P-006/2b) is already a *deterministic* spec miner for local + functions: `release` inside a body → `consume`, use-only → `borrow`, + forward-only → unresolved (deliberately not `return`→consume). The cheap, safe + half of spec mining is **done**; only the boundary-API (BCL/NuGet) half is + open. See the dedicated LLM section below for why that ordering matters. +- **Differentiation is already demonstrated, not hypothetical.** The doc asks + for an oracle and a benchmark; we already ran the 3-way oracle (Own.NET vs + Infer# vs CodeQL) on WalletWasabi and have an own-only subscription-leak set + (CodeQL ships no subscription-token query). So the benchmark ask is *formalize + what we already did*, not net-new research. See `docs/notes/oracle.md` and + `docs/notes/real-world-mining.md`. + +## The LLM layer — our position (the load-bearing section) + +This is the one place we **push back on the survey's framing**. + +The hybrid pattern the doc endorses (InferROI / IRIS / MemHint) is: *LLM +proposes specs/summaries → deterministic core validates*. The **shape** is +right. But the doc still centers the LLM as a **spec source for detection**, and +that quietly puts LLM output in the **trusted base**: a wrong mined spec does not +produce a visible false finding you can argue with — it silently changes what +the checker *believes*, corrupting every downstream proof. A spec whose only +provenance is "the model said so" is `source: trust me bro`, and that is not an +acceptable trusted base. + +Own.NET's safer division of labor: + +1. **Deterministic fixes for the mechanical ~80%** — add the missing `-=`, wrap + in `using`, cascade `Dispose`. No LLM in the loop at all. +2. **LLM strictly downstream of the verifier, as a falsifiable assistant** for + the non-local ~20% and for **migration into the own.net model**. Every LLM + output is a *hypothesis* that the deterministic core + compile + tests accept + or reject. The LLM proposes; it never decides. + +Why the **fix/refactor** role beats the **spec-source** role — the asymmetry is +the whole point: + +- An LLM **fix** is *locally falsifiable*: re-run Own.NET + the test suite and + observe. Wrong fixes are caught by the same checker that flagged the bug. +- An LLM **spec** is *trusted-base*: nothing locally re-checks it; it just + changes the checker's beliefs. Wrong specs are **silent**. + +So the refactor-assistant role is **safe by construction**; the spec-source role +is not. The verifier is what makes the LLM safe to use at all — the LLM is only +ever as trustworthy as the deterministic thing that re-checks its output. + +Therefore, **if** a spec miner is built, it must be **validator-gated, never +trust-the-source**: each candidate spec is downgraded from "trusted" to +"candidate validated against the API body / call sites" — symbol exists, CFG +reachable, path feasible, consistent with observed uses. A candidate that cannot +be validated against a body is **dropped, not assumed**. That is exactly what our +existing deterministic miner already does (`_infer_param_effect` reads the body), +extended to boundary APIs — not the LLM-trust version. The LLM's only job there +is to *propose candidates faster* over the huge BCL/NuGet surface we will never +hand-spec; the validator, not the model, admits them. + +The product shape this implies is a **fix-loop**, not a scanner: flag → LLM +proposes a multi-edit fix/refactor → re-run Own.NET + compile + tests → +accept/reject. Honest caveat: **green ≠ behavior-preserving**, so the loop needs +a **metamorphic conformance harness** (the doc's StaAgent / Statfier line) as the +check, not human trust. + +## Concrete backlog this implies (recorded, NOT scheduled) + +Ordered by leverage; each annotated with where it attaches and its real cost. + +- **SARIF exporter.** Standard interchange (OASIS), GitHub-native code scanning, + and — the under-sold reason — *scientific reproducibility* (frozen, diffable + run artifacts). Cheap, high-leverage. **Attaches to** P-012 / the distribution + surface (P-013). +- **Benchmark corpus as a first-class artifact.** Formalize the WalletWasabi + mining + oracle into a labeled (bug / no-bug / unknown), before/after, + SARIF-harnessed corpus. This is the survey's strongest "this is a research + contribution, not a hobby tool" lever, and we are already ~70% there (miner + + oracle exist). **Extends** P-012. Highest research-value item on the shelf. +- **Metamorphic robustness harness.** Semantically-equivalent mutants (rename + handlers, `lambda ↔ method-group`, reorder under no-semantic-change, add + harmless branches) must yield **invariant** diagnostics modulo location. This + is simultaneously (a) the conformance check that makes the LLM fix-loop + trustworthy and (b) a separable contribution on its own. **New, far horizon.** +- **Validator-gated spec miner for boundary APIs.** Extend the existing + deterministic `contract-inference` to BCL/NuGet acquire/release/transfer/ + borrow specs; LLM only as a candidate proposer *behind* the validator. **Far + horizon, explicitly NOT trusted-base** (see the LLM section). + +## What we deliberately do NOT take from the survey + +- **The arXiv/paper roadmap** is fine as motivation and is recorded as context, + but it is **not a code task** — no deliverable is filed off it here. +- **The full SUB/DIS/DI/BOR code-rename matrix** (SUB001, DIS001, …) overlaps the + `WPFxxx → SUB/TMR/DISP` rename **already logged** in + `consolidation-and-positioning.md`. Do **not** double-track it; that note owns + the rename decision (fold into the OwnIR v1 / profile-config work, not a + standalone churn PR). +- **The effects / typestate / session-types layer** stays far-horizon (P-008), + exactly as the survey itself agrees. No move toward refinement types / general + effect systems now. + +## The actual priority (unchanged) + +Same conclusion as `consolidation-and-positioning.md`, reached from the research +side instead of the form side: **prove value, don't reshape form or chase the +frontier.** Concretely — turn the subscription differentiation we already have +into a labeled, SARIF-emitting, reproducible **benchmark corpus**, and keep the +LLM strictly downstream of the deterministic core as a *falsifiable* fix/ +refactor assistant. The one new technical brick worth its weight is the +**metamorphic harness**, because it is what lets us trust an LLM fix-loop at all. From a3476d687f14c654d1bc7543fd6c368260c3853a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 12:27:12 +0000 Subject: [PATCH 2/2] docs: correct WalletWasabi citation to the documented ScreenToGif oracle run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit (PR #41) correctly flagged that the note cited oracle.md / real-world-mining.md as evidence for a WalletWasabi 3-way oracle run, but those files document the ScreenToGif and Dapper runs — WalletWasabi is not written up anywhere in docs/. The WalletWasabi mining/oracle happened in CI but its result was never distilled into the repo, so the citation was broken. Retarget the "differentiation is already demonstrated" claim to the *documented* ScreenToGif oracle result (SystemEvents error + VideoSource warnings, own-only; CodeQL has no "subscribed-never-unsubscribed" query, Infer# misses it too — all in real-world-mining.md "Cross-tool validation"), and label the larger WalletWasabi run honestly as "exercised in CI, not yet distilled into a committed corpus artifact" — which is precisely the benchmark-corpus backlog item, not a result to lean on. Same fix in the backlog bullet. The other flagged reference (consolidation-and-positioning.md) was a merge-timing artifact: it lives in #38, which merged ~3 min after the review; the branch is now rebased onto main, so the file is present. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- docs/notes/research-landscape-2026.md | 29 ++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/docs/notes/research-landscape-2026.md b/docs/notes/research-landscape-2026.md index d8e07acc..765ea5cf 100644 --- a/docs/notes/research-landscape-2026.md +++ b/docs/notes/research-landscape-2026.md @@ -55,11 +55,19 @@ redirect. Two places we are already **ahead of the doc's own roadmap**: half of spec mining is **done**; only the boundary-API (BCL/NuGet) half is open. See the dedicated LLM section below for why that ordering matters. - **Differentiation is already demonstrated, not hypothetical.** The doc asks - for an oracle and a benchmark; we already ran the 3-way oracle (Own.NET vs - Infer# vs CodeQL) on WalletWasabi and have an own-only subscription-leak set - (CodeQL ships no subscription-token query). So the benchmark ask is *formalize - what we already did*, not net-new research. See `docs/notes/oracle.md` and - `docs/notes/real-world-mining.md`. + for an oracle and a benchmark; the 3-way oracle (Own.NET vs Infer# vs CodeQL) + has already run on real C# and produced an own-only subscription-leak set. On + ScreenToGif it flags `SystemEvents.DisplaySettingsChanged` (error) and the four + `VideoSource` view→view-model lambdas (warning) that **CodeQL flags none of** — + its query set has no "event subscribed, never unsubscribed" rule — and that + Infer# misses too. So the benchmark ask is *formalize what we already did* into + a labeled corpus, not net-new research. The harness and the agree/own-only/ + oracle-only buckets are in `docs/notes/oracle.md`; the ScreenToGif run is + written up in `docs/notes/real-world-mining.md` ("Cross-tool validation"). A + larger reactive-code run (WalletWasabi) has been exercised through the same CI + harness but is **not yet distilled into a committed corpus artifact** — that + distillation is exactly the benchmark-corpus backlog item below, not a + documented result to lean on here. ## The LLM layer — our position (the load-bearing section) @@ -119,11 +127,14 @@ Ordered by leverage; each annotated with where it attaches and its real cost. and — the under-sold reason — *scientific reproducibility* (frozen, diffable run artifacts). Cheap, high-leverage. **Attaches to** P-012 / the distribution surface (P-013). -- **Benchmark corpus as a first-class artifact.** Formalize the WalletWasabi - mining + oracle into a labeled (bug / no-bug / unknown), before/after, +- **Benchmark corpus as a first-class artifact.** Formalize the existing mining + + oracle runs — the documented ScreenToGif differentiation + (`real-world-mining.md`) plus the larger WalletWasabi run that currently lives + only in CI artifacts — into a labeled (bug / no-bug / unknown), before/after, SARIF-harnessed corpus. This is the survey's strongest "this is a research - contribution, not a hobby tool" lever, and we are already ~70% there (miner + - oracle exist). **Extends** P-012. Highest research-value item on the shelf. + contribution, not a hobby tool" lever, and we are already partway there (miner + + oracle exist; what is missing is the committed, labeled artifact). **Extends** + P-012. Highest research-value item on the shelf. - **Metamorphic robustness harness.** Semantically-equivalent mutants (rename handlers, `lambda ↔ method-group`, reorder under no-semantic-change, add harmless branches) must yield **invariant** diagnostics modulo location. This