Skip to content

Commit 3745975

Browse files
claudeclaude
committed
P-037 A18-0: RESULT PASS — the eight-row decomposition holds
The eight B1 UNEXPLAINED rows decompose into two seams with no fourth class: - G == L_canonical == may on 8/8, and the G <-> L_canonical class is EQUAL; - L_canonical <-> L_actual has one deterministic reason per row: CONSUMES_PARAM_FOLD x6 (must -> may) and ARGUMENT_SHAPE_LOSS x2 (no -> may); - every witness holds, and the shape-loss probe shows the wrapper masks a fold. No KILL fired. L_actual and G match B1's committed values, and G does not move under the rewrite. The diff since 92cedb7 is the note and one 158-line script. B1 stays FAIL in #373. This authorizes A18-1 only; A18-1 is not started. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KmiyfrkaG9sJruTcshM2oq
1 parent a3270b9 commit 3745975

2 files changed

Lines changed: 252 additions & 3 deletions

File tree

‎docs/evidence/p037-a18/eight-rows.json‎

Lines changed: 176 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,176 @@
1+
{
2+
"schema": "p037-a18-eight-rows/1",
3+
"population_commit": "571669e8c40e46d1c29908f00dea2311b88ae4fd",
4+
"instrument_commit": "a3270b9d75dccfbff890dad47eec74f4ed1d74df",
5+
"rows_checked": 8,
6+
"g_equals_canonical": 8,
7+
"deterministic_reason": 8,
8+
"witnessed": 8,
9+
"rows": [
10+
{
11+
"doc": "corpus/p036-bakeoff/guarded-consume-negation-wrapper/after.cs",
12+
"method": "GuardedNegation.Outer",
13+
"index": 0,
14+
"ordinal": 0,
15+
"param": "s",
16+
"actual": "must",
17+
"guarded": "may",
18+
"void": false,
19+
"reason": "CONSUMES_PARAM_FOLD",
20+
"legacy_op": "release",
21+
"callee": "GuardedNegation.Inner",
22+
"callee_actual": "may",
23+
"line": 18,
24+
"canonical": "may",
25+
"guarded_after_rewrite": "may",
26+
"canonical_class": "EQUAL",
27+
"witness": true
28+
},
29+
{
30+
"doc": "corpus/p036-bakeoff/guarded-consume-negation-wrapper/before.cs",
31+
"method": "GuardedNegation.Outer",
32+
"index": 0,
33+
"ordinal": 0,
34+
"param": "s",
35+
"actual": "must",
36+
"guarded": "may",
37+
"void": false,
38+
"reason": "CONSUMES_PARAM_FOLD",
39+
"legacy_op": "release",
40+
"callee": "GuardedNegation.Inner",
41+
"callee_actual": "may",
42+
"line": 18,
43+
"canonical": "may",
44+
"guarded_after_rewrite": "may",
45+
"canonical_class": "EQUAL",
46+
"witness": true
47+
},
48+
{
49+
"doc": "corpus/p036-bakeoff/guarded-consume-wrapper-forward/after.cs",
50+
"method": "GuardedWrapper.Outer",
51+
"index": 0,
52+
"ordinal": 0,
53+
"param": "s",
54+
"actual": "must",
55+
"guarded": "may",
56+
"void": false,
57+
"reason": "CONSUMES_PARAM_FOLD",
58+
"legacy_op": "release",
59+
"callee": "GuardedWrapper.Inner",
60+
"callee_actual": "may",
61+
"line": 18,
62+
"canonical": "may",
63+
"guarded_after_rewrite": "may",
64+
"canonical_class": "EQUAL",
65+
"witness": true
66+
},
67+
{
68+
"doc": "corpus/p036-bakeoff/guarded-consume-wrapper-forward/before.cs",
69+
"method": "GuardedWrapper.Outer",
70+
"index": 0,
71+
"ordinal": 0,
72+
"param": "s",
73+
"actual": "must",
74+
"guarded": "may",
75+
"void": false,
76+
"reason": "CONSUMES_PARAM_FOLD",
77+
"legacy_op": "release",
78+
"callee": "GuardedWrapper.Inner",
79+
"callee_actual": "may",
80+
"line": 19,
81+
"canonical": "may",
82+
"guarded_after_rewrite": "may",
83+
"canonical_class": "EQUAL",
84+
"witness": true
85+
},
86+
{
87+
"doc": "arg-cast-and-bang",
88+
"method": "ShapeCastBang.Cast",
89+
"index": 0,
90+
"ordinal": 0,
91+
"param": "p",
92+
"actual": "no",
93+
"guarded": "may",
94+
"void": false,
95+
"reason": "ARGUMENT_SHAPE_LOSS",
96+
"legacy_op": "use",
97+
"callee": "ShapeCastBang.Keep",
98+
"callee_actual": "may",
99+
"line": 28,
100+
"canonical": "may",
101+
"guarded_after_rewrite": "may",
102+
"canonical_class": "EQUAL",
103+
"probe": {
104+
"line_before": "Keep((Stream)p, keep);",
105+
"line_after": "Keep(p, keep);",
106+
"op_after": "release",
107+
"actual_after": "must"
108+
},
109+
"witness": true
110+
},
111+
{
112+
"doc": "arg-cast-and-bang",
113+
"method": "ShapeCastBang.Bang",
114+
"index": 0,
115+
"ordinal": 0,
116+
"param": "p",
117+
"actual": "no",
118+
"guarded": "may",
119+
"void": false,
120+
"reason": "ARGUMENT_SHAPE_LOSS",
121+
"legacy_op": "use",
122+
"callee": "ShapeCastBang.Keep",
123+
"callee_actual": "may",
124+
"line": 33,
125+
"canonical": "may",
126+
"guarded_after_rewrite": "may",
127+
"canonical_class": "EQUAL",
128+
"probe": {
129+
"line_before": "Keep(p!, keep);",
130+
"line_after": "Keep(p, keep);",
131+
"op_after": "release",
132+
"actual_after": "must"
133+
},
134+
"witness": true
135+
},
136+
{
137+
"doc": "guard-forward-bare",
138+
"method": "ShapeForwardBare.Outer",
139+
"index": 0,
140+
"ordinal": 0,
141+
"param": "s",
142+
"actual": "must",
143+
"guarded": "may",
144+
"void": false,
145+
"reason": "CONSUMES_PARAM_FOLD",
146+
"legacy_op": "release",
147+
"callee": "ShapeForwardBare.Inner",
148+
"callee_actual": "may",
149+
"line": 17,
150+
"canonical": "may",
151+
"guarded_after_rewrite": "may",
152+
"canonical_class": "EQUAL",
153+
"witness": true
154+
},
155+
{
156+
"doc": "guard-forward-negated",
157+
"method": "ShapeForwardNegated.Outer",
158+
"index": 0,
159+
"ordinal": 0,
160+
"param": "s",
161+
"actual": "must",
162+
"guarded": "may",
163+
"void": false,
164+
"reason": "CONSUMES_PARAM_FOLD",
165+
"legacy_op": "release",
166+
"callee": "ShapeForwardNegated.Inner",
167+
"callee_actual": "may",
168+
"line": 17,
169+
"canonical": "may",
170+
"guarded_after_rewrite": "may",
171+
"canonical_class": "EQUAL",
172+
"witness": true
173+
}
174+
],
175+
"result": "PASS \u2014 A18 8-ROW DECOMPOSITION HOLDS"
176+
}

