Skip to content

Commit 5daa6e3

Browse files
committed
P-037 A2.2: pre-register the honest-call-facts contract and record its census at the base
Before any treatment code: docs/notes/p037-a2.2-call-facts.md freezes the A2.2 scope (every relevant call inside an emitted record reaches the guarded-fact sidecar), the measured gap inventory at 23e3203 (G-A object creation, G-B constructor initializer, G-C value-preserving cast/!, G-D as/?:/?? relevance), the treatment rules (no vocabulary change), the falsifiers N1-N8, the negative controls and the same-environment (M2) evidence plan. Eight census shapes are added under corpus/p037-shapes and recorded at the base, so the treatment's diff shows per shape: five pending_a2 gap shapes, two anchored negative controls (duplicate same-type named arguments, unresolved callee) and the record-absence boundary R (a record-less method carries no sidecar; closing it is a case-5 decision, escalated with the measurement: 1 relevant call on the repo tree, 0 on the corpus). Census: 22/22 match on both engines. No extractor, schema or engine change. Refs #304 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KmiyfrkaG9sJruTcshM2oq
1 parent 23e3203 commit 5daa6e3

17 files changed

Lines changed: 1015 additions & 0 deletions

File tree

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
// A2.2 G-C: a handle behind a VALUE-PRESERVING wrapper is still the handle.
2+
// `(Stream)p` (reference conversion) and `p!` (no runtime effect) are the same
3+
// object as `p`, so the slot is `param`; A2.1 loses the whole call record
4+
// because the argument is not a bare identifier. A boxing cast is NOT value-
5+
// preserving: its slot stays opaque, but the call is still relevant.
6+
using System;
7+
using System.IO;
8+
9+
struct Handle : IDisposable
10+
{
11+
public void Dispose() { }
12+
}
13+
14+
static class ShapeCastBang
15+
{
16+
static void Keep(Stream s, bool keep)
17+
{
18+
if (!keep)
19+
{
20+
s.Dispose();
21+
}
22+
}
23+
24+
static void Sink(object o) { }
25+
26+
static void Cast(Stream p, bool keep)
27+
{
28+
Keep((Stream)p, keep);
29+
}
30+
31+
static void Bang(Stream? p, bool keep)
32+
{
33+
Keep(p!, keep);
34+
}
35+
36+
static void Boxed(Handle h)
37+
{
38+
Sink((object)h);
39+
}
40+
}
Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "arg-cast-and-bang",
4+
"status": "pending_a2",
5+
"why": "A2.2 G-C. A handle behind a value-preserving wrapper is the same object: `(Stream)p` (reference conversion) and `p!` (null-forgiving). A2.1 loses the call record because the argument is not a bare identifier. A boxing cast `(object)h` is not value-preserving.",
6+
"a2_contract": "A2.2 unwraps parentheses, `!` and identity/non-user-defined reference casts before classifying: Cast and Bang record Keep with param 0 -> param{source_param 0}. Boxed records Sink with param 0 -> opaque (boxing copies), call present because the handle flowed.",
7+
"measured_at": "23e3203",
8+
"facts": {
9+
"ShapeCastBang.Keep": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 16
14+
}
15+
],
16+
"body": [
17+
"if:None@18",
18+
"then:release:s@20"
19+
],
20+
"guarded_facts": {
21+
"version": 1,
22+
"calls": [],
23+
"guards": [
24+
{
25+
"site": {
26+
"line": 18,
27+
"column": 9
28+
},
29+
"param": 1,
30+
"predicate": "truth",
31+
"negated": true
32+
}
33+
]
34+
}
35+
},
36+
"ShapeCastBang.Cast": {
37+
"params": [
38+
{
39+
"name": "p",
40+
"line": 26
41+
}
42+
],
43+
"body": [
44+
"use:p@28"
45+
],
46+
"guarded_facts": null
47+
},
48+
"ShapeCastBang.Bang": {
49+
"params": [
50+
{
51+
"name": "p",
52+
"line": 31
53+
}
54+
],
55+
"body": [
56+
"use:p@33"
57+
],
58+
"guarded_facts": null
59+
},
60+
"ShapeCastBang.Boxed": {
61+
"params": [
62+
{
63+
"name": "h",
64+
"line": 36
65+
}
66+
],
67+
"body": [
68+
"use:h@38"
69+
],
70+
"guarded_facts": null
71+
}
72+
},
73+
"verdict": {
74+
"rust": [],
75+
"python": []
76+
}
77+
}
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// A2.2 G-D: a handle inside a compound argument (`as`, `?:`, `??`) cannot be
2+
// represented precisely, so the slot is opaque — but the handle still flows
3+
// into the call, so the call record must exist (opaque, not absent; the same
4+
// rule A' applied to params/ref/out slots).
5+
using System.IO;
6+
7+
static class ShapeCompound
8+
{
9+
static void Keep(Stream s, bool keep)
10+
{
11+
if (!keep)
12+
{
13+
s.Dispose();
14+
}
15+
}
16+
17+
static void As(Stream p, bool keep)
18+
{
19+
Keep(p as Stream, keep);
20+
}
21+
22+
static void Conditional(Stream p, Stream q, bool c)
23+
{
24+
Keep(c ? p : q, true);
25+
}
26+
27+
static void Coalesce(Stream? p, Stream q)
28+
{
29+
Keep(p ?? q, false);
30+
}
31+
}
Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "arg-compound-relevance",
4+
"status": "pending_a2",
5+
"why": "A2.2 G-D. `p as Stream`, `c ? p : q`, `p ?? q` carry a handle into the call but cannot be represented precisely; A2.1 drops the whole record.",
6+
"a2_contract": "A2.2 records each call with the compound slot `opaque` (relevance = a value operand is a handle after unwrapping): opaque, not absent — the rule A' applied to params/ref/out slots.",
7+
"measured_at": "23e3203",
8+
"facts": {
9+
"ShapeCompound.Keep": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 9
14+
}
15+
],
16+
"body": [
17+
"if:None@11",
18+
"then:release:s@13"
19+
],
20+
"guarded_facts": {
21+
"version": 1,
22+
"calls": [],
23+
"guards": [
24+
{
25+
"site": {
26+
"line": 11,
27+
"column": 9
28+
},
29+
"param": 1,
30+
"predicate": "truth",
31+
"negated": true
32+
}
33+
]
34+
}
35+
},
36+
"ShapeCompound.As": {
37+
"params": [
38+
{
39+
"name": "p",
40+
"line": 17
41+
}
42+
],
43+
"body": [
44+
"use:p@19"
45+
],
46+
"guarded_facts": null
47+
},
48+
"ShapeCompound.Conditional": {
49+
"params": [
50+
{
51+
"name": "p",
52+
"line": 22
53+
},
54+
{
55+
"name": "q",
56+
"line": 22
57+
}
58+
],
59+
"body": [
60+
"use:p@24",
61+
"use:q@24"
62+
],
63+
"guarded_facts": null
64+
},
65+
"ShapeCompound.Coalesce": {
66+
"params": [
67+
{
68+
"name": "p",
69+
"line": 27
70+
},
71+
{
72+
"name": "q",
73+
"line": 27
74+
}
75+
],
76+
"body": [
77+
"use:p@29",
78+
"use:q@29"
79+
],
80+
"guarded_facts": null
81+
}
82+
},
83+
"verdict": {
84+
"rust": [],
85+
"python": []
86+
}
87+
}
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// A2.2 G-B: `: base(s, keep)` hands the owned parameter to the base
2+
// constructor before the body runs. It is a call; A2.1 does not record it.
3+
// (The constructor has a body so that its record exists at all: an empty-body
4+
// constructor is the record-absence boundary, see record-absence-boundary.)
5+
using System.IO;
6+
7+
class GuardedBase
8+
{
9+
protected GuardedBase(Stream s, bool keep)
10+
{
11+
if (!keep)
12+
{
13+
s.Dispose();
14+
}
15+
}
16+
}
17+
18+
class ForwardingDerived : GuardedBase
19+
{
20+
public ForwardingDerived(Stream s, bool keep) : base(s, keep)
21+
{
22+
s.Flush();
23+
}
24+
}
Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "ctor-initializer",
4+
"status": "pending_a2",
5+
"why": "A2.2 G-B. `: base(s, keep)` is a call that hands the owned parameter to the base constructor before the body runs; A2.1 does not record constructor initializers.",
6+
"a2_contract": "A2.2 records the initializer as a calls[] entry: callee = `GuardedBase..ctor`, site = the initializer, statement_line = its line, form = statement (it runs as a statement and its result is discarded), args param 0 -> param{0}, param 1 -> param{1}.",
7+
"measured_at": "23e3203",
8+
"facts": {
9+
"GuardedBase..ctor": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 9
14+
}
15+
],
16+
"body": [
17+
"if:None@11",
18+
"then:release:s@13"
19+
],
20+
"guarded_facts": {
21+
"version": 1,
22+
"calls": [],
23+
"guards": [
24+
{
25+
"site": {
26+
"line": 11,
27+
"column": 9
28+
},
29+
"param": 1,
30+
"predicate": "truth",
31+
"negated": true
32+
}
33+
]
34+
}
35+
},
36+
"ForwardingDerived..ctor": {
37+
"params": [
38+
{
39+
"name": "s",
40+
"line": 20
41+
}
42+
],
43+
"body": [
44+
"use:s@22"
45+
],
46+
"guarded_facts": null
47+
}
48+
},
49+
"verdict": {
50+
"rust": [],
51+
"python": []
52+
}
53+
}
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Negative control for named-argument binding: two parameters of the SAME
2+
// type, passed by name in reversed order. Positional guessing and type-based
3+
// guessing are both wrong here; only symbolic resolution binds `b: p` to
4+
// ordinal 1 and `a: q` to ordinal 0.
5+
using System.IO;
6+
7+
static class ShapeDuplicateNamed
8+
{
9+
static void Pair(Stream a, Stream b)
10+
{
11+
a.Dispose();
12+
}
13+
14+
static void Caller(Stream p, Stream q)
15+
{
16+
Pair(b: p, a: q);
17+
}
18+
}

0 commit comments

Comments
 (0)