Skip to content

Commit 23e3203

Browse files
PhysShellPhysShell
authored
Merge pull request #363 from PhysShell/claude/p037-a2.1-relevance-fix
P-037 A2.1: guarded-fact sidecar (corrected), richer facts with zero MOS/verdict movement
2 parents 184dba5 + cd7e020 commit 23e3203

31 files changed

Lines changed: 15828 additions & 59 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3039,6 +3039,12 @@ jobs:
30393039
# re-hashed and removed again. No baseline is taken here.
30403040
python scripts/p037_evidence.py artifacts
30413041
python scripts/p037_evidence.py population --source repo --materialize --cleanup
3042+
# A2.1: the guarded-fact sidecar is validated and INERT. Every census
3043+
# shape and the samples compilation go through both engines three
3044+
# times (as emitted, stripped, deliberately contradictory) and the
3045+
# lowered/summaries/verdicts layers must not move. Needs the
3046+
# own-shadow-engine the artifacts step just built.
3047+
python scripts/p037_sidecar_inertness.py
30423048
# The Windows launcher is a separate implementation, not a wrapper around
30433049
# the shell one, so the Windows leg has to go through it to mean anything.
30443050
- name: Own.NET's own tree, through own-check.ps1 on the Rust core

‎corpus/p037-shapes/call-expression-statement/expected.json‎

Lines changed: 90 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,47 @@
11
{
22
"schema": "p037-fact-shape/1",
33
"shape": "call-expression-statement",
4-
"status": "pending_a2",
4+
"status": "anchored",
55
"why": "The heart of the a2 gap. The C# lowering emits a `call` op in exactly ONE place and only for `var x = Foo(...)` — a call whose RESULT binds to a local. `Inner(r, true);` as a STATEMENT produces no `call` node, which the recorded facts show: `Caller`'s body is `acquire:r`, `release:r` — the fabricated release — and no call at all. So F3 cannot be carried through the existing summary layer today: there is no node for a guarded summary to specialise.",
66
"a2_contract": "a2 emits a real `call` op for relevant first-party statement-level calls. This is also where a2's zero-semantic-cut risk lives, and it must be measured rather than hoped: a real `call` op is ALREADY semantically active and MOS reads it, so emitting one here can move an existing summary long before the guarded kernel is anywhere near. A verdict that happens to stay the same is not a pass — an unintended MOS collapsed-view change means a2 began the semantic cut early, and the answer is to isolate it or restage, never to note that the tests are green.",
7+
"a2_landed": "A2.1 landed the guarded-fact SIDECAR (`guarded_facts`, spec/OwnIR.md §5.2), not a body op: the legacy `body` stays authoritative through A2 and C+ canonicalizes the two views (docs/notes/p037-formal-kernel.md §10.3/§10.5). The `a2_expect` entries are this shape's contract, checked by name; `facts` pins the whole record byte for byte.",
8+
"a2_expect": [
9+
{
10+
"function": "ShapeStatementCall.Caller",
11+
"call": {
12+
"site": {
13+
"line": 26
14+
},
15+
"form": "statement",
16+
"callee": "ShapeStatementCall.Inner",
17+
"sig": "System.IO.Stream,System.Boolean",
18+
"first_party": true,
19+
"args": [
20+
{
21+
"param": 0,
22+
"kind": "var",
23+
"name": "r"
24+
},
25+
{
26+
"param": 1,
27+
"kind": "bool_const",
28+
"value": true
29+
}
30+
]
31+
}
32+
},
33+
{
34+
"function": "ShapeStatementCall.Inner",
35+
"guard": {
36+
"site": {
37+
"line": 17
38+
},
39+
"param": 1,
40+
"predicate": "truth",
41+
"negated": true
42+
}
43+
}
44+
],
745
"measured_at": "464308b",
846
"facts": {
947
"ShapeStatementCall.Inner": {
@@ -16,18 +54,66 @@
1654
"body": [
1755
"if:None@17",
1856
"then:release:s@19"
19-
]
57+
],
58+
"guarded_facts": {
59+
"version": 1,
60+
"calls": [],
61+
"guards": [
62+
{
63+
"site": {
64+
"line": 17,
65+
"column": 9
66+
},
67+
"param": 1,
68+
"predicate": "truth",
69+
"negated": true
70+
}
71+
]
72+
}
2073
},
2174
"ShapeStatementCall.Caller": {
2275
"params": null,
2376
"body": [
2477
"acquire:r@25",
2578
"release:r@26"
26-
]
79+
],
80+
"guarded_facts": {
81+
"version": 1,
82+
"calls": [
83+
{
84+
"site": {
85+
"line": 26,
86+
"column": 9
87+
},
88+
"statement_line": 26,
89+
"form": "statement",
90+
"callee": "ShapeStatementCall.Inner",
91+
"sig": "System.IO.Stream,System.Boolean",
92+
"first_party": true,
93+
"args": [
94+
{
95+
"param": 0,
96+
"kind": "var",
97+
"name": "r"
98+
},
99+
{
100+
"param": 1,
101+
"kind": "bool_const",
102+
"value": true
103+
}
104+
]
105+
}
106+
],
107+
"guards": []
108+
}
27109
}
28110
},
29111
"verdict": {
30112
"rust": [],
31113
"python": []
32-
}
114+
},
115+
"status_history": [
116+
"pending_a2 (recorded at 464308b)",
117+
"anchored (A2.1 sidecar)"
118+
]
33119
}

