Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates)

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 WPF002 Stop().
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 canonical if (disposing) exemption is branch-aware. Residual attack families C/E/D/F are recorded in docs/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 at 4a01f0e (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 (selected must; unanimous must); 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).

AMENDED 2026-09-18 — see the governance amendment comment Two clauses in the paragraph above are superseded by later owner rulings and are kept here only as the record of what was accepted at 4a01f0e. G-T2 was split at A0.5 (7cf1f93) into G-T2a (algebraic collapse refinement, stated pre-finalization, machine-checked in formal/p037-kernel) and G-T2b (legacy observational compatibility — verdicts, not values), because finalization does not commute with collapse and the value-level ≤ against legacy is false with a pinned kernel counterexample. And there are three declared difference classes, not two: APPLICATION_REFINEMENT, SUMMARY_REFINEMENT, and LEGACY_HONESTY (unknown where today says may; both lower to plain + OWN051, so the verdict is unchanged, and class 3 may not be used to change a verdict). A difference outside the three is a defect of the implementation or of the contract — never a fourth class by fiat.

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:

lifecycle-root reachability + must-release composition through MethodSummary application (helpers prove release via summaries, not name/symbol fixpoints inside the extractor);
guarded effects for simple parameter predicates (the Teardown(bool skip) shape) with constant-argument substitution at callsites; unsupported predicates degrade to may/unknown, never must — per P-037;
the LifecycleEffect vs LifecycleEnrollment split: a release guaranteed if the root runs is not proof the root runs — enrollment evidence (using/DI scope disposal/wired framework callback/owner dispose chain/registered callback) is required before a clean verdict;
exceptional-exit and degraded virtual/external-target handling with explicit precision.

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.

