Skip to content

Commit cfe7e19

Browse files
committed
P-037 Phase B / B1-F2: correct the extractor's instrument/treatment boundary
B1 classified frontend/roslyn/OwnSharp.Extractor/ as full measurement instrument with no carve-out, while the frozen A1 acceptance matrix (formal-kernel.md #8.1, items 5 and 8) requires an extractor-side semantic change there: ConsumesParam's flow-insensitive fabrication is decided in the raw extractor facts.json, before either engine runs, so no Rust-only change can discharge it. A treatment surface cannot simultaneously be frozen measurement instrument. This is the boundary repair, not the semantic treatment: - scripts/p037_b_extractor_diff_gate.py: a second, item-granular production-diff gate mirroring p037_b_production_diff_gate.py, scoped to exactly three named methods (ConsumeReleaseArgs/ConsumesParam/ CallReleasesReceiver) traced from the real call graph. Compares items in normalized form (p037_door_diff_gate._normalize), matching how rust_items already compares every Rust item, so incidental formatting next to an authorized new method can't masquerade as an unrelated change. - scripts/p037_evidence_b.py: INSTRUMENT_CARVE_OUTS/TREATMENT_PATHS now carve the whole extractor directory out (same shape as mos.rs/lower.rs), relying on the new gate to police it at method granularity. closure_problems() cross-checks the epoch record's new production_diff_gate.extractor.unit, same self-authorization-hole fix B1-F1 already applied to the Rust side. - docs/evidence/p037-b-epoch.json: new production_diff_gate.extractor and treatment.extractor_seam sections; must_not_touch_yet corrected in place; old T_B/R_B (a02ccf1/the B1-F1 baseline) named explicitly as superseded_by_b1_f2, not deleted or rewritten; named_later.T_B/R_B cleared pending this fix's own retake. - tests/test_p037_a2d_epoch.py: PHASE_B_GOVERNANCE_FILES gains exactly one entry for the new gate script (not a "frontend/" prefix -- this task never touches Program.cs itself). - docs/notes/p037-formal-kernel.md: §10.8e documents the defect and repair. Verified: p037_controls.py --engine both still matches current exactly; --post-a1 is still fully RED on both engines (no semantic treatment occurred); full tests/run_tests.py, ruff, mypy all clean; all four B1 selftests (extractor gate, Rust gate, classifier, evidence_b) green; proof-boundary audit still GREEN. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AN6xHbpovxrmZ4AMjS7WQA
1 parent bfa8647 commit cfe7e19

5 files changed

Lines changed: 1077 additions & 25 deletions

File tree

‎docs/evidence/p037-b-epoch.json‎

Lines changed: 32 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -47,11 +47,20 @@
4747
"rust/crates/own-bridge/src/mos.rs": "every top-level item except two: `fn call_graph` and `fn sccs` are pure graph-topology helpers (SCC condensation over an adjacency map) that read no Transfer/join value at all and stay frozen; the other 15 items (enum Transfer, fn join, impl Transfer, enum PathAction, enum ReturnSkeleton, struct ParamSkeleton, struct MethodSkeleton, struct ParamSummary, struct MethodSummary, type Mos, type ParamKey, fn solve_with_log, fn solve, plus the file's one `use` and its `#![allow(...)]` inner attribute) are the guarded-kernel seam and may move",
4848
"rust/crates/own-bridge/src/lower.rs": "four named items, not one and not the file (73 top-level items total; the other 69 stay frozen at item granularity) -- corrected from the original 'fn lower_fn_params only' claim: lower_fn_params computes only a parameter's OWN type-shape from its OWN function's MethodSummary and never resolves a call site; the call-site decision (matching an argument against the CALLEE's summary, and choosing the may/unknown optimistic-default OWN051 path) is made in `fn unverified_transfer_calls` and `fn kill_sites_for_unverified`, with the advisory itself minted inside `fn lower_full`. A guard-aware call-site selection cannot land touching lower_fn_params alone; all four are the honest seam."
4949
},
50+
"extractor_seam": {
51+
"added_by": "B1-F2, correcting a boundary defect B1 itself introduced (see superseded_by_b1_f2): the frozen A1 acceptance matrix (docs/notes/p037-formal-kernel.md #8.1, items 5 and 8) requires an extractor-side semantic change -- the four F3-S* controls' `fabricated_release_at_call_site` must go false post-A1, measured from the RAW extractor facts.json output (scripts/own-check.sh --emit-facts is a byte copy of the extractor's own output, taken before either engine runs) that no Rust-only change can affect. A treatment surface cannot simultaneously be frozen measurement instrument.",
52+
"unit": "frontend/roslyn/OwnSharp.Extractor/ (Program.cs only; the .csproj stays frozen -- no new dependency)",
53+
"mutable_methods": ["ConsumeReleaseArgs", "ConsumesParam", "CallReleasesReceiver"],
54+
"seam_derivation": "traced directly from source, not assumed: ConsumeReleaseArgs calls ConsumesParam, which recurses through first-party callees; CallReleasesReceiver is the extension-method-receiver twin of the same call. DisposesLocal, ParameterIsStable (the existing G-V4 whole-body write-exposure test) and BuildGuardedFacts (the guarded_facts producer) all stay FROZEN -- confirmed independent both by source reading and by running the real extractor on real fixtures.",
55+
"authorized_change_shape": "abstain from the unconditional legacy release fabrication when the callee's OWN already-emitted guarded_facts say the call is guard territory -- never a new guard-eligibility test, never Election/Cells/Transform/fixpoint math inside Roslyn. That math stays exactly where B1 already froze it: rust/crates/own-bridge/, policed by production_diff_gate.rust. Making ConsumesParam path-sensitive is explicitly NOT authorized by this seam.",
56+
"governed_by": "production_diff_gate.extractor (this record) + scripts/p037_b_extractor_diff_gate.py, mirroring production_diff_gate.rust + scripts/p037_b_production_diff_gate.py exactly: path-level provenance carve-out (scripts/p037_evidence_b.py's INSTRUMENT_CARVE_OUTS/TREATMENT_PATHS) plus item-level production diff gate is the actual permitted semantic boundary",
57+
"not_implemented_by_b1_f2": true
58+
},
5059
"must_not_touch_yet": [
5160
"ownlang/ownir.py (stays reference/oracle/rollback; not a Phase B treatment path)",
52-
"frontend/roslyn/OwnSharp.Extractor/",
53-
"OwnIR / extractor guarded-fact vocabulary",
54-
"verdict mapping outside the named seam",
61+
"frontend/roslyn/OwnSharp.Extractor/ outside extractor_seam.mutable_methods (as of B1-F2; before B1-F2 the WHOLE directory was listed here with no carve-out at all, which was itself the boundary defect B1-F2 corrects -- see superseded_by_b1_f2)",
62+
"OwnIR / extractor guarded-fact VOCABULARY (the guarded_facts/guarded_functions SCHEMA, frozen by A2.2-D) -- extractor_seam authorizes reading the already-emitted sidecar as an input signal, never changing what it contains or how it validates",
63+
"verdict mapping outside the named seam(s)",
5564
"launcher behaviour",
5665
"any docs/evidence/p037-a2d-* file"
5766
]
@@ -92,7 +101,16 @@
92101
"controls": ["tests/"]
93102
},
94103
"registered_new_items_policy": "empty by design in B1: no treatment exists yet to know what new production items it needs, and a treatment registers its own new items in the SAME commit that defines them -- exactly A2.2-D's own door-gate discipline, not a relaxation of it",
95-
"b1_must_measure": "IDENTICAL against 5571ba4 (the closed Phase-B entry-gate head): B1 adds tooling, ledgers and documentation and moves no byte of rust/crates/own-bridge/"
104+
"b1_must_measure": "IDENTICAL against 5571ba4 (the closed Phase-B entry-gate head): B1 adds tooling, ledgers and documentation and moves no byte of rust/crates/own-bridge/",
105+
"extractor": {
106+
"unit": "frontend/roslyn/OwnSharp.Extractor/",
107+
"tool": "scripts/p037_b_extractor_diff_gate.py",
108+
"note": "Added by B1-F2. A second, separate item-level gate -- not scripts/p037_door_diff_gate.py repointed a third time, and not scripts/p037_b_production_diff_gate.py extended: that module's Policy/compare_rust are Rust-syntax-specific (classify_chars/_item_head parse Rust item heads, not C#). The extractor gate reuses only p037_door_diff_gate.py's language-agnostic half (compare_items/Tree/snapshot/UnitReport/_normalize) plus its own C#-aware csharp_items() extraction -- the same relationship compare_python already has to that shared half, now a third instance of it.",
109+
"frozen_files": ["OwnSharp.Extractor.csproj"],
110+
"mutable_methods": ["ConsumeReleaseArgs", "ConsumesParam", "CallReleasesReceiver"],
111+
"registered_methods": [],
112+
"b1_f2_must_measure": "IDENTICAL against bfa8647 (the closed, corrected-T_B B1-F1 head) for rust/crates/own-bridge/ -- B1-F2 moves no Rust production byte either. Only scripts/p037_evidence_b.py (the provenance-closure carve-out), the new scripts/p037_b_extractor_diff_gate.py, this record, tests/test_p037_a2d_epoch.py's one-file allowlist addition and docs/notes/p037-formal-kernel.md move."
113+
}
96114
},
97115
"environment": {
98116
"id": "P037_B_MEASUREMENT_M3",
@@ -181,10 +199,18 @@
181199
"no edit, regeneration, reinterpretation or retaking of any a2/a2d evidence",
182200
"no change to ownlang/ownir.py, the extractor, OwnIR guarded-fact vocabulary, verdict mapping or launcher behaviour"
183201
],
184-
"named_later": {
202+
"superseded_by_b1_f2": {
203+
"reason": "B1 classified frontend/roslyn/OwnSharp.Extractor/ as full measurement instrument with no carve-out at all, while the frozen A1 acceptance matrix (formal-kernel.md #8.1, items 5 and 8) requires an extractor-side semantic change there -- a treatment surface cannot simultaneously be frozen measurement instrument. B1-F2 corrects the boundary (scripts/p037_evidence_b.py's INSTRUMENT_CARVE_OUTS/TREATMENT_PATHS, plus the new item-level scripts/p037_b_extractor_diff_gate.py) before any semantic movement. The measurements below were honest at the boundary B1 drew -- the boundary was wrong, not the measurement -- so they are superseded, never deleted or rewritten.",
185204
"T_B": "a02ccf17d22eaf62c046fb95ba5060e6d66ffeae",
205+
"T_B_title": "P-037 Phase B / B1: name T_B at the corrected instrument (df9a433's evidence)",
186206
"R_B": "docs/evidence/p037-b-baseline-manifest.md",
207+
"status": "historical: honest B1 evidence at a boundary later found incomplete; not a baseline for any future comparison; superseded by the T_B/R_B this same field family names once B1-F2's own retake lands (see named_later below)"
208+
},
209+
"named_later": {
210+
"T_B": null,
211+
"R_B": null,
187212
"B_treatment_head": null,
188-
"B_after_evidence": null
213+
"B_after_evidence": null,
214+
"note": "cleared by B1-F2 pending its own corrected-instrument retake (order: land the boundary fix terminal-green, THEN name the new T_B, THEN take R_B fresh at it) -- see superseded_by_b1_f2 for what these named before B1-F2"
189215
}
190216
}

