feat(p014): add opt-in project-aware binding coverage

.github/workflows/ci.yml

@@ -2132,6 +2132,50 @@ jobs:
                <(jq -S . "$RUNNER_TEMP/proj-facts-norefs.json") \
             || { echo "FAIL: --no-project-refs changed the facts for an unbuilt sample project"; exit 1; }
           echo "OK: --help renders the option list; --no-project-refs is accepted"
+      # P-014 PROD0: the opt-in --binding-coverage sidecar is OBSERVATION ONLY. The facts are byte-identical with
+      # and without it; a directory or an unrestored project is recorded UNSUPPORTED (never measured by substitution);
+      # a restored copy of the sample is measured per project with no foreign binding, deterministically.
+      # Evidence: docs/evidence/p014-prod0-2026-10.
+      - name: P-014 PROD0 — --binding-coverage sidecar (observation only)
+        run: |
+          x="dotnet run --project frontend/roslyn/OwnSharp.Extractor --"
+          proj=frontend/roslyn/project-input-sample/ProjectInputSample.csproj
+          $x "$proj" -o "$RUNNER_TEMP/bc-off.json"
+          $x "$proj" -o "$RUNNER_TEMP/bc-on.json" --binding-coverage "$RUNNER_TEMP/bc-unrestored.json"
+          cmp "$RUNNER_TEMP/bc-off.json" "$RUNNER_TEMP/bc-on.json" \
+            || { echo "FAIL: --binding-coverage changed the facts document"; exit 1; }
+          $x frontend/roslyn/samples -o "$RUNNER_TEMP/bc-dir-off.json"
+          $x frontend/roslyn/samples -o "$RUNNER_TEMP/bc-dir-on.json" --binding-coverage "$RUNNER_TEMP/bc-dir.json"
+          cmp "$RUNNER_TEMP/bc-dir-off.json" "$RUNNER_TEMP/bc-dir-on.json" \
+            || { echo "FAIL: --binding-coverage changed the facts document (directory input)"; exit 1; }
+          # a restored COPY of the sample (the sample itself stays unbuilt for the parity checks above)
+          cp -r frontend/roslyn/project-input-sample "$RUNNER_TEMP/bc-sample"
+          dotnet restore "$RUNNER_TEMP/bc-sample/ProjectInputSample.csproj"
+          for run in 1 2; do
+            $x "$RUNNER_TEMP/bc-sample/ProjectInputSample.csproj" -o "$RUNNER_TEMP/bc-r$run-facts.json" \
+              --binding-coverage "$RUNNER_TEMP/bc-restored-$run.json"
+          done
+          cmp "$RUNNER_TEMP/bc-restored-1.json" "$RUNNER_TEMP/bc-restored-2.json" \
+            || { echo "FAIL: the binding-coverage sidecar is not deterministic"; exit 1; }
+          python - "$RUNNER_TEMP" <<'PY'
+          import json, sys
+          t = sys.argv[1]
+          def units(name):
+              return json.load(open(f"{t}/{name}.json"))["units"]
+          [u] = units("bc-unrestored")
+          assert u["unit_status"] == "UNSUPPORTED" and u["reasons"]["unsupported"] == ["no-assets"], u
+          [u] = units("bc-dir")
+          assert u["unit_status"] == "UNSUPPORTED" and u["reasons"]["unsupported"] == ["input-kind:directory"], u
+          [u] = units("bc-restored-1")
+          assert u["reference_status"] == "COMPLETE", u["reasons"]
+          assert u["foreign_binding"] == 0 and u["invariants_failed"] == [], u
+          # fail closed: COMPLETE only with no reason on any axis
+          reasons = u["reasons"]["reference"] + u["reasons"]["source_set"] + u["reasons"]["unsupported"]
+          assert (u["unit_status"] == "COMPLETE") == (not reasons), (u["unit_status"], reasons)
+          assert u["sites"]["event_assign"]["event"] >= 1, u["sites"]
+          print("OK: PROD0 sidecar —", u["unit_status"], u["tfm"], u["tfm_status"], "reasons:", reasons)
+          PY
+          echo "OK: --binding-coverage leaves facts byte-identical; UNSUPPORTED inputs recorded; restored sample measured"
       # explain: the diagnostic-catalogue CLI surface lives in the core (one checker). Smoke
       # it end-to-end — explain a code, and harvest+explain every code in a real findings file.
       - name: explain command (code + --json harvest)

docs/evidence/p014-prod0-2026-10/00-preregistration.md

