Repository navigation
Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304
Description
Activity
- added 9 commits that reference this issue
on Jul 25, 2026 Governance amendment — Stage 3 landed, A1 unblocked, and two clauses in the body above are superseded
This is the P-037 A1 Phase-0.2 correction. Two of the governance clauses in the issue body were written against the design as accepted at
4a01f0eand have since been changed by owner rulings. They are the clauses A1 will be held to, so leaving them stale would have meant gating A1 on a contract nobody still holds. The body's original wording is preserved above; this comment is the amendment of record.Status
item state P-022 Stage 3 (#262) LANDED — merged as #359, mainat63148d0#304 gate ("no verdict-changing implementation before cutover") DISCHARGED — the condition is met, not waived P-037 A0 (formal kernel spike) DONE / KEEP — terminal 9523fac, 22/22 Kani harnesses provenP-037 A0.5 (the G-T2 correction) DONE — 7cf1f93P-037 A1 prep (controls, expectations, two-layer checker) DONE — 7751d1b,ce2e6bcP-037 A1 production (the guarded-transfer kernel in the engine) READY TO START — acceptance in docs/notes/p037-formal-kernel.md§8.1Amendment 1 — G-T2 is split into G-T2a and G-T2b
Body says: "G-T1 precision floor and G-T2 post-finalization lax refinement (
≤, not equality) with the residual-⊥ lemma as implementation proof obligations".Superseded by the A0.5 ruling (
7cf1f93). The single G-T2 was not provable as stated, and the formal kernel is what found it — not inspection. It is now two obligations, and they live at different levels:- G-T2a — algebraic collapse refinement, stated PRE-finalization.
C(lfp F_G) ≤ lfp F_Cagainst the collapsed semantic system. Machine-checked informal/p037-kernel(K11 one-step on symbolic 3-coordinate SCCs; the lfp form on 2-coordinate SCCs). - G-T2b — legacy observational compatibility, verdicts not values. At the INF-A1 lowering, against today's actual
_build_skeletonsderivation.
The reason the split is load-bearing and not bookkeeping: finalization does not commute with collapse.
C(fin(must, ⊥)) = maywhilefin(C(must, ⊥)) = must. So the bare collapsed system is not a post-finalization bound, and §8 row 14 is the standing witness —F(p, g) { if (g) release p; else F(p, g); }collapses tomaywhereF_Csaysmust, which is simply wrong forF(p, false).And the value-level
≤against legacy is outright false, with a pinned counterexample the kernel produced (K11′):if (g) p.Dispose(); else Extern(p);withExternunresolved is guarded(must, unknown), collapseunknown, while today's release priority saysmay.unknown ≰ may— and the guarded value is the honest one, because theelsepath hands the resource to code nobody has summarized. A theorem that holds only after the inconvenient programs are removed by hypothesis is not a contract for a static analyzer, so that claim was dropped rather than narrowed.Amendment 2 — three declared difference classes, not two
Body says: "exactly two declared verdict-change classes (application refinement via cell selection; summary refinement via cellwise derivation + guard-aware edges)", and in Acceptance: "the two P-037 verdict-change classes are the only permitted diffs against the collapsed-view golden dumps".
Superseded. There are three, and the third is deliberately not a verdict-change class:
- APPLICATION_REFINEMENT — cell selection at the final call site (G-A1/G-A2 route 1).
- SUMMARY_REFINEMENT — cellwise derivation plus guard-aware edge transforms refining today's path-insensitive skeleton, no selection at the final site; the guarded value is strictly below today's. Three shapes, one phenomenon: release/forward separation, forward/forward separation, and const specialization through a wrapper on a
None-election coordinate. - LEGACY_HONESTY — the guarded value is
unknownwhere today saysmay, because today's release priority dropped a forward to an unresolved callee. Both lower toplain+ OWN051, so the verdict is unchanged.
Class 3 exists precisely so that the
unknown ≰ maycase has somewhere honest to go instead of being repaired away. Two failure modes are named and both are defects:- an implementation that "repairs"
unknownback tomayto match legacy has re-introduced the optimism the class was created to expose; - an implementation that turns it into a finding has invented a class.
No fourth class by convenience
Standing rule, carried over verbatim in force: a collapsed-view difference outside these three is a defect of the implementation or of the contract, never a fourth class by fiat; and a class-3 difference that changes a verdict is a defect, not a refinement. If A1 produces a diff that fits none of the three, the correct outcome is that A1 is wrong or this contract is wrong — not that the taxonomy grows.
Amendment 3 — the gate clause
Body says: "Gate. Blocked on the P-022 parity/cutover discipline (#262): no verdict-changing implementation before cutover."
The condition is now met. The rest of that clause stands unchanged and is not softened: "The landed predicates are the regression floor — no fixture they catch (or deliberately keep silent) may regress." That was never conditional on the cutover.
Phase 0.1 — the pre-A1 anchors, re-measured against the post-cutover baseline
The four conformance controls'
currentrecords were measured at70189a3, when a bareown-check.shmeant Python. Since Stage 3 the same bare invocation means Rust, so the records were re-taken, not rewritten:measured_at,currentandpost_a1are byte-identical to the source branch, and eachexpected.jsongains an append-onlyremeasured[]entry.Measured on both engines explicitly, at
main63148d0:P-037 controls — checking the current record (measured at 70189a3), engine=both ok gv4-control-aliased-self-null python/rust findings=['OWN003'] fabricated@29=True ok gv4-control-mutated-guard python/rust findings=['OWN003'] fabricated@39=True ok gv4-control-ref-alias-guard python/rust findings=['OWN003'] fabricated@36=True ok legacy-honesty-else-unresolved-forward python/rust findings=[] fabricated@41=True RESULT: all match (--post-a1: MISMATCH 4/4, rc=1, as designed)UNCHANGED on both layers under both engines. The cutover moved none of it, so the Phase-0 STOP condition did not trigger. The two engines agreeing is the two-layer design paying out rather than luck: the fabricated
releaseis emitted by the Roslyn extractor before either engine sees a fact, which is what the facts already suggested and this now confirms by running both. The consequence for A1 is worth stating as the inference it is — A1's first target is extractor-side, and a fix visible only under--engine rustwould be evidence of a second mechanism, not of the fix.
Generated by Claude Code
- G-T2a — algebraic collapse refinement, stated PRE-finalization.
A1 has a missing fact-surface prerequisite before the guarded engine work
Found while scoping A1.1. This does not change P-037's architecture — it changes A1's order, and it inserts a prerequisite that has to land before any guarded-lattice code is written.
Stating the framing precisely, because the sloppy version of this sentence is wrong: it is not "A1's target is the fact surface rather than the engine". The engine work is still exactly what P-037 §8.1 says it is. What changed is that a layer of wiring between the C# frontend and the already-existing MOS turns out to be absent, and nothing downstream can be built on facts that were thrown away at the door.
MEASURED OBSERVATION — the existing MOS is already honest about
must/may/noHand-fed OwnIR documents (one per row; only the callee's body differs,
params[]present,callop forwardings), run against the Rust core at63148d0+ the A1.0 port:callee body MOS transfer verdict if (…) release s— guardedmayOWN051advisory, optimistic untrackrelease s— unconditionalmustclean (ownership transferred) use s— borrow onlynoOWN001leakThree-way discrimination, all three correct.
lower.rs:858even says so in as many words — "a kept path exists, so the join ismay, never a flattenedmust."Two consequences worth separating:
- Good news. The last row is the F3 target verdict. Once a guard resolves to "this call does not consume", the engine already produces
OWN001with no further change. The verdict machinery is finished. - Not yet P-037.
mayis honest, not precise. TurningmayintoSplit(keep, no, must)and selecting a cell atClose(s, keep: true)is the guarded-kernel work, and it is untouched by any of this.
MEASURED OBSERVATION — none of that layer runs for C#
Three defects, each verified against the tree rather than inferred:
frontend/roslyn/OwnSharp.Extractor/Program.cs:6621—if (tracked.Count == 0) continue;. A method is emitted intofunctions[]only when it has tracked disposable locals.Close(Stream s, bool keep)has only a parameter, so it is dropped before a record exists.- The extractor emits no
paramsfield and noeffectfield anywhere.build_skeletonsreadsf.get("params")— a field the C# frontend has never produced. (The onlyparamsinProgram.csis the C#params string[]keyword at:4481.) - The OwnIR
callop cannot express a constant argument.argsholds variable names only; a literaltrueis refused withundefined name 'true'. So cell selection has no fact-level input either.
Net effect, confirmed on
guarded-consume-flag-branch,guarded-consume-wrapper-forwardandgv4-control-mutated-guard: the emittedfunctions[]contains only the caller. The guard-holding callee is absent entirely. The engine is not wrong about these programs — it is handed facts from which the guard and the callee have already been erased, byConsumesParamanswering the same question syntactically and flatteningmaytomust.gv4-control-mutated-guard's facts readacquire r@38,release r@39(fabricated),release r@40(the honestr.Dispose()) — two releases, hence the falseOWN003. The false positives and the F3 false negatives are one mechanism seen from two sides.OWNER RULING (2026-09-18) — feed the existing layer; do not fix
ConsumesParamin placeTeaching
ConsumesParamto return a guarded transfer and selecting cells inside the extractor was rejected, as the trap the earlier ruling already named: a few more conditions and there is a second guarded-summary engine written in Roslyn predicates under the name of fixing one function.The layering, as ruled:
Roslyn C# ↓ HONEST FACT SURFACE ← the missing prerequisite ↓ existing MOS machinery ↓ P-037 extension: Election · Split cells · const-pos/const-neg · id/neg/opaque · finalize · apply/select ↓ verdictThe frontend reports raw canonical semantic facts; it never reports P-037 interpretations. OwnIR gains no
const-pos,idornegvocabulary — those are interpretations relative to the callee's elected guard, and they belong to Rust:{ "arg": { "kind": "bool_const", "value": true } } { "arg": { "kind": "param", "name": "g", "negated": true } }from which Rust derives
bool_const(true) → const-pos,g → id,!g → neg, anything else →opaque. Same rule forif: Roslyn says what the condition means, never which summary cell to select. The boundary staysRoslyn: syntax + symbol semantics, guard eligibility / stability evidenceagainstRust: P-037 semantics— and notRoslyn: secretly half of P-037againstRust: the other half, probably.tracked.Count == 0is not to be deleted. Dropping thecontinuewould make the frontend emit a mass of previously non-existent functions, including irrelevant ones — a five-figure diff bought with one line that looked suspicious. The replacement is an eligibility predicate:emit flow function iff: tracked locals exist OR it has ownership-relevant disposable params OR it is otherwise required as an interprocedural summary targetwith body lowering taught to handle parameter handles, not only tracked locals.
Sequence (ruled)
A1.1 FACT SURFACE ↓ prove richer facts, SAME verdicts A1.1 GUARDED KERNEL ↓ prove integration before the semantic cut RETIRE the ConsumesParam-derived fabricated releases ↓ F3 red→green · G-V4 red→green · three-class diff · unexplained = 0first commits:
- A1.1-a1 — parameter-bearing functions reach OwnIR,
params[]populated, zero semantic cut; - A1.1-a2 — guard / call-argument fact vocabulary, zero semantic cut;
- then kernel integration, then retirement of
ConsumesParam's fabricated release.
A1.1 lands on a branch cut from
mainafter #360 (A1.0 bootstrap) merges — not stacked on it. A1.1 touches OwnIR vocabulary and frontend facts, so it is a production contract change and does not belong on top of a bootstrap PR that is already ready to merge.Note on A0
The formal work was not premature. It now functions as the specification of which facts the frontend is obliged to preserve for any downstream analysis to be entitled to these conclusions — which is a considerably better place to learn it than 1500 lines into the Rust, having discovered the extractor binned
gat the door.
Generated by Claude Code
- Good news. The last row is the F3 target verdict. Once a guard resolves to "this call does not consume", the engine already produces
Correction to the diagnosis above, and A1.1-a1 landed
Two things in the fact-surface diagnosis were wrong in detail. The conclusions hold; the details are what someone would go and read, so they get fixed here.
The gate is
Program.cs:6509, not:6621That comment said a method is dropped at
if (tracked.Count == 0) continue;(:6621). There are two gates in that loop, and a parameter-only method never reaches the second:6446 foreach (var method in cls.Members.OfType<BaseMethodDeclarationSyntax>()) 6509 if (candidates.Count == 0) continue; <-- Close(Stream s, bool keep) exits HERE 6621 if (tracked.Count == 0) continue;candidatesis the set of disposable locals.Close(Stream s, bool keep)has none, so it leaves at:6509and the second gate never sees it. A patch applied only at:6621— the line that comment names — builds, runs, and changes nothing at all. Found the way anyone following that citation would find it, by applying it and watching nothing happen. Both gates now admit a method with an ownership-relevant parameter.The predicate is
IsOwnedDisposableType, notImplementsIDisposableConsumesParamuses the strictImplementsIDisposable, which demands a resolved symbol and silently answers false for any type the compilation cannot see — on a single-file run, most of the BCL. Locals useIsOwnedDisposableType, which falls back to the syntactic name heuristic precisely for that case and says so in its own comment. Parameters now use the same predicate as locals: a frontend that tracks aStreamlocal but not aStreamparameter is inconsistent about one type for no reason a reader could defend.A1.1-a1 is done —
claude/p037-a1-production,464308bParameter-bearing methods reach OwnIR with
params[]; lowering runs over locals and owned parameters;paramsrides only when non-empty so every other record keeps its exact previous shape.ConsumesParamis untouched and nothing reads the new field to change a verdict — the semantic cut is a later step, deliberately, so a verdict movement here is a defect rather than a feature.The callees now reach the facts:
Guarded.Close params=[{s,14}] body=[if@16] guarded -> may GuardedWrapper.Inner params=[{s,9}] body=[if@11] guarded -> may GuardedWrapper.Outer params=[{s,17}] body=[release:s@19]That third line deserves a second reading.
Outermerely callsInner(s, keep), butConsumesParamjudgesInnera consumer, so areleaseis emitted where acallbelongs, andOuternow enters the summary layer as an unconditional consumer. The fabrication does not only corrupt the caller's facts; now that summaries exist it will corrupt those too. That is not a regression introduced by a1 — it is the reason retiringConsumesParamis its own later step, and it is now visible rather than implied.One real defect on the way, and what it teaches
The first version of a1 turned six CI jobs red:
[OWN004] 'parg_59' is a borrow and cannot be returned (it would outlive the resource it borrows)on
samples/OverloadSigSample.cs:public static FileStream Open(FileStream existing, bool flush) { ... return existing; // returns a PARAMETER -> not fresh }
The rule at that site already said what it meant — "a tracked LOCAL returned BARE is a fresh-factory transfer" — and held for free only because a parameter could never be in the set. a1 put owned parameters there, so
return existinglowered as a fresh return, and the core read a fresh return of something it never saw acquired as an escaping borrow. The core was right and the fact was wrong: the resource belongs to the caller and outlives the call.What that return actually is, is an alias of the parameter, and OwnIR cannot say so —
aliasOf/aliasedare reserved in the schema and the production skeleton builder has never emitted them (own-bridge/src/mos.rsstates this in its own header). So the frontend keeps the silence it has always kept there rather than asserting a kind that is false. Teaching the IR alias returns is a semantic change and not a1's business; the gap is now named instead of filled with an invention.Zero semantic cut, on two independent sources
corpus, 137 files, clean trees, 17e7285 -> 2de574a rust verdict UNCHANGED all levels UNCHANGED python verdict UNCHANGED all levels UNCHANGED the repository's own C#, 81 files, main's extractor vs a1's frontend/ + audit/ rust 165 · python 165 IDENTICAL frontend/roslyn/samples (dogfood) 164 IDENTICAL, rc=1 the five --flow-locals samples 40 IDENTICALWhy two sources. The 137-file corpus reported UNCHANGED for the broken version of a1 as well. It contains no method that returns its own disposable parameter; the repository's tree does. The corpus is labelled for verdicts, and a1 changes the fact surface — not the same coverage question. A corpus can be complete for the bugs it names and still miss the syntax that breaks a lowering, and treating a green corpus as a green change is exactly how the broken version got pushed. The repo-tree comparison stays in the gate for a2.
Both were run against
origin/main's extractor, not against the previous commit — a mistake made once here and worth naming: the previous commit already carried the broken a1, so diffing against it answered a different question with total confidence.Next: A1.1-a2, the guard / call-argument fact vocabulary, same zero-semantic-cut obligation. Two things found while reading that shape the step: the C# lowering emits a
callop in exactly one place and only forvar x = Foo(...)— a statement-levelClose(s, keep: true);produces nocallat all — andargsdrops named arguments outright (a.NameColon is null), which is every one of the F3 fixtures. The comment there is right that keeping a named argument in syntactic order would mis-align a positional mapping; the fix is to resolve it to its parameter position, not to discard it.
Generated by Claude Code
32 remaining items
- added 15 commits that reference this issue
on Sep 28, 2026
Tracker for P-036 Phase 2 (#303) — the first post-cutover feature consumer of the interprocedural summary architecture.
Context
Soundness: OWN001 treats any
-=in the class as a release — a-=behind a flag, or in a method nobody calls, silently swallows a real leak (heap-proven on SectorTS) #278 (closed) is the historical motivating incident: a-=that exists syntactically but never runs (flag-guarded, in a non-teardown method, or in a method nobody calls) — heap-proven on SectorTS.PR fix(extractor): #278 — a
-=releases only in a proven, unguarded teardown context #293 closed it with bounded extractor predicates: teardown-context requirement, parameter-guard handling, symbol-based helper reachability (follow-ups: finalizers, unwired name-only handlers, overload conflation/ambiguity).PR fix(extractor): WPF002 Stop() teardown soundness — one doctrine with
-=#302 extended the same invariant to WPF002Stop().PR fix(bridge+extractor): #294 tolerant-door contract + #305 teardown-predicate soundness (audit → red → green) #306 (adversarial audit, Soundness: the #293 teardown/guard predicates swallow a leak behind an early-return guard and in the else-branch of
if (disposing)— adversarial audit, 2 P1 holes pinned red #305) hardened the predicates further: early-return parameter guards demote; the canonicalif (disposing)exemption is branch-aware. Residual attack families C/E/D/F are recorded indocs/notes/teardown-predicate-adversarial-audit.md.Design — ACCEPTED (frozen): the guarded-effects core contract is
docs/proposals/P-037-guarded-effect-summaries.md, design-arbitrated and accepted at4a01f0e(no design re-review needed for implementation). Load-bearing decisions: flat election lattice (None/One(g)/Conflict) solved by a monotone pre-solver fixpoint, so the value solver runs in a fixed product lattice and keeps order-independence; five-transform edge propagation (const-pos/const-neg/id/neg/opaque); two consume routes (selectedmust; unanimousmust); G-T1 precision floor and G-T2 post-finalization lax refinement (≤, not equality) with the residual-⊥ lemma as implementation proof obligations; exactly two declared verdict-change classes (application refinement via cell selection; summary refinement via cellwise derivation + guard-aware edges). Its §8 seventeen worked cases are the conformance-vector seeds, plus a dedicated machine-checked pure-ungrounded fixture for residual-⊥ lemma branch 3 (an arbitration requirement).The landed #293/#302/#306 extractor predicates are the current bounded implementation. This issue tracks replacing or generalizing them with CFG-backed, summary-composed lifecycle reasoning per P-036:
MethodSummaryapplication (helpers prove release via summaries, not name/symbol fixpoints inside the extractor);Teardown(bool skip)shape) with constant-argument substitution at callsites; unsupported predicates degrade to may/unknown, never must — per P-037;using/DI scope disposal/wired framework callback/owner dispose chain/registered callback) is required before a clean verdict;Gate
Blocked on the P-022 parity/cutover discipline (#262): no verdict-changing implementation before cutover. The landed predicates are the regression floor — no fixture they catch (or deliberately keep silent) may regress.
Acceptance
The eight fixture families of P-036 §Phase 2 plus P-037 §8's seventeen worked cases and the branch-3 pure-ungrounded fixture: families 1–3 become regression anchors over the landed predicates; families 4–8 (summary-proven helper release, may-release policy, degraded virtual/external targets, exceptional exits, runtime-correlated confirmation) are the new summary-backed capability. Findings carry call/branch witnesses; runtime correlation keeps stable static identities; the two P-037 verdict-change classes are the only permitted diffs against the collapsed-view golden dumps.