From f164dd3726a1758676de5081579dd3c0b336de25 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 16:27:38 +0000 Subject: [PATCH 1/3] Only a definite release makes a call-site handoff (INF-S2, #380) ConsumesParam treated a first-party parameter as consumed when the callee contained any immediate Dispose/Close of it, so a release behind a guard was lowered as an unconditional release of the caller's argument. That is the flattened must INF-S2 forbids: on pinned dotnet/runtime code it produced false OWN009 at two callers of VerifyPersistedKey(..., disposeKey: false) and a false must summary for the public Mono.Options GetArguments(TextReader) wrapper. A direct release or a forward to another consumer now counts only when it runs on every normal-return path of the callee: not under a condition, loop or catch, and not behind an earlier return unless a finally covers it. The guard's value is never read and no OwnIR field changes. A declined argument stays an ordinary escape (an untracked local, a used parameter), so no opposite verdict is invented. GuardedConsumeSample + tests/test_guarded_consume.py pin the partial shapes (guard false, guarded early return, guarded forward), the guard-true caller (no fabricated release, no fabricated leak), the definite anchors (plain and finally dispose still give OWN002 on a later use) and the borrowing wrapper (summary no). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp --- .github/workflows/ci.yml | 8 + frontend/roslyn/OwnSharp.Extractor/Program.cs | 52 +++++- .../roslyn/samples/GuardedConsumeSample.cs | 113 +++++++++++++ tests/test_guarded_consume.py | 158 ++++++++++++++++++ 4 files changed, 329 insertions(+), 2 deletions(-) create mode 100644 frontend/roslyn/samples/GuardedConsumeSample.cs create mode 100644 tests/test_guarded_consume.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 89b6db21..200a4ff7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -802,6 +802,14 @@ jobs: env: OWN_TIERB_REQUIRED: "1" run: python tests/test_extractor_columns.py + - name: Guarded release is not a call-site handoff (INF-S2, #380) + # A callee that releases its parameter only under a guard is a PARTIAL release, so + # its call must not be lowered as the caller's `release` (the fabricated `must`), + # while a definite consumer stays a handoff. Facts and verdicts on the real + # extractor; REQUIRED here, skips cleanly in the offline Tier-A job. + env: + OWN_TIERB_REQUIRED: "1" + run: python tests/test_guarded_consume.py - name: S2 step 10 analyzer-delta verifier (Tier B, full public CLI) env: OWN_TIERB_REQUIRED: "1" diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 7f6f0daf..7103683d 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -4975,6 +4975,10 @@ static bool ConsumesParam(IMethodSymbol method, IParameterSymbol param, var bodyModel = model.Compilation.GetSemanticModel(body.SyntaxTree); foreach (var inv in ImmediateInvocations(body)) { + // INF-S2 (#380): only a DEFINITE forward transfers — a hand-off behind a guard is the + // same partial release as a guarded `Dispose`, one call further away. + if (!IsDefiniteInBody(inv, body)) + continue; if (bodyModel.GetSymbolInfo(inv).Symbol is not IMethodSymbol callee) continue; var cargs = inv.ArgumentList.Arguments; @@ -4995,17 +4999,61 @@ static bool ConsumesParam(IMethodSymbol method, IParameterSymbol param, // Does `body` dispose the local/parameter named `name` — a `name.Dispose()` / `.Close()` / // `.DisposeAsync()` call (the consume signal)? Only IMMEDIATE calls count (`ImmediateInvocations` // excludes nested lambda / local-function bodies): a `name.Dispose()` inside a stored callback -// runs deferred, not at this call site, so it is not a discharge here. +// runs deferred, not at this call site, so it is not a discharge here. Only a DEFINITE release +// counts (INF-S2, #380): see IsDefiniteInBody. static bool DisposesLocal(SyntaxNode body, string name) { foreach (var i in ImmediateInvocations(body)) if (i.Expression is MemberAccessExpressionSyntax m && m.Name.Identifier.Text is "Dispose" or "Close" or "DisposeAsync" - && m.Expression is IdentifierNameSyntax id && id.Identifier.Text == name) + && m.Expression is IdentifierNameSyntax id && id.Identifier.Text == name + && IsDefiniteInBody(i, body)) return true; return false; } +// INF-S2 (#380): does `site` run on EVERY normal-return path of `body`? The call-site handoff +// models a consumer's release as a `release` of the caller's argument — an unconditional +// `must`. That is only true when the callee's release is definite. A release under a +// condition, inside a loop or a `catch`, or behind an earlier `return` is PARTIAL: the core +// derives `may` for it (INF-S2), and flattening it to a call-site release is the fabricated +// `must` the precision floor forbids — a false OWN002/OWN003/OWN009 at a caller that keeps the +// resource (`Close(s, dispose: false)`), and a false `must` summary on a wrapper that forwards +// its own parameter that way. Declining here never invents the opposite verdict: a declined +// argument stays an ordinary escape (an untracked local, a used parameter), not a borrow the +// caller is charged for. Purely syntactic and deliberately conservative — the guard's value +// is never read, and an unrecognised shape is not definite (it costs a use-after-handoff +// finding, never a false one). +static bool IsDefiniteInBody(SyntaxNode site, SyntaxNode body) +{ + for (var n = site.Parent; n is not null && n != body; n = n.Parent) + if (n is IfStatementSyntax or ElseClauseSyntax or SwitchStatementSyntax + or SwitchExpressionSyntax or ConditionalExpressionSyntax + or ConditionalAccessExpressionSyntax + or WhileStatementSyntax or DoStatementSyntax or ForStatementSyntax + or ForEachStatementSyntax or CatchClauseSyntax + || n is BinaryExpressionSyntax b + && (b.IsKind(SyntaxKind.LogicalAndExpression) + || b.IsKind(SyntaxKind.LogicalOrExpression) + || b.IsKind(SyntaxKind.CoalesceExpression))) + return false; + // An earlier exit leaves without reaching `site` — unless `site` sits in a `finally` the + // exit runs through. Exits inside nested lambdas / local functions leave THEM, not `body`. + foreach (var exit in body.DescendantNodes(n => n is not (AnonymousFunctionExpressionSyntax + or LocalFunctionStatementSyntax))) + { + if (exit is not (ReturnStatementSyntax or YieldStatementSyntax { RawKind: (int)SyntaxKind.YieldBreakStatement }) + || exit.SpanStart >= site.SpanStart) + continue; + var coveredByFinally = site.Ancestors().OfType().Any(f => + f.Parent is TryStatementSyntax t + && (t.Block.Span.Contains(exit.Span) || t.Catches.Any(c => c.Span.Contains(exit.Span)))); + if (!coveredByFinally) + return false; + } + return true; +} + // Does the call `recv.M(...)` RELEASE its receiver — i.e. is `M` a first-party // EXTENSION method whose body disposes the value it is invoked on? The dispose is // then laundered through a custom "drain and dispose" sink (e.g. NLog's diff --git a/frontend/roslyn/samples/GuardedConsumeSample.cs b/frontend/roslyn/samples/GuardedConsumeSample.cs new file mode 100644 index 00000000..1caa06c2 --- /dev/null +++ b/frontend/roslyn/samples/GuardedConsumeSample.cs @@ -0,0 +1,113 @@ +using System.IO; + +// #380 (INF-S2): the call-site handoff models a first-party consumer's release as a `release` +// of the caller's argument — an unconditional `must`. It may only do so when the callee's +// release is DEFINITE. A release behind a guard is partial (INF-S2 -> `may`), and lowering its +// call as a handoff fabricated false OWN002/OWN003/OWN009 at callers that keep the resource, and +// a false `must` summary on wrappers that forward their own parameter that way. +// +// Checked by tests/test_guarded_consume.py (facts AND verdicts, on the real extractor). +public static class GuardedConsumeSample +{ + // Partial: releases only when the flag says so. + private static void MaybeClose(Stream s, bool dispose) + { + if (dispose) + s.Dispose(); + } + + // Partial: a guarded early return skips the release. + private static void CloseUnlessKept(Stream s, bool keep) + { + if (keep) + return; + s.Dispose(); + } + + // Partial through the chain: forwards to a definite consumer only under a guard. + private static void MaybeForward(Stream s, bool forward) + { + if (forward) + Close(s); + } + + // Definite: the handoff anchor. + private static void Close(Stream s) + { + s.Dispose(); + } + + // Definite: every return runs through the finally. + private static int CloseInFinally(Stream s) + { + try + { + return s.ReadByte(); + } + finally + { + s.Dispose(); + } + } + + // (a) the guard is false, so the callee keeps the stream; the caller uses it and disposes it. + // Must NOT be lowered as a release (it was: a false OWN002 on the write, a false OWN003 on + // the dispose). + public static void GuardFalseThenUseAndDispose() + { + var keptStream = new MemoryStream(); + MaybeClose(keptStream, false); + keptStream.WriteByte(1); + keptStream.Dispose(); + } + + // (a) early-return spelling of the same partial release. + public static void EarlyReturnKeptThenUseAndDispose() + { + var earlyKept = new MemoryStream(); + CloseUnlessKept(earlyKept, true); + earlyKept.WriteByte(1); + earlyKept.Dispose(); + } + + // (a) guarded transitive forward. + public static void GuardedForwardFalseThenUseAndDispose() + { + var forwardKept = new MemoryStream(); + MaybeForward(forwardKept, false); + forwardKept.WriteByte(1); + forwardKept.Dispose(); + } + + // (b) the guard is true, so the callee releases and the caller relies on it. Nothing beyond + // current sound inference may be claimed: no fabricated release, and no fabricated leak + // either — the caller must stay silent. + public static void GuardTrueRelyOnCallee() + { + var handedStream = new MemoryStream(); + MaybeClose(handedStream, true); + } + + // (c) definite consumer: still a handoff, so a later use is a true use-after-handoff. + public static void DefiniteHandoffThenUse() + { + var handoffStream = new MemoryStream(); + Close(handoffStream); + handoffStream.WriteByte(1); + } + + // (c) definite through a finally: still a handoff. + public static void FinallyHandoffThenUse() + { + var finallyStream = new MemoryStream(); + CloseInFinally(finallyStream); + finallyStream.WriteByte(1); + } + + // Wrapper forwarding its OWN parameter with the guard false: the parameter is borrowed, so + // its summary must be `no`, never a fabricated `must`. + public static void BorrowingWrapper(Stream borrowed) + { + MaybeClose(borrowed, false); + } +} diff --git a/tests/test_guarded_consume.py b/tests/test_guarded_consume.py new file mode 100644 index 00000000..576bf12b --- /dev/null +++ b/tests/test_guarded_consume.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""#380 — a guarded release is not a call-site handoff (INF-S2), on the real extractor. + +The Roslyn call-site handoff (`ConsumeReleaseArgs` -> `ConsumesParam` -> `DisposesLocal`) +lowers a first-party consumer's release as a `release` of the caller's argument: an +unconditional `must`. INF-S2 allows that only for a DEFINITE release. Before #380 a callee +that disposed its parameter only under a guard (`if (dispose) s.Dispose();`) was treated +as a consumer too, which fabricated a release at callers that keep the resource +(`MaybeClose(s, false)`): false OWN002/OWN003/OWN009 there, and a false `must` summary on +a wrapper forwarding its own parameter that way. Reproduced on pinned dotnet/runtime code; +see the issue for the evidence. + +The fixture (frontend/roslyn/samples/GuardedConsumeSample.cs) pins three families: + + (a) partial release — guard false, guarded early return, guarded transitive forward: + the call is NOT lowered as a release and the caller that keeps, uses and disposes + the stream stays silent; + (b) guard true, caller relies on the callee: nothing beyond sound inference — no + fabricated release AND no fabricated leak; + (c) definite consumers — plain dispose and dispose in a finally every return runs + through: still a handoff, so a later use is still OWN002. This is the regression + anchor that keeps the fix from disabling the consume contract wholesale. + +plus the wrapper case: a parameter forwarded with the guard false summarizes as `no`. + +Line numbers are read off the fixture's text, not hard-coded, so an edit to the comments +cannot silently shift what is being checked. + +REQUIRED VS SKIPPED — the tests/test_extractor_columns.py convention: required exactly +when OWN_TIERB_REQUIRED=1, a clean printed skip otherwise. + +Run: OWN_TIERB_REQUIRED=1 python3 tests/test_guarded_consume.py +""" + +from __future__ import annotations + +import json +import os +import shutil +import subprocess +import sys +import tempfile + +_REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +_EXT = os.path.join(_REPO, "frontend", "roslyn", "OwnSharp.Extractor") +_SAMPLE_REL = os.path.join("frontend", "roslyn", "samples", "GuardedConsumeSample.cs") +_SAMPLE = os.path.join(_REPO, _SAMPLE_REL) + +# (call text in the fixture, the tracked argument) — the call must NOT be a release. +_PARTIAL = [ + ("MaybeClose(keptStream, false);", "keptStream"), + ("CloseUnlessKept(earlyKept, true);", "earlyKept"), + ("MaybeForward(forwardKept, false);", "forwardKept"), + ("MaybeClose(handedStream, true);", "handedStream"), +] +# (call text, argument) — definite consumers: the call IS a release (the handoff anchor). +_DEFINITE = [ + ("Close(handoffStream);", "handoffStream"), + ("CloseInFinally(finallyStream);", "finallyStream"), +] +_SILENT = ["keptStream", "earlyKept", "forwardKept", "handedStream"] +_USE_AFTER_HANDOFF = ["handoffStream", "finallyStream"] + + +def _line_of(text: str) -> int: + hits = [i for i, ln in enumerate(open(_SAMPLE, encoding="utf-8"), 1) if text in ln] + if len(hits) != 1: + raise AssertionError(f"fixture must contain {text!r} exactly once, found {len(hits)}") + return hits[0] + + +def _walk(body: list, out: list) -> None: + for op in body or []: + out.append(op) + for key in ("then", "else", "body"): + if key in op: + _walk(op[key], out) + + +def _ops(facts: dict) -> list[dict]: + out: list[dict] = [] + for fn in facts.get("functions", []): + _walk(fn.get("body"), out) + return out + + +def _core(argv: list[str]) -> subprocess.CompletedProcess: + return subprocess.run([sys.executable, "-m", "ownlang", *argv], cwd=_REPO, + capture_output=True, text=True, + env={**os.environ, "PYTHONPATH": _REPO}) + + +def run() -> int: + if not shutil.which("dotnet"): + if os.environ.get("OWN_TIERB_REQUIRED") == "1": + print("guarded consume: FAIL - dotnet is REQUIRED here " + "(OWN_TIERB_REQUIRED=1) and is not on PATH") + return 1 + print("guarded consume: SKIP - dotnet not on PATH") + return 0 + + fails: list[str] = [] + with tempfile.TemporaryDirectory() as tmp: + facts_path = os.path.join(tmp, "facts.json") + try: + subprocess.run(["dotnet", "run", "--project", _EXT, "--", "--flow-locals", + _SAMPLE_REL, "-o", facts_path], + cwd=_REPO, check=True, capture_output=True, text=True) + except subprocess.CalledProcessError as exc: + print(f"guarded consume: FAIL - the extractor exited {exc.returncode}\n" + f"{exc.stdout}\n{exc.stderr}") + return 1 + with open(facts_path, encoding="utf-8") as fh: + facts = json.load(fh) + verdict = _core(["ownir", facts_path, "--severity", "warning"]) + summaries = _core(["summaries", facts_path]) + + releases = {(op.get("var"), op.get("line")) for op in _ops(facts) if op.get("op") == "release"} + for text, var in _PARTIAL: + if (var, _line_of(text)) in releases: + fails.append(f"{text!r}: a partial (guarded) release was lowered as a call-site " + "release — the fabricated `must` of #380") + for text, var in _DEFINITE: + if (var, _line_of(text)) not in releases: + fails.append(f"{text!r}: a definite consumer is no longer a call-site release — " + "the consume contract regressed") + + if verdict.returncode >= 2: + fails.append(f"ownir hard error (rc={verdict.returncode}): {verdict.stderr.strip()}") + report = verdict.stdout + verdict.stderr + for var in _SILENT: + if f"'{var}'" in report: + fails.append(f"{var}: expected silence (no fabricated release, no fabricated leak), " + f"got a finding") + for var in _USE_AFTER_HANDOFF: + if not any("[OWN002]" in ln and f"'{var}'" in ln for ln in report.splitlines()): + fails.append(f"{var}: expected OWN002 (use after a definite handoff)") + + try: + docs = json.loads(summaries.stdout)["summaries"] + except (ValueError, KeyError, TypeError): + docs = [] + fails.append(f"summaries dump unreadable (rc={summaries.returncode})") + wrapper_name = "GuardedConsumeSample.BorrowingWrapper" + wrapper = [p for d in docs if d.get("method", "").endswith(wrapper_name) + for p in d.get("params", []) if p.get("name") == "borrowed"] + if [p.get("transfer") for p in wrapper] != ["no"]: + fails.append(f"BorrowingWrapper.borrowed: expected transfer 'no', got " + f"{[p.get('transfer') for p in wrapper]}") + + for f in fails: + print(f"FAIL: {f}") + print(f"guarded consume: {len(fails)} failed") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From c662032f7f0cf42923daf8018e640b878db02294 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 17:46:33 +0000 Subject: [PATCH 2/3] Record the #380 baseline transition for the P-037 controls and fact shapes No production logic changes. #380 stopped lowering a guarded release as a call-site release, which moves two records the P-037 evidence pins; both are moved on purpose and in view. Conformance controls: `current` pinned the fabricated release and, for the three G-V4 controls, the known-false-positive OWN003 it caused. It is re-measured on both engines and now equals the `post_a1` record those files have carried since afeca38. The superseded record is kept in each control's append-only remeasured[] entry. Fact shapes: nine shapes re-recorded with `p037_fact_shapes.py record`. Seven guarded callers lose their functions[] record and with it the A2 sidecar; two wrappers move release -> use; two verdicts lose OWN003. Each moved shape gains a baseline_transitions[] entry keeping the superseded facts, verdicts and a2_expect verbatim. The vanished records' a2_expect entries are replaced by an asserted absence ({"record": "absent"}), which the checker now enforces by name, so a record that comes back fails the census instead of being re-pinned. Classified as an accepted baseline movement caused by #380: not a P-037 implementation, not a #304 reopen, not evidence that the A2 contract holds. Canonical first-party call transport remains absent; see docs/notes/p037-fact-shape-baseline-transition-380.md. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp --- .../expected.json | 37 +++- .../gv4-control-mutated-guard/expected.json | 37 +++- .../gv4-control-ref-alias-guard/expected.json | 37 +++- .../expected.json | 31 +++- corpus/p037-shapes/README.md | 15 ++ .../call-expression-statement/expected.json | 157 ++++++++++------- .../guard-bool-const-false/expected.json | 145 +++++++++------- .../guard-bool-const-true/expected.json | 145 +++++++++------- .../guard-forward-bare/expected.json | 71 +++++++- .../guard-forward-negated/expected.json | 72 +++++++- .../p037-shapes/guard-mutated/expected.json | 158 +++++++++++------- .../guard-opaque-expression/expected.json | 141 ++++++++++------ .../p037-shapes/guard-ref-alias/expected.json | 158 +++++++++++------- .../named-arguments-reordered/expected.json | 151 ++++++++++------- ...p037-fact-shape-baseline-transition-380.md | 67 ++++++++ scripts/p037_controls.py | 8 +- scripts/p037_fact_shapes.py | 9 + 17 files changed, 1004 insertions(+), 435 deletions(-) create mode 100644 docs/notes/p037-fact-shape-baseline-transition-380.md diff --git a/corpus/p036-bakeoff/gv4-control-aliased-self-null/expected.json b/corpus/p036-bakeoff/gv4-control-aliased-self-null/expected.json index 89b2ef8f..f26b2941 100644 --- a/corpus/p036-bakeoff/gv4-control-aliased-self-null/expected.json +++ b/corpus/p036-bakeoff/gv4-control-aliased-self-null/expected.json @@ -3,15 +3,13 @@ "control": "gv4-control-aliased-self-null", "p037": "§8 row 19 — G-V4, writably aliased self-null resource parameter", "classification": "KNOWN_FALSE_POSITIVE", - "measured_at": "70189a3", + "measured_at": "f164dd3", "owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3", "call_site_line": 29, "defensive_dispose_line": 30, "current": { - "findings": [ - "OWN003" - ], - "fabricated_release_at_call_site": true + "findings": [], + "fabricated_release_at_call_site": false }, "post_a1": { "findings": [], @@ -37,7 +35,34 @@ } }, "result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs." + }, + { + "at": "f164dd3", + "on": "2026-09-29", + "why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.", + "engines": { + "python": { + "findings": [], + "fabricated_release_at_call_site": false + }, + "rust": { + "findings": [], + "fabricated_release_at_call_site": false + } + }, + "superseded_current": { + "measured_at": "70189a3", + "current": { + "findings": [ + "OWN003" + ], + "fabricated_release_at_call_site": true + } + }, + "result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied" } ], - "note": "Close disposes r through the alias, not the caller's s; today Close(s, other) is lowered to a release of s (may-as-must), so s.Dispose() is a false OWN003. After A1: no split for the aliased q, no release op at the call, the dispose is clean." + "note": "Close disposes r through the alias, not the caller's s; today Close(s, other) is lowered to a release of s (may-as-must), so s.Dispose() is a false OWN003. After A1: no split for the aliased q, no release op at the call, the dispose is clean.", + "resolved_by": "#380 (fix commit f164dd3)" } diff --git a/corpus/p036-bakeoff/gv4-control-mutated-guard/expected.json b/corpus/p036-bakeoff/gv4-control-mutated-guard/expected.json index 99c05ccc..525c1d72 100644 --- a/corpus/p036-bakeoff/gv4-control-mutated-guard/expected.json +++ b/corpus/p036-bakeoff/gv4-control-mutated-guard/expected.json @@ -3,15 +3,13 @@ "control": "gv4-control-mutated-guard", "p037": "§8 row 18a — G-V4, mutated guard (direct write)", "classification": "KNOWN_FALSE_POSITIVE", - "measured_at": "70189a3", + "measured_at": "f164dd3", "owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3", "call_site_line": 39, "defensive_dispose_line": 40, "current": { - "findings": [ - "OWN003" - ], - "fabricated_release_at_call_site": true + "findings": [], + "fabricated_release_at_call_site": false }, "post_a1": { "findings": [], @@ -37,7 +35,34 @@ } }, "result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs." + }, + { + "at": "f164dd3", + "on": "2026-09-29", + "why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.", + "engines": { + "python": { + "findings": [], + "fabricated_release_at_call_site": false + }, + "rust": { + "findings": [], + "fabricated_release_at_call_site": false + } + }, + "superseded_current": { + "measured_at": "70189a3", + "current": { + "findings": [ + "OWN003" + ], + "fabricated_release_at_call_site": true + } + }, + "result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied" } ], - "note": "Today the extractor lowers Outer(r, true) to a release of r (may-as-must ConsumesParam), so the honest r.Dispose() is a false OWN003. After A1 the call must carry no release op and lower to plain + OWN051; the dispose is clean." + "note": "Today the extractor lowers Outer(r, true) to a release of r (may-as-must ConsumesParam), so the honest r.Dispose() is a false OWN003. After A1 the call must carry no release op and lower to plain + OWN051; the dispose is clean.", + "resolved_by": "#380 (fix commit f164dd3)" } diff --git a/corpus/p036-bakeoff/gv4-control-ref-alias-guard/expected.json b/corpus/p036-bakeoff/gv4-control-ref-alias-guard/expected.json index 92e4e10f..dd85fbbd 100644 --- a/corpus/p036-bakeoff/gv4-control-ref-alias-guard/expected.json +++ b/corpus/p036-bakeoff/gv4-control-ref-alias-guard/expected.json @@ -3,15 +3,13 @@ "control": "gv4-control-ref-alias-guard", "p037": "§8 row 18b — G-V4, writable ref-alias of the guard", "classification": "KNOWN_FALSE_POSITIVE", - "measured_at": "70189a3", + "measured_at": "f164dd3", "owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3", "call_site_line": 36, "defensive_dispose_line": 37, "current": { - "findings": [ - "OWN003" - ], - "fabricated_release_at_call_site": true + "findings": [], + "fabricated_release_at_call_site": false }, "post_a1": { "findings": [], @@ -37,7 +35,34 @@ } }, "result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs." + }, + { + "at": "f164dd3", + "on": "2026-09-29", + "why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.", + "engines": { + "python": { + "findings": [], + "fabricated_release_at_call_site": false + }, + "rust": { + "findings": [], + "fabricated_release_at_call_site": false + } + }, + "superseded_current": { + "measured_at": "70189a3", + "current": { + "findings": [ + "OWN003" + ], + "fabricated_release_at_call_site": true + } + }, + "result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied" } ], - "note": "Same mechanism as row 18a; the alias write must disqualify the guard (fail-closed) and the call must not fabricate a consume." + "note": "Same mechanism as row 18a; the alias write must disqualify the guard (fail-closed) and the call must not fabricate a consume.", + "resolved_by": "#380 (fix commit f164dd3)" } diff --git a/corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/expected.json b/corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/expected.json index bb997661..350349a8 100644 --- a/corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/expected.json +++ b/corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/expected.json @@ -3,13 +3,13 @@ "control": "legacy-honesty-else-unresolved-forward", "p037": "G-T2b class 3 — guarded local release, unresolved forward on the other branch", "classification": "VERDICT_COMPATIBLE_VALUE_DIFFERENCE", - "measured_at": "70189a3", + "measured_at": "f164dd3", "owner_ruling": "2026-09-18: accepted as pre-A1 regression anchors, not as authorization for a pre-cutover fix; no ConsumesParam change before P-022 Stage 3", "call_site_line": 41, "defensive_dispose_line": null, "current": { "findings": [], - "fabricated_release_at_call_site": true + "fabricated_release_at_call_site": false }, "post_a1": { "findings": [], @@ -31,7 +31,32 @@ } }, "result": "UNCHANGED — both engines reproduce the `current` record above exactly, on both layers. Stage 3 moved none of this control, which is what the two-layer design predicted: the fabricated release is decided in the Roslyn extractor, before either engine runs." + }, + { + "at": "f164dd3", + "on": "2026-09-29", + "why": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`. The `current` record pinned the fabricated call-site release and, for the three G-V4 controls, the KNOWN_FALSE_POSITIVE OWN003 it caused; once an independent correctness fix removes the release, continuing to require it would require the bug. Re-measured on both engines explicitly.", + "engines": { + "python": { + "findings": [], + "fabricated_release_at_call_site": false + }, + "rust": { + "findings": [], + "fabricated_release_at_call_site": false + } + }, + "superseded_current": { + "measured_at": "70189a3", + "current": { + "findings": [], + "fabricated_release_at_call_site": true + } + }, + "result": "CHANGED — `current` re-recorded to the new measurement, which equals the `post_a1` record this file has carried since the controls landed on main (afeca38, 2026-09-18; the record was measured at 70189a3) and which is unchanged here: the new expectation was not chosen after the fix. P-037 is not implemented by this; `post_a1` being met is a consequence of removing the fabricated release, not of cell selection.", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied" } ], - "note": "0 findings at warning severity today AND after A1 (class 3 is verdict-equivalent). The facts layer differs: today the extractor lowers M(r, flag, sink) to a release (may-as-must) and even the OWN051 advisory is suppressed; after A1 the guarded value is unknown, the call is plain + OWN051 at note level, and no release op may appear at the call site. The value-level pin (unknown, never repaired to may) is the kernel test k11_finding_release_priority_drops_an_unresolved_forward." + "note": "0 findings at warning severity today AND after A1 (class 3 is verdict-equivalent). The facts layer differs: today the extractor lowers M(r, flag, sink) to a release (may-as-must) and even the OWN051 advisory is suppressed; after A1 the guarded value is unknown, the call is plain + OWN051 at note level, and no release op may appear at the call site. The value-level pin (unknown, never repaired to may) is the kernel test k11_finding_release_priority_drops_an_unresolved_forward.", + "resolved_by": "#380 (fix commit f164dd3)" } diff --git a/corpus/p037-shapes/README.md b/corpus/p037-shapes/README.md index 0cbd8029..46fa0984 100644 --- a/corpus/p037-shapes/README.md +++ b/corpus/p037-shapes/README.md @@ -32,3 +32,18 @@ of aggregated into a number. Checked by `scripts/p037_fact_shapes.py`, which names its engine explicitly (#262 Stage 3) and runs one extractor invocation per case. + +## Baseline transitions + +A record that moves because a step *meant* to move it is re-recorded +deliberately, with the move written into the record itself +(`baseline_transitions[]`, which keeps the superseded facts, verdicts and +`a2_expect` verbatim). An `a2_expect` entry of the form +`{"function": …, "record": "absent"}` asserts that a record is gone on +purpose; the checker fails by name if it comes back. + +- **#380** (`23e3203` → `f164dd3`): an independent INF-S2 fix stopped lowering + a guarded release as a call-site release. Seven caller records and their + sidecars disappear, and two wrappers move `release` → `use`. This is not a + P-037 implementation, not a #304 reopen, and not evidence that A2 holds. + See [`docs/notes/p037-fact-shape-baseline-transition-380.md`](../../docs/notes/p037-fact-shape-baseline-transition-380.md). diff --git a/corpus/p037-shapes/call-expression-statement/expected.json b/corpus/p037-shapes/call-expression-statement/expected.json index 10638be6..df2ccaab 100644 --- a/corpus/p037-shapes/call-expression-statement/expected.json +++ b/corpus/p037-shapes/call-expression-statement/expected.json @@ -6,30 +6,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.", "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": { @@ -40,9 +16,14 @@ "predicate": "truth", "negated": true } + }, + { + "function": "ShapeStatementCall.Caller", + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeStatementCall.Inner": { "params": [ @@ -70,42 +51,6 @@ } ] } - }, - "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": { @@ -114,6 +59,94 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeStatementCall.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "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": [] + } + } + }, + "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 + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-bool-const-false/expected.json b/corpus/p037-shapes/guard-bool-const-false/expected.json index 1874469e..5ec8f004 100644 --- a/corpus/p037-shapes/guard-bool-const-false/expected.json +++ b/corpus/p037-shapes/guard-bool-const-false/expected.json @@ -6,24 +6,6 @@ "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": { @@ -31,9 +13,14 @@ "predicate": "truth", "negated": true } + }, + { + "function": "ShapeConstFalse.Caller", + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeConstFalse.Inner": { "params": [ @@ -61,42 +48,6 @@ } ] } - }, - "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": { @@ -105,6 +56,88 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeConstFalse.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "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": [] + } + } + }, + "a2_expect": [ + { + "function": "ShapeConstFalse.Caller", + "call": { + "callee": "ShapeConstFalse.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "bool_const", + "value": false + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-bool-const-true/expected.json b/corpus/p037-shapes/guard-bool-const-true/expected.json index 410dc516..77aa40ea 100644 --- a/corpus/p037-shapes/guard-bool-const-true/expected.json +++ b/corpus/p037-shapes/guard-bool-const-true/expected.json @@ -6,24 +6,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.", "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": "ShapeConstTrue.Caller", - "call": { - "callee": "ShapeConstTrue.Inner", - "args": [ - { - "param": 0, - "kind": "var", - "name": "r" - }, - { - "param": 1, - "kind": "bool_const", - "value": true - } - ] - } - }, { "function": "ShapeConstTrue.Inner", "guard": { @@ -31,9 +13,14 @@ "predicate": "truth", "negated": true } + }, + { + "function": "ShapeConstTrue.Caller", + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeConstTrue.Inner": { "params": [ @@ -61,42 +48,6 @@ } ] } - }, - "ShapeConstTrue.Caller": { - "params": null, - "body": [ - "acquire:r@19", - "release:r@20" - ], - "guarded_facts": { - "version": 1, - "calls": [ - { - "site": { - "line": 20, - "column": 9 - }, - "statement_line": 20, - "form": "statement", - "callee": "ShapeConstTrue.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": { @@ -105,6 +56,88 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeConstTrue.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "ShapeConstTrue.Caller": { + "params": null, + "body": [ + "acquire:r@19", + "release:r@20" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 20, + "column": 9 + }, + "statement_line": 20, + "form": "statement", + "callee": "ShapeConstTrue.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": [] + } + } + }, + "a2_expect": [ + { + "function": "ShapeConstTrue.Caller", + "call": { + "callee": "ShapeConstTrue.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "bool_const", + "value": true + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-forward-bare/expected.json b/corpus/p037-shapes/guard-forward-bare/expected.json index b1f3d694..7dcb5f71 100644 --- a/corpus/p037-shapes/guard-forward-bare/expected.json +++ b/corpus/p037-shapes/guard-forward-bare/expected.json @@ -33,7 +33,7 @@ } } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeForwardBare.Inner": { "params": [ @@ -70,7 +70,7 @@ } ], "body": [ - "release:s@17" + "use:s@17" ], "guarded_facts": { "version": 1, @@ -109,6 +109,71 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (wrapper forward release -> use; sidecar unchanged)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeForwardBare.Outer: body ['release:s@17'] -> ['use:s@17'] (a parameter forwarded to a guarded consumer is a use now, not a release; the sidecar is unchanged)" + ], + "superseded": { + "facts": { + "ShapeForwardBare.Outer": { + "params": [ + { + "name": "s", + "line": 15 + } + ], + "body": [ + "release:s@17" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 17, + "column": 9 + }, + "statement_line": 17, + "form": "statement", + "callee": "ShapeForwardBare.Inner", + "sig": "System.IO.Stream,System.Boolean", + "first_party": true, + "args": [ + { + "param": 0, + "kind": "param", + "source_param": 0 + }, + { + "param": 1, + "kind": "param", + "source_param": 1 + } + ] + } + ], + "guards": [] + } + } + } + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-forward-negated/expected.json b/corpus/p037-shapes/guard-forward-negated/expected.json index 9602cff9..c716c952 100644 --- a/corpus/p037-shapes/guard-forward-negated/expected.json +++ b/corpus/p037-shapes/guard-forward-negated/expected.json @@ -34,7 +34,7 @@ } } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeForwardNegated.Inner": { "params": [ @@ -71,7 +71,7 @@ } ], "body": [ - "release:s@17" + "use:s@17" ], "guarded_facts": { "version": 1, @@ -111,6 +111,72 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (wrapper forward release -> use; sidecar unchanged)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeForwardNegated.Outer: body ['release:s@17'] -> ['use:s@17'] (a parameter forwarded to a guarded consumer is a use now, not a release; the sidecar is unchanged)" + ], + "superseded": { + "facts": { + "ShapeForwardNegated.Outer": { + "params": [ + { + "name": "s", + "line": 15 + } + ], + "body": [ + "release:s@17" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 17, + "column": 9 + }, + "statement_line": 17, + "form": "statement", + "callee": "ShapeForwardNegated.Inner", + "sig": "System.IO.Stream,System.Boolean", + "first_party": true, + "args": [ + { + "param": 0, + "kind": "param", + "source_param": 0 + }, + { + "param": 1, + "kind": "param", + "source_param": 1, + "negated": true + } + ] + } + ], + "guards": [] + } + } + } + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-mutated/expected.json b/corpus/p037-shapes/guard-mutated/expected.json index 686d863b..cafa7c4b 100644 --- a/corpus/p037-shapes/guard-mutated/expected.json +++ b/corpus/p037-shapes/guard-mutated/expected.json @@ -12,24 +12,11 @@ }, { "function": "ShapeMutatedGuard.Caller", - "call": { - "callee": "ShapeMutatedGuard.Inner", - "args": [ - { - "param": 0, - "kind": "var", - "name": "r" - }, - { - "param": 1, - "kind": "bool_const", - "value": true - } - ] - } + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeMutatedGuard.Inner": { "params": [ @@ -43,55 +30,106 @@ "then:release:p@15" ], "guarded_facts": null - }, - "ShapeMutatedGuard.Caller": { - "params": null, - "body": [ - "acquire:r@21", - "release:r@22", - "release:r@23" - ], - "guarded_facts": { - "version": 1, - "calls": [ - { - "site": { - "line": 22, - "column": 9 - }, - "statement_line": 22, - "form": "statement", - "callee": "ShapeMutatedGuard.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": [ - "OWN003:warning@21" - ], - "python": [ - "OWN003:warning@21" - ] + "rust": [], + "python": [] }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeMutatedGuard.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "verdict {'rust': ['OWN003:warning@21'], 'python': ['OWN003:warning@21']} -> {'rust': [], 'python': []} (the fabricated release was the cause of that finding)", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "ShapeMutatedGuard.Caller": { + "params": null, + "body": [ + "acquire:r@21", + "release:r@22", + "release:r@23" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 22, + "column": 9 + }, + "statement_line": 22, + "form": "statement", + "callee": "ShapeMutatedGuard.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": [ + "OWN003:warning@21" + ], + "python": [ + "OWN003:warning@21" + ] + }, + "a2_expect": [ + { + "function": "ShapeMutatedGuard.Caller", + "call": { + "callee": "ShapeMutatedGuard.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "bool_const", + "value": true + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-opaque-expression/expected.json b/corpus/p037-shapes/guard-opaque-expression/expected.json index df249a49..b34fb926 100644 --- a/corpus/p037-shapes/guard-opaque-expression/expected.json +++ b/corpus/p037-shapes/guard-opaque-expression/expected.json @@ -6,23 +6,6 @@ "a2_contract": "{\"param\":1,\"kind\":\"opaque\"} and nothing else. Specifically NOT `\"expr\": \"n > 0 && !flag\"` for something downstream to parse later: humanity already has one C# front end and does not need a second one growing quietly inside a summary engine.", "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": "ShapeOpaqueArg.Caller", - "call": { - "callee": "ShapeOpaqueArg.Inner", - "args": [ - { - "param": 0, - "kind": "var", - "name": "r" - }, - { - "param": 1, - "kind": "opaque" - } - ] - } - }, { "function": "ShapeOpaqueArg.Inner", "guard": { @@ -30,9 +13,14 @@ "predicate": "truth", "negated": true } + }, + { + "function": "ShapeOpaqueArg.Caller", + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeOpaqueArg.Inner": { "params": [ @@ -60,41 +48,6 @@ } ] } - }, - "ShapeOpaqueArg.Caller": { - "params": null, - "body": [ - "acquire:r@19", - "release:r@20" - ], - "guarded_facts": { - "version": 1, - "calls": [ - { - "site": { - "line": 20, - "column": 9 - }, - "statement_line": 20, - "form": "statement", - "callee": "ShapeOpaqueArg.Inner", - "sig": "System.IO.Stream,System.Boolean", - "first_party": true, - "args": [ - { - "param": 0, - "kind": "var", - "name": "r" - }, - { - "param": 1, - "kind": "opaque" - } - ] - } - ], - "guards": [] - } } }, "verdict": { @@ -103,6 +56,86 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeOpaqueArg.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "ShapeOpaqueArg.Caller": { + "params": null, + "body": [ + "acquire:r@19", + "release:r@20" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 20, + "column": 9 + }, + "statement_line": 20, + "form": "statement", + "callee": "ShapeOpaqueArg.Inner", + "sig": "System.IO.Stream,System.Boolean", + "first_party": true, + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "opaque" + } + ] + } + ], + "guards": [] + } + } + }, + "a2_expect": [ + { + "function": "ShapeOpaqueArg.Caller", + "call": { + "callee": "ShapeOpaqueArg.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "opaque" + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/guard-ref-alias/expected.json b/corpus/p037-shapes/guard-ref-alias/expected.json index 3cb19ced..0867af03 100644 --- a/corpus/p037-shapes/guard-ref-alias/expected.json +++ b/corpus/p037-shapes/guard-ref-alias/expected.json @@ -12,24 +12,11 @@ }, { "function": "ShapeRefAliasGuard.Caller", - "call": { - "callee": "ShapeRefAliasGuard.Inner", - "args": [ - { - "param": 0, - "kind": "var", - "name": "r" - }, - { - "param": 1, - "kind": "bool_const", - "value": true - } - ] - } + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeRefAliasGuard.Inner": { "params": [ @@ -43,55 +30,106 @@ "then:release:p@18" ], "guarded_facts": null - }, - "ShapeRefAliasGuard.Caller": { - "params": null, - "body": [ - "acquire:r@24", - "release:r@25", - "release:r@26" - ], - "guarded_facts": { - "version": 1, - "calls": [ - { - "site": { - "line": 25, - "column": 9 - }, - "statement_line": 25, - "form": "statement", - "callee": "ShapeRefAliasGuard.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": [ - "OWN003:warning@24" - ], - "python": [ - "OWN003:warning@24" - ] + "rust": [], + "python": [] }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeRefAliasGuard.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "verdict {'rust': ['OWN003:warning@24'], 'python': ['OWN003:warning@24']} -> {'rust': [], 'python': []} (the fabricated release was the cause of that finding)", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "ShapeRefAliasGuard.Caller": { + "params": null, + "body": [ + "acquire:r@24", + "release:r@25", + "release:r@26" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 25, + "column": 9 + }, + "statement_line": 25, + "form": "statement", + "callee": "ShapeRefAliasGuard.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": [ + "OWN003:warning@24" + ], + "python": [ + "OWN003:warning@24" + ] + }, + "a2_expect": [ + { + "function": "ShapeRefAliasGuard.Caller", + "call": { + "callee": "ShapeRefAliasGuard.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "r" + }, + { + "param": 1, + "kind": "bool_const", + "value": true + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/corpus/p037-shapes/named-arguments-reordered/expected.json b/corpus/p037-shapes/named-arguments-reordered/expected.json index f281304e..06cf0b81 100644 --- a/corpus/p037-shapes/named-arguments-reordered/expected.json +++ b/corpus/p037-shapes/named-arguments-reordered/expected.json @@ -6,27 +6,6 @@ "a2_contract": "a2 emits a `call` op here whose `arg_bindings` resolve BY DECLARED PARAMETER INDEX, so this reordered call and a positional `Inner(s, true)` produce the same bindings: param 0 -> {kind: var, name: s}, param 1 -> {kind: bool_const, value: true}. Source order is Roslyn's problem and stops being anyone else's. The legacy `args: string[]` field keeps its current contents and meaning — additive only, so the Python rollback reads an unchanged document.", "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": "ShapeNamedArgs.Caller", - "call": { - "site": { - "line": 21 - }, - "callee": "ShapeNamedArgs.Inner", - "args": [ - { - "param": 0, - "kind": "var", - "name": "s" - }, - { - "param": 1, - "kind": "bool_const", - "value": true - } - ] - } - }, { "function": "ShapeNamedArgs.Inner", "guard": { @@ -34,9 +13,14 @@ "predicate": "truth", "negated": true } + }, + { + "function": "ShapeNamedArgs.Caller", + "record": "absent", + "since": "#380" } ], - "measured_at": "464308b", + "measured_at": "f164dd3", "facts": { "ShapeNamedArgs.Inner": { "params": [ @@ -64,42 +48,6 @@ } ] } - }, - "ShapeNamedArgs.Caller": { - "params": null, - "body": [ - "acquire:s@20", - "release:s@21" - ], - "guarded_facts": { - "version": 1, - "calls": [ - { - "site": { - "line": 21, - "column": 9 - }, - "statement_line": 21, - "form": "statement", - "callee": "ShapeNamedArgs.Inner", - "sig": "System.IO.Stream,System.Boolean", - "first_party": true, - "args": [ - { - "param": 0, - "kind": "var", - "name": "s" - }, - { - "param": 1, - "kind": "bool_const", - "value": true - } - ] - } - ], - "guards": [] - } } }, "verdict": { @@ -108,6 +56,91 @@ }, "status_history": [ "pending_a2 (recorded at 464308b)", - "anchored (A2.1 sidecar)" + "anchored (A2.1 sidecar)", + "anchored — baseline transition #380 at f164dd3 (caller record absent; A2 carrier lost, asserted as absent)" + ], + "baseline_transitions": [ + { + "id": "380", + "on": "2026-09-29", + "from": { + "measured_at": "464308b", + "extractor": "23e3203" + }, + "to": { + "measured_at": "f164dd3" + }, + "cause": "PhysShell/Own.NET#380 — an independent INF-S2 correctness fix: ConsumesParam now counts a release (or a forward to another consumer) only when it is definite on every normal-return path of the callee, so a guarded one is no longer lowered as the caller's `release`", + "classification": "ACCEPTED BASELINE MOVEMENT CAUSED BY #380 — NOT a P-037 implementation, NOT a reopen of #304, NOT evidence that the A2 contract is satisfied", + "consequences": [ + "ShapeNamedArgs.Caller: record no longer emitted — its only tracked local now escapes instead of being released at the guarded call, so the method has no tracked local and no owned parameter, and its guarded_facts sidecar goes with it", + "a2_expect entries for the vanished record(s) are superseded and replaced by asserted record absence; their promise is NOT met by this baseline" + ], + "superseded": { + "facts": { + "ShapeNamedArgs.Caller": { + "params": null, + "body": [ + "acquire:s@20", + "release:s@21" + ], + "guarded_facts": { + "version": 1, + "calls": [ + { + "site": { + "line": 21, + "column": 9 + }, + "statement_line": 21, + "form": "statement", + "callee": "ShapeNamedArgs.Inner", + "sig": "System.IO.Stream,System.Boolean", + "first_party": true, + "args": [ + { + "param": 0, + "kind": "var", + "name": "s" + }, + { + "param": 1, + "kind": "bool_const", + "value": true + } + ] + } + ], + "guards": [] + } + } + }, + "a2_expect": [ + { + "function": "ShapeNamedArgs.Caller", + "call": { + "site": { + "line": 21 + }, + "callee": "ShapeNamedArgs.Inner", + "args": [ + { + "param": 0, + "kind": "var", + "name": "s" + }, + { + "param": 1, + "kind": "bool_const", + "value": true + } + ] + } + } + ] + }, + "known_limitation": "canonical first-party call transport remains absent: the honest call reaches the facts only through the sidecar of a record that ordinary relevance filtering may drop", + "note": "docs/notes/p037-fact-shape-baseline-transition-380.md" + } ] } diff --git a/docs/notes/p037-fact-shape-baseline-transition-380.md b/docs/notes/p037-fact-shape-baseline-transition-380.md new file mode 100644 index 00000000..96e52542 --- /dev/null +++ b/docs/notes/p037-fact-shape-baseline-transition-380.md @@ -0,0 +1,67 @@ +# P-037 fact-shape baseline transition — #380 + +A baseline transition of the P-037 fact-shape census (`corpus/p037-shapes`) and +the conformance controls (`corpus/p036-bakeoff`), caused by an independent +production fix. It is recorded here and in every moved record +(`baseline_transitions[]` on a shape, `remeasured[]` on a control) so the +records are moved on purpose and in view. + +## Old and new baseline + +| | commit | what the lowering did at a guarded first-party call | +|---|---|---| +| old | `23e3203` | `ConsumesParam` treated any immediate `Dispose`/`Close` of the parameter as a consume, so a *guarded* release was lowered as an unconditional `release` of the caller's argument (the fabricated `must`). Guarded caller records survived **because** of that fabricated release. | +| new | `f164dd3` | #380: a release, or a forward to another consumer, counts only when it is definite on every normal-return path of the callee (INF-S2). A guarded one is no longer a call-site release. | + +## Intentional consequences + +- **Some local-caller records disappear.** A caller whose only tracked local + is handed to a guarded consumer no longer releases it at the call. The local + becomes an ordinary escape, so the method has no tracked local and no owned + parameter, and its `functions[]` record is not emitted. Its `guarded_facts` + sidecar goes with it. Shapes: `call-expression-statement`, + `guard-bool-const-false`, `guard-bool-const-true`, `guard-mutated`, + `guard-opaque-expression`, `guard-ref-alias`, `named-arguments-reordered`. +- **Parameter-forward wrappers move `release` → `use`.** Shapes: + `guard-forward-bare`, `guard-forward-negated`. Their sidecar is unchanged. +- **Two verdicts move.** `guard-mutated` and `guard-ref-alias` lose the + `OWN003` that the fabricated release caused. +- **The guarded call sidecar is no longer guaranteed to survive** ordinary + relevance filtering: it lives on a record that relevance filtering may drop. +- **The four conformance controls' `current` now equals their `post_a1`**: + no fabricated release, and no `OWN003` on the three G-V4 controls. `post_a1` + itself is unchanged; it has been in the files since the controls landed + (`afeca38`, measured at `70189a3`). + +## How the loss is kept visible + +The `a2_expect` entries that promised a record with a sidecar for a vanished +caller are **not deleted**. They are copied verbatim into the shape's +`baseline_transitions[].superseded.a2_expect` and replaced by an asserted +absence, `{"function": …, "record": "absent", "since": "#380"}`. +`scripts/p037_fact_shapes.py` checks that assertion by name. A record that +comes back — for example once first-party calls reach the facts canonically — +fails the census instead of being silently re-pinned. The superseded facts and +verdicts are kept in the same place. + +## Classification + +**ACCEPTED BASELINE MOVEMENT CAUSED BY #380.** + +- NOT a P-037 implementation: no cell selection, no guard value read, no + `guarded_facts` consumer, no OwnIR, schema or lattice change. +- NOT a reopen of #304: reopen condition 1 is **not** met. The legacy body + still folds first-party forwards (into `release` for definite consumers, into + `use` for parameters, and now into an escape for guarded locals), and no + `call` op reaches either engine. +- NOT evidence that the A2 contract is satisfied: for the seven shapes above, + the A2 promise is explicitly not met by this baseline. + +## Known limitation + +**Canonical first-party call transport remains absent.** The honest call +reaches the facts only through the sidecar of a record that ordinary relevance +filtering may drop. INF-S3 would summarize a wrapper that forwards its parameter +to a guarded consumer as `may`; today it is `no`, because the forward is folded +into a `use`. Reaching `may` needs a canonical call representation, which is +outside #380. diff --git a/scripts/p037_controls.py b/scripts/p037_controls.py index 253da487..9eafeef6 100755 --- a/scripts/p037_controls.py +++ b/scripts/p037_controls.py @@ -11,6 +11,12 @@ BOTH what Owen does today (``current``) and what A1 must make it do (``post_a1``), so the evidence lies about neither. +Since #380 (an independent INF-S2 correctness fix, not P-037) ``ConsumesParam`` +no longer lowers a guarded release as a call-site release, and ``current`` was +re-measured to what now happens — which equals ``post_a1``. The superseded +record is kept in each control's ``remeasured[]``; see +docs/notes/p037-fact-shape-baseline-transition-380.md. + Two layers, because the emitted facts show the defect is decided in the extractor before either engine runs (docs/notes/p037-formal-kernel.md §8.2): @@ -176,7 +182,7 @@ def main(argv: list[str]) -> int: file=sys.stderr, ) return 2 - layer = "post-A1 acceptance" if args.post_a1 else "current record (measured at 70189a3)" + layer = "post-A1 acceptance" if args.post_a1 else "current record (each control's measured_at)" print(f"P-037 controls — checking the {layer}, engine={args.engine}") all_ok = True for control in controls: diff --git a/scripts/p037_fact_shapes.py b/scripts/p037_fact_shapes.py index abe1108c..e989a713 100755 --- a/scripts/p037_fact_shapes.py +++ b/scripts/p037_fact_shapes.py @@ -145,6 +145,15 @@ def a2_problems(spec: dict[str, Any], facts: dict[str, Any]) -> list[str]: for exp in spec.get("a2_expect", []): fn = exp.get("function") rec = facts.get(fn) if isinstance(fn, str) else None + # Record ABSENCE as an asserted fact (#380 baseline transition): the record, and + # with it the sidecar, is gone on purpose. Asserting it keeps the loss visible — a + # record that comes back (e.g. once first-party calls reach the facts canonically) + # fails here by name instead of being silently re-pinned. + if exp.get("record") == "absent": + if rec is not None: + problems.append(f"{fn}: expected NO function record (see the shape's " + f"baseline_transitions), got one") + continue if rec is None: problems.append(f"{fn}: no function record") continue From 410431a45be33770dfa09b0b2b78b524caebeedd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 18:12:05 +0000 Subject: [PATCH 3/3] docs(#380): scope the definiteness comment and pin the dynamic-forward limitation The comment on IsDefiniteInBody claimed that declining a partial release "never invents the opposite verdict". That holds for owned locals, which become untracked escapes, but not for forwarded parameters: the remaining `use` lets the existing inference derive `no`, which is right for a false guard and wrong for a true or forwarded one. The comment now says what #380 guarantees (no fabricated `must`) and what it does not (INF-S2's `may`). Comment-only change; the algorithm is untouched. GuardedConsumeSample.ForwardDynamic forwards both its parameter and the guard. INF-S3 would summarize it `may`; today it is `no`. tests/test_guarded_consume.py pins `no` as a KNOWN LIMITATION, not as acceptance, and fails with a message naming the direction if it moves: `must` means the fabricated consume is back; `may` means a canonical call fact reached the core, so the pin must be re-recorded and #304's reopen condition 1 re-checked. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017znWXJbuLfmfZ7Un9GXzNp --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 14 +++++++---- .../roslyn/samples/GuardedConsumeSample.cs | 10 ++++++++ tests/test_guarded_consume.py | 23 +++++++++++++++++++ 3 files changed, 43 insertions(+), 4 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 7103683d..3d64e9c2 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -5019,10 +5019,16 @@ static bool DisposesLocal(SyntaxNode body, string name) // derives `may` for it (INF-S2), and flattening it to a call-site release is the fabricated // `must` the precision floor forbids — a false OWN002/OWN003/OWN009 at a caller that keeps the // resource (`Close(s, dispose: false)`), and a false `must` summary on a wrapper that forwards -// its own parameter that way. Declining here never invents the opposite verdict: a declined -// argument stays an ordinary escape (an untracked local, a used parameter), not a borrow the -// caller is charged for. Purely syntactic and deliberately conservative — the guard's value -// is never read, and an unrecognised shape is not definite (it costs a use-after-handoff +// its own parameter that way. +// +// Declining here avoids fabricating an unconditional `must`; it does NOT produce INF-S2's +// `may`. For an owned LOCAL the declined argument is an ordinary escape: the local goes +// untracked and the caller stays silent. For a forwarded PARAMETER the remaining `use` lets the +// existing inference derive `no` — right when the guard is false, not when it is true or +// forwarded (GuardedConsumeSample.ForwardDynamic pins that as a known limitation). A partial +// forward is only representable as `may` through a canonical call fact, which is outside #380. +// Purely syntactic and deliberately conservative: the guard's value is never read, and an +// unrecognised shape is treated as not definite (for a local that costs a use-after-handoff // finding, never a false one). static bool IsDefiniteInBody(SyntaxNode site, SyntaxNode body) { diff --git a/frontend/roslyn/samples/GuardedConsumeSample.cs b/frontend/roslyn/samples/GuardedConsumeSample.cs index 1caa06c2..acc79032 100644 --- a/frontend/roslyn/samples/GuardedConsumeSample.cs +++ b/frontend/roslyn/samples/GuardedConsumeSample.cs @@ -110,4 +110,14 @@ public static void BorrowingWrapper(Stream borrowed) { MaybeClose(borrowed, false); } + + // KNOWN LIMITATION, pinned rather than accepted: the guard is forwarded, so whether the + // stream is consumed depends on the caller. INF-S3 would summarize this `may` (a forward to a + // `may` callee); today the forward is folded into a `use` and the summary is `no`. Reaching + // `may` needs a canonical first-party call fact, outside #380. When that representation + // lands this pin moves, and #304's reopen condition 1 is due for a re-check. + public static void ForwardDynamic(Stream forwarded, bool dispose) + { + MaybeClose(forwarded, dispose); + } } diff --git a/tests/test_guarded_consume.py b/tests/test_guarded_consume.py index 576bf12b..85919e82 100644 --- a/tests/test_guarded_consume.py +++ b/tests/test_guarded_consume.py @@ -23,6 +23,14 @@ plus the wrapper case: a parameter forwarded with the guard false summarizes as `no`. +And one PINNED KNOWN LIMITATION, which is not acceptance: `ForwardDynamic` forwards its own +parameter AND the guard, so INF-S3 would summarize it `may`. Today the forward is folded +into a `use`, so the summary is `no`. #380 guarantees no fabricated `must`; it does not +guarantee `may`. The pin is there so that the move is loud: if a canonical first-party call +fact ever carries this forward to the core, the pin turns red and should be re-recorded, +and #304's reopen condition 1 is due for a re-check. A move to `must` would mean the +fabricated consume is back. + Line numbers are read off the fixture's text, not hard-coded, so an edit to the comments cannot silently shift what is being checked. @@ -148,6 +156,21 @@ def run() -> int: fails.append(f"BorrowingWrapper.borrowed: expected transfer 'no', got " f"{[p.get('transfer') for p in wrapper]}") + # KNOWN LIMITATION pin (see the module docstring): `no` is today's value, not the right one. + dynamic_name = "GuardedConsumeSample.ForwardDynamic" + dynamic = [p.get("transfer") for d in docs if d.get("method", "").endswith(dynamic_name) + for p in d.get("params", []) if p.get("name") == "forwarded"] + if dynamic != ["no"]: + if dynamic == ["must"]: + why = "the fabricated consume is back (#380 regressed)" + elif dynamic == ["may"]: + why = ("the INF-S3 `may` arrived — canonical call facts likely landed: re-record this " + "pin and re-check #304 reopen condition 1") + else: + why = "the representation moved; classify it before re-recording this pin" + fails.append(f"KNOWN-LIMITATION PIN MOVED: ForwardDynamic.forwarded is {dynamic}, " + f"pinned ['no'] — {why}") + for f in fails: print(f"FAIL: {f}") print(f"guarded consume: {len(fails)} failed")