Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3039,6 +3039,12 @@ jobs:
# re-hashed and removed again. No baseline is taken here.
python scripts/p037_evidence.py artifacts
python scripts/p037_evidence.py population --source repo --materialize --cleanup
# A2.1: the guarded-fact sidecar is validated and INERT. Every census
# shape and the samples compilation go through both engines three
# times (as emitted, stripped, deliberately contradictory) and the
# lowered/summaries/verdicts layers must not move. Needs the
# own-shadow-engine the artifacts step just built.
python scripts/p037_sidecar_inertness.py
# The Windows launcher is a separate implementation, not a wrapper around
# the shell one, so the Windows leg has to go through it to mean anything.
- name: Own.NET's own tree, through own-check.ps1 on the Rust core
Expand Down
94 changes: 90 additions & 4 deletions corpus/p037-shapes/call-expression-statement/expected.json
Original file line number Diff line number Diff line change
@@ -1,9 +1,47 @@
{
"schema": "p037-fact-shape/1",
"shape": "call-expression-statement",
"status": "pending_a2",
"status": "anchored",
"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.",
"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.",
"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.",
"a2_expect": [
{
"function": "ShapeStatementCall.Caller",
"call": {
"site": {
"line": 26
},
"form": "statement",
"callee": "ShapeStatementCall.Inner",
"sig": "System.IO.Stream,System.Boolean",
"first_party": true,
"args": [
{
"param": 0,
"kind": "var",
"name": "r"
},
{
"param": 1,
"kind": "bool_const",
"value": true
}
]
}
},
{
"function": "ShapeStatementCall.Inner",
"guard": {
"site": {
"line": 17
},
"param": 1,
"predicate": "truth",
"negated": true
}
}
],
"measured_at": "464308b",
"facts": {
"ShapeStatementCall.Inner": {
Expand All @@ -16,18 +54,66 @@
"body": [
"if:None@17",
"then:release:s@19"
]
],
"guarded_facts": {
"version": 1,
"calls": [],
"guards": [
{
"site": {
"line": 17,
"column": 9
},
"param": 1,
"predicate": "truth",
"negated": true
}
]
}
},
"ShapeStatementCall.Caller": {
"params": null,
"body": [
"acquire:r@25",
"release:r@26"
]
],
"guarded_facts": {
"version": 1,
"calls": [
{
"site": {
"line": 26,
"column": 9
},
"statement_line": 26,
"form": "statement",
"callee": "ShapeStatementCall.Inner",
"sig": "System.IO.Stream,System.Boolean",
"first_party": true,
"args": [
{
"param": 0,
"kind": "var",
"name": "r"
},
{
"param": 1,
"kind": "bool_const",
"value": true
}
]
}
],
"guards": []
}
}
},
"verdict": {
"rust": [],
"python": []
}
},
"status_history": [
"pending_a2 (recorded at 464308b)",
"anchored (A2.1 sidecar)"
]
}
69 changes: 65 additions & 4 deletions corpus/p037-shapes/extension-receiver/expected.json
Original file line number Diff line number Diff line change
@@ -1,9 +1,37 @@
{
"schema": "p037-fact-shape/1",
"shape": "extension-receiver",
"status": "pending_a2",
"status": "anchored",
"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.",
"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.",
"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.",
"a2_expect": [
{
"function": "ShapeExtensionReceiver.Caller",
"call": {
"site": {
"line": 23
},
"callee": "ShapeExtensionReceiver.WaitForDispose",
"sig": "System.IO.Stream,System.Int32",
"args": [
{
"param": 0,
"kind": "var",
"name": "s"
},
{
"param": 1,
"kind": "opaque"
}
]
}
},
{
"function": "ShapeExtensionReceiver.WaitForDispose",
"guarded_facts": "absent"
}
],
"measured_at": "464308b",
"facts": {
"ShapeExtensionReceiver.WaitForDispose": {
Expand All @@ -16,14 +44,43 @@
"body": [
"if:None@14",
"then:release:self@16"
]
],
"guarded_facts": null
},
"ShapeExtensionReceiver.Caller": {
"params": null,
"body": [
"acquire:s@22",
"use:s@23"
]
],
"guarded_facts": {
"version": 1,
"calls": [
{
"site": {
"line": 23,
"column": 9
},
"statement_line": 23,
"form": "statement",
"callee": "ShapeExtensionReceiver.WaitForDispose",
"sig": "System.IO.Stream,System.Int32",
"first_party": true,
"args": [
{
"param": 0,
"kind": "var",
"name": "s"
},
{
"param": 1,
"kind": "opaque"
}
]
}
],
"guards": []
}
}
},
"verdict": {
Expand All @@ -33,5 +90,9 @@
"python": [
"OWN001:warning@22"
]
}
},
"status_history": [
"pending_a2 (recorded at 464308b)",
"anchored (A2.1 sidecar)"
]
}
85 changes: 81 additions & 4 deletions corpus/p037-shapes/guard-bool-const-false/expected.json
Original file line number Diff line number Diff line change
@@ -1,9 +1,38 @@
{
"schema": "p037-fact-shape/1",
"shape": "guard-bool-const-false",
"status": "pending_a2",
"status": "anchored",
"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.",
"a2_contract": "{\"param\":1,\"kind\":\"bool_const\",\"value\":false}; Rust derives `const-neg`.",
"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.",
"a2_expect": [
{
"function": "ShapeConstFalse.Caller",
"call": {
"callee": "ShapeConstFalse.Inner",
"args": [
{
"param": 0,
"kind": "var",
"name": "r"
},
{
"param": 1,
"kind": "bool_const",
"value": false
}
]
}
},
{
"function": "ShapeConstFalse.Inner",
"guard": {
"param": 1,
"predicate": "truth",
"negated": true
}
}
],
"measured_at": "464308b",
"facts": {
"ShapeConstFalse.Inner": {
Expand All @@ -16,18 +45,66 @@
"body": [
"if:None@10",
"then:release:s@12"
]
],
"guarded_facts": {
"version": 1,
"calls": [],
"guards": [
{
"site": {
"line": 10,
"column": 9
},
"param": 1,
"predicate": "truth",
"negated": true
}
]
}
},
"ShapeConstFalse.Caller": {
"params": null,
"body": [
"acquire:r@18",
"release:r@19"
]
],
"guarded_facts": {
"version": 1,
"calls": [
{
"site": {
"line": 19,
"column": 9
},
"statement_line": 19,
"form": "statement",
"callee": "ShapeConstFalse.Inner",
"sig": "System.IO.Stream,System.Boolean",
"first_party": true,
"args": [
{
"param": 0,
"kind": "var",
"name": "r"
},
{
"param": 1,
"kind": "bool_const",
"value": false
}
]
}
],
"guards": []
}
}
},
"verdict": {
"rust": [],
"python": []
}
},
"status_history": [
"pending_a2 (recorded at 464308b)",
"anchored (A2.1 sidecar)"
]
}
Loading
Loading