Skip to content

Commit fb06adc

Browse files
PhysShellclaude
PhysShell
and
claude
authored
Merge pull request #381 from PhysShell/ccr-d1573cc1-g41e75
fix: only a definite release makes a call-site handoff (INF-S2, #380) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp
2 parents 23e3203 + 410431a commit fb06adc

21 files changed

Lines changed: 1372 additions & 437 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -802,6 +802,14 @@ jobs:
802802
env:
803803
OWN_TIERB_REQUIRED: "1"
804804
run: python tests/test_extractor_columns.py
805+
- name: Guarded release is not a call-site handoff (INF-S2, #380)
806+
# A callee that releases its parameter only under a guard is a PARTIAL release, so
807+
# its call must not be lowered as the caller's `release` (the fabricated `must`),
808+
# while a definite consumer stays a handoff. Facts and verdicts on the real
809+
# extractor; REQUIRED here, skips cleanly in the offline Tier-A job.
810+
env:
811+
OWN_TIERB_REQUIRED: "1"
812+
run: python tests/test_guarded_consume.py
805813
- name: S2 step 10 analyzer-delta verifier (Tier B, full public CLI)
806814
env:
807815
OWN_TIERB_REQUIRED: "1"

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

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,13 @@
33
"control": "gv4-control-aliased-self-null",
44
"p037": "§8 row 19 — G-V4, writably aliased self-null resource parameter",
55
"classification": "KNOWN_FALSE_POSITIVE",
6-
"measured_at": "70189a3",
6+
"measured_at": "f164dd3",
77
"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",
88
"call_site_line": 29,
99
"defensive_dispose_line": 30,
1010
"current": {
11-
"findings": [
12-
"OWN003"
13-
],
14-
"fabricated_release_at_call_site": true
11+
"findings": [],
12+
"fabricated_release_at_call_site": false
1513
},
1614
"post_a1": {
1715
"findings": [],
@@ -37,7 +35,34 @@
3735
}
3836
},
3937
"result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs."
38+
},
39+
{
40+
"at": "f164dd3",
41+
"on": "2026-09-29",
42+
"why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.",
43+
"engines": {
44+
"python": {
45+
"findings": [],
46+
"fabricated_release_at_call_site": false
47+
},
48+
"rust": {
49+
"findings": [],
50+
"fabricated_release_at_call_site": false
51+
}
52+
},
53+
"superseded_current": {
54+
"measured_at": "70189a3",
55+
"current": {
56+
"findings": [
57+
"OWN003"
58+
],
59+
"fabricated_release_at_call_site": true
60+
}
61+
},
62+
"result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.",
63+
"classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied"
4064
}
4165
],
42-
"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."
66+
"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.",
67+
"resolved_by": "#380 (fix commit f164dd3)"
4368
}

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

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,13 @@
33
"control": "gv4-control-mutated-guard",
44
"p037": "§8 row 18a — G-V4, mutated guard (direct write)",
55
"classification": "KNOWN_FALSE_POSITIVE",
6-
"measured_at": "70189a3",
6+
"measured_at": "f164dd3",
77
"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",
88
"call_site_line": 39,
99
"defensive_dispose_line": 40,
1010
"current": {
11-
"findings": [
12-
"OWN003"
13-
],
14-
"fabricated_release_at_call_site": true
11+
"findings": [],
12+
"fabricated_release_at_call_site": false
1513
},
1614
"post_a1": {
1715
"findings": [],
@@ -37,7 +35,34 @@
3735
}
3836
},
3937
"result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs."
38+
},
39+
{
40+
"at": "f164dd3",
41+
"on": "2026-09-29",
42+
"why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.",
43+
"engines": {
44+
"python": {
45+
"findings": [],
46+
"fabricated_release_at_call_site": false
47+
},
48+
"rust": {
49+
"findings": [],
50+
"fabricated_release_at_call_site": false
51+
}
52+
},
53+
"superseded_current": {
54+
"measured_at": "70189a3",
55+
"current": {
56+
"findings": [
57+
"OWN003"
58+
],
59+
"fabricated_release_at_call_site": true
60+
}
61+
},
62+
"result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.",
63+
"classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied"
4064
}
4165
],
42-
"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."
66+
"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.",
67+
"resolved_by": "#380 (fix commit f164dd3)"
4368
}

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

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,13 @@
33
"control": "gv4-control-ref-alias-guard",
44
"p037": "§8 row 18b — G-V4, writable ref-alias of the guard",
55
"classification": "KNOWN_FALSE_POSITIVE",
6-
"measured_at": "70189a3",
6+
"measured_at": "f164dd3",
77
"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",
88
"call_site_line": 36,
99
"defensive_dispose_line": 37,
1010
"current": {
11-
"findings": [
12-
"OWN003"
13-
],
14-
"fabricated_release_at_call_site": true
11+
"findings": [],
12+
"fabricated_release_at_call_site": false
1513
},
1614
"post_a1": {
1715
"findings": [],
@@ -37,7 +35,34 @@
3735
}
3836
},
3937
"result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs."
38+
},
39+
{
40+
"at": "f164dd3",
41+
"on": "2026-09-29",
42+
"why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.",
43+
"engines": {
44+
"python": {
45+
"findings": [],
46+
"fabricated_release_at_call_site": false
47+
},
48+
"rust": {
49+
"findings": [],
50+
"fabricated_release_at_call_site": false
51+
}
52+
},
53+
"superseded_current": {
54+
"measured_at": "70189a3",
55+
"current": {
56+
"findings": [
57+
"OWN003"
58+
],
59+
"fabricated_release_at_call_site": true
60+
}
61+
},
62+
"result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.",
63+
"classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied"
4064
}
4165
],
42-
"note": "Same mechanism as row 18a; the alias write must disqualify the guard (fail-closed) and the call must not fabricate a consume."
66+
"note": "Same mechanism as row 18a; the alias write must disqualify the guard (fail-closed) and the call must not fabricate a consume.",
67+
"resolved_by": "#380 (fix commit f164dd3)"
4368
}

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