‎docs/notes/p037-formal-kernel.md‎

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2872,3 +2872,165 @@ was wrong. `75764c81ac49185adad6a02657b373a7453fc03ba337bb61b86d4694bd8d5065`,
28722872
measured at `eb6c211`, is Phase B's true current instrument identity and
28732873
is the value that `T_B`'s naming and every retaken `R_B` artifact will
28742874
cite from here on -- not `ed6ee5f8...`.
2875+
2876+
#### 10.8e Phase B / B1-F2: the extractor's instrument/treatment boundary was wrong (OWNER RULING)
2877+
2878+
B2.0 (a separate, read-only preregistration task run against the frozen
2879+
B1 instrument) traced the "may-as-must `ConsumesParam` hole" all the way
2880+
to ground truth — not just source reading, but running the real extractor
2881+
on real fixtures and inspecting the emitted `facts.json` — and found a
2882+
contract conflict the task's own instructions required stopping on: the
2883+
frozen A1 ACCEPTANCE block (§8.1, items 5 and 8) requires `fabricated_
2884+
release_at_call_site: false` post-A1 for the four named F3-S* controls,
2885+
and that field is measured from the RAW extractor `facts.json`
2886+
(`scripts/own-check.sh --emit-facts` is a byte copy of the extractor's own
2887+
output, taken before either engine ever runs) — a fact no Rust-only change
2888+
can affect. This document already said as much: "A1's first target is
2889+
therefore extractor-side," with the two-layer-acceptance rationale stated
2890+
explicitly — a Rust summary engine must not compensate a bad extractor
2891+
fact with another heuristic and produce a falsely green end-to-end result.
2892+
2893+
**OWNER RULING.** Weakening A1-5/A1-8 to a verdict-only acceptance (B2.0's
2894+
own "option 1") is refused: that is a post-hoc weakening of a frozen
2895+
acceptance, not a discharge of it. An extractor-side A1 change is
2896+
eventually required and is NOT authorized yet. Before it can be, a second,
2897+
independent defect in B1's OWN governance must be fixed:
2898+
`p037_evidence_b.INSTRUMENT_PATHS` classified
2899+
`frontend/roslyn/OwnSharp.Extractor/` as full measurement instrument, in
2900+
full, with no carve-out at all — while the frozen A1 contract requires
2901+
that exact path to become a treatment surface. A treatment surface cannot
2902+
simultaneously be treated as immutable measurement instrumentation. This
2903+
is B1-F2, and it is scoped narrowly: fix the boundary and build the
2904+
tooling that will police the eventual extractor treatment; do not perform
2905+
that treatment yet. People sometimes build a perfectly convincing system
2906+
of proofs for an incorrectly drawn boundary — that does not make the
2907+
boundary correct.
2908+
2909+
**REPOSITORY FACT: the seam, traced from source.** The extractor's
2910+
flow-insensitive fabrication is jointly produced by exactly three named
2911+
methods in `frontend/roslyn/OwnSharp.Extractor/Program.cs`:
2912+
`ConsumeReleaseArgs` (`Program.cs:5223`, the call site) calls
2913+
`ConsumesParam` (`Program.cs:5280`, the recursive "does the callee dispose
2914+
this parameter on *some* path" flow-insensitive check), and
2915+
`CallReleasesReceiver` (`Program.cs:5343`) is the extension-method-receiver
2916+
twin of the same call. `DisposesLocal` (`Program.cs:5320`),
2917+
`ParameterIsStable` (`Program.cs:2911`, the already-correct G-V4
2918+
whole-body write-exposure test) and `BuildGuardedFacts` (`Program.cs:2962`,
2919+
the `guarded_facts` sidecar producer) are independent and stay frozen —
2920+
confirmed both by reading the call graph and by running the real extractor
2921+
on two real fixtures
2922+
(`corpus/p036-bakeoff/guarded-consume-flag-branch/before.cs` and
2923+
`corpus/p036-bakeoff/legacy-honesty-else-unresolved-forward/control.cs`)
2924+
and inspecting the emitted JSON directly: `guarded_facts.guards[]`/
2925+
`calls[]` are already honest and unaffected by `ConsumesParam`'s
2926+
fabrication, confirming the two mechanisms are genuinely independent, not
2927+
merely presumed so.
2928+
2929+
**Fix, in three parts.**
2930+
2931+
1. **A second, item-granular production-diff gate.**
2932+
`scripts/p037_b_extractor_diff_gate.py`, mirroring `scripts/p037_b_
2933+
production_diff_gate.py`'s own architecture exactly (the same
2934+
IDENTICAL/WITHIN_ALLOWLIST/VIOLATION/REFUSED verdicts, the same
2935+
self-authorization-hole protection `IMMUTABLE_POLICY_FIELDS`/
2936+
`policy_drift()` applies from the start rather than after a second
2937+
owner-found bug) but for C# rather than Rust: `csharp_items()` locates
2938+
the three named methods by signature and brace-balances each one's body
2939+
using a conservative same-file character classifier (line/block
2940+
comments — which, unlike Rust's, do not nest — char literals, plain/
2941+
verbatim/interpolated strings), collapsing everything else in the
2942+
7600+-line file into one opaque remainder item compared as a whole. Two
2943+
corrections the gate's own `selftest()` caught before this section was
2944+
written, not assumed correct: raw-byte round-trip losslessness is
2945+
checked BEFORE normalization (proving the named spans plus the
2946+
remainder exactly cover the file); and every item — including the
2947+
remainder — is compared in NORMALIZED form (comments dropped,
2948+
whitespace collapsed), reusing `p037_door_diff_gate._normalize` exactly
2949+
as `rust_items` already does for every Rust item. Without that second
2950+
correction, formatting incidental to a genuinely authorized new
2951+
registered method (a blank line, an indent) would have masqueraded as
2952+
an unrelated change to "the rest of `Program.cs`" — the gate's own
2953+
hostile test (`registered-helper-is-allowed`) failed under raw-byte
2954+
comparison and passes under normalized comparison, which is what fixed
2955+
it. 18 selftest checks pass, including all six hostile cases named for
2956+
this gate (authorized item changed -> allowed; unrelated item changed
2957+
-> violation; new unregistered helper -> violation; registered helper
2958+
-> allowed; frozen `.csproj` changed -> violation; and a live-source
2959+
sanity block against the real `Program.cs`).
2960+
2961+
2. **Provenance closure correction.** `scripts/p037_evidence_b.py`'s
2962+
`INSTRUMENT_CARVE_OUTS`/`TREATMENT_PATHS` now carve the WHOLE extractor
2963+
directory out — the same way `mos.rs`/`lower.rs` are carved out whole
2964+
even though only four of their functions are actually mutable under
2965+
`p037_b_production_diff_gate.py` — relying on the new item-level gate to
2966+
close the resulting hole at method granularity: path-level provenance
2967+
carve-out plus item-level production diff gate is the actual permitted
2968+
semantic boundary, the same composition A2.2-D and B1 already use for
2969+
`mos.rs`/`lower.rs`. `closure_problems()`'s `_record_closure_problems`
2970+
now cross-checks the epoch record's new `production_diff_gate.
2971+
extractor.unit` against this module's own, exactly as it already did
2972+
for the Rust gate's unit — the same self-authorization-hole fix B1-F1
2973+
found for the Rust side, applied here from the start. Two new
2974+
`selftest()` checks prove the composition actually holds, not just that
2975+
it is declared: the whole extractor carve-out is absent from
2976+
`instrument_manifest()` at `HEAD` (so an eventual edit to the three
2977+
mutable methods cannot masquerade as instrument drift), and the new
2978+
gate script itself is present in `INSTRUMENT_PATHS` (so a change to the
2979+
gate's own correctness moves `instrument_identity`, exactly as
2980+
`p037_b_production_diff_gate.py` already does).
2981+
2982+
3. **`docs/evidence/p037-b-epoch.json` corrected truthfully.** A new
2983+
`production_diff_gate.extractor` section mirrors `.rust`'s shape
2984+
exactly (`unit`/`frozen_files`/`mutable_methods`/`registered_methods`,
2985+
byte-identical to the gate's own `frozen_policy()`). A new `treatment.
2986+
extractor_seam` section documents the seam, its derivation and its
2987+
authorized change shape, and `treatment.must_not_touch_yet` is corrected
2988+
in place — the old blanket "`frontend/roslyn/OwnSharp.Extractor/`"
2989+
entry is replaced with the precise statement (outside the three named
2990+
methods; the OwnIR guarded-fact VOCABULARY/SCHEMA itself, frozen by
2991+
A2.2-D, stays untouched regardless) rather than silently dropped, so the
2992+
correction is visible in place, the same pattern §10.8c/10.8d above
2993+
already use for a wrong claim discovered after the fact. The old `T_B`
2994+
(`a02ccf1`) and `R_B` (the B1-F1-corrected baseline manifest) are not
2995+
deleted, not declared garbage, and not rewritten: a new `superseded_by_
2996+
b1_f2` section names them explicitly, machine-readable, with the reason
2997+
— they were honest measurements at a boundary later found incomplete,
2998+
not a false measurement. `named_later.T_B`/`.R_B` are cleared to `null`
2999+
pending B1-F2's own retake (below), matching how `B_treatment_head`/
3000+
`B_after_evidence` already read `null` pending their own later steps.
3001+
3002+
**Severity.** The defect was in classification, not in any measurement
3003+
already taken: every fact/MOS/verdict `R_B` recorded was, and remains,
3004+
accurate for the boundary B1 actually drew. What was wrong is that the
3005+
boundary itself excluded a path the frozen A1 contract requires to move.
3006+
No verdict was ever falsely accepted as A1-compliant because of this —
3007+
`--post-a1` was, and must remain, RED throughout (reconfirmed as part of
3008+
this same fix's own verification) — so this is a governance-boundary
3009+
defect, not a silent correctness escape.
3010+
3011+
**`tests/test_p037_a2d_epoch.py`.** This test governs a DIFFERENT epoch's
3012+
record (`docs/evidence/p037-a2d-epoch.json`, A2.2-D's own door-registration
3013+
closure) and its own hardcoded `extractor-is-instrument-not-treatment`
3014+
check reads THAT record's `instrument.roots`/`treatment.paths`, not Phase
3015+
B's — confirmed unaffected and still green. The only real gap this test
3016+
had was `PHASE_B_GOVERNANCE_FILES` not yet naming the new gate script (the
3017+
same allowlist-lags-a-new-Phase-B-file gap `b234599` hit twice before);
3018+
fixed by adding exactly one entry, `scripts/p037_b_extractor_diff_gate.py`
3019+
— not a `"frontend/"` prefix, since B1-F2 never touches `Program.cs`
3020+
itself.
3021+
3022+
**Consequence for `T_B`/`R_B`.** Widening `INSTRUMENT_CARVE_OUTS` moves
3023+
`instrument_identity` (mechanically the same kind of event that forced a
3024+
`T_B` retake in §10.8c/10.8d) — so B1-F2 ends the same way those did: name
3025+
the corrected head as the new `T_B` once it is terminal-green, then retake
3026+
all four `R_B` snapshots fresh at it, with the extractor still carrying
3027+
its PRE-A1 semantics (B1-F2 performs no semantic treatment). B2.1a — the
3028+
actual extractor-side A1 change — remains a separate, later, not-yet-
3029+
authorized task, and it is scoped narrowly on purpose: stop emitting the
3030+
unconditional legacy release where the callee's own already-emitted
3031+
`guarded_facts` say the call is guard territory; never make `ConsumesParam`
3032+
path-sensitive, and never re-implement Election/Cells/Transform/fixpoint
3033+
math in C# — that stays exactly where B1 already froze it, in
3034+
`rust/crates/own-bridge/`, policed by `production_diff_gate.rust`. Doing
3035+
the narrower thing simultaneously satisfies the standing owner ruling and
3036+
avoids creating a third implementation of P-037 inside Roslyn.

0 commit comments

Comments
 (0)