Skip to content

Commit 80af136

Browse files
claudeclaude
committed
P-037 A1.1: the fact-shape census, and both P-037 checkers wired into CI
Two gaps closed. The second one was embarrassing. THE CENSUS — corpus/p037-shapes, 11 shapes, scripts/p037_fact_shapes.py a1 taught this the hard way: the 137-file VERDICT corpus reported UNCHANGED for a version of a1 that turned six CI jobs red. It contains no method returning its own disposable parameter; the repository's tree does. verdict coverage != syntax / fact-shape coverage Two hundred more random C# files would not have closed that gap. One fixture per shape does, and it fails by NAME rather than as a number that moved somewhere. Each case records today's emitted facts and verdict; `anchored` means the facts must stay, `pending_a2` pins today's facts anyway so a2's diff is visible per shape instead of aggregated away, and carries its contract in prose. return-disposable-parameter ANCHORED — the OWN004 shape, nailed down so it does not depend on OverloadSigSample.cs happening to survive in the tree named-arguments-reordered a2: resolve to declared parameter index extension-receiver a2: receiver -> declared parameter 0 guard-bool-const-true/false a2: {kind: bool_const, value: …} guard-forward-bare/negated a2: {kind: param, source_param, negated?} guard-mutated, guard-ref-alias a2: NOT eligible, no guard metadata at all guard-opaque-expression a2: {kind: opaque} and nothing else call-expression-statement a2: emit a real `call` for statement-level calls Two findings while recording them, both corrections to things stated earlier: 1. `CallReleasesReceiver` is reached ONLY from two sites gated on `ThisFieldName(...)`. It is part of the FIELD disposal detector and never runs on a local. The earlier claim — that fixing the seam only at `ConsumeReleaseArgs` would leave a guarded `this T` receiver fabricating call-site releases — was wrong in its location. Corrected inventory: A ConsumeReleaseArgs @3762 flow-locals, ARGUMENT handoff <- the seam B recursion @4586 internal to ConsumesParam C CallReleasesReceiver FIELD channel only, @5785 @5801 D ConsumeReleaseArgs @6562 escape analysis, rides on A 2. Consequently `var s = ...; s.DisposeIt();` — a first-party extension that disposes its receiver UNCONDITIONALLY — is charged OWN001. Verified with an unguarded probe, so the guard is not what does it. A pre-existing false positive of exactly the family P-037 addresses, arriving through the RECEIVER rather than the argument. Not A1's to fix; recorded so it cannot later be mistaken for something A1 caused. CI — neither P-037 checker was running anywhere `scripts/p037_controls.py` shipped with the A1.0 bootstrap and nothing invoked it. A conformance control that no job runs is a file, not a control. Both censuses now run in the Rust-default dogfood job, the one place that already has a .NET SDK, a built Rust candidate and a Python, on the Linux leg only: both are about the extractor's output and the two engines' reading of it, neither of which is platform-shaped, and the Windows leg exists for own-check.ps1. The verdict snapshot is deliberately NOT wired: 137 files times two engines is about fourteen minutes, and it is the per-STEP gate each A1.1 commit runs and records under docs/evidence/. Said out loud in the workflow itself, because an unstated omission is indistinguishable from an oversight. scripts/p037_controls.py --engine both 4/4 match scripts/p037_fact_shapes.py check 11/11 shapes, both engines ruff / mypy clean, 56 source files tests/test_stage3_surfaces.py rc=0, 66 invocations, 26 explicit Refs #304. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01376o4syzCem5aQ6NssxwX2
1 parent 464308b commit 80af136

26 files changed

Lines changed: 916 additions & 0 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2998,6 +2998,32 @@ jobs:
29982998
[ "$rc" -eq 1 ] || { echo "FAIL: expected exit 1 (findings), got $rc"; exit 1; }
29992999
case "$out" in *OWN001*) ;; *) echo "FAIL: the Rust core found no OWN001"; exit 1 ;; esac
30003000
echo "OK: Rust-default dogfood on ${{ matrix.os }} (own-check.sh)"
3001+
# P-037 A1.1 (#304). Both censuses run here because this is the one job that
3002+
# already has all three things they need — a .NET SDK for the extractor, a
3003+
# built Rust candidate, and a Python for the reference engine.
3004+
#
3005+
# Linux only, deliberately: both censuses are about the EXTRACTOR's output and
3006+
# the two engines' reading of it, neither of which is platform-shaped. The
3007+
# Windows leg of this job exists for own-check.ps1, which is a separate
3008+
# launcher implementation and is the thing Windows actually tests.
3009+
#
3010+
# NOT here: scripts/p037_verdict_snapshot.py. It is 137 files times two
3011+
# engines, roughly fourteen minutes, and it is the per-STEP gate each A1.1
3012+
# commit runs and records under docs/evidence/ — not a per-push check. Saying
3013+
# so out loud because an unstated omission looks identical to an oversight.
3014+
- name: P-037 conformance controls + fact-shape census
3015+
if: matrix.os == 'ubuntu-latest'
3016+
run: |
3017+
export OWEN_RUST_CORE="$PWD/rust/target/release/own-cli"
3018+
# The four G-V4 / class-3 controls, on both engines against one record.
3019+
# Today's record must match; --post-a1 is expected to FAIL until the
3020+
# semantic cut lands and is therefore NOT run as a gate here.
3021+
python scripts/p037_controls.py --engine both
3022+
# The eleven fact shapes. This is the census that exists because the
3023+
# 137-file VERDICT corpus reported UNCHANGED for a version of a1 that
3024+
# turned six jobs in this very workflow red: verdict coverage is not
3025+
# syntax/fact-shape coverage, and one fixture per shape fails by NAME.
3026+
python scripts/p037_fact_shapes.py check --engine both
30013027
# The Windows launcher is a separate implementation, not a wrapper around
30023028
# the shell one, so the Windows leg has to go through it to mean anything.
30033029
- name: Own.NET's own tree, through own-check.ps1 on the Rust core

