proof(Semantics_L1): close 3 Affine-only bullet-structure regressions by hyperpolymath · Pull Request #187 · hyperpolymath/ephapax

hyperpolymath · 2026-05-27T16:23:00Z

Summary

L2-β follow-up landing. The L2-hybrid in #176 + #177 added three Affine-only constructors (T_Lam_L1_Affine, T_Case_L1_Affine, T_If_L1_Affine) which regressed 6 supporting lemmas in formal/Semantics_L1.v to Admitted. This PR closes the 3 pure bullet-structure regressions and generalises typing_preserves_length_l1 to modality-polymorphic.

Net delta: 15 Qed + 7 Admitted → 19 Qed + 4 Admitted in Semantics_L1.v.

Closed lemmas

typing_preserves_bindings_l1 — output-ctx lookup preserved under typing. Restored from commit 56f592f with 2 new bullets for T_Case_L1_Affine + T_If_L1_Affine (T_Lam_L1_Affine auto-discharges via R/G-unchanged path).
unrestricted_flag_unchanged_l1 — non-linear bindings stable through typing. Same 3-new-bullet pattern.
shift_typing_gen_l1 — extracted m-polymorphic shift_typing_gen_l1_m (mirrors region_liveness_at_split_l1_gen's shape); Linear-only shift_typing_gen_l1 retained as thin wrapper.

Generalised

typing_preserves_length_l1 now stated over forall m. All 12 call sites in this file updated; Linear-only callers continue to work via instantiation.

Residual admits (L2-β follow-up #2)

subst_typing_gen_l1 — goal mentions modality, needs m-polymorphic generalisation. Pure bullet-restoration insufficient; documented in lemma comment.
region_shrink_preserves_typing_l1_gen — list-vs-multiset bridge for T_Region_Active_L1 shadowed case (pre-L2 issue, not new debt).
region_liveness_at_split_l1_gen — 1 narrow admit (genuinely false per documented ERegion rv (EI32 5) counterexample).
preservation_l1 — capstone, depends on subst_typing_gen_l1.

Owner-directive compliance

Per CLAUDE.md 2026-05-27:

No new `Axiom` declarations.
No ad-hoc side conditions on compound rules.
No legacy `Theorem preservation` patching (untouched).
Per-layer derivation against explicit invariants (L1 supporting infrastructure).

Test plan

`just clean && just all` in `formal/` — full project rebuild clean
`grep "^Admitted." Semantics_L1.v` confirms exactly 4 residual admits (down from 7)
`coqc 8.18.0` accepts every restored proof
CI Coq proofs job passes

Refs `PROOF-NEEDS.md` §2 "Near-term (L1 ⇒ L2 integration debt)".

🤖 Generated with Claude Code

L2-β follow-up landing. The L2-hybrid in PRs #176+#177 added three Affine-only constructors (T_Lam_L1_Affine, T_Case_L1_Affine, T_If_L1_Affine) which regressed 6 supporting lemmas in Semantics_L1.v to Admitted. This PR closes the 3 pure bullet-structure regressions and generalises typing_preserves_length_l1 to modality-polymorphic. Net file delta: 15 Qed + 7 Admitted → 19 Qed + 4 Admitted. Closed lemmas: - typing_preserves_bindings_l1 — output-ctx lookup preserved under typing. Restored from commit 56f592f with 2 new bullets for T_Case_L1_Affine + T_If_L1_Affine (T_Lam_L1_Affine auto-discharges via R/G-unchanged path). - unrestricted_flag_unchanged_l1 — non-linear bindings stable through typing. Same 3-new-bullet pattern. - shift_typing_gen_l1 — extracted m-polymorphic shift_typing_gen_l1_m (mirrors region_liveness_at_split_l1_gen's shape); Linear-only shift_typing_gen_l1 retained as thin wrapper for existing callers. Generalised: typing_preserves_length_l1 now stated over forall m; all 12 call sites in this file updated. Linear-only callers continue to work via instantiation. Residual admits (L2-β follow-up #2): - subst_typing_gen_l1 (line ~961): goal mentions modality, needs m-polymorphic generalisation. Pure bullet-restoration is insufficient; cleanly tracked in the lemma comment. - region_shrink_preserves_typing_l1_gen: list-vs-multiset structural bridge for T_Region_Active_L1 shadowed case (pre-L2 issue). - region_liveness_at_split_l1_gen: 1 narrow admit (genuinely false per documented ERegion rv (EI32 5) counterexample). - preservation_l1: capstone, depends on subst_typing_gen_l1. PROOF-NEEDS.md §1, §2, §4 updated to reflect new counts. Semantics_L1.v file-header banner updated 9→4 admits. Refs PROOF-NEEDS.md §2 "Near-term (L1 ⇒ L2 integration debt)". Per CLAUDE.md owner directive 2026-05-27: no new Axioms, no ad-hoc side conditions, no legacy preservation patching. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ralisation (L2-β #2) (#188) ## Summary Closes `subst_typing_gen_l1` (the substitution lemma) by m-polymorphic generalisation, mirroring the `shift_typing_gen_l1_m` pattern landed in #187. Net debt in `formal/Semantics_L1.v`: **19 Qed + 4 Admitted → 25 Qed + 3 Admitted**. ## What changed - New `subst_typing_gen_l1_m` (m-polymorphic, 29 explicit bullets covering all L1 constructors). - `subst_typing_gen_l1` becomes a Linear wrapper around `_m`. - `typing_preserves_bindings_l1` and `output_shape_at_l1` generalised to modality-polymorphic (mechanical signature change; body unchanged — only used by `subst_typing_gen_l1` internally, no other estate callers). - New `loc_retype_at_R_l1_m` (m-polymorphic sibling of the existing Linear wrapper) so the substituted-value retyping at compound-rule split points works at the active modality `m`. - Internal calls switched to `region_liveness_at_split_l1_gen` (m-polymorphic) instead of the Linear wrapper. ## Why this shape The substituted-value premise `Hv_type` stays at Linear — callers (`subst_preserves_typing_l1`, `preservation_l1`) always have a Linear v-typing. Inside the m-polymorphic body it is unpacked via `linear_value_is_loc_l1` and reconstructed at the active `m` via `loc_retype_at_R_l1_m`. Mode-split rules — T_Lam_L1_{Linear,Affine}, T_Case_L1_{Linear,Affine}, T_If_L1_{Linear,Affine} — each get their own bullet. Affine cases mirror Linear because substitution threading is modality-independent (the Affine rules differ only in permitted output flags, which are quantified inside each rule and transparent to the IH). ## Residual admits in `Semantics_L1.v` (3, down from 4) 1. `region_shrink_preserves_typing_l1_gen` — list-vs-multiset structural mismatch in T_Region_Active_L1 shadowed case. 2. `region_liveness_at_split_l1_gen` — 1 narrow admit in T_Region_Active_L1 `[r = rv]` sub-case (genuinely false per documented counterexample `ERegion rv (EI32 5)`). 3. `preservation_l1` — capstone; depends on closing (1)+(2) under L2 dispatch + lambda-rigidity gap resolution. ## Doctrine compliance (CLAUDE.md 2026-05-27) - ✅ No new \`Axiom\` declarations. - ✅ No ad-hoc side conditions on compound rules. - ✅ No strengthened lemma signatures dodging the L2 dispatch — the generalisation moves \`m\` *into* the signature, exposing the modality dispatch, not hiding it. - ✅ Legacy \`formal/Semantics.v\` and \`formal/Typing.v\` untouched. ## Test plan - [x] \`coqc\` clean build via \`cd formal && just clean && just all\` (Coq 8.18.0). - [x] \`grep -c "Admitted\.$" Semantics_L1.v\` → 3 (was 4). - [x] \`grep -c "Qed\.$" Semantics_L1.v\` → 25 (was 19). - [x] No new \`Axiom\` introduced (\`grep -c "^Axiom " formal/*.v\` unchanged). - [ ] CI passes. ## Stacking This PR is stacked on #187 (the 3 affine-only bullet-structure regressions). GitHub will auto-retarget to \`main\` when #187 squash-merges. --- 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…llet structure via m-polymorphic helper (L2-β #3) (#189) ## Summary Restores the pre-L2 proof body of `region_shrink_preserves_typing_l1_gen` as a modality-polymorphic helper `region_shrink_preserves_typing_l1_gen_m`, mirroring the pattern established by #187/#188 (`shift_typing_gen_l1_m`, `subst_typing_gen_l1_m`). The Linear wrapper `_gen` becomes a one-line derivation. Net effect: the outer `Admitted` on `_gen` is gone (now Qed via wrapper); one structural residual remains as an internal `admit` inside `_gen_m` — the genuine T_Region_Active_L1 [rr = r] shadowed sub-case (list-vs-multiset bridge), unchanged in substance from the pre-L2 baseline. ## What changed - New `count_occ_le_l1_m` (m-polymorphic count monotonicity); the existing Linear `count_occ_le_l1` becomes a 2-line wrapper. - New `region_shrink_preserves_typing_l1_gen_m` with the 29-bullet proof body adapted from commit 56f592f. Three new Affine-only constructors (T_Lam_L1_Affine, T_Case_L1_Affine, T_If_L1_Affine) close identically to their Linear siblings since region operations are mode-blind. - `region_shrink_preserves_typing_l1_gen` now derives from `_gen_m` by `apply (… Linear); auto.` — Qed. - Design-note comment above the lemma corrected: the earlier suggestion that the value-restricted wrapper could bypass `_gen_m` by inducting on `is_value` fails on the VLam case (lambda body's internal `ERegion r' e'` shadowing); wrapper still goes through `_gen_m`. ## Net debt `formal/Semantics_L1.v`: 21 Qed + 3 Admitted → **23 Qed + 3 Admitted**. The 3 Admitted: 1. `region_shrink_preserves_typing_l1_gen_m` — NEW location of the structural residual; internal `admit` in the T_Region_Active_L1 shadowed sub-case 2. `region_liveness_at_split_l1_gen` — owner-gated per CLAUDE.md doctrine; closes at L2 dispatch 3. `preservation_l1` — capstone ## Out of scope The structural residual itself — closure options listed in PROOF-NEEDS.md §2 (L2-β follow-up #4). ## Test plan - [x] `coqc` accepts the file (full Coq tree builds with no errors) - [x] `Counterexample.v` re-builds cleanly (no regression of the 5 pinned Qed lemmas) - [x] No new `Axiom` declarations - [x] No legacy `Semantics.v` / `Typing.v` edits - [x] No closure attempts on `region_liveness_at_split_l1_gen` (owner-gated) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Foundation for L3 wiring (PROOF-NEEDS.md §2). [Echo.v](formal/Echo.v) calculus (12 Qed, 0 admits) is already in place; this PR adds the surface AST needed before [T_Observe] and step-emission rules can land in subsequent slices. This is slice 1 of 4 in the L3 wiring sequence: 1. **This PR** — AST extension (TEcho + EEcho + cascades) 2. T_Observe typing rule + S_Region_Exit / S_Drop emission 3. G (echo context) threading through compound rules 4. preservation_l3 capstone ## Changes (formal/Syntax.v) - New `ty` constructor `TEcho : ty -> ty`. The type of an echo value witnessing an irreversible step that erased a value of type `T`. Documented at `PRESERVATION-DESIGN.md §6.3`. - New `expr` constructor `EEcho : ty -> expr -> expr`. Runtime-only residue value, mirroring the `ELoc` pattern (no surface syntax). - New `is_value` constructor `VEcho` so `S_Region_Exit` / `S_Drop` can reduce to a normal form. - Cascade-mechanical updates: `expr_free_of_region`, `shift`, `subst` all recurse into the witness sub-expression. The witness type annotation `T` is closed. ## Cascade fixes - `formal/Typing.v` `free_regions` gains a `TEcho T' => free_regions T'` case (linear in the witness). - `formal/Semantics_L1.v` `value_R_G_preserving_l1` gains a `VEcho` case closed by inversion (no L1 typing rule produces `EEcho` yet, so the hypothesis is vacuous in this slice). ## What is NOT in this slice (deliberately deferred per slice plan) - `T_Observe` typing rule → **slice 2** - `S_Region_Exit` / `S_Drop` echo emission in step rules → **slice 2** - `G` (echo context) threading through compound rules → **slice 3** - `preservation_l3` → **slice 4** `is_linear_ty` is deliberately not extended — `TEcho` hits the catch-all returning `false` in this slice. The linearity discipline lives in the (forthcoming) `T_Observe` rule's modality dispatch, not in `is_linear_ty`. Revisit in slice 2 if the rule shape demands it. ## Build oracle - `coqc 8.18.0` closes the full formal/ tree (Syntax / Typing / TypingL1 / Semantics / Semantics_L1 / Counterexample / TypingL2). - Net debt: unchanged on this branch (`Semantics_L1.v`: 23 Qed + 3 Admitted, all pre-existing). ## Refs - `PROOF-NEEDS.md §2` (L3 wiring) - `PRESERVATION-DESIGN.md §6` (L3 design — fiber + observation discipline) - `formal/Echo.v` (12 Qed L3 calculus this builds toward integrating) ## Test plan - [x] `coqc 8.18.0` closes full formal/ tree - [x] No new Admitted / Axiom - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ice 2) (#191) ## Summary Slice 2 of 4 in the L3 wiring sequence. [Slice 1 (#190)](../pull/190) added the `TEcho` / `EEcho` AST surface; this slice adds the explicit observation rule that consumes an echo. ## Changes (formal/Syntax.v) - New `expr` constructor `EObserve : expr -> expr`. Surface-writable (unlike `EEcho` which is runtime-only). - Cascade-mechanical: `expr_free_of_region`, `shift`, `subst` all recurse into the sub-expression. ## Changes (formal/TypingL1.v) - New typing rule: ```coq T_Observe_L1 : has_type_l1 m R G e (TEcho T) R' G' -> has_type_l1 m R G (EObserve e) (TBase TUnit) R' G' ``` Modality-polymorphic: fires in both Linear and Affine modes. What differs across modes is the **obligation shape**, not the rule: - **Linear** discipline makes the echo a must-observe (an unobserved `TEcho` in scope is a typing failure). - **Affine** permits implicit lowering (no `T_Observe` required). The mandatoriness is to be enforced via `is_linear_ty TEcho` or the implicit-drop discipline in a follow-up — the present rule is the necessary precondition. ## Cascade fixes (formal/Semantics_L1.v) - `shift_typing_gen_l1_m`: explicit `T_Observe_L1` bullet (commutes with the witness sub-expression via the IH). - `subst_typing_gen_l1_m`: explicit `T_Observe_L1` bullet (same shape). - `region_shrink_preserves_typing_l1_gen_m`: explicit `T_Observe_L1` bullet added before \`Admitted\` (closes via IH; would otherwise be silently absorbed by the outer Admitted). - All other inductions (\`typing_preserves_bindings_l1\`, \`unrestricted_flag_unchanged_l1\`, \`count_occ_le_l1_m\`, \`region_liveness_at_split_l1_gen\`) absorb \`T_Observe_L1\` via their existing catch-all patterns (T_Observe_L1 propagates the IH unchanged on G' and R' — no new structural obligation). ## What is NOT in this slice (deliberately deferred) - **\`S_Region_Exit\` / \`S_Drop\` echo emission in step rules.** The step relation lives in \`Semantics.v\` which is owner-touchy (CLAUDE.md Owner directive 2026-05-27 anti-pattern detector). Will escalate before slice 3. - \`G\` (echo context) threading through compound rules → slice 3 - \`preservation_l3\` → slice 4 - \`is_linear_ty TEcho_ = true\` (mandatoriness enforcement) → follow-up ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree. - Net debt unchanged on this branch (3 Admitted in \`Semantics_L1.v\`, all pre-existing from prior slices). ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`formal/Echo.v\` (12 Qed L3 calculus) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new Admitted / Axiom (3 Admitted unchanged from base) - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…a) (#192) ## Summary Slice 3a of the L3 wiring sequence. Slices [1 (#190)](../pull/190) and [2 (#191)](../pull/191) added the AST surface and the observation consumer; this slice closes the typing for the runtime echo VALUE form so that the forthcoming step rules (\`S_Region_Exit_Echo\`, \`S_Drop_Echo\` — slice 3b) have a type-preserving target. ## Changes (formal/TypingL1.v) New typing rule: \`\`\`coq T_Echo_L1 : forall m R G v T, is_value v -> R; G |=L1[m] v : T -| R; G -> R; G |=L1[m] EEcho T v : TEcho T -| R; G \`\`\` Modality-polymorphic. Echoes are runtime values that preserve both \`R\` and \`G\` (no resource state change at the typing layer), mirroring \`T_Borrow_Val_L1\`'s value-of-value pattern. ## Cascade fixes (formal/Semantics_L1.v) - \`value_R_G_preserving_l1\` \`VEcho\` case: was \`inversion Ht\` expecting vacuity; now inverts to \`T_Echo_L1\` which gives \`R_out = R\` and \`G_out = G\` directly. - \`shift_typing_gen_l1_m\`: explicit \`T_Echo_L1\` bullet (uses \`shift_preserves_value\` for the value premise + IH for the witness typing). - \`subst_typing_gen_l1_m\`: explicit \`T_Echo_L1\` bullet (uses \`subst_preserves_value\` + IH). - \`region_shrink_preserves_typing_l1_gen_m\`: explicit \`T_Echo_L1\` bullet before \`Admitted\` (closes via IH on the witness; the \`is_value\` premise is preserved by structure). The new constructor's insertion before \`T_Observe_L1\` in the inductive declaration shifted the bullet indices in three proofs; each now has the matching \`T_Echo_L1\` bullet. ## What is NOT in this slice (still deferred) - \`S_Region_Exit_Echo\` / \`S_Drop_Echo\` step rules in \`Semantics.v\` — **slice 3b** (parallel-rule strategy approved 2026-05-27) - \`T_Region_L1_Echo\` / \`T_Drop_L1_Echo\` (parallel typing rules matching the new step-rule output type) — slice 3b - \`G\` (echo context) threading through compound rules — slice 3c - \`preservation_l3\` — slice 4 ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree. - Net debt unchanged (3 Admitted in \`Semantics_L1.v\`, all pre-existing). ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`formal/Echo.v\` (12 Qed L3 calculus) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new Admitted / Axiom (3 Admitted unchanged) - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Slice 3b of the L3 wiring sequence. Per **owner-approved strategy 2026-05-27**: introduce PARALLEL typing rules that output \`TEcho T\` where the legacy rules output \`T\` or \`TBase TUnit\`. This pairs with the (forthcoming, slice 3c) parallel step rules \`S_Region_Exit_Echo\` and \`S_Drop_Echo\`. Programs choose at typing time which path they're on; the two paths are non-deterministic at the rule-application level. \`preservation_l3\` (slice 4) will dispatch per-rule. ## Changes (formal/TypingL1.v) — three new typing rules - \`T_Region_L1_Echo\`: mirror of \`T_Region_L1\` with echo-typed output. - \`T_Region_Active_L1_Echo\`: mirror of \`T_Region_Active_L1\`. - \`T_Drop_L1_Echo\`: mirror of \`T_Drop_L1\` (output \`TEcho T\` instead of \`TBase TUnit\`). All three modality-polymorphic; same premises as their originals. ## Cascade fixes (formal/Semantics_L1.v) — bullets in inductions - \`count_occ_le_l1_m\`: 2 explicit bullets for \`T_Region_*_L1_Echo\`. - \`shift_typing_gen_l1_m\`: 3 explicit bullets (mirror tactics). - \`subst_typing_gen_l1_m\`: 3 explicit bullets (mirror tactics). - \`region_shrink_preserves_typing_l1_gen_m\`: 3 bullets; T_Drop_L1_Echo Qed via mirror; T_Region_*_L1_Echo admit (parallel-rule mirrors of pre-existing structural admits). - \`region_liveness_at_split_l1_gen\`: 3 bullets; T_Region_L1_Echo + T_Drop_L1_Echo Qed via mirror; T_Region_Active_L1_Echo \`r = rv\` sub-case admit (mirror of the genuinely-false sub-case). ## Net debt change - **3 outer Admitted unchanged** (\`region_shrink_preserves_typing_l1_gen_m\`, \`region_liveness_at_split_l1_gen\`, \`preservation_l1\`). - **+3 INTERNAL admits**, all parallel-rule MIRRORS of pre-existing structural admits — same list-vs-multiset / counterexample obstacles. **NOT new structural debt**; they close when the originals do (cross-layer per \`PRESERVATION-DESIGN.md §5.1\`). ## What is NOT in this slice (still deferred) - \`S_Region_Exit_Echo\` / \`S_Drop_Echo\` step rules in \`Semantics.v\` — **slice 3c** - \`G\` (echo context) threading through compound rules — **slice 3d** - \`preservation_l3\` — **slice 4** ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree. ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`PRESERVATION-DESIGN.md §5.1\` (cross-layer dependency annotations) - \`formal/Echo.v\` (12 Qed L3 calculus) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new outer Admitted / Axiom (3 outer Admitted unchanged) - [x] New internal admits are parallel-rule MIRRORS of existing structural admits, documented inline - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…slice 3c) (#194) ## Summary Slice 3c of the L3 wiring sequence. **Owner-approved 2026-05-27**: PARALLEL step rules in Semantics.v that emit echo residues at irreversible boundaries. Legacy \`S_Region_Exit\` + \`S_Drop\` are **untouched** (kept for backward-compat with non-echo typing paths). The new rules pair with the typing rules added in [slice 3b (#193)](../pull/193): - \`S_Region_Exit_Echo\` + \`T_Region_L1_Echo\` / \`T_Region_Active_L1_Echo\` - \`S_Drop_Echo\` + \`T_Drop_L1_Echo\` Each emits \`EEcho T v\` (resp. \`EEcho T (ELoc l r)\`) where T is quantified universally; \`preservation_l3\` (slice 4) picks T to match the typing derivation. ## Changes (formal/Semantics.v) \`\`\`coq S_Region_Exit_Echo : forall mu R r v T, is_value v -> In r R -> expr_free_of_region r v -> (mu, R, ERegion r v) -->> (mem_free_region mu r, remove_first r R, EEcho T v) S_Drop_Echo : forall mu R l r T, (mu, R, EDrop (ELoc l r)) -->> (mem_write mu l CFree, R, EEcho T (ELoc l r)) \`\`\` ## Cascade fixes - \`step_from_eregion\`: extended from 3-disjunct classification to **4-disjunct** (Enter / Exit / Exit_Echo / Step). \`Exit_Echo\`'s shape matches \`Exit\`'s except the output is \`exists T, e1 = EEcho T e\`. - \`no_leaks_gen\`: 4th case handled mirroring \`Exit\`. \`EEcho T e\` is a value (VEcho), so multi_step from there can only be reflexive; memory cleanup discharge via \`mem_free_region_clears\` is identical. - \`step_R_change_shape\`: explicit bullet for \`S_Region_Exit_Echo\` — same R-shape as \`S_Region_Exit\` (\`remove_first r R\`, \`In r R\`). ## What is NOT in this slice (still deferred) - \`G\` (echo context) threading through compound rules — **slice 3d** - \`preservation_l3\` — **slice 4** ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree (incl. cascades through \`step_from_eregion\` + \`no_leaks_gen\` + \`step_R_change_shape\`). - Net debt unchanged (3 outer Admitted in \`Semantics_L1.v\`, all pre-existing). ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`formal/Echo.v\` (12 Qed L3 calculus) - Owner directive 2026-05-27 (parallel-rule strategy approved) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new Admitted / Axiom - [x] Legacy \`S_Region_Exit\` + \`S_Drop\` rules untouched (backward-compat) - [ ] CI rust-ci → Coq proofs job passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary The original PROOF-NEEDS.md §2 task \"thread G (echo context) alongside R through compound rules\" was speculative — the design question was whether L3 wiring would need a NEW context parameter on every \`has_type_l1\` constructor. Under the **owner-approved parallel-rules design** landed via slices 3a–3c ([#192](../pull/192), [#193](../pull/193), [#194](../pull/194)): - Echoes are runtime VALUES of type \`TEcho T\` (slice 1 + 3a). - They flow through the EXISTING \`ctx\` G context like any other value — no new context parameter needed. - \`T_Observe_L1\` consumes them like any ordinary expression (slice 2). - The two paths (legacy + echo-aware) coexist via parallel typing/step rules, not via context augmentation (slices 3b + 3c). So the G-threading task is **OBSOLETE**. PROOF-NEEDS.md §2 updated to mark it struck-through with explanation. The L3 wiring sequence proceeds directly from 3c to slice 4 (\`preservation_l3\` capstone). ## No code changes Documentation-only update to PROOF-NEEDS.md §2. ## Refs - PROOF-NEEDS.md §2 (L3 wiring) - PRs #192, #193, #194 for the prerequisite slices that obviated this task - PRESERVATION-DESIGN.md §6.3 (L3 design) ## Test plan - [x] No code changes (docs-only) - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-28T00:49:31Z

🔍 Hypatia Security Scan

Findings: 50 issues detected

Severity	Count
🔴 Critical	9
🟠 High	9
🟡 Medium	32

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in abi-verify.yml",
    "type": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "unknown",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

hyperpolymath enabled auto-merge (squash) May 27, 2026 16:23

hyperpolymath mentioned this pull request May 27, 2026

proof(Semantics_L1): close subst_typing_gen_l1 via m-polymorphic generalisation (L2-β #2) #188

Merged

5 tasks

hyperpolymath mentioned this pull request May 27, 2026

proof(Semantics_L1): restore region_shrink_preserves_typing_l1_gen bullet structure via m-polymorphic helper (L2-β #3) #189

Merged

5 tasks

hyperpolymath and others added 7 commits May 27, 2026 18:54

hyperpolymath disabled auto-merge May 27, 2026 19:23

hyperpolymath merged commit 54006dc into main May 27, 2026
6 of 15 checks passed

hyperpolymath deleted the proof/semantics-l1-affine-bullet-fix branch May 27, 2026 19:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof(Semantics_L1): close 3 Affine-only bullet-structure regressions#187

proof(Semantics_L1): close 3 Affine-only bullet-structure regressions#187
hyperpolymath merged 9 commits into
mainfrom
proof/semantics-l1-affine-bullet-fix

hyperpolymath commented May 27, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 27, 2026

Summary

Closed lemmas

Generalised

Residual admits (L2-β follow-up #2)

Owner-directive compliance

Test plan

Uh oh!

Uh oh!

github-actions Bot commented May 28, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant