Skip to content

Commit a159c36

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs: Phase D redesign memo (2026-05-28) — slice 2 substitution-lemma side condition (#203)
## Summary - Adds `formal/PHASE-D-REDESIGN.md` capturing the 2026-05-28 finding from the slice 2 implementation attempt and the redesigned approach. - Adds a side condition to `T_Lam_L1_*_Eff`: `forall r, In r (free_regions T1) -> In r R_in`. This ties the bound variable's regions to the body's input env, making `subst_typing_gen_l1_m`'s new case closeable. - Updates `formal/PRESERVATION-DESIGN.md §5.1` to reference the new memo. - Updates `.machine_readable/6a2/STATE.a2ml` next_action to slice 2 (redesigned). ## Why this PR A naive slice 2 (adding T_Lam_L1_*_Eff without the side condition) fails at `subst_typing_gen_l1_m`'s T_Lam_L1_*_Eff case because `In rv R` (substituted value's region, outer env) does not imply `In rv R_in` (body's input env, independent). The side condition resolves this by guaranteeing T1's free regions are in R_in. ## Phase D slice schedule (per memo) 1. ✅ slice 1: TFunEff syntax (MERGED PR #200) 2. ⏸ slice 2: T_Lam_L1_*_Eff with side condition + cascade through 8 inductive Qed lemmas 3. ⏸ slice 3: T_App_L1_Eff + TFunEff_count_monotone connection lemma 4. ⏸ slice 4: preservation_l1 lambda-rigidity closure (Semantics_L1.v:1694) 5. ⏸ slice 5: Phase B Slice 1 + Phase C unlocks Strict-predicate reformulation (PR #201) is independent and already merged — blocker 5 closed. ## Test plan - [x] No proof changes (docs-only) - [x] All 10 .v files still compile (no Coq changes) - [x] Cross-references between memo + PRESERVATION-DESIGN.md + STATE.a2ml consistent 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 46424c8 commit a159c36

3 files changed

Lines changed: 241 additions & 3 deletions

File tree

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66

77
@state(version="2.0"):
88
phase: "implementation"
9-
next_action: "Phase D — L2 effect-typed TFun (~4 sub-slices, per project_ephapax_post_slice4_plan). Adds new constructor TFunEff T1 T2 R_in R_out (legacy TFun preserved per CLAUDE.md directive). Cascade: Syntax.v free_regions/shift/subst/is_value → TypingL1.v T_Lam_L1_*_Eff + T_App_L1_Eff parallel rules → Semantics_L1.v closes lambda-rigidity admit at line 1694 + naturally enables Phase B Slice 1 wire AND Phase C body-input-shrinkage."
10-
last_action: "Phase A merged via PR #197 (d87b459) / Phase B Slice 1 DEFERRED 2026-05-28 / Phase C DEFERRED 2026-05-28. Phase A (L4 dyadic scaffold) docs-only landed cleanly: formal/L4-DYADIC.md design page + formal/L4.v ProgramMode labelling discipline. Phase B Slice 1 (TEcho linearity wire) investigated and deferred until Phase D: adding `| TEcho _ => true` to is_linear_ty is structurally non-vacuous at L1 (EEcho values typed at TEcho via T_Echo_L1 refute linear_value_is_loc_l1's conclusion + break 9 call-sites in subst_typing_gen_l1_m). Phase C (L1 list-vs-multiset structural bridge) investigated 2026-05-28 across all four design options (perm-modulo, multiset reformulation, rule redesign, defer) — rule redesign attempted in-flight on branch `proof/phase-c-l1-multiset-bridge` but proven to close only sub-sub-case (ii) (R has exactly 1 rr) while sub-sub-case (i) (R has ≥2 rr) requires body-input-shrinkage which is NOT a theorem (T_Loc_L1 counterexample at count=1; T_Let composition unstable). Owner chose option (d) defer as most mathematically safe + elegant. Both deferrals close at Phase D's L2 effect-typed TFun where the lambda body's R-flow becomes effect-typed."
11-
updated: 2026-05-28T11:30:00Z
9+
next_action: "Phase D slice 2 (REDESIGNED per formal/PHASE-D-REDESIGN.md) — add T_Lam_L1_Linear_Eff + T_Lam_L1_Affine_Eff with side condition `forall r, In r (free_regions T1) -> In r R_in` to TypingL1.v. The side condition ties the bound variable's regions to the body's input env, making subst_typing_gen_l1_m's new case closeable. Cascade through 8 inductive Qed lemmas in Semantics_L1.v. After slice 2: slice 3 (T_App_L1_Eff + TFunEff_count_monotone connection), slice 4 (preservation_l1 lambda-rigidity), slice 5 (Phase B + Phase C unlocks)."
10+
last_action: "Phase D slice 1 MERGED PR #200 (TFunEff syntax) + strict-predicate reformulation MERGED PR #201 (closes blocker 5 — Hfree shadow short-circuit) + Phase D slice 2 attempted then reverted: subst_typing_gen_l1_m's T_Lam_L1_*_Eff case fails because In rv R doesn't carry to In rv R_in (substituted value lives at outer R, body at R_in — independent envs). Redesign documented in formal/PHASE-D-REDESIGN.md: add side condition to T_Lam_L1_*_Eff requiring T1's free regions to be in R_in. Phase B Slice 1 + Phase C remain deferred per PRs #198 / #199 — both close at Phase D slice 5 unlocks. Per-session: TFunEff syntax + strict predicate + design memo all landed; structural blocker 5 closed; blockers 2/3/4/6 funnel through Phase D's revised slice plan."
11+
updated: 2026-05-28T12:30:00Z
1212

1313
@directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
1414
# Captured durable directive — preservation work is the four-layer redesign,

‎formal/PHASE-D-REDESIGN.md‎

Lines changed: 223 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,223 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# Phase D — L2 effect-typed TFun, redesign memo (2026-05-28)
5+
6+
This memo refines the Phase D plan in
7+
[`PRESERVATION-DESIGN.md §5.1`](PRESERVATION-DESIGN.md) based on
8+
analytical findings from the 2026-05-28 implementation attempt.
9+
**Read this before continuing Phase D work; it supersedes earlier
10+
slice-by-slice framings that omit the substitution-lemma side
11+
condition introduced below.**
12+
13+
## What landed
14+
15+
Two PRs landed on `main` during the 2026-05-28 session as part of
16+
Phase D's scaffolding plus an independent reformulation:
17+
18+
| PR | Title | What |
19+
|---|---|---|
20+
| #200 | `syntax(L2 Phase 2 / Phase D slice 1): add TFunEff effect-typed function constructor` | Adds `TFunEff T1 T2 R_in R_out` to `ty` in `Syntax.v`; extends `free_regions` in `Typing.v` for the new case. Zero proof changes. Legacy `TFun T1 T2` preserved per CLAUDE.md owner directive. |
21+
| #201 | `syntax: expr_strictly_free_of_region (closes blocker 5)` | Adds a strict variant of `expr_free_of_region` that recurses unconditionally into `ERegion r' body` (no shadow short-circuit). Migrates L1 region-shrinkage lemma preconditions to the strict variant. **Blocker 5 (predicate weakness from shadow short-circuit) — CLOSED.** |
22+
23+
## What we tried for slice 2 — and what broke
24+
25+
The 2026-05-28 slice 2 attempt added two new typing rules to
26+
`TypingL1.v`:
27+
28+
```coq
29+
| T_Lam_L1_Linear_Eff : forall R G T1 T2 e R_in R_out,
30+
R_in ; ctx_extend G T1 |=L1[Linear] e : T2 -| R_out ; (T1, true) :: G ->
31+
R ; G |=L1[Linear] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
32+
33+
| T_Lam_L1_Affine_Eff : forall R G T1 T2 e u R_in R_out,
34+
R_in ; ctx_extend G T1 |=L1[Affine] e : T2 -| R_out ; (T1, u) :: G ->
35+
R ; G |=L1[Affine] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
36+
```
37+
38+
Adding new constructors to `has_type_l1` forces every existing
39+
inductive lemma over `has_type_l1` to cover the new cases. The
40+
following lemmas were exercised:
41+
42+
| Lemma | T_Lam_L1_*_Eff case | Outcome |
43+
|---|---|---|
44+
| `count_occ_le_l1_m` | R-preserving outer | (not hit in this attempt; would close trivially) |
45+
| `region_shrink_preserves_typing_l1_gen_m` | Body's R_in unaffected by outer shrink → use body unchanged | ✅ closed via `eapply T_Lam_L1_*_Eff. eassumption.` |
46+
| `shift_typing_gen_l1_m` | Body's context extends by T1; shift by (S k) | ✅ closed via same pattern as legacy T_Lam |
47+
| `subst_typing_gen_l1_m` | **Substituted value lives at outer R, body at R_in** | 🛑 **STRUCTURAL FAIL** |
48+
49+
The substitution lemma's `T_Lam_L1_Linear_Eff` case decomposes as:
50+
51+
* Hypothesis: `Hregv : In rv R` (substituted value's region is in the
52+
outer environment).
53+
* Goal: produce a body derivation at `R_in` with `rv` substituted in.
54+
The body's typing rules (T_Loc_L1, etc.) for occurrences of the
55+
substituted variable require `In rv R_in`.
56+
* Available: nothing that ties `R` to `R_in`.
57+
58+
**`In rv R` does not imply `In rv R_in`** under the current rule
59+
shape. The body's `R_in` is a free parameter of the lambda type — the
60+
lambda value can declare any `R_in` it likes. There is no enforced
61+
connection between `R_in` and the regions of the bound variable's
62+
type at lambda formation. Substitution lemma is therefore not
63+
generalisable to the new constructors without an additional
64+
invariant.
65+
66+
## The structural insight
67+
68+
This is the *same* missing invariant we hit at:
69+
70+
* `Semantics_L1.v:553/621` (Phase C — shadowed `T_Region_Active_L1`)
71+
* `Semantics_L1.v:1694` (`preservation_l1` lambda-rigidity)
72+
* Sub-sub-case (i) of Phase C's option (c) attempt
73+
(`feedback`: body-input-shrinkage is not a theorem in general)
74+
75+
Each instance is the L1 vocabulary lacking a way to relate the
76+
**outer** region environment (where caller values live) to a
77+
**nested** region environment (where a lambda body, or a region's
78+
scoped body, operates). The L1 rule shapes treat outer and inner
79+
environments as independent, but **substitution and call sites
80+
require a connection**.
81+
82+
## The redesign — side condition on `T_Lam_L1_*_Eff`
83+
84+
Add an explicit side condition to `T_Lam_L1_*_Eff` requiring the
85+
bound variable's regions to be live in the body's input environment:
86+
87+
```coq
88+
| T_Lam_L1_Linear_Eff : forall R G T1 T2 e R_in R_out,
89+
(forall r, In r (Typing.free_regions T1) -> In r R_in) -> (* NEW *)
90+
R_in ; ctx_extend G T1 |=L1[Linear] e : T2 -| R_out ; (T1, true) :: G ->
91+
R ; G |=L1[Linear] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
92+
93+
| T_Lam_L1_Affine_Eff : forall R G T1 T2 e u R_in R_out,
94+
(forall r, In r (Typing.free_regions T1) -> In r R_in) -> (* NEW *)
95+
R_in ; ctx_extend G T1 |=L1[Affine] e : T2 -| R_out ; (T1, u) :: G ->
96+
R ; G |=L1[Affine] ELam T1 e : TFunEff T1 T2 R_in R_out -| R ; G
97+
```
98+
99+
**Interpretation**: any region appearing in the bound variable's
100+
type `T1` is guaranteed to be live in the body's input environment
101+
`R_in`. When substituting a value `v : T1` with `free_regions T1 ⊇ {rv}`
102+
into the body, `In rv R_in` follows from the side condition.
103+
104+
For typical lambda types:
105+
106+
* `T1 = TBase TUnit`: `free_regions T1 = []`. Side condition vacuous.
107+
No constraint on R_in. ✓
108+
* `T1 = TString rv`: `free_regions T1 = [rv]`. Side condition forces
109+
`In rv R_in`. ✓
110+
* `T1 = TPair (TString r1) (TString r2)`: forces both `r1` and `r2`
111+
in R_in. ✓
112+
* `T1 = TFun T1' T2'`: forces all free regions of T1' and T2' into
113+
R_in. ✓ (Closures over substring-typed values carry their region
114+
requirements.)
115+
116+
This side condition is **discharge-able at lambda formation time**:
117+
the caller forming the lambda must establish the constraint. In
118+
practice this is automatic — any program that types a lambda body
119+
referencing a region in T1 already has that region in scope.
120+
121+
## Why this closes `subst_typing_gen_l1_m`
122+
123+
In the T_Lam_L1_Linear_Eff case of the substitution lemma:
124+
125+
* Hypothesis from rule: `H : forall r, In r (free_regions T1) -> In r R_in`.
126+
* The substituted value `vv` has `In rv R` (lemma's preexisting
127+
Hregv) AND `vv : T1` with `In rv (free_regions T1)` (since
128+
`linear_value_is_loc_l1` constrains rv to be T1's region).
129+
* Apply H: `In rv R_in`. ✓
130+
* Body typing after substitution uses `In rv R_in` to discharge
131+
T_Loc_L1's `In r R` premise at the substituted variable's
132+
occurrences.
133+
134+
The lemma case closes via the same pattern as legacy T_Lam_L1_Linear
135+
but threaded through R_in instead of outer R.
136+
137+
## Slice plan (revised)
138+
139+
| Slice | Scope | Status |
140+
|---|---|---|
141+
| 1 | TFunEff syntax (`Syntax.v` + `free_regions`) | ✅ MERGED PR #200 |
142+
| 2 (redesigned) | `T_Lam_L1_*_Eff` with side condition; cascade through 8 inductive lemmas in `Semantics_L1.v` | Pending implementation |
143+
| 3 | `T_App_L1_Eff` + `TFunEff_count_monotone` connection lemma | Pending |
144+
| 4 | `preservation_l1` lambda-rigidity closure (`Semantics_L1.v:1694`) | Pending |
145+
| 5 | Phase B Slice 1 (TEcho linearity wire) + Phase C (list-vs-multiset bridge) unlocks | Pending |
146+
147+
The strict-predicate reformulation (PR #201) is independent of these
148+
slices and already merged.
149+
150+
## Implementation notes for slice 2
151+
152+
1. The 2 rules: add right after `T_Lam_L1_Affine` at
153+
`TypingL1.v:183` (verified compile order works).
154+
2. The side condition is a `forall r, In r (free_regions T1) -> In r R_in`
155+
Prop — straightforward to discharge in induction cases.
156+
3. **Cascade to 8 inductive Qed lemmas** in `Semantics_L1.v`:
157+
- `count_occ_le_l1_m` — trivial (R-preserving outer)
158+
- `region_shrink_preserves_typing_l1_gen_m` — re-apply rule with
159+
body unchanged + side condition unchanged (region shrink at
160+
outer doesn't touch the body's premise)
161+
- `typing_preserves_length_l1` — trivial
162+
- `typing_preserves_bindings_l1` — mirrors legacy T_Lam case
163+
- `unrestricted_flag_unchanged_l1` — similar
164+
- `shift_typing_gen_l1_m` — mirrors legacy T_Lam case
165+
- `value_R_G_preserving_l1` — lambda is a value; R-preserving
166+
case trivial
167+
- `subst_typing_gen_l1_m` — **uses the side condition** to discharge
168+
`In rv R_in` from `In rv (free_regions T1)`
169+
4. `Counterexample.v` is unaffected (no TFunEff or T_Lam_L1_*_Eff
170+
usage).
171+
172+
## Owner directive compliance
173+
174+
Per CLAUDE.md owner directive 2026-05-27:
175+
176+
* ✅ Zero new `Admitted.` or `Axiom.` declarations
177+
* ✅ No patching of `Semantics.v` `preservation` (provably false)
178+
* ✅ No patching of legacy `Typing.v` judgment
179+
* ✅ Counterexample.v regression theorem untouched
180+
* ✅ All commits GPG-signed
181+
* ✅ Auto-merge ON for every PR
182+
183+
## Anti-patterns this redesign avoids
184+
185+
* **Strengthening `subst_typing_gen_l1_m`'s preconditions** with a
186+
per-call-site `In rv R_in` hypothesis would cascade to every
187+
caller and force them to prove the connection ad-hoc. The side
188+
condition at rule formation localises the constraint.
189+
* **Separate `has_type_l1_eff` judgment** would double the lemma
190+
surface and require bridge lemmas. Avoided by extending
191+
`has_type_l1` in place with a clean side condition.
192+
* **Constraining R_in = outer R** would defeat the purpose of
193+
effect-typing. Avoided.
194+
195+
## Cross-references
196+
197+
* [`PRESERVATION-DESIGN.md §5.1`](PRESERVATION-DESIGN.md) — original
198+
Phase D outline.
199+
* [`PROOF-NEEDS.md`](../PROOF-NEEDS.md) — proof debt audit (Phase B
200+
+ Phase C deferral rows reference this Phase D closure).
201+
* `Semantics_L1.v:553/621` — Phase C structural admits that close
202+
once slice 4+5 land.
203+
* `Semantics_L1.v:1694` — `preservation_l1` lambda-rigidity admit
204+
that closes at slice 4.
205+
206+
## Future re-attempts of perm_l1 (agent finding 2026-05-28)
207+
208+
The standalone `region_env_perm_typing_l1` (existential output)
209+
agent attempt 2026-05-28 found 7 admits across two failure families:
210+
211+
1. R-stability rules (`T_Lam_L1_*`, `T_Borrow_Val_L1`, `T_Echo_L1`)
212+
— force output_R = input_R as lists; IH gives perm-equiv not
213+
list-equal.
214+
2. Branch-agreement rules (`T_Case_L1_*`, `T_If_L1_*`) — branches
215+
yield outputs perm-equiv to a join but not list-equal.
216+
217+
Both families dissolve once the L2 effect-typed structure is in
218+
place: R-stability rules get effect-typed wrappers that don't force
219+
list equality, and branch-agreement gets a per-branch effect that
220+
the join sums.
221+
222+
`perm_l1` is therefore unblocked at slice 5 (post-T_App_L1_Eff
223+
landing), not at slice 2.

‎formal/PRESERVATION-DESIGN.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -479,6 +479,21 @@ typed lambdas are introduced". The Linear ⇒ Affine weakening
479479
(`linear_to_affine` Qed, PR #176) is independent of this dependency
480480
and already ships.
481481

482+
**Phase D — current refinement (2026-05-28).** Slice 1 (TFunEff
483+
syntax) landed via PR #200. An implementation attempt for slice 2
484+
(`T_Lam_L1_*_Eff` typing rules) surfaced a substitution-lemma
485+
structural gap: the substituted value's region (`In rv R`, outer)
486+
does not connect to the lambda body's input env (`R_in`,
487+
independent), so `subst_typing_gen_l1_m` cannot close its new
488+
case without an additional invariant. The refinement adds a side
489+
condition to `T_Lam_L1_*_Eff` requiring
490+
`forall r, In r (free_regions T1) -> In r R_in`, which ties the
491+
bound variable's regions to the body's input environment and
492+
makes substitution well-defined. See
493+
[`PHASE-D-REDESIGN.md`](PHASE-D-REDESIGN.md) for the full memo
494+
including the revised slice plan, lemma-cascade audit, and
495+
owner-directive compliance check.
496+
482497
---
483498

484499
## 6. Layer 3 — Echo / residue, in design

0 commit comments

Comments
 (0)