Skip to content

Commit ce2e6bc

Browse files
committed
P-037 controls: owner ruling (no pre-cutover ConsumesParam fix), explicit current/post-A1 expectations, two-layer checker
Owner ruling recorded verbatim (docs/notes/p037-formal-kernel.md §8.2): the three measured false-OWN003 controls are pre-A1 regression anchors, not authorization for a pre-cutover fix; Roslyn ConsumesParam semantics do not change before P-022 Stage 3 — the freeze is on verdict-changing inference, the shared-extractor location is no exception, and #305 (bounded P1 false-negative soundness holes under the pre-cutover floor doctrine) is not controlling precedent for a false-positive precision failure that is A1's first target. Consequences: each control now carries expected.json with a classification (KNOWN_FALSE_POSITIVE x3, VERDICT_COMPATIBLE_VALUE_DIFFERENCE for the class-3 shape), the `current` record measured at 70189a3 and the `post_a1` acceptance, replacing the empty expected-diagnostics.txt that would have read as clean today. scripts/p037_controls.py (held to mypy --strict) verifies them on two layers — the fabricated `release` op at the call site in the emitted facts, and the finding codes at warning severity — so a summary engine can never compensate a bad extractor fact and hand A1 a green end-to-end result over a broken seam. Today: current record 4/4 match; --post-a1 fails 4/4 as expected until A1 lands after Stage 3. All four controls carry the fabricated release at the call site today, the class-3 shape included (where it also suppresses the OWN051 advisory). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb
1 parent 7751d1b commit ce2e6bc

12 files changed

Lines changed: 314 additions & 18 deletions

File tree

‎corpus/p036-bakeoff/README.md‎

Lines changed: 23 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -49,23 +49,34 @@ from every preregistered decision predicate and read only in
4949
## G-V4 / trusted-input negative controls and the class-3 shape (class 4)
5050

5151
Not bug fixtures and not bakeoff cases: each `control.cs` carries an honest
52-
defensive dispose that a *fabricated* `must` would charge a false OWN003,
53-
so the required verdict at `--severity warning` is **no findings** (the empty
54-
`expected-diagnostics.txt` is the post-A1 target). They are the executable
55-
form of P-037 §8 rows 18–19 and G-T2b class 3, and A1's acceptance items 5
56-
and 8 (`docs/notes/p037-formal-kernel.md` §8.1). Measured on Owen today
57-
(`70189a3`, `scripts/own-check.sh --severity warning`):
52+
defensive dispose that a *fabricated* `must` would charge a false OWN003.
53+
Each directory holds `expected.json` with **both** the `current` record
54+
(measured on Owen at `70189a3`) and the `post_a1` acceptance, plus a
55+
`classification` — three are `KNOWN_FALSE_POSITIVE`, the class-3 shape is
56+
`VERDICT_COMPATIBLE_VALUE_DIFFERENCE` — so the evidence lies about neither
57+
today nor the target. `scripts/p037_controls.py` verifies them on two layers
58+
(the fabricated `release` op at the call site in the emitted facts; the
59+
finding codes at `--severity warning`): the default mode must pass today,
60+
`--post-a1` is the acceptance A1 discharges after P-022 Stage 3 and fails
61+
until then. They are the executable form of P-037 §8 rows 18–19 and G-T2b
62+
class 3, and A1's acceptance items 5 and 8
63+
(`docs/notes/p037-formal-kernel.md` §8.1). Owner ruling (2026-09-18): the
64+
three false positives are pre-A1 regression anchors, **not** authorization
65+
for a pre-cutover `ConsumesParam` fix — the P-022 freeze is on
66+
verdict-changing inference, and the shared-extractor location is no
67+
exception. Measured today:
5868

