Skip to content

Commit 2fcd402

Browse files
claudeclaude
committed
P-037 A2.2: result — stop point reached, R escalated; pin the raw argument facts
docs/notes/p037-a2.2-call-facts.md §9 records the result against the pre-registered contract (§§1-8 left as registered): - N1..N8 hold, checked per shape by name; - M2 zero semantic cut: MOS and verdicts UNCHANGED on both engines; - the boxing-cast defect the pre-registered control caught; - R (record-level absence) classified case 5 and escalated for an owner decision, not coded around. Coverage fix, after registration: null_literal, object_creation and call_result were counted as covered at A2.1 on the strength of probes, but no census shape pinned the Roslyn side, and test_p037_sidecar checks only the validator. New anchored shape corpus/p037-shapes/arg-raw-facts, recorded at the base 23e3203 first and byte-identical at the treatment; three named a2_expect checks; a mutant call_result -> fresh_owned expectation fails the check. Inert on both engines (4 sidecars). Refs #304 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KmiyfrkaG9sJruTcshM2oq
1 parent ee2ee53 commit 2fcd402

3 files changed

Lines changed: 387 additions & 4 deletions

File tree

‎corpus/p037-shapes/arg-raw-facts/case.cs‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// Required control (A2.2, #304): the raw argument facts that are NOT a
2+
// handle. A relevant call (the local `r` flows into it) carries, in its other
3+
// slot, `null` -> null_literal, `new MemoryStream()` -> object_creation, and
4+
// a call's result -> call_result{callee, sig}. Freshness of that result is a
5+
// summary conclusion, so no `fresh_owned` is ever written. The creation and
6+
// the inner call have no handle argument of their own, so neither gets a
7+
// calls[] record: G-A records a creation only when a handle flows into it.
8+
using System.IO;
9+
10+
static class ShapeRawArgFacts
11+
{
12+
static void Keep(Stream s, Stream? other, bool keep)
13+
{
14+
if (!keep)
15+
{
16+
s.Dispose();
17+
}
18+
}
19+
20+
static Stream Open(string path) => File.OpenRead(path);
21+
22+
static void NullArg(string path)
23+
{
24+
var r = File.OpenRead(path);
25+
Keep(r, null, true);
26+
r.Dispose();
27+
}
28+
29+
static void CreationArg(string path)
30+
{
31+
var r = File.OpenRead(path);
32+
Keep(r, new MemoryStream(), true);
33+
r.Dispose();
34+
}
35+
36+
static void CallResultArg(string path)
37+
{
38+
var r = File.OpenRead(path);
39+
Keep(r, Open(path), true);
40+
r.Dispose();
41+
}
42+
}