‎docs/notes/p037-a18-legacy-decomposition.md‎

Lines changed: 76 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
# P-037 A18: legacy decomposition (pre-registered)
22

3-
> Status: **PRE-REGISTERED.** Committed before any implementation. The owner
4-
> authorized implementing A18-0 right after this commit, without a further
5-
> review stop. The boundaries below do not move after this SHA.
3+
> Status: **RESULT: PASS — A18 8-ROW DECOMPOSITION HOLDS (§F).**
4+
> Pre-registered in `ccde27c` before any implementation; the boundaries did
5+
> not move. This PASS does not make B1 pass. It only authorizes A18-1.
66
>
77
> - Base: `92cedb7`, the head of #373 (B1, `RESULT: FAIL — B1 BLOCKED (KILL 5)`).
88
> - Branch: `research/p037-a18-legacy-decomposition`.
@@ -167,3 +167,76 @@ Phase C.
167167
- Not touched: `ConsumesParam`, B1's eight classifications, missing-sidecar
168168
behavior, R, A14, #368, Phase C, the three P-037 difference classes,
169169
production verdicts/MOS, `own-guarded`, and the extractor.
170+
171+
## F. Result (MEASURED OBSERVATION)
172+
173+
`RESULT: PASS — A18 8-ROW DECOMPOSITION HOLDS`
174+
175+
- Instrument: `scripts/p037_a18_decompose.py` at `a3270b9`. It reuses the
176+
unchanged B1 extractor and `own-guarded-report`.
177+
- Population: `571669e`.
178+
- Evidence: `docs/evidence/p037-a18/eight-rows.json`.
179+
180+
| row | legacy op at the forward | `L_actual` | `L_canonical` | `G` | `G ↔ L_canonical` | reason |
181+
|---|---|---|---|---|---|---|
182+
| `GuardedNegation.Outer` (before, after) | `release`, line 18 | must | may | may | EQUAL | `CONSUMES_PARAM_FOLD` |
183+
| `GuardedWrapper.Outer` (after, before) | `release`, lines 18 / 19 | must | may | may | EQUAL | `CONSUMES_PARAM_FOLD` |
184+
| `ShapeForwardBare.Outer` | `release`, line 17 | must | may | may | EQUAL | `CONSUMES_PARAM_FOLD` |
185+
| `ShapeForwardNegated.Outer` | `release`, line 17 | must | may | may | EQUAL | `CONSUMES_PARAM_FOLD` |
186+
| `ShapeCastBang.Cast` | `use`, line 28 | no | may | may | EQUAL | `ARGUMENT_SHAPE_LOSS` |
187+
| `ShapeCastBang.Bang` | `use`, line 33 | no | may | may | EQUAL | `ARGUMENT_SHAPE_LOSS` |
188+
189+
The PASS conditions:
190+
- rows checked 8;
191+
- `G == L_canonical` 8;
192+
- deterministic reason 8;
193+
- witness holds 8;
194+
- unexplained decomposition 0.
195+
196+
`L_actual` and `G` equal the values B1 committed on all eight, so the gate is
197+
not void. `G` is unchanged by the rewrite on all eight: the rewrite does not
198+
leak into the guarded read.
199+
200+
**Witnesses.**
201+
- `CONSUMES_PARAM_FOLD`: each row's callee has production MOS `may` (the four
202+
`Inner`s), yet a `release` stands at the forwarding line. That is
203+
may-as-must. Rewriting only that op to the honest forward moves the row
204+
from `must` to `may`.
205+
- `ARGUMENT_SHAPE_LOSS`: the same one-op rewrite moves the row from `no` to
206+
`may`. The source probe strips only the value-preserving wrapper on that
207+
line:
208+
- `Keep((Stream)p, keep);` → `Keep(p, keep);`
209+
- `Keep(p!, keep);` → `Keep(p, keep);`
210+
211+
After that change, legacy emits `release` and `L_actual` becomes `must`.
212+
213+
**Hard KILL: none fired.**
214+
1. `G == L_canonical` on 8.
215+
2. Guarded semantics were not modified.
216+
3. `ConsumesParam` was not changed.
217+
4. OwnIR/A2 facts were not changed; the rewrite is a measurement input.
218+
5. `L_canonical` reads only the frozen records, bodies and sidecars. The
219+
callee position comes from B1's own coordinate rows. Source text is used
220+
only by the shape-loss witness.
221+
6. One deterministic reason per row.
222+
7. There is no framework: one 158-line script.
223+
224+
The diff since `92cedb7` is this note and that script only.
225+
226+
### F.1 Findings for A18-1 (INFERENCE, not measured beyond these eight)
227+
228+
- **The two reasons compose.** Under the wrapper, the shape-loss rows hide a
229+
fold: without the wrapper they read `must`, exactly like the six fold rows.
230+
So `L_actual` of a shape-loss row is "the fold, masked by an argument shape
231+
legacy cannot see through". In A18-1 a row must therefore get the reason
232+
that explains **its own** `L_actual` (here `ARGUMENT_SHAPE_LOSS`), never the
233+
one it would have without the wrapper. Stacked reasons on one row would
234+
need a pre-registered rule first.
235+
- **The rewrite rule is narrow on purpose.** It needs exactly one forwarding
236+
sidecar call and exactly one legacy op on the parameter at that line. In
237+
the population, rows outside that shape have no reason under this rule.
238+
Per §D they stay `UNEXPLAINED` and block Phase C; they are never bucketed.
239+
240+
**Authorized next:** A18-1, the same decomposition on the frozen `571669e`
241+
population, with the §D two-classification rule. Not started here. B1 stays
242+
`RESULT: FAIL — B1 BLOCKED (KILL 5)` in #373.

0 commit comments

Comments
 (0)