5969
| control | P-037 | today | why |
6070
|---|---|---|---|
6171
| `gv4-control-mutated-guard` | §8 row 18a | **OWN003 (false)** on `r.Dispose()` | the extractor's flow-insensitive `ConsumesParam` lowers `Inner(p, g)` to a release because `Inner` disposes on *some* path — the may-as-must hole, A1's first bug; the mutated guard never even gets a say |
6272
| `gv4-control-ref-alias-guard` | §8 row 18b | **OWN003 (false)** | same mechanism |
6373
| `gv4-control-aliased-self-null` | §8 row 19 | **OWN003 (false)** on `s.Dispose()` | `q.Dispose()` somewhere in `Close` ⇒ the call is a release of the caller's argument, which the alias write makes untrue |
64-
| `legacy-honesty-else-unresolved-forward` | G-T2b class 3 | 0 findings | plain + OWN051 for the unknown guard, as required; the value-level pin (`unknown`, never repaired to `may`) is the kernel test `k11_finding_release_priority_drops_an_unresolved_forward` |
74+
| `legacy-honesty-else-unresolved-forward` | G-T2b class 3 | 0 findings at warning severity — but the facts layer shows the same fabricated release at the call site, which today also suppresses the OWN051 advisory | verdict-compatible today and after A1; after A1 the call is plain + OWN051 with no release op; the value-level pin (`unknown`, never repaired to `may`) is the kernel test `k11_finding_release_priority_drops_an_unresolved_forward` |
6575

66-
Three of four are therefore **red today**: they pin a production false-positive
67-
class that A1's first target removes, and they must turn green without any
68-
of them turning into a fabricated consume elsewhere. Owner ruling: nothing in
69-
the extractor, the engines or the launcher surfaces changes before P-022
70-
Stage 3; these anchors wait with A1.
76+
Three of four are therefore **red today** on the end-to-end layer and all
77+
four on the facts layer: they pin a production false-positive class that
78+
A1's first target removes, and they must turn green on both layers without
79+
any of them turning into a fabricated consume elsewhere. Nothing in the
80+
extractor, the engines or the launcher surfaces changes before P-022 Stage
81+
3; these anchors wait with A1.
7182

‎corpus/p036-bakeoff/gv4-control-aliased-self-null/expected-diagnostics.txt‎

Whitespace-only changes.
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"schema": "p037-control-expectation/1",
3+
"control": "gv4-control-aliased-self-null",
4+
"p037": "§8 row 19 — G-V4, writably aliased self-null resource parameter",
5+
"classification": "KNOWN_FALSE_POSITIVE",
6+
"measured_at": "70189a3",
7+
"owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3",
8+
"call_site_line": 29,
9+
"defensive_dispose_line": 30,
10+
"current": {
11+
"findings": [
12+
"OWN003"
13+
],
14+
"fabricated_release_at_call_site": true
15+
},
16+
"post_a1": {
17+
"findings": [],
18+
"fabricated_release_at_call_site": false
19+
},
20+
"note": "Close disposes r through the alias, not the caller's s; today Close(s, other) is lowered to a release of s (may-as-must), so s.Dispose() is a false OWN003. After A1: no split for the aliased q, no release op at the call, the dispose is clean."
21+
}

‎corpus/p036-bakeoff/gv4-control-mutated-guard/expected-diagnostics.txt‎

Whitespace-only changes.
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"schema": "p037-control-expectation/1",
3+
"control": "gv4-control-mutated-guard",
4+
"p037": "§8 row 18a — G-V4, mutated guard (direct write)",
5+
"classification": "KNOWN_FALSE_POSITIVE",
6+
"measured_at": "70189a3",
7+
"owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3",
8+
"call_site_line": 39,
9+
"defensive_dispose_line": 40,
10+
"current": {
11+
"findings": [
12+
"OWN003"
13+
],
14+
"fabricated_release_at_call_site": true
15+
},
16+
"post_a1": {
17+
"findings": [],
18+
"fabricated_release_at_call_site": false
19+
},
20+
"note": "Today the extractor lowers Outer(r, true) to a release of r (may-as-must ConsumesParam), so the honest r.Dispose() is a false OWN003. After A1 the call must carry no release op and lower to plain + OWN051; the dispose is clean."
21+
}