‎corpus/p037-shapes/arg-raw-facts/expected.json‎

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "arg-raw-facts",
4+
"status": "anchored",
5+
"why": "Required A2.2 control (#304): the raw non-handle argument facts. In a relevant call, `null` is null_literal, `new MemoryStream()` is object_creation, and `Open(path)` is call_result{callee, sig}, never fresh_owned (freshness is a summary conclusion). The creation and the inner call carry no handle, so neither gets its own calls[] record. The OWN003 verdicts are the legacy ConsumesParam reading of `Keep(r, ..., true)` (the P-037 motivating false positive), pinned unchanged because A2 moves no verdict.",
6+
"a2_contract": "Already correct at A2.1 and must stay so: one calls[] record per caller, for Keep only; slot 1 is null_literal / object_creation / call_result{ShapeRawArgFacts.Open, System.String}; no fresh_owned; no record for `new MemoryStream()` or `Open(path)`. Added after the A2.2 pre-registration as a coverage fix (the kinds were probed, not pinned), recorded at the base first.",
7+
"a2_expect": [
8+
{
9+
"function": "ShapeRawArgFacts.NullArg",
10+
"call": {
11+
"form": "statement",
12+
"callee": "ShapeRawArgFacts.Keep",
13+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
14+
"args": [
15+
{
16+
"param": 0,
17+
"kind": "var",
18+
"name": "r"
19+
},
20+
{
21+
"param": 1,
22+
"kind": "null_literal"
23+
},
24+
{
25+
"param": 2,
26+
"kind": "bool_const",
27+
"value": true
28+
}
29+
]
30+
}
31+
},
32+
{
33+
"function": "ShapeRawArgFacts.CreationArg",
34+
"call": {
35+
"form": "statement",
36+
"callee": "ShapeRawArgFacts.Keep",
37+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
38+
"args": [
39+
{
40+
"param": 0,
41+
"kind": "var",
42+
"name": "r"
43+
},
44+
{
45+
"param": 1,
46+
"kind": "object_creation"
47+
},
48+
{
49+
"param": 2,
50+
"kind": "bool_const",
51+
"value": true
52+
}
53+
]
54+
}
55+
},
56+
{
57+
"function": "ShapeRawArgFacts.CallResultArg",
58+
"call": {
59+
"form": "statement",
60+
"callee": "ShapeRawArgFacts.Keep",
61+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
62+
"args": [
63+
{
64+
"param": 0,
65+
"kind": "var",
66+
"name": "r"
67+
},
68+
{
69+
"param": 1,
70+
"kind": "call_result",
71+
"callee": "ShapeRawArgFacts.Open",
72+
"sig": "System.String"
73+
},
74+
{
75+
"param": 2,
76+
"kind": "bool_const",
77+
"value": true
78+
}
79+
]
80+
}
81+
}
82+
],
83+
"measured_at": "23e3203",
84+
"facts": {
85+
"ShapeRawArgFacts.Keep": {
86+
"params": [
87+
{
88+
"name": "s",
89+
"line": 12
90+
},
91+
{
92+
"name": "other",
93+
"line": 12
94+
}
95+
],
96+
"body": [
97+
"if:None@14",
98+
"then:release:s@16"
99+
],
100+
"guarded_facts": {
101+
"version": 1,
102+
"calls": [],
103+
"guards": [
104+
{
105+
"site": {
106+
"line": 14,
107+
"column": 9
108+
},
109+
"param": 2,
110+
"predicate": "truth",
111+
"negated": true
112+
}
113+
]
114+
}
115+
},
116+
"ShapeRawArgFacts.NullArg": {
117+
"params": null,
118+
"body": [
119+
"acquire:r@24",
120+
"release:r@25",
121+
"release:r@26"
122+
],
123+
"guarded_facts": {
124+
"version": 1,
125+
"calls": [
126+
{
127+
"site": {
128+
"line": 25,
129+
"column": 9
130+
},
131+
"statement_line": 25,
132+
"form": "statement",
133+
"callee": "ShapeRawArgFacts.Keep",
134+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
135+
"first_party": true,
136+
"args": [
137+
{
138+
"param": 0,
139+
"kind": "var",
140+
"name": "r"
141+
},
142+
{
143+
"param": 1,
144+
"kind": "null_literal"
145+
},
146+
{
147+
"param": 2,
148+
"kind": "bool_const",
149+
"value": true
150+
}
151+
]
152+
}
153+
],
154+
"guards": []
155+
}
156+
},
157+
"ShapeRawArgFacts.CreationArg": {
158+
"params": null,
159+
"body": [
160+
"acquire:r@31",
161+
"release:r@32",
162+
"release:r@33"
163+
],
164+
"guarded_facts": {
165+
"version": 1,
166+
"calls": [
167+
{
168+
"site": {
169+
"line": 32,
170+
"column": 9
171+
},
172+
"statement_line": 32,
173+
"form": "statement",
174+
"callee": "ShapeRawArgFacts.Keep",
175+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
176+
"first_party": true,
177+
"args": [
178+
{
179+
"param": 0,
180+
"kind": "var",
181+
"name": "r"
182+
},
183+
{
184+
"param": 1,
185+
"kind": "object_creation"
186+
},
187+
{
188+
"param": 2,
189+
"kind": "bool_const",
190+
"value": true
191+
}
192+
]
193+
}
194+
],
195+
"guards": []
196+
}
197+
},
198+
"ShapeRawArgFacts.CallResultArg": {
199+
"params": null,
200+
"body": [
201+
"acquire:r@38",
202+
"release:r@39",
203+
"release:r@40"
204+
],
205+
"guarded_facts": {
206+
"version": 1,
207+
"calls": [
208+
{
209+
"site": {
210+
"line": 39,
211+
"column": 9
212+
},
213+
"statement_line": 39,
214+
"form": "statement",
215+
"callee": "ShapeRawArgFacts.Keep",
216+
"sig": "System.IO.Stream,System.IO.Stream,System.Boolean",
217+
"first_party": true,
218+
"args": [
219+
{
220+
"param": 0,
221+
"kind": "var",
222+
"name": "r"
223+
},
224+
{
225+
"param": 1,
226+
"kind": "call_result",
227+
"callee": "ShapeRawArgFacts.Open",
228+
"sig": "System.String"
229+
},
230+
{
231+
"param": 2,
232+
"kind": "bool_const",
233+
"value": true
234+
}
235+
]
236+
}
237+
],
238+
"guards": []
239+
}
240+
}
241+
},
242+
"verdict": {
243+
"rust": [
244+
"OWN003:warning@24",
245+
"OWN003:warning@31",
246+
"OWN003:warning@38"
247+
],
248+
"python": [
249+
"OWN003:warning@24",
250+
"OWN003:warning@31",
251+
"OWN003:warning@38"
252+
]
253+
}
254+
}

0 commit comments

Comments
 (0)