Skip to content

Commit 3ffd9d7

Browse files
claudeclaude
committed
P-037 A2.2-3P: the guarded_functions[] orphan carrier, production side
Treatment-only (extractor, spec), under the sequencing ruling recorded in §10.6.6/§10.6.9 (a §10.1 case-4 clarification): production now, door registration later as A2.2-D after A2.2-S. No instrument path moves; the existing T and R stay valid. - A method the legacy pass does not admit — no handle at all, every candidate escaped, or an unmodelled construct — still has raw guarded facts worth carrying. Each of the three admission gates hands such a method to CarryOrphan, and the facts ride in the top-level `guarded_functions[]` ({name, file, [sig], guarded_facts}), never in a dummy `functions[]` record: a record, even with an empty body, enters the first-party universe at the doors and can move MOS resolution. - The document is assembled as an ordered dictionary so the carrier rides ONLY when non-empty and as the last key: measured on the samples and the probe, the bytes before the carrier are identical to the previous head's output, and a document without orphans keeps its bytes. - ValidateOrphanCarrier: every entry is a complete envelope, and one method identity (file, name, sig) in both `functions[]` and `guarded_functions[]` refuses the run (exit 2, no facts written). The control knob OWN_P037_SELFCHECK_PROBE=duplicate_identity adds such a duplicate on purpose so the refusal is witnessed; it never changes facts. - Doors: the Python loader reads named keys and the Rust document struct flattens unknown top-level fields, so both carry the list as additive unknown metadata; neither lowerer reads it. No strict-door recognition here. Measured, not assumed: lock, goto and a local-function declaration are the constructs the legacy pass still refuses (try, switch, for and using declarations are modelled), so the unmodelled shape uses lock; the samples carry 7 orphans, among them the disposing-guarded Dispose methods whose guards had been undeliverable; the probe rows PlainSame and the inner call of Nested read orphan_call, the local-handle delegate row orphan_call:delegate_invocation, and Tuple / Closure / UserConversion / Indexer stay no_record because their only occurrence is a named exclusion. Pins: - corpus/p037-shapes: eight orphan-* shapes — nonconsuming-callee, ctor-statement, delegate-local, guards-only, unmodelled-lock, nested-inner-call (the inner call carried, the outer provably not), none-for-excluded (carried nowhere) and disjoint-from-records (a recorded method and an orphan in one file, one carrier each). The census tool pins orphan entries beside records and asserts which carrier an expectation means; the 44 earlier shapes are byte-identical. - scripts/p037_sidecar_inertness.py: four variants (emitted, stripped, orphans_stripped, contradictory in both carriers) over the census, the relevance probe and the samples, the identity invariant per document, the refusal witness through the knob, non-vacuity of the carrier: 54 documents, 97 sidecars, 17 orphans, inert on both engines, python == rust. - corpus/p037-relevance/probe: a2_2_3p_observed measured with the orphan vocabulary; the freeze test pins that exactly the relevant no_record rows became orphans, that the nested inner call is the one indirect fact carried, and that recorded rows did not move. - spec/OwnIR.md §5.3, spec/ownir.schema.json (top-level guarded_functions, $defs guardedOrphan), docs/notes §10.6.6/§10.6.9 synchronized. Refs #304 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb
1 parent 7de7a6f commit 3ffd9d7

25 files changed

Lines changed: 1068 additions & 80 deletions

File tree