‎corpus/p036-bakeoff/gv4-control-ref-alias-guard/expected-diagnostics.txt‎

Whitespace-only changes.
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"schema": "p037-control-expectation/1",
3+
"control": "gv4-control-ref-alias-guard",
4+
"p037": "§8 row 18b — G-V4, writable ref-alias of the guard",
5+
"classification": "KNOWN_FALSE_POSITIVE",
6+
"measured_at": "70189a3",
7+
"owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3",
8+
"call_site_line": 36,
9+
"defensive_dispose_line": 37,
10+
"current": {
11+
"findings": [
12+
"OWN003"
13+
],
14+
"fabricated_release_at_call_site": true
15+
},
16+
"post_a1": {
17+
"findings": [],
18+
"fabricated_release_at_call_site": false
19+
},
20+
"note": "Same mechanism as row 18a; the alias write must disqualify the guard (fail-closed) and the call must not fabricate a consume."
21+
}

‎corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/expected-diagnostics.txt‎

Whitespace-only changes.
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"schema": "p037-control-expectation/1",
3+
"control": "legacy-honesty-else-unresolved-forward",
4+
"p037": "G-T2b class 3 — guarded local release, unresolved forward on the other branch",
5+
"classification": "VERDICT_COMPATIBLE_VALUE_DIFFERENCE",
6+
"measured_at": "70189a3",
7+
"owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3",
8+
"call_site_line": 41,
9+
"defensive_dispose_line": null,
10+
"current": {
11+
"findings": [],
12+
"fabricated_release_at_call_site": true
13+
},
14+
"post_a1": {
15+
"findings": [],
16+
"fabricated_release_at_call_site": false
17+
},
18+
"note": "0 findings at warning severity today AND after A1 (class 3 is verdict-equivalent). The facts layer differs: today the extractor lowers M(r, flag, sink) to a release (may-as-must) and even the OWN051 advisory is suppressed; after A1 the guarded value is unknown, the call is plain + OWN051 at note level, and no release op may appear at the call site. The value-level pin (unknown, never repaired to may) is the kernel test k11_finding_release_priority_drops_an_unresolved_forward."
19+
}

‎docs/notes/p037-formal-kernel.md‎

