Skip to content

Commit 56f592f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(formal): L1 closure status — §4.7 status + §4.8 soundness finding + PROOF-STATUS.a2ml
Post-L1.A-F closure snapshot. Documents that the L1 chain landed six PRs (#155 / #157-#163) and now sits at: - 4 admits remain in Semantics_L1.v (down from 7 mid-chain) - 1 narrower Axiom (region_liveness_at_split_l1) replacing the original unsound loc_retype_at_R_l1 - 2 Admitted markers (region_shrink_gen, preservation_l1) Each residual admit now has an in-source structural diagnosis. Two are tractable supporting-lemma work (L1.B residual + L1.D-StringConcat). TWO surface a calculus-design soundness gap, not a proof-engineering gap: T_Lam_L1 rigidly fixes the lambda body's R at lambda-creation; T_Var_*_L1 permit typing TString r at empty R. Combined, the L1 typing is too permissive for preservation under R-shifting steps. PRESERVATION-DESIGN.md §4.8 documents three independent resolution paths (effect-typed lambdas / restrict T_Lam / restrict T_Var). None is in scope for L1 minimal-fix — each is a follow-up. New machine-readable manifest: formal/PROOF-STATUS.a2ml — TOML-flavoured a2ml snapshot of every Qed lemma, every residual admit/axiom, and the proof-debt classes. Consumed by automated trackers and CI gates that need to know what counts as proven here. Human-readable companion: PRESERVATION-DESIGN.md §4.7 and §4.8. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent f35da79 commit 56f592f

2 files changed

Lines changed: 289 additions & 0 deletions

File tree

‎formal/PRESERVATION-DESIGN.md‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,70 @@ The at-pre helper pattern survives because it is orthogonal to the
224224
threading change: the pre-step env is the new `R_in` of the
225225
diagonal typing rule.
226226

227+
### 4.7 L1 closure status (2026-05-27)
228+
229+
Six follow-up PRs against `proof/l1-region-threading-design` (the
230+
design branch) landed the L1 implementation incrementally:
231+
232+
| PR | Scope | Outcome |
233+
|---|---|---|
234+
| #155 | `TypingL1.v` — the R-threaded judgment + counterexample regression | `bad_input_untypable_l1` Qed |
235+
| #157 | `Semantics_L1.v` skeleton — `preservation_l1` stated | scaffold |
236+
| #158 (L1.A) | `value_R_G_preserving_l1` | Qed |
237+
| #159 (L1.B) | `region_shrink_preserves_typing_l1` (routes via `_gen`) | Qed; `_gen` Admitted (2 internal admits at the time) |
238+
| #160 (L1.C) | `subst_preserves_typing_l1` (strengthened statement) | Qed; introduced a sub-Axiom for the inner-R retype obligation |
239+
| #161 (L1.D) | `preservation_l1` proof body | 29/33 cases Qed; 4 admits surface region-env weakening gap |
240+
| #162 (L1.F) | Discharge unsound `loc_retype_at_R_l1` axiom | Original Axiom replaced by a Qed-able Lemma + a narrower (still admitted) `region_liveness_at_split_l1`; 2 of 11 call sites discharge directly |
241+
| #163 (L1.E) | Region-env weakening attack on the 6 admits (2 in `_gen` + 4 in `preservation_l1`) | 2 admits closed via new `count_occ_le_l1` monotonicity lemma; 4 admits remain with structural diagnosis (see below) |
242+
243+
After all six PRs land on the design branch:
244+
245+
- **4 admits remain** in `Semantics_L1.v`:
246+
1. `region_shrink_preserves_typing_l1_gen` line ~390 — `T_Region_Active_L1` shadowed case. List-vs-multiset mismatch: set-equality bridges don't preserve `remove_first_L1` outputs (the operation depends on list position, not just membership).
247+
2. `preservation_l1` `S_StringConcat_Step2` — operationally sound; needs a `step_pop_disjoint_from_type_l1` lemma (tractable, deferred to L1.G).
248+
3. `preservation_l1` `S_App_Step2` — see §4.8 (fundamental soundness gap).
249+
4. `preservation_l1` `S_Pair_Step2` — see §4.8 (same gap).
250+
251+
- **1 Axiom remains**: `region_liveness_at_split_l1` (a narrower, sound-as-stated statement of what the original unsound `loc_retype_at_R_l1` was reaching for). Three closure paths documented in-file: strengthen `T_Var_Lin_L1`, add a side condition to `subst_typing_gen_l1`, or carry `In rv R_intermediate` through the induction.
252+
253+
- **2 `Admitted.` markers** remain (`region_shrink_preserves_typing_l1_gen` and `preservation_l1`) — each closes the moment its internal admits close.
254+
255+
### 4.8 Soundness finding: T_Lam_L1 + T_Var_*_L1 are too permissive
256+
257+
L1.E surfaced a genuine soundness issue, separate from the proof-
258+
engineering gaps:
259+
260+
**The finding.** `T_Lam_L1` rigidly fixes the lambda body's region
261+
environment `R` at lambda-creation time, with no mechanism to retype
262+
the body at a shifted `R` before application. Combined with the
263+
orthogonal observation that `T_Var_Lin_L1` and `T_Var_Unr_L1` permit
264+
typing variables of type `TString r` at *any* `R` (including `R = []`),
265+
the L1 typing system is genuinely too permissive about region presence
266+
for preservation under `R`-shifting steps.
267+
268+
**Why this matters operationally.** `S_App_Step2` evaluates the
269+
argument of `EApp v_fn e_arg` when `v_fn` is a value (a lambda). The
270+
inner step on `e_arg` may shift `R → R'` via a region operation. The
271+
lambda's typing was fixed at the *original* `R`; the rules give no
272+
way to re-derive its typing at `R'`. The preservation theorem is
273+
therefore unprovable for these cases under the current rules — not a
274+
proof-engineering gap but a calculus-design gap.
275+
276+
**Resolution paths** (each independent):
277+
278+
1. **Effect-typed lambdas (L2/L3 territory)**: parameterise function
279+
types over the region-effect they have, so the typing rule sees
280+
how the body changes `R` and can re-derive at the call site.
281+
2. **Restrict T_Lam_L1**: require the lambda body to be region-pure
282+
(no free regions in `T1`, `T2`, or the body's intermediate types).
283+
This is restrictive but unblocks preservation immediately.
284+
3. **Restrict T_Var_*_L1**: require `In r R` for any variable whose
285+
type contains `r`. This propagates the region constraint into the
286+
variable-use side, closing the gap.
287+
288+
The L1.E PR documents this in-source. None of (1)/(2)/(3) is in scope
289+
for the L1 minimal-fix; each is a follow-up. See ROADMAP for sequencing.
290+
227291
---
228292

229293
## 5. Layer 2 in detail — Linear vs Affine modality

‎formal/PROOF-STATUS.a2ml‎

Lines changed: 225 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,225 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# PROOF-STATUS.a2ml — machine-readable Coq proof state
5+
#
6+
# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F).
7+
# Consumed by automated proof-debt trackers, status dashboards, and
8+
# CI gates that need to know "what counts as proven here".
9+
#
10+
# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7 and §4.8.
11+
12+
[metadata]
13+
version = "1.0.0"
14+
snapshot-date = "2026-05-27"
15+
design-branch = "proof/l1-region-threading-design"
16+
spec-doc = "formal/PRESERVATION-DESIGN.md"
17+
counterexample = "formal/Counterexample.v"
18+
19+
# ============================================================================
20+
# FILES — what's in formal/ and its proof-status posture
21+
# ============================================================================
22+
23+
[[files]]
24+
path = "formal/Syntax.v"
25+
purpose = "AST + region/context infrastructure"
26+
status = "stable"
27+
qed-only = true
28+
29+
[[files]]
30+
path = "formal/Typing.v"
31+
purpose = "legacy has_type judgment (single R, no threading)"
32+
status = "frozen"
33+
qed-only = true
34+
note = "Retained for legacy preservation. L1 judgment lives in TypingL1.v."
35+
36+
[[files]]
37+
path = "formal/TypingL1.v"
38+
purpose = "L1 has_type_l1 judgment (R-threaded)"
39+
status = "stable"
40+
qed-only = true
41+
landed-in = "PR-155"
42+
43+
[[files]]
44+
path = "formal/Counterexample.v"
45+
purpose = "verified counterexample to preservation as originally stated"
46+
status = "stable"
47+
qed-only = true
48+
key-lemmas = [
49+
"bad_typable",
50+
"bad_step",
51+
"bad_post_untypable",
52+
"bad_input_untypable_l1"
53+
]
54+
55+
[[files]]
56+
path = "formal/Semantics.v"
57+
purpose = "operational step + legacy preservation"
58+
status = "frozen-with-1-residual"
59+
admit-count = 1
60+
note = "Legacy preservation has 1 residual admit (S_Region_Step + T_Region_Active region weakening). Out of scope for L1 redesign."
61+
62+
[[files]]
63+
path = "formal/Semantics_L1.v"
64+
purpose = "L1 preservation theorem + helpers"
65+
status = "active"
66+
admit-count = 4
67+
axiom-count = 1
68+
admitted-lemma-count = 2
69+
landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163"]
70+
71+
# ============================================================================
72+
# L1 PROOF CHAIN — Qed lemmas
73+
# ============================================================================
74+
75+
[[qed-lemmas]]
76+
name = "remove_first_eq_l1"
77+
file = "Semantics_L1.v"
78+
purpose = "trivial bridge between remove_first and remove_first_L1"
79+
80+
[[qed-lemmas]]
81+
name = "value_R_G_preserving_l1"
82+
file = "Semantics_L1.v"
83+
landed-in = "PR-158"
84+
swarm-stream = "L1.A"
85+
purpose = "value v at R;G -| R';G' implies R'=R and G'=G"
86+
87+
[[qed-lemmas]]
88+
name = "region_shrink_preserves_typing_l1"
89+
file = "Semantics_L1.v"
90+
landed-in = "PR-159"
91+
swarm-stream = "L1.B"
92+
purpose = "shrink region env for value typings (wraps _gen)"
93+
depends-on-admitted = ["region_shrink_preserves_typing_l1_gen"]
94+
95+
[[qed-lemmas]]
96+
name = "subst_preserves_typing_l1"
97+
file = "Semantics_L1.v"
98+
landed-in = "PR-160"
99+
swarm-stream = "L1.C"
100+
purpose = "substitution preserves L1 typing (strengthened statement)"
101+
note = "Original statement was unsound (typed v at independent R1); strengthened to share R with body."
102+
103+
[[qed-lemmas]]
104+
name = "loc_retype_at_R_l1"
105+
file = "Semantics_L1.v"
106+
landed-in = "PR-162"
107+
swarm-stream = "L1.F"
108+
purpose = "ELoc l r retypes at any R_inner that has r — pure T_Loc_L1 consequence"
109+
note = "Replaces the original UNSOUND axiom of the same name. Adds 'In r R_inner' premise that the axiom omitted."
110+
111+
[[qed-lemmas]]
112+
name = "count_occ_le_l1"
113+
file = "Semantics_L1.v"
114+
landed-in = "PR-163"
115+
swarm-stream = "L1.E"
116+
purpose = "typing is region-count monotonic: count r R' ≤ count r R"
117+
118+
[[qed-lemmas]]
119+
name = "count_occ_in_input_l1"
120+
file = "Semantics_L1.v"
121+
landed-in = "PR-163"
122+
swarm-stream = "L1.E"
123+
purpose = "corollary: In r R' implies In r R"
124+
125+
# ============================================================================
126+
# PRESERVATION THEOREM
127+
# ============================================================================
128+
129+
[preservation-l1]
130+
file = "Semantics_L1.v"
131+
landed-in = "PR-161"
132+
swarm-stream = "L1.D"
133+
status = "Admitted"
134+
cases-total = 33
135+
cases-qed = 29
136+
cases-admit = 4
137+
note = "All Qed cases use the four Qed helpers above. The 4 admits all surface a single structural class (see [proof-debt] below)."
138+
139+
# ============================================================================
140+
# OUTSTANDING PROOF DEBT
141+
# ============================================================================
142+
143+
[[proof-debt]]
144+
id = "L1.B-residual-1"
145+
file = "Semantics_L1.v"
146+
line-anchor = "region_shrink_preserves_typing_l1_gen T_Region_Active_L1 shadowed"
147+
class = "list-vs-multiset"
148+
tractable = true
149+
diagnosis = "set-equality bridges don't preserve remove_first_L1 output because the operation is positional, not set-theoretic"
150+
closes-when = "redesign remove_first_L1 as a multiset operation, OR prove a position-aware bridge"
151+
152+
[[proof-debt]]
153+
id = "L1.D-StringConcat"
154+
file = "Semantics_L1.v"
155+
line-anchor = "preservation_l1 S_StringConcat_Step2"
156+
class = "operationally-sound-needs-supporting-lemma"
157+
tractable = true
158+
diagnosis = "value v1 left, e2 steps right. Need step_pop_disjoint_from_type_l1 lemma (operational claim: a step's R-pop doesn't pop a region appearing in any sibling's free regions)"
159+
closes-when = "prove step_pop_disjoint_from_type_l1"
160+
161+
[[proof-debt]]
162+
id = "L1.D-App"
163+
file = "Semantics_L1.v"
164+
line-anchor = "preservation_l1 S_App_Step2"
165+
class = "calculus-soundness-gap"
166+
tractable = false
167+
diagnosis = "T_Lam_L1 rigidly fixes the lambda body's R at lambda-creation; T_Var_*_L1 permit typing TString r at empty R. Combined, the L1 typing is too permissive for preservation under R-shifting steps."
168+
closes-when = "one of (1) effect-typed lambdas (L2/L3), (2) restrict T_Lam_L1 to region-pure bodies, (3) restrict T_Var_*_L1 to require In r R for variables of type containing r"
169+
follow-up = "see PRESERVATION-DESIGN.md §4.8"
170+
171+
[[proof-debt]]
172+
id = "L1.D-Pair"
173+
file = "Semantics_L1.v"
174+
line-anchor = "preservation_l1 S_Pair_Step2"
175+
class = "calculus-soundness-gap"
176+
tractable = false
177+
diagnosis = "same as L1.D-App"
178+
closes-when = "see L1.D-App"
179+
follow-up = "see PRESERVATION-DESIGN.md §4.8"
180+
181+
[[proof-debt]]
182+
id = "L1.C-region-liveness"
183+
file = "Semantics_L1.v"
184+
line-anchor = "region_liveness_at_split_l1 (Axiom)"
185+
class = "carry-invariant-through-induction"
186+
tractable = true
187+
diagnosis = "subst_typing_gen_l1 needs to know that In rv R_inner at each compound-rule split point. The outer call provides In rv R; the inductive descent doesn't propagate it because T_Var_Lin_L1 doesn't enforce In rv R."
188+
closes-when = "one of (1) strengthen T_Var_Lin_L1 to require In rv R, (2) add a side condition to subst_typing_gen_l1 stating In rv R at every R_inner reached, (3) prove a region-liveness corollary of L1.B's count monotonicity"
189+
190+
# ============================================================================
191+
# DOCUMENTATION POINTERS
192+
# ============================================================================
193+
194+
[docs]
195+
design = "formal/PRESERVATION-DESIGN.md"
196+
handoff = "formal/PRESERVATION-HANDOFF.md"
197+
roadmap = "ROADMAP.adoc"
198+
counterexample = "formal/Counterexample.v"
199+
disambiguation = "nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md"
200+
201+
[docs.sections]
202+
preservation-design-§4-1-judgment = "L1 judgment signature"
203+
preservation-design-§4-5-statement = "Preservation under the new judgment"
204+
preservation-design-§4-7-status = "L1 closure status (2026-05-27)"
205+
preservation-design-§4-8-soundness-finding = "T_Lam_L1 + T_Var_*_L1 are too permissive — soundness gap surfaced by L1.E"
206+
preservation-design-§12-15-bounds = "Proof-debt bounds (named cases that remain)"
207+
preservation-design-§12-16-roadmap = "v2 echo-as-foundation forward look"
208+
209+
# ============================================================================
210+
# BUILD VERIFICATION
211+
# ============================================================================
212+
213+
[build]
214+
coq-version = "8.18.0"
215+
project-file = "formal/_CoqProject"
216+
invocation = "coq_makefile -f _CoqProject -o Makefile && make"
217+
last-clean-build = "2026-05-27"
218+
modules = [
219+
"Syntax",
220+
"Typing",
221+
"TypingL1",
222+
"Semantics",
223+
"Semantics_L1",
224+
"Counterexample"
225+
]

0 commit comments

Comments
 (0)