‎corpus/p037-shapes/README.md‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
# `corpus/p037-shapes` — the FACT-SHAPE census for P-037 A1.1
2+
3+
A small, deliberate census of the C# shapes whose **emitted facts** the A1.1
4+
steps must preserve or must change — not a second verdict corpus.
5+
6+
## Why this exists
7+
8+
A1.1-a1 taught the lesson the hard way. The 137-file verdict corpus reported
9+
`UNCHANGED` for a version of a1 that turned six CI jobs red, because it contains
10+
no method that returns its own disposable parameter and the repository's own
11+
tree does. The corpus is labelled for **verdicts**; the A1.1 steps change the
12+
**fact surface**.
13+
14+
> **verdict coverage ≠ syntax / fact-shape coverage**
15+
16+
Two hundred more random C# files would not have closed that gap. One fixture per
17+
shape does. Each case here pins what the extractor emits for a shape it is known
18+
to be sensitive to, so a step that changes a shape it did not mean to touch is
19+
caught by name rather than by a CI job failing somewhere downstream.
20+
21+
## Layout
22+
23+
<shape>/case.cs the minimal program
24+
<shape>/expected.json what the facts must look like, and the verdict
25+
26+
`expected.json` records `facts` (asserted structure of the emitted
27+
`functions[]` record) and `verdict` (the finding codes at warning severity).
28+
A case whose shape belongs to a step that has not landed carries
29+
`"status": "pending_a2"` with the contract it will be held to, and asserts
30+
today's facts meanwhile — so the diff a2 produces is visible per shape instead
31+
of aggregated into a number.
32+
33+
Checked by `scripts/p037_fact_shapes.py`, which names its engine explicitly
34+
(#262 Stage 3) and runs one extractor invocation per case.

‎corpus/p037-shapes/call-expression-statement/case.cs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// A statement-level call. The C# lowering emits a `call` op in exactly ONE
2+
// place and only for `var x = Foo(...)` — a call whose RESULT binds to a local.
3+
// `Inner(s, true);` as a statement produces no `call` node at all, so there is
4+
// nothing for a summary layer to specialise. Without this, F3 cannot be carried
5+
// through the existing summary layer at all.
6+
//
7+
// This is also where a2's zero-semantic-cut risk lives: a real `call` op is
8+
// already semantically active and MOS reads it, so emitting one here can move
9+
// an existing summary before the guarded kernel is anywhere near. The MOS
10+
// collapsed-view diff is what catches that.
11+
using System.IO;
12+
13+
static class ShapeStatementCall
14+
{
15+
static void Inner(Stream s, bool keep)
16+
{
17+
if (!keep)
18+
{
19+
s.Dispose();
20+
}
21+
}
22+
23+
static void Caller(string path)
24+
{
25+
var r = File.OpenRead(path);
26+
Inner(r, true);
27+
}
28+
}

‎corpus/p037-shapes/call-expression-statement/expected.json‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "call-expression-statement",
4+
"status": "pending_a2",
5+
"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.",
6+
"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+
"measured_at": "464308b",
8+
"facts": {
9+
"ShapeStatementCall.Inner": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 15
14+
}
15+
],
16+
"body": [
17+
"if:None@17",
18+
"then:release:s@19"
19+
]
20+
},
21+
"ShapeStatementCall.Caller": {
22+
"params": null,
23+
"body": [
24+
"acquire:r@25",
25+
"release:r@26"
26+
]
27+
}
28+
},
29+
"verdict": {
30+
"rust": [],
31+
"python": []
32+
}
33+
}