Lines changed: 28 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@
33
"control": "legacy-honesty-else-unresolved-forward",
44
"p037": "G-T2b class 3 — guarded local release, unresolved forward on the other branch",
55
"classification": "VERDICT_COMPATIBLE_VALUE_DIFFERENCE",
6-
"measured_at": "70189a3",
6+
"measured_at": "f164dd3",
77
"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",
88
"call_site_line": 41,
99
"defensive_dispose_line": null,
1010
"current": {
1111
"findings": [],
12-
"fabricated_release_at_call_site": true
12+
"fabricated_release_at_call_site": false
1313
},
1414
"post_a1": {
1515
"findings": [],
@@ -31,7 +31,32 @@
3131
}
3232
},
3333
"result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs."
34+
},
35+
{
36+
"at": "f164dd3",
37+
"on": "2026-09-29",
38+
"why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.",
39+
"engines": {
40+
"python": {
41+
"findings": [],
42+
"fabricated_release_at_call_site": false
43+
},
44+
"rust": {
45+
"findings": [],
46+
"fabricated_release_at_call_site": false
47+
}
48+
},
49+
"superseded_current": {
50+
"measured_at": "70189a3",
51+
"current": {
52+
"findings": [],
53+
"fabricated_release_at_call_site": true
54+
}
55+
},
56+
"result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.",
57+
"classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied"
3458
}
3559
],
36-
"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."
60+
"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.",
61+
"resolved_by": "#380 (fix commit f164dd3)"
3762
}

‎corpus/p037-shapes/README.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,3 +32,18 @@ of aggregated into a number.
3232

3333
Checked by `scripts/p037_fact_shapes.py`, which names its engine explicitly
3434
(#262 Stage 3) and runs one extractor invocation per case.
35+
36+
## Baseline transitions
37+
38+
A record that moves because a step *meant* to move it is re-recorded
39+
deliberately, with the move written into the record itself
40+
(`baseline_transitions[]`, which keeps the superseded facts, verdicts and
41+
`a2_expect` verbatim). An `a2_expect` entry of the form
42+
`{"function": …, "record": "absent"}` asserts that a record is gone on
43+
purpose; the checker fails by name if it comes back.
44+
45+
- **#380** (`23e3203` → `f164dd3`): an independent INF-S2 fix stopped lowering
46+
a guarded release as a call-site release. Seven caller records and their
47+
sidecars disappear, and two wrappers move `release` → `use`. This is not a
48+
P-037 implementation, not a #304 reopen, and not evidence that A2 holds.
49+
See [`docs/notes/p037-fact-shape-baseline-transition-380.md`](../../docs/notes/p037-fact-shape-baseline-transition-380.md).

0 commit comments

Comments
 (0)