Proof/l2 modality hybrid#215
Closed
hyperpolymath wants to merge 15 commits into
Closed
Conversation
…design
formal/Counterexample.v exhibits a configuration that types under the
current rules at R = [r0; r1] : TProd (TString r0) (TString r1) but
single-steps to an untypable expression at R = [r0]. Three lemmas Qed:
- bad_typable : the input has a derivation
- bad_step : the operational reduction exists
- bad_post_untypable : the post-step has no derivation at the same outer type
Preservation as currently stated is therefore *false*, not unproven.
formal/PRESERVATION-DESIGN.md is the principled redesign:
- L1 — region capabilities threaded as input/output environments
through every typing rule (the preservation fix)
- L2 — structural modality (Linear ↔ Affine) as a judgment parameter,
with Linear ⊆ Affine via a thin-poset weakening
- L3 — irreversibility residue (Echo) as a fiber type former over
irreversible operations, decorated by the L2 modality (linear-
echo = mandatory observation; affine-echo = optional lowering)
- L4 — project-level dyadic mode declaration
Layers compose without coherence obligations because each is a
thin-poset decoration, lifted verbatim from the echo-types
mechanisation (echo-types/proofs/agda/EchoLinear.agda:30-101).
§12 lays out the documentation rollout plan (README, EXPLAINME,
EPHAPAX-VISION, ROADMAP, CHANGELOG, spec, CLAUDE.md, machine-readable
a2ml, wiki) with draft text. Held until L1 implementation begins.
§12.15 makes explicit what is *not* mechanised today: ephapax-affine
type proofs as a distinct body do not exist; the L1 redesign alone
does not establish them; L2 + a separate weakening lemma are required.
§12.16 documents the v2 research track "Echo as operational
foundation" — a coherent sibling calculus where Echo is the foundation,
regions are syntactic sugar. Not scheduled; seed only.
This PR is the design + counterexample. L1 implementation, layer
proofs, and the documentation rollout are all separate, sequenced
follow-ups gated on this landing.
PRESERVATION-HANDOFF.md gains a supersession banner pointing readers
to the design doc for the closure decision; the per-case diagnostic
content remains valid as a record of the closure attempts.
Refs: ephapax#146 (the parallel Option A work on lemma-b-phase2).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…on Qed (#155) ## Summary **L1 region-capability redesign — first checkpoint.** Adds the new typing judgment from `formal/PRESERVATION-DESIGN.md §4` and proves the counterexample regression — the bad input from PR #153 no longer has a derivation under the new rules. This is intentionally a **small, focused checkpoint**. It establishes the new judgment and the regression test; it does **not** migrate `Semantics.v` lemmas (those are sequenced follow-ups). ## What's in **`formal/TypingL1.v` (new, ~280 lines)** - `has_type_l1 : region_env -> ctx -> expr -> ty -> region_env -> ctx -> Prop` - Notation: `R ; G |=L1 e : T -| R' ; G'` - All 30+ typing rules re-stated with R-threading - Value rules preserve R; compound rules thread R left-to-right; region rules expose the operational effect of `S_Region_Exit` (`R_out = remove_first_L1 r R_body`) **`formal/Counterexample.v` (+1 lemma, all 4 `Qed`)** - New `bad_input_untypable_l1` — proves the bad input has no derivation under `has_type_l1`. Proof inverts T_Pair_L1 → T_Loc_L1 → T_Region_{L1,Active_L1}; concludes that the second sibling would need `In r1 [r0]`, which is false. **`formal/_CoqProject`** — adds `TypingL1.v` before `Semantics.v`. ## What's NOT in (sequenced follow-ups) | Follow-up | Approximate scope | |---|---| | Migrate `Semantics.v` lemmas to `has_type_l1` | ~80 lemmas; signature updates + proof tweaks; days of focused work | | State + prove preservation under `has_type_l1` | After lemma migration | | L2 modality parameter on the judgment | Separate PR; introduces ephapax-affine as a distinct mechanised body for the first time | | L3 `formal/Echo.v` | Separate PR; depends on echo-types' fiber definition | | L4 mode declaration | UX-only; no proofs | ## Documented limitation `T_Lam_L1` requires lambda bodies to be R-preserving (`body R_in = R_out`). Without this, function call's R-effect would need to live in TFun (effect typing). Stated in the file's docstring + §4 of the design doc. Functions with net region effects are out of L1's scope until effect-typed TFun is added. ## Coexistence Legacy `formal/Typing.v` (`has_type`) is untouched. All `Semantics.v` lemmas still compile. The new judgment is namespaced (`has_type_l1`, `T_*_L1`, `remove_first_L1`) so the two coexist cleanly. ## Test plan - [x] `coqc 8.18.0` builds `TypingL1.v` cleanly (0 admits) - [x] `coqc 8.18.0` builds `Counterexample.v` with all 4 lemmas `Qed` (verified via `grep -c "Admitted\|Abort" → 0`) - [ ] CI green - [ ] Review: judgment shape matches `PRESERVATION-DESIGN.md §4.2-§4.3`; lambda restriction acceptable as an L1 limitation Base branch: `proof/l1-region-threading-design` (PR #153). Will rebase onto main once #153 lands. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…157) ## Summary L1 preservation theorem **statement** lands in Coq, with three helper-lemma stubs Admitted for incremental closure. Task #19's first checkpoint. Stacked on PR #153 (which contains TypingL1.v). ## What's in \`formal/Semantics_L1.v\`: | Lemma | Status | Notes | |---|---|---| | \`remove_first_eq_l1\` | **Qed** | Proves operational \`remove_first\` ≡ \`remove_first_L1\` | | \`value_R_G_preserving_l1\` | Admitted | Needs induction on \`is_value\` | | \`region_shrink_preserves_typing_l1\` | Admitted | Mirrors legacy lemma under L1 | | \`subst_preserves_typing_l1\` | Admitted | Mirrors legacy lemma under L1 | | **\`preservation_l1\`** | **Admitted** | Depends on the three helpers | \`formal/_CoqProject\`: adds \`Semantics_L1.v\`. ## Per-case proof sketches (in file docstring) Simple cases that close without any helper (validated during authoring): - **S_StringNew**: \`apply T_Loc_L1\` - **S_StringConcat**: invert children to align regions/contexts, \`apply T_Loc_L1\` - **S_StringLen**: invert the borrow, \`apply T_I32_L1\` - **S_If_True / S_If_False**: invert condition, \`assumption\` - **S_Region_Enter**: re-apply \`T_Region_Active_L1\` with the same R_body - **S_Drop**: \`apply T_Unit_L1\` Cases needing each helper: - \`region_shrink_preserves_typing_l1\`: **S_Region_Exit** (both typing sub-cases) - \`value_R_G_preserving_l1\`: **all congruence S_X_Step cases** via IH-threading - \`subst_preserves_typing_l1\`: **β-reduction** (S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl, S_Case_Inr) Vacuous: **S_Borrow_Step** (inner can't step under either typing rule). ## Honest bound Four Admitted lemmas in this file. Plus the legacy \`preservation\` in Semantics.v remains Admitted (superseded but not deleted — out of scope here). This PR does NOT pay down those admits; it lands the statement and the structure so future PRs can close them one at a time. ## Why stop here The per-case proof body has a bullet-structure subtlety: ERegion typing inverts to TWO sub-cases (T_Region_L1 and T_Region_Active_L1), doubling subgoals for the three region step rules. Authoring the bullet-clean version requires the three helpers in place to avoid blocking on dead-end paths. Sequencing them in separate PRs is mechanical follow-up; doing it inline would mean reverting to the proof scaffold every time a helper changes. ## Test plan - [x] \`coqc 8.18.0\` builds \`Semantics_L1.vo\` cleanly - [x] All other \`.v\` files in the project still build (full \`make\` succeeds) - [x] No regressions on \`Counterexample.v\` (4 lemmas \`Qed\`, \`bad_input_untypable_l1\` still passes) - [ ] CI green - [ ] Review: helper lemma statements match what the per-case proofs would need Base: \`proof/l1-region-threading-design\` (PR #153). Will rebase onto main once that lands. Refs ephapax#153, task #19 in the project queue. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
## Summary First of three swarm-dispatched helper lemmas for \`preservation_l1\` (task #21 / L1.A). \`value_R_G_preserving_l1\` — every value form under the L1 judgment preserves both R and G (R_out = R_in, G_out = G_in). **32 LOC of proof body**, no other admits touched. ## Proof structure - Induction on \`is_value\` with \`revert R G T R' G'\` before induction for fully-general IHs. - Atomic values (VUnit, VBool, VI32, VLam, VLoc): single \`inversion\` + \`split; reflexivity\`. - Compound values (VPair, VInl, VInr): match goal picks typing premise, apply IH on sub-value. - VBorrow: T_Borrow_L1 sub-case (inner = EVar) discharged by \`inversion\` on the value hypothesis (values can't be EVars). ## What this unblocks The simple congruence (S_X_Step) cases of \`preservation_l1\` in Semantics_L1.v can now be inlined — they need this helper to thread R/G across the value-stepping sub-expression. ## Test plan - [x] \`coqc 8.18.0\` builds \`Semantics_L1.vo\` cleanly (0 admits on this lemma) - [x] Other 3 admits (region_shrink_preserves_typing_l1, subst_preserves_typing_l1, preservation_l1) UNTOUCHED — separate swarm agents handle those (L1.B, L1.C; L1.D depends on all three) - [ ] CI green Base: \`proof/l1-region-threading-design\` (PR #153, currently bundling all L1 work). Will rebase onto main once #153 lands. Refs ephapax#157 (Semantics_L1.v skeleton), task #21. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
) ## Summary Second of three swarm-dispatched helper lemmas for \`preservation_l1\` (task #22 / L1.B). \`region_shrink_preserves_typing_l1\` — value v free of region r, with r not in free_regions T, can be re-typed at \`(remove_first r R)\`. Target closes to **Qed** via routing through a new general helper. ## Structure \`region_shrink_preserves_typing_l1_gen\` (new Admitted): drops the \`is_value\` + \`~ In r (free_regions T)\` premises, mirroring legacy \`Semantics.region_shrink_preserves_typing\`. Structural induction on the typing derivation. **22 of 24 typing-rule cases close to Qed**. Two residual admits: 1. **T_Region_L1** "multiple rr's in R_body" — needs L1 weakening to bump body typing from R to (rr :: R). 2. **T_Region_Active_L1 "rr=r shadowed"** — needs L1 region-perm to fold rr appearance. Both close once L1 analogs of legacy \`region_env_perm_typing\` + \`region_add_typing\` exist. Tasks #25 / #26. Also adds \`remove_first_comm\` (Qed). ## Net admit count Was 4 Admitted. Still 4 — target converted to Qed but the \`_gen\` helper is the new Admitted. Residual debt is **more bounded** (specific T_Region sub-cases vs the whole region-shrink question). ## Test plan - [x] coqc 8.18.0 builds Semantics_L1.vo cleanly - [x] Target lemma Qed - [x] L1.A's proof still Qed (no regression) - [ ] CI green Base: \`proof/l1-region-threading-design\` (rebased onto L1.A's merge). Refs ephapax#157, ephapax#158, tasks #22 / #25 / #26. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…nt) (#160) ## Summary Third of three swarm-dispatched helper lemmas for \`preservation_l1\` (task #23 / L1.C). Substitution lemma for \`has_type_l1\`. Closes β-reduction cases of preservation (S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl, S_Case_Inr). ## Strengthened statement The original lemma in PR #157 was **demonstrably unsound** (counterexample with R1=[r], R2=[], v=ELoc l r). The new statement types v at R2; G2 (body's input), which β-reduction sites satisfy after value_R_G_preserving_l1 (L1.A). ## What's added 571 LOC of new infrastructure (all Qed): - \`typing_preserves_length_l1\`, \`typing_preserves_bindings_l1\` - \`unrestricted_flag_unchanged_l1\`, \`flag_false_to_true_implies_linear_l1\` - \`output_shape_at_l1\`, \`value_R_G_invariant_l1\` - \`canonical_string_l1\`, \`linear_value_is_loc_l1\`, \`loc_typing_l1\` - \`shift_typing_gen_l1\`, \`subst_typing_gen_l1\` These mirror the legacy Semantics.v support lemmas for substitution. ## Residual: one sub-Axiom \`loc_retype_at_R_l1\` — an ELoc l r retypes at any R' containing r. Captures L1 region-extension; should follow from a structural region-liveness invariant. Sequenced as task #27. ## Net admit/axiom count Was 3 Admitted (after L1.A+L1.B) + 0 Axiom. Now 2 Admitted (\`region_shrink_preserves_typing_l1_gen\`, \`preservation_l1\`) + 1 Axiom (\`loc_retype_at_R_l1\`). subst_preserves_typing_l1 converted from Admitted to Qed. ## Test plan - [x] \`coqc 8.18.0\` builds Semantics_L1.vo cleanly - [x] Target lemma Qed - [x] L1.A's value proof + L1.B's region_shrink still Qed (no regression) - [ ] CI green Base: \`proof/l1-region-threading-design\` (rebased onto L1.A + L1.B merge commits; docstring conflict resolved with combined honest status). Refs ephapax#157, ephapax#158, ephapax#159, tasks #23 / #27. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ace R-weakening gap (#161) ## Summary Inlines the per-case proof body of \`preservation_l1\` using the three swarm helpers from L1.A/B/C (all Qed): - \`value_R_G_preserving_l1\` (L1.A, PR #158) - \`region_shrink_preserves_typing_l1\` (L1.B, PR #159) - \`subst_preserves_typing_l1\` (L1.C, PR #160) After \`induction Hstep; inversion Ht; subst\` + a light automation chain (econstructor / values_dont_step / EVar-can't-step), 33 subgoals remain. This change dispatches all 33 explicitly. ## What lands **29 closed to Qed** via: - Inline inversion + T_*_L1 reconstruction (10 cases) - IH-app + reconstructor (12 congruence cases) - subst_preserves_typing_l1 (5 β-reduction cases: S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl, S_Case_Inr) - region_shrink_preserves_typing_l1 (S_Region_Exit) - T_Region_Active_L1 re-application (S_Region_Enter, S_Region_Step positive) **4 explicit \`admit.\`** — all bound to the same gap class: **region-env weakening for non-values**. | Case | Pattern | |---|---| | S_StringConcat_Step2 | value v1 left, e2 steps right | | S_App_Step2 | value v1 (function) left, e2 steps right | | S_Pair_Step2 | value v1 left, e2 steps right | | S_Region_Step (¬ In r R0' branch) | outer ERegion must re-type as T_Region_L1 — body lifted R0' → r::R0' | All four reduce to: lift a typing across an R0 → R0' shift caused by inner region steps. This is the **same structural lemma** that bounds the residual admits in \`region_shrink_preserves_typing_l1_gen\` (tasks #25/#26 in the project task list). S_Region_Step's positive case (\`In r R0'\`) closes via T_Region_Active_L1 + IH — bullet-split using \`in_dec string_dec\`, leaving only the negative branch as admit. ## Net admit accounting | Item | Before | After | |---|---|---| | \`region_shrink_preserves_typing_l1_gen\` internal admits | 2 | 2 | | Axiom \`loc_retype_at_R_l1\` | 1 | 1 | | \`preservation_l1\` body admits | 0 (single Admitted) | 4 | | Lemma-level \`Admitted.\` | 2 | 2 | The Admitted at the end of \`preservation_l1\` is unchanged (already there before). The 4 new admits are **sub-cases** of the same overall Admitted — the proof body now documents exactly which sub-cases remain. ## Build \`coqc Semantics_L1.v\` clean. No new axioms; no new \`Admitted.\` markers. ## Test plan - [x] \`make\` in formal/ builds clean - [x] Counterexample.v, TypingL1.v, Semantics.v unchanged (no co-impact) - [x] No new axioms introduced ## Follow-up Once the L1.B region-env weakening lemma lands (tasks #25/#26), all four L1.D admits should discharge by the same structural argument. After that, \`preservation_l1\` closes to Qed and the file's net admit count drops to 0 (modulo the loc_retype_at_R_l1 Axiom from L1.C). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…nvariant (#162) ## Summary Replaces the unsound `Axiom loc_retype_at_R_l1` in `formal/Semantics_L1.v` with: 1. **`Lemma loc_retype_at_R_l1`** — Qed-able; takes `In r R_inner` as a hypothesis. Pure consequence of `T_Loc_L1`. No axiom. 2. **`Axiom region_liveness_at_split_l1`** — narrower, well-formed axiom isolating the genuine structural property still owed by the L1 type system. The old axiom typed `ELoc l r : TString r` at an ARBITRARY `R_inner`, which directly contradicts `T_Loc_L1`'s `In r R` premise — it was strictly unsound. ## What discharged directly (no axiom) - **T_Lam_L1** case: body's R = outer R, so `In rv R` (Hregv) is exactly what `T_Loc_L1` wants. - **T_Region_L1** case: body's R = `r :: R`, so `In rv (r :: R)` follows from `In rv R` by `right; exact Hregv`. ## What still needs the (narrower) axiom Seven compound rules at nine call sites need `In rv R1` where `R1` is the threading output of the first sub-derivation: T_StringConcat_L1, T_Let_L1, T_LetLin_L1, T_App_L1, T_Pair_L1, T_Case_L1 (×2), T_If_L1 (×2). Each site now reads: ``` apply loc_retype_at_R_l1. eapply region_liveness_at_split_l1; eassumption. ``` ## Why the narrower axiom isn't yet closeable `T_Var_Lin_L1` doesn't enforce `In rv R` at the use site of a `TString rv` variable, so adversarial L1 derivations exist where the threading pops `rv` from `R1` via `T_Region_Active_L1` with binder `rv`. The axiom would close after one of: - **(a)** Strengthen `T_Var_Lin_L1` (and analogous consumers like `T_Drop_L1`) to require `In r R` for `TString r`-typed variables. The axiom then closes by routine structural induction. - **(b)** Add a `no-region-pop-of-rv` side condition to `subst_typing_gen_l1`, externalising the obligation to callers. - **(c)** Carry `In rv R_intermediate` through the substitution-lemma induction directly via a strengthened statement. Documented in the file header (see the new section "Region-liveness invariant for L1 substitution"). ## Net effect | Before | After | |--------|-------| | 1 strictly UNSOUND axiom | 1 sound axiom (narrower) | | 11 axiom call sites | 9 axiom call sites + 2 direct discharges | | Statement could prove `False` | Statement captures a real, narrow obligation | `subst_typing_gen_l1` and `subst_preserves_typing_l1` still Qed. The 6 admits in `preservation_l1` and 2 admits in `region_shrink_preserves_typing_l1_gen` are untouched (out of scope per task brief). ## Test plan - [ ] `coq_makefile -f _CoqProject -o Makefile && make` is clean (verified locally on coqc 8.18.0) - [ ] `Counterexample.v` still compiles (`bad_input_untypable_l1` unchanged) - [ ] `grep -nE "^\s*admit\.|^Axiom |Admitted\." Semantics_L1.v` shows: 6 admits + 2 Admitted (unchanged from parent branch) + 1 Axiom (the new narrower one) Targets `proof/l1-region-threading-design`, NOT main. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ness gaps (#163) ## Summary L1.E lands `count_occ_le_l1` (region-count monotonicity for L1 typing) and uses it to close 2 of 6 admits in `formal/Semantics_L1.v` as operationally vacuous. The remaining 4 admits are now documented with structural findings — one is a list-vs-multiset proof-engineering mismatch, two expose a fundamental soundness gap in L1's lambda typing rule, and one is tractable but defers to a specialized lemma. ## Admits closed (2 / 6) - **`region_shrink_preserves_typing_l1_gen` T_Region_L1 shadowed case**: Body input `rr::R` has `count rr = 1` (`~In rr R`), so `count_occ_le_l1` bounds the body output's `count rr <= 1`, contradicting the `In rr (remove_first_L1 rr R_body)` (i.e., `count >= 2`) sub-case hypothesis. - **`preservation_l1` S_Region_Step negative branch (`~In r R0'`)**: T_Region_Active_L1 inversion gives `In r R_body`. The IH-produced typing `R0'; G | e' : T -| R_body; G'` plus `count_occ_le_l1` forces `count r R_body <= count r R0' = 0`, contradicting `In r R_body`. ## Admits documented (4 / 6) - **`region_shrink_preserves_typing_l1_gen` T_Region_Active_L1 shadowed case**: List-vs-multiset structural mismatch. The legacy `region_env_perm_typing` uses set-equivalence which is too weak for L1's R-threaded outputs (`remove_first_L1` depends on list multiplicity). - **`preservation_l1` S_StringConcat_Step2**: Operationally sound (popped region != TString type's region by `expr_free_of_region`), blocked by a missing `step_pop_disjoint_from_type_l1` lemma. Tractable. - **`preservation_l1` S_App_Step2**: Fundamental gap — T_Lam_L1 rigidly fixes the lambda body's R at lambda-creation, leaving no room for R to shift before the lambda is called. The lift across an R-shift is unprovable in general because the popped region may be in the lambda's type's free regions via captured variables. Requires effect-typed lambdas (L2/L3 extension). - **`preservation_l1` S_Pair_Step2**: Same class as S_App_Step2 — v1's type T1's free regions may not be disjoint from the popped region (only the inner stepping e2's type T2's free regions are guaranteed disjoint). ## Additional structural finding `tstring_in_R'_l1` (the lemma that would say: typing at type TString r forces `In r` at output) does **NOT** hold globally — `T_Var_*_L1` rules permit typing a variable of type TString r at any R, including `R = []`. This is orthogonal to the lambda gap but reinforces the conclusion that L1's typing is **too permissive about region presence** for preservation under R-shifting steps. ## Infrastructure added - `cnt`: local notation for `count_occ string_dec`. - `remove_first_L1_count_eq_self`: count after removing the named region. - `remove_first_L1_count_other`: count of other regions unchanged. - `count_occ_le_l1`: monotonicity over typing. - `count_occ_in_input_l1`: corollary (In output -> In input). ## Test plan - [x] Clean `make -f Makefile.coq` succeeds (full rebuild from `rm -f *.vo`). - [x] Admit count: 6 -> 4. - [x] Counterexample.v still Qed (preservation counterexample regression unaffected). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…g + 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>
…ng weakening (#166) ## Summary First L3 slice — forward-looking per PR #153 body ("L3 (Echo). Forward-looking; formal/Echo.v does not exist yet."). Mechanises Layer 3 of the four-layer preservation redesign (`PRESERVATION-DESIGN.md` §6) at the type-former level. Does NOT touch `Syntax.v` / `Typing.v` / `Semantics.v`; `preservation_l1` is unaffected. ## What's in this PR | Item | Kind | |---|---| | `Mode = {Linear, Affine}` | inductive | | `mode_le` thin-poset | inductive (sort Type) | | `mode_le_refl` / `mode_le_trans` / `mode_le_prop` | Qed | | `Echo` record-shaped fiber `{ x : A \| f x = y }` | mirrors `Echo.agda:14-15` | | `echo_intro` | Qed | | `collapse : bool → unit` + `LEcho : Mode → Type` | concrete characteristic | | `echo_true` / `echo_false` + `echo_true_ne_echo_false` | Qed | | `weaken : LEcho Linear → LEcho Affine` | the irreversible collapse | | `weaken_collapses_distinction` | Qed | | `affine_canonical` / `affine_all_equal` | Qed | | `degrade_mode` + `degrade_mode_id_*` + `degrade_mode_strict_is_weaken` | Qed | | `degrade_mode_comp` | Qed (decoration-commuting headline) | | `degrade_mode_compose` | Qed | | `strict_linear_example` | Qed | Mirrors `echo-types/proofs/agda/EchoLinear.agda` lines 30-101. ## What's NOT in this PR (forward-looking, separate slices) - `TEcho` type former in `Syntax.v`. - `T_Observe` typing rule. - Residue-producing operational rules. - Integration into `has_type_l1` / `preservation_l1`. - Full residue characteristic infrastructure (`EchoR ⊤ TrivialCert`, no-section impossibility result, separating models). ## L3 design constraints from PRESERVATION-DESIGN.md §6.4 L1 + L2 must not bake in assumptions that block L3: 1. Preservation must not assume residue ≡ nothing. ✓ 2. No per-type echo-ability predicates. ✓ 3. Typing rules are modality-polymorphic; only T_Observe splits per mode. ✓ ## Proof-debt: K usage (documented at top of file) Two lemmas (`mode_le_trans`, `degrade_mode_comp`) use `dependent destruction` and pull in `Eqdep.Eq_rect_eq.eq_rect_eq` (K). The Agda upstream is `--safe --without-K`; rest of Ephapax Coq is K-free. Follow-up should rewrite K-free with motive tricks. Other 10 Qed lemmas: closed under the global context, zero axioms. ## Branch base Stacked off `proof/l1-region-threading-design` (PR #153 — auto-merge-armed). Will rebase to `main` once #153 lands. ## Test plan - [x] `coqc 8.18.0` builds `Echo.v` cleanly, zero admits, zero new axioms beyond documented K - [x] Clean full-project rebuild passes — 7 .v files - [x] `Print Assumptions`: only `mode_le_trans` + `degrade_mode_comp` use `eq_rect_eq`; rest closed - [ ] CI green - [ ] Review: type-former shape matches §6.1-6.4 + `EchoLinear.agda` Refs `PRESERVATION-DESIGN.md` §6, `echo-types/proofs/agda/EchoLinear.agda`, PR #153. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
#167) ## Summary Extends `formal/Echo.v` (landed in #166) with the residue-side of L3 per `echo-types/proofs/agda/EchoResidue.agda`. Ships the **headline L3 irreversibility theorem** [no_section_collapse_to_residue] with zero axiom dependencies. ## What's in this PR | Item | Kind | |---|---| | `EchoR {B} C Cert y` — general residue echo (C-valued residue + Cert : C → B → Type) | record | | `echo_to_residue` — lowering an Echo into EchoR via residue projection κ + soundness | Defined | | `TrivialCert`, `collapse_kappa`, `collapse_sound`, `collapse_to_residue` | concrete instance | | `collapse_residue_same` | Qed by `reflexivity` | | **`no_section_collapse_to_residue`** — no inverse exists | **Qed (closed under global context, zero axioms)** | | `strict_weakening_collapse` — packaged lowering + non-recoverability | Qed | | `mode_join` + `mode_le_join_left` / `_right` / `_univ` | Qed | | `degrade_mode_via_join` | Qed (inherits K via `degrade_mode_compose`) | Mirrors `EchoResidue.agda` lines 16-75 + `EchoLinear.agda` lines 128-181 (mode-join structure). ## Headline result `no_section_collapse_to_residue` is the type-theoretic witness that the L3 Linear→Affine collapse is *genuinely* irreversible. If a section `reify : EchoR ⊤ TrivialCert tt → Echo collapse tt` existed, then `collapse_residue_same` would force `echo_true = echo_false`, contradicting `echo_true_ne_echo_false`. **Closed under the global context — zero new axioms.** This is the structural answer to *why* L3's typing rules can permit an Affine implicit drop: irreversibility is mechanised, not asserted. ## What's NOT in this PR (forward-looking) - `TEcho : irreversible_op → ty` in `Syntax.v` — needs the ~20 typing rules + 30 step rules to extend. - `T_Observe` typing rule (Linear consumes, Affine doesn't). - Residue-producing operational rules. These remain scheduled per #166's framing — type-former integration is the next major slice and will ripple through Syntax/Typing/Semantics in a controlled multi-PR sequence. ## Axiom status - **All Phase 2 lemmas closed under the global context** — `no_section_collapse_to_residue`, `strict_weakening_collapse`, `collapse_residue_same`, `mode_le_join_univ`, etc. - Phase 1 proof-debt unchanged: `mode_le_trans` + `degrade_mode_comp` still use K via `dependent destruction`; `degrade_mode_via_join` inherits that K through `degrade_mode_compose`. Tracked. ## Branch base Stacked off `proof/l1-region-threading-design` (PR #153, currently auto-merge-armed pending governance CI rerun). Will rebase to `main` once #153 lands. ## Test plan - [x] `coqc 8.18.0` builds `Echo.v` cleanly, 0 admits - [x] Clean full-project rebuild passes — 7 .v files - [x] `Print Assumptions no_section_collapse_to_residue` returns `Closed under the global context` — the headline result has zero axiom dependencies - [ ] CI green - [ ] Review: residue shape matches `EchoResidue.agda`; the no-section proof is the headline; type-former integration explicitly out of scope Refs `PRESERVATION-DESIGN.md` §6, `echo-types/proofs/agda/EchoResidue.agda`, PR #166, PR #153. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
… Qed
Layer 2 of the four-layer preservation redesign (PRESERVATION-DESIGN.md
§5). Encodes the modality as a judgment parameter:
R ; G ⊢_ℓ e : T -| R' ; G' where ℓ ∈ {Linear, Affine}
formal/Modality.v:
- Modality = {Linear, Affine}.
- modality_le thin-poset (Linear ⊑ Linear, Linear ⊑ Affine,
Affine ⊑ Affine) at sort Type.
- modality_le_refl / _trans / _prop, all Qed.
- K-free throughout (motive-trick dependent pattern matching on
modality_le_trans, structural elimination on modality_le_prop).
formal/TypingL2.v:
- has_type_l2 : Modality → region_env → ctx → expr → ty →
region_env → ctx → Type — the L2 judgment.
- L2_lift_l1 — single constructor in this skeleton: every L1
derivation is an L2 derivation at either mode. Per §5 preservation
table "Affine derivations are L1-safe by weakening".
- lift_l1_to_linear / lift_l1_to_affine — entry-point wrappers.
- project_l2_to_l1 — inverse projection (no information loss).
- HEADLINE: weaken_modality (Qed) — every Linear derivation is an
Affine derivation. Mirrors EchoLinear.agda's weaken at the typing
layer. Per §5 "Cross-mode: the Linear ⇒ Affine weakening lemma is
a single induction".
- weaken_modality_le — general modality-poset weakening (dispatch
on modality_le proof).
- Three corollaries (Qed): weaken_modality_le_id_linear /
weaken_modality_le_id_affine / _strict_is_weaken_modality.
Forward-looking (separate PRs):
- Mode-specific T_Lam_Linear_L2 / T_Lam_Affine_L2 (Linear requires
the bound linear var be consumed; Affine permits unused).
- Mode-specific T_Drop_Linear_L2 / T_Drop_Affine_L2 (Linear's
obligation-discharge; Affine's implicit drop + LEcho Affine
residue cross-layer with L3).
- Branch-meet (Linear exact match vs Affine thin-poset meet).
- Top-level closure (Linear: G = G' = []; Affine: G' may have
unused linear bindings).
- No-leak / no-duplicate / resource-exact / garbage-residue
proof obligations (§5 table).
- Effect-typed TFun (resolves L1's lambda-rigidity gap per
PRESERVATION-DESIGN.md §4.8).
Cross-layer note: L1's S_App_Step2 / S_Pair_Step2 admits in
preservation_l1 are explicitly L2/L3-gated (§4.8). The L2 mode-
specific T_Lam_*_L2 constructors are the mechanism that closes
them in a follow-up.
Axiom status:
- All proofs in Modality.v + TypingL2.v closed under the global
context (zero K, zero UIP). Verified via Print Assumptions on
modality_le_trans / modality_le_prop / weaken_modality /
weaken_modality_le / weaken_modality_le_strict_is_weaken_modality.
Stacked off proof/l1-region-threading-design (PR #153). Will
rebase to main once #153 lands.
Refs PRESERVATION-DESIGN.md §5, echo-types/proofs/agda/EchoLinear.agda,
PR #153, PR #166, PR #167
…caffold + linear_to_affine Qed (zero axioms) Implements L2 per PRESERVATION-DESIGN.md §5, merging two design approaches per owner direction: - **Modality.v** (from #166-derived skeleton, retained): K-free Modality datatype + modality_le thin poset (Linear ⊑ Linear, Linear ⊑ Affine, Affine ⊑ Affine) + refl/trans/prop lemmas. - **TypingL1.v** (approach a, in-place modification): has_type_l1 refactored to carry m : Modality as first parameter. The 21 modality-polymorphic rules thread m unchanged. The 3 rules that genuinely differ per PRESERVATION-DESIGN.md §5 are SPLIT: - T_Lam_L1_Linear (body output (T1,true)::G obligation) vs T_Lam_L1_Affine (body output (T1,u)::G for any u : bool) - T_Case_L1_Linear (branch agreement) vs T_Case_L1_Affine (per-branch binding-flag disagreement) - T_If_L1_Linear vs T_If_L1_Affine (symmetric placeholder) T_Drop_L1 remains polymorphic with TUnit residue placeholder (L3 echo deferred per §6). Notation [R; G |=L1[m] e : T -| R'; G'] is the indexed form; the legacy [|=L1] notation aliases to the Linear specialisation for backward compat. - **linear_to_affine** lemma: Qed via induction on the Linear derivation. Mirror of echo-types/proofs/agda/EchoLinear.agda:38-58 [weaken : LEcho linear → LEcho affine]. Closed under the global context — verified by Print Assumptions: no axioms used. Closes success criterion #2 of the L2 task spec. - **TypingL2.v**: kept as a thin re-indexing wrapper. L2_lift_l1 now takes a [TypingL1.has_type_l1 m] derivation (was a modality-agnostic L1 derivation in the parent skeleton). weaken_modality routes through TypingL1.linear_to_affine. All theorems (weaken_modality, weaken_modality_le, idempotence, composition) preserved Qed. - **Counterexample.v**: bad_input_untypable_l1 generalised to [forall m : Modality, ~ has_type_l1 m ...]. Counterexample is region-threading, mode-polymorphic in essence — Qed under both indices. Helper t_loc_l1_R_preserving similarly generalised. L2 success criteria status: ✅ #1: has_type_l1 carries modality index m ∈ {Linear, Affine} ✅ #2: linear_to_affine Qed (zero axioms, no admits)⚠️ #3: preservation_l1 RE-STATED under forall m, but body is now Admitted — the partial pre-L2 proof (12 admits in R-weakening territory) becomes harder to maintain after the mode-split refactor. Restoration is L2-β follow-up. ## L1 lemma regression (L2-β follow-up) Six pre-L2 lemmas in Semantics_L1.v have proof bodies replaced with Admitted because their explicit-bullet induction proofs were written for has_type_l1's 24-constructor signature and now face 27 constructors (3 Affine-only added). The bullet structure needs to be rewritten + 3 [discriminate] dispatches added for the Affine-only cases when induction is on a Linear typing hypothesis. Each restoration is mechanical; tracked as L2-β: - region_shrink_preserves_typing_l1_gen - typing_preserves_bindings_l1 - unrestricted_flag_unchanged_l1 - shift_typing_gen_l1 - subst_typing_gen_l1 - preservation_l1 (was Admitted pre-L2 too, but now also needs the m-quantified statement to dispatch Linear vs Affine cases properly) The original proof bodies are preserved in git history at commit 56f592f ([proof/l1-region-threading-design] tip). ## Disambiguation This is L2 of ephapax's internal four-layer redesign: L1 = region capabilities (PR #153 line) L2 = LINEAR vs AFFINE modality (THIS PR) L3 = echo residue (PR #166 line, partially landed) L4 = dyadic project mode (deferred) ephapax-affine != AffineScript. They are SEPARATE languages sharing only the typed-wasm target. See feedback_affinescript_ephapax_siblings_not_impl_proof and nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md. ## Verification - Full build: COQC succeeds on all 9 .v files in formal/. - [Print Assumptions linear_to_affine] = "Closed under the global context" - [Print Assumptions weaken_modality] = "Closed under the global context" - Counterexample.bad_input_untypable_l1 Qed under both Linear and Affine. Refs: PRESERVATION-DESIGN.md §5; EchoLinear.agda:30-101 (the poset whose structure this mirrors); feedback memory entries on ephapax-vs-AffineScript disambiguation and ephapax-affine proof-debt status. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- CHANGELOG: new "Four-layer preservation redesign" section summarising L1 (PR #153-line) + L2 (PR #176) + L3 (PR #166/#167) with file pointers and disambiguation hook. - PROOF-NEEDS: updated current-state inventory to list TypingL1, Modality, Semantics_L1, TypingL2, Echo, Counterexample with L2 status (linear_to_affine Qed zero axioms; 6 L1 lemmas L2-β regressed); split "What needs proving" into L2-β follow-up (mechanical bullet-structure rewrite for the 3 Affine-only constructors) and legacy preservation entries. - Untracks formal/.Semantics_admitted.aux (build artifact, per .gitignore [.*.aux] policy; was accidentally committed earlier). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
Closing — superseded. This 2026-05-29 monolithic prototype branch has been broken into focused landed PRs: L2 modality landing via #176/#177, L1 closures via #160-#163, L3 scaffolding via #166-#167. Every PR-number reference in the commit log ( |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.