Skip to content

Commit dce26ed

Browse files
committed
P-037 A2.1: emit the guarded-fact sidecar from the Roslyn extractor, validated and inert
Treatment-only step of the A2 staging (docs/notes/p037-formal-kernel.md §10.3): the extractor now writes `functions[].guarded_facts`, the raw record of what flows into each relevant call and what each eligible `if` tests, keyed by declared parameter ordinal. Neither engine reads it; the legacy `body` stays authoritative; no path under the A2.0 instrument freeze is touched, so the after-takes on M1 compare directly against the R baselines with population_commit = T. Producer (frontend/roslyn/OwnSharp.Extractor/Program.cs): - calls[]: one per call a disposable candidate local or an owned parameter flows into (argument or reduced-extension receiver); site {line, column} of the invocation plus statement_line as the join identity with the legacy ops; form statement|initializer|expression; callee/sig or null when unresolved; first_party; args bound by declared ordinal (named args resolved, extension receiver = 0, params/ref/out = opaque, unresolved callee = source position). - arg kinds (raw facts only, §10.2): var{name}, param{source_param[,negated]}, bool_const{value}, null_literal, object_creation, call_result{callee,sig}, opaque. No const-pos/id/neg and no fresh_owned are ever written. - guards[]: one per eligible `if` on a stable by-value parameter — truth on a bool, is_null/not_null on a reference or Nullable<T>; G-V4 stability is whole-body write exposure (assignment, ++/--, ref/out, ref alias, address). Ineligible guards get no entry: absence is the fail-closed signal. - Self-check: a sidecar that violates its own vocabulary makes the run refuse to write facts at all (exit 2), so a producer defect never reaches a door. Contract (spec/ownir.schema.json, spec/OwnIR.md §5.2, §4.2): - closed $defs guardedFacts/guardedCall/guardedArg/guardedGuard/sourceSite; the sidecar is optional and additive, OWNIR_VERSION stays 0. - sourceSite is deliberately UNBOUND (type only): the doors do not read the sidecar in A2.1, and §4.2 forbids a schema narrower than the door on a coordinate the door does not check. tests/test_ownir_defensive_limits.py classifies it as the one UNBOUND entry; the instrument step that registers the sidecar at the doors moves it to BOUND. Controls: - corpus/p037-shapes: all 11 shapes re-recorded with the sidecar (body ops, params and both engines' verdicts byte-identical to before), status pending_a2 -> anchored, and a2_expect contract checks per shape that fail by name (scripts/p037_fact_shapes.py check). - tests/test_p037_sidecar.py pins the schema enums against the producer's vocabularies and the raw-fact boundary. - scripts/p037_sidecar_inertness.py (CI dogfood step): for every census shape and the samples tree, the emitted, stripped and contradictory sidecars yield identical lowered/summaries/verdicts layers on both engines, python == rust, and the control is non-vacuous (39 sidecars over 12 documents locally). Known A2.1 boundary, owed by A2.2 (honest emission for every relevant call): object-creation arguments (`new X(handle, leaveOpen: true)`) are not yet a call fact; A2.1 covers invocation expressions. Refs #304 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb
1 parent 4a8e658 commit dce26ed

20 files changed

Lines changed: 2005 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)