‎corpus/p037-shapes/extension-receiver/expected.json‎

Lines changed: 65 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,37 @@
11
{
22
"schema": "p037-fact-shape/1",
33
"shape": "extension-receiver",
4-
"status": "pending_a2",
4+
"status": "anchored",
55
"why": "A reduced extension method. Roslyn's reduced symbol drops `this` from Parameters while the summary lives on the UNREDUCED declaration, where the receiver is parameter 0.\n\nTwo things measured here, and the second was a surprise. (1) `CallReleasesReceiver` — the `ConsumesParam` consumer that handles this shape — is reached ONLY from two sites gated on `ThisFieldName(...)`: it is part of the FIELD disposal detector and never runs on a local. (2) Consequently `var s = ...; s.WaitForDispose(5);` is charged OWN001 even when the extension disposes its receiver UNCONDITIONALLY — verified with an unguarded probe, so it is not the guard doing it. That is a pre-existing false positive of exactly the family P-037 addresses (a first-party callee that releases, unrecognised), arriving through the RECEIVER rather than the argument. It is not A1's to fix and is recorded here so it is not mistaken for something A1 caused.",
66
"a2_contract": "a2 synthesises the receiver binding against the UNREDUCED declaration: receiver -> declared parameter 0, `timeout` -> declared parameter 1. Without it `CallReleasesReceiver` can never be honestly retired — the guarded summaries would be complete except for one old tunnel under the fence, on the field path where nobody is looking.",
7+
"a2_landed": "A2.1 landed the guarded-fact SIDECAR (`guarded_facts`, spec/OwnIR.md §5.2), not a body op: the legacy `body` stays authoritative through A2 and C+ canonicalizes the two views (docs/notes/p037-formal-kernel.md §10.3/§10.5). The `a2_expect` entries are this shape's contract, checked by name; `facts` pins the whole record byte for byte.",
8+
"a2_expect": [
9+
{
10+
"function": "ShapeExtensionReceiver.Caller",
11+
"call": {
12+
"site": {
13+
"line": 23
14+
},
15+
"callee": "ShapeExtensionReceiver.WaitForDispose",
16+
"sig": "System.IO.Stream,System.Int32",
17+
"args": [
18+
{
19+
"param": 0,
20+
"kind": "var",
21+
"name": "s"
22+
},
23+
{
24+
"param": 1,
25+
"kind": "opaque"
26+
}
27+
]
28+
}
29+
},
30+
{
31+
"function": "ShapeExtensionReceiver.WaitForDispose",
32+
"guarded_facts": "absent"
33+
}
34+
],
735
"measured_at": "464308b",
836
"facts": {
937
"ShapeExtensionReceiver.WaitForDispose": {
@@ -16,14 +44,43 @@
1644
"body": [
1745
"if:None@14",
1846
"then:release:self@16"
19-
]
47+
],
48+
"guarded_facts": null
2049
},
2150
"ShapeExtensionReceiver.Caller": {
2251
"params": null,
2352
"body": [
2453
"acquire:s@22",
2554
"use:s@23"
26-
]
55+
],
56+
"guarded_facts": {
57+
"version": 1,
58+
"calls": [
59+
{
60+
"site": {
61+
"line": 23,
62+
"column": 9
63+
},
64+
"statement_line": 23,
65+
"form": "statement",
66+
"callee": "ShapeExtensionReceiver.WaitForDispose",
67+
"sig": "System.IO.Stream,System.Int32",
68+
"first_party": true,
69+
"args": [
70+
{
71+
"param": 0,
72+
"kind": "var",
73+
"name": "s"
74+
},
75+
{
76+
"param": 1,
77+
"kind": "opaque"
78+
}
79+
]
80+
}
81+
],
82+
"guards": []
83+
}
2784
}
2885
},
2986
"verdict": {
@@ -33,5 +90,9 @@
3390
"python": [
3491
"OWN001:warning@22"
3592
]
36-
}
93+
},
94+
"status_history": [
95+
"pending_a2 (recorded at 464308b)",
96+
"anchored (A2.1 sidecar)"
97+
]
3798
}