Lines changed: 67 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -284,14 +284,20 @@ A1 ACCEPTANCE
284284
4. Application on FINALIZED state only: a raw solver cell is never consumable
285285
(kernel K7 witness ported as a production test).
286286
5. G-V4 failures — mutable / ref / out / aliased guard: the edge degrades to
287-
opaque, never fabricates must (P-037 §8 rows 18-19 as fixtures).
287+
opaque, never fabricates must (P-037 §8 rows 18-19 as fixtures) — on BOTH
288+
layers: no fabricated `release` op at the call site in the emitted facts
289+
(extractor-fact acceptance) AND no false OWN003 end to end
290+
(`scripts/p037_controls.py --post-a1`, the three KNOWN_FALSE_POSITIVE
291+
controls turning red -> green).
288292
6. The formal kernel's twins run over the SAME production functions, not a
289293
copy: the kernel is moved, its properties move with it.
290294
7. Kani: value-level harnesses mandatory (PR gate); solver-heavy harnesses
291295
opt-in / nightly.
292296
8. The F1 pin: `if (g) p.Dispose(); else Extern(p);` with Extern unresolved
293297
yields the collapsed value UNKNOWN (class 3), lowered to plain + OWN051 —
294-
an implementation that "repairs" it to legacy's optimistic MAY fails.
298+
an implementation that "repairs" it to legacy's optimistic MAY fails;
299+
on the facts layer the call site carries no release op (today it does:
300+
the class-3 control's `current` record), and the OWN051 advisory appears.
295301
```
296302

297303
**The gate, as a REPOSITORY FACT that needs a ruling before any production
@@ -431,7 +437,62 @@ target, now with
431437
three executable witnesses that fail until it is fixed and must pass
432438
without a fabricated consume appearing anywhere else. It lives in the
433439
extractor (`frontend/roslyn/OwnSharp.Extractor/Program.cs`), which both
434-
engines share — a fix there would not split the compare gate, but it is
435-
launcher-visible behaviour and therefore waits, per the ruling, unless the
436-
owner rules otherwise for the extractor-side floor specifically (the #305
437-
precedent).
440+
engines share. The owner ruled on the carve-out question the same day:
441+
442+
```text
443+
OWNER RULING — ConsumesParam false OWN003 controls (2026-09-18)
444+
445+
The three newly measured false-OWN003 cases are accepted as
446+
pre-A1 regression anchors, not as authorization for a pre-cutover fix.
447+
448+
Do NOT change Roslyn ConsumesParam semantics before P-022 Stage 3.
449+
450+
Reason:
451+
- the defect is launcher-visible;
452+
- fixing it changes interprocedural inference verdicts;
453+
- the P-022 freeze is on verdict-changing inference, not merely
454+
on Python/Rust divergence;
455+
- the shared-extractor location therefore does not create an exception.
456+
457+
#305 is not controlling precedent:
458+
- it repaired bounded P1 false-negative soundness holes in teardown
459+
crediting under the explicit pre-cutover floor doctrine;
460+
- this defect is a false-positive / precision failure in cross-call
461+
consume inference and is the first target of post-cutover A1.
462+
463+
Keep the three failing controls exactly as measured.
464+
They become mandatory red→green acceptance witnesses for A1 after Stage 3.
465+
466+
No production fix before cutover.
467+
```
468+
469+
In the owner's words on why a "small bounded fix" is a trap here: the
470+
moment `ConsumesParam` is restricted to unconditional disposes, the next
471+
questions are `if (x) Dispose(); else Dispose();`, early return,
472+
`try/finally`, the self-null guard, forwarding helpers, exception paths,
473+
guards on parameters vs locals vs fields, callee forwarding into another
474+
consumer — three patches later the guarded-summary semantics is being
475+
written into the Roslyn extractor under the name of a bugfix, which is the
476+
road the bakeoff already mapped. The freeze stopped exactly the kind of work
477+
it exists to stop; drilling neat holes in it right after it first worked
478+
would be comic.
479+
480+
**Consequences applied.** The controls no longer carry an empty
481+
`expected-diagnostics.txt` that would read as "clean today": each has an
482+
`expected.json` with `classification` (`KNOWN_FALSE_POSITIVE` for the three
483+
G-V4 controls, `VERDICT_COMPATIBLE_VALUE_DIFFERENCE` for the class-3 shape),
484+
the `current` record measured at `70189a3`, and the `post_a1` acceptance —
485+
so the evidence lies about neither. `scripts/p037_controls.py` checks them
486+
on **two layers**, because the facts showed the defect is decided before the
487+
engine boundary: (1) the extractor-fact layer — does the call site carry a
488+
fabricated `release` op in the emitted facts; (2) the end-to-end layer — the
489+
finding codes at `--severity warning`. Default mode checks `current` and
490+
must pass today (a mismatch means Owen's behaviour moved and the record must
491+
be re-measured, never silently); `--post-a1` checks the acceptance and is
492+
expected to fail until A1 lands after Stage 3. Two layers so that a Rust
493+
summary engine can never compensate a bad extractor fact with another
494+
heuristic and hand A1 a green end-to-end result over a still-broken seam.
495+
Measured today, all four controls carry the fabricated release at the call
496+
site — including the class-3 shape, where it also suppresses the OWN051
497+
advisory the unknown guard should earn (0 findings either way at warning
498+
severity: verdict-compatible, value-different, exactly class 3).

0 commit comments

Comments
 (0)