From d84adf5941fe7a3db5d334829458721d827c8d9d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 10 Aug 2026 07:30:19 +0000 Subject: [PATCH 1/2] docs(P-012): record the loop-invariant-call mining packet as a research seed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The merged invariant-cost note measured a 1.0x-1092x spread over four hand-picked shapes and closed by saying the honest first step is mining, not a rule. This records what that scan should collect, so the measurement design does not evaporate — it survives even if a future checker turns out to be a completely different thing, because it describes an observation, not an architecture. The packet keeps three independent label axes -- input stability, call repeatability, placement safety -- with the flat bucket derived from them and never recorded instead of them. Collapsing early is what would waste the scan: inputs-proven/repeatability-proven/placement-unknown and inputs-proven/repeatability-unknown/placement-proven both flatten to UNKNOWN, and the product question of which axis is the bottleneck stops being answerable from the data. Two fields exist specifically because the presence of a control transfer is not discriminating on its own: `var x = F(); if (c) break;` and `if (c) break; var x = F();` record identical control-transfer syntax and have entirely different placement stories, so call_control_context and call_reachability_per_iteration keep a difference the scan is not required to resolve but must not lose. Two guards are stated in the text because a column list invites being turned into a predicate: no single field, receiver immutability included, is evidence that hoisting preserves semantics, and the pass must preserve unknown rather than infer safety from the absence of a recognised hazard. Pure addition inside the stage-2 material, marked "Research seed only; does not schedule or specify a checker." Status, dependencies, non-goals, the ROADMAP and the proposal index are untouched; no issue is filed; no attribute, receiver whitelist, lattice or fix-arm design is introduced -- those are conclusions from numbers that do not exist yet. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01PbyzyVi7fibuSKLweuXgea --- docs/proposals/P-012-bug-corpus-mining.md | 78 +++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/docs/proposals/P-012-bug-corpus-mining.md b/docs/proposals/P-012-bug-corpus-mining.md index 7d58562f..4e3cc6a5 100644 --- a/docs/proposals/P-012-bug-corpus-mining.md +++ b/docs/proposals/P-012-bug-corpus-mining.md @@ -148,6 +148,84 @@ dotnet/runtime use-after-return; Nethermind ArrayPool leaks / double-return; AiDotNet.Tensors pooled-buffer leak / over-clear. Reproduce each, reduce it into `corpus/`, and confirm the checker's verdict matches the real fix. +### Focused stage-2 mining packet: repeated loop-invariant-call candidates + +*Research seed only; does not schedule or specify a checker.* + +A stage-2 sub-scan for one syntactic shape — a call inside a loop whose result +may not change across iterations. It exists to answer a prevalence question that +[`docs/notes/invariant-cost-static-vs-runtime.md`](../notes/invariant-cost-static-vs-runtime.md) +raised and could not answer: that note measured a **1.0×–1092× cost spread over +four hand-picked shapes** and closed by saying the honest first step is mining, +not a rule. This packet is that mining and nothing more. + +**Why three label axes and not one verdict.** "Can this call be hoisted" is not +one property. It decomposes into three independent ones — the inputs not +changing, the call returning the same thing when repeated, and the move itself +being legal — and a flat safe/unsafe label destroys the only interesting +measurement: *which* axis eats the coverage of a cheap version. (Production +compilers keep repeatability and placement legality as separate function +attributes, which is precedent for the decomposition — not a ready-made mapping +onto C#.) + +**Per-candidate observations.** Facts only; several are deliberately +three-valued because the scan is syntactic: + +| field | values | +| --- | --- | +| `callee_symbol` | resolved FQN, or `unresolved` | +| `loop_kind` | `for` / `foreach` / `while` / `do` | +| `receiver_static_type` | declared type, or none for a static call | +| `receiver_provenance` | local / parameter / field / property / call-result / literal / unknown | +| `capture_count`, `capture_types` | count and declared types of captured locals | +| `writes_to_receiver_in_loop` | yes / no / unknown | +| `writes_to_captures_in_loop` | yes / no / unknown | +| `lambda_contains_calls` | yes / no / not-applicable | +| `lambda_contains_ambient_reads` | static or externally-reachable reads: yes / no / unknown | +| `result_type` | declared return type | +| `invocation_multiplicity` | syntactic estimate of evaluations per loop entry | +| `loop_may_execute_zero_times` | yes / no / unknown | +| `control_transfer_in_body` | which of `break` / `continue` / `return` / `throw` occur, with positions | +| `call_control_context` | unconditional-in-body / conditional / short-circuit-operand / nested-lambda-or-local-function / unknown | +| `call_reachability_per_iteration` | every-entered-iteration / may-be-skipped-before-first-execution / unknown | + +The last two fields exist because the presence of a control transfer is not by +itself discriminating — `var x = F(); if (c) break;` and `if (c) break; var x = +F();` record the same `control_transfer_in_body` and have entirely different +placement stories. The scan does not have to resolve that difference; it must +not lose it. + +**Three independent labels, assigned per candidate:** + +| axis | values | +| --- | --- | +| `input_stability` | cheap-proven / disproven / unknown | +| `call_repeatability` | cheap-proven / disproven / needs-effect-reasoning / unknown | +| `placement_safety` | cheap-proven / disproven / needs-cfg-reasoning / unknown | + +…and only then a **derived** bucket: `CHEAP_PROVABLE` (all three cheap-proven) / +`NEEDS_EFFECT_REASONING` / `NEEDS_PLACEMENT_REASONING` / `DEFINITELY_UNSAFE` / +`UNKNOWN`. Derived — never recorded instead of the three. + +Collapsing the axes early is what would waste the scan: *inputs proven, +repeatability proven, placement unknown* and *inputs proven, repeatability +unknown, placement proven* both flatten to `UNKNOWN`, and the product question — +which axis is the bottleneck — becomes unanswerable from the data. + +**Two guards on reading this packet:** + +> These fields are observations for prevalence measurement, not a specification +> of a loop-hoisting checker. No individual field — including receiver +> immutability, the absence of control-transfer syntax, or a recognised callee +> symbol — is by itself evidence that hoisting is semantics-preserving. + +> The mining pass must preserve `unknown` rather than infer safety from the +> absence of a recognised hazard. + +Both are here because a column list is an inviting thing to turn into a +predicate, and `if immutable_receiver and not contains_throw: report()` is +exactly the shape this packet exists to prevent someone deriving. + ## Open questions 1. Repo selection for stage 2 — top-N by stars, or weight toward the high-load From 173db50ca17dbd4a65bd270a30d1e67410f46c31 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 10 Aug 2026 08:30:48 +0000 Subject: [PATCH 2/2] =?UTF-8?q?docs(P-012):=20address=20review=20=E2=80=94?= =?UTF-8?q?=20make=20the=20mining=20schema=20unambiguous?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four review findings, all checked against the text and all valid; none changes what the packet says, each removes a way to read it two ways. capture_count and capture_types shared one table row, so the table had one fewer row than it had identifiers and a miner could reasonably emit either shape. They are now one row each: 19 rows, 19 identifiers, no composite left implicit. call_control_context was written as a single value while its values genuinely overlap -- `c && F()` is both conditional and short-circuit-operand, and a call in a lambda under an if is also nested-lambda-or-local-function. Forcing one value would discard exactly the distinctions the field exists to keep, so it is now explicitly a set, with the overlap spelled out. The derived bucket named five outcomes without saying how a label tuple maps to one, and two tuples matched two buckets: needs-effect-reasoning together with needs-cfg-reasoning, and disproven together with any reasoning-required axis. It now derives by an ordered, total rule. A settled negative takes precedence over an open axis; the order of the two reasoning rungs is a reporting convention rather than a claim about which reasoning dominates, and it costs nothing because the three axis labels are always kept, so a candidate needing both is recoverable from the data whichever bucket it rolls into. The two guards were two blockquotes separated by a blank line, which trips markdownlint MD028; they are one blockquote with two bullets now. Verified: MD028 count is 0. The MD013 line-length reports that remain on the new table rows match this document's existing tables, which already run past 100 characters, so they are its convention and are left alone. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01PbyzyVi7fibuSKLweuXgea --- docs/proposals/P-012-bug-corpus-mining.md | 42 ++++++++++++++++------- 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/docs/proposals/P-012-bug-corpus-mining.md b/docs/proposals/P-012-bug-corpus-mining.md index 4e3cc6a5..3f2d283d 100644 --- a/docs/proposals/P-012-bug-corpus-mining.md +++ b/docs/proposals/P-012-bug-corpus-mining.md @@ -177,7 +177,8 @@ three-valued because the scan is syntactic: | `loop_kind` | `for` / `foreach` / `while` / `do` | | `receiver_static_type` | declared type, or none for a static call | | `receiver_provenance` | local / parameter / field / property / call-result / literal / unknown | -| `capture_count`, `capture_types` | count and declared types of captured locals | +| `capture_count` | number of captured locals | +| `capture_types` | declared types of those captured locals | | `writes_to_receiver_in_loop` | yes / no / unknown | | `writes_to_captures_in_loop` | yes / no / unknown | | `lambda_contains_calls` | yes / no / not-applicable | @@ -186,9 +187,14 @@ three-valued because the scan is syntactic: | `invocation_multiplicity` | syntactic estimate of evaluations per loop entry | | `loop_may_execute_zero_times` | yes / no / unknown | | `control_transfer_in_body` | which of `break` / `continue` / `return` / `throw` occur, with positions | -| `call_control_context` | unconditional-in-body / conditional / short-circuit-operand / nested-lambda-or-local-function / unknown | +| `call_control_context` | **set**, not one value — any of unconditional-in-body / conditional / short-circuit-operand / nested-lambda-or-local-function, or unknown | | `call_reachability_per_iteration` | every-entered-iteration / may-be-skipped-before-first-execution / unknown | +`call_control_context` is a **set** because its values genuinely overlap: +`c && F()` is both `conditional` and `short-circuit-operand`, and a call in a +lambda under an `if` is also `nested-lambda-or-local-function`. Forcing one +value would discard exactly the distinctions the field exists to keep. + The last two fields exist because the presence of a control transfer is not by itself discriminating — `var x = F(); if (c) break;` and `if (c) break; var x = F();` record the same `control_transfer_in_body` and have entirely different @@ -203,9 +209,21 @@ not lose it. | `call_repeatability` | cheap-proven / disproven / needs-effect-reasoning / unknown | | `placement_safety` | cheap-proven / disproven / needs-cfg-reasoning / unknown | -…and only then a **derived** bucket: `CHEAP_PROVABLE` (all three cheap-proven) / -`NEEDS_EFFECT_REASONING` / `NEEDS_PLACEMENT_REASONING` / `DEFINITELY_UNSAFE` / -`UNKNOWN`. Derived — never recorded instead of the three. +…and only then a **derived** bucket. Derived — never recorded instead of the +three. Derivation is ordered and total, so every label tuple maps to exactly one +bucket: + +1. any axis `disproven` → `DEFINITELY_UNSAFE` +2. else all three `cheap-proven` → `CHEAP_PROVABLE` +3. else any axis `needs-effect-reasoning` → `NEEDS_EFFECT_REASONING` +4. else any axis `needs-cfg-reasoning` → `NEEDS_PLACEMENT_REASONING` +5. else → `UNKNOWN` + +Rule 1 precedes the reasoning rungs because a settled negative is not made less +settled by another axis being open. The order of rungs 3 and 4 is a reporting +convention, not a claim that effect reasoning dominates control-flow reasoning — +the three axis labels are always kept, so a candidate needing both is fully +recoverable from the data whichever bucket it rolls up into. Collapsing the axes early is what would waste the scan: *inputs proven, repeatability proven, placement unknown* and *inputs proven, repeatability @@ -214,13 +232,13 @@ which axis is the bottleneck — becomes unanswerable from the data. **Two guards on reading this packet:** -> These fields are observations for prevalence measurement, not a specification -> of a loop-hoisting checker. No individual field — including receiver -> immutability, the absence of control-transfer syntax, or a recognised callee -> symbol — is by itself evidence that hoisting is semantics-preserving. - -> The mining pass must preserve `unknown` rather than infer safety from the -> absence of a recognised hazard. +> - These fields are observations for prevalence measurement, not a +> specification of a loop-hoisting checker. No individual field — including +> receiver immutability, the absence of control-transfer syntax, or a +> recognised callee symbol — is by itself evidence that hoisting is +> semantics-preserving. +> - The mining pass must preserve `unknown` rather than infer safety from the +> absence of a recognised hazard. Both are here because a column list is an inviting thing to turn into a predicate, and `if immutable_receiver and not contains_throw: report()` is