‎corpus/p037-relevance/README.md‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,12 @@ landed: the object_creation row reads `sidecar_call:object_creation` in
5050
`a2_2_2_observed`; A2.2-2b re-shaped the delegate_invocation row with a record
5151
to `sidecar_call:delegate_invocation` (A' had captured it as a plain invocation
5252
of the delegate's `Invoke`, which the coarse vocabulary could not see), and the
53-
local-handle delegate row stays `no_record` at every step.
53+
local-handle delegate row stays `no_record` at every step. A2.2-3P landed: the
54+
orphan carrier `guarded_functions[]` delivers the facts of the methods the legacy
55+
pass never admitted; `a2_2_3p_observed` reads `orphan_call` for PlainSame and the
56+
inner call of Nested, `orphan_call:delegate_invocation` for the local-handle
57+
delegate row, and stays `no_record` only where the sole occurrence is a named
58+
exclusion (Tuple, Closure, UserConversion, Indexer): no fact exists to carry.
5459

5560
Only an A2.2 step, deliberately, one row at a time: a transparent wrapper
5661
becomes `captured` in A2.2-1, a call-like form in A2.2-2, an orphan record

‎corpus/p037-relevance/probe/expected.json‎

Lines changed: 62 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,17 @@
77
"a2_2_1_note": "Measured with the A2.2-1 extractor (the IOperation value-flow walker) from the tree this file is committed in, before the commit: the SHA that carries this file is the SHA it was measured at. A2.2-1 promises exactly the transparent and may-value rows move to sidecar_call; every other row must read as it did at A'. A2.2-1a added the CheckedRef and Boxing rows, measured at both points.",
88
"a2_2_2_note": "Measured with the A2.2-2 extractor (constructor calls as call-like sites) from the tree this file is committed in. A2.2-2 promises exactly the object_creation row(s) move to sidecar_call; every other row, delegate_invocation included, must read as it did after A2.2-1.",
99
"a2_2_2b_note": "Measured with the A2.2-2b extractor (delegate invocation as a call-like site) from the tree this file is committed in. A2.2-2b promises exactly the delegate_invocation row that HAS a record moves to sidecar_call; the local-handle delegate row stays no_record (orphan carrier), every other row reads as after A2.2-2. Every historical column of a row added later was measured with that step's extractor, rebuilt at its commit, never assumed.",
10+
"a2_2_3p_note": "Measured with the A2.2-3P extractor (the guarded_functions[] orphan carrier) from the tree this file is committed in. A2.2-3P promises exactly the rows that read no_record after A2.2-2b AND have a relevant call or an eligible guard move to an orphan_* reading; a no_record row whose occurrence is a named exclusion stays no_record (no fact exists to carry); every row with a record reads as after A2.2-2b.",
1011
"observed_vocabulary": {
1112
"sidecar_call": "a function record with a guarded_facts call fact for the probe call, all captured calls being invocation expressions (no call_kind)",
1213
"sidecar_call:object_creation": "captured, and the captured call is a constructor call (call_kind object_creation)",
1314
"sidecar_call:delegate_invocation": "captured, and the captured call is a delegate invocation (call_kind delegate_invocation, callee/sig null)",
1415
"sidecar_call:mixed": "captured calls of more than one kind in one probe method (none expected; a row reading this is a probe defect)",
16+
"orphan_call": "no functions[] record, but a guarded_functions[] entry whose calls are invocation expressions (A2.2-3P)",
17+
"orphan_call:object_creation": "no functions[] record; the orphan entry's call is a constructor call",
18+
"orphan_call:delegate_invocation": "no functions[] record; the orphan entry's call is a delegate invocation",
19+
"orphan_call:mixed": "orphan entry with calls of more than one kind (none expected)",
20+
"orphan_guards_only": "no functions[] record; the orphan entry carries guards and no call",
1521
"record_without_call_fact": "a function record exists but carries no call fact for the probe call",
1622
"no_record": "the legacy pass emitted no function record at all (every candidate escaped)"
1723
},
@@ -38,7 +44,8 @@
3844
"a2_1_observed": "sidecar_call",
3945
"a2_2_1_observed": "sidecar_call",
4046
"a2_2_2_observed": "sidecar_call",
41-
"a2_2_2b_observed": "sidecar_call"
47+
"a2_2_2b_observed": "sidecar_call",
48+
"a2_2_3p_observed": "sidecar_call"
4249
},
4350
"PlainSame": {
4451
"class": "direct",
@@ -47,7 +54,8 @@
4754
"a2_1_observed": "no_record",
4855
"a2_2_1_observed": "no_record",
4956
"a2_2_2_observed": "no_record",
50-
"a2_2_2b_observed": "no_record"
57+
"a2_2_2b_observed": "no_record",
58+
"a2_2_3p_observed": "orphan_call"
5159
},
5260
"Parens": {
5361
"class": "transparent",
@@ -56,7 +64,8 @@
5664
"a2_1_observed": "sidecar_call",
5765
"a2_2_1_observed": "sidecar_call",
5866
"a2_2_2_observed": "sidecar_call",
59-
"a2_2_2b_observed": "sidecar_call"
67+
"a2_2_2b_observed": "sidecar_call",
68+
"a2_2_3p_observed": "sidecar_call"
6069
},
6170
"IdentityCast": {
6271
"class": "transparent",
@@ -65,7 +74,8 @@
6574
"a2_1_observed": "record_without_call_fact",
6675
"a2_2_1_observed": "sidecar_call",
6776
"a2_2_2_observed": "sidecar_call",
68-
"a2_2_2b_observed": "sidecar_call"
77+
"a2_2_2b_observed": "sidecar_call",
78+
"a2_2_3p_observed": "sidecar_call"
6979
},
7080
"Cast": {
7181
"class": "transparent",
@@ -74,7 +84,8 @@
7484
"a2_1_observed": "record_without_call_fact",
7585
"a2_2_1_observed": "sidecar_call",
7686
"a2_2_2_observed": "sidecar_call",
77-
"a2_2_2b_observed": "sidecar_call"
87+
"a2_2_2b_observed": "sidecar_call",
88+
"a2_2_3p_observed": "sidecar_call"
7889
},
7990
"AsCast": {
8091
"class": "transparent",
@@ -83,7 +94,8 @@
8394
"a2_1_observed": "record_without_call_fact",
8495
"a2_2_1_observed": "sidecar_call",
8596
"a2_2_2_observed": "sidecar_call",
86-
"a2_2_2b_observed": "sidecar_call"
97+
"a2_2_2b_observed": "sidecar_call",
98+
"a2_2_3p_observed": "sidecar_call"
8799
},
88100
"Bang": {
89101
"class": "transparent",
@@ -92,7 +104,8 @@
92104
"a2_1_observed": "record_without_call_fact",
93105
"a2_2_1_observed": "sidecar_call",
94106
"a2_2_2_observed": "sidecar_call",
95-
"a2_2_2b_observed": "sidecar_call"
107+
"a2_2_2b_observed": "sidecar_call",
108+
"a2_2_3p_observed": "sidecar_call"
96109
},
97110
"CheckedRef": {
98111
"class": "transparent",
@@ -102,7 +115,8 @@
102115
"a2_1_observed": "record_without_call_fact",
103116
"a2_2_1_observed": "sidecar_call",
104117
"a2_2_2_observed": "sidecar_call",
105-
"a2_2_2b_observed": "sidecar_call"
118+
"a2_2_2b_observed": "sidecar_call",
119+
"a2_2_3p_observed": "sidecar_call"
106120
},
107121
"Ternary": {
108122
"class": "may_value",
@@ -111,7 +125,8 @@
111125
"a2_1_observed": "record_without_call_fact",
112126
"a2_2_1_observed": "sidecar_call",
113127
"a2_2_2_observed": "sidecar_call",
114-
"a2_2_2b_observed": "sidecar_call"
128+
"a2_2_2b_observed": "sidecar_call",
129+
"a2_2_3p_observed": "sidecar_call"
115130
},
116131
"Coalesce": {
117132
"class": "may_value",
@@ -120,7 +135,8 @@
120135
"a2_1_observed": "record_without_call_fact",
121136
"a2_2_1_observed": "sidecar_call",
122137
"a2_2_2_observed": "sidecar_call",
123-
"a2_2_2b_observed": "sidecar_call"
138+
"a2_2_2b_observed": "sidecar_call",
139+
"a2_2_3p_observed": "sidecar_call"
124140
},
125141
"Switch": {
126142
"class": "may_value",
@@ -129,7 +145,8 @@
129145
"a2_1_observed": "record_without_call_fact",
130146
"a2_2_1_observed": "sidecar_call",
131147
"a2_2_2_observed": "sidecar_call",
132-
"a2_2_2b_observed": "sidecar_call"
148+
"a2_2_2b_observed": "sidecar_call",
149+
"a2_2_3p_observed": "sidecar_call"
133150
},
134151
"AsMayFail": {
135152
"class": "may_value",
@@ -138,7 +155,8 @@
138155
"a2_1_observed": "record_without_call_fact",
139156
"a2_2_1_observed": "sidecar_call",
140157
"a2_2_2_observed": "sidecar_call",
141-
"a2_2_2b_observed": "sidecar_call"
158+
"a2_2_2b_observed": "sidecar_call",
159+
"a2_2_3p_observed": "sidecar_call"
142160
},
143161
"Ctor": {
144162
"class": "call_like",
@@ -147,7 +165,8 @@
147165
"a2_1_observed": "record_without_call_fact",
148166
"a2_2_1_observed": "record_without_call_fact",
149167
"a2_2_2_observed": "sidecar_call:object_creation",
150-
"a2_2_2b_observed": "sidecar_call:object_creation"
168+
"a2_2_2b_observed": "sidecar_call:object_creation",
169+
"a2_2_3p_observed": "sidecar_call:object_creation"
151170
},
152171
"DelegateCall": {
153172
"class": "call_like",
@@ -157,7 +176,8 @@
157176
"a2_1_observed": "no_record",
158177
"a2_2_1_observed": "no_record",
159178
"a2_2_2_observed": "no_record",
160-
"a2_2_2b_observed": "no_record"
179+
"a2_2_2b_observed": "no_record",
180+
"a2_2_3p_observed": "orphan_call:delegate_invocation"
161181
},
162182
"DelegateCallOwned": {
163183
"class": "call_like",
@@ -167,7 +187,8 @@
167187
"a2_1_observed": "sidecar_call",
168188
"a2_2_1_observed": "sidecar_call",
169189
"a2_2_2_observed": "sidecar_call",
170-
"a2_2_2b_observed": "sidecar_call:delegate_invocation"
190+
"a2_2_2b_observed": "sidecar_call:delegate_invocation",
191+
"a2_2_3p_observed": "sidecar_call:delegate_invocation"
171192
},
172193
"Nested": {
173194
"class": "indirect",
@@ -177,7 +198,8 @@
177198
"a2_1_observed": "no_record",
178199
"a2_2_1_observed": "no_record",
179200
"a2_2_2_observed": "no_record",
180-
"a2_2_2b_observed": "no_record"
201+
"a2_2_2b_observed": "no_record",
202+
"a2_2_3p_observed": "orphan_call"
181203
},
182204
"ArrayInit": {
183205
"class": "indirect",
@@ -186,7 +208,8 @@
186208
"a2_1_observed": "record_without_call_fact",
187209
"a2_2_1_observed": "record_without_call_fact",
188210
"a2_2_2_observed": "record_without_call_fact",
189-
"a2_2_2b_observed": "record_without_call_fact"
211+
"a2_2_2b_observed": "record_without_call_fact",
212+
"a2_2_3p_observed": "record_without_call_fact"
190213
},
191214
"CollectionInit": {
192215
"class": "indirect",
@@ -195,7 +218,8 @@
195218
"a2_1_observed": "record_without_call_fact",
196219
"a2_2_1_observed": "record_without_call_fact",
197220
"a2_2_2_observed": "record_without_call_fact",
198-
"a2_2_2b_observed": "record_without_call_fact"
221+
"a2_2_2b_observed": "record_without_call_fact",
222+
"a2_2_3p_observed": "record_without_call_fact"
199223
},
200224
"Tuple": {
201225
"class": "indirect",
@@ -204,7 +228,8 @@
204228
"a2_1_observed": "no_record",
205229
"a2_2_1_observed": "no_record",
206230
"a2_2_2_observed": "no_record",
207-
"a2_2_2b_observed": "no_record"
231+
"a2_2_2b_observed": "no_record",
232+
"a2_2_3p_observed": "no_record"
208233
},
209234
"Closure": {
210235
"class": "indirect",
@@ -214,7 +239,8 @@
214239
"a2_1_observed": "no_record",
215240
"a2_2_1_observed": "no_record",
216241
"a2_2_2_observed": "no_record",
217-
"a2_2_2b_observed": "no_record"
242+
"a2_2_2b_observed": "no_record",
243+
"a2_2_3p_observed": "no_record"
218244
},
219245
"MethodGroup": {
220246
"class": "indirect",
@@ -223,7 +249,8 @@
223249
"a2_1_observed": "record_without_call_fact",
224250
"a2_2_1_observed": "record_without_call_fact",
225251
"a2_2_2_observed": "record_without_call_fact",
226-
"a2_2_2b_observed": "record_without_call_fact"
252+
"a2_2_2b_observed": "record_without_call_fact",
253+
"a2_2_3p_observed": "record_without_call_fact"
227254
},
228255
"UserConversion": {
229256
"class": "indirect",
@@ -233,7 +260,8 @@
233260
"a2_1_observed": "no_record",
234261
"a2_2_1_observed": "no_record",
235262
"a2_2_2_observed": "no_record",
236-
"a2_2_2b_observed": "no_record"
263+
"a2_2_2b_observed": "no_record",
264+
"a2_2_3p_observed": "no_record"
237265
},
238266
"ExplicitUserConversion": {
239267
"class": "indirect",
@@ -243,7 +271,8 @@
243271
"a2_1_observed": "record_without_call_fact",
244272
"a2_2_1_observed": "record_without_call_fact",
245273
"a2_2_2_observed": "record_without_call_fact",
246-
"a2_2_2b_observed": "record_without_call_fact"
274+
"a2_2_2b_observed": "record_without_call_fact",
275+
"a2_2_3p_observed": "record_without_call_fact"
247276
},
248277
"NameOf": {
249278
"class": "indirect",
@@ -252,7 +281,8 @@
252281
"a2_1_observed": "record_without_call_fact",
253282
"a2_2_1_observed": "record_without_call_fact",
254283
"a2_2_2_observed": "record_without_call_fact",
255-
"a2_2_2b_observed": "record_without_call_fact"
284+
"a2_2_2b_observed": "record_without_call_fact",
285+
"a2_2_3p_observed": "record_without_call_fact"
256286
},
257287
"MemberAccess": {
258288
"class": "indirect",
@@ -261,7 +291,8 @@
261291
"a2_1_observed": "record_without_call_fact",
262292
"a2_2_1_observed": "record_without_call_fact",
263293
"a2_2_2_observed": "record_without_call_fact",
264-
"a2_2_2b_observed": "record_without_call_fact"
294+
"a2_2_2b_observed": "record_without_call_fact",
295+
"a2_2_3p_observed": "record_without_call_fact"
265296
},
266297
"Boxing": {
267298
"class": "indirect",
@@ -271,7 +302,8 @@
271302
"a2_1_observed": "sidecar_call",
272303
"a2_2_1_observed": "record_without_call_fact",
273304
"a2_2_2_observed": "record_without_call_fact",
274-
"a2_2_2b_observed": "record_without_call_fact"
305+
"a2_2_2b_observed": "record_without_call_fact",
306+
"a2_2_3p_observed": "record_without_call_fact"
275307
},
276308
"Receiver": {
277309
"class": "indirect",
@@ -280,7 +312,8 @@
280312
"a2_1_observed": "record_without_call_fact",
281313
"a2_2_1_observed": "record_without_call_fact",
282314
"a2_2_2_observed": "record_without_call_fact",
283-
"a2_2_2b_observed": "record_without_call_fact"
315+
"a2_2_2b_observed": "record_without_call_fact",
316+
"a2_2_3p_observed": "record_without_call_fact"
284317
},
285318
"Indexer": {
286319
"class": "indirect",
@@ -289,7 +322,8 @@
289322
"a2_1_observed": "no_record",
290323
"a2_2_1_observed": "no_record",
291324
"a2_2_2_observed": "no_record",
292-
"a2_2_2b_observed": "no_record"
325+
"a2_2_2b_observed": "no_record",
326+
"a2_2_3p_observed": "no_record"
293327
}
294328
}
295329
}