@@ -0,0 +1,112 @@
+# P-014 PROD0 (coverage only) — pre-registration
+
+Written 2026-10-21 12:40 +05, before any gate run and before any production change. Base: `main` `22b29d5b`
+(merge of #422). Owner decision: `GO-P014-PROD0-COVERAGE-ONLY`. PROD1 (diagnostic semantics) stays forbidden.
+
+**Budget.** 0.5 agent-day to the next kill-gate, counted from 12:35. STOP at 16:35, not extended. When the budget
+runs out, I commit what exists and the verdict is `INCONCLUSIVE-P014-PROD0`.
+
+## 1. What will be built (only if G0 and G1 pass)
+
+**Flag.** An opt-in extractor flag `--binding-coverage <file>`, for `.csproj` inputs. It writes the deterministic
+coverage sidecar of the Tiny PoC (#422) into `<file>`:
+- one `CSharpCompilation` **per project**, from the existing `obj/project.assets.json`, local targeting packs and
+  the global packages folder, with project references as `CompilationReference`s;
+- binding-site counts, unit status, reasons, reference manifest and conflicts;
+- the foreign-binding guard.
+
+**The mechanism.** It is the #422 instrument's code, moved into the extractor as one new file (types public so
+that the evidence harness can call the same code). Behaviour changes allowed:
+- **Fail closed.** `unit_status = COMPLETE` requires all of the following: reference status `COMPLETE`, **and** no
+  source-set reason, **and** no unsupported item. Every other case is `UNSUPPORTED`, `REFERENCE_MISSING`
+  (including `CONFLICT_UNRESOLVED`) or `SOURCE_SET_INCOMPLETE`.
+- **No TPA substitution.** The process TPA is never used as a reference in this mode.
+- **Unsupported inputs.** A directory, a `.sln` or a `.cs` input gets a sidecar with a single `UNSUPPORTED` record
+  and no measurement.
+- **Separate from facts.** The sidecar is computed **after** the facts document is written, from fresh
+  compilations, and it never feeds the existing analysis.
+
+**Unchanged:**
+- the default behaviour, every existing flag, directory mode;
+- OwnIR, OWN001/OWN014/OWN050;
+- SARIF and exit codes;
+- the facts document: byte-identical with and without the flag;
+- the core, the Rust engine, goldens.
+
+A sidecar write failure is reported on stderr and does **not** change the exit code.
+
+## 2. Gates, in order (fixed now)
+
+### G0 — package-vs-package conflict against the SDK oracle (first, before any integration)
+
+**Fixture.** My own synthetic project, `net10.0-windows` with `UseWPF`, referencing `unchihugo.WPF-UI` 4.4.2 and
+`WPF-UI.Tray` 4.3.0. These are the packages that produce P5's `Wpf.Ui.dll` conflict: `unchihugo.WPF-UI` 4.4.2,
+AssemblyVersion 4.4.1.0, against the transitive `WPF-UI` 4.3.0, AssemblyVersion 4.3.0.0.
+- It is restored offline, with the global packages folder as the only source.
+- The oracle is `dotnet msbuild -t:FindReferenceAssembliesForReferences -getItem:ReferencePathWithRefAssemblies`.
+
+**PASS.** The #422 instrument's manifest equals the oracle's, compared by path and assembly version, including
+which `Wpf.Ui.dll` is chosen.
+
+**Outcomes:**
+- **Mismatch.** The resolver is **not** tuned to fit. The supported set is narrowed instead: any package-vs-package
+  conflict on the same file name becomes `CONFLICT_UNRESOLVED`, so the unit is not `COMPLETE`. That narrowing is
+  then what gets integrated.
+- **The fixture cannot restore offline.** G0 is `INCONCLUSIVE`, and the same narrowing applies.
+
+### G1 — the sidecar does not call P4/P5 fully checked
+
+Run on P4 and P5 with the #422 instrument data (`data/real/P*.exact.sidecar.json`).
+
+**PASS.** Every unit has `unit_status != COMPLETE`. Today's output has every unit at `SOURCE_SET_INCOMPLETE` and
+reference status `COMPLETE`.
+
+**KILL if** any unit is `COMPLETE` while it has a named source-set reason.
+
+### G2 — compatibility (after integration)
+
+1. **Facts.** For P4 and P5 (`.csproj`, `--flow-locals --no-project-refs`), and for the extractor's sample tree
+   `frontend/roslyn/samples` (directory mode), the facts document is **byte-identical** with and without
+   `--binding-coverage`. It must also equal the extractor built from `main` `22b29d5b` without the flag.
+2. **Controls.** K1, K2, K4, K5, K6, K7, K11, K12, F2.3, F2.4, F2.5 and the guard self-test are run against the
+   **production** code: the evidence harness references the built extractor assembly. K3, K8a, K8b, K8c, K9, K10
+   and G0 run through the production flag and are compared with the SDK oracle.
+   - All results must equal #422's.
+   - G0 must equal the oracle, or the narrowed rule must apply.
+3. **Isolation.** `foreign_binding = 0` in every control and in P4/P5.
+4. **Determinism.** The sidecar is byte-identical across 3 runs for P4 and P5.
+5. **Repository gates.**
+   - `ruff check .` passes.
+   - The repository's Python test suite passes, as far as it runs on this host.
+   - The extractor builds with no new warnings.
+
+### G3 — cost (limits not loosened from the Tiny PoC)
+
+- **Where.** P5 and P4, 3 separate processes each, through the production flag.
+- **Wall time.** Measured with and without the flag. The added time for the flag must be ≤ **3 ×** the #422
+  `legacy-merged` warm median measured in the same session. In practice, the exact-mode warm cost must stay within
+  the #422 limit: P5 warm exact ≤ 3 × legacy.
+- **Peak working set.** ≤ **2.0 GB**.
+- **Reported:** the extractor's total wall time with and without the flag.
+
+## 3. Verdict
+
+- **`PASS-P014-PROD0`.** G0 is PASS, or G0 is resolved by the pre-registered narrowing, **and** G1, G2 and G3 hold.
+- **`KILL-P014-PROD0`.** Any of:
+  - a facts byte difference;
+  - a foreign binding, or a silent false binding;
+  - G1 fails;
+  - the cost limit is exceeded;
+  - a forbidden action is needed.
+- **`INCONCLUSIVE-P014-PROD0`.** The budget runs out, or a gate is undecidable because an input is missing.
+
+A PASS allows **only** the opt-in coverage flag. It does not switch the extractor to the new resolver, and it does
+not feed any new fact to diagnostics.
+
+## 4. Not done
+
+- Restore or build of third-party projects; any network access.
+- MSBuild evaluation of P4/P5.
+- Changes to OwnIR, the core, the Rust engine, goldens or SARIF.
+- Reopening #407.
+- Any change to the lifetime model.

docs/evidence/p014-prod0-2026-10/01-review-falsifiers.md

@@ -0,0 +1,32 @@
+# P-014 PROD0 — adversarial review falsifiers (pre-registration addendum)
+
+Written 2026-10-21 15:12 +05, before any run.
+- **Trigger.** The owner's code review of #423 at `f84943d`: `CI-PASS / CODE-REVIEW-HOLD / NO-MERGE`.
+- **Budget.** 0.1 agent-day, counted from 15:11. STOP at 16:00.
+- **Out of scope.** No sweep, no PROD1.
+
+The original pre-registration (`00-preregistration.md`, `6ec551f`) is **not** changed. This file adds three
+falsifiers against the binary built from `f84943d`'s sources.
+
+| # | Fixture (own, synthetic, restored offline) | The claim under test | Falsified if |
+|---|---|---|---|
+| F-PROD0-1 | `net8.0`, no `<DefineConstants>`, a source with `#if NET8_0 … #else … #endif` | a unit whose measured preprocessor branch may differ from the SDK's is never `COMPLETE` | the sidecar says `COMPLETE` |
+| F-PROD0-2 | `net8.0`, a source line `Console.WriteLine("/*probe:");` | text in an analysed source cannot stop the sidecar from being written | no sidecar is written, or the run fails |
+| F-PROD0-3 | `net8.0`, one `.cs` made unreadable for the current user (ACL deny read) | `files.unreadable > 0` excludes `COMPLETE` | `unreadable > 0` together with `COMPLETE` |
+
+## Consequence, fixed now
+
+- **F-PROD0-1 confirmed.** This is a silent false claim of completeness, which falls under PROD0's original KILL
+  ("silent false binding"). The report then records **`KILL-P014-PROD0`** for `f84943d`. That KILL stands even if a
+  fix follows.
+- **F-PROD0-2 or F-PROD0-3 confirmed.** Recorded as defects, not as a KILL by themselves.
+- **Fix gate.** It is allowed only as a new, separately recorded gate: the fix plus F-PROD0-1, F-PROD0-2 and
+  F-PROD0-3 re-run on the new head, plus all original G0–G3 checks re-run. The original PASS is not re-issued for
+  `f84943d`. Any new head needs CI again.
+- **Fix shape, fixed now (fail closed, no new semantics):**
+  - any `#if`/`#elif` directive in a unit's sources becomes `SOURCE_SET_INCOMPLETE(preprocessor-conditional)`;
+  - any unreadable source becomes `SOURCE_SET_INCOMPLETE(unreadable-source)`;
+  - the research probe-marker parsing is removed from the production path (kept only behind an explicit harness
+    switch, and bounds-checked).
+
+  No defines and no implicit usings are applied (#407 stays separate).

docs/evidence/p014-prod0-2026-10/02-review-result.md

@@ -0,0 +1,64 @@
+# P-014 PROD0 — adversarial review result
+
+**Verdict for `f84943d`: `KILL-P014-PROD0`.**
+- **What it replaces.** The `PASS-P014-PROD0` in `REPORT.md` was issued on G0–G3. It did not survive the owner's
+  code review.
+- **Rule.** Fixed in `01-review-falsifiers.md`, commit `b446be4` (15:11:50 +05), before any run.
+- **What is unchanged.** The original pre-registration and `REPORT.md` stay as they were, as the record of what
+  was claimed.
+
+## Runs [run, 15:13 +05]
+
+- **Binary.** The extractor built from `f84943d`'s sources. `BindingCoverage.cs` and `Program.cs` were compared
+  byte for byte with `git show f84943d:…`.
+- **Fixtures.** `fixtures/F1`, `F2`, `F3`: `net8.0`, restored offline from the global packages folder.
+- **Log.** `data/review_f84943d.log`.
+
+| # | Observed | Claim | Result |
+|---|---|---|---|
+| F-PROD0-1 | `#if NET8_0 … #else … #endif`, no `<DefineConstants>`: exit 0, sidecar written, **`unit_status = COMPLETE`**, no source-set reason | a unit whose measured preprocessor branch may differ from the SDK's is never `COMPLETE` | **falsified.** The SDK defines `NET8_0` for `net8.0` [owner review, SDK behaviour]. The extractor parses with no defines, so it measured the `#else` branch and called the unit complete |
+| F-PROD0-2 | a source line `System.Console.WriteLine("/*probe:");`: exit 0, **no sidecar**, stderr `ArgumentOutOfRangeException: length ('-56')` | text in an analysed source cannot stop the sidecar | **falsified.** The research probe-marker parsing in `Coverage.Measure` runs in production and does not check for the closing `*/` |
+| F-PROD0-3 | `B.cs` denied read by ACL: exit 0, sidecar written, **`files.unreadable = 1` and `unit_status = COMPLETE`** | `unreadable > 0` excludes `COMPLETE` | **falsified.** `UnitStatus` does not read `Unreadable`, and the source-set scan skips the unreadable file silently |
+
+**Not affected.** The facts document and the exit code. The flag still never changes them; F-PROD0-2's failure was
+caught and reported on stderr, as designed. The defects are in what the sidecar **claims**.
+
+## A further limit (from the review, by reading)
+
+`foreign_binding` is computed against an allowlist built from the **same compilation's** references
+(`Coverage.Allowed`). An assembly wrongly put into the manifest is therefore "allowed" by construction.
+- The counter catches leaks **between source units**; the #422 guard self-test shows that.
+- It does **not** independently prove that the manifest is right. The SDK-oracle comparisons (K3, K8a–c, K9, G0)
+  are the evidence for the manifest; `foreign_binding = 0` is not.
+- `REPORT.md` and #423 should not be read as claiming more.
+
+## Proposed fix gate `FIX0` (not started; needs the owner's GO)
+
+**Scope.** Fail-closed changes only. No defines and no implicit usings applied, no new semantics, no PROD1.
+
+| Change | Rule |
+|---|---|
+| Preprocessor | any `#if`/`#elif` directive in a unit's sources, found when the source set is scanned (so it propagates to project-reference parents), gives `SOURCE_SET_INCOMPLETE(preprocessor-conditional)` |
+| Unreadable source | a source the scan cannot read gives `SOURCE_SET_INCOMPLETE(unreadable-source)`; `Compile` also adds it if a later read fails |
+| Probe markers | removed from the production path. `Coverage.Measure` records probes only when the harness passes an explicit switch, and then with a bounds check |
+| `foreign_binding` | renamed in the report text only, as "cross-unit leak guard"; the sidecar field is unchanged. The manifest-correctness claim stays with the oracle checks |
+
+**Acceptance (all on the new head):**
+1. **The three falsifiers.**
+   - F-PROD0-1: `SOURCE_SET_INCOMPLETE` with `preprocessor-conditional`.
+   - F-PROD0-2: the sidecar is written.
+   - F-PROD0-3: `SOURCE_SET_INCOMPLETE` with `unreadable-source`.
+2. **G0–G3 re-run unchanged:**
+   - facts byte-identical with `main`;
+   - K1–K12 and the oracle fixtures;
+   - P4/P5 not `COMPLETE`;
+   - determinism;
+   - cost within the original limits.
+3. **Expected movements.** The only expected change in K-results is K7, whose `#if` now marks the unit
+   `SOURCE_SET_INCOMPLETE`. Any other difference is a FAIL.
+4. **CI** green again on the new head; `Owen: NEUTRAL` is the only accepted exception.
+
+**Budget, proposed.** 0.25 agent-day. **KILL** if any of:
+- a falsifier still holds;
+- facts change;
+- another unexpected K-result changes.