‎corpus/p037-shapes/extension-receiver/case.cs‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// A reduced EXTENSION method. Roslyn's reduced symbol drops the `this`
2+
// parameter from `Parameters`, but the summary lives on the UNREDUCED
3+
// declaration where the receiver is parameter 0. a2 must synthesise
4+
// receiver -> declared parameter 0
5+
// timeout -> declared parameter 1
6+
// or `CallReleasesReceiver` can never be honestly retired: the guarded
7+
// summaries would be complete except for one old tunnel under the fence.
8+
using System.IO;
9+
10+
static class ShapeExtensionReceiver
11+
{
12+
static void WaitForDispose(this Stream self, int timeout)
13+
{
14+
if (timeout >= 0)
15+
{
16+
self.Dispose();
17+
}
18+
}
19+
20+
static void Caller(string path)
21+
{
22+
var s = File.OpenRead(path);
23+
s.WaitForDispose(5);
24+
}
25+
}

‎corpus/p037-shapes/extension-receiver/expected.json‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "extension-receiver",
4+
"status": "pending_a2",
5+
"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.",
6+
"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+
"measured_at": "464308b",
8+
"facts": {
9+
"ShapeExtensionReceiver.WaitForDispose": {
10+
"params": [
11+
{
12+
"name": "self",
13+
"line": 12
14+
}
15+
],
16+
"body": [
17+
"if:None@14",
18+
"then:release:self@16"
19+
]
20+
},
21+
"ShapeExtensionReceiver.Caller": {
22+
"params": null,
23+
"body": [
24+
"acquire:s@22",
25+
"use:s@23"
26+
]
27+
}
28+
},
29+
"verdict": {
30+
"rust": [
31+
"OWN001:warning@22"
32+
],
33+
"python": [
34+
"OWN001:warning@22"
35+
]
36+
}
37+
}

‎corpus/p037-shapes/guard-bool-const-false/case.cs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// The same call with `false`. The two constants must be distinguishable in the
2+
// facts: a single "is a constant" bit would collapse the exact distinction the
3+
// cell selection turns on.
4+
using System.IO;
5+
6+
static class ShapeConstFalse
7+
{
8+
static void Inner(Stream s, bool keep)
9+
{
10+
if (!keep)
11+
{
12+
s.Dispose();
13+
}
14+
}
15+
16+
static void Caller(string path)
17+
{
18+
var r = File.OpenRead(path);
19+
Inner(r, false);
20+
}
21+
}

‎corpus/p037-shapes/guard-bool-const-false/expected.json‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "guard-bool-const-false",
4+
"status": "pending_a2",
5+
"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.",
6+
"a2_contract": "{\"param\":1,\"kind\":\"bool_const\",\"value\":false}; Rust derives `const-neg`.",
7+
"measured_at": "464308b",
8+
"facts": {
9+
"ShapeConstFalse.Inner": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 8
14+
}
15+
],
16+
"body": [
17+
"if:None@10",
18+
"then:release:s@12"
19+
]
20+
},
21+
"ShapeConstFalse.Caller": {
22+
"params": null,
23+
"body": [
24+
"acquire:r@18",
25+
"release:r@19"
26+
]
27+
}
28+
},
29+
"verdict": {
30+
"rust": [],
31+
"python": []
32+
}
33+
}

‎corpus/p037-shapes/guard-bool-const-true/case.cs‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// `Inner(s, true)`: a BOOL CONSTANT argument. a2 must record it as
2+
// {"param":1,"kind":"bool_const","value":true}; Rust derives `const-pos`.
3+
// The frontend never names const-pos itself — that is an interpretation
4+
// relative to the callee's elected guard, and it belongs to Rust.
5+
using System.IO;
6+
7+
static class ShapeConstTrue
8+
{
9+
static void Inner(Stream s, bool keep)
10+
{
11+
if (!keep)
12+
{
13+
s.Dispose();
14+
}
15+
}
16+
17+
static void Caller(string path)
18+
{
19+
var r = File.OpenRead(path);
20+
Inner(r, true);
21+
}
22+
}

‎corpus/p037-shapes/guard-bool-const-true/expected.json‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{
2+
"schema": "p037-fact-shape/1",
3+
"shape": "guard-bool-const-true",
4+
"status": "pending_a2",
5+
"why": "`Inner(r, true)`: the constant that decides the callee's branch. Today it reaches the facts as nothing at all — the statement-level call emits no `call` op, and the fabricated `release` from ConsumesParam stands in its place.",
6+
"a2_contract": "{\"param\":1,\"kind\":\"bool_const\",\"value\":true}. The frontend never writes `const-pos`: that is an interpretation relative to the callee's ELECTED guard and belongs to Rust.",
7+
"measured_at": "464308b",
8+
"facts": {
9+
"ShapeConstTrue.Inner": {
10+
"params": [
11+
{
12+
"name": "s",
13+
"line": 9
14+
}
15+
],
16+
"body": [
17+
"if:None@11",
18+
"then:release:s@13"
19+
]
20+
},
21+
"ShapeConstTrue.Caller": {
22+
"params": null,
23+
"body": [
24+
"acquire:r@19",
25+
"release:r@20"
26+
]
27+
}
28+
},
29+
"verdict": {
30+
"rust": [],
31+
"python": []
32+
}
33+
}

0 commit comments

Comments
 (0)