‎corpus/p037-shapes/orphan-ctor-statement/case.cs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
using System;
2+
using System.IO;
3+
4+
// A2.2-3P: a constructor call as a statement, wrapper discarded: the legacy pass tracks nothing
5+
// and emits no record; the orphan carries the constructor call (object_creation).
6+
static class ShapeOrphanCtorStatement
7+
{
8+
sealed class Wrapper : IDisposable { public Wrapper(Stream s, bool leaveOpen) { } public void Dispose() { } }
9+
static void Caller(string path) { var s = File.OpenRead(path); new Wrapper(s, true); }
10+
}

‎corpus/p037-shapes/orphan-ctor-statement/expected.json‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "orphan-ctor-statement",
4+
"status": "anchored",
5+
"why": "P-037 A2.2-3P (formal note §10.6.6, the orphan carrier): a discarded constructor call has no legacy record and is carried as an orphan. A row that moves without a step meaning to move it is a regression.",
6+
"a2_expect": [
7+
{
8+
"function": "ShapeOrphanCtorStatement.Caller",
9+
"carrier": "guarded_functions",
10+
"call": {
11+
"call_kind": "object_creation",
12+
"callee": "ShapeOrphanCtorStatement.Wrapper..ctor",
13+
"args": [
14+
{
15+
"param": 0,
16+
"kind": "var",
17+
"name": "s"
18+
},
19+
{
20+
"param": 1,
21+
"kind": "bool_const",
22+
"value": true
23+
}
24+
]
25+
}
26+
}
27+
],
28+
"facts": {
29+
"ShapeOrphanCtorStatement.Caller": {
30+
"carrier": "guarded_functions",
31+
"sig": "System.String",
32+
"guarded_facts": {
33+
"version": 1,
34+
"calls": [
35+
{
36+
"site": {
37+
"line": 9,
38+
"column": 68
39+
},
40+
"statement_line": 9,
41+
"form": "statement",
42+
"callee": "ShapeOrphanCtorStatement.Wrapper..ctor",
43+
"sig": "System.IO.Stream,System.Boolean",
44+
"first_party": true,
45+
"args": [
46+
{
47+
"param": 0,
48+
"kind": "var",
49+
"name": "s"
50+
},
51+
{
52+
"param": 1,
53+
"kind": "bool_const",
54+
"value": true
55+
}
56+
],
57+
"call_kind": "object_creation"
58+
}
59+
],
60+
"guards": []
61+
}
62+
}
63+
},
64+
"verdict": {
65+
"rust": [],
66+
"python": []
67+
}
68+
}

0 commit comments

Comments
 (0)