‎corpus/p037-shapes/guard-bool-const-false/expected.json‎

Lines changed: 81 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,38 @@
11
{
22
"schema": "p037-fact-shape/1",
33
"shape": "guard-bool-const-false",
4-
"status": "pending_a2",
4+
"status": "anchored",
55
"why": "The same call with `false`. Present so the two constants are distinguishable in the facts: a single `is a constant` bit would collapse the exact distinction cell selection turns on, and would do it invisibly.",
66
"a2_contract": "{\"param\":1,\"kind\":\"bool_const\",\"value\":false}; Rust derives `const-neg`.",
7+
"a2_landed": "A2.1 landed the guarded-fact SIDECAR (`guarded_facts`, spec/OwnIR.md §5.2), not a body op: the legacy `body` stays authoritative through A2 and C+ canonicalizes the two views (docs/notes/p037-formal-kernel.md §10.3/§10.5). The `a2_expect` entries are this shape's contract, checked by name; `facts` pins the whole record byte for byte.",
8+
"a2_expect": [
9+
{
10+
"function": "ShapeConstFalse.Caller",
11+
"call": {
12+
"callee": "ShapeConstFalse.Inner",
13+
"args": [
14+
{
15+
"param": 0,
16+
"kind": "var",
17+
"name": "r"
18+
},
19+
{
20+
"param": 1,
21+
"kind": "bool_const",
22+
"value": false
23+
}
24+
]
25+
}
26+
},
27+
{
28+
"function": "ShapeConstFalse.Inner",
29+
"guard": {
30+
"param": 1,
31+
"predicate": "truth",
32+
"negated": true
33+
}
34+
}
35+
],
736
"measured_at": "464308b",
837
"facts": {
938
"ShapeConstFalse.Inner": {
@@ -16,18 +45,66 @@
1645
"body": [
1746
"if:None@10",
1847
"then:release:s@12"
19-
]
48+
],
49+
"guarded_facts": {
50+
"version": 1,
51+
"calls": [],
52+
"guards": [
53+
{
54+
"site": {
55+
"line": 10,
56+
"column": 9
57+
},
58+
"param": 1,
59+
"predicate": "truth",
60+
"negated": true
61+
}
62+
]
63+
}
2064
},
2165
"ShapeConstFalse.Caller": {
2266
"params": null,
2367
"body": [
2468
"acquire:r@18",
2569
"release:r@19"
26-
]
70+
],
71+
"guarded_facts": {
72+
"version": 1,
73+
"calls": [
74+
{
75+
"site": {
76+
"line": 19,
77+
"column": 9
78+
},
79+
"statement_line": 19,
80+
"form": "statement",
81+
"callee": "ShapeConstFalse.Inner",
82+
"sig": "System.IO.Stream,System.Boolean",
83+
"first_party": true,
84+
"args": [
85+
{
86+
"param": 0,
87+
"kind": "var",
88+
"name": "r"
89+
},
90+
{
91+
"param": 1,
92+
"kind": "bool_const",
93+
"value": false
94+
}
95+
]
96+
}
97+
],
98+
"guards": []
99+
}
27100
}
28101
},
29102
"verdict": {
30103
"rust": [],
31104
"python": []
32-
}
105+
},
106+
"status_history": [
107+
"pending_a2 (recorded at 464308b)",
108+
"anchored (A2.1 sidecar)"
109+
]
33110
}

0 commit comments

Comments
 (0)