[DISCHARGED 2026-09-18] P-022 Stage 3 landed (merged as #359, main at 63148d0), so the cutover condition is met, not waived. The regression-floor sentence stands unchanged and was never conditional on the cutover.

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.

[AMENDED 2026-09-18] Read "the three P-037 declared difference classes" — APPLICATION_REFINEMENT, SUMMARY_REFINEMENT, LEGACY_HONESTY — per the governance amendment. Class 3 is verdict-preserving by construction and may not be used to change a verdict; a collapsed-view difference outside the three is a defect, not a fourth class.

P-037 A1.1: the fact-shape census, and both P-037 checkers wired into CI

A2 execution governance freeze — before the first vocabulary change

Landed in aff77cdb162f7f9e72383a08a83ba27138705598 under
docs/notes/p037-formal-kernel.md §10.

This freezes A2.0 through A2.2. New implementation findings are classified as:

contradict frozen P-037 -> implementation defect;
expose an unrecorded theorem assumption -> proof-boundary manifest amendment;
expose an unrepresented syntax/fact shape -> shape-census addition;
expose a missing test/control -> evidence-infrastructure addition;
require new semantics or change a frozen rule -> STOP; explicit contract amendment.

Only case 5 reopens architecture.

Raw fact boundary

Roslyn reports source facts, never summary conclusions.

Reference argument facts are:
NullLiteral | ObjectCreation | StableParam(param) | CallResult(callee,sig) | Opaque.

The frontend must never emit a synthetic fresh_owned fact. A call result is
mapped to the positive nullness cell only at G-A1 application, after finalized
summaries prove that callee returns fresh. It is opaque otherwise. Reading
CallResult as a solver-edge transform would make the fixed pre-solver
system depend on the value solver's own output and is a case-5 STOP.

For nullness, forwarding the same stable nullable reference is id, never
const-pos: identity of the predicate is not truth of the predicate.
null is const-neg; object creation is statically non-null. Roslyn
nullable-flow inference is not part of this contract.

A2 staging

A2.1: guarded sidecar becomes a known fail-loud OwnIR vocabulary on both
doors, but remains semantically inert.

A2.2: Roslyn emits honest sidecar facts for every relevant call, including
sites the legacy ConsumesParam path currently treats as consuming. The
legacy body remains authoritative.

Acceptance through A2:

FACT shape: deliberate changes allowed;
whole MOS document: unchanged;
public verdicts: unchanged.

A deliberately contradictory but valid sidecar is the named inertness control:
A2 must accept it while leaving MOS and verdict unchanged; phase B flips the
same fixture to a required-read control for the guarded shadow path.

Phase B proof boundary

No semantic wiring in B until a proof-boundary audit is green. The bounded
Kani model (3 coordinates / 2 edges per coordinate) remains a bounded adapter
over shared production algebra; production uses a dynamic driver. The bound is
explicitly outside the proof boundary. Harness inventory is derived, and every
load-bearing assumption must name either a production guarantor or
OUTSIDE_KANI_BOUNDARY.

Before phase C

P-022 shadow/rollback policy must be re-scoped before intentional Rust/Python
P-037 divergence:

shadow accepts only machine-classified per-document differences in the three
declared classes;
rollback mechanics, exact parity on an unaffected sample, and classified
intentional P-037 divergence are separate contracts.

C+ is an explicit post-cut checkpoint to canonicalize the temporary double
representation; A2 introduces stable call-site identity now.

P-037 A2.0: add evidence provenance closure

P-037 A2.0: add whole-MOS differential gate

P-037 A2.0: wire provenance controls into evidence gates

P-037 A2.0: bind MOS source set to committed inputs

P-037 A2.0: satisfy lint and launcher census

P-037 A2.0: normalize MOS snapshot imports

P-037 A2.0: preserve repository compilation in MOS gate

P-037 A2.0: make provenance closure fail on phantom paths

P-037 A2.0: expose provenance control to the regression suite

P-037 A2.0: close evidence integrity gaps before baselines

P-037 A2.0: make snapshot integrity narrowing explicit

P-037 A2.0: harden the evidence harness into a T-candidate contract

P-037 A2.0: seal the executed Rust artifacts per take and attest them…

P-037 A2.1: emit the guarded-fact sidecar from the Roslyn extractor, …

P-037 A2.2-0: freeze the relevance taxonomy, the named exclusions and…

P-037 A2.2-1: decide argument relevance by value flow, not by syntax

P-037 A2.2-1a: close the conversion vocabulary (reference_checked, bo…

P-037 A2.2-2: constructor calls are call sites of their own (call_kin…

P-037 A2.2-2b: delegate invocation is a call site of its own (call_ki…

P-037 A2.2-3P: the guarded_functions[] orphan carrier, production side

P-037 A2.2-3P-fix: repair the ownir_version producer pin and the orph…

P-037 A2.2-3P-fix2: remove the stale "validated by both doors" claim …

P-037 A2.2: result — stop point reached, R escalated; pin the raw arg…

P-037 A2.2: record the owner ruling on R (record-level absence)

OWNER RULING — R / record-level absence (2026-09-28), recorded from the owner's decision on the case-5 escalation in #371. It is committed verbatim in docs/notes/p037-formal-kernel.md §10.6 (0ae8213).

Decision: accept R as an explicit out-of-A2 precision boundary. Do not add a new carrier and do not create new functions[] records in A2.

A2.2's completeness claim is henceforth scoped as follows:

Roslyn emits honest guarded_facts for every relevant call inside every emitted functions[] record.

This is a scope clarification required by the measured record-level boundary, not authorization to weaken the per-record contract. For every emitted function record, the existing A2.2 rule remains absolute: every relevant call must appear, and absence is a defect.

R boundary. A source method for which the frontend emits no functions[] record has no guarded_facts carrier in A2. Examples currently include:

methods whose disposable locals all escape and that have no owned parameter;
methods whose lowered body is empty;
expression-bodied members not represented by the flow-function surface.

A2 does not create a flow record merely to host guarded facts, because that would change the MOS population and violate A2's zero-semantic-cut contract.

A2 also does not introduce a second top-level method/sidecar carrier. Doing so would change the frozen OwnIR layout and create two representations that Phase B/C+ would later have to reconcile.

record-absence-boundary remains an executable census boundary.

Phase B semantics. Record absence is fail-closed. If no emitted functions[] record exists, the guarded engine has no evidence for that method. Absence must never be interpreted as:

must;
no / definite borrow;
an unconditional summary;
an eligible guard;
an id / neg transform;
proof that a call has no ownership effect.

It is simply outside the guarded fact domain. Any implementation that converts record absence into a positive semantic claim is a defect.

Phase B consequences:

Guardrail. Phase B never reads a missing record or sidecar as "no effects", borrow, unconditional, or "guard irrelevant". It means unknown: no guarded evidence.
Negative control. record-absence-boundary becomes a permanent Phase-B negative control. A mutant that draws a positive conclusion from absence must turn it red.

What this decision does and does not claim. It accepts a precision / recall boundary, not semantic completeness over arbitrary C# methods. Expression-bodied wrappers and other record-less methods may hide useful guarded-summary information. That is a known gap, not evidence that such methods are semantically irrelevant. No claim is made that R is permanently acceptable.

Reopen condition. Do not expand the carrier pre-emptively. Reopen R only when a bounded experiment demonstrates practical value that cannot be obtained through the existing functions[] surface. For example:

a real or corpus-derived P-037 case whose required summary path crosses a record-less method;
a material missed finding or unresolved summary attributable specifically to R;
Phase B coverage showing that record absence forms a significant fraction of otherwise eligible guarded paths.

At that point, run a separate kill-first experiment comparing:

extending the existing flow-function population; versus
introducing a distinct fact-only method carrier.

Neither design is authorized by this ruling.

A future kill-gate, not now: after the first Phase-B shadow run, measure how many potential guarded paths break specifically because a functions[] record is missing.

Near zero: the carrier stays as it is.
A material share (for example 15–20% of real wrapper chains breaking at expression-bodied members): that is the basis for an IR extension, through the comparison above.

Acceptance consequence for #371. #371 may close A2.2 with R recorded as this boundary if all existing A2.2 gates remain green:

per-emitted-record call completeness;
sidecar inertness;
whole MOS unchanged;
public verdicts unchanged;
record-absence-boundary pinned.

After this ruling, Phase B may start from the #371 fact surface. R is not to be silently removed from the census when Phase B begins.

Generated by Claude Code

P-037 B0: record the owner ruling on B0 and A14

OWNER RULING — B0 / A14 (2026-09-28). Recorded from the owner's decision on #372 (the P-037 Phase B0 proof-boundary audit). The ruling is committed verbatim in docs/notes/p037-formal-kernel.md §10.7 (0e2c01a), together with the context the owner gave with it.

Decisions

B0 PASS is accepted.
Both §E.4 interpretations stand:
- PRODUCTION_GUARANTOR means a mechanism that exists now;
- apply / lower are the current formal-to-production seam, and B1 must move the K7 witness onto the real adapter.
B1 shadow is authorized, with all 16 entry obligations.
- B1 must report guarded results as conditional on static dispatch.
- B1 must not change public semantics.

A14 (static dispatch)
A14 is NOT accepted as a permanent production assumption. It is a mandatory pre-Phase-C gate. Before guarded summaries can become authoritative:

measure dynamic-dispatch exposure on the first B1 shadow population;
test whether any admissible runtime target can invalidate a static-target positive conclusion, especially MUST;
if yes, Phase C must fail closed for non-exact dispatch, either through a minimal dispatch fact or another explicitly approved mechanism;
no non-exact call may fabricate MUST merely from the statically resolved callee.

Do not amend OwnIR before the measurement establishes that the information is actually needed.

The A14 gate runs after the first B1 shadow run and before Phase C. It is sized in hours, not weeks.

Population:
- the repo tree;
- the committed corpus;
- the P-037 controls and shapes;
- the first B1 shadow corpus.
Counts:
- relevant calls;
- exact calls;
- virtual/interface/abstract candidates;
- candidates that take part in a guarded summary chain;
- candidates where two or more possible implementations have different summary classes.
Hard KILL: if even one reachable virtual/interface call has a static callee that can give MUST and an admissible runtime target that does not, static dispatch cannot enter an authoritative Phase C.
If the KILL fires, the preferred remedy is a minimal producer fact, dispatch: exact | open, with non-exact dispatch degrading to Opaque/Unknown and never to MUST.

Not changed now

A13 (finalize before cross-SCC export) is an ordinary B1 obligation.
A16 (normal-return scope) is an inherited, honestly classified boundary.

Generated by Claude Code

P-037 B1: amend the pre-registration per owner review (no code)

P-037 governance record — the A18 population decomposition and PCS-0 (2026-09-28)

1. A18-1F (#378): terminal KILL, owner-accepted.

The approach killed is post-processing population decomposition: rewriting OwnIR in Python after the fact and reconstructing forward closures there.
It hit its pre-registered final budget at 165/145 measurement lines, before any test was written. Nothing was run.
There is no A18-1G and no further line-budget re-plan.
The unrun draft is not merged; P-037 A18-1F: TERMINAL KILL — population-decomposition approach (budget 165/145), not run — do not merge #378 stays open only as the research artifact.
This is an operational KILL of that method. The two-seam model was neither confirmed nor refuted on the population.

2. Standing state:

P-037 B1: guarded shadow read — RESULT FAIL, B1 BLOCKED (KILL 5, owner decision) #373 B1: RESULT: FAIL — B1 BLOCKED (KILL 5), kept.
P-037 A18-0: legacy decomposition of the eight B1 rows — RESULT PASS (B1 stays FAIL) #374 A18-0: PASS on its 8 rows.
P-037 B1 evidence completion: per-row comparable summary snapshot (case 4) #376: the supplemental 36-row per-row baseline. It reproduces B1's aggregates and its 8 committed rows; it claims no historical per-row identity for the other 28, and the extractor DLL sha deviation stays disclosed.
P-037 A18-1: population decomposition — STOP at the hard cap (preserved artifact; superseded by A18-1R) #375 and P-037 A18-1R: population decomposition, re-planned — STOP at the cap (192/180, not run) #377: STOP artifacts.
Phase C stays blocked. missing-sidecar, R and A14 are untouched.

3. PCS-0 (#379): the producer-side canonical shadow, a new premise. RESULT: KILL on budget, not run.

It was pre-registered at 96810e5 before any code.
Caps: C# ≤ 100, driver ≤ 40, tests ≤ 60, total ≤ 180.
The first complete draft came to C# 83/100 and tests plus probe 57/60, but the driver was 68/40 and the total 208/180.
The overrun is the new standalone driver's own plumbing. The producer shadow itself fit its cap, with no schema change and the ordinary lowering unchanged with the switch off.
Nothing was measured: neither the F0 transitive falsifier nor the 8 rows. There is no PCS-1R2.
Per the pre-registration, the next question is whether to freeze the P-037 implementation as a whole. That is the owner's decision.

Generated by Claude Code

OWNER RULING (2026-09-28): P-037 IMPLEMENTATION FREEZE

P-037 STATUS: IMPLEMENTATION FROZEN

Design:                                KEEP
formal/p037-kernel:                    KEEP
A2 honest guarded-fact surface:        KEEP as validated research/producer work
B0 proof-boundary result:              KEEP / PASS
B1:                                    historical RESULT = FAIL — B1 BLOCKED (KILL 5)
A18-0:                                 KEEP as bounded evidence only
A18 population decomposition:          KILLED operationally
PCS producer canonical shadow:         KILLED operationally
Phase C:                               NOT AUTHORIZED

No further P-037 implementation experiment is authorized.

What is frozen. The P-037 design and the formal kernel are not rejected. Only the production migration path is frozen: B1 → reconciliation → Phase C → authoritative guarded summaries. It stopped after B1 because the migration boundary needed to justify authoritative guarded semantics could not be established within the pre-registered operational budgets.

Evidence:

B0 (P-037 B0: audit the formal/production proof boundary #372): PASS.
B1 (P-037 B1: guarded shadow read — RESULT FAIL, B1 BLOCKED (KILL 5, owner decision) #373): FAIL / KILL 5, 8 summary rows unexplained.
A18-0 (P-037 A18-0: legacy decomposition of the eight B1 rows — RESULT PASS (B1 stays FAIL) #374): bounded 8/8 decomposition PASS.
A18 population post-processing (P-037 A18-1: population decomposition — STOP at the hard cap (preserved artifact; superseded by A18-1R) #375 STOP, P-037 A18-1R: population decomposition, re-planned — STOP at the cap (192/180, not run) #377 STOP, P-037 A18-1F: TERMINAL KILL — population-decomposition approach (budget 165/145), not run — do not merge #378): terminal operational KILL before any population measurement.
PCS-0 producer canonical shadow (P-037 PCS-0: KILL — producer canonical shadow (budget: driver 68/40, total 208/180), not run #379): operational KILL on budget before any falsifier or measurement. Its C# was 83/100; the driver was 68/40 and the total 208/180. Green CI on P-037 PCS-0: KILL — producer canonical shadow (budget: driver 68/40, total 208/180), not run #379 is not a PCS-0 PASS; at most it shows the ordinary extractor path survives the standard tests.
So population-wide compatibility of the two-seam model is neither established nor refuted.

Consequences:

Phase C is NOT AUTHORIZED.
No B1 reconciliation.
No additional A18 or PCS budget re-plan: no A18-1G and no PCS-0R. "Reuse the existing driver" is explicitly excluded; a post-hoc way to fit a lost budget does not reopen it.
No P-037-motivated ConsumesParam change.
No P-037-motivated OwnIR, schema or carrier expansion.
A14, R, missing-sidecar and P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368 are not worked while the implementation is frozen.
The existing production predicates (fix(extractor): #278 — a -= releases only in a proven, unguarded teardown context #293 / fix(extractor): WPF002 Stop() teardown soundness — one doctrine with -= #302 / fix(bridge+extractor): #294 tolerant-door contract + #305 teardown-predicate soundness (audit → red → green) #306) remain the regression floor.

PR stack:

P-037 B1: guarded shadow read — RESULT FAIL, B1 BLOCKED (KILL 5, owner decision) #373–P-037 PCS-0: KILL — producer canonical shadow (budget: driver 68/40, total 208/180), not run #379 are closed without merge as historical research artifacts:
They are not merged to preserve the work, and their branches stay available.
P-037 A2.2: honest call facts for every relevant call (zero semantic cut) #371 (A2.2 honest facts) and P-037 B0: audit the formal/production proof boundary #372 (B0) are KEEP candidates that are not merged for now. They may be merged separately, as a zero-semantic-cut foundation, only if guarded_facts gets a consumer independent of P-037, or if the A2 producer contract is to be fixed officially. "The work would be lost" is not a reason.

Reopen conditions. Only an external structural change that lowers the cost of the necessary condition reopens P-037. Time passing does not, and neither does a new way to measure the same thing. One of:

Canonical calls: independent production work makes the call representation canonical. For example, the legacy body stops folding first-party forwards into release/use, so the honest call becomes the MOS's natural source.
Measurable need: a real production defect class with measurable value appears that the current predicates do not cover, with a material count on corpus or real-world code.
Cheap population checks: independent infrastructure makes the population check nearly free. For example, an existing evidence runner already emits both representations and per-row MOS without a specialized driver.

A reopen gate starts with this question, not with code: what changed since the KILL that makes the previous upper cost bound no longer apply? "We now know how to write the same script shorter" does not lift the freeze.

#304 stays open with status FROZEN; it is not closed as "the idea is bad", because that was not established.

Generated by Claude Code

research(p037): consolidate plain Rocq proof layer

research(p037): value benchmark — R2 evidence, REOPEN_CANDIDATE_R2

docs(p037): correct value benchmark to capability-gap-only

fix(p037): tighten mining note carve-out from a prefix to exact paths

Record the #380 baseline transition for the P-037 controls and fact s…

docs(#380): scope the definiteness comment and pin the dynamic-forwar…

P-037-X Stage 1: re-record the census, the controls and the #380 pins…

P-037-X Stage 1: the stage note with the population evidence (EXPLORA…

P-037-X Stage 2: replay the frozen P-037 unchanged on canonical calls…

P-037-X Stage 2b: driver fidelity for the frozen replay (EXPLORATORY,…

P-037-X Stage 2b: the stage note (EXPLORATORY, research branch)

P-037-X Stage 2c: initializer-form argument use (EXPLORATORY, pre-reg…

P-037-X Stage 2c: the stage note (EXPLORATORY, research branch)

P-037-X Stage 2d: the legacy borrow at a call line without a coordina…

P-037-X Stage 2d: the stage note (EXPLORATORY, research branch)

Navigation Menu

Repository navigation

Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304

Context

Gate

Acceptance

A2 execution governance freeze — before the first vocabulary change

Raw fact boundary

A2 staging

Phase B proof boundary

Before phase C

OWNER RULING (2026-09-28): P-037 IMPLEMENTATION FREEZE

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304

Description

Context

Gate

Acceptance

Activity

PhysShell commented on Sep 18, 2026

A2 execution governance freeze — before the first vocabulary change

Raw fact boundary

A2 staging

Phase B proof boundary

Before phase C

PhysShell commented on Sep 28, 2026

PhysShell commented on Sep 28, 2026

PhysShell commented on Sep 28, 2026

PhysShell commented on Sep 28, 2026

OWNER RULING (2026-09-28): P-037 IMPLEMENTATION